5.087/5.087 YES 5.087/5.087 5.087/5.087 Problem 1: 5.087/5.087 5.087/5.087 5.087/5.087 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.087/5.087 Confluence Problem: 5.087/5.087 (VAR vNonEmpty:S x:S y:S) 5.087/5.087 (STRATEGY CONTEXTSENSITIVE 5.087/5.087 (a) 5.087/5.087 (b) 5.087/5.087 (c) 5.087/5.087 (d) 5.087/5.087 (f 1) 5.087/5.087 (g 1 2) 5.087/5.087 (k) 5.087/5.087 (l) 5.087/5.087 (s 1) 5.087/5.087 (e) 5.087/5.087 (fSNonEmpty) 5.087/5.087 (h 1 2) 5.087/5.087 (pair 1 2) 5.087/5.087 (t 1) 5.087/5.087 ) 5.087/5.087 (RULES 5.087/5.087 a -> c 5.087/5.087 a -> d 5.087/5.087 b -> c 5.087/5.087 b -> d 5.087/5.087 c -> e 5.087/5.087 d -> e 5.087/5.087 f(x:S) -> pair(x:S,y:S) | s(x:S) ->* t(y:S) 5.087/5.087 g(x:S,x:S) -> h(x:S,x:S) 5.087/5.087 k -> e 5.087/5.087 l -> e 5.087/5.087 s(c) -> t(k) 5.087/5.087 s(c) -> t(l) 5.087/5.087 s(e) -> t(e) 5.087/5.087 ) 5.087/5.087 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.087/5.087 5.087/5.087 5.087/5.087 Problem 1: 5.087/5.087 5.087/5.087 Inlining of Conditions Processor [STERN17]: 5.087/5.087 5.087/5.087 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.087/5.087 Confluence Problem: 5.087/5.087 (VAR vNonEmpty:S x:S y:S) 5.087/5.087 (STRATEGY CONTEXTSENSITIVE 5.087/5.087 (a) 5.087/5.087 (b) 5.087/5.087 (c) 5.087/5.087 (d) 5.087/5.087 (f 1) 5.087/5.087 (g 1 2) 5.087/5.087 (k) 5.087/5.087 (l) 5.087/5.087 (s 1) 5.087/5.087 (e) 5.087/5.087 (fSNonEmpty) 5.087/5.087 (h 1 2) 5.087/5.087 (pair 1 2) 5.087/5.087 (t 1) 5.087/5.087 ) 5.087/5.087 (RULES 5.087/5.087 a -> c 5.087/5.087 a -> d 5.087/5.087 b -> c 5.087/5.087 b -> d 5.087/5.087 c -> e 5.087/5.087 d -> e 5.087/5.087 f(x:S) -> pair(x:S,y:S) | s(x:S) ->* t(y:S) 5.087/5.087 g(x:S,x:S) -> h(x:S,x:S) 5.087/5.087 k -> e 5.087/5.087 l -> e 5.087/5.087 s(c) -> t(k) 5.087/5.087 s(c) -> t(l) 5.087/5.087 s(e) -> t(e) 5.087/5.087 ) 5.087/5.087 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.087/5.087 5.087/5.087 5.087/5.087 Problem 1: 5.087/5.087 5.087/5.087 Clean CTRS Processor: 5.087/5.087 5.087/5.087 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.087/5.087 Confluence Problem: 5.087/5.087 (VAR x:S y:S) 5.087/5.087 (STRATEGY CONTEXTSENSITIVE 5.087/5.087 (a) 5.087/5.087 (b) 5.087/5.087 (c) 5.087/5.087 (d) 5.087/5.087 (f 1) 5.087/5.087 (g 1 2) 5.087/5.087 (k) 5.087/5.087 (l) 5.087/5.087 (s 1) 5.087/5.087 (e) 5.087/5.087 (fSNonEmpty) 5.087/5.087 (h 1 2) 5.087/5.087 (pair 1 2) 5.087/5.087 (t 1) 5.087/5.087 ) 5.087/5.087 (RULES 5.087/5.087 a -> c 5.087/5.087 a -> d 5.087/5.087 b -> c 5.087/5.087 b -> d 5.087/5.087 c -> e 5.087/5.087 d -> e 5.087/5.087 f(x:S) -> pair(x:S,y:S) | s(x:S) ->* t(y:S) 5.087/5.087 g(x:S,x:S) -> h(x:S,x:S) 5.087/5.087 k -> e 5.087/5.087 l -> e 5.087/5.087 s(c) -> t(k) 5.087/5.087 s(c) -> t(l) 5.087/5.087 s(e) -> t(e) 5.087/5.087 ) 5.087/5.087 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.087/5.087 5.087/5.087 CRule InfChecker Info: 5.087/5.087 a -> c 5.087/5.087 Rule remains 5.087/5.087 Proof: 5.087/5.087 NO_CONDS 5.087/5.087 5.087/5.087 CRule InfChecker Info: 5.087/5.087 a -> d 5.087/5.087 Rule remains 5.087/5.087 Proof: 5.087/5.087 NO_CONDS 5.087/5.087 5.087/5.087 CRule InfChecker Info: 5.087/5.087 b -> c 5.087/5.087 Rule remains 5.087/5.087 Proof: 5.087/5.087 NO_CONDS 5.087/5.087 5.087/5.087 CRule InfChecker Info: 5.087/5.087 b -> d 5.087/5.087 Rule remains 5.087/5.087 Proof: 5.087/5.087 NO_CONDS 5.087/5.087 5.087/5.087 CRule InfChecker Info: 5.087/5.087 c -> e 5.087/5.087 Rule remains 5.087/5.087 Proof: 5.087/5.087 NO_CONDS 5.087/5.087 5.087/5.087 CRule InfChecker Info: 5.087/5.087 d -> e 5.087/5.087 Rule remains 5.087/5.087 Proof: 5.087/5.087 NO_CONDS 5.087/5.087 5.087/5.087 CRule InfChecker Info: 5.087/5.087 f(x:S) -> pair(x:S,y:S) | s(x:S) ->* t(y:S) 5.087/5.087 Rule remains 5.087/5.087 Proof: 5.087/5.087 NO 5.087/5.087 5.087/5.087 Problem 1: 5.087/5.087 5.087/5.087 Infeasibility Problem: 5.087/5.087 [(VAR vNonEmpty:S vNonEmpty:S:S x:S:S y:S:S) 5.087/5.087 (STRATEGY CONTEXTSENSITIVE 5.087/5.087 (a) 5.087/5.087 (b) 5.087/5.087 (c) 5.087/5.087 (d) 5.087/5.087 (f 1) 5.087/5.087 (g 1 2) 5.087/5.087 (k) 5.087/5.087 (l) 5.087/5.087 (s 1) 5.087/5.087 (e) 5.087/5.087 (fSNonEmpty) 5.087/5.087 (h 1 2) 5.087/5.087 (pair 1 2) 5.087/5.087 (t 1) 5.087/5.087 ) 5.087/5.087 (RULES 5.087/5.087 a -> c 5.087/5.087 a -> d 5.087/5.087 b -> c 5.087/5.087 b -> d 5.087/5.087 c -> e 5.087/5.087 d -> e 5.087/5.087 f(x:S:S) -> pair(x:S:S,y:S:S) | s(x:S:S) ->* t(y:S:S) 5.087/5.087 g(x:S:S,x:S:S) -> h(x:S:S,x:S:S) 5.087/5.087 k -> e 5.087/5.087 l -> e 5.087/5.087 s(c) -> t(k) 5.087/5.087 s(c) -> t(l) 5.087/5.087 s(e) -> t(e) 5.087/5.087 )] 5.087/5.087 5.087/5.087 Infeasibility Conditions: 5.087/5.087 s(x:S:S) ->* t(y:S:S) 5.087/5.087 5.087/5.087 Problem 1: 5.087/5.087 5.087/5.087 Obtaining a proof using Prover9: 5.087/5.087 5.087/5.087 -> Prover9 Output: 5.087/5.087 ============================== Prover9 =============================== 5.087/5.087 Prover9 (64) version 2009-11A, November 2009. 5.087/5.087 Process 109873 was started by ubuntu on ubuntu, 5.087/5.087 Fri Jul 16 15:06:05 2021 5.087/5.087 The command was "./prover9 -f /tmp/prover9109866-0.in". 5.087/5.087 ============================== end of head =========================== 5.087/5.087 5.087/5.087 ============================== INPUT ================================= 5.087/5.087 5.087/5.087 % Reading from file /tmp/prover9109866-0.in 5.087/5.087 5.087/5.087 assign(max_seconds,20). 5.087/5.087 5.087/5.087 formulas(assumptions). 5.087/5.087 ->*_s0(x,x) # label(reflexivity). 5.087/5.087 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 5.087/5.087 ->_s0(x1,y) -> ->_s0(f(x1),f(y)) # label(congruence). 5.087/5.087 ->_s0(x1,y) -> ->_s0(g(x1,x2),g(y,x2)) # label(congruence). 5.087/5.087 ->_s0(x2,y) -> ->_s0(g(x1,x2),g(x1,y)) # label(congruence). 5.087/5.087 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence). 5.087/5.087 ->_s0(x1,y) -> ->_s0(h(x1,x2),h(y,x2)) # label(congruence). 5.087/5.087 ->_s0(x2,y) -> ->_s0(h(x1,x2),h(x1,y)) # label(congruence). 5.087/5.087 ->_s0(x1,y) -> ->_s0(pair(x1,x2),pair(y,x2)) # label(congruence). 5.087/5.087 ->_s0(x2,y) -> ->_s0(pair(x1,x2),pair(x1,y)) # label(congruence). 5.087/5.087 ->_s0(x1,y) -> ->_s0(t(x1),t(y)) # label(congruence). 5.087/5.087 ->_s0(a,c) # label(replacement). 5.087/5.087 ->_s0(a,d) # label(replacement). 5.087/5.087 ->_s0(b,c) # label(replacement). 5.087/5.087 ->_s0(b,d) # label(replacement). 5.087/5.087 ->_s0(c,e) # label(replacement). 5.087/5.087 ->_s0(d,e) # label(replacement). 5.087/5.087 ->*_s0(s(x2),t(x3)) -> ->_s0(f(x2),pair(x2,x3)) # label(replacement). 5.087/5.087 ->_s0(g(x2,x2),h(x2,x2)) # label(replacement). 5.087/5.087 ->_s0(k,e) # label(replacement). 5.087/5.087 ->_s0(l,e) # label(replacement). 5.087/5.087 ->_s0(s(c),t(k)) # label(replacement). 5.087/5.087 ->_s0(s(c),t(l)) # label(replacement). 5.087/5.087 ->_s0(s(e),t(e)) # label(replacement). 5.087/5.087 end_of_list. 5.087/5.087 5.087/5.087 formulas(goals). 5.087/5.087 (exists x2 exists x3 ->*_s0(s(x2),t(x3))) # label(goal). 5.087/5.087 end_of_list. 5.087/5.087 5.087/5.087 ============================== end of input ========================== 5.087/5.087 5.087/5.087 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 5.087/5.087 5.087/5.087 % Formulas that are not ordinary clauses: 5.087/5.087 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 5.087/5.087 2 ->_s0(x1,y) -> ->_s0(f(x1),f(y)) # label(congruence) # label(non_clause). [assumption]. 5.087/5.087 3 ->_s0(x1,y) -> ->_s0(g(x1,x2),g(y,x2)) # label(congruence) # label(non_clause). [assumption]. 5.087/5.087 4 ->_s0(x2,y) -> ->_s0(g(x1,x2),g(x1,y)) # label(congruence) # label(non_clause). [assumption]. 5.087/5.087 5 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 5.087/5.087 6 ->_s0(x1,y) -> ->_s0(h(x1,x2),h(y,x2)) # label(congruence) # label(non_clause). [assumption]. 5.087/5.087 7 ->_s0(x2,y) -> ->_s0(h(x1,x2),h(x1,y)) # label(congruence) # label(non_clause). [assumption]. 5.087/5.087 8 ->_s0(x1,y) -> ->_s0(pair(x1,x2),pair(y,x2)) # label(congruence) # label(non_clause). [assumption]. 5.087/5.087 9 ->_s0(x2,y) -> ->_s0(pair(x1,x2),pair(x1,y)) # label(congruence) # label(non_clause). [assumption]. 5.087/5.087 10 ->_s0(x1,y) -> ->_s0(t(x1),t(y)) # label(congruence) # label(non_clause). [assumption]. 5.087/5.087 11 ->*_s0(s(x2),t(x3)) -> ->_s0(f(x2),pair(x2,x3)) # label(replacement) # label(non_clause). [assumption]. 5.087/5.087 12 (exists x2 exists x3 ->*_s0(s(x2),t(x3))) # label(goal) # label(non_clause) # label(goal). [goal]. 5.087/5.087 5.087/5.087 ============================== end of process non-clausal formulas === 5.087/5.087 5.087/5.087 ============================== PROCESS INITIAL CLAUSES =============== 5.087/5.087 5.087/5.087 % Clauses before input processing: 5.087/5.087 5.087/5.087 formulas(usable). 5.087/5.087 end_of_list. 5.087/5.087 5.087/5.087 formulas(sos). 5.087/5.087 ->*_s0(x,x) # label(reflexivity). [assumption]. 5.087/5.087 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 5.087/5.087 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(2)]. 5.087/5.087 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence). [clausify(3)]. 5.087/5.087 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence). [clausify(4)]. 5.087/5.087 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(5)]. 5.087/5.087 -->_s0(x,y) | ->_s0(h(x,z),h(y,z)) # label(congruence). [clausify(6)]. 5.087/5.087 -->_s0(x,y) | ->_s0(h(z,x),h(z,y)) # label(congruence). [clausify(7)]. 5.087/5.087 -->_s0(x,y) | ->_s0(pair(x,z),pair(y,z)) # label(congruence). [clausify(8)]. 5.087/5.087 -->_s0(x,y) | ->_s0(pair(z,x),pair(z,y)) # label(congruence). [clausify(9)]. 5.087/5.087 -->_s0(x,y) | ->_s0(t(x),t(y)) # label(congruence). [clausify(10)]. 5.087/5.087 ->_s0(a,c) # label(replacement). [assumption]. 5.087/5.087 ->_s0(a,d) # label(replacement). [assumption]. 5.087/5.087 ->_s0(b,c) # label(replacement). [assumption]. 5.087/5.087 ->_s0(b,d) # label(replacement). [assumption]. 5.087/5.087 ->_s0(c,e) # label(replacement). [assumption]. 5.087/5.087 ->_s0(d,e) # label(replacement). [assumption]. 5.087/5.087 -->*_s0(s(x),t(y)) | ->_s0(f(x),pair(x,y)) # label(replacement). [clausify(11)]. 5.087/5.087 ->_s0(g(x,x),h(x,x)) # label(replacement). [assumption]. 5.087/5.087 ->_s0(k,e) # label(replacement). [assumption]. 5.087/5.087 ->_s0(l,e) # label(replacement). [assumption]. 5.087/5.087 ->_s0(s(c),t(k)) # label(replacement). [assumption]. 5.087/5.087 ->_s0(s(c),t(l)) # label(replacement). [assumption]. 5.087/5.087 ->_s0(s(e),t(e)) # label(replacement). [assumption]. 5.087/5.087 -->*_s0(s(x),t(y)) # label(goal). [deny(12)]. 5.087/5.087 end_of_list. 5.087/5.087 5.087/5.087 formulas(demodulators). 5.087/5.087 end_of_list. 5.087/5.087 5.087/5.087 ============================== PREDICATE ELIMINATION ================= 5.087/5.087 5.087/5.087 No predicates eliminated. 5.087/5.087 5.087/5.087 ============================== end predicate elimination ============= 5.087/5.087 5.087/5.087 Auto_denials: 5.087/5.087 % copying label goal to answer in negative clause 5.087/5.087 5.087/5.087 Term ordering decisions: 5.087/5.087 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 5.087/5.087 Function symbol precedence: function_order([ e, c, d, a, b, k, l, h, pair, g, s, t, f ]). 5.087/5.087 After inverse_order: (no changes). 5.087/5.087 Unfolding symbols: (none). 5.087/5.087 5.087/5.087 Auto_inference settings: 5.087/5.087 % set(neg_binary_resolution). % (HNE depth_diff=-9) 5.087/5.087 % clear(ordered_res). % (HNE depth_diff=-9) 5.087/5.087 % set(ur_resolution). % (HNE depth_diff=-9) 5.087/5.087 % set(ur_resolution) -> set(pos_ur_resolution). 5.087/5.087 % set(ur_resolution) -> set(neg_ur_resolution). 5.087/5.087 5.087/5.087 Auto_process settings: (no changes). 5.087/5.087 5.087/5.087 kept: 13 ->*_s0(x,x) # label(reflexivity). [assumption]. 5.087/5.087 kept: 14 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 5.087/5.087 kept: 15 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(2)]. 5.087/5.087 kept: 16 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence). [clausify(3)]. 5.087/5.087 kept: 17 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence). [clausify(4)]. 5.087/5.087 kept: 18 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(5)]. 5.087/5.087 kept: 19 -->_s0(x,y) | ->_s0(h(x,z),h(y,z)) # label(congruence). [clausify(6)]. 5.087/5.087 kept: 20 -->_s0(x,y) | ->_s0(h(z,x),h(z,y)) # label(congruence). [clausify(7)]. 5.087/5.087 kept: 21 -->_s0(x,y) | ->_s0(pair(x,z),pair(y,z)) # label(congruence). [clausify(8)]. 5.087/5.087 kept: 22 -->_s0(x,y) | ->_s0(pair(z,x),pair(z,y)) # label(congruence). [clausify(9)]. 5.087/5.087 kept: 23 -->_s0(x,y) | ->_s0(t(x),t(y)) # label(congruence). [clausify(10)]. 5.087/5.087 kept: 24 ->_s0(a,c) # label(replacement). [assumption]. 5.087/5.087 kept: 25 ->_s0(a,d) # label(replacement). [assumption]. 5.087/5.087 kept: 26 ->_s0(b,c) # label(replacement). [assumption]. 5.087/5.087 kept: 27 ->_s0(b,d) # label(replacement). [assumption]. 5.087/5.087 kept: 28 ->_s0(c,e) # label(replacement). [assumption]. 5.087/5.087 kept: 29 ->_s0(d,e) # label(replacement). [assumption]. 5.087/5.087 kept: 30 -->*_s0(s(x),t(y)) | ->_s0(f(x),pair(x,y)) # label(replacement). [clausify(11)]. 5.087/5.087 kept: 31 ->_s0(g(x,x),h(x,x)) # label(replacement). [assumption]. 5.087/5.087 kept: 32 ->_s0(k,e) # label(replacement). [assumption]. 5.087/5.087 kept: 33 ->_s0(l,e) # label(replacement). [assumption]. 5.087/5.087 kept: 34 ->_s0(s(c),t(k)) # label(replacement). [assumption]. 5.087/5.087 kept: 35 ->_s0(s(c),t(l)) # label(replacement). [assumption]. 5.087/5.087 kept: 36 ->_s0(s(e),t(e)) # label(replacement). [assumption]. 5.087/5.087 kept: 37 -->*_s0(s(x),t(y)) # label(goal) # answer(goal). [deny(12)]. 5.087/5.087 5.087/5.087 ============================== end of process initial clauses ======== 5.087/5.087 5.087/5.087 ============================== CLAUSES FOR SEARCH ==================== 5.087/5.087 5.087/5.087 % Clauses after input processing: 5.087/5.087 5.087/5.087 formulas(usable). 5.087/5.087 end_of_list. 5.087/5.087 5.087/5.087 formulas(sos). 5.087/5.087 13 ->*_s0(x,x) # label(reflexivity). [assumption]. 5.087/5.087 14 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 5.087/5.087 15 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(2)]. 5.087/5.087 16 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence). [clausify(3)]. 5.087/5.087 17 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence). [clausify(4)]. 5.087/5.087 18 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(5)]. 5.087/5.087 19 -->_s0(x,y) | ->_s0(h(x,z),h(y,z)) # label(congruence). [clausify(6)]. 5.087/5.087 20 -->_s0(x,y) | ->_s0(h(z,x),h(z,y)) # label(congruence). [clausify(7)]. 5.087/5.087 21 -->_s0(x,y) | ->_s0(pair(x,z),pair(y,z)) # label(congruence). [clausify(8)]. 5.087/5.087 22 -->_s0(x,y) | ->_s0(pair(z,x),pair(z,y)) # label(congruence). [clausify(9)]. 5.087/5.087 23 -->_s0(x,y) | ->_s0(t(x),t(y)) # label(congruence). [clausify(10)]. 5.087/5.087 24 ->_s0(a,c) # label(replacement). [assumption]. 5.087/5.087 25 ->_s0(a,d) # label(replacement). [assumption]. 5.087/5.087 26 ->_s0(b,c) # label(replacement). [assumption]. 5.087/5.087 27 ->_s0(b,d) # label(replacement). [assumption]. 5.087/5.087 28 ->_s0(c,e) # label(replacement). [assumption]. 5.087/5.087 29 ->_s0(d,e) # label(replacement). [assumption]. 5.087/5.087 31 ->_s0(g(x,x),h(x,x)) # label(replacement). [assumption]. 5.087/5.087 32 ->_s0(k,e) # label(replacement). [assumption]. 5.087/5.087 33 ->_s0(l,e) # label(replacement). [assumption]. 5.087/5.087 34 ->_s0(s(c),t(k)) # label(replacement). [assumption]. 5.087/5.087 35 ->_s0(s(c),t(l)) # label(replacement). [assumption]. 5.087/5.087 36 ->_s0(s(e),t(e)) # label(replacement). [assumption]. 5.087/5.087 37 -->*_s0(s(x),t(y)) # label(goal) # answer(goal). [deny(12)]. 5.087/5.087 end_of_list. 5.087/5.087 5.087/5.087 formulas(demodulators). 5.087/5.087 end_of_list. 5.087/5.087 5.087/5.087 ============================== end of clauses for search ============= 5.087/5.087 5.087/5.087 ============================== SEARCH ================================ 5.087/5.087 5.087/5.087 % Starting search at 0.00 seconds. 5.087/5.087 5.087/5.087 given #1 (I,wt=3): 13 ->*_s0(x,x) # label(reflexivity). [assumption]. 5.087/5.087 5.087/5.087 given #2 (I,wt=9): 14 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 5.087/5.087 5.087/5.087 given #3 (I,wt=8): 15 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(2)]. 5.087/5.087 5.087/5.087 given #4 (I,wt=10): 16 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence). [clausify(3)]. 5.087/5.087 5.087/5.087 given #5 (I,wt=10): 17 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence). [clausify(4)]. 5.087/5.087 5.087/5.087 given #6 (I,wt=8): 18 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(5)]. 5.087/5.087 5.087/5.087 given #7 (I,wt=10): 19 -->_s0(x,y) | ->_s0(h(x,z),h(y,z)) # label(congruence). [clausify(6)]. 5.087/5.087 5.087/5.087 given #8 (I,wt=10): 20 -->_s0(x,y) | ->_s0(h(z,x),h(z,y)) # label(congruence). [clausify(7)]. 5.087/5.087 5.087/5.087 given #9 (I,wt=10): 21 -->_s0(x,y) | ->_s0(pair(x,z),pair(y,z)) # label(congruence). [clausify(8)]. 5.087/5.087 5.087/5.087 given #10 (I,wt=10): 22 -->_s0(x,y) | ->_s0(pair(z,x),pair(z,y)) # label(congruence). [clausify(9)]. 5.087/5.087 5.087/5.087 given #11 (I,wt=8): 23 -->_s0(x,y) | ->_s0(t(x),t(y)) # label(congruence). [clausify(10)]. 5.087/5.087 5.087/5.087 given #12 (I,wt=3): 24 ->_s0(a,c) # label(replacement). [assumption]. 5.087/5.087 5.087/5.087 given #13 (I,wt=3): 25 ->_s0(a,d) # label(replacement). [assumption]. 5.087/5.087 5.087/5.087 given #14 (I,wt=3): 26 ->_s0(b,c) # label(replacement). [assumption]. 5.087/5.087 5.087/5.087 given #15 (I,wt=3): 27 ->_s0(b,d) # label(replacement). [assumption]. 5.087/5.087 5.087/5.087 given #16 (I,wt=3): 28 ->_s0(c,e) # label(replacement). [assumption]. 5.087/5.087 5.087/5.087 given #17 (I,wt=3): 29 ->_s0(d,e) # label(replacement). [assumption]. 5.087/5.087 5.087/5.087 given #18 (I,wt=7): 31 ->_s0(g(x,x),h(x,x)) # label(replacement). [assumption]. 5.087/5.087 5.087/5.087 given #19 (I,wt=3): 32 ->_s0(k,e) # label(replacement). [assumption]. 5.087/5.087 5.087/5.087 given #20 (I,wt=3): 33 ->_s0(l,e) # label(replacement). [assumption]. 5.087/5.087 5.087/5.087 given #21 (I,wt=5): 34 ->_s0(s(c),t(k)) # label(replacement). [assumption]. 5.087/5.087 5.087/5.087 ============================== PROOF ================================= 5.087/5.087 5.087/5.087 % Proof 1 at 0.00 (+ 0.00) seconds: goal. 5.087/5.087 % Length of proof is 8. 5.087/5.087 % Level of proof is 3. 5.087/5.087 % Maximum clause weight is 9.000. 5.087/5.087 % Given clauses 21. 5.087/5.087 5.087/5.087 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 5.087/5.087 12 (exists x2 exists x3 ->*_s0(s(x2),t(x3))) # label(goal) # label(non_clause) # label(goal). [goal]. 5.087/5.087 13 ->*_s0(x,x) # label(reflexivity). [assumption]. 5.087/5.087 14 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 5.087/5.087 34 ->_s0(s(c),t(k)) # label(replacement). [assumption]. 5.087/5.087 37 -->*_s0(s(x),t(y)) # label(goal) # answer(goal). [deny(12)]. 5.087/5.087 137 ->*_s0(s(c),t(k)). [ur(14,a,34,a,b,13,a)]. 5.087/5.087 138 $F # answer(goal). [resolve(137,a,37,a)]. 5.087/5.087 5.087/5.087 ============================== end of proof ========================== 5.087/5.087 5.087/5.087 ============================== STATISTICS ============================ 5.087/5.087 5.087/5.087 Given=21. Generated=125. Kept=125. proofs=1. 5.087/5.087 Usable=21. Sos=93. Demods=0. Limbo=9, Disabled=26. Hints=0. 5.087/5.087 Kept_by_rule=0, Deleted_by_rule=0. 5.087/5.087 Forward_subsumed=0. Back_subsumed=1. 5.087/5.087 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 5.087/5.087 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 5.087/5.087 Demod_attempts=0. Demod_rewrites=0. 5.087/5.087 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 5.087/5.087 Nonunit_fsub_feature_tests=3. Nonunit_bsub_feature_tests=19. 5.087/5.087 Megabytes=0.20. 5.087/5.087 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 5.087/5.087 5.087/5.087 ============================== end of statistics ===================== 5.087/5.087 5.087/5.087 ============================== end of search ========================= 5.087/5.087 5.087/5.087 THEOREM PROVED 5.087/5.087 5.087/5.087 Exiting with 1 proof. 5.087/5.087 5.087/5.087 Process 109873 exit (max_proofs) Fri Jul 16 15:06:05 2021 5.087/5.087 5.087/5.087 5.087/5.087 The problem is feasible. 5.087/5.087 5.087/5.087 5.087/5.087 CRule InfChecker Info: 5.087/5.087 g(x:S,x:S) -> h(x:S,x:S) 5.087/5.087 Rule remains 5.087/5.087 Proof: 5.087/5.087 NO_CONDS 5.087/5.087 5.087/5.087 CRule InfChecker Info: 5.087/5.087 k -> e 5.087/5.087 Rule remains 5.087/5.087 Proof: 5.087/5.087 NO_CONDS 5.087/5.087 5.087/5.087 CRule InfChecker Info: 5.087/5.087 l -> e 5.087/5.087 Rule remains 5.087/5.087 Proof: 5.087/5.087 NO_CONDS 5.087/5.087 5.087/5.087 CRule InfChecker Info: 5.087/5.087 s(c) -> t(k) 5.087/5.087 Rule remains 5.087/5.087 Proof: 5.087/5.087 NO_CONDS 5.087/5.087 5.087/5.087 CRule InfChecker Info: 5.087/5.087 s(c) -> t(l) 5.087/5.087 Rule remains 5.087/5.087 Proof: 5.087/5.087 NO_CONDS 5.087/5.087 5.087/5.087 CRule InfChecker Info: 5.087/5.087 s(e) -> t(e) 5.087/5.087 Rule remains 5.087/5.087 Proof: 5.087/5.087 NO_CONDS 5.087/5.087 5.087/5.087 Problem 1: 5.087/5.087 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.087/5.087 Confluence Problem: 5.087/5.087 (VAR x:S y:S) 5.087/5.087 (STRATEGY CONTEXTSENSITIVE 5.087/5.087 (a) 5.087/5.087 (b) 5.087/5.087 (c) 5.087/5.087 (d) 5.087/5.087 (f 1) 5.087/5.087 (g 1 2) 5.087/5.087 (k) 5.087/5.087 (l) 5.087/5.087 (s 1) 5.087/5.087 (e) 5.087/5.087 (fSNonEmpty) 5.087/5.087 (h 1 2) 5.087/5.087 (pair 1 2) 5.087/5.087 (t 1) 5.087/5.087 ) 5.087/5.087 (RULES 5.087/5.087 a -> c 5.087/5.087 a -> d 5.087/5.087 b -> c 5.087/5.087 b -> d 5.087/5.087 c -> e 5.087/5.087 d -> e 5.087/5.087 f(x:S) -> pair(x:S,y:S) | s(x:S) ->* t(y:S) 5.087/5.087 g(x:S,x:S) -> h(x:S,x:S) 5.087/5.087 k -> e 5.087/5.087 l -> e 5.087/5.087 s(c) -> t(k) 5.087/5.087 s(c) -> t(l) 5.087/5.087 s(e) -> t(e) 5.087/5.087 ) 5.087/5.087 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.087/5.087 5.087/5.087 Critical Pairs Processor: 5.087/5.087 -> Rules: 5.087/5.087 a -> c 5.087/5.087 a -> d 5.087/5.087 b -> c 5.087/5.087 b -> d 5.087/5.087 c -> e 5.087/5.087 d -> e 5.087/5.087 f(x:S) -> pair(x:S,y:S) | s(x:S) ->* t(y:S) 5.087/5.087 g(x:S,x:S) -> h(x:S,x:S) 5.087/5.087 k -> e 5.087/5.087 l -> e 5.087/5.087 s(c) -> t(k) 5.087/5.087 s(c) -> t(l) 5.087/5.087 s(e) -> t(e) 5.087/5.087 -> Vars: 5.087/5.087 "x", "y", "x" 5.087/5.087 -> FVars: 5.087/5.087 "x3", "x4", "x5" 5.087/5.087 -> PVars: 5.087/5.087 "x": ["x3", "x5"], "y": ["x4"] 5.087/5.087 5.087/5.087 -> Rlps: 5.087/5.087 crule: a -> c, id: 1, possubterms: a-> [] 5.087/5.087 crule: a -> d, id: 2, possubterms: a-> [] 5.087/5.087 crule: b -> c, id: 3, possubterms: b-> [] 5.087/5.087 crule: b -> d, id: 4, possubterms: b-> [] 5.087/5.087 crule: c -> e, id: 5, possubterms: c-> [] 5.087/5.087 crule: d -> e, id: 6, possubterms: d-> [] 5.087/5.087 crule: f(x3:S) -> pair(x3:S,x4:S) | s(x3:S) ->* t(x4:S), id: 7, possubterms: f(x3:S)-> [] 5.087/5.087 crule: g(x5:S,x5:S) -> h(x5:S,x5:S), id: 8, possubterms: g(x5:S,x5:S)-> [] 5.087/5.087 crule: k -> e, id: 9, possubterms: k-> [] 5.087/5.087 crule: l -> e, id: 10, possubterms: l-> [] 5.087/5.087 crule: s(c) -> t(k), id: 11, possubterms: s(c)-> [], c-> [1] 5.087/5.087 crule: s(c) -> t(l), id: 12, possubterms: s(c)-> [], c-> [1] 5.087/5.087 crule: s(e) -> t(e), id: 13, possubterms: s(e)-> [], e-> [1] 5.087/5.087 5.087/5.087 -> Unifications: 5.087/5.087 R2 unifies with R1 at p: [], l: a, lp: a, conds: {}, sig: {}, l': a, r: d, r': c 5.087/5.087 R4 unifies with R3 at p: [], l: b, lp: b, conds: {}, sig: {}, l': b, r: d, r': c 5.087/5.087 R11 unifies with R5 at p: [1], l: s(c), lp: c, conds: {}, sig: {}, l': c, r: t(k), r': e 5.087/5.087 R12 unifies with R11 at p: [], l: s(c), lp: s(c), conds: {}, sig: {}, l': s(c), r: t(l), r': t(k) 5.087/5.087 R12 unifies with R5 at p: [1], l: s(c), lp: c, conds: {}, sig: {}, l': c, r: t(l), r': e 5.087/5.087 5.087/5.087 -> Critical pairs info: 5.087/5.087 => Not trivial, Not overlay, N1 5.087/5.087 => Not trivial, Overlay, N2 5.087/5.087 => Not trivial, Not overlay, N3 5.087/5.087 => Not trivial, Overlay, N4 5.087/5.087 5.087/5.087 -> Problem conclusions: 5.087/5.087 Not left linear, Not right linear, Not linear 5.087/5.087 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 5.087/5.087 CTRS Type: 3 5.087/5.087 Deterministic, Strongly deterministic 5.087/5.087 Oriented CTRS, Properly oriented CTRS, Not join CTRS 5.087/5.087 Maybe right-stable CTRS, Not overlay CTRS 5.087/5.087 Maybe normal CTRS, Maybe almost normal CTRS 5.087/5.087 Maybe terminating CTRS, Maybe joinable CCPs 5.087/5.087 Maybe level confluent 5.087/5.087 Maybe confluent 5.087/5.087 5.087/5.087 Problem 1: 5.087/5.087 Clean Infeasible CCPs Processor: 5.087/5.087 Num of CPIs: 4 5.087/5.087 Timeout: 30 5.087/5.087 Timeout for each infeasibility problem: 30 s 5.087/5.087 => Not trivial, Not overlay, N1 5.087/5.087 5.087/5.087 Proof: 5.087/5.087 NO_CONDS 5.087/5.087 5.087/5.087 5.087/5.087 5.087/5.087 => Not trivial, Overlay, N2 5.087/5.087 5.087/5.087 Proof: 5.087/5.087 NO_CONDS 5.087/5.087 5.087/5.087 5.087/5.087 5.087/5.087 => Not trivial, Not overlay, N3 5.087/5.087 5.087/5.087 Proof: 5.087/5.087 NO_CONDS 5.087/5.087 5.087/5.087 5.087/5.087 5.087/5.087 => Not trivial, Overlay, N4 5.087/5.087 5.087/5.087 Proof: 5.087/5.087 NO_CONDS 5.087/5.087 5.087/5.087 5.087/5.087 5.087/5.087 -> Problem conclusions: 5.087/5.087 Not left linear, Not right linear, Not linear 5.087/5.087 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 5.087/5.087 CTRS Type: 3 5.087/5.087 Deterministic, Strongly deterministic 5.087/5.087 Oriented CTRS, Properly oriented CTRS, Not join CTRS 5.087/5.087 Maybe right-stable CTRS, Not overlay CTRS 5.087/5.087 Maybe normal CTRS, Maybe almost normal CTRS 5.087/5.087 Maybe terminating CTRS, Maybe joinable CCPs 5.087/5.087 Maybe level confluent 5.087/5.087 Maybe confluent 5.087/5.087 5.087/5.087 Resulting CCPs: 5.087/5.087 => Not trivial, Not overlay, N1 5.087/5.087 => Not trivial, Overlay, N2 5.087/5.087 => Not trivial, Not overlay, N3 5.087/5.087 => Not trivial, Overlay, N4 5.087/5.087 5.087/5.087 Problem 1: 5.087/5.087 Operation Termination Processor: 5.087/5.087 Operational terminating? 5.087/5.087 YES 5.087/5.087 5.087/5.087 Problem 1: 5.087/5.087 5.087/5.087 (VAR vu95NonEmpty:S xu58S:S yu58S:S) 5.087/5.087 (RULES 5.087/5.087 a -> c 5.087/5.087 a -> d 5.087/5.087 b -> c 5.087/5.087 b -> d 5.087/5.087 c -> e 5.087/5.087 d -> e 5.087/5.087 f(xu58S:S) -> pair(xu58S:S,yu58S:S) | s(xu58S:S) ->* t(yu58S:S) 5.087/5.087 g(xu58S:S,xu58S:S) -> h(xu58S:S,xu58S:S) 5.087/5.087 k -> e 5.087/5.087 l -> e 5.087/5.087 s(c) -> t(k) 5.087/5.087 s(c) -> t(l) 5.087/5.087 s(e) -> t(e) 5.087/5.087 ) 5.087/5.087 5.087/5.087 Problem 1: 5.087/5.087 Valid CTRS Processor: 5.087/5.087 -> Rules: 5.087/5.087 a -> c 5.087/5.087 a -> d 5.087/5.087 b -> c 5.087/5.087 b -> d 5.087/5.087 c -> e 5.087/5.087 d -> e 5.087/5.087 f(xu58S:S) -> pair(xu58S:S,yu58S:S) | s(xu58S:S) ->* t(yu58S:S) 5.087/5.087 g(xu58S:S,xu58S:S) -> h(xu58S:S,xu58S:S) 5.087/5.087 k -> e 5.087/5.087 l -> e 5.087/5.087 s(c) -> t(k) 5.087/5.087 s(c) -> t(l) 5.087/5.087 s(e) -> t(e) 5.087/5.087 -> The system is a deterministic 3-CTRS. 5.087/5.087 5.087/5.087 Problem 1: 5.087/5.087 5.087/5.087 2D Dependency Pair Processor: 5.087/5.087 5.087/5.087 Conditional Termination Problem 1: 5.087/5.087 -> Pairs: 5.087/5.087 A -> C 5.087/5.087 A -> D 5.087/5.087 B -> C 5.087/5.087 B -> D 5.087/5.087 S(c) -> K 5.087/5.087 S(c) -> L 5.087/5.087 -> QPairs: 5.087/5.087 Empty 5.087/5.087 -> Rules: 5.087/5.087 a -> c 5.087/5.087 a -> d 5.087/5.087 b -> c 5.087/5.087 b -> d 5.087/5.087 c -> e 5.087/5.087 d -> e 5.087/5.087 f(xu58S:S) -> pair(xu58S:S,yu58S:S) | s(xu58S:S) ->* t(yu58S:S) 5.087/5.087 g(xu58S:S,xu58S:S) -> h(xu58S:S,xu58S:S) 5.087/5.087 k -> e 5.087/5.087 l -> e 5.087/5.087 s(c) -> t(k) 5.087/5.087 s(c) -> t(l) 5.087/5.087 s(e) -> t(e) 5.087/5.087 5.087/5.087 Conditional Termination Problem 2: 5.087/5.087 -> Pairs: 5.087/5.087 F(xu58S:S) -> S(xu58S:S) 5.087/5.087 -> QPairs: 5.087/5.087 S(c) -> K 5.087/5.087 S(c) -> L 5.087/5.087 -> Rules: 5.087/5.087 a -> c 5.087/5.087 a -> d 5.087/5.087 b -> c 5.087/5.087 b -> d 5.087/5.087 c -> e 5.087/5.087 d -> e 5.087/5.087 f(xu58S:S) -> pair(xu58S:S,yu58S:S) | s(xu58S:S) ->* t(yu58S:S) 5.087/5.087 g(xu58S:S,xu58S:S) -> h(xu58S:S,xu58S:S) 5.087/5.087 k -> e 5.087/5.087 l -> e 5.087/5.087 s(c) -> t(k) 5.087/5.087 s(c) -> t(l) 5.087/5.087 s(e) -> t(e) 5.087/5.087 5.087/5.087 5.087/5.087 The problem is decomposed in 2 subproblems. 5.087/5.087 5.087/5.087 Problem 1.1: 5.087/5.087 5.087/5.087 SCC Processor: 5.087/5.087 -> Pairs: 5.087/5.087 A -> C 5.087/5.087 A -> D 5.087/5.087 B -> C 5.087/5.087 B -> D 5.087/5.087 S(c) -> K 5.087/5.087 S(c) -> L 5.087/5.087 -> QPairs: 5.087/5.087 Empty 5.087/5.087 -> Rules: 5.087/5.087 a -> c 5.087/5.087 a -> d 5.087/5.087 b -> c 5.087/5.087 b -> d 5.087/5.087 c -> e 5.087/5.087 d -> e 5.087/5.087 f(xu58S:S) -> pair(xu58S:S,yu58S:S) | s(xu58S:S) ->* t(yu58S:S) 5.087/5.087 g(xu58S:S,xu58S:S) -> h(xu58S:S,xu58S:S) 5.087/5.087 k -> e 5.087/5.087 l -> e 5.087/5.087 s(c) -> t(k) 5.087/5.087 s(c) -> t(l) 5.087/5.087 s(e) -> t(e) 5.087/5.087 ->Strongly Connected Components: 5.087/5.087 There is no strongly connected component 5.087/5.087 5.087/5.087 The problem is finite. 5.087/5.087 5.087/5.087 Problem 1.2: 5.087/5.087 5.087/5.087 SCC Processor: 5.087/5.087 -> Pairs: 5.087/5.087 F(xu58S:S) -> S(xu58S:S) 5.087/5.087 -> QPairs: 5.087/5.087 S(c) -> K 5.087/5.087 S(c) -> L 5.087/5.087 -> Rules: 5.087/5.087 a -> c 5.087/5.087 a -> d 5.087/5.087 b -> c 5.087/5.087 b -> d 5.087/5.087 c -> e 5.087/5.087 d -> e 5.087/5.087 f(xu58S:S) -> pair(xu58S:S,yu58S:S) | s(xu58S:S) ->* t(yu58S:S) 5.087/5.087 g(xu58S:S,xu58S:S) -> h(xu58S:S,xu58S:S) 5.087/5.087 k -> e 5.087/5.087 l -> e 5.087/5.087 s(c) -> t(k) 5.087/5.087 s(c) -> t(l) 5.087/5.087 s(e) -> t(e) 5.087/5.087 ->Strongly Connected Components: 5.087/5.087 There is no strongly connected component 5.087/5.087 5.087/5.087 The problem is finite. 5.087/5.087 5.087/5.087 5.087/5.087 -> Problem conclusions: 5.087/5.087 Not left linear, Not right linear, Not linear 5.087/5.087 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 5.087/5.087 CTRS Type: 3 5.087/5.087 Deterministic, Strongly deterministic 5.087/5.087 Oriented CTRS, Properly oriented CTRS, Not join CTRS 5.087/5.087 Maybe right-stable CTRS, Not overlay CTRS 5.087/5.087 Maybe normal CTRS, Maybe almost normal CTRS 5.087/5.087 Terminating CTRS, Maybe joinable CCPs 5.087/5.087 Maybe level confluent 5.087/5.087 Maybe confluent 5.087/5.087 5.087/5.087 Problem 1: 5.087/5.087 5.087/5.087 Transform CTRS Processor: 5.087/5.087 5.087/5.087 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.087/5.087 Confluence Problem: 5.087/5.087 (VAR x:S y:S) 5.087/5.087 (STRATEGY CONTEXTSENSITIVE 5.087/5.087 (a) 5.087/5.087 (b) 5.087/5.087 (c) 5.087/5.087 (d) 5.087/5.087 (f 1) 5.087/5.087 (g 1 2) 5.087/5.087 (k) 5.087/5.087 (l) 5.087/5.087 (s 1) 5.087/5.087 (e) 5.087/5.087 (fSNonEmpty) 5.087/5.087 (h 1 2) 5.087/5.087 (pair 1 2) 5.087/5.087 (t 1) 5.087/5.087 ) 5.087/5.087 (RULES 5.087/5.087 a -> c 5.087/5.087 a -> d 5.087/5.087 b -> c 5.087/5.087 b -> d 5.087/5.087 c -> e 5.087/5.087 d -> e 5.087/5.087 f(x:S) -> pair(x:S,y:S) | s(x:S) ->* t(y:S) 5.087/5.087 g(x:S,x:S) -> h(x:S,x:S) 5.087/5.087 k -> e 5.087/5.087 l -> e 5.087/5.087 s(c) -> t(k) 5.087/5.087 s(c) -> t(l) 5.087/5.087 s(e) -> t(e) 5.087/5.087 ) 5.087/5.087 Critical Pairs: 5.087/5.087 => Not trivial, Not overlay, N1 5.087/5.087 => Not trivial, Overlay, N2 5.087/5.087 => Not trivial, Not overlay, N3 5.087/5.087 => Not trivial, Overlay, N4 5.087/5.087 Terminating:YES 5.087/5.087 5.087/5.087 -> Problem conclusions: 5.087/5.087 Not left linear, Not right linear, Not linear 5.087/5.087 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 5.087/5.087 CTRS Type: 3 5.087/5.087 Deterministic, Strongly deterministic 5.087/5.087 Oriented CTRS, Properly oriented CTRS, Not join CTRS 5.087/5.087 Maybe right-stable CTRS, Not overlay CTRS 5.087/5.087 Maybe normal CTRS, Maybe almost normal CTRS 5.087/5.087 Terminating CTRS, Maybe joinable CCPs 5.087/5.087 Maybe level confluent 5.087/5.087 Maybe confluent 5.087/5.087 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.087/5.087 Resulting U(R): 5.087/5.087 (VAR x:S y:S) 5.087/5.087 (STRATEGY CONTEXTSENSITIVE 5.087/5.087 (a) 5.087/5.087 (b) 5.087/5.087 (c) 5.087/5.087 (d) 5.087/5.087 (f 1) 5.087/5.087 (g 1 2) 5.087/5.087 (k) 5.087/5.087 (l) 5.087/5.087 (s 1) 5.087/5.087 (e) 5.087/5.087 (fSNonEmpty) 5.087/5.087 (h 1 2) 5.087/5.087 (pair 1 2) 5.087/5.087 (t 1) 5.087/5.087 (U15_1 1 2) 5.087/5.087 ) 5.087/5.087 (RULES 5.087/5.087 a -> c 5.087/5.087 a -> d 5.087/5.087 b -> c 5.087/5.087 b -> d 5.087/5.087 c -> e 5.087/5.087 d -> e 5.087/5.087 f(x:S) -> U15_1(s(x:S),x:S) 5.087/5.087 g(x:S,x:S) -> h(x:S,x:S) 5.087/5.087 k -> e 5.087/5.087 l -> e 5.087/5.087 s(c) -> t(k) 5.087/5.087 s(c) -> t(l) 5.087/5.087 s(e) -> t(e) 5.087/5.087 U15_1(t(y:S),x:S) -> pair(x:S,y:S) 5.087/5.087 ) 5.087/5.087 5.087/5.087 Problem 1: 5.087/5.087 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.087/5.087 Confluence Problem: 5.087/5.087 (VAR x:S y:S) 5.087/5.087 (STRATEGY CONTEXTSENSITIVE 5.087/5.087 (a) 5.087/5.087 (b) 5.087/5.087 (c) 5.087/5.087 (d) 5.087/5.087 (f 1) 5.087/5.087 (g 1 2) 5.087/5.087 (k) 5.087/5.087 (l) 5.087/5.087 (s 1) 5.087/5.087 (e) 5.087/5.087 (fSNonEmpty) 5.087/5.087 (h 1 2) 5.087/5.087 (pair 1 2) 5.087/5.087 (t 1) 5.087/5.087 (U15_1 1 2) 5.087/5.087 ) 5.087/5.087 (RULES 5.087/5.087 a -> c 5.087/5.087 a -> d 5.087/5.087 b -> c 5.087/5.087 b -> d 5.087/5.087 c -> e 5.087/5.087 d -> e 5.087/5.087 f(x:S) -> U15_1(s(x:S),x:S) 5.087/5.087 g(x:S,x:S) -> h(x:S,x:S) 5.087/5.087 k -> e 5.087/5.087 l -> e 5.087/5.087 s(c) -> t(k) 5.087/5.087 s(c) -> t(l) 5.087/5.087 s(e) -> t(e) 5.087/5.087 U15_1(t(y:S),x:S) -> pair(x:S,y:S) 5.087/5.087 ) 5.087/5.087 Terminating:"YES" 5.087/5.087 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.087/5.087 5.087/5.087 Huet Levy Processor: 5.087/5.087 -> Rules: 5.087/5.087 a -> c 5.087/5.087 a -> d 5.087/5.087 b -> c 5.087/5.087 b -> d 5.087/5.087 c -> e 5.087/5.087 d -> e 5.087/5.087 f(x:S) -> U15_1(s(x:S),x:S) 5.087/5.087 g(x:S,x:S) -> h(x:S,x:S) 5.087/5.087 k -> e 5.087/5.087 l -> e 5.087/5.087 s(c) -> t(k) 5.087/5.087 s(c) -> t(l) 5.087/5.087 s(e) -> t(e) 5.087/5.087 U15_1(t(y:S),x:S) -> pair(x:S,y:S) 5.087/5.087 -> Vars: 5.087/5.087 x, x, x, y 5.087/5.087 -> FVars: 5.087/5.087 x3, x4, x5, x6 5.087/5.087 -> PVars: 5.087/5.087 x: [x3, x4, x5], y: [x6] 5.087/5.087 5.087/5.087 -> Rlps: 5.087/5.087 (rule: a -> c, id: 1, possubterms: a->[]) 5.087/5.087 (rule: a -> d, id: 2, possubterms: a->[]) 5.087/5.087 (rule: b -> c, id: 3, possubterms: b->[]) 5.087/5.087 (rule: b -> d, id: 4, possubterms: b->[]) 5.087/5.087 (rule: c -> e, id: 5, possubterms: c->[]) 5.087/5.087 (rule: d -> e, id: 6, possubterms: d->[]) 5.087/5.087 (rule: f(x3:S) -> U15_1(s(x3:S),x3:S), id: 7, possubterms: f(x3:S)->[]) 5.087/5.087 (rule: g(x4:S,x4:S) -> h(x4:S,x4:S), id: 8, possubterms: g(x4:S,x4:S)->[]) 5.087/5.087 (rule: k -> e, id: 9, possubterms: k->[]) 5.087/5.087 (rule: l -> e, id: 10, possubterms: l->[]) 5.087/5.087 (rule: s(c) -> t(k), id: 11, possubterms: s(c)->[], c->[1]) 5.087/5.087 (rule: s(c) -> t(l), id: 12, possubterms: s(c)->[], c->[1]) 5.087/5.087 (rule: s(e) -> t(e), id: 13, possubterms: s(e)->[], e->[1]) 5.087/5.087 (rule: U15_1(t(x6:S),x5:S) -> pair(x5:S,x6:S), id: 14, possubterms: U15_1(t(x6:S),x5:S)->[], t(x6:S)->[1]) 5.087/5.087 5.087/5.087 -> Unifications: 5.087/5.087 (R2 unifies with R1 at p: [], l: a, lp: a, sig: {}, l': a, r: d, r': c) 5.087/5.087 (R4 unifies with R3 at p: [], l: b, lp: b, sig: {}, l': b, r: d, r': c) 5.087/5.087 (R11 unifies with R5 at p: [1], l: s(c), lp: c, sig: {}, l': c, r: t(k), r': e) 5.087/5.087 (R12 unifies with R11 at p: [], l: s(c), lp: s(c), sig: {}, l': s(c), r: t(l), r': t(k)) 5.087/5.087 (R12 unifies with R5 at p: [1], l: s(c), lp: c, sig: {}, l': c, r: t(l), r': e) 5.087/5.087 5.087/5.087 -> Critical pairs info: 5.087/5.087 => Not trivial, Overlay, N1 5.087/5.087 => Not trivial, Not overlay, N2 5.087/5.087 => Not trivial, Not overlay, N3 5.087/5.087 => Not trivial, Overlay, N4 5.087/5.087 5.087/5.087 -> Problem conclusions: 5.087/5.087 Not left linear, Not right linear, Not linear 5.087/5.087 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 5.087/5.087 Not Huet-Levy confluent, Not Newman confluent 5.087/5.087 R is a TRS 5.087/5.087 5.087/5.087 5.087/5.087 5.087/5.087 The problem is decomposed in 4 subproblems. 5.087/5.087 5.087/5.087 Problem 1.1: 5.087/5.087 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.087/5.087 Confluence Problem: 5.087/5.087 (VAR x:S y:S) 5.087/5.087 (STRATEGY CONTEXTSENSITIVE 5.087/5.087 (a) 5.087/5.087 (b) 5.087/5.087 (c) 5.087/5.087 (d) 5.087/5.087 (f 1) 5.087/5.087 (g 1 2) 5.087/5.087 (k) 5.087/5.087 (l) 5.087/5.087 (s 1) 5.087/5.087 (e) 5.087/5.087 (fSNonEmpty) 5.087/5.087 (h 1 2) 5.087/5.087 (pair 1 2) 5.087/5.087 (t 1) 5.087/5.087 (U15_1 1 2) 5.087/5.087 ) 5.087/5.087 (RULES 5.087/5.087 a -> c 5.087/5.087 a -> d 5.087/5.087 b -> c 5.087/5.087 b -> d 5.087/5.087 c -> e 5.087/5.087 d -> e 5.087/5.087 f(x:S) -> U15_1(s(x:S),x:S) 5.087/5.087 g(x:S,x:S) -> h(x:S,x:S) 5.087/5.087 k -> e 5.087/5.087 l -> e 5.087/5.087 s(c) -> t(k) 5.087/5.087 s(c) -> t(l) 5.087/5.087 s(e) -> t(e) 5.087/5.087 U15_1(t(y:S),x:S) -> pair(x:S,y:S) 5.087/5.087 ) 5.087/5.087 Critical Pairs: 5.087/5.087 => Not trivial, Overlay, N1 5.087/5.087 Terminating:"YES" 5.087/5.087 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.087/5.087 5.087/5.087 Huet Brute Force Joinability Processor: 5.087/5.087 -> Rewritings: 5.087/5.087 s: t(k) 5.087/5.087 Nodes: [0,1] 5.087/5.087 Edges: [(0,1)] 5.087/5.087 ID: 0 => ('t(k)', D0) 5.087/5.087 ID: 1 => ('t(e)', D1, R9, P[1], S{}), NR: 'e' 5.087/5.087 t: t(l) 5.087/5.087 Nodes: [0,1] 5.087/5.087 Edges: [(0,1)] 5.087/5.087 ID: 0 => ('t(l)', D0) 5.087/5.087 ID: 1 => ('t(e)', D1, R10, P[1], S{}), NR: 'e' 5.087/5.087 t(k) ->* t(e) *<- t(l) 5.087/5.087 "Joinable" 5.087/5.087 5.087/5.087 The problem is joinable. 5.087/5.087 5.087/5.087 Problem 1.2: 5.087/5.087 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.087/5.087 Confluence Problem: 5.087/5.087 (VAR x:S y:S) 5.087/5.087 (STRATEGY CONTEXTSENSITIVE 5.087/5.087 (a) 5.087/5.087 (b) 5.087/5.087 (c) 5.087/5.087 (d) 5.087/5.087 (f 1) 5.087/5.087 (g 1 2) 5.087/5.087 (k) 5.087/5.087 (l) 5.087/5.087 (s 1) 5.087/5.087 (e) 5.087/5.087 (fSNonEmpty) 5.087/5.087 (h 1 2) 5.087/5.087 (pair 1 2) 5.087/5.087 (t 1) 5.087/5.087 (U15_1 1 2) 5.087/5.087 ) 5.087/5.087 (RULES 5.087/5.087 a -> c 5.087/5.087 a -> d 5.087/5.087 b -> c 5.087/5.087 b -> d 5.087/5.087 c -> e 5.087/5.087 d -> e 5.087/5.087 f(x:S) -> U15_1(s(x:S),x:S) 5.087/5.087 g(x:S,x:S) -> h(x:S,x:S) 5.087/5.087 k -> e 5.087/5.087 l -> e 5.087/5.087 s(c) -> t(k) 5.087/5.087 s(c) -> t(l) 5.087/5.087 s(e) -> t(e) 5.087/5.087 U15_1(t(y:S),x:S) -> pair(x:S,y:S) 5.087/5.087 ) 5.087/5.087 Critical Pairs: 5.087/5.087 => Not trivial, Not overlay, N2 5.087/5.087 Terminating:"YES" 5.087/5.087 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.087/5.087 5.087/5.087 Huet Brute Force Joinability Processor: 5.087/5.087 -> Rewritings: 5.087/5.087 s: s(e) 5.087/5.087 Nodes: [0,1] 5.087/5.087 Edges: [(0,1)] 5.087/5.087 ID: 0 => ('s(e)', D0) 5.087/5.087 ID: 1 => ('t(e)', D1, R13, P[], S{}), NR: 't(e)' 5.087/5.087 t: t(l) 5.087/5.087 Nodes: [0,1] 5.087/5.087 Edges: [(0,1)] 5.087/5.087 ID: 0 => ('t(l)', D0) 5.087/5.087 ID: 1 => ('t(e)', D1, R10, P[1], S{}), NR: 'e' 5.087/5.087 s(e) ->* t(e) *<- t(l) 5.087/5.087 "Joinable" 5.087/5.087 5.087/5.087 The problem is joinable. 5.087/5.087 5.087/5.087 Problem 1.3: 5.087/5.087 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.087/5.087 Confluence Problem: 5.087/5.087 (VAR x:S y:S) 5.087/5.087 (STRATEGY CONTEXTSENSITIVE 5.087/5.087 (a) 5.087/5.087 (b) 5.087/5.087 (c) 5.087/5.087 (d) 5.087/5.087 (f 1) 5.087/5.087 (g 1 2) 5.087/5.087 (k) 5.087/5.087 (l) 5.087/5.087 (s 1) 5.087/5.087 (e) 5.087/5.087 (fSNonEmpty) 5.087/5.087 (h 1 2) 5.087/5.087 (pair 1 2) 5.087/5.087 (t 1) 5.087/5.087 (U15_1 1 2) 5.087/5.087 ) 5.087/5.087 (RULES 5.087/5.087 a -> c 5.087/5.087 a -> d 5.087/5.087 b -> c 5.087/5.087 b -> d 5.087/5.087 c -> e 5.087/5.087 d -> e 5.087/5.087 f(x:S) -> U15_1(s(x:S),x:S) 5.087/5.087 g(x:S,x:S) -> h(x:S,x:S) 5.087/5.087 k -> e 5.087/5.087 l -> e 5.087/5.087 s(c) -> t(k) 5.087/5.087 s(c) -> t(l) 5.087/5.087 s(e) -> t(e) 5.087/5.087 U15_1(t(y:S),x:S) -> pair(x:S,y:S) 5.087/5.087 ) 5.087/5.087 Critical Pairs: 5.087/5.087 => Not trivial, Not overlay, N3 5.087/5.087 Terminating:"YES" 5.087/5.087 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.087/5.087 5.087/5.087 Huet Brute Force Joinability Processor: 5.087/5.087 -> Rewritings: 5.087/5.087 s: s(e) 5.087/5.087 Nodes: [0,1] 5.087/5.087 Edges: [(0,1)] 5.087/5.087 ID: 0 => ('s(e)', D0) 5.087/5.087 ID: 1 => ('t(e)', D1, R13, P[], S{}), NR: 't(e)' 5.087/5.087 t: t(k) 5.087/5.087 Nodes: [0,1] 5.087/5.087 Edges: [(0,1)] 5.087/5.087 ID: 0 => ('t(k)', D0) 5.087/5.087 ID: 1 => ('t(e)', D1, R9, P[1], S{}), NR: 'e' 5.087/5.087 s(e) ->* t(e) *<- t(k) 5.087/5.087 "Joinable" 5.087/5.087 5.087/5.087 The problem is joinable. 5.087/5.087 5.087/5.087 Problem 1.4: 5.087/5.087 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.087/5.087 Confluence Problem: 5.087/5.087 (VAR x:S y:S) 5.087/5.087 (STRATEGY CONTEXTSENSITIVE 5.087/5.087 (a) 5.087/5.087 (b) 5.087/5.087 (c) 5.087/5.087 (d) 5.087/5.087 (f 1) 5.087/5.087 (g 1 2) 5.087/5.087 (k) 5.087/5.087 (l) 5.087/5.087 (s 1) 5.087/5.087 (e) 5.087/5.087 (fSNonEmpty) 5.087/5.087 (h 1 2) 5.087/5.087 (pair 1 2) 5.087/5.087 (t 1) 5.087/5.087 (U15_1 1 2) 5.087/5.087 ) 5.087/5.087 (RULES 5.087/5.087 a -> c 5.087/5.087 a -> d 5.087/5.087 b -> c 5.087/5.087 b -> d 5.087/5.087 c -> e 5.087/5.087 d -> e 5.087/5.087 f(x:S) -> U15_1(s(x:S),x:S) 5.087/5.087 g(x:S,x:S) -> h(x:S,x:S) 5.087/5.087 k -> e 5.087/5.087 l -> e 5.087/5.087 s(c) -> t(k) 5.087/5.087 s(c) -> t(l) 5.087/5.087 s(e) -> t(e) 5.087/5.087 U15_1(t(y:S),x:S) -> pair(x:S,y:S) 5.087/5.087 ) 5.087/5.087 Critical Pairs: 5.087/5.087 => Not trivial, Overlay, N4 5.087/5.087 Terminating:"YES" 5.087/5.087 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.087/5.087 5.087/5.087 Huet Brute Force Joinability Processor: 5.087/5.087 -> Rewritings: 5.087/5.087 s: c 5.087/5.087 Nodes: [0,1] 5.087/5.087 Edges: [(0,1)] 5.087/5.087 ID: 0 => ('c', D0) 5.087/5.087 ID: 1 => ('e', D1, R5, P[], S{}), NR: 'e' 5.087/5.087 t: d 5.087/5.087 Nodes: [0,1] 5.087/5.087 Edges: [(0,1)] 5.087/5.087 ID: 0 => ('d', D0) 5.087/5.087 ID: 1 => ('e', D1, R6, P[], S{}), NR: 'e' 5.087/5.087 c ->* e *<- d 5.087/5.087 "Joinable" 5.087/5.087 5.087/5.087 The problem is joinable. 5.087/5.087 0.48user 0.06system 0:05.87elapsed 9%CPU (0avgtext+0avgdata 12908maxresident)k 5.087/5.087 8inputs+0outputs (0major+24487minor)pagefaults 0swaps