0.015/0.015 YES 0.015/0.015 0.015/0.015 Problem 1: 0.015/0.015 0.015/0.015 0.015/0.015 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.015/0.015 Confluence Problem: 0.015/0.015 (VAR vNonEmpty:S M:S N:S) 0.015/0.015 (STRATEGY CONTEXTSENSITIVE 0.015/0.015 (U11 1) 0.015/0.015 (U12 1) 0.015/0.015 (plus 1 2) 0.015/0.015 (0) 0.015/0.015 (fSNonEmpty) 0.015/0.015 (s 1) 0.015/0.015 (tt) 0.015/0.015 ) 0.015/0.015 (RULES 0.015/0.015 U11(tt,M:S,N:S) -> U12(tt,M:S,N:S) 0.015/0.015 U12(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.015/0.015 plus(N:S,0) -> N:S 0.015/0.015 plus(N:S,s(M:S)) -> U11(tt,M:S,N:S) 0.015/0.015 ) 0.015/0.015 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.015/0.015 0.015/0.015 0.015/0.015 Problem 1: 0.015/0.015 0.015/0.015 CleanTRS Processor: 0.015/0.015 0.015/0.015 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.015/0.015 Confluence Problem: 0.015/0.015 (VAR vNonEmpty:S M:S N:S) 0.015/0.015 (STRATEGY CONTEXTSENSITIVE 0.015/0.015 (U11 1) 0.015/0.015 (U12 1) 0.015/0.015 (plus 1 2) 0.015/0.015 (0) 0.015/0.015 (fSNonEmpty) 0.015/0.015 (s 1) 0.015/0.015 (tt) 0.015/0.015 ) 0.015/0.015 (RULES 0.015/0.015 U11(tt,M:S,N:S) -> U12(tt,M:S,N:S) 0.015/0.015 U12(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.015/0.015 plus(N:S,0) -> N:S 0.015/0.015 plus(N:S,s(M:S)) -> U11(tt,M:S,N:S) 0.015/0.015 ) 0.015/0.015 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.015/0.015 0.015/0.015 0.015/0.015 Problem 1: 0.015/0.015 0.015/0.015 Modular Confluence Combinations Decomposition Processor: 0.015/0.015 It is a CTRS -> No modular confluence 0.015/0.015 0.015/0.015 Problem 1: 0.015/0.015 CS-TRS Processor: 0.015/0.015 R is a CS-TRS 0.015/0.015 0.015/0.015 Problem 1: 0.015/0.015 Termination Processor: 0.015/0.015 (STRATEGY CONTEXTSENSITIVE 0.015/0.015 (U11 1) 0.015/0.015 (U12 1) 0.015/0.015 (plus 1 2) 0.015/0.015 (0) 0.015/0.015 (fSNonEmpty) 0.015/0.015 (s 1) 0.015/0.015 (tt) 0.015/0.015 ) 0.015/0.015 Terminating? 0.015/0.015 YES 0.015/0.015 0.015/0.015 Problem 1: 0.015/0.015 0.015/0.015 (VAR vu95NonEmpty:S vNonEmpty:S M:S N:S) 0.015/0.015 (STRATEGY CONTEXTSENSITIVE 0.015/0.015 (U11 1) 0.015/0.015 (U12 1) 0.015/0.015 (plus 1 2) 0.015/0.015 (num0) 0.015/0.015 (fSNonEmpty) 0.015/0.015 (s 1) 0.015/0.015 (tt) 0.015/0.015 ) 0.015/0.015 (RULES 0.015/0.015 U11(tt,M:S,N:S) -> U12(tt,M:S,N:S) 0.015/0.015 U12(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.015/0.015 plus(N:S,num0) -> N:S 0.015/0.015 plus(N:S,s(M:S)) -> U11(tt,M:S,N:S) 0.015/0.015 ) 0.015/0.015 0.015/0.015 Problem 1: 0.015/0.015 0.015/0.015 Innermost Equivalent Processor: 0.015/0.015 -> Rules: 0.015/0.015 U11(tt,M:S,N:S) -> U12(tt,M:S,N:S) 0.015/0.015 U12(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.015/0.015 plus(N:S,num0) -> N:S 0.015/0.015 plus(N:S,s(M:S)) -> U11(tt,M:S,N:S) 0.015/0.015 -> The context-sensitive term rewriting system is an orthogonal system. Therefore, innermost cs-termination implies cs-termination. 0.015/0.015 0.015/0.015 0.015/0.015 Problem 1: 0.015/0.015 0.015/0.015 Dependency Pairs Processor: 0.015/0.015 -> Pairs: 0.015/0.015 U11Sharp(tt,M:S,N:S) -> U12Sharp(tt,M:S,N:S) 0.015/0.015 U12Sharp(tt,M:S,N:S) -> PLUS(N:S,M:S) 0.015/0.015 U12Sharp(tt,M:S,N:S) -> M:S 0.015/0.015 U12Sharp(tt,M:S,N:S) -> N:S 0.015/0.015 PLUS(N:S,s(M:S)) -> U11Sharp(tt,M:S,N:S) 0.015/0.015 -> Rules: 0.015/0.015 U11(tt,M:S,N:S) -> U12(tt,M:S,N:S) 0.015/0.015 U12(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.015/0.015 plus(N:S,num0) -> N:S 0.015/0.015 plus(N:S,s(M:S)) -> U11(tt,M:S,N:S) 0.015/0.015 -> Unhiding Rules: 0.015/0.015 Empty 0.015/0.015 0.015/0.015 Problem 1: 0.015/0.015 0.015/0.015 SCC Processor: 0.015/0.015 -> Pairs: 0.015/0.015 U11Sharp(tt,M:S,N:S) -> U12Sharp(tt,M:S,N:S) 0.015/0.015 U12Sharp(tt,M:S,N:S) -> PLUS(N:S,M:S) 0.015/0.015 U12Sharp(tt,M:S,N:S) -> M:S 0.015/0.015 U12Sharp(tt,M:S,N:S) -> N:S 0.015/0.015 PLUS(N:S,s(M:S)) -> U11Sharp(tt,M:S,N:S) 0.015/0.015 -> Rules: 0.015/0.015 U11(tt,M:S,N:S) -> U12(tt,M:S,N:S) 0.015/0.015 U12(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.015/0.015 plus(N:S,num0) -> N:S 0.015/0.015 plus(N:S,s(M:S)) -> U11(tt,M:S,N:S) 0.015/0.015 -> Unhiding rules: 0.015/0.015 Empty 0.015/0.015 ->Strongly Connected Components: 0.015/0.015 ->->Cycle: 0.015/0.015 ->->-> Pairs: 0.015/0.015 U11Sharp(tt,M:S,N:S) -> U12Sharp(tt,M:S,N:S) 0.015/0.015 U12Sharp(tt,M:S,N:S) -> PLUS(N:S,M:S) 0.015/0.015 PLUS(N:S,s(M:S)) -> U11Sharp(tt,M:S,N:S) 0.015/0.015 ->->-> Rules: 0.015/0.015 U11(tt,M:S,N:S) -> U12(tt,M:S,N:S) 0.015/0.015 U12(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.015/0.015 plus(N:S,num0) -> N:S 0.015/0.015 plus(N:S,s(M:S)) -> U11(tt,M:S,N:S) 0.015/0.015 ->->-> Unhiding rules: 0.015/0.015 Empty 0.015/0.015 0.015/0.015 Problem 1: 0.015/0.015 0.015/0.015 SubNColl Processor: 0.015/0.015 -> Pairs: 0.015/0.015 U11Sharp(tt,M:S,N:S) -> U12Sharp(tt,M:S,N:S) 0.015/0.015 U12Sharp(tt,M:S,N:S) -> PLUS(N:S,M:S) 0.015/0.015 PLUS(N:S,s(M:S)) -> U11Sharp(tt,M:S,N:S) 0.015/0.015 -> Rules: 0.015/0.015 U11(tt,M:S,N:S) -> U12(tt,M:S,N:S) 0.015/0.015 U12(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.015/0.015 plus(N:S,num0) -> N:S 0.015/0.015 plus(N:S,s(M:S)) -> U11(tt,M:S,N:S) 0.015/0.015 -> Unhiding rules: 0.015/0.015 Empty 0.015/0.015 ->Projection: 0.015/0.015 pi(U11Sharp) = 2 0.015/0.015 pi(U12Sharp) = 2 0.015/0.015 pi(PLUS) = 2 0.015/0.015 0.015/0.015 Problem 1: 0.015/0.015 0.015/0.015 SCC Processor: 0.015/0.015 -> Pairs: 0.015/0.015 U11Sharp(tt,M:S,N:S) -> U12Sharp(tt,M:S,N:S) 0.015/0.015 U12Sharp(tt,M:S,N:S) -> PLUS(N:S,M:S) 0.015/0.015 -> Rules: 0.015/0.015 U11(tt,M:S,N:S) -> U12(tt,M:S,N:S) 0.015/0.015 U12(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.015/0.015 plus(N:S,num0) -> N:S 0.015/0.015 plus(N:S,s(M:S)) -> U11(tt,M:S,N:S) 0.015/0.015 -> Unhiding rules: 0.015/0.015 Empty 0.015/0.015 ->Strongly Connected Components: 0.015/0.015 There is no strongly connected component 0.015/0.015 0.015/0.015 The problem is finite. 0.015/0.015 0.015/0.015 Problem 1.1: 0.015/0.015 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.015/0.015 Confluence Problem: 0.015/0.015 (VAR vNonEmpty:S M:S N:S) 0.015/0.015 (STRATEGY CONTEXTSENSITIVE 0.015/0.015 (U11 1) 0.015/0.015 (U12 1) 0.015/0.015 (plus 1 2) 0.015/0.015 (0) 0.015/0.015 (fSNonEmpty) 0.015/0.015 (s 1) 0.015/0.015 (tt) 0.015/0.015 ) 0.015/0.015 (RULES 0.015/0.015 U11(tt,M:S,N:S) -> U12(tt,M:S,N:S) 0.015/0.015 U12(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.015/0.015 plus(N:S,0) -> N:S 0.015/0.015 plus(N:S,s(M:S)) -> U11(tt,M:S,N:S) 0.015/0.015 ) 0.015/0.015 Terminating:"YES" 0.015/0.015 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.015/0.015 0.015/0.015 LH u-Critical Pairs Processor [JLAMP21-Def12]: 0.015/0.015 ->LH u-Critical Pair: 0.015/0.015 Rule 4 (l :-> r) => plus(N:S,s(M:S)) -> U11(tt,M:S,N:S) 0.015/0.015 Var x => M:S 0.015/0.015 Var y => y:S 0.015/0.015 Pos M:S in l => [2,1] 0.015/0.015 s => plus(N:S,s(y:S)) 0.015/0.015 t => U11(tt,M:S,N:S) 0.015/0.015 C => M:S \-> y:S 0.015/0.015 NW => 0 0.015/0.015 0.015/0.015 0.015/0.015 ->LH u-Critical Pair: 0.015/0.015 Rule 4 (l :-> r) => plus(N:S,s(M:S)) -> U11(tt,M:S,N:S) 0.015/0.015 Var x => N:S 0.015/0.015 Var y => y:S 0.015/0.015 Pos N:S in l => [1] 0.015/0.015 s => plus(y:S,s(M:S)) 0.015/0.015 t => U11(tt,M:S,N:S) 0.015/0.015 C => N:S \-> y:S 0.015/0.015 NW => 0 0.015/0.015 0.015/0.015 0.015/0.015 Problem 1.1: 0.015/0.015 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.015/0.015 Confluence Problem: 0.015/0.015 (VAR vNonEmpty:S M:S N:S) 0.015/0.015 (STRATEGY CONTEXTSENSITIVE 0.015/0.015 (U11 1) 0.015/0.015 (U12 1) 0.015/0.015 (plus 1 2) 0.015/0.015 (0) 0.015/0.015 (fSNonEmpty) 0.015/0.015 (s 1) 0.015/0.015 (tt) 0.015/0.015 ) 0.015/0.015 (RULES 0.015/0.015 U11(tt,M:S,N:S) -> U12(tt,M:S,N:S) 0.015/0.015 U12(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.015/0.015 plus(N:S,0) -> N:S 0.015/0.015 plus(N:S,s(M:S)) -> U11(tt,M:S,N:S) 0.015/0.015 ) 0.015/0.015 Critical Pairs: 0.015/0.015 | M:S \-> y:S => Not trivial, Not overlay, NW0, N1 0.015/0.015 | N:S \-> y:S => Not trivial, Not overlay, NW0, N2 0.015/0.015 Terminating:"YES" 0.015/0.015 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.015/0.015 0.015/0.015 Huet Levy NW Processor: 0.015/0.015 -> Rules: 0.015/0.015 U11(tt,M:S,N:S) -> U12(tt,M:S,N:S) 0.015/0.015 U12(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.015/0.015 plus(N:S,0) -> N:S 0.015/0.015 plus(N:S,s(M:S)) -> U11(tt,M:S,N:S) 0.015/0.015 -> Vars: 0.015/0.015 M, N, M, N, N, M, N 0.015/0.015 -> UVars: 0.015/0.015 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [], UV-LFrozen: [M, N], UV-RFrozen: [M, N]) 0.015/0.015 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [M, N], UV-LFrozen: [M, N], UV-RFrozen: []) 0.015/0.015 (UV-RuleId: 3, UV-LActive: [N], UV-RActive: [N], UV-LFrozen: [], UV-RFrozen: []) 0.015/0.015 (UV-RuleId: 4, UV-LActive: [M, N], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [M, N]) 0.015/0.015 -> FVars: 0.015/0.015 x3, x4, x5, x6, x7, x8, x9 0.015/0.015 -> PVars: 0.015/0.015 y: [y], M: [x3, x5, x8], N: [x4, x6, x7, x9] 0.015/0.015 0.015/0.015 -> Rlps: 0.015/0.015 (rule: U11(tt,x3:S,x4:S) -> U12(tt,x3:S,x4:S), id: 1, possubterms: U11(tt,x3:S,x4:S)->[], tt->[1]) 0.015/0.015 (rule: U12(tt,x5:S,x6:S) -> s(plus(x6:S,x5:S)), id: 2, possubterms: U12(tt,x5:S,x6:S)->[], tt->[1]) 0.015/0.015 (rule: plus(x7:S,0) -> x7:S, id: 3, possubterms: plus(x7:S,0)->[], 0->[2]) 0.015/0.015 (rule: plus(x9:S,s(x8:S)) -> U11(tt,x8:S,x9:S), id: 4, possubterms: plus(x9:S,s(x8:S))->[], s(x8:S)->[2]) 0.015/0.015 0.015/0.015 -> Unifications: 0.015/0.015 0.015/0.015 0.015/0.015 -> Critical pairs info: 0.015/0.015 | M:S \-> y:S => Not trivial, Not overlay, NW0, N1 0.015/0.015 | N:S \-> y:S => Not trivial, Not overlay, NW0, N2 0.015/0.015 0.015/0.015 -> Problem conclusions: 0.015/0.015 Left linear, Right linear, Linear 0.015/0.015 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.015/0.015 Not Huet-Levy confluent, Not Newman confluent 0.015/0.015 R is a CS-TRS, Not left-homogeneous u-replacing variables 0.015/0.015 0.015/0.015 0.015/0.015 0.015/0.015 The problem is decomposed in 2 subproblems. 0.015/0.015 0.015/0.015 Problem 1.1.1: 0.015/0.015 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.015/0.015 Confluence Problem: 0.015/0.015 (VAR vNonEmpty:S M:S N:S) 0.015/0.015 (STRATEGY CONTEXTSENSITIVE 0.015/0.015 (U11 1) 0.015/0.015 (U12 1) 0.015/0.015 (plus 1 2) 0.015/0.015 (0) 0.015/0.015 (fSNonEmpty) 0.015/0.015 (s 1) 0.015/0.015 (tt) 0.015/0.015 ) 0.015/0.015 (RULES 0.015/0.015 U11(tt,M:S,N:S) -> U12(tt,M:S,N:S) 0.015/0.015 U12(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.015/0.015 plus(N:S,0) -> N:S 0.015/0.015 plus(N:S,s(M:S)) -> U11(tt,M:S,N:S) 0.015/0.015 ) 0.015/0.015 Critical Pairs: 0.015/0.015 | M:S \-> y:S => Not trivial, Not overlay, NW0, N1 0.015/0.015 Terminating:"YES" 0.015/0.015 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.015/0.015 0.015/0.015 Huet Brute Force Joinability Processor: 0.015/0.015 That is a LHCP. Trying another procedure. 0.015/0.015 0.015/0.015 Problem 1.1.1: 0.015/0.015 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.015/0.015 Confluence Problem: 0.015/0.015 (VAR vNonEmpty:S M:S N:S) 0.015/0.015 (STRATEGY CONTEXTSENSITIVE 0.015/0.015 (U11 1) 0.015/0.015 (U12 1) 0.015/0.015 (plus 1 2) 0.015/0.015 (0) 0.015/0.015 (fSNonEmpty) 0.015/0.015 (s 1) 0.015/0.015 (tt) 0.015/0.015 ) 0.015/0.015 (RULES 0.015/0.015 U11(tt,M:S,N:S) -> U12(tt,M:S,N:S) 0.015/0.015 U12(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.015/0.015 plus(N:S,0) -> N:S 0.015/0.015 plus(N:S,s(M:S)) -> U11(tt,M:S,N:S) 0.015/0.015 ) 0.015/0.015 Critical Pairs: 0.015/0.015 | M:S \-> y:S => Not trivial, Not overlay, NW0, N1 0.015/0.015 Terminating:"YES" 0.015/0.015 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.015/0.015 0.015/0.015 Prover9 LHCP Convergence Checker Processor: 0.015/0.015 formulas(sos). 0.015/0.015 %Reflexivity 0.015/0.015 reds(x,x). 0.015/0.015 0.015/0.015 %Transitivity 0.015/0.015 (red(x,y) & reds(y,z)) -> reds(x,z). 0.015/0.015 0.015/0.015 %Congruence 0.015/0.015 red(x,y) -> red(U11(x,z2,z3),U11(y,z2,z3)). 0.015/0.015 red(x,y) -> red(U12(x,z2,z3),U12(y,z2,z3)). 0.015/0.015 red(x,y) -> red(plus(x,z2),plus(y,z2)). 0.015/0.015 red(x,y) -> red(plus(z1,x),plus(z1,y)). 0.015/0.015 0.015/0.015 0.015/0.015 red(x,y) -> red(s(x),s(y)). 0.015/0.015 %Replacement 0.015/0.015 all M all N ( red(U11(tt,M,N),U12(tt,M,N)) ). 0.015/0.015 all M all N ( red(U12(tt,M,N),s(plus(N,M))) ). 0.015/0.015 all N ( red(plus(N,0),N) ). 0.015/0.015 all M all N ( red(plus(N,s(M)),U11(tt,M,N)) ). 0.015/0.015 end_of_list. 0.015/0.015 0.015/0.015 formulas(goals). 0.015/0.015 all M all y exists z ( red(M,y) -> (reds(plus(c_N,s(y)),z) & reds(U11(tt,M,c_N),z)) ). 0.015/0.015 end_of_list. 0.015/0.015 0.015/0.015 Proof: 0.015/0.015 ============================== Prover9 =============================== 0.015/0.015 Prover9 (64) version 2009-11A, November 2009. 0.015/0.015 Process 43168 was started by ubuntu on ubuntu, 0.015/0.015 Tue Nov 16 11:31:22 2021 0.015/0.015 The command was "./prover9 -t 30 -f /tmp/prover943130-4.in". 0.015/0.015 ============================== end of head =========================== 0.015/0.015 0.015/0.015 ============================== INPUT ================================= 0.015/0.015 0.015/0.015 % Reading from file /tmp/prover943130-4.in 0.015/0.015 0.015/0.015 0.015/0.015 formulas(sos). 0.015/0.015 reds(x,x). 0.015/0.015 red(x,y) & reds(y,z) -> reds(x,z). 0.015/0.015 red(x,y) -> red(U11(x,z2,z3),U11(y,z2,z3)). 0.015/0.015 red(x,y) -> red(U12(x,z2,z3),U12(y,z2,z3)). 0.015/0.015 red(x,y) -> red(plus(x,z2),plus(y,z2)). 0.015/0.015 red(x,y) -> red(plus(z1,x),plus(z1,y)). 0.015/0.015 red(x,y) -> red(s(x),s(y)). 0.015/0.015 (all M all N red(U11(tt,M,N),U12(tt,M,N))). 0.015/0.015 (all M all N red(U12(tt,M,N),s(plus(N,M)))). 0.015/0.015 (all N red(plus(N,0),N)). 0.015/0.015 (all M all N red(plus(N,s(M)),U11(tt,M,N))). 0.015/0.015 end_of_list. 0.015/0.015 0.015/0.015 formulas(goals). 0.015/0.015 (all M all y exists z (red(M,y) -> reds(plus(c_N,s(y)),z) & reds(U11(tt,M,c_N),z))). 0.015/0.015 end_of_list. 0.015/0.015 assign(max_megs,-1). 0.015/0.015 set(quiet). 0.015/0.015 0.015/0.015 ============================== end of input ========================== 0.015/0.015 0.015/0.015 % From the command line: assign(max_seconds, 30). 0.015/0.015 0.015/0.015 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 0.015/0.015 0.015/0.015 % Formulas that are not ordinary clauses: 0.015/0.015 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 0.015/0.015 2 red(x,y) -> red(U11(x,z2,z3),U11(y,z2,z3)) # label(non_clause). [assumption]. 0.015/0.015 3 red(x,y) -> red(U12(x,z2,z3),U12(y,z2,z3)) # label(non_clause). [assumption]. 0.015/0.015 4 red(x,y) -> red(plus(x,z2),plus(y,z2)) # label(non_clause). [assumption]. 0.015/0.015 5 red(x,y) -> red(plus(z1,x),plus(z1,y)) # label(non_clause). [assumption]. 0.015/0.015 6 red(x,y) -> red(s(x),s(y)) # label(non_clause). [assumption]. 0.015/0.015 7 (all M all N red(U11(tt,M,N),U12(tt,M,N))) # label(non_clause). [assumption]. 0.015/0.015 8 (all M all N red(U12(tt,M,N),s(plus(N,M)))) # label(non_clause). [assumption]. 0.015/0.015 9 (all N red(plus(N,0),N)) # label(non_clause). [assumption]. 0.015/0.015 10 (all M all N red(plus(N,s(M)),U11(tt,M,N))) # label(non_clause). [assumption]. 0.015/0.015 11 (all M all y exists z (red(M,y) -> reds(plus(c_N,s(y)),z) & reds(U11(tt,M,c_N),z))) # label(non_clause) # label(goal). [goal]. 0.015/0.015 0.015/0.015 ============================== end of process non-clausal formulas === 0.015/0.015 0.015/0.015 ============================== PROCESS INITIAL CLAUSES =============== 0.015/0.015 0.015/0.015 % Clauses before input processing: 0.015/0.015 0.015/0.015 formulas(usable). 0.015/0.015 end_of_list. 0.015/0.015 0.015/0.015 formulas(sos). 0.015/0.015 reds(x,x). [assumption]. 0.015/0.015 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 0.015/0.015 -red(x,y) | red(U11(x,z,u),U11(y,z,u)). [clausify(2)]. 0.015/0.015 -red(x,y) | red(U12(x,z,u),U12(y,z,u)). [clausify(3)]. 0.015/0.015 -red(x,y) | red(plus(x,z),plus(y,z)). [clausify(4)]. 0.015/0.015 -red(x,y) | red(plus(z,x),plus(z,y)). [clausify(5)]. 0.015/0.015 -red(x,y) | red(s(x),s(y)). [clausify(6)]. 0.015/0.015 red(U11(tt,x,y),U12(tt,x,y)). [clausify(7)]. 0.015/0.015 red(U12(tt,x,y),s(plus(y,x))). [clausify(8)]. 0.015/0.015 red(plus(x,0),x). [clausify(9)]. 0.015/0.015 red(plus(x,s(y)),U11(tt,y,x)). [clausify(10)]. 0.015/0.015 red(c1,c2). [deny(11)]. 0.015/0.015 -reds(plus(c_N,s(c2)),x) | -reds(U11(tt,c1,c_N),x). [deny(11)]. 0.015/0.015 end_of_list. 0.015/0.015 0.015/0.015 formulas(demodulators). 0.015/0.015 end_of_list. 0.015/0.015 0.015/0.015 ============================== PREDICATE ELIMINATION ================= 0.015/0.015 0.015/0.015 ============================== end predicate elimination ============= 0.015/0.015 0.015/0.015 Auto_denials: (no changes). 0.015/0.015 0.015/0.015 Term ordering decisions: 0.015/0.015 0.015/0.015 kept: 12 reds(x,x). [assumption]. 0.015/0.015 kept: 13 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 0.015/0.015 kept: 14 -red(x,y) | red(U11(x,z,u),U11(y,z,u)). [clausify(2)]. 0.015/0.015 kept: 15 -red(x,y) | red(U12(x,z,u),U12(y,z,u)). [clausify(3)]. 0.015/0.015 kept: 16 -red(x,y) | red(plus(x,z),plus(y,z)). [clausify(4)]. 0.015/0.015 kept: 17 -red(x,y) | red(plus(z,x),plus(z,y)). [clausify(5)]. 0.015/0.015 kept: 18 -red(x,y) | red(s(x),s(y)). [clausify(6)]. 0.015/0.015 kept: 19 red(U11(tt,x,y),U12(tt,x,y)). [clausify(7)]. 0.015/0.015 kept: 20 red(U12(tt,x,y),s(plus(y,x))). [clausify(8)]. 0.015/0.015 kept: 21 red(plus(x,0),x). [clausify(9)]. 0.015/0.015 kept: 22 red(plus(x,s(y)),U11(tt,y,x)). [clausify(10)]. 0.015/0.015 kept: 23 red(c1,c2). [deny(11)]. 0.015/0.015 kept: 24 -reds(plus(c_N,s(c2)),x) | -reds(U11(tt,c1,c_N),x). [deny(11)]. 0.015/0.015 0.015/0.015 ============================== end of process initial clauses ======== 0.015/0.015 0.015/0.015 ============================== CLAUSES FOR SEARCH ==================== 0.015/0.015 0.015/0.015 % Clauses after input processing: 0.015/0.015 0.015/0.015 formulas(usable). 0.015/0.015 end_of_list. 0.015/0.015 0.015/0.015 formulas(sos). 0.015/0.015 12 reds(x,x). [assumption]. 0.015/0.015 13 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 0.015/0.015 14 -red(x,y) | red(U11(x,z,u),U11(y,z,u)). [clausify(2)]. 0.015/0.015 15 -red(x,y) | red(U12(x,z,u),U12(y,z,u)). [clausify(3)]. 0.015/0.015 16 -red(x,y) | red(plus(x,z),plus(y,z)). [clausify(4)]. 0.015/0.015 17 -red(x,y) | red(plus(z,x),plus(z,y)). [clausify(5)]. 0.015/0.015 18 -red(x,y) | red(s(x),s(y)). [clausify(6)]. 0.015/0.015 19 red(U11(tt,x,y),U12(tt,x,y)). [clausify(7)]. 0.015/0.015 20 red(U12(tt,x,y),s(plus(y,x))). [clausify(8)]. 0.015/0.015 21 red(plus(x,0),x). [clausify(9)]. 0.015/0.015 22 red(plus(x,s(y)),U11(tt,y,x)). [clausify(10)]. 0.015/0.015 23 red(c1,c2). [deny(11)]. 0.015/0.015 24 -reds(plus(c_N,s(c2)),x) | -reds(U11(tt,c1,c_N),x). [deny(11)]. 0.015/0.015 end_of_list. 0.015/0.015 0.015/0.015 formulas(demodulators). 0.015/0.015 end_of_list. 0.015/0.015 0.015/0.015 ============================== end of clauses for search ============= 0.015/0.015 0.015/0.015 ============================== SEARCH ================================ 0.015/0.015 0.015/0.015 % Starting search at 0.00 seconds. 0.015/0.015 0.015/0.015 given #1 (I,wt=3): 12 reds(x,x). [assumption]. 0.015/0.015 0.015/0.015 given #2 (I,wt=9): 13 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 0.015/0.015 0.015/0.015 given #3 (I,wt=12): 14 -red(x,y) | red(U11(x,z,u),U11(y,z,u)). [clausify(2)]. 0.015/0.015 0.015/0.015 given #4 (I,wt=12): 15 -red(x,y) | red(U12(x,z,u),U12(y,z,u)). [clausify(3)]. 0.015/0.015 0.015/0.015 given #5 (I,wt=10): 16 -red(x,y) | red(plus(x,z),plus(y,z)). [clausify(4)]. 0.015/0.015 0.015/0.015 given #6 (I,wt=10): 17 -red(x,y) | red(plus(z,x),plus(z,y)). [clausify(5)]. 0.015/0.015 0.015/0.015 given #7 (I,wt=8): 18 -red(x,y) | red(s(x),s(y)). [clausify(6)]. 0.015/0.015 0.015/0.015 given #8 (I,wt=9): 19 red(U11(tt,x,y),U12(tt,x,y)). [clausify(7)]. 0.015/0.015 0.015/0.015 given #9 (I,wt=9): 20 red(U12(tt,x,y),s(plus(y,x))). [clausify(8)]. 0.015/0.015 0.015/0.015 given #10 (I,wt=5): 21 red(plus(x,0),x). [clausify(9)]. 0.015/0.015 0.015/0.015 given #11 (I,wt=9): 22 red(plus(x,s(y)),U11(tt,y,x)). [clausify(10)]. 0.015/0.015 0.015/0.015 given #12 (I,wt=3): 23 red(c1,c2). [deny(11)]. 0.015/0.015 0.015/0.015 given #13 (I,wt=12): 24 -reds(plus(c_N,s(c2)),x) | -reds(U11(tt,c1,c_N),x). [deny(11)]. 0.015/0.015 0.015/0.015 given #14 (A,wt=11): 25 red(s(U11(tt,x,y)),s(U12(tt,x,y))). [ur(18,a,19,a)]. 0.015/0.015 0.015/0.015 given #15 (F,wt=9): 56 -reds(U11(tt,c1,c_N),plus(c_N,s(c2))). [resolve(24,a,12,a)]. 0.015/0.015 0.015/0.015 given #16 (F,wt=9): 58 -reds(plus(c_N,s(c2)),U11(tt,c1,c_N)). [resolve(24,b,12,a)]. 0.015/0.015 0.015/0.015 given #17 (F,wt=9): 66 -red(U11(tt,c1,c_N),plus(c_N,s(c2))). [ur(13,b,12,a,c,56,a)]. 0.015/0.015 0.015/0.015 given #18 (F,wt=9): 67 -reds(U12(tt,c1,c_N),plus(c_N,s(c2))). [ur(13,a,19,a,c,56,a)]. 0.015/0.015 0.015/0.015 given #19 (T,wt=3): 54 reds(c1,c2). [ur(13,a,23,a,b,12,a)]. 0.015/0.015 0.015/0.015 given #20 (T,wt=5): 42 reds(plus(x,0),x). [ur(13,a,21,a,b,12,a)]. 0.015/0.015 0.015/0.015 given #21 (T,wt=5): 49 red(s(c1),s(c2)). [ur(18,a,23,a)]. 0.015/0.015 0.015/0.015 given #22 (T,wt=5): 74 reds(plus(c1,0),c2). [ur(13,a,21,a,b,54,a)]. 0.015/0.015 0.015/0.015 given #23 (A,wt=13): 26 red(plus(x,U11(tt,y,z)),plus(x,U12(tt,y,z))). [ur(17,a,19,a)]. 0.015/0.015 0.015/0.015 given #24 (F,wt=9): 69 -red(plus(c_N,s(c2)),U11(tt,c1,c_N)). [ur(13,b,12,a,c,58,a)]. 0.015/0.015 0.015/0.015 given #25 (F,wt=9): 70 -reds(U11(tt,c2,c_N),U11(tt,c1,c_N)). [ur(13,a,22,a,c,58,a)]. 0.015/0.015 0.015/0.015 given #26 (F,wt=9): 72 -red(U12(tt,c1,c_N),plus(c_N,s(c2))). [ur(13,b,12,a,c,67,a)]. 0.015/0.015 0.015/0.015 given #27 (F,wt=9): 73 -reds(s(plus(c_N,c1)),plus(c_N,s(c2))). [ur(13,a,20,a,c,67,a)]. 0.015/0.015 0.015/0.015 given #28 (T,wt=5): 84 reds(s(c1),s(c2)). [ur(13,a,49,a,b,12,a)]. 0.015/0.015 0.015/0.015 given #29 (T,wt=7): 37 red(s(plus(x,0)),s(x)). [ur(18,a,21,a)]. 0.015/0.015 0.015/0.015 given #30 (T,wt=7): 50 red(plus(x,c1),plus(x,c2)). [ur(17,a,23,a)]. 0.015/0.015 0.015/0.015 given #31 (T,wt=7): 51 red(plus(c1,x),plus(c2,x)). [ur(16,a,23,a)]. 0.015/0.015 0.015/0.015 given #32 (A,wt=13): 27 red(plus(U11(tt,x,y),z),plus(U12(tt,x,y),z)). [ur(16,a,19,a)]. 0.015/0.015 0.015/0.015 given #33 (F,wt=9): 94 -red(U11(tt,c2,c_N),U11(tt,c1,c_N)). [ur(13,b,12,a,c,70,a)]. 0.015/0.015 0.015/0.015 given #34 (F,wt=9): 95 -reds(U12(tt,c2,c_N),U11(tt,c1,c_N)). [ur(13,a,19,a,c,70,a)]. 0.015/0.015 0.015/0.015 given #35 (F,wt=9): 98 -red(s(plus(c_N,c1)),plus(c_N,s(c2))). [ur(13,b,12,a,c,73,a)]. 0.015/0.015 0.015/0.015 given #36 (F,wt=9): 128 -red(U12(tt,c2,c_N),U11(tt,c1,c_N)). [ur(13,b,12,a,c,95,a)]. 0.015/0.015 0.015/0.015 given #37 (T,wt=7): 75 reds(plus(plus(x,0),0),x). [ur(13,a,21,a,b,42,a)]. 0.015/0.015 0.015/0.015 given #38 (T,wt=7): 79 red(s(s(c1)),s(s(c2))). [ur(18,a,49,a)]. 0.015/0.015 0.015/0.015 given #39 (T,wt=7): 85 reds(plus(plus(c1,0),0),c2). [ur(13,a,21,a,b,74,a)]. 0.015/0.015 0.015/0.015 given #40 (T,wt=7): 99 reds(plus(s(c1),0),s(c2)). [ur(13,a,21,a,b,84,a)]. 0.015/0.015 0.015/0.015 given #41 (A,wt=15): 28 red(U12(U11(tt,x,y),z,u),U12(U12(tt,x,y),z,u)). [ur(15,a,19,a)]. 0.015/0.015 0.015/0.015 given #42 (F,wt=9): 129 -reds(s(plus(c_N,c2)),U11(tt,c1,c_N)). [ur(13,a,20,a,c,95,a)]. 0.015/0.015 0.015/0.015 given #43 (F,wt=9): 154 -red(s(plus(c_N,c2)),U11(tt,c1,c_N)). [ur(13,b,12,a,c,129,a)]. 0.015/0.015 0.015/0.015 given #44 (F,wt=11): 76 -red(U12(tt,c1,c_N),plus(plus(c_N,s(c2)),0)). [ur(13,b,42,a,c,67,a)]. 0.015/0.015 0.015/0.015 given #45 (F,wt=11): 77 -red(plus(c_N,s(c2)),plus(U11(tt,c1,c_N),0)). [ur(13,b,42,a,c,58,a)]. 0.015/0.015 0.015/0.015 given #46 (T,wt=7): 105 reds(s(plus(c1,0)),s(c2)). [ur(13,a,37,a,b,84,a)]. 0.015/0.015 0.015/0.015 given #47 (T,wt=7): 106 reds(s(plus(x,0)),s(x)). [ur(13,a,37,a,b,12,a)]. 0.015/0.015 0.015/0.015 given #48 (T,wt=7): 112 reds(plus(x,c1),plus(x,c2)). [ur(13,a,50,a,b,12,a)]. 0.015/0.015 0.015/0.015 given #49 (T,wt=7): 118 reds(plus(c1,x),plus(c2,x)). [ur(13,a,51,a,b,12,a)]. 0.015/0.015 0.015/0.015 given #50 (A,wt=15): 29 red(U11(U11(tt,x,y),z,u),U11(U12(tt,x,y),z,u)). [ur(14,a,19,a)]. 0.015/0.015 0.015/0.015 given #51 (F,wt=11): 78 -red(U11(tt,c1,c_N),plus(plus(c_N,s(c2)),0)). [ur(13,b,42,a,c,56,a)]. 0.015/0.015 0.015/0.015 given #52 (F,wt=11): 93 -red(U11(tt,c2,c_N),plus(U11(tt,c1,c_N),0)). [ur(13,b,42,a,c,70,a)]. 0.015/0.015 0.015/0.015 given #53 (F,wt=11): 97 -red(s(plus(c_N,c1)),plus(plus(c_N,s(c2)),0)). [ur(13,b,42,a,c,73,a)]. 0.015/0.015 0.015/0.015 given #54 (F,wt=11): 127 -red(U12(tt,c2,c_N),plus(U11(tt,c1,c_N),0)). [ur(13,b,42,a,c,95,a)]. 0.015/0.015 0.015/0.015 given #55 (T,wt=7): 142 reds(s(s(c1)),s(s(c2))). [ur(13,a,79,a,b,12,a)]. 0.015/0.015 0.015/0.015 given #56 (T,wt=7): 157 reds(U12(tt,0,c1),s(c2)). [ur(13,a,20,a,b,105,a)]. 0.015/0.015 0.015/0.015 given #57 (T,wt=7): 160 reds(U12(tt,0,x),s(x)). [ur(13,a,20,a,b,106,a)]. 0.015/0.015 0.015/0.015 given #58 (T,wt=7): 161 reds(plus(c1,c1),plus(c2,c2)). [ur(13,a,51,a,b,112,a)]. 0.015/0.015 0.015/0.015 given #59 (A,wt=9): 30 reds(U11(tt,x,y),U12(tt,x,y)). [ur(13,a,19,a,b,12,a)]. 0.015/0.015 0.015/0.015 given #60 (F,wt=9): 179 -reds(plus(c_N,s(c2)),U12(tt,c1,c_N)). [resolve(30,a,24,b)]. 0.015/0.015 0.015/0.015 given #61 (F,wt=9): 184 -red(plus(c_N,s(c2)),U12(tt,c1,c_N)). [ur(13,b,12,a,c,179,a)]. 0.015/0.015 0.015/0.015 given #62 (F,wt=9): 185 -reds(U11(tt,c2,c_N),U12(tt,c1,c_N)). [ur(13,a,22,a,c,179,a)]. 0.015/0.015 0.015/0.015 given #63 (F,wt=9): 189 -red(U11(tt,c2,c_N),U12(tt,c1,c_N)). [ur(13,b,12,a,c,185,a)]. 0.015/0.015 0.015/0.015 given #64 (T,wt=7): 175 reds(U11(tt,0,c1),s(c2)). [ur(13,a,19,a,b,157,a)]. 0.015/0.015 0.015/0.015 given #65 (T,wt=7): 177 reds(U11(tt,0,x),s(x)). [ur(13,a,19,a,b,160,a)]. 0.015/0.015 0.015/0.015 given #66 (T,wt=7): 191 reds(plus(c1,s(0)),s(c2)). [ur(13,a,22,a,b,175,a)]. 0.015/0.015 0.015/0.015 given #67 (T,wt=7): 193 reds(plus(x,s(0)),s(x)). [ur(13,a,22,a,b,177,a)]. 0.015/0.015 0.015/0.015 given #68 (A,wt=11): 31 red(s(U12(tt,x,y)),s(s(plus(y,x)))). [ur(18,a,20,a)]. 0.015/0.015 0.015/0.015 given #69 (F,wt=9): 190 -reds(U12(tt,c2,c_N),U12(tt,c1,c_N)). [ur(13,a,19,a,c,185,a)]. 0.015/0.015 0.015/0.015 given #70 (F,wt=9): 207 -red(U12(tt,c2,c_N),U12(tt,c1,c_N)). [ur(13,b,12,a,c,190,a)]. 0.015/0.015 0.015/0.015 given #71 (F,wt=9): 208 -reds(s(plus(c_N,c2)),U12(tt,c1,c_N)). [ur(13,a,20,a,c,190,a)]. 0.015/0.015 0.015/0.015 given #72 (F,wt=9): 212 -red(s(plus(c_N,c2)),U12(tt,c1,c_N)). [ur(13,b,12,a,c,208,a)]. 0.015/0.015 0.015/0.015 given #73 (T,wt=9): 36 reds(U12(tt,x,y),s(plus(y,x))). [ur(13,a,20,a,b,12,a)]. 0.015/0.015 0.015/0.015 given #74 (T,wt=9): 38 red(plus(x,plus(y,0)),plus(x,y)). [ur(17,a,21,a)]. 0.015/0.015 0.015/0.015 given #75 (T,wt=7): 228 reds(plus(c1,plus(0,0)),c2). [ur(13,a,38,a,b,74,a)]. 0.015/0.015 0.015/0.015 given #76 (T,wt=7): 229 reds(plus(x,plus(0,0)),x). [ur(13,a,38,a,b,42,a)]. 0.015/0.015 0.015/0.015 given #77 (A,wt=13): 32 red(plus(x,U12(tt,y,z)),plus(x,s(plus(z,y)))). [ur(17,a,20,a)]. 0.015/0.015 0.015/0.015 given #78 (F,wt=11): 153 -red(s(plus(c_N,c2)),plus(U11(tt,c1,c_N),0)). [ur(13,b,42,a,c,129,a)]. 0.015/0.015 0.015/0.015 given #79 (F,wt=11): 183 -red(plus(c_N,s(c2)),plus(U12(tt,c1,c_N),0)). [ur(13,b,42,a,c,179,a)]. 0.015/0.015 0.015/0.015 given #80 (F,wt=11): 188 -red(U11(tt,c2,c_N),plus(U12(tt,c1,c_N),0)). [ur(13,b,42,a,c,185,a)]. 0.015/0.015 0.015/0.015 given #81 (F,wt=11): 206 -red(U12(tt,c2,c_N),plus(U12(tt,c1,c_N),0)). [ur(13,b,42,a,c,190,a)]. 0.015/0.015 0.015/0.015 given #82 (T,wt=9): 39 red(plus(plus(x,0),y),plus(x,y)). [ur(16,a,21,a)]. 0.015/0.015 0.015/0.015 given #83 (T,wt=9): 48 reds(plus(x,s(y)),U11(tt,y,x)). [ur(13,a,22,a,b,12,a)]. 0.015/0.015 0.015/0.015 given #84 (T,wt=9): 52 red(U12(c1,x,y),U12(c2,x,y)). [ur(15,a,23,a)]. 0.015/0.015 0.015/0.015 given #85 (T,wt=9): 53 red(U11(c1,x,y),U11(c2,x,y)). [ur(14,a,23,a)]. 0.015/0.015 0.015/0.015 given #86 (A,wt=13): 33 red(plus(U12(tt,x,y),z),plus(s(plus(y,x)),z)). [ur(16,a,20,a)]. 0.015/0.015 0.015/0.015 given #87 (F,wt=9): 265 -reds(U11(tt,c1,c_N),U11(tt,c2,c_N)). [resolve(48,a,24,a)]. 0.015/0.015 0.015/0.015 given #88 (F,wt=9): 272 -red(s(plus(c_N,c2)),plus(c_N,s(c1))). [ur(13,b,48,a,c,129,a)]. 0.015/0.015 0.015/0.015 given #89 (F,wt=9): 273 -red(U12(tt,c2,c_N),plus(c_N,s(c1))). [ur(13,b,48,a,c,95,a)]. 0.015/0.015 0.015/0.015 given #90 (F,wt=9): 274 -red(U11(tt,c2,c_N),plus(c_N,s(c1))). [ur(13,b,48,a,c,70,a)]. 0.015/0.015 0.015/0.015 given #91 (T,wt=9): 80 red(plus(x,s(c1)),plus(x,s(c2))). [ur(17,a,49,a)]. 0.015/0.015 0.015/0.015 given #92 (T,wt=9): 81 red(plus(s(c1),x),plus(s(c2),x)). [ur(16,a,49,a)]. 0.015/0.015 0.015/0.015 given #93 (T,wt=9): 100 red(s(s(plus(x,0))),s(s(x))). [ur(18,a,37,a)]. 0.015/0.015 0.015/0.015 given #94 (T,wt=9): 107 red(s(plus(x,c1)),s(plus(x,c2))). [ur(18,a,50,a)]. 0.015/0.015 0.015/0.015 given #95 (A,wt=15): 34 red(U12(U12(tt,x,y),z,u),U12(s(plus(y,x)),z,u)). [ur(15,a,20,a)]. 0.015/0.015 0.015/0.015 given #96 (F,wt=9): 275 -red(plus(c_N,s(c2)),plus(c_N,s(c1))). [ur(13,b,48,a,c,58,a)]. 0.015/0.015 0.015/0.015 given #97 (F,wt=5): 341 -red(s(c2),s(c1)). [resolve(275,a,17,b)]. 0.015/0.015 0.015/0.015 given #98 (F,wt=3): 342 -red(c2,c1). [resolve(341,a,18,b)]. 0.015/0.015 0.015/0.015 given #99 (F,wt=9): 302 -red(U11(tt,c1,c_N),U11(tt,c2,c_N)). [ur(13,b,12,a,c,265,a)]. 0.015/0.015 0.015/0.015 given #100 (T,wt=9): 113 red(s(plus(c1,x)),s(plus(c2,x))). [ur(18,a,51,a)]. 0.015/0.015 0.015/0.015 given #101 (T,wt=9): 130 reds(plus(plus(plus(x,0),0),0),x). [ur(13,a,21,a,b,75,a)]. 0.015/0.015 0.015/0.015 given #102 (T,wt=9): 137 red(s(s(s(c1))),s(s(s(c2)))). [ur(18,a,79,a)]. 0.015/0.015 0.015/0.015 given #103 (T,wt=9): 143 reds(plus(plus(plus(c1,0),0),0),c2). [ur(13,a,21,a,b,85,a)]. 0.015/0.015 0.015/0.015 given #104 (A,wt=15): 35 red(U11(U12(tt,x,y),z,u),U11(s(plus(y,x)),z,u)). [ur(14,a,20,a)]. 0.015/0.015 0.015/0.015 given #105 (F,wt=9): 303 -reds(U12(tt,c1,c_N),U11(tt,c2,c_N)). [ur(13,a,19,a,c,265,a)]. 0.015/0.015 0.015/0.015 given #106 (F,wt=9): 334 -reds(s(plus(c_N,c2)),plus(c_N,s(c2))). [ur(13,a,107,a,c,73,a)]. 0.015/0.015 0.015/0.015 given #107 (F,wt=9): 382 -red(U12(tt,c1,c_N),U11(tt,c2,c_N)). [ur(13,b,12,a,c,303,a)]. 0.015/0.015 0.015/0.015 given #108 (F,wt=9): 383 -reds(s(plus(c_N,c1)),U11(tt,c2,c_N)). [ur(13,a,20,a,c,303,a)]. 0.015/0.015 0.015/0.015 given #109 (T,wt=9): 144 reds(plus(plus(s(c1),0),0),s(c2)). [ur(13,a,21,a,b,99,a)]. 0.015/0.015 0.015/0.015 given #110 (T,wt=9): 155 reds(s(plus(plus(c1,0),0)),s(c2)). [ur(13,a,37,a,b,105,a)]. 0.015/0.015 0.015/0.015 given #111 (T,wt=9): 156 reds(plus(s(plus(c1,0)),0),s(c2)). [ur(13,a,21,a,b,105,a)]. 0.015/0.015 0.015/0.015 given #112 (T,wt=9): 158 reds(s(plus(plus(x,0),0)),s(x)). [ur(13,a,37,a,b,106,a)]. 0.015/0.015 0.015/0.015 given #113 (A,wt=11): 40 red(U12(plus(x,0),y,z),U12(x,y,z)). [ur(15,a,21,a)]. 0.015/0.015 0.015/0.015 given #114 (F,wt=9): 389 -red(s(plus(c_N,c2)),plus(c_N,s(c2))). [ur(13,b,12,a,c,334,a)]. 0.015/0.015 0.015/0.015 given #115 (F,wt=9): 395 -red(s(plus(c_N,c1)),U11(tt,c2,c_N)). [ur(13,b,12,a,c,383,a)]. 0.015/0.015 0.015/0.015 given #116 (F,wt=9): 396 -reds(s(plus(c_N,c2)),U11(tt,c2,c_N)). [ur(13,a,107,a,c,383,a)]. 0.015/0.015 0.015/0.015 given #117 (F,wt=9): 421 -red(s(plus(c_N,c2)),U11(tt,c2,c_N)). [ur(13,b,12,a,c,396,a)]. 0.015/0.015 0.015/0.015 given #118 (T,wt=9): 159 reds(plus(s(plus(x,0)),0),s(x)). [ur(13,a,21,a,b,106,a)]. 0.015/0.015 0.015/0.015 given #119 (T,wt=9): 163 reds(plus(plus(x,c1),0),plus(x,c2)). [ur(13,a,21,a,b,112,a)]. 0.015/0.015 0.015/0.015 given #120 (T,wt=9): 165 reds(plus(plus(c1,x),0),plus(c2,x)). [ur(13,a,21,a,b,118,a)]. 0.015/0.015 0.015/0.015 given #121 (T,wt=9): 172 reds(s(plus(s(c1),0)),s(s(c2))). [ur(13,a,37,a,b,142,a)]. 0.015/0.015 0.015/0.015 given #122 (A,wt=11): 41 red(U11(plus(x,0),y,z),U11(x,y,z)). [ur(14,a,21,a)]. 0.015/0.015 0.015/0.015 given #123 (F,wt=11): 211 -red(s(plus(c_N,c2)),plus(U12(tt,c1,c_N),0)). [ur(13,b,42,a,c,208,a)]. 0.015/0.015 0.015/0.015 given #124 (F,wt=11): 301 -red(U11(tt,c1,c_N),plus(U11(tt,c2,c_N),0)). [ur(13,b,42,a,c,265,a)]. 0.015/0.015 0.015/0.015 given #125 (F,wt=11): 381 -red(U12(tt,c1,c_N),plus(U11(tt,c2,c_N),0)). [ur(13,b,42,a,c,303,a)]. 0.015/0.015 0.015/0.015 given #126 (F,wt=11): 388 -red(s(plus(c_N,c2)),plus(plus(c_N,s(c2)),0)). [ur(13,b,42,a,c,334,a)]. 0.015/0.015 0.015/0.015 given #127 (T,wt=9): 173 reds(plus(s(s(c1)),0),s(s(c2))). [ur(13,a,21,a,b,142,a)]. 0.015/0.015 0.015/0.015 given #128 (T,wt=9): 174 reds(plus(U12(tt,0,c1),0),s(c2)). [ur(13,a,21,a,b,157,a)]. 0.015/0.015 0.015/0.015 given #129 (T,wt=9): 176 reds(plus(U12(tt,0,x),0),s(x)). [ur(13,a,21,a,b,160,a)]. 0.015/0.015 0.015/0.015 given #130 (T,wt=9): 178 reds(plus(plus(c1,c1),0),plus(c2,c2)). [ur(13,a,21,a,b,161,a)]. 0.015/0.015 0.015/0.015 given #131 (A,wt=11): 43 red(s(plus(x,s(y))),s(U11(tt,y,x))). [ur(18,a,22,a)]. 0.015/0.015 0.015/0.015 given #132 (F,wt=11): 394 -red(s(plus(c_N,c1)),plus(U11(tt,c2,c_N),0)). [ur(13,b,42,a,c,383,a)]. 0.015/0.015 0.015/0.015 given #133 (F,wt=11): 420 -red(s(plus(c_N,c2)),plus(U11(tt,c2,c_N),0)). [ur(13,b,42,a,c,396,a)]. 0.015/0.015 0.015/0.015 given #134 (F,wt=12): 65 -red(U11(tt,c1,c_N),x) | -reds(x,plus(c_N,s(c2))). [resolve(56,a,13,c)]. 0.015/0.015 0.015/0.015 given #135 (F,wt=12): 68 -red(plus(c_N,s(c2)),x) | -reds(x,U11(tt,c1,c_N)). [resolve(58,a,13,c)]. 0.015/0.015 0.015/0.015 given #136 (T,wt=9): 180 reds(plus(x,s(y)),U12(tt,y,x)). [ur(13,a,22,a,b,30,a)]. 0.015/0.015 0.015/0.015 given #137 (T,wt=9): 192 reds(plus(U11(tt,0,c1),0),s(c2)). [ur(13,a,21,a,b,175,a)]. 0.015/0.015 0.015/0.015 given #138 (T,wt=9): 194 reds(plus(U11(tt,0,x),0),s(x)). [ur(13,a,21,a,b,177,a)]. 0.015/0.015 0.015/0.015 given #139 (T,wt=9): 195 reds(plus(plus(c1,s(0)),0),s(c2)). [ur(13,a,21,a,b,191,a)]. 0.015/0.015 0.015/0.015 given #140 (A,wt=13): 44 red(plus(x,plus(y,s(z))),plus(x,U11(tt,z,y))). [ur(17,a,22,a)]. 0.015/0.015 0.015/0.015 given #141 (F,wt=9): 459 -reds(U11(tt,c1,c_N),U12(tt,c2,c_N)). [resolve(180,a,24,a)]. 0.015/0.015 0.015/0.015 given #142 (F,wt=9): 487 -red(U11(tt,c1,c_N),U12(tt,c2,c_N)). [ur(13,b,12,a,c,459,a)]. 0.015/0.015 0.015/0.015 given #143 (F,wt=9): 488 -reds(U12(tt,c1,c_N),U12(tt,c2,c_N)). [ur(13,a,19,a,c,459,a)]. 0.015/0.015 0.015/0.015 given #144 (F,wt=9): 494 -red(U12(tt,c1,c_N),U12(tt,c2,c_N)). [ur(13,b,12,a,c,488,a)]. 0.015/0.015 0.015/0.015 given #145 (T,wt=9): 197 reds(plus(plus(x,s(0)),0),s(x)). [ur(13,a,21,a,b,193,a)]. 0.015/0.015 0.015/0.015 given #146 (T,wt=9): 214 reds(U11(tt,x,y),s(plus(y,x))). [ur(13,a,19,a,b,36,a)]. 0.015/0.015 0.015/0.015 given #147 (T,wt=9): 220 reds(plus(x,plus(s(0),0)),s(x)). [ur(13,a,38,a,b,193,a)]. 0.015/0.015 0.015/0.015 given #148 (T,wt=9): 221 reds(plus(c1,plus(s(0),0)),s(c2)). [ur(13,a,38,a,b,191,a)]. 0.015/0.015 0.015/0.015 given #149 (A,wt=13): 45 red(plus(plus(x,s(y)),z),plus(U11(tt,y,x),z)). [ur(16,a,22,a)]. 0.015/0.015 0.015/0.015 given #150 (F,wt=9): 495 -reds(s(plus(c_N,c1)),U12(tt,c2,c_N)). [ur(13,a,20,a,c,488,a)]. 0.015/0.015 0.015/0.015 given #151 (F,wt=9): 498 -reds(plus(c_N,s(c2)),s(plus(c_N,c1))). [resolve(214,a,24,b)]. 0.015/0.015 0.015/0.015 given #152 (F,wt=9): 528 -red(s(plus(c_N,c1)),U12(tt,c2,c_N)). [ur(13,b,12,a,c,495,a)]. 0.015/0.015 0.015/0.015 given #153 (F,wt=9): 529 -reds(s(plus(c_N,c2)),U12(tt,c2,c_N)). [ur(13,a,107,a,c,495,a)]. 0.015/0.015 0.015/0.015 given #154 (T,wt=9): 222 reds(plus(c1,plus(c1,0)),plus(c2,c2)). [ur(13,a,38,a,b,161,a)]. 0.015/0.015 0.015/0.015 given #155 (T,wt=9): 223 reds(plus(c1,plus(x,0)),plus(c2,x)). [ur(13,a,38,a,b,118,a)]. 0.015/0.015 0.015/0.015 given #156 (T,wt=9): 224 reds(plus(x,plus(c1,0)),plus(x,c2)). [ur(13,a,38,a,b,112,a)]. 0.015/0.015 0.015/0.015 given #157 (T,wt=9): 225 reds(plus(s(c1),plus(0,0)),s(c2)). [ur(13,a,38,a,b,99,a)]. 0.015/0.015 0.015/0.015 given #158 (A,wt=15): 46 red(U12(plus(x,s(y)),z,u),U12(U11(tt,y,x),z,u)). [ur(15,a,22,a)]. 0.015/0.015 0.015/0.015 given #159 (F,wt=9): 545 -red(plus(c_N,s(c2)),s(plus(c_N,c1))). [ur(13,b,12,a,c,498,a)]. 0.015/0.015 0.015/0.015 given #160 (F,wt=9): 546 -reds(U11(tt,c2,c_N),s(plus(c_N,c1))). [ur(13,a,22,a,c,498,a)]. 0.015/0.015 0.015/0.015 given #161 (F,wt=9): 552 -red(s(plus(c_N,c2)),U12(tt,c2,c_N)). [ur(13,b,12,a,c,529,a)]. 0.015/0.015 0.015/0.015 given #162 (F,wt=9): 589 -red(U11(tt,c2,c_N),s(plus(c_N,c1))). [ur(13,b,12,a,c,546,a)]. 0.015/0.015 0.015/0.015 given #163 (T,wt=9): 226 reds(plus(plus(c1,0),plus(0,0)),c2). [ur(13,a,38,a,b,85,a)]. 0.015/0.015 0.015/0.015 given #164 (T,wt=9): 227 reds(plus(plus(x,0),plus(0,0)),x). [ur(13,a,38,a,b,75,a)]. 0.015/0.015 0.015/0.015 given #165 (T,wt=9): 230 reds(plus(x,plus(y,0)),plus(x,y)). [ur(13,a,38,a,b,12,a)]. 0.015/0.015 0.015/0.015 given #166 (T,wt=9): 231 reds(plus(c1,plus(plus(0,0),0)),c2). [ur(13,a,38,a,b,228,a)]. 0.015/0.015 0.015/0.015 given #167 (A,wt=15): 47 red(U11(plus(x,s(y)),z,u),U11(U11(tt,y,x),z,u)). [ur(14,a,22,a)]. 0.015/0.015 0.015/0.015 given #168 (F,wt=9): 590 -reds(U12(tt,c2,c_N),s(plus(c_N,c1))). [ur(13,a,19,a,c,546,a)]. 0.015/0.015 0.015/0.015 given #169 (F,wt=9): 652 -red(U12(tt,c2,c_N),s(plus(c_N,c1))). [ur(13,b,12,a,c,590,a)]. 0.015/0.015 0.015/0.015 given #170 (F,wt=9): 653 -reds(s(plus(c_N,c2)),s(plus(c_N,c1))). [ur(13,a,20,a,c,590,a)]. 0.015/0.015 0.015/0.015 given #171 (F,wt=9): 670 -red(s(plus(c_N,c2)),s(plus(c_N,c1))). [ur(13,b,12,a,c,653,a)]. 0.015/0.015 0.015/0.015 given #172 (T,wt=9): 232 reds(plus(plus(c1,plus(0,0)),0),c2). [ur(13,a,21,a,b,228,a)]. 0.015/0.015 0.015/0.015 given #173 (T,wt=9): 233 reds(plus(x,plus(plus(0,0),0)),x). [ur(13,a,38,a,b,229,a)]. 0.015/0.015 0.015/0.015 given #174 (T,wt=9): 235 reds(plus(plus(x,plus(0,0)),0),x). [ur(13,a,21,a,b,229,a)]. 0.015/0.015 0.015/0.015 given #175 (T,wt=9): 259 reds(plus(plus(x,0),s(0)),s(x)). [ur(13,a,39,a,b,193,a)]. 0.015/0.015 0.015/0.015 given #176 (A,wt=15): 55 -reds(U11(tt,c1,c_N),x) | -red(plus(c_N,s(c2)),y) | -reds(y,x). [resolve(24,a,13,c)]. 0.015/0.015 0.015/0.015 given #177 (F,wt=7): 671 -red(plus(c_N,c2),plus(c_N,c1)). [resolve(670,a,18,b)]. 0.015/0.015 0.015/0.015 given #178 (F,wt=9): 799 -reds(U11(tt,c1,c_N),s(plus(c_N,c2))). [ur(55,b,22,a,c,214,a)]. 0.015/0.015 0.015/0.015 given #179 (F,wt=9): 819 -red(U11(tt,c1,c_N),s(plus(c_N,c2))). [ur(13,b,12,a,c,799,a)]. 0.015/0.015 0.015/0.015 given #180 (F,wt=9): 820 -reds(U12(tt,c1,c_N),s(plus(c_N,c2))). [ur(13,a,19,a,c,799,a)]. 0.015/0.015 0.015/0.015 ============================== PROOF ================================= 0.015/0.015 0.015/0.015 % Proof 1 at 0.02 (+ 0.01) seconds. 0.015/0.015 % Length of proof is 25. 0.015/0.015 % Level of proof is 6. 0.015/0.015 % Maximum clause weight is 15.000. 0.015/0.015 % Given clauses 180. 0.015/0.015 0.015/0.015 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 0.015/0.015 5 red(x,y) -> red(plus(z1,x),plus(z1,y)) # label(non_clause). [assumption]. 0.015/0.015 6 red(x,y) -> red(s(x),s(y)) # label(non_clause). [assumption]. 0.015/0.015 7 (all M all N red(U11(tt,M,N),U12(tt,M,N))) # label(non_clause). [assumption]. 0.015/0.015 8 (all M all N red(U12(tt,M,N),s(plus(N,M)))) # label(non_clause). [assumption]. 0.015/0.015 10 (all M all N red(plus(N,s(M)),U11(tt,M,N))) # label(non_clause). [assumption]. 0.015/0.015 11 (all M all y exists z (red(M,y) -> reds(plus(c_N,s(y)),z) & reds(U11(tt,M,c_N),z))) # label(non_clause) # label(goal). [goal]. 0.015/0.015 12 reds(x,x). [assumption]. 0.015/0.015 13 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 0.015/0.015 17 -red(x,y) | red(plus(z,x),plus(z,y)). [clausify(5)]. 0.015/0.015 18 -red(x,y) | red(s(x),s(y)). [clausify(6)]. 0.015/0.015 19 red(U11(tt,x,y),U12(tt,x,y)). [clausify(7)]. 0.015/0.015 20 red(U12(tt,x,y),s(plus(y,x))). [clausify(8)]. 0.015/0.015 22 red(plus(x,s(y)),U11(tt,y,x)). [clausify(10)]. 0.015/0.015 23 red(c1,c2). [deny(11)]. 0.015/0.015 24 -reds(plus(c_N,s(c2)),x) | -reds(U11(tt,c1,c_N),x). [deny(11)]. 0.015/0.015 36 reds(U12(tt,x,y),s(plus(y,x))). [ur(13,a,20,a,b,12,a)]. 0.015/0.015 50 red(plus(x,c1),plus(x,c2)). [ur(17,a,23,a)]. 0.015/0.015 55 -reds(U11(tt,c1,c_N),x) | -red(plus(c_N,s(c2)),y) | -reds(y,x). [resolve(24,a,13,c)]. 0.015/0.015 107 red(s(plus(x,c1)),s(plus(x,c2))). [ur(18,a,50,a)]. 0.015/0.015 214 reds(U11(tt,x,y),s(plus(y,x))). [ur(13,a,19,a,b,36,a)]. 0.015/0.015 333 reds(s(plus(x,c1)),s(plus(x,c2))). [ur(13,a,107,a,b,12,a)]. 0.015/0.015 799 -reds(U11(tt,c1,c_N),s(plus(c_N,c2))). [ur(55,b,22,a,c,214,a)]. 0.015/0.015 820 -reds(U12(tt,c1,c_N),s(plus(c_N,c2))). [ur(13,a,19,a,c,799,a)]. 0.015/0.015 841 $F. [ur(13,a,20,a,c,820,a),unit_del(a,333)]. 0.015/0.015 0.015/0.015 ============================== end of proof ========================== 0.015/0.015 0.015/0.015 ============================== STATISTICS ============================ 0.015/0.015 0.015/0.015 Given=180. Generated=1012. Kept=829. proofs=1. 0.015/0.015 Usable=180. Sos=629. Demods=0. Limbo=20, Disabled=13. Hints=0. 0.015/0.015 Kept_by_rule=0, Deleted_by_rule=0. 0.015/0.015 Forward_subsumed=182. Back_subsumed=0. 0.015/0.015 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 0.015/0.015 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 0.015/0.015 Demod_attempts=0. Demod_rewrites=0. 0.015/0.015 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 0.015/0.015 Nonunit_fsub_feature_tests=530. Nonunit_bsub_feature_tests=693. 0.015/0.015 Megabytes=1.45. 0.015/0.015 User_CPU=0.02, System_CPU=0.01, Wall_clock=0. 0.015/0.015 0.015/0.015 ============================== end of statistics ===================== 0.015/0.015 0.015/0.015 ============================== end of search ========================= 0.015/0.015 0.015/0.015 THEOREM PROVED 0.015/0.015 0.015/0.015 Exiting with 1 proof. 0.015/0.015 0.015/0.015 Process 43168 exit (max_proofs) Tue Nov 16 11:31:22 2021 0.015/0.015 0.015/0.015 0.015/0.015 The problem is joinable. 0.015/0.015 0.015/0.015 Problem 1.1.2: 0.015/0.015 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.015/0.015 Confluence Problem: 0.015/0.015 (VAR vNonEmpty:S M:S N:S) 0.015/0.015 (STRATEGY CONTEXTSENSITIVE 0.015/0.015 (U11 1) 0.015/0.015 (U12 1) 0.015/0.015 (plus 1 2) 0.015/0.015 (0) 0.015/0.015 (fSNonEmpty) 0.015/0.015 (s 1) 0.015/0.015 (tt) 0.015/0.015 ) 0.015/0.015 (RULES 0.015/0.015 U11(tt,M:S,N:S) -> U12(tt,M:S,N:S) 0.015/0.015 U12(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.015/0.015 plus(N:S,0) -> N:S 0.015/0.015 plus(N:S,s(M:S)) -> U11(tt,M:S,N:S) 0.015/0.015 ) 0.015/0.015 Critical Pairs: 0.015/0.015 | N:S \-> y:S => Not trivial, Not overlay, NW0, N2 0.015/0.015 Terminating:"YES" 0.015/0.015 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.015/0.015 0.015/0.015 Huet Brute Force Joinability Processor: 0.015/0.015 That is a LHCP. Trying another procedure. 0.015/0.015 0.015/0.015 Problem 1.1.2: 0.015/0.015 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.015/0.015 Confluence Problem: 0.015/0.015 (VAR vNonEmpty:S M:S N:S) 0.015/0.015 (STRATEGY CONTEXTSENSITIVE 0.015/0.015 (U11 1) 0.015/0.015 (U12 1) 0.015/0.015 (plus 1 2) 0.015/0.015 (0) 0.015/0.015 (fSNonEmpty) 0.015/0.015 (s 1) 0.015/0.015 (tt) 0.015/0.015 ) 0.015/0.015 (RULES 0.015/0.015 U11(tt,M:S,N:S) -> U12(tt,M:S,N:S) 0.015/0.015 U12(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.015/0.015 plus(N:S,0) -> N:S 0.015/0.015 plus(N:S,s(M:S)) -> U11(tt,M:S,N:S) 0.015/0.015 ) 0.015/0.015 Critical Pairs: 0.015/0.015 | N:S \-> y:S => Not trivial, Not overlay, NW0, N2 0.015/0.015 Terminating:"YES" 0.015/0.015 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.015/0.015 0.015/0.015 Prover9 LHCP Convergence Checker Processor: 0.015/0.015 formulas(sos). 0.015/0.015 %Reflexivity 0.015/0.015 reds(x,x). 0.015/0.015 0.015/0.015 %Transitivity 0.015/0.015 (red(x,y) & reds(y,z)) -> reds(x,z). 0.015/0.015 0.015/0.015 %Congruence 0.015/0.015 red(x,y) -> red(U11(x,z2,z3),U11(y,z2,z3)). 0.015/0.015 red(x,y) -> red(U12(x,z2,z3),U12(y,z2,z3)). 0.015/0.015 red(x,y) -> red(plus(x,z2),plus(y,z2)). 0.015/0.015 red(x,y) -> red(plus(z1,x),plus(z1,y)). 0.015/0.015 0.015/0.015 0.015/0.015 red(x,y) -> red(s(x),s(y)). 0.015/0.015 %Replacement 0.015/0.015 all M all N ( red(U11(tt,M,N),U12(tt,M,N)) ). 0.015/0.015 all M all N ( red(U12(tt,M,N),s(plus(N,M))) ). 0.015/0.015 all N ( red(plus(N,0),N) ). 0.015/0.015 all M all N ( red(plus(N,s(M)),U11(tt,M,N)) ). 0.015/0.015 end_of_list. 0.015/0.015 0.015/0.015 formulas(goals). 0.015/0.015 all N all y exists z ( red(N,y) -> (reds(plus(y,s(c_M)),z) & reds(U11(tt,c_M,N),z)) ). 0.015/0.015 end_of_list. 0.015/0.015 0.015/0.015 Proof: 0.015/0.015 ============================== Prover9 =============================== 0.015/0.015 Prover9 (64) version 2009-11A, November 2009. 0.015/0.015 Process 43196 was started by ubuntu on ubuntu, 0.015/0.015 Tue Nov 16 11:31:22 2021 0.015/0.015 The command was "./prover9 -t 30 -f /tmp/prover943130-8.in". 0.015/0.015 ============================== end of head =========================== 0.015/0.015 0.015/0.015 ============================== INPUT ================================= 0.015/0.015 0.015/0.015 % Reading from file /tmp/prover943130-8.in 0.015/0.015 0.015/0.015 0.015/0.015 formulas(sos). 0.015/0.015 reds(x,x). 0.015/0.015 red(x,y) & reds(y,z) -> reds(x,z). 0.015/0.015 red(x,y) -> red(U11(x,z2,z3),U11(y,z2,z3)). 0.015/0.015 red(x,y) -> red(U12(x,z2,z3),U12(y,z2,z3)). 0.015/0.015 red(x,y) -> red(plus(x,z2),plus(y,z2)). 0.015/0.015 red(x,y) -> red(plus(z1,x),plus(z1,y)). 0.015/0.015 red(x,y) -> red(s(x),s(y)). 0.015/0.015 (all M all N red(U11(tt,M,N),U12(tt,M,N))). 0.015/0.015 (all M all N red(U12(tt,M,N),s(plus(N,M)))). 0.015/0.015 (all N red(plus(N,0),N)). 0.015/0.015 (all M all N red(plus(N,s(M)),U11(tt,M,N))). 0.015/0.015 end_of_list. 0.015/0.015 0.015/0.015 formulas(goals). 0.015/0.015 (all N all y exists z (red(N,y) -> reds(plus(y,s(c_M)),z) & reds(U11(tt,c_M,N),z))). 0.015/0.015 end_of_list. 0.015/0.015 assign(max_megs,-1). 0.015/0.015 set(quiet). 0.015/0.015 0.015/0.015 ============================== end of input ========================== 0.015/0.015 0.015/0.015 % From the command line: assign(max_seconds, 30). 0.015/0.015 0.015/0.015 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 0.015/0.015 0.015/0.015 % Formulas that are not ordinary clauses: 0.015/0.015 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 0.015/0.015 2 red(x,y) -> red(U11(x,z2,z3),U11(y,z2,z3)) # label(non_clause). [assumption]. 0.015/0.015 3 red(x,y) -> red(U12(x,z2,z3),U12(y,z2,z3)) # label(non_clause). [assumption]. 0.015/0.015 4 red(x,y) -> red(plus(x,z2),plus(y,z2)) # label(non_clause). [assumption]. 0.015/0.015 5 red(x,y) -> red(plus(z1,x),plus(z1,y)) # label(non_clause). [assumption]. 0.015/0.015 6 red(x,y) -> red(s(x),s(y)) # label(non_clause). [assumption]. 0.015/0.015 7 (all M all N red(U11(tt,M,N),U12(tt,M,N))) # label(non_clause). [assumption]. 0.015/0.015 8 (all M all N red(U12(tt,M,N),s(plus(N,M)))) # label(non_clause). [assumption]. 0.015/0.015 9 (all N red(plus(N,0),N)) # label(non_clause). [assumption]. 0.015/0.015 10 (all M all N red(plus(N,s(M)),U11(tt,M,N))) # label(non_clause). [assumption]. 0.015/0.015 11 (all N all y exists z (red(N,y) -> reds(plus(y,s(c_M)),z) & reds(U11(tt,c_M,N),z))) # label(non_clause) # label(goal). [goal]. 0.015/0.015 0.015/0.015 ============================== end of process non-clausal formulas === 0.015/0.015 0.015/0.015 ============================== PROCESS INITIAL CLAUSES =============== 0.015/0.015 0.015/0.015 % Clauses before input processing: 0.015/0.015 0.015/0.015 formulas(usable). 0.015/0.015 end_of_list. 0.015/0.015 0.015/0.015 formulas(sos). 0.015/0.015 reds(x,x). [assumption]. 0.015/0.015 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 0.015/0.015 -red(x,y) | red(U11(x,z,u),U11(y,z,u)). [clausify(2)]. 0.015/0.015 -red(x,y) | red(U12(x,z,u),U12(y,z,u)). [clausify(3)]. 0.015/0.015 -red(x,y) | red(plus(x,z),plus(y,z)). [clausify(4)]. 0.015/0.015 -red(x,y) | red(plus(z,x),plus(z,y)). [clausify(5)]. 0.015/0.015 -red(x,y) | red(s(x),s(y)). [clausify(6)]. 0.015/0.015 red(U11(tt,x,y),U12(tt,x,y)). [clausify(7)]. 0.015/0.015 red(U12(tt,x,y),s(plus(y,x))). [clausify(8)]. 0.015/0.015 red(plus(x,0),x). [clausify(9)]. 0.015/0.015 red(plus(x,s(y)),U11(tt,y,x)). [clausify(10)]. 0.015/0.015 red(c1,c2). [deny(11)]. 0.015/0.015 -reds(plus(c2,s(c_M)),x) | -reds(U11(tt,c_M,c1),x). [deny(11)]. 0.015/0.015 end_of_list. 0.015/0.015 0.015/0.015 formulas(demodulators). 0.015/0.015 end_of_list. 0.015/0.015 0.015/0.015 ============================== PREDICATE ELIMINATION ================= 0.015/0.015 0.015/0.015 ============================== end predicate elimination ============= 0.015/0.015 0.015/0.015 Auto_denials: (no changes). 0.015/0.015 0.015/0.015 Term ordering decisions: 0.015/0.015 0.015/0.015 kept: 12 reds(x,x). [assumption]. 0.015/0.015 kept: 13 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 0.015/0.015 kept: 14 -red(x,y) | red(U11(x,z,u),U11(y,z,u)). [clausify(2)]. 0.015/0.015 kept: 15 -red(x,y) | red(U12(x,z,u),U12(y,z,u)). [clausify(3)]. 0.015/0.015 kept: 16 -red(x,y) | red(plus(x,z),plus(y,z)). [clausify(4)]. 0.015/0.015 kept: 17 -red(x,y) | red(plus(z,x),plus(z,y)). [clausify(5)]. 0.015/0.015 kept: 18 -red(x,y) | red(s(x),s(y)). [clausify(6)]. 0.015/0.015 kept: 19 red(U11(tt,x,y),U12(tt,x,y)). [clausify(7)]. 0.015/0.015 kept: 20 red(U12(tt,x,y),s(plus(y,x))). [clausify(8)]. 0.015/0.015 kept: 21 red(plus(x,0),x). [clausify(9)]. 0.015/0.015 kept: 22 red(plus(x,s(y)),U11(tt,y,x)). [clausify(10)]. 0.015/0.015 kept: 23 red(c1,c2). [deny(11)]. 0.015/0.015 kept: 24 -reds(plus(c2,s(c_M)),x) | -reds(U11(tt,c_M,c1),x). [deny(11)]. 0.015/0.015 0.015/0.015 ============================== end of process initial clauses ======== 0.015/0.015 0.015/0.015 ============================== CLAUSES FOR SEARCH ==================== 0.015/0.015 0.015/0.015 % Clauses after input processing: 0.015/0.015 0.015/0.015 formulas(usable). 0.015/0.015 end_of_list. 0.015/0.015 0.015/0.015 formulas(sos). 0.015/0.015 12 reds(x,x). [assumption]. 0.015/0.015 13 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 0.015/0.015 14 -red(x,y) | red(U11(x,z,u),U11(y,z,u)). [clausify(2)]. 0.015/0.015 15 -red(x,y) | red(U12(x,z,u),U12(y,z,u)). [clausify(3)]. 0.015/0.015 16 -red(x,y) | red(plus(x,z),plus(y,z)). [clausify(4)]. 0.015/0.015 17 -red(x,y) | red(plus(z,x),plus(z,y)). [clausify(5)]. 0.015/0.015 18 -red(x,y) | red(s(x),s(y)). [clausify(6)]. 0.015/0.015 19 red(U11(tt,x,y),U12(tt,x,y)). [clausify(7)]. 0.015/0.015 20 red(U12(tt,x,y),s(plus(y,x))). [clausify(8)]. 0.015/0.015 21 red(plus(x,0),x). [clausify(9)]. 0.015/0.015 22 red(plus(x,s(y)),U11(tt,y,x)). [clausify(10)]. 0.015/0.015 23 red(c1,c2). [deny(11)]. 0.015/0.015 24 -reds(plus(c2,s(c_M)),x) | -reds(U11(tt,c_M,c1),x). [deny(11)]. 0.015/0.015 end_of_list. 0.015/0.015 0.015/0.015 formulas(demodulators). 0.015/0.015 end_of_list. 0.015/0.015 0.015/0.015 ============================== end of clauses for search ============= 0.015/0.015 0.015/0.015 ============================== SEARCH ================================ 0.015/0.015 0.015/0.015 % Starting search at 0.00 seconds. 0.015/0.015 0.015/0.015 given #1 (I,wt=3): 12 reds(x,x). [assumption]. 0.015/0.015 0.015/0.015 given #2 (I,wt=9): 13 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 0.015/0.015 0.015/0.015 given #3 (I,wt=12): 14 -red(x,y) | red(U11(x,z,u),U11(y,z,u)). [clausify(2)]. 0.015/0.015 0.015/0.015 given #4 (I,wt=12): 15 -red(x,y) | red(U12(x,z,u),U12(y,z,u)). [clausify(3)]. 0.015/0.015 0.015/0.015 given #5 (I,wt=10): 16 -red(x,y) | red(plus(x,z),plus(y,z)). [clausify(4)]. 0.015/0.015 0.015/0.015 given #6 (I,wt=10): 17 -red(x,y) | red(plus(z,x),plus(z,y)). [clausify(5)]. 0.015/0.015 0.015/0.015 given #7 (I,wt=8): 18 -red(x,y) | red(s(x),s(y)). [clausify(6)]. 0.015/0.015 0.015/0.015 given #8 (I,wt=9): 19 red(U11(tt,x,y),U12(tt,x,y)). [clausify(7)]. 0.015/0.015 0.015/0.015 given #9 (I,wt=9): 20 red(U12(tt,x,y),s(plus(y,x))). [clausify(8)]. 0.015/0.015 0.015/0.015 given #10 (I,wt=5): 21 red(plus(x,0),x). [clausify(9)]. 0.015/0.015 0.015/0.015 given #11 (I,wt=9): 22 red(plus(x,s(y)),U11(tt,y,x)). [clausify(10)]. 0.015/0.015 0.015/0.015 given #12 (I,wt=3): 23 red(c1,c2). [deny(11)]. 0.015/0.015 0.015/0.015 given #13 (I,wt=12): 24 -reds(plus(c2,s(c_M)),x) | -reds(U11(tt,c_M,c1),x). [deny(11)]. 0.015/0.015 0.015/0.015 given #14 (A,wt=11): 25 red(s(U11(tt,x,y)),s(U12(tt,x,y))). [ur(18,a,19,a)]. 0.015/0.015 0.015/0.015 given #15 (F,wt=9): 56 -reds(U11(tt,c_M,c1),plus(c2,s(c_M))). [resolve(24,a,12,a)]. 0.015/0.015 0.015/0.015 given #16 (F,wt=9): 58 -reds(plus(c2,s(c_M)),U11(tt,c_M,c1)). [resolve(24,b,12,a)]. 0.015/0.015 0.015/0.015 given #17 (F,wt=9): 66 -red(U11(tt,c_M,c1),plus(c2,s(c_M))). [ur(13,b,12,a,c,56,a)]. 0.015/0.015 0.015/0.015 given #18 (F,wt=9): 67 -reds(U12(tt,c_M,c1),plus(c2,s(c_M))). [ur(13,a,19,a,c,56,a)]. 0.015/0.015 0.015/0.015 given #19 (T,wt=3): 54 reds(c1,c2). [ur(13,a,23,a,b,12,a)]. 0.015/0.015 0.015/0.015 given #20 (T,wt=5): 42 reds(plus(x,0),x). [ur(13,a,21,a,b,12,a)]. 0.015/0.015 0.015/0.015 given #21 (T,wt=5): 49 red(s(c1),s(c2)). [ur(18,a,23,a)]. 0.015/0.015 0.015/0.015 given #22 (T,wt=5): 74 reds(plus(c1,0),c2). [ur(13,a,21,a,b,54,a)]. 0.015/0.015 0.015/0.015 given #23 (A,wt=13): 26 red(plus(x,U11(tt,y,z)),plus(x,U12(tt,y,z))). [ur(17,a,19,a)]. 0.015/0.015 0.015/0.015 given #24 (F,wt=9): 69 -red(plus(c2,s(c_M)),U11(tt,c_M,c1)). [ur(13,b,12,a,c,58,a)]. 0.015/0.015 0.015/0.015 given #25 (F,wt=9): 70 -reds(U11(tt,c_M,c2),U11(tt,c_M,c1)). [ur(13,a,22,a,c,58,a)]. 0.015/0.015 0.015/0.015 given #26 (F,wt=9): 72 -red(U12(tt,c_M,c1),plus(c2,s(c_M))). [ur(13,b,12,a,c,67,a)]. 0.015/0.015 0.015/0.015 given #27 (F,wt=9): 73 -reds(s(plus(c1,c_M)),plus(c2,s(c_M))). [ur(13,a,20,a,c,67,a)]. 0.015/0.015 0.015/0.015 given #28 (T,wt=5): 84 reds(s(c1),s(c2)). [ur(13,a,49,a,b,12,a)]. 0.015/0.015 0.015/0.015 given #29 (T,wt=7): 37 red(s(plus(x,0)),s(x)). [ur(18,a,21,a)]. 0.015/0.015 0.015/0.015 given #30 (T,wt=7): 50 red(plus(x,c1),plus(x,c2)). [ur(17,a,23,a)]. 0.015/0.015 0.015/0.015 given #31 (T,wt=7): 51 red(plus(c1,x),plus(c2,x)). [ur(16,a,23,a)]. 0.015/0.015 0.015/0.015 given #32 (A,wt=13): 27 red(plus(U11(tt,x,y),z),plus(U12(tt,x,y),z)). [ur(16,a,19,a)]. 0.015/0.015 0.015/0.015 given #33 (F,wt=9): 94 -red(U11(tt,c_M,c2),U11(tt,c_M,c1)). [ur(13,b,12,a,c,70,a)]. 0.015/0.015 0.015/0.015 given #34 (F,wt=9): 95 -reds(U12(tt,c_M,c2),U11(tt,c_M,c1)). [ur(13,a,19,a,c,70,a)]. 0.015/0.015 0.015/0.015 given #35 (F,wt=9): 98 -red(s(plus(c1,c_M)),plus(c2,s(c_M))). [ur(13,b,12,a,c,73,a)]. 0.015/0.015 0.015/0.015 given #36 (F,wt=9): 128 -red(U12(tt,c_M,c2),U11(tt,c_M,c1)). [ur(13,b,12,a,c,95,a)]. 0.015/0.015 0.015/0.015 given #37 (T,wt=7): 75 reds(plus(plus(x,0),0),x). [ur(13,a,21,a,b,42,a)]. 0.015/0.015 0.015/0.015 given #38 (T,wt=7): 79 red(s(s(c1)),s(s(c2))). [ur(18,a,49,a)]. 0.015/0.015 0.015/0.015 given #39 (T,wt=7): 85 reds(plus(plus(c1,0),0),c2). [ur(13,a,21,a,b,74,a)]. 0.015/0.015 0.015/0.015 given #40 (T,wt=7): 99 reds(plus(s(c1),0),s(c2)). [ur(13,a,21,a,b,84,a)]. 0.015/0.015 0.015/0.015 given #41 (A,wt=15): 28 red(U12(U11(tt,x,y),z,u),U12(U12(tt,x,y),z,u)). [ur(15,a,19,a)]. 0.015/0.015 0.015/0.015 given #42 (F,wt=9): 129 -reds(s(plus(c2,c_M)),U11(tt,c_M,c1)). [ur(13,a,20,a,c,95,a)]. 0.015/0.015 0.015/0.015 given #43 (F,wt=9): 154 -red(s(plus(c2,c_M)),U11(tt,c_M,c1)). [ur(13,b,12,a,c,129,a)]. 0.015/0.015 0.015/0.015 given #44 (F,wt=11): 76 -red(U12(tt,c_M,c1),plus(plus(c2,s(c_M)),0)). [ur(13,b,42,a,c,67,a)]. 0.015/0.015 0.015/0.015 given #45 (F,wt=11): 77 -red(plus(c2,s(c_M)),plus(U11(tt,c_M,c1),0)). [ur(13,b,42,a,c,58,a)]. 0.015/0.015 0.015/0.015 given #46 (T,wt=7): 105 reds(s(plus(c1,0)),s(c2)). [ur(13,a,37,a,b,84,a)]. 0.015/0.015 0.015/0.015 given #47 (T,wt=7): 106 reds(s(plus(x,0)),s(x)). [ur(13,a,37,a,b,12,a)]. 0.015/0.015 0.015/0.015 given #48 (T,wt=7): 112 reds(plus(x,c1),plus(x,c2)). [ur(13,a,50,a,b,12,a)]. 0.015/0.015 0.015/0.015 given #49 (T,wt=7): 118 reds(plus(c1,x),plus(c2,x)). [ur(13,a,51,a,b,12,a)]. 0.015/0.015 0.015/0.015 given #50 (A,wt=15): 29 red(U11(U11(tt,x,y),z,u),U11(U12(tt,x,y),z,u)). [ur(14,a,19,a)]. 0.015/0.015 0.015/0.015 given #51 (F,wt=9): 166 -red(s(plus(c1,c_M)),plus(c1,s(c_M))). [ur(13,b,118,a,c,73,a)]. 0.015/0.015 0.015/0.015 given #52 (F,wt=9): 167 -red(U12(tt,c_M,c1),plus(c1,s(c_M))). [ur(13,b,118,a,c,67,a)]. 0.015/0.015 0.015/0.015 given #53 (F,wt=9): 168 -red(U11(tt,c_M,c1),plus(c1,s(c_M))). [ur(13,b,118,a,c,56,a)]. 0.015/0.015 0.015/0.015 given #54 (F,wt=11): 78 -red(U11(tt,c_M,c1),plus(plus(c2,s(c_M)),0)). [ur(13,b,42,a,c,56,a)]. 0.015/0.015 0.015/0.015 given #55 (T,wt=7): 142 reds(s(s(c1)),s(s(c2))). [ur(13,a,79,a,b,12,a)]. 0.015/0.015 0.015/0.015 given #56 (T,wt=7): 157 reds(U12(tt,0,c1),s(c2)). [ur(13,a,20,a,b,105,a)]. 0.015/0.015 0.015/0.015 given #57 (T,wt=7): 160 reds(U12(tt,0,x),s(x)). [ur(13,a,20,a,b,106,a)]. 0.015/0.015 0.015/0.015 given #58 (T,wt=7): 161 reds(plus(c1,c1),plus(c2,c2)). [ur(13,a,51,a,b,112,a)]. 0.015/0.015 0.015/0.015 given #59 (A,wt=9): 30 reds(U11(tt,x,y),U12(tt,x,y)). [ur(13,a,19,a,b,12,a)]. 0.015/0.015 0.015/0.015 given #60 (F,wt=9): 182 -reds(plus(c2,s(c_M)),U12(tt,c_M,c1)). [resolve(30,a,24,b)]. 0.015/0.015 0.015/0.015 given #61 (F,wt=9): 187 -red(plus(c2,s(c_M)),U12(tt,c_M,c1)). [ur(13,b,12,a,c,182,a)]. 0.015/0.015 0.015/0.015 given #62 (F,wt=9): 188 -reds(U11(tt,c_M,c2),U12(tt,c_M,c1)). [ur(13,a,22,a,c,182,a)]. 0.015/0.015 0.015/0.015 given #63 (F,wt=9): 192 -red(U11(tt,c_M,c2),U12(tt,c_M,c1)). [ur(13,b,12,a,c,188,a)]. 0.015/0.015 0.015/0.015 given #64 (T,wt=7): 178 reds(U11(tt,0,c1),s(c2)). [ur(13,a,19,a,b,157,a)]. 0.015/0.015 0.015/0.015 given #65 (T,wt=7): 180 reds(U11(tt,0,x),s(x)). [ur(13,a,19,a,b,160,a)]. 0.015/0.015 0.015/0.015 given #66 (T,wt=7): 194 reds(plus(c1,s(0)),s(c2)). [ur(13,a,22,a,b,178,a)]. 0.015/0.015 0.015/0.015 given #67 (T,wt=7): 196 reds(plus(x,s(0)),s(x)). [ur(13,a,22,a,b,180,a)]. 0.015/0.015 0.015/0.015 given #68 (A,wt=11): 31 red(s(U12(tt,x,y)),s(s(plus(y,x)))). [ur(18,a,20,a)]. 0.015/0.015 0.015/0.015 given #69 (F,wt=9): 193 -reds(U12(tt,c_M,c2),U12(tt,c_M,c1)). [ur(13,a,19,a,c,188,a)]. 0.015/0.015 0.015/0.015 given #70 (F,wt=9): 210 -red(U12(tt,c_M,c2),U12(tt,c_M,c1)). [ur(13,b,12,a,c,193,a)]. 0.015/0.015 0.015/0.015 given #71 (F,wt=9): 211 -reds(s(plus(c2,c_M)),U12(tt,c_M,c1)). [ur(13,a,20,a,c,193,a)]. 0.015/0.015 0.015/0.015 given #72 (F,wt=9): 215 -red(s(plus(c2,c_M)),U12(tt,c_M,c1)). [ur(13,b,12,a,c,211,a)]. 0.015/0.015 0.015/0.015 given #73 (T,wt=9): 36 reds(U12(tt,x,y),s(plus(y,x))). [ur(13,a,20,a,b,12,a)]. 0.015/0.015 0.015/0.015 given #74 (T,wt=9): 38 red(plus(x,plus(y,0)),plus(x,y)). [ur(17,a,21,a)]. 0.015/0.015 0.015/0.015 given #75 (T,wt=7): 231 reds(plus(c1,plus(0,0)),c2). [ur(13,a,38,a,b,74,a)]. 0.015/0.015 0.015/0.015 given #76 (T,wt=7): 232 reds(plus(x,plus(0,0)),x). [ur(13,a,38,a,b,42,a)]. 0.015/0.015 0.015/0.015 given #77 (A,wt=13): 32 red(plus(x,U12(tt,y,z)),plus(x,s(plus(z,y)))). [ur(17,a,20,a)]. 0.015/0.015 0.015/0.015 given #78 (F,wt=11): 93 -red(U11(tt,c_M,c2),plus(U11(tt,c_M,c1),0)). [ur(13,b,42,a,c,70,a)]. 0.015/0.015 0.015/0.015 given #79 (F,wt=11): 97 -red(s(plus(c1,c_M)),plus(plus(c2,s(c_M)),0)). [ur(13,b,42,a,c,73,a)]. 0.015/0.015 0.015/0.015 given #80 (F,wt=11): 127 -red(U12(tt,c_M,c2),plus(U11(tt,c_M,c1),0)). [ur(13,b,42,a,c,95,a)]. 0.015/0.015 0.015/0.015 given #81 (F,wt=11): 153 -red(s(plus(c2,c_M)),plus(U11(tt,c_M,c1),0)). [ur(13,b,42,a,c,129,a)]. 0.015/0.015 0.015/0.015 given #82 (T,wt=9): 39 red(plus(plus(x,0),y),plus(x,y)). [ur(16,a,21,a)]. 0.015/0.015 0.015/0.015 given #83 (T,wt=9): 48 reds(plus(x,s(y)),U11(tt,y,x)). [ur(13,a,22,a,b,12,a)]. 0.015/0.015 0.015/0.015 given #84 (T,wt=9): 52 red(U12(c1,x,y),U12(c2,x,y)). [ur(15,a,23,a)]. 0.015/0.015 0.015/0.015 given #85 (T,wt=9): 53 red(U11(c1,x,y),U11(c2,x,y)). [ur(14,a,23,a)]. 0.015/0.015 0.015/0.015 given #86 (A,wt=13): 33 red(plus(U12(tt,x,y),z),plus(s(plus(y,x)),z)). [ur(16,a,20,a)]. 0.015/0.015 0.015/0.015 given #87 (F,wt=9): 268 -reds(U11(tt,c_M,c1),U11(tt,c_M,c2)). [resolve(48,a,24,a)]. 0.015/0.015 0.015/0.015 given #88 (F,wt=9): 275 -red(s(plus(c2,c_M)),plus(c1,s(c_M))). [ur(13,b,48,a,c,129,a)]. 0.015/0.015 0.015/0.015 given #89 (F,wt=9): 276 -red(U12(tt,c_M,c2),plus(c1,s(c_M))). [ur(13,b,48,a,c,95,a)]. 0.015/0.015 0.015/0.015 given #90 (F,wt=9): 277 -red(U11(tt,c_M,c2),plus(c1,s(c_M))). [ur(13,b,48,a,c,70,a)]. 0.015/0.015 0.015/0.015 given #91 (T,wt=9): 80 red(plus(x,s(c1)),plus(x,s(c2))). [ur(17,a,49,a)]. 0.015/0.015 0.015/0.015 given #92 (T,wt=9): 81 red(plus(s(c1),x),plus(s(c2),x)). [ur(16,a,49,a)]. 0.015/0.015 0.015/0.015 given #93 (T,wt=9): 100 red(s(s(plus(x,0))),s(s(x))). [ur(18,a,37,a)]. 0.015/0.015 0.015/0.015 given #94 (T,wt=9): 107 red(s(plus(x,c1)),s(plus(x,c2))). [ur(18,a,50,a)]. 0.015/0.015 0.015/0.015 given #95 (A,wt=15): 34 red(U12(U12(tt,x,y),z,u),U12(s(plus(y,x)),z,u)). [ur(15,a,20,a)]. 0.015/0.015 0.015/0.015 given #96 (F,wt=9): 278 -red(plus(c2,s(c_M)),plus(c1,s(c_M))). [ur(13,b,48,a,c,58,a)]. 0.015/0.015 0.015/0.015 given #97 (F,wt=3): 343 -red(c2,c1). [resolve(278,a,16,b)]. 0.015/0.015 0.015/0.015 given #98 (F,wt=9): 305 -red(U11(tt,c_M,c1),U11(tt,c_M,c2)). [ur(13,b,12,a,c,268,a)]. 0.015/0.015 0.015/0.015 given #99 (F,wt=9): 306 -reds(U12(tt,c_M,c1),U11(tt,c_M,c2)). [ur(13,a,19,a,c,268,a)]. 0.015/0.015 0.015/0.015 given #100 (T,wt=9): 113 red(s(plus(c1,x)),s(plus(c2,x))). [ur(18,a,51,a)]. 0.015/0.015 0.015/0.015 given #101 (T,wt=9): 130 reds(plus(plus(plus(x,0),0),0),x). [ur(13,a,21,a,b,75,a)]. 0.015/0.015 0.015/0.015 given #102 (T,wt=9): 137 red(s(s(s(c1))),s(s(s(c2)))). [ur(18,a,79,a)]. 0.015/0.015 0.015/0.015 given #103 (T,wt=9): 143 reds(plus(plus(plus(c1,0),0),0),c2). [ur(13,a,21,a,b,85,a)]. 0.015/0.015 0.015/0.015 given #104 (A,wt=15): 35 red(U11(U12(tt,x,y),z,u),U11(s(plus(y,x)),z,u)). [ur(14,a,20,a)]. 0.015/0.015 0.015/0.015 given #105 (F,wt=9): 348 -red(U12(tt,c_M,c1),U11(tt,c_M,c2)). [ur(13,b,12,a,c,306,a)]. 0.015/0.015 0.015/0.015 given #106 (F,wt=9): 349 -reds(s(plus(c1,c_M)),U11(tt,c_M,c2)). [ur(13,a,20,a,c,306,a)]. 0.015/0.015 0.015/0.015 given #107 (F,wt=9): 356 -reds(s(plus(c2,c_M)),plus(c2,s(c_M))). [ur(13,a,113,a,c,73,a)]. 0.015/0.015 0.015/0.015 given #108 (F,wt=9): 391 -red(s(plus(c1,c_M)),U11(tt,c_M,c2)). [ur(13,b,12,a,c,349,a)]. 0.015/0.015 0.015/0.015 given #109 (T,wt=9): 144 reds(plus(plus(s(c1),0),0),s(c2)). [ur(13,a,21,a,b,99,a)]. 0.015/0.015 0.015/0.015 given #110 (T,wt=9): 155 reds(s(plus(plus(c1,0),0)),s(c2)). [ur(13,a,37,a,b,105,a)]. 0.015/0.015 0.015/0.015 given #111 (T,wt=9): 156 reds(plus(s(plus(c1,0)),0),s(c2)). [ur(13,a,21,a,b,105,a)]. 0.015/0.015 0.015/0.015 given #112 (T,wt=9): 158 reds(s(plus(plus(x,0),0)),s(x)). [ur(13,a,37,a,b,106,a)]. 0.015/0.015 0.015/0.015 given #113 (A,wt=11): 40 red(U12(plus(x,0),y,z),U12(x,y,z)). [ur(15,a,21,a)]. 0.015/0.015 0.015/0.015 given #114 (F,wt=9): 392 -reds(s(plus(c2,c_M)),U11(tt,c_M,c2)). [ur(13,a,113,a,c,349,a)]. 0.015/0.015 0.015/0.015 given #115 (F,wt=9): 398 -red(s(plus(c2,c_M)),plus(c2,s(c_M))). [ur(13,b,12,a,c,356,a)]. 0.015/0.015 0.015/0.015 given #116 (F,wt=9): 423 -red(s(plus(c2,c_M)),U11(tt,c_M,c2)). [ur(13,b,12,a,c,392,a)]. 0.015/0.015 0.015/0.015 given #117 (F,wt=11): 186 -red(plus(c2,s(c_M)),plus(U12(tt,c_M,c1),0)). [ur(13,b,42,a,c,182,a)]. 0.015/0.015 0.015/0.015 given #118 (T,wt=9): 159 reds(plus(s(plus(x,0)),0),s(x)). [ur(13,a,21,a,b,106,a)]. 0.015/0.015 0.015/0.015 given #119 (T,wt=9): 163 reds(plus(plus(x,c1),0),plus(x,c2)). [ur(13,a,21,a,b,112,a)]. 0.015/0.015 0.015/0.015 given #120 (T,wt=9): 165 reds(plus(plus(c1,x),0),plus(c2,x)). [ur(13,a,21,a,b,118,a)]. 0.015/0.015 0.015/0.015 given #121 (T,wt=9): 175 reds(s(plus(s(c1),0)),s(s(c2))). [ur(13,a,37,a,b,142,a)]. 0.015/0.015 0.015/0.015 given #122 (A,wt=11): 41 red(U11(plus(x,0),y,z),U11(x,y,z)). [ur(14,a,21,a)]. 0.015/0.015 0.015/0.015 given #123 (F,wt=11): 191 -red(U11(tt,c_M,c2),plus(U12(tt,c_M,c1),0)). [ur(13,b,42,a,c,188,a)]. 0.015/0.015 0.015/0.015 given #124 (F,wt=11): 209 -red(U12(tt,c_M,c2),plus(U12(tt,c_M,c1),0)). [ur(13,b,42,a,c,193,a)]. 0.015/0.015 0.015/0.015 given #125 (F,wt=11): 214 -red(s(plus(c2,c_M)),plus(U12(tt,c_M,c1),0)). [ur(13,b,42,a,c,211,a)]. 0.015/0.015 0.015/0.015 given #126 (F,wt=11): 304 -red(U11(tt,c_M,c1),plus(U11(tt,c_M,c2),0)). [ur(13,b,42,a,c,268,a)]. 0.015/0.015 0.015/0.015 given #127 (T,wt=9): 176 reds(plus(s(s(c1)),0),s(s(c2))). [ur(13,a,21,a,b,142,a)]. 0.015/0.015 0.015/0.015 given #128 (T,wt=9): 177 reds(plus(U12(tt,0,c1),0),s(c2)). [ur(13,a,21,a,b,157,a)]. 0.015/0.015 0.015/0.015 given #129 (T,wt=9): 179 reds(plus(U12(tt,0,x),0),s(x)). [ur(13,a,21,a,b,160,a)]. 0.015/0.015 0.015/0.015 given #130 (T,wt=9): 181 reds(plus(plus(c1,c1),0),plus(c2,c2)). [ur(13,a,21,a,b,161,a)]. 0.015/0.015 0.015/0.015 given #131 (A,wt=11): 43 red(s(plus(x,s(y))),s(U11(tt,y,x))). [ur(18,a,22,a)]. 0.015/0.015 0.015/0.015 given #132 (F,wt=11): 347 -red(U12(tt,c_M,c1),plus(U11(tt,c_M,c2),0)). [ur(13,b,42,a,c,306,a)]. 0.015/0.015 0.015/0.015 given #133 (F,wt=11): 390 -red(s(plus(c1,c_M)),plus(U11(tt,c_M,c2),0)). [ur(13,b,42,a,c,349,a)]. 0.015/0.015 0.015/0.015 given #134 (F,wt=11): 397 -red(s(plus(c2,c_M)),plus(plus(c2,s(c_M)),0)). [ur(13,b,42,a,c,356,a)]. 0.015/0.015 0.015/0.015 given #135 (F,wt=11): 422 -red(s(plus(c2,c_M)),plus(U11(tt,c_M,c2),0)). [ur(13,b,42,a,c,392,a)]. 0.015/0.015 0.015/0.015 given #136 (T,wt=9): 183 reds(plus(x,s(y)),U12(tt,y,x)). [ur(13,a,22,a,b,30,a)]. 0.015/0.015 0.015/0.015 given #137 (T,wt=9): 195 reds(plus(U11(tt,0,c1),0),s(c2)). [ur(13,a,21,a,b,178,a)]. 0.015/0.015 0.015/0.015 given #138 (T,wt=9): 197 reds(plus(U11(tt,0,x),0),s(x)). [ur(13,a,21,a,b,180,a)]. 0.015/0.015 0.015/0.015 given #139 (T,wt=9): 198 reds(plus(plus(c1,s(0)),0),s(c2)). [ur(13,a,21,a,b,194,a)]. 0.015/0.015 0.015/0.015 given #140 (A,wt=13): 44 red(plus(x,plus(y,s(z))),plus(x,U11(tt,z,y))). [ur(17,a,22,a)]. 0.015/0.015 0.015/0.015 given #141 (F,wt=9): 460 -reds(U11(tt,c_M,c1),U12(tt,c_M,c2)). [resolve(183,a,24,a)]. 0.015/0.015 0.015/0.015 given #142 (F,wt=9): 488 -red(U11(tt,c_M,c1),U12(tt,c_M,c2)). [ur(13,b,12,a,c,460,a)]. 0.015/0.015 0.015/0.015 given #143 (F,wt=9): 489 -reds(U12(tt,c_M,c1),U12(tt,c_M,c2)). [ur(13,a,19,a,c,460,a)]. 0.015/0.015 0.015/0.015 given #144 (F,wt=9): 495 -red(U12(tt,c_M,c1),U12(tt,c_M,c2)). [ur(13,b,12,a,c,489,a)]. 0.015/0.015 0.015/0.015 given #145 (T,wt=9): 200 reds(plus(plus(x,s(0)),0),s(x)). [ur(13,a,21,a,b,196,a)]. 0.015/0.015 0.015/0.015 given #146 (T,wt=9): 217 reds(U11(tt,x,y),s(plus(y,x))). [ur(13,a,19,a,b,36,a)]. 0.015/0.015 0.015/0.015 given #147 (T,wt=9): 223 reds(plus(x,plus(s(0),0)),s(x)). [ur(13,a,38,a,b,196,a)]. 0.015/0.015 0.015/0.015 given #148 (T,wt=9): 224 reds(plus(c1,plus(s(0),0)),s(c2)). [ur(13,a,38,a,b,194,a)]. 0.015/0.015 0.015/0.015 given #149 (A,wt=13): 45 red(plus(plus(x,s(y)),z),plus(U11(tt,y,x),z)). [ur(16,a,22,a)]. 0.015/0.015 0.015/0.015 given #150 (F,wt=9): 496 -reds(s(plus(c1,c_M)),U12(tt,c_M,c2)). [ur(13,a,20,a,c,489,a)]. 0.015/0.015 0.015/0.015 given #151 (F,wt=9): 499 -reds(plus(c2,s(c_M)),s(plus(c1,c_M))). [resolve(217,a,24,b)]. 0.015/0.015 0.015/0.015 given #152 (F,wt=9): 529 -red(s(plus(c1,c_M)),U12(tt,c_M,c2)). [ur(13,b,12,a,c,496,a)]. 0.015/0.015 0.015/0.015 given #153 (F,wt=9): 530 -reds(s(plus(c2,c_M)),U12(tt,c_M,c2)). [ur(13,a,113,a,c,496,a)]. 0.015/0.015 0.015/0.015 given #154 (T,wt=9): 225 reds(plus(c1,plus(c1,0)),plus(c2,c2)). [ur(13,a,38,a,b,161,a)]. 0.015/0.015 0.015/0.015 given #155 (T,wt=9): 226 reds(plus(c1,plus(x,0)),plus(c2,x)). [ur(13,a,38,a,b,118,a)]. 0.015/0.015 0.015/0.015 given #156 (T,wt=9): 227 reds(plus(x,plus(c1,0)),plus(x,c2)). [ur(13,a,38,a,b,112,a)]. 0.015/0.015 0.015/0.015 given #157 (T,wt=9): 228 reds(plus(s(c1),plus(0,0)),s(c2)). [ur(13,a,38,a,b,99,a)]. 0.015/0.015 0.015/0.015 given #158 (A,wt=15): 46 red(U12(plus(x,s(y)),z,u),U12(U11(tt,y,x),z,u)). [ur(15,a,22,a)]. 0.015/0.015 0.015/0.015 given #159 (F,wt=9): 546 -red(plus(c2,s(c_M)),s(plus(c1,c_M))). [ur(13,b,12,a,c,499,a)]. 0.015/0.015 0.015/0.015 given #160 (F,wt=9): 547 -reds(U11(tt,c_M,c2),s(plus(c1,c_M))). [ur(13,a,22,a,c,499,a)]. 0.015/0.015 0.015/0.015 given #161 (F,wt=9): 553 -red(s(plus(c2,c_M)),U12(tt,c_M,c2)). [ur(13,b,12,a,c,530,a)]. 0.015/0.015 0.015/0.015 given #162 (F,wt=9): 594 -red(U11(tt,c_M,c2),s(plus(c1,c_M))). [ur(13,b,12,a,c,547,a)]. 0.015/0.015 0.015/0.015 given #163 (T,wt=9): 229 reds(plus(plus(c1,0),plus(0,0)),c2). [ur(13,a,38,a,b,85,a)]. 0.015/0.015 0.015/0.015 given #164 (T,wt=9): 230 reds(plus(plus(x,0),plus(0,0)),x). [ur(13,a,38,a,b,75,a)]. 0.015/0.015 0.015/0.015 given #165 (T,wt=9): 233 reds(plus(x,plus(y,0)),plus(x,y)). [ur(13,a,38,a,b,12,a)]. 0.015/0.015 0.015/0.015 given #166 (T,wt=9): 234 reds(plus(c1,plus(plus(0,0),0)),c2). [ur(13,a,38,a,b,231,a)]. 0.015/0.015 0.015/0.015 given #167 (A,wt=15): 47 red(U11(plus(x,s(y)),z,u),U11(U11(tt,y,x),z,u)). [ur(14,a,22,a)]. 0.015/0.015 0.015/0.015 given #168 (F,wt=9): 595 -reds(U12(tt,c_M,c2),s(plus(c1,c_M))). [ur(13,a,19,a,c,547,a)]. 0.015/0.015 0.015/0.015 given #169 (F,wt=9): 657 -red(U12(tt,c_M,c2),s(plus(c1,c_M))). [ur(13,b,12,a,c,595,a)]. 0.015/0.015 0.015/0.015 given #170 (F,wt=9): 658 -reds(s(plus(c2,c_M)),s(plus(c1,c_M))). [ur(13,a,20,a,c,595,a)]. 0.015/0.015 0.015/0.015 given #171 (F,wt=9): 675 -red(s(plus(c2,c_M)),s(plus(c1,c_M))). [ur(13,b,12,a,c,658,a)]. 0.015/0.015 0.015/0.015 given #172 (T,wt=9): 235 reds(plus(plus(c1,plus(0,0)),0),c2). [ur(13,a,21,a,b,231,a)]. 0.015/0.015 0.015/0.015 given #173 (T,wt=9): 236 reds(plus(x,plus(plus(0,0),0)),x). [ur(13,a,38,a,b,232,a)]. 0.015/0.015 0.015/0.015 given #174 (T,wt=9): 238 reds(plus(plus(x,plus(0,0)),0),x). [ur(13,a,21,a,b,232,a)]. 0.015/0.015 0.015/0.015 given #175 (T,wt=9): 262 reds(plus(plus(x,0),s(0)),s(x)). [ur(13,a,39,a,b,196,a)]. 0.015/0.015 0.015/0.015 given #176 (A,wt=15): 55 -reds(U11(tt,c_M,c1),x) | -red(plus(c2,s(c_M)),y) | -reds(y,x). [resolve(24,a,13,c)]. 0.015/0.015 0.015/0.015 given #177 (F,wt=7): 676 -red(plus(c2,c_M),plus(c1,c_M)). [resolve(675,a,18,b)]. 0.015/0.015 0.015/0.015 given #178 (F,wt=9): 804 -reds(U11(tt,c_M,c1),s(plus(c2,c_M))). [ur(55,b,22,a,c,217,a)]. 0.015/0.015 0.015/0.015 given #179 (F,wt=9): 824 -red(U11(tt,c_M,c1),s(plus(c2,c_M))). [ur(13,b,12,a,c,804,a)]. 0.015/0.015 0.015/0.015 given #180 (F,wt=9): 825 -reds(U12(tt,c_M,c1),s(plus(c2,c_M))). [ur(13,a,19,a,c,804,a)]. 0.015/0.015 0.015/0.015 ============================== PROOF ================================= 0.015/0.015 0.015/0.015 % Proof 1 at 0.02 (+ 0.01) seconds. 0.015/0.015 % Length of proof is 25. 0.015/0.015 % Level of proof is 6. 0.015/0.015 % Maximum clause weight is 15.000. 0.015/0.015 % Given clauses 180. 0.015/0.015 0.015/0.015 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 0.015/0.015 4 red(x,y) -> red(plus(x,z2),plus(y,z2)) # label(non_clause). [assumption]. 0.015/0.015 6 red(x,y) -> red(s(x),s(y)) # label(non_clause). [assumption]. 0.015/0.015 7 (all M all N red(U11(tt,M,N),U12(tt,M,N))) # label(non_clause). [assumption]. 0.015/0.015 8 (all M all N red(U12(tt,M,N),s(plus(N,M)))) # label(non_clause). [assumption]. 0.015/0.015 10 (all M all N red(plus(N,s(M)),U11(tt,M,N))) # label(non_clause). [assumption]. 0.015/0.015 11 (all N all y exists z (red(N,y) -> reds(plus(y,s(c_M)),z) & reds(U11(tt,c_M,N),z))) # label(non_clause) # label(goal). [goal]. 0.015/0.015 12 reds(x,x). [assumption]. 0.015/0.015 13 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 0.015/0.015 16 -red(x,y) | red(plus(x,z),plus(y,z)). [clausify(4)]. 0.015/0.015 18 -red(x,y) | red(s(x),s(y)). [clausify(6)]. 0.015/0.015 19 red(U11(tt,x,y),U12(tt,x,y)). [clausify(7)]. 0.015/0.015 20 red(U12(tt,x,y),s(plus(y,x))). [clausify(8)]. 0.015/0.015 22 red(plus(x,s(y)),U11(tt,y,x)). [clausify(10)]. 0.015/0.015 23 red(c1,c2). [deny(11)]. 0.015/0.015 24 -reds(plus(c2,s(c_M)),x) | -reds(U11(tt,c_M,c1),x). [deny(11)]. 0.015/0.015 36 reds(U12(tt,x,y),s(plus(y,x))). [ur(13,a,20,a,b,12,a)]. 0.015/0.015 51 red(plus(c1,x),plus(c2,x)). [ur(16,a,23,a)]. 0.015/0.015 55 -reds(U11(tt,c_M,c1),x) | -red(plus(c2,s(c_M)),y) | -reds(y,x). [resolve(24,a,13,c)]. 0.015/0.015 113 red(s(plus(c1,x)),s(plus(c2,x))). [ur(18,a,51,a)]. 0.015/0.015 217 reds(U11(tt,x,y),s(plus(y,x))). [ur(13,a,19,a,b,36,a)]. 0.015/0.015 355 reds(s(plus(c1,x)),s(plus(c2,x))). [ur(13,a,113,a,b,12,a)]. 0.015/0.015 804 -reds(U11(tt,c_M,c1),s(plus(c2,c_M))). [ur(55,b,22,a,c,217,a)]. 0.015/0.015 825 -reds(U12(tt,c_M,c1),s(plus(c2,c_M))). [ur(13,a,19,a,c,804,a)]. 0.015/0.015 846 $F. [ur(13,a,20,a,c,825,a),unit_del(a,355)]. 0.015/0.015 0.015/0.015 ============================== end of proof ========================== 0.015/0.015 0.015/0.015 ============================== STATISTICS ============================ 0.015/0.015 0.015/0.015 Given=180. Generated=977. Kept=834. proofs=1. 0.015/0.015 Usable=180. Sos=634. Demods=0. Limbo=20, Disabled=13. Hints=0. 0.015/0.015 Kept_by_rule=0, Deleted_by_rule=0. 0.015/0.015 Forward_subsumed=142. Back_subsumed=0. 0.015/0.015 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 0.015/0.015 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 0.015/0.015 Demod_attempts=0. Demod_rewrites=0. 0.015/0.015 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 0.015/0.015 Nonunit_fsub_feature_tests=364. Nonunit_bsub_feature_tests=664. 0.015/0.015 Megabytes=1.45. 0.015/0.015 User_CPU=0.02, System_CPU=0.01, Wall_clock=0. 0.015/0.015 0.015/0.015 ============================== end of statistics ===================== 0.015/0.015 0.015/0.015 ============================== end of search ========================= 0.015/0.015 0.015/0.015 THEOREM PROVED 0.015/0.015 0.015/0.015 Exiting with 1 proof. 0.015/0.015 0.015/0.015 Process 43196 exit (max_proofs) Tue Nov 16 11:31:22 2021 0.015/0.015 0.015/0.015 0.015/0.015 The problem is joinable. 0.015/0.015 0.11user 0.03system 0:00.15elapsed 98%CPU (0avgtext+0avgdata 26752maxresident)k 0.015/0.015 0inputs+0outputs (0major+9157minor)pagefaults 0swaps