NO
Problem 1:
Infeasibility Problem:
[(VAR vNonEmpty x n h t m pid st1 in2 st2 in3 st3 vNonEmpty x6 x1 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(fstsplit(x6,x1)) ->* false, empty(mapf(three,head(x4))) ->* true
Problem 1:
Obtaining a proof using Prover9:
-> Prover9 Output:
============================== Prover9 ===============================
Prover9 (64) version 2009-11A, November 2009.
Process 3136747 was started by sandbox2 on z020.star.cs.uiowa.edu,
Tue Jul 30 08:23:10 2024
The command was "./prover9 -f /tmp/prover93136740-0.in".
============================== end of head ===========================
============================== INPUT =================================
% Reading from file /tmp/prover93136740-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 exists x15 (->*_s0(empty(fstsplit(x13,x14)),false) & ->*_s0(empty(mapf(three,head(x15))),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 exists x15 (->*_s0(empty(fstsplit(x13,x14)),false) & ->*_s0(empty(mapf(three,head(x15))),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(fstsplit(x,y)),false) | -->*_s0(empty(mapf(three,head(z))),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(fstsplit(x,y)),false) | -->*_s0(empty(mapf(three,head(z))),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(fstsplit(x,y)),false) | -->*_s0(empty(mapf(three,head(z))),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=13): 88 -->*_s0(empty(fstsplit(x,y)),false) | -->*_s0(empty(mapf(three,head(z))),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=16): 583 -->*_s0(empty(mapf(three,head(x))),true) | -->_s0(empty(fstsplit(y,z)),u) | -->*_s0(u,false) # answer(goal). [resolve(88,a,87,c)].
given #57 (F,wt=13): 614 -->*_s0(empty(mapf(three,head(x))),true) | -->_s0(empty(fstsplit(y,z)),false) # answer(goal). [resolve(583,c,86,a)].
given #58 (F,wt=16): 584 -->*_s0(empty(fstsplit(x,y)),false) | -->_s0(empty(mapf(three,head(z))),u) | -->*_s0(u,true) # answer(goal). [resolve(88,b,87,c)].
given #59 (F,wt=13): 618 -->*_s0(empty(fstsplit(x,y)),false) | -->_s0(empty(mapf(three,head(z))),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=14): 624 -->*_s0(empty(fstsplit(x,y)),false) | -->_s0(empty(mapf(three,head(z))),empty(nil)) # answer(goal). [resolve(579,a,584,c)].
given #66 (F,wt=12): 667 -->*_s0(empty(fstsplit(x,y)),false) | -->_s0(mapf(three,head(z)),nil) # answer(goal). [resolve(624,b,37,b)].
given #67 (F,wt=15): 629 -->*_s0(empty(fstsplit(x,y)),false) | -->_s0(empty(mapf(three,head(z))),sndsplit(0,true)) # answer(goal). [resolve(567,a,584,c)].
given #68 (F,wt=15): 630 -->*_s0(empty(mapf(three,head(x))),true) | -->_s0(empty(fstsplit(y,z)),sndsplit(0,false)) # answer(goal). [resolve(567,a,583,c)].
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=15): 668 -->_s0(mapf(three,head(x)),nil) | -->_s0(empty(fstsplit(y,z)),u) | -->*_s0(u,false) # answer(goal). [resolve(667,a,87,c)].
given #75 (F,wt=12): 743 -->_s0(mapf(three,head(x)),nil) | -->_s0(empty(fstsplit(y,z)),false) # answer(goal). [resolve(668,c,86,a)].
given #76 (F,wt=14): 740 -->_s0(mapf(three,head(x)),nil) | -->_s0(empty(fstsplit(y,z)),app(nil,false)) # answer(goal). [resolve(668,c,581,a)].
given #77 (F,wt=14): 741 -->_s0(mapf(three,head(x)),nil) | -->_s0(empty(fstsplit(y,z)),sndsplit(0,false)) # answer(goal). [resolve(668,c,567,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=15): 671 -->*_s0(empty(fstsplit(x,y)),false) | -->_s0(empty(mapf(three,head(z))),leq(0,u)) # answer(goal). [resolve(572,a,584,c)].
given #84 (F,wt=15): 681 -->*_s0(empty(fstsplit(x,y)),false) | -->_s0(empty(mapf(three,head(z))),app(nil,true)) # answer(goal). [resolve(581,a,584,c)].
given #85 (F,wt=15): 682 -->*_s0(empty(mapf(three,head(x))),true) | -->_s0(empty(fstsplit(y,z)),app(nil,false)) # answer(goal). [resolve(581,a,583,c)].
given #86 (F,wt=15): 739 -->_s0(mapf(three,head(x)),nil) | -->*_s0(empty(y),false) | -->_s0(fstsplit(z,u),y) # answer(goal). [resolve(668,b,37,b)].
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=6): 879 -->_s0(mapf(three,head(x)),nil) # answer(goal). [resolve(739,c,65,a),unit_del(b,580)].
given #93 (F,wt=16): 612 -->*_s0(empty(mapf(three,head(x))),true) | -->*_s0(empty(y),false) | -->_s0(fstsplit(z,u),y) # answer(goal). [resolve(583,b,37,b)].
given #94 (F,wt=7): 1013 -->*_s0(empty(mapf(three,head(x))),true) # answer(goal). [resolve(612,c,65,a),unit_del(b,580)].
given #95 (F,wt=7): 1019 -->_s0(empty(mapf(three,head(x))),true) # answer(goal). [ur(87,b,86,a,c,1013,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=8): 1016 -->_s0(empty(mapf(three,head(x))),empty(nil)) # answer(goal). [ur(87,b,579,a,c,1013,a)].
given #102 (F,wt=9): 1015 -->_s0(empty(mapf(three,head(x))),app(nil,true)) # answer(goal). [ur(87,b,581,a,c,1013,a)].
given #103 (F,wt=9): 1017 -->_s0(empty(mapf(three,head(x))),leq(0,y)) # answer(goal). [ur(87,b,572,a,c,1013,a)].
given #104 (F,wt=9): 1018 -->_s0(empty(mapf(three,head(x))),sndsplit(0,true)) # answer(goal). [ur(87,b,567,a,c,1013,a)].
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=10): 1014 -->_s0(empty(mapf(three,head(x))),y) | -->*_s0(y,true) # answer(goal). [resolve(1013,a,87,c)].
given #111 (F,wt=10): 1050 -->_s0(empty(mapf(three,head(x))),tail(cons(y,true))) # answer(goal). [ur(87,b,564,a,c,1013,a)].
given #112 (F,wt=10): 1092 -->_s0(empty(mapf(three,head(x))),head(cons(true,y))) # answer(goal). [ur(87,b,575,a,c,1013,a)].
given #113 (F,wt=10): 1133 -->*_s0(empty(x),true) | -->_s0(mapf(three,head(y)),x) # answer(goal). [resolve(1014,a,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): 626 ->*_s0(sndsplit(0,empty(nil)),true). [ur(87,a,82,a,b,579,a)].
given #116 (T,wt=6): 628 ->*_s0(app(nil,empty(nil)),true). [ur(87,a,61,a,b,579,a)].
given #117 (T,wt=6): 687 ->*_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=10): 1136 -->*_s0(empty(mapf(three,x)),true) | -->_s0(head(y),x) # answer(goal). [resolve(1133,b,45,b)].
given #120 (F,wt=6): 1184 -->*_s0(empty(mapf(three,x)),true) # answer(goal). [resolve(1136,b,67,a)].
============================== PROOF =================================
% Proof 1 at 0.04 (+ 0.00) seconds: goal.
% Length of proof is 26.
% Level of proof is 10.
% Maximum clause weight is 16.000.
% Given clauses 120.
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 exists x15 (->*_s0(empty(fstsplit(x13,x14)),false) & ->*_s0(empty(mapf(three,head(x15))),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)].
62 ->_s0(empty(cons(x,y)),false) # label(replacement). [assumption].
63 ->_s0(empty(nil),true) # label(replacement). [assumption].
65 ->_s0(fstsplit(s(x),cons(y,z)),cons(y,fstsplit(x,z))) # 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(fstsplit(x,y)),false) | -->*_s0(empty(mapf(three,head(z))),true) # label(goal) # answer(goal). [deny(34)].
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)].
580 ->*_s0(empty(cons(x,y)),false). [ur(87,a,62,a,b,86,a)].
583 -->*_s0(empty(mapf(three,head(x))),true) | -->_s0(empty(fstsplit(y,z)),u) | -->*_s0(u,false) # answer(goal). [resolve(88,a,87,c)].
612 -->*_s0(empty(mapf(three,head(x))),true) | -->*_s0(empty(y),false) | -->_s0(fstsplit(z,u),y) # answer(goal). [resolve(583,b,37,b)].
1013 -->*_s0(empty(mapf(three,head(x))),true) # answer(goal). [resolve(612,c,65,a),unit_del(b,580)].
1014 -->_s0(empty(mapf(three,head(x))),y) | -->*_s0(y,true) # answer(goal). [resolve(1013,a,87,c)].
1133 -->*_s0(empty(x),true) | -->_s0(mapf(three,head(y)),x) # answer(goal). [resolve(1014,a,37,b)].
1136 -->*_s0(empty(mapf(three,x)),true) | -->_s0(head(y),x) # answer(goal). [resolve(1133,b,45,b)].
1184 -->*_s0(empty(mapf(three,x)),true) # answer(goal). [resolve(1136,b,67,a)].
1189 -->_s0(empty(mapf(three,x)),empty(nil)) # answer(goal). [ur(87,b,579,a,c,1184,a)].
1190 $F # answer(goal). [resolve(1189,a,461,a)].
============================== end of proof ==========================
============================== STATISTICS ============================
Given=120. Generated=1190. Kept=1155. proofs=1.
Usable=99. Sos=1012. Demods=0. Limbo=4, Disabled=93. Hints=0.
Kept_by_rule=0, Deleted_by_rule=0.
Forward_subsumed=35. Back_subsumed=39.
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=109. Nonunit_bsub_feature_tests=256.
Megabytes=2.79.
User_CPU=0.04, System_CPU=0.00, Wall_clock=0.
============================== end of statistics =====================
============================== end of search =========================
THEOREM PROVED
Exiting with 1 proof.
Process 3136747 exit (max_proofs) Tue Jul 30 08:23:10 2024
The problem is feasible.