30.16/20.48 NO 30.16/20.48 30.16/20.48 Problem 1: 30.16/20.48 30.16/20.48 30.16/20.48 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 30.16/20.48 Confluence Problem: 30.16/20.48 (VAR vNonEmpty:S xs:S y':S ws:S v:S ys':S w:S x':S xs':S zs:S z:S ys:S y:S) 30.16/20.48 (STRATEGY CONTEXTSENSITIVE 30.16/20.48 (get 1) 30.16/20.48 (ssp' 1 2) 30.16/20.48 (sub 1 2) 30.16/20.48 (0) 30.16/20.48 (cons 1 2) 30.16/20.48 (fSNonEmpty) 30.16/20.48 (nil) 30.16/20.48 (s 1) 30.16/20.48 (tp2 1 2) 30.16/20.48 ) 30.16/20.48 (RULES 30.16/20.48 get(cons(x':S,xs':S)) -> tp2(y:S,cons(x':S,zs:S)) | get(xs':S) ->* tp2(y:S,zs:S) 30.16/20.48 get(cons(y:S,ys:S)) -> tp2(y:S,ys:S) 30.16/20.48 ssp'(cons(y':S,ws:S),v:S) -> cons(y':S,ys':S) | sub(v:S,y':S) ->* w:S, ssp'(ws:S,w:S) ->* ys':S 30.16/20.48 ssp'(cons(x':S,xs':S),v:S) -> cons(y':S,ys':S) | get(xs':S) ->* tp2(y':S,zs:S), sub(v:S,y':S) ->* w:S, ssp'(cons(x':S,zs:S),w:S) ->* ys':S 30.16/20.48 ssp'(xs:S,0) -> nil 30.16/20.48 sub(s(v:S),s(w:S)) -> z:S | sub(v:S,w:S) ->* z:S 30.16/20.48 sub(z:S,0) -> z:S 30.16/20.48 ) 30.16/20.48 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 30.16/20.48 30.16/20.48 30.16/20.48 Problem 1: 30.16/20.48 30.16/20.48 Inlining of Conditions Processor [STERN17]: 30.16/20.48 30.16/20.48 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 30.16/20.48 Confluence Problem: 30.16/20.48 (VAR vNonEmpty:S xs:S y':S ws:S v:S ys':S w:S x':S xs':S zs:S z:S ys:S y:S) 30.16/20.48 (STRATEGY CONTEXTSENSITIVE 30.16/20.48 (get 1) 30.16/20.48 (ssp' 1 2) 30.16/20.48 (sub 1 2) 30.16/20.48 (0) 30.16/20.48 (cons 1 2) 30.16/20.48 (fSNonEmpty) 30.16/20.48 (nil) 30.16/20.48 (s 1) 30.16/20.48 (tp2 1 2) 30.16/20.48 ) 30.16/20.48 (RULES 30.16/20.48 get(cons(x':S,xs':S)) -> tp2(y:S,cons(x':S,zs:S)) | get(xs':S) ->* tp2(y:S,zs:S) 30.16/20.48 get(cons(y:S,ys:S)) -> tp2(y:S,ys:S) 30.16/20.48 ssp'(cons(y':S,ws:S),v:S) -> cons(y':S,ssp'(ws:S,sub(v:S,y':S))) 30.16/20.48 ssp'(cons(x':S,xs':S),v:S) -> cons(y':S,ssp'(cons(x':S,zs:S),sub(v:S,y':S))) | get(xs':S) ->* tp2(y':S,zs:S) 30.16/20.48 ssp'(xs:S,0) -> nil 30.16/20.48 sub(s(v:S),s(w:S)) -> sub(v:S,w:S) 30.16/20.48 sub(z:S,0) -> z:S 30.16/20.48 ) 30.16/20.48 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 30.16/20.48 30.16/20.48 30.16/20.48 Problem 1: 30.16/20.48 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 30.16/20.48 Confluence Problem: 30.16/20.48 (VAR vNonEmpty:S xs:S y':S ws:S v:S ys':S w:S x':S xs':S zs:S z:S ys:S y:S) 30.16/20.48 (STRATEGY CONTEXTSENSITIVE 30.16/20.48 (get 1) 30.16/20.48 (ssp' 1 2) 30.16/20.48 (sub 1 2) 30.16/20.48 (0) 30.16/20.48 (cons 1 2) 30.16/20.48 (fSNonEmpty) 30.16/20.48 (nil) 30.16/20.48 (s 1) 30.16/20.48 (tp2 1 2) 30.16/20.48 ) 30.16/20.48 (RULES 30.16/20.48 get(cons(x':S,xs':S)) -> tp2(y:S,cons(x':S,zs:S)) | get(xs':S) ->* tp2(y:S,zs:S) 30.16/20.48 get(cons(y:S,ys:S)) -> tp2(y:S,ys:S) 30.16/20.48 ssp'(cons(y':S,ws:S),v:S) -> cons(y':S,ssp'(ws:S,sub(v:S,y':S))) 30.16/20.48 ssp'(cons(x':S,xs':S),v:S) -> cons(y':S,ssp'(cons(x':S,zs:S),sub(v:S,y':S))) | get(xs':S) ->* tp2(y':S,zs:S) 30.16/20.48 ssp'(xs:S,0) -> nil 30.16/20.48 sub(s(v:S),s(w:S)) -> sub(v:S,w:S) 30.16/20.48 sub(z:S,0) -> z:S 30.16/20.48 ) 30.16/20.48 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 30.16/20.48 30.16/20.48 Critical Pairs Processor: 30.16/20.48 -> Rules: 30.16/20.48 get(cons(x':S,xs':S)) -> tp2(y:S,cons(x':S,zs:S)) | get(xs':S) ->* tp2(y:S,zs:S) 30.16/20.48 get(cons(y:S,ys:S)) -> tp2(y:S,ys:S) 30.16/20.48 ssp'(cons(y':S,ws:S),v:S) -> cons(y':S,ssp'(ws:S,sub(v:S,y':S))) 30.16/20.48 ssp'(cons(x':S,xs':S),v:S) -> cons(y':S,ssp'(cons(x':S,zs:S),sub(v:S,y':S))) | get(xs':S) ->* tp2(y':S,zs:S) 30.16/20.48 ssp'(xs:S,0) -> nil 30.16/20.48 sub(s(v:S),s(w:S)) -> sub(v:S,w:S) 30.16/20.48 sub(z:S,0) -> z:S 30.16/20.48 -> Vars: 30.16/20.48 "x'", "xs'", "zs", "y", "ys", "y", "y'", "ws", "v", "y'", "v", "x'", "xs'", "zs", "xs", "v", "w", "z" 30.16/20.48 -> FVars: 30.16/20.48 "x13", "x14", "x15", "x16", "x17", "x18", "x19", "x20", "x21", "x22", "x23", "x24", "x25", "x26", "x27", "x28", "x29", "x30" 30.16/20.48 -> PVars: 30.16/20.48 "x'": ["x13", "x24"], "xs'": ["x14", "x25"], "zs": ["x15", "x26"], "y": ["x16", "x18"], "ys": ["x17"], "y'": ["x19", "x22"], "ws": ["x20"], "v": ["x21", "x23", "x28"], "xs": ["x27"], "w": ["x29"], "z": ["x30"] 30.16/20.48 30.16/20.48 -> Rlps: 30.16/20.48 crule: get(cons(x13:S,x14:S)) -> tp2(x16:S,cons(x13:S,x15:S)) | get(x14:S) ->* tp2(x16:S,x15:S), id: 1, possubterms: get(cons(x13:S,x14:S))-> [], cons(x13:S,x14:S)-> [1] 30.16/20.48 crule: get(cons(x18:S,x17:S)) -> tp2(x18:S,x17:S), id: 2, possubterms: get(cons(x18:S,x17:S))-> [], cons(x18:S,x17:S)-> [1] 30.16/20.48 crule: ssp'(cons(x19:S,x20:S),x21:S) -> cons(x19:S,ssp'(x20:S,sub(x21:S,x19:S))), id: 3, possubterms: ssp'(cons(x19:S,x20:S),x21:S)-> [], cons(x19:S,x20:S)-> [1] 30.16/20.48 crule: ssp'(cons(x24:S,x25:S),x23:S) -> cons(x22:S,ssp'(cons(x24:S,x26:S),sub(x23:S,x22:S))) | get(x25:S) ->* tp2(x22:S,x26:S), id: 4, possubterms: ssp'(cons(x24:S,x25:S),x23:S)-> [], cons(x24:S,x25:S)-> [1] 30.16/20.48 crule: ssp'(x27:S,0) -> nil, id: 5, possubterms: ssp'(x27:S,0)-> [], 0-> [2] 30.16/20.48 crule: sub(s(x28:S),s(x29:S)) -> sub(x28:S,x29:S), id: 6, possubterms: sub(s(x28:S),s(x29:S))-> [], s(x28:S)-> [1], s(x29:S)-> [2] 30.16/20.48 crule: sub(x30:S,0) -> x30:S, id: 7, possubterms: sub(x30:S,0)-> [], 0-> [2] 30.16/20.48 30.16/20.48 -> Unifications: 30.16/20.48 R2 unifies with R1 at p: [], l: get(cons(x18:S,x17:S)), lp: get(cons(x18:S,x17:S)), conds: {get(xs':S) ->* tp2(y:S,zs:S)}, sig: {x17:S -> xs':S,x18:S -> x':S}, l': get(cons(x':S,xs':S)), r: tp2(x18:S,x17:S), r': tp2(y:S,cons(x':S,zs:S)) 30.16/20.48 R4 unifies with R3 at p: [], l: ssp'(cons(x24:S,x25:S),x23:S), lp: ssp'(cons(x24:S,x25:S),x23:S), conds: {get(x25:S) ->* tp2(x22:S,x26:S)}, sig: {x23:S -> v:S,x24:S -> y':S,x25:S -> ws:S}, l': ssp'(cons(y':S,ws:S),v:S), r: cons(x22:S,ssp'(cons(x24:S,x26:S),sub(x23:S,x22:S))), r': cons(y':S,ssp'(ws:S,sub(v:S,y':S))) 30.16/20.48 R5 unifies with R3 at p: [], l: ssp'(x27:S,0), lp: ssp'(x27:S,0), conds: {}, sig: {v:S -> 0,x27:S -> cons(y':S,ws:S)}, l': ssp'(cons(y':S,ws:S),v:S), r: nil, r': cons(y':S,ssp'(ws:S,sub(v:S,y':S))) 30.16/20.48 R5 unifies with R4 at p: [], l: ssp'(x27:S,0), lp: ssp'(x27:S,0), conds: {get(xs':S) ->* tp2(y':S,zs:S)}, sig: {v:S -> 0,x27:S -> cons(x':S,xs':S)}, l': ssp'(cons(x':S,xs':S),v:S), r: nil, r': cons(y':S,ssp'(cons(x':S,zs:S),sub(v:S,y':S))) 30.16/20.48 30.16/20.48 -> Critical pairs info: 30.16/20.48 => Not trivial, Overlay, N1 30.16/20.48 | get(xs':S) ->* tp2(y':S,zs:S) => Not trivial, Overlay, N2 30.16/20.48 | get(xs':S) ->* tp2(y:S,zs:S) => Not trivial, Overlay, N3 30.16/20.48 | get(ws:S) ->* tp2(y':S,zs:S) => Not trivial, Overlay, N4 30.16/20.48 30.16/20.48 -> Problem conclusions: 30.16/20.48 Left linear, Not right linear, Not linear 30.16/20.48 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 30.16/20.48 CTRS Type: 3 30.16/20.48 Deterministic, Strongly deterministic 30.16/20.48 Oriented CTRS, Properly oriented CTRS, Maybe right-stable CTRS 30.16/20.48 Maybe normal CTRS, Maybe almost normal CTRS 30.16/20.48 Maybe level confluent 30.16/20.48 30.16/20.48 Problem 1: 30.16/20.48 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 30.16/20.48 Confluence Problem: 30.16/20.48 (VAR vNonEmpty:S xs:S y':S ws:S v:S ys':S w:S x':S xs':S zs:S z:S ys:S y:S) 30.16/20.48 (STRATEGY CONTEXTSENSITIVE 30.16/20.48 (get 1) 30.16/20.48 (ssp' 1 2) 30.16/20.48 (sub 1 2) 30.16/20.48 (0) 30.16/20.48 (cons 1 2) 30.16/20.48 (fSNonEmpty) 30.16/20.48 (nil) 30.16/20.48 (s 1) 30.16/20.48 (tp2 1 2) 30.16/20.48 ) 30.16/20.48 (RULES 30.16/20.48 get(cons(x':S,xs':S)) -> tp2(y:S,cons(x':S,zs:S)) | get(xs':S) ->* tp2(y:S,zs:S) 30.16/20.48 get(cons(y:S,ys:S)) -> tp2(y:S,ys:S) 30.16/20.48 ssp'(cons(y':S,ws:S),v:S) -> cons(y':S,ssp'(ws:S,sub(v:S,y':S))) 30.16/20.48 ssp'(cons(x':S,xs':S),v:S) -> cons(y':S,ssp'(cons(x':S,zs:S),sub(v:S,y':S))) | get(xs':S) ->* tp2(y':S,zs:S) 30.16/20.48 ssp'(xs:S,0) -> nil 30.16/20.48 sub(s(v:S),s(w:S)) -> sub(v:S,w:S) 30.16/20.48 sub(z:S,0) -> z:S 30.16/20.48 ) 30.16/20.48 Critical Pairs: 30.16/20.48 => Not trivial, Overlay, N1 30.16/20.48 | get(xs':S) ->* tp2(y':S,zs:S) => Not trivial, Overlay, N2 30.16/20.48 | get(xs':S) ->* tp2(y:S,zs:S) => Not trivial, Overlay, N3 30.16/20.48 | get(ws:S) ->* tp2(y':S,zs:S) => Not trivial, Overlay, N4 30.16/20.48 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 30.16/20.48 30.16/20.48 Conditional Critical Pairs Distributor Processor 30.16/20.48 30.16/20.48 Problem 1: 30.16/20.48 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 30.16/20.48 Confluence Problem: 30.16/20.48 (VAR vNonEmpty:S xs:S y':S ws:S v:S ys':S w:S x':S xs':S zs:S z:S ys:S y:S) 30.16/20.48 (STRATEGY CONTEXTSENSITIVE 30.16/20.48 (get 1) 30.16/20.48 (ssp' 1 2) 30.16/20.48 (sub 1 2) 30.16/20.48 (0) 30.16/20.48 (cons 1 2) 30.16/20.48 (fSNonEmpty) 30.16/20.48 (nil) 30.16/20.48 (s 1) 30.16/20.48 (tp2 1 2) 30.16/20.48 ) 30.16/20.48 (RULES 30.16/20.48 get(cons(x':S,xs':S)) -> tp2(y:S,cons(x':S,zs:S)) | get(xs':S) ->* tp2(y:S,zs:S) 30.16/20.48 get(cons(y:S,ys:S)) -> tp2(y:S,ys:S) 30.16/20.48 ssp'(cons(y':S,ws:S),v:S) -> cons(y':S,ssp'(ws:S,sub(v:S,y':S))) 30.16/20.48 ssp'(cons(x':S,xs':S),v:S) -> cons(y':S,ssp'(cons(x':S,zs:S),sub(v:S,y':S))) | get(xs':S) ->* tp2(y':S,zs:S) 30.16/20.48 ssp'(xs:S,0) -> nil 30.16/20.48 sub(s(v:S),s(w:S)) -> sub(v:S,w:S) 30.16/20.48 sub(z:S,0) -> z:S 30.16/20.48 ) 30.16/20.48 Critical Pairs: 30.16/20.48 => Not trivial, Overlay, N1 30.16/20.48 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 30.16/20.48 30.16/20.48 Infeasible Convergence No Conditions CCP Processor: 30.16/20.48 Infeasible convergence? 30.16/20.48 YES 30.16/20.48 30.16/20.48 Problem 1: 30.16/20.48 30.16/20.48 Infeasibility Problem: 30.16/20.48 [(VAR vNonEmpty:S xs:S y1:S ws:S v:S ys1:S w:S x1:S xs1:S zs:S z:S ys:S y:S x:S) 30.16/20.49 (STRATEGY CONTEXTSENSITIVE 30.16/20.49 (get 1) 30.16/20.49 (ssp1 1 2) 30.16/20.49 (sub 1 2) 30.16/20.49 (0) 30.16/20.49 (cons 1 2) 30.16/20.49 (cws) 30.16/20.49 (cy') 30.16/20.49 (fSNonEmpty) 30.16/20.49 (nil) 30.16/20.49 (s 1) 30.16/20.49 (ssp' 1 2) 30.16/20.49 (tp2 1 2) 30.16/20.49 ) 30.16/20.49 (RULES 30.16/20.49 get(cons(x1:S,xs1:S)) -> tp2(y:S,cons(x1:S,zs:S)) | get(xs1:S) ->* tp2(y:S,zs:S) 30.16/20.49 get(cons(y:S,ys:S)) -> tp2(y:S,ys:S) 30.16/20.49 ssp1(cons(y1:S,ws:S),v:S) -> cons(y1:S,ssp1(ws:S,sub(v:S,y1:S))) 30.16/20.49 ssp1(cons(x1:S,xs1:S),v:S) -> cons(y1:S,ssp1(cons(x1:S,zs:S),sub(v:S,y1:S))) | get(xs1:S) ->* tp2(y1:S,zs:S) 30.16/20.49 ssp1(xs:S,0) -> nil 30.16/20.49 sub(s(v:S),s(w:S)) -> sub(v:S,w:S) 30.16/20.49 sub(z:S,0) -> z:S 30.16/20.49 )] 30.16/20.49 30.16/20.49 Infeasibility Conditions: 30.16/20.49 cons(cy',ssp'(cws,sub(0,cy'))) ->* x:S, nil ->* x:S 30.16/20.49 30.16/20.49 Problem 1: 30.16/20.49 30.16/20.49 Obtaining a model using Mace4: 30.16/20.49 30.16/20.49 -> Usable Rules: 30.16/20.49 sub(s(v:S),s(w:S)) -> sub(v:S,w:S) 30.16/20.49 sub(z:S,0) -> z:S 30.16/20.49 30.16/20.49 -> Mace4 Output: 30.16/20.49 ============================== Mace4 ================================= 30.16/20.49 Mace4 (64) version 2009-11A, November 2009. 30.16/20.49 Process 12880 was started by sandbox2 on n150.star.cs.uiowa.edu, 30.16/20.49 Tue Jul 6 10:41:05 2021 30.16/20.49 The command was "./mace4 -c -f /tmp/mace412864.in". 30.16/20.49 ============================== end of head =========================== 30.16/20.49 30.16/20.49 ============================== INPUT ================================= 30.16/20.49 30.16/20.49 % Reading from file /tmp/mace412864.in 30.16/20.49 30.16/20.49 assign(max_seconds,10). 30.16/20.49 30.16/20.49 formulas(assumptions). 30.16/20.49 ->(x1,y) -> ->(get(x1),get(y)) # label(congruence). 30.16/20.49 ->(x1,y) -> ->(ssp1(x1,x2),ssp1(y,x2)) # label(congruence). 30.16/20.49 ->(x2,y) -> ->(ssp1(x1,x2),ssp1(x1,y)) # label(congruence). 30.16/20.49 ->(x1,y) -> ->(sub(x1,x2),sub(y,x2)) # label(congruence). 30.16/20.49 ->(x2,y) -> ->(sub(x1,x2),sub(x1,y)) # label(congruence). 30.16/20.49 ->(x1,y) -> ->(cons(x1,x2),cons(y,x2)) # label(congruence). 30.16/20.49 ->(x2,y) -> ->(cons(x1,x2),cons(x1,y)) # label(congruence). 30.16/20.49 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence). 30.16/20.49 ->(x1,y) -> ->(ssp'(x1,x2),ssp'(y,x2)) # label(congruence). 30.16/20.49 ->(x2,y) -> ->(ssp'(x1,x2),ssp'(x1,y)) # label(congruence). 30.16/20.49 ->(x1,y) -> ->(tp2(x1,x2),tp2(y,x2)) # label(congruence). 30.16/20.49 ->(x2,y) -> ->(tp2(x1,x2),tp2(x1,y)) # label(congruence). 30.16/20.49 ->(sub(s(x4),s(x6)),sub(x4,x6)) # label(replacement). 30.16/20.49 ->(sub(x10,0),x10) # label(replacement). 30.16/20.49 ->*(x,x) # label(reflexivity). 30.16/20.49 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 30.16/20.49 end_of_list. 30.16/20.49 30.16/20.49 formulas(goals). 30.16/20.49 (exists x13 (->*(cons(cy',ssp'(cws,sub(0,cy'))),x13) & ->*(nil,x13))) # label(goal). 30.16/20.49 end_of_list. 30.16/20.49 30.16/20.49 ============================== end of input ========================== 30.16/20.49 30.16/20.49 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 30.16/20.49 30.16/20.49 % Formulas that are not ordinary clauses: 30.16/20.49 1 ->(x1,y) -> ->(get(x1),get(y)) # label(congruence) # label(non_clause). [assumption]. 30.16/20.49 2 ->(x1,y) -> ->(ssp1(x1,x2),ssp1(y,x2)) # label(congruence) # label(non_clause). [assumption]. 30.16/20.49 3 ->(x2,y) -> ->(ssp1(x1,x2),ssp1(x1,y)) # label(congruence) # label(non_clause). [assumption]. 30.16/20.49 4 ->(x1,y) -> ->(sub(x1,x2),sub(y,x2)) # label(congruence) # label(non_clause). [assumption]. 30.16/20.49 5 ->(x2,y) -> ->(sub(x1,x2),sub(x1,y)) # label(congruence) # label(non_clause). [assumption]. 30.16/20.49 6 ->(x1,y) -> ->(cons(x1,x2),cons(y,x2)) # label(congruence) # label(non_clause). [assumption]. 30.16/20.49 7 ->(x2,y) -> ->(cons(x1,x2),cons(x1,y)) # label(congruence) # label(non_clause). [assumption]. 30.16/20.49 8 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 30.16/20.49 9 ->(x1,y) -> ->(ssp'(x1,x2),ssp'(y,x2)) # label(congruence) # label(non_clause). [assumption]. 30.16/20.49 10 ->(x2,y) -> ->(ssp'(x1,x2),ssp'(x1,y)) # label(congruence) # label(non_clause). [assumption]. 30.16/20.49 11 ->(x1,y) -> ->(tp2(x1,x2),tp2(y,x2)) # label(congruence) # label(non_clause). [assumption]. 30.16/20.49 12 ->(x2,y) -> ->(tp2(x1,x2),tp2(x1,y)) # label(congruence) # label(non_clause). [assumption]. 30.16/20.49 13 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 30.16/20.49 14 (exists x13 (->*(cons(cy',ssp'(cws,sub(0,cy'))),x13) & ->*(nil,x13))) # label(goal) # label(non_clause) # label(goal). [goal]. 30.16/20.49 30.16/20.49 ============================== end of process non-clausal formulas === 30.16/20.49 30.16/20.49 ============================== CLAUSES FOR SEARCH ==================== 30.16/20.49 30.16/20.49 formulas(mace4_clauses). 30.16/20.49 -->(x,y) | ->(get(x),get(y)) # label(congruence). 30.16/20.49 -->(x,y) | ->(ssp1(x,z),ssp1(y,z)) # label(congruence). 30.16/20.49 -->(x,y) | ->(ssp1(z,x),ssp1(z,y)) # label(congruence). 30.16/20.49 -->(x,y) | ->(sub(x,z),sub(y,z)) # label(congruence). 30.16/20.49 -->(x,y) | ->(sub(z,x),sub(z,y)) # label(congruence). 30.16/20.49 -->(x,y) | ->(cons(x,z),cons(y,z)) # label(congruence). 30.16/20.49 -->(x,y) | ->(cons(z,x),cons(z,y)) # label(congruence). 30.16/20.49 -->(x,y) | ->(s(x),s(y)) # label(congruence). 30.16/20.49 -->(x,y) | ->(ssp'(x,z),ssp'(y,z)) # label(congruence). 30.16/20.49 -->(x,y) | ->(ssp'(z,x),ssp'(z,y)) # label(congruence). 30.16/20.49 -->(x,y) | ->(tp2(x,z),tp2(y,z)) # label(congruence). 30.16/20.49 -->(x,y) | ->(tp2(z,x),tp2(z,y)) # label(congruence). 30.16/20.49 ->(sub(s(x),s(y)),sub(x,y)) # label(replacement). 30.16/20.49 ->(sub(x,0),x) # label(replacement). 30.16/20.49 ->*(x,x) # label(reflexivity). 30.16/20.49 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 30.16/20.49 -->*(cons(cy',ssp'(cws,sub(0,cy'))),x) | -->*(nil,x) # label(goal). 30.16/20.49 end_of_list. 30.16/20.49 30.16/20.49 ============================== end of clauses for search ============= 30.16/20.49 30.16/20.49 % There are no natural numbers in the input. 30.16/20.49 30.16/20.49 ============================== DOMAIN SIZE 2 ========================= 30.16/20.49 30.16/20.49 ============================== MODEL ================================= 30.16/20.49 30.16/20.49 interpretation( 2, [number=1, seconds=0], [ 30.16/20.49 30.16/20.49 function(nil, [ 0 ]), 30.16/20.49 30.16/20.49 function(0, [ 0 ]), 30.16/20.49 30.16/20.49 function(cws, [ 0 ]), 30.16/20.49 30.16/20.49 function(cy', [ 0 ]), 30.16/20.49 30.16/20.49 function(s(_), [ 0, 1 ]), 30.16/20.49 30.16/20.49 function(get(_), [ 0, 0 ]), 30.16/20.49 30.16/20.49 function(ssp'(_,_), [ 30.16/20.49 0, 0, 30.16/20.49 0, 0 ]), 30.16/20.49 30.16/20.49 function(tp2(_,_), [ 30.16/20.49 0, 0, 30.16/20.49 0, 0 ]), 30.16/20.49 30.16/20.49 function(ssp1(_,_), [ 30.16/20.49 0, 0, 30.16/20.49 0, 0 ]), 30.16/20.49 30.16/20.49 function(sub(_,_), [ 30.16/20.49 0, 0, 30.16/20.49 1, 0 ]), 30.16/20.49 30.16/20.49 function(cons(_,_), [ 30.16/20.49 1, 0, 30.16/20.49 0, 0 ]), 30.16/20.49 30.16/20.49 relation(->*(_,_), [ 30.16/20.49 1, 0, 30.16/20.49 0, 1 ]), 30.16/20.49 30.16/20.49 relation(->(_,_), [ 30.16/20.49 1, 0, 30.16/20.49 0, 1 ]) 30.16/20.49 ]). 30.16/20.49 30.16/20.49 ============================== end of model ========================== 30.16/20.49 30.16/20.49 ============================== STATISTICS ============================ 30.16/20.49 30.16/20.49 For domain size 2. 30.16/20.49 30.16/20.49 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 30.16/20.49 Ground clauses: seen=106, kept=102. 30.16/20.49 Selections=27, assignments=29, propagations=11, current_models=1. 30.16/20.49 Rewrite_terms=235, rewrite_bools=150, indexes=22. 30.16/20.49 Rules_from_neg_clauses=3, cross_offs=3. 30.16/20.49 30.16/20.49 ============================== end of statistics ===================== 30.16/20.49 30.16/20.49 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 30.16/20.49 30.16/20.49 Exiting with 1 model. 30.16/20.49 30.16/20.49 Process 12880 exit (max_models) Tue Jul 6 10:41:05 2021 30.16/20.49 The process finished Tue Jul 6 10:41:05 2021 30.16/20.49 30.16/20.49 30.16/20.49 Mace4 cooked interpretation: 30.16/20.49 30.16/20.49 % number = 1 30.16/20.49 % seconds = 0 30.16/20.49 30.16/20.49 % Interpretation of size 2 30.16/20.49 30.16/20.49 nil = 0. 30.16/20.49 30.16/20.49 0 = 0. 30.16/20.49 30.16/20.49 cws = 0. 30.16/20.49 30.16/20.49 cy' = 0. 30.16/20.49 30.16/20.49 s(0) = 0. 30.16/20.49 s(1) = 1. 30.16/20.49 30.16/20.49 get(0) = 0. 30.16/20.49 get(1) = 0. 30.16/20.49 30.16/20.49 ssp'(0,0) = 0. 30.16/20.49 ssp'(0,1) = 0. 30.16/20.49 ssp'(1,0) = 0. 30.16/20.49 ssp'(1,1) = 0. 30.16/20.49 30.16/20.49 tp2(0,0) = 0. 30.16/20.49 tp2(0,1) = 0. 30.16/20.49 tp2(1,0) = 0. 30.16/20.49 tp2(1,1) = 0. 30.16/20.49 30.16/20.49 ssp1(0,0) = 0. 30.16/20.49 ssp1(0,1) = 0. 30.16/20.49 ssp1(1,0) = 0. 30.16/20.49 ssp1(1,1) = 0. 30.16/20.49 30.16/20.49 sub(0,0) = 0. 30.16/20.49 sub(0,1) = 0. 30.16/20.49 sub(1,0) = 1. 30.16/20.49 sub(1,1) = 0. 30.16/20.49 30.16/20.49 cons(0,0) = 1. 30.16/20.49 cons(0,1) = 0. 30.16/20.49 cons(1,0) = 0. 30.16/20.49 cons(1,1) = 0. 30.16/20.49 30.16/20.49 ->*(0,0). 30.16/20.49 - ->*(0,1). 30.16/20.49 - ->*(1,0). 30.16/20.49 ->*(1,1). 30.16/20.49 30.16/20.49 ->(0,0). 30.16/20.49 - ->(0,1). 30.16/20.49 - ->(1,0). 30.16/20.49 ->(1,1). 30.16/20.49 30.16/20.49 30.16/20.49 The problem is infeasible. 30.16/20.49 30.16/20.49 30.16/20.49 The problem is not joinable. 30.16/20.49 EOF