YES Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty) (REPLACEMENT-MAP (a1) (a10) (a2) (a3) (a4) (a5) (a6) (a7) (a8) (a9) (b1) (b10) (b2) (b3) (b4) (b5) (b6) (b7) (b8) (b9) (c1) (c10) (c2) (c3) (c4) (c5) (c6) (c7) (c8) (c9) (b11) (fSNonEmpty) ) (RULES a1 -> b1 a1 -> c1 a10 -> b11 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b5 a5 -> c5 a6 -> b6 a6 -> c6 a7 -> b7 a7 -> c7 a8 -> b8 a8 -> c8 a9 -> b9 a9 -> c9 b1 -> b2 b10 -> b11 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 b6 -> b7 b7 -> b8 b8 -> b9 b9 -> b10 c1 -> c2 c10 -> b11 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> c6 c6 -> c7 c7 -> c8 c8 -> c9 c9 -> c10 ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: Termination Procedure: Terminating? YES Problem 1: (VAR vu95NonEmpty vNonEmpty) (RULES a1 -> b1 a1 -> c1 a10 -> b11 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b5 a5 -> c5 a6 -> b6 a6 -> c6 a7 -> b7 a7 -> c7 a8 -> b8 a8 -> c8 a9 -> b9 a9 -> c9 b1 -> b2 b10 -> b11 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 b6 -> b7 b7 -> b8 b8 -> b9 b9 -> b10 c1 -> c2 c10 -> b11 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> c6 c6 -> c7 c7 -> c8 c8 -> c9 c9 -> c10 ) Problem 1: Dependency Pairs Processor: -> Pairs: A1 -> B1 A1 -> C1 A2 -> B2 A2 -> C2 A3 -> B3 A3 -> C3 A4 -> B4 A4 -> C4 A5 -> B5 A5 -> C5 A6 -> B6 A6 -> C6 A7 -> B7 A7 -> C7 A8 -> B8 A8 -> C8 A9 -> B9 A9 -> C9 B1 -> B2 B2 -> B3 B3 -> B4 B4 -> B5 B5 -> B6 B6 -> B7 B7 -> B8 B8 -> B9 B9 -> B10 C1 -> C2 C2 -> C3 C3 -> C4 C4 -> C5 C5 -> C6 C6 -> C7 C7 -> C8 C8 -> C9 C9 -> C10 -> Rules: a1 -> b1 a1 -> c1 a10 -> b11 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b5 a5 -> c5 a6 -> b6 a6 -> c6 a7 -> b7 a7 -> c7 a8 -> b8 a8 -> c8 a9 -> b9 a9 -> c9 b1 -> b2 b10 -> b11 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 b6 -> b7 b7 -> b8 b8 -> b9 b9 -> b10 c1 -> c2 c10 -> b11 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> c6 c6 -> c7 c7 -> c8 c8 -> c9 c9 -> c10 Problem 1: SCC Processor: -> Pairs: A1 -> B1 A1 -> C1 A2 -> B2 A2 -> C2 A3 -> B3 A3 -> C3 A4 -> B4 A4 -> C4 A5 -> B5 A5 -> C5 A6 -> B6 A6 -> C6 A7 -> B7 A7 -> C7 A8 -> B8 A8 -> C8 A9 -> B9 A9 -> C9 B1 -> B2 B2 -> B3 B3 -> B4 B4 -> B5 B5 -> B6 B6 -> B7 B7 -> B8 B8 -> B9 B9 -> B10 C1 -> C2 C2 -> C3 C3 -> C4 C4 -> C5 C5 -> C6 C6 -> C7 C7 -> C8 C8 -> C9 C9 -> C10 -> Rules: a1 -> b1 a1 -> c1 a10 -> b11 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b5 a5 -> c5 a6 -> b6 a6 -> c6 a7 -> b7 a7 -> c7 a8 -> b8 a8 -> c8 a9 -> b9 a9 -> c9 b1 -> b2 b10 -> b11 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 b6 -> b7 b7 -> b8 b8 -> b9 b9 -> b10 c1 -> c2 c10 -> b11 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> c6 c6 -> c7 c7 -> c8 c8 -> c9 c9 -> c10 ->Strongly Connected Components: There is no strongly connected component The problem is finite. Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty) (REPLACEMENT-MAP (a1) (a10) (a2) (a3) (a4) (a5) (a6) (a7) (a8) (a9) (b1) (b10) (b2) (b3) (b4) (b5) (b6) (b7) (b8) (b9) (c1) (c10) (c2) (c3) (c4) (c5) (c6) (c7) (c8) (c9) (b11) (fSNonEmpty) ) (RULES a1 -> b1 a1 -> c1 a10 -> b11 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b5 a5 -> c5 a6 -> b6 a6 -> c6 a7 -> b7 a7 -> c7 a8 -> b8 a8 -> c8 a9 -> b9 a9 -> c9 b1 -> b2 b10 -> b11 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 b6 -> b7 b7 -> b8 b8 -> b9 b9 -> b10 c1 -> c2 c10 -> b11 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> c6 c6 -> c7 c7 -> c8 c8 -> c9 c9 -> c10 ) Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy NW Procedure: -> Rules: a1 -> b1 a1 -> c1 a10 -> b11 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b5 a5 -> c5 a6 -> b6 a6 -> c6 a7 -> b7 a7 -> c7 a8 -> b8 a8 -> c8 a9 -> b9 a9 -> c9 b1 -> b2 b10 -> b11 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 b6 -> b7 b7 -> b8 b8 -> b9 b9 -> b10 c1 -> c2 c10 -> b11 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> c6 c6 -> c7 c7 -> c8 c8 -> c9 c9 -> c10 -> Vars: -> Rlps: (rule: a1 -> b1, id: 1, possubterms: a1->[]) (rule: a1 -> c1, id: 2, possubterms: a1->[]) (rule: a10 -> b11, id: 3, possubterms: a10->[]) (rule: a2 -> b2, id: 4, possubterms: a2->[]) (rule: a2 -> c2, id: 5, possubterms: a2->[]) (rule: a3 -> b3, id: 6, possubterms: a3->[]) (rule: a3 -> c3, id: 7, possubterms: a3->[]) (rule: a4 -> b4, id: 8, possubterms: a4->[]) (rule: a4 -> c4, id: 9, possubterms: a4->[]) (rule: a5 -> b5, id: 10, possubterms: a5->[]) (rule: a5 -> c5, id: 11, possubterms: a5->[]) (rule: a6 -> b6, id: 12, possubterms: a6->[]) (rule: a6 -> c6, id: 13, possubterms: a6->[]) (rule: a7 -> b7, id: 14, possubterms: a7->[]) (rule: a7 -> c7, id: 15, possubterms: a7->[]) (rule: a8 -> b8, id: 16, possubterms: a8->[]) (rule: a8 -> c8, id: 17, possubterms: a8->[]) (rule: a9 -> b9, id: 18, possubterms: a9->[]) (rule: a9 -> c9, id: 19, possubterms: a9->[]) (rule: b1 -> b2, id: 20, possubterms: b1->[]) (rule: b10 -> b11, id: 21, possubterms: b10->[]) (rule: b2 -> b3, id: 22, possubterms: b2->[]) (rule: b3 -> b4, id: 23, possubterms: b3->[]) (rule: b4 -> b5, id: 24, possubterms: b4->[]) (rule: b5 -> b6, id: 25, possubterms: b5->[]) (rule: b6 -> b7, id: 26, possubterms: b6->[]) (rule: b7 -> b8, id: 27, possubterms: b7->[]) (rule: b8 -> b9, id: 28, possubterms: b8->[]) (rule: b9 -> b10, id: 29, possubterms: b9->[]) (rule: c1 -> c2, id: 30, possubterms: c1->[]) (rule: c10 -> b11, id: 31, possubterms: c10->[]) (rule: c2 -> c3, id: 32, possubterms: c2->[]) (rule: c3 -> c4, id: 33, possubterms: c3->[]) (rule: c4 -> c5, id: 34, possubterms: c4->[]) (rule: c5 -> c6, id: 35, possubterms: c5->[]) (rule: c6 -> c7, id: 36, possubterms: c6->[]) (rule: c7 -> c8, id: 37, possubterms: c7->[]) (rule: c8 -> c9, id: 38, possubterms: c8->[]) (rule: c9 -> c10, id: 39, possubterms: c9->[]) -> Unifications: (R2 unifies with R1 at p: [], l: a1, lp: a1, sig: {}, l': a1, r: c1, r': b1) (R5 unifies with R4 at p: [], l: a2, lp: a2, sig: {}, l': a2, r: c2, r': b2) (R7 unifies with R6 at p: [], l: a3, lp: a3, sig: {}, l': a3, r: c3, r': b3) (R9 unifies with R8 at p: [], l: a4, lp: a4, sig: {}, l': a4, r: c4, r': b4) (R11 unifies with R10 at p: [], l: a5, lp: a5, sig: {}, l': a5, r: c5, r': b5) (R13 unifies with R12 at p: [], l: a6, lp: a6, sig: {}, l': a6, r: c6, r': b6) (R15 unifies with R14 at p: [], l: a7, lp: a7, sig: {}, l': a7, r: c7, r': b7) (R17 unifies with R16 at p: [], l: a8, lp: a8, sig: {}, l': a8, r: c8, r': b8) (R19 unifies with R18 at p: [], l: a9, lp: a9, sig: {}, l': a9, r: c9, r': b9) -> Critical pairs info: => Not trivial, Overlay, Proper, NW0, N1 => Not trivial, Overlay, Proper, NW0, N2 => Not trivial, Overlay, Proper, NW0, N3 => Not trivial, Overlay, Proper, NW0, N4 => Not trivial, Overlay, Proper, NW0, N5 => Not trivial, Overlay, Proper, NW0, N6 => Not trivial, Overlay, Proper, NW0, N7 => Not trivial, Overlay, Proper, NW0, N8 => Not trivial, Overlay, Proper, NW0, N9 -> Problem conclusions: Left linear, Right linear, Linear Not weakly orthogonal, Not almost orthogonal, Not orthogonal Not Huet-Levy confluent, Not Newman confluent R is a TRS The problem is decomposed in 9 subproblems. Problem 1.1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (REPLACEMENT-MAP (a1) (a10) (a2) (a3) (a4) (a5) (a6) (a7) (a8) (a9) (b1) (b10) (b2) (b3) (b4) (b5) (b6) (b7) (b8) (b9) (c1) (c10) (c2) (c3) (c4) (c5) (c6) (c7) (c8) (c9) (b11) (fSNonEmpty) ) (RULES a1 -> b1 a1 -> c1 a10 -> b11 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b5 a5 -> c5 a6 -> b6 a6 -> c6 a7 -> b7 a7 -> c7 a8 -> b8 a8 -> c8 a9 -> b9 a9 -> c9 b1 -> b2 b10 -> b11 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 b6 -> b7 b7 -> b8 b8 -> b9 b9 -> b10 c1 -> c2 c10 -> b11 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> c6 c6 -> c7 c7 -> c8 c8 -> c9 c9 -> c10 ) Critical Pairs: => Not trivial, Overlay, Proper, NW0, N1 Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Brute Force Joinability Procedure: -> Rewritings: s: b7 Nodes: [0,1,2,3,4] Edges: [(0,1),(1,2),(2,3),(3,4)] ID: 0 => ('b7', D0) ID: 1 => ('b8', D1, R27, P[], S{}), NR: 'b8' ID: 2 => ('b9', D2, R28, P[], S{}), NR: 'b9' ID: 3 => ('b10', D3, R29, P[], S{}), NR: 'b10' ID: 4 => ('b11', D4, R21, P[], S{}), NR: 'b11' t: c7 Nodes: [0,1,2,3,4] Edges: [(0,1),(1,2),(2,3),(3,4)] ID: 0 => ('c7', D0) ID: 1 => ('c8', D1, R37, P[], S{}), NR: 'c8' ID: 2 => ('c9', D2, R38, P[], S{}), NR: 'c9' ID: 3 => ('c10', D3, R39, P[], S{}), NR: 'c10' ID: 4 => ('b11', D4, R31, P[], S{}), NR: 'b11' SNodesPath: b7 -> b8 -> b9 -> b10 -> b11 TNodesPath: c7 -> c8 -> c9 -> c10 -> b11 b7 ->* b11 *<- c7 "Joinable" The problem is confluent. Problem 1.2: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (REPLACEMENT-MAP (a1) (a10) (a2) (a3) (a4) (a5) (a6) (a7) (a8) (a9) (b1) (b10) (b2) (b3) (b4) (b5) (b6) (b7) (b8) (b9) (c1) (c10) (c2) (c3) (c4) (c5) (c6) (c7) (c8) (c9) (b11) (fSNonEmpty) ) (RULES a1 -> b1 a1 -> c1 a10 -> b11 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b5 a5 -> c5 a6 -> b6 a6 -> c6 a7 -> b7 a7 -> c7 a8 -> b8 a8 -> c8 a9 -> b9 a9 -> c9 b1 -> b2 b10 -> b11 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 b6 -> b7 b7 -> b8 b8 -> b9 b9 -> b10 c1 -> c2 c10 -> b11 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> c6 c6 -> c7 c7 -> c8 c8 -> c9 c9 -> c10 ) Critical Pairs: => Not trivial, Overlay, Proper, NW0, N2 Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet InfChecker Procedure: Infeasible convergence? NO Problem 1: Infeasibility Problem: [(VAR vNonEmpty vNonEmpty z0) (STRATEGY CONTEXTSENSITIVE (a1) (a10) (a2) (a3) (a4) (a5) (a6) (a7) (a8) (a9) (b1) (b10) (b2) (b3) (b4) (b5) (b6) (b7) (b8) (b9) (c1) (c10) (c2) (c3) (c4) (c5) (c6) (c7) (c8) (c9) (b11) (fSNonEmpty) ) (RULES a1 -> b1 a1 -> c1 a10 -> b11 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b5 a5 -> c5 a6 -> b6 a6 -> c6 a7 -> b7 a7 -> c7 a8 -> b8 a8 -> c8 a9 -> b9 a9 -> c9 b1 -> b2 b10 -> b11 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 b6 -> b7 b7 -> b8 b8 -> b9 b9 -> b10 c1 -> c2 c10 -> b11 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> c6 c6 -> c7 c7 -> c8 c8 -> c9 c9 -> c10 )] Infeasibility Conditions: b3 ->* z0, c3 ->* z0 Problem 1: Obtaining a proof using Prover9: -> Prover9 Output: ============================== Prover9 =============================== Prover9 (64) version 2009-11A, November 2009. Process 2696367 was started by shintani on shintani-XPS-13-9310, Fri Jun 9 15:47:25 2023 The command was "./prover9 -f /tmp/prover92696351-0.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file /tmp/prover92696351-0.in assign(max_seconds,20). formulas(assumptions). ->_s0(b10,b11) # label(replacement). ->_s0(b3,b4) # label(replacement). ->_s0(b4,b5) # label(replacement). ->_s0(b5,b6) # label(replacement). ->_s0(b6,b7) # label(replacement). ->_s0(b7,b8) # label(replacement). ->_s0(b8,b9) # label(replacement). ->_s0(b9,b10) # label(replacement). ->_s0(c10,b11) # label(replacement). ->_s0(c3,c4) # label(replacement). ->_s0(c4,c5) # label(replacement). ->_s0(c5,c6) # label(replacement). ->_s0(c6,c7) # label(replacement). ->_s0(c7,c8) # label(replacement). ->_s0(c8,c9) # label(replacement). ->_s0(c9,c10) # label(replacement). ->*_s0(x,x) # label(reflexivity). ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). end_of_list. formulas(goals). (exists x2 (->*_s0(b3,x2) & ->*_s0(c3,x2))) # label(goal). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 2 (exists x2 (->*_s0(b3,x2) & ->*_s0(c3,x2))) # label(goal) # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). ->_s0(b10,b11) # label(replacement). [assumption]. ->_s0(b3,b4) # label(replacement). [assumption]. ->_s0(b4,b5) # label(replacement). [assumption]. ->_s0(b5,b6) # label(replacement). [assumption]. ->_s0(b6,b7) # label(replacement). [assumption]. ->_s0(b7,b8) # label(replacement). [assumption]. ->_s0(b8,b9) # label(replacement). [assumption]. ->_s0(b9,b10) # label(replacement). [assumption]. ->_s0(c10,b11) # label(replacement). [assumption]. ->_s0(c3,c4) # label(replacement). [assumption]. ->_s0(c4,c5) # label(replacement). [assumption]. ->_s0(c5,c6) # label(replacement). [assumption]. ->_s0(c6,c7) # label(replacement). [assumption]. ->_s0(c7,c8) # label(replacement). [assumption]. ->_s0(c8,c9) # label(replacement). [assumption]. ->_s0(c9,c10) # label(replacement). [assumption]. ->*_s0(x,x) # label(reflexivity). [assumption]. -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. -->*_s0(b3,x) | -->*_s0(c3,x) # label(goal). [deny(2)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating ->_s0/2 3 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 4 ->_s0(b10,b11) # label(replacement). [assumption]. 5 ->_s0(b3,b4) # label(replacement). [assumption]. 6 ->_s0(b4,b5) # label(replacement). [assumption]. 7 ->_s0(b5,b6) # label(replacement). [assumption]. 8 ->_s0(b6,b7) # label(replacement). [assumption]. 9 ->_s0(b7,b8) # label(replacement). [assumption]. 10 ->_s0(b8,b9) # label(replacement). [assumption]. 11 ->_s0(b9,b10) # label(replacement). [assumption]. 12 ->_s0(c10,b11) # label(replacement). [assumption]. 13 ->_s0(c3,c4) # label(replacement). [assumption]. 14 ->_s0(c4,c5) # label(replacement). [assumption]. 15 ->_s0(c5,c6) # label(replacement). [assumption]. 16 ->_s0(c6,c7) # label(replacement). [assumption]. 17 ->_s0(c7,c8) # label(replacement). [assumption]. 18 ->_s0(c8,c9) # label(replacement). [assumption]. 19 ->_s0(c9,c10) # label(replacement). [assumption]. Derived: -->*_s0(b11,x) | ->*_s0(b10,x). [resolve(3,a,4,a)]. Derived: -->*_s0(b4,x) | ->*_s0(b3,x). [resolve(3,a,5,a)]. Derived: -->*_s0(b5,x) | ->*_s0(b4,x). [resolve(3,a,6,a)]. Derived: -->*_s0(b6,x) | ->*_s0(b5,x). [resolve(3,a,7,a)]. Derived: -->*_s0(b7,x) | ->*_s0(b6,x). [resolve(3,a,8,a)]. Derived: -->*_s0(b8,x) | ->*_s0(b7,x). [resolve(3,a,9,a)]. Derived: -->*_s0(b9,x) | ->*_s0(b8,x). [resolve(3,a,10,a)]. Derived: -->*_s0(b10,x) | ->*_s0(b9,x). [resolve(3,a,11,a)]. Derived: -->*_s0(b11,x) | ->*_s0(c10,x). [resolve(3,a,12,a)]. Derived: -->*_s0(c4,x) | ->*_s0(c3,x). [resolve(3,a,13,a)]. Derived: -->*_s0(c5,x) | ->*_s0(c4,x). [resolve(3,a,14,a)]. Derived: -->*_s0(c6,x) | ->*_s0(c5,x). [resolve(3,a,15,a)]. Derived: -->*_s0(c7,x) | ->*_s0(c6,x). [resolve(3,a,16,a)]. Derived: -->*_s0(c8,x) | ->*_s0(c7,x). [resolve(3,a,17,a)]. Derived: -->*_s0(c9,x) | ->*_s0(c8,x). [resolve(3,a,18,a)]. Derived: -->*_s0(c10,x) | ->*_s0(c9,x). [resolve(3,a,19,a)]. ============================== end predicate elimination ============= Auto_denials: % copying label goal to answer in negative clause Term ordering decisions: Predicate symbol precedence: predicate_order([ ->*_s0 ]). Function symbol precedence: function_order([ b10, b4, b5, b6, b7, b8, b9, c10, c4, c5, c6, c7, c8, c9, b11, b3, c3 ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(neg_binary_resolution). % (HNE depth_diff=0) % clear(ordered_res). % (HNE depth_diff=0) % set(ur_resolution). % (HNE depth_diff=0) % set(ur_resolution) -> set(pos_ur_resolution). % set(ur_resolution) -> set(neg_ur_resolution). Auto_process settings: % set(unit_deletion). % (Horn set with negative nonunits) kept: 20 ->*_s0(x,x) # label(reflexivity). [assumption]. kept: 21 -->*_s0(b3,x) | -->*_s0(c3,x) # label(goal) # answer(goal). [deny(2)]. kept: 22 -->*_s0(b11,x) | ->*_s0(b10,x). [resolve(3,a,4,a)]. kept: 23 -->*_s0(b4,x) | ->*_s0(b3,x). [resolve(3,a,5,a)]. kept: 24 -->*_s0(b5,x) | ->*_s0(b4,x). [resolve(3,a,6,a)]. kept: 25 -->*_s0(b6,x) | ->*_s0(b5,x). [resolve(3,a,7,a)]. kept: 26 -->*_s0(b7,x) | ->*_s0(b6,x). [resolve(3,a,8,a)]. kept: 27 -->*_s0(b8,x) | ->*_s0(b7,x). [resolve(3,a,9,a)]. kept: 28 -->*_s0(b9,x) | ->*_s0(b8,x). [resolve(3,a,10,a)]. kept: 29 -->*_s0(b10,x) | ->*_s0(b9,x). [resolve(3,a,11,a)]. kept: 30 -->*_s0(b11,x) | ->*_s0(c10,x). [resolve(3,a,12,a)]. kept: 31 -->*_s0(c4,x) | ->*_s0(c3,x). [resolve(3,a,13,a)]. kept: 32 -->*_s0(c5,x) | ->*_s0(c4,x). [resolve(3,a,14,a)]. kept: 33 -->*_s0(c6,x) | ->*_s0(c5,x). [resolve(3,a,15,a)]. kept: 34 -->*_s0(c7,x) | ->*_s0(c6,x). [resolve(3,a,16,a)]. kept: 35 -->*_s0(c8,x) | ->*_s0(c7,x). [resolve(3,a,17,a)]. kept: 36 -->*_s0(c9,x) | ->*_s0(c8,x). [resolve(3,a,18,a)]. kept: 37 -->*_s0(c10,x) | ->*_s0(c9,x). [resolve(3,a,19,a)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 20 ->*_s0(x,x) # label(reflexivity). [assumption]. 21 -->*_s0(b3,x) | -->*_s0(c3,x) # label(goal) # answer(goal). [deny(2)]. 22 -->*_s0(b11,x) | ->*_s0(b10,x). [resolve(3,a,4,a)]. 23 -->*_s0(b4,x) | ->*_s0(b3,x). [resolve(3,a,5,a)]. 24 -->*_s0(b5,x) | ->*_s0(b4,x). [resolve(3,a,6,a)]. 25 -->*_s0(b6,x) | ->*_s0(b5,x). [resolve(3,a,7,a)]. 26 -->*_s0(b7,x) | ->*_s0(b6,x). [resolve(3,a,8,a)]. 27 -->*_s0(b8,x) | ->*_s0(b7,x). [resolve(3,a,9,a)]. 28 -->*_s0(b9,x) | ->*_s0(b8,x). [resolve(3,a,10,a)]. 29 -->*_s0(b10,x) | ->*_s0(b9,x). [resolve(3,a,11,a)]. 30 -->*_s0(b11,x) | ->*_s0(c10,x). [resolve(3,a,12,a)]. 31 -->*_s0(c4,x) | ->*_s0(c3,x). [resolve(3,a,13,a)]. 32 -->*_s0(c5,x) | ->*_s0(c4,x). [resolve(3,a,14,a)]. 33 -->*_s0(c6,x) | ->*_s0(c5,x). [resolve(3,a,15,a)]. 34 -->*_s0(c7,x) | ->*_s0(c6,x). [resolve(3,a,16,a)]. 35 -->*_s0(c8,x) | ->*_s0(c7,x). [resolve(3,a,17,a)]. 36 -->*_s0(c9,x) | ->*_s0(c8,x). [resolve(3,a,18,a)]. 37 -->*_s0(c10,x) | ->*_s0(c9,x). [resolve(3,a,19,a)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=3): 20 ->*_s0(x,x) # label(reflexivity). [assumption]. given #2 (I,wt=6): 21 -->*_s0(b3,x) | -->*_s0(c3,x) # label(goal) # answer(goal). [deny(2)]. given #3 (I,wt=6): 22 -->*_s0(b11,x) | ->*_s0(b10,x). [resolve(3,a,4,a)]. given #4 (I,wt=6): 23 -->*_s0(b4,x) | ->*_s0(b3,x). [resolve(3,a,5,a)]. given #5 (I,wt=6): 24 -->*_s0(b5,x) | ->*_s0(b4,x). [resolve(3,a,6,a)]. given #6 (I,wt=6): 25 -->*_s0(b6,x) | ->*_s0(b5,x). [resolve(3,a,7,a)]. given #7 (I,wt=6): 26 -->*_s0(b7,x) | ->*_s0(b6,x). [resolve(3,a,8,a)]. given #8 (I,wt=6): 27 -->*_s0(b8,x) | ->*_s0(b7,x). [resolve(3,a,9,a)]. given #9 (I,wt=6): 28 -->*_s0(b9,x) | ->*_s0(b8,x). [resolve(3,a,10,a)]. given #10 (I,wt=6): 29 -->*_s0(b10,x) | ->*_s0(b9,x). [resolve(3,a,11,a)]. given #11 (I,wt=6): 30 -->*_s0(b11,x) | ->*_s0(c10,x). [resolve(3,a,12,a)]. given #12 (I,wt=6): 31 -->*_s0(c4,x) | ->*_s0(c3,x). [resolve(3,a,13,a)]. given #13 (I,wt=6): 32 -->*_s0(c5,x) | ->*_s0(c4,x). [resolve(3,a,14,a)]. given #14 (I,wt=6): 33 -->*_s0(c6,x) | ->*_s0(c5,x). [resolve(3,a,15,a)]. given #15 (I,wt=6): 34 -->*_s0(c7,x) | ->*_s0(c6,x). [resolve(3,a,16,a)]. given #16 (I,wt=6): 35 -->*_s0(c8,x) | ->*_s0(c7,x). [resolve(3,a,17,a)]. given #17 (I,wt=6): 36 -->*_s0(c9,x) | ->*_s0(c8,x). [resolve(3,a,18,a)]. given #18 (I,wt=6): 37 -->*_s0(c10,x) | ->*_s0(c9,x). [resolve(3,a,19,a)]. given #19 (A,wt=3): 38 -->*_s0(c3,b3) # answer(goal). [resolve(21,a,20,a)]. given #20 (F,wt=3): 39 -->*_s0(b3,c3) # answer(goal). [resolve(21,b,20,a)]. given #21 (F,wt=3): 58 -->*_s0(c4,b3) # answer(goal). [resolve(38,a,31,b)]. given #22 (F,wt=3): 59 -->*_s0(b4,c3) # answer(goal). [resolve(39,a,23,b)]. given #23 (F,wt=3): 60 -->*_s0(c5,b3) # answer(goal). [resolve(58,a,32,b)]. given #24 (T,wt=3): 40 ->*_s0(b10,b11). [ur(22,a,20,a)]. given #25 (T,wt=3): 42 ->*_s0(b3,b4). [ur(23,a,20,a)]. given #26 (T,wt=3): 43 ->*_s0(b4,b5). [ur(24,a,20,a)]. given #27 (T,wt=3): 44 ->*_s0(b5,b6). [ur(25,a,20,a)]. given #28 (A,wt=6): 41 -->*_s0(b4,x) | -->*_s0(c3,x) # answer(goal). [resolve(23,b,21,a)]. given #29 (F,wt=3): 61 -->*_s0(b5,c3) # answer(goal). [resolve(59,a,24,b)]. given #30 (F,wt=3): 62 -->*_s0(c6,b3) # answer(goal). [resolve(60,a,33,b)]. given #31 (F,wt=3): 64 -->*_s0(c3,b4) # answer(goal). [resolve(42,a,21,a)]. given #32 (F,wt=3): 67 -->*_s0(c3,b5) # answer(goal). [resolve(41,a,43,a)]. given #33 (T,wt=3): 45 ->*_s0(b6,b7). [ur(26,a,20,a)]. given #34 (T,wt=3): 46 ->*_s0(b7,b8). [ur(27,a,20,a)]. given #35 (T,wt=3): 47 ->*_s0(b8,b9). [ur(28,a,20,a)]. given #36 (T,wt=3): 48 ->*_s0(b9,b10). [ur(29,a,20,a)]. given #37 (A,wt=3): 49 ->*_s0(c10,b11). [ur(30,a,20,a)]. given #38 (F,wt=3): 70 -->*_s0(b6,c3) # answer(goal). [resolve(61,a,25,b)]. given #39 (F,wt=3): 71 -->*_s0(c7,b3) # answer(goal). [resolve(62,a,34,b)]. given #40 (F,wt=3): 72 -->*_s0(c4,b4) # answer(goal). [resolve(64,a,31,b)]. given #41 (F,wt=3): 73 -->*_s0(c4,b5) # answer(goal). [resolve(67,a,31,b)]. given #42 (T,wt=3): 51 ->*_s0(c3,c4). [ur(31,a,20,a)]. given #43 (T,wt=3): 52 ->*_s0(c4,c5). [ur(32,a,20,a)]. given #44 (T,wt=3): 53 ->*_s0(c5,c6). [ur(33,a,20,a)]. given #45 (T,wt=3): 54 ->*_s0(c6,c7). [ur(34,a,20,a)]. given #46 (A,wt=6): 50 -->*_s0(c4,x) | -->*_s0(b3,x) # answer(goal). [resolve(31,b,21,b)]. given #47 (F,wt=3): 79 -->*_s0(b7,c3) # answer(goal). [resolve(70,a,26,b)]. given #48 (F,wt=3): 80 -->*_s0(c8,b3) # answer(goal). [resolve(71,a,35,b)]. given #49 (F,wt=3): 81 -->*_s0(c5,b4) # answer(goal). [resolve(72,a,32,b)]. given #50 (F,wt=3): 82 -->*_s0(c5,b5) # answer(goal). [resolve(73,a,32,b)]. given #51 (T,wt=3): 55 ->*_s0(c7,c8). [ur(35,a,20,a)]. given #52 (T,wt=3): 56 ->*_s0(c8,c9). [ur(36,a,20,a)]. given #53 (T,wt=3): 57 ->*_s0(c9,c10). [ur(37,a,20,a)]. given #54 (T,wt=3): 63 ->*_s0(b9,b11). [ur(29,a,40,a)]. given #55 (A,wt=3): 65 ->*_s0(b3,b5). [ur(23,a,43,a)]. given #56 (F,wt=3): 83 -->*_s0(b4,c4) # answer(goal). [resolve(51,a,41,b)]. given #57 (F,wt=3): 84 -->*_s0(b3,c4) # answer(goal). [resolve(51,a,21,b)]. given #58 (F,wt=3): 88 -->*_s0(b3,c5) # answer(goal). [resolve(50,a,52,a)]. given #59 (F,wt=3): 90 -->*_s0(b8,c3) # answer(goal). [resolve(79,a,27,b)]. given #60 (T,wt=3): 66 ->*_s0(b4,b6). [ur(24,a,44,a)]. given #61 (T,wt=3): 74 ->*_s0(b5,b7). [ur(25,a,45,a)]. given #62 (T,wt=3): 75 ->*_s0(b6,b8). [ur(26,a,46,a)]. given #63 (T,wt=3): 76 ->*_s0(b7,b9). [ur(27,a,47,a)]. given #64 (A,wt=6): 68 -->*_s0(c3,x) | -->*_s0(b5,x) # answer(goal). [resolve(41,a,24,b)]. given #65 (F,wt=3): 91 -->*_s0(c9,b3) # answer(goal). [resolve(80,a,36,b)]. given #66 (F,wt=3): 92 -->*_s0(c6,b4) # answer(goal). [resolve(81,a,33,b)]. given #67 (F,wt=3): 93 -->*_s0(c6,b5) # answer(goal). [resolve(82,a,33,b)]. given #68 (F,wt=3): 98 -->*_s0(b5,c4) # answer(goal). [resolve(83,a,24,b)]. given #69 (T,wt=3): 77 ->*_s0(b8,b10). [ur(28,a,48,a)]. given #70 (T,wt=3): 78 ->*_s0(c9,b11). [ur(37,a,49,a)]. given #71 (T,wt=3): 85 ->*_s0(c3,c5). [ur(31,a,52,a)]. given #72 (T,wt=3): 86 ->*_s0(c4,c6). [ur(32,a,53,a)]. given #73 (A,wt=6): 69 -->*_s0(b4,x) | -->*_s0(c4,x) # answer(goal). [resolve(41,b,31,b)]. given #74 (F,wt=3): 99 -->*_s0(b4,c5) # answer(goal). [resolve(88,a,23,b)]. given #75 (F,wt=3): 100 -->*_s0(b9,c3) # answer(goal). [resolve(90,a,28,b)]. given #76 (F,wt=3): 101 -->*_s0(c3,b6) # answer(goal). [resolve(66,a,41,a)]. given #77 (F,wt=3): 107 -->*_s0(c3,b7) # answer(goal). [resolve(68,b,74,a)]. given #78 (T,wt=3): 87 ->*_s0(c5,c7). [ur(33,a,54,a)]. given #79 (T,wt=3): 94 ->*_s0(c6,c8). [ur(34,a,55,a)]. given #80 (T,wt=3): 95 ->*_s0(c7,c9). [ur(35,a,56,a)]. given #81 (T,wt=3): 96 ->*_s0(c8,c10). [ur(36,a,57,a)]. given #82 (A,wt=6): 89 -->*_s0(b3,x) | -->*_s0(c5,x) # answer(goal). [resolve(50,a,32,b)]. given #83 (F,wt=3): 109 -->*_s0(c10,b3) # answer(goal). [resolve(91,a,37,b)]. given #84 (F,wt=3): 110 -->*_s0(c7,b4) # answer(goal). [resolve(92,a,34,b)]. given #85 (F,wt=3): 111 -->*_s0(c7,b5) # answer(goal). [resolve(93,a,34,b)]. given #86 (F,wt=3): 112 -->*_s0(b6,c4) # answer(goal). [resolve(98,a,25,b)]. given #87 (T,wt=3): 97 ->*_s0(b8,b11). [ur(28,a,63,a)]. given #88 (T,wt=3): 102 ->*_s0(b3,b6). [ur(23,a,66,a)]. given #89 (T,wt=3): 103 ->*_s0(b4,b7). [ur(24,a,74,a)]. given #90 (T,wt=3): 104 ->*_s0(b5,b8). [ur(25,a,75,a)]. given #91 (A,wt=3): 105 ->*_s0(b6,b9). [ur(26,a,76,a)]. given #92 (F,wt=3): 115 -->*_s0(b5,c5) # answer(goal). [resolve(85,a,68,a)]. given #93 (F,wt=3): 116 -->*_s0(b3,c6) # answer(goal). [resolve(86,a,50,a)]. given #94 (F,wt=3): 118 -->*_s0(c4,b6) # answer(goal). [resolve(69,a,66,a)]. given #95 (F,wt=3): 119 -->*_s0(b4,c6) # answer(goal). [resolve(69,b,86,a)]. given #96 (T,wt=3): 113 ->*_s0(b7,b10). [ur(27,a,77,a)]. given #97 (T,wt=3): 114 ->*_s0(c8,b11). [ur(36,a,78,a)]. given #98 (T,wt=3): 117 ->*_s0(c3,c6). [ur(31,a,86,a)]. given #99 (T,wt=3): 123 ->*_s0(c4,c7). [ur(32,a,87,a)]. given #100 (A,wt=6): 106 -->*_s0(b5,x) | -->*_s0(c4,x) # answer(goal). [resolve(68,a,31,b)]. given #101 (F,wt=3): 121 -->*_s0(b10,c3) # answer(goal). [resolve(100,a,29,b)]. given #102 (F,wt=3): 122 -->*_s0(c4,b7) # answer(goal). [resolve(107,a,31,b)]. given #103 (F,wt=3): 127 -->*_s0(b3,c7) # answer(goal). [resolve(89,b,87,a)]. given #104 (F,wt=3): 129 -->*_s0(b11,b3) # answer(goal). [resolve(109,a,30,b)]. given #105 (T,wt=3): 124 ->*_s0(c5,c8). [ur(33,a,94,a)]. given #106 (T,wt=3): 125 ->*_s0(c6,c9). [ur(34,a,95,a)]. given #107 (T,wt=3): 126 ->*_s0(c7,c10). [ur(35,a,96,a)]. given #108 (T,wt=3): 133 ->*_s0(b7,b11). [ur(27,a,97,a)]. given #109 (A,wt=6): 108 -->*_s0(c3,x) | -->*_s0(b6,x) # answer(goal). [resolve(68,b,25,b)]. given #110 (F,wt=3): 130 -->*_s0(c8,b4) # answer(goal). [resolve(110,a,35,b)]. given #111 (F,wt=3): 131 -->*_s0(c8,b5) # answer(goal). [resolve(111,a,35,b)]. given #112 (F,wt=3): 132 -->*_s0(b7,c4) # answer(goal). [resolve(112,a,26,b)]. given #113 (F,wt=3): 134 -->*_s0(c5,b6) # answer(goal). [resolve(102,a,89,a)]. given #114 (T,wt=3): 135 ->*_s0(b3,b7). [ur(23,a,103,a)]. given #115 (T,wt=3): 137 ->*_s0(b4,b8). [ur(24,a,104,a)]. given #116 (T,wt=3): 138 ->*_s0(b5,b9). [ur(25,a,105,a)]. given #117 (T,wt=3): 141 ->*_s0(b6,b10). [ur(26,a,113,a)]. given #118 (A,wt=6): 120 -->*_s0(b4,x) | -->*_s0(c5,x) # answer(goal). [resolve(69,b,32,b)]. given #119 (F,wt=3): 136 -->*_s0(c3,b8) # answer(goal). [resolve(104,a,68,b)]. given #120 (F,wt=3): 139 -->*_s0(b6,c5) # answer(goal). [resolve(115,a,25,b)]. given #121 (F,wt=3): 140 -->*_s0(b5,c6) # answer(goal). [resolve(119,a,24,b)]. given #122 (F,wt=3): 143 -->*_s0(b4,c7) # answer(goal). [resolve(123,a,69,b)]. given #123 (T,wt=3): 142 ->*_s0(c7,b11). [ur(35,a,114,a)]. given #124 (T,wt=3): 144 ->*_s0(c3,c7). [ur(31,a,123,a)]. given #125 (T,wt=3): 152 ->*_s0(c4,c8). [ur(32,a,124,a)]. given #126 (T,wt=3): 153 ->*_s0(c5,c9). [ur(33,a,125,a)]. given #127 (A,wt=6): 128 -->*_s0(b3,x) | -->*_s0(c6,x) # answer(goal). [resolve(89,b,33,b)]. given #128 (F,wt=3): 145 -->*_s0(c4,b8) # answer(goal). [resolve(106,a,104,a)]. given #129 (F,wt=3): 147 -->*_s0(b5,c7) # answer(goal). [resolve(106,b,123,a)]. given #130 (F,wt=3): 149 -->*_s0(b11,c3) # answer(goal). [resolve(121,a,22,b)]. given #131 (F,wt=3): 150 -->*_s0(c5,b7) # answer(goal). [resolve(122,a,32,b)]. given #132 (T,wt=3): 154 ->*_s0(c6,c10). [ur(34,a,126,a)]. given #133 (T,wt=3): 155 ->*_s0(b6,b11). [ur(26,a,133,a)]. given #134 (T,wt=3): 163 ->*_s0(b3,b8). [ur(23,a,137,a)]. given #135 (T,wt=3): 165 ->*_s0(b4,b9). [ur(24,a,138,a)]. given #136 (A,wt=6): 146 -->*_s0(c4,x) | -->*_s0(b6,x) # answer(goal). [resolve(106,a,25,b)]. given #137 (F,wt=3): 151 -->*_s0(b3,c8) # answer(goal). [resolve(124,a,89,b)]. given #138 (F,wt=3): 156 -->*_s0(b6,c6) # answer(goal). [resolve(108,a,117,a)]. given #139 (F,wt=3): 157 -->*_s0(c3,b9) # answer(goal). [resolve(108,b,105,a)]. given #140 (F,wt=3): 159 -->*_s0(c9,b4) # answer(goal). [resolve(130,a,36,b)]. given #141 (T,wt=3): 167 ->*_s0(b5,b10). [ur(25,a,141,a)]. given #142 (T,wt=3): 172 ->*_s0(c6,b11). [ur(34,a,142,a)]. given #143 (T,wt=3): 175 ->*_s0(c3,c8). [ur(31,a,152,a)]. given #144 (T,wt=3): 178 ->*_s0(c4,c9). [ur(32,a,153,a)]. given #145 (A,wt=6): 148 -->*_s0(b5,x) | -->*_s0(c5,x) # answer(goal). [resolve(106,b,32,b)]. given #146 (F,wt=3): 160 -->*_s0(c9,b5) # answer(goal). [resolve(131,a,36,b)]. given #147 (F,wt=3): 161 -->*_s0(b8,c4) # answer(goal). [resolve(132,a,27,b)]. given #148 (F,wt=3): 162 -->*_s0(c6,b6) # answer(goal). [resolve(134,a,33,b)]. given #149 (F,wt=3): 164 -->*_s0(c4,b9) # answer(goal). [resolve(138,a,106,a)]. given #150 (T,wt=3): 182 ->*_s0(c5,c10). [ur(33,a,154,a)]. given #151 (T,wt=3): 184 ->*_s0(b5,b11). [ur(25,a,155,a)]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds: goal. % Length of proof is 54. % Level of proof is 9. % Maximum clause weight is 6.000. % Given clauses 151. 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 2 (exists x2 (->*_s0(b3,x2) & ->*_s0(c3,x2))) # label(goal) # label(non_clause) # label(goal). [goal]. 3 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 4 ->_s0(b10,b11) # label(replacement). [assumption]. 5 ->_s0(b3,b4) # label(replacement). [assumption]. 6 ->_s0(b4,b5) # label(replacement). [assumption]. 7 ->_s0(b5,b6) # label(replacement). [assumption]. 8 ->_s0(b6,b7) # label(replacement). [assumption]. 9 ->_s0(b7,b8) # label(replacement). [assumption]. 10 ->_s0(b8,b9) # label(replacement). [assumption]. 11 ->_s0(b9,b10) # label(replacement). [assumption]. 12 ->_s0(c10,b11) # label(replacement). [assumption]. 13 ->_s0(c3,c4) # label(replacement). [assumption]. 14 ->_s0(c4,c5) # label(replacement). [assumption]. 15 ->_s0(c5,c6) # label(replacement). [assumption]. 16 ->_s0(c6,c7) # label(replacement). [assumption]. 17 ->_s0(c7,c8) # label(replacement). [assumption]. 18 ->_s0(c8,c9) # label(replacement). [assumption]. 19 ->_s0(c9,c10) # label(replacement). [assumption]. 20 ->*_s0(x,x) # label(reflexivity). [assumption]. 21 -->*_s0(b3,x) | -->*_s0(c3,x) # label(goal) # answer(goal). [deny(2)]. 22 -->*_s0(b11,x) | ->*_s0(b10,x). [resolve(3,a,4,a)]. 23 -->*_s0(b4,x) | ->*_s0(b3,x). [resolve(3,a,5,a)]. 24 -->*_s0(b5,x) | ->*_s0(b4,x). [resolve(3,a,6,a)]. 25 -->*_s0(b6,x) | ->*_s0(b5,x). [resolve(3,a,7,a)]. 26 -->*_s0(b7,x) | ->*_s0(b6,x). [resolve(3,a,8,a)]. 27 -->*_s0(b8,x) | ->*_s0(b7,x). [resolve(3,a,9,a)]. 28 -->*_s0(b9,x) | ->*_s0(b8,x). [resolve(3,a,10,a)]. 29 -->*_s0(b10,x) | ->*_s0(b9,x). [resolve(3,a,11,a)]. 30 -->*_s0(b11,x) | ->*_s0(c10,x). [resolve(3,a,12,a)]. 31 -->*_s0(c4,x) | ->*_s0(c3,x). [resolve(3,a,13,a)]. 32 -->*_s0(c5,x) | ->*_s0(c4,x). [resolve(3,a,14,a)]. 33 -->*_s0(c6,x) | ->*_s0(c5,x). [resolve(3,a,15,a)]. 34 -->*_s0(c7,x) | ->*_s0(c6,x). [resolve(3,a,16,a)]. 35 -->*_s0(c8,x) | ->*_s0(c7,x). [resolve(3,a,17,a)]. 36 -->*_s0(c9,x) | ->*_s0(c8,x). [resolve(3,a,18,a)]. 37 -->*_s0(c10,x) | ->*_s0(c9,x). [resolve(3,a,19,a)]. 40 ->*_s0(b10,b11). [ur(22,a,20,a)]. 41 -->*_s0(b4,x) | -->*_s0(c3,x) # answer(goal). [resolve(23,b,21,a)]. 49 ->*_s0(c10,b11). [ur(30,a,20,a)]. 63 ->*_s0(b9,b11). [ur(29,a,40,a)]. 68 -->*_s0(c3,x) | -->*_s0(b5,x) # answer(goal). [resolve(41,a,24,b)]. 78 ->*_s0(c9,b11). [ur(37,a,49,a)]. 97 ->*_s0(b8,b11). [ur(28,a,63,a)]. 106 -->*_s0(b5,x) | -->*_s0(c4,x) # answer(goal). [resolve(68,a,31,b)]. 114 ->*_s0(c8,b11). [ur(36,a,78,a)]. 133 ->*_s0(b7,b11). [ur(27,a,97,a)]. 142 ->*_s0(c7,b11). [ur(35,a,114,a)]. 148 -->*_s0(b5,x) | -->*_s0(c5,x) # answer(goal). [resolve(106,b,32,b)]. 155 ->*_s0(b6,b11). [ur(26,a,133,a)]. 172 ->*_s0(c6,b11). [ur(34,a,142,a)]. 184 ->*_s0(b5,b11). [ur(25,a,155,a)]. 197 ->*_s0(c5,b11). [ur(33,a,172,a)]. 209 $F # answer(goal). [resolve(184,a,148,a),unit_del(a,197)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=151. Generated=515. Kept=189. proofs=1. Usable=151. Sos=38. Demods=0. Limbo=0, Disabled=35. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=325. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=7. Nonunit_bsub_feature_tests=60. Megabytes=0.20. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 2696367 exit (max_proofs) Fri Jun 9 15:47:25 2023 The problem is feasible. The problem is confluent. Problem 1.3: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (REPLACEMENT-MAP (a1) (a10) (a2) (a3) (a4) (a5) (a6) (a7) (a8) (a9) (b1) (b10) (b2) (b3) (b4) (b5) (b6) (b7) (b8) (b9) (c1) (c10) (c2) (c3) (c4) (c5) (c6) (c7) (c8) (c9) (b11) (fSNonEmpty) ) (RULES a1 -> b1 a1 -> c1 a10 -> b11 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b5 a5 -> c5 a6 -> b6 a6 -> c6 a7 -> b7 a7 -> c7 a8 -> b8 a8 -> c8 a9 -> b9 a9 -> c9 b1 -> b2 b10 -> b11 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 b6 -> b7 b7 -> b8 b8 -> b9 b9 -> b10 c1 -> c2 c10 -> b11 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> c6 c6 -> c7 c7 -> c8 c8 -> c9 c9 -> c10 ) Critical Pairs: => Not trivial, Overlay, Proper, NW0, N3 Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Brute Force Joinability Procedure: -> Rewritings: s: b8 Nodes: [0,1,2,3] Edges: [(0,1),(1,2),(2,3)] ID: 0 => ('b8', D0) ID: 1 => ('b9', D1, R28, P[], S{}), NR: 'b9' ID: 2 => ('b10', D2, R29, P[], S{}), NR: 'b10' ID: 3 => ('b11', D3, R21, P[], S{}), NR: 'b11' t: c8 Nodes: [0,1,2,3] Edges: [(0,1),(1,2),(2,3)] ID: 0 => ('c8', D0) ID: 1 => ('c9', D1, R38, P[], S{}), NR: 'c9' ID: 2 => ('c10', D2, R39, P[], S{}), NR: 'c10' ID: 3 => ('b11', D3, R31, P[], S{}), NR: 'b11' SNodesPath: b8 -> b9 -> b10 -> b11 TNodesPath: c8 -> c9 -> c10 -> b11 b8 ->* b11 *<- c8 "Joinable" The problem is confluent. Problem 1.4: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (REPLACEMENT-MAP (a1) (a10) (a2) (a3) (a4) (a5) (a6) (a7) (a8) (a9) (b1) (b10) (b2) (b3) (b4) (b5) (b6) (b7) (b8) (b9) (c1) (c10) (c2) (c3) (c4) (c5) (c6) (c7) (c8) (c9) (b11) (fSNonEmpty) ) (RULES a1 -> b1 a1 -> c1 a10 -> b11 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b5 a5 -> c5 a6 -> b6 a6 -> c6 a7 -> b7 a7 -> c7 a8 -> b8 a8 -> c8 a9 -> b9 a9 -> c9 b1 -> b2 b10 -> b11 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 b6 -> b7 b7 -> b8 b8 -> b9 b9 -> b10 c1 -> c2 c10 -> b11 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> c6 c6 -> c7 c7 -> c8 c8 -> c9 c9 -> c10 ) Critical Pairs: => Not trivial, Overlay, Proper, NW0, N4 Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Brute Force Joinability Procedure: -> Rewritings: s: b5 Nodes: [0,1,2,3,4,5,6] Edges: [(0,1),(1,2),(2,3),(3,4),(4,5),(5,6)] ID: 0 => ('b5', D0) ID: 1 => ('b6', D1, R25, P[], S{}), NR: 'b6' ID: 2 => ('b7', D2, R26, P[], S{}), NR: 'b7' ID: 3 => ('b8', D3, R27, P[], S{}), NR: 'b8' ID: 4 => ('b9', D4, R28, P[], S{}), NR: 'b9' ID: 5 => ('b10', D5, R29, P[], S{}), NR: 'b10' ID: 6 => ('b11', D6, R21, P[], S{}), NR: 'b11' t: c5 Nodes: [0,1,2,3,4,5,6] Edges: [(0,1),(1,2),(2,3),(3,4),(4,5),(5,6)] ID: 0 => ('c5', D0) ID: 1 => ('c6', D1, R35, P[], S{}), NR: 'c6' ID: 2 => ('c7', D2, R36, P[], S{}), NR: 'c7' ID: 3 => ('c8', D3, R37, P[], S{}), NR: 'c8' ID: 4 => ('c9', D4, R38, P[], S{}), NR: 'c9' ID: 5 => ('c10', D5, R39, P[], S{}), NR: 'c10' ID: 6 => ('b11', D6, R31, P[], S{}), NR: 'b11' SNodesPath: b5 -> b6 -> b7 -> b8 -> b9 -> b10 -> b11 TNodesPath: c5 -> c6 -> c7 -> c8 -> c9 -> c10 -> b11 b5 ->* b11 *<- c5 "Joinable" The problem is confluent. Problem 1.5: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (REPLACEMENT-MAP (a1) (a10) (a2) (a3) (a4) (a5) (a6) (a7) (a8) (a9) (b1) (b10) (b2) (b3) (b4) (b5) (b6) (b7) (b8) (b9) (c1) (c10) (c2) (c3) (c4) (c5) (c6) (c7) (c8) (c9) (b11) (fSNonEmpty) ) (RULES a1 -> b1 a1 -> c1 a10 -> b11 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b5 a5 -> c5 a6 -> b6 a6 -> c6 a7 -> b7 a7 -> c7 a8 -> b8 a8 -> c8 a9 -> b9 a9 -> c9 b1 -> b2 b10 -> b11 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 b6 -> b7 b7 -> b8 b8 -> b9 b9 -> b10 c1 -> c2 c10 -> b11 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> c6 c6 -> c7 c7 -> c8 c8 -> c9 c9 -> c10 ) Critical Pairs: => Not trivial, Overlay, Proper, NW0, N5 Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet InfChecker Procedure: Infeasible convergence? NO Problem 1: Infeasibility Problem: [(VAR vNonEmpty vNonEmpty z0) (STRATEGY CONTEXTSENSITIVE (a1) (a10) (a2) (a3) (a4) (a5) (a6) (a7) (a8) (a9) (b1) (b10) (b2) (b3) (b4) (b5) (b6) (b7) (b8) (b9) (c1) (c10) (c2) (c3) (c4) (c5) (c6) (c7) (c8) (c9) (b11) (fSNonEmpty) ) (RULES a1 -> b1 a1 -> c1 a10 -> b11 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b5 a5 -> c5 a6 -> b6 a6 -> c6 a7 -> b7 a7 -> c7 a8 -> b8 a8 -> c8 a9 -> b9 a9 -> c9 b1 -> b2 b10 -> b11 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 b6 -> b7 b7 -> b8 b8 -> b9 b9 -> b10 c1 -> c2 c10 -> b11 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> c6 c6 -> c7 c7 -> c8 c8 -> c9 c9 -> c10 )] Infeasibility Conditions: b1 ->* z0, c1 ->* z0 Problem 1: Obtaining a proof using Prover9: -> Prover9 Output: ============================== Prover9 =============================== Prover9 (64) version 2009-11A, November 2009. Process 2696439 was started by shintani on shintani-XPS-13-9310, Fri Jun 9 15:47:25 2023 The command was "./prover9 -f /tmp/prover92696402-0.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file /tmp/prover92696402-0.in assign(max_seconds,20). formulas(assumptions). ->_s0(b1,b2) # label(replacement). ->_s0(b10,b11) # label(replacement). ->_s0(b2,b3) # label(replacement). ->_s0(b3,b4) # label(replacement). ->_s0(b4,b5) # label(replacement). ->_s0(b5,b6) # label(replacement). ->_s0(b6,b7) # label(replacement). ->_s0(b7,b8) # label(replacement). ->_s0(b8,b9) # label(replacement). ->_s0(b9,b10) # label(replacement). ->_s0(c1,c2) # label(replacement). ->_s0(c10,b11) # label(replacement). ->_s0(c2,c3) # label(replacement). ->_s0(c3,c4) # label(replacement). ->_s0(c4,c5) # label(replacement). ->_s0(c5,c6) # label(replacement). ->_s0(c6,c7) # label(replacement). ->_s0(c7,c8) # label(replacement). ->_s0(c8,c9) # label(replacement). ->_s0(c9,c10) # label(replacement). ->*_s0(x,x) # label(reflexivity). ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). end_of_list. formulas(goals). (exists x2 (->*_s0(b1,x2) & ->*_s0(c1,x2))) # label(goal). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 2 (exists x2 (->*_s0(b1,x2) & ->*_s0(c1,x2))) # label(goal) # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). ->_s0(b1,b2) # label(replacement). [assumption]. ->_s0(b10,b11) # label(replacement). [assumption]. ->_s0(b2,b3) # label(replacement). [assumption]. ->_s0(b3,b4) # label(replacement). [assumption]. ->_s0(b4,b5) # label(replacement). [assumption]. ->_s0(b5,b6) # label(replacement). [assumption]. ->_s0(b6,b7) # label(replacement). [assumption]. ->_s0(b7,b8) # label(replacement). [assumption]. ->_s0(b8,b9) # label(replacement). [assumption]. ->_s0(b9,b10) # label(replacement). [assumption]. ->_s0(c1,c2) # label(replacement). [assumption]. ->_s0(c10,b11) # label(replacement). [assumption]. ->_s0(c2,c3) # label(replacement). [assumption]. ->_s0(c3,c4) # label(replacement). [assumption]. ->_s0(c4,c5) # label(replacement). [assumption]. ->_s0(c5,c6) # label(replacement). [assumption]. ->_s0(c6,c7) # label(replacement). [assumption]. ->_s0(c7,c8) # label(replacement). [assumption]. ->_s0(c8,c9) # label(replacement). [assumption]. ->_s0(c9,c10) # label(replacement). [assumption]. ->*_s0(x,x) # label(reflexivity). [assumption]. -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. -->*_s0(b1,x) | -->*_s0(c1,x) # label(goal). [deny(2)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating ->_s0/2 3 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 4 ->_s0(b1,b2) # label(replacement). [assumption]. 5 ->_s0(b10,b11) # label(replacement). [assumption]. 6 ->_s0(b2,b3) # label(replacement). [assumption]. 7 ->_s0(b3,b4) # label(replacement). [assumption]. 8 ->_s0(b4,b5) # label(replacement). [assumption]. 9 ->_s0(b5,b6) # label(replacement). [assumption]. 10 ->_s0(b6,b7) # label(replacement). [assumption]. 11 ->_s0(b7,b8) # label(replacement). [assumption]. 12 ->_s0(b8,b9) # label(replacement). [assumption]. 13 ->_s0(b9,b10) # label(replacement). [assumption]. 14 ->_s0(c1,c2) # label(replacement). [assumption]. 15 ->_s0(c10,b11) # label(replacement). [assumption]. 16 ->_s0(c2,c3) # label(replacement). [assumption]. 17 ->_s0(c3,c4) # label(replacement). [assumption]. 18 ->_s0(c4,c5) # label(replacement). [assumption]. 19 ->_s0(c5,c6) # label(replacement). [assumption]. 20 ->_s0(c6,c7) # label(replacement). [assumption]. 21 ->_s0(c7,c8) # label(replacement). [assumption]. 22 ->_s0(c8,c9) # label(replacement). [assumption]. 23 ->_s0(c9,c10) # label(replacement). [assumption]. Derived: -->*_s0(b2,x) | ->*_s0(b1,x). [resolve(3,a,4,a)]. Derived: -->*_s0(b11,x) | ->*_s0(b10,x). [resolve(3,a,5,a)]. Derived: -->*_s0(b3,x) | ->*_s0(b2,x). [resolve(3,a,6,a)]. Derived: -->*_s0(b4,x) | ->*_s0(b3,x). [resolve(3,a,7,a)]. Derived: -->*_s0(b5,x) | ->*_s0(b4,x). [resolve(3,a,8,a)]. Derived: -->*_s0(b6,x) | ->*_s0(b5,x). [resolve(3,a,9,a)]. Derived: -->*_s0(b7,x) | ->*_s0(b6,x). [resolve(3,a,10,a)]. Derived: -->*_s0(b8,x) | ->*_s0(b7,x). [resolve(3,a,11,a)]. Derived: -->*_s0(b9,x) | ->*_s0(b8,x). [resolve(3,a,12,a)]. Derived: -->*_s0(b10,x) | ->*_s0(b9,x). [resolve(3,a,13,a)]. Derived: -->*_s0(c2,x) | ->*_s0(c1,x). [resolve(3,a,14,a)]. Derived: -->*_s0(b11,x) | ->*_s0(c10,x). [resolve(3,a,15,a)]. Derived: -->*_s0(c3,x) | ->*_s0(c2,x). [resolve(3,a,16,a)]. Derived: -->*_s0(c4,x) | ->*_s0(c3,x). [resolve(3,a,17,a)]. Derived: -->*_s0(c5,x) | ->*_s0(c4,x). [resolve(3,a,18,a)]. Derived: -->*_s0(c6,x) | ->*_s0(c5,x). [resolve(3,a,19,a)]. Derived: -->*_s0(c7,x) | ->*_s0(c6,x). [resolve(3,a,20,a)]. Derived: -->*_s0(c8,x) | ->*_s0(c7,x). [resolve(3,a,21,a)]. Derived: -->*_s0(c9,x) | ->*_s0(c8,x). [resolve(3,a,22,a)]. Derived: -->*_s0(c10,x) | ->*_s0(c9,x). [resolve(3,a,23,a)]. ============================== end predicate elimination ============= Auto_denials: % copying label goal to answer in negative clause Term ordering decisions: Predicate symbol precedence: predicate_order([ ->*_s0 ]). Function symbol precedence: function_order([ b10, b2, b3, b4, b5, b6, b7, b8, b9, c10, c2, c3, c4, c5, c6, c7, c8, c9, b11, b1, c1 ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(neg_binary_resolution). % (HNE depth_diff=0) % clear(ordered_res). % (HNE depth_diff=0) % set(ur_resolution). % (HNE depth_diff=0) % set(ur_resolution) -> set(pos_ur_resolution). % set(ur_resolution) -> set(neg_ur_resolution). Auto_process settings: % set(unit_deletion). % (Horn set with negative nonunits) kept: 24 ->*_s0(x,x) # label(reflexivity). [assumption]. kept: 25 -->*_s0(b1,x) | -->*_s0(c1,x) # label(goal) # answer(goal). [deny(2)]. kept: 26 -->*_s0(b2,x) | ->*_s0(b1,x). [resolve(3,a,4,a)]. kept: 27 -->*_s0(b11,x) | ->*_s0(b10,x). [resolve(3,a,5,a)]. kept: 28 -->*_s0(b3,x) | ->*_s0(b2,x). [resolve(3,a,6,a)]. kept: 29 -->*_s0(b4,x) | ->*_s0(b3,x). [resolve(3,a,7,a)]. kept: 30 -->*_s0(b5,x) | ->*_s0(b4,x). [resolve(3,a,8,a)]. kept: 31 -->*_s0(b6,x) | ->*_s0(b5,x). [resolve(3,a,9,a)]. kept: 32 -->*_s0(b7,x) | ->*_s0(b6,x). [resolve(3,a,10,a)]. kept: 33 -->*_s0(b8,x) | ->*_s0(b7,x). [resolve(3,a,11,a)]. kept: 34 -->*_s0(b9,x) | ->*_s0(b8,x). [resolve(3,a,12,a)]. kept: 35 -->*_s0(b10,x) | ->*_s0(b9,x). [resolve(3,a,13,a)]. kept: 36 -->*_s0(c2,x) | ->*_s0(c1,x). [resolve(3,a,14,a)]. kept: 37 -->*_s0(b11,x) | ->*_s0(c10,x). [resolve(3,a,15,a)]. kept: 38 -->*_s0(c3,x) | ->*_s0(c2,x). [resolve(3,a,16,a)]. kept: 39 -->*_s0(c4,x) | ->*_s0(c3,x). [resolve(3,a,17,a)]. kept: 40 -->*_s0(c5,x) | ->*_s0(c4,x). [resolve(3,a,18,a)]. kept: 41 -->*_s0(c6,x) | ->*_s0(c5,x). [resolve(3,a,19,a)]. kept: 42 -->*_s0(c7,x) | ->*_s0(c6,x). [resolve(3,a,20,a)]. kept: 43 -->*_s0(c8,x) | ->*_s0(c7,x). [resolve(3,a,21,a)]. kept: 44 -->*_s0(c9,x) | ->*_s0(c8,x). [resolve(3,a,22,a)]. kept: 45 -->*_s0(c10,x) | ->*_s0(c9,x). [resolve(3,a,23,a)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 24 ->*_s0(x,x) # label(reflexivity). [assumption]. 25 -->*_s0(b1,x) | -->*_s0(c1,x) # label(goal) # answer(goal). [deny(2)]. 26 -->*_s0(b2,x) | ->*_s0(b1,x). [resolve(3,a,4,a)]. 27 -->*_s0(b11,x) | ->*_s0(b10,x). [resolve(3,a,5,a)]. 28 -->*_s0(b3,x) | ->*_s0(b2,x). [resolve(3,a,6,a)]. 29 -->*_s0(b4,x) | ->*_s0(b3,x). [resolve(3,a,7,a)]. 30 -->*_s0(b5,x) | ->*_s0(b4,x). [resolve(3,a,8,a)]. 31 -->*_s0(b6,x) | ->*_s0(b5,x). [resolve(3,a,9,a)]. 32 -->*_s0(b7,x) | ->*_s0(b6,x). [resolve(3,a,10,a)]. 33 -->*_s0(b8,x) | ->*_s0(b7,x). [resolve(3,a,11,a)]. 34 -->*_s0(b9,x) | ->*_s0(b8,x). [resolve(3,a,12,a)]. 35 -->*_s0(b10,x) | ->*_s0(b9,x). [resolve(3,a,13,a)]. 36 -->*_s0(c2,x) | ->*_s0(c1,x). [resolve(3,a,14,a)]. 37 -->*_s0(b11,x) | ->*_s0(c10,x). [resolve(3,a,15,a)]. 38 -->*_s0(c3,x) | ->*_s0(c2,x). [resolve(3,a,16,a)]. 39 -->*_s0(c4,x) | ->*_s0(c3,x). [resolve(3,a,17,a)]. 40 -->*_s0(c5,x) | ->*_s0(c4,x). [resolve(3,a,18,a)]. 41 -->*_s0(c6,x) | ->*_s0(c5,x). [resolve(3,a,19,a)]. 42 -->*_s0(c7,x) | ->*_s0(c6,x). [resolve(3,a,20,a)]. 43 -->*_s0(c8,x) | ->*_s0(c7,x). [resolve(3,a,21,a)]. 44 -->*_s0(c9,x) | ->*_s0(c8,x). [resolve(3,a,22,a)]. 45 -->*_s0(c10,x) | ->*_s0(c9,x). [resolve(3,a,23,a)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=3): 24 ->*_s0(x,x) # label(reflexivity). [assumption]. given #2 (I,wt=6): 25 -->*_s0(b1,x) | -->*_s0(c1,x) # label(goal) # answer(goal). [deny(2)]. given #3 (I,wt=6): 26 -->*_s0(b2,x) | ->*_s0(b1,x). [resolve(3,a,4,a)]. given #4 (I,wt=6): 27 -->*_s0(b11,x) | ->*_s0(b10,x). [resolve(3,a,5,a)]. given #5 (I,wt=6): 28 -->*_s0(b3,x) | ->*_s0(b2,x). [resolve(3,a,6,a)]. given #6 (I,wt=6): 29 -->*_s0(b4,x) | ->*_s0(b3,x). [resolve(3,a,7,a)]. given #7 (I,wt=6): 30 -->*_s0(b5,x) | ->*_s0(b4,x). [resolve(3,a,8,a)]. given #8 (I,wt=6): 31 -->*_s0(b6,x) | ->*_s0(b5,x). [resolve(3,a,9,a)]. given #9 (I,wt=6): 32 -->*_s0(b7,x) | ->*_s0(b6,x). [resolve(3,a,10,a)]. given #10 (I,wt=6): 33 -->*_s0(b8,x) | ->*_s0(b7,x). [resolve(3,a,11,a)]. given #11 (I,wt=6): 34 -->*_s0(b9,x) | ->*_s0(b8,x). [resolve(3,a,12,a)]. given #12 (I,wt=6): 35 -->*_s0(b10,x) | ->*_s0(b9,x). [resolve(3,a,13,a)]. given #13 (I,wt=6): 36 -->*_s0(c2,x) | ->*_s0(c1,x). [resolve(3,a,14,a)]. given #14 (I,wt=6): 37 -->*_s0(b11,x) | ->*_s0(c10,x). [resolve(3,a,15,a)]. given #15 (I,wt=6): 38 -->*_s0(c3,x) | ->*_s0(c2,x). [resolve(3,a,16,a)]. given #16 (I,wt=6): 39 -->*_s0(c4,x) | ->*_s0(c3,x). [resolve(3,a,17,a)]. given #17 (I,wt=6): 40 -->*_s0(c5,x) | ->*_s0(c4,x). [resolve(3,a,18,a)]. given #18 (I,wt=6): 41 -->*_s0(c6,x) | ->*_s0(c5,x). [resolve(3,a,19,a)]. given #19 (I,wt=6): 42 -->*_s0(c7,x) | ->*_s0(c6,x). [resolve(3,a,20,a)]. given #20 (I,wt=6): 43 -->*_s0(c8,x) | ->*_s0(c7,x). [resolve(3,a,21,a)]. given #21 (I,wt=6): 44 -->*_s0(c9,x) | ->*_s0(c8,x). [resolve(3,a,22,a)]. given #22 (I,wt=6): 45 -->*_s0(c10,x) | ->*_s0(c9,x). [resolve(3,a,23,a)]. given #23 (A,wt=3): 46 -->*_s0(c1,b1) # answer(goal). [resolve(25,a,24,a)]. given #24 (F,wt=3): 47 -->*_s0(b1,c1) # answer(goal). [resolve(25,b,24,a)]. given #25 (F,wt=3): 70 -->*_s0(c2,b1) # answer(goal). [resolve(46,a,36,b)]. given #26 (F,wt=3): 71 -->*_s0(b2,c1) # answer(goal). [resolve(47,a,26,b)]. given #27 (F,wt=3): 72 -->*_s0(c3,b1) # answer(goal). [resolve(70,a,38,b)]. given #28 (T,wt=3): 49 ->*_s0(b1,b2). [ur(26,a,24,a)]. given #29 (T,wt=3): 50 ->*_s0(b10,b11). [ur(27,a,24,a)]. given #30 (T,wt=3): 51 ->*_s0(b2,b3). [ur(28,a,24,a)]. given #31 (T,wt=3): 52 ->*_s0(b3,b4). [ur(29,a,24,a)]. given #32 (A,wt=6): 48 -->*_s0(b2,x) | -->*_s0(c1,x) # answer(goal). [resolve(26,b,25,a)]. given #33 (F,wt=3): 73 -->*_s0(b3,c1) # answer(goal). [resolve(71,a,28,b)]. given #34 (F,wt=3): 74 -->*_s0(c4,b1) # answer(goal). [resolve(72,a,39,b)]. given #35 (F,wt=3): 75 -->*_s0(c1,b2) # answer(goal). [resolve(49,a,25,a)]. given #36 (F,wt=3): 79 -->*_s0(c1,b3) # answer(goal). [resolve(48,a,51,a)]. given #37 (T,wt=3): 53 ->*_s0(b4,b5). [ur(30,a,24,a)]. given #38 (T,wt=3): 54 ->*_s0(b5,b6). [ur(31,a,24,a)]. given #39 (T,wt=3): 55 ->*_s0(b6,b7). [ur(32,a,24,a)]. given #40 (T,wt=3): 56 ->*_s0(b7,b8). [ur(33,a,24,a)]. given #41 (A,wt=3): 57 ->*_s0(b8,b9). [ur(34,a,24,a)]. given #42 (F,wt=3): 82 -->*_s0(b4,c1) # answer(goal). [resolve(73,a,29,b)]. given #43 (F,wt=3): 83 -->*_s0(c5,b1) # answer(goal). [resolve(74,a,40,b)]. given #44 (F,wt=3): 84 -->*_s0(c2,b2) # answer(goal). [resolve(75,a,36,b)]. given #45 (F,wt=3): 85 -->*_s0(c2,b3) # answer(goal). [resolve(79,a,36,b)]. given #46 (T,wt=3): 58 ->*_s0(b9,b10). [ur(35,a,24,a)]. given #47 (T,wt=3): 60 ->*_s0(c1,c2). [ur(36,a,24,a)]. given #48 (T,wt=3): 61 ->*_s0(c10,b11). [ur(37,a,24,a)]. given #49 (T,wt=3): 62 ->*_s0(c2,c3). [ur(38,a,24,a)]. given #50 (A,wt=6): 59 -->*_s0(c2,x) | -->*_s0(b1,x) # answer(goal). [resolve(36,b,25,b)]. given #51 (F,wt=3): 91 -->*_s0(b5,c1) # answer(goal). [resolve(82,a,30,b)]. given #52 (F,wt=3): 92 -->*_s0(c6,b1) # answer(goal). [resolve(83,a,41,b)]. given #53 (F,wt=3): 93 -->*_s0(c3,b2) # answer(goal). [resolve(84,a,38,b)]. given #54 (F,wt=3): 94 -->*_s0(c3,b3) # answer(goal). [resolve(85,a,38,b)]. given #55 (T,wt=3): 63 ->*_s0(c3,c4). [ur(39,a,24,a)]. given #56 (T,wt=3): 64 ->*_s0(c4,c5). [ur(40,a,24,a)]. given #57 (T,wt=3): 65 ->*_s0(c5,c6). [ur(41,a,24,a)]. given #58 (T,wt=3): 66 ->*_s0(c6,c7). [ur(42,a,24,a)]. given #59 (A,wt=3): 67 ->*_s0(c7,c8). [ur(43,a,24,a)]. given #60 (F,wt=3): 96 -->*_s0(b2,c2) # answer(goal). [resolve(60,a,48,b)]. given #61 (F,wt=3): 97 -->*_s0(b1,c2) # answer(goal). [resolve(60,a,25,b)]. given #62 (F,wt=3): 100 -->*_s0(b1,c3) # answer(goal). [resolve(59,a,62,a)]. given #63 (F,wt=3): 102 -->*_s0(b6,c1) # answer(goal). [resolve(91,a,31,b)]. given #64 (T,wt=3): 68 ->*_s0(c8,c9). [ur(44,a,24,a)]. given #65 (T,wt=3): 69 ->*_s0(c9,c10). [ur(45,a,24,a)]. given #66 (T,wt=3): 76 ->*_s0(b9,b11). [ur(35,a,50,a)]. given #67 (T,wt=3): 77 ->*_s0(b1,b3). [ur(26,a,51,a)]. given #68 (A,wt=3): 78 ->*_s0(b2,b4). [ur(28,a,52,a)]. given #69 (F,wt=3): 103 -->*_s0(c7,b1) # answer(goal). [resolve(92,a,42,b)]. given #70 (F,wt=3): 104 -->*_s0(c4,b2) # answer(goal). [resolve(93,a,39,b)]. given #71 (F,wt=3): 105 -->*_s0(c4,b3) # answer(goal). [resolve(94,a,39,b)]. given #72 (F,wt=3): 111 -->*_s0(b3,c2) # answer(goal). [resolve(96,a,28,b)]. given #73 (T,wt=3): 86 ->*_s0(b3,b5). [ur(29,a,53,a)]. given #74 (T,wt=3): 87 ->*_s0(b4,b6). [ur(30,a,54,a)]. given #75 (T,wt=3): 88 ->*_s0(b5,b7). [ur(31,a,55,a)]. given #76 (T,wt=3): 89 ->*_s0(b6,b8). [ur(32,a,56,a)]. given #77 (A,wt=6): 80 -->*_s0(c1,x) | -->*_s0(b3,x) # answer(goal). [resolve(48,a,28,b)]. given #78 (F,wt=3): 112 -->*_s0(b2,c3) # answer(goal). [resolve(100,a,26,b)]. given #79 (F,wt=3): 113 -->*_s0(b7,c1) # answer(goal). [resolve(102,a,32,b)]. given #80 (F,wt=3): 117 -->*_s0(c1,b4) # answer(goal). [resolve(78,a,48,a)]. given #81 (F,wt=3): 119 -->*_s0(c8,b1) # answer(goal). [resolve(103,a,43,b)]. given #82 (T,wt=3): 90 ->*_s0(b7,b9). [ur(33,a,57,a)]. given #83 (T,wt=3): 95 ->*_s0(b8,b10). [ur(34,a,58,a)]. given #84 (T,wt=3): 98 ->*_s0(c9,b11). [ur(45,a,61,a)]. given #85 (T,wt=3): 99 ->*_s0(c1,c3). [ur(36,a,62,a)]. given #86 (A,wt=6): 81 -->*_s0(b2,x) | -->*_s0(c2,x) # answer(goal). [resolve(48,b,36,b)]. given #87 (F,wt=3): 120 -->*_s0(c5,b2) # answer(goal). [resolve(104,a,40,b)]. given #88 (F,wt=3): 121 -->*_s0(c5,b3) # answer(goal). [resolve(105,a,40,b)]. given #89 (F,wt=3): 122 -->*_s0(b4,c2) # answer(goal). [resolve(111,a,29,b)]. given #90 (F,wt=3): 128 -->*_s0(c1,b5) # answer(goal). [resolve(80,b,86,a)]. given #91 (T,wt=3): 106 ->*_s0(c2,c4). [ur(38,a,63,a)]. given #92 (T,wt=3): 107 ->*_s0(c3,c5). [ur(39,a,64,a)]. given #93 (T,wt=3): 108 ->*_s0(c4,c6). [ur(40,a,65,a)]. given #94 (T,wt=3): 109 ->*_s0(c5,c7). [ur(41,a,66,a)]. given #95 (A,wt=6): 101 -->*_s0(b1,x) | -->*_s0(c3,x) # answer(goal). [resolve(59,a,38,b)]. given #96 (F,wt=3): 130 -->*_s0(b3,c3) # answer(goal). [resolve(112,a,28,b)]. given #97 (F,wt=3): 131 -->*_s0(b8,c1) # answer(goal). [resolve(113,a,33,b)]. given #98 (F,wt=3): 132 -->*_s0(c2,b4) # answer(goal). [resolve(117,a,36,b)]. given #99 (F,wt=3): 133 -->*_s0(c9,b1) # answer(goal). [resolve(119,a,44,b)]. given #100 (T,wt=3): 110 ->*_s0(c6,c8). [ur(42,a,67,a)]. given #101 (T,wt=3): 114 ->*_s0(c7,c9). [ur(43,a,68,a)]. given #102 (T,wt=3): 115 ->*_s0(c8,c10). [ur(44,a,69,a)]. given #103 (T,wt=3): 116 ->*_s0(b8,b11). [ur(34,a,76,a)]. given #104 (A,wt=3): 118 ->*_s0(b1,b4). [ur(26,a,78,a)]. given #105 (F,wt=3): 138 -->*_s0(c6,b2) # answer(goal). [resolve(120,a,41,b)]. given #106 (F,wt=3): 139 -->*_s0(c6,b3) # answer(goal). [resolve(121,a,41,b)]. given #107 (F,wt=3): 140 -->*_s0(b5,c2) # answer(goal). [resolve(122,a,30,b)]. given #108 (F,wt=3): 141 -->*_s0(c2,b5) # answer(goal). [resolve(128,a,36,b)]. given #109 (T,wt=3): 123 ->*_s0(b2,b5). [ur(28,a,86,a)]. given #110 (T,wt=3): 124 ->*_s0(b3,b6). [ur(29,a,87,a)]. given #111 (T,wt=3): 125 ->*_s0(b4,b7). [ur(30,a,88,a)]. given #112 (T,wt=3): 126 ->*_s0(b5,b8). [ur(31,a,89,a)]. given #113 (A,wt=6): 127 -->*_s0(b3,x) | -->*_s0(c2,x) # answer(goal). [resolve(80,a,36,b)]. given #114 (F,wt=3): 142 -->*_s0(b2,c4) # answer(goal). [resolve(106,a,81,b)]. given #115 (F,wt=3): 143 -->*_s0(b1,c4) # answer(goal). [resolve(106,a,59,a)]. given #116 (F,wt=3): 148 -->*_s0(b1,c5) # answer(goal). [resolve(101,b,107,a)]. given #117 (F,wt=3): 150 -->*_s0(b4,c3) # answer(goal). [resolve(130,a,29,b)]. given #118 (T,wt=3): 134 ->*_s0(b6,b9). [ur(32,a,90,a)]. given #119 (T,wt=3): 135 ->*_s0(b7,b10). [ur(33,a,95,a)]. given #120 (T,wt=3): 136 ->*_s0(c8,b11). [ur(44,a,98,a)]. given #121 (T,wt=3): 144 ->*_s0(c1,c4). [ur(36,a,106,a)]. given #122 (A,wt=6): 129 -->*_s0(c1,x) | -->*_s0(b4,x) # answer(goal). [resolve(80,b,29,b)]. given #123 (F,wt=3): 151 -->*_s0(b9,c1) # answer(goal). [resolve(131,a,34,b)]. given #124 (F,wt=3): 152 -->*_s0(c3,b4) # answer(goal). [resolve(132,a,38,b)]. given #125 (F,wt=3): 153 -->*_s0(c10,b1) # answer(goal). [resolve(133,a,45,b)]. given #126 (F,wt=3): 158 -->*_s0(c7,b2) # answer(goal). [resolve(138,a,42,b)]. given #127 (T,wt=3): 145 ->*_s0(c2,c5). [ur(38,a,107,a)]. given #128 (T,wt=3): 146 ->*_s0(c3,c6). [ur(39,a,108,a)]. given #129 (T,wt=3): 147 ->*_s0(c4,c7). [ur(40,a,109,a)]. given #130 (T,wt=3): 154 ->*_s0(c5,c8). [ur(41,a,110,a)]. given #131 (A,wt=6): 137 -->*_s0(b2,x) | -->*_s0(c3,x) # answer(goal). [resolve(81,b,38,b)]. given #132 (F,wt=3): 159 -->*_s0(c7,b3) # answer(goal). [resolve(139,a,42,b)]. given #133 (F,wt=3): 160 -->*_s0(b6,c2) # answer(goal). [resolve(140,a,31,b)]. given #134 (F,wt=3): 161 -->*_s0(c3,b5) # answer(goal). [resolve(141,a,38,b)]. given #135 (F,wt=3): 163 -->*_s0(c1,b6) # answer(goal). [resolve(124,a,80,b)]. given #136 (T,wt=3): 155 ->*_s0(c6,c9). [ur(42,a,114,a)]. given #137 (T,wt=3): 156 ->*_s0(c7,c10). [ur(43,a,115,a)]. given #138 (T,wt=3): 157 ->*_s0(b7,b11). [ur(33,a,116,a)]. given #139 (T,wt=3): 162 ->*_s0(b1,b5). [ur(26,a,123,a)]. given #140 (A,wt=6): 149 -->*_s0(b1,x) | -->*_s0(c4,x) # answer(goal). [resolve(101,b,39,b)]. given #141 (F,wt=3): 167 -->*_s0(c2,b6) # answer(goal). [resolve(127,a,124,a)]. given #142 (F,wt=3): 169 -->*_s0(b3,c4) # answer(goal). [resolve(127,b,106,a)]. given #143 (F,wt=3): 171 -->*_s0(b2,c5) # answer(goal). [resolve(148,a,26,b)]. given #144 (F,wt=3): 172 -->*_s0(b5,c3) # answer(goal). [resolve(150,a,30,b)]. given #145 (T,wt=3): 164 ->*_s0(b2,b6). [ur(28,a,124,a)]. given #146 (T,wt=3): 165 ->*_s0(b3,b7). [ur(29,a,125,a)]. given #147 (T,wt=3): 166 ->*_s0(b4,b8). [ur(30,a,126,a)]. given #148 (T,wt=3): 173 ->*_s0(b5,b9). [ur(31,a,134,a)]. given #149 (A,wt=6): 168 -->*_s0(c2,x) | -->*_s0(b4,x) # answer(goal). [resolve(127,a,29,b)]. given #150 (F,wt=3): 176 -->*_s0(b4,c4) # answer(goal). [resolve(129,a,144,a)]. given #151 (F,wt=3): 177 -->*_s0(c1,b7) # answer(goal). [resolve(129,b,125,a)]. given #152 (F,wt=3): 179 -->*_s0(b10,c1) # answer(goal). [resolve(151,a,35,b)]. given #153 (F,wt=3): 180 -->*_s0(c4,b4) # answer(goal). [resolve(152,a,39,b)]. given #154 (T,wt=3): 174 ->*_s0(b6,b10). [ur(32,a,135,a)]. given #155 (T,wt=3): 175 ->*_s0(c7,b11). [ur(43,a,136,a)]. given #156 (T,wt=3): 184 ->*_s0(c1,c5). [ur(36,a,145,a)]. given #157 (T,wt=3): 186 ->*_s0(c2,c6). [ur(38,a,146,a)]. given #158 (A,wt=6): 170 -->*_s0(b3,x) | -->*_s0(c3,x) # answer(goal). [resolve(127,b,38,b)]. given #159 (F,wt=3): 181 -->*_s0(b11,b1) # answer(goal). [resolve(153,a,37,b)]. given #160 (F,wt=3): 182 -->*_s0(c8,b2) # answer(goal). [resolve(158,a,43,b)]. given #161 (F,wt=3): 183 -->*_s0(b3,c5) # answer(goal). [resolve(145,a,127,b)]. given #162 (F,wt=3): 185 -->*_s0(b1,c6) # answer(goal). [resolve(146,a,101,b)]. given #163 (T,wt=3): 187 ->*_s0(c3,c7). [ur(39,a,147,a)]. given #164 (T,wt=3): 188 ->*_s0(c4,c8). [ur(40,a,154,a)]. given #165 (T,wt=3): 194 ->*_s0(c5,c9). [ur(41,a,155,a)]. given #166 (T,wt=3): 195 ->*_s0(c6,c10). [ur(42,a,156,a)]. given #167 (A,wt=6): 178 -->*_s0(c1,x) | -->*_s0(b5,x) # answer(goal). [resolve(129,b,30,b)]. given #168 (F,wt=3): 189 -->*_s0(b2,c6) # answer(goal). [resolve(137,b,146,a)]. given #169 (F,wt=3): 191 -->*_s0(c8,b3) # answer(goal). [resolve(159,a,43,b)]. given #170 (F,wt=3): 192 -->*_s0(b7,c2) # answer(goal). [resolve(160,a,32,b)]. given #171 (F,wt=3): 193 -->*_s0(c4,b5) # answer(goal). [resolve(161,a,39,b)]. given #172 (T,wt=3): 196 ->*_s0(b6,b11). [ur(32,a,157,a)]. given #173 (T,wt=3): 201 ->*_s0(b1,b6). [ur(26,a,164,a)]. given #174 (T,wt=3): 203 ->*_s0(b2,b7). [ur(28,a,165,a)]. given #175 (T,wt=3): 205 ->*_s0(b3,b8). [ur(29,a,166,a)]. given #176 (A,wt=6): 190 -->*_s0(b2,x) | -->*_s0(c4,x) # answer(goal). [resolve(137,b,39,b)]. given #177 (F,wt=3): 197 -->*_s0(b1,c7) # answer(goal). [resolve(149,b,147,a)]. given #178 (F,wt=3): 199 -->*_s0(c3,b6) # answer(goal). [resolve(167,a,38,b)]. given #179 (F,wt=3): 200 -->*_s0(b6,c3) # answer(goal). [resolve(172,a,31,b)]. given #180 (F,wt=3): 202 -->*_s0(c2,b7) # answer(goal). [resolve(165,a,127,a)]. given #181 (T,wt=3): 206 ->*_s0(b4,b9). [ur(30,a,173,a)]. given #182 (T,wt=3): 214 ->*_s0(b5,b10). [ur(31,a,174,a)]. given #183 (T,wt=3): 215 ->*_s0(c6,b11). [ur(42,a,175,a)]. given #184 (T,wt=3): 218 ->*_s0(c1,c6). [ur(36,a,186,a)]. given #185 (A,wt=6): 198 -->*_s0(b1,x) | -->*_s0(c5,x) # answer(goal). [resolve(149,b,40,b)]. given #186 (F,wt=3): 204 -->*_s0(c1,b8) # answer(goal). [resolve(166,a,129,b)]. given #187 (F,wt=3): 207 -->*_s0(b4,c5) # answer(goal). [resolve(168,a,145,a)]. given #188 (F,wt=3): 209 -->*_s0(c2,b8) # answer(goal). [resolve(168,b,166,a)]. given #189 (F,wt=3): 211 -->*_s0(b5,c4) # answer(goal). [resolve(176,a,30,b)]. given #190 (T,wt=3): 224 ->*_s0(c2,c7). [ur(38,a,187,a)]. given #191 (T,wt=3): 226 ->*_s0(c3,c8). [ur(39,a,188,a)]. given #192 (T,wt=3): 227 ->*_s0(c4,c9). [ur(40,a,194,a)]. given #193 (T,wt=3): 228 ->*_s0(c5,c10). [ur(41,a,195,a)]. given #194 (A,wt=6): 208 -->*_s0(b4,x) | -->*_s0(c3,x) # answer(goal). [resolve(168,a,38,b)]. given #195 (F,wt=3): 212 -->*_s0(b11,c1) # answer(goal). [resolve(179,a,27,b)]. given #196 (F,wt=3): 213 -->*_s0(c5,b4) # answer(goal). [resolve(180,a,40,b)]. given #197 (F,wt=3): 216 -->*_s0(b4,c6) # answer(goal). [resolve(186,a,168,a)]. given #198 (F,wt=3): 217 -->*_s0(b3,c6) # answer(goal). [resolve(186,a,127,b)]. given #199 (T,wt=3): 235 ->*_s0(b5,b11). [ur(31,a,196,a)]. given #200 (T,wt=3): 237 ->*_s0(b1,b7). [ur(26,a,203,a)]. given #201 (T,wt=3): 239 ->*_s0(b2,b8). [ur(28,a,205,a)]. given #202 (T,wt=3): 245 ->*_s0(b3,b9). [ur(29,a,206,a)]. given #203 (A,wt=6): 210 -->*_s0(c2,x) | -->*_s0(b5,x) # answer(goal). [resolve(168,b,30,b)]. given #204 (F,wt=3): 219 -->*_s0(c3,b7) # answer(goal). [resolve(170,a,165,a)]. given #205 (F,wt=3): 221 -->*_s0(c9,b2) # answer(goal). [resolve(182,a,44,b)]. given #206 (F,wt=3): 222 -->*_s0(b3,c7) # answer(goal). [resolve(187,a,170,b)]. given #207 (F,wt=3): 223 -->*_s0(b2,c7) # answer(goal). [resolve(187,a,137,b)]. given #208 (T,wt=3): 247 ->*_s0(b4,b10). [ur(30,a,214,a)]. given #209 (T,wt=3): 248 ->*_s0(c5,b11). [ur(41,a,215,a)]. given #210 (T,wt=3): 255 ->*_s0(c1,c7). [ur(36,a,224,a)]. given #211 (T,wt=3): 257 ->*_s0(c2,c8). [ur(38,a,226,a)]. given #212 (A,wt=6): 220 -->*_s0(b3,x) | -->*_s0(c4,x) # answer(goal). [resolve(170,b,39,b)]. given #213 (F,wt=3): 225 -->*_s0(b1,c8) # answer(goal). [resolve(188,a,149,b)]. given #214 (F,wt=3): 229 -->*_s0(b5,c5) # answer(goal). [resolve(178,a,184,a)]. given #215 (F,wt=3): 230 -->*_s0(c1,b9) # answer(goal). [resolve(178,b,173,a)]. given #216 (F,wt=3): 232 -->*_s0(c9,b3) # answer(goal). [resolve(191,a,44,b)]. given #217 (T,wt=3): 259 ->*_s0(c3,c9). [ur(39,a,227,a)]. given #218 (T,wt=3): 261 ->*_s0(c4,c10). [ur(40,a,228,a)]. given #219 (T,wt=3): 268 ->*_s0(b4,b11). [ur(30,a,235,a)]. given #220 (T,wt=3): 271 ->*_s0(b1,b8). [ur(26,a,239,a)]. given #221 (A,wt=6): 231 -->*_s0(c1,x) | -->*_s0(b6,x) # answer(goal). [resolve(178,b,31,b)]. given #222 (F,wt=3): 233 -->*_s0(b8,c2) # answer(goal). [resolve(192,a,33,b)]. given #223 (F,wt=3): 234 -->*_s0(c5,b5) # answer(goal). [resolve(193,a,40,b)]. given #224 (F,wt=3): 236 -->*_s0(c4,b6) # answer(goal). [resolve(201,a,149,a)]. given #225 (F,wt=3): 238 -->*_s0(c3,b8) # answer(goal). [resolve(205,a,170,a)]. given #226 (T,wt=3): 272 ->*_s0(b2,b9). [ur(28,a,245,a)]. given #227 (T,wt=3): 279 ->*_s0(b3,b10). [ur(29,a,247,a)]. given #228 (T,wt=3): 281 ->*_s0(c4,b11). [ur(40,a,248,a)]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.01) seconds: goal. % Length of proof is 66. % Level of proof is 11. % Maximum clause weight is 6.000. % Given clauses 228. 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 2 (exists x2 (->*_s0(b1,x2) & ->*_s0(c1,x2))) # label(goal) # label(non_clause) # label(goal). [goal]. 3 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 4 ->_s0(b1,b2) # label(replacement). [assumption]. 5 ->_s0(b10,b11) # label(replacement). [assumption]. 6 ->_s0(b2,b3) # label(replacement). [assumption]. 7 ->_s0(b3,b4) # label(replacement). [assumption]. 8 ->_s0(b4,b5) # label(replacement). [assumption]. 9 ->_s0(b5,b6) # label(replacement). [assumption]. 10 ->_s0(b6,b7) # label(replacement). [assumption]. 11 ->_s0(b7,b8) # label(replacement). [assumption]. 12 ->_s0(b8,b9) # label(replacement). [assumption]. 13 ->_s0(b9,b10) # label(replacement). [assumption]. 14 ->_s0(c1,c2) # label(replacement). [assumption]. 15 ->_s0(c10,b11) # label(replacement). [assumption]. 16 ->_s0(c2,c3) # label(replacement). [assumption]. 17 ->_s0(c3,c4) # label(replacement). [assumption]. 18 ->_s0(c4,c5) # label(replacement). [assumption]. 19 ->_s0(c5,c6) # label(replacement). [assumption]. 20 ->_s0(c6,c7) # label(replacement). [assumption]. 21 ->_s0(c7,c8) # label(replacement). [assumption]. 22 ->_s0(c8,c9) # label(replacement). [assumption]. 23 ->_s0(c9,c10) # label(replacement). [assumption]. 24 ->*_s0(x,x) # label(reflexivity). [assumption]. 25 -->*_s0(b1,x) | -->*_s0(c1,x) # label(goal) # answer(goal). [deny(2)]. 26 -->*_s0(b2,x) | ->*_s0(b1,x). [resolve(3,a,4,a)]. 27 -->*_s0(b11,x) | ->*_s0(b10,x). [resolve(3,a,5,a)]. 28 -->*_s0(b3,x) | ->*_s0(b2,x). [resolve(3,a,6,a)]. 29 -->*_s0(b4,x) | ->*_s0(b3,x). [resolve(3,a,7,a)]. 30 -->*_s0(b5,x) | ->*_s0(b4,x). [resolve(3,a,8,a)]. 31 -->*_s0(b6,x) | ->*_s0(b5,x). [resolve(3,a,9,a)]. 32 -->*_s0(b7,x) | ->*_s0(b6,x). [resolve(3,a,10,a)]. 33 -->*_s0(b8,x) | ->*_s0(b7,x). [resolve(3,a,11,a)]. 34 -->*_s0(b9,x) | ->*_s0(b8,x). [resolve(3,a,12,a)]. 35 -->*_s0(b10,x) | ->*_s0(b9,x). [resolve(3,a,13,a)]. 36 -->*_s0(c2,x) | ->*_s0(c1,x). [resolve(3,a,14,a)]. 37 -->*_s0(b11,x) | ->*_s0(c10,x). [resolve(3,a,15,a)]. 38 -->*_s0(c3,x) | ->*_s0(c2,x). [resolve(3,a,16,a)]. 39 -->*_s0(c4,x) | ->*_s0(c3,x). [resolve(3,a,17,a)]. 40 -->*_s0(c5,x) | ->*_s0(c4,x). [resolve(3,a,18,a)]. 41 -->*_s0(c6,x) | ->*_s0(c5,x). [resolve(3,a,19,a)]. 42 -->*_s0(c7,x) | ->*_s0(c6,x). [resolve(3,a,20,a)]. 43 -->*_s0(c8,x) | ->*_s0(c7,x). [resolve(3,a,21,a)]. 44 -->*_s0(c9,x) | ->*_s0(c8,x). [resolve(3,a,22,a)]. 45 -->*_s0(c10,x) | ->*_s0(c9,x). [resolve(3,a,23,a)]. 48 -->*_s0(b2,x) | -->*_s0(c1,x) # answer(goal). [resolve(26,b,25,a)]. 50 ->*_s0(b10,b11). [ur(27,a,24,a)]. 61 ->*_s0(c10,b11). [ur(37,a,24,a)]. 76 ->*_s0(b9,b11). [ur(35,a,50,a)]. 80 -->*_s0(c1,x) | -->*_s0(b3,x) # answer(goal). [resolve(48,a,28,b)]. 98 ->*_s0(c9,b11). [ur(45,a,61,a)]. 116 ->*_s0(b8,b11). [ur(34,a,76,a)]. 127 -->*_s0(b3,x) | -->*_s0(c2,x) # answer(goal). [resolve(80,a,36,b)]. 136 ->*_s0(c8,b11). [ur(44,a,98,a)]. 157 ->*_s0(b7,b11). [ur(33,a,116,a)]. 170 -->*_s0(b3,x) | -->*_s0(c3,x) # answer(goal). [resolve(127,b,38,b)]. 175 ->*_s0(c7,b11). [ur(43,a,136,a)]. 196 ->*_s0(b6,b11). [ur(32,a,157,a)]. 215 ->*_s0(c6,b11). [ur(42,a,175,a)]. 220 -->*_s0(b3,x) | -->*_s0(c4,x) # answer(goal). [resolve(170,b,39,b)]. 235 ->*_s0(b5,b11). [ur(31,a,196,a)]. 248 ->*_s0(c5,b11). [ur(41,a,215,a)]. 268 ->*_s0(b4,b11). [ur(30,a,235,a)]. 281 ->*_s0(c4,b11). [ur(40,a,248,a)]. 295 ->*_s0(b3,b11). [ur(29,a,268,a)]. 305 $F # answer(goal). [resolve(281,a,220,b),unit_del(a,295)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=228. Generated=906. Kept=281. proofs=1. Usable=228. Sos=53. Demods=0. Limbo=0, Disabled=43. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=624. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=13. Nonunit_bsub_feature_tests=76. Megabytes=0.28. User_CPU=0.01, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 2696439 exit (max_proofs) Fri Jun 9 15:47:25 2023 The problem is feasible. The problem is confluent. Problem 1.6: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (REPLACEMENT-MAP (a1) (a10) (a2) (a3) (a4) (a5) (a6) (a7) (a8) (a9) (b1) (b10) (b2) (b3) (b4) (b5) (b6) (b7) (b8) (b9) (c1) (c10) (c2) (c3) (c4) (c5) (c6) (c7) (c8) (c9) (b11) (fSNonEmpty) ) (RULES a1 -> b1 a1 -> c1 a10 -> b11 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b5 a5 -> c5 a6 -> b6 a6 -> c6 a7 -> b7 a7 -> c7 a8 -> b8 a8 -> c8 a9 -> b9 a9 -> c9 b1 -> b2 b10 -> b11 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 b6 -> b7 b7 -> b8 b8 -> b9 b9 -> b10 c1 -> c2 c10 -> b11 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> c6 c6 -> c7 c7 -> c8 c8 -> c9 c9 -> c10 ) Critical Pairs: => Not trivial, Overlay, Proper, NW0, N6 Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Brute Force Joinability Procedure: -> Rewritings: s: b9 Nodes: [0,1,2] Edges: [(0,1),(1,2)] ID: 0 => ('b9', D0) ID: 1 => ('b10', D1, R29, P[], S{}), NR: 'b10' ID: 2 => ('b11', D2, R21, P[], S{}), NR: 'b11' t: c9 Nodes: [0,1,2] Edges: [(0,1),(1,2)] ID: 0 => ('c9', D0) ID: 1 => ('c10', D1, R39, P[], S{}), NR: 'c10' ID: 2 => ('b11', D2, R31, P[], S{}), NR: 'b11' SNodesPath: b9 -> b10 -> b11 TNodesPath: c9 -> c10 -> b11 b9 ->* b11 *<- c9 "Joinable" The problem is confluent. Problem 1.7: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (REPLACEMENT-MAP (a1) (a10) (a2) (a3) (a4) (a5) (a6) (a7) (a8) (a9) (b1) (b10) (b2) (b3) (b4) (b5) (b6) (b7) (b8) (b9) (c1) (c10) (c2) (c3) (c4) (c5) (c6) (c7) (c8) (c9) (b11) (fSNonEmpty) ) (RULES a1 -> b1 a1 -> c1 a10 -> b11 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b5 a5 -> c5 a6 -> b6 a6 -> c6 a7 -> b7 a7 -> c7 a8 -> b8 a8 -> c8 a9 -> b9 a9 -> c9 b1 -> b2 b10 -> b11 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 b6 -> b7 b7 -> b8 b8 -> b9 b9 -> b10 c1 -> c2 c10 -> b11 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> c6 c6 -> c7 c7 -> c8 c8 -> c9 c9 -> c10 ) Critical Pairs: => Not trivial, Overlay, Proper, NW0, N7 Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Brute Force Joinability Procedure: -> Rewritings: s: b6 Nodes: [0,1,2,3,4,5] Edges: [(0,1),(1,2),(2,3),(3,4),(4,5)] ID: 0 => ('b6', D0) ID: 1 => ('b7', D1, R26, P[], S{}), NR: 'b7' ID: 2 => ('b8', D2, R27, P[], S{}), NR: 'b8' ID: 3 => ('b9', D3, R28, P[], S{}), NR: 'b9' ID: 4 => ('b10', D4, R29, P[], S{}), NR: 'b10' ID: 5 => ('b11', D5, R21, P[], S{}), NR: 'b11' t: c6 Nodes: [0,1,2,3,4,5] Edges: [(0,1),(1,2),(2,3),(3,4),(4,5)] ID: 0 => ('c6', D0) ID: 1 => ('c7', D1, R36, P[], S{}), NR: 'c7' ID: 2 => ('c8', D2, R37, P[], S{}), NR: 'c8' ID: 3 => ('c9', D3, R38, P[], S{}), NR: 'c9' ID: 4 => ('c10', D4, R39, P[], S{}), NR: 'c10' ID: 5 => ('b11', D5, R31, P[], S{}), NR: 'b11' SNodesPath: b6 -> b7 -> b8 -> b9 -> b10 -> b11 TNodesPath: c6 -> c7 -> c8 -> c9 -> c10 -> b11 b6 ->* b11 *<- c6 "Joinable" The problem is confluent. Problem 1.8: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (REPLACEMENT-MAP (a1) (a10) (a2) (a3) (a4) (a5) (a6) (a7) (a8) (a9) (b1) (b10) (b2) (b3) (b4) (b5) (b6) (b7) (b8) (b9) (c1) (c10) (c2) (c3) (c4) (c5) (c6) (c7) (c8) (c9) (b11) (fSNonEmpty) ) (RULES a1 -> b1 a1 -> c1 a10 -> b11 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b5 a5 -> c5 a6 -> b6 a6 -> c6 a7 -> b7 a7 -> c7 a8 -> b8 a8 -> c8 a9 -> b9 a9 -> c9 b1 -> b2 b10 -> b11 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 b6 -> b7 b7 -> b8 b8 -> b9 b9 -> b10 c1 -> c2 c10 -> b11 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> c6 c6 -> c7 c7 -> c8 c8 -> c9 c9 -> c10 ) Critical Pairs: => Not trivial, Overlay, Proper, NW0, N8 Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Brute Force Joinability Procedure: -> Rewritings: s: b4 Nodes: [0,1,2,3,4,5,6,7] Edges: [(0,1),(1,2),(2,3),(3,4),(4,5),(5,6),(6,7)] ID: 0 => ('b4', D0) ID: 1 => ('b5', D1, R24, P[], S{}), NR: 'b5' ID: 2 => ('b6', D2, R25, P[], S{}), NR: 'b6' ID: 3 => ('b7', D3, R26, P[], S{}), NR: 'b7' ID: 4 => ('b8', D4, R27, P[], S{}), NR: 'b8' ID: 5 => ('b9', D5, R28, P[], S{}), NR: 'b9' ID: 6 => ('b10', D6, R29, P[], S{}), NR: 'b10' ID: 7 => ('b11', D7, R21, P[], S{}), NR: 'b11' t: c4 Nodes: [0,1,2,3,4,5,6,7] Edges: [(0,1),(1,2),(2,3),(3,4),(4,5),(5,6),(6,7)] ID: 0 => ('c4', D0) ID: 1 => ('c5', D1, R34, P[], S{}), NR: 'c5' ID: 2 => ('c6', D2, R35, P[], S{}), NR: 'c6' ID: 3 => ('c7', D3, R36, P[], S{}), NR: 'c7' ID: 4 => ('c8', D4, R37, P[], S{}), NR: 'c8' ID: 5 => ('c9', D5, R38, P[], S{}), NR: 'c9' ID: 6 => ('c10', D6, R39, P[], S{}), NR: 'c10' ID: 7 => ('b11', D7, R31, P[], S{}), NR: 'b11' SNodesPath: b4 -> b5 -> b6 -> b7 -> b8 -> b9 -> b10 -> b11 TNodesPath: c4 -> c5 -> c6 -> c7 -> c8 -> c9 -> c10 -> b11 b4 ->* b11 *<- c4 "Joinable" The problem is confluent. Problem 1.9: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (REPLACEMENT-MAP (a1) (a10) (a2) (a3) (a4) (a5) (a6) (a7) (a8) (a9) (b1) (b10) (b2) (b3) (b4) (b5) (b6) (b7) (b8) (b9) (c1) (c10) (c2) (c3) (c4) (c5) (c6) (c7) (c8) (c9) (b11) (fSNonEmpty) ) (RULES a1 -> b1 a1 -> c1 a10 -> b11 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b5 a5 -> c5 a6 -> b6 a6 -> c6 a7 -> b7 a7 -> c7 a8 -> b8 a8 -> c8 a9 -> b9 a9 -> c9 b1 -> b2 b10 -> b11 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 b6 -> b7 b7 -> b8 b8 -> b9 b9 -> b10 c1 -> c2 c10 -> b11 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> c6 c6 -> c7 c7 -> c8 c8 -> c9 c9 -> c10 ) Critical Pairs: => Not trivial, Overlay, Proper, NW0, N9 Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet InfChecker Procedure: Infeasible convergence? NO Problem 1: Infeasibility Problem: [(VAR vNonEmpty vNonEmpty z0) (STRATEGY CONTEXTSENSITIVE (a1) (a10) (a2) (a3) (a4) (a5) (a6) (a7) (a8) (a9) (b1) (b10) (b2) (b3) (b4) (b5) (b6) (b7) (b8) (b9) (c1) (c10) (c2) (c3) (c4) (c5) (c6) (c7) (c8) (c9) (b11) (fSNonEmpty) ) (RULES a1 -> b1 a1 -> c1 a10 -> b11 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b5 a5 -> c5 a6 -> b6 a6 -> c6 a7 -> b7 a7 -> c7 a8 -> b8 a8 -> c8 a9 -> b9 a9 -> c9 b1 -> b2 b10 -> b11 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 b6 -> b7 b7 -> b8 b8 -> b9 b9 -> b10 c1 -> c2 c10 -> b11 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> c6 c6 -> c7 c7 -> c8 c8 -> c9 c9 -> c10 )] Infeasibility Conditions: b2 ->* z0, c2 ->* z0 Problem 1: Obtaining a proof using Prover9: -> Prover9 Output: ============================== Prover9 =============================== Prover9 (64) version 2009-11A, November 2009. Process 2696486 was started by shintani on shintani-XPS-13-9310, Fri Jun 9 15:47:26 2023 The command was "./prover9 -f /tmp/prover92696472-0.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file /tmp/prover92696472-0.in assign(max_seconds,20). formulas(assumptions). ->_s0(b10,b11) # label(replacement). ->_s0(b2,b3) # label(replacement). ->_s0(b3,b4) # label(replacement). ->_s0(b4,b5) # label(replacement). ->_s0(b5,b6) # label(replacement). ->_s0(b6,b7) # label(replacement). ->_s0(b7,b8) # label(replacement). ->_s0(b8,b9) # label(replacement). ->_s0(b9,b10) # label(replacement). ->_s0(c10,b11) # label(replacement). ->_s0(c2,c3) # label(replacement). ->_s0(c3,c4) # label(replacement). ->_s0(c4,c5) # label(replacement). ->_s0(c5,c6) # label(replacement). ->_s0(c6,c7) # label(replacement). ->_s0(c7,c8) # label(replacement). ->_s0(c8,c9) # label(replacement). ->_s0(c9,c10) # label(replacement). ->*_s0(x,x) # label(reflexivity). ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). end_of_list. formulas(goals). (exists x2 (->*_s0(b2,x2) & ->*_s0(c2,x2))) # label(goal). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 2 (exists x2 (->*_s0(b2,x2) & ->*_s0(c2,x2))) # label(goal) # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). ->_s0(b10,b11) # label(replacement). [assumption]. ->_s0(b2,b3) # label(replacement). [assumption]. ->_s0(b3,b4) # label(replacement). [assumption]. ->_s0(b4,b5) # label(replacement). [assumption]. ->_s0(b5,b6) # label(replacement). [assumption]. ->_s0(b6,b7) # label(replacement). [assumption]. ->_s0(b7,b8) # label(replacement). [assumption]. ->_s0(b8,b9) # label(replacement). [assumption]. ->_s0(b9,b10) # label(replacement). [assumption]. ->_s0(c10,b11) # label(replacement). [assumption]. ->_s0(c2,c3) # label(replacement). [assumption]. ->_s0(c3,c4) # label(replacement). [assumption]. ->_s0(c4,c5) # label(replacement). [assumption]. ->_s0(c5,c6) # label(replacement). [assumption]. ->_s0(c6,c7) # label(replacement). [assumption]. ->_s0(c7,c8) # label(replacement). [assumption]. ->_s0(c8,c9) # label(replacement). [assumption]. ->_s0(c9,c10) # label(replacement). [assumption]. ->*_s0(x,x) # label(reflexivity). [assumption]. -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. -->*_s0(b2,x) | -->*_s0(c2,x) # label(goal). [deny(2)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating ->_s0/2 3 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 4 ->_s0(b10,b11) # label(replacement). [assumption]. 5 ->_s0(b2,b3) # label(replacement). [assumption]. 6 ->_s0(b3,b4) # label(replacement). [assumption]. 7 ->_s0(b4,b5) # label(replacement). [assumption]. 8 ->_s0(b5,b6) # label(replacement). [assumption]. 9 ->_s0(b6,b7) # label(replacement). [assumption]. 10 ->_s0(b7,b8) # label(replacement). [assumption]. 11 ->_s0(b8,b9) # label(replacement). [assumption]. 12 ->_s0(b9,b10) # label(replacement). [assumption]. 13 ->_s0(c10,b11) # label(replacement). [assumption]. 14 ->_s0(c2,c3) # label(replacement). [assumption]. 15 ->_s0(c3,c4) # label(replacement). [assumption]. 16 ->_s0(c4,c5) # label(replacement). [assumption]. 17 ->_s0(c5,c6) # label(replacement). [assumption]. 18 ->_s0(c6,c7) # label(replacement). [assumption]. 19 ->_s0(c7,c8) # label(replacement). [assumption]. 20 ->_s0(c8,c9) # label(replacement). [assumption]. 21 ->_s0(c9,c10) # label(replacement). [assumption]. Derived: -->*_s0(b11,x) | ->*_s0(b10,x). [resolve(3,a,4,a)]. Derived: -->*_s0(b3,x) | ->*_s0(b2,x). [resolve(3,a,5,a)]. Derived: -->*_s0(b4,x) | ->*_s0(b3,x). [resolve(3,a,6,a)]. Derived: -->*_s0(b5,x) | ->*_s0(b4,x). [resolve(3,a,7,a)]. Derived: -->*_s0(b6,x) | ->*_s0(b5,x). [resolve(3,a,8,a)]. Derived: -->*_s0(b7,x) | ->*_s0(b6,x). [resolve(3,a,9,a)]. Derived: -->*_s0(b8,x) | ->*_s0(b7,x). [resolve(3,a,10,a)]. Derived: -->*_s0(b9,x) | ->*_s0(b8,x). [resolve(3,a,11,a)]. Derived: -->*_s0(b10,x) | ->*_s0(b9,x). [resolve(3,a,12,a)]. Derived: -->*_s0(b11,x) | ->*_s0(c10,x). [resolve(3,a,13,a)]. Derived: -->*_s0(c3,x) | ->*_s0(c2,x). [resolve(3,a,14,a)]. Derived: -->*_s0(c4,x) | ->*_s0(c3,x). [resolve(3,a,15,a)]. Derived: -->*_s0(c5,x) | ->*_s0(c4,x). [resolve(3,a,16,a)]. Derived: -->*_s0(c6,x) | ->*_s0(c5,x). [resolve(3,a,17,a)]. Derived: -->*_s0(c7,x) | ->*_s0(c6,x). [resolve(3,a,18,a)]. Derived: -->*_s0(c8,x) | ->*_s0(c7,x). [resolve(3,a,19,a)]. Derived: -->*_s0(c9,x) | ->*_s0(c8,x). [resolve(3,a,20,a)]. Derived: -->*_s0(c10,x) | ->*_s0(c9,x). [resolve(3,a,21,a)]. ============================== end predicate elimination ============= Auto_denials: % copying label goal to answer in negative clause Term ordering decisions: Predicate symbol precedence: predicate_order([ ->*_s0 ]). Function symbol precedence: function_order([ b10, b3, b4, b5, b6, b7, b8, b9, c10, c3, c4, c5, c6, c7, c8, c9, b11, b2, c2 ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(neg_binary_resolution). % (HNE depth_diff=0) % clear(ordered_res). % (HNE depth_diff=0) % set(ur_resolution). % (HNE depth_diff=0) % set(ur_resolution) -> set(pos_ur_resolution). % set(ur_resolution) -> set(neg_ur_resolution). Auto_process settings: % set(unit_deletion). % (Horn set with negative nonunits) kept: 22 ->*_s0(x,x) # label(reflexivity). [assumption]. kept: 23 -->*_s0(b2,x) | -->*_s0(c2,x) # label(goal) # answer(goal). [deny(2)]. kept: 24 -->*_s0(b11,x) | ->*_s0(b10,x). [resolve(3,a,4,a)]. kept: 25 -->*_s0(b3,x) | ->*_s0(b2,x). [resolve(3,a,5,a)]. kept: 26 -->*_s0(b4,x) | ->*_s0(b3,x). [resolve(3,a,6,a)]. kept: 27 -->*_s0(b5,x) | ->*_s0(b4,x). [resolve(3,a,7,a)]. kept: 28 -->*_s0(b6,x) | ->*_s0(b5,x). [resolve(3,a,8,a)]. kept: 29 -->*_s0(b7,x) | ->*_s0(b6,x). [resolve(3,a,9,a)]. kept: 30 -->*_s0(b8,x) | ->*_s0(b7,x). [resolve(3,a,10,a)]. kept: 31 -->*_s0(b9,x) | ->*_s0(b8,x). [resolve(3,a,11,a)]. kept: 32 -->*_s0(b10,x) | ->*_s0(b9,x). [resolve(3,a,12,a)]. kept: 33 -->*_s0(b11,x) | ->*_s0(c10,x). [resolve(3,a,13,a)]. kept: 34 -->*_s0(c3,x) | ->*_s0(c2,x). [resolve(3,a,14,a)]. kept: 35 -->*_s0(c4,x) | ->*_s0(c3,x). [resolve(3,a,15,a)]. kept: 36 -->*_s0(c5,x) | ->*_s0(c4,x). [resolve(3,a,16,a)]. kept: 37 -->*_s0(c6,x) | ->*_s0(c5,x). [resolve(3,a,17,a)]. kept: 38 -->*_s0(c7,x) | ->*_s0(c6,x). [resolve(3,a,18,a)]. kept: 39 -->*_s0(c8,x) | ->*_s0(c7,x). [resolve(3,a,19,a)]. kept: 40 -->*_s0(c9,x) | ->*_s0(c8,x). [resolve(3,a,20,a)]. kept: 41 -->*_s0(c10,x) | ->*_s0(c9,x). [resolve(3,a,21,a)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 22 ->*_s0(x,x) # label(reflexivity). [assumption]. 23 -->*_s0(b2,x) | -->*_s0(c2,x) # label(goal) # answer(goal). [deny(2)]. 24 -->*_s0(b11,x) | ->*_s0(b10,x). [resolve(3,a,4,a)]. 25 -->*_s0(b3,x) | ->*_s0(b2,x). [resolve(3,a,5,a)]. 26 -->*_s0(b4,x) | ->*_s0(b3,x). [resolve(3,a,6,a)]. 27 -->*_s0(b5,x) | ->*_s0(b4,x). [resolve(3,a,7,a)]. 28 -->*_s0(b6,x) | ->*_s0(b5,x). [resolve(3,a,8,a)]. 29 -->*_s0(b7,x) | ->*_s0(b6,x). [resolve(3,a,9,a)]. 30 -->*_s0(b8,x) | ->*_s0(b7,x). [resolve(3,a,10,a)]. 31 -->*_s0(b9,x) | ->*_s0(b8,x). [resolve(3,a,11,a)]. 32 -->*_s0(b10,x) | ->*_s0(b9,x). [resolve(3,a,12,a)]. 33 -->*_s0(b11,x) | ->*_s0(c10,x). [resolve(3,a,13,a)]. 34 -->*_s0(c3,x) | ->*_s0(c2,x). [resolve(3,a,14,a)]. 35 -->*_s0(c4,x) | ->*_s0(c3,x). [resolve(3,a,15,a)]. 36 -->*_s0(c5,x) | ->*_s0(c4,x). [resolve(3,a,16,a)]. 37 -->*_s0(c6,x) | ->*_s0(c5,x). [resolve(3,a,17,a)]. 38 -->*_s0(c7,x) | ->*_s0(c6,x). [resolve(3,a,18,a)]. 39 -->*_s0(c8,x) | ->*_s0(c7,x). [resolve(3,a,19,a)]. 40 -->*_s0(c9,x) | ->*_s0(c8,x). [resolve(3,a,20,a)]. 41 -->*_s0(c10,x) | ->*_s0(c9,x). [resolve(3,a,21,a)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=3): 22 ->*_s0(x,x) # label(reflexivity). [assumption]. given #2 (I,wt=6): 23 -->*_s0(b2,x) | -->*_s0(c2,x) # label(goal) # answer(goal). [deny(2)]. given #3 (I,wt=6): 24 -->*_s0(b11,x) | ->*_s0(b10,x). [resolve(3,a,4,a)]. given #4 (I,wt=6): 25 -->*_s0(b3,x) | ->*_s0(b2,x). [resolve(3,a,5,a)]. given #5 (I,wt=6): 26 -->*_s0(b4,x) | ->*_s0(b3,x). [resolve(3,a,6,a)]. given #6 (I,wt=6): 27 -->*_s0(b5,x) | ->*_s0(b4,x). [resolve(3,a,7,a)]. given #7 (I,wt=6): 28 -->*_s0(b6,x) | ->*_s0(b5,x). [resolve(3,a,8,a)]. given #8 (I,wt=6): 29 -->*_s0(b7,x) | ->*_s0(b6,x). [resolve(3,a,9,a)]. given #9 (I,wt=6): 30 -->*_s0(b8,x) | ->*_s0(b7,x). [resolve(3,a,10,a)]. given #10 (I,wt=6): 31 -->*_s0(b9,x) | ->*_s0(b8,x). [resolve(3,a,11,a)]. given #11 (I,wt=6): 32 -->*_s0(b10,x) | ->*_s0(b9,x). [resolve(3,a,12,a)]. given #12 (I,wt=6): 33 -->*_s0(b11,x) | ->*_s0(c10,x). [resolve(3,a,13,a)]. given #13 (I,wt=6): 34 -->*_s0(c3,x) | ->*_s0(c2,x). [resolve(3,a,14,a)]. given #14 (I,wt=6): 35 -->*_s0(c4,x) | ->*_s0(c3,x). [resolve(3,a,15,a)]. given #15 (I,wt=6): 36 -->*_s0(c5,x) | ->*_s0(c4,x). [resolve(3,a,16,a)]. given #16 (I,wt=6): 37 -->*_s0(c6,x) | ->*_s0(c5,x). [resolve(3,a,17,a)]. given #17 (I,wt=6): 38 -->*_s0(c7,x) | ->*_s0(c6,x). [resolve(3,a,18,a)]. given #18 (I,wt=6): 39 -->*_s0(c8,x) | ->*_s0(c7,x). [resolve(3,a,19,a)]. given #19 (I,wt=6): 40 -->*_s0(c9,x) | ->*_s0(c8,x). [resolve(3,a,20,a)]. given #20 (I,wt=6): 41 -->*_s0(c10,x) | ->*_s0(c9,x). [resolve(3,a,21,a)]. given #21 (A,wt=3): 42 -->*_s0(c2,b2) # answer(goal). [resolve(23,a,22,a)]. given #22 (F,wt=3): 43 -->*_s0(b2,c2) # answer(goal). [resolve(23,b,22,a)]. given #23 (F,wt=3): 64 -->*_s0(c3,b2) # answer(goal). [resolve(42,a,34,b)]. given #24 (F,wt=3): 65 -->*_s0(b3,c2) # answer(goal). [resolve(43,a,25,b)]. given #25 (F,wt=3): 66 -->*_s0(c4,b2) # answer(goal). [resolve(64,a,35,b)]. given #26 (T,wt=3): 44 ->*_s0(b10,b11). [ur(24,a,22,a)]. given #27 (T,wt=3): 46 ->*_s0(b2,b3). [ur(25,a,22,a)]. given #28 (T,wt=3): 47 ->*_s0(b3,b4). [ur(26,a,22,a)]. given #29 (T,wt=3): 48 ->*_s0(b4,b5). [ur(27,a,22,a)]. given #30 (A,wt=6): 45 -->*_s0(b3,x) | -->*_s0(c2,x) # answer(goal). [resolve(25,b,23,a)]. given #31 (F,wt=3): 67 -->*_s0(b4,c2) # answer(goal). [resolve(65,a,26,b)]. given #32 (F,wt=3): 68 -->*_s0(c5,b2) # answer(goal). [resolve(66,a,36,b)]. given #33 (F,wt=3): 70 -->*_s0(c2,b3) # answer(goal). [resolve(46,a,23,a)]. given #34 (F,wt=3): 73 -->*_s0(c2,b4) # answer(goal). [resolve(45,a,47,a)]. given #35 (T,wt=3): 49 ->*_s0(b5,b6). [ur(28,a,22,a)]. given #36 (T,wt=3): 50 ->*_s0(b6,b7). [ur(29,a,22,a)]. given #37 (T,wt=3): 51 ->*_s0(b7,b8). [ur(30,a,22,a)]. given #38 (T,wt=3): 52 ->*_s0(b8,b9). [ur(31,a,22,a)]. given #39 (A,wt=3): 53 ->*_s0(b9,b10). [ur(32,a,22,a)]. given #40 (F,wt=3): 76 -->*_s0(b5,c2) # answer(goal). [resolve(67,a,27,b)]. given #41 (F,wt=3): 77 -->*_s0(c6,b2) # answer(goal). [resolve(68,a,37,b)]. given #42 (F,wt=3): 78 -->*_s0(c3,b3) # answer(goal). [resolve(70,a,34,b)]. given #43 (F,wt=3): 79 -->*_s0(c3,b4) # answer(goal). [resolve(73,a,34,b)]. given #44 (T,wt=3): 54 ->*_s0(c10,b11). [ur(33,a,22,a)]. given #45 (T,wt=3): 56 ->*_s0(c2,c3). [ur(34,a,22,a)]. given #46 (T,wt=3): 57 ->*_s0(c3,c4). [ur(35,a,22,a)]. given #47 (T,wt=3): 58 ->*_s0(c4,c5). [ur(36,a,22,a)]. given #48 (A,wt=6): 55 -->*_s0(c3,x) | -->*_s0(b2,x) # answer(goal). [resolve(34,b,23,b)]. given #49 (F,wt=3): 85 -->*_s0(b6,c2) # answer(goal). [resolve(76,a,28,b)]. given #50 (F,wt=3): 86 -->*_s0(c7,b2) # answer(goal). [resolve(77,a,38,b)]. given #51 (F,wt=3): 87 -->*_s0(c4,b3) # answer(goal). [resolve(78,a,35,b)]. given #52 (F,wt=3): 88 -->*_s0(c4,b4) # answer(goal). [resolve(79,a,35,b)]. given #53 (T,wt=3): 59 ->*_s0(c5,c6). [ur(37,a,22,a)]. given #54 (T,wt=3): 60 ->*_s0(c6,c7). [ur(38,a,22,a)]. given #55 (T,wt=3): 61 ->*_s0(c7,c8). [ur(39,a,22,a)]. given #56 (T,wt=3): 62 ->*_s0(c8,c9). [ur(40,a,22,a)]. given #57 (A,wt=3): 63 ->*_s0(c9,c10). [ur(41,a,22,a)]. given #58 (F,wt=3): 90 -->*_s0(b3,c3) # answer(goal). [resolve(56,a,45,b)]. given #59 (F,wt=3): 91 -->*_s0(b2,c3) # answer(goal). [resolve(56,a,23,b)]. given #60 (F,wt=3): 94 -->*_s0(b2,c4) # answer(goal). [resolve(55,a,57,a)]. given #61 (F,wt=3): 96 -->*_s0(b7,c2) # answer(goal). [resolve(85,a,29,b)]. given #62 (T,wt=3): 69 ->*_s0(b9,b11). [ur(32,a,44,a)]. given #63 (T,wt=3): 71 ->*_s0(b2,b4). [ur(25,a,47,a)]. given #64 (T,wt=3): 72 ->*_s0(b3,b5). [ur(26,a,48,a)]. given #65 (T,wt=3): 80 ->*_s0(b4,b6). [ur(27,a,49,a)]. given #66 (A,wt=6): 74 -->*_s0(c2,x) | -->*_s0(b4,x) # answer(goal). [resolve(45,a,26,b)]. given #67 (F,wt=3): 97 -->*_s0(c8,b2) # answer(goal). [resolve(86,a,39,b)]. given #68 (F,wt=3): 98 -->*_s0(c5,b3) # answer(goal). [resolve(87,a,36,b)]. given #69 (F,wt=3): 99 -->*_s0(c5,b4) # answer(goal). [resolve(88,a,36,b)]. given #70 (F,wt=3): 105 -->*_s0(b4,c3) # answer(goal). [resolve(90,a,26,b)]. given #71 (T,wt=3): 81 ->*_s0(b5,b7). [ur(28,a,50,a)]. given #72 (T,wt=3): 82 ->*_s0(b6,b8). [ur(29,a,51,a)]. given #73 (T,wt=3): 83 ->*_s0(b7,b9). [ur(30,a,52,a)]. given #74 (T,wt=3): 84 ->*_s0(b8,b10). [ur(31,a,53,a)]. given #75 (A,wt=6): 75 -->*_s0(b3,x) | -->*_s0(c3,x) # answer(goal). [resolve(45,b,34,b)]. given #76 (F,wt=3): 106 -->*_s0(b3,c4) # answer(goal). [resolve(94,a,25,b)]. given #77 (F,wt=3): 107 -->*_s0(b8,c2) # answer(goal). [resolve(96,a,30,b)]. given #78 (F,wt=3): 109 -->*_s0(c2,b5) # answer(goal). [resolve(72,a,45,a)]. given #79 (F,wt=3): 113 -->*_s0(c2,b6) # answer(goal). [resolve(74,b,80,a)]. given #80 (T,wt=3): 89 ->*_s0(c9,b11). [ur(41,a,54,a)]. given #81 (T,wt=3): 92 ->*_s0(c2,c4). [ur(34,a,57,a)]. given #82 (T,wt=3): 93 ->*_s0(c3,c5). [ur(35,a,58,a)]. given #83 (T,wt=3): 100 ->*_s0(c4,c6). [ur(36,a,59,a)]. given #84 (A,wt=6): 95 -->*_s0(b2,x) | -->*_s0(c4,x) # answer(goal). [resolve(55,a,35,b)]. given #85 (F,wt=3): 115 -->*_s0(c9,b2) # answer(goal). [resolve(97,a,40,b)]. given #86 (F,wt=3): 116 -->*_s0(c6,b3) # answer(goal). [resolve(98,a,37,b)]. given #87 (F,wt=3): 117 -->*_s0(c6,b4) # answer(goal). [resolve(99,a,37,b)]. given #88 (F,wt=3): 118 -->*_s0(b5,c3) # answer(goal). [resolve(105,a,27,b)]. given #89 (T,wt=3): 101 ->*_s0(c5,c7). [ur(37,a,60,a)]. given #90 (T,wt=3): 102 ->*_s0(c6,c8). [ur(38,a,61,a)]. given #91 (T,wt=3): 103 ->*_s0(c7,c9). [ur(39,a,62,a)]. given #92 (T,wt=3): 104 ->*_s0(c8,c10). [ur(40,a,63,a)]. given #93 (A,wt=3): 108 ->*_s0(b8,b11). [ur(31,a,69,a)]. given #94 (F,wt=3): 123 -->*_s0(c3,b5) # answer(goal). [resolve(75,a,72,a)]. given #95 (F,wt=3): 125 -->*_s0(b4,c4) # answer(goal). [resolve(106,a,26,b)]. given #96 (F,wt=3): 126 -->*_s0(b9,c2) # answer(goal). [resolve(107,a,31,b)]. given #97 (F,wt=3): 127 -->*_s0(c3,b6) # answer(goal). [resolve(113,a,34,b)]. given #98 (T,wt=3): 110 ->*_s0(b2,b5). [ur(25,a,72,a)]. given #99 (T,wt=3): 111 ->*_s0(b3,b6). [ur(26,a,80,a)]. given #100 (T,wt=3): 119 ->*_s0(b4,b7). [ur(27,a,81,a)]. given #101 (T,wt=3): 120 ->*_s0(b5,b8). [ur(28,a,82,a)]. given #102 (A,wt=6): 112 -->*_s0(b4,x) | -->*_s0(c3,x) # answer(goal). [resolve(74,a,34,b)]. given #103 (F,wt=3): 129 -->*_s0(b3,c5) # answer(goal). [resolve(93,a,75,b)]. given #104 (F,wt=3): 130 -->*_s0(b2,c5) # answer(goal). [resolve(93,a,55,a)]. given #105 (F,wt=3): 133 -->*_s0(b2,c6) # answer(goal). [resolve(95,b,100,a)]. given #106 (F,wt=3): 135 -->*_s0(c10,b2) # answer(goal). [resolve(115,a,41,b)]. given #107 (T,wt=3): 121 ->*_s0(b6,b9). [ur(29,a,83,a)]. given #108 (T,wt=3): 122 ->*_s0(b7,b10). [ur(30,a,84,a)]. given #109 (T,wt=3): 128 ->*_s0(c8,b11). [ur(40,a,89,a)]. given #110 (T,wt=3): 131 ->*_s0(c2,c5). [ur(34,a,93,a)]. given #111 (A,wt=6): 114 -->*_s0(c2,x) | -->*_s0(b5,x) # answer(goal). [resolve(74,b,27,b)]. given #112 (F,wt=3): 136 -->*_s0(c7,b3) # answer(goal). [resolve(116,a,38,b)]. given #113 (F,wt=3): 137 -->*_s0(c7,b4) # answer(goal). [resolve(117,a,38,b)]. given #114 (F,wt=3): 138 -->*_s0(b6,c3) # answer(goal). [resolve(118,a,28,b)]. given #115 (F,wt=3): 144 -->*_s0(c4,b5) # answer(goal). [resolve(123,a,35,b)]. given #116 (T,wt=3): 132 ->*_s0(c3,c6). [ur(35,a,100,a)]. given #117 (T,wt=3): 139 ->*_s0(c4,c7). [ur(36,a,101,a)]. given #118 (T,wt=3): 140 ->*_s0(c5,c8). [ur(37,a,102,a)]. given #119 (T,wt=3): 141 ->*_s0(c6,c9). [ur(38,a,103,a)]. given #120 (A,wt=6): 124 -->*_s0(b3,x) | -->*_s0(c4,x) # answer(goal). [resolve(75,b,35,b)]. given #121 (F,wt=3): 145 -->*_s0(b5,c4) # answer(goal). [resolve(125,a,27,b)]. given #122 (F,wt=3): 146 -->*_s0(b10,c2) # answer(goal). [resolve(126,a,32,b)]. given #123 (F,wt=3): 147 -->*_s0(c4,b6) # answer(goal). [resolve(127,a,35,b)]. given #124 (F,wt=3): 149 -->*_s0(c2,b7) # answer(goal). [resolve(119,a,74,b)]. given #125 (T,wt=3): 142 ->*_s0(c7,c10). [ur(39,a,104,a)]. given #126 (T,wt=3): 143 ->*_s0(b7,b11). [ur(30,a,108,a)]. given #127 (T,wt=3): 148 ->*_s0(b2,b6). [ur(25,a,111,a)]. given #128 (T,wt=3): 150 ->*_s0(b3,b7). [ur(26,a,119,a)]. given #129 (A,wt=6): 134 -->*_s0(b2,x) | -->*_s0(c5,x) # answer(goal). [resolve(95,b,36,b)]. given #130 (F,wt=3): 152 -->*_s0(c3,b7) # answer(goal). [resolve(112,a,119,a)]. given #131 (F,wt=3): 154 -->*_s0(b4,c5) # answer(goal). [resolve(112,b,93,a)]. given #132 (F,wt=3): 156 -->*_s0(b3,c6) # answer(goal). [resolve(133,a,25,b)]. given #133 (F,wt=3): 157 -->*_s0(b11,b2) # answer(goal). [resolve(135,a,33,b)]. given #134 (T,wt=3): 151 ->*_s0(b4,b8). [ur(27,a,120,a)]. given #135 (T,wt=3): 158 ->*_s0(b5,b9). [ur(28,a,121,a)]. given #136 (T,wt=3): 159 ->*_s0(b6,b10). [ur(29,a,122,a)]. given #137 (T,wt=3): 160 ->*_s0(c7,b11). [ur(39,a,128,a)]. given #138 (A,wt=6): 153 -->*_s0(c3,x) | -->*_s0(b5,x) # answer(goal). [resolve(112,a,27,b)]. given #139 (F,wt=3): 161 -->*_s0(b5,c5) # answer(goal). [resolve(114,a,131,a)]. given #140 (F,wt=3): 162 -->*_s0(c2,b8) # answer(goal). [resolve(114,b,120,a)]. given #141 (F,wt=3): 164 -->*_s0(c8,b3) # answer(goal). [resolve(136,a,39,b)]. given #142 (F,wt=3): 165 -->*_s0(c8,b4) # answer(goal). [resolve(137,a,39,b)]. given #143 (T,wt=3): 169 ->*_s0(c2,c6). [ur(34,a,132,a)]. given #144 (T,wt=3): 171 ->*_s0(c3,c7). [ur(35,a,139,a)]. given #145 (T,wt=3): 172 ->*_s0(c4,c8). [ur(36,a,140,a)]. given #146 (T,wt=3): 173 ->*_s0(c5,c9). [ur(37,a,141,a)]. given #147 (A,wt=6): 155 -->*_s0(b4,x) | -->*_s0(c4,x) # answer(goal). [resolve(112,b,35,b)]. given #148 (F,wt=3): 166 -->*_s0(b7,c3) # answer(goal). [resolve(138,a,29,b)]. given #149 (F,wt=3): 167 -->*_s0(c5,b5) # answer(goal). [resolve(144,a,36,b)]. given #150 (F,wt=3): 168 -->*_s0(b4,c6) # answer(goal). [resolve(132,a,112,b)]. given #151 (F,wt=3): 170 -->*_s0(b2,c7) # answer(goal). [resolve(139,a,95,b)]. given #152 (T,wt=3): 179 ->*_s0(c6,c10). [ur(38,a,142,a)]. given #153 (T,wt=3): 180 ->*_s0(b6,b11). [ur(29,a,143,a)]. given #154 (T,wt=3): 182 ->*_s0(b2,b7). [ur(25,a,150,a)]. given #155 (T,wt=3): 186 ->*_s0(b3,b8). [ur(26,a,151,a)]. given #156 (A,wt=6): 163 -->*_s0(c2,x) | -->*_s0(b6,x) # answer(goal). [resolve(114,b,28,b)]. given #157 (F,wt=3): 174 -->*_s0(b3,c7) # answer(goal). [resolve(124,b,139,a)]. given #158 (F,wt=3): 176 -->*_s0(b6,c4) # answer(goal). [resolve(145,a,28,b)]. given #159 (F,wt=3): 177 -->*_s0(b11,c2) # answer(goal). [resolve(146,a,24,b)]. given #160 (F,wt=3): 178 -->*_s0(c5,b6) # answer(goal). [resolve(147,a,36,b)]. given #161 (T,wt=3): 188 ->*_s0(b4,b9). [ur(27,a,158,a)]. given #162 (T,wt=3): 189 ->*_s0(b5,b10). [ur(28,a,159,a)]. given #163 (T,wt=3): 190 ->*_s0(c6,b11). [ur(38,a,160,a)]. given #164 (T,wt=3): 200 ->*_s0(c2,c7). [ur(34,a,171,a)]. given #165 (A,wt=6): 175 -->*_s0(b3,x) | -->*_s0(c5,x) # answer(goal). [resolve(124,b,36,b)]. given #166 (F,wt=3): 181 -->*_s0(c4,b7) # answer(goal). [resolve(150,a,124,a)]. given #167 (F,wt=3): 183 -->*_s0(b2,c8) # answer(goal). [resolve(134,b,140,a)]. given #168 (F,wt=3): 185 -->*_s0(c3,b8) # answer(goal). [resolve(151,a,112,a)]. given #169 (F,wt=3): 187 -->*_s0(c2,b9) # answer(goal). [resolve(158,a,114,b)]. given #170 (T,wt=3): 202 ->*_s0(c3,c8). [ur(35,a,172,a)]. given #171 (T,wt=3): 204 ->*_s0(c4,c9). [ur(36,a,173,a)]. given #172 (T,wt=3): 210 ->*_s0(c5,c10). [ur(37,a,179,a)]. given #173 (T,wt=3): 211 ->*_s0(b5,b11). [ur(28,a,180,a)]. given #174 (A,wt=6): 184 -->*_s0(b2,x) | -->*_s0(c6,x) # answer(goal). [resolve(134,b,37,b)]. given #175 (F,wt=3): 191 -->*_s0(b5,c6) # answer(goal). [resolve(153,a,132,a)]. given #176 (F,wt=3): 193 -->*_s0(c3,b9) # answer(goal). [resolve(153,b,158,a)]. given #177 (F,wt=3): 195 -->*_s0(b6,c5) # answer(goal). [resolve(161,a,28,b)]. given #178 (F,wt=3): 196 -->*_s0(c9,b3) # answer(goal). [resolve(164,a,40,b)]. given #179 (T,wt=3): 213 ->*_s0(b2,b8). [ur(25,a,186,a)]. given #180 (T,wt=3): 221 ->*_s0(b3,b9). [ur(26,a,188,a)]. given #181 (T,wt=3): 223 ->*_s0(b4,b10). [ur(27,a,189,a)]. given #182 (T,wt=3): 224 ->*_s0(c5,b11). [ur(37,a,190,a)]. given #183 (A,wt=6): 192 -->*_s0(b5,x) | -->*_s0(c4,x) # answer(goal). [resolve(153,a,35,b)]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds: goal. % Length of proof is 60. % Level of proof is 10. % Maximum clause weight is 6.000. % Given clauses 183. 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 2 (exists x2 (->*_s0(b2,x2) & ->*_s0(c2,x2))) # label(goal) # label(non_clause) # label(goal). [goal]. 3 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 4 ->_s0(b10,b11) # label(replacement). [assumption]. 5 ->_s0(b2,b3) # label(replacement). [assumption]. 6 ->_s0(b3,b4) # label(replacement). [assumption]. 7 ->_s0(b4,b5) # label(replacement). [assumption]. 8 ->_s0(b5,b6) # label(replacement). [assumption]. 9 ->_s0(b6,b7) # label(replacement). [assumption]. 10 ->_s0(b7,b8) # label(replacement). [assumption]. 11 ->_s0(b8,b9) # label(replacement). [assumption]. 12 ->_s0(b9,b10) # label(replacement). [assumption]. 13 ->_s0(c10,b11) # label(replacement). [assumption]. 14 ->_s0(c2,c3) # label(replacement). [assumption]. 15 ->_s0(c3,c4) # label(replacement). [assumption]. 16 ->_s0(c4,c5) # label(replacement). [assumption]. 17 ->_s0(c5,c6) # label(replacement). [assumption]. 18 ->_s0(c6,c7) # label(replacement). [assumption]. 19 ->_s0(c7,c8) # label(replacement). [assumption]. 20 ->_s0(c8,c9) # label(replacement). [assumption]. 21 ->_s0(c9,c10) # label(replacement). [assumption]. 22 ->*_s0(x,x) # label(reflexivity). [assumption]. 23 -->*_s0(b2,x) | -->*_s0(c2,x) # label(goal) # answer(goal). [deny(2)]. 24 -->*_s0(b11,x) | ->*_s0(b10,x). [resolve(3,a,4,a)]. 25 -->*_s0(b3,x) | ->*_s0(b2,x). [resolve(3,a,5,a)]. 26 -->*_s0(b4,x) | ->*_s0(b3,x). [resolve(3,a,6,a)]. 27 -->*_s0(b5,x) | ->*_s0(b4,x). [resolve(3,a,7,a)]. 28 -->*_s0(b6,x) | ->*_s0(b5,x). [resolve(3,a,8,a)]. 29 -->*_s0(b7,x) | ->*_s0(b6,x). [resolve(3,a,9,a)]. 30 -->*_s0(b8,x) | ->*_s0(b7,x). [resolve(3,a,10,a)]. 31 -->*_s0(b9,x) | ->*_s0(b8,x). [resolve(3,a,11,a)]. 32 -->*_s0(b10,x) | ->*_s0(b9,x). [resolve(3,a,12,a)]. 33 -->*_s0(b11,x) | ->*_s0(c10,x). [resolve(3,a,13,a)]. 34 -->*_s0(c3,x) | ->*_s0(c2,x). [resolve(3,a,14,a)]. 35 -->*_s0(c4,x) | ->*_s0(c3,x). [resolve(3,a,15,a)]. 36 -->*_s0(c5,x) | ->*_s0(c4,x). [resolve(3,a,16,a)]. 37 -->*_s0(c6,x) | ->*_s0(c5,x). [resolve(3,a,17,a)]. 38 -->*_s0(c7,x) | ->*_s0(c6,x). [resolve(3,a,18,a)]. 39 -->*_s0(c8,x) | ->*_s0(c7,x). [resolve(3,a,19,a)]. 40 -->*_s0(c9,x) | ->*_s0(c8,x). [resolve(3,a,20,a)]. 41 -->*_s0(c10,x) | ->*_s0(c9,x). [resolve(3,a,21,a)]. 44 ->*_s0(b10,b11). [ur(24,a,22,a)]. 45 -->*_s0(b3,x) | -->*_s0(c2,x) # answer(goal). [resolve(25,b,23,a)]. 54 ->*_s0(c10,b11). [ur(33,a,22,a)]. 69 ->*_s0(b9,b11). [ur(32,a,44,a)]. 74 -->*_s0(c2,x) | -->*_s0(b4,x) # answer(goal). [resolve(45,a,26,b)]. 89 ->*_s0(c9,b11). [ur(41,a,54,a)]. 108 ->*_s0(b8,b11). [ur(31,a,69,a)]. 112 -->*_s0(b4,x) | -->*_s0(c3,x) # answer(goal). [resolve(74,a,34,b)]. 128 ->*_s0(c8,b11). [ur(40,a,89,a)]. 143 ->*_s0(b7,b11). [ur(30,a,108,a)]. 153 -->*_s0(c3,x) | -->*_s0(b5,x) # answer(goal). [resolve(112,a,27,b)]. 160 ->*_s0(c7,b11). [ur(39,a,128,a)]. 180 ->*_s0(b6,b11). [ur(29,a,143,a)]. 190 ->*_s0(c6,b11). [ur(38,a,160,a)]. 192 -->*_s0(b5,x) | -->*_s0(c4,x) # answer(goal). [resolve(153,a,35,b)]. 211 ->*_s0(b5,b11). [ur(28,a,180,a)]. 224 ->*_s0(c5,b11). [ur(37,a,190,a)]. 249 ->*_s0(c4,b11). [ur(36,a,224,a)]. 250 $F # answer(goal). [resolve(192,a,211,a),unit_del(a,249)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=183. Generated=667. Kept=228. proofs=1. Usable=183. Sos=45. Demods=0. Limbo=0, Disabled=39. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=438. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=10. Nonunit_bsub_feature_tests=67. Megabytes=0.24. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 2696486 exit (max_proofs) Fri Jun 9 15:47:26 2023 The problem is feasible. The problem is confluent.