41.042/41.042 YES 41.042/41.042 41.042/41.042 Problem 1: 41.042/41.042 41.042/41.042 41.042/41.042 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 41.042/41.042 Confluence Problem: 41.042/41.042 (VAR vNonEmpty x) 41.042/41.042 (REPLACEMENT-MAP 41.042/41.042 (even 1) 41.042/41.042 (odd 1) 41.042/41.042 (0) 41.042/41.042 (fSNonEmpty) 41.042/41.042 (false) 41.042/41.042 (s 1) 41.042/41.042 (true) 41.042/41.042 ) 41.042/41.042 (RULES 41.042/41.042 even(0) -> true 41.042/41.042 even(s(x)) -> false | odd(x) ->* false 41.042/41.042 even(s(x)) -> true | odd(x) ->* true 41.042/41.042 odd(0) -> false 41.042/41.042 odd(s(x)) -> false | even(x) ->* false 41.042/41.042 odd(s(x)) -> true | even(x) ->* true 41.042/41.042 ) 41.042/41.042 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 41.042/41.042 41.042/41.042 41.042/41.042 Problem 1: 41.042/41.042 41.042/41.042 Inlining of Conditions Processor [STERN17]: 41.042/41.042 41.042/41.042 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 41.042/41.042 Confluence Problem: 41.042/41.042 (VAR vNonEmpty x) 41.042/41.042 (REPLACEMENT-MAP 41.042/41.042 (even 1) 41.042/41.042 (odd 1) 41.042/41.042 (0) 41.042/41.042 (fSNonEmpty) 41.042/41.042 (false) 41.042/41.042 (s 1) 41.042/41.042 (true) 41.042/41.042 ) 41.042/41.042 (RULES 41.042/41.042 even(0) -> true 41.042/41.042 even(s(x)) -> false | odd(x) ->* false 41.042/41.042 even(s(x)) -> true | odd(x) ->* true 41.042/41.042 odd(0) -> false 41.042/41.042 odd(s(x)) -> false | even(x) ->* false 41.042/41.042 odd(s(x)) -> true | even(x) ->* true 41.042/41.042 ) 41.042/41.042 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 41.042/41.042 41.042/41.042 41.042/41.042 Problem 1: 41.042/41.042 41.042/41.042 Clean CTRS Processor: 41.042/41.042 41.042/41.042 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 41.042/41.042 Confluence Problem: 41.042/41.042 (VAR x) 41.042/41.042 (REPLACEMENT-MAP 41.042/41.042 (even 1) 41.042/41.042 (odd 1) 41.042/41.042 (0) 41.042/41.042 (fSNonEmpty) 41.042/41.042 (false) 41.042/41.042 (s 1) 41.042/41.042 (true) 41.042/41.042 ) 41.042/41.042 (RULES 41.042/41.042 even(0) -> true 41.042/41.042 even(s(x)) -> false | odd(x) ->* false 41.042/41.042 even(s(x)) -> true | odd(x) ->* true 41.042/41.042 odd(0) -> false 41.042/41.042 odd(s(x)) -> false | even(x) ->* false 41.042/41.042 odd(s(x)) -> true | even(x) ->* true 41.042/41.042 ) 41.042/41.042 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 41.042/41.042 41.042/41.042 CRule InfChecker Info: 41.042/41.042 even(0) -> true 41.042/41.042 Rule remains 41.042/41.042 Proof: 41.042/41.042 NO_CONDS 41.042/41.042 41.042/41.042 CRule InfChecker Info: 41.042/41.042 even(s(x)) -> false | odd(x) ->* false 41.042/41.042 Rule remains 41.042/41.042 Proof: 41.042/41.042 NO 41.042/41.042 41.042/41.042 Problem 1: 41.042/41.042 41.042/41.042 Infeasibility Problem: 41.042/41.042 [(VAR vNonEmpty x vNonEmpty x) 41.042/41.042 (STRATEGY CONTEXTSENSITIVE 41.042/41.042 (even 1) 41.042/41.042 (odd 1) 41.042/41.042 (0) 41.042/41.042 (fSNonEmpty) 41.042/41.042 (false) 41.042/41.042 (s 1) 41.042/41.042 (true) 41.042/41.042 ) 41.042/41.042 (RULES 41.042/41.042 even(0) -> true 41.042/41.042 even(s(x)) -> false | odd(x) ->* false 41.042/41.042 even(s(x)) -> true | odd(x) ->* true 41.042/41.042 odd(0) -> false 41.042/41.042 odd(s(x)) -> false | even(x) ->* false 41.042/41.042 odd(s(x)) -> true | even(x) ->* true 41.042/41.042 )] 41.042/41.042 41.042/41.042 Infeasibility Conditions: 41.042/41.042 odd(x) ->* false 41.042/41.042 41.042/41.042 Problem 1: 41.042/41.042 41.042/41.042 Obtaining a proof using Prover9: 41.042/41.042 41.042/41.042 -> Prover9 Output: 41.042/41.042 ============================== Prover9 =============================== 41.042/41.042 Prover9 (64) version 2009-11A, November 2009. 41.042/41.042 Process 14053 was started by ubuntu on ubuntu, 41.042/41.042 Wed Mar 9 09:27:25 2022 41.042/41.042 The command was "./prover9 -f /tmp/prover914044-0.in". 41.042/41.042 ============================== end of head =========================== 41.042/41.042 41.042/41.042 ============================== INPUT ================================= 41.042/41.042 41.042/41.042 % Reading from file /tmp/prover914044-0.in 41.042/41.042 41.042/41.042 assign(max_seconds,20). 41.042/41.042 41.042/41.042 formulas(assumptions). 41.042/41.042 ->_s0(x1,y) -> ->_s0(even(x1),even(y)) # label(congruence). 41.042/41.042 ->_s0(x1,y) -> ->_s0(odd(x1),odd(y)) # label(congruence). 41.042/41.042 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence). 41.042/41.042 ->_s0(even(0),true) # label(replacement). 41.042/41.042 ->*_s0(odd(x1),false) -> ->_s0(even(s(x1)),false) # label(replacement). 41.042/41.042 ->*_s0(odd(x1),true) -> ->_s0(even(s(x1)),true) # label(replacement). 41.042/41.042 ->_s0(odd(0),false) # label(replacement). 41.042/41.042 ->*_s0(even(x1),false) -> ->_s0(odd(s(x1)),false) # label(replacement). 41.042/41.042 ->*_s0(even(x1),true) -> ->_s0(odd(s(x1)),true) # label(replacement). 41.042/41.042 ->*_s0(x,x) # label(reflexivity). 41.042/41.042 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 formulas(goals). 41.042/41.042 (exists x3 ->*_s0(odd(x3),false)) # label(goal). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 ============================== end of input ========================== 41.042/41.042 41.042/41.042 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 41.042/41.042 41.042/41.042 % Formulas that are not ordinary clauses: 41.042/41.042 1 ->_s0(x1,y) -> ->_s0(even(x1),even(y)) # label(congruence) # label(non_clause). [assumption]. 41.042/41.042 2 ->_s0(x1,y) -> ->_s0(odd(x1),odd(y)) # label(congruence) # label(non_clause). [assumption]. 41.042/41.042 3 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 41.042/41.042 4 ->*_s0(odd(x1),false) -> ->_s0(even(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 5 ->*_s0(odd(x1),true) -> ->_s0(even(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 6 ->*_s0(even(x1),false) -> ->_s0(odd(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 7 ->*_s0(even(x1),true) -> ->_s0(odd(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 8 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 41.042/41.042 9 (exists x3 ->*_s0(odd(x3),false)) # label(goal) # label(non_clause) # label(goal). [goal]. 41.042/41.042 41.042/41.042 ============================== end of process non-clausal formulas === 41.042/41.042 41.042/41.042 ============================== PROCESS INITIAL CLAUSES =============== 41.042/41.042 41.042/41.042 % Clauses before input processing: 41.042/41.042 41.042/41.042 formulas(usable). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 formulas(sos). 41.042/41.042 -->_s0(x,y) | ->_s0(even(x),even(y)) # label(congruence). [clausify(1)]. 41.042/41.042 -->_s0(x,y) | ->_s0(odd(x),odd(y)) # label(congruence). [clausify(2)]. 41.042/41.042 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.042/41.042 ->_s0(even(0),true) # label(replacement). [assumption]. 41.042/41.042 -->*_s0(odd(x),false) | ->_s0(even(s(x)),false) # label(replacement). [clausify(4)]. 41.042/41.042 -->*_s0(odd(x),true) | ->_s0(even(s(x)),true) # label(replacement). [clausify(5)]. 41.042/41.042 ->_s0(odd(0),false) # label(replacement). [assumption]. 41.042/41.042 -->*_s0(even(x),false) | ->_s0(odd(s(x)),false) # label(replacement). [clausify(6)]. 41.042/41.042 -->*_s0(even(x),true) | ->_s0(odd(s(x)),true) # label(replacement). [clausify(7)]. 41.042/41.042 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.042/41.042 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.042/41.042 -->*_s0(odd(x),false) # label(goal). [deny(9)]. 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 formulas(demodulators). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 ============================== PREDICATE ELIMINATION ================= 41.042/41.042 41.042/41.042 No predicates eliminated. 41.042/41.042 41.042/41.042 ============================== end predicate elimination ============= 41.042/41.042 41.042/41.042 Auto_denials: 41.042/41.042 % copying label goal to answer in negative clause 41.042/41.042 41.042/41.042 Term ordering decisions: 41.042/41.042 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 41.042/41.042 Function symbol precedence: function_order([ false, true, 0, even, odd, s ]). 41.042/41.042 After inverse_order: (no changes). 41.042/41.042 Unfolding symbols: (none). 41.042/41.042 41.042/41.042 Auto_inference settings: 41.042/41.042 % set(neg_binary_resolution). % (HNE depth_diff=-7) 41.042/41.042 % clear(ordered_res). % (HNE depth_diff=-7) 41.042/41.042 % set(ur_resolution). % (HNE depth_diff=-7) 41.042/41.042 % set(ur_resolution) -> set(pos_ur_resolution). 41.042/41.042 % set(ur_resolution) -> set(neg_ur_resolution). 41.042/41.042 41.042/41.042 Auto_process settings: (no changes). 41.042/41.042 41.042/41.042 kept: 10 -->_s0(x,y) | ->_s0(even(x),even(y)) # label(congruence). [clausify(1)]. 41.042/41.042 kept: 11 -->_s0(x,y) | ->_s0(odd(x),odd(y)) # label(congruence). [clausify(2)]. 41.042/41.042 kept: 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.042/41.042 kept: 13 ->_s0(even(0),true) # label(replacement). [assumption]. 41.042/41.042 kept: 14 -->*_s0(odd(x),false) | ->_s0(even(s(x)),false) # label(replacement). [clausify(4)]. 41.042/41.042 kept: 15 -->*_s0(odd(x),true) | ->_s0(even(s(x)),true) # label(replacement). [clausify(5)]. 41.042/41.042 kept: 16 ->_s0(odd(0),false) # label(replacement). [assumption]. 41.042/41.042 kept: 17 -->*_s0(even(x),false) | ->_s0(odd(s(x)),false) # label(replacement). [clausify(6)]. 41.042/41.042 kept: 18 -->*_s0(even(x),true) | ->_s0(odd(s(x)),true) # label(replacement). [clausify(7)]. 41.042/41.042 kept: 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.042/41.042 kept: 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.042/41.042 kept: 21 -->*_s0(odd(x),false) # label(goal) # answer(goal). [deny(9)]. 41.042/41.042 41.042/41.042 ============================== end of process initial clauses ======== 41.042/41.042 41.042/41.042 ============================== CLAUSES FOR SEARCH ==================== 41.042/41.042 41.042/41.042 % Clauses after input processing: 41.042/41.042 41.042/41.042 formulas(usable). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 formulas(sos). 41.042/41.042 10 -->_s0(x,y) | ->_s0(even(x),even(y)) # label(congruence). [clausify(1)]. 41.042/41.042 11 -->_s0(x,y) | ->_s0(odd(x),odd(y)) # label(congruence). [clausify(2)]. 41.042/41.042 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.042/41.042 13 ->_s0(even(0),true) # label(replacement). [assumption]. 41.042/41.042 15 -->*_s0(odd(x),true) | ->_s0(even(s(x)),true) # label(replacement). [clausify(5)]. 41.042/41.042 16 ->_s0(odd(0),false) # label(replacement). [assumption]. 41.042/41.042 17 -->*_s0(even(x),false) | ->_s0(odd(s(x)),false) # label(replacement). [clausify(6)]. 41.042/41.042 18 -->*_s0(even(x),true) | ->_s0(odd(s(x)),true) # label(replacement). [clausify(7)]. 41.042/41.042 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.042/41.042 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.042/41.042 21 -->*_s0(odd(x),false) # label(goal) # answer(goal). [deny(9)]. 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 formulas(demodulators). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 ============================== end of clauses for search ============= 41.042/41.042 41.042/41.042 ============================== SEARCH ================================ 41.042/41.042 41.042/41.042 % Starting search at 0.00 seconds. 41.042/41.042 41.042/41.042 given #1 (I,wt=8): 10 -->_s0(x,y) | ->_s0(even(x),even(y)) # label(congruence). [clausify(1)]. 41.042/41.042 41.042/41.042 given #2 (I,wt=8): 11 -->_s0(x,y) | ->_s0(odd(x),odd(y)) # label(congruence). [clausify(2)]. 41.042/41.042 41.042/41.042 given #3 (I,wt=8): 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.042/41.042 41.042/41.042 given #4 (I,wt=4): 13 ->_s0(even(0),true) # label(replacement). [assumption]. 41.042/41.042 41.042/41.042 given #5 (I,wt=9): 15 -->*_s0(odd(x),true) | ->_s0(even(s(x)),true) # label(replacement). [clausify(5)]. 41.042/41.042 41.042/41.042 given #6 (I,wt=4): 16 ->_s0(odd(0),false) # label(replacement). [assumption]. 41.042/41.042 41.042/41.042 given #7 (I,wt=9): 17 -->*_s0(even(x),false) | ->_s0(odd(s(x)),false) # label(replacement). [clausify(6)]. 41.042/41.042 41.042/41.042 given #8 (I,wt=9): 18 -->*_s0(even(x),true) | ->_s0(odd(s(x)),true) # label(replacement). [clausify(7)]. 41.042/41.042 41.042/41.042 given #9 (I,wt=3): 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.042/41.042 41.042/41.042 given #10 (I,wt=9): 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.042/41.042 41.042/41.042 ============================== PROOF ================================= 41.042/41.042 41.042/41.042 % Proof 1 at 0.00 (+ 0.00) seconds: goal. 41.042/41.042 % Length of proof is 8. 41.042/41.042 % Level of proof is 3. 41.042/41.042 % Maximum clause weight is 9.000. 41.042/41.042 % Given clauses 10. 41.042/41.042 41.042/41.042 8 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 41.042/41.042 9 (exists x3 ->*_s0(odd(x3),false)) # label(goal) # label(non_clause) # label(goal). [goal]. 41.042/41.042 16 ->_s0(odd(0),false) # label(replacement). [assumption]. 41.042/41.042 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.042/41.042 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.042/41.042 21 -->*_s0(odd(x),false) # label(goal) # answer(goal). [deny(9)]. 41.042/41.042 28 ->*_s0(odd(0),false). [ur(20,a,16,a,b,19,a)]. 41.042/41.042 29 $F # answer(goal). [resolve(28,a,21,a)]. 41.042/41.042 41.042/41.042 ============================== end of proof ========================== 41.042/41.042 41.042/41.042 ============================== STATISTICS ============================ 41.042/41.042 41.042/41.042 Given=10. Generated=19. Kept=19. proofs=1. 41.042/41.042 Usable=10. Sos=7. Demods=0. Limbo=0, Disabled=13. Hints=0. 41.042/41.042 Kept_by_rule=0, Deleted_by_rule=0. 41.042/41.042 Forward_subsumed=0. Back_subsumed=1. 41.042/41.042 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 41.042/41.042 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 41.042/41.042 Demod_attempts=0. Demod_rewrites=0. 41.042/41.042 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 41.042/41.042 Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=10. 41.042/41.042 Megabytes=0.07. 41.042/41.042 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 41.042/41.042 41.042/41.042 ============================== end of statistics ===================== 41.042/41.042 41.042/41.042 ============================== end of search ========================= 41.042/41.042 41.042/41.042 THEOREM PROVED 41.042/41.042 41.042/41.042 Exiting with 1 proof. 41.042/41.042 41.042/41.042 Process 14053 exit (max_proofs) Wed Mar 9 09:27:25 2022 41.042/41.042 41.042/41.042 41.042/41.042 The problem is feasible. 41.042/41.042 41.042/41.042 41.042/41.042 CRule InfChecker Info: 41.042/41.042 even(s(x)) -> true | odd(x) ->* true 41.042/41.042 Rule remains 41.042/41.042 Proof: 41.042/41.042 NO 41.042/41.042 41.042/41.042 Problem 1: 41.042/41.042 41.042/41.042 Infeasibility Problem: 41.042/41.042 [(VAR vNonEmpty x vNonEmpty x) 41.042/41.042 (STRATEGY CONTEXTSENSITIVE 41.042/41.042 (even 1) 41.042/41.042 (odd 1) 41.042/41.042 (0) 41.042/41.042 (fSNonEmpty) 41.042/41.042 (false) 41.042/41.042 (s 1) 41.042/41.042 (true) 41.042/41.042 ) 41.042/41.042 (RULES 41.042/41.042 even(0) -> true 41.042/41.042 even(s(x)) -> false | odd(x) ->* false 41.042/41.042 even(s(x)) -> true | odd(x) ->* true 41.042/41.042 odd(0) -> false 41.042/41.042 odd(s(x)) -> false | even(x) ->* false 41.042/41.042 odd(s(x)) -> true | even(x) ->* true 41.042/41.042 )] 41.042/41.042 41.042/41.042 Infeasibility Conditions: 41.042/41.042 odd(x) ->* true 41.042/41.042 41.042/41.042 Problem 1: 41.042/41.042 41.042/41.042 Obtaining a proof using Prover9: 41.042/41.042 41.042/41.042 -> Prover9 Output: 41.042/41.042 ============================== Prover9 =============================== 41.042/41.042 Prover9 (64) version 2009-11A, November 2009. 41.042/41.042 Process 14076 was started by ubuntu on ubuntu, 41.042/41.042 Wed Mar 9 09:27:25 2022 41.042/41.042 The command was "./prover9 -f /tmp/prover914065-0.in". 41.042/41.042 ============================== end of head =========================== 41.042/41.042 41.042/41.042 ============================== INPUT ================================= 41.042/41.042 41.042/41.042 % Reading from file /tmp/prover914065-0.in 41.042/41.042 41.042/41.042 assign(max_seconds,20). 41.042/41.042 41.042/41.042 formulas(assumptions). 41.042/41.042 ->_s0(x1,y) -> ->_s0(even(x1),even(y)) # label(congruence). 41.042/41.042 ->_s0(x1,y) -> ->_s0(odd(x1),odd(y)) # label(congruence). 41.042/41.042 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence). 41.042/41.042 ->_s0(even(0),true) # label(replacement). 41.042/41.042 ->*_s0(odd(x1),false) -> ->_s0(even(s(x1)),false) # label(replacement). 41.042/41.042 ->*_s0(odd(x1),true) -> ->_s0(even(s(x1)),true) # label(replacement). 41.042/41.042 ->_s0(odd(0),false) # label(replacement). 41.042/41.042 ->*_s0(even(x1),false) -> ->_s0(odd(s(x1)),false) # label(replacement). 41.042/41.042 ->*_s0(even(x1),true) -> ->_s0(odd(s(x1)),true) # label(replacement). 41.042/41.042 ->*_s0(x,x) # label(reflexivity). 41.042/41.042 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 formulas(goals). 41.042/41.042 (exists x3 ->*_s0(odd(x3),true)) # label(goal). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 ============================== end of input ========================== 41.042/41.042 41.042/41.042 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 41.042/41.042 41.042/41.042 % Formulas that are not ordinary clauses: 41.042/41.042 1 ->_s0(x1,y) -> ->_s0(even(x1),even(y)) # label(congruence) # label(non_clause). [assumption]. 41.042/41.042 2 ->_s0(x1,y) -> ->_s0(odd(x1),odd(y)) # label(congruence) # label(non_clause). [assumption]. 41.042/41.042 3 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 41.042/41.042 4 ->*_s0(odd(x1),false) -> ->_s0(even(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 5 ->*_s0(odd(x1),true) -> ->_s0(even(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 6 ->*_s0(even(x1),false) -> ->_s0(odd(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 7 ->*_s0(even(x1),true) -> ->_s0(odd(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 8 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 41.042/41.042 9 (exists x3 ->*_s0(odd(x3),true)) # label(goal) # label(non_clause) # label(goal). [goal]. 41.042/41.042 41.042/41.042 ============================== end of process non-clausal formulas === 41.042/41.042 41.042/41.042 ============================== PROCESS INITIAL CLAUSES =============== 41.042/41.042 41.042/41.042 % Clauses before input processing: 41.042/41.042 41.042/41.042 formulas(usable). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 formulas(sos). 41.042/41.042 -->_s0(x,y) | ->_s0(even(x),even(y)) # label(congruence). [clausify(1)]. 41.042/41.042 -->_s0(x,y) | ->_s0(odd(x),odd(y)) # label(congruence). [clausify(2)]. 41.042/41.042 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.042/41.042 ->_s0(even(0),true) # label(replacement). [assumption]. 41.042/41.042 -->*_s0(odd(x),false) | ->_s0(even(s(x)),false) # label(replacement). [clausify(4)]. 41.042/41.042 -->*_s0(odd(x),true) | ->_s0(even(s(x)),true) # label(replacement). [clausify(5)]. 41.042/41.042 ->_s0(odd(0),false) # label(replacement). [assumption]. 41.042/41.042 -->*_s0(even(x),false) | ->_s0(odd(s(x)),false) # label(replacement). [clausify(6)]. 41.042/41.042 -->*_s0(even(x),true) | ->_s0(odd(s(x)),true) # label(replacement). [clausify(7)]. 41.042/41.042 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.042/41.042 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.042/41.042 -->*_s0(odd(x),true) # label(goal). [deny(9)]. 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 formulas(demodulators). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 ============================== PREDICATE ELIMINATION ================= 41.042/41.042 41.042/41.042 No predicates eliminated. 41.042/41.042 41.042/41.042 ============================== end predicate elimination ============= 41.042/41.042 41.042/41.042 Auto_denials: 41.042/41.042 % copying label goal to answer in negative clause 41.042/41.042 41.042/41.042 Term ordering decisions: 41.042/41.042 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 41.042/41.042 Function symbol precedence: function_order([ false, true, 0, even, odd, s ]). 41.042/41.042 After inverse_order: (no changes). 41.042/41.042 Unfolding symbols: (none). 41.042/41.042 41.042/41.042 Auto_inference settings: 41.042/41.042 % set(neg_binary_resolution). % (HNE depth_diff=-7) 41.042/41.042 % clear(ordered_res). % (HNE depth_diff=-7) 41.042/41.042 % set(ur_resolution). % (HNE depth_diff=-7) 41.042/41.042 % set(ur_resolution) -> set(pos_ur_resolution). 41.042/41.042 % set(ur_resolution) -> set(neg_ur_resolution). 41.042/41.042 41.042/41.042 Auto_process settings: (no changes). 41.042/41.042 41.042/41.042 kept: 10 -->_s0(x,y) | ->_s0(even(x),even(y)) # label(congruence). [clausify(1)]. 41.042/41.042 kept: 11 -->_s0(x,y) | ->_s0(odd(x),odd(y)) # label(congruence). [clausify(2)]. 41.042/41.042 kept: 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.042/41.042 kept: 13 ->_s0(even(0),true) # label(replacement). [assumption]. 41.042/41.042 kept: 14 -->*_s0(odd(x),false) | ->_s0(even(s(x)),false) # label(replacement). [clausify(4)]. 41.042/41.042 kept: 15 -->*_s0(odd(x),true) | ->_s0(even(s(x)),true) # label(replacement). [clausify(5)]. 41.042/41.042 kept: 16 ->_s0(odd(0),false) # label(replacement). [assumption]. 41.042/41.042 kept: 17 -->*_s0(even(x),false) | ->_s0(odd(s(x)),false) # label(replacement). [clausify(6)]. 41.042/41.042 kept: 18 -->*_s0(even(x),true) | ->_s0(odd(s(x)),true) # label(replacement). [clausify(7)]. 41.042/41.042 kept: 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.042/41.042 kept: 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.042/41.042 kept: 21 -->*_s0(odd(x),true) # label(goal) # answer(goal). [deny(9)]. 41.042/41.042 41.042/41.042 ============================== end of process initial clauses ======== 41.042/41.042 41.042/41.042 ============================== CLAUSES FOR SEARCH ==================== 41.042/41.042 41.042/41.042 % Clauses after input processing: 41.042/41.042 41.042/41.042 formulas(usable). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 formulas(sos). 41.042/41.042 10 -->_s0(x,y) | ->_s0(even(x),even(y)) # label(congruence). [clausify(1)]. 41.042/41.042 11 -->_s0(x,y) | ->_s0(odd(x),odd(y)) # label(congruence). [clausify(2)]. 41.042/41.042 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.042/41.042 13 ->_s0(even(0),true) # label(replacement). [assumption]. 41.042/41.042 14 -->*_s0(odd(x),false) | ->_s0(even(s(x)),false) # label(replacement). [clausify(4)]. 41.042/41.042 16 ->_s0(odd(0),false) # label(replacement). [assumption]. 41.042/41.042 17 -->*_s0(even(x),false) | ->_s0(odd(s(x)),false) # label(replacement). [clausify(6)]. 41.042/41.042 18 -->*_s0(even(x),true) | ->_s0(odd(s(x)),true) # label(replacement). [clausify(7)]. 41.042/41.042 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.042/41.042 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.042/41.042 21 -->*_s0(odd(x),true) # label(goal) # answer(goal). [deny(9)]. 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 formulas(demodulators). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 ============================== end of clauses for search ============= 41.042/41.042 41.042/41.042 ============================== SEARCH ================================ 41.042/41.042 41.042/41.042 % Starting search at 0.00 seconds. 41.042/41.042 41.042/41.042 given #1 (I,wt=8): 10 -->_s0(x,y) | ->_s0(even(x),even(y)) # label(congruence). [clausify(1)]. 41.042/41.042 41.042/41.042 given #2 (I,wt=8): 11 -->_s0(x,y) | ->_s0(odd(x),odd(y)) # label(congruence). [clausify(2)]. 41.042/41.042 41.042/41.042 given #3 (I,wt=8): 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.042/41.042 41.042/41.042 given #4 (I,wt=4): 13 ->_s0(even(0),true) # label(replacement). [assumption]. 41.042/41.042 41.042/41.042 given #5 (I,wt=9): 14 -->*_s0(odd(x),false) | ->_s0(even(s(x)),false) # label(replacement). [clausify(4)]. 41.042/41.042 41.042/41.042 given #6 (I,wt=4): 16 ->_s0(odd(0),false) # label(replacement). [assumption]. 41.042/41.042 41.042/41.042 given #7 (I,wt=9): 17 -->*_s0(even(x),false) | ->_s0(odd(s(x)),false) # label(replacement). [clausify(6)]. 41.042/41.042 41.042/41.042 given #8 (I,wt=9): 18 -->*_s0(even(x),true) | ->_s0(odd(s(x)),true) # label(replacement). [clausify(7)]. 41.042/41.042 41.042/41.042 given #9 (I,wt=3): 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.042/41.042 41.042/41.042 given #10 (I,wt=9): 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.042/41.042 41.042/41.042 given #11 (I,wt=4): 21 -->*_s0(odd(x),true) # label(goal) # answer(goal). [deny(9)]. 41.042/41.042 41.042/41.042 given #12 (A,wt=6): 22 ->_s0(s(even(0)),s(true)). [ur(12,a,13,a)]. 41.042/41.042 41.042/41.042 given #13 (F,wt=3): 32 -->*_s0(false,true) # answer(goal). [ur(20,a,16,a,c,21,a)]. 41.042/41.042 41.042/41.042 given #14 (F,wt=3): 38 -->_s0(false,true) # answer(goal). [ur(20,b,19,a,c,32,a)]. 41.042/41.042 41.042/41.042 given #15 (F,wt=4): 31 -->_s0(odd(x),true) # answer(goal). [ur(20,b,19,a,c,21,a)]. 41.042/41.042 41.042/41.042 ============================== PROOF ================================= 41.042/41.042 41.042/41.042 % Proof 1 at 0.00 (+ 0.00) seconds: goal. 41.042/41.042 % Length of proof is 12. 41.042/41.042 % Level of proof is 4. 41.042/41.042 % Maximum clause weight is 9.000. 41.042/41.042 % Given clauses 15. 41.042/41.042 41.042/41.042 7 ->*_s0(even(x1),true) -> ->_s0(odd(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 8 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 41.042/41.042 9 (exists x3 ->*_s0(odd(x3),true)) # label(goal) # label(non_clause) # label(goal). [goal]. 41.042/41.042 13 ->_s0(even(0),true) # label(replacement). [assumption]. 41.042/41.042 18 -->*_s0(even(x),true) | ->_s0(odd(s(x)),true) # label(replacement). [clausify(7)]. 41.042/41.042 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.042/41.042 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.042/41.042 21 -->*_s0(odd(x),true) # label(goal) # answer(goal). [deny(9)]. 41.042/41.042 29 ->*_s0(even(0),true). [ur(20,a,13,a,b,19,a)]. 41.042/41.042 31 -->_s0(odd(x),true) # answer(goal). [ur(20,b,19,a,c,21,a)]. 41.042/41.042 39 -->*_s0(even(x),true) # answer(goal). [resolve(31,a,18,b)]. 41.042/41.042 40 $F # answer(goal). [resolve(39,a,29,a)]. 41.042/41.042 41.042/41.042 ============================== end of proof ========================== 41.042/41.042 41.042/41.042 ============================== STATISTICS ============================ 41.042/41.042 41.042/41.042 Given=15. Generated=30. Kept=30. proofs=1. 41.042/41.042 Usable=15. Sos=13. Demods=0. Limbo=0, Disabled=13. Hints=0. 41.042/41.042 Kept_by_rule=0, Deleted_by_rule=0. 41.042/41.042 Forward_subsumed=0. Back_subsumed=1. 41.042/41.042 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 41.042/41.042 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 41.042/41.042 Demod_attempts=0. Demod_rewrites=0. 41.042/41.042 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 41.042/41.042 Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=14. 41.042/41.042 Megabytes=0.09. 41.042/41.042 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 41.042/41.042 41.042/41.042 ============================== end of statistics ===================== 41.042/41.042 41.042/41.042 ============================== end of search ========================= 41.042/41.042 41.042/41.042 THEOREM PROVED 41.042/41.042 41.042/41.042 Exiting with 1 proof. 41.042/41.042 41.042/41.042 Process 14076 exit (max_proofs) Wed Mar 9 09:27:25 2022 41.042/41.042 41.042/41.042 41.042/41.042 The problem is feasible. 41.042/41.042 41.042/41.042 41.042/41.042 CRule InfChecker Info: 41.042/41.042 odd(0) -> false 41.042/41.042 Rule remains 41.042/41.042 Proof: 41.042/41.042 NO_CONDS 41.042/41.042 41.042/41.042 CRule InfChecker Info: 41.042/41.042 odd(s(x)) -> false | even(x) ->* false 41.042/41.042 Rule remains 41.042/41.042 Proof: 41.042/41.042 NO 41.042/41.042 41.042/41.042 Problem 1: 41.042/41.042 41.042/41.042 Infeasibility Problem: 41.042/41.042 [(VAR vNonEmpty x vNonEmpty x) 41.042/41.042 (STRATEGY CONTEXTSENSITIVE 41.042/41.042 (even 1) 41.042/41.042 (odd 1) 41.042/41.042 (0) 41.042/41.042 (fSNonEmpty) 41.042/41.042 (false) 41.042/41.042 (s 1) 41.042/41.042 (true) 41.042/41.042 ) 41.042/41.042 (RULES 41.042/41.042 even(0) -> true 41.042/41.042 even(s(x)) -> false | odd(x) ->* false 41.042/41.042 even(s(x)) -> true | odd(x) ->* true 41.042/41.042 odd(0) -> false 41.042/41.042 odd(s(x)) -> false | even(x) ->* false 41.042/41.042 odd(s(x)) -> true | even(x) ->* true 41.042/41.042 )] 41.042/41.042 41.042/41.042 Infeasibility Conditions: 41.042/41.042 even(x) ->* false 41.042/41.042 41.042/41.042 Problem 1: 41.042/41.042 41.042/41.042 Obtaining a proof using Prover9: 41.042/41.042 41.042/41.042 -> Prover9 Output: 41.042/41.042 ============================== Prover9 =============================== 41.042/41.042 Prover9 (64) version 2009-11A, November 2009. 41.042/41.042 Process 14097 was started by ubuntu on ubuntu, 41.042/41.042 Wed Mar 9 09:27:25 2022 41.042/41.042 The command was "./prover9 -f /tmp/prover914088-0.in". 41.042/41.042 ============================== end of head =========================== 41.042/41.042 41.042/41.042 ============================== INPUT ================================= 41.042/41.042 41.042/41.042 % Reading from file /tmp/prover914088-0.in 41.042/41.042 41.042/41.042 assign(max_seconds,20). 41.042/41.042 41.042/41.042 formulas(assumptions). 41.042/41.042 ->_s0(x1,y) -> ->_s0(even(x1),even(y)) # label(congruence). 41.042/41.042 ->_s0(x1,y) -> ->_s0(odd(x1),odd(y)) # label(congruence). 41.042/41.042 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence). 41.042/41.042 ->_s0(even(0),true) # label(replacement). 41.042/41.042 ->*_s0(odd(x1),false) -> ->_s0(even(s(x1)),false) # label(replacement). 41.042/41.042 ->*_s0(odd(x1),true) -> ->_s0(even(s(x1)),true) # label(replacement). 41.042/41.042 ->_s0(odd(0),false) # label(replacement). 41.042/41.042 ->*_s0(even(x1),false) -> ->_s0(odd(s(x1)),false) # label(replacement). 41.042/41.042 ->*_s0(even(x1),true) -> ->_s0(odd(s(x1)),true) # label(replacement). 41.042/41.042 ->*_s0(x,x) # label(reflexivity). 41.042/41.042 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 formulas(goals). 41.042/41.042 (exists x3 ->*_s0(even(x3),false)) # label(goal). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 ============================== end of input ========================== 41.042/41.042 41.042/41.042 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 41.042/41.042 41.042/41.042 % Formulas that are not ordinary clauses: 41.042/41.042 1 ->_s0(x1,y) -> ->_s0(even(x1),even(y)) # label(congruence) # label(non_clause). [assumption]. 41.042/41.042 2 ->_s0(x1,y) -> ->_s0(odd(x1),odd(y)) # label(congruence) # label(non_clause). [assumption]. 41.042/41.042 3 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 41.042/41.042 4 ->*_s0(odd(x1),false) -> ->_s0(even(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 5 ->*_s0(odd(x1),true) -> ->_s0(even(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 6 ->*_s0(even(x1),false) -> ->_s0(odd(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 7 ->*_s0(even(x1),true) -> ->_s0(odd(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 8 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 41.042/41.042 9 (exists x3 ->*_s0(even(x3),false)) # label(goal) # label(non_clause) # label(goal). [goal]. 41.042/41.042 41.042/41.042 ============================== end of process non-clausal formulas === 41.042/41.042 41.042/41.042 ============================== PROCESS INITIAL CLAUSES =============== 41.042/41.042 41.042/41.042 % Clauses before input processing: 41.042/41.042 41.042/41.042 formulas(usable). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 formulas(sos). 41.042/41.042 -->_s0(x,y) | ->_s0(even(x),even(y)) # label(congruence). [clausify(1)]. 41.042/41.042 -->_s0(x,y) | ->_s0(odd(x),odd(y)) # label(congruence). [clausify(2)]. 41.042/41.042 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.042/41.042 ->_s0(even(0),true) # label(replacement). [assumption]. 41.042/41.042 -->*_s0(odd(x),false) | ->_s0(even(s(x)),false) # label(replacement). [clausify(4)]. 41.042/41.042 -->*_s0(odd(x),true) | ->_s0(even(s(x)),true) # label(replacement). [clausify(5)]. 41.042/41.042 ->_s0(odd(0),false) # label(replacement). [assumption]. 41.042/41.042 -->*_s0(even(x),false) | ->_s0(odd(s(x)),false) # label(replacement). [clausify(6)]. 41.042/41.042 -->*_s0(even(x),true) | ->_s0(odd(s(x)),true) # label(replacement). [clausify(7)]. 41.042/41.042 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.042/41.042 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.042/41.042 -->*_s0(even(x),false) # label(goal). [deny(9)]. 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 formulas(demodulators). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 ============================== PREDICATE ELIMINATION ================= 41.042/41.042 41.042/41.042 No predicates eliminated. 41.042/41.042 41.042/41.042 ============================== end predicate elimination ============= 41.042/41.042 41.042/41.042 Auto_denials: 41.042/41.042 % copying label goal to answer in negative clause 41.042/41.042 41.042/41.042 Term ordering decisions: 41.042/41.042 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 41.042/41.042 Function symbol precedence: function_order([ false, true, 0, even, odd, s ]). 41.042/41.042 After inverse_order: (no changes). 41.042/41.042 Unfolding symbols: (none). 41.042/41.042 41.042/41.042 Auto_inference settings: 41.042/41.042 % set(neg_binary_resolution). % (HNE depth_diff=-7) 41.042/41.042 % clear(ordered_res). % (HNE depth_diff=-7) 41.042/41.042 % set(ur_resolution). % (HNE depth_diff=-7) 41.042/41.042 % set(ur_resolution) -> set(pos_ur_resolution). 41.042/41.042 % set(ur_resolution) -> set(neg_ur_resolution). 41.042/41.042 41.042/41.042 Auto_process settings: (no changes). 41.042/41.042 41.042/41.042 kept: 10 -->_s0(x,y) | ->_s0(even(x),even(y)) # label(congruence). [clausify(1)]. 41.042/41.042 kept: 11 -->_s0(x,y) | ->_s0(odd(x),odd(y)) # label(congruence). [clausify(2)]. 41.042/41.042 kept: 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.042/41.042 kept: 13 ->_s0(even(0),true) # label(replacement). [assumption]. 41.042/41.042 kept: 14 -->*_s0(odd(x),false) | ->_s0(even(s(x)),false) # label(replacement). [clausify(4)]. 41.042/41.042 kept: 15 -->*_s0(odd(x),true) | ->_s0(even(s(x)),true) # label(replacement). [clausify(5)]. 41.042/41.042 kept: 16 ->_s0(odd(0),false) # label(replacement). [assumption]. 41.042/41.042 kept: 17 -->*_s0(even(x),false) | ->_s0(odd(s(x)),false) # label(replacement). [clausify(6)]. 41.042/41.042 kept: 18 -->*_s0(even(x),true) | ->_s0(odd(s(x)),true) # label(replacement). [clausify(7)]. 41.042/41.042 kept: 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.042/41.042 kept: 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.042/41.042 kept: 21 -->*_s0(even(x),false) # label(goal) # answer(goal). [deny(9)]. 41.042/41.042 41.042/41.042 ============================== end of process initial clauses ======== 41.042/41.042 41.042/41.042 ============================== CLAUSES FOR SEARCH ==================== 41.042/41.042 41.042/41.042 % Clauses after input processing: 41.042/41.042 41.042/41.042 formulas(usable). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 formulas(sos). 41.042/41.042 10 -->_s0(x,y) | ->_s0(even(x),even(y)) # label(congruence). [clausify(1)]. 41.042/41.042 11 -->_s0(x,y) | ->_s0(odd(x),odd(y)) # label(congruence). [clausify(2)]. 41.042/41.042 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.042/41.042 13 ->_s0(even(0),true) # label(replacement). [assumption]. 41.042/41.042 14 -->*_s0(odd(x),false) | ->_s0(even(s(x)),false) # label(replacement). [clausify(4)]. 41.042/41.042 15 -->*_s0(odd(x),true) | ->_s0(even(s(x)),true) # label(replacement). [clausify(5)]. 41.042/41.042 16 ->_s0(odd(0),false) # label(replacement). [assumption]. 41.042/41.042 18 -->*_s0(even(x),true) | ->_s0(odd(s(x)),true) # label(replacement). [clausify(7)]. 41.042/41.042 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.042/41.042 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.042/41.042 21 -->*_s0(even(x),false) # label(goal) # answer(goal). [deny(9)]. 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 formulas(demodulators). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 ============================== end of clauses for search ============= 41.042/41.042 41.042/41.042 ============================== SEARCH ================================ 41.042/41.042 41.042/41.042 % Starting search at 0.00 seconds. 41.042/41.042 41.042/41.042 given #1 (I,wt=8): 10 -->_s0(x,y) | ->_s0(even(x),even(y)) # label(congruence). [clausify(1)]. 41.042/41.042 41.042/41.042 given #2 (I,wt=8): 11 -->_s0(x,y) | ->_s0(odd(x),odd(y)) # label(congruence). [clausify(2)]. 41.042/41.042 41.042/41.042 given #3 (I,wt=8): 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.042/41.042 41.042/41.042 given #4 (I,wt=4): 13 ->_s0(even(0),true) # label(replacement). [assumption]. 41.042/41.042 41.042/41.042 given #5 (I,wt=9): 14 -->*_s0(odd(x),false) | ->_s0(even(s(x)),false) # label(replacement). [clausify(4)]. 41.042/41.042 41.042/41.042 given #6 (I,wt=9): 15 -->*_s0(odd(x),true) | ->_s0(even(s(x)),true) # label(replacement). [clausify(5)]. 41.042/41.042 41.042/41.042 given #7 (I,wt=4): 16 ->_s0(odd(0),false) # label(replacement). [assumption]. 41.042/41.042 41.042/41.042 given #8 (I,wt=9): 18 -->*_s0(even(x),true) | ->_s0(odd(s(x)),true) # label(replacement). [clausify(7)]. 41.042/41.042 41.042/41.042 given #9 (I,wt=3): 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.042/41.042 41.042/41.042 given #10 (I,wt=9): 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.042/41.042 41.042/41.042 given #11 (I,wt=4): 21 -->*_s0(even(x),false) # label(goal) # answer(goal). [deny(9)]. 41.042/41.042 41.042/41.042 given #12 (A,wt=6): 22 ->_s0(s(even(0)),s(true)). [ur(12,a,13,a)]. 41.042/41.042 41.042/41.042 given #13 (F,wt=3): 32 -->*_s0(true,false) # answer(goal). [ur(20,a,13,a,c,21,a)]. 41.042/41.042 41.042/41.042 given #14 (F,wt=3): 38 -->_s0(true,false) # answer(goal). [ur(20,b,19,a,c,32,a)]. 41.042/41.042 41.042/41.042 given #15 (F,wt=4): 31 -->_s0(even(x),false) # answer(goal). [ur(20,b,19,a,c,21,a)]. 41.042/41.042 41.042/41.042 ============================== PROOF ================================= 41.042/41.042 41.042/41.042 % Proof 1 at 0.00 (+ 0.00) seconds: goal. 41.042/41.042 % Length of proof is 12. 41.042/41.042 % Level of proof is 4. 41.042/41.042 % Maximum clause weight is 9.000. 41.042/41.042 % Given clauses 15. 41.042/41.042 41.042/41.042 4 ->*_s0(odd(x1),false) -> ->_s0(even(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 8 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 41.042/41.042 9 (exists x3 ->*_s0(even(x3),false)) # label(goal) # label(non_clause) # label(goal). [goal]. 41.042/41.042 14 -->*_s0(odd(x),false) | ->_s0(even(s(x)),false) # label(replacement). [clausify(4)]. 41.042/41.042 16 ->_s0(odd(0),false) # label(replacement). [assumption]. 41.042/41.042 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.042/41.042 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.042/41.042 21 -->*_s0(even(x),false) # label(goal) # answer(goal). [deny(9)]. 41.042/41.042 28 ->*_s0(odd(0),false). [ur(20,a,16,a,b,19,a)]. 41.042/41.042 31 -->_s0(even(x),false) # answer(goal). [ur(20,b,19,a,c,21,a)]. 41.042/41.042 39 -->*_s0(odd(x),false) # answer(goal). [resolve(31,a,14,b)]. 41.042/41.042 40 $F # answer(goal). [resolve(39,a,28,a)]. 41.042/41.042 41.042/41.042 ============================== end of proof ========================== 41.042/41.042 41.042/41.042 ============================== STATISTICS ============================ 41.042/41.042 41.042/41.042 Given=15. Generated=30. Kept=30. proofs=1. 41.042/41.042 Usable=15. Sos=13. Demods=0. Limbo=0, Disabled=13. Hints=0. 41.042/41.042 Kept_by_rule=0, Deleted_by_rule=0. 41.042/41.042 Forward_subsumed=0. Back_subsumed=1. 41.042/41.042 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 41.042/41.042 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 41.042/41.042 Demod_attempts=0. Demod_rewrites=0. 41.042/41.042 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 41.042/41.042 Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=14. 41.042/41.042 Megabytes=0.09. 41.042/41.042 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 41.042/41.042 41.042/41.042 ============================== end of statistics ===================== 41.042/41.042 41.042/41.042 ============================== end of search ========================= 41.042/41.042 41.042/41.042 THEOREM PROVED 41.042/41.042 41.042/41.042 Exiting with 1 proof. 41.042/41.042 41.042/41.042 Process 14097 exit (max_proofs) Wed Mar 9 09:27:25 2022 41.042/41.042 41.042/41.042 41.042/41.042 The problem is feasible. 41.042/41.042 41.042/41.042 41.042/41.042 CRule InfChecker Info: 41.042/41.042 odd(s(x)) -> true | even(x) ->* true 41.042/41.042 Rule remains 41.042/41.042 Proof: 41.042/41.042 NO 41.042/41.042 41.042/41.042 Problem 1: 41.042/41.042 41.042/41.042 Infeasibility Problem: 41.042/41.042 [(VAR vNonEmpty x vNonEmpty x) 41.042/41.042 (STRATEGY CONTEXTSENSITIVE 41.042/41.042 (even 1) 41.042/41.042 (odd 1) 41.042/41.042 (0) 41.042/41.042 (fSNonEmpty) 41.042/41.042 (false) 41.042/41.042 (s 1) 41.042/41.042 (true) 41.042/41.042 ) 41.042/41.042 (RULES 41.042/41.042 even(0) -> true 41.042/41.042 even(s(x)) -> false | odd(x) ->* false 41.042/41.042 even(s(x)) -> true | odd(x) ->* true 41.042/41.042 odd(0) -> false 41.042/41.042 odd(s(x)) -> false | even(x) ->* false 41.042/41.042 odd(s(x)) -> true | even(x) ->* true 41.042/41.042 )] 41.042/41.042 41.042/41.042 Infeasibility Conditions: 41.042/41.042 even(x) ->* true 41.042/41.042 41.042/41.042 Problem 1: 41.042/41.042 41.042/41.042 Obtaining a proof using Prover9: 41.042/41.042 41.042/41.042 -> Prover9 Output: 41.042/41.042 ============================== Prover9 =============================== 41.042/41.042 Prover9 (64) version 2009-11A, November 2009. 41.042/41.042 Process 14129 was started by ubuntu on ubuntu, 41.042/41.042 Wed Mar 9 09:27:25 2022 41.042/41.042 The command was "./prover9 -f /tmp/prover914110-0.in". 41.042/41.042 ============================== end of head =========================== 41.042/41.042 41.042/41.042 ============================== INPUT ================================= 41.042/41.042 41.042/41.042 % Reading from file /tmp/prover914110-0.in 41.042/41.042 41.042/41.042 assign(max_seconds,20). 41.042/41.042 41.042/41.042 formulas(assumptions). 41.042/41.042 ->_s0(x1,y) -> ->_s0(even(x1),even(y)) # label(congruence). 41.042/41.042 ->_s0(x1,y) -> ->_s0(odd(x1),odd(y)) # label(congruence). 41.042/41.042 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence). 41.042/41.042 ->_s0(even(0),true) # label(replacement). 41.042/41.042 ->*_s0(odd(x1),false) -> ->_s0(even(s(x1)),false) # label(replacement). 41.042/41.042 ->*_s0(odd(x1),true) -> ->_s0(even(s(x1)),true) # label(replacement). 41.042/41.042 ->_s0(odd(0),false) # label(replacement). 41.042/41.042 ->*_s0(even(x1),false) -> ->_s0(odd(s(x1)),false) # label(replacement). 41.042/41.042 ->*_s0(even(x1),true) -> ->_s0(odd(s(x1)),true) # label(replacement). 41.042/41.042 ->*_s0(x,x) # label(reflexivity). 41.042/41.042 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 formulas(goals). 41.042/41.042 (exists x3 ->*_s0(even(x3),true)) # label(goal). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 ============================== end of input ========================== 41.042/41.042 41.042/41.042 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 41.042/41.042 41.042/41.042 % Formulas that are not ordinary clauses: 41.042/41.042 1 ->_s0(x1,y) -> ->_s0(even(x1),even(y)) # label(congruence) # label(non_clause). [assumption]. 41.042/41.042 2 ->_s0(x1,y) -> ->_s0(odd(x1),odd(y)) # label(congruence) # label(non_clause). [assumption]. 41.042/41.042 3 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 41.042/41.042 4 ->*_s0(odd(x1),false) -> ->_s0(even(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 5 ->*_s0(odd(x1),true) -> ->_s0(even(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 6 ->*_s0(even(x1),false) -> ->_s0(odd(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 7 ->*_s0(even(x1),true) -> ->_s0(odd(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 8 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 41.042/41.042 9 (exists x3 ->*_s0(even(x3),true)) # label(goal) # label(non_clause) # label(goal). [goal]. 41.042/41.042 41.042/41.042 ============================== end of process non-clausal formulas === 41.042/41.042 41.042/41.042 ============================== PROCESS INITIAL CLAUSES =============== 41.042/41.042 41.042/41.042 % Clauses before input processing: 41.042/41.042 41.042/41.042 formulas(usable). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 formulas(sos). 41.042/41.042 -->_s0(x,y) | ->_s0(even(x),even(y)) # label(congruence). [clausify(1)]. 41.042/41.042 -->_s0(x,y) | ->_s0(odd(x),odd(y)) # label(congruence). [clausify(2)]. 41.042/41.042 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.042/41.042 ->_s0(even(0),true) # label(replacement). [assumption]. 41.042/41.042 -->*_s0(odd(x),false) | ->_s0(even(s(x)),false) # label(replacement). [clausify(4)]. 41.042/41.042 -->*_s0(odd(x),true) | ->_s0(even(s(x)),true) # label(replacement). [clausify(5)]. 41.042/41.042 ->_s0(odd(0),false) # label(replacement). [assumption]. 41.042/41.042 -->*_s0(even(x),false) | ->_s0(odd(s(x)),false) # label(replacement). [clausify(6)]. 41.042/41.042 -->*_s0(even(x),true) | ->_s0(odd(s(x)),true) # label(replacement). [clausify(7)]. 41.042/41.042 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.042/41.042 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.042/41.042 -->*_s0(even(x),true) # label(goal). [deny(9)]. 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 formulas(demodulators). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 ============================== PREDICATE ELIMINATION ================= 41.042/41.042 41.042/41.042 No predicates eliminated. 41.042/41.042 41.042/41.042 ============================== end predicate elimination ============= 41.042/41.042 41.042/41.042 Auto_denials: 41.042/41.042 % copying label goal to answer in negative clause 41.042/41.042 41.042/41.042 Term ordering decisions: 41.042/41.042 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 41.042/41.042 Function symbol precedence: function_order([ false, true, 0, even, odd, s ]). 41.042/41.042 After inverse_order: (no changes). 41.042/41.042 Unfolding symbols: (none). 41.042/41.042 41.042/41.042 Auto_inference settings: 41.042/41.042 % set(neg_binary_resolution). % (HNE depth_diff=-7) 41.042/41.042 % clear(ordered_res). % (HNE depth_diff=-7) 41.042/41.042 % set(ur_resolution). % (HNE depth_diff=-7) 41.042/41.042 % set(ur_resolution) -> set(pos_ur_resolution). 41.042/41.042 % set(ur_resolution) -> set(neg_ur_resolution). 41.042/41.042 41.042/41.042 Auto_process settings: (no changes). 41.042/41.042 41.042/41.042 kept: 10 -->_s0(x,y) | ->_s0(even(x),even(y)) # label(congruence). [clausify(1)]. 41.042/41.042 kept: 11 -->_s0(x,y) | ->_s0(odd(x),odd(y)) # label(congruence). [clausify(2)]. 41.042/41.042 kept: 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.042/41.042 kept: 13 ->_s0(even(0),true) # label(replacement). [assumption]. 41.042/41.042 kept: 14 -->*_s0(odd(x),false) | ->_s0(even(s(x)),false) # label(replacement). [clausify(4)]. 41.042/41.042 kept: 15 -->*_s0(odd(x),true) | ->_s0(even(s(x)),true) # label(replacement). [clausify(5)]. 41.042/41.042 kept: 16 ->_s0(odd(0),false) # label(replacement). [assumption]. 41.042/41.042 kept: 17 -->*_s0(even(x),false) | ->_s0(odd(s(x)),false) # label(replacement). [clausify(6)]. 41.042/41.042 kept: 18 -->*_s0(even(x),true) | ->_s0(odd(s(x)),true) # label(replacement). [clausify(7)]. 41.042/41.042 kept: 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.042/41.042 kept: 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.042/41.042 kept: 21 -->*_s0(even(x),true) # label(goal) # answer(goal). [deny(9)]. 41.042/41.042 41.042/41.042 ============================== end of process initial clauses ======== 41.042/41.042 41.042/41.042 ============================== CLAUSES FOR SEARCH ==================== 41.042/41.042 41.042/41.042 % Clauses after input processing: 41.042/41.042 41.042/41.042 formulas(usable). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 formulas(sos). 41.042/41.042 10 -->_s0(x,y) | ->_s0(even(x),even(y)) # label(congruence). [clausify(1)]. 41.042/41.042 11 -->_s0(x,y) | ->_s0(odd(x),odd(y)) # label(congruence). [clausify(2)]. 41.042/41.042 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.042/41.042 13 ->_s0(even(0),true) # label(replacement). [assumption]. 41.042/41.042 14 -->*_s0(odd(x),false) | ->_s0(even(s(x)),false) # label(replacement). [clausify(4)]. 41.042/41.042 15 -->*_s0(odd(x),true) | ->_s0(even(s(x)),true) # label(replacement). [clausify(5)]. 41.042/41.042 16 ->_s0(odd(0),false) # label(replacement). [assumption]. 41.042/41.042 17 -->*_s0(even(x),false) | ->_s0(odd(s(x)),false) # label(replacement). [clausify(6)]. 41.042/41.042 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.042/41.042 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.042/41.042 21 -->*_s0(even(x),true) # label(goal) # answer(goal). [deny(9)]. 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 formulas(demodulators). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 ============================== end of clauses for search ============= 41.042/41.042 41.042/41.042 ============================== SEARCH ================================ 41.042/41.042 41.042/41.042 % Starting search at 0.00 seconds. 41.042/41.042 41.042/41.042 given #1 (I,wt=8): 10 -->_s0(x,y) | ->_s0(even(x),even(y)) # label(congruence). [clausify(1)]. 41.042/41.042 41.042/41.042 given #2 (I,wt=8): 11 -->_s0(x,y) | ->_s0(odd(x),odd(y)) # label(congruence). [clausify(2)]. 41.042/41.042 41.042/41.042 given #3 (I,wt=8): 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.042/41.042 41.042/41.042 given #4 (I,wt=4): 13 ->_s0(even(0),true) # label(replacement). [assumption]. 41.042/41.042 41.042/41.042 given #5 (I,wt=9): 14 -->*_s0(odd(x),false) | ->_s0(even(s(x)),false) # label(replacement). [clausify(4)]. 41.042/41.042 41.042/41.042 given #6 (I,wt=9): 15 -->*_s0(odd(x),true) | ->_s0(even(s(x)),true) # label(replacement). [clausify(5)]. 41.042/41.042 41.042/41.042 given #7 (I,wt=4): 16 ->_s0(odd(0),false) # label(replacement). [assumption]. 41.042/41.042 41.042/41.042 given #8 (I,wt=9): 17 -->*_s0(even(x),false) | ->_s0(odd(s(x)),false) # label(replacement). [clausify(6)]. 41.042/41.042 41.042/41.042 given #9 (I,wt=3): 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.042/41.042 41.042/41.042 given #10 (I,wt=9): 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.042/41.042 41.042/41.042 ============================== PROOF ================================= 41.042/41.042 41.042/41.042 % Proof 1 at 0.00 (+ 0.01) seconds: goal. 41.042/41.042 % Length of proof is 8. 41.042/41.042 % Level of proof is 3. 41.042/41.042 % Maximum clause weight is 9.000. 41.042/41.042 % Given clauses 10. 41.042/41.042 41.042/41.042 8 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 41.042/41.042 9 (exists x3 ->*_s0(even(x3),true)) # label(goal) # label(non_clause) # label(goal). [goal]. 41.042/41.042 13 ->_s0(even(0),true) # label(replacement). [assumption]. 41.042/41.042 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.042/41.042 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.042/41.042 21 -->*_s0(even(x),true) # label(goal) # answer(goal). [deny(9)]. 41.042/41.042 29 ->*_s0(even(0),true). [ur(20,a,13,a,b,19,a)]. 41.042/41.042 30 $F # answer(goal). [resolve(29,a,21,a)]. 41.042/41.042 41.042/41.042 ============================== end of proof ========================== 41.042/41.042 41.042/41.042 ============================== STATISTICS ============================ 41.042/41.042 41.042/41.042 Given=10. Generated=20. Kept=20. proofs=1. 41.042/41.042 Usable=10. Sos=7. Demods=0. Limbo=1, Disabled=13. Hints=0. 41.042/41.042 Kept_by_rule=0, Deleted_by_rule=0. 41.042/41.042 Forward_subsumed=0. Back_subsumed=1. 41.042/41.042 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 41.042/41.042 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 41.042/41.042 Demod_attempts=0. Demod_rewrites=0. 41.042/41.042 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 41.042/41.042 Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=10. 41.042/41.042 Megabytes=0.08. 41.042/41.042 User_CPU=0.00, System_CPU=0.01, Wall_clock=0. 41.042/41.042 41.042/41.042 ============================== end of statistics ===================== 41.042/41.042 41.042/41.042 ============================== end of search ========================= 41.042/41.042 41.042/41.042 THEOREM PROVED 41.042/41.042 41.042/41.042 Exiting with 1 proof. 41.042/41.042 41.042/41.042 Process 14129 exit (max_proofs) Wed Mar 9 09:27:25 2022 41.042/41.042 41.042/41.042 41.042/41.042 The problem is feasible. 41.042/41.042 41.042/41.042 41.042/41.042 Problem 1: 41.042/41.042 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 41.042/41.042 Confluence Problem: 41.042/41.042 (VAR x) 41.042/41.042 (REPLACEMENT-MAP 41.042/41.042 (even 1) 41.042/41.042 (odd 1) 41.042/41.042 (0) 41.042/41.042 (fSNonEmpty) 41.042/41.042 (false) 41.042/41.042 (s 1) 41.042/41.042 (true) 41.042/41.042 ) 41.042/41.042 (RULES 41.042/41.042 even(0) -> true 41.042/41.042 even(s(x)) -> false | odd(x) ->* false 41.042/41.042 even(s(x)) -> true | odd(x) ->* true 41.042/41.042 odd(0) -> false 41.042/41.042 odd(s(x)) -> false | even(x) ->* false 41.042/41.042 odd(s(x)) -> true | even(x) ->* true 41.042/41.042 ) 41.042/41.042 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 41.042/41.042 41.042/41.042 Critical Pairs Processor: 41.042/41.042 -> Rules: 41.042/41.042 even(0) -> true 41.042/41.042 even(s(x)) -> false | odd(x) ->* false 41.042/41.042 even(s(x)) -> true | odd(x) ->* true 41.042/41.042 odd(0) -> false 41.042/41.042 odd(s(x)) -> false | even(x) ->* false 41.042/41.042 odd(s(x)) -> true | even(x) ->* true 41.042/41.042 -> Vars: 41.042/41.042 "x" 41.042/41.042 41.042/41.042 -> Rlps: 41.042/41.042 crule: even(0) -> true, id: 1, possubterms: even(0)-> [], 0-> [1] 41.042/41.042 crule: even(s(x)) -> false | odd(x) ->* false, id: 2, possubterms: even(s(x))-> [], s(x)-> [1] 41.042/41.042 crule: even(s(x)) -> true | odd(x) ->* true, id: 3, possubterms: even(s(x))-> [], s(x)-> [1] 41.042/41.042 crule: odd(0) -> false, id: 4, possubterms: odd(0)-> [], 0-> [1] 41.042/41.042 crule: odd(s(x)) -> false | even(x) ->* false, id: 5, possubterms: odd(s(x))-> [], s(x)-> [1] 41.042/41.042 crule: odd(s(x)) -> true | even(x) ->* true, id: 6, possubterms: odd(s(x))-> [], s(x)-> [1] 41.042/41.042 41.042/41.042 -> Unifications: 41.042/41.042 R3 unifies with R2 at p: [], l: even(s(x)), lp: even(s(x)), conds: {odd(x) ->* true, odd(x') ->* false}, sig: {x -> x'}, l': even(s(x')), r: true, r': false 41.042/41.042 R6 unifies with R5 at p: [], l: odd(s(x)), lp: odd(s(x)), conds: {even(x) ->* true, even(x') ->* false}, sig: {x -> x'}, l': odd(s(x')), r: true, r': false 41.042/41.042 41.042/41.042 -> Critical pairs info: 41.042/41.042 | odd(x') ->* true, odd(x') ->* false => Not trivial, Overlay, NW2, N1 41.042/41.042 | even(x') ->* true, even(x') ->* false => Not trivial, Overlay, NW2, N2 41.042/41.042 41.042/41.042 -> Problem conclusions: 41.042/41.042 Left linear, Right linear, Linear 41.042/41.042 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 41.042/41.042 CTRS Type: 1 41.042/41.042 Deterministic, Strongly deterministic 41.042/41.042 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 41.042/41.042 Maybe right-stable CTRS, Overlay CTRS 41.042/41.042 Maybe normal CTRS, Maybe almost normal CTRS 41.042/41.042 Maybe terminating CTRS, Maybe operational terminating CTRS, Maybe joinable CCPs 41.042/41.042 Maybe level confluent 41.042/41.042 Maybe confluent 41.042/41.042 41.042/41.042 Problem 1: 41.042/41.042 Clean Infeasible CCPs Processor: 41.042/41.042 Num of CPIs: 2 41.042/41.042 Timeout: 60 41.042/41.042 Timeout for each infeasibility problem: 60 s 41.042/41.042 | odd(x') ->* true, odd(x') ->* false => Not trivial, Overlay, NW2, N1 41.042/41.042 (CONDITIONTYPE ORIENTED) 41.042/41.042 (VAR x x1) 41.042/41.042 (RULES 41.042/41.042 even(0) -> true 41.042/41.042 even(s(x)) -> false | odd(x) ->* false 41.042/41.042 even(s(x)) -> true | odd(x) ->* true 41.042/41.042 odd(0) -> false 41.042/41.042 odd(s(x)) -> false | even(x) ->* false 41.042/41.042 odd(s(x)) -> true | even(x) ->* true) 41.042/41.042 (VAR x4) 41.042/41.042 (CONDITION odd(x4) ->* true, odd(x4) ->* false) 41.042/41.042 41.042/41.042 Proof: 41.042/41.042 YES 41.042/41.042 41.042/41.042 Problem 1: 41.042/41.042 41.042/41.042 Infeasibility Problem: 41.042/41.042 [(VAR vNonEmpty x x1 vNonEmpty x4) 41.042/41.042 (STRATEGY CONTEXTSENSITIVE 41.042/41.042 (even 1) 41.042/41.042 (odd 1) 41.042/41.042 (0) 41.042/41.042 (fSNonEmpty) 41.042/41.042 (false) 41.042/41.042 (s 1) 41.042/41.042 (true) 41.042/41.042 ) 41.042/41.042 (RULES 41.042/41.042 even(0) -> true 41.042/41.042 even(s(x)) -> false | odd(x) ->* false 41.042/41.042 even(s(x)) -> true | odd(x) ->* true 41.042/41.042 odd(0) -> false 41.042/41.042 odd(s(x)) -> false | even(x) ->* false 41.042/41.042 odd(s(x)) -> true | even(x) ->* true 41.042/41.042 )] 41.042/41.042 41.042/41.042 Infeasibility Conditions: 41.042/41.042 odd(x4) ->* true, odd(x4) ->* false 41.042/41.042 41.042/41.042 Problem 1: 41.042/41.042 41.042/41.042 Obtaining a model using Mace4: 41.042/41.042 41.042/41.042 -> Usable Rules: 41.042/41.042 even(0) -> true 41.042/41.042 even(s(x)) -> false | odd(x) ->* false 41.042/41.042 even(s(x)) -> true | odd(x) ->* true 41.042/41.042 odd(0) -> false 41.042/41.042 odd(s(x)) -> false | even(x) ->* false 41.042/41.042 odd(s(x)) -> true | even(x) ->* true 41.042/41.042 41.042/41.042 -> Mace4 Output: 41.042/41.042 ============================== Mace4 ================================= 41.042/41.042 Mace4 (64) version 2009-11A, November 2009. 41.042/41.042 Process 14172 was started by ubuntu on ubuntu, 41.042/41.042 Wed Mar 9 09:27:25 2022 41.042/41.042 The command was "./mace4 -c -f /tmp/mace414139-2.in". 41.042/41.042 ============================== end of head =========================== 41.042/41.042 41.042/41.042 ============================== INPUT ================================= 41.042/41.042 41.042/41.042 % Reading from file /tmp/mace414139-2.in 41.042/41.042 41.042/41.042 assign(max_seconds,20). 41.042/41.042 41.042/41.042 formulas(assumptions). 41.042/41.042 ->(x1,y) -> ->(even(x1),even(y)) # label(congruence). 41.042/41.042 ->(x1,y) -> ->(odd(x1),odd(y)) # label(congruence). 41.042/41.042 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence). 41.042/41.042 ->(even(0),true) # label(replacement). 41.042/41.042 ->*(odd(x1),false) -> ->(even(s(x1)),false) # label(replacement). 41.042/41.042 ->*(odd(x1),true) -> ->(even(s(x1)),true) # label(replacement). 41.042/41.042 ->(odd(0),false) # label(replacement). 41.042/41.042 ->*(even(x1),false) -> ->(odd(s(x1)),false) # label(replacement). 41.042/41.042 ->*(even(x1),true) -> ->(odd(s(x1)),true) # label(replacement). 41.042/41.042 ->*(x,x) # label(reflexivity). 41.042/41.042 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 formulas(goals). 41.042/41.042 (exists x4 (->*(odd(x4),true) & ->*(odd(x4),false))) # label(goal). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 ============================== end of input ========================== 41.042/41.042 41.042/41.042 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 41.042/41.042 41.042/41.042 % Formulas that are not ordinary clauses: 41.042/41.042 1 ->(x1,y) -> ->(even(x1),even(y)) # label(congruence) # label(non_clause). [assumption]. 41.042/41.042 2 ->(x1,y) -> ->(odd(x1),odd(y)) # label(congruence) # label(non_clause). [assumption]. 41.042/41.042 3 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 41.042/41.042 4 ->*(odd(x1),false) -> ->(even(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 5 ->*(odd(x1),true) -> ->(even(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 6 ->*(even(x1),false) -> ->(odd(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 7 ->*(even(x1),true) -> ->(odd(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 8 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 41.042/41.042 9 (exists x4 (->*(odd(x4),true) & ->*(odd(x4),false))) # label(goal) # label(non_clause) # label(goal). [goal]. 41.042/41.042 41.042/41.042 ============================== end of process non-clausal formulas === 41.042/41.042 41.042/41.042 ============================== CLAUSES FOR SEARCH ==================== 41.042/41.042 41.042/41.042 formulas(mace4_clauses). 41.042/41.042 -->(x,y) | ->(even(x),even(y)) # label(congruence). 41.042/41.042 -->(x,y) | ->(odd(x),odd(y)) # label(congruence). 41.042/41.042 -->(x,y) | ->(s(x),s(y)) # label(congruence). 41.042/41.042 ->(even(0),true) # label(replacement). 41.042/41.042 -->*(odd(x),false) | ->(even(s(x)),false) # label(replacement). 41.042/41.042 -->*(odd(x),true) | ->(even(s(x)),true) # label(replacement). 41.042/41.042 ->(odd(0),false) # label(replacement). 41.042/41.042 -->*(even(x),false) | ->(odd(s(x)),false) # label(replacement). 41.042/41.042 -->*(even(x),true) | ->(odd(s(x)),true) # label(replacement). 41.042/41.042 ->*(x,x) # label(reflexivity). 41.042/41.042 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 41.042/41.042 -->*(odd(x),true) | -->*(odd(x),false) # label(goal). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 ============================== end of clauses for search ============= 41.042/41.042 41.042/41.042 % There are no natural numbers in the input. 41.042/41.042 41.042/41.042 ============================== DOMAIN SIZE 2 ========================= 41.042/41.042 41.042/41.042 ============================== MODEL ================================= 41.042/41.042 41.042/41.042 interpretation( 2, [number=1, seconds=0], [ 41.042/41.042 41.042/41.042 function(0, [ 0 ]), 41.042/41.042 41.042/41.042 function(false, [ 0 ]), 41.042/41.042 41.042/41.042 function(true, [ 1 ]), 41.042/41.042 41.042/41.042 function(even(_), [ 1, 0 ]), 41.042/41.042 41.042/41.042 function(odd(_), [ 0, 1 ]), 41.042/41.042 41.042/41.042 function(s(_), [ 1, 0 ]), 41.042/41.042 41.042/41.042 relation(->*(_,_), [ 41.042/41.042 1, 0, 41.042/41.042 0, 1 ]), 41.042/41.042 41.042/41.042 relation(->(_,_), [ 41.042/41.042 1, 0, 41.042/41.042 0, 1 ]) 41.042/41.042 ]). 41.042/41.042 41.042/41.042 ============================== end of model ========================== 41.042/41.042 41.042/41.042 ============================== STATISTICS ============================ 41.042/41.042 41.042/41.042 For domain size 2. 41.042/41.042 41.042/41.042 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 41.042/41.042 Ground clauses: seen=34, kept=30. 41.042/41.042 Selections=11, assignments=18, propagations=22, current_models=1. 41.042/41.042 Rewrite_terms=142, rewrite_bools=102, indexes=32. 41.042/41.042 Rules_from_neg_clauses=2, cross_offs=2. 41.042/41.042 41.042/41.042 ============================== end of statistics ===================== 41.042/41.042 41.042/41.042 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 41.042/41.042 41.042/41.042 Exiting with 1 model. 41.042/41.042 41.042/41.042 Process 14172 exit (max_models) Wed Mar 9 09:27:25 2022 41.042/41.042 The process finished Wed Mar 9 09:27:25 2022 41.042/41.042 41.042/41.042 41.042/41.042 Mace4 cooked interpretation: 41.042/41.042 41.042/41.042 41.042/41.042 41.042/41.042 The problem is infeasible. 41.042/41.042 41.042/41.042 41.042/41.042 41.042/41.042 41.042/41.042 | even(x') ->* true, even(x') ->* false => Not trivial, Overlay, NW2, N2 41.042/41.042 (CONDITIONTYPE ORIENTED) 41.042/41.042 (VAR x x1) 41.042/41.042 (RULES 41.042/41.042 even(0) -> true 41.042/41.042 even(s(x)) -> false | odd(x) ->* false 41.042/41.042 even(s(x)) -> true | odd(x) ->* true 41.042/41.042 odd(0) -> false 41.042/41.042 odd(s(x)) -> false | even(x) ->* false 41.042/41.042 odd(s(x)) -> true | even(x) ->* true) 41.042/41.042 (VAR x4) 41.042/41.042 (CONDITION even(x4) ->* true, even(x4) ->* false) 41.042/41.042 41.042/41.042 Proof: 41.042/41.042 YES 41.042/41.042 41.042/41.042 Problem 1: 41.042/41.042 41.042/41.042 Infeasibility Problem: 41.042/41.042 [(VAR vNonEmpty x x1 vNonEmpty x4) 41.042/41.042 (STRATEGY CONTEXTSENSITIVE 41.042/41.042 (even 1) 41.042/41.042 (odd 1) 41.042/41.042 (0) 41.042/41.042 (fSNonEmpty) 41.042/41.042 (false) 41.042/41.042 (s 1) 41.042/41.042 (true) 41.042/41.042 ) 41.042/41.042 (RULES 41.042/41.042 even(0) -> true 41.042/41.042 even(s(x)) -> false | odd(x) ->* false 41.042/41.042 even(s(x)) -> true | odd(x) ->* true 41.042/41.042 odd(0) -> false 41.042/41.042 odd(s(x)) -> false | even(x) ->* false 41.042/41.042 odd(s(x)) -> true | even(x) ->* true 41.042/41.042 )] 41.042/41.042 41.042/41.042 Infeasibility Conditions: 41.042/41.042 even(x4) ->* true, even(x4) ->* false 41.042/41.042 41.042/41.042 Problem 1: 41.042/41.042 41.042/41.042 Obtaining a model using Mace4: 41.042/41.042 41.042/41.042 -> Usable Rules: 41.042/41.042 even(0) -> true 41.042/41.042 even(s(x)) -> false | odd(x) ->* false 41.042/41.042 even(s(x)) -> true | odd(x) ->* true 41.042/41.042 odd(0) -> false 41.042/41.042 odd(s(x)) -> false | even(x) ->* false 41.042/41.042 odd(s(x)) -> true | even(x) ->* true 41.042/41.042 41.042/41.042 -> Mace4 Output: 41.042/41.042 ============================== Mace4 ================================= 41.042/41.042 Mace4 (64) version 2009-11A, November 2009. 41.042/41.042 Process 14210 was started by ubuntu on ubuntu, 41.042/41.042 Wed Mar 9 09:27:45 2022 41.042/41.042 The command was "./mace4 -c -f /tmp/mace414198-2.in". 41.042/41.042 ============================== end of head =========================== 41.042/41.042 41.042/41.042 ============================== INPUT ================================= 41.042/41.042 41.042/41.042 % Reading from file /tmp/mace414198-2.in 41.042/41.042 41.042/41.042 assign(max_seconds,20). 41.042/41.042 41.042/41.042 formulas(assumptions). 41.042/41.042 ->(x1,y) -> ->(even(x1),even(y)) # label(congruence). 41.042/41.042 ->(x1,y) -> ->(odd(x1),odd(y)) # label(congruence). 41.042/41.042 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence). 41.042/41.042 ->(even(0),true) # label(replacement). 41.042/41.042 ->*(odd(x1),false) -> ->(even(s(x1)),false) # label(replacement). 41.042/41.042 ->*(odd(x1),true) -> ->(even(s(x1)),true) # label(replacement). 41.042/41.042 ->(odd(0),false) # label(replacement). 41.042/41.042 ->*(even(x1),false) -> ->(odd(s(x1)),false) # label(replacement). 41.042/41.042 ->*(even(x1),true) -> ->(odd(s(x1)),true) # label(replacement). 41.042/41.042 ->*(x,x) # label(reflexivity). 41.042/41.042 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 formulas(goals). 41.042/41.042 (exists x4 (->*(even(x4),true) & ->*(even(x4),false))) # label(goal). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 ============================== end of input ========================== 41.042/41.042 41.042/41.042 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 41.042/41.042 41.042/41.042 % Formulas that are not ordinary clauses: 41.042/41.042 1 ->(x1,y) -> ->(even(x1),even(y)) # label(congruence) # label(non_clause). [assumption]. 41.042/41.042 2 ->(x1,y) -> ->(odd(x1),odd(y)) # label(congruence) # label(non_clause). [assumption]. 41.042/41.042 3 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 41.042/41.042 4 ->*(odd(x1),false) -> ->(even(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 5 ->*(odd(x1),true) -> ->(even(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 6 ->*(even(x1),false) -> ->(odd(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 7 ->*(even(x1),true) -> ->(odd(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.042/41.042 8 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 41.042/41.042 9 (exists x4 (->*(even(x4),true) & ->*(even(x4),false))) # label(goal) # label(non_clause) # label(goal). [goal]. 41.042/41.042 41.042/41.042 ============================== end of process non-clausal formulas === 41.042/41.042 41.042/41.042 ============================== CLAUSES FOR SEARCH ==================== 41.042/41.042 41.042/41.042 formulas(mace4_clauses). 41.042/41.042 -->(x,y) | ->(even(x),even(y)) # label(congruence). 41.042/41.042 -->(x,y) | ->(odd(x),odd(y)) # label(congruence). 41.042/41.042 -->(x,y) | ->(s(x),s(y)) # label(congruence). 41.042/41.042 ->(even(0),true) # label(replacement). 41.042/41.042 -->*(odd(x),false) | ->(even(s(x)),false) # label(replacement). 41.042/41.042 -->*(odd(x),true) | ->(even(s(x)),true) # label(replacement). 41.042/41.042 ->(odd(0),false) # label(replacement). 41.042/41.042 -->*(even(x),false) | ->(odd(s(x)),false) # label(replacement). 41.042/41.042 -->*(even(x),true) | ->(odd(s(x)),true) # label(replacement). 41.042/41.042 ->*(x,x) # label(reflexivity). 41.042/41.042 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 41.042/41.042 -->*(even(x),true) | -->*(even(x),false) # label(goal). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 ============================== end of clauses for search ============= 41.042/41.042 41.042/41.042 % There are no natural numbers in the input. 41.042/41.042 41.042/41.042 ============================== DOMAIN SIZE 2 ========================= 41.042/41.042 41.042/41.042 ============================== MODEL ================================= 41.042/41.042 41.042/41.042 interpretation( 2, [number=1, seconds=0], [ 41.042/41.042 41.042/41.042 function(0, [ 0 ]), 41.042/41.042 41.042/41.042 function(false, [ 0 ]), 41.042/41.042 41.042/41.042 function(true, [ 1 ]), 41.042/41.042 41.042/41.042 function(even(_), [ 1, 0 ]), 41.042/41.042 41.042/41.042 function(odd(_), [ 0, 1 ]), 41.042/41.042 41.042/41.042 function(s(_), [ 1, 0 ]), 41.042/41.042 41.042/41.042 relation(->*(_,_), [ 41.042/41.042 1, 0, 41.042/41.042 0, 1 ]), 41.042/41.042 41.042/41.042 relation(->(_,_), [ 41.042/41.042 1, 0, 41.042/41.042 0, 1 ]) 41.042/41.042 ]). 41.042/41.042 41.042/41.042 ============================== end of model ========================== 41.042/41.042 41.042/41.042 ============================== STATISTICS ============================ 41.042/41.042 41.042/41.042 For domain size 2. 41.042/41.042 41.042/41.042 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 41.042/41.042 Ground clauses: seen=34, kept=30. 41.042/41.042 Selections=7, assignments=11, propagations=17, current_models=1. 41.042/41.042 Rewrite_terms=118, rewrite_bools=63, indexes=24. 41.042/41.042 Rules_from_neg_clauses=3, cross_offs=3. 41.042/41.042 41.042/41.042 ============================== end of statistics ===================== 41.042/41.042 41.042/41.042 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 41.042/41.042 41.042/41.042 Exiting with 1 model. 41.042/41.042 41.042/41.042 Process 14210 exit (max_models) Wed Mar 9 09:27:45 2022 41.042/41.042 The process finished Wed Mar 9 09:27:45 2022 41.042/41.042 41.042/41.042 41.042/41.042 Mace4 cooked interpretation: 41.042/41.042 41.042/41.042 41.042/41.042 41.042/41.042 The problem is infeasible. 41.042/41.042 41.042/41.042 41.042/41.042 41.042/41.042 41.042/41.042 -> Problem conclusions: 41.042/41.042 Left linear, Right linear, Linear 41.042/41.042 Weakly orthogonal, Almost orthogonal, Orthogonal 41.042/41.042 CTRS Type: 1 41.042/41.042 Deterministic, Strongly deterministic 41.042/41.042 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 41.042/41.042 Maybe right-stable CTRS, Overlay CTRS 41.042/41.042 Maybe normal CTRS, Maybe almost normal CTRS 41.042/41.042 Maybe terminating CTRS, Maybe operational terminating CTRS, Joinable CCPs 41.042/41.042 Maybe level confluent 41.042/41.042 Maybe confluent 41.042/41.042 41.042/41.042 Resulting CCPs: 41.042/41.042 No CCPs left 41.042/41.042 41.042/41.042 Problem 1: 41.042/41.042 Underlying TRS Termination Processor: 41.042/41.042 41.042/41.042 Resulting Underlying TRS: 41.042/41.042 (VAR x x') 41.042/41.042 (STRATEGY CONTEXTSENSITIVE 41.042/41.042 (even 1) 41.042/41.042 (odd 1) 41.042/41.042 (false) 41.042/41.042 (true) 41.042/41.042 ) 41.042/41.042 (RULES 41.042/41.042 even(0) -> true 41.042/41.042 even(s(x)) -> false 41.042/41.042 even(s(x)) -> true 41.042/41.042 odd(0) -> false 41.042/41.042 odd(s(x)) -> false 41.042/41.042 odd(s(x)) -> true 41.042/41.042 ) 41.042/41.042 Underlying TRS terminating? 41.042/41.042 YES 41.042/41.042 41.042/41.042 Problem 1: 41.042/41.042 41.042/41.042 (VAR vu95NonEmpty x xu39) 41.042/41.042 (RULES 41.042/41.042 even(num0) -> ftrue 41.042/41.042 even(s(x)) -> ffalse 41.042/41.042 even(s(x)) -> ftrue 41.042/41.042 odd(num0) -> ffalse 41.042/41.042 odd(s(x)) -> ffalse 41.042/41.042 odd(s(x)) -> ftrue 41.042/41.042 ) 41.042/41.042 41.042/41.042 Problem 1: 41.042/41.042 41.042/41.042 Dependency Pairs Processor: 41.042/41.042 -> Pairs: 41.042/41.042 Empty 41.042/41.042 -> Rules: 41.042/41.042 even(num0) -> ftrue 41.042/41.042 even(s(x)) -> ffalse 41.042/41.042 even(s(x)) -> ftrue 41.042/41.042 odd(num0) -> ffalse 41.042/41.042 odd(s(x)) -> ffalse 41.042/41.042 odd(s(x)) -> ftrue 41.042/41.042 41.042/41.042 Problem 1: 41.042/41.042 41.042/41.042 SCC Processor: 41.042/41.042 -> Pairs: 41.042/41.042 Empty 41.042/41.042 -> Rules: 41.042/41.042 even(num0) -> ftrue 41.042/41.042 even(s(x)) -> ffalse 41.042/41.042 even(s(x)) -> ftrue 41.042/41.042 odd(num0) -> ffalse 41.042/41.042 odd(s(x)) -> ffalse 41.042/41.042 odd(s(x)) -> ftrue 41.042/41.042 ->Strongly Connected Components: 41.042/41.042 There is no strongly connected component 41.042/41.042 41.042/41.042 The problem is finite. 41.042/41.042 41.042/41.042 41.042/41.042 -> Problem conclusions: 41.042/41.042 Left linear, Right linear, Linear 41.042/41.042 Weakly orthogonal, Almost orthogonal, Orthogonal 41.042/41.042 CTRS Type: 1 41.042/41.042 Deterministic, Strongly deterministic 41.042/41.042 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 41.042/41.042 Maybe right-stable CTRS, Overlay CTRS 41.042/41.042 Maybe normal CTRS, Maybe almost normal CTRS 41.042/41.042 Terminating CTRS, Maybe operational terminating CTRS, Joinable CCPs 41.042/41.042 Maybe level confluent 41.042/41.042 Maybe confluent 41.042/41.042 41.042/41.042 Problem 1: 41.042/41.042 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 41.042/41.042 Confluence Problem: 41.042/41.042 (VAR x x') 41.042/41.042 (REPLACEMENT-MAP 41.042/41.042 (even 1) 41.042/41.042 (odd 1) 41.042/41.042 (0) 41.042/41.042 (fSNonEmpty) 41.042/41.042 (false) 41.042/41.042 (s 1) 41.042/41.042 (true) 41.042/41.042 ) 41.042/41.042 (RULES 41.042/41.042 even(0) -> true 41.042/41.042 even(s(x)) -> false | odd(x) ->* false 41.042/41.042 even(s(x)) -> true | odd(x) ->* true 41.042/41.042 odd(0) -> false 41.042/41.042 odd(s(x)) -> false | even(x) ->* false 41.042/41.042 odd(s(x)) -> true | even(x) ->* true 41.042/41.042 ) 41.042/41.042 Critical Pairs: 41.042/41.042 41.042/41.042 Terminating:YES 41.042/41.042 41.042/41.042 -> Problem conclusions: 41.042/41.042 Left linear, Right linear, Linear 41.042/41.042 Weakly orthogonal, Almost orthogonal, Orthogonal 41.042/41.042 CTRS Type: 1 41.042/41.042 Deterministic, Strongly deterministic 41.042/41.042 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 41.042/41.042 Maybe right-stable CTRS, Overlay CTRS 41.042/41.042 Maybe normal CTRS, Maybe almost normal CTRS 41.042/41.042 Terminating CTRS, Maybe operational terminating CTRS, Joinable CCPs 41.042/41.042 Maybe level confluent 41.042/41.042 Maybe confluent 41.042/41.042 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 41.042/41.042 41.042/41.042 Right Stable Processor: 41.042/41.042 Right-stable CTRS 41.042/41.042 Justification: 41.042/41.042 41.042/41.042 -> Term right-stability conditions: 41.042/41.042 Term: false 41.042/41.042 Right-stable term 41.042/41.042 Linear constructor form 41.042/41.042 Don't know if term is a ground normal form (not needed) 41.042/41.042 Right-stability condition achieved 41.042/41.042 A call to InfChecker wasn't needed 41.042/41.042 41.042/41.042 41.042/41.042 -> Term right-stability conditions: 41.042/41.042 Term: true 41.042/41.042 Right-stable term 41.042/41.042 Linear constructor form 41.042/41.042 Don't know if term is a ground normal form (not needed) 41.042/41.042 Right-stability condition achieved 41.042/41.042 A call to InfChecker wasn't needed 41.042/41.042 41.042/41.042 41.042/41.042 -> Term right-stability conditions: 41.042/41.042 Term: false 41.042/41.042 Right-stable term 41.042/41.042 Linear constructor form 41.042/41.042 Don't know if term is a ground normal form (not needed) 41.042/41.042 Right-stability condition achieved 41.042/41.042 A call to InfChecker wasn't needed 41.042/41.042 41.042/41.042 41.042/41.042 -> Term right-stability conditions: 41.042/41.042 Term: true 41.042/41.042 Right-stable term 41.042/41.042 Linear constructor form 41.042/41.042 Don't know if term is a ground normal form (not needed) 41.042/41.042 Right-stability condition achieved 41.042/41.042 A call to InfChecker wasn't needed 41.042/41.042 41.042/41.042 -> Problem conclusions: 41.042/41.042 Left linear, Right linear, Linear 41.042/41.042 Weakly orthogonal, Almost orthogonal, Orthogonal 41.042/41.042 CTRS Type: 1 41.042/41.042 Deterministic, Strongly deterministic 41.042/41.042 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 41.042/41.042 Right-stable CTRS, Overlay CTRS 41.042/41.042 Maybe normal CTRS, Almost normal CTRS 41.042/41.042 Terminating CTRS, Maybe operational terminating CTRS, Joinable CCPs 41.042/41.042 Level confluent 41.042/41.042 Confluent 41.042/41.042 41.042/41.042 Problem 1: 41.042/41.042 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 41.042/41.042 Confluence Problem: 41.042/41.042 (VAR x x') 41.042/41.042 (REPLACEMENT-MAP 41.042/41.042 (even 1) 41.042/41.042 (odd 1) 41.042/41.042 (0) 41.042/41.042 (fSNonEmpty) 41.042/41.042 (false) 41.042/41.042 (s 1) 41.042/41.042 (true) 41.042/41.042 ) 41.042/41.042 (RULES 41.042/41.042 even(0) -> true 41.042/41.042 even(s(x)) -> false | odd(x) ->* false 41.042/41.042 even(s(x)) -> true | odd(x) ->* true 41.042/41.042 odd(0) -> false 41.042/41.042 odd(s(x)) -> false | even(x) ->* false 41.042/41.042 odd(s(x)) -> true | even(x) ->* true 41.042/41.042 ) 41.042/41.042 Critical Pairs: 41.042/41.042 41.042/41.042 Terminating:YES 41.042/41.042 41.042/41.042 -> Problem conclusions: 41.042/41.042 Left linear, Right linear, Linear 41.042/41.042 Weakly orthogonal, Almost orthogonal, Orthogonal 41.042/41.042 CTRS Type: 1 41.042/41.042 Deterministic, Strongly deterministic 41.042/41.042 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 41.042/41.042 Right-stable CTRS, Overlay CTRS 41.042/41.042 Maybe normal CTRS, Almost normal CTRS 41.042/41.042 Terminating CTRS, Maybe operational terminating CTRS, Joinable CCPs 41.042/41.042 Level confluent 41.042/41.042 Confluent 41.042/41.042 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 41.042/41.042 41.042/41.042 Normal RConds Processor: 41.042/41.042 YES 41.042/41.042 41.042/41.042 Problem 1: 41.042/41.042 41.042/41.042 Infeasibility Problem: 41.042/41.042 [(VAR vNonEmpty x x1 vNonEmpty z z1) 41.042/41.042 (STRATEGY CONTEXTSENSITIVE 41.042/41.042 (even 1) 41.042/41.042 (odd 1) 41.042/41.042 (0) 41.042/41.042 (fSNonEmpty) 41.042/41.042 (false) 41.042/41.042 (s 1) 41.042/41.042 (true) 41.042/41.042 ) 41.042/41.042 (RULES 41.042/41.042 even(0) -> true 41.042/41.042 even(s(x)) -> false | odd(x) ->* false 41.042/41.042 even(s(x)) -> true | odd(x) ->* true 41.042/41.042 odd(0) -> false 41.042/41.042 odd(s(x)) -> false | even(x) ->* false 41.042/41.042 odd(s(x)) -> true | even(x) ->* true 41.042/41.042 )] 41.042/41.042 41.042/41.042 Infeasibility Conditions: 41.042/41.042 false -> z, true -> z1 41.042/41.042 41.042/41.042 Problem 1: 41.042/41.042 41.042/41.042 Obtaining a model using Mace4: 41.042/41.042 41.042/41.042 -> Usable Rules: 41.042/41.042 Empty 41.042/41.042 41.042/41.042 -> Mace4 Output: 41.042/41.042 ============================== Mace4 ================================= 41.042/41.042 Mace4 (64) version 2009-11A, November 2009. 41.042/41.042 Process 14283 was started by ubuntu on ubuntu, 41.042/41.042 Wed Mar 9 09:28:06 2022 41.042/41.042 The command was "./mace4 -c -f /tmp/mace414272-2.in". 41.042/41.042 ============================== end of head =========================== 41.042/41.042 41.042/41.042 ============================== INPUT ================================= 41.042/41.042 41.042/41.042 % Reading from file /tmp/mace414272-2.in 41.042/41.042 41.042/41.042 assign(max_seconds,13). 41.042/41.042 41.042/41.042 formulas(assumptions). 41.042/41.042 ->(x1,y) -> ->(even(x1),even(y)) # label(congruence). 41.042/41.042 ->(x1,y) -> ->(odd(x1),odd(y)) # label(congruence). 41.042/41.042 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 formulas(goals). 41.042/41.042 (exists x4 exists x5 (->(false,x4) & ->(true,x5))) # label(goal). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 ============================== end of input ========================== 41.042/41.042 41.042/41.042 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 41.042/41.042 41.042/41.042 % Formulas that are not ordinary clauses: 41.042/41.042 1 ->(x1,y) -> ->(even(x1),even(y)) # label(congruence) # label(non_clause). [assumption]. 41.042/41.042 2 ->(x1,y) -> ->(odd(x1),odd(y)) # label(congruence) # label(non_clause). [assumption]. 41.042/41.042 3 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 41.042/41.042 4 (exists x4 exists x5 (->(false,x4) & ->(true,x5))) # label(goal) # label(non_clause) # label(goal). [goal]. 41.042/41.042 41.042/41.042 ============================== end of process non-clausal formulas === 41.042/41.042 41.042/41.042 ============================== CLAUSES FOR SEARCH ==================== 41.042/41.042 41.042/41.042 formulas(mace4_clauses). 41.042/41.042 -->(x,y) | ->(even(x),even(y)) # label(congruence). 41.042/41.042 -->(x,y) | ->(odd(x),odd(y)) # label(congruence). 41.042/41.042 -->(x,y) | ->(s(x),s(y)) # label(congruence). 41.042/41.042 -->(false,x) | -->(true,y) # label(goal). 41.042/41.042 end_of_list. 41.042/41.042 41.042/41.042 ============================== end of clauses for search ============= 41.042/41.042 41.042/41.042 % There are no natural numbers in the input. 41.042/41.042 41.042/41.042 ============================== DOMAIN SIZE 2 ========================= 41.042/41.042 41.042/41.042 ============================== MODEL ================================= 41.042/41.042 41.042/41.042 interpretation( 2, [number=1, seconds=0], [ 41.042/41.042 41.042/41.042 function(false, [ 0 ]), 41.042/41.042 41.042/41.042 function(true, [ 0 ]), 41.042/41.042 41.042/41.042 function(even(_), [ 0, 0 ]), 41.042/41.042 41.042/41.042 function(odd(_), [ 0, 0 ]), 41.042/41.042 41.042/41.042 function(s(_), [ 0, 0 ]), 41.042/41.042 41.042/41.042 relation(->(_,_), [ 41.042/41.042 0, 0, 41.042/41.042 0, 0 ]) 41.042/41.042 ]). 41.042/41.042 41.042/41.042 ============================== end of model ========================== 41.042/41.042 41.042/41.042 ============================== STATISTICS ============================ 41.042/41.042 41.042/41.042 For domain size 2. 41.042/41.042 41.042/41.042 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 41.042/41.042 Ground clauses: seen=16, kept=16. 41.042/41.042 Selections=9, assignments=9, propagations=3, current_models=1. 41.042/41.042 Rewrite_terms=32, rewrite_bools=22, indexes=11. 41.042/41.042 Rules_from_neg_clauses=0, cross_offs=0. 41.042/41.042 41.042/41.042 ============================== end of statistics ===================== 41.042/41.042 41.042/41.042 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 41.042/41.042 41.042/41.042 Exiting with 1 model. 41.042/41.042 41.042/41.042 Process 14283 exit (max_models) Wed Mar 9 09:28:06 2022 41.042/41.042 The process finished Wed Mar 9 09:28:06 2022 41.042/41.042 41.042/41.042 41.042/41.042 Mace4 cooked interpretation: 41.042/41.042 41.042/41.042 41.042/41.042 41.042/41.042 The problem is infeasible. 41.042/41.042 41.042/41.042 41.042/41.042 -> Problem conclusions: 41.042/41.042 Left linear, Right linear, Linear 41.042/41.042 Weakly orthogonal, Almost orthogonal, Orthogonal 41.042/41.042 CTRS Type: 1 41.042/41.042 Deterministic, Strongly deterministic 41.042/41.042 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 41.042/41.042 Right-stable CTRS, Overlay CTRS 41.042/41.042 Normal CTRS, Almost normal CTRS 41.042/41.042 Terminating CTRS, Maybe operational terminating CTRS, Joinable CCPs 41.042/41.042 Level confluent 41.042/41.042 Confluent 41.042/41.042 41.042/41.042 The problem is joinable. 41.042/41.042 64.21user 1.80system 0:41.42elapsed 159%CPU (0avgtext+0avgdata 118580maxresident)k 41.042/41.042 8inputs+0outputs (0major+141644minor)pagefaults 0swaps