20.038/20.038 NO 20.038/20.038 20.038/20.038 Problem 1: 20.038/20.038 20.038/20.038 20.038/20.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.038/20.038 Confluence Problem: 20.038/20.038 (VAR vNonEmpty x y z) 20.038/20.038 (REPLACEMENT-MAP 20.038/20.038 (between 1, 2, 3) 20.038/20.038 (down 1) 20.038/20.038 (up 1) 20.038/20.038 (fSNonEmpty) 20.038/20.038 (s 1) 20.038/20.038 (true) 20.038/20.038 ) 20.038/20.038 (RULES 20.038/20.038 between(x,y,z) -> true | up(x) ->* y, down(z) ->* y 20.038/20.038 down(s(x)) -> down(x) 20.038/20.038 down(x) -> x 20.038/20.038 up(x) -> up(s(x)) 20.038/20.038 up(x) -> x 20.038/20.038 ) 20.038/20.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.038/20.038 20.038/20.038 20.038/20.038 Problem 1: 20.038/20.038 20.038/20.038 Inlining of Conditions Processor [STERN17]: 20.038/20.038 20.038/20.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.038/20.038 Confluence Problem: 20.038/20.038 (VAR vNonEmpty x y z) 20.038/20.038 (REPLACEMENT-MAP 20.038/20.038 (between 1, 2, 3) 20.038/20.038 (down 1) 20.038/20.038 (up 1) 20.038/20.038 (fSNonEmpty) 20.038/20.038 (s 1) 20.038/20.038 (true) 20.038/20.038 ) 20.038/20.038 (RULES 20.038/20.038 between(x,y,z) -> true | down(z) ->* y, up(x) ->* y 20.038/20.038 down(s(x)) -> down(x) 20.038/20.038 down(x) -> x 20.038/20.038 up(x) -> up(s(x)) 20.038/20.038 up(x) -> x 20.038/20.038 ) 20.038/20.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.038/20.038 20.038/20.038 20.038/20.038 Problem 1: 20.038/20.038 20.038/20.038 Clean CTRS Processor: 20.038/20.038 20.038/20.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.038/20.038 Confluence Problem: 20.038/20.038 (VAR x y z) 20.038/20.038 (REPLACEMENT-MAP 20.038/20.038 (between 1, 2, 3) 20.038/20.038 (down 1) 20.038/20.038 (up 1) 20.038/20.038 (fSNonEmpty) 20.038/20.038 (s 1) 20.038/20.038 (true) 20.038/20.038 ) 20.038/20.038 (RULES 20.038/20.038 between(x,y,z) -> true | down(z) ->* y, up(x) ->* y 20.038/20.038 down(s(x)) -> down(x) 20.038/20.038 down(x) -> x 20.038/20.038 up(x) -> up(s(x)) 20.038/20.038 up(x) -> x 20.038/20.038 ) 20.038/20.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.038/20.038 20.038/20.038 CRule InfChecker Info: 20.038/20.038 between(x,y,z) -> true | down(z) ->* y, up(x) ->* y 20.038/20.038 Rule remains 20.038/20.038 Proof: 20.038/20.038 NO 20.038/20.038 20.038/20.038 Problem 1: 20.038/20.038 20.038/20.038 Infeasibility Problem: 20.038/20.038 [(VAR vNonEmpty x y z vNonEmpty x y z) 20.038/20.038 (STRATEGY CONTEXTSENSITIVE 20.038/20.038 (between 1 2 3) 20.038/20.038 (down 1) 20.038/20.038 (up 1) 20.038/20.038 (fSNonEmpty) 20.038/20.038 (s 1) 20.038/20.038 (true) 20.038/20.038 ) 20.038/20.038 (RULES 20.038/20.038 between(x,y,z) -> true | down(z) ->* y, up(x) ->* y 20.038/20.038 down(s(x)) -> down(x) 20.038/20.038 down(x) -> x 20.038/20.038 up(x) -> up(s(x)) 20.038/20.038 up(x) -> x 20.038/20.038 )] 20.038/20.038 20.038/20.038 Infeasibility Conditions: 20.038/20.038 down(z) ->* y, up(x) ->* y 20.038/20.038 20.038/20.038 Problem 1: 20.038/20.038 20.038/20.038 Obtaining a proof using Prover9: 20.038/20.038 20.038/20.038 -> Prover9 Output: 20.038/20.038 ============================== Prover9 =============================== 20.038/20.038 Prover9 (64) version 2009-11A, November 2009. 20.038/20.038 Process 61518 was started by ubuntu on ubuntu, 20.038/20.038 Wed Mar 9 09:48:35 2022 20.038/20.038 The command was "./prover9 -f /tmp/prover961509-0.in". 20.038/20.038 ============================== end of head =========================== 20.038/20.038 20.038/20.038 ============================== INPUT ================================= 20.038/20.038 20.038/20.038 % Reading from file /tmp/prover961509-0.in 20.038/20.038 20.038/20.038 assign(max_seconds,20). 20.038/20.038 20.038/20.038 formulas(assumptions). 20.038/20.038 ->_s0(x1,y) -> ->_s0(between(x1,x2,x3),between(y,x2,x3)) # label(congruence). 20.038/20.038 ->_s0(x2,y) -> ->_s0(between(x1,x2,x3),between(x1,y,x3)) # label(congruence). 20.038/20.038 ->_s0(x3,y) -> ->_s0(between(x1,x2,x3),between(x1,x2,y)) # label(congruence). 20.038/20.038 ->_s0(x1,y) -> ->_s0(down(x1),down(y)) # label(congruence). 20.038/20.038 ->_s0(x1,y) -> ->_s0(up(x1),up(y)) # label(congruence). 20.038/20.038 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence). 20.038/20.038 ->*_s0(down(x3),x2) & ->*_s0(up(x1),x2) -> ->_s0(between(x1,x2,x3),true) # label(replacement). 20.038/20.038 ->_s0(down(s(x1)),down(x1)) # label(replacement). 20.038/20.038 ->_s0(down(x1),x1) # label(replacement). 20.038/20.038 ->_s0(up(x1),up(s(x1))) # label(replacement). 20.038/20.038 ->_s0(up(x1),x1) # label(replacement). 20.038/20.038 ->*_s0(x,x) # label(reflexivity). 20.038/20.038 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 20.038/20.038 end_of_list. 20.038/20.038 20.038/20.038 formulas(goals). 20.038/20.038 (exists x5 exists x6 exists x7 (->*_s0(down(x7),x6) & ->*_s0(up(x5),x6))) # label(goal). 20.038/20.038 end_of_list. 20.038/20.038 20.038/20.038 ============================== end of input ========================== 20.038/20.038 20.038/20.038 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 20.038/20.038 20.038/20.038 % Formulas that are not ordinary clauses: 20.038/20.038 1 ->_s0(x1,y) -> ->_s0(between(x1,x2,x3),between(y,x2,x3)) # label(congruence) # label(non_clause). [assumption]. 20.038/20.038 2 ->_s0(x2,y) -> ->_s0(between(x1,x2,x3),between(x1,y,x3)) # label(congruence) # label(non_clause). [assumption]. 20.038/20.038 3 ->_s0(x3,y) -> ->_s0(between(x1,x2,x3),between(x1,x2,y)) # label(congruence) # label(non_clause). [assumption]. 20.038/20.038 4 ->_s0(x1,y) -> ->_s0(down(x1),down(y)) # label(congruence) # label(non_clause). [assumption]. 20.038/20.038 5 ->_s0(x1,y) -> ->_s0(up(x1),up(y)) # label(congruence) # label(non_clause). [assumption]. 20.038/20.038 6 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 20.038/20.038 7 ->*_s0(down(x3),x2) & ->*_s0(up(x1),x2) -> ->_s0(between(x1,x2,x3),true) # label(replacement) # label(non_clause). [assumption]. 20.038/20.038 8 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 20.038/20.038 9 (exists x5 exists x6 exists x7 (->*_s0(down(x7),x6) & ->*_s0(up(x5),x6))) # label(goal) # label(non_clause) # label(goal). [goal]. 20.038/20.038 20.038/20.038 ============================== end of process non-clausal formulas === 20.038/20.038 20.038/20.038 ============================== PROCESS INITIAL CLAUSES =============== 20.038/20.038 20.038/20.038 % Clauses before input processing: 20.038/20.038 20.038/20.038 formulas(usable). 20.038/20.038 end_of_list. 20.038/20.038 20.038/20.038 formulas(sos). 20.038/20.038 -->_s0(x,y) | ->_s0(between(x,z,u),between(y,z,u)) # label(congruence). [clausify(1)]. 20.038/20.038 -->_s0(x,y) | ->_s0(between(z,x,u),between(z,y,u)) # label(congruence). [clausify(2)]. 20.038/20.038 -->_s0(x,y) | ->_s0(between(z,u,x),between(z,u,y)) # label(congruence). [clausify(3)]. 20.038/20.038 -->_s0(x,y) | ->_s0(down(x),down(y)) # label(congruence). [clausify(4)]. 20.038/20.038 -->_s0(x,y) | ->_s0(up(x),up(y)) # label(congruence). [clausify(5)]. 20.038/20.038 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(6)]. 20.038/20.038 -->*_s0(down(x),y) | -->*_s0(up(z),y) | ->_s0(between(z,y,x),true) # label(replacement). [clausify(7)]. 20.038/20.038 ->_s0(down(s(x)),down(x)) # label(replacement). [assumption]. 20.038/20.038 ->_s0(down(x),x) # label(replacement). [assumption]. 20.038/20.038 ->_s0(up(x),up(s(x))) # label(replacement). [assumption]. 20.038/20.038 ->_s0(up(x),x) # label(replacement). [assumption]. 20.038/20.038 ->*_s0(x,x) # label(reflexivity). [assumption]. 20.038/20.038 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 20.038/20.038 -->*_s0(down(x),y) | -->*_s0(up(z),y) # label(goal). [deny(9)]. 20.038/20.038 end_of_list. 20.038/20.038 20.038/20.038 formulas(demodulators). 20.038/20.038 end_of_list. 20.038/20.038 20.038/20.038 ============================== PREDICATE ELIMINATION ================= 20.038/20.038 20.038/20.038 No predicates eliminated. 20.038/20.038 20.038/20.038 ============================== end predicate elimination ============= 20.038/20.038 20.038/20.038 Auto_denials: 20.038/20.038 % copying label goal to answer in negative clause 20.038/20.038 20.038/20.038 Term ordering decisions: 20.038/20.038 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 20.038/20.038 Function symbol precedence: function_order([ true, down, up, s, between ]). 20.038/20.038 After inverse_order: (no changes). 20.038/20.038 Unfolding symbols: (none). 20.038/20.038 20.038/20.038 Auto_inference settings: 20.038/20.038 % set(neg_binary_resolution). % (HNE depth_diff=-6) 20.038/20.038 % clear(ordered_res). % (HNE depth_diff=-6) 20.038/20.038 % set(ur_resolution). % (HNE depth_diff=-6) 20.038/20.038 % set(ur_resolution) -> set(pos_ur_resolution). 20.038/20.038 % set(ur_resolution) -> set(neg_ur_resolution). 20.038/20.038 20.038/20.038 Auto_process settings: 20.038/20.038 % set(unit_deletion). % (Horn set with negative nonunits) 20.038/20.038 20.038/20.038 kept: 10 -->_s0(x,y) | ->_s0(between(x,z,u),between(y,z,u)) # label(congruence). [clausify(1)]. 20.038/20.038 kept: 11 -->_s0(x,y) | ->_s0(between(z,x,u),between(z,y,u)) # label(congruence). [clausify(2)]. 20.038/20.038 kept: 12 -->_s0(x,y) | ->_s0(between(z,u,x),between(z,u,y)) # label(congruence). [clausify(3)]. 20.038/20.038 kept: 13 -->_s0(x,y) | ->_s0(down(x),down(y)) # label(congruence). [clausify(4)]. 20.038/20.038 kept: 14 -->_s0(x,y) | ->_s0(up(x),up(y)) # label(congruence). [clausify(5)]. 20.038/20.038 kept: 15 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(6)]. 20.038/20.038 kept: 16 -->*_s0(down(x),y) | -->*_s0(up(z),y) | ->_s0(between(z,y,x),true) # label(replacement). [clausify(7)]. 20.038/20.038 kept: 17 ->_s0(down(s(x)),down(x)) # label(replacement). [assumption]. 20.038/20.038 kept: 18 ->_s0(down(x),x) # label(replacement). [assumption]. 20.038/20.038 kept: 19 ->_s0(up(x),up(s(x))) # label(replacement). [assumption]. 20.038/20.038 kept: 20 ->_s0(up(x),x) # label(replacement). [assumption]. 20.038/20.038 kept: 21 ->*_s0(x,x) # label(reflexivity). [assumption]. 20.038/20.038 kept: 22 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 20.038/20.038 kept: 23 -->*_s0(down(x),y) | -->*_s0(up(z),y) # label(goal) # answer(goal). [deny(9)]. 20.038/20.038 20.038/20.038 ============================== end of process initial clauses ======== 20.038/20.038 20.038/20.038 ============================== CLAUSES FOR SEARCH ==================== 20.038/20.038 20.038/20.038 % Clauses after input processing: 20.038/20.038 20.038/20.038 formulas(usable). 20.038/20.038 end_of_list. 20.038/20.038 20.038/20.038 formulas(sos). 20.038/20.038 10 -->_s0(x,y) | ->_s0(between(x,z,u),between(y,z,u)) # label(congruence). [clausify(1)]. 20.038/20.038 11 -->_s0(x,y) | ->_s0(between(z,x,u),between(z,y,u)) # label(congruence). [clausify(2)]. 20.038/20.038 12 -->_s0(x,y) | ->_s0(between(z,u,x),between(z,u,y)) # label(congruence). [clausify(3)]. 20.038/20.038 13 -->_s0(x,y) | ->_s0(down(x),down(y)) # label(congruence). [clausify(4)]. 20.038/20.038 14 -->_s0(x,y) | ->_s0(up(x),up(y)) # label(congruence). [clausify(5)]. 20.038/20.038 15 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(6)]. 20.038/20.038 17 ->_s0(down(s(x)),down(x)) # label(replacement). [assumption]. 20.038/20.038 18 ->_s0(down(x),x) # label(replacement). [assumption]. 20.038/20.038 19 ->_s0(up(x),up(s(x))) # label(replacement). [assumption]. 20.038/20.038 20 ->_s0(up(x),x) # label(replacement). [assumption]. 20.038/20.038 21 ->*_s0(x,x) # label(reflexivity). [assumption]. 20.038/20.038 22 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 20.038/20.038 23 -->*_s0(down(x),y) | -->*_s0(up(z),y) # label(goal) # answer(goal). [deny(9)]. 20.038/20.038 end_of_list. 20.038/20.038 20.038/20.038 formulas(demodulators). 20.038/20.038 end_of_list. 20.038/20.038 20.038/20.038 ============================== end of clauses for search ============= 20.038/20.038 20.038/20.038 ============================== SEARCH ================================ 20.038/20.038 20.038/20.038 % Starting search at 0.00 seconds. 20.038/20.038 20.038/20.038 given #1 (I,wt=12): 10 -->_s0(x,y) | ->_s0(between(x,z,u),between(y,z,u)) # label(congruence). [clausify(1)]. 20.038/20.038 20.038/20.038 given #2 (I,wt=12): 11 -->_s0(x,y) | ->_s0(between(z,x,u),between(z,y,u)) # label(congruence). [clausify(2)]. 20.038/20.038 20.038/20.038 given #3 (I,wt=12): 12 -->_s0(x,y) | ->_s0(between(z,u,x),between(z,u,y)) # label(congruence). [clausify(3)]. 20.038/20.038 20.038/20.038 given #4 (I,wt=8): 13 -->_s0(x,y) | ->_s0(down(x),down(y)) # label(congruence). [clausify(4)]. 20.038/20.038 20.038/20.038 given #5 (I,wt=8): 14 -->_s0(x,y) | ->_s0(up(x),up(y)) # label(congruence). [clausify(5)]. 20.038/20.038 20.038/20.038 given #6 (I,wt=8): 15 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(6)]. 20.038/20.038 20.038/20.038 given #7 (I,wt=6): 17 ->_s0(down(s(x)),down(x)) # label(replacement). [assumption]. 20.038/20.038 20.038/20.038 given #8 (I,wt=4): 18 ->_s0(down(x),x) # label(replacement). [assumption]. 20.038/20.038 20.038/20.038 given #9 (I,wt=6): 19 ->_s0(up(x),up(s(x))) # label(replacement). [assumption]. 20.038/20.038 20.038/20.038 given #10 (I,wt=4): 20 ->_s0(up(x),x) # label(replacement). [assumption]. 20.038/20.038 20.038/20.038 given #11 (I,wt=3): 21 ->*_s0(x,x) # label(reflexivity). [assumption]. 20.038/20.038 20.038/20.038 given #12 (I,wt=9): 22 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 20.038/20.038 20.038/20.038 given #13 (I,wt=8): 23 -->*_s0(down(x),y) | -->*_s0(up(z),y) # label(goal) # answer(goal). [deny(9)]. 20.038/20.038 20.038/20.038 ============================== PROOF ================================= 20.038/20.038 20.038/20.038 % Proof 1 at 0.01 (+ 0.00) seconds: goal. 20.038/20.038 % Length of proof is 9. 20.038/20.038 % Level of proof is 3. 20.038/20.038 % Maximum clause weight is 9.000. 20.038/20.038 % Given clauses 13. 20.038/20.038 20.038/20.038 8 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 20.038/20.038 9 (exists x5 exists x6 exists x7 (->*_s0(down(x7),x6) & ->*_s0(up(x5),x6))) # label(goal) # label(non_clause) # label(goal). [goal]. 20.038/20.038 20 ->_s0(up(x),x) # label(replacement). [assumption]. 20.038/20.038 21 ->*_s0(x,x) # label(reflexivity). [assumption]. 20.038/20.038 22 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 20.038/20.038 23 -->*_s0(down(x),y) | -->*_s0(up(z),y) # label(goal) # answer(goal). [deny(9)]. 20.038/20.038 46 ->*_s0(up(x),x). [ur(22,a,20,a,b,21,a)]. 20.038/20.038 51 -->*_s0(up(x),down(y)) # answer(goal). [resolve(23,a,21,a)]. 20.038/20.038 52 $F # answer(goal). [resolve(51,a,46,a)]. 20.038/20.038 20.038/20.038 ============================== end of proof ========================== 20.038/20.038 20.038/20.038 ============================== STATISTICS ============================ 20.038/20.038 20.038/20.038 Given=13. Generated=44. Kept=42. proofs=1. 20.038/20.038 Usable=13. Sos=26. Demods=0. Limbo=1, Disabled=15. Hints=0. 20.038/20.038 Kept_by_rule=0, Deleted_by_rule=0. 20.038/20.038 Forward_subsumed=2. Back_subsumed=1. 20.038/20.038 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 20.038/20.038 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 20.038/20.038 Demod_attempts=0. Demod_rewrites=0. 20.038/20.038 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 20.038/20.038 Nonunit_fsub_feature_tests=4. Nonunit_bsub_feature_tests=19. 20.038/20.038 Megabytes=0.11. 20.038/20.038 User_CPU=0.01, System_CPU=0.00, Wall_clock=0. 20.038/20.038 20.038/20.038 ============================== end of statistics ===================== 20.038/20.038 20.038/20.038 ============================== end of search ========================= 20.038/20.038 20.038/20.038 THEOREM PROVED 20.038/20.038 20.038/20.038 Exiting with 1 proof. 20.038/20.038 20.038/20.038 Process 61518 exit (max_proofs) Wed Mar 9 09:48:35 2022 20.038/20.038 20.038/20.038 20.038/20.038 The problem is feasible. 20.038/20.038 20.038/20.038 20.038/20.038 CRule InfChecker Info: 20.038/20.038 down(s(x)) -> down(x) 20.038/20.038 Rule remains 20.038/20.038 Proof: 20.038/20.038 NO_CONDS 20.038/20.038 20.038/20.038 CRule InfChecker Info: 20.038/20.038 down(x) -> x 20.038/20.038 Rule remains 20.038/20.038 Proof: 20.038/20.038 NO_CONDS 20.038/20.038 20.038/20.038 CRule InfChecker Info: 20.038/20.038 up(x) -> up(s(x)) 20.038/20.038 Rule remains 20.038/20.038 Proof: 20.038/20.038 NO_CONDS 20.038/20.038 20.038/20.038 CRule InfChecker Info: 20.038/20.038 up(x) -> x 20.038/20.038 Rule remains 20.038/20.038 Proof: 20.038/20.038 NO_CONDS 20.038/20.038 20.038/20.038 Problem 1: 20.038/20.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.038/20.038 Confluence Problem: 20.038/20.038 (VAR x y z) 20.038/20.038 (REPLACEMENT-MAP 20.038/20.038 (between 1, 2, 3) 20.038/20.038 (down 1) 20.038/20.038 (up 1) 20.038/20.038 (fSNonEmpty) 20.038/20.038 (s 1) 20.038/20.038 (true) 20.038/20.038 ) 20.038/20.038 (RULES 20.038/20.038 between(x,y,z) -> true | down(z) ->* y, up(x) ->* y 20.038/20.038 down(s(x)) -> down(x) 20.038/20.038 down(x) -> x 20.038/20.038 up(x) -> up(s(x)) 20.038/20.038 up(x) -> x 20.038/20.038 ) 20.038/20.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.038/20.038 20.038/20.038 Critical Pairs Processor: 20.038/20.038 -> Rules: 20.038/20.038 between(x,y,z) -> true | down(z) ->* y, up(x) ->* y 20.038/20.038 down(s(x)) -> down(x) 20.038/20.038 down(x) -> x 20.038/20.038 up(x) -> up(s(x)) 20.038/20.038 up(x) -> x 20.038/20.038 -> Vars: 20.038/20.038 "x", "y", "z" 20.038/20.038 20.038/20.038 -> Rlps: 20.038/20.038 crule: between(x,y,z) -> true | down(z) ->* y, up(x) ->* y, id: 1, possubterms: between(x,y,z)-> [] 20.038/20.038 crule: down(s(x)) -> down(x), id: 2, possubterms: down(s(x))-> [], s(x)-> [1] 20.038/20.038 crule: down(x) -> x, id: 3, possubterms: down(x)-> [] 20.038/20.038 crule: up(x) -> up(s(x)), id: 4, possubterms: up(x)-> [] 20.038/20.038 crule: up(x) -> x, id: 5, possubterms: up(x)-> [] 20.038/20.038 20.038/20.038 -> Unifications: 20.038/20.038 R3 unifies with R2 at p: [], l: down(x), lp: down(x), conds: {}, sig: {x -> s(x')}, l': down(s(x')), r: x, r': down(x') 20.038/20.038 R5 unifies with R4 at p: [], l: up(x), lp: up(x), conds: {}, sig: {x -> x'}, l': up(x'), r: x, r': up(s(x')) 20.038/20.038 20.038/20.038 -> Critical pairs info: 20.038/20.038 => Not trivial, Overlay, NW1, N1 20.038/20.038 => Not trivial, Overlay, NW1, N2 20.038/20.038 20.038/20.038 -> Problem conclusions: 20.038/20.038 Left linear, Right linear, Linear 20.038/20.038 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 20.038/20.038 CTRS Type: 1 20.038/20.038 Deterministic, Strongly deterministic 20.038/20.038 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 20.038/20.038 Maybe right-stable CTRS, Overlay CTRS 20.038/20.038 Maybe normal CTRS, Maybe almost normal CTRS 20.038/20.038 Maybe terminating CTRS, Maybe operational terminating CTRS, Maybe joinable CCPs 20.038/20.038 Maybe level confluent 20.038/20.038 Maybe confluent 20.038/20.038 20.038/20.038 Problem 1: 20.038/20.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.038/20.038 Confluence Problem: 20.038/20.038 (VAR x y z x') 20.038/20.038 (REPLACEMENT-MAP 20.038/20.038 (between 1, 2, 3) 20.038/20.038 (down 1) 20.038/20.038 (up 1) 20.038/20.038 (fSNonEmpty) 20.038/20.038 (s 1) 20.038/20.038 (true) 20.038/20.038 ) 20.038/20.038 (RULES 20.038/20.038 between(x,y,z) -> true | down(z) ->* y, up(x) ->* y 20.038/20.038 down(s(x)) -> down(x) 20.038/20.038 down(x) -> x 20.038/20.038 up(x) -> up(s(x)) 20.038/20.038 up(x) -> x 20.038/20.038 ) 20.038/20.038 Critical Pairs: 20.038/20.038 => Not trivial, Overlay, NW1, N1 20.038/20.038 => Not trivial, Overlay, NW1, N2 20.038/20.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.038/20.038 20.038/20.038 Conditional Critical Pairs Distributor Processor 20.038/20.038 20.038/20.038 Problem 1: 20.038/20.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.038/20.038 Confluence Problem: 20.038/20.038 (VAR x y z x') 20.038/20.038 (REPLACEMENT-MAP 20.038/20.038 (between 1, 2, 3) 20.038/20.038 (down 1) 20.038/20.038 (up 1) 20.038/20.038 (fSNonEmpty) 20.038/20.038 (s 1) 20.038/20.038 (true) 20.038/20.038 ) 20.038/20.038 (RULES 20.038/20.038 between(x,y,z) -> true | down(z) ->* y, up(x) ->* y 20.038/20.038 down(s(x)) -> down(x) 20.038/20.038 down(x) -> x 20.038/20.038 up(x) -> up(s(x)) 20.038/20.038 up(x) -> x 20.038/20.038 ) 20.038/20.038 Critical Pairs: 20.038/20.038 => Not trivial, Overlay, NW1, N1 20.038/20.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.038/20.038 20.038/20.038 Infeasible Convergence No Conditions CCP Processor: 20.038/20.038 Infeasible convergence? 20.038/20.038 YES 20.038/20.038 20.038/20.038 Problem 1: 20.038/20.038 20.038/20.038 Infeasibility Problem: 20.038/20.038 [(VAR vNonEmpty x y z x1 vNonEmpty z) 20.038/20.038 (STRATEGY CONTEXTSENSITIVE 20.038/20.038 (between 1 2 3) 20.038/20.038 (down 1) 20.038/20.038 (up 1) 20.038/20.038 (c_x1) 20.038/20.038 (fSNonEmpty) 20.038/20.038 (s 1) 20.038/20.038 (true) 20.038/20.038 ) 20.038/20.038 (RULES 20.038/20.038 between(x,y,z) -> true | down(z) ->* y, up(x) ->* y 20.038/20.038 down(s(x)) -> down(x) 20.038/20.038 down(x) -> x 20.038/20.038 up(x) -> up(s(x)) 20.038/20.038 up(x) -> x 20.038/20.038 )] 20.038/20.038 20.038/20.038 Infeasibility Conditions: 20.038/20.038 up(s(c_x1)) ->* z, c_x1 ->* z 20.038/20.038 20.038/20.038 Problem 1: 20.038/20.038 20.038/20.038 Obtaining a model using Mace4: 20.038/20.038 20.038/20.038 -> Usable Rules: 20.038/20.038 up(x) -> up(s(x)) 20.038/20.038 up(x) -> x 20.038/20.038 20.038/20.038 -> Mace4 Output: 20.038/20.038 ============================== Mace4 ================================= 20.038/20.038 Mace4 (64) version 2009-11A, November 2009. 20.038/20.038 Process 61544 was started by ubuntu on ubuntu, 20.038/20.038 Wed Mar 9 09:48:35 2022 20.038/20.038 The command was "./mace4 -c -f /tmp/mace461531-2.in". 20.038/20.038 ============================== end of head =========================== 20.038/20.038 20.038/20.038 ============================== INPUT ================================= 20.038/20.038 20.038/20.038 % Reading from file /tmp/mace461531-2.in 20.038/20.038 20.038/20.038 assign(max_seconds,20). 20.038/20.038 20.038/20.038 formulas(assumptions). 20.038/20.038 ->(x1,y) -> ->(between(x1,x2,x3),between(y,x2,x3)) # label(congruence). 20.038/20.038 ->(x2,y) -> ->(between(x1,x2,x3),between(x1,y,x3)) # label(congruence). 20.038/20.038 ->(x3,y) -> ->(between(x1,x2,x3),between(x1,x2,y)) # label(congruence). 20.038/20.038 ->(x1,y) -> ->(down(x1),down(y)) # label(congruence). 20.038/20.038 ->(x1,y) -> ->(up(x1),up(y)) # label(congruence). 20.038/20.038 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence). 20.038/20.038 ->(up(x1),up(s(x1))) # label(replacement). 20.038/20.038 ->(up(x1),x1) # label(replacement). 20.038/20.038 ->*(x,x) # label(reflexivity). 20.038/20.038 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 20.038/20.038 end_of_list. 20.038/20.038 20.038/20.038 formulas(goals). 20.038/20.038 (exists x6 (->*(up(s(c_x1)),x6) & ->*(c_x1,x6))) # label(goal). 20.038/20.038 end_of_list. 20.038/20.038 20.038/20.038 ============================== end of input ========================== 20.038/20.038 20.038/20.038 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 20.038/20.038 20.038/20.038 % Formulas that are not ordinary clauses: 20.038/20.038 1 ->(x1,y) -> ->(between(x1,x2,x3),between(y,x2,x3)) # label(congruence) # label(non_clause). [assumption]. 20.038/20.038 2 ->(x2,y) -> ->(between(x1,x2,x3),between(x1,y,x3)) # label(congruence) # label(non_clause). [assumption]. 20.038/20.038 3 ->(x3,y) -> ->(between(x1,x2,x3),between(x1,x2,y)) # label(congruence) # label(non_clause). [assumption]. 20.038/20.038 4 ->(x1,y) -> ->(down(x1),down(y)) # label(congruence) # label(non_clause). [assumption]. 20.038/20.038 5 ->(x1,y) -> ->(up(x1),up(y)) # label(congruence) # label(non_clause). [assumption]. 20.038/20.038 6 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 20.038/20.038 7 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 20.038/20.038 8 (exists x6 (->*(up(s(c_x1)),x6) & ->*(c_x1,x6))) # label(goal) # label(non_clause) # label(goal). [goal]. 20.038/20.038 20.038/20.038 ============================== end of process non-clausal formulas === 20.038/20.038 20.038/20.038 ============================== CLAUSES FOR SEARCH ==================== 20.038/20.038 20.038/20.038 formulas(mace4_clauses). 20.038/20.038 -->(x,y) | ->(between(x,z,u),between(y,z,u)) # label(congruence). 20.038/20.038 -->(x,y) | ->(between(z,x,u),between(z,y,u)) # label(congruence). 20.038/20.038 -->(x,y) | ->(between(z,u,x),between(z,u,y)) # label(congruence). 20.038/20.038 -->(x,y) | ->(down(x),down(y)) # label(congruence). 20.038/20.038 -->(x,y) | ->(up(x),up(y)) # label(congruence). 20.038/20.038 -->(x,y) | ->(s(x),s(y)) # label(congruence). 20.038/20.038 ->(up(x),up(s(x))) # label(replacement). 20.038/20.038 ->(up(x),x) # label(replacement). 20.038/20.038 ->*(x,x) # label(reflexivity). 20.038/20.038 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 20.038/20.038 -->*(up(s(c_x1)),x) | -->*(c_x1,x) # label(goal). 20.038/20.038 end_of_list. 20.038/20.038 20.038/20.038 ============================== end of clauses for search ============= 20.038/20.038 20.038/20.038 % There are no natural numbers in the input. 20.038/20.038 20.038/20.038 ============================== DOMAIN SIZE 2 ========================= 20.038/20.038 20.038/20.038 ============================== STATISTICS ============================ 20.038/20.038 20.038/20.038 For domain size 2. 20.038/20.038 20.038/20.038 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 20.038/20.038 Ground clauses: seen=76, kept=72. 20.038/20.038 Selections=8, assignments=15, propagations=22, current_models=0. 20.038/20.038 Rewrite_terms=90, rewrite_bools=168, indexes=32. 20.038/20.038 Rules_from_neg_clauses=4, cross_offs=4. 20.038/20.038 20.038/20.038 ============================== end of statistics ===================== 20.038/20.038 20.038/20.038 ============================== DOMAIN SIZE 3 ========================= 20.038/20.038 20.038/20.038 ============================== MODEL ================================= 20.038/20.038 20.038/20.038 interpretation( 3, [number=1, seconds=0], [ 20.038/20.038 20.038/20.038 function(c_x1, [ 0 ]), 20.038/20.038 20.038/20.038 function(down(_), [ 0, 0, 0 ]), 20.038/20.038 20.038/20.038 function(up(_), [ 1, 1, 2 ]), 20.038/20.038 20.038/20.038 function(s(_), [ 2, 1, 2 ]), 20.038/20.038 20.038/20.038 function(between(_,_,_), [ 20.038/20.038 0, 0, 0, 20.038/20.038 0, 0, 0, 20.038/20.038 0, 0, 0, 20.038/20.038 0, 0, 0, 20.038/20.038 0, 0, 0, 20.038/20.038 0, 0, 0, 20.038/20.038 0, 0, 0, 20.038/20.038 0, 0, 0, 20.038/20.038 0, 0, 0 ]), 20.038/20.038 20.038/20.038 relation(->*(_,_), [ 20.038/20.038 1, 0, 0, 20.038/20.038 1, 1, 1, 20.038/20.038 0, 0, 1 ]), 20.038/20.038 20.038/20.038 relation(->(_,_), [ 20.038/20.038 1, 0, 0, 20.038/20.038 1, 1, 1, 20.038/20.038 0, 0, 1 ]) 20.038/20.038 ]). 20.038/20.038 20.038/20.038 ============================== end of model ========================== 20.038/20.038 20.038/20.038 ============================== STATISTICS ============================ 20.038/20.038 20.038/20.038 For domain size 3. 20.038/20.038 20.038/20.038 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 20.038/20.038 Ground clauses: seen=309, kept=300. 20.038/20.038 Selections=19, assignments=28, propagations=57, current_models=1. 20.038/20.038 Rewrite_terms=647, rewrite_bools=667, indexes=48. 20.038/20.038 Rules_from_neg_clauses=23, cross_offs=56. 20.038/20.038 20.038/20.038 ============================== end of statistics ===================== 20.038/20.038 20.038/20.038 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 20.038/20.038 20.038/20.038 Exiting with 1 model. 20.038/20.038 20.038/20.038 Process 61544 exit (max_models) Wed Mar 9 09:48:35 2022 20.038/20.038 The process finished Wed Mar 9 09:48:35 2022 20.038/20.038 20.038/20.038 20.038/20.038 Mace4 cooked interpretation: 20.038/20.038 20.038/20.038 20.038/20.038 20.038/20.038 The problem is infeasible. 20.038/20.038 20.038/20.038 20.038/20.038 The problem is not joinable. 20.038/20.038 19.93user 0.60system 0:20.38elapsed 100%CPU (0avgtext+0avgdata 116552maxresident)k 20.038/20.038 8inputs+0outputs (0major+43957minor)pagefaults 0swaps