1.052/1.052 YES 1.052/1.052 1.052/1.052 Problem 1: 1.052/1.052 1.052/1.052 1.052/1.052 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 1.052/1.052 Confluence Problem: 1.052/1.052 (VAR vNonEmpty x y) 1.052/1.052 (REPLACEMENT-MAP 1.052/1.052 (a) 1.052/1.052 (b) 1.052/1.052 (c) 1.052/1.052 (d) 1.052/1.052 (f 1) 1.052/1.052 (g 1, 2) 1.052/1.052 (k) 1.052/1.052 (l) 1.052/1.052 (s 1) 1.052/1.052 (e) 1.052/1.052 (fSNonEmpty) 1.052/1.052 (h 1, 2) 1.052/1.052 (pair 1, 2) 1.052/1.052 (t 1) 1.052/1.052 ) 1.052/1.052 (RULES 1.052/1.052 a -> c 1.052/1.052 a -> d 1.052/1.052 b -> c 1.052/1.052 b -> d 1.052/1.052 c -> e 1.052/1.052 d -> e 1.052/1.052 f(x) -> pair(x,y) | s(x) ->* t(y) 1.052/1.052 g(x,x) -> h(x,x) 1.052/1.052 k -> e 1.052/1.052 l -> e 1.052/1.052 s(c) -> t(k) 1.052/1.052 s(c) -> t(l) 1.052/1.052 s(e) -> t(e) 1.052/1.052 ) 1.052/1.052 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 1.052/1.052 1.052/1.052 1.052/1.052 Problem 1: 1.052/1.052 1.052/1.052 Inlining of Conditions Processor [STERN17]: 1.052/1.052 1.052/1.052 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 1.052/1.052 Confluence Problem: 1.052/1.052 (VAR vNonEmpty x y) 1.052/1.052 (REPLACEMENT-MAP 1.052/1.052 (a) 1.052/1.052 (b) 1.052/1.052 (c) 1.052/1.052 (d) 1.052/1.052 (f 1) 1.052/1.052 (g 1, 2) 1.052/1.052 (k) 1.052/1.052 (l) 1.052/1.052 (s 1) 1.052/1.052 (e) 1.052/1.052 (fSNonEmpty) 1.052/1.052 (h 1, 2) 1.052/1.052 (pair 1, 2) 1.052/1.052 (t 1) 1.052/1.052 ) 1.052/1.052 (RULES 1.052/1.052 a -> c 1.052/1.052 a -> d 1.052/1.052 b -> c 1.052/1.052 b -> d 1.052/1.052 c -> e 1.052/1.052 d -> e 1.052/1.052 f(x) -> pair(x,y) | s(x) ->* t(y) 1.052/1.052 g(x,x) -> h(x,x) 1.052/1.052 k -> e 1.052/1.052 l -> e 1.052/1.052 s(c) -> t(k) 1.052/1.052 s(c) -> t(l) 1.052/1.052 s(e) -> t(e) 1.052/1.052 ) 1.052/1.052 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 1.052/1.052 1.052/1.052 1.052/1.052 Problem 1: 1.052/1.052 1.052/1.052 Clean CTRS Processor: 1.052/1.052 1.052/1.052 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 1.052/1.052 Confluence Problem: 1.052/1.052 (VAR x y) 1.052/1.052 (REPLACEMENT-MAP 1.052/1.052 (a) 1.052/1.052 (b) 1.052/1.052 (c) 1.052/1.052 (d) 1.052/1.052 (f 1) 1.052/1.052 (g 1, 2) 1.052/1.052 (k) 1.052/1.052 (l) 1.052/1.052 (s 1) 1.052/1.052 (e) 1.052/1.052 (fSNonEmpty) 1.052/1.052 (h 1, 2) 1.052/1.052 (pair 1, 2) 1.052/1.052 (t 1) 1.052/1.052 ) 1.052/1.052 (RULES 1.052/1.052 a -> c 1.052/1.052 a -> d 1.052/1.052 b -> c 1.052/1.052 b -> d 1.052/1.052 c -> e 1.052/1.052 d -> e 1.052/1.052 f(x) -> pair(x,y) | s(x) ->* t(y) 1.052/1.052 g(x,x) -> h(x,x) 1.052/1.052 k -> e 1.052/1.052 l -> e 1.052/1.052 s(c) -> t(k) 1.052/1.052 s(c) -> t(l) 1.052/1.052 s(e) -> t(e) 1.052/1.052 ) 1.052/1.052 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 1.052/1.052 1.052/1.052 CRule InfChecker Info: 1.052/1.052 a -> c 1.052/1.052 Rule remains 1.052/1.052 Proof: 1.052/1.052 NO_CONDS 1.052/1.052 1.052/1.052 CRule InfChecker Info: 1.052/1.052 a -> d 1.052/1.052 Rule remains 1.052/1.052 Proof: 1.052/1.052 NO_CONDS 1.052/1.052 1.052/1.052 CRule InfChecker Info: 1.052/1.052 b -> c 1.052/1.052 Rule remains 1.052/1.052 Proof: 1.052/1.052 NO_CONDS 1.052/1.052 1.052/1.052 CRule InfChecker Info: 1.052/1.052 b -> d 1.052/1.052 Rule remains 1.052/1.052 Proof: 1.052/1.052 NO_CONDS 1.052/1.052 1.052/1.052 CRule InfChecker Info: 1.052/1.052 c -> e 1.052/1.052 Rule remains 1.052/1.052 Proof: 1.052/1.052 NO_CONDS 1.052/1.052 1.052/1.052 CRule InfChecker Info: 1.052/1.052 d -> e 1.052/1.052 Rule remains 1.052/1.052 Proof: 1.052/1.052 NO_CONDS 1.052/1.052 1.052/1.052 CRule InfChecker Info: 1.052/1.052 f(x) -> pair(x,y) | s(x) ->* t(y) 1.052/1.052 Rule remains 1.052/1.052 Proof: 1.052/1.052 NO 1.052/1.052 1.052/1.052 Problem 1: 1.052/1.052 1.052/1.052 Infeasibility Problem: 1.052/1.052 [(VAR vNonEmpty x y vNonEmpty x y) 1.052/1.052 (STRATEGY CONTEXTSENSITIVE 1.052/1.052 (a) 1.052/1.052 (b) 1.052/1.052 (c) 1.052/1.052 (d) 1.052/1.052 (f 1) 1.052/1.052 (g 1 2) 1.052/1.052 (k) 1.052/1.052 (l) 1.052/1.052 (s 1) 1.052/1.052 (e) 1.052/1.052 (fSNonEmpty) 1.052/1.052 (h 1 2) 1.052/1.052 (pair 1 2) 1.052/1.052 (t 1) 1.052/1.052 ) 1.052/1.052 (RULES 1.052/1.052 a -> c 1.052/1.052 a -> d 1.052/1.052 b -> c 1.052/1.052 b -> d 1.052/1.052 c -> e 1.052/1.052 d -> e 1.052/1.052 f(x) -> pair(x,y) | s(x) ->* t(y) 1.052/1.052 g(x,x) -> h(x,x) 1.052/1.052 k -> e 1.052/1.052 l -> e 1.052/1.052 s(c) -> t(k) 1.052/1.052 s(c) -> t(l) 1.052/1.052 s(e) -> t(e) 1.052/1.052 )] 1.052/1.052 1.052/1.052 Infeasibility Conditions: 1.052/1.052 s(x) ->* t(y) 1.052/1.052 1.052/1.052 Problem 1: 1.052/1.052 1.052/1.052 Obtaining a proof using Prover9: 1.052/1.052 1.052/1.052 -> Prover9 Output: 1.052/1.052 ============================== Prover9 =============================== 1.052/1.052 Prover9 (64) version 2009-11A, November 2009. 1.052/1.052 Process 60100 was started by ubuntu on ubuntu, 1.052/1.052 Wed Mar 9 09:44:09 2022 1.052/1.052 The command was "./prover9 -f /tmp/prover960093-0.in". 1.052/1.052 ============================== end of head =========================== 1.052/1.052 1.052/1.052 ============================== INPUT ================================= 1.052/1.052 1.052/1.052 % Reading from file /tmp/prover960093-0.in 1.052/1.052 1.052/1.052 assign(max_seconds,20). 1.052/1.052 1.052/1.052 formulas(assumptions). 1.052/1.052 ->_s0(x1,y) -> ->_s0(f(x1),f(y)) # label(congruence). 1.052/1.052 ->_s0(x1,y) -> ->_s0(g(x1,x2),g(y,x2)) # label(congruence). 1.052/1.052 ->_s0(x2,y) -> ->_s0(g(x1,x2),g(x1,y)) # label(congruence). 1.052/1.052 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence). 1.052/1.052 ->_s0(x1,y) -> ->_s0(h(x1,x2),h(y,x2)) # label(congruence). 1.052/1.052 ->_s0(x2,y) -> ->_s0(h(x1,x2),h(x1,y)) # label(congruence). 1.052/1.052 ->_s0(x1,y) -> ->_s0(pair(x1,x2),pair(y,x2)) # label(congruence). 1.052/1.052 ->_s0(x2,y) -> ->_s0(pair(x1,x2),pair(x1,y)) # label(congruence). 1.052/1.052 ->_s0(x1,y) -> ->_s0(t(x1),t(y)) # label(congruence). 1.052/1.052 ->_s0(a,c) # label(replacement). 1.052/1.052 ->_s0(a,d) # label(replacement). 1.052/1.052 ->_s0(b,c) # label(replacement). 1.052/1.052 ->_s0(b,d) # label(replacement). 1.052/1.052 ->_s0(c,e) # label(replacement). 1.052/1.052 ->_s0(d,e) # label(replacement). 1.052/1.052 ->*_s0(s(x1),t(x2)) -> ->_s0(f(x1),pair(x1,x2)) # label(replacement). 1.052/1.052 ->_s0(g(x1,x1),h(x1,x1)) # label(replacement). 1.052/1.052 ->_s0(k,e) # label(replacement). 1.052/1.052 ->_s0(l,e) # label(replacement). 1.052/1.052 ->_s0(s(c),t(k)) # label(replacement). 1.052/1.052 ->_s0(s(c),t(l)) # label(replacement). 1.052/1.052 ->_s0(s(e),t(e)) # label(replacement). 1.052/1.052 ->*_s0(x,x) # label(reflexivity). 1.052/1.052 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(goals). 1.052/1.052 (exists x4 exists x5 ->*_s0(s(x4),t(x5))) # label(goal). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 ============================== end of input ========================== 1.052/1.052 1.052/1.052 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 1.052/1.052 1.052/1.052 % Formulas that are not ordinary clauses: 1.052/1.052 1 ->_s0(x1,y) -> ->_s0(f(x1),f(y)) # label(congruence) # label(non_clause). [assumption]. 1.052/1.052 2 ->_s0(x1,y) -> ->_s0(g(x1,x2),g(y,x2)) # label(congruence) # label(non_clause). [assumption]. 1.052/1.052 3 ->_s0(x2,y) -> ->_s0(g(x1,x2),g(x1,y)) # label(congruence) # label(non_clause). [assumption]. 1.052/1.052 4 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 1.052/1.052 5 ->_s0(x1,y) -> ->_s0(h(x1,x2),h(y,x2)) # label(congruence) # label(non_clause). [assumption]. 1.052/1.052 6 ->_s0(x2,y) -> ->_s0(h(x1,x2),h(x1,y)) # label(congruence) # label(non_clause). [assumption]. 1.052/1.052 7 ->_s0(x1,y) -> ->_s0(pair(x1,x2),pair(y,x2)) # label(congruence) # label(non_clause). [assumption]. 1.052/1.052 8 ->_s0(x2,y) -> ->_s0(pair(x1,x2),pair(x1,y)) # label(congruence) # label(non_clause). [assumption]. 1.052/1.052 9 ->_s0(x1,y) -> ->_s0(t(x1),t(y)) # label(congruence) # label(non_clause). [assumption]. 1.052/1.052 10 ->*_s0(s(x1),t(x2)) -> ->_s0(f(x1),pair(x1,x2)) # label(replacement) # label(non_clause). [assumption]. 1.052/1.052 11 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 1.052/1.052 12 (exists x4 exists x5 ->*_s0(s(x4),t(x5))) # label(goal) # label(non_clause) # label(goal). [goal]. 1.052/1.052 1.052/1.052 ============================== end of process non-clausal formulas === 1.052/1.052 1.052/1.052 ============================== PROCESS INITIAL CLAUSES =============== 1.052/1.052 1.052/1.052 % Clauses before input processing: 1.052/1.052 1.052/1.052 formulas(usable). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(sos). 1.052/1.052 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(1)]. 1.052/1.052 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence). [clausify(2)]. 1.052/1.052 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence). [clausify(3)]. 1.052/1.052 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(4)]. 1.052/1.052 -->_s0(x,y) | ->_s0(h(x,z),h(y,z)) # label(congruence). [clausify(5)]. 1.052/1.052 -->_s0(x,y) | ->_s0(h(z,x),h(z,y)) # label(congruence). [clausify(6)]. 1.052/1.052 -->_s0(x,y) | ->_s0(pair(x,z),pair(y,z)) # label(congruence). [clausify(7)]. 1.052/1.052 -->_s0(x,y) | ->_s0(pair(z,x),pair(z,y)) # label(congruence). [clausify(8)]. 1.052/1.052 -->_s0(x,y) | ->_s0(t(x),t(y)) # label(congruence). [clausify(9)]. 1.052/1.052 ->_s0(a,c) # label(replacement). [assumption]. 1.052/1.052 ->_s0(a,d) # label(replacement). [assumption]. 1.052/1.052 ->_s0(b,c) # label(replacement). [assumption]. 1.052/1.052 ->_s0(b,d) # label(replacement). [assumption]. 1.052/1.052 ->_s0(c,e) # label(replacement). [assumption]. 1.052/1.052 ->_s0(d,e) # label(replacement). [assumption]. 1.052/1.052 -->*_s0(s(x),t(y)) | ->_s0(f(x),pair(x,y)) # label(replacement). [clausify(10)]. 1.052/1.052 ->_s0(g(x,x),h(x,x)) # label(replacement). [assumption]. 1.052/1.052 ->_s0(k,e) # label(replacement). [assumption]. 1.052/1.052 ->_s0(l,e) # label(replacement). [assumption]. 1.052/1.052 ->_s0(s(c),t(k)) # label(replacement). [assumption]. 1.052/1.052 ->_s0(s(c),t(l)) # label(replacement). [assumption]. 1.052/1.052 ->_s0(s(e),t(e)) # label(replacement). [assumption]. 1.052/1.052 ->*_s0(x,x) # label(reflexivity). [assumption]. 1.052/1.052 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(11)]. 1.052/1.052 -->*_s0(s(x),t(y)) # label(goal). [deny(12)]. 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(demodulators). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 ============================== PREDICATE ELIMINATION ================= 1.052/1.052 1.052/1.052 No predicates eliminated. 1.052/1.052 1.052/1.052 ============================== end predicate elimination ============= 1.052/1.052 1.052/1.052 Auto_denials: 1.052/1.052 % copying label goal to answer in negative clause 1.052/1.052 1.052/1.052 Term ordering decisions: 1.052/1.052 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 1.052/1.052 Function symbol precedence: function_order([ e, c, d, a, b, k, l, h, pair, g, s, t, f ]). 1.052/1.052 After inverse_order: (no changes). 1.052/1.052 Unfolding symbols: (none). 1.052/1.052 1.052/1.052 Auto_inference settings: 1.052/1.052 % set(neg_binary_resolution). % (HNE depth_diff=-9) 1.052/1.052 % clear(ordered_res). % (HNE depth_diff=-9) 1.052/1.052 % set(ur_resolution). % (HNE depth_diff=-9) 1.052/1.052 % set(ur_resolution) -> set(pos_ur_resolution). 1.052/1.052 % set(ur_resolution) -> set(neg_ur_resolution). 1.052/1.052 1.052/1.052 Auto_process settings: (no changes). 1.052/1.052 1.052/1.052 kept: 13 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(1)]. 1.052/1.052 kept: 14 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence). [clausify(2)]. 1.052/1.052 kept: 15 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence). [clausify(3)]. 1.052/1.052 kept: 16 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(4)]. 1.052/1.052 kept: 17 -->_s0(x,y) | ->_s0(h(x,z),h(y,z)) # label(congruence). [clausify(5)]. 1.052/1.052 kept: 18 -->_s0(x,y) | ->_s0(h(z,x),h(z,y)) # label(congruence). [clausify(6)]. 1.052/1.052 kept: 19 -->_s0(x,y) | ->_s0(pair(x,z),pair(y,z)) # label(congruence). [clausify(7)]. 1.052/1.052 kept: 20 -->_s0(x,y) | ->_s0(pair(z,x),pair(z,y)) # label(congruence). [clausify(8)]. 1.052/1.052 kept: 21 -->_s0(x,y) | ->_s0(t(x),t(y)) # label(congruence). [clausify(9)]. 1.052/1.052 kept: 22 ->_s0(a,c) # label(replacement). [assumption]. 1.052/1.052 kept: 23 ->_s0(a,d) # label(replacement). [assumption]. 1.052/1.052 kept: 24 ->_s0(b,c) # label(replacement). [assumption]. 1.052/1.052 kept: 25 ->_s0(b,d) # label(replacement). [assumption]. 1.052/1.052 kept: 26 ->_s0(c,e) # label(replacement). [assumption]. 1.052/1.052 kept: 27 ->_s0(d,e) # label(replacement). [assumption]. 1.052/1.052 kept: 28 -->*_s0(s(x),t(y)) | ->_s0(f(x),pair(x,y)) # label(replacement). [clausify(10)]. 1.052/1.052 kept: 29 ->_s0(g(x,x),h(x,x)) # label(replacement). [assumption]. 1.052/1.052 kept: 30 ->_s0(k,e) # label(replacement). [assumption]. 1.052/1.052 kept: 31 ->_s0(l,e) # label(replacement). [assumption]. 1.052/1.052 kept: 32 ->_s0(s(c),t(k)) # label(replacement). [assumption]. 1.052/1.052 kept: 33 ->_s0(s(c),t(l)) # label(replacement). [assumption]. 1.052/1.052 kept: 34 ->_s0(s(e),t(e)) # label(replacement). [assumption]. 1.052/1.052 kept: 35 ->*_s0(x,x) # label(reflexivity). [assumption]. 1.052/1.052 kept: 36 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(11)]. 1.052/1.052 kept: 37 -->*_s0(s(x),t(y)) # label(goal) # answer(goal). [deny(12)]. 1.052/1.052 1.052/1.052 ============================== end of process initial clauses ======== 1.052/1.052 1.052/1.052 ============================== CLAUSES FOR SEARCH ==================== 1.052/1.052 1.052/1.052 % Clauses after input processing: 1.052/1.052 1.052/1.052 formulas(usable). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(sos). 1.052/1.052 13 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(1)]. 1.052/1.052 14 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence). [clausify(2)]. 1.052/1.052 15 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence). [clausify(3)]. 1.052/1.052 16 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(4)]. 1.052/1.052 17 -->_s0(x,y) | ->_s0(h(x,z),h(y,z)) # label(congruence). [clausify(5)]. 1.052/1.052 18 -->_s0(x,y) | ->_s0(h(z,x),h(z,y)) # label(congruence). [clausify(6)]. 1.052/1.052 19 -->_s0(x,y) | ->_s0(pair(x,z),pair(y,z)) # label(congruence). [clausify(7)]. 1.052/1.052 20 -->_s0(x,y) | ->_s0(pair(z,x),pair(z,y)) # label(congruence). [clausify(8)]. 1.052/1.052 21 -->_s0(x,y) | ->_s0(t(x),t(y)) # label(congruence). [clausify(9)]. 1.052/1.052 22 ->_s0(a,c) # label(replacement). [assumption]. 1.052/1.052 23 ->_s0(a,d) # label(replacement). [assumption]. 1.052/1.052 24 ->_s0(b,c) # label(replacement). [assumption]. 1.052/1.052 25 ->_s0(b,d) # label(replacement). [assumption]. 1.052/1.052 26 ->_s0(c,e) # label(replacement). [assumption]. 1.052/1.052 27 ->_s0(d,e) # label(replacement). [assumption]. 1.052/1.052 29 ->_s0(g(x,x),h(x,x)) # label(replacement). [assumption]. 1.052/1.052 30 ->_s0(k,e) # label(replacement). [assumption]. 1.052/1.052 31 ->_s0(l,e) # label(replacement). [assumption]. 1.052/1.052 32 ->_s0(s(c),t(k)) # label(replacement). [assumption]. 1.052/1.052 33 ->_s0(s(c),t(l)) # label(replacement). [assumption]. 1.052/1.052 34 ->_s0(s(e),t(e)) # label(replacement). [assumption]. 1.052/1.052 35 ->*_s0(x,x) # label(reflexivity). [assumption]. 1.052/1.052 36 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(11)]. 1.052/1.052 37 -->*_s0(s(x),t(y)) # label(goal) # answer(goal). [deny(12)]. 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(demodulators). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 ============================== end of clauses for search ============= 1.052/1.052 1.052/1.052 ============================== SEARCH ================================ 1.052/1.052 1.052/1.052 % Starting search at 0.00 seconds. 1.052/1.052 1.052/1.052 given #1 (I,wt=8): 13 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(1)]. 1.052/1.052 1.052/1.052 given #2 (I,wt=10): 14 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence). [clausify(2)]. 1.052/1.052 1.052/1.052 given #3 (I,wt=10): 15 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence). [clausify(3)]. 1.052/1.052 1.052/1.052 given #4 (I,wt=8): 16 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(4)]. 1.052/1.052 1.052/1.052 given #5 (I,wt=10): 17 -->_s0(x,y) | ->_s0(h(x,z),h(y,z)) # label(congruence). [clausify(5)]. 1.052/1.052 1.052/1.052 given #6 (I,wt=10): 18 -->_s0(x,y) | ->_s0(h(z,x),h(z,y)) # label(congruence). [clausify(6)]. 1.052/1.052 1.052/1.052 given #7 (I,wt=10): 19 -->_s0(x,y) | ->_s0(pair(x,z),pair(y,z)) # label(congruence). [clausify(7)]. 1.052/1.052 1.052/1.052 given #8 (I,wt=10): 20 -->_s0(x,y) | ->_s0(pair(z,x),pair(z,y)) # label(congruence). [clausify(8)]. 1.052/1.052 1.052/1.052 given #9 (I,wt=8): 21 -->_s0(x,y) | ->_s0(t(x),t(y)) # label(congruence). [clausify(9)]. 1.052/1.052 1.052/1.052 given #10 (I,wt=3): 22 ->_s0(a,c) # label(replacement). [assumption]. 1.052/1.052 1.052/1.052 given #11 (I,wt=3): 23 ->_s0(a,d) # label(replacement). [assumption]. 1.052/1.052 1.052/1.052 given #12 (I,wt=3): 24 ->_s0(b,c) # label(replacement). [assumption]. 1.052/1.052 1.052/1.052 given #13 (I,wt=3): 25 ->_s0(b,d) # label(replacement). [assumption]. 1.052/1.052 1.052/1.052 given #14 (I,wt=3): 26 ->_s0(c,e) # label(replacement). [assumption]. 1.052/1.052 1.052/1.052 given #15 (I,wt=3): 27 ->_s0(d,e) # label(replacement). [assumption]. 1.052/1.052 1.052/1.052 given #16 (I,wt=7): 29 ->_s0(g(x,x),h(x,x)) # label(replacement). [assumption]. 1.052/1.052 1.052/1.052 given #17 (I,wt=3): 30 ->_s0(k,e) # label(replacement). [assumption]. 1.052/1.052 1.052/1.052 given #18 (I,wt=3): 31 ->_s0(l,e) # label(replacement). [assumption]. 1.052/1.052 1.052/1.052 given #19 (I,wt=5): 32 ->_s0(s(c),t(k)) # label(replacement). [assumption]. 1.052/1.052 1.052/1.052 given #20 (I,wt=5): 33 ->_s0(s(c),t(l)) # label(replacement). [assumption]. 1.052/1.052 1.052/1.052 given #21 (I,wt=5): 34 ->_s0(s(e),t(e)) # label(replacement). [assumption]. 1.052/1.052 1.052/1.052 given #22 (I,wt=3): 35 ->*_s0(x,x) # label(reflexivity). [assumption]. 1.052/1.052 1.052/1.052 given #23 (I,wt=9): 36 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(11)]. 1.052/1.052 1.052/1.052 ============================== PROOF ================================= 1.052/1.052 1.052/1.052 % Proof 1 at 0.01 (+ 0.00) seconds: goal. 1.052/1.052 % Length of proof is 8. 1.052/1.052 % Level of proof is 3. 1.052/1.052 % Maximum clause weight is 9.000. 1.052/1.052 % Given clauses 23. 1.052/1.052 1.052/1.052 11 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 1.052/1.052 12 (exists x4 exists x5 ->*_s0(s(x4),t(x5))) # label(goal) # label(non_clause) # label(goal). [goal]. 1.052/1.052 34 ->_s0(s(e),t(e)) # label(replacement). [assumption]. 1.052/1.052 35 ->*_s0(x,x) # label(reflexivity). [assumption]. 1.052/1.052 36 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(11)]. 1.052/1.052 37 -->*_s0(s(x),t(y)) # label(goal) # answer(goal). [deny(12)]. 1.052/1.052 146 ->*_s0(s(e),t(e)). [ur(36,a,34,a,b,35,a)]. 1.052/1.052 147 $F # answer(goal). [resolve(146,a,37,a)]. 1.052/1.052 1.052/1.052 ============================== end of proof ========================== 1.052/1.052 1.052/1.052 ============================== STATISTICS ============================ 1.052/1.052 1.052/1.052 Given=23. Generated=134. Kept=134. proofs=1. 1.052/1.052 Usable=23. Sos=109. Demods=0. Limbo=0, Disabled=26. Hints=0. 1.052/1.052 Kept_by_rule=0, Deleted_by_rule=0. 1.052/1.052 Forward_subsumed=0. Back_subsumed=1. 1.052/1.052 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 1.052/1.052 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 1.052/1.052 Demod_attempts=0. Demod_rewrites=0. 1.052/1.052 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 1.052/1.052 Nonunit_fsub_feature_tests=3. Nonunit_bsub_feature_tests=19. 1.052/1.052 Megabytes=0.23. 1.052/1.052 User_CPU=0.01, System_CPU=0.00, Wall_clock=0. 1.052/1.052 1.052/1.052 ============================== end of statistics ===================== 1.052/1.052 1.052/1.052 ============================== end of search ========================= 1.052/1.052 1.052/1.052 THEOREM PROVED 1.052/1.052 1.052/1.052 Exiting with 1 proof. 1.052/1.052 1.052/1.052 Process 60100 exit (max_proofs) Wed Mar 9 09:44:09 2022 1.052/1.052 1.052/1.052 1.052/1.052 The problem is feasible. 1.052/1.052 1.052/1.052 1.052/1.052 CRule InfChecker Info: 1.052/1.052 g(x,x) -> h(x,x) 1.052/1.052 Rule remains 1.052/1.052 Proof: 1.052/1.052 NO_CONDS 1.052/1.052 1.052/1.052 CRule InfChecker Info: 1.052/1.052 k -> e 1.052/1.052 Rule remains 1.052/1.052 Proof: 1.052/1.052 NO_CONDS 1.052/1.052 1.052/1.052 CRule InfChecker Info: 1.052/1.052 l -> e 1.052/1.052 Rule remains 1.052/1.052 Proof: 1.052/1.052 NO_CONDS 1.052/1.052 1.052/1.052 CRule InfChecker Info: 1.052/1.052 s(c) -> t(k) 1.052/1.052 Rule remains 1.052/1.052 Proof: 1.052/1.052 NO_CONDS 1.052/1.052 1.052/1.052 CRule InfChecker Info: 1.052/1.052 s(c) -> t(l) 1.052/1.052 Rule remains 1.052/1.052 Proof: 1.052/1.052 NO_CONDS 1.052/1.052 1.052/1.052 CRule InfChecker Info: 1.052/1.052 s(e) -> t(e) 1.052/1.052 Rule remains 1.052/1.052 Proof: 1.052/1.052 NO_CONDS 1.052/1.052 1.052/1.052 Problem 1: 1.052/1.052 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 1.052/1.052 Confluence Problem: 1.052/1.052 (VAR x y) 1.052/1.052 (REPLACEMENT-MAP 1.052/1.052 (a) 1.052/1.052 (b) 1.052/1.052 (c) 1.052/1.052 (d) 1.052/1.052 (f 1) 1.052/1.052 (g 1, 2) 1.052/1.052 (k) 1.052/1.052 (l) 1.052/1.052 (s 1) 1.052/1.052 (e) 1.052/1.052 (fSNonEmpty) 1.052/1.052 (h 1, 2) 1.052/1.052 (pair 1, 2) 1.052/1.052 (t 1) 1.052/1.052 ) 1.052/1.052 (RULES 1.052/1.052 a -> c 1.052/1.052 a -> d 1.052/1.052 b -> c 1.052/1.052 b -> d 1.052/1.052 c -> e 1.052/1.052 d -> e 1.052/1.052 f(x) -> pair(x,y) | s(x) ->* t(y) 1.052/1.052 g(x,x) -> h(x,x) 1.052/1.052 k -> e 1.052/1.052 l -> e 1.052/1.052 s(c) -> t(k) 1.052/1.052 s(c) -> t(l) 1.052/1.052 s(e) -> t(e) 1.052/1.052 ) 1.052/1.052 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 1.052/1.052 1.052/1.052 Critical Pairs Processor: 1.052/1.052 -> Rules: 1.052/1.052 a -> c 1.052/1.052 a -> d 1.052/1.052 b -> c 1.052/1.052 b -> d 1.052/1.052 c -> e 1.052/1.052 d -> e 1.052/1.052 f(x) -> pair(x,y) | s(x) ->* t(y) 1.052/1.052 g(x,x) -> h(x,x) 1.052/1.052 k -> e 1.052/1.052 l -> e 1.052/1.052 s(c) -> t(k) 1.052/1.052 s(c) -> t(l) 1.052/1.052 s(e) -> t(e) 1.052/1.052 -> Vars: 1.052/1.052 "x", "y" 1.052/1.052 1.052/1.052 -> Rlps: 1.052/1.052 crule: a -> c, id: 1, possubterms: a-> [] 1.052/1.052 crule: a -> d, id: 2, possubterms: a-> [] 1.052/1.052 crule: b -> c, id: 3, possubterms: b-> [] 1.052/1.052 crule: b -> d, id: 4, possubterms: b-> [] 1.052/1.052 crule: c -> e, id: 5, possubterms: c-> [] 1.052/1.052 crule: d -> e, id: 6, possubterms: d-> [] 1.052/1.052 crule: f(x) -> pair(x,y) | s(x) ->* t(y), id: 7, possubterms: f(x)-> [] 1.052/1.052 crule: g(x,x) -> h(x,x), id: 8, possubterms: g(x,x)-> [] 1.052/1.052 crule: k -> e, id: 9, possubterms: k-> [] 1.052/1.052 crule: l -> e, id: 10, possubterms: l-> [] 1.052/1.052 crule: s(c) -> t(k), id: 11, possubterms: s(c)-> [], c-> [1] 1.052/1.052 crule: s(c) -> t(l), id: 12, possubterms: s(c)-> [], c-> [1] 1.052/1.052 crule: s(e) -> t(e), id: 13, possubterms: s(e)-> [], e-> [1] 1.052/1.052 1.052/1.052 -> Unifications: 1.052/1.052 R2 unifies with R1 at p: [], l: a, lp: a, conds: {}, sig: {}, l': a, r: d, r': c 1.052/1.052 R4 unifies with R3 at p: [], l: b, lp: b, conds: {}, sig: {}, l': b, r: d, r': c 1.052/1.052 R11 unifies with R5 at p: [1], l: s(c), lp: c, conds: {}, sig: {}, l': c, r: t(k), r': e 1.052/1.052 R12 unifies with R11 at p: [], l: s(c), lp: s(c), conds: {}, sig: {}, l': s(c), r: t(l), r': t(k) 1.052/1.052 R12 unifies with R5 at p: [1], l: s(c), lp: c, conds: {}, sig: {}, l': c, r: t(l), r': e 1.052/1.052 1.052/1.052 -> Critical pairs info: 1.052/1.052 => Not trivial, Not overlay, NW0, N1 1.052/1.052 => Not trivial, Overlay, NW0, N2 1.052/1.052 => Not trivial, Not overlay, NW0, N3 1.052/1.052 => Not trivial, Overlay, NW0, N4 1.052/1.052 1.052/1.052 -> Problem conclusions: 1.052/1.052 Not left linear, Not right linear, Not linear 1.052/1.052 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 1.052/1.052 CTRS Type: 3 1.052/1.052 Deterministic, Strongly deterministic 1.052/1.052 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 1.052/1.052 Maybe right-stable CTRS, Not overlay CTRS 1.052/1.052 Maybe normal CTRS, Maybe almost normal CTRS 1.052/1.052 Maybe terminating CTRS, Maybe operational terminating CTRS, Maybe joinable CCPs 1.052/1.052 Maybe level confluent 1.052/1.052 Maybe confluent 1.052/1.052 1.052/1.052 Problem 1: 1.052/1.052 Clean Infeasible CCPs Processor: 1.052/1.052 Num of CPIs: 4 1.052/1.052 Timeout: 60 1.052/1.052 Timeout for each infeasibility problem: 60 s 1.052/1.052 => Not trivial, Not overlay, NW0, N1 1.052/1.052 1.052/1.052 Proof: 1.052/1.052 NO_CONDS 1.052/1.052 1.052/1.052 1.052/1.052 1.052/1.052 => Not trivial, Overlay, NW0, N2 1.052/1.052 1.052/1.052 Proof: 1.052/1.052 NO_CONDS 1.052/1.052 1.052/1.052 1.052/1.052 1.052/1.052 => Not trivial, Not overlay, NW0, N3 1.052/1.052 1.052/1.052 Proof: 1.052/1.052 NO_CONDS 1.052/1.052 1.052/1.052 1.052/1.052 1.052/1.052 => Not trivial, Overlay, NW0, N4 1.052/1.052 1.052/1.052 Proof: 1.052/1.052 NO_CONDS 1.052/1.052 1.052/1.052 1.052/1.052 1.052/1.052 -> Problem conclusions: 1.052/1.052 Not left linear, Not right linear, Not linear 1.052/1.052 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 1.052/1.052 CTRS Type: 3 1.052/1.052 Deterministic, Strongly deterministic 1.052/1.052 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 1.052/1.052 Maybe right-stable CTRS, Not overlay CTRS 1.052/1.052 Maybe normal CTRS, Maybe almost normal CTRS 1.052/1.052 Maybe terminating CTRS, Maybe operational terminating CTRS, Maybe joinable CCPs 1.052/1.052 Maybe level confluent 1.052/1.052 Maybe confluent 1.052/1.052 1.052/1.052 Resulting CCPs: 1.052/1.052 => Not trivial, Not overlay, NW0, N1 1.052/1.052 => Not trivial, Overlay, NW0, N2 1.052/1.052 => Not trivial, Not overlay, NW0, N3 1.052/1.052 => Not trivial, Overlay, NW0, N4 1.052/1.052 1.052/1.052 Problem 1: 1.052/1.052 Operation Termination Processor: 1.052/1.052 Operational terminating? 1.052/1.052 YES 1.052/1.052 1.052/1.052 Problem 1: 1.052/1.052 1.052/1.052 (VAR vu95NonEmpty x y) 1.052/1.052 (RULES 1.052/1.052 a -> c 1.052/1.052 a -> d 1.052/1.052 b -> c 1.052/1.052 b -> d 1.052/1.052 c -> e 1.052/1.052 d -> e 1.052/1.052 f(x) -> pair(x,y) | s(x) ->* t(y) 1.052/1.052 g(x,x) -> h(x,x) 1.052/1.052 k -> e 1.052/1.052 l -> e 1.052/1.052 s(c) -> t(k) 1.052/1.052 s(c) -> t(l) 1.052/1.052 s(e) -> t(e) 1.052/1.052 ) 1.052/1.052 1.052/1.052 Problem 1: 1.052/1.052 Valid CTRS Processor: 1.052/1.052 -> Rules: 1.052/1.052 a -> c 1.052/1.052 a -> d 1.052/1.052 b -> c 1.052/1.052 b -> d 1.052/1.052 c -> e 1.052/1.052 d -> e 1.052/1.052 f(x) -> pair(x,y) | s(x) ->* t(y) 1.052/1.052 g(x,x) -> h(x,x) 1.052/1.052 k -> e 1.052/1.052 l -> e 1.052/1.052 s(c) -> t(k) 1.052/1.052 s(c) -> t(l) 1.052/1.052 s(e) -> t(e) 1.052/1.052 -> The system is a deterministic 3-CTRS. 1.052/1.052 1.052/1.052 Problem 1: 1.052/1.052 1.052/1.052 2D Dependency Pair Processor: 1.052/1.052 1.052/1.052 Conditional Termination Problem 1: 1.052/1.052 -> Pairs: 1.052/1.052 A -> C 1.052/1.052 A -> D 1.052/1.052 B -> C 1.052/1.052 B -> D 1.052/1.052 S(c) -> K 1.052/1.052 S(c) -> L 1.052/1.052 -> QPairs: 1.052/1.052 Empty 1.052/1.052 -> Rules: 1.052/1.052 a -> c 1.052/1.052 a -> d 1.052/1.052 b -> c 1.052/1.052 b -> d 1.052/1.052 c -> e 1.052/1.052 d -> e 1.052/1.052 f(x) -> pair(x,y) | s(x) ->* t(y) 1.052/1.052 g(x,x) -> h(x,x) 1.052/1.052 k -> e 1.052/1.052 l -> e 1.052/1.052 s(c) -> t(k) 1.052/1.052 s(c) -> t(l) 1.052/1.052 s(e) -> t(e) 1.052/1.052 1.052/1.052 Conditional Termination Problem 2: 1.052/1.052 -> Pairs: 1.052/1.052 F(x) -> S(x) 1.052/1.052 -> QPairs: 1.052/1.052 S(c) -> K 1.052/1.052 S(c) -> L 1.052/1.052 -> Rules: 1.052/1.052 a -> c 1.052/1.052 a -> d 1.052/1.052 b -> c 1.052/1.052 b -> d 1.052/1.052 c -> e 1.052/1.052 d -> e 1.052/1.052 f(x) -> pair(x,y) | s(x) ->* t(y) 1.052/1.052 g(x,x) -> h(x,x) 1.052/1.052 k -> e 1.052/1.052 l -> e 1.052/1.052 s(c) -> t(k) 1.052/1.052 s(c) -> t(l) 1.052/1.052 s(e) -> t(e) 1.052/1.052 1.052/1.052 1.052/1.052 The problem is decomposed in 2 subproblems. 1.052/1.052 1.052/1.052 Problem 1.1: 1.052/1.052 1.052/1.052 SCC Processor: 1.052/1.052 -> Pairs: 1.052/1.052 A -> C 1.052/1.052 A -> D 1.052/1.052 B -> C 1.052/1.052 B -> D 1.052/1.052 S(c) -> K 1.052/1.052 S(c) -> L 1.052/1.052 -> QPairs: 1.052/1.052 Empty 1.052/1.052 -> Rules: 1.052/1.052 a -> c 1.052/1.052 a -> d 1.052/1.052 b -> c 1.052/1.052 b -> d 1.052/1.052 c -> e 1.052/1.052 d -> e 1.052/1.052 f(x) -> pair(x,y) | s(x) ->* t(y) 1.052/1.052 g(x,x) -> h(x,x) 1.052/1.052 k -> e 1.052/1.052 l -> e 1.052/1.052 s(c) -> t(k) 1.052/1.052 s(c) -> t(l) 1.052/1.052 s(e) -> t(e) 1.052/1.052 ->Strongly Connected Components: 1.052/1.052 There is no strongly connected component 1.052/1.052 1.052/1.052 The problem is finite. 1.052/1.052 1.052/1.052 Problem 1.2: 1.052/1.052 1.052/1.052 SCC Processor: 1.052/1.052 -> Pairs: 1.052/1.052 F(x) -> S(x) 1.052/1.052 -> QPairs: 1.052/1.052 S(c) -> K 1.052/1.052 S(c) -> L 1.052/1.052 -> Rules: 1.052/1.052 a -> c 1.052/1.052 a -> d 1.052/1.052 b -> c 1.052/1.052 b -> d 1.052/1.052 c -> e 1.052/1.052 d -> e 1.052/1.052 f(x) -> pair(x,y) | s(x) ->* t(y) 1.052/1.052 g(x,x) -> h(x,x) 1.052/1.052 k -> e 1.052/1.052 l -> e 1.052/1.052 s(c) -> t(k) 1.052/1.052 s(c) -> t(l) 1.052/1.052 s(e) -> t(e) 1.052/1.052 ->Strongly Connected Components: 1.052/1.052 There is no strongly connected component 1.052/1.052 1.052/1.052 The problem is finite. 1.052/1.052 1.052/1.052 1.052/1.052 -> Problem conclusions: 1.052/1.052 Not left linear, Not right linear, Not linear 1.052/1.052 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 1.052/1.052 CTRS Type: 3 1.052/1.052 Deterministic, Strongly deterministic 1.052/1.052 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 1.052/1.052 Maybe right-stable CTRS, Not overlay CTRS 1.052/1.052 Maybe normal CTRS, Maybe almost normal CTRS 1.052/1.052 Terminating CTRS, Operational terminating CTRS, Maybe joinable CCPs 1.052/1.052 Maybe level confluent 1.052/1.052 Maybe confluent 1.052/1.052 1.052/1.052 Problem 1: 1.052/1.052 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 1.052/1.052 Confluence Problem: 1.052/1.052 (VAR x y) 1.052/1.052 (REPLACEMENT-MAP 1.052/1.052 (a) 1.052/1.052 (b) 1.052/1.052 (c) 1.052/1.052 (d) 1.052/1.052 (f 1) 1.052/1.052 (g 1, 2) 1.052/1.052 (k) 1.052/1.052 (l) 1.052/1.052 (s 1) 1.052/1.052 (e) 1.052/1.052 (fSNonEmpty) 1.052/1.052 (h 1, 2) 1.052/1.052 (pair 1, 2) 1.052/1.052 (t 1) 1.052/1.052 ) 1.052/1.052 (RULES 1.052/1.052 a -> c 1.052/1.052 a -> d 1.052/1.052 b -> c 1.052/1.052 b -> d 1.052/1.052 c -> e 1.052/1.052 d -> e 1.052/1.052 f(x) -> pair(x,y) | s(x) ->* t(y) 1.052/1.052 g(x,x) -> h(x,x) 1.052/1.052 k -> e 1.052/1.052 l -> e 1.052/1.052 s(c) -> t(k) 1.052/1.052 s(c) -> t(l) 1.052/1.052 s(e) -> t(e) 1.052/1.052 ) 1.052/1.052 Critical Pairs: 1.052/1.052 => Not trivial, Not overlay, NW0, N1 1.052/1.052 => Not trivial, Overlay, NW0, N2 1.052/1.052 => Not trivial, Not overlay, NW0, N3 1.052/1.052 => Not trivial, Overlay, NW0, N4 1.052/1.052 Terminating:YES 1.052/1.052 1.052/1.052 -> Problem conclusions: 1.052/1.052 Not left linear, Not right linear, Not linear 1.052/1.052 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 1.052/1.052 CTRS Type: 3 1.052/1.052 Deterministic, Strongly deterministic 1.052/1.052 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 1.052/1.052 Maybe right-stable CTRS, Not overlay CTRS 1.052/1.052 Maybe normal CTRS, Maybe almost normal CTRS 1.052/1.052 Terminating CTRS, Operational terminating CTRS, Maybe joinable CCPs 1.052/1.052 Maybe level confluent 1.052/1.052 Maybe confluent 1.052/1.052 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 1.052/1.052 1.052/1.052 Right Stable Processor: 1.052/1.052 Right-stable CTRS 1.052/1.052 Justification: 1.052/1.052 1.052/1.052 -> Term right-stability conditions: 1.052/1.052 Term: t(c_y) 1.052/1.052 Right-stable term 1.052/1.052 Linear constructor form 1.052/1.052 Don't know if term is a ground normal form (not needed) 1.052/1.052 Right-stability condition achieved 1.052/1.052 A call to InfChecker wasn't needed 1.052/1.052 1.052/1.052 -> Problem conclusions: 1.052/1.052 Not left linear, Not right linear, Not linear 1.052/1.052 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 1.052/1.052 CTRS Type: 3 1.052/1.052 Deterministic, Strongly deterministic 1.052/1.052 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 1.052/1.052 Right-stable CTRS, Not overlay CTRS 1.052/1.052 Maybe normal CTRS, Almost normal CTRS 1.052/1.052 Terminating CTRS, Operational terminating CTRS, Maybe joinable CCPs 1.052/1.052 Maybe level confluent 1.052/1.052 Maybe confluent 1.052/1.052 1.052/1.052 Problem 1: 1.052/1.052 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 1.052/1.052 Confluence Problem: 1.052/1.052 (VAR x y) 1.052/1.052 (REPLACEMENT-MAP 1.052/1.052 (a) 1.052/1.052 (b) 1.052/1.052 (c) 1.052/1.052 (d) 1.052/1.052 (f 1) 1.052/1.052 (g 1, 2) 1.052/1.052 (k) 1.052/1.052 (l) 1.052/1.052 (s 1) 1.052/1.052 (e) 1.052/1.052 (fSNonEmpty) 1.052/1.052 (h 1, 2) 1.052/1.052 (pair 1, 2) 1.052/1.052 (t 1) 1.052/1.052 ) 1.052/1.052 (RULES 1.052/1.052 a -> c 1.052/1.052 a -> d 1.052/1.052 b -> c 1.052/1.052 b -> d 1.052/1.052 c -> e 1.052/1.052 d -> e 1.052/1.052 f(x) -> pair(x,y) | s(x) ->* t(y) 1.052/1.052 g(x,x) -> h(x,x) 1.052/1.052 k -> e 1.052/1.052 l -> e 1.052/1.052 s(c) -> t(k) 1.052/1.052 s(c) -> t(l) 1.052/1.052 s(e) -> t(e) 1.052/1.052 ) 1.052/1.052 Critical Pairs: 1.052/1.052 => Not trivial, Not overlay, NW0, N1 1.052/1.052 => Not trivial, Overlay, NW0, N2 1.052/1.052 => Not trivial, Not overlay, NW0, N3 1.052/1.052 => Not trivial, Overlay, NW0, N4 1.052/1.052 Terminating:YES 1.052/1.052 1.052/1.052 -> Problem conclusions: 1.052/1.052 Not left linear, Not right linear, Not linear 1.052/1.052 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 1.052/1.052 CTRS Type: 3 1.052/1.052 Deterministic, Strongly deterministic 1.052/1.052 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 1.052/1.052 Right-stable CTRS, Not overlay CTRS 1.052/1.052 Maybe normal CTRS, Almost normal CTRS 1.052/1.052 Terminating CTRS, Operational terminating CTRS, Maybe joinable CCPs 1.052/1.052 Maybe level confluent 1.052/1.052 Maybe confluent 1.052/1.052 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 1.052/1.052 1.052/1.052 Normal RConds Processor: 1.052/1.052 YES 1.052/1.052 1.052/1.052 Problem 1: 1.052/1.052 1.052/1.052 Infeasibility Problem: 1.052/1.052 [(VAR vNonEmpty x y vNonEmpty z) 1.052/1.052 (STRATEGY CONTEXTSENSITIVE 1.052/1.052 (a) 1.052/1.052 (b) 1.052/1.052 (c) 1.052/1.052 (d) 1.052/1.052 (f 1) 1.052/1.052 (g 1 2) 1.052/1.052 (k) 1.052/1.052 (l) 1.052/1.052 (s 1) 1.052/1.052 (c_x0) 1.052/1.052 (e) 1.052/1.052 (fSNonEmpty) 1.052/1.052 (h 1 2) 1.052/1.052 (pair 1 2) 1.052/1.052 (t 1) 1.052/1.052 ) 1.052/1.052 (RULES 1.052/1.052 a -> c 1.052/1.052 a -> d 1.052/1.052 b -> c 1.052/1.052 b -> d 1.052/1.052 c -> e 1.052/1.052 d -> e 1.052/1.052 f(x) -> pair(x,y) | s(x) ->* t(y) 1.052/1.052 g(x,x) -> h(x,x) 1.052/1.052 k -> e 1.052/1.052 l -> e 1.052/1.052 s(c) -> t(k) 1.052/1.052 s(c) -> t(l) 1.052/1.052 s(e) -> t(e) 1.052/1.052 )] 1.052/1.052 1.052/1.052 Infeasibility Conditions: 1.052/1.052 t(c_x0) -> z 1.052/1.052 1.052/1.052 Problem 1: 1.052/1.052 1.052/1.052 Obtaining a model using Mace4: 1.052/1.052 1.052/1.052 -> Usable Rules: 1.052/1.052 Empty 1.052/1.052 1.052/1.052 -> Mace4 Output: 1.052/1.052 ============================== Mace4 ================================= 1.052/1.052 Mace4 (64) version 2009-11A, November 2009. 1.052/1.052 Process 60334 was started by ubuntu on ubuntu, 1.052/1.052 Wed Mar 9 09:44:10 2022 1.052/1.052 The command was "./mace4 -c -f /tmp/mace460323-2.in". 1.052/1.052 ============================== end of head =========================== 1.052/1.052 1.052/1.052 ============================== INPUT ================================= 1.052/1.052 1.052/1.052 % Reading from file /tmp/mace460323-2.in 1.052/1.052 1.052/1.052 assign(max_seconds,13). 1.052/1.052 1.052/1.052 formulas(assumptions). 1.052/1.052 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence). 1.052/1.052 ->(x1,y) -> ->(g(x1,x2),g(y,x2)) # label(congruence). 1.052/1.052 ->(x2,y) -> ->(g(x1,x2),g(x1,y)) # label(congruence). 1.052/1.052 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence). 1.052/1.052 ->(x1,y) -> ->(h(x1,x2),h(y,x2)) # label(congruence). 1.052/1.052 ->(x2,y) -> ->(h(x1,x2),h(x1,y)) # label(congruence). 1.052/1.052 ->(x1,y) -> ->(pair(x1,x2),pair(y,x2)) # label(congruence). 1.052/1.052 ->(x2,y) -> ->(pair(x1,x2),pair(x1,y)) # label(congruence). 1.052/1.052 ->(x1,y) -> ->(t(x1),t(y)) # label(congruence). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(goals). 1.052/1.052 (exists x4 ->(t(c_x0),x4)) # label(goal). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 ============================== end of input ========================== 1.052/1.052 1.052/1.052 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 1.052/1.052 1.052/1.052 % Formulas that are not ordinary clauses: 1.052/1.052 1 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence) # label(non_clause). [assumption]. 1.052/1.052 2 ->(x1,y) -> ->(g(x1,x2),g(y,x2)) # label(congruence) # label(non_clause). [assumption]. 1.052/1.052 3 ->(x2,y) -> ->(g(x1,x2),g(x1,y)) # label(congruence) # label(non_clause). [assumption]. 1.052/1.052 4 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 1.052/1.052 5 ->(x1,y) -> ->(h(x1,x2),h(y,x2)) # label(congruence) # label(non_clause). [assumption]. 1.052/1.052 6 ->(x2,y) -> ->(h(x1,x2),h(x1,y)) # label(congruence) # label(non_clause). [assumption]. 1.052/1.052 7 ->(x1,y) -> ->(pair(x1,x2),pair(y,x2)) # label(congruence) # label(non_clause). [assumption]. 1.052/1.052 8 ->(x2,y) -> ->(pair(x1,x2),pair(x1,y)) # label(congruence) # label(non_clause). [assumption]. 1.052/1.052 9 ->(x1,y) -> ->(t(x1),t(y)) # label(congruence) # label(non_clause). [assumption]. 1.052/1.052 10 (exists x4 ->(t(c_x0),x4)) # label(goal) # label(non_clause) # label(goal). [goal]. 1.052/1.052 1.052/1.052 ============================== end of process non-clausal formulas === 1.052/1.052 1.052/1.052 ============================== CLAUSES FOR SEARCH ==================== 1.052/1.052 1.052/1.052 formulas(mace4_clauses). 1.052/1.052 -->(x,y) | ->(f(x),f(y)) # label(congruence). 1.052/1.052 -->(x,y) | ->(g(x,z),g(y,z)) # label(congruence). 1.052/1.052 -->(x,y) | ->(g(z,x),g(z,y)) # label(congruence). 1.052/1.052 -->(x,y) | ->(s(x),s(y)) # label(congruence). 1.052/1.052 -->(x,y) | ->(h(x,z),h(y,z)) # label(congruence). 1.052/1.052 -->(x,y) | ->(h(z,x),h(z,y)) # label(congruence). 1.052/1.052 -->(x,y) | ->(pair(x,z),pair(y,z)) # label(congruence). 1.052/1.052 -->(x,y) | ->(pair(z,x),pair(z,y)) # label(congruence). 1.052/1.052 -->(x,y) | ->(t(x),t(y)) # label(congruence). 1.052/1.052 -->(t(c_x0),x) # label(goal). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 ============================== end of clauses for search ============= 1.052/1.052 1.052/1.052 % There are no natural numbers in the input. 1.052/1.052 1.052/1.052 ============================== DOMAIN SIZE 2 ========================= 1.052/1.052 1.052/1.052 ============================== MODEL ================================= 1.052/1.052 1.052/1.052 interpretation( 2, [number=1, seconds=0], [ 1.052/1.052 1.052/1.052 function(c_x0, [ 0 ]), 1.052/1.052 1.052/1.052 function(s(_), [ 0, 0 ]), 1.052/1.052 1.052/1.052 function(t(_), [ 0, 0 ]), 1.052/1.052 1.052/1.052 function(f(_), [ 0, 0 ]), 1.052/1.052 1.052/1.052 function(h(_,_), [ 1.052/1.052 0, 0, 1.052/1.052 0, 0 ]), 1.052/1.052 1.052/1.052 function(pair(_,_), [ 1.052/1.052 0, 0, 1.052/1.052 0, 0 ]), 1.052/1.052 1.052/1.052 function(g(_,_), [ 1.052/1.052 0, 0, 1.052/1.052 0, 0 ]), 1.052/1.052 1.052/1.052 relation(->(_,_), [ 1.052/1.052 0, 0, 1.052/1.052 0, 0 ]) 1.052/1.052 ]). 1.052/1.052 1.052/1.052 ============================== end of model ========================== 1.052/1.052 1.052/1.052 ============================== STATISTICS ============================ 1.052/1.052 1.052/1.052 For domain size 2. 1.052/1.052 1.052/1.052 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 1.052/1.052 Ground clauses: seen=62, kept=62. 1.052/1.052 Selections=19, assignments=19, propagations=4, current_models=1. 1.052/1.052 Rewrite_terms=124, rewrite_bools=66, indexes=5. 1.052/1.052 Rules_from_neg_clauses=0, cross_offs=0. 1.052/1.052 1.052/1.052 ============================== end of statistics ===================== 1.052/1.052 1.052/1.052 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 1.052/1.052 1.052/1.052 Exiting with 1 model. 1.052/1.052 1.052/1.052 Process 60334 exit (max_models) Wed Mar 9 09:44:10 2022 1.052/1.052 The process finished Wed Mar 9 09:44:10 2022 1.052/1.052 1.052/1.052 1.052/1.052 Mace4 cooked interpretation: 1.052/1.052 1.052/1.052 1.052/1.052 1.052/1.052 The problem is infeasible. 1.052/1.052 1.052/1.052 1.052/1.052 -> Problem conclusions: 1.052/1.052 Not left linear, Not right linear, Not linear 1.052/1.052 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 1.052/1.052 CTRS Type: 3 1.052/1.052 Deterministic, Strongly deterministic 1.052/1.052 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 1.052/1.052 Right-stable CTRS, Not overlay CTRS 1.052/1.052 Not normal CTRS, Almost normal CTRS 1.052/1.052 Terminating CTRS, Operational terminating CTRS, Maybe joinable CCPs 1.052/1.052 Maybe level confluent 1.052/1.052 Maybe confluent 1.052/1.052 1.052/1.052 Problem 1: 1.052/1.052 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 1.052/1.052 Confluence Problem: 1.052/1.052 (VAR x y) 1.052/1.052 (REPLACEMENT-MAP 1.052/1.052 (a) 1.052/1.052 (b) 1.052/1.052 (c) 1.052/1.052 (d) 1.052/1.052 (f 1) 1.052/1.052 (g 1, 2) 1.052/1.052 (k) 1.052/1.052 (l) 1.052/1.052 (s 1) 1.052/1.052 (e) 1.052/1.052 (fSNonEmpty) 1.052/1.052 (h 1, 2) 1.052/1.052 (pair 1, 2) 1.052/1.052 (t 1) 1.052/1.052 ) 1.052/1.052 (RULES 1.052/1.052 a -> c 1.052/1.052 a -> d 1.052/1.052 b -> c 1.052/1.052 b -> d 1.052/1.052 c -> e 1.052/1.052 d -> e 1.052/1.052 f(x) -> pair(x,y) | s(x) ->* t(y) 1.052/1.052 g(x,x) -> h(x,x) 1.052/1.052 k -> e 1.052/1.052 l -> e 1.052/1.052 s(c) -> t(k) 1.052/1.052 s(c) -> t(l) 1.052/1.052 s(e) -> t(e) 1.052/1.052 ) 1.052/1.052 Critical Pairs: 1.052/1.052 => Not trivial, Not overlay, NW0, N1 1.052/1.052 => Not trivial, Overlay, NW0, N2 1.052/1.052 => Not trivial, Not overlay, NW0, N3 1.052/1.052 => Not trivial, Overlay, NW0, N4 1.052/1.052 Terminating:YES 1.052/1.052 1.052/1.052 -> Problem conclusions: 1.052/1.052 Not left linear, Not right linear, Not linear 1.052/1.052 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 1.052/1.052 CTRS Type: 3 1.052/1.052 Deterministic, Strongly deterministic 1.052/1.052 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 1.052/1.052 Right-stable CTRS, Not overlay CTRS 1.052/1.052 Not normal CTRS, Almost normal CTRS 1.052/1.052 Terminating CTRS, Operational terminating CTRS, Maybe joinable CCPs 1.052/1.052 Maybe level confluent 1.052/1.052 Maybe confluent 1.052/1.052 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 1.052/1.052 1.052/1.052 Conditional Critical Pairs Distributor Processor 1.052/1.052 1.052/1.052 1.052/1.052 The problem is decomposed in 4 subproblems. 1.052/1.052 1.052/1.052 Problem 1.1: 1.052/1.052 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 1.052/1.052 Confluence Problem: 1.052/1.052 (VAR x y) 1.052/1.052 (REPLACEMENT-MAP 1.052/1.052 (a) 1.052/1.052 (b) 1.052/1.052 (c) 1.052/1.052 (d) 1.052/1.052 (f 1) 1.052/1.052 (g 1, 2) 1.052/1.052 (k) 1.052/1.052 (l) 1.052/1.052 (s 1) 1.052/1.052 (e) 1.052/1.052 (fSNonEmpty) 1.052/1.052 (h 1, 2) 1.052/1.052 (pair 1, 2) 1.052/1.052 (t 1) 1.052/1.052 ) 1.052/1.052 (RULES 1.052/1.052 a -> c 1.052/1.052 a -> d 1.052/1.052 b -> c 1.052/1.052 b -> d 1.052/1.052 c -> e 1.052/1.052 d -> e 1.052/1.052 f(x) -> pair(x,y) | s(x) ->* t(y) 1.052/1.052 g(x,x) -> h(x,x) 1.052/1.052 k -> e 1.052/1.052 l -> e 1.052/1.052 s(c) -> t(k) 1.052/1.052 s(c) -> t(l) 1.052/1.052 s(e) -> t(e) 1.052/1.052 ) 1.052/1.052 Critical Pairs: 1.052/1.052 => Not trivial, Not overlay, NW0, N1 1.052/1.052 Terminating:YES 1.052/1.052 1.052/1.052 -> Problem conclusions: 1.052/1.052 Not left linear, Not right linear, Not linear 1.052/1.052 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 1.052/1.052 CTRS Type: 3 1.052/1.052 Deterministic, Strongly deterministic 1.052/1.052 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 1.052/1.052 Right-stable CTRS, Not overlay CTRS 1.052/1.052 Not normal CTRS, Almost normal CTRS 1.052/1.052 Terminating CTRS, Operational terminating CTRS, Maybe joinable CCPs 1.052/1.052 Maybe level confluent 1.052/1.052 Maybe confluent 1.052/1.052 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 1.052/1.052 1.052/1.052 Prover9 CCP Convergence Checker Processor: 1.052/1.052 Proof: 1.052/1.052 ============================== Prover9 =============================== 1.052/1.052 Prover9 (64) version 2009-11A, November 2009. 1.052/1.052 Process 60349 was started by ubuntu on ubuntu, 1.052/1.052 Wed Mar 9 09:44:10 2022 1.052/1.052 The command was "./prover9 -t 60 -f /tmp/prover960079-28.in". 1.052/1.052 ============================== end of head =========================== 1.052/1.052 1.052/1.052 ============================== INPUT ================================= 1.052/1.052 1.052/1.052 % Reading from file /tmp/prover960079-28.in 1.052/1.052 1.052/1.052 1.052/1.052 formulas(sos). 1.052/1.052 reds(x,x). 1.052/1.052 red(x,y) & reds(y,z) -> reds(x,z). 1.052/1.052 red(x,y) -> red(f(x),f(y)). 1.052/1.052 red(x,y) -> red(g(x,z1),g(y,z1)). 1.052/1.052 red(x,y) -> red(g(z,x),g(z,y)). 1.052/1.052 red(x,y) -> red(s(x),s(y)). 1.052/1.052 red(x,y) -> red(h(x,z1),h(y,z1)). 1.052/1.052 red(x,y) -> red(h(z,x),h(z,y)). 1.052/1.052 red(x,y) -> red(pair(x,z1),pair(y,z1)). 1.052/1.052 red(x,y) -> red(pair(z,x),pair(z,y)). 1.052/1.052 red(x,y) -> red(t(x),t(y)). 1.052/1.052 red(a,c). 1.052/1.052 red(a,d). 1.052/1.052 red(b,c). 1.052/1.052 red(b,d). 1.052/1.052 red(c,e). 1.052/1.052 red(d,e). 1.052/1.052 (all x all y (reds(s(x),t(y)) -> red(f(x),pair(x,y)))). 1.052/1.052 (all x red(g(x,x),h(x,x))). 1.052/1.052 red(k,e). 1.052/1.052 red(l,e). 1.052/1.052 red(s(c),t(k)). 1.052/1.052 red(s(c),t(l)). 1.052/1.052 red(s(e),t(e)). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(goals). 1.052/1.052 (exists z (reds(s(e),z) & reds(t(l),z))). 1.052/1.052 end_of_list. 1.052/1.052 assign(max_megs,-1). 1.052/1.052 set(quiet). 1.052/1.052 1.052/1.052 ============================== end of input ========================== 1.052/1.052 1.052/1.052 % From the command line: assign(max_seconds, 60). 1.052/1.052 1.052/1.052 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 1.052/1.052 1.052/1.052 % Formulas that are not ordinary clauses: 1.052/1.052 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 1.052/1.052 2 red(x,y) -> red(f(x),f(y)) # label(non_clause). [assumption]. 1.052/1.052 3 red(x,y) -> red(g(x,z1),g(y,z1)) # label(non_clause). [assumption]. 1.052/1.052 4 red(x,y) -> red(g(z,x),g(z,y)) # label(non_clause). [assumption]. 1.052/1.052 5 red(x,y) -> red(s(x),s(y)) # label(non_clause). [assumption]. 1.052/1.052 6 red(x,y) -> red(h(x,z1),h(y,z1)) # label(non_clause). [assumption]. 1.052/1.052 7 red(x,y) -> red(h(z,x),h(z,y)) # label(non_clause). [assumption]. 1.052/1.052 8 red(x,y) -> red(pair(x,z1),pair(y,z1)) # label(non_clause). [assumption]. 1.052/1.052 9 red(x,y) -> red(pair(z,x),pair(z,y)) # label(non_clause). [assumption]. 1.052/1.052 10 red(x,y) -> red(t(x),t(y)) # label(non_clause). [assumption]. 1.052/1.052 11 (all x all y (reds(s(x),t(y)) -> red(f(x),pair(x,y)))) # label(non_clause). [assumption]. 1.052/1.052 12 (all x red(g(x,x),h(x,x))) # label(non_clause). [assumption]. 1.052/1.052 13 (exists z (reds(s(e),z) & reds(t(l),z))) # label(non_clause) # label(goal). [goal]. 1.052/1.052 1.052/1.052 ============================== end of process non-clausal formulas === 1.052/1.052 1.052/1.052 ============================== PROCESS INITIAL CLAUSES =============== 1.052/1.052 1.052/1.052 % Clauses before input processing: 1.052/1.052 1.052/1.052 formulas(usable). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(sos). 1.052/1.052 reds(x,x). [assumption]. 1.052/1.052 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 1.052/1.052 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 1.052/1.052 -red(x,y) | red(g(x,z),g(y,z)). [clausify(3)]. 1.052/1.052 -red(x,y) | red(g(z,x),g(z,y)). [clausify(4)]. 1.052/1.052 -red(x,y) | red(s(x),s(y)). [clausify(5)]. 1.052/1.052 -red(x,y) | red(h(x,z),h(y,z)). [clausify(6)]. 1.052/1.052 -red(x,y) | red(h(z,x),h(z,y)). [clausify(7)]. 1.052/1.052 -red(x,y) | red(pair(x,z),pair(y,z)). [clausify(8)]. 1.052/1.052 -red(x,y) | red(pair(z,x),pair(z,y)). [clausify(9)]. 1.052/1.052 -red(x,y) | red(t(x),t(y)). [clausify(10)]. 1.052/1.052 red(a,c). [assumption]. 1.052/1.052 red(a,d). [assumption]. 1.052/1.052 red(b,c). [assumption]. 1.052/1.052 red(b,d). [assumption]. 1.052/1.052 red(c,e). [assumption]. 1.052/1.052 red(d,e). [assumption]. 1.052/1.052 -reds(s(x),t(y)) | red(f(x),pair(x,y)). [clausify(11)]. 1.052/1.052 red(g(x,x),h(x,x)). [clausify(12)]. 1.052/1.052 red(k,e). [assumption]. 1.052/1.052 red(l,e). [assumption]. 1.052/1.052 red(s(c),t(k)). [assumption]. 1.052/1.052 red(s(c),t(l)). [assumption]. 1.052/1.052 red(s(e),t(e)). [assumption]. 1.052/1.052 -reds(s(e),x) | -reds(t(l),x). [deny(13)]. 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(demodulators). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 ============================== PREDICATE ELIMINATION ================= 1.052/1.052 1.052/1.052 ============================== end predicate elimination ============= 1.052/1.052 1.052/1.052 Auto_denials: (no changes). 1.052/1.052 1.052/1.052 Term ordering decisions: 1.052/1.052 1.052/1.052 kept: 14 reds(x,x). [assumption]. 1.052/1.052 kept: 15 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 1.052/1.052 kept: 16 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 1.052/1.052 kept: 17 -red(x,y) | red(g(x,z),g(y,z)). [clausify(3)]. 1.052/1.052 kept: 18 -red(x,y) | red(g(z,x),g(z,y)). [clausify(4)]. 1.052/1.052 kept: 19 -red(x,y) | red(s(x),s(y)). [clausify(5)]. 1.052/1.052 kept: 20 -red(x,y) | red(h(x,z),h(y,z)). [clausify(6)]. 1.052/1.052 kept: 21 -red(x,y) | red(h(z,x),h(z,y)). [clausify(7)]. 1.052/1.052 kept: 22 -red(x,y) | red(pair(x,z),pair(y,z)). [clausify(8)]. 1.052/1.052 kept: 23 -red(x,y) | red(pair(z,x),pair(z,y)). [clausify(9)]. 1.052/1.052 kept: 24 -red(x,y) | red(t(x),t(y)). [clausify(10)]. 1.052/1.052 kept: 25 red(a,c). [assumption]. 1.052/1.052 kept: 26 red(a,d). [assumption]. 1.052/1.052 kept: 27 red(b,c). [assumption]. 1.052/1.052 kept: 28 red(b,d). [assumption]. 1.052/1.052 kept: 29 red(c,e). [assumption]. 1.052/1.052 kept: 30 red(d,e). [assumption]. 1.052/1.052 kept: 31 -reds(s(x),t(y)) | red(f(x),pair(x,y)). [clausify(11)]. 1.052/1.052 kept: 32 red(g(x,x),h(x,x)). [clausify(12)]. 1.052/1.052 kept: 33 red(k,e). [assumption]. 1.052/1.052 kept: 34 red(l,e). [assumption]. 1.052/1.052 kept: 35 red(s(c),t(k)). [assumption]. 1.052/1.052 kept: 36 red(s(c),t(l)). [assumption]. 1.052/1.052 kept: 37 red(s(e),t(e)). [assumption]. 1.052/1.052 kept: 38 -reds(s(e),x) | -reds(t(l),x). [deny(13)]. 1.052/1.052 1.052/1.052 ============================== end of process initial clauses ======== 1.052/1.052 1.052/1.052 ============================== CLAUSES FOR SEARCH ==================== 1.052/1.052 1.052/1.052 % Clauses after input processing: 1.052/1.052 1.052/1.052 formulas(usable). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(sos). 1.052/1.052 14 reds(x,x). [assumption]. 1.052/1.052 15 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 1.052/1.052 16 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 1.052/1.052 17 -red(x,y) | red(g(x,z),g(y,z)). [clausify(3)]. 1.052/1.052 18 -red(x,y) | red(g(z,x),g(z,y)). [clausify(4)]. 1.052/1.052 19 -red(x,y) | red(s(x),s(y)). [clausify(5)]. 1.052/1.052 20 -red(x,y) | red(h(x,z),h(y,z)). [clausify(6)]. 1.052/1.052 21 -red(x,y) | red(h(z,x),h(z,y)). [clausify(7)]. 1.052/1.052 22 -red(x,y) | red(pair(x,z),pair(y,z)). [clausify(8)]. 1.052/1.052 23 -red(x,y) | red(pair(z,x),pair(z,y)). [clausify(9)]. 1.052/1.052 24 -red(x,y) | red(t(x),t(y)). [clausify(10)]. 1.052/1.052 25 red(a,c). [assumption]. 1.052/1.052 26 red(a,d). [assumption]. 1.052/1.052 27 red(b,c). [assumption]. 1.052/1.052 28 red(b,d). [assumption]. 1.052/1.052 29 red(c,e). [assumption]. 1.052/1.052 30 red(d,e). [assumption]. 1.052/1.052 31 -reds(s(x),t(y)) | red(f(x),pair(x,y)). [clausify(11)]. 1.052/1.052 32 red(g(x,x),h(x,x)). [clausify(12)]. 1.052/1.052 33 red(k,e). [assumption]. 1.052/1.052 34 red(l,e). [assumption]. 1.052/1.052 35 red(s(c),t(k)). [assumption]. 1.052/1.052 36 red(s(c),t(l)). [assumption]. 1.052/1.052 37 red(s(e),t(e)). [assumption]. 1.052/1.052 38 -reds(s(e),x) | -reds(t(l),x). [deny(13)]. 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(demodulators). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 ============================== end of clauses for search ============= 1.052/1.052 1.052/1.052 ============================== SEARCH ================================ 1.052/1.052 1.052/1.052 % Starting search at 0.01 seconds. 1.052/1.052 1.052/1.052 given #1 (I,wt=3): 14 reds(x,x). [assumption]. 1.052/1.052 1.052/1.052 given #2 (I,wt=9): 15 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 1.052/1.052 1.052/1.052 given #3 (I,wt=8): 16 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 1.052/1.052 1.052/1.052 given #4 (I,wt=10): 17 -red(x,y) | red(g(x,z),g(y,z)). [clausify(3)]. 1.052/1.052 1.052/1.052 given #5 (I,wt=10): 18 -red(x,y) | red(g(z,x),g(z,y)). [clausify(4)]. 1.052/1.052 1.052/1.052 given #6 (I,wt=8): 19 -red(x,y) | red(s(x),s(y)). [clausify(5)]. 1.052/1.052 1.052/1.052 given #7 (I,wt=10): 20 -red(x,y) | red(h(x,z),h(y,z)). [clausify(6)]. 1.052/1.052 1.052/1.052 given #8 (I,wt=10): 21 -red(x,y) | red(h(z,x),h(z,y)). [clausify(7)]. 1.052/1.052 1.052/1.052 given #9 (I,wt=10): 22 -red(x,y) | red(pair(x,z),pair(y,z)). [clausify(8)]. 1.052/1.052 1.052/1.052 given #10 (I,wt=10): 23 -red(x,y) | red(pair(z,x),pair(z,y)). [clausify(9)]. 1.052/1.052 1.052/1.052 given #11 (I,wt=8): 24 -red(x,y) | red(t(x),t(y)). [clausify(10)]. 1.052/1.052 1.052/1.052 given #12 (I,wt=3): 25 red(a,c). [assumption]. 1.052/1.052 1.052/1.052 given #13 (I,wt=3): 26 red(a,d). [assumption]. 1.052/1.052 1.052/1.052 given #14 (I,wt=3): 27 red(b,c). [assumption]. 1.052/1.052 1.052/1.052 given #15 (I,wt=3): 28 red(b,d). [assumption]. 1.052/1.052 1.052/1.052 given #16 (I,wt=3): 29 red(c,e). [assumption]. 1.052/1.052 1.052/1.052 given #17 (I,wt=3): 30 red(d,e). [assumption]. 1.052/1.052 1.052/1.052 given #18 (I,wt=11): 31 -reds(s(x),t(y)) | red(f(x),pair(x,y)). [clausify(11)]. 1.052/1.052 1.052/1.052 given #19 (I,wt=7): 32 red(g(x,x),h(x,x)). [clausify(12)]. 1.052/1.052 1.052/1.052 given #20 (I,wt=3): 33 red(k,e). [assumption]. 1.052/1.052 1.052/1.052 given #21 (I,wt=3): 34 red(l,e). [assumption]. 1.052/1.052 1.052/1.052 given #22 (I,wt=5): 35 red(s(c),t(k)). [assumption]. 1.052/1.052 1.052/1.052 given #23 (I,wt=5): 36 red(s(c),t(l)). [assumption]. 1.052/1.052 1.052/1.052 given #24 (I,wt=5): 37 red(s(e),t(e)). [assumption]. 1.052/1.052 1.052/1.052 given #25 (I,wt=8): 38 -reds(s(e),x) | -reds(t(l),x). [deny(13)]. 1.052/1.052 1.052/1.052 given #26 (A,wt=5): 39 red(t(a),t(c)). [ur(24,a,25,a)]. 1.052/1.052 1.052/1.052 given #27 (F,wt=5): 160 -reds(t(l),s(e)). [resolve(38,a,14,a)]. 1.052/1.052 1.052/1.052 given #28 (F,wt=5): 162 -reds(s(e),t(l)). [resolve(38,b,14,a)]. 1.052/1.052 1.052/1.052 given #29 (F,wt=5): 174 -red(t(l),s(e)). [ur(15,b,14,a,c,160,a)]. 1.052/1.052 1.052/1.052 given #30 (F,wt=5): 176 -red(s(e),t(l)). [ur(15,b,14,a,c,162,a)]. 1.052/1.052 1.052/1.052 given #31 (T,wt=3): 48 reds(a,c). [ur(15,a,25,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #32 (T,wt=3): 58 reds(a,d). [ur(15,a,26,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #33 (T,wt=3): 68 reds(b,c). [ur(15,a,27,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #34 (T,wt=3): 78 reds(b,d). [ur(15,a,28,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #35 (A,wt=7): 40 red(pair(x,a),pair(x,c)). [ur(23,a,25,a)]. 1.052/1.052 1.052/1.052 given #36 (F,wt=5): 177 -reds(t(e),t(l)). [ur(15,a,37,a,c,162,a)]. 1.052/1.052 1.052/1.052 given #37 (F,wt=5): 189 -red(t(e),t(l)). [ur(15,b,14,a,c,177,a)]. 1.052/1.052 1.052/1.052 given #38 (F,wt=3): 190 -red(e,l). [resolve(189,a,24,b)]. 1.052/1.052 1.052/1.052 given #39 (F,wt=8): 173 -red(t(l),x) | -reds(x,s(e)). [resolve(160,a,15,c)]. 1.052/1.052 1.052/1.052 given #40 (T,wt=3): 88 reds(c,e). [ur(15,a,29,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #41 (T,wt=3): 98 reds(d,e). [ur(15,a,30,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #42 (T,wt=3): 118 reds(k,e). [ur(15,a,33,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #43 (T,wt=3): 128 reds(l,e). [ur(15,a,34,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #44 (A,wt=7): 41 red(pair(a,x),pair(c,x)). [ur(22,a,25,a)]. 1.052/1.052 1.052/1.052 given #45 (F,wt=8): 175 -red(s(e),x) | -reds(x,t(l)). [resolve(162,a,15,c)]. 1.052/1.052 1.052/1.052 given #46 (F,wt=8): 188 -red(t(e),x) | -reds(x,t(l)). [resolve(177,a,15,c)]. 1.052/1.052 1.052/1.052 given #47 (F,wt=8): 191 -reds(t(x),s(e)) | -red(l,x). [resolve(173,a,24,b)]. 1.052/1.052 1.052/1.052 given #48 (F,wt=5): 210 -reds(t(e),s(e)). [resolve(191,b,34,a)]. 1.052/1.052 1.052/1.052 given #49 (T,wt=3): 193 reds(b,e). [ur(15,a,27,a,b,88,a)]. 1.052/1.052 1.052/1.052 given #50 (T,wt=3): 194 reds(a,e). [ur(15,a,25,a,b,88,a)]. 1.052/1.052 1.052/1.052 given #51 (T,wt=5): 44 red(s(a),s(c)). [ur(19,a,25,a)]. 1.052/1.052 1.052/1.052 given #52 (T,wt=5): 47 red(f(a),f(c)). [ur(16,a,25,a)]. 1.052/1.052 1.052/1.052 given #53 (A,wt=7): 42 red(h(x,a),h(x,c)). [ur(21,a,25,a)]. 1.052/1.052 1.052/1.052 given #54 (F,wt=5): 212 -red(t(e),s(e)). [ur(15,b,14,a,c,210,a)]. 1.052/1.052 1.052/1.052 given #55 (F,wt=8): 205 -reds(s(x),t(l)) | -red(e,x). [resolve(175,a,19,b)]. 1.052/1.052 1.052/1.052 given #56 (F,wt=8): 207 -reds(t(x),t(l)) | -red(e,x). [resolve(188,a,24,b)]. 1.052/1.052 1.052/1.052 given #57 (F,wt=8): 211 -red(t(e),x) | -reds(x,s(e)). [resolve(210,a,15,c)]. 1.052/1.052 1.052/1.052 given #58 (T,wt=5): 49 red(t(a),t(d)). [ur(24,a,26,a)]. 1.052/1.052 1.052/1.052 given #59 (T,wt=5): 54 red(s(a),s(d)). [ur(19,a,26,a)]. 1.052/1.052 1.052/1.052 given #60 (T,wt=5): 57 red(f(a),f(d)). [ur(16,a,26,a)]. 1.052/1.052 1.052/1.052 given #61 (T,wt=5): 59 red(t(b),t(c)). [ur(24,a,27,a)]. 1.052/1.052 1.052/1.052 given #62 (A,wt=7): 43 red(h(a,x),h(c,x)). [ur(20,a,25,a)]. 1.052/1.052 1.052/1.052 given #63 (F,wt=8): 245 -reds(t(x),s(e)) | -red(e,x). [resolve(211,a,24,b)]. 1.052/1.052 1.052/1.052 given #64 (F,wt=11): 159 -reds(t(l),x) | -red(s(e),y) | -reds(y,x). [resolve(38,a,15,c)]. 1.052/1.052 1.052/1.052 given #65 (F,wt=5): 313 -reds(t(l),t(e)). [ur(159,b,37,a,c,14,a)]. 1.052/1.052 1.052/1.052 ============================== PROOF ================================= 1.052/1.052 1.052/1.052 % Proof 1 at 0.01 (+ 0.00) seconds. 1.052/1.052 % Length of proof is 13. 1.052/1.052 % Level of proof is 4. 1.052/1.052 % Maximum clause weight is 11.000. 1.052/1.052 % Given clauses 65. 1.052/1.052 1.052/1.052 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 1.052/1.052 10 red(x,y) -> red(t(x),t(y)) # label(non_clause). [assumption]. 1.052/1.052 13 (exists z (reds(s(e),z) & reds(t(l),z))) # label(non_clause) # label(goal). [goal]. 1.052/1.052 14 reds(x,x). [assumption]. 1.052/1.052 15 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 1.052/1.052 24 -red(x,y) | red(t(x),t(y)). [clausify(10)]. 1.052/1.052 34 red(l,e). [assumption]. 1.052/1.052 37 red(s(e),t(e)). [assumption]. 1.052/1.052 38 -reds(s(e),x) | -reds(t(l),x). [deny(13)]. 1.052/1.052 119 red(t(l),t(e)). [ur(24,a,34,a)]. 1.052/1.052 159 -reds(t(l),x) | -red(s(e),y) | -reds(y,x). [resolve(38,a,15,c)]. 1.052/1.052 313 -reds(t(l),t(e)). [ur(159,b,37,a,c,14,a)]. 1.052/1.052 315 $F. [ur(15,b,14,a,c,313,a),unit_del(a,119)]. 1.052/1.052 1.052/1.052 ============================== end of proof ========================== 1.052/1.052 1.052/1.052 ============================== STATISTICS ============================ 1.052/1.052 1.052/1.052 Given=65. Generated=323. Kept=301. proofs=1. 1.052/1.052 Usable=65. Sos=235. Demods=0. Limbo=1, Disabled=25. Hints=0. 1.052/1.052 Kept_by_rule=0, Deleted_by_rule=0. 1.052/1.052 Forward_subsumed=21. Back_subsumed=0. 1.052/1.052 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 1.052/1.052 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 1.052/1.052 Demod_attempts=0. Demod_rewrites=0. 1.052/1.052 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 1.052/1.052 Nonunit_fsub_feature_tests=112. Nonunit_bsub_feature_tests=128. 1.052/1.052 Megabytes=0.45. 1.052/1.052 User_CPU=0.01, System_CPU=0.00, Wall_clock=0. 1.052/1.052 1.052/1.052 ============================== end of statistics ===================== 1.052/1.052 1.052/1.052 ============================== end of search ========================= 1.052/1.052 1.052/1.052 THEOREM PROVED 1.052/1.052 1.052/1.052 Exiting with 1 proof. 1.052/1.052 1.052/1.052 Process 60349 exit (max_proofs) Wed Mar 9 09:44:10 2022 1.052/1.052 1.052/1.052 1.052/1.052 The problem is joinable. 1.052/1.052 1.052/1.052 Problem 1.2: 1.052/1.052 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 1.052/1.052 Confluence Problem: 1.052/1.052 (VAR x y) 1.052/1.052 (REPLACEMENT-MAP 1.052/1.052 (a) 1.052/1.052 (b) 1.052/1.052 (c) 1.052/1.052 (d) 1.052/1.052 (f 1) 1.052/1.052 (g 1, 2) 1.052/1.052 (k) 1.052/1.052 (l) 1.052/1.052 (s 1) 1.052/1.052 (e) 1.052/1.052 (fSNonEmpty) 1.052/1.052 (h 1, 2) 1.052/1.052 (pair 1, 2) 1.052/1.052 (t 1) 1.052/1.052 ) 1.052/1.052 (RULES 1.052/1.052 a -> c 1.052/1.052 a -> d 1.052/1.052 b -> c 1.052/1.052 b -> d 1.052/1.052 c -> e 1.052/1.052 d -> e 1.052/1.052 f(x) -> pair(x,y) | s(x) ->* t(y) 1.052/1.052 g(x,x) -> h(x,x) 1.052/1.052 k -> e 1.052/1.052 l -> e 1.052/1.052 s(c) -> t(k) 1.052/1.052 s(c) -> t(l) 1.052/1.052 s(e) -> t(e) 1.052/1.052 ) 1.052/1.052 Critical Pairs: 1.052/1.052 => Not trivial, Overlay, NW0, N2 1.052/1.052 Terminating:YES 1.052/1.052 1.052/1.052 -> Problem conclusions: 1.052/1.052 Not left linear, Not right linear, Not linear 1.052/1.052 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 1.052/1.052 CTRS Type: 3 1.052/1.052 Deterministic, Strongly deterministic 1.052/1.052 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 1.052/1.052 Right-stable CTRS, Not overlay CTRS 1.052/1.052 Not normal CTRS, Almost normal CTRS 1.052/1.052 Terminating CTRS, Operational terminating CTRS, Maybe joinable CCPs 1.052/1.052 Maybe level confluent 1.052/1.052 Maybe confluent 1.052/1.052 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 1.052/1.052 1.052/1.052 Prover9 CCP Convergence Checker Processor: 1.052/1.052 Proof: 1.052/1.052 ============================== Prover9 =============================== 1.052/1.052 Prover9 (64) version 2009-11A, November 2009. 1.052/1.052 Process 60354 was started by ubuntu on ubuntu, 1.052/1.052 Wed Mar 9 09:44:11 2022 1.052/1.052 The command was "./prover9 -t 60 -f /tmp/prover960079-30.in". 1.052/1.052 ============================== end of head =========================== 1.052/1.052 1.052/1.052 ============================== INPUT ================================= 1.052/1.052 1.052/1.052 % Reading from file /tmp/prover960079-30.in 1.052/1.052 1.052/1.052 1.052/1.052 formulas(sos). 1.052/1.052 reds(x,x). 1.052/1.052 red(x,y) & reds(y,z) -> reds(x,z). 1.052/1.052 red(x,y) -> red(f(x),f(y)). 1.052/1.052 red(x,y) -> red(g(x,z1),g(y,z1)). 1.052/1.052 red(x,y) -> red(g(z,x),g(z,y)). 1.052/1.052 red(x,y) -> red(s(x),s(y)). 1.052/1.052 red(x,y) -> red(h(x,z1),h(y,z1)). 1.052/1.052 red(x,y) -> red(h(z,x),h(z,y)). 1.052/1.052 red(x,y) -> red(pair(x,z1),pair(y,z1)). 1.052/1.052 red(x,y) -> red(pair(z,x),pair(z,y)). 1.052/1.052 red(x,y) -> red(t(x),t(y)). 1.052/1.052 red(a,c). 1.052/1.052 red(a,d). 1.052/1.052 red(b,c). 1.052/1.052 red(b,d). 1.052/1.052 red(c,e). 1.052/1.052 red(d,e). 1.052/1.052 (all x all y (reds(s(x),t(y)) -> red(f(x),pair(x,y)))). 1.052/1.052 (all x red(g(x,x),h(x,x))). 1.052/1.052 red(k,e). 1.052/1.052 red(l,e). 1.052/1.052 red(s(c),t(k)). 1.052/1.052 red(s(c),t(l)). 1.052/1.052 red(s(e),t(e)). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(goals). 1.052/1.052 (exists z (reds(c,z) & reds(d,z))). 1.052/1.052 end_of_list. 1.052/1.052 assign(max_megs,-1). 1.052/1.052 set(quiet). 1.052/1.052 1.052/1.052 ============================== end of input ========================== 1.052/1.052 1.052/1.052 % From the command line: assign(max_seconds, 60). 1.052/1.052 1.052/1.052 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 1.052/1.052 1.052/1.052 % Formulas that are not ordinary clauses: 1.052/1.052 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 1.052/1.052 2 red(x,y) -> red(f(x),f(y)) # label(non_clause). [assumption]. 1.052/1.052 3 red(x,y) -> red(g(x,z1),g(y,z1)) # label(non_clause). [assumption]. 1.052/1.052 4 red(x,y) -> red(g(z,x),g(z,y)) # label(non_clause). [assumption]. 1.052/1.052 5 red(x,y) -> red(s(x),s(y)) # label(non_clause). [assumption]. 1.052/1.052 6 red(x,y) -> red(h(x,z1),h(y,z1)) # label(non_clause). [assumption]. 1.052/1.052 7 red(x,y) -> red(h(z,x),h(z,y)) # label(non_clause). [assumption]. 1.052/1.052 8 red(x,y) -> red(pair(x,z1),pair(y,z1)) # label(non_clause). [assumption]. 1.052/1.052 9 red(x,y) -> red(pair(z,x),pair(z,y)) # label(non_clause). [assumption]. 1.052/1.052 10 red(x,y) -> red(t(x),t(y)) # label(non_clause). [assumption]. 1.052/1.052 11 (all x all y (reds(s(x),t(y)) -> red(f(x),pair(x,y)))) # label(non_clause). [assumption]. 1.052/1.052 12 (all x red(g(x,x),h(x,x))) # label(non_clause). [assumption]. 1.052/1.052 13 (exists z (reds(c,z) & reds(d,z))) # label(non_clause) # label(goal). [goal]. 1.052/1.052 1.052/1.052 ============================== end of process non-clausal formulas === 1.052/1.052 1.052/1.052 ============================== PROCESS INITIAL CLAUSES =============== 1.052/1.052 1.052/1.052 % Clauses before input processing: 1.052/1.052 1.052/1.052 formulas(usable). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(sos). 1.052/1.052 reds(x,x). [assumption]. 1.052/1.052 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 1.052/1.052 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 1.052/1.052 -red(x,y) | red(g(x,z),g(y,z)). [clausify(3)]. 1.052/1.052 -red(x,y) | red(g(z,x),g(z,y)). [clausify(4)]. 1.052/1.052 -red(x,y) | red(s(x),s(y)). [clausify(5)]. 1.052/1.052 -red(x,y) | red(h(x,z),h(y,z)). [clausify(6)]. 1.052/1.052 -red(x,y) | red(h(z,x),h(z,y)). [clausify(7)]. 1.052/1.052 -red(x,y) | red(pair(x,z),pair(y,z)). [clausify(8)]. 1.052/1.052 -red(x,y) | red(pair(z,x),pair(z,y)). [clausify(9)]. 1.052/1.052 -red(x,y) | red(t(x),t(y)). [clausify(10)]. 1.052/1.052 red(a,c). [assumption]. 1.052/1.052 red(a,d). [assumption]. 1.052/1.052 red(b,c). [assumption]. 1.052/1.052 red(b,d). [assumption]. 1.052/1.052 red(c,e). [assumption]. 1.052/1.052 red(d,e). [assumption]. 1.052/1.052 -reds(s(x),t(y)) | red(f(x),pair(x,y)). [clausify(11)]. 1.052/1.052 red(g(x,x),h(x,x)). [clausify(12)]. 1.052/1.052 red(k,e). [assumption]. 1.052/1.052 red(l,e). [assumption]. 1.052/1.052 red(s(c),t(k)). [assumption]. 1.052/1.052 red(s(c),t(l)). [assumption]. 1.052/1.052 red(s(e),t(e)). [assumption]. 1.052/1.052 -reds(c,x) | -reds(d,x). [deny(13)]. 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(demodulators). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 ============================== PREDICATE ELIMINATION ================= 1.052/1.052 1.052/1.052 ============================== end predicate elimination ============= 1.052/1.052 1.052/1.052 Auto_denials: (no changes). 1.052/1.052 1.052/1.052 Term ordering decisions: 1.052/1.052 1.052/1.052 kept: 14 reds(x,x). [assumption]. 1.052/1.052 kept: 15 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 1.052/1.052 kept: 16 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 1.052/1.052 kept: 17 -red(x,y) | red(g(x,z),g(y,z)). [clausify(3)]. 1.052/1.052 kept: 18 -red(x,y) | red(g(z,x),g(z,y)). [clausify(4)]. 1.052/1.052 kept: 19 -red(x,y) | red(s(x),s(y)). [clausify(5)]. 1.052/1.052 kept: 20 -red(x,y) | red(h(x,z),h(y,z)). [clausify(6)]. 1.052/1.052 kept: 21 -red(x,y) | red(h(z,x),h(z,y)). [clausify(7)]. 1.052/1.052 kept: 22 -red(x,y) | red(pair(x,z),pair(y,z)). [clausify(8)]. 1.052/1.052 kept: 23 -red(x,y) | red(pair(z,x),pair(z,y)). [clausify(9)]. 1.052/1.052 kept: 24 -red(x,y) | red(t(x),t(y)). [clausify(10)]. 1.052/1.052 kept: 25 red(a,c). [assumption]. 1.052/1.052 kept: 26 red(a,d). [assumption]. 1.052/1.052 kept: 27 red(b,c). [assumption]. 1.052/1.052 kept: 28 red(b,d). [assumption]. 1.052/1.052 kept: 29 red(c,e). [assumption]. 1.052/1.052 kept: 30 red(d,e). [assumption]. 1.052/1.052 kept: 31 -reds(s(x),t(y)) | red(f(x),pair(x,y)). [clausify(11)]. 1.052/1.052 kept: 32 red(g(x,x),h(x,x)). [clausify(12)]. 1.052/1.052 kept: 33 red(k,e). [assumption]. 1.052/1.052 kept: 34 red(l,e). [assumption]. 1.052/1.052 kept: 35 red(s(c),t(k)). [assumption]. 1.052/1.052 kept: 36 red(s(c),t(l)). [assumption]. 1.052/1.052 kept: 37 red(s(e),t(e)). [assumption]. 1.052/1.052 kept: 38 -reds(c,x) | -reds(d,x). [deny(13)]. 1.052/1.052 1.052/1.052 ============================== end of process initial clauses ======== 1.052/1.052 1.052/1.052 ============================== CLAUSES FOR SEARCH ==================== 1.052/1.052 1.052/1.052 % Clauses after input processing: 1.052/1.052 1.052/1.052 formulas(usable). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(sos). 1.052/1.052 14 reds(x,x). [assumption]. 1.052/1.052 15 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 1.052/1.052 16 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 1.052/1.052 17 -red(x,y) | red(g(x,z),g(y,z)). [clausify(3)]. 1.052/1.052 18 -red(x,y) | red(g(z,x),g(z,y)). [clausify(4)]. 1.052/1.052 19 -red(x,y) | red(s(x),s(y)). [clausify(5)]. 1.052/1.052 20 -red(x,y) | red(h(x,z),h(y,z)). [clausify(6)]. 1.052/1.052 21 -red(x,y) | red(h(z,x),h(z,y)). [clausify(7)]. 1.052/1.052 22 -red(x,y) | red(pair(x,z),pair(y,z)). [clausify(8)]. 1.052/1.052 23 -red(x,y) | red(pair(z,x),pair(z,y)). [clausify(9)]. 1.052/1.052 24 -red(x,y) | red(t(x),t(y)). [clausify(10)]. 1.052/1.052 25 red(a,c). [assumption]. 1.052/1.052 26 red(a,d). [assumption]. 1.052/1.052 27 red(b,c). [assumption]. 1.052/1.052 28 red(b,d). [assumption]. 1.052/1.052 29 red(c,e). [assumption]. 1.052/1.052 30 red(d,e). [assumption]. 1.052/1.052 31 -reds(s(x),t(y)) | red(f(x),pair(x,y)). [clausify(11)]. 1.052/1.052 32 red(g(x,x),h(x,x)). [clausify(12)]. 1.052/1.052 33 red(k,e). [assumption]. 1.052/1.052 34 red(l,e). [assumption]. 1.052/1.052 35 red(s(c),t(k)). [assumption]. 1.052/1.052 36 red(s(c),t(l)). [assumption]. 1.052/1.052 37 red(s(e),t(e)). [assumption]. 1.052/1.052 38 -reds(c,x) | -reds(d,x). [deny(13)]. 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(demodulators). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 ============================== end of clauses for search ============= 1.052/1.052 1.052/1.052 ============================== SEARCH ================================ 1.052/1.052 1.052/1.052 % Starting search at 0.01 seconds. 1.052/1.052 1.052/1.052 given #1 (I,wt=3): 14 reds(x,x). [assumption]. 1.052/1.052 1.052/1.052 given #2 (I,wt=9): 15 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 1.052/1.052 1.052/1.052 given #3 (I,wt=8): 16 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 1.052/1.052 1.052/1.052 given #4 (I,wt=10): 17 -red(x,y) | red(g(x,z),g(y,z)). [clausify(3)]. 1.052/1.052 1.052/1.052 given #5 (I,wt=10): 18 -red(x,y) | red(g(z,x),g(z,y)). [clausify(4)]. 1.052/1.052 1.052/1.052 given #6 (I,wt=8): 19 -red(x,y) | red(s(x),s(y)). [clausify(5)]. 1.052/1.052 1.052/1.052 given #7 (I,wt=10): 20 -red(x,y) | red(h(x,z),h(y,z)). [clausify(6)]. 1.052/1.052 1.052/1.052 given #8 (I,wt=10): 21 -red(x,y) | red(h(z,x),h(z,y)). [clausify(7)]. 1.052/1.052 1.052/1.052 given #9 (I,wt=10): 22 -red(x,y) | red(pair(x,z),pair(y,z)). [clausify(8)]. 1.052/1.052 1.052/1.052 given #10 (I,wt=10): 23 -red(x,y) | red(pair(z,x),pair(z,y)). [clausify(9)]. 1.052/1.052 1.052/1.052 given #11 (I,wt=8): 24 -red(x,y) | red(t(x),t(y)). [clausify(10)]. 1.052/1.052 1.052/1.052 given #12 (I,wt=3): 25 red(a,c). [assumption]. 1.052/1.052 1.052/1.052 given #13 (I,wt=3): 26 red(a,d). [assumption]. 1.052/1.052 1.052/1.052 given #14 (I,wt=3): 27 red(b,c). [assumption]. 1.052/1.052 1.052/1.052 given #15 (I,wt=3): 28 red(b,d). [assumption]. 1.052/1.052 1.052/1.052 given #16 (I,wt=3): 29 red(c,e). [assumption]. 1.052/1.052 1.052/1.052 given #17 (I,wt=3): 30 red(d,e). [assumption]. 1.052/1.052 1.052/1.052 given #18 (I,wt=11): 31 -reds(s(x),t(y)) | red(f(x),pair(x,y)). [clausify(11)]. 1.052/1.052 1.052/1.052 given #19 (I,wt=7): 32 red(g(x,x),h(x,x)). [clausify(12)]. 1.052/1.052 1.052/1.052 given #20 (I,wt=3): 33 red(k,e). [assumption]. 1.052/1.052 1.052/1.052 given #21 (I,wt=3): 34 red(l,e). [assumption]. 1.052/1.052 1.052/1.052 given #22 (I,wt=5): 35 red(s(c),t(k)). [assumption]. 1.052/1.052 1.052/1.052 given #23 (I,wt=5): 36 red(s(c),t(l)). [assumption]. 1.052/1.052 1.052/1.052 given #24 (I,wt=5): 37 red(s(e),t(e)). [assumption]. 1.052/1.052 1.052/1.052 given #25 (I,wt=6): 38 -reds(c,x) | -reds(d,x). [deny(13)]. 1.052/1.052 1.052/1.052 given #26 (A,wt=5): 39 red(t(a),t(c)). [ur(24,a,25,a)]. 1.052/1.052 1.052/1.052 given #27 (F,wt=3): 160 -reds(d,c). [resolve(38,a,14,a)]. 1.052/1.052 1.052/1.052 given #28 (F,wt=3): 162 -reds(c,d). [resolve(38,b,14,a)]. 1.052/1.052 1.052/1.052 given #29 (F,wt=3): 174 -red(d,c). [ur(15,b,14,a,c,160,a)]. 1.052/1.052 1.052/1.052 given #30 (F,wt=3): 175 -reds(e,c). [ur(15,a,30,a,c,160,a)]. 1.052/1.052 1.052/1.052 given #31 (T,wt=3): 48 reds(a,c). [ur(15,a,25,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #32 (T,wt=3): 58 reds(a,d). [ur(15,a,26,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #33 (T,wt=3): 68 reds(b,c). [ur(15,a,27,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #34 (T,wt=3): 78 reds(b,d). [ur(15,a,28,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #35 (A,wt=7): 40 red(pair(x,a),pair(x,c)). [ur(23,a,25,a)]. 1.052/1.052 1.052/1.052 given #36 (F,wt=3): 177 -red(c,d). [ur(15,b,14,a,c,162,a)]. 1.052/1.052 1.052/1.052 given #37 (F,wt=3): 178 -reds(e,d). [ur(15,a,29,a,c,162,a)]. 1.052/1.052 1.052/1.052 given #38 (F,wt=3): 180 -red(e,c). [ur(15,b,14,a,c,175,a)]. 1.052/1.052 1.052/1.052 given #39 (F,wt=3): 181 -red(e,a). [ur(15,b,48,a,c,175,a)]. 1.052/1.052 1.052/1.052 given #40 (T,wt=3): 88 reds(c,e). [ur(15,a,29,a,b,14,a)]. 1.052/1.052 1.052/1.052 ============================== PROOF ================================= 1.052/1.052 1.052/1.052 % Proof 1 at 0.01 (+ 0.00) seconds. 1.052/1.052 % Length of proof is 10. 1.052/1.052 % Level of proof is 3. 1.052/1.052 % Maximum clause weight is 9.000. 1.052/1.052 % Given clauses 40. 1.052/1.052 1.052/1.052 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 1.052/1.052 13 (exists z (reds(c,z) & reds(d,z))) # label(non_clause) # label(goal). [goal]. 1.052/1.052 14 reds(x,x). [assumption]. 1.052/1.052 15 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 1.052/1.052 29 red(c,e). [assumption]. 1.052/1.052 30 red(d,e). [assumption]. 1.052/1.052 38 -reds(c,x) | -reds(d,x). [deny(13)]. 1.052/1.052 88 reds(c,e). [ur(15,a,29,a,b,14,a)]. 1.052/1.052 98 reds(d,e). [ur(15,a,30,a,b,14,a)]. 1.052/1.052 199 $F. [resolve(88,a,38,a),unit_del(a,98)]. 1.052/1.052 1.052/1.052 ============================== end of proof ========================== 1.052/1.052 1.052/1.052 ============================== STATISTICS ============================ 1.052/1.052 1.052/1.052 Given=40. Generated=190. Kept=185. proofs=1. 1.052/1.052 Usable=40. Sos=145. Demods=0. Limbo=0, Disabled=25. Hints=0. 1.052/1.052 Kept_by_rule=0, Deleted_by_rule=0. 1.052/1.052 Forward_subsumed=4. Back_subsumed=0. 1.052/1.052 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 1.052/1.052 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 1.052/1.052 Demod_attempts=0. Demod_rewrites=0. 1.052/1.052 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 1.052/1.052 Nonunit_fsub_feature_tests=7. Nonunit_bsub_feature_tests=47. 1.052/1.052 Megabytes=0.29. 1.052/1.052 User_CPU=0.01, System_CPU=0.00, Wall_clock=0. 1.052/1.052 1.052/1.052 ============================== end of statistics ===================== 1.052/1.052 1.052/1.052 ============================== end of search ========================= 1.052/1.052 1.052/1.052 THEOREM PROVED 1.052/1.052 1.052/1.052 Exiting with 1 proof. 1.052/1.052 1.052/1.052 Process 60354 exit (max_proofs) Wed Mar 9 09:44:11 2022 1.052/1.052 1.052/1.052 1.052/1.052 The problem is joinable. 1.052/1.052 1.052/1.052 Problem 1.3: 1.052/1.052 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 1.052/1.052 Confluence Problem: 1.052/1.052 (VAR x y) 1.052/1.052 (REPLACEMENT-MAP 1.052/1.052 (a) 1.052/1.052 (b) 1.052/1.052 (c) 1.052/1.052 (d) 1.052/1.052 (f 1) 1.052/1.052 (g 1, 2) 1.052/1.052 (k) 1.052/1.052 (l) 1.052/1.052 (s 1) 1.052/1.052 (e) 1.052/1.052 (fSNonEmpty) 1.052/1.052 (h 1, 2) 1.052/1.052 (pair 1, 2) 1.052/1.052 (t 1) 1.052/1.052 ) 1.052/1.052 (RULES 1.052/1.052 a -> c 1.052/1.052 a -> d 1.052/1.052 b -> c 1.052/1.052 b -> d 1.052/1.052 c -> e 1.052/1.052 d -> e 1.052/1.052 f(x) -> pair(x,y) | s(x) ->* t(y) 1.052/1.052 g(x,x) -> h(x,x) 1.052/1.052 k -> e 1.052/1.052 l -> e 1.052/1.052 s(c) -> t(k) 1.052/1.052 s(c) -> t(l) 1.052/1.052 s(e) -> t(e) 1.052/1.052 ) 1.052/1.052 Critical Pairs: 1.052/1.052 => Not trivial, Not overlay, NW0, N3 1.052/1.052 Terminating:YES 1.052/1.052 1.052/1.052 -> Problem conclusions: 1.052/1.052 Not left linear, Not right linear, Not linear 1.052/1.052 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 1.052/1.052 CTRS Type: 3 1.052/1.052 Deterministic, Strongly deterministic 1.052/1.052 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 1.052/1.052 Right-stable CTRS, Not overlay CTRS 1.052/1.052 Not normal CTRS, Almost normal CTRS 1.052/1.052 Terminating CTRS, Operational terminating CTRS, Maybe joinable CCPs 1.052/1.052 Maybe level confluent 1.052/1.052 Maybe confluent 1.052/1.052 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 1.052/1.052 1.052/1.052 Prover9 CCP Convergence Checker Processor: 1.052/1.052 Proof: 1.052/1.052 ============================== Prover9 =============================== 1.052/1.052 Prover9 (64) version 2009-11A, November 2009. 1.052/1.052 Process 60358 was started by ubuntu on ubuntu, 1.052/1.052 Wed Mar 9 09:44:11 2022 1.052/1.052 The command was "./prover9 -t 60 -f /tmp/prover960079-32.in". 1.052/1.052 ============================== end of head =========================== 1.052/1.052 1.052/1.052 ============================== INPUT ================================= 1.052/1.052 1.052/1.052 % Reading from file /tmp/prover960079-32.in 1.052/1.052 1.052/1.052 1.052/1.052 formulas(sos). 1.052/1.052 reds(x,x). 1.052/1.052 red(x,y) & reds(y,z) -> reds(x,z). 1.052/1.052 red(x,y) -> red(f(x),f(y)). 1.052/1.052 red(x,y) -> red(g(x,z1),g(y,z1)). 1.052/1.052 red(x,y) -> red(g(z,x),g(z,y)). 1.052/1.052 red(x,y) -> red(s(x),s(y)). 1.052/1.052 red(x,y) -> red(h(x,z1),h(y,z1)). 1.052/1.052 red(x,y) -> red(h(z,x),h(z,y)). 1.052/1.052 red(x,y) -> red(pair(x,z1),pair(y,z1)). 1.052/1.052 red(x,y) -> red(pair(z,x),pair(z,y)). 1.052/1.052 red(x,y) -> red(t(x),t(y)). 1.052/1.052 red(a,c). 1.052/1.052 red(a,d). 1.052/1.052 red(b,c). 1.052/1.052 red(b,d). 1.052/1.052 red(c,e). 1.052/1.052 red(d,e). 1.052/1.052 (all x all y (reds(s(x),t(y)) -> red(f(x),pair(x,y)))). 1.052/1.052 (all x red(g(x,x),h(x,x))). 1.052/1.052 red(k,e). 1.052/1.052 red(l,e). 1.052/1.052 red(s(c),t(k)). 1.052/1.052 red(s(c),t(l)). 1.052/1.052 red(s(e),t(e)). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(goals). 1.052/1.052 (exists z (reds(s(e),z) & reds(t(k),z))). 1.052/1.052 end_of_list. 1.052/1.052 assign(max_megs,-1). 1.052/1.052 set(quiet). 1.052/1.052 1.052/1.052 ============================== end of input ========================== 1.052/1.052 1.052/1.052 % From the command line: assign(max_seconds, 60). 1.052/1.052 1.052/1.052 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 1.052/1.052 1.052/1.052 % Formulas that are not ordinary clauses: 1.052/1.052 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 1.052/1.052 2 red(x,y) -> red(f(x),f(y)) # label(non_clause). [assumption]. 1.052/1.052 3 red(x,y) -> red(g(x,z1),g(y,z1)) # label(non_clause). [assumption]. 1.052/1.052 4 red(x,y) -> red(g(z,x),g(z,y)) # label(non_clause). [assumption]. 1.052/1.052 5 red(x,y) -> red(s(x),s(y)) # label(non_clause). [assumption]. 1.052/1.052 6 red(x,y) -> red(h(x,z1),h(y,z1)) # label(non_clause). [assumption]. 1.052/1.052 7 red(x,y) -> red(h(z,x),h(z,y)) # label(non_clause). [assumption]. 1.052/1.052 8 red(x,y) -> red(pair(x,z1),pair(y,z1)) # label(non_clause). [assumption]. 1.052/1.052 9 red(x,y) -> red(pair(z,x),pair(z,y)) # label(non_clause). [assumption]. 1.052/1.052 10 red(x,y) -> red(t(x),t(y)) # label(non_clause). [assumption]. 1.052/1.052 11 (all x all y (reds(s(x),t(y)) -> red(f(x),pair(x,y)))) # label(non_clause). [assumption]. 1.052/1.052 12 (all x red(g(x,x),h(x,x))) # label(non_clause). [assumption]. 1.052/1.052 13 (exists z (reds(s(e),z) & reds(t(k),z))) # label(non_clause) # label(goal). [goal]. 1.052/1.052 1.052/1.052 ============================== end of process non-clausal formulas === 1.052/1.052 1.052/1.052 ============================== PROCESS INITIAL CLAUSES =============== 1.052/1.052 1.052/1.052 % Clauses before input processing: 1.052/1.052 1.052/1.052 formulas(usable). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(sos). 1.052/1.052 reds(x,x). [assumption]. 1.052/1.052 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 1.052/1.052 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 1.052/1.052 -red(x,y) | red(g(x,z),g(y,z)). [clausify(3)]. 1.052/1.052 -red(x,y) | red(g(z,x),g(z,y)). [clausify(4)]. 1.052/1.052 -red(x,y) | red(s(x),s(y)). [clausify(5)]. 1.052/1.052 -red(x,y) | red(h(x,z),h(y,z)). [clausify(6)]. 1.052/1.052 -red(x,y) | red(h(z,x),h(z,y)). [clausify(7)]. 1.052/1.052 -red(x,y) | red(pair(x,z),pair(y,z)). [clausify(8)]. 1.052/1.052 -red(x,y) | red(pair(z,x),pair(z,y)). [clausify(9)]. 1.052/1.052 -red(x,y) | red(t(x),t(y)). [clausify(10)]. 1.052/1.052 red(a,c). [assumption]. 1.052/1.052 red(a,d). [assumption]. 1.052/1.052 red(b,c). [assumption]. 1.052/1.052 red(b,d). [assumption]. 1.052/1.052 red(c,e). [assumption]. 1.052/1.052 red(d,e). [assumption]. 1.052/1.052 -reds(s(x),t(y)) | red(f(x),pair(x,y)). [clausify(11)]. 1.052/1.052 red(g(x,x),h(x,x)). [clausify(12)]. 1.052/1.052 red(k,e). [assumption]. 1.052/1.052 red(l,e). [assumption]. 1.052/1.052 red(s(c),t(k)). [assumption]. 1.052/1.052 red(s(c),t(l)). [assumption]. 1.052/1.052 red(s(e),t(e)). [assumption]. 1.052/1.052 -reds(s(e),x) | -reds(t(k),x). [deny(13)]. 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(demodulators). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 ============================== PREDICATE ELIMINATION ================= 1.052/1.052 1.052/1.052 ============================== end predicate elimination ============= 1.052/1.052 1.052/1.052 Auto_denials: (no changes). 1.052/1.052 1.052/1.052 Term ordering decisions: 1.052/1.052 1.052/1.052 kept: 14 reds(x,x). [assumption]. 1.052/1.052 kept: 15 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 1.052/1.052 kept: 16 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 1.052/1.052 kept: 17 -red(x,y) | red(g(x,z),g(y,z)). [clausify(3)]. 1.052/1.052 kept: 18 -red(x,y) | red(g(z,x),g(z,y)). [clausify(4)]. 1.052/1.052 kept: 19 -red(x,y) | red(s(x),s(y)). [clausify(5)]. 1.052/1.052 kept: 20 -red(x,y) | red(h(x,z),h(y,z)). [clausify(6)]. 1.052/1.052 kept: 21 -red(x,y) | red(h(z,x),h(z,y)). [clausify(7)]. 1.052/1.052 kept: 22 -red(x,y) | red(pair(x,z),pair(y,z)). [clausify(8)]. 1.052/1.052 kept: 23 -red(x,y) | red(pair(z,x),pair(z,y)). [clausify(9)]. 1.052/1.052 kept: 24 -red(x,y) | red(t(x),t(y)). [clausify(10)]. 1.052/1.052 kept: 25 red(a,c). [assumption]. 1.052/1.052 kept: 26 red(a,d). [assumption]. 1.052/1.052 kept: 27 red(b,c). [assumption]. 1.052/1.052 kept: 28 red(b,d). [assumption]. 1.052/1.052 kept: 29 red(c,e). [assumption]. 1.052/1.052 kept: 30 red(d,e). [assumption]. 1.052/1.052 kept: 31 -reds(s(x),t(y)) | red(f(x),pair(x,y)). [clausify(11)]. 1.052/1.052 kept: 32 red(g(x,x),h(x,x)). [clausify(12)]. 1.052/1.052 kept: 33 red(k,e). [assumption]. 1.052/1.052 kept: 34 red(l,e). [assumption]. 1.052/1.052 kept: 35 red(s(c),t(k)). [assumption]. 1.052/1.052 kept: 36 red(s(c),t(l)). [assumption]. 1.052/1.052 kept: 37 red(s(e),t(e)). [assumption]. 1.052/1.052 kept: 38 -reds(s(e),x) | -reds(t(k),x). [deny(13)]. 1.052/1.052 1.052/1.052 ============================== end of process initial clauses ======== 1.052/1.052 1.052/1.052 ============================== CLAUSES FOR SEARCH ==================== 1.052/1.052 1.052/1.052 % Clauses after input processing: 1.052/1.052 1.052/1.052 formulas(usable). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(sos). 1.052/1.052 14 reds(x,x). [assumption]. 1.052/1.052 15 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 1.052/1.052 16 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 1.052/1.052 17 -red(x,y) | red(g(x,z),g(y,z)). [clausify(3)]. 1.052/1.052 18 -red(x,y) | red(g(z,x),g(z,y)). [clausify(4)]. 1.052/1.052 19 -red(x,y) | red(s(x),s(y)). [clausify(5)]. 1.052/1.052 20 -red(x,y) | red(h(x,z),h(y,z)). [clausify(6)]. 1.052/1.052 21 -red(x,y) | red(h(z,x),h(z,y)). [clausify(7)]. 1.052/1.052 22 -red(x,y) | red(pair(x,z),pair(y,z)). [clausify(8)]. 1.052/1.052 23 -red(x,y) | red(pair(z,x),pair(z,y)). [clausify(9)]. 1.052/1.052 24 -red(x,y) | red(t(x),t(y)). [clausify(10)]. 1.052/1.052 25 red(a,c). [assumption]. 1.052/1.052 26 red(a,d). [assumption]. 1.052/1.052 27 red(b,c). [assumption]. 1.052/1.052 28 red(b,d). [assumption]. 1.052/1.052 29 red(c,e). [assumption]. 1.052/1.052 30 red(d,e). [assumption]. 1.052/1.052 31 -reds(s(x),t(y)) | red(f(x),pair(x,y)). [clausify(11)]. 1.052/1.052 32 red(g(x,x),h(x,x)). [clausify(12)]. 1.052/1.052 33 red(k,e). [assumption]. 1.052/1.052 34 red(l,e). [assumption]. 1.052/1.052 35 red(s(c),t(k)). [assumption]. 1.052/1.052 36 red(s(c),t(l)). [assumption]. 1.052/1.052 37 red(s(e),t(e)). [assumption]. 1.052/1.052 38 -reds(s(e),x) | -reds(t(k),x). [deny(13)]. 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(demodulators). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 ============================== end of clauses for search ============= 1.052/1.052 1.052/1.052 ============================== SEARCH ================================ 1.052/1.052 1.052/1.052 % Starting search at 0.00 seconds. 1.052/1.052 1.052/1.052 given #1 (I,wt=3): 14 reds(x,x). [assumption]. 1.052/1.052 1.052/1.052 given #2 (I,wt=9): 15 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 1.052/1.052 1.052/1.052 given #3 (I,wt=8): 16 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 1.052/1.052 1.052/1.052 given #4 (I,wt=10): 17 -red(x,y) | red(g(x,z),g(y,z)). [clausify(3)]. 1.052/1.052 1.052/1.052 given #5 (I,wt=10): 18 -red(x,y) | red(g(z,x),g(z,y)). [clausify(4)]. 1.052/1.052 1.052/1.052 given #6 (I,wt=8): 19 -red(x,y) | red(s(x),s(y)). [clausify(5)]. 1.052/1.052 1.052/1.052 given #7 (I,wt=10): 20 -red(x,y) | red(h(x,z),h(y,z)). [clausify(6)]. 1.052/1.052 1.052/1.052 given #8 (I,wt=10): 21 -red(x,y) | red(h(z,x),h(z,y)). [clausify(7)]. 1.052/1.052 1.052/1.052 given #9 (I,wt=10): 22 -red(x,y) | red(pair(x,z),pair(y,z)). [clausify(8)]. 1.052/1.052 1.052/1.052 given #10 (I,wt=10): 23 -red(x,y) | red(pair(z,x),pair(z,y)). [clausify(9)]. 1.052/1.052 1.052/1.052 given #11 (I,wt=8): 24 -red(x,y) | red(t(x),t(y)). [clausify(10)]. 1.052/1.052 1.052/1.052 given #12 (I,wt=3): 25 red(a,c). [assumption]. 1.052/1.052 1.052/1.052 given #13 (I,wt=3): 26 red(a,d). [assumption]. 1.052/1.052 1.052/1.052 given #14 (I,wt=3): 27 red(b,c). [assumption]. 1.052/1.052 1.052/1.052 given #15 (I,wt=3): 28 red(b,d). [assumption]. 1.052/1.052 1.052/1.052 given #16 (I,wt=3): 29 red(c,e). [assumption]. 1.052/1.052 1.052/1.052 given #17 (I,wt=3): 30 red(d,e). [assumption]. 1.052/1.052 1.052/1.052 given #18 (I,wt=11): 31 -reds(s(x),t(y)) | red(f(x),pair(x,y)). [clausify(11)]. 1.052/1.052 1.052/1.052 given #19 (I,wt=7): 32 red(g(x,x),h(x,x)). [clausify(12)]. 1.052/1.052 1.052/1.052 given #20 (I,wt=3): 33 red(k,e). [assumption]. 1.052/1.052 1.052/1.052 given #21 (I,wt=3): 34 red(l,e). [assumption]. 1.052/1.052 1.052/1.052 given #22 (I,wt=5): 35 red(s(c),t(k)). [assumption]. 1.052/1.052 1.052/1.052 given #23 (I,wt=5): 36 red(s(c),t(l)). [assumption]. 1.052/1.052 1.052/1.052 given #24 (I,wt=5): 37 red(s(e),t(e)). [assumption]. 1.052/1.052 1.052/1.052 given #25 (I,wt=8): 38 -reds(s(e),x) | -reds(t(k),x). [deny(13)]. 1.052/1.052 1.052/1.052 given #26 (A,wt=5): 39 red(t(a),t(c)). [ur(24,a,25,a)]. 1.052/1.052 1.052/1.052 given #27 (F,wt=5): 160 -reds(t(k),s(e)). [resolve(38,a,14,a)]. 1.052/1.052 1.052/1.052 given #28 (F,wt=5): 162 -reds(s(e),t(k)). [resolve(38,b,14,a)]. 1.052/1.052 1.052/1.052 given #29 (F,wt=5): 174 -red(t(k),s(e)). [ur(15,b,14,a,c,160,a)]. 1.052/1.052 1.052/1.052 given #30 (F,wt=5): 176 -red(s(e),t(k)). [ur(15,b,14,a,c,162,a)]. 1.052/1.052 1.052/1.052 given #31 (T,wt=3): 48 reds(a,c). [ur(15,a,25,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #32 (T,wt=3): 58 reds(a,d). [ur(15,a,26,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #33 (T,wt=3): 68 reds(b,c). [ur(15,a,27,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #34 (T,wt=3): 78 reds(b,d). [ur(15,a,28,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #35 (A,wt=7): 40 red(pair(x,a),pair(x,c)). [ur(23,a,25,a)]. 1.052/1.052 1.052/1.052 given #36 (F,wt=5): 177 -reds(t(e),t(k)). [ur(15,a,37,a,c,162,a)]. 1.052/1.052 1.052/1.052 given #37 (F,wt=5): 189 -red(t(e),t(k)). [ur(15,b,14,a,c,177,a)]. 1.052/1.052 1.052/1.052 given #38 (F,wt=3): 190 -red(e,k). [resolve(189,a,24,b)]. 1.052/1.052 1.052/1.052 given #39 (F,wt=8): 173 -red(t(k),x) | -reds(x,s(e)). [resolve(160,a,15,c)]. 1.052/1.052 1.052/1.052 given #40 (T,wt=3): 88 reds(c,e). [ur(15,a,29,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #41 (T,wt=3): 98 reds(d,e). [ur(15,a,30,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #42 (T,wt=3): 118 reds(k,e). [ur(15,a,33,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #43 (T,wt=3): 128 reds(l,e). [ur(15,a,34,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #44 (A,wt=7): 41 red(pair(a,x),pair(c,x)). [ur(22,a,25,a)]. 1.052/1.052 1.052/1.052 given #45 (F,wt=8): 175 -red(s(e),x) | -reds(x,t(k)). [resolve(162,a,15,c)]. 1.052/1.052 1.052/1.052 given #46 (F,wt=8): 188 -red(t(e),x) | -reds(x,t(k)). [resolve(177,a,15,c)]. 1.052/1.052 1.052/1.052 given #47 (F,wt=8): 191 -reds(t(x),s(e)) | -red(k,x). [resolve(173,a,24,b)]. 1.052/1.052 1.052/1.052 given #48 (F,wt=5): 210 -reds(t(e),s(e)). [resolve(191,b,33,a)]. 1.052/1.052 1.052/1.052 given #49 (T,wt=3): 193 reds(b,e). [ur(15,a,27,a,b,88,a)]. 1.052/1.052 1.052/1.052 given #50 (T,wt=3): 194 reds(a,e). [ur(15,a,25,a,b,88,a)]. 1.052/1.052 1.052/1.052 given #51 (T,wt=5): 44 red(s(a),s(c)). [ur(19,a,25,a)]. 1.052/1.052 1.052/1.052 given #52 (T,wt=5): 47 red(f(a),f(c)). [ur(16,a,25,a)]. 1.052/1.052 1.052/1.052 given #53 (A,wt=7): 42 red(h(x,a),h(x,c)). [ur(21,a,25,a)]. 1.052/1.052 1.052/1.052 given #54 (F,wt=5): 212 -red(t(e),s(e)). [ur(15,b,14,a,c,210,a)]. 1.052/1.052 1.052/1.052 given #55 (F,wt=8): 205 -reds(s(x),t(k)) | -red(e,x). [resolve(175,a,19,b)]. 1.052/1.052 1.052/1.052 given #56 (F,wt=8): 207 -reds(t(x),t(k)) | -red(e,x). [resolve(188,a,24,b)]. 1.052/1.052 1.052/1.052 given #57 (F,wt=8): 211 -red(t(e),x) | -reds(x,s(e)). [resolve(210,a,15,c)]. 1.052/1.052 1.052/1.052 given #58 (T,wt=5): 49 red(t(a),t(d)). [ur(24,a,26,a)]. 1.052/1.052 1.052/1.052 given #59 (T,wt=5): 54 red(s(a),s(d)). [ur(19,a,26,a)]. 1.052/1.052 1.052/1.052 given #60 (T,wt=5): 57 red(f(a),f(d)). [ur(16,a,26,a)]. 1.052/1.052 1.052/1.052 given #61 (T,wt=5): 59 red(t(b),t(c)). [ur(24,a,27,a)]. 1.052/1.052 1.052/1.052 given #62 (A,wt=7): 43 red(h(a,x),h(c,x)). [ur(20,a,25,a)]. 1.052/1.052 1.052/1.052 given #63 (F,wt=8): 245 -reds(t(x),s(e)) | -red(e,x). [resolve(211,a,24,b)]. 1.052/1.052 1.052/1.052 given #64 (F,wt=11): 159 -reds(t(k),x) | -red(s(e),y) | -reds(y,x). [resolve(38,a,15,c)]. 1.052/1.052 1.052/1.052 given #65 (F,wt=5): 313 -reds(t(k),t(e)). [ur(159,b,37,a,c,14,a)]. 1.052/1.052 1.052/1.052 ============================== PROOF ================================= 1.052/1.052 1.052/1.052 % Proof 1 at 0.01 (+ 0.00) seconds. 1.052/1.052 % Length of proof is 13. 1.052/1.052 % Level of proof is 4. 1.052/1.052 % Maximum clause weight is 11.000. 1.052/1.052 % Given clauses 65. 1.052/1.052 1.052/1.052 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 1.052/1.052 10 red(x,y) -> red(t(x),t(y)) # label(non_clause). [assumption]. 1.052/1.052 13 (exists z (reds(s(e),z) & reds(t(k),z))) # label(non_clause) # label(goal). [goal]. 1.052/1.052 14 reds(x,x). [assumption]. 1.052/1.052 15 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 1.052/1.052 24 -red(x,y) | red(t(x),t(y)). [clausify(10)]. 1.052/1.052 33 red(k,e). [assumption]. 1.052/1.052 37 red(s(e),t(e)). [assumption]. 1.052/1.052 38 -reds(s(e),x) | -reds(t(k),x). [deny(13)]. 1.052/1.052 109 red(t(k),t(e)). [ur(24,a,33,a)]. 1.052/1.052 159 -reds(t(k),x) | -red(s(e),y) | -reds(y,x). [resolve(38,a,15,c)]. 1.052/1.052 313 -reds(t(k),t(e)). [ur(159,b,37,a,c,14,a)]. 1.052/1.052 315 $F. [ur(15,b,14,a,c,313,a),unit_del(a,109)]. 1.052/1.052 1.052/1.052 ============================== end of proof ========================== 1.052/1.052 1.052/1.052 ============================== STATISTICS ============================ 1.052/1.052 1.052/1.052 Given=65. Generated=323. Kept=301. proofs=1. 1.052/1.052 Usable=65. Sos=235. Demods=0. Limbo=1, Disabled=25. Hints=0. 1.052/1.052 Kept_by_rule=0, Deleted_by_rule=0. 1.052/1.052 Forward_subsumed=21. Back_subsumed=0. 1.052/1.052 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 1.052/1.052 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 1.052/1.052 Demod_attempts=0. Demod_rewrites=0. 1.052/1.052 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 1.052/1.052 Nonunit_fsub_feature_tests=112. Nonunit_bsub_feature_tests=128. 1.052/1.052 Megabytes=0.45. 1.052/1.052 User_CPU=0.01, System_CPU=0.00, Wall_clock=0. 1.052/1.052 1.052/1.052 ============================== end of statistics ===================== 1.052/1.052 1.052/1.052 ============================== end of search ========================= 1.052/1.052 1.052/1.052 THEOREM PROVED 1.052/1.052 1.052/1.052 Exiting with 1 proof. 1.052/1.052 1.052/1.052 Process 60358 exit (max_proofs) Wed Mar 9 09:44:11 2022 1.052/1.052 1.052/1.052 1.052/1.052 The problem is joinable. 1.052/1.052 1.052/1.052 Problem 1.4: 1.052/1.052 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 1.052/1.052 Confluence Problem: 1.052/1.052 (VAR x y) 1.052/1.052 (REPLACEMENT-MAP 1.052/1.052 (a) 1.052/1.052 (b) 1.052/1.052 (c) 1.052/1.052 (d) 1.052/1.052 (f 1) 1.052/1.052 (g 1, 2) 1.052/1.052 (k) 1.052/1.052 (l) 1.052/1.052 (s 1) 1.052/1.052 (e) 1.052/1.052 (fSNonEmpty) 1.052/1.052 (h 1, 2) 1.052/1.052 (pair 1, 2) 1.052/1.052 (t 1) 1.052/1.052 ) 1.052/1.052 (RULES 1.052/1.052 a -> c 1.052/1.052 a -> d 1.052/1.052 b -> c 1.052/1.052 b -> d 1.052/1.052 c -> e 1.052/1.052 d -> e 1.052/1.052 f(x) -> pair(x,y) | s(x) ->* t(y) 1.052/1.052 g(x,x) -> h(x,x) 1.052/1.052 k -> e 1.052/1.052 l -> e 1.052/1.052 s(c) -> t(k) 1.052/1.052 s(c) -> t(l) 1.052/1.052 s(e) -> t(e) 1.052/1.052 ) 1.052/1.052 Critical Pairs: 1.052/1.052 => Not trivial, Overlay, NW0, N4 1.052/1.052 Terminating:YES 1.052/1.052 1.052/1.052 -> Problem conclusions: 1.052/1.052 Not left linear, Not right linear, Not linear 1.052/1.052 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 1.052/1.052 CTRS Type: 3 1.052/1.052 Deterministic, Strongly deterministic 1.052/1.052 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 1.052/1.052 Right-stable CTRS, Not overlay CTRS 1.052/1.052 Not normal CTRS, Almost normal CTRS 1.052/1.052 Terminating CTRS, Operational terminating CTRS, Maybe joinable CCPs 1.052/1.052 Maybe level confluent 1.052/1.052 Maybe confluent 1.052/1.052 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 1.052/1.052 1.052/1.052 Prover9 CCP Convergence Checker Processor: 1.052/1.052 Proof: 1.052/1.052 ============================== Prover9 =============================== 1.052/1.052 Prover9 (64) version 2009-11A, November 2009. 1.052/1.052 Process 60362 was started by ubuntu on ubuntu, 1.052/1.052 Wed Mar 9 09:44:11 2022 1.052/1.052 The command was "./prover9 -t 60 -f /tmp/prover960079-34.in". 1.052/1.052 ============================== end of head =========================== 1.052/1.052 1.052/1.052 ============================== INPUT ================================= 1.052/1.052 1.052/1.052 % Reading from file /tmp/prover960079-34.in 1.052/1.052 1.052/1.052 1.052/1.052 formulas(sos). 1.052/1.052 reds(x,x). 1.052/1.052 red(x,y) & reds(y,z) -> reds(x,z). 1.052/1.052 red(x,y) -> red(f(x),f(y)). 1.052/1.052 red(x,y) -> red(g(x,z1),g(y,z1)). 1.052/1.052 red(x,y) -> red(g(z,x),g(z,y)). 1.052/1.052 red(x,y) -> red(s(x),s(y)). 1.052/1.052 red(x,y) -> red(h(x,z1),h(y,z1)). 1.052/1.052 red(x,y) -> red(h(z,x),h(z,y)). 1.052/1.052 red(x,y) -> red(pair(x,z1),pair(y,z1)). 1.052/1.052 red(x,y) -> red(pair(z,x),pair(z,y)). 1.052/1.052 red(x,y) -> red(t(x),t(y)). 1.052/1.052 red(a,c). 1.052/1.052 red(a,d). 1.052/1.052 red(b,c). 1.052/1.052 red(b,d). 1.052/1.052 red(c,e). 1.052/1.052 red(d,e). 1.052/1.052 (all x all y (reds(s(x),t(y)) -> red(f(x),pair(x,y)))). 1.052/1.052 (all x red(g(x,x),h(x,x))). 1.052/1.052 red(k,e). 1.052/1.052 red(l,e). 1.052/1.052 red(s(c),t(k)). 1.052/1.052 red(s(c),t(l)). 1.052/1.052 red(s(e),t(e)). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(goals). 1.052/1.052 (exists z (reds(t(k),z) & reds(t(l),z))). 1.052/1.052 end_of_list. 1.052/1.052 assign(max_megs,-1). 1.052/1.052 set(quiet). 1.052/1.052 1.052/1.052 ============================== end of input ========================== 1.052/1.052 1.052/1.052 % From the command line: assign(max_seconds, 60). 1.052/1.052 1.052/1.052 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 1.052/1.052 1.052/1.052 % Formulas that are not ordinary clauses: 1.052/1.052 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 1.052/1.052 2 red(x,y) -> red(f(x),f(y)) # label(non_clause). [assumption]. 1.052/1.052 3 red(x,y) -> red(g(x,z1),g(y,z1)) # label(non_clause). [assumption]. 1.052/1.052 4 red(x,y) -> red(g(z,x),g(z,y)) # label(non_clause). [assumption]. 1.052/1.052 5 red(x,y) -> red(s(x),s(y)) # label(non_clause). [assumption]. 1.052/1.052 6 red(x,y) -> red(h(x,z1),h(y,z1)) # label(non_clause). [assumption]. 1.052/1.052 7 red(x,y) -> red(h(z,x),h(z,y)) # label(non_clause). [assumption]. 1.052/1.052 8 red(x,y) -> red(pair(x,z1),pair(y,z1)) # label(non_clause). [assumption]. 1.052/1.052 9 red(x,y) -> red(pair(z,x),pair(z,y)) # label(non_clause). [assumption]. 1.052/1.052 10 red(x,y) -> red(t(x),t(y)) # label(non_clause). [assumption]. 1.052/1.052 11 (all x all y (reds(s(x),t(y)) -> red(f(x),pair(x,y)))) # label(non_clause). [assumption]. 1.052/1.052 12 (all x red(g(x,x),h(x,x))) # label(non_clause). [assumption]. 1.052/1.052 13 (exists z (reds(t(k),z) & reds(t(l),z))) # label(non_clause) # label(goal). [goal]. 1.052/1.052 1.052/1.052 ============================== end of process non-clausal formulas === 1.052/1.052 1.052/1.052 ============================== PROCESS INITIAL CLAUSES =============== 1.052/1.052 1.052/1.052 % Clauses before input processing: 1.052/1.052 1.052/1.052 formulas(usable). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(sos). 1.052/1.052 reds(x,x). [assumption]. 1.052/1.052 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 1.052/1.052 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 1.052/1.052 -red(x,y) | red(g(x,z),g(y,z)). [clausify(3)]. 1.052/1.052 -red(x,y) | red(g(z,x),g(z,y)). [clausify(4)]. 1.052/1.052 -red(x,y) | red(s(x),s(y)). [clausify(5)]. 1.052/1.052 -red(x,y) | red(h(x,z),h(y,z)). [clausify(6)]. 1.052/1.052 -red(x,y) | red(h(z,x),h(z,y)). [clausify(7)]. 1.052/1.052 -red(x,y) | red(pair(x,z),pair(y,z)). [clausify(8)]. 1.052/1.052 -red(x,y) | red(pair(z,x),pair(z,y)). [clausify(9)]. 1.052/1.052 -red(x,y) | red(t(x),t(y)). [clausify(10)]. 1.052/1.052 red(a,c). [assumption]. 1.052/1.052 red(a,d). [assumption]. 1.052/1.052 red(b,c). [assumption]. 1.052/1.052 red(b,d). [assumption]. 1.052/1.052 red(c,e). [assumption]. 1.052/1.052 red(d,e). [assumption]. 1.052/1.052 -reds(s(x),t(y)) | red(f(x),pair(x,y)). [clausify(11)]. 1.052/1.052 red(g(x,x),h(x,x)). [clausify(12)]. 1.052/1.052 red(k,e). [assumption]. 1.052/1.052 red(l,e). [assumption]. 1.052/1.052 red(s(c),t(k)). [assumption]. 1.052/1.052 red(s(c),t(l)). [assumption]. 1.052/1.052 red(s(e),t(e)). [assumption]. 1.052/1.052 -reds(t(k),x) | -reds(t(l),x). [deny(13)]. 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(demodulators). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 ============================== PREDICATE ELIMINATION ================= 1.052/1.052 1.052/1.052 ============================== end predicate elimination ============= 1.052/1.052 1.052/1.052 Auto_denials: (no changes). 1.052/1.052 1.052/1.052 Term ordering decisions: 1.052/1.052 1.052/1.052 kept: 14 reds(x,x). [assumption]. 1.052/1.052 kept: 15 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 1.052/1.052 kept: 16 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 1.052/1.052 kept: 17 -red(x,y) | red(g(x,z),g(y,z)). [clausify(3)]. 1.052/1.052 kept: 18 -red(x,y) | red(g(z,x),g(z,y)). [clausify(4)]. 1.052/1.052 kept: 19 -red(x,y) | red(s(x),s(y)). [clausify(5)]. 1.052/1.052 kept: 20 -red(x,y) | red(h(x,z),h(y,z)). [clausify(6)]. 1.052/1.052 kept: 21 -red(x,y) | red(h(z,x),h(z,y)). [clausify(7)]. 1.052/1.052 kept: 22 -red(x,y) | red(pair(x,z),pair(y,z)). [clausify(8)]. 1.052/1.052 kept: 23 -red(x,y) | red(pair(z,x),pair(z,y)). [clausify(9)]. 1.052/1.052 kept: 24 -red(x,y) | red(t(x),t(y)). [clausify(10)]. 1.052/1.052 kept: 25 red(a,c). [assumption]. 1.052/1.052 kept: 26 red(a,d). [assumption]. 1.052/1.052 kept: 27 red(b,c). [assumption]. 1.052/1.052 kept: 28 red(b,d). [assumption]. 1.052/1.052 kept: 29 red(c,e). [assumption]. 1.052/1.052 kept: 30 red(d,e). [assumption]. 1.052/1.052 kept: 31 -reds(s(x),t(y)) | red(f(x),pair(x,y)). [clausify(11)]. 1.052/1.052 kept: 32 red(g(x,x),h(x,x)). [clausify(12)]. 1.052/1.052 kept: 33 red(k,e). [assumption]. 1.052/1.052 kept: 34 red(l,e). [assumption]. 1.052/1.052 kept: 35 red(s(c),t(k)). [assumption]. 1.052/1.052 kept: 36 red(s(c),t(l)). [assumption]. 1.052/1.052 kept: 37 red(s(e),t(e)). [assumption]. 1.052/1.052 kept: 38 -reds(t(k),x) | -reds(t(l),x). [deny(13)]. 1.052/1.052 1.052/1.052 ============================== end of process initial clauses ======== 1.052/1.052 1.052/1.052 ============================== CLAUSES FOR SEARCH ==================== 1.052/1.052 1.052/1.052 % Clauses after input processing: 1.052/1.052 1.052/1.052 formulas(usable). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(sos). 1.052/1.052 14 reds(x,x). [assumption]. 1.052/1.052 15 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 1.052/1.052 16 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 1.052/1.052 17 -red(x,y) | red(g(x,z),g(y,z)). [clausify(3)]. 1.052/1.052 18 -red(x,y) | red(g(z,x),g(z,y)). [clausify(4)]. 1.052/1.052 19 -red(x,y) | red(s(x),s(y)). [clausify(5)]. 1.052/1.052 20 -red(x,y) | red(h(x,z),h(y,z)). [clausify(6)]. 1.052/1.052 21 -red(x,y) | red(h(z,x),h(z,y)). [clausify(7)]. 1.052/1.052 22 -red(x,y) | red(pair(x,z),pair(y,z)). [clausify(8)]. 1.052/1.052 23 -red(x,y) | red(pair(z,x),pair(z,y)). [clausify(9)]. 1.052/1.052 24 -red(x,y) | red(t(x),t(y)). [clausify(10)]. 1.052/1.052 25 red(a,c). [assumption]. 1.052/1.052 26 red(a,d). [assumption]. 1.052/1.052 27 red(b,c). [assumption]. 1.052/1.052 28 red(b,d). [assumption]. 1.052/1.052 29 red(c,e). [assumption]. 1.052/1.052 30 red(d,e). [assumption]. 1.052/1.052 31 -reds(s(x),t(y)) | red(f(x),pair(x,y)). [clausify(11)]. 1.052/1.052 32 red(g(x,x),h(x,x)). [clausify(12)]. 1.052/1.052 33 red(k,e). [assumption]. 1.052/1.052 34 red(l,e). [assumption]. 1.052/1.052 35 red(s(c),t(k)). [assumption]. 1.052/1.052 36 red(s(c),t(l)). [assumption]. 1.052/1.052 37 red(s(e),t(e)). [assumption]. 1.052/1.052 38 -reds(t(k),x) | -reds(t(l),x). [deny(13)]. 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 formulas(demodulators). 1.052/1.052 end_of_list. 1.052/1.052 1.052/1.052 ============================== end of clauses for search ============= 1.052/1.052 1.052/1.052 ============================== SEARCH ================================ 1.052/1.052 1.052/1.052 % Starting search at 0.01 seconds. 1.052/1.052 1.052/1.052 given #1 (I,wt=3): 14 reds(x,x). [assumption]. 1.052/1.052 1.052/1.052 given #2 (I,wt=9): 15 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 1.052/1.052 1.052/1.052 given #3 (I,wt=8): 16 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 1.052/1.052 1.052/1.052 given #4 (I,wt=10): 17 -red(x,y) | red(g(x,z),g(y,z)). [clausify(3)]. 1.052/1.052 1.052/1.052 given #5 (I,wt=10): 18 -red(x,y) | red(g(z,x),g(z,y)). [clausify(4)]. 1.052/1.052 1.052/1.052 given #6 (I,wt=8): 19 -red(x,y) | red(s(x),s(y)). [clausify(5)]. 1.052/1.052 1.052/1.052 given #7 (I,wt=10): 20 -red(x,y) | red(h(x,z),h(y,z)). [clausify(6)]. 1.052/1.052 1.052/1.052 given #8 (I,wt=10): 21 -red(x,y) | red(h(z,x),h(z,y)). [clausify(7)]. 1.052/1.052 1.052/1.052 given #9 (I,wt=10): 22 -red(x,y) | red(pair(x,z),pair(y,z)). [clausify(8)]. 1.052/1.052 1.052/1.052 given #10 (I,wt=10): 23 -red(x,y) | red(pair(z,x),pair(z,y)). [clausify(9)]. 1.052/1.052 1.052/1.052 given #11 (I,wt=8): 24 -red(x,y) | red(t(x),t(y)). [clausify(10)]. 1.052/1.052 1.052/1.052 given #12 (I,wt=3): 25 red(a,c). [assumption]. 1.052/1.052 1.052/1.052 given #13 (I,wt=3): 26 red(a,d). [assumption]. 1.052/1.052 1.052/1.052 given #14 (I,wt=3): 27 red(b,c). [assumption]. 1.052/1.052 1.052/1.052 given #15 (I,wt=3): 28 red(b,d). [assumption]. 1.052/1.052 1.052/1.052 given #16 (I,wt=3): 29 red(c,e). [assumption]. 1.052/1.052 1.052/1.052 given #17 (I,wt=3): 30 red(d,e). [assumption]. 1.052/1.052 1.052/1.052 given #18 (I,wt=11): 31 -reds(s(x),t(y)) | red(f(x),pair(x,y)). [clausify(11)]. 1.052/1.052 1.052/1.052 given #19 (I,wt=7): 32 red(g(x,x),h(x,x)). [clausify(12)]. 1.052/1.052 1.052/1.052 given #20 (I,wt=3): 33 red(k,e). [assumption]. 1.052/1.052 1.052/1.052 given #21 (I,wt=3): 34 red(l,e). [assumption]. 1.052/1.052 1.052/1.052 given #22 (I,wt=5): 35 red(s(c),t(k)). [assumption]. 1.052/1.052 1.052/1.052 given #23 (I,wt=5): 36 red(s(c),t(l)). [assumption]. 1.052/1.052 1.052/1.052 given #24 (I,wt=5): 37 red(s(e),t(e)). [assumption]. 1.052/1.052 1.052/1.052 given #25 (I,wt=8): 38 -reds(t(k),x) | -reds(t(l),x). [deny(13)]. 1.052/1.052 1.052/1.052 given #26 (A,wt=5): 39 red(t(a),t(c)). [ur(24,a,25,a)]. 1.052/1.052 1.052/1.052 given #27 (F,wt=5): 160 -reds(t(l),t(k)). [resolve(38,a,14,a)]. 1.052/1.052 1.052/1.052 given #28 (F,wt=5): 162 -reds(t(k),t(l)). [resolve(38,b,14,a)]. 1.052/1.052 1.052/1.052 given #29 (F,wt=5): 174 -red(t(l),t(k)). [ur(15,b,14,a,c,160,a)]. 1.052/1.052 1.052/1.052 given #30 (F,wt=3): 177 -red(l,k). [resolve(174,a,24,b)]. 1.052/1.052 1.052/1.052 given #31 (T,wt=3): 48 reds(a,c). [ur(15,a,25,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #32 (T,wt=3): 58 reds(a,d). [ur(15,a,26,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #33 (T,wt=3): 68 reds(b,c). [ur(15,a,27,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #34 (T,wt=3): 78 reds(b,d). [ur(15,a,28,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #35 (A,wt=7): 40 red(pair(x,a),pair(x,c)). [ur(23,a,25,a)]. 1.052/1.052 1.052/1.052 given #36 (F,wt=5): 176 -red(t(k),t(l)). [ur(15,b,14,a,c,162,a)]. 1.052/1.052 1.052/1.052 given #37 (F,wt=3): 188 -red(k,l). [resolve(176,a,24,b)]. 1.052/1.052 1.052/1.052 given #38 (F,wt=8): 173 -red(t(l),x) | -reds(x,t(k)). [resolve(160,a,15,c)]. 1.052/1.052 1.052/1.052 given #39 (F,wt=8): 175 -red(t(k),x) | -reds(x,t(l)). [resolve(162,a,15,c)]. 1.052/1.052 1.052/1.052 given #40 (T,wt=3): 88 reds(c,e). [ur(15,a,29,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #41 (T,wt=3): 98 reds(d,e). [ur(15,a,30,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #42 (T,wt=3): 118 reds(k,e). [ur(15,a,33,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #43 (T,wt=3): 128 reds(l,e). [ur(15,a,34,a,b,14,a)]. 1.052/1.052 1.052/1.052 given #44 (A,wt=7): 41 red(pair(a,x),pair(c,x)). [ur(22,a,25,a)]. 1.052/1.052 1.052/1.052 given #45 (F,wt=8): 189 -reds(t(x),t(k)) | -red(l,x). [resolve(173,a,24,b)]. 1.052/1.052 1.052/1.052 given #46 (F,wt=5): 206 -reds(t(e),t(k)). [resolve(189,b,34,a)]. 1.052/1.052 1.052/1.052 given #47 (F,wt=5): 208 -red(t(e),t(k)). [ur(15,b,14,a,c,206,a)]. 1.052/1.052 1.052/1.052 given #48 (F,wt=3): 209 -red(e,k). [resolve(208,a,24,b)]. 1.052/1.052 1.052/1.052 given #49 (T,wt=3): 193 reds(b,e). [ur(15,a,27,a,b,88,a)]. 1.052/1.052 1.052/1.052 given #50 (T,wt=3): 194 reds(a,e). [ur(15,a,25,a,b,88,a)]. 1.052/1.052 1.052/1.052 given #51 (T,wt=5): 44 red(s(a),s(c)). [ur(19,a,25,a)]. 1.052/1.052 1.052/1.052 given #52 (T,wt=5): 47 red(f(a),f(c)). [ur(16,a,25,a)]. 1.052/1.052 1.052/1.052 given #53 (A,wt=7): 42 red(h(x,a),h(x,c)). [ur(21,a,25,a)]. 1.052/1.052 1.052/1.052 given #54 (F,wt=8): 191 -reds(t(x),t(l)) | -red(k,x). [resolve(175,a,24,b)]. 1.052/1.052 1.052/1.052 given #55 (F,wt=5): 241 -reds(t(e),t(l)). [resolve(191,b,33,a)]. 1.052/1.052 1.052/1.052 given #56 (F,wt=5): 243 -red(t(e),t(l)). [ur(15,b,14,a,c,241,a)]. 1.052/1.052 1.052/1.052 given #57 (F,wt=3): 244 -red(e,l). [resolve(243,a,24,b)]. 1.052/1.052 1.052/1.052 given #58 (T,wt=5): 49 red(t(a),t(d)). [ur(24,a,26,a)]. 1.052/1.052 1.052/1.052 given #59 (T,wt=5): 54 red(s(a),s(d)). [ur(19,a,26,a)]. 1.052/1.052 1.052/1.052 given #60 (T,wt=5): 57 red(f(a),f(d)). [ur(16,a,26,a)]. 1.052/1.052 1.052/1.052 given #61 (T,wt=5): 59 red(t(b),t(c)). [ur(24,a,27,a)]. 1.052/1.052 1.052/1.052 given #62 (A,wt=7): 43 red(h(a,x),h(c,x)). [ur(20,a,25,a)]. 1.052/1.052 1.052/1.052 given #63 (F,wt=8): 207 -red(t(e),x) | -reds(x,t(k)). [resolve(206,a,15,c)]. 1.052/1.052 1.052/1.052 given #64 (F,wt=8): 242 -red(t(e),x) | -reds(x,t(l)). [resolve(241,a,15,c)]. 1.052/1.052 1.052/1.052 given #65 (F,wt=8): 295 -reds(t(x),t(k)) | -red(e,x). [resolve(207,a,24,b)]. 1.052/1.052 1.052/1.052 given #66 (F,wt=8): 297 -reds(t(x),t(l)) | -red(e,x). [resolve(242,a,24,b)]. 1.052/1.052 1.052/1.052 given #67 (T,wt=5): 64 red(s(b),s(c)). [ur(19,a,27,a)]. 1.052/1.052 1.052/1.052 given #68 (T,wt=5): 67 red(f(b),f(c)). [ur(16,a,27,a)]. 1.052/1.052 1.052/1.052 given #69 (T,wt=5): 69 red(t(b),t(d)). [ur(24,a,28,a)]. 1.052/1.052 1.052/1.052 given #70 (T,wt=5): 74 red(s(b),s(d)). [ur(19,a,28,a)]. 1.052/1.052 1.052/1.052 given #71 (A,wt=7): 45 red(g(x,a),g(x,c)). [ur(18,a,25,a)]. 1.052/1.052 1.052/1.052 given #72 (F,wt=11): 159 -reds(t(l),x) | -red(t(k),y) | -reds(y,x). [resolve(38,a,15,c)]. 1.052/1.052 1.052/1.052 given #73 (F,wt=8): 353 -reds(t(l),e) | -red(t(k),a). [resolve(159,c,194,a)]. 1.052/1.052 1.052/1.052 given #74 (F,wt=8): 354 -reds(t(l),e) | -red(t(k),b). [resolve(159,c,193,a)]. 1.052/1.052 1.052/1.052 given #75 (F,wt=8): 355 -reds(t(l),e) | -red(t(k),l). [resolve(159,c,128,a)]. 1.052/1.052 1.052/1.052 given #76 (T,wt=5): 77 red(f(b),f(d)). [ur(16,a,28,a)]. 1.052/1.052 1.052/1.052 given #77 (T,wt=5): 79 red(t(c),t(e)). [ur(24,a,29,a)]. 1.052/1.052 1.052/1.052 given #78 (T,wt=5): 84 red(s(c),s(e)). [ur(19,a,29,a)]. 1.052/1.052 1.052/1.052 given #79 (T,wt=5): 87 red(f(c),f(e)). [ur(16,a,29,a)]. 1.052/1.052 1.052/1.052 given #80 (A,wt=7): 46 red(g(a,x),g(c,x)). [ur(17,a,25,a)]. 1.052/1.052 1.052/1.052 given #81 (F,wt=8): 356 -reds(t(l),e) | -red(t(k),k). [resolve(159,c,118,a)]. 1.052/1.052 1.052/1.052 given #82 (F,wt=8): 357 -reds(t(l),e) | -red(t(k),d). [resolve(159,c,98,a)]. 1.052/1.052 1.052/1.052 given #83 (F,wt=8): 358 -reds(t(l),e) | -red(t(k),c). [resolve(159,c,88,a)]. 1.052/1.052 1.052/1.052 given #84 (F,wt=8): 359 -reds(t(l),d) | -red(t(k),b). [resolve(159,c,78,a)]. 1.052/1.052 1.052/1.052 given #85 (T,wt=5): 89 red(t(d),t(e)). [ur(24,a,30,a)]. 1.052/1.052 1.052/1.052 given #86 (T,wt=5): 94 red(s(d),s(e)). [ur(19,a,30,a)]. 1.052/1.052 1.052/1.052 given #87 (T,wt=5): 97 red(f(d),f(e)). [ur(16,a,30,a)]. 1.052/1.052 1.052/1.052 given #88 (T,wt=5): 109 red(t(k),t(e)). [ur(24,a,33,a)]. 1.052/1.052 1.052/1.052 given #89 (A,wt=7): 50 red(pair(x,a),pair(x,d)). [ur(23,a,26,a)]. 1.052/1.052 1.052/1.052 given #90 (F,wt=5): 463 -reds(t(l),t(e)). [ur(159,b,109,a,c,14,a)]. 1.052/1.052 1.052/1.052 ============================== PROOF ================================= 1.052/1.052 1.052/1.052 % Proof 1 at 0.02 (+ 0.00) seconds. 1.052/1.052 % Length of proof is 14. 1.052/1.052 % Level of proof is 4. 1.052/1.052 % Maximum clause weight is 11.000. 1.052/1.052 % Given clauses 90. 1.052/1.052 1.052/1.052 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 1.052/1.052 10 red(x,y) -> red(t(x),t(y)) # label(non_clause). [assumption]. 1.052/1.052 13 (exists z (reds(t(k),z) & reds(t(l),z))) # label(non_clause) # label(goal). [goal]. 1.052/1.052 14 reds(x,x). [assumption]. 1.052/1.052 15 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 1.052/1.052 24 -red(x,y) | red(t(x),t(y)). [clausify(10)]. 1.052/1.052 33 red(k,e). [assumption]. 1.052/1.052 34 red(l,e). [assumption]. 1.052/1.052 38 -reds(t(k),x) | -reds(t(l),x). [deny(13)]. 1.052/1.052 109 red(t(k),t(e)). [ur(24,a,33,a)]. 1.052/1.052 119 red(t(l),t(e)). [ur(24,a,34,a)]. 1.052/1.052 159 -reds(t(l),x) | -red(t(k),y) | -reds(y,x). [resolve(38,a,15,c)]. 1.052/1.052 463 -reds(t(l),t(e)). [ur(159,b,109,a,c,14,a)]. 1.052/1.052 475 $F. [ur(15,b,14,a,c,463,a),unit_del(a,119)]. 1.052/1.052 1.052/1.052 ============================== end of proof ========================== 1.052/1.052 1.052/1.052 ============================== STATISTICS ============================ 1.052/1.052 1.052/1.052 Given=90. Generated=494. Kept=461. proofs=1. 1.052/1.052 Usable=90. Sos=370. Demods=0. Limbo=1, Disabled=25. Hints=0. 1.052/1.052 Kept_by_rule=0, Deleted_by_rule=0. 1.052/1.052 Forward_subsumed=32. Back_subsumed=0. 1.052/1.052 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 1.052/1.052 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 1.052/1.052 Demod_attempts=0. Demod_rewrites=0. 1.052/1.052 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 1.052/1.052 Nonunit_fsub_feature_tests=203. Nonunit_bsub_feature_tests=140. 1.052/1.052 Megabytes=0.61. 1.052/1.052 User_CPU=0.02, System_CPU=0.00, Wall_clock=0. 1.052/1.052 1.052/1.052 ============================== end of statistics ===================== 1.052/1.052 1.052/1.052 ============================== end of search ========================= 1.052/1.052 1.052/1.052 THEOREM PROVED 1.052/1.052 1.052/1.052 Exiting with 1 proof. 1.052/1.052 1.052/1.052 Process 60362 exit (max_proofs) Wed Mar 9 09:44:11 2022 1.052/1.052 1.052/1.052 1.052/1.052 The problem is joinable. 1.052/1.052 0.46user 0.09system 0:01.52elapsed 36%CPU (0avgtext+0avgdata 24656maxresident)k 1.052/1.052 8inputs+0outputs (0major+25881minor)pagefaults 0swaps