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