YES Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x) (REPLACEMENT-MAP (even 1) (odd 1) (0) (false) (s) (true) ) (RULES even(0) -> true even(s(x)) -> false | even(x) \->* true even(s(x)) -> true | odd(x) \->* true odd(0) -> false odd(s(x)) -> false | odd(x) \->* true odd(s(x)) -> true | even(x) \->* true ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Problem 1: Clean CTRS Procedure: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x) (REPLACEMENT-MAP (even 1) (odd 1) (0) (false) (s) (true) ) (RULES even(0) -> true even(s(x)) -> false | even(x) \->* true even(s(x)) -> true | odd(x) \->* true odd(0) -> false odd(s(x)) -> false | odd(x) \->* true odd(s(x)) -> true | even(x) \->* true ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: CRule InfChecker Info: even(0) -> true Rule remains Proof: NO_CONDS CRule InfChecker Info: even(s(x)) -> false | even(x) \->* true Rule remains Proof: NO Problem 1: Infeasibility Problem: [(VAR vNonEmpty x vNonEmpty x) (STRATEGY CONTEXTSENSITIVE (even 1) (odd 1) (0) (fSNonEmpty) (false) (s) (true) ) (RULES even(0) -> true even(s(x)) -> false | even(x) \->* true even(s(x)) -> true | odd(x) \->* true odd(0) -> false odd(s(x)) -> false | odd(x) \->* true odd(s(x)) -> true | even(x) \->* true ) ] Infeasibility Conditions: even(x) \->* true Problem 1: Obtaining a proof using Prover9: -> Prover9 Output: ============================== Prover9 =============================== Prover9 (64) version 2009-11A, November 2009. Process 2773168 was started by sandbox on z021.star.cs.uiowa.edu, Thu Jun 27 11:11:08 2024 The command was "./prover9 -f /tmp/prover92773155-0.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file /tmp/prover92773155-0.in assign(max_seconds,20). formulas(assumptions). \->_s0(x1,y) -> \->_s0(even(x1),even(y)) # label(cscongruence). \->_s0(x1,y) -> \->_s0(odd(x1),odd(y)) # label(cscongruence). \->_s0(even(0),true) # label(csreplacement). \->*_s0(even(x1),true) -> \->_s0(even(s(x1)),false) # label(csreplacement). \->*_s0(odd(x1),true) -> \->_s0(even(s(x1)),true) # label(csreplacement). \->_s0(odd(0),false) # label(csreplacement). \->*_s0(odd(x1),true) -> \->_s0(odd(s(x1)),false) # label(csreplacement). \->*_s0(even(x1),true) -> \->_s0(odd(s(x1)),true) # label(csreplacement). \->*_s0(x,x) # label(csreflexivity). \->_s0(x,y) & \->*_s0(y,z) -> \->*_s0(x,z) # label(cstransitivity). end_of_list. formulas(goals). (exists x3 \->*_s0(even(x3),true)) # label(goal). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 \->_s0(x1,y) -> \->_s0(even(x1),even(y)) # label(cscongruence) # label(non_clause). [assumption]. 2 \->_s0(x1,y) -> \->_s0(odd(x1),odd(y)) # label(cscongruence) # label(non_clause). [assumption]. 3 \->*_s0(even(x1),true) -> \->_s0(even(s(x1)),false) # label(csreplacement) # label(non_clause). [assumption]. 4 \->*_s0(odd(x1),true) -> \->_s0(even(s(x1)),true) # label(csreplacement) # label(non_clause). [assumption]. 5 \->*_s0(odd(x1),true) -> \->_s0(odd(s(x1)),false) # label(csreplacement) # label(non_clause). [assumption]. 6 \->*_s0(even(x1),true) -> \->_s0(odd(s(x1)),true) # label(csreplacement) # label(non_clause). [assumption]. 7 \->_s0(x,y) & \->*_s0(y,z) -> \->*_s0(x,z) # label(cstransitivity) # label(non_clause). [assumption]. 8 (exists x3 \->*_s0(even(x3),true)) # label(goal) # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). -\->_s0(x,y) | \->_s0(even(x),even(y)) # label(cscongruence). [clausify(1)]. -\->_s0(x,y) | \->_s0(odd(x),odd(y)) # label(cscongruence). [clausify(2)]. \->_s0(even(0),true) # label(csreplacement). [assumption]. -\->*_s0(even(x),true) | \->_s0(even(s(x)),false) # label(csreplacement). [clausify(3)]. -\->*_s0(odd(x),true) | \->_s0(even(s(x)),true) # label(csreplacement). [clausify(4)]. \->_s0(odd(0),false) # label(csreplacement). [assumption]. -\->*_s0(odd(x),true) | \->_s0(odd(s(x)),false) # label(csreplacement). [clausify(5)]. -\->*_s0(even(x),true) | \->_s0(odd(s(x)),true) # label(csreplacement). [clausify(6)]. \->*_s0(x,x) # label(csreflexivity). [assumption]. -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(7)]. -\->*_s0(even(x),true) # label(goal). [deny(8)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % copying label goal to answer in negative clause Term ordering decisions: Predicate symbol precedence: predicate_order([ \->_s0, \->*_s0 ]). Function symbol precedence: function_order([ true, false, 0, even, odd, s ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(neg_binary_resolution). % (HNE depth_diff=-6) % clear(ordered_res). % (HNE depth_diff=-6) % set(ur_resolution). % (HNE depth_diff=-6) % set(ur_resolution) -> set(pos_ur_resolution). % set(ur_resolution) -> set(neg_ur_resolution). Auto_process settings: (no changes). kept: 9 -\->_s0(x,y) | \->_s0(even(x),even(y)) # label(cscongruence). [clausify(1)]. kept: 10 -\->_s0(x,y) | \->_s0(odd(x),odd(y)) # label(cscongruence). [clausify(2)]. kept: 11 \->_s0(even(0),true) # label(csreplacement). [assumption]. kept: 12 -\->*_s0(even(x),true) | \->_s0(even(s(x)),false) # label(csreplacement). [clausify(3)]. kept: 13 -\->*_s0(odd(x),true) | \->_s0(even(s(x)),true) # label(csreplacement). [clausify(4)]. kept: 14 \->_s0(odd(0),false) # label(csreplacement). [assumption]. kept: 15 -\->*_s0(odd(x),true) | \->_s0(odd(s(x)),false) # label(csreplacement). [clausify(5)]. kept: 16 -\->*_s0(even(x),true) | \->_s0(odd(s(x)),true) # label(csreplacement). [clausify(6)]. kept: 17 \->*_s0(x,x) # label(csreflexivity). [assumption]. kept: 18 -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(7)]. kept: 19 -\->*_s0(even(x),true) # label(goal) # answer(goal). [deny(8)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 9 -\->_s0(x,y) | \->_s0(even(x),even(y)) # label(cscongruence). [clausify(1)]. 10 -\->_s0(x,y) | \->_s0(odd(x),odd(y)) # label(cscongruence). [clausify(2)]. 11 \->_s0(even(0),true) # label(csreplacement). [assumption]. 13 -\->*_s0(odd(x),true) | \->_s0(even(s(x)),true) # label(csreplacement). [clausify(4)]. 14 \->_s0(odd(0),false) # label(csreplacement). [assumption]. 15 -\->*_s0(odd(x),true) | \->_s0(odd(s(x)),false) # label(csreplacement). [clausify(5)]. 17 \->*_s0(x,x) # label(csreflexivity). [assumption]. 18 -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(7)]. 19 -\->*_s0(even(x),true) # label(goal) # answer(goal). [deny(8)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=8): 9 -\->_s0(x,y) | \->_s0(even(x),even(y)) # label(cscongruence). [clausify(1)]. given #2 (I,wt=8): 10 -\->_s0(x,y) | \->_s0(odd(x),odd(y)) # label(cscongruence). [clausify(2)]. given #3 (I,wt=4): 11 \->_s0(even(0),true) # label(csreplacement). [assumption]. given #4 (I,wt=9): 13 -\->*_s0(odd(x),true) | \->_s0(even(s(x)),true) # label(csreplacement). [clausify(4)]. given #5 (I,wt=4): 14 \->_s0(odd(0),false) # label(csreplacement). [assumption]. given #6 (I,wt=9): 15 -\->*_s0(odd(x),true) | \->_s0(odd(s(x)),false) # label(csreplacement). [clausify(5)]. given #7 (I,wt=3): 17 \->*_s0(x,x) # label(csreflexivity). [assumption]. given #8 (I,wt=9): 18 -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(7)]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds: goal. % Length of proof is 8. % Level of proof is 3. % Maximum clause weight is 9.000. % Given clauses 8. 7 \->_s0(x,y) & \->*_s0(y,z) -> \->*_s0(x,z) # label(cstransitivity) # label(non_clause). [assumption]. 8 (exists x3 \->*_s0(even(x3),true)) # label(goal) # label(non_clause) # label(goal). [goal]. 11 \->_s0(even(0),true) # label(csreplacement). [assumption]. 17 \->*_s0(x,x) # label(csreflexivity). [assumption]. 18 -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(7)]. 19 -\->*_s0(even(x),true) # label(goal) # answer(goal). [deny(8)]. 25 \->*_s0(even(0),true). [ur(18,a,11,a,b,17,a)]. 26 $F # answer(goal). [resolve(25,a,19,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=8. Generated=17. Kept=17. proofs=1. Usable=8. Sos=5. Demods=0. Limbo=1, Disabled=13. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=0. Back_subsumed=2. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=10. Megabytes=0.07. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 2773168 exit (max_proofs) Thu Jun 27 11:11:08 2024 The problem is feasible. CRule InfChecker Info: even(s(x)) -> true | odd(x) \->* true Rule remains Proof: NO Problem 1: Infeasibility Problem: [(VAR vNonEmpty x vNonEmpty x) (STRATEGY CONTEXTSENSITIVE (even 1) (odd 1) (0) (fSNonEmpty) (false) (s) (true) ) (RULES even(0) -> true even(s(x)) -> false | even(x) \->* true even(s(x)) -> true | odd(x) \->* true odd(0) -> false odd(s(x)) -> false | odd(x) \->* true odd(s(x)) -> true | even(x) \->* true ) ] Infeasibility Conditions: odd(x) \->* true Problem 1: Obtaining a proof using Prover9: -> Prover9 Output: ============================== Prover9 =============================== Prover9 (64) version 2009-11A, November 2009. Process 2773194 was started by sandbox on z021.star.cs.uiowa.edu, Thu Jun 27 11:11:08 2024 The command was "./prover9 -f /tmp/prover92773185-0.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file /tmp/prover92773185-0.in assign(max_seconds,20). formulas(assumptions). \->_s0(x1,y) -> \->_s0(even(x1),even(y)) # label(cscongruence). \->_s0(x1,y) -> \->_s0(odd(x1),odd(y)) # label(cscongruence). \->_s0(even(0),true) # label(csreplacement). \->*_s0(even(x1),true) -> \->_s0(even(s(x1)),false) # label(csreplacement). \->*_s0(odd(x1),true) -> \->_s0(even(s(x1)),true) # label(csreplacement). \->_s0(odd(0),false) # label(csreplacement). \->*_s0(odd(x1),true) -> \->_s0(odd(s(x1)),false) # label(csreplacement). \->*_s0(even(x1),true) -> \->_s0(odd(s(x1)),true) # label(csreplacement). \->*_s0(x,x) # label(csreflexivity). \->_s0(x,y) & \->*_s0(y,z) -> \->*_s0(x,z) # label(cstransitivity). end_of_list. formulas(goals). (exists x3 \->*_s0(odd(x3),true)) # label(goal). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 \->_s0(x1,y) -> \->_s0(even(x1),even(y)) # label(cscongruence) # label(non_clause). [assumption]. 2 \->_s0(x1,y) -> \->_s0(odd(x1),odd(y)) # label(cscongruence) # label(non_clause). [assumption]. 3 \->*_s0(even(x1),true) -> \->_s0(even(s(x1)),false) # label(csreplacement) # label(non_clause). [assumption]. 4 \->*_s0(odd(x1),true) -> \->_s0(even(s(x1)),true) # label(csreplacement) # label(non_clause). [assumption]. 5 \->*_s0(odd(x1),true) -> \->_s0(odd(s(x1)),false) # label(csreplacement) # label(non_clause). [assumption]. 6 \->*_s0(even(x1),true) -> \->_s0(odd(s(x1)),true) # label(csreplacement) # label(non_clause). [assumption]. 7 \->_s0(x,y) & \->*_s0(y,z) -> \->*_s0(x,z) # label(cstransitivity) # label(non_clause). [assumption]. 8 (exists x3 \->*_s0(odd(x3),true)) # label(goal) # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). -\->_s0(x,y) | \->_s0(even(x),even(y)) # label(cscongruence). [clausify(1)]. -\->_s0(x,y) | \->_s0(odd(x),odd(y)) # label(cscongruence). [clausify(2)]. \->_s0(even(0),true) # label(csreplacement). [assumption]. -\->*_s0(even(x),true) | \->_s0(even(s(x)),false) # label(csreplacement). [clausify(3)]. -\->*_s0(odd(x),true) | \->_s0(even(s(x)),true) # label(csreplacement). [clausify(4)]. \->_s0(odd(0),false) # label(csreplacement). [assumption]. -\->*_s0(odd(x),true) | \->_s0(odd(s(x)),false) # label(csreplacement). [clausify(5)]. -\->*_s0(even(x),true) | \->_s0(odd(s(x)),true) # label(csreplacement). [clausify(6)]. \->*_s0(x,x) # label(csreflexivity). [assumption]. -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(7)]. -\->*_s0(odd(x),true) # label(goal). [deny(8)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % copying label goal to answer in negative clause Term ordering decisions: Predicate symbol precedence: predicate_order([ \->_s0, \->*_s0 ]). Function symbol precedence: function_order([ true, false, 0, even, odd, s ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(neg_binary_resolution). % (HNE depth_diff=-6) % clear(ordered_res). % (HNE depth_diff=-6) % set(ur_resolution). % (HNE depth_diff=-6) % set(ur_resolution) -> set(pos_ur_resolution). % set(ur_resolution) -> set(neg_ur_resolution). Auto_process settings: (no changes). kept: 9 -\->_s0(x,y) | \->_s0(even(x),even(y)) # label(cscongruence). [clausify(1)]. kept: 10 -\->_s0(x,y) | \->_s0(odd(x),odd(y)) # label(cscongruence). [clausify(2)]. kept: 11 \->_s0(even(0),true) # label(csreplacement). [assumption]. kept: 12 -\->*_s0(even(x),true) | \->_s0(even(s(x)),false) # label(csreplacement). [clausify(3)]. kept: 13 -\->*_s0(odd(x),true) | \->_s0(even(s(x)),true) # label(csreplacement). [clausify(4)]. kept: 14 \->_s0(odd(0),false) # label(csreplacement). [assumption]. kept: 15 -\->*_s0(odd(x),true) | \->_s0(odd(s(x)),false) # label(csreplacement). [clausify(5)]. kept: 16 -\->*_s0(even(x),true) | \->_s0(odd(s(x)),true) # label(csreplacement). [clausify(6)]. kept: 17 \->*_s0(x,x) # label(csreflexivity). [assumption]. kept: 18 -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(7)]. kept: 19 -\->*_s0(odd(x),true) # label(goal) # answer(goal). [deny(8)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 9 -\->_s0(x,y) | \->_s0(even(x),even(y)) # label(cscongruence). [clausify(1)]. 10 -\->_s0(x,y) | \->_s0(odd(x),odd(y)) # label(cscongruence). [clausify(2)]. 11 \->_s0(even(0),true) # label(csreplacement). [assumption]. 12 -\->*_s0(even(x),true) | \->_s0(even(s(x)),false) # label(csreplacement). [clausify(3)]. 14 \->_s0(odd(0),false) # label(csreplacement). [assumption]. 16 -\->*_s0(even(x),true) | \->_s0(odd(s(x)),true) # label(csreplacement). [clausify(6)]. 17 \->*_s0(x,x) # label(csreflexivity). [assumption]. 18 -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(7)]. 19 -\->*_s0(odd(x),true) # label(goal) # answer(goal). [deny(8)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=8): 9 -\->_s0(x,y) | \->_s0(even(x),even(y)) # label(cscongruence). [clausify(1)]. given #2 (I,wt=8): 10 -\->_s0(x,y) | \->_s0(odd(x),odd(y)) # label(cscongruence). [clausify(2)]. given #3 (I,wt=4): 11 \->_s0(even(0),true) # label(csreplacement). [assumption]. given #4 (I,wt=9): 12 -\->*_s0(even(x),true) | \->_s0(even(s(x)),false) # label(csreplacement). [clausify(3)]. given #5 (I,wt=4): 14 \->_s0(odd(0),false) # label(csreplacement). [assumption]. given #6 (I,wt=9): 16 -\->*_s0(even(x),true) | \->_s0(odd(s(x)),true) # label(csreplacement). [clausify(6)]. given #7 (I,wt=3): 17 \->*_s0(x,x) # label(csreflexivity). [assumption]. given #8 (I,wt=9): 18 -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(7)]. given #9 (I,wt=4): 19 -\->*_s0(odd(x),true) # label(goal) # answer(goal). [deny(8)]. given #10 (A,wt=6): 20 \->_s0(odd(even(0)),odd(true)). [ur(10,a,11,a)]. given #11 (F,wt=3): 28 -\->*_s0(false,true) # answer(goal). [ur(18,a,14,a,c,19,a)]. given #12 (F,wt=3): 33 -\->_s0(false,true) # answer(goal). [ur(18,b,17,a,c,28,a)]. given #13 (F,wt=4): 27 -\->_s0(odd(x),true) # answer(goal). [ur(18,b,17,a,c,19,a)]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds: goal. % Length of proof is 12. % Level of proof is 4. % Maximum clause weight is 9.000. % Given clauses 13. 6 \->*_s0(even(x1),true) -> \->_s0(odd(s(x1)),true) # label(csreplacement) # label(non_clause). [assumption]. 7 \->_s0(x,y) & \->*_s0(y,z) -> \->*_s0(x,z) # label(cstransitivity) # label(non_clause). [assumption]. 8 (exists x3 \->*_s0(odd(x3),true)) # label(goal) # label(non_clause) # label(goal). [goal]. 11 \->_s0(even(0),true) # label(csreplacement). [assumption]. 16 -\->*_s0(even(x),true) | \->_s0(odd(s(x)),true) # label(csreplacement). [clausify(6)]. 17 \->*_s0(x,x) # label(csreflexivity). [assumption]. 18 -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(7)]. 19 -\->*_s0(odd(x),true) # label(goal) # answer(goal). [deny(8)]. 25 \->*_s0(even(0),true). [ur(18,a,11,a,b,17,a)]. 27 -\->_s0(odd(x),true) # answer(goal). [ur(18,b,17,a,c,19,a)]. 34 -\->*_s0(even(x),true) # answer(goal). [resolve(27,a,16,b)]. 35 $F # answer(goal). [resolve(34,a,25,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=13. Generated=27. Kept=26. proofs=1. Usable=13. Sos=10. Demods=0. Limbo=0, Disabled=13. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=1. Back_subsumed=2. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=14. Megabytes=0.08. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 2773194 exit (max_proofs) Thu Jun 27 11:11:08 2024 The problem is feasible. CRule InfChecker Info: odd(0) -> false Rule remains Proof: NO_CONDS CRule InfChecker Info: odd(s(x)) -> false | odd(x) \->* true Rule remains Proof: ALREADY_CHECKED_FEASIBLE_CONDS CRule InfChecker Info: odd(s(x)) -> true | even(x) \->* true Rule remains Proof: ALREADY_CHECKED_FEASIBLE_CONDS Problem 1: Problem 1: Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x) (REPLACEMENT-MAP (even 1) (odd 1) (0) (false) (s) (true) ) (RULES even(0) -> true even(s(x)) -> false | even(x) \->* true even(s(x)) -> true | odd(x) \->* true odd(0) -> false odd(s(x)) -> false | odd(x) \->* true odd(s(x)) -> true | even(x) \->* true ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Critical Pairs CProcedure: -> Rules: even(0) -> true even(s(x)) -> false | even(x) \->* true even(s(x)) -> true | odd(x) \->* true odd(0) -> false odd(s(x)) -> false | odd(x) \->* true odd(s(x)) -> true | even(x) \->* true -> Vars: "x" -> Rlps: crule: even(0) -> true, id: 1, possubterms: even(0)-> [], 0-> [1] crule: even(s(x)) -> false | even(x) \->* true, id: 2, possubterms: even(s(x))-> [], s(x)-> [1] crule: even(s(x)) -> true | odd(x) \->* true, id: 3, possubterms: even(s(x))-> [], s(x)-> [1] crule: odd(0) -> false, id: 4, possubterms: odd(0)-> [], 0-> [1] crule: odd(s(x)) -> false | odd(x) \->* true, id: 5, possubterms: odd(s(x))-> [], s(x)-> [1] crule: odd(s(x)) -> true | even(x) \->* true, id: 6, possubterms: odd(s(x))-> [], s(x)-> [1] -> Unifications: R3 unifies with R2 at p: [], l: even(s(x)), lp: even(s(x)), conds: {odd(x) \->* true, even(x') \->* true}, sig: {x -> x'}, l': even(s(x')), r: true, r': false R6 unifies with R5 at p: [], l: odd(s(x)), lp: odd(s(x)), conds: {even(x) \->* true, odd(x') \->* true}, sig: {x -> x'}, l': odd(s(x')), r: true, r': false -> Critical pairs info: | even(x') \->* true, odd(x') \->* true => Not trivial, Overlay, Proper, NW2, N1 -> Problem conclusions: Left linear, Right linear, Linear, Weakly left-Linear Not weakly orthogonal, Not almost orthogonal, Not orthogonal, Not strongly orthogonal CTRS Type: 1 Deterministic, Strongly deterministic Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS Maybe right-stable CTRS, Overlay CTRS Maybe normal CTRS, Maybe almost normal CTRS ECCPs not considered Maybe terminating CTRS, Maybe operational terminating CTRS Maybe joinable CCPs Maybe level confluent, Maybe confluent Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (even 1) (odd 1) (0) (false) (s) (true) ) (RULES even(0) -> true even(s(x)) -> false | even(x) \->* true even(s(x)) -> true | odd(x) \->* true odd(0) -> false odd(s(x)) -> false | odd(x) \->* true odd(s(x)) -> true | even(x) \->* true ) Critical Pairs: | even(x') \->* true, odd(x') \->* true => Not trivial, Overlay, Proper, NW2, N1 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Improper Critical Pairs Procedure: No iCCPs found Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (even 1) (odd 1) (0) (false) (s) (true) ) (RULES even(0) -> true even(s(x)) -> false | even(x) \->* true even(s(x)) -> true | odd(x) \->* true odd(0) -> false odd(s(x)) -> false | odd(x) \->* true odd(s(x)) -> true | even(x) \->* true ) Critical Pairs: | even(x') \->* true, odd(x') \->* true => Not trivial, Overlay, Proper, NW2, N1 -> Problem conclusions: Left linear, Right linear, Linear, Weakly left-Linear Not weakly orthogonal, Not almost orthogonal, Not orthogonal, Not strongly orthogonal CTRS Type: 1 Deterministic, Strongly deterministic Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS Maybe right-stable CTRS, Overlay CTRS Maybe normal CTRS, Maybe almost normal CTRS ECCPs considered Maybe terminating CTRS, Maybe operational terminating CTRS Maybe joinable CCPs Maybe level confluent, Maybe confluent ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Conditional Variable Pairs Procedure: No CVPs found All CVPs join by definition -> Problem conclusions: Left linear, Right linear, Linear, Weakly left-Linear Not weakly orthogonal, Not almost orthogonal, Not orthogonal, Not strongly orthogonal CTRS Type: 1 Deterministic, Strongly deterministic Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS Maybe right-stable CTRS, Overlay CTRS Maybe normal CTRS, Maybe almost normal CTRS ECCPs considered Maybe terminating CTRS, Maybe operational terminating CTRS Maybe joinable CCPs Maybe level confluent, Maybe confluent Problem 1: Problem 1: Clean Infeasible CCPs Procedure: Num of CPIs: 1 Timeout: 30 Timeout for each infeasibility problem: 30 s | even(x') \->* true, odd(x') \->* true => Not trivial, Overlay, Proper, NW2, N1 (PROBLEM INFEASIBILITY) (STRATEGY CONTEXTSENSITIVE (even 1) (odd 1) (0) (false) (s) (true) ) (VAR x xap) (RULES even(0) -> true even(s(x)) -> false | even(x) \->* true even(s(x)) -> true | odd(x) \->* true odd(0) -> false odd(s(x)) -> false | odd(x) \->* true odd(s(x)) -> true | even(x) \->* true) (VAR x2) (CONDITION even(x2) \->* true, odd(x2) \->* true) Proof: YES Problem 1: Infeasibility Problem: [(VAR vNonEmpty x xap vNonEmpty x2) (STRATEGY CONTEXTSENSITIVE (even 1) (odd 1) (0) (fSNonEmpty) (false) (s) (true) ) (RULES even(0) -> true even(s(x)) -> false | even(x) \->* true even(s(x)) -> true | odd(x) \->* true odd(0) -> false odd(s(x)) -> false | odd(x) \->* true odd(s(x)) -> true | even(x) \->* true ) ] Infeasibility Conditions: even(x2) \->* true, odd(x2) \->* true Problem 1: Obtaining a model using Mace4: -> Usable Rules: even(0) -> true even(s(x)) -> false | even(x) \->* true even(s(x)) -> true | odd(x) \->* true odd(0) -> false odd(s(x)) -> false | odd(x) \->* true odd(s(x)) -> true | even(x) \->* true -> Mace4 Output: ============================== Mace4 ================================= Mace4 (64) version 2009-11A, November 2009. Process 2774099 was started by sandbox on z021.star.cs.uiowa.edu, Thu Jun 27 11:11:28 2024 The command was "./mace4 -c -f /tmp/mace42774086-2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file /tmp/mace42774086-2.in assign(max_seconds,10). formulas(assumptions). \->(x1,y) -> \->(even(x1),even(y)) # label(cscongruence). \->(x1,y) -> \->(odd(x1),odd(y)) # label(cscongruence). \->(even(0),true) # label(csreplacement). \->*(even(x1),true) -> \->(even(s(x1)),false) # label(csreplacement). \->*(odd(x1),true) -> \->(even(s(x1)),true) # label(csreplacement). \->(odd(0),false) # label(csreplacement). \->*(odd(x1),true) -> \->(odd(s(x1)),false) # label(csreplacement). \->*(even(x1),true) -> \->(odd(s(x1)),true) # label(csreplacement). \->*(x,x) # label(csreflexivity). \->(x,y) & \->*(y,z) -> \->*(x,z) # label(cstransitivity). end_of_list. formulas(goals). (exists x4 (\->*(even(x4),true) & \->*(odd(x4),true))) # label(goal). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 \->(x1,y) -> \->(even(x1),even(y)) # label(cscongruence) # label(non_clause). [assumption]. 2 \->(x1,y) -> \->(odd(x1),odd(y)) # label(cscongruence) # label(non_clause). [assumption]. 3 \->*(even(x1),true) -> \->(even(s(x1)),false) # label(csreplacement) # label(non_clause). [assumption]. 4 \->*(odd(x1),true) -> \->(even(s(x1)),true) # label(csreplacement) # label(non_clause). [assumption]. 5 \->*(odd(x1),true) -> \->(odd(s(x1)),false) # label(csreplacement) # label(non_clause). [assumption]. 6 \->*(even(x1),true) -> \->(odd(s(x1)),true) # label(csreplacement) # label(non_clause). [assumption]. 7 \->(x,y) & \->*(y,z) -> \->*(x,z) # label(cstransitivity) # label(non_clause). [assumption]. 8 (exists x4 (\->*(even(x4),true) & \->*(odd(x4),true))) # label(goal) # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== CLAUSES FOR SEARCH ==================== formulas(mace4_clauses). -\->(x,y) | \->(even(x),even(y)) # label(cscongruence). -\->(x,y) | \->(odd(x),odd(y)) # label(cscongruence). \->(even(0),true) # label(csreplacement). -\->*(even(x),true) | \->(even(s(x)),false) # label(csreplacement). -\->*(odd(x),true) | \->(even(s(x)),true) # label(csreplacement). \->(odd(0),false) # label(csreplacement). -\->*(odd(x),true) | \->(odd(s(x)),false) # label(csreplacement). -\->*(even(x),true) | \->(odd(s(x)),true) # label(csreplacement). \->*(x,x) # label(csreflexivity). -\->(x,y) | -\->*(y,z) | \->*(x,z) # label(cstransitivity). -\->*(even(x),true) | -\->*(odd(x),true) # label(goal). end_of_list. ============================== end of clauses for search ============= % There are no natural numbers in the input. ============================== DOMAIN SIZE 2 ========================= ============================== MODEL ================================= interpretation( 2, [number=1, seconds=0], [ function(0, [ 0 ]), function(false, [ 0 ]), function(true, [ 1 ]), function(even(_), [ 1, 0 ]), function(odd(_), [ 0, 1 ]), function(s(_), [ 1, 0 ]), relation(\->*(_,_), [ 1, 0, 0, 1 ]), relation(\->(_,_), [ 1, 0, 0, 1 ]) ]). ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 2. Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=30, kept=26. Selections=8, assignments=12, propagations=22, current_models=1. Rewrite_terms=125, rewrite_bools=71, indexes=27. Rules_from_neg_clauses=6, cross_offs=6. ============================== end of statistics ===================== User_CPU=0.01, System_CPU=0.00, Wall_clock=0. Exiting with 1 model. Process 2774099 exit (max_models) Thu Jun 27 11:11:28 2024 The process finished Thu Jun 27 11:11:28 2024 Mace4 cooked interpretation: The problem is infeasible. -> Problem conclusions: Left linear, Right linear, Linear, Weakly left-Linear Weakly orthogonal, Almost orthogonal, Orthogonal, Strongly orthogonal CTRS Type: 1 Deterministic, Strongly deterministic Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS Maybe right-stable CTRS, Overlay CTRS Maybe normal CTRS, Maybe almost normal CTRS ECCPs considered Maybe terminating CTRS, Maybe operational terminating CTRS Joinable CCPs Maybe level confluent, Confluent Resulting CCPs: No CCPs left The problem is confluent.