82.05/82.05 YES 82.05/82.05 82.05/82.05 Problem 1: 82.05/82.05 82.05/82.05 82.05/82.05 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.05/82.05 Confluence Problem: 82.05/82.05 (VAR vNonEmpty:S x:S y:S) 82.05/82.05 (STRATEGY CONTEXTSENSITIVE 82.05/82.05 (b) 82.05/82.05 (f 1 2) 82.05/82.05 (g 1) 82.05/82.05 (h 1) 82.05/82.05 (a) 82.05/82.05 (c 1) 82.05/82.05 (fSNonEmpty) 82.05/82.05 (s 1) 82.05/82.05 ) 82.05/82.05 (RULES 82.05/82.05 b -> b 82.05/82.05 f(x:S,y:S) -> g(s(x:S)) | c(g(x:S)) ->* c(a) 82.05/82.05 f(x:S,y:S) -> h(s(x:S)) | c(h(x:S)) ->* c(a) 82.05/82.05 g(s(x:S)) -> x:S 82.05/82.05 h(s(x:S)) -> x:S 82.05/82.05 ) 82.05/82.05 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.05/82.05 82.05/82.05 82.05/82.05 Problem 1: 82.05/82.05 82.05/82.05 Inlining of Conditions Processor [STERN17]: 82.05/82.05 82.05/82.05 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.05/82.05 Confluence Problem: 82.05/82.05 (VAR vNonEmpty:S x:S y:S) 82.05/82.05 (STRATEGY CONTEXTSENSITIVE 82.05/82.05 (b) 82.05/82.05 (f 1 2) 82.05/82.05 (g 1) 82.05/82.05 (h 1) 82.05/82.05 (a) 82.05/82.05 (c 1) 82.05/82.05 (fSNonEmpty) 82.05/82.05 (s 1) 82.05/82.05 ) 82.05/82.05 (RULES 82.05/82.05 b -> b 82.05/82.05 f(x:S,y:S) -> g(s(x:S)) | c(g(x:S)) ->* c(a) 82.05/82.05 f(x:S,y:S) -> h(s(x:S)) | c(h(x:S)) ->* c(a) 82.05/82.05 g(s(x:S)) -> x:S 82.05/82.05 h(s(x:S)) -> x:S 82.05/82.05 ) 82.05/82.05 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.05/82.05 82.05/82.05 82.05/82.05 Problem 1: 82.05/82.05 82.05/82.05 Clean CTRS Processor: 82.05/82.05 82.05/82.05 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.05/82.05 Confluence Problem: 82.05/82.05 (VAR x:S y:S) 82.05/82.05 (STRATEGY CONTEXTSENSITIVE 82.05/82.05 (b) 82.05/82.05 (f 1 2) 82.05/82.05 (g 1) 82.05/82.05 (h 1) 82.05/82.05 (a) 82.05/82.05 (c 1) 82.05/82.05 (fSNonEmpty) 82.05/82.05 (s 1) 82.05/82.05 ) 82.05/82.05 (RULES 82.05/82.05 f(x:S,y:S) -> g(s(x:S)) | c(g(x:S)) ->* c(a) 82.05/82.05 f(x:S,y:S) -> h(s(x:S)) | c(h(x:S)) ->* c(a) 82.05/82.05 g(s(x:S)) -> x:S 82.05/82.05 h(s(x:S)) -> x:S 82.05/82.05 ) 82.05/82.05 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.05/82.05 82.05/82.05 CRule InfChecker Info: 82.05/82.05 b -> b 82.05/82.05 Rule deleted 82.05/82.05 Proof: 82.05/82.05 SAME_LHS_AND_RHS 82.05/82.05 82.05/82.05 CRule InfChecker Info: 82.05/82.05 f(x:S,y:S) -> g(s(x:S)) | c(g(x:S)) ->* c(a) 82.05/82.05 Rule remains 82.05/82.05 Proof: 82.05/82.05 NO 82.05/82.05 82.05/82.05 Problem 1: 82.05/82.05 82.05/82.05 Infeasibility Problem: 82.05/82.05 [(VAR vNonEmpty:S x:S:S y:S:S) 82.05/82.05 (STRATEGY CONTEXTSENSITIVE 82.05/82.05 (f 1 2) 82.05/82.05 (g 1) 82.05/82.05 (h 1) 82.05/82.05 (a) 82.05/82.05 (c 1) 82.05/82.05 (fSNonEmpty) 82.05/82.05 (s 1) 82.05/82.05 ) 82.05/82.05 (RULES 82.05/82.05 f(x:S:S,y:S:S) -> g(s(x:S:S)) | c(g(x:S:S)) ->* c(a) 82.05/82.05 f(x:S:S,y:S:S) -> h(s(x:S:S)) | c(h(x:S:S)) ->* c(a) 82.05/82.05 g(s(x:S:S)) -> x:S:S 82.05/82.05 h(s(x:S:S)) -> x:S:S 82.05/82.05 )] 82.05/82.05 82.05/82.05 Infeasibility Conditions: 82.05/82.05 c(g(x:S:S)) ->* c(a) 82.05/82.05 82.05/82.05 Problem 1: 82.05/82.05 82.05/82.05 Obtaining a proof using Prover9: 82.05/82.05 82.05/82.05 -> Prover9 Output: 82.05/82.05 ============================== Prover9 =============================== 82.05/82.05 Prover9 (64) version 2009-11A, November 2009. 82.05/82.05 Process 54652 was started by ubuntu on ubuntu, 82.05/82.05 Wed Jul 14 11:13:08 2021 82.05/82.05 The command was "./prover9 -f /tmp/prover954643-0.in". 82.05/82.05 ============================== end of head =========================== 82.05/82.05 82.05/82.05 ============================== INPUT ================================= 82.05/82.05 82.05/82.05 % Reading from file /tmp/prover954643-0.in 82.05/82.05 82.05/82.05 assign(max_seconds,20). 82.05/82.05 82.05/82.05 formulas(assumptions). 82.05/82.05 ->*_s0(x,x) # label(reflexivity). 82.05/82.05 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 82.05/82.05 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence). 82.05/82.05 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence). 82.05/82.05 ->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence). 82.05/82.05 ->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence). 82.05/82.05 ->_s0(x1,y) -> ->_s0(c(x1),c(y)) # label(congruence). 82.05/82.05 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence). 82.05/82.05 ->*_s0(c(g(x1)),c(a)) -> ->_s0(f(x1,x2),g(s(x1))) # label(replacement). 82.05/82.05 ->*_s0(c(h(x1)),c(a)) -> ->_s0(f(x1,x2),h(s(x1))) # label(replacement). 82.05/82.05 ->_s0(g(s(x1)),x1) # label(replacement). 82.05/82.05 ->_s0(h(s(x1)),x1) # label(replacement). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 formulas(goals). 82.05/82.05 (exists x1 ->*_s0(c(g(x1)),c(a))) # label(goal). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 ============================== end of input ========================== 82.05/82.05 82.05/82.05 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 82.05/82.05 82.05/82.05 % Formulas that are not ordinary clauses: 82.05/82.05 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 82.05/82.05 2 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 3 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 4 ->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 5 ->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 6 ->_s0(x1,y) -> ->_s0(c(x1),c(y)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 7 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 8 ->*_s0(c(g(x1)),c(a)) -> ->_s0(f(x1,x2),g(s(x1))) # label(replacement) # label(non_clause). [assumption]. 82.05/82.05 9 ->*_s0(c(h(x1)),c(a)) -> ->_s0(f(x1,x2),h(s(x1))) # label(replacement) # label(non_clause). [assumption]. 82.05/82.05 10 (exists x1 ->*_s0(c(g(x1)),c(a))) # label(goal) # label(non_clause) # label(goal). [goal]. 82.05/82.05 82.05/82.05 ============================== end of process non-clausal formulas === 82.05/82.05 82.05/82.05 ============================== PROCESS INITIAL CLAUSES =============== 82.05/82.05 82.05/82.05 % Clauses before input processing: 82.05/82.05 82.05/82.05 formulas(usable). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 formulas(sos). 82.05/82.05 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.05/82.05 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.05/82.05 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 82.05/82.05 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 82.05/82.05 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 82.05/82.05 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 82.05/82.05 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.05/82.05 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(7)]. 82.05/82.05 -->*_s0(c(g(x)),c(a)) | ->_s0(f(x,y),g(s(x))) # label(replacement). [clausify(8)]. 82.05/82.05 -->*_s0(c(h(x)),c(a)) | ->_s0(f(x,y),h(s(x))) # label(replacement). [clausify(9)]. 82.05/82.05 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 -->*_s0(c(g(x)),c(a)) # label(goal). [deny(10)]. 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 formulas(demodulators). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 ============================== PREDICATE ELIMINATION ================= 82.05/82.05 82.05/82.05 No predicates eliminated. 82.05/82.05 82.05/82.05 ============================== end predicate elimination ============= 82.05/82.05 82.05/82.05 Auto_denials: 82.05/82.05 % copying label goal to answer in negative clause 82.05/82.05 82.05/82.05 Term ordering decisions: 82.05/82.05 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 82.05/82.05 Function symbol precedence: function_order([ a, f, c, s, g, h ]). 82.05/82.05 After inverse_order: (no changes). 82.05/82.05 Unfolding symbols: (none). 82.05/82.05 82.05/82.05 Auto_inference settings: 82.05/82.05 % set(neg_binary_resolution). % (HNE depth_diff=-6) 82.05/82.05 % clear(ordered_res). % (HNE depth_diff=-6) 82.05/82.05 % set(ur_resolution). % (HNE depth_diff=-6) 82.05/82.05 % set(ur_resolution) -> set(pos_ur_resolution). 82.05/82.05 % set(ur_resolution) -> set(neg_ur_resolution). 82.05/82.05 82.05/82.05 Auto_process settings: (no changes). 82.05/82.05 82.05/82.05 kept: 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.05/82.05 kept: 12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.05/82.05 kept: 13 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 82.05/82.05 kept: 14 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 82.05/82.05 kept: 15 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 82.05/82.05 kept: 16 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 82.05/82.05 kept: 17 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.05/82.05 kept: 18 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(7)]. 82.05/82.05 kept: 19 -->*_s0(c(g(x)),c(a)) | ->_s0(f(x,y),g(s(x))) # label(replacement). [clausify(8)]. 82.05/82.05 kept: 20 -->*_s0(c(h(x)),c(a)) | ->_s0(f(x,y),h(s(x))) # label(replacement). [clausify(9)]. 82.05/82.05 kept: 21 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 kept: 22 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 kept: 23 -->*_s0(c(g(x)),c(a)) # label(goal) # answer(goal). [deny(10)]. 82.05/82.05 82.05/82.05 ============================== end of process initial clauses ======== 82.05/82.05 82.05/82.05 ============================== CLAUSES FOR SEARCH ==================== 82.05/82.05 82.05/82.05 % Clauses after input processing: 82.05/82.05 82.05/82.05 formulas(usable). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 formulas(sos). 82.05/82.05 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.05/82.05 12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.05/82.05 13 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 82.05/82.05 14 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 82.05/82.05 15 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 82.05/82.05 16 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 82.05/82.05 17 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.05/82.05 18 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(7)]. 82.05/82.05 20 -->*_s0(c(h(x)),c(a)) | ->_s0(f(x,y),h(s(x))) # label(replacement). [clausify(9)]. 82.05/82.05 21 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 22 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 23 -->*_s0(c(g(x)),c(a)) # label(goal) # answer(goal). [deny(10)]. 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 formulas(demodulators). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 ============================== end of clauses for search ============= 82.05/82.05 82.05/82.05 ============================== SEARCH ================================ 82.05/82.05 82.05/82.05 % Starting search at 0.00 seconds. 82.05/82.05 82.05/82.05 given #1 (I,wt=3): 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.05/82.05 82.05/82.05 given #2 (I,wt=9): 12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.05/82.05 82.05/82.05 given #3 (I,wt=10): 13 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 82.05/82.05 82.05/82.05 given #4 (I,wt=10): 14 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 82.05/82.05 82.05/82.05 given #5 (I,wt=8): 15 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 82.05/82.05 82.05/82.05 given #6 (I,wt=8): 16 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 82.05/82.05 82.05/82.05 given #7 (I,wt=8): 17 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.05/82.05 82.05/82.05 given #8 (I,wt=8): 18 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(7)]. 82.05/82.05 82.05/82.05 given #9 (I,wt=13): 20 -->*_s0(c(h(x)),c(a)) | ->_s0(f(x,y),h(s(x))) # label(replacement). [clausify(9)]. 82.05/82.05 82.05/82.05 given #10 (I,wt=5): 21 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 82.05/82.05 given #11 (I,wt=5): 22 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 82.05/82.05 given #12 (I,wt=6): 23 -->*_s0(c(g(x)),c(a)) # label(goal) # answer(goal). [deny(10)]. 82.05/82.05 82.05/82.05 ============================== PROOF ================================= 82.05/82.05 82.05/82.05 % Proof 1 at 0.00 (+ 0.00) seconds: goal. 82.05/82.05 % Length of proof is 11. 82.05/82.05 % Level of proof is 3. 82.05/82.05 % Maximum clause weight is 9.000. 82.05/82.05 % Given clauses 12. 82.05/82.05 82.05/82.05 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 82.05/82.05 6 ->_s0(x1,y) -> ->_s0(c(x1),c(y)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 10 (exists x1 ->*_s0(c(g(x1)),c(a))) # label(goal) # label(non_clause) # label(goal). [goal]. 82.05/82.05 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.05/82.05 12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.05/82.05 17 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.05/82.05 21 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 23 -->*_s0(c(g(x)),c(a)) # label(goal) # answer(goal). [deny(10)]. 82.05/82.05 25 ->_s0(c(g(s(x))),c(x)). [ur(17,a,21,a)]. 82.05/82.05 39 -->_s0(c(g(x)),c(a)) # answer(goal). [ur(12,b,11,a,c,23,a)]. 82.05/82.05 40 $F # answer(goal). [resolve(39,a,25,a)]. 82.05/82.05 82.05/82.05 ============================== end of proof ========================== 82.05/82.05 82.05/82.05 ============================== STATISTICS ============================ 82.05/82.05 82.05/82.05 Given=12. Generated=29. Kept=29. proofs=1. 82.05/82.05 Usable=12. Sos=14. Demods=0. Limbo=1, Disabled=14. Hints=0. 82.05/82.05 Kept_by_rule=0, Deleted_by_rule=0. 82.05/82.05 Forward_subsumed=0. Back_subsumed=1. 82.05/82.05 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 82.05/82.05 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 82.05/82.05 Demod_attempts=0. Demod_rewrites=0. 82.05/82.05 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 82.05/82.05 Nonunit_fsub_feature_tests=1. Nonunit_bsub_feature_tests=15. 82.05/82.05 Megabytes=0.09. 82.05/82.05 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 82.05/82.05 82.05/82.05 ============================== end of statistics ===================== 82.05/82.05 82.05/82.05 ============================== end of search ========================= 82.05/82.05 82.05/82.05 THEOREM PROVED 82.05/82.05 82.05/82.05 Exiting with 1 proof. 82.05/82.05 82.05/82.05 Process 54652 exit (max_proofs) Wed Jul 14 11:13:08 2021 82.05/82.05 82.05/82.05 82.05/82.05 The problem is feasible. 82.05/82.05 82.05/82.05 82.05/82.05 CRule InfChecker Info: 82.05/82.05 f(x:S,y:S) -> h(s(x:S)) | c(h(x:S)) ->* c(a) 82.05/82.05 Rule remains 82.05/82.05 Proof: 82.05/82.05 NO 82.05/82.05 82.05/82.05 Problem 1: 82.05/82.05 82.05/82.05 Infeasibility Problem: 82.05/82.05 [(VAR vNonEmpty:S x:S:S y:S:S) 82.05/82.05 (STRATEGY CONTEXTSENSITIVE 82.05/82.05 (f 1 2) 82.05/82.05 (g 1) 82.05/82.05 (h 1) 82.05/82.05 (a) 82.05/82.05 (c 1) 82.05/82.05 (fSNonEmpty) 82.05/82.05 (s 1) 82.05/82.05 ) 82.05/82.05 (RULES 82.05/82.05 f(x:S:S,y:S:S) -> g(s(x:S:S)) | c(g(x:S:S)) ->* c(a) 82.05/82.05 f(x:S:S,y:S:S) -> h(s(x:S:S)) | c(h(x:S:S)) ->* c(a) 82.05/82.05 g(s(x:S:S)) -> x:S:S 82.05/82.05 h(s(x:S:S)) -> x:S:S 82.05/82.05 )] 82.05/82.05 82.05/82.05 Infeasibility Conditions: 82.05/82.05 c(h(x:S:S)) ->* c(a) 82.05/82.05 82.05/82.05 Problem 1: 82.05/82.05 82.05/82.05 Obtaining a proof using Prover9: 82.05/82.05 82.05/82.05 -> Prover9 Output: 82.05/82.05 ============================== Prover9 =============================== 82.05/82.05 Prover9 (64) version 2009-11A, November 2009. 82.05/82.05 Process 54674 was started by ubuntu on ubuntu, 82.05/82.05 Wed Jul 14 11:13:08 2021 82.05/82.05 The command was "./prover9 -f /tmp/prover954665-0.in". 82.05/82.05 ============================== end of head =========================== 82.05/82.05 82.05/82.05 ============================== INPUT ================================= 82.05/82.05 82.05/82.05 % Reading from file /tmp/prover954665-0.in 82.05/82.05 82.05/82.05 assign(max_seconds,20). 82.05/82.05 82.05/82.05 formulas(assumptions). 82.05/82.05 ->*_s0(x,x) # label(reflexivity). 82.05/82.05 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 82.05/82.05 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence). 82.05/82.05 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence). 82.05/82.05 ->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence). 82.05/82.05 ->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence). 82.05/82.05 ->_s0(x1,y) -> ->_s0(c(x1),c(y)) # label(congruence). 82.05/82.05 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence). 82.05/82.05 ->*_s0(c(g(x1)),c(a)) -> ->_s0(f(x1,x2),g(s(x1))) # label(replacement). 82.05/82.05 ->*_s0(c(h(x1)),c(a)) -> ->_s0(f(x1,x2),h(s(x1))) # label(replacement). 82.05/82.05 ->_s0(g(s(x1)),x1) # label(replacement). 82.05/82.05 ->_s0(h(s(x1)),x1) # label(replacement). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 formulas(goals). 82.05/82.05 (exists x1 ->*_s0(c(h(x1)),c(a))) # label(goal). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 ============================== end of input ========================== 82.05/82.05 82.05/82.05 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 82.05/82.05 82.05/82.05 % Formulas that are not ordinary clauses: 82.05/82.05 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 82.05/82.05 2 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 3 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 4 ->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 5 ->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 6 ->_s0(x1,y) -> ->_s0(c(x1),c(y)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 7 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 8 ->*_s0(c(g(x1)),c(a)) -> ->_s0(f(x1,x2),g(s(x1))) # label(replacement) # label(non_clause). [assumption]. 82.05/82.05 9 ->*_s0(c(h(x1)),c(a)) -> ->_s0(f(x1,x2),h(s(x1))) # label(replacement) # label(non_clause). [assumption]. 82.05/82.05 10 (exists x1 ->*_s0(c(h(x1)),c(a))) # label(goal) # label(non_clause) # label(goal). [goal]. 82.05/82.05 82.05/82.05 ============================== end of process non-clausal formulas === 82.05/82.05 82.05/82.05 ============================== PROCESS INITIAL CLAUSES =============== 82.05/82.05 82.05/82.05 % Clauses before input processing: 82.05/82.05 82.05/82.05 formulas(usable). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 formulas(sos). 82.05/82.05 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.05/82.05 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.05/82.05 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 82.05/82.05 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 82.05/82.05 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 82.05/82.05 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 82.05/82.05 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.05/82.05 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(7)]. 82.05/82.05 -->*_s0(c(g(x)),c(a)) | ->_s0(f(x,y),g(s(x))) # label(replacement). [clausify(8)]. 82.05/82.05 -->*_s0(c(h(x)),c(a)) | ->_s0(f(x,y),h(s(x))) # label(replacement). [clausify(9)]. 82.05/82.05 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 -->*_s0(c(h(x)),c(a)) # label(goal). [deny(10)]. 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 formulas(demodulators). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 ============================== PREDICATE ELIMINATION ================= 82.05/82.05 82.05/82.05 No predicates eliminated. 82.05/82.05 82.05/82.05 ============================== end predicate elimination ============= 82.05/82.05 82.05/82.05 Auto_denials: 82.05/82.05 % copying label goal to answer in negative clause 82.05/82.05 82.05/82.05 Term ordering decisions: 82.05/82.05 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 82.05/82.05 Function symbol precedence: function_order([ a, f, c, s, g, h ]). 82.05/82.05 After inverse_order: (no changes). 82.05/82.05 Unfolding symbols: (none). 82.05/82.05 82.05/82.05 Auto_inference settings: 82.05/82.05 % set(neg_binary_resolution). % (HNE depth_diff=-6) 82.05/82.05 % clear(ordered_res). % (HNE depth_diff=-6) 82.05/82.05 % set(ur_resolution). % (HNE depth_diff=-6) 82.05/82.05 % set(ur_resolution) -> set(pos_ur_resolution). 82.05/82.05 % set(ur_resolution) -> set(neg_ur_resolution). 82.05/82.05 82.05/82.05 Auto_process settings: (no changes). 82.05/82.05 82.05/82.05 kept: 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.05/82.05 kept: 12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.05/82.05 kept: 13 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 82.05/82.05 kept: 14 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 82.05/82.05 kept: 15 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 82.05/82.05 kept: 16 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 82.05/82.05 kept: 17 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.05/82.05 kept: 18 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(7)]. 82.05/82.05 kept: 19 -->*_s0(c(g(x)),c(a)) | ->_s0(f(x,y),g(s(x))) # label(replacement). [clausify(8)]. 82.05/82.05 kept: 20 -->*_s0(c(h(x)),c(a)) | ->_s0(f(x,y),h(s(x))) # label(replacement). [clausify(9)]. 82.05/82.05 kept: 21 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 kept: 22 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 kept: 23 -->*_s0(c(h(x)),c(a)) # label(goal) # answer(goal). [deny(10)]. 82.05/82.05 82.05/82.05 ============================== end of process initial clauses ======== 82.05/82.05 82.05/82.05 ============================== CLAUSES FOR SEARCH ==================== 82.05/82.05 82.05/82.05 % Clauses after input processing: 82.05/82.05 82.05/82.05 formulas(usable). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 formulas(sos). 82.05/82.05 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.05/82.05 12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.05/82.05 13 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 82.05/82.05 14 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 82.05/82.05 15 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 82.05/82.05 16 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 82.05/82.05 17 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.05/82.05 18 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(7)]. 82.05/82.05 19 -->*_s0(c(g(x)),c(a)) | ->_s0(f(x,y),g(s(x))) # label(replacement). [clausify(8)]. 82.05/82.05 21 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 22 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 23 -->*_s0(c(h(x)),c(a)) # label(goal) # answer(goal). [deny(10)]. 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 formulas(demodulators). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 ============================== end of clauses for search ============= 82.05/82.05 82.05/82.05 ============================== SEARCH ================================ 82.05/82.05 82.05/82.05 % Starting search at 0.00 seconds. 82.05/82.05 82.05/82.05 given #1 (I,wt=3): 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.05/82.05 82.05/82.05 given #2 (I,wt=9): 12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.05/82.05 82.05/82.05 given #3 (I,wt=10): 13 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 82.05/82.05 82.05/82.05 given #4 (I,wt=10): 14 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 82.05/82.05 82.05/82.05 given #5 (I,wt=8): 15 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 82.05/82.05 82.05/82.05 given #6 (I,wt=8): 16 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 82.05/82.05 82.05/82.05 given #7 (I,wt=8): 17 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.05/82.05 82.05/82.05 given #8 (I,wt=8): 18 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(7)]. 82.05/82.05 82.05/82.05 given #9 (I,wt=13): 19 -->*_s0(c(g(x)),c(a)) | ->_s0(f(x,y),g(s(x))) # label(replacement). [clausify(8)]. 82.05/82.05 82.05/82.05 given #10 (I,wt=5): 21 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 82.05/82.05 given #11 (I,wt=5): 22 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 82.05/82.05 given #12 (I,wt=6): 23 -->*_s0(c(h(x)),c(a)) # label(goal) # answer(goal). [deny(10)]. 82.05/82.05 82.05/82.05 ============================== PROOF ================================= 82.05/82.05 82.05/82.05 % Proof 1 at 0.00 (+ 0.00) seconds: goal. 82.05/82.05 % Length of proof is 11. 82.05/82.05 % Level of proof is 3. 82.05/82.05 % Maximum clause weight is 9.000. 82.05/82.05 % Given clauses 12. 82.05/82.05 82.05/82.05 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 82.05/82.05 6 ->_s0(x1,y) -> ->_s0(c(x1),c(y)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 10 (exists x1 ->*_s0(c(h(x1)),c(a))) # label(goal) # label(non_clause) # label(goal). [goal]. 82.05/82.05 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.05/82.05 12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.05/82.05 17 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.05/82.05 22 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 23 -->*_s0(c(h(x)),c(a)) # label(goal) # answer(goal). [deny(10)]. 82.05/82.05 32 ->_s0(c(h(s(x))),c(x)). [ur(17,a,22,a)]. 82.05/82.05 39 -->_s0(c(h(x)),c(a)) # answer(goal). [ur(12,b,11,a,c,23,a)]. 82.05/82.05 40 $F # answer(goal). [resolve(39,a,32,a)]. 82.05/82.05 82.05/82.05 ============================== end of proof ========================== 82.05/82.05 82.05/82.05 ============================== STATISTICS ============================ 82.05/82.05 82.05/82.05 Given=12. Generated=29. Kept=29. proofs=1. 82.05/82.05 Usable=12. Sos=14. Demods=0. Limbo=1, Disabled=14. Hints=0. 82.05/82.05 Kept_by_rule=0, Deleted_by_rule=0. 82.05/82.05 Forward_subsumed=0. Back_subsumed=1. 82.05/82.05 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 82.05/82.05 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 82.05/82.05 Demod_attempts=0. Demod_rewrites=0. 82.05/82.05 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 82.05/82.05 Nonunit_fsub_feature_tests=1. Nonunit_bsub_feature_tests=15. 82.05/82.05 Megabytes=0.09. 82.05/82.05 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 82.05/82.05 82.05/82.05 ============================== end of statistics ===================== 82.05/82.05 82.05/82.05 ============================== end of search ========================= 82.05/82.05 82.05/82.05 THEOREM PROVED 82.05/82.05 82.05/82.05 Exiting with 1 proof. 82.05/82.05 82.05/82.05 Process 54674 exit (max_proofs) Wed Jul 14 11:13:08 2021 82.05/82.05 82.05/82.05 82.05/82.05 The problem is feasible. 82.05/82.05 82.05/82.05 82.05/82.05 CRule InfChecker Info: 82.05/82.05 g(s(x:S)) -> x:S 82.05/82.05 Rule remains 82.05/82.05 Proof: 82.05/82.05 NO_CONDS 82.05/82.05 82.05/82.05 CRule InfChecker Info: 82.05/82.05 h(s(x:S)) -> x:S 82.05/82.05 Rule remains 82.05/82.05 Proof: 82.05/82.05 NO_CONDS 82.05/82.05 82.05/82.05 Problem 1: 82.05/82.05 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.05/82.05 Confluence Problem: 82.05/82.05 (VAR x:S y:S) 82.05/82.05 (STRATEGY CONTEXTSENSITIVE 82.05/82.05 (b) 82.05/82.05 (f 1 2) 82.05/82.05 (g 1) 82.05/82.05 (h 1) 82.05/82.05 (a) 82.05/82.05 (c 1) 82.05/82.05 (fSNonEmpty) 82.05/82.05 (s 1) 82.05/82.05 ) 82.05/82.05 (RULES 82.05/82.05 f(x:S,y:S) -> g(s(x:S)) | c(g(x:S)) ->* c(a) 82.05/82.05 f(x:S,y:S) -> h(s(x:S)) | c(h(x:S)) ->* c(a) 82.05/82.05 g(s(x:S)) -> x:S 82.05/82.05 h(s(x:S)) -> x:S 82.05/82.05 ) 82.05/82.05 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.05/82.05 82.05/82.05 Critical Pairs Processor: 82.05/82.05 -> Rules: 82.05/82.05 f(x:S,y:S) -> g(s(x:S)) | c(g(x:S)) ->* c(a) 82.05/82.05 f(x:S,y:S) -> h(s(x:S)) | c(h(x:S)) ->* c(a) 82.05/82.05 g(s(x:S)) -> x:S 82.05/82.05 h(s(x:S)) -> x:S 82.05/82.05 -> Vars: 82.05/82.05 "x", "y", "x", "y", "x", "x" 82.05/82.05 -> FVars: 82.05/82.05 "x3", "x4", "x5", "x6", "x7", "x8" 82.05/82.05 -> PVars: 82.05/82.05 "x": ["x3", "x5", "x7", "x8"], "y": ["x4", "x6"] 82.05/82.05 82.05/82.05 -> Rlps: 82.05/82.05 crule: f(x3:S,x4:S) -> g(s(x3:S)) | c(g(x3:S)) ->* c(a), id: 1, possubterms: f(x3:S,x4:S)-> [] 82.05/82.05 crule: f(x5:S,x6:S) -> h(s(x5:S)) | c(h(x5:S)) ->* c(a), id: 2, possubterms: f(x5:S,x6:S)-> [] 82.05/82.05 crule: g(s(x7:S)) -> x7:S, id: 3, possubterms: g(s(x7:S))-> [], s(x7:S)-> [1] 82.05/82.05 crule: h(s(x8:S)) -> x8:S, id: 4, possubterms: h(s(x8:S))-> [], s(x8:S)-> [1] 82.05/82.05 82.05/82.05 -> Unifications: 82.05/82.05 R2 unifies with R1 at p: [], l: f(x5:S,x6:S), lp: f(x5:S,x6:S), conds: {c(h(x5:S)) ->* c(a), c(g(x:S)) ->* c(a)}, sig: {x5:S -> x:S,x6:S -> y:S}, l': f(x:S,y:S), r: h(s(x5:S)), r': g(s(x:S)) 82.05/82.05 82.05/82.05 -> Critical pairs info: 82.05/82.05 | c(h(x:S)) ->* c(a), c(g(x:S)) ->* c(a) => Not trivial, Overlay, N1 82.05/82.05 82.05/82.05 -> Problem conclusions: 82.05/82.05 Left linear, Right linear, Linear 82.05/82.05 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 82.05/82.05 CTRS Type: 1 82.05/82.05 Deterministic, Strongly deterministic 82.05/82.05 Oriented CTRS, Properly oriented CTRS, Not join CTRS 82.05/82.05 Maybe right-stable CTRS, Overlay CTRS 82.05/82.05 Maybe normal CTRS, Maybe almost normal CTRS 82.05/82.05 Maybe terminating CTRS, Maybe joinable CCPs 82.05/82.05 Maybe level confluent 82.05/82.05 Maybe confluent 82.05/82.05 82.05/82.05 Problem 1: 82.05/82.05 Clean Infeasible CCPs Processor: 82.05/82.05 Num of CPIs: 1 82.05/82.05 Timeout: 60 82.05/82.05 Timeout for each infeasibility problem: 60 s 82.05/82.05 | c(h(x:S)) ->* c(a), c(g(x:S)) ->* c(a) => Not trivial, Overlay, Feasible conditions, N1 82.05/82.05 (PROBLEM INFEASIBILITY) 82.05/82.05 (VAR x y) 82.05/82.05 (RULES 82.05/82.05 f(x,y) -> g(s(x)) | c(g(x)) ->* c(a) 82.05/82.05 f(x,y) -> h(s(x)) | c(h(x)) ->* c(a) 82.05/82.05 g(s(x)) -> x 82.05/82.05 h(s(x)) -> x) 82.05/82.05 (VAR x5) 82.05/82.05 (CONDITION c(h(x5)) ->* c(a), c(g(x5)) ->* c(a)) 82.05/82.05 82.05/82.05 Proof: 82.05/82.05 NO 82.05/82.05 82.05/82.05 Problem 1: 82.05/82.05 82.05/82.05 Infeasibility Problem: 82.05/82.05 [(VAR vNonEmpty:S x:S y:S x5:S) 82.05/82.05 (STRATEGY CONTEXTSENSITIVE 82.05/82.05 (f 1 2) 82.05/82.05 (g 1) 82.05/82.05 (h 1) 82.05/82.05 (a) 82.05/82.05 (c 1) 82.05/82.05 (fSNonEmpty) 82.05/82.05 (s 1) 82.05/82.05 ) 82.05/82.05 (RULES 82.05/82.05 f(x:S,y:S) -> g(s(x:S)) | c(g(x:S)) ->* c(a) 82.05/82.05 f(x:S,y:S) -> h(s(x:S)) | c(h(x:S)) ->* c(a) 82.05/82.05 g(s(x:S)) -> x:S 82.05/82.05 h(s(x:S)) -> x:S 82.05/82.05 )] 82.05/82.05 82.05/82.05 Infeasibility Conditions: 82.05/82.05 c(h(x5:S)) ->* c(a), c(g(x5:S)) ->* c(a) 82.05/82.05 82.05/82.05 Problem 1: 82.05/82.05 82.05/82.05 Obtaining a proof using Prover9: 82.05/82.05 82.05/82.05 -> Prover9 Output: 82.05/82.05 ============================== Prover9 =============================== 82.05/82.05 Prover9 (64) version 2009-11A, November 2009. 82.05/82.05 Process 54707 was started by ubuntu on ubuntu, 82.05/82.05 Wed Jul 14 11:13:08 2021 82.05/82.05 The command was "./prover9 -f /tmp/prover954691-0.in". 82.05/82.05 ============================== end of head =========================== 82.05/82.05 82.05/82.05 ============================== INPUT ================================= 82.05/82.05 82.05/82.05 % Reading from file /tmp/prover954691-0.in 82.05/82.05 82.05/82.05 assign(max_seconds,20). 82.05/82.05 82.05/82.05 formulas(assumptions). 82.05/82.05 ->*_s0(x,x) # label(reflexivity). 82.05/82.05 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 82.05/82.05 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence). 82.05/82.05 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence). 82.05/82.05 ->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence). 82.05/82.05 ->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence). 82.05/82.05 ->_s0(x1,y) -> ->_s0(c(x1),c(y)) # label(congruence). 82.05/82.05 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence). 82.05/82.05 ->*_s0(c(g(x1)),c(a)) -> ->_s0(f(x1,x2),g(s(x1))) # label(replacement). 82.05/82.05 ->*_s0(c(h(x1)),c(a)) -> ->_s0(f(x1,x2),h(s(x1))) # label(replacement). 82.05/82.05 ->_s0(g(s(x1)),x1) # label(replacement). 82.05/82.05 ->_s0(h(s(x1)),x1) # label(replacement). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 formulas(goals). 82.05/82.05 (exists x3 (->*_s0(c(h(x3)),c(a)) & ->*_s0(c(g(x3)),c(a)))) # label(goal). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 ============================== end of input ========================== 82.05/82.05 82.05/82.05 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 82.05/82.05 82.05/82.05 % Formulas that are not ordinary clauses: 82.05/82.05 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 82.05/82.05 2 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 3 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 4 ->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 5 ->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 6 ->_s0(x1,y) -> ->_s0(c(x1),c(y)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 7 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 8 ->*_s0(c(g(x1)),c(a)) -> ->_s0(f(x1,x2),g(s(x1))) # label(replacement) # label(non_clause). [assumption]. 82.05/82.05 9 ->*_s0(c(h(x1)),c(a)) -> ->_s0(f(x1,x2),h(s(x1))) # label(replacement) # label(non_clause). [assumption]. 82.05/82.05 10 (exists x3 (->*_s0(c(h(x3)),c(a)) & ->*_s0(c(g(x3)),c(a)))) # label(goal) # label(non_clause) # label(goal). [goal]. 82.05/82.05 82.05/82.05 ============================== end of process non-clausal formulas === 82.05/82.05 82.05/82.05 ============================== PROCESS INITIAL CLAUSES =============== 82.05/82.05 82.05/82.05 % Clauses before input processing: 82.05/82.05 82.05/82.05 formulas(usable). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 formulas(sos). 82.05/82.05 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.05/82.05 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.05/82.05 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 82.05/82.05 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 82.05/82.05 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 82.05/82.05 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 82.05/82.05 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.05/82.05 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(7)]. 82.05/82.05 -->*_s0(c(g(x)),c(a)) | ->_s0(f(x,y),g(s(x))) # label(replacement). [clausify(8)]. 82.05/82.05 -->*_s0(c(h(x)),c(a)) | ->_s0(f(x,y),h(s(x))) # label(replacement). [clausify(9)]. 82.05/82.05 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 -->*_s0(c(h(x)),c(a)) | -->*_s0(c(g(x)),c(a)) # label(goal). [deny(10)]. 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 formulas(demodulators). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 ============================== PREDICATE ELIMINATION ================= 82.05/82.05 82.05/82.05 No predicates eliminated. 82.05/82.05 82.05/82.05 ============================== end predicate elimination ============= 82.05/82.05 82.05/82.05 Auto_denials: 82.05/82.05 % copying label goal to answer in negative clause 82.05/82.05 82.05/82.05 Term ordering decisions: 82.05/82.05 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 82.05/82.05 Function symbol precedence: function_order([ a, f, c, s, g, h ]). 82.05/82.05 After inverse_order: (no changes). 82.05/82.05 Unfolding symbols: (none). 82.05/82.05 82.05/82.05 Auto_inference settings: 82.05/82.05 % set(neg_binary_resolution). % (HNE depth_diff=-6) 82.05/82.05 % clear(ordered_res). % (HNE depth_diff=-6) 82.05/82.05 % set(ur_resolution). % (HNE depth_diff=-6) 82.05/82.05 % set(ur_resolution) -> set(pos_ur_resolution). 82.05/82.05 % set(ur_resolution) -> set(neg_ur_resolution). 82.05/82.05 82.05/82.05 Auto_process settings: 82.05/82.05 % set(unit_deletion). % (Horn set with negative nonunits) 82.05/82.05 82.05/82.05 kept: 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.05/82.05 kept: 12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.05/82.05 kept: 13 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 82.05/82.05 kept: 14 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 82.05/82.05 kept: 15 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 82.05/82.05 kept: 16 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 82.05/82.05 kept: 17 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.05/82.05 kept: 18 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(7)]. 82.05/82.05 kept: 19 -->*_s0(c(g(x)),c(a)) | ->_s0(f(x,y),g(s(x))) # label(replacement). [clausify(8)]. 82.05/82.05 kept: 20 -->*_s0(c(h(x)),c(a)) | ->_s0(f(x,y),h(s(x))) # label(replacement). [clausify(9)]. 82.05/82.05 kept: 21 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 kept: 22 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 kept: 23 -->*_s0(c(h(x)),c(a)) | -->*_s0(c(g(x)),c(a)) # label(goal) # answer(goal). [deny(10)]. 82.05/82.05 82.05/82.05 ============================== end of process initial clauses ======== 82.05/82.05 82.05/82.05 ============================== CLAUSES FOR SEARCH ==================== 82.05/82.05 82.05/82.05 % Clauses after input processing: 82.05/82.05 82.05/82.05 formulas(usable). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 formulas(sos). 82.05/82.05 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.05/82.05 12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.05/82.05 13 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 82.05/82.05 14 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 82.05/82.05 15 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 82.05/82.05 16 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 82.05/82.05 17 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.05/82.05 18 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(7)]. 82.05/82.05 19 -->*_s0(c(g(x)),c(a)) | ->_s0(f(x,y),g(s(x))) # label(replacement). [clausify(8)]. 82.05/82.05 20 -->*_s0(c(h(x)),c(a)) | ->_s0(f(x,y),h(s(x))) # label(replacement). [clausify(9)]. 82.05/82.05 21 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 22 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 23 -->*_s0(c(h(x)),c(a)) | -->*_s0(c(g(x)),c(a)) # label(goal) # answer(goal). [deny(10)]. 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 formulas(demodulators). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 ============================== end of clauses for search ============= 82.05/82.05 82.05/82.05 ============================== SEARCH ================================ 82.05/82.05 82.05/82.05 % Starting search at 0.00 seconds. 82.05/82.05 82.05/82.05 given #1 (I,wt=3): 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.05/82.05 82.05/82.05 given #2 (I,wt=9): 12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.05/82.05 82.05/82.05 given #3 (I,wt=10): 13 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 82.05/82.05 82.05/82.05 given #4 (I,wt=10): 14 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 82.05/82.05 82.05/82.05 given #5 (I,wt=8): 15 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 82.05/82.05 82.05/82.05 given #6 (I,wt=8): 16 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 82.05/82.05 82.05/82.05 given #7 (I,wt=8): 17 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.05/82.05 82.05/82.05 given #8 (I,wt=8): 18 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(7)]. 82.05/82.05 82.05/82.05 given #9 (I,wt=13): 19 -->*_s0(c(g(x)),c(a)) | ->_s0(f(x,y),g(s(x))) # label(replacement). [clausify(8)]. 82.05/82.05 82.05/82.05 given #10 (I,wt=13): 20 -->*_s0(c(h(x)),c(a)) | ->_s0(f(x,y),h(s(x))) # label(replacement). [clausify(9)]. 82.05/82.05 82.05/82.05 given #11 (I,wt=5): 21 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 82.05/82.05 given #12 (I,wt=5): 22 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 82.05/82.05 given #13 (I,wt=12): 23 -->*_s0(c(h(x)),c(a)) | -->*_s0(c(g(x)),c(a)) # label(goal) # answer(goal). [deny(10)]. 82.05/82.05 82.05/82.05 given #14 (A,wt=7): 24 ->_s0(s(g(s(x))),s(x)). [ur(18,a,21,a)]. 82.05/82.05 82.05/82.05 given #15 (F,wt=15): 38 -->*_s0(c(g(x)),c(a)) | -->_s0(c(h(x)),y) | -->*_s0(y,c(a)) # answer(goal). [resolve(23,a,12,c)]. 82.05/82.05 82.05/82.05 given #16 (F,wt=12): 49 -->*_s0(c(g(x)),c(a)) | -->_s0(c(h(x)),c(a)) # answer(goal). [resolve(38,c,11,a)]. 82.05/82.05 82.05/82.05 given #17 (F,wt=10): 51 -->*_s0(c(g(x)),c(a)) | -->_s0(h(x),a) # answer(goal). [resolve(49,b,17,b)]. 82.05/82.05 82.05/82.05 given #18 (F,wt=7): 53 -->*_s0(c(g(s(a))),c(a)) # answer(goal). [resolve(51,b,22,a)]. 82.05/82.05 82.05/82.05 ============================== PROOF ================================= 82.05/82.05 82.05/82.05 % Proof 1 at 0.01 (+ 0.00) seconds: goal. 82.05/82.05 % Length of proof is 15. 82.05/82.05 % Level of proof is 6. 82.05/82.05 % Maximum clause weight is 15.000. 82.05/82.05 % Given clauses 18. 82.05/82.05 82.05/82.05 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 82.05/82.05 6 ->_s0(x1,y) -> ->_s0(c(x1),c(y)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 10 (exists x3 (->*_s0(c(h(x3)),c(a)) & ->*_s0(c(g(x3)),c(a)))) # label(goal) # label(non_clause) # label(goal). [goal]. 82.05/82.05 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.05/82.05 12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.05/82.05 17 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.05/82.05 21 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 22 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.05/82.05 23 -->*_s0(c(h(x)),c(a)) | -->*_s0(c(g(x)),c(a)) # label(goal) # answer(goal). [deny(10)]. 82.05/82.05 25 ->_s0(c(g(s(x))),c(x)). [ur(17,a,21,a)]. 82.05/82.05 38 -->*_s0(c(g(x)),c(a)) | -->_s0(c(h(x)),y) | -->*_s0(y,c(a)) # answer(goal). [resolve(23,a,12,c)]. 82.05/82.05 49 -->*_s0(c(g(x)),c(a)) | -->_s0(c(h(x)),c(a)) # answer(goal). [resolve(38,c,11,a)]. 82.05/82.05 51 -->*_s0(c(g(x)),c(a)) | -->_s0(h(x),a) # answer(goal). [resolve(49,b,17,b)]. 82.05/82.05 53 -->*_s0(c(g(s(a))),c(a)) # answer(goal). [resolve(51,b,22,a)]. 82.05/82.05 55 $F # answer(goal). [ur(12,b,11,a,c,53,a),unit_del(a,25)]. 82.05/82.05 82.05/82.05 ============================== end of proof ========================== 82.05/82.05 82.05/82.05 ============================== STATISTICS ============================ 82.05/82.05 82.05/82.05 Given=18. Generated=47. Kept=44. proofs=1. 82.05/82.05 Usable=18. Sos=25. Demods=0. Limbo=1, Disabled=13. Hints=0. 82.05/82.05 Kept_by_rule=0, Deleted_by_rule=0. 82.05/82.05 Forward_subsumed=2. Back_subsumed=0. 82.05/82.05 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 82.05/82.05 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 82.05/82.05 Demod_attempts=0. Demod_rewrites=0. 82.05/82.05 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 82.05/82.05 Nonunit_fsub_feature_tests=14. Nonunit_bsub_feature_tests=48. 82.05/82.05 Megabytes=0.12. 82.05/82.05 User_CPU=0.01, System_CPU=0.00, Wall_clock=0. 82.05/82.05 82.05/82.05 ============================== end of statistics ===================== 82.05/82.05 82.05/82.05 ============================== end of search ========================= 82.05/82.05 82.05/82.05 THEOREM PROVED 82.05/82.05 82.05/82.05 Exiting with 1 proof. 82.05/82.05 82.05/82.05 Process 54707 exit (max_proofs) Wed Jul 14 11:13:08 2021 82.05/82.05 82.05/82.05 82.05/82.05 The problem is feasible. 82.05/82.05 82.05/82.05 82.05/82.05 82.05/82.05 82.05/82.05 -> Problem conclusions: 82.05/82.05 Left linear, Right linear, Linear 82.05/82.05 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 82.05/82.05 CTRS Type: 1 82.05/82.05 Deterministic, Strongly deterministic 82.05/82.05 Oriented CTRS, Properly oriented CTRS, Not join CTRS 82.05/82.05 Maybe right-stable CTRS, Overlay CTRS 82.05/82.05 Maybe normal CTRS, Maybe almost normal CTRS 82.05/82.05 Maybe terminating CTRS, Maybe joinable CCPs 82.05/82.05 Maybe level confluent 82.05/82.05 Maybe confluent 82.05/82.05 82.05/82.05 Resulting CCPs: 82.05/82.05 | c(h(x:S)) ->* c(a), c(g(x:S)) ->* c(a) => Not trivial, Overlay, Feasible conditions, N1 82.05/82.05 82.05/82.05 Problem 1: 82.05/82.05 Underlying TRS Termination Processor: 82.05/82.05 82.05/82.05 Resulting Underlying TRS: 82.05/82.05 (VAR x:S y:S) 82.05/82.05 (STRATEGY CONTEXTSENSITIVE 82.05/82.05 (f 1 2) 82.05/82.05 (g 1) 82.05/82.05 (h 1) 82.05/82.05 ) 82.05/82.05 (RULES 82.05/82.05 f(x:S,y:S) -> g(s(x:S)) 82.05/82.05 f(x:S,y:S) -> h(s(x:S)) 82.05/82.05 g(s(x:S)) -> x:S 82.05/82.05 h(s(x:S)) -> x:S 82.05/82.05 ) 82.05/82.05 Underlying TRS terminating? 82.05/82.05 YES 82.05/82.05 82.05/82.05 Problem 1: 82.05/82.05 82.05/82.05 (VAR vu95NonEmpty:S xu58S:S yu58S:S) 82.05/82.05 (RULES 82.05/82.05 f(xu58S:S,yu58S:S) -> g(s(xu58S:S)) 82.05/82.05 f(xu58S:S,yu58S:S) -> h(s(xu58S:S)) 82.05/82.05 g(s(xu58S:S)) -> xu58S:S 82.05/82.05 h(s(xu58S:S)) -> xu58S:S 82.05/82.05 ) 82.05/82.05 82.05/82.05 Problem 1: 82.05/82.05 82.05/82.05 Dependency Pairs Processor: 82.05/82.05 -> Pairs: 82.05/82.05 F(xu58S:S,yu58S:S) -> G(s(xu58S:S)) 82.05/82.05 F(xu58S:S,yu58S:S) -> H(s(xu58S:S)) 82.05/82.05 -> Rules: 82.05/82.05 f(xu58S:S,yu58S:S) -> g(s(xu58S:S)) 82.05/82.05 f(xu58S:S,yu58S:S) -> h(s(xu58S:S)) 82.05/82.05 g(s(xu58S:S)) -> xu58S:S 82.05/82.05 h(s(xu58S:S)) -> xu58S:S 82.05/82.05 82.05/82.05 Problem 1: 82.05/82.05 82.05/82.05 SCC Processor: 82.05/82.05 -> Pairs: 82.05/82.05 F(xu58S:S,yu58S:S) -> G(s(xu58S:S)) 82.05/82.05 F(xu58S:S,yu58S:S) -> H(s(xu58S:S)) 82.05/82.05 -> Rules: 82.05/82.05 f(xu58S:S,yu58S:S) -> g(s(xu58S:S)) 82.05/82.05 f(xu58S:S,yu58S:S) -> h(s(xu58S:S)) 82.05/82.05 g(s(xu58S:S)) -> xu58S:S 82.05/82.05 h(s(xu58S:S)) -> xu58S:S 82.05/82.05 ->Strongly Connected Components: 82.05/82.05 There is no strongly connected component 82.05/82.05 82.05/82.05 The problem is finite. 82.05/82.05 82.05/82.05 82.05/82.05 -> Problem conclusions: 82.05/82.05 Left linear, Right linear, Linear 82.05/82.05 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 82.05/82.05 CTRS Type: 1 82.05/82.05 Deterministic, Strongly deterministic 82.05/82.05 Oriented CTRS, Properly oriented CTRS, Not join CTRS 82.05/82.05 Maybe right-stable CTRS, Overlay CTRS 82.05/82.05 Maybe normal CTRS, Maybe almost normal CTRS 82.05/82.05 Terminating CTRS, Maybe joinable CCPs 82.05/82.05 Maybe level confluent 82.05/82.05 Maybe confluent 82.05/82.05 82.05/82.05 Problem 1: 82.05/82.05 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.05/82.05 Confluence Problem: 82.05/82.05 (VAR x:S y:S) 82.05/82.05 (STRATEGY CONTEXTSENSITIVE 82.05/82.05 (b) 82.05/82.05 (f 1 2) 82.05/82.05 (g 1) 82.05/82.05 (h 1) 82.05/82.05 (a) 82.05/82.05 (c 1) 82.05/82.05 (fSNonEmpty) 82.05/82.05 (s 1) 82.05/82.05 ) 82.05/82.05 (RULES 82.05/82.05 f(x:S,y:S) -> g(s(x:S)) | c(g(x:S)) ->* c(a) 82.05/82.05 f(x:S,y:S) -> h(s(x:S)) | c(h(x:S)) ->* c(a) 82.05/82.05 g(s(x:S)) -> x:S 82.05/82.05 h(s(x:S)) -> x:S 82.05/82.05 ) 82.05/82.05 Critical Pairs: 82.05/82.05 | c(h(x:S)) ->* c(a), c(g(x:S)) ->* c(a) => Not trivial, Overlay, Feasible conditions, N1 82.05/82.05 Terminating:YES 82.05/82.05 82.05/82.05 -> Problem conclusions: 82.05/82.05 Left linear, Right linear, Linear 82.05/82.05 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 82.05/82.05 CTRS Type: 1 82.05/82.05 Deterministic, Strongly deterministic 82.05/82.05 Oriented CTRS, Properly oriented CTRS, Not join CTRS 82.05/82.05 Maybe right-stable CTRS, Overlay CTRS 82.05/82.05 Maybe normal CTRS, Maybe almost normal CTRS 82.05/82.05 Terminating CTRS, Maybe joinable CCPs 82.05/82.05 Maybe level confluent 82.05/82.05 Maybe confluent 82.05/82.05 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.05/82.05 82.05/82.05 Right Stable Processor: 82.05/82.05 Right-stable CTRS 82.05/82.05 Justification: 82.05/82.05 82.05/82.05 -> Term right-stability conditions: 82.05/82.05 Term: c(a) 82.05/82.05 Right-stable term 82.05/82.05 Linear constructor form 82.05/82.05 Don't know if term is a ground normal form (not needed) 82.05/82.05 Right-stability condition achieved 82.05/82.05 A call to InfChecker wasn't needed 82.05/82.05 82.05/82.05 82.05/82.05 -> Term right-stability conditions: 82.05/82.05 Term: c(a) 82.05/82.05 Right-stable term 82.05/82.05 Linear constructor form 82.05/82.05 Don't know if term is a ground normal form (not needed) 82.05/82.05 Right-stability condition achieved 82.05/82.05 A call to InfChecker wasn't needed 82.05/82.05 82.05/82.05 -> Problem conclusions: 82.05/82.05 Left linear, Right linear, Linear 82.05/82.05 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 82.05/82.05 CTRS Type: 1 82.05/82.05 Deterministic, Strongly deterministic 82.05/82.05 Oriented CTRS, Properly oriented CTRS, Not join CTRS 82.05/82.05 Right-stable CTRS, Overlay CTRS 82.05/82.05 Maybe normal CTRS, Almost normal CTRS 82.05/82.05 Terminating CTRS, Maybe joinable CCPs 82.05/82.05 Maybe level confluent 82.05/82.05 Maybe confluent 82.05/82.05 82.05/82.05 Problem 1: 82.05/82.05 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.05/82.05 Confluence Problem: 82.05/82.05 (VAR x:S y:S) 82.05/82.05 (STRATEGY CONTEXTSENSITIVE 82.05/82.05 (b) 82.05/82.05 (f 1 2) 82.05/82.05 (g 1) 82.05/82.05 (h 1) 82.05/82.05 (a) 82.05/82.05 (c 1) 82.05/82.05 (fSNonEmpty) 82.05/82.05 (s 1) 82.05/82.05 ) 82.05/82.05 (RULES 82.05/82.05 f(x:S,y:S) -> g(s(x:S)) | c(g(x:S)) ->* c(a) 82.05/82.05 f(x:S,y:S) -> h(s(x:S)) | c(h(x:S)) ->* c(a) 82.05/82.05 g(s(x:S)) -> x:S 82.05/82.05 h(s(x:S)) -> x:S 82.05/82.05 ) 82.05/82.05 Critical Pairs: 82.05/82.05 | c(h(x:S)) ->* c(a), c(g(x:S)) ->* c(a) => Not trivial, Overlay, Feasible conditions, N1 82.05/82.05 Terminating:YES 82.05/82.05 82.05/82.05 -> Problem conclusions: 82.05/82.05 Left linear, Right linear, Linear 82.05/82.05 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 82.05/82.05 CTRS Type: 1 82.05/82.05 Deterministic, Strongly deterministic 82.05/82.05 Oriented CTRS, Properly oriented CTRS, Not join CTRS 82.05/82.05 Right-stable CTRS, Overlay CTRS 82.05/82.05 Maybe normal CTRS, Almost normal CTRS 82.05/82.05 Terminating CTRS, Maybe joinable CCPs 82.05/82.05 Maybe level confluent 82.05/82.05 Maybe confluent 82.05/82.05 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.05/82.05 82.05/82.05 Normal RConds Processor: 82.05/82.05 YES 82.05/82.05 82.05/82.05 Problem 1: 82.05/82.05 82.05/82.05 Infeasibility Problem: 82.05/82.05 [(VAR vNonEmpty:S x:S y:S x1:S) 82.05/82.05 (STRATEGY CONTEXTSENSITIVE 82.05/82.05 (f 1 2) 82.05/82.05 (g 1) 82.05/82.05 (h 1) 82.05/82.05 (a) 82.05/82.05 (c 1) 82.05/82.05 (fSNonEmpty) 82.05/82.05 (s 1) 82.05/82.05 ) 82.05/82.05 (RULES 82.05/82.05 f(x:S,y:S) -> g(s(x:S)) | c(g(x:S)) ->* c(a) 82.05/82.05 f(x:S,y:S) -> h(s(x:S)) | c(h(x:S)) ->* c(a) 82.05/82.05 g(s(x:S)) -> x:S 82.05/82.05 h(s(x:S)) -> x:S 82.05/82.05 )] 82.05/82.05 82.05/82.05 Infeasibility Conditions: 82.05/82.05 c(a) -> x1:S 82.05/82.05 82.05/82.05 Problem 1: 82.05/82.05 82.05/82.05 Obtaining a model using Mace4: 82.05/82.05 82.05/82.05 -> Usable Rules: 82.05/82.05 Empty 82.05/82.05 82.05/82.05 -> Mace4 Output: 82.05/82.05 ============================== Mace4 ================================= 82.05/82.05 Mace4 (64) version 2009-11A, November 2009. 82.05/82.05 Process 55025 was started by ubuntu on ubuntu, 82.05/82.05 Wed Jul 14 11:14:01 2021 82.05/82.05 The command was "./mace4 -c -f /tmp/mace455013-2.in". 82.05/82.05 ============================== end of head =========================== 82.05/82.05 82.05/82.05 ============================== INPUT ================================= 82.05/82.05 82.05/82.05 % Reading from file /tmp/mace455013-2.in 82.05/82.05 82.05/82.05 assign(max_seconds,8). 82.05/82.05 82.05/82.05 formulas(assumptions). 82.05/82.05 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence). 82.05/82.05 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence). 82.05/82.05 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence). 82.05/82.05 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence). 82.05/82.05 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence). 82.05/82.05 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 formulas(goals). 82.05/82.05 (exists x3 ->(c(a),x3)) # label(goal). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 ============================== end of input ========================== 82.05/82.05 82.05/82.05 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 82.05/82.05 82.05/82.05 % Formulas that are not ordinary clauses: 82.05/82.05 1 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 2 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 3 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 4 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 5 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 6 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 82.05/82.05 7 (exists x3 ->(c(a),x3)) # label(goal) # label(non_clause) # label(goal). [goal]. 82.05/82.05 82.05/82.05 ============================== end of process non-clausal formulas === 82.05/82.05 82.05/82.05 ============================== CLAUSES FOR SEARCH ==================== 82.05/82.05 82.05/82.05 formulas(mace4_clauses). 82.05/82.05 -->(x,y) | ->(f(x,z),f(y,z)) # label(congruence). 82.05/82.05 -->(x,y) | ->(f(z,x),f(z,y)) # label(congruence). 82.05/82.05 -->(x,y) | ->(g(x),g(y)) # label(congruence). 82.05/82.05 -->(x,y) | ->(h(x),h(y)) # label(congruence). 82.05/82.05 -->(x,y) | ->(c(x),c(y)) # label(congruence). 82.05/82.05 -->(x,y) | ->(s(x),s(y)) # label(congruence). 82.05/82.05 -->(c(a),x) # label(goal). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 ============================== end of clauses for search ============= 82.05/82.05 82.05/82.05 % There are no natural numbers in the input. 82.05/82.05 82.05/82.05 ============================== DOMAIN SIZE 2 ========================= 82.05/82.05 82.05/82.05 ============================== MODEL ================================= 82.05/82.05 82.05/82.05 interpretation( 2, [number=1, seconds=0], [ 82.05/82.05 82.05/82.05 function(a, [ 0 ]), 82.05/82.05 82.05/82.05 function(g(_), [ 0, 0 ]), 82.05/82.05 82.05/82.05 function(h(_), [ 0, 0 ]), 82.05/82.05 82.05/82.05 function(c(_), [ 0, 0 ]), 82.05/82.05 82.05/82.05 function(s(_), [ 0, 0 ]), 82.05/82.05 82.05/82.05 function(f(_,_), [ 82.05/82.05 0, 0, 82.05/82.05 0, 0 ]), 82.05/82.05 82.05/82.05 relation(->(_,_), [ 82.05/82.05 0, 0, 82.05/82.05 0, 0 ]) 82.05/82.05 ]). 82.05/82.05 82.05/82.05 ============================== end of model ========================== 82.05/82.05 82.05/82.05 ============================== STATISTICS ============================ 82.05/82.05 82.05/82.05 For domain size 2. 82.05/82.05 82.05/82.05 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 82.05/82.05 Ground clauses: seen=34, kept=34. 82.05/82.05 Selections=13, assignments=13, propagations=4, current_models=1. 82.05/82.05 Rewrite_terms=68, rewrite_bools=39, indexes=6. 82.05/82.05 Rules_from_neg_clauses=0, cross_offs=0. 82.05/82.05 82.05/82.05 ============================== end of statistics ===================== 82.05/82.05 82.05/82.05 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 82.05/82.05 82.05/82.05 Exiting with 1 model. 82.05/82.05 82.05/82.05 Process 55025 exit (max_models) Wed Jul 14 11:14:01 2021 82.05/82.05 The process finished Wed Jul 14 11:14:01 2021 82.05/82.05 82.05/82.05 82.05/82.05 Mace4 cooked interpretation: 82.05/82.05 82.05/82.05 82.05/82.05 82.05/82.05 The problem is infeasible. 82.05/82.05 82.05/82.05 82.05/82.05 -> Problem conclusions: 82.05/82.05 Left linear, Right linear, Linear 82.05/82.05 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 82.05/82.05 CTRS Type: 1 82.05/82.05 Deterministic, Strongly deterministic 82.05/82.05 Oriented CTRS, Properly oriented CTRS, Not join CTRS 82.05/82.05 Right-stable CTRS, Overlay CTRS 82.05/82.05 Normal CTRS, Almost normal CTRS 82.05/82.05 Terminating CTRS, Maybe joinable CCPs 82.05/82.05 Maybe level confluent 82.05/82.05 Maybe confluent 82.05/82.05 82.05/82.05 Problem 1: 82.05/82.05 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.05/82.05 Confluence Problem: 82.05/82.05 (VAR x:S y:S) 82.05/82.05 (STRATEGY CONTEXTSENSITIVE 82.05/82.05 (b) 82.05/82.05 (f 1 2) 82.05/82.05 (g 1) 82.05/82.05 (h 1) 82.05/82.05 (a) 82.05/82.05 (c 1) 82.05/82.05 (fSNonEmpty) 82.05/82.05 (s 1) 82.05/82.05 ) 82.05/82.05 (RULES 82.05/82.05 f(x:S,y:S) -> g(s(x:S)) | c(g(x:S)) ->* c(a) 82.05/82.05 f(x:S,y:S) -> h(s(x:S)) | c(h(x:S)) ->* c(a) 82.05/82.05 g(s(x:S)) -> x:S 82.05/82.05 h(s(x:S)) -> x:S 82.05/82.05 ) 82.05/82.05 Critical Pairs: 82.05/82.05 | c(h(x:S)) ->* c(a), c(g(x:S)) ->* c(a) => Not trivial, Overlay, Feasible conditions, N1 82.05/82.05 Terminating:YES 82.05/82.05 82.05/82.05 -> Problem conclusions: 82.05/82.05 Left linear, Right linear, Linear 82.05/82.05 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 82.05/82.05 CTRS Type: 1 82.05/82.05 Deterministic, Strongly deterministic 82.05/82.05 Oriented CTRS, Properly oriented CTRS, Not join CTRS 82.05/82.05 Right-stable CTRS, Overlay CTRS 82.05/82.05 Normal CTRS, Almost normal CTRS 82.05/82.05 Terminating CTRS, Maybe joinable CCPs 82.05/82.05 Maybe level confluent 82.05/82.05 Maybe confluent 82.05/82.05 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.05/82.05 82.05/82.05 Conditional Critical Pairs Distributor Processor 82.05/82.05 Problem 1.1: 82.05/82.05 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.05/82.05 Confluence Problem: 82.05/82.05 (VAR x:S y:S) 82.05/82.05 (STRATEGY CONTEXTSENSITIVE 82.05/82.05 (b) 82.05/82.05 (f 1 2) 82.05/82.05 (g 1) 82.05/82.05 (h 1) 82.05/82.05 (a) 82.05/82.05 (c 1) 82.05/82.05 (fSNonEmpty) 82.05/82.05 (s 1) 82.05/82.05 ) 82.05/82.05 (RULES 82.05/82.05 f(x:S,y:S) -> g(s(x:S)) | c(g(x:S)) ->* c(a) 82.05/82.05 f(x:S,y:S) -> h(s(x:S)) | c(h(x:S)) ->* c(a) 82.05/82.05 g(s(x:S)) -> x:S 82.05/82.05 h(s(x:S)) -> x:S 82.05/82.05 ) 82.05/82.05 Critical Pairs: 82.05/82.05 | c(h(x:S)) ->* c(a), c(g(x:S)) ->* c(a) => Not trivial, Overlay, Feasible conditions, N1 82.05/82.05 Terminating:YES 82.05/82.05 82.05/82.05 -> Problem conclusions: 82.05/82.05 Left linear, Right linear, Linear 82.05/82.05 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 82.05/82.05 CTRS Type: 1 82.05/82.05 Deterministic, Strongly deterministic 82.05/82.05 Oriented CTRS, Properly oriented CTRS, Not join CTRS 82.05/82.05 Right-stable CTRS, Overlay CTRS 82.05/82.05 Normal CTRS, Almost normal CTRS 82.05/82.05 Terminating CTRS, Maybe joinable CCPs 82.05/82.05 Maybe level confluent 82.05/82.05 Maybe confluent 82.05/82.05 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.05/82.05 82.05/82.05 Prover9 CCP Convergence Checker Processor: 82.05/82.05 formulas(sos). 82.05/82.05 %Reflexivity 82.05/82.05 reds(x,x). 82.05/82.05 82.05/82.05 %Transitivity 82.05/82.05 (red(x,y) & reds(y,z)) -> reds(x,z). 82.05/82.05 82.05/82.05 %Congruence 82.05/82.05 82.05/82.05 red(x,y) -> red(f(x,z2),f(y,z2)). 82.05/82.05 red(x,y) -> red(f(z1,x),f(z1,y)). 82.05/82.05 red(x,y) -> red(g(x),g(y)). 82.05/82.05 red(x,y) -> red(h(x),h(y)). 82.05/82.05 82.05/82.05 red(x,y) -> red(c(x),c(y)). 82.05/82.05 82.05/82.05 red(x,y) -> red(s(x),s(y)). %Replacement 82.05/82.05 reds(c(g(x)),c(a)) -> red(f(x,y),g(s(x))). 82.05/82.05 reds(c(h(x)),c(a)) -> red(f(x,y),h(s(x))). 82.05/82.05 red(g(s(x)),x). 82.05/82.05 red(h(s(x)),x). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 formulas(goals). 82.05/82.05 exists z (reds(g(s(c_x)),z) & reds(h(s(c_x)),z)). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 Proof: 82.05/82.05 ============================== Prover9 =============================== 82.05/82.05 Prover9 (64) version 2009-11A, November 2009. 82.05/82.05 Process 55041 was started by ubuntu on ubuntu, 82.05/82.05 Wed Jul 14 11:14:25 2021 82.05/82.05 The command was "./prover9 -t 60 -f /tmp/prover954599-44.in". 82.05/82.05 ============================== end of head =========================== 82.05/82.05 82.05/82.05 ============================== INPUT ================================= 82.05/82.05 82.05/82.05 % Reading from file /tmp/prover954599-44.in 82.05/82.05 82.05/82.05 82.05/82.05 formulas(sos). 82.05/82.05 reds(x,x). 82.05/82.05 red(x,y) & reds(y,z) -> reds(x,z). 82.05/82.05 red(x,y) -> red(f(x,z2),f(y,z2)). 82.05/82.05 red(x,y) -> red(f(z1,x),f(z1,y)). 82.05/82.05 red(x,y) -> red(g(x),g(y)). 82.05/82.05 red(x,y) -> red(h(x),h(y)). 82.05/82.05 red(x,y) -> red(c(x),c(y)). 82.05/82.05 red(x,y) -> red(s(x),s(y)). 82.05/82.05 reds(c(g(x)),c(a)) -> red(f(x,y),g(s(x))). 82.05/82.05 reds(c(h(x)),c(a)) -> red(f(x,y),h(s(x))). 82.05/82.05 red(g(s(x)),x). 82.05/82.05 red(h(s(x)),x). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 formulas(goals). 82.05/82.05 (exists z (reds(g(s(c_x)),z) & reds(h(s(c_x)),z))). 82.05/82.05 end_of_list. 82.05/82.05 assign(max_megs,-1). 82.05/82.05 set(quiet). 82.05/82.05 82.05/82.05 ============================== end of input ========================== 82.05/82.05 82.05/82.05 % From the command line: assign(max_seconds, 60). 82.05/82.05 82.05/82.05 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 82.05/82.05 82.05/82.05 % Formulas that are not ordinary clauses: 82.05/82.05 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 82.05/82.05 2 red(x,y) -> red(f(x,z2),f(y,z2)) # label(non_clause). [assumption]. 82.05/82.05 3 red(x,y) -> red(f(z1,x),f(z1,y)) # label(non_clause). [assumption]. 82.05/82.05 4 red(x,y) -> red(g(x),g(y)) # label(non_clause). [assumption]. 82.05/82.05 5 red(x,y) -> red(h(x),h(y)) # label(non_clause). [assumption]. 82.05/82.05 6 red(x,y) -> red(c(x),c(y)) # label(non_clause). [assumption]. 82.05/82.05 7 red(x,y) -> red(s(x),s(y)) # label(non_clause). [assumption]. 82.05/82.05 8 reds(c(g(x)),c(a)) -> red(f(x,y),g(s(x))) # label(non_clause). [assumption]. 82.05/82.05 9 reds(c(h(x)),c(a)) -> red(f(x,y),h(s(x))) # label(non_clause). [assumption]. 82.05/82.05 10 (exists z (reds(g(s(c_x)),z) & reds(h(s(c_x)),z))) # label(non_clause) # label(goal). [goal]. 82.05/82.05 82.05/82.05 ============================== end of process non-clausal formulas === 82.05/82.05 82.05/82.05 ============================== PROCESS INITIAL CLAUSES =============== 82.05/82.05 82.05/82.05 % Clauses before input processing: 82.05/82.05 82.05/82.05 formulas(usable). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 formulas(sos). 82.05/82.05 reds(x,x). [assumption]. 82.05/82.05 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 82.05/82.05 -red(x,y) | red(f(x,z),f(y,z)). [clausify(2)]. 82.05/82.05 -red(x,y) | red(f(z,x),f(z,y)). [clausify(3)]. 82.05/82.05 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 82.05/82.05 -red(x,y) | red(h(x),h(y)). [clausify(5)]. 82.05/82.05 -red(x,y) | red(c(x),c(y)). [clausify(6)]. 82.05/82.05 -red(x,y) | red(s(x),s(y)). [clausify(7)]. 82.05/82.05 -reds(c(g(x)),c(a)) | red(f(x,y),g(s(x))). [clausify(8)]. 82.05/82.05 -reds(c(h(x)),c(a)) | red(f(x,y),h(s(x))). [clausify(9)]. 82.05/82.05 red(g(s(x)),x). [assumption]. 82.05/82.05 red(h(s(x)),x). [assumption]. 82.05/82.05 -reds(g(s(c_x)),x) | -reds(h(s(c_x)),x). [deny(10)]. 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 formulas(demodulators). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 ============================== PREDICATE ELIMINATION ================= 82.05/82.05 82.05/82.05 ============================== end predicate elimination ============= 82.05/82.05 82.05/82.05 Auto_denials: (no changes). 82.05/82.05 82.05/82.05 Term ordering decisions: 82.05/82.05 82.05/82.05 kept: 11 reds(x,x). [assumption]. 82.05/82.05 kept: 12 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 82.05/82.05 kept: 13 -red(x,y) | red(f(x,z),f(y,z)). [clausify(2)]. 82.05/82.05 kept: 14 -red(x,y) | red(f(z,x),f(z,y)). [clausify(3)]. 82.05/82.05 kept: 15 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 82.05/82.05 kept: 16 -red(x,y) | red(h(x),h(y)). [clausify(5)]. 82.05/82.05 kept: 17 -red(x,y) | red(c(x),c(y)). [clausify(6)]. 82.05/82.05 kept: 18 -red(x,y) | red(s(x),s(y)). [clausify(7)]. 82.05/82.05 kept: 19 -reds(c(g(x)),c(a)) | red(f(x,y),g(s(x))). [clausify(8)]. 82.05/82.05 kept: 20 -reds(c(h(x)),c(a)) | red(f(x,y),h(s(x))). [clausify(9)]. 82.05/82.05 kept: 21 red(g(s(x)),x). [assumption]. 82.05/82.05 kept: 22 red(h(s(x)),x). [assumption]. 82.05/82.05 kept: 23 -reds(g(s(c_x)),x) | -reds(h(s(c_x)),x). [deny(10)]. 82.05/82.05 82.05/82.05 ============================== end of process initial clauses ======== 82.05/82.05 82.05/82.05 ============================== CLAUSES FOR SEARCH ==================== 82.05/82.05 82.05/82.05 % Clauses after input processing: 82.05/82.05 82.05/82.05 formulas(usable). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 formulas(sos). 82.05/82.05 11 reds(x,x). [assumption]. 82.05/82.05 12 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 82.05/82.05 13 -red(x,y) | red(f(x,z),f(y,z)). [clausify(2)]. 82.05/82.05 14 -red(x,y) | red(f(z,x),f(z,y)). [clausify(3)]. 82.05/82.05 15 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 82.05/82.05 16 -red(x,y) | red(h(x),h(y)). [clausify(5)]. 82.05/82.05 17 -red(x,y) | red(c(x),c(y)). [clausify(6)]. 82.05/82.05 18 -red(x,y) | red(s(x),s(y)). [clausify(7)]. 82.05/82.05 19 -reds(c(g(x)),c(a)) | red(f(x,y),g(s(x))). [clausify(8)]. 82.05/82.05 20 -reds(c(h(x)),c(a)) | red(f(x,y),h(s(x))). [clausify(9)]. 82.05/82.05 21 red(g(s(x)),x). [assumption]. 82.05/82.05 22 red(h(s(x)),x). [assumption]. 82.05/82.05 23 -reds(g(s(c_x)),x) | -reds(h(s(c_x)),x). [deny(10)]. 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 formulas(demodulators). 82.05/82.05 end_of_list. 82.05/82.05 82.05/82.05 ============================== end of clauses for search ============= 82.05/82.05 82.05/82.05 ============================== SEARCH ================================ 82.05/82.05 82.05/82.05 % Starting search at 0.00 seconds. 82.05/82.05 82.05/82.05 given #1 (I,wt=3): 11 reds(x,x). [assumption]. 82.05/82.05 82.05/82.05 given #2 (I,wt=9): 12 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 82.05/82.05 82.05/82.05 given #3 (I,wt=10): 13 -red(x,y) | red(f(x,z),f(y,z)). [clausify(2)]. 82.05/82.05 82.05/82.05 given #4 (I,wt=10): 14 -red(x,y) | red(f(z,x),f(z,y)). [clausify(3)]. 82.05/82.05 82.05/82.05 given #5 (I,wt=8): 15 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 82.05/82.05 82.05/82.05 given #6 (I,wt=8): 16 -red(x,y) | red(h(x),h(y)). [clausify(5)]. 82.05/82.05 82.05/82.05 given #7 (I,wt=8): 17 -red(x,y) | red(c(x),c(y)). [clausify(6)]. 82.05/82.05 82.05/82.05 given #8 (I,wt=8): 18 -red(x,y) | red(s(x),s(y)). [clausify(7)]. 82.05/82.05 82.05/82.05 given #9 (I,wt=13): 19 -reds(c(g(x)),c(a)) | red(f(x,y),g(s(x))). [clausify(8)]. 82.05/82.05 82.05/82.05 given #10 (I,wt=13): 20 -reds(c(h(x)),c(a)) | red(f(x,y),h(s(x))). [clausify(9)]. 82.05/82.05 82.05/82.05 given #11 (I,wt=5): 21 red(g(s(x)),x). [assumption]. 82.05/82.05 82.05/82.05 given #12 (I,wt=5): 22 red(h(s(x)),x). [assumption]. 82.05/82.05 82.05/82.05 given #13 (I,wt=10): 23 -reds(g(s(c_x)),x) | -reds(h(s(c_x)),x). [deny(10)]. 82.05/82.05 82.05/82.05 given #14 (A,wt=7): 24 red(s(g(s(x))),s(x)). [ur(18,a,21,a)]. 82.05/82.05 82.05/82.05 given #15 (F,wt=7): 39 -reds(h(s(c_x)),g(s(c_x))). [resolve(23,a,11,a)]. 82.05/82.05 82.05/82.05 given #16 (F,wt=5): 50 -reds(c_x,g(s(c_x))). [ur(12,a,22,a,c,39,a)]. 82.05/82.05 82.05/82.05 given #17 (F,wt=5): 52 -red(c_x,g(s(c_x))). [ur(12,b,11,a,c,50,a)]. 82.05/82.05 82.05/82.05 given #18 (F,wt=7): 41 -reds(g(s(c_x)),h(s(c_x))). [resolve(23,b,11,a)]. 82.05/82.05 82.05/82.05 given #19 (T,wt=5): 30 reds(g(s(x)),x). [ur(12,a,21,a,b,11,a)]. 82.05/82.05 82.05/82.05 ============================== PROOF ================================= 82.05/82.05 82.05/82.05 % Proof 1 at 0.00 (+ 0.00) seconds. 82.05/82.05 % Length of proof is 10. 82.05/82.05 % Level of proof is 3. 82.05/82.05 % Maximum clause weight is 10.000. 82.05/82.05 % Given clauses 19. 82.05/82.05 82.05/82.05 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 82.05/82.05 10 (exists z (reds(g(s(c_x)),z) & reds(h(s(c_x)),z))) # label(non_clause) # label(goal). [goal]. 82.05/82.05 11 reds(x,x). [assumption]. 82.05/82.05 12 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 82.05/82.05 21 red(g(s(x)),x). [assumption]. 82.05/82.05 22 red(h(s(x)),x). [assumption]. 82.05/82.05 23 -reds(g(s(c_x)),x) | -reds(h(s(c_x)),x). [deny(10)]. 82.05/82.05 30 reds(g(s(x)),x). [ur(12,a,21,a,b,11,a)]. 82.05/82.05 37 reds(h(s(x)),x). [ur(12,a,22,a,b,11,a)]. 82.05/82.05 56 $F. [resolve(30,a,23,a),unit_del(a,37)]. 82.05/82.05 82.05/82.05 ============================== end of proof ========================== 82.05/82.05 82.05/82.05 ============================== STATISTICS ============================ 82.05/82.05 82.05/82.05 Given=19. Generated=49. Kept=45. proofs=1. 82.05/82.05 Usable=19. Sos=26. Demods=0. Limbo=0, Disabled=13. Hints=0. 82.05/82.05 Kept_by_rule=0, Deleted_by_rule=0. 82.05/82.05 Forward_subsumed=3. Back_subsumed=0. 82.05/82.05 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 82.05/82.05 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 82.05/82.05 Demod_attempts=0. Demod_rewrites=0. 82.05/82.05 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 82.05/82.05 Nonunit_fsub_feature_tests=6. Nonunit_bsub_feature_tests=56. 82.05/82.05 Megabytes=0.12. 82.05/82.05 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 82.05/82.05 82.05/82.05 ============================== end of statistics ===================== 82.05/82.05 82.05/82.05 ============================== end of search ========================= 82.05/82.05 82.05/82.05 THEOREM PROVED 82.05/82.05 82.05/82.05 Exiting with 1 proof. 82.05/82.05 82.05/82.05 Process 55041 exit (max_proofs) Wed Jul 14 11:14:25 2021 82.05/82.05 82.05/82.05 82.05/82.05 The problem is joinable. 82.05/82.05 46.33user 3.09system 1:22.50elapsed 59%CPU (0avgtext+0avgdata 1960584maxresident)k 82.05/82.05 8inputs+0outputs (0major+677975minor)pagefaults 0swaps