NO
Problem 1:
Infeasibility Problem:
[(VAR vNonEmpty x n h t m pid st1 in2 st2 in3 st3 vNonEmpty x2 x4)
(STRATEGY CONTEXTSENSITIVE
(app 1 2)
(empty 1)
(fstsplit 1 2)
(head 1)
(length 1)
(leq 1 2)
(mapf 1 2)
(ring 1 2 3 4 5 6)
(sndsplit 1 2)
(tail 1)
(0)
(cons 1 2)
(f 1 2)
(fSNonEmpty)
(false)
(nil)
(s 1)
(three)
(true)
(two)
)
(RULES
app(cons(h,t),x) -> cons(h,app(t,x))
app(nil,x) -> x
empty(cons(h,t)) -> false
empty(nil) -> true
fstsplit(0,x) -> nil
fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t))
fstsplit(s(n),nil) -> nil
head(cons(h,t)) -> h
length(cons(h,t)) -> s(length(t))
length(nil) -> 0
leq(0,m) -> true
leq(s(n),0) -> false
leq(s(n),s(m)) -> leq(n,m)
mapf(pid,cons(h,t)) -> app(f(pid,h),mapf(pid,t))
mapf(pid,nil) -> nil
ring(st1,in2,st2,in3,st3,m) -> ring(sndsplit(m,st1),cons(fstsplit(m,st1),in2),st2,in3,st3,m) | empty(fstsplit(m,st1)) ->* false
ring(st1,in2,st2,in3,st3,m) -> ring(st1,tail(in2),sndsplit(m,app(mapf(two,head(in2)),st2)),cons(fstsplit(m,app(mapf(two,head(in2)),st2)),in3),st3,m) | leq(m,length(st2)) ->* false, empty(fstsplit(m,app(mapf(two,head(in2)),st2))) ->* false
ring(st1,in2,st2,in3,st3,m) -> ring(st1,tail(in2),st2,in3,st3,m) | empty(mapf(two,head(in2))) ->* true
ring(st1,in2,st2,in3,st3,m) -> ring(st1,in2,sndsplit(m,st2),cons(fstsplit(m,st2),in3),st3,m) | leq(m,length(st2)) ->* true, empty(fstsplit(m,st2)) ->* false
ring(st1,in2,st2,in3,st3,m) -> ring(st1,in2,st2,tail(in3),sndsplit(m,app(mapf(three,head(in3)),st3)),m) | leq(m,length(st3)) ->* false, empty(fstsplit(m,app(mapf(three,head(in3)),st3))) ->* false
ring(st1,in2,st2,in3,st3,m) -> ring(st1,in2,st2,tail(in3),st3,m) | empty(mapf(three,head(in3))) ->* true
ring(st1,in2,st2,in3,st3,m) -> ring(st1,in2,st2,in3,sndsplit(m,st3),m) | leq(m,length(st3)) ->* true, empty(fstsplit(m,st3)) ->* false
sndsplit(0,x) -> x
sndsplit(s(n),cons(h,t)) -> sndsplit(n,t)
sndsplit(s(n),nil) -> nil
tail(cons(h,t)) -> t
)
]
Infeasibility Conditions:
empty(mapf(two,head(x2))) ->* true, empty(mapf(three,head(x4))) ->* true
Problem 1:
Obtaining a proof using Prover9:
-> Prover9 Output:
============================== Prover9 ===============================
Prover9 (64) version 2009-11A, November 2009.
Process 3174756 was started by sandbox on z034.star.cs.uiowa.edu,
Tue Jul 30 08:47:40 2024
The command was "./prover9 -f /tmp/prover93174749-0.in".
============================== end of head ===========================
============================== INPUT =================================
% Reading from file /tmp/prover93174749-0.in
assign(max_seconds,20).
formulas(assumptions).
->_s0(x1,y) -> ->_s0(app(x1,x2),app(y,x2)) # label(congruence).
->_s0(x2,y) -> ->_s0(app(x1,x2),app(x1,y)) # label(congruence).
->_s0(x1,y) -> ->_s0(empty(x1),empty(y)) # label(congruence).
->_s0(x1,y) -> ->_s0(fstsplit(x1,x2),fstsplit(y,x2)) # label(congruence).
->_s0(x2,y) -> ->_s0(fstsplit(x1,x2),fstsplit(x1,y)) # label(congruence).
->_s0(x1,y) -> ->_s0(head(x1),head(y)) # label(congruence).
->_s0(x1,y) -> ->_s0(length(x1),length(y)) # label(congruence).
->_s0(x1,y) -> ->_s0(leq(x1,x2),leq(y,x2)) # label(congruence).
->_s0(x2,y) -> ->_s0(leq(x1,x2),leq(x1,y)) # label(congruence).
->_s0(x1,y) -> ->_s0(mapf(x1,x2),mapf(y,x2)) # label(congruence).
->_s0(x2,y) -> ->_s0(mapf(x1,x2),mapf(x1,y)) # label(congruence).
->_s0(x1,y) -> ->_s0(ring(x1,x2,x3,x4,x5,x6),ring(y,x2,x3,x4,x5,x6)) # label(congruence).
->_s0(x2,y) -> ->_s0(ring(x1,x2,x3,x4,x5,x6),ring(x1,y,x3,x4,x5,x6)) # label(congruence).
->_s0(x3,y) -> ->_s0(ring(x1,x2,x3,x4,x5,x6),ring(x1,x2,y,x4,x5,x6)) # label(congruence).
->_s0(x4,y) -> ->_s0(ring(x1,x2,x3,x4,x5,x6),ring(x1,x2,x3,y,x5,x6)) # label(congruence).
->_s0(x5,y) -> ->_s0(ring(x1,x2,x3,x4,x5,x6),ring(x1,x2,x3,x4,y,x6)) # label(congruence).
->_s0(x6,y) -> ->_s0(ring(x1,x2,x3,x4,x5,x6),ring(x1,x2,x3,x4,x5,y)) # label(congruence).
->_s0(x1,y) -> ->_s0(sndsplit(x1,x2),sndsplit(y,x2)) # label(congruence).
->_s0(x2,y) -> ->_s0(sndsplit(x1,x2),sndsplit(x1,y)) # label(congruence).
->_s0(x1,y) -> ->_s0(tail(x1),tail(y)) # label(congruence).
->_s0(x1,y) -> ->_s0(cons(x1,x2),cons(y,x2)) # label(congruence).
->_s0(x2,y) -> ->_s0(cons(x1,x2),cons(x1,y)) # label(congruence).
->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence).
->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence).
->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence).
->_s0(app(cons(x3,x4),x1),cons(x3,app(x4,x1))) # label(replacement).
->_s0(app(nil,x1),x1) # label(replacement).
->_s0(empty(cons(x3,x4)),false) # label(replacement).
->_s0(empty(nil),true) # label(replacement).
->_s0(fstsplit(0,x1),nil) # label(replacement).
->_s0(fstsplit(s(x2),cons(x3,x4)),cons(x3,fstsplit(x2,x4))) # label(replacement).
->_s0(fstsplit(s(x2),nil),nil) # label(replacement).
->_s0(head(cons(x3,x4)),x3) # label(replacement).
->_s0(length(cons(x3,x4)),s(length(x4))) # label(replacement).
->_s0(length(nil),0) # label(replacement).
->_s0(leq(0,x5),true) # label(replacement).
->_s0(leq(s(x2),0),false) # label(replacement).
->_s0(leq(s(x2),s(x5)),leq(x2,x5)) # label(replacement).
->_s0(mapf(x6,cons(x3,x4)),app(f(x6,x3),mapf(x6,x4))) # label(replacement).
->_s0(mapf(x6,nil),nil) # label(replacement).
->*_s0(empty(fstsplit(x5,x7)),false) -> ->_s0(ring(x7,x8,x9,x10,x11,x5),ring(sndsplit(x5,x7),cons(fstsplit(x5,x7),x8),x9,x10,x11,x5)) # label(replacement).
->*_s0(leq(x5,length(x9)),false) & ->*_s0(empty(fstsplit(x5,app(mapf(two,head(x8)),x9))),false) -> ->_s0(ring(x7,x8,x9,x10,x11,x5),ring(x7,tail(x8),sndsplit(x5,app(mapf(two,head(x8)),x9)),cons(fstsplit(x5,app(mapf(two,head(x8)),x9)),x10),x11,x5)) # label(replacement).
->*_s0(empty(mapf(two,head(x8))),true) -> ->_s0(ring(x7,x8,x9,x10,x11,x5),ring(x7,tail(x8),x9,x10,x11,x5)) # label(replacement).
->*_s0(leq(x5,length(x9)),true) & ->*_s0(empty(fstsplit(x5,x9)),false) -> ->_s0(ring(x7,x8,x9,x10,x11,x5),ring(x7,x8,sndsplit(x5,x9),cons(fstsplit(x5,x9),x10),x11,x5)) # label(replacement).
->*_s0(leq(x5,length(x11)),false) & ->*_s0(empty(fstsplit(x5,app(mapf(three,head(x10)),x11))),false) -> ->_s0(ring(x7,x8,x9,x10,x11,x5),ring(x7,x8,x9,tail(x10),sndsplit(x5,app(mapf(three,head(x10)),x11)),x5)) # label(replacement).
->*_s0(empty(mapf(three,head(x10))),true) -> ->_s0(ring(x7,x8,x9,x10,x11,x5),ring(x7,x8,x9,tail(x10),x11,x5)) # label(replacement).
->*_s0(leq(x5,length(x11)),true) & ->*_s0(empty(fstsplit(x5,x11)),false) -> ->_s0(ring(x7,x8,x9,x10,x11,x5),ring(x7,x8,x9,x10,sndsplit(x5,x11),x5)) # label(replacement).
->_s0(sndsplit(0,x1),x1) # label(replacement).
->_s0(sndsplit(s(x2),cons(x3,x4)),sndsplit(x2,x4)) # label(replacement).
->_s0(sndsplit(s(x2),nil),nil) # label(replacement).
->_s0(tail(cons(x3,x4)),x4) # label(replacement).
->*_s0(x,x) # label(reflexivity).
->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity).
end_of_list.
formulas(goals).
(exists x13 exists x14 (->*_s0(empty(mapf(two,head(x13))),true) & ->*_s0(empty(mapf(three,head(x14))),true))) # label(goal).
end_of_list.
============================== end of input ==========================
============================== PROCESS NON-CLAUSAL FORMULAS ==========
% Formulas that are not ordinary clauses:
1 ->_s0(x1,y) -> ->_s0(app(x1,x2),app(y,x2)) # label(congruence) # label(non_clause). [assumption].
2 ->_s0(x2,y) -> ->_s0(app(x1,x2),app(x1,y)) # label(congruence) # label(non_clause). [assumption].
3 ->_s0(x1,y) -> ->_s0(empty(x1),empty(y)) # label(congruence) # label(non_clause). [assumption].
4 ->_s0(x1,y) -> ->_s0(fstsplit(x1,x2),fstsplit(y,x2)) # label(congruence) # label(non_clause). [assumption].
5 ->_s0(x2,y) -> ->_s0(fstsplit(x1,x2),fstsplit(x1,y)) # label(congruence) # label(non_clause). [assumption].
6 ->_s0(x1,y) -> ->_s0(head(x1),head(y)) # label(congruence) # label(non_clause). [assumption].
7 ->_s0(x1,y) -> ->_s0(length(x1),length(y)) # label(congruence) # label(non_clause). [assumption].
8 ->_s0(x1,y) -> ->_s0(leq(x1,x2),leq(y,x2)) # label(congruence) # label(non_clause). [assumption].
9 ->_s0(x2,y) -> ->_s0(leq(x1,x2),leq(x1,y)) # label(congruence) # label(non_clause). [assumption].
10 ->_s0(x1,y) -> ->_s0(mapf(x1,x2),mapf(y,x2)) # label(congruence) # label(non_clause). [assumption].
11 ->_s0(x2,y) -> ->_s0(mapf(x1,x2),mapf(x1,y)) # label(congruence) # label(non_clause). [assumption].
12 ->_s0(x1,y) -> ->_s0(ring(x1,x2,x3,x4,x5,x6),ring(y,x2,x3,x4,x5,x6)) # label(congruence) # label(non_clause). [assumption].
13 ->_s0(x2,y) -> ->_s0(ring(x1,x2,x3,x4,x5,x6),ring(x1,y,x3,x4,x5,x6)) # label(congruence) # label(non_clause). [assumption].
14 ->_s0(x3,y) -> ->_s0(ring(x1,x2,x3,x4,x5,x6),ring(x1,x2,y,x4,x5,x6)) # label(congruence) # label(non_clause). [assumption].
15 ->_s0(x4,y) -> ->_s0(ring(x1,x2,x3,x4,x5,x6),ring(x1,x2,x3,y,x5,x6)) # label(congruence) # label(non_clause). [assumption].
16 ->_s0(x5,y) -> ->_s0(ring(x1,x2,x3,x4,x5,x6),ring(x1,x2,x3,x4,y,x6)) # label(congruence) # label(non_clause). [assumption].
17 ->_s0(x6,y) -> ->_s0(ring(x1,x2,x3,x4,x5,x6),ring(x1,x2,x3,x4,x5,y)) # label(congruence) # label(non_clause). [assumption].
18 ->_s0(x1,y) -> ->_s0(sndsplit(x1,x2),sndsplit(y,x2)) # label(congruence) # label(non_clause). [assumption].
19 ->_s0(x2,y) -> ->_s0(sndsplit(x1,x2),sndsplit(x1,y)) # label(congruence) # label(non_clause). [assumption].
20 ->_s0(x1,y) -> ->_s0(tail(x1),tail(y)) # label(congruence) # label(non_clause). [assumption].
21 ->_s0(x1,y) -> ->_s0(cons(x1,x2),cons(y,x2)) # label(congruence) # label(non_clause). [assumption].
22 ->_s0(x2,y) -> ->_s0(cons(x1,x2),cons(x1,y)) # label(congruence) # label(non_clause). [assumption].
23 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption].
24 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption].
25 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption].
26 ->*_s0(empty(fstsplit(x5,x7)),false) -> ->_s0(ring(x7,x8,x9,x10,x11,x5),ring(sndsplit(x5,x7),cons(fstsplit(x5,x7),x8),x9,x10,x11,x5)) # label(replacement) # label(non_clause). [assumption].
27 ->*_s0(leq(x5,length(x9)),false) & ->*_s0(empty(fstsplit(x5,app(mapf(two,head(x8)),x9))),false) -> ->_s0(ring(x7,x8,x9,x10,x11,x5),ring(x7,tail(x8),sndsplit(x5,app(mapf(two,head(x8)),x9)),cons(fstsplit(x5,app(mapf(two,head(x8)),x9)),x10),x11,x5)) # label(replacement) # label(non_clause). [assumption].
28 ->*_s0(empty(mapf(two,head(x8))),true) -> ->_s0(ring(x7,x8,x9,x10,x11,x5),ring(x7,tail(x8),x9,x10,x11,x5)) # label(replacement) # label(non_clause). [assumption].
29 ->*_s0(leq(x5,length(x9)),true) & ->*_s0(empty(fstsplit(x5,x9)),false) -> ->_s0(ring(x7,x8,x9,x10,x11,x5),ring(x7,x8,sndsplit(x5,x9),cons(fstsplit(x5,x9),x10),x11,x5)) # label(replacement) # label(non_clause). [assumption].
30 ->*_s0(leq(x5,length(x11)),false) & ->*_s0(empty(fstsplit(x5,app(mapf(three,head(x10)),x11))),false) -> ->_s0(ring(x7,x8,x9,x10,x11,x5),ring(x7,x8,x9,tail(x10),sndsplit(x5,app(mapf(three,head(x10)),x11)),x5)) # label(replacement) # label(non_clause). [assumption].
31 ->*_s0(empty(mapf(three,head(x10))),true) -> ->_s0(ring(x7,x8,x9,x10,x11,x5),ring(x7,x8,x9,tail(x10),x11,x5)) # label(replacement) # label(non_clause). [assumption].
32 ->*_s0(leq(x5,length(x11)),true) & ->*_s0(empty(fstsplit(x5,x11)),false) -> ->_s0(ring(x7,x8,x9,x10,x11,x5),ring(x7,x8,x9,x10,sndsplit(x5,x11),x5)) # label(replacement) # label(non_clause). [assumption].
33 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption].
34 (exists x13 exists x14 (->*_s0(empty(mapf(two,head(x13))),true) & ->*_s0(empty(mapf(three,head(x14))),true))) # label(goal) # label(non_clause) # label(goal). [goal].
============================== end of process non-clausal formulas ===
============================== PROCESS INITIAL CLAUSES ===============
% Clauses before input processing:
formulas(usable).
end_of_list.
formulas(sos).
-->_s0(x,y) | ->_s0(app(x,z),app(y,z)) # label(congruence). [clausify(1)].
-->_s0(x,y) | ->_s0(app(z,x),app(z,y)) # label(congruence). [clausify(2)].
-->_s0(x,y) | ->_s0(empty(x),empty(y)) # label(congruence). [clausify(3)].
-->_s0(x,y) | ->_s0(fstsplit(x,z),fstsplit(y,z)) # label(congruence). [clausify(4)].
-->_s0(x,y) | ->_s0(fstsplit(z,x),fstsplit(z,y)) # label(congruence). [clausify(5)].
-->_s0(x,y) | ->_s0(head(x),head(y)) # label(congruence). [clausify(6)].
-->_s0(x,y) | ->_s0(length(x),length(y)) # label(congruence). [clausify(7)].
-->_s0(x,y) | ->_s0(leq(x,z),leq(y,z)) # label(congruence). [clausify(8)].
-->_s0(x,y) | ->_s0(leq(z,x),leq(z,y)) # label(congruence). [clausify(9)].
-->_s0(x,y) | ->_s0(mapf(x,z),mapf(y,z)) # label(congruence). [clausify(10)].
-->_s0(x,y) | ->_s0(mapf(z,x),mapf(z,y)) # label(congruence). [clausify(11)].
-->_s0(x,y) | ->_s0(ring(x,z,u,w,v5,v6),ring(y,z,u,w,v5,v6)) # label(congruence). [clausify(12)].
-->_s0(x,y) | ->_s0(ring(z,x,u,w,v5,v6),ring(z,y,u,w,v5,v6)) # label(congruence). [clausify(13)].
-->_s0(x,y) | ->_s0(ring(z,u,x,w,v5,v6),ring(z,u,y,w,v5,v6)) # label(congruence). [clausify(14)].
-->_s0(x,y) | ->_s0(ring(z,u,w,x,v5,v6),ring(z,u,w,y,v5,v6)) # label(congruence). [clausify(15)].
-->_s0(x,y) | ->_s0(ring(z,u,w,v5,x,v6),ring(z,u,w,v5,y,v6)) # label(congruence). [clausify(16)].
-->_s0(x,y) | ->_s0(ring(z,u,w,v5,v6,x),ring(z,u,w,v5,v6,y)) # label(congruence). [clausify(17)].
-->_s0(x,y) | ->_s0(sndsplit(x,z),sndsplit(y,z)) # label(congruence). [clausify(18)].
-->_s0(x,y) | ->_s0(sndsplit(z,x),sndsplit(z,y)) # label(congruence). [clausify(19)].
-->_s0(x,y) | ->_s0(tail(x),tail(y)) # label(congruence). [clausify(20)].
-->_s0(x,y) | ->_s0(cons(x,z),cons(y,z)) # label(congruence). [clausify(21)].
-->_s0(x,y) | ->_s0(cons(z,x),cons(z,y)) # label(congruence). [clausify(22)].
-->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(23)].
-->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(24)].
-->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(25)].
->_s0(app(cons(x,y),z),cons(x,app(y,z))) # label(replacement). [assumption].
->_s0(app(nil,x),x) # label(replacement). [assumption].
->_s0(empty(cons(x,y)),false) # label(replacement). [assumption].
->_s0(empty(nil),true) # label(replacement). [assumption].
->_s0(fstsplit(0,x),nil) # label(replacement). [assumption].
->_s0(fstsplit(s(x),cons(y,z)),cons(y,fstsplit(x,z))) # label(replacement). [assumption].
->_s0(fstsplit(s(x),nil),nil) # label(replacement). [assumption].
->_s0(head(cons(x,y)),x) # label(replacement). [assumption].
->_s0(length(cons(x,y)),s(length(y))) # label(replacement). [assumption].
->_s0(length(nil),0) # label(replacement). [assumption].
->_s0(leq(0,x),true) # label(replacement). [assumption].
->_s0(leq(s(x),0),false) # label(replacement). [assumption].
->_s0(leq(s(x),s(y)),leq(x,y)) # label(replacement). [assumption].
->_s0(mapf(x,cons(y,z)),app(f(x,y),mapf(x,z))) # label(replacement). [assumption].
->_s0(mapf(x,nil),nil) # label(replacement). [assumption].
-->*_s0(empty(fstsplit(x,y)),false) | ->_s0(ring(y,z,u,w,v5,x),ring(sndsplit(x,y),cons(fstsplit(x,y),z),u,w,v5,x)) # label(replacement). [clausify(26)].
-->*_s0(leq(x,length(y)),false) | -->*_s0(empty(fstsplit(x,app(mapf(two,head(z)),y))),false) | ->_s0(ring(u,z,y,w,v5,x),ring(u,tail(z),sndsplit(x,app(mapf(two,head(z)),y)),cons(fstsplit(x,app(mapf(two,head(z)),y)),w),v5,x)) # label(replacement). [clausify(27)].
-->*_s0(empty(mapf(two,head(x))),true) | ->_s0(ring(y,x,z,u,w,v5),ring(y,tail(x),z,u,w,v5)) # label(replacement). [clausify(28)].
-->*_s0(leq(x,length(y)),true) | -->*_s0(empty(fstsplit(x,y)),false) | ->_s0(ring(z,u,y,w,v5,x),ring(z,u,sndsplit(x,y),cons(fstsplit(x,y),w),v5,x)) # label(replacement). [clausify(29)].
-->*_s0(leq(x,length(y)),false) | -->*_s0(empty(fstsplit(x,app(mapf(three,head(z)),y))),false) | ->_s0(ring(u,w,v5,z,y,x),ring(u,w,v5,tail(z),sndsplit(x,app(mapf(three,head(z)),y)),x)) # label(replacement). [clausify(30)].
-->*_s0(empty(mapf(three,head(x))),true) | ->_s0(ring(y,z,u,x,w,v5),ring(y,z,u,tail(x),w,v5)) # label(replacement). [clausify(31)].
-->*_s0(leq(x,length(y)),true) | -->*_s0(empty(fstsplit(x,y)),false) | ->_s0(ring(z,u,w,v5,y,x),ring(z,u,w,v5,sndsplit(x,y),x)) # label(replacement). [clausify(32)].
->_s0(sndsplit(0,x),x) # label(replacement). [assumption].
->_s0(sndsplit(s(x),cons(y,z)),sndsplit(x,z)) # label(replacement). [assumption].
->_s0(sndsplit(s(x),nil),nil) # label(replacement). [assumption].
->_s0(tail(cons(x,y)),y) # label(replacement). [assumption].
->*_s0(x,x) # label(reflexivity). [assumption].
-->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(33)].
-->*_s0(empty(mapf(two,head(x))),true) | -->*_s0(empty(mapf(three,head(y))),true) # label(goal). [deny(34)].
end_of_list.
formulas(demodulators).
end_of_list.
============================== PREDICATE ELIMINATION =================
No predicates eliminated.
============================== end predicate elimination =============
Auto_denials:
% copying label goal to answer in negative clause
Term ordering decisions:
Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]).
Function symbol precedence: function_order([ nil, false, true, 0, two, three, cons, fstsplit, mapf, sndsplit, app, leq, f, empty, s, head, length, tail, ring ]).
After inverse_order: (no changes).
Unfolding symbols: (none).
Auto_inference settings:
% set(neg_binary_resolution). % (HNE depth_diff=-26)
% clear(ordered_res). % (HNE depth_diff=-26)
% set(ur_resolution). % (HNE depth_diff=-26)
% set(ur_resolution) -> set(pos_ur_resolution).
% set(ur_resolution) -> set(neg_ur_resolution).
Auto_process settings:
% set(unit_deletion). % (Horn set with negative nonunits)
kept: 35 -->_s0(x,y) | ->_s0(app(x,z),app(y,z)) # label(congruence). [clausify(1)].
kept: 36 -->_s0(x,y) | ->_s0(app(z,x),app(z,y)) # label(congruence). [clausify(2)].
kept: 37 -->_s0(x,y) | ->_s0(empty(x),empty(y)) # label(congruence). [clausify(3)].
kept: 38 -->_s0(x,y) | ->_s0(fstsplit(x,z),fstsplit(y,z)) # label(congruence). [clausify(4)].
kept: 39 -->_s0(x,y) | ->_s0(fstsplit(z,x),fstsplit(z,y)) # label(congruence). [clausify(5)].
kept: 40 -->_s0(x,y) | ->_s0(head(x),head(y)) # label(congruence). [clausify(6)].
kept: 41 -->_s0(x,y) | ->_s0(length(x),length(y)) # label(congruence). [clausify(7)].
kept: 42 -->_s0(x,y) | ->_s0(leq(x,z),leq(y,z)) # label(congruence). [clausify(8)].
kept: 43 -->_s0(x,y) | ->_s0(leq(z,x),leq(z,y)) # label(congruence). [clausify(9)].
kept: 44 -->_s0(x,y) | ->_s0(mapf(x,z),mapf(y,z)) # label(congruence). [clausify(10)].
kept: 45 -->_s0(x,y) | ->_s0(mapf(z,x),mapf(z,y)) # label(congruence). [clausify(11)].
kept: 46 -->_s0(x,y) | ->_s0(ring(x,z,u,w,v5,v6),ring(y,z,u,w,v5,v6)) # label(congruence). [clausify(12)].
kept: 47 -->_s0(x,y) | ->_s0(ring(z,x,u,w,v5,v6),ring(z,y,u,w,v5,v6)) # label(congruence). [clausify(13)].
kept: 48 -->_s0(x,y) | ->_s0(ring(z,u,x,w,v5,v6),ring(z,u,y,w,v5,v6)) # label(congruence). [clausify(14)].
kept: 49 -->_s0(x,y) | ->_s0(ring(z,u,w,x,v5,v6),ring(z,u,w,y,v5,v6)) # label(congruence). [clausify(15)].
kept: 50 -->_s0(x,y) | ->_s0(ring(z,u,w,v5,x,v6),ring(z,u,w,v5,y,v6)) # label(congruence). [clausify(16)].
kept: 51 -->_s0(x,y) | ->_s0(ring(z,u,w,v5,v6,x),ring(z,u,w,v5,v6,y)) # label(congruence). [clausify(17)].
kept: 52 -->_s0(x,y) | ->_s0(sndsplit(x,z),sndsplit(y,z)) # label(congruence). [clausify(18)].
kept: 53 -->_s0(x,y) | ->_s0(sndsplit(z,x),sndsplit(z,y)) # label(congruence). [clausify(19)].
kept: 54 -->_s0(x,y) | ->_s0(tail(x),tail(y)) # label(congruence). [clausify(20)].
kept: 55 -->_s0(x,y) | ->_s0(cons(x,z),cons(y,z)) # label(congruence). [clausify(21)].
kept: 56 -->_s0(x,y) | ->_s0(cons(z,x),cons(z,y)) # label(congruence). [clausify(22)].
kept: 57 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(23)].
kept: 58 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(24)].
kept: 59 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(25)].
kept: 60 ->_s0(app(cons(x,y),z),cons(x,app(y,z))) # label(replacement). [assumption].
kept: 61 ->_s0(app(nil,x),x) # label(replacement). [assumption].
kept: 62 ->_s0(empty(cons(x,y)),false) # label(replacement). [assumption].
kept: 63 ->_s0(empty(nil),true) # label(replacement). [assumption].
kept: 64 ->_s0(fstsplit(0,x),nil) # label(replacement). [assumption].
kept: 65 ->_s0(fstsplit(s(x),cons(y,z)),cons(y,fstsplit(x,z))) # label(replacement). [assumption].
kept: 66 ->_s0(fstsplit(s(x),nil),nil) # label(replacement). [assumption].
kept: 67 ->_s0(head(cons(x,y)),x) # label(replacement). [assumption].
kept: 68 ->_s0(length(cons(x,y)),s(length(y))) # label(replacement). [assumption].
kept: 69 ->_s0(length(nil),0) # label(replacement). [assumption].
kept: 70 ->_s0(leq(0,x),true) # label(replacement). [assumption].
kept: 71 ->_s0(leq(s(x),0),false) # label(replacement). [assumption].
kept: 72 ->_s0(leq(s(x),s(y)),leq(x,y)) # label(replacement). [assumption].
kept: 73 ->_s0(mapf(x,cons(y,z)),app(f(x,y),mapf(x,z))) # label(replacement). [assumption].
kept: 74 ->_s0(mapf(x,nil),nil) # label(replacement). [assumption].
kept: 75 -->*_s0(empty(fstsplit(x,y)),false) | ->_s0(ring(y,z,u,w,v5,x),ring(sndsplit(x,y),cons(fstsplit(x,y),z),u,w,v5,x)) # label(replacement). [clausify(26)].
kept: 76 -->*_s0(leq(x,length(y)),false) | -->*_s0(empty(fstsplit(x,app(mapf(two,head(z)),y))),false) | ->_s0(ring(u,z,y,w,v5,x),ring(u,tail(z),sndsplit(x,app(mapf(two,head(z)),y)),cons(fstsplit(x,app(mapf(two,head(z)),y)),w),v5,x)) # label(replacement). [clausify(27)].
kept: 77 -->*_s0(empty(mapf(two,head(x))),true) | ->_s0(ring(y,x,z,u,w,v5),ring(y,tail(x),z,u,w,v5)) # label(replacement). [clausify(28)].
kept: 78 -->*_s0(leq(x,length(y)),true) | -->*_s0(empty(fstsplit(x,y)),false) | ->_s0(ring(z,u,y,w,v5,x),ring(z,u,sndsplit(x,y),cons(fstsplit(x,y),w),v5,x)) # label(replacement). [clausify(29)].
kept: 79 -->*_s0(leq(x,length(y)),false) | -->*_s0(empty(fstsplit(x,app(mapf(three,head(z)),y))),false) | ->_s0(ring(u,w,v5,z,y,x),ring(u,w,v5,tail(z),sndsplit(x,app(mapf(three,head(z)),y)),x)) # label(replacement). [clausify(30)].
kept: 80 -->*_s0(empty(mapf(three,head(x))),true) | ->_s0(ring(y,z,u,x,w,v5),ring(y,z,u,tail(x),w,v5)) # label(replacement). [clausify(31)].
kept: 81 -->*_s0(leq(x,length(y)),true) | -->*_s0(empty(fstsplit(x,y)),false) | ->_s0(ring(z,u,w,v5,y,x),ring(z,u,w,v5,sndsplit(x,y),x)) # label(replacement). [clausify(32)].
kept: 82 ->_s0(sndsplit(0,x),x) # label(replacement). [assumption].
kept: 83 ->_s0(sndsplit(s(x),cons(y,z)),sndsplit(x,z)) # label(replacement). [assumption].
kept: 84 ->_s0(sndsplit(s(x),nil),nil) # label(replacement). [assumption].
kept: 85 ->_s0(tail(cons(x,y)),y) # label(replacement). [assumption].
kept: 86 ->*_s0(x,x) # label(reflexivity). [assumption].
kept: 87 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(33)].
kept: 88 -->*_s0(empty(mapf(two,head(x))),true) | -->*_s0(empty(mapf(three,head(y))),true) # label(goal) # answer(goal). [deny(34)].
============================== end of process initial clauses ========
============================== CLAUSES FOR SEARCH ====================
% Clauses after input processing:
formulas(usable).
end_of_list.
formulas(sos).
35 -->_s0(x,y) | ->_s0(app(x,z),app(y,z)) # label(congruence). [clausify(1)].
36 -->_s0(x,y) | ->_s0(app(z,x),app(z,y)) # label(congruence). [clausify(2)].
37 -->_s0(x,y) | ->_s0(empty(x),empty(y)) # label(congruence). [clausify(3)].
38 -->_s0(x,y) | ->_s0(fstsplit(x,z),fstsplit(y,z)) # label(congruence). [clausify(4)].
39 -->_s0(x,y) | ->_s0(fstsplit(z,x),fstsplit(z,y)) # label(congruence). [clausify(5)].
40 -->_s0(x,y) | ->_s0(head(x),head(y)) # label(congruence). [clausify(6)].
41 -->_s0(x,y) | ->_s0(length(x),length(y)) # label(congruence). [clausify(7)].
42 -->_s0(x,y) | ->_s0(leq(x,z),leq(y,z)) # label(congruence). [clausify(8)].
43 -->_s0(x,y) | ->_s0(leq(z,x),leq(z,y)) # label(congruence). [clausify(9)].
44 -->_s0(x,y) | ->_s0(mapf(x,z),mapf(y,z)) # label(congruence). [clausify(10)].
45 -->_s0(x,y) | ->_s0(mapf(z,x),mapf(z,y)) # label(congruence). [clausify(11)].
46 -->_s0(x,y) | ->_s0(ring(x,z,u,w,v5,v6),ring(y,z,u,w,v5,v6)) # label(congruence). [clausify(12)].
47 -->_s0(x,y) | ->_s0(ring(z,x,u,w,v5,v6),ring(z,y,u,w,v5,v6)) # label(congruence). [clausify(13)].
48 -->_s0(x,y) | ->_s0(ring(z,u,x,w,v5,v6),ring(z,u,y,w,v5,v6)) # label(congruence). [clausify(14)].
49 -->_s0(x,y) | ->_s0(ring(z,u,w,x,v5,v6),ring(z,u,w,y,v5,v6)) # label(congruence). [clausify(15)].
50 -->_s0(x,y) | ->_s0(ring(z,u,w,v5,x,v6),ring(z,u,w,v5,y,v6)) # label(congruence). [clausify(16)].
51 -->_s0(x,y) | ->_s0(ring(z,u,w,v5,v6,x),ring(z,u,w,v5,v6,y)) # label(congruence). [clausify(17)].
52 -->_s0(x,y) | ->_s0(sndsplit(x,z),sndsplit(y,z)) # label(congruence). [clausify(18)].
53 -->_s0(x,y) | ->_s0(sndsplit(z,x),sndsplit(z,y)) # label(congruence). [clausify(19)].
54 -->_s0(x,y) | ->_s0(tail(x),tail(y)) # label(congruence). [clausify(20)].
55 -->_s0(x,y) | ->_s0(cons(x,z),cons(y,z)) # label(congruence). [clausify(21)].
56 -->_s0(x,y) | ->_s0(cons(z,x),cons(z,y)) # label(congruence). [clausify(22)].
57 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(23)].
58 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(24)].
59 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(25)].
60 ->_s0(app(cons(x,y),z),cons(x,app(y,z))) # label(replacement). [assumption].
61 ->_s0(app(nil,x),x) # label(replacement). [assumption].
62 ->_s0(empty(cons(x,y)),false) # label(replacement). [assumption].
63 ->_s0(empty(nil),true) # label(replacement). [assumption].
64 ->_s0(fstsplit(0,x),nil) # label(replacement). [assumption].
65 ->_s0(fstsplit(s(x),cons(y,z)),cons(y,fstsplit(x,z))) # label(replacement). [assumption].
66 ->_s0(fstsplit(s(x),nil),nil) # label(replacement). [assumption].
67 ->_s0(head(cons(x,y)),x) # label(replacement). [assumption].
68 ->_s0(length(cons(x,y)),s(length(y))) # label(replacement). [assumption].
69 ->_s0(length(nil),0) # label(replacement). [assumption].
70 ->_s0(leq(0,x),true) # label(replacement). [assumption].
71 ->_s0(leq(s(x),0),false) # label(replacement). [assumption].
72 ->_s0(leq(s(x),s(y)),leq(x,y)) # label(replacement). [assumption].
73 ->_s0(mapf(x,cons(y,z)),app(f(x,y),mapf(x,z))) # label(replacement). [assumption].
74 ->_s0(mapf(x,nil),nil) # label(replacement). [assumption].
75 -->*_s0(empty(fstsplit(x,y)),false) | ->_s0(ring(y,z,u,w,v5,x),ring(sndsplit(x,y),cons(fstsplit(x,y),z),u,w,v5,x)) # label(replacement). [clausify(26)].
76 -->*_s0(leq(x,length(y)),false) | -->*_s0(empty(fstsplit(x,app(mapf(two,head(z)),y))),false) | ->_s0(ring(u,z,y,w,v5,x),ring(u,tail(z),sndsplit(x,app(mapf(two,head(z)),y)),cons(fstsplit(x,app(mapf(two,head(z)),y)),w),v5,x)) # label(replacement). [clausify(27)].
77 -->*_s0(empty(mapf(two,head(x))),true) | ->_s0(ring(y,x,z,u,w,v5),ring(y,tail(x),z,u,w,v5)) # label(replacement). [clausify(28)].
78 -->*_s0(leq(x,length(y)),true) | -->*_s0(empty(fstsplit(x,y)),false) | ->_s0(ring(z,u,y,w,v5,x),ring(z,u,sndsplit(x,y),cons(fstsplit(x,y),w),v5,x)) # label(replacement). [clausify(29)].
79 -->*_s0(leq(x,length(y)),false) | -->*_s0(empty(fstsplit(x,app(mapf(three,head(z)),y))),false) | ->_s0(ring(u,w,v5,z,y,x),ring(u,w,v5,tail(z),sndsplit(x,app(mapf(three,head(z)),y)),x)) # label(replacement). [clausify(30)].
80 -->*_s0(empty(mapf(three,head(x))),true) | ->_s0(ring(y,z,u,x,w,v5),ring(y,z,u,tail(x),w,v5)) # label(replacement). [clausify(31)].
81 -->*_s0(leq(x,length(y)),true) | -->*_s0(empty(fstsplit(x,y)),false) | ->_s0(ring(z,u,w,v5,y,x),ring(z,u,w,v5,sndsplit(x,y),x)) # label(replacement). [clausify(32)].
82 ->_s0(sndsplit(0,x),x) # label(replacement). [assumption].
83 ->_s0(sndsplit(s(x),cons(y,z)),sndsplit(x,z)) # label(replacement). [assumption].
84 ->_s0(sndsplit(s(x),nil),nil) # label(replacement). [assumption].
85 ->_s0(tail(cons(x,y)),y) # label(replacement). [assumption].
86 ->*_s0(x,x) # label(reflexivity). [assumption].
87 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(33)].
88 -->*_s0(empty(mapf(two,head(x))),true) | -->*_s0(empty(mapf(three,head(y))),true) # label(goal) # answer(goal). [deny(34)].
end_of_list.
formulas(demodulators).
end_of_list.
============================== end of clauses for search =============
============================== SEARCH ================================
% Starting search at 0.02 seconds.
given #1 (I,wt=10): 35 -->_s0(x,y) | ->_s0(app(x,z),app(y,z)) # label(congruence). [clausify(1)].
given #2 (I,wt=10): 36 -->_s0(x,y) | ->_s0(app(z,x),app(z,y)) # label(congruence). [clausify(2)].
given #3 (I,wt=8): 37 -->_s0(x,y) | ->_s0(empty(x),empty(y)) # label(congruence). [clausify(3)].
given #4 (I,wt=10): 38 -->_s0(x,y) | ->_s0(fstsplit(x,z),fstsplit(y,z)) # label(congruence). [clausify(4)].
given #5 (I,wt=10): 39 -->_s0(x,y) | ->_s0(fstsplit(z,x),fstsplit(z,y)) # label(congruence). [clausify(5)].
given #6 (I,wt=8): 40 -->_s0(x,y) | ->_s0(head(x),head(y)) # label(congruence). [clausify(6)].
given #7 (I,wt=8): 41 -->_s0(x,y) | ->_s0(length(x),length(y)) # label(congruence). [clausify(7)].
given #8 (I,wt=10): 42 -->_s0(x,y) | ->_s0(leq(x,z),leq(y,z)) # label(congruence). [clausify(8)].
given #9 (I,wt=10): 43 -->_s0(x,y) | ->_s0(leq(z,x),leq(z,y)) # label(congruence). [clausify(9)].
given #10 (I,wt=10): 44 -->_s0(x,y) | ->_s0(mapf(x,z),mapf(y,z)) # label(congruence). [clausify(10)].
given #11 (I,wt=10): 45 -->_s0(x,y) | ->_s0(mapf(z,x),mapf(z,y)) # label(congruence). [clausify(11)].
given #12 (I,wt=18): 46 -->_s0(x,y) | ->_s0(ring(x,z,u,w,v5,v6),ring(y,z,u,w,v5,v6)) # label(congruence). [clausify(12)].
given #13 (I,wt=18): 47 -->_s0(x,y) | ->_s0(ring(z,x,u,w,v5,v6),ring(z,y,u,w,v5,v6)) # label(congruence). [clausify(13)].
given #14 (I,wt=18): 48 -->_s0(x,y) | ->_s0(ring(z,u,x,w,v5,v6),ring(z,u,y,w,v5,v6)) # label(congruence). [clausify(14)].
given #15 (I,wt=18): 49 -->_s0(x,y) | ->_s0(ring(z,u,w,x,v5,v6),ring(z,u,w,y,v5,v6)) # label(congruence). [clausify(15)].
given #16 (I,wt=18): 50 -->_s0(x,y) | ->_s0(ring(z,u,w,v5,x,v6),ring(z,u,w,v5,y,v6)) # label(congruence). [clausify(16)].
given #17 (I,wt=18): 51 -->_s0(x,y) | ->_s0(ring(z,u,w,v5,v6,x),ring(z,u,w,v5,v6,y)) # label(congruence). [clausify(17)].
given #18 (I,wt=10): 52 -->_s0(x,y) | ->_s0(sndsplit(x,z),sndsplit(y,z)) # label(congruence). [clausify(18)].
given #19 (I,wt=10): 53 -->_s0(x,y) | ->_s0(sndsplit(z,x),sndsplit(z,y)) # label(congruence). [clausify(19)].
given #20 (I,wt=8): 54 -->_s0(x,y) | ->_s0(tail(x),tail(y)) # label(congruence). [clausify(20)].
given #21 (I,wt=10): 55 -->_s0(x,y) | ->_s0(cons(x,z),cons(y,z)) # label(congruence). [clausify(21)].
given #22 (I,wt=10): 56 -->_s0(x,y) | ->_s0(cons(z,x),cons(z,y)) # label(congruence). [clausify(22)].
given #23 (I,wt=10): 57 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(23)].
given #24 (I,wt=10): 58 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(24)].
given #25 (I,wt=8): 59 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(25)].
given #26 (I,wt=11): 60 ->_s0(app(cons(x,y),z),cons(x,app(y,z))) # label(replacement). [assumption].
given #27 (I,wt=5): 61 ->_s0(app(nil,x),x) # label(replacement). [assumption].
given #28 (I,wt=6): 62 ->_s0(empty(cons(x,y)),false) # label(replacement). [assumption].
given #29 (I,wt=4): 63 ->_s0(empty(nil),true) # label(replacement). [assumption].
given #30 (I,wt=5): 64 ->_s0(fstsplit(0,x),nil) # label(replacement). [assumption].
given #31 (I,wt=12): 65 ->_s0(fstsplit(s(x),cons(y,z)),cons(y,fstsplit(x,z))) # label(replacement). [assumption].
given #32 (I,wt=6): 66 ->_s0(fstsplit(s(x),nil),nil) # label(replacement). [assumption].
given #33 (I,wt=6): 67 ->_s0(head(cons(x,y)),x) # label(replacement). [assumption].
given #34 (I,wt=8): 68 ->_s0(length(cons(x,y)),s(length(y))) # label(replacement). [assumption].
given #35 (I,wt=4): 69 ->_s0(length(nil),0) # label(replacement). [assumption].
given #36 (I,wt=5): 70 ->_s0(leq(0,x),true) # label(replacement). [assumption].
given #37 (I,wt=6): 71 ->_s0(leq(s(x),0),false) # label(replacement). [assumption].
given #38 (I,wt=9): 72 ->_s0(leq(s(x),s(y)),leq(x,y)) # label(replacement). [assumption].
given #39 (I,wt=13): 73 ->_s0(mapf(x,cons(y,z)),app(f(x,y),mapf(x,z))) # label(replacement). [assumption].
given #40 (I,wt=5): 74 ->_s0(mapf(x,nil),nil) # label(replacement). [assumption].
given #41 (I,wt=27): 75 -->*_s0(empty(fstsplit(x,y)),false) | ->_s0(ring(y,z,u,w,v5,x),ring(sndsplit(x,y),cons(fstsplit(x,y),z),u,w,v5,x)) # label(replacement). [clausify(26)].
given #42 (I,wt=49): 76 -->*_s0(leq(x,length(y)),false) | -->*_s0(empty(fstsplit(x,app(mapf(two,head(z)),y))),false) | ->_s0(ring(u,z,y,w,v5,x),ring(u,tail(z),sndsplit(x,app(mapf(two,head(z)),y)),cons(fstsplit(x,app(mapf(two,head(z)),y)),w),v5,x)) # label(replacement). [clausify(27)].
given #43 (I,wt=23): 77 -->*_s0(empty(mapf(two,head(x))),true) | ->_s0(ring(y,x,z,u,w,v5),ring(y,tail(x),z,u,w,v5)) # label(replacement). [clausify(28)].
given #44 (I,wt=33): 78 -->*_s0(leq(x,length(y)),true) | -->*_s0(empty(fstsplit(x,y)),false) | ->_s0(ring(z,u,y,w,v5,x),ring(z,u,sndsplit(x,y),cons(fstsplit(x,y),w),v5,x)) # label(replacement). [clausify(29)].
given #45 (I,wt=40): 79 -->*_s0(leq(x,length(y)),false) | -->*_s0(empty(fstsplit(x,app(mapf(three,head(z)),y))),false) | ->_s0(ring(u,w,v5,z,y,x),ring(u,w,v5,tail(z),sndsplit(x,app(mapf(three,head(z)),y)),x)) # label(replacement). [clausify(30)].
given #46 (I,wt=23): 80 -->*_s0(empty(mapf(three,head(x))),true) | ->_s0(ring(y,z,u,x,w,v5),ring(y,z,u,tail(x),w,v5)) # label(replacement). [clausify(31)].
given #47 (I,wt=29): 81 -->*_s0(leq(x,length(y)),true) | -->*_s0(empty(fstsplit(x,y)),false) | ->_s0(ring(z,u,w,v5,y,x),ring(z,u,w,v5,sndsplit(x,y),x)) # label(replacement). [clausify(32)].
given #48 (I,wt=5): 82 ->_s0(sndsplit(0,x),x) # label(replacement). [assumption].
given #49 (I,wt=10): 83 ->_s0(sndsplit(s(x),cons(y,z)),sndsplit(x,z)) # label(replacement). [assumption].
given #50 (I,wt=6): 84 ->_s0(sndsplit(s(x),nil),nil) # label(replacement). [assumption].
given #51 (I,wt=6): 85 ->_s0(tail(cons(x,y)),y) # label(replacement). [assumption].
given #52 (I,wt=3): 86 ->*_s0(x,x) # label(reflexivity). [assumption].
given #53 (I,wt=9): 87 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(33)].
given #54 (I,wt=14): 88 -->*_s0(empty(mapf(two,head(x))),true) | -->*_s0(empty(mapf(three,head(y))),true) # label(goal) # answer(goal). [deny(34)].
given #55 (A,wt=13): 89 ->_s0(s(app(cons(x,y),z)),s(cons(x,app(y,z)))). [ur(59,a,60,a)].
given #56 (F,wt=17): 583 -->*_s0(empty(mapf(three,head(x))),true) | -->_s0(empty(mapf(two,head(y))),z) | -->*_s0(z,true) # answer(goal). [resolve(88,a,87,c)].
given #57 (F,wt=14): 614 -->*_s0(empty(mapf(three,head(x))),true) | -->_s0(empty(mapf(two,head(y))),true) # answer(goal). [resolve(583,c,86,a)].
given #58 (F,wt=17): 584 -->*_s0(empty(mapf(two,head(x))),true) | -->_s0(empty(mapf(three,head(y))),z) | -->*_s0(z,true) # answer(goal). [resolve(88,b,87,c)].
given #59 (F,wt=14): 618 -->*_s0(empty(mapf(two,head(x))),true) | -->_s0(empty(mapf(three,head(y))),true) # answer(goal). [resolve(584,c,86,a)].
given #60 (T,wt=4): 573 ->*_s0(length(nil),0). [ur(87,a,69,a,b,86,a)].
given #61 (T,wt=4): 579 ->*_s0(empty(nil),true). [ur(87,a,63,a,b,86,a)].
given #62 (T,wt=5): 567 ->*_s0(sndsplit(0,x),x). [ur(87,a,82,a,b,86,a)].
given #63 (T,wt=5): 568 ->*_s0(mapf(x,nil),nil). [ur(87,a,74,a,b,86,a)].
given #64 (A,wt=15): 90 ->_s0(f(x,app(cons(y,z),u)),f(x,cons(y,app(z,u)))). [ur(58,a,60,a)].
given #65 (F,wt=15): 624 -->*_s0(empty(mapf(two,head(x))),true) | -->_s0(empty(mapf(three,head(y))),empty(nil)) # answer(goal). [resolve(579,a,584,c)].
given #66 (F,wt=13): 668 -->*_s0(empty(mapf(two,head(x))),true) | -->_s0(mapf(three,head(y)),nil) # answer(goal). [resolve(624,b,37,b)].
given #67 (F,wt=15): 625 -->*_s0(empty(mapf(three,head(x))),true) | -->_s0(empty(mapf(two,head(y))),empty(nil)) # answer(goal). [resolve(579,a,583,c)].
given #68 (F,wt=13): 671 -->*_s0(empty(mapf(three,head(x))),true) | -->_s0(mapf(two,head(y)),nil) # answer(goal). [resolve(625,b,37,b)].
given #69 (T,wt=5): 572 ->*_s0(leq(0,x),true). [ur(87,a,70,a,b,86,a)].
given #70 (T,wt=5): 578 ->*_s0(fstsplit(0,x),nil). [ur(87,a,64,a,b,86,a)].
given #71 (T,wt=5): 581 ->*_s0(app(nil,x),x). [ur(87,a,61,a,b,86,a)].
given #72 (T,wt=6): 164 ->_s0(s(empty(nil)),s(true)). [ur(59,a,63,a)].
given #73 (A,wt=15): 91 ->_s0(f(app(cons(x,y),z),u),f(cons(x,app(y,z)),u)). [ur(57,a,60,a)].
given #74 (F,wt=16): 630 -->*_s0(empty(mapf(two,head(x))),true) | -->_s0(empty(mapf(three,head(y))),sndsplit(0,true)) # answer(goal). [resolve(567,a,584,c)].
given #75 (F,wt=16): 631 -->*_s0(empty(mapf(three,head(x))),true) | -->_s0(empty(mapf(two,head(y))),sndsplit(0,true)) # answer(goal). [resolve(567,a,583,c)].
given #76 (F,wt=16): 669 -->_s0(mapf(three,head(x)),nil) | -->_s0(empty(mapf(two,head(y))),z) | -->*_s0(z,true) # answer(goal). [resolve(668,a,87,c)].
given #77 (F,wt=13): 750 -->_s0(mapf(three,head(x)),nil) | -->_s0(empty(mapf(two,head(y))),true) # answer(goal). [resolve(669,c,86,a)].
given #78 (T,wt=6): 169 ->_s0(tail(empty(nil)),tail(true)). [ur(54,a,63,a)].
given #79 (T,wt=6): 182 ->_s0(length(empty(nil)),length(true)). [ur(41,a,63,a)].
given #80 (T,wt=6): 183 ->_s0(head(empty(nil)),head(true)). [ur(40,a,63,a)].
given #81 (T,wt=6): 186 ->_s0(empty(empty(nil)),empty(true)). [ur(37,a,63,a)].
given #82 (A,wt=15): 92 ->_s0(cons(x,app(cons(y,z),u)),cons(x,cons(y,app(z,u)))). [ur(56,a,60,a)].
given #83 (F,wt=14): 746 -->_s0(mapf(three,head(x)),nil) | -->_s0(empty(mapf(two,head(y))),empty(nil)) # answer(goal). [resolve(669,c,579,a)].
given #84 (F,wt=12): 881 -->_s0(mapf(three,head(x)),nil) | -->_s0(mapf(two,head(y)),nil) # answer(goal). [resolve(746,b,37,b)].
given #85 (F,wt=15): 745 -->_s0(mapf(three,head(x)),nil) | -->_s0(empty(mapf(two,head(y))),app(nil,true)) # answer(goal). [resolve(669,c,581,a)].
given #86 (F,wt=15): 747 -->_s0(mapf(three,head(x)),nil) | -->_s0(empty(mapf(two,head(y))),leq(0,z)) # answer(goal). [resolve(669,c,572,a)].
given #87 (T,wt=6): 314 ->_s0(s(length(nil)),s(0)). [ur(59,a,69,a)].
given #88 (T,wt=6): 319 ->_s0(tail(length(nil)),tail(0)). [ur(54,a,69,a)].
given #89 (T,wt=6): 332 ->_s0(length(length(nil)),length(0)). [ur(41,a,69,a)].
given #90 (T,wt=6): 333 ->_s0(head(length(nil)),head(0)). [ur(40,a,69,a)].
given #91 (A,wt=15): 93 ->_s0(cons(app(cons(x,y),z),u),cons(cons(x,app(y,z)),u)). [ur(55,a,60,a)].
given #92 (F,wt=15): 748 -->_s0(mapf(three,head(x)),nil) | -->_s0(empty(mapf(two,head(y))),sndsplit(0,true)) # answer(goal). [resolve(669,c,567,a)].
given #93 (F,wt=16): 672 -->_s0(mapf(two,head(x)),nil) | -->_s0(empty(mapf(three,head(y))),z) | -->*_s0(z,true) # answer(goal). [resolve(671,a,87,c)].
given #94 (F,wt=13): 1018 -->_s0(mapf(two,head(x)),nil) | -->_s0(empty(mapf(three,head(y))),true) # answer(goal). [resolve(672,c,86,a)].
given #95 (F,wt=14): 1014 -->_s0(mapf(two,head(x)),nil) | -->_s0(empty(mapf(three,head(y))),empty(nil)) # answer(goal). [resolve(672,c,579,a)].
given #96 (T,wt=6): 336 ->_s0(empty(length(nil)),empty(0)). [ur(37,a,69,a)].
given #97 (T,wt=6): 564 ->*_s0(tail(cons(x,y)),y). [ur(87,a,85,a,b,86,a)].
given #98 (T,wt=6): 565 ->*_s0(sndsplit(s(x),nil),nil). [ur(87,a,84,a,b,86,a)].
given #99 (T,wt=6): 571 ->*_s0(leq(s(x),0),false). [ur(87,a,71,a,b,86,a)].
given #100 (A,wt=13): 94 ->_s0(tail(app(cons(x,y),z)),tail(cons(x,app(y,z)))). [ur(54,a,60,a)].
given #101 (F,wt=15): 1013 -->_s0(mapf(two,head(x)),nil) | -->_s0(empty(mapf(three,head(y))),app(nil,true)) # answer(goal). [resolve(672,c,581,a)].
given #102 (F,wt=15): 1015 -->_s0(mapf(two,head(x)),nil) | -->_s0(empty(mapf(three,head(y))),leq(0,z)) # answer(goal). [resolve(672,c,572,a)].
given #103 (F,wt=15): 1016 -->_s0(mapf(two,head(x)),nil) | -->_s0(empty(mapf(three,head(y))),sndsplit(0,true)) # answer(goal). [resolve(672,c,567,a)].
given #104 (F,wt=16): 673 -->*_s0(empty(mapf(two,head(x))),true) | -->_s0(empty(mapf(three,head(y))),leq(0,z)) # answer(goal). [resolve(572,a,584,c)].
given #105 (T,wt=6): 575 ->*_s0(head(cons(x,y)),x). [ur(87,a,67,a,b,86,a)].
given #106 (T,wt=6): 576 ->*_s0(fstsplit(s(x),nil),nil). [ur(87,a,66,a,b,86,a)].
given #107 (T,wt=6): 580 ->*_s0(empty(cons(x,y)),false). [ur(87,a,62,a,b,86,a)].
given #108 (T,wt=6): 621 ->*_s0(sndsplit(0,length(nil)),0). [ur(87,a,82,a,b,573,a)].
given #109 (A,wt=15): 95 ->_s0(sndsplit(x,app(cons(y,z),u)),sndsplit(x,cons(y,app(z,u)))). [ur(53,a,60,a)].
given #110 (F,wt=16): 674 -->*_s0(empty(mapf(three,head(x))),true) | -->_s0(empty(mapf(two,head(y))),leq(0,z)) # answer(goal). [resolve(572,a,583,c)].
given #111 (F,wt=16): 684 -->*_s0(empty(mapf(two,head(x))),true) | -->_s0(empty(mapf(three,head(y))),app(nil,true)) # answer(goal). [resolve(581,a,584,c)].
given #112 (F,wt=16): 685 -->*_s0(empty(mapf(three,head(x))),true) | -->_s0(empty(mapf(two,head(y))),app(nil,true)) # answer(goal). [resolve(581,a,583,c)].
given #113 (F,wt=16): 744 -->_s0(mapf(three,head(x)),nil) | -->*_s0(empty(y),true) | -->_s0(mapf(two,head(z)),y) # answer(goal). [resolve(669,b,37,b)].
given #114 (T,wt=6): 623 ->*_s0(app(nil,length(nil)),0). [ur(87,a,61,a,b,573,a)].
given #115 (T,wt=6): 627 ->*_s0(sndsplit(0,empty(nil)),true). [ur(87,a,82,a,b,579,a)].
given #116 (T,wt=6): 629 ->*_s0(app(nil,empty(nil)),true). [ur(87,a,61,a,b,579,a)].
given #117 (T,wt=6): 690 ->*_s0(s(empty(nil)),s(true)). [ur(87,a,164,a,b,86,a)].
given #118 (A,wt=15): 96 ->_s0(sndsplit(app(cons(x,y),z),u),sndsplit(cons(x,app(y,z)),u)). [ur(52,a,60,a)].
given #119 (F,wt=16): 1012 -->_s0(mapf(two,head(x)),nil) | -->*_s0(empty(y),true) | -->_s0(mapf(three,head(z)),y) # answer(goal). [resolve(672,b,37,b)].
given #120 (F,wt=16): 1045 -->_s0(mapf(two,head(x)),nil) | -->_s0(empty(mapf(three,head(y))),tail(cons(z,true))) # answer(goal). [resolve(564,a,672,c)].
given #121 (F,wt=16): 1046 -->_s0(mapf(three,head(x)),nil) | -->_s0(empty(mapf(two,head(y))),tail(cons(z,true))) # answer(goal). [resolve(564,a,669,c)].
given #122 (F,wt=16): 1091 -->_s0(mapf(two,head(x)),nil) | -->_s0(empty(mapf(three,head(y))),head(cons(true,z))) # answer(goal). [resolve(575,a,672,c)].
given #123 (T,wt=6): 751 ->*_s0(tail(empty(nil)),tail(true)). [ur(87,a,169,a,b,86,a)].
given #124 (T,wt=6): 777 ->*_s0(length(empty(nil)),length(true)). [ur(87,a,182,a,b,86,a)].
given #125 (T,wt=6): 803 ->*_s0(head(empty(nil)),head(true)). [ur(87,a,183,a,b,86,a)].
given #126 (T,wt=6): 829 ->*_s0(empty(empty(nil)),empty(true)). [ur(87,a,186,a,b,86,a)].
given #127 (A,wt=23): 97 ->_s0(ring(x,y,z,u,w,app(cons(v5,v6),v7)),ring(x,y,z,u,w,cons(v5,app(v6,v7)))). [ur(51,a,60,a)].
given #128 (F,wt=16): 1092 -->_s0(mapf(three,head(x)),nil) | -->_s0(empty(mapf(two,head(y))),head(cons(true,z))) # answer(goal). [resolve(575,a,669,c)].
given #129 (F,wt=16): 1143 -->_s0(mapf(three,head(x)),nil) | -->*_s0(empty(mapf(two,y)),true) | -->_s0(head(z),y) # answer(goal). [resolve(744,c,45,b)].
given #130 (F,wt=12): 1242 -->_s0(mapf(three,head(x)),nil) | -->*_s0(empty(mapf(two,y)),true) # answer(goal). [resolve(1143,c,67,a)].
given #131 (F,wt=15): 1243 -->_s0(mapf(three,head(x)),nil) | -->_s0(empty(mapf(two,y)),z) | -->*_s0(z,true) # answer(goal). [resolve(1242,b,87,c)].
given #132 (T,wt=6): 882 ->*_s0(s(length(nil)),s(0)). [ur(87,a,314,a,b,86,a)].
given #133 (T,wt=6): 908 ->*_s0(tail(length(nil)),tail(0)). [ur(87,a,319,a,b,86,a)].
given #134 (T,wt=6): 934 ->*_s0(length(length(nil)),length(0)). [ur(87,a,332,a,b,86,a)].
given #135 (T,wt=6): 960 ->*_s0(head(length(nil)),head(0)). [ur(87,a,333,a,b,86,a)].
given #136 (A,wt=23): 98 ->_s0(ring(x,y,z,u,app(cons(w,v5),v6),v7),ring(x,y,z,u,cons(w,app(v5,v6)),v7)). [ur(50,a,60,a)].
given #137 (F,wt=12): 1254 -->_s0(mapf(three,head(x)),nil) | -->_s0(empty(mapf(two,y)),true) # answer(goal). [resolve(1243,c,86,a)].
given #138 (F,wt=13): 1248 -->_s0(mapf(three,head(x)),nil) | -->_s0(empty(mapf(two,y)),empty(nil)) # answer(goal). [resolve(1243,c,579,a)].
given #139 (F,wt=11): 1298 -->_s0(mapf(three,head(x)),nil) | -->_s0(mapf(two,y),nil) # answer(goal). [resolve(1248,b,37,b)].
given #140 (F,wt=6): 1299 -->_s0(mapf(three,head(x)),nil) # answer(goal). [resolve(1298,b,74,a)].
given #141 (T,wt=6): 1019 ->*_s0(empty(length(nil)),empty(0)). [ur(87,a,336,a,b,86,a)].
given #142 (T,wt=7): 114 ->_s0(s(app(nil,x)),s(x)). [ur(59,a,61,a)].
given #143 (T,wt=7): 119 ->_s0(tail(app(nil,x)),tail(x)). [ur(54,a,61,a)].
given #144 (T,wt=7): 132 ->_s0(length(app(nil,x)),length(x)). [ur(41,a,61,a)].
given #145 (A,wt=23): 99 ->_s0(ring(x,y,z,app(cons(u,w),v5),v6,v7),ring(x,y,z,cons(u,app(w,v5)),v6,v7)). [ur(49,a,60,a)].
given #146 (F,wt=16): 1149 -->_s0(mapf(two,head(x)),nil) | -->_s0(empty(mapf(three,head(y))),sndsplit(0,empty(nil))) # answer(goal). [resolve(627,a,672,c)].
given #147 (F,wt=16): 1158 -->_s0(mapf(two,head(x)),nil) | -->_s0(empty(mapf(three,head(y))),app(nil,empty(nil))) # answer(goal). [resolve(629,a,672,c)].
given #148 (F,wt=16): 1197 -->_s0(mapf(two,head(x)),nil) | -->*_s0(empty(mapf(three,y)),true) | -->_s0(head(z),y) # answer(goal). [resolve(1012,c,45,b)].
given #149 (F,wt=12): 1417 -->_s0(mapf(two,head(x)),nil) | -->*_s0(empty(mapf(three,y)),true) # answer(goal). [resolve(1197,c,67,a)].
given #150 (T,wt=6): 1363 ->*_s0(length(app(nil,nil)),0). [ur(87,a,132,a,b,573,a)].
given #151 (T,wt=7): 133 ->_s0(head(app(nil,x)),head(x)). [ur(40,a,61,a)].
given #152 (T,wt=7): 136 ->_s0(empty(app(nil,x)),empty(x)). [ur(37,a,61,a)].
given #153 (T,wt=6): 1456 ->*_s0(empty(app(nil,nil)),true). [ur(87,a,136,a,b,579,a)].
given #154 (A,wt=23): 100 ->_s0(ring(x,y,app(cons(z,u),w),v5,v6,v7),ring(x,y,cons(z,app(u,w)),v5,v6,v7)). [ur(48,a,60,a)].
given #155 (F,wt=14): 1483 -->_s0(mapf(two,head(x)),nil) | -->_s0(mapf(three,head(y)),app(nil,nil)) # answer(goal). [resolve(1456,a,1012,b)].
given #156 (F,wt=15): 1418 -->_s0(mapf(two,head(x)),nil) | -->_s0(empty(mapf(three,y)),z) | -->*_s0(z,true) # answer(goal). [resolve(1417,b,87,c)].
given #157 (F,wt=12): 1528 -->_s0(mapf(two,head(x)),nil) | -->_s0(empty(mapf(three,y)),true) # answer(goal). [resolve(1418,c,86,a)].
given #158 (F,wt=13): 1522 -->_s0(mapf(two,head(x)),nil) | -->_s0(empty(mapf(three,y)),empty(nil)) # answer(goal). [resolve(1418,c,579,a)].
given #159 (T,wt=7): 189 ->_s0(s(fstsplit(0,x)),s(nil)). [ur(59,a,64,a)].
given #160 (T,wt=7): 194 ->_s0(tail(fstsplit(0,x)),tail(nil)). [ur(54,a,64,a)].
given #161 (T,wt=7): 207 ->_s0(length(fstsplit(0,x)),length(nil)). [ur(41,a,64,a)].
given #162 (T,wt=6): 1582 ->*_s0(length(fstsplit(0,x)),0). [ur(87,a,207,a,b,573,a)].
given #163 (A,wt=23): 101 ->_s0(ring(x,app(cons(y,z),u),w,v5,v6,v7),ring(x,cons(y,app(z,u)),w,v5,v6,v7)). [ur(47,a,60,a)].
given #164 (F,wt=11): 1529 -->_s0(mapf(two,head(x)),nil) | -->_s0(mapf(three,y),nil) # answer(goal). [resolve(1522,b,37,b)].
given #165 (F,wt=6): 1640 -->_s0(mapf(two,head(x)),nil) # answer(goal). [resolve(1529,b,74,a)].
given #166 (F,wt=17): 612 -->*_s0(empty(mapf(three,head(x))),true) | -->*_s0(empty(y),true) | -->_s0(mapf(two,head(z)),y) # answer(goal). [resolve(583,b,37,b)].
given #167 (F,wt=15): 1642 -->*_s0(empty(mapf(three,head(x))),true) | -->_s0(mapf(two,head(y)),app(nil,nil)) # answer(goal). [resolve(612,b,1456,a)].
given #168 (T,wt=7): 208 ->_s0(head(fstsplit(0,x)),head(nil)). [ur(40,a,64,a)].
given #169 (T,wt=7): 211 ->_s0(empty(fstsplit(0,x)),empty(nil)). [ur(37,a,64,a)].
given #170 (T,wt=6): 1673 ->*_s0(empty(fstsplit(0,x)),true). [ur(87,a,211,a,b,579,a)].
given #171 (T,wt=7): 339 ->_s0(s(leq(0,x)),s(true)). [ur(59,a,70,a)].
given #172 (A,wt=23): 102 ->_s0(ring(app(cons(x,y),z),u,w,v5,v6,v7),ring(cons(x,app(y,z)),u,w,v5,v6,v7)). [ur(46,a,60,a)].
given #173 (F,wt=15): 1700 -->*_s0(empty(mapf(three,head(x))),true) | -->_s0(mapf(two,head(y)),fstsplit(0,z)) # answer(goal). [resolve(1673,a,612,b)].
given #174 (F,wt=17): 615 -->_s0(empty(mapf(two,head(x))),true) | -->_s0(empty(mapf(three,head(y))),z) | -->*_s0(z,true) # answer(goal). [resolve(614,a,87,c)].
given #175 (F,wt=14): 1773 -->_s0(empty(mapf(two,head(x))),true) | -->_s0(empty(mapf(three,head(y))),true) # answer(goal). [resolve(615,c,86,a)].
given #176 (F,wt=15): 1767 -->_s0(empty(mapf(two,head(x))),true) | -->_s0(empty(mapf(three,head(y))),empty(nil)) # answer(goal). [resolve(615,c,579,a)].
given #177 (T,wt=7): 344 ->_s0(tail(leq(0,x)),tail(true)). [ur(54,a,70,a)].
given #178 (T,wt=7): 357 ->_s0(length(leq(0,x)),length(true)). [ur(41,a,70,a)].
given #179 (T,wt=7): 358 ->_s0(head(leq(0,x)),head(true)). [ur(40,a,70,a)].
given #180 (T,wt=7): 361 ->_s0(empty(leq(0,x)),empty(true)). [ur(37,a,70,a)].
given #181 (A,wt=15): 103 ->_s0(mapf(x,app(cons(y,z),u)),mapf(x,cons(y,app(z,u)))). [ur(45,a,60,a)].
given #182 (F,wt=16): 1766 -->_s0(empty(mapf(two,head(x))),true) | -->_s0(empty(mapf(three,head(y))),app(nil,true)) # answer(goal). [resolve(615,c,581,a)].
given #183 (F,wt=16): 1769 -->_s0(empty(mapf(two,head(x))),true) | -->_s0(empty(mapf(three,head(y))),leq(0,z)) # answer(goal). [resolve(615,c,572,a)].
given #184 (F,wt=16): 1770 -->_s0(empty(mapf(two,head(x))),true) | -->_s0(empty(mapf(three,head(y))),sndsplit(0,true)) # answer(goal). [resolve(615,c,567,a)].
given #185 (F,wt=17): 616 -->*_s0(empty(mapf(two,head(x))),true) | -->*_s0(empty(y),true) | -->_s0(mapf(three,head(z)),y) # answer(goal). [resolve(584,b,37,b)].
given #186 (T,wt=7): 439 ->_s0(s(mapf(x,nil)),s(nil)). [ur(59,a,74,a)].
given #187 (T,wt=7): 444 ->_s0(tail(mapf(x,nil)),tail(nil)). [ur(54,a,74,a)].
given #188 (T,wt=7): 457 ->_s0(length(mapf(x,nil)),length(nil)). [ur(41,a,74,a)].
given #189 (T,wt=6): 1962 ->*_s0(length(mapf(x,nil)),0). [ur(87,a,457,a,b,573,a)].
given #190 (A,wt=15): 104 ->_s0(mapf(app(cons(x,y),z),u),mapf(cons(x,app(y,z)),u)). [ur(44,a,60,a)].
given #191 (F,wt=15): 1905 -->*_s0(empty(mapf(two,head(x))),true) | -->_s0(mapf(three,head(y)),fstsplit(0,z)) # answer(goal). [resolve(616,b,1673,a)].
given #192 (F,wt=15): 1906 -->*_s0(empty(mapf(two,head(x))),true) | -->_s0(mapf(three,head(y)),app(nil,nil)) # answer(goal). [resolve(616,b,1456,a)].
given #193 (F,wt=17): 619 -->_s0(empty(mapf(three,head(x))),true) | -->_s0(empty(mapf(two,head(y))),z) | -->*_s0(z,true) # answer(goal). [resolve(618,a,87,c)].
given #194 (F,wt=15): 2028 -->_s0(empty(mapf(three,head(x))),true) | -->_s0(empty(mapf(two,head(y))),empty(nil)) # answer(goal). [resolve(619,c,579,a)].
given #195 (T,wt=7): 458 ->_s0(head(mapf(x,nil)),head(nil)). [ur(40,a,74,a)].
given #196 (T,wt=7): 461 ->_s0(empty(mapf(x,nil)),empty(nil)). [ur(37,a,74,a)].
given #197 (T,wt=6): 2060 ->*_s0(empty(mapf(x,nil)),true). [ur(87,a,461,a,b,579,a)].
given #198 (T,wt=7): 464 ->_s0(s(sndsplit(0,x)),s(x)). [ur(59,a,82,a)].
given #199 (A,wt=15): 105 ->_s0(leq(x,app(cons(y,z),u)),leq(x,cons(y,app(z,u)))). [ur(43,a,60,a)].
given #200 (F,wt=15): 2088 -->*_s0(empty(mapf(two,head(x))),true) | -->_s0(mapf(three,head(y)),mapf(z,nil)) # answer(goal). [resolve(2060,a,616,b)].
given #201 (F,wt=11): 2153 -->*_s0(empty(mapf(two,head(x))),true) | -->_s0(head(y),nil) # answer(goal). [resolve(2088,b,45,b)].
given #202 (F,wt=7): 2155 -->*_s0(empty(mapf(two,head(x))),true) # answer(goal). [resolve(2153,b,67,a)].
given #203 (F,wt=7): 2168 -->_s0(empty(mapf(two,head(x))),true) # answer(goal). [ur(87,b,86,a,c,2155,a)].
given #204 (T,wt=7): 469 ->_s0(tail(sndsplit(0,x)),tail(x)). [ur(54,a,82,a)].
given #205 (T,wt=7): 482 ->_s0(length(sndsplit(0,x)),length(x)). [ur(41,a,82,a)].
given #206 (T,wt=6): 2203 ->*_s0(length(sndsplit(0,nil)),0). [ur(87,a,482,a,b,573,a)].
given #207 (T,wt=7): 483 ->_s0(head(sndsplit(0,x)),head(x)). [ur(40,a,82,a)].
given #208 (A,wt=15): 106 ->_s0(leq(app(cons(x,y),z),u),leq(cons(x,app(y,z)),u)). [ur(42,a,60,a)].
given #209 (F,wt=8): 2163 -->_s0(empty(mapf(two,head(x))),empty(nil)) # answer(goal). [ur(87,b,579,a,c,2155,a)].
given #210 (F,wt=9): 2162 -->_s0(empty(mapf(two,head(x))),app(nil,true)) # answer(goal). [ur(87,b,581,a,c,2155,a)].
given #211 (F,wt=9): 2165 -->_s0(empty(mapf(two,head(x))),leq(0,y)) # answer(goal). [ur(87,b,572,a,c,2155,a)].
given #212 (F,wt=9): 2166 -->_s0(empty(mapf(two,head(x))),sndsplit(0,true)) # answer(goal). [ur(87,b,567,a,c,2155,a)].
given #213 (T,wt=7): 486 ->_s0(empty(sndsplit(0,x)),empty(x)). [ur(37,a,82,a)].
given #214 (T,wt=6): 2297 ->*_s0(empty(sndsplit(0,nil)),true). [ur(87,a,486,a,b,579,a)].
given #215 (T,wt=7): 620 ->*_s0(tail(cons(x,length(nil))),0). [ur(87,a,85,a,b,573,a)].
given #216 (T,wt=7): 622 ->*_s0(head(cons(length(nil),x)),0). [ur(87,a,67,a,b,573,a)].
given #217 (A,wt=13): 107 ->_s0(length(app(cons(x,y),z)),length(cons(x,app(y,z)))). [ur(41,a,60,a)].
given #218 (F,wt=10): 2156 -->_s0(empty(mapf(two,head(x))),y) | -->*_s0(y,true) # answer(goal). [resolve(2155,a,87,c)].
given #219 (F,wt=10): 2157 -->_s0(empty(mapf(two,head(x))),empty(mapf(y,nil))) # answer(goal). [ur(87,b,2060,a,c,2155,a)].
============================== PROOF =================================
% Proof 1 at 0.06 (+ 0.00) seconds: goal.
% Length of proof is 24.
% Level of proof is 9.
% Maximum clause weight is 17.000.
% Given clauses 219.
3 ->_s0(x1,y) -> ->_s0(empty(x1),empty(y)) # label(congruence) # label(non_clause). [assumption].
11 ->_s0(x2,y) -> ->_s0(mapf(x1,x2),mapf(x1,y)) # label(congruence) # label(non_clause). [assumption].
33 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption].
34 (exists x13 exists x14 (->*_s0(empty(mapf(two,head(x13))),true) & ->*_s0(empty(mapf(three,head(x14))),true))) # label(goal) # label(non_clause) # label(goal). [goal].
37 -->_s0(x,y) | ->_s0(empty(x),empty(y)) # label(congruence). [clausify(3)].
45 -->_s0(x,y) | ->_s0(mapf(z,x),mapf(z,y)) # label(congruence). [clausify(11)].
63 ->_s0(empty(nil),true) # label(replacement). [assumption].
67 ->_s0(head(cons(x,y)),x) # label(replacement). [assumption].
74 ->_s0(mapf(x,nil),nil) # label(replacement). [assumption].
86 ->*_s0(x,x) # label(reflexivity). [assumption].
87 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(33)].
88 -->*_s0(empty(mapf(two,head(x))),true) | -->*_s0(empty(mapf(three,head(y))),true) # label(goal) # answer(goal). [deny(34)].
278 ->_s0(mapf(x,head(cons(y,z))),mapf(x,y)). [ur(45,a,67,a)].
461 ->_s0(empty(mapf(x,nil)),empty(nil)). [ur(37,a,74,a)].
579 ->*_s0(empty(nil),true). [ur(87,a,63,a,b,86,a)].
584 -->*_s0(empty(mapf(two,head(x))),true) | -->_s0(empty(mapf(three,head(y))),z) | -->*_s0(z,true) # answer(goal). [resolve(88,b,87,c)].
616 -->*_s0(empty(mapf(two,head(x))),true) | -->*_s0(empty(y),true) | -->_s0(mapf(three,head(z)),y) # answer(goal). [resolve(584,b,37,b)].
2060 ->*_s0(empty(mapf(x,nil)),true). [ur(87,a,461,a,b,579,a)].
2088 -->*_s0(empty(mapf(two,head(x))),true) | -->_s0(mapf(three,head(y)),mapf(z,nil)) # answer(goal). [resolve(2060,a,616,b)].
2153 -->*_s0(empty(mapf(two,head(x))),true) | -->_s0(head(y),nil) # answer(goal). [resolve(2088,b,45,b)].
2155 -->*_s0(empty(mapf(two,head(x))),true) # answer(goal). [resolve(2153,b,67,a)].
2157 -->_s0(empty(mapf(two,head(x))),empty(mapf(y,nil))) # answer(goal). [ur(87,b,2060,a,c,2155,a)].
2372 -->_s0(mapf(two,head(x)),mapf(y,nil)) # answer(goal). [resolve(2157,a,37,b)].
2373 $F # answer(goal). [resolve(2372,a,278,a)].
============================== end of proof ==========================
============================== STATISTICS ============================
Given=219. Generated=2386. Kept=2338. proofs=1.
Usable=155. Sos=2034. Demods=0. Limbo=0, Disabled=202. Hints=0.
Kept_by_rule=0, Deleted_by_rule=0.
Forward_subsumed=48. Back_subsumed=148.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
Demod_attempts=0. Demod_rewrites=0.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=300. Nonunit_bsub_feature_tests=926.
Megabytes=5.65.
User_CPU=0.06, System_CPU=0.00, Wall_clock=0.
============================== end of statistics =====================
============================== end of search =========================
THEOREM PROVED
Exiting with 1 proof.
Process 3174756 exit (max_proofs) Tue Jul 30 08:47:40 2024
The problem is feasible.