49.011/49.011 NO 49.011/49.011 49.011/49.011 Problem 1: 49.011/49.011 49.011/49.011 49.011/49.011 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 49.011/49.011 Confluence Problem: 49.011/49.011 (VAR vNonEmpty:S x:S y:S) 49.011/49.011 (STRATEGY CONTEXTSENSITIVE 49.011/49.011 (f 1 2) 49.011/49.011 (a) 49.011/49.011 (b) 49.011/49.011 (fSNonEmpty) 49.011/49.011 ) 49.011/49.011 (RULES 49.011/49.011 f(x:S,x:S) -> b | f(x:S,x:S) ->* a, x:S ->* a 49.011/49.011 f(y:S,y:S) -> a 49.011/49.011 ) 49.011/49.011 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 49.011/49.011 49.011/49.011 49.011/49.011 Problem 1: 49.011/49.011 49.011/49.011 Inlining of Conditions Processor [STERN17]: 49.011/49.011 49.011/49.011 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 49.011/49.011 Confluence Problem: 49.011/49.011 (VAR vNonEmpty:S x:S y:S) 49.011/49.011 (STRATEGY CONTEXTSENSITIVE 49.011/49.011 (f 1 2) 49.011/49.011 (a) 49.011/49.011 (b) 49.011/49.011 (fSNonEmpty) 49.011/49.011 ) 49.011/49.011 (RULES 49.011/49.011 f(x:S,x:S) -> b | f(x:S,x:S) ->* a, x:S ->* a 49.011/49.011 f(y:S,y:S) -> a 49.011/49.011 ) 49.011/49.011 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 49.011/49.011 49.011/49.011 49.011/49.011 Problem 1: 49.011/49.011 49.011/49.011 Clean CTRS Processor: 49.011/49.011 49.011/49.011 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 49.011/49.011 Confluence Problem: 49.011/49.011 (VAR x:S y:S) 49.011/49.011 (STRATEGY CONTEXTSENSITIVE 49.011/49.011 (f 1 2) 49.011/49.011 (a) 49.011/49.011 (b) 49.011/49.011 (fSNonEmpty) 49.011/49.011 ) 49.011/49.011 (RULES 49.011/49.011 f(x:S,x:S) -> b | f(x:S,x:S) ->* a, x:S ->* a 49.011/49.011 f(y:S,y:S) -> a 49.011/49.011 ) 49.011/49.011 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 49.011/49.011 49.011/49.011 CRule InfChecker Info: 49.011/49.011 f(x:S,x:S) -> b | f(x:S,x:S) ->* a, x:S ->* a 49.011/49.011 Rule remains 49.011/49.011 Proof: 49.011/49.011 NO 49.011/49.011 49.011/49.011 Problem 1: 49.011/49.011 49.011/49.011 Infeasibility Problem: 49.011/49.011 [(VAR vNonEmpty:S vNonEmpty:S:S x:S:S y:S:S) 49.011/49.011 (STRATEGY CONTEXTSENSITIVE 49.011/49.011 (f 1 2) 49.011/49.011 (a) 49.011/49.011 (b) 49.011/49.011 (fSNonEmpty) 49.011/49.011 ) 49.011/49.011 (RULES 49.011/49.011 f(x:S:S,x:S:S) -> b | f(x:S:S,x:S:S) ->* a, x:S:S ->* a 49.011/49.011 f(y:S:S,y:S:S) -> a 49.011/49.011 )] 49.011/49.011 49.011/49.011 Infeasibility Conditions: 49.011/49.011 f(x:S:S,x:S:S) ->* a, x:S:S ->* a 49.011/49.011 49.011/49.011 Problem 1: 49.011/49.011 49.011/49.011 Obtaining a proof using Prover9: 49.011/49.011 49.011/49.011 -> Prover9 Output: 49.011/49.011 ============================== Prover9 =============================== 49.011/49.011 Prover9 (64) version 2009-11A, November 2009. 49.011/49.011 Process 32954 was started by ubuntu on ubuntu, 49.011/49.011 Wed Jul 14 09:46:52 2021 49.011/49.011 The command was "./prover9 -f /tmp/prover932945-0.in". 49.011/49.011 ============================== end of head =========================== 49.011/49.011 49.011/49.011 ============================== INPUT ================================= 49.011/49.011 49.011/49.011 % Reading from file /tmp/prover932945-0.in 49.011/49.011 49.011/49.011 assign(max_seconds,20). 49.011/49.011 49.011/49.011 formulas(assumptions). 49.011/49.011 ->*_s0(x,x) # label(reflexivity). 49.011/49.011 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 49.011/49.011 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence). 49.011/49.011 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence). 49.011/49.011 ->*_s0(f(x2,x2),a) & ->*_s0(x2,a) -> ->_s0(f(x2,x2),b) # label(replacement). 49.011/49.011 ->_s0(f(x3,x3),a) # label(replacement). 49.011/49.011 end_of_list. 49.011/49.011 49.011/49.011 formulas(goals). 49.011/49.011 (exists x2 (->*_s0(f(x2,x2),a) & ->*_s0(x2,a))) # label(goal). 49.011/49.011 end_of_list. 49.011/49.011 49.011/49.011 ============================== end of input ========================== 49.011/49.011 49.011/49.011 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 49.011/49.011 49.011/49.011 % Formulas that are not ordinary clauses: 49.011/49.011 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 49.011/49.011 2 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 49.011/49.011 3 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 49.011/49.011 4 ->*_s0(f(x2,x2),a) & ->*_s0(x2,a) -> ->_s0(f(x2,x2),b) # label(replacement) # label(non_clause). [assumption]. 49.011/49.011 5 (exists x2 (->*_s0(f(x2,x2),a) & ->*_s0(x2,a))) # label(goal) # label(non_clause) # label(goal). [goal]. 49.011/49.011 49.011/49.011 ============================== end of process non-clausal formulas === 49.011/49.011 49.011/49.011 ============================== PROCESS INITIAL CLAUSES =============== 49.011/49.011 49.011/49.011 % Clauses before input processing: 49.011/49.011 49.011/49.011 formulas(usable). 49.011/49.011 end_of_list. 49.011/49.011 49.011/49.011 formulas(sos). 49.011/49.011 ->*_s0(x,x) # label(reflexivity). [assumption]. 49.011/49.011 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 49.011/49.011 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 49.011/49.011 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 49.011/49.011 -->*_s0(f(x,x),a) | -->*_s0(x,a) | ->_s0(f(x,x),b) # label(replacement). [clausify(4)]. 49.011/49.011 ->_s0(f(x,x),a) # label(replacement). [assumption]. 49.011/49.011 -->*_s0(f(x,x),a) | -->*_s0(x,a) # label(goal). [deny(5)]. 49.011/49.011 end_of_list. 49.011/49.011 49.011/49.011 formulas(demodulators). 49.011/49.011 end_of_list. 49.011/49.011 49.011/49.011 ============================== PREDICATE ELIMINATION ================= 49.011/49.011 49.011/49.011 No predicates eliminated. 49.011/49.011 49.011/49.011 ============================== end predicate elimination ============= 49.011/49.011 49.011/49.011 Auto_denials: 49.011/49.011 % copying label goal to answer in negative clause 49.011/49.011 49.011/49.011 Term ordering decisions: 49.011/49.011 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 49.011/49.011 Function symbol precedence: function_order([ a, b, f ]). 49.011/49.011 After inverse_order: (no changes). 49.011/49.011 Unfolding symbols: (none). 49.011/49.011 49.011/49.011 Auto_inference settings: 49.011/49.011 % set(neg_binary_resolution). % (HNE depth_diff=-2) 49.011/49.011 % clear(ordered_res). % (HNE depth_diff=-2) 49.011/49.011 % set(ur_resolution). % (HNE depth_diff=-2) 49.011/49.011 % set(ur_resolution) -> set(pos_ur_resolution). 49.011/49.011 % set(ur_resolution) -> set(neg_ur_resolution). 49.011/49.011 49.011/49.011 Auto_process settings: 49.011/49.011 % set(unit_deletion). % (Horn set with negative nonunits) 49.011/49.011 49.011/49.011 kept: 6 ->*_s0(x,x) # label(reflexivity). [assumption]. 49.011/49.011 kept: 7 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 49.011/49.011 kept: 8 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 49.011/49.011 kept: 9 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 49.011/49.011 kept: 10 -->*_s0(f(x,x),a) | -->*_s0(x,a) | ->_s0(f(x,x),b) # label(replacement). [clausify(4)]. 49.011/49.011 kept: 11 ->_s0(f(x,x),a) # label(replacement). [assumption]. 49.011/49.011 kept: 12 -->*_s0(f(x,x),a) | -->*_s0(x,a) # label(goal) # answer(goal). [deny(5)]. 49.011/49.011 49.011/49.011 ============================== end of process initial clauses ======== 49.011/49.011 49.011/49.011 ============================== CLAUSES FOR SEARCH ==================== 49.011/49.011 49.011/49.011 % Clauses after input processing: 49.011/49.011 49.011/49.011 formulas(usable). 49.011/49.011 end_of_list. 49.011/49.011 49.011/49.011 formulas(sos). 49.011/49.011 6 ->*_s0(x,x) # label(reflexivity). [assumption]. 49.011/49.011 7 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 49.011/49.011 8 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 49.011/49.011 9 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 49.011/49.011 11 ->_s0(f(x,x),a) # label(replacement). [assumption]. 49.011/49.011 12 -->*_s0(f(x,x),a) | -->*_s0(x,a) # label(goal) # answer(goal). [deny(5)]. 49.011/49.011 end_of_list. 49.011/49.011 49.011/49.011 formulas(demodulators). 49.011/49.011 end_of_list. 49.011/49.011 49.011/49.011 ============================== end of clauses for search ============= 49.011/49.011 49.011/49.011 ============================== SEARCH ================================ 49.011/49.011 49.011/49.011 % Starting search at 0.00 seconds. 49.011/49.011 49.011/49.011 given #1 (I,wt=3): 6 ->*_s0(x,x) # label(reflexivity). [assumption]. 49.011/49.011 49.011/49.011 given #2 (I,wt=9): 7 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 49.011/49.011 49.011/49.011 given #3 (I,wt=10): 8 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 49.011/49.011 49.011/49.011 given #4 (I,wt=10): 9 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 49.011/49.011 49.011/49.011 given #5 (I,wt=5): 11 ->_s0(f(x,x),a) # label(replacement). [assumption]. 49.011/49.011 49.011/49.011 ============================== PROOF ================================= 49.011/49.011 49.011/49.011 % Proof 1 at 0.00 (+ 0.00) seconds: goal. 49.011/49.011 % Length of proof is 9. 49.011/49.011 % Level of proof is 4. 49.011/49.011 % Maximum clause weight is 9.000. 49.011/49.011 % Given clauses 5. 49.011/49.011 49.011/49.011 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 49.011/49.011 5 (exists x2 (->*_s0(f(x2,x2),a) & ->*_s0(x2,a))) # label(goal) # label(non_clause) # label(goal). [goal]. 49.011/49.011 6 ->*_s0(x,x) # label(reflexivity). [assumption]. 49.011/49.011 7 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 49.011/49.011 11 ->_s0(f(x,x),a) # label(replacement). [assumption]. 49.011/49.011 12 -->*_s0(f(x,x),a) | -->*_s0(x,a) # label(goal) # answer(goal). [deny(5)]. 49.011/49.011 15 ->*_s0(f(x,x),a). [ur(7,a,11,a,b,6,a)]. 49.011/49.011 16 -->*_s0(x,a) # answer(goal). [back_unit_del(12),unit_del(a,15)]. 49.011/49.011 17 $F # answer(goal). [resolve(16,a,15,a)]. 49.011/49.011 49.011/49.011 ============================== end of proof ========================== 49.011/49.011 49.011/49.011 ============================== STATISTICS ============================ 49.011/49.011 49.011/49.011 Given=5. Generated=11. Kept=11. proofs=1. 49.011/49.011 Usable=5. Sos=2. Demods=0. Limbo=1, Disabled=9. Hints=0. 49.011/49.011 Kept_by_rule=0, Deleted_by_rule=0. 49.011/49.011 Forward_subsumed=0. Back_subsumed=1. 49.011/49.011 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 49.011/49.011 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=1. 49.011/49.011 Demod_attempts=0. Demod_rewrites=0. 49.011/49.011 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 49.011/49.011 Nonunit_fsub_feature_tests=1. Nonunit_bsub_feature_tests=9. 49.011/49.011 Megabytes=0.06. 49.011/49.011 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 49.011/49.011 49.011/49.011 ============================== end of statistics ===================== 49.011/49.011 49.011/49.011 ============================== end of search ========================= 49.011/49.011 49.011/49.011 THEOREM PROVED 49.011/49.011 49.011/49.011 Exiting with 1 proof. 49.011/49.011 49.011/49.011 Process 32954 exit (max_proofs) Wed Jul 14 09:46:52 2021 49.011/49.011 49.011/49.011 49.011/49.011 The problem is feasible. 49.011/49.011 49.011/49.011 49.011/49.011 CRule InfChecker Info: 49.011/49.011 f(y:S,y:S) -> a 49.011/49.011 Rule remains 49.011/49.011 Proof: 49.011/49.011 NO_CONDS 49.011/49.011 49.011/49.011 Problem 1: 49.011/49.011 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 49.011/49.011 Confluence Problem: 49.011/49.011 (VAR x:S y:S) 49.011/49.011 (STRATEGY CONTEXTSENSITIVE 49.011/49.011 (f 1 2) 49.011/49.011 (a) 49.011/49.011 (b) 49.011/49.011 (fSNonEmpty) 49.011/49.011 ) 49.011/49.011 (RULES 49.011/49.011 f(x:S,x:S) -> b | f(x:S,x:S) ->* a, x:S ->* a 49.011/49.011 f(y:S,y:S) -> a 49.011/49.011 ) 49.011/49.011 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 49.011/49.011 49.011/49.011 Critical Pairs Processor: 49.011/49.011 -> Rules: 49.011/49.011 f(x:S,x:S) -> b | f(x:S,x:S) ->* a, x:S ->* a 49.011/49.011 f(y:S,y:S) -> a 49.011/49.011 -> Vars: 49.011/49.011 "x", "y" 49.011/49.011 -> FVars: 49.011/49.011 "x3", "x4" 49.011/49.011 -> PVars: 49.011/49.011 "x": ["x3"], "y": ["x4"] 49.011/49.011 49.011/49.011 -> Rlps: 49.011/49.011 crule: f(x3:S,x3:S) -> b | f(x3:S,x3:S) ->* a, x3:S ->* a, id: 1, possubterms: f(x3:S,x3:S)-> [] 49.011/49.011 crule: f(x4:S,x4:S) -> a, id: 2, possubterms: f(x4:S,x4:S)-> [] 49.011/49.011 49.011/49.011 -> Unifications: 49.011/49.011 R2 unifies with R1 at p: [], l: f(x4:S,x4:S), lp: f(x4:S,x4:S), conds: {f(x:S,x:S) ->* a, x:S ->* a}, sig: {x4:S -> x:S}, l': f(x:S,x:S), r: a, r': b 49.011/49.011 49.011/49.011 -> Critical pairs info: 49.011/49.011 | f(x:S,x:S) ->* a, x:S ->* a => Not trivial, Overlay, N1 49.011/49.011 49.011/49.011 -> Problem conclusions: 49.011/49.011 Not left linear, Right linear, Not linear 49.011/49.011 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 49.011/49.011 CTRS Type: 1 49.011/49.011 Deterministic, Strongly deterministic 49.011/49.011 Oriented CTRS, Properly oriented CTRS, Not join CTRS 49.011/49.011 Maybe right-stable CTRS, Overlay CTRS 49.011/49.011 Maybe normal CTRS, Maybe almost normal CTRS 49.011/49.011 Maybe terminating CTRS, Maybe joinable CCPs 49.011/49.011 Maybe level confluent 49.011/49.011 Maybe confluent 49.011/49.011 49.011/49.011 Problem 1: 49.011/49.011 Clean Infeasible CCPs Processor: 49.011/49.011 Num of CPIs: 1 49.011/49.011 Timeout: 60 49.011/49.011 Timeout for each infeasibility problem: 60 s 49.011/49.011 | f(x:S,x:S) ->* a, x:S ->* a => Not trivial, Overlay, Feasible conditions, N1 49.011/49.011 (PROBLEM INFEASIBILITY) 49.011/49.011 (VAR x y) 49.011/49.011 (RULES 49.011/49.011 f(x,x) -> b | f(x,x) ->* a, x ->* a 49.011/49.011 f(y,y) -> a) 49.011/49.011 (VAR x3) 49.011/49.011 (CONDITION f(x3,x3) ->* a, x3 ->* a) 49.011/49.011 49.011/49.011 Proof: 49.011/49.011 NO 49.011/49.011 49.011/49.011 Problem 1: 49.011/49.011 49.011/49.011 Infeasibility Problem: 49.011/49.011 [(VAR vNonEmpty:S x:S y:S x3:S) 49.011/49.011 (STRATEGY CONTEXTSENSITIVE 49.011/49.011 (f 1 2) 49.011/49.011 (a) 49.011/49.011 (b) 49.011/49.011 (fSNonEmpty) 49.011/49.011 ) 49.011/49.011 (RULES 49.011/49.011 f(x:S,x:S) -> b | f(x:S,x:S) ->* a, x:S ->* a 49.011/49.011 f(y:S,y:S) -> a 49.011/49.011 )] 49.011/49.011 49.011/49.011 Infeasibility Conditions: 49.011/49.011 f(x3:S,x3:S) ->* a, x3:S ->* a 49.011/49.011 49.011/49.011 Problem 1: 49.011/49.011 49.011/49.011 Obtaining a proof using Prover9: 49.011/49.011 49.011/49.011 -> Prover9 Output: 49.011/49.011 ============================== Prover9 =============================== 49.011/49.011 Prover9 (64) version 2009-11A, November 2009. 49.011/49.011 Process 32987 was started by ubuntu on ubuntu, 49.011/49.011 Wed Jul 14 09:46:52 2021 49.011/49.011 The command was "./prover9 -f /tmp/prover932971-0.in". 49.011/49.011 ============================== end of head =========================== 49.011/49.011 49.011/49.011 ============================== INPUT ================================= 49.011/49.011 49.011/49.011 % Reading from file /tmp/prover932971-0.in 49.011/49.011 49.011/49.011 assign(max_seconds,20). 49.011/49.011 49.011/49.011 formulas(assumptions). 49.011/49.011 ->*_s0(x,x) # label(reflexivity). 49.011/49.011 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 49.011/49.011 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence). 49.011/49.011 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence). 49.011/49.011 ->*_s0(f(x1,x1),a) & ->*_s0(x1,a) -> ->_s0(f(x1,x1),b) # label(replacement). 49.011/49.011 ->_s0(f(x2,x2),a) # label(replacement). 49.011/49.011 end_of_list. 49.011/49.011 49.011/49.011 formulas(goals). 49.011/49.011 (exists x3 (->*_s0(f(x3,x3),a) & ->*_s0(x3,a))) # label(goal). 49.011/49.011 end_of_list. 49.011/49.011 49.011/49.011 ============================== end of input ========================== 49.011/49.011 49.011/49.011 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 49.011/49.011 49.011/49.011 % Formulas that are not ordinary clauses: 49.011/49.011 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 49.011/49.011 2 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 49.011/49.011 3 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 49.011/49.011 4 ->*_s0(f(x1,x1),a) & ->*_s0(x1,a) -> ->_s0(f(x1,x1),b) # label(replacement) # label(non_clause). [assumption]. 49.011/49.011 5 (exists x3 (->*_s0(f(x3,x3),a) & ->*_s0(x3,a))) # label(goal) # label(non_clause) # label(goal). [goal]. 49.011/49.011 49.011/49.011 ============================== end of process non-clausal formulas === 49.011/49.011 49.011/49.011 ============================== PROCESS INITIAL CLAUSES =============== 49.011/49.011 49.011/49.011 % Clauses before input processing: 49.011/49.011 49.011/49.011 formulas(usable). 49.011/49.011 end_of_list. 49.011/49.011 49.011/49.011 formulas(sos). 49.011/49.011 ->*_s0(x,x) # label(reflexivity). [assumption]. 49.011/49.011 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 49.011/49.011 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 49.011/49.011 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 49.011/49.011 -->*_s0(f(x,x),a) | -->*_s0(x,a) | ->_s0(f(x,x),b) # label(replacement). [clausify(4)]. 49.011/49.011 ->_s0(f(x,x),a) # label(replacement). [assumption]. 49.011/49.011 -->*_s0(f(x,x),a) | -->*_s0(x,a) # label(goal). [deny(5)]. 49.011/49.011 end_of_list. 49.011/49.011 49.011/49.011 formulas(demodulators). 49.011/49.011 end_of_list. 49.011/49.011 49.011/49.011 ============================== PREDICATE ELIMINATION ================= 49.011/49.011 49.011/49.011 No predicates eliminated. 49.011/49.011 49.011/49.011 ============================== end predicate elimination ============= 49.011/49.011 49.011/49.011 Auto_denials: 49.011/49.011 % copying label goal to answer in negative clause 49.011/49.011 49.011/49.011 Term ordering decisions: 49.011/49.011 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 49.011/49.011 Function symbol precedence: function_order([ a, b, f ]). 49.011/49.011 After inverse_order: (no changes). 49.011/49.011 Unfolding symbols: (none). 49.011/49.011 49.011/49.011 Auto_inference settings: 49.011/49.011 % set(neg_binary_resolution). % (HNE depth_diff=-2) 49.011/49.011 % clear(ordered_res). % (HNE depth_diff=-2) 49.011/49.011 % set(ur_resolution). % (HNE depth_diff=-2) 49.011/49.011 % set(ur_resolution) -> set(pos_ur_resolution). 49.011/49.011 % set(ur_resolution) -> set(neg_ur_resolution). 49.011/49.011 49.011/49.011 Auto_process settings: 49.011/49.011 % set(unit_deletion). % (Horn set with negative nonunits) 49.011/49.011 49.011/49.011 kept: 6 ->*_s0(x,x) # label(reflexivity). [assumption]. 49.011/49.011 kept: 7 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 49.011/49.011 kept: 8 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 49.011/49.011 kept: 9 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 49.011/49.011 kept: 10 -->*_s0(f(x,x),a) | -->*_s0(x,a) | ->_s0(f(x,x),b) # label(replacement). [clausify(4)]. 49.011/49.011 kept: 11 ->_s0(f(x,x),a) # label(replacement). [assumption]. 49.011/49.011 kept: 12 -->*_s0(f(x,x),a) | -->*_s0(x,a) # label(goal) # answer(goal). [deny(5)]. 49.011/49.011 49.011/49.011 ============================== end of process initial clauses ======== 49.011/49.011 49.011/49.011 ============================== CLAUSES FOR SEARCH ==================== 49.011/49.011 49.011/49.011 % Clauses after input processing: 49.011/49.011 49.011/49.011 formulas(usable). 49.011/49.011 end_of_list. 49.011/49.011 49.011/49.011 formulas(sos). 49.011/49.011 6 ->*_s0(x,x) # label(reflexivity). [assumption]. 49.011/49.011 7 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 49.011/49.011 8 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 49.011/49.011 9 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 49.011/49.011 11 ->_s0(f(x,x),a) # label(replacement). [assumption]. 49.011/49.011 12 -->*_s0(f(x,x),a) | -->*_s0(x,a) # label(goal) # answer(goal). [deny(5)]. 49.011/49.011 end_of_list. 49.011/49.011 49.011/49.011 formulas(demodulators). 49.011/49.011 end_of_list. 49.011/49.011 49.011/49.011 ============================== end of clauses for search ============= 49.011/49.011 49.011/49.011 ============================== SEARCH ================================ 49.011/49.011 49.011/49.011 % Starting search at 0.00 seconds. 49.011/49.011 49.011/49.011 given #1 (I,wt=3): 6 ->*_s0(x,x) # label(reflexivity). [assumption]. 49.011/49.011 49.011/49.011 given #2 (I,wt=9): 7 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 49.011/49.011 49.011/49.011 given #3 (I,wt=10): 8 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 49.011/49.011 49.011/49.011 given #4 (I,wt=10): 9 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 49.011/49.011 49.011/49.011 given #5 (I,wt=5): 11 ->_s0(f(x,x),a) # label(replacement). [assumption]. 49.011/49.011 49.011/49.011 ============================== PROOF ================================= 49.011/49.011 49.011/49.011 % Proof 1 at 0.00 (+ 0.00) seconds: goal. 49.011/49.011 % Length of proof is 9. 49.011/49.011 % Level of proof is 4. 49.011/49.011 % Maximum clause weight is 9.000. 49.011/49.011 % Given clauses 5. 49.011/49.011 49.011/49.011 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 49.011/49.011 5 (exists x3 (->*_s0(f(x3,x3),a) & ->*_s0(x3,a))) # label(goal) # label(non_clause) # label(goal). [goal]. 49.011/49.011 6 ->*_s0(x,x) # label(reflexivity). [assumption]. 49.011/49.011 7 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 49.011/49.011 11 ->_s0(f(x,x),a) # label(replacement). [assumption]. 49.011/49.011 12 -->*_s0(f(x,x),a) | -->*_s0(x,a) # label(goal) # answer(goal). [deny(5)]. 49.011/49.011 15 ->*_s0(f(x,x),a). [ur(7,a,11,a,b,6,a)]. 49.011/49.011 16 -->*_s0(x,a) # answer(goal). [back_unit_del(12),unit_del(a,15)]. 49.011/49.011 17 $F # answer(goal). [resolve(16,a,15,a)]. 49.011/49.011 49.011/49.011 ============================== end of proof ========================== 49.011/49.011 49.011/49.011 ============================== STATISTICS ============================ 49.011/49.011 49.011/49.011 Given=5. Generated=11. Kept=11. proofs=1. 49.011/49.011 Usable=5. Sos=2. Demods=0. Limbo=1, Disabled=9. Hints=0. 49.011/49.011 Kept_by_rule=0, Deleted_by_rule=0. 49.011/49.011 Forward_subsumed=0. Back_subsumed=1. 49.011/49.011 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 49.011/49.011 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=1. 49.011/49.011 Demod_attempts=0. Demod_rewrites=0. 49.011/49.011 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 49.011/49.011 Nonunit_fsub_feature_tests=1. Nonunit_bsub_feature_tests=9. 49.011/49.011 Megabytes=0.06. 49.011/49.011 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 49.011/49.011 49.011/49.011 ============================== end of statistics ===================== 49.011/49.011 49.011/49.011 ============================== end of search ========================= 49.011/49.011 49.011/49.011 THEOREM PROVED 49.011/49.011 49.011/49.011 Exiting with 1 proof. 49.011/49.011 49.011/49.011 Process 32987 exit (max_proofs) Wed Jul 14 09:46:52 2021 49.011/49.011 49.011/49.011 49.011/49.011 The problem is feasible. 49.011/49.011 49.011/49.011 49.011/49.011 49.011/49.011 49.011/49.011 -> Problem conclusions: 49.011/49.011 Not left linear, Right linear, Not linear 49.011/49.011 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 49.011/49.011 CTRS Type: 1 49.011/49.011 Deterministic, Strongly deterministic 49.011/49.011 Oriented CTRS, Properly oriented CTRS, Not join CTRS 49.011/49.011 Maybe right-stable CTRS, Overlay CTRS 49.011/49.011 Maybe normal CTRS, Maybe almost normal CTRS 49.011/49.011 Maybe terminating CTRS, Maybe joinable CCPs 49.011/49.011 Maybe level confluent 49.011/49.011 Maybe confluent 49.011/49.011 49.011/49.011 Resulting CCPs: 49.011/49.011 | f(x:S,x:S) ->* a, x:S ->* a => Not trivial, Overlay, Feasible conditions, N1 49.011/49.011 49.011/49.011 Problem 1: 49.011/49.011 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 49.011/49.011 Confluence Problem: 49.011/49.011 (VAR x:S y:S) 49.011/49.011 (STRATEGY CONTEXTSENSITIVE 49.011/49.011 (f 1 2) 49.011/49.011 (a) 49.011/49.011 (b) 49.011/49.011 (fSNonEmpty) 49.011/49.011 ) 49.011/49.011 (RULES 49.011/49.011 f(x:S,x:S) -> b | f(x:S,x:S) ->* a, x:S ->* a 49.011/49.011 f(y:S,y:S) -> a 49.011/49.011 ) 49.011/49.011 Critical Pairs: 49.011/49.011 | f(x:S,x:S) ->* a, x:S ->* a => Not trivial, Overlay, Feasible conditions, N1 49.011/49.011 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 49.011/49.011 49.011/49.011 Conditional Critical Pairs Distributor Processor 49.011/49.011 49.011/49.011 Problem 1: 49.011/49.011 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 49.011/49.011 Confluence Problem: 49.011/49.011 (VAR x:S y:S) 49.011/49.011 (STRATEGY CONTEXTSENSITIVE 49.011/49.011 (f 1 2) 49.011/49.011 (a) 49.011/49.011 (b) 49.011/49.011 (fSNonEmpty) 49.011/49.011 ) 49.011/49.011 (RULES 49.011/49.011 f(x:S,x:S) -> b | f(x:S,x:S) ->* a, x:S ->* a 49.011/49.011 f(y:S,y:S) -> a 49.011/49.011 ) 49.011/49.011 Critical Pairs: 49.011/49.011 | f(x:S,x:S) ->* a, x:S ->* a => Not trivial, Overlay, Feasible conditions, N1 49.011/49.011 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 49.011/49.011 49.011/49.011 Infeasible Convergence CCP Processor: 49.011/49.011 Infeasible convergence? 49.011/49.011 YES 49.011/49.011 49.011/49.011 Problem 1: 49.011/49.011 49.011/49.011 Infeasibility Problem: 49.011/49.011 [(VAR vNonEmpty:S x:S y:S z:S) 49.011/49.011 (STRATEGY CONTEXTSENSITIVE 49.011/49.011 (f 1 2) 49.011/49.011 (a) 49.011/49.011 (b) 49.011/49.011 (fSNonEmpty) 49.011/49.011 ) 49.011/49.011 (RULES 49.011/49.011 f(x:S,x:S) -> b | f(x:S,x:S) ->* a, x:S ->* a 49.011/49.011 f(y:S,y:S) -> a 49.011/49.011 )] 49.011/49.011 49.011/49.011 Infeasibility Conditions: 49.011/49.011 b ->* z:S, a ->* z:S 49.011/49.011 49.011/49.011 Problem 1: 49.011/49.011 49.011/49.011 Obtaining a model using Mace4: 49.011/49.011 49.011/49.011 -> Usable Rules: 49.011/49.011 Empty 49.011/49.011 49.011/49.011 -> Mace4 Output: 49.011/49.011 ============================== Mace4 ================================= 49.011/49.011 Mace4 (64) version 2009-11A, November 2009. 49.011/49.011 Process 33094 was started by ubuntu on ubuntu, 49.011/49.011 Wed Jul 14 09:47:16 2021 49.011/49.011 The command was "./mace4 -c -f /tmp/mace433034-2.in". 49.011/49.011 ============================== end of head =========================== 49.011/49.011 49.011/49.011 ============================== INPUT ================================= 49.011/49.011 49.011/49.011 % Reading from file /tmp/mace433034-2.in 49.011/49.011 49.011/49.011 assign(max_seconds,20). 49.011/49.011 49.011/49.011 formulas(assumptions). 49.011/49.011 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence). 49.011/49.011 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence). 49.011/49.011 ->*(x,x) # label(reflexivity). 49.011/49.011 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 49.011/49.011 end_of_list. 49.011/49.011 49.011/49.011 formulas(goals). 49.011/49.011 (exists x3 (->*(b,x3) & ->*(a,x3))) # label(goal). 49.011/49.011 end_of_list. 49.011/49.011 49.011/49.011 ============================== end of input ========================== 49.011/49.011 49.011/49.011 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 49.011/49.011 49.011/49.011 % Formulas that are not ordinary clauses: 49.011/49.011 1 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 49.011/49.011 2 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 49.011/49.011 3 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 49.011/49.011 4 (exists x3 (->*(b,x3) & ->*(a,x3))) # label(goal) # label(non_clause) # label(goal). [goal]. 49.011/49.011 49.011/49.011 ============================== end of process non-clausal formulas === 49.011/49.011 49.011/49.011 ============================== CLAUSES FOR SEARCH ==================== 49.011/49.011 49.011/49.011 formulas(mace4_clauses). 49.011/49.011 -->(x,y) | ->(f(x,z),f(y,z)) # label(congruence). 49.011/49.011 -->(x,y) | ->(f(z,x),f(z,y)) # label(congruence). 49.011/49.011 ->*(x,x) # label(reflexivity). 49.011/49.011 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 49.011/49.011 -->*(b,x) | -->*(a,x) # label(goal). 49.011/49.011 end_of_list. 49.011/49.011 49.011/49.011 ============================== end of clauses for search ============= 49.011/49.011 49.011/49.011 % There are no natural numbers in the input. 49.011/49.011 49.011/49.011 ============================== DOMAIN SIZE 2 ========================= 49.011/49.011 49.011/49.011 ============================== MODEL ================================= 49.011/49.011 49.011/49.011 interpretation( 2, [number=1, seconds=0], [ 49.011/49.011 49.011/49.011 function(a, [ 0 ]), 49.011/49.011 49.011/49.011 function(b, [ 1 ]), 49.011/49.011 49.011/49.011 function(f(_,_), [ 49.011/49.011 0, 0, 49.011/49.011 0, 0 ]), 49.011/49.011 49.011/49.011 relation(->*(_,_), [ 49.011/49.011 1, 0, 49.011/49.011 0, 1 ]), 49.011/49.011 49.011/49.011 relation(->(_,_), [ 49.011/49.011 0, 0, 49.011/49.011 0, 0 ]) 49.011/49.011 ]). 49.011/49.011 49.011/49.011 ============================== end of model ========================== 49.011/49.011 49.011/49.011 ============================== STATISTICS ============================ 49.011/49.011 49.011/49.011 For domain size 2. 49.011/49.011 49.011/49.011 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 49.011/49.011 Ground clauses: seen=28, kept=24. 49.011/49.011 Selections=6, assignments=6, propagations=8, current_models=1. 49.011/49.011 Rewrite_terms=36, rewrite_bools=33, indexes=4. 49.011/49.011 Rules_from_neg_clauses=1, cross_offs=1. 49.011/49.011 49.011/49.011 ============================== end of statistics ===================== 49.011/49.011 49.011/49.011 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 49.011/49.011 49.011/49.011 Exiting with 1 model. 49.011/49.011 49.011/49.011 Process 33094 exit (max_models) Wed Jul 14 09:47:16 2021 49.011/49.011 The process finished Wed Jul 14 09:47:16 2021 49.011/49.011 49.011/49.011 49.011/49.011 Mace4 cooked interpretation: 49.011/49.011 49.011/49.011 49.011/49.011 49.011/49.011 The problem is infeasible. 49.011/49.011 49.011/49.011 49.011/49.011 The problem is not joinable. 49.011/49.011 73.56user 4.64system 0:49.11elapsed 159%CPU (0avgtext+0avgdata 5730208maxresident)k 49.011/49.011 12inputs+0outputs (0major+1726587minor)pagefaults 0swaps