%------------------------------------------------------------------------------
% File : EQP---0.9e
% Problem : SWX239-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : tptp2X_and_run_eqp %s
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 07:00:13 PM UTC 2026
% Result : Unsatisfiable 15.45s 15.85s
% Output : Refutation 15.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 12
% Syntax : Number of clauses : 29 ( 29 unt; 0 nHn; 8 RR)
% Number of literals : 29 ( 0 equ; 3 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 4 con; 0-4 aty)
% Number of variables : 44 ( 11 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,plain,
equal(aux(A,B,btrue),eps),
file('SWX239-1.p',unknown),
[] ).
cnf(6,plain,
equal(aux3(A,B,C,bfalse),bfalse),
file('SWX239-1.p',unknown),
[] ).
cnf(72,plain,
equal(notb(btrue),bfalse),
file('SWX239-1.p',unknown),
[] ).
cnf(74,plain,
equal(andb(btrue,A),A),
file('SWX239-1.p',unknown),
[] ).
cnf(76,plain,
equal(eps2(eps),btrue),
file('SWX239-1.p',unknown),
[] ).
cnf(78,plain,
equal(eps2(y(A,B)),andb(eps2(A),eps2(B))),
file('SWX239-1.p',unknown),
[] ).
cnf(79,plain,
equal(eps2(star(A)),btrue),
file('SWX239-1.p',unknown),
[] ).
cnf(82,plain,
equal(step(atom(A),B),aux(B,A,eq(A,B))),
file('SWX239-1.p',unknown),
[] ).
cnf(86,plain,
equal(y(step(A,B),star(A)),step(star(A),B)),
inference(flip,[status(thm),theory(equality)],[1]),
[iquote('flip(1)')] ).
cnf(89,plain,
equal(eps2(A),rec(A,nil2)),
inference(flip,[status(thm),theory(equality)],[1]),
[iquote('flip(1)')] ).
cnf(93,plain,
equal(rec(star(A),nil2),btrue),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[79]),89]),
[iquote('back_demod(79),demod([89])')] ).
cnf(94,plain,
equal(rec(y(A,B),nil2),andb(rec(A,nil2),rec(B,nil2))),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[78]),89,89,89]),
[iquote('back_demod(78),demod([89,89,89])')] ).
cnf(96,plain,
equal(rec(eps,nil2),btrue),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[76]),89]),
[iquote('back_demod(76),demod([89])')] ).
cnf(97,plain,
equal(rec(step(A,B),C),rec(A,cons2(B,C))),
inference(flip,[status(thm),theory(equality)],[1]),
[iquote('flip(1)')] ).
cnf(110,plain,
equal(reck2(star(A),cons2(B,C)),aux3(A,B,C,notb(rec(A,nil2)))),
inference(demod,[status(thm),theory(equality)],[89]),
[iquote('demod([89])')] ).
cnf(111,plain,
equal(eq2(rec(A,B),reck2(A,B)),prop_same(A,B)),
inference(flip,[status(thm),theory(equality)],[1]),
[iquote('flip(1)')] ).
cnf(119,plain,
equal(eq2(btrue,bfalse),bfalse),
file('SWX239-1.p',unknown),
[] ).
cnf(120,plain,
equal(eq(A,A),btrue),
file('SWX239-1.p',unknown),
[] ).
cnf(121,plain,
equal(eq2(A,A),btrue),
file('SWX239-1.p',unknown),
[] ).
cnf(122,plain,
~ equal(eq2(prop_same(A,B),bfalse),btrue),
file('SWX239-1.p',unknown),
[] ).
cnf(317,plain,
equal(rec(star(A),cons2(B,nil2)),andb(rec(A,cons2(B,nil2)),btrue)),
inference(demod,[status(thm),theory(equality)],[inference(para,[status(thm),theory(equality)],[86,94]),97,97,93]),
[iquote('para(86,94),demod([97,97,93])')] ).
cnf(325,plain,
equal(rec(aux(A,B,eq(B,A)),C),rec(atom(B),cons2(A,C))),
inference(para,[status(thm),theory(equality)],[82,97]),
[iquote('para(82,97)')] ).
cnf(424,plain,
equal(rec(atom(A),cons2(A,B)),rec(eps,B)),
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(para,[status(thm),theory(equality)],[120,325]),1]),1]),
[iquote('para(120,325),demod([1]),flip(1)')] ).
cnf(1639,plain,
equal(eq2(andb(rec(A,cons2(B,nil2)),btrue),aux3(A,B,nil2,notb(rec(A,nil2)))),prop_same(star(A),cons2(B,nil2))),
inference(demod,[status(thm),theory(equality)],[inference(para,[status(thm),theory(equality)],[317,111]),110]),
[iquote('para(317,111),demod([110])')] ).
cnf(28738,plain,
equal(eq2(andb(andb(rec(A,cons2(B,nil2)),btrue),btrue),bfalse),prop_same(star(star(A)),cons2(B,nil2))),
inference(demod,[status(thm),theory(equality)],[inference(para,[status(thm),theory(equality)],[93,1639]),317,72,6]),
[iquote('para(93,1639),demod([317,72,6])')] ).
cnf(28739,plain,
equal(prop_same(star(star(A)),cons2(B,nil2)),eq2(andb(andb(rec(A,cons2(B,nil2)),btrue),btrue),bfalse)),
inference(flip,[status(thm),theory(equality)],[28738]),
[iquote('flip(28738)')] ).
cnf(28741,plain,
~ equal(eq2(eq2(andb(andb(rec(A,cons2(B,nil2)),btrue),btrue),bfalse),bfalse),btrue),
inference(para,[status(thm),theory(equality)],[28739,122]),
[iquote('para(28739,122)')] ).
cnf(28742,plain,
~ equal(btrue,btrue),
inference(demod,[status(thm),theory(equality)],[inference(para,[status(thm),theory(equality)],[424,28741]),96,74,74,119,121]),
[iquote('para(424,28741),demod([96,74,74,119,121])')] ).
cnf(28743,plain,
$false,
inference(conflict,[status(thm)],[28742]),
[iquote('xx_conflict(28742)')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX239-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : tptp2X_and_run_eqp %s
% 0.16/0.33 % Computer : n009.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 13:18:55 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.70/1.09 ----- EQP 0.9e, May 2009 -----
% 0.70/1.09 The job began on n009.cluster.edu, Tue May 5 13:18:56 2026
% 0.70/1.09 The command was "./eqp09e".
% 0.70/1.09
% 0.70/1.09 set(prolog_style_variables).
% 0.70/1.09 set(lrpo).
% 0.70/1.09 set(basic_paramod).
% 0.70/1.09 set(functional_subsume).
% 0.70/1.09 set(ordered_paramod).
% 0.70/1.09 set(prime_paramod).
% 0.70/1.09 set(para_pairs).
% 0.70/1.09 assign(pick_given_ratio,4).
% 0.70/1.09 clear(print_kept).
% 0.70/1.09 clear(print_new_demod).
% 0.70/1.09 clear(print_back_demod).
% 0.70/1.09 clear(print_given).
% 0.70/1.09 assign(max_mem,64000).
% 0.70/1.09 end_of_commands.
% 0.70/1.09
% 0.70/1.09 Usable:
% 0.70/1.09 end_of_list.
% 0.70/1.09
% 0.70/1.09 Sos:
% 0.70/1.09 0 (wt=-1) [] aux(A,B,btrue) = eps.
% 0.70/1.09 0 (wt=-1) [] aux(A,B,bfalse) = nil4.
% 0.70/1.09 0 (wt=-1) [] aux2(A,B,C,btrue) = x(y(step(B,A),C),step(C,A)).
% 0.70/1.09 0 (wt=-1) [] aux2(A,B,C,bfalse) = x(y(step(B,A),C),nil4).
% 0.70/1.09 0 (wt=-1) [] aux3(A,B,C,btrue) = rec(y(A,star(A)),cons2(B,C)).
% 0.70/1.09 0 (wt=-1) [] aux3(A,B,C,bfalse) = bfalse.
% 0.70/1.09 0 (wt=-1) [] z(nil4,A) = nil4.
% 0.70/1.09 0 (wt=-1) [] z(eps,A) = A.
% 0.70/1.09 0 (wt=-1) [] z(atom(A),nil4) = nil4.
% 0.70/1.09 0 (wt=-1) [] z(atom(A),eps) = atom(A).
% 0.70/1.09 0 (wt=-1) [] z(atom(A),atom(B)) = y(atom(A),atom(B)).
% 0.70/1.09 0 (wt=-1) [] z(atom(A),x(B,C)) = y(atom(A),x(B,C)).
% 0.70/1.09 0 (wt=-1) [] z(atom(A),y(B,C)) = y(atom(A),y(B,C)).
% 0.70/1.09 0 (wt=-1) [] z(atom(A),star(B)) = y(atom(A),star(B)).
% 0.70/1.09 0 (wt=-1) [] z(x(A,B),nil4) = nil4.
% 0.70/1.09 0 (wt=-1) [] z(x(A,B),eps) = x(A,B).
% 0.70/1.09 0 (wt=-1) [] z(x(A,B),atom(C)) = y(x(A,B),atom(C)).
% 0.70/1.09 0 (wt=-1) [] z(x(A,B),x(C,D)) = y(x(A,B),x(C,D)).
% 0.70/1.09 0 (wt=-1) [] z(x(A,B),y(C,D)) = y(x(A,B),y(C,D)).
% 0.70/1.09 0 (wt=-1) [] z(x(A,B),star(C)) = y(x(A,B),star(C)).
% 0.70/1.09 0 (wt=-1) [] z(y(A,B),nil4) = nil4.
% 0.70/1.09 0 (wt=-1) [] z(y(A,B),eps) = y(A,B).
% 0.70/1.09 0 (wt=-1) [] z(y(A,B),atom(C)) = y(y(A,B),atom(C)).
% 0.70/1.09 0 (wt=-1) [] z(y(A,B),x(C,D)) = y(y(A,B),x(C,D)).
% 0.70/1.09 0 (wt=-1) [] z(y(A,B),y(C,D)) = y(y(A,B),y(C,D)).
% 0.70/1.09 0 (wt=-1) [] z(y(A,B),star(C)) = y(y(A,B),star(C)).
% 0.70/1.09 0 (wt=-1) [] z(star(A),nil4) = nil4.
% 0.70/1.09 0 (wt=-1) [] z(star(A),eps) = star(A).
% 0.70/1.09 0 (wt=-1) [] z(star(A),atom(B)) = y(star(A),atom(B)).
% 0.70/1.09 0 (wt=-1) [] z(star(A),x(B,C)) = y(star(A),x(B,C)).
% 0.70/1.09 0 (wt=-1) [] z(star(A),y(B,C)) = y(star(A),y(B,C)).
% 0.70/1.09 0 (wt=-1) [] z(star(A),star(B)) = y(star(A),star(B)).
% 0.70/1.09 0 (wt=-1) [] x2(nil4,A) = A.
% 0.70/1.09 0 (wt=-1) [] x2(eps,nil4) = eps.
% 0.70/1.09 0 (wt=-1) [] x2(eps,eps) = x(eps,eps).
% 0.70/1.09 0 (wt=-1) [] x2(eps,atom(A)) = x(eps,atom(A)).
% 0.70/1.09 0 (wt=-1) [] x2(eps,x(A,B)) = x(eps,x(A,B)).
% 0.70/1.09 0 (wt=-1) [] x2(eps,y(A,B)) = x(eps,y(A,B)).
% 0.70/1.09 0 (wt=-1) [] x2(eps,star(A)) = x(eps,star(A)).
% 0.70/1.09 0 (wt=-1) [] x2(atom(A),nil4) = atom(A).
% 0.70/1.09 0 (wt=-1) [] x2(atom(A),eps) = x(atom(A),eps).
% 0.70/1.09 0 (wt=-1) [] x2(atom(A),atom(B)) = x(atom(A),atom(B)).
% 0.70/1.09 0 (wt=-1) [] x2(atom(A),x(B,C)) = x(atom(A),x(B,C)).
% 0.70/1.09 0 (wt=-1) [] x2(atom(A),y(B,C)) = x(atom(A),y(B,C)).
% 0.70/1.09 0 (wt=-1) [] x2(atom(A),star(B)) = x(atom(A),star(B)).
% 0.70/1.09 0 (wt=-1) [] x2(x(A,B),nil4) = x(A,B).
% 0.70/1.09 0 (wt=-1) [] x2(x(A,B),eps) = x(x(A,B),eps).
% 0.70/1.09 0 (wt=-1) [] x2(x(A,B),atom(C)) = x(x(A,B),atom(C)).
% 0.70/1.09 0 (wt=-1) [] x2(x(A,B),x(C,D)) = x(x(A,B),x(C,D)).
% 0.70/1.09 0 (wt=-1) [] x2(x(A,B),y(C,D)) = x(x(A,B),y(C,D)).
% 0.70/1.09 0 (wt=-1) [] x2(x(A,B),star(C)) = x(x(A,B),star(C)).
% 0.70/1.09 0 (wt=-1) [] x2(y(A,B),nil4) = y(A,B).
% 0.70/1.09 0 (wt=-1) [] x2(y(A,B),eps) = x(y(A,B),eps).
% 0.70/1.09 0 (wt=-1) [] x2(y(A,B),atom(C)) = x(y(A,B),atom(C)).
% 0.70/1.09 0 (wt=-1) [] x2(y(A,B),x(C,D)) = x(y(A,B),x(C,D)).
% 0.70/1.09 0 (wt=-1) [] x2(y(A,B),y(C,D)) = x(y(A,B),y(C,D)).
% 0.70/1.09 0 (wt=-1) [] x2(y(A,B),star(C)) = x(y(A,B),star(C)).
% 0.70/1.09 0 (wt=-1) [] x2(star(A),nil4) = star(A).
% 0.70/1.09 0 (wt=-1) [] x2(star(A),eps) = x(star(A),eps).
% 0.70/1.09 0 (wt=-1) [] x2(star(A),atom(B)) = x(star(A),atom(B)).
% 0.70/1.09 0 (wt=-1) [] x2(star(A),x(B,C)) = x(star(A),x(B,C)).
% 0.70/1.09 0 (wt=-1) [] x2(star(A),y(B,C)) = x(star(A),y(B,C)).
% 0.70/1.09 0 (wt=-1) [] x2(star(A),star(B)) = x(star(A),star(B)).
% 0.70/1.09 0 (wt=-1) [] splits(A,nil) = nil.
% 0.70/1.09 0 (wt=-1) [] splits(A,cons(pair2(B,C),D)) = cons(pair2(cons2(A,B),C),splits(A,D)).
% 0.70/1.09 0 (wt=-1) [] splits2(nil2) = cons(pair2(nil2,nil2),nil).
% 0.70/1.09 0 (wt=-1) [] splits2(cons2(A,B)) = cons(pair2(nil2,cons2(A,B)),splits(A,splits2(B))).
% 0.70/1.09 0 (wt=-1) [] orb(btrue,A) = btrue.
% 0.70/1.09 0 (wt=-1) [] orb(bfalse,A) = A.
% 0.70/1.09 0 (wt=-1) [] or2(nil3) = bfalse.
% 0.70/1.09 0 (wt=-1) [] or2(cons3(A,B)) = orb(A,or2(B)).
% 0.70/1.09 0 (wt=-1) [] notb(btrue) = bfalse.
% 0.70/1.09 0 (wt=-1) [] notb(bfalse) = btrue.
% 0.70/1.09 0 (wt=-1) [] andb(btrue,A) = A.
% 0.70/1.09 0 (wt=-1) [] andb(bfalse,A) = bfalse.
% 0.70/1.09 0 (wt=-1) [] eps2(eps) = btrue.
% 0.70/1.09 0 (wt=-1) [] eps2(x(A,B)) = orb(eps2(A),eps2(B)).
% 0.70/1.09 0 (wt=-1) [] eps2(y(A,B)) = andb(eps2(A),eps2(B)).
% 0.70/1.09 0 (wt=-1) [] eps2(star(A)) = btrue.
% 0.70/1.09 0 (wt=-1) [] eps2(nil4) = bfalse.
% 0.70/1.09 0 (wt=-1) [] eps2(atom(A)) = bfalse.
% 0.70/1.09 0 (wt=-1) [] step(atom(A),B) = aux(B,A,eq(A,B)).
% 0.70/1.09 0 (wt=-1) [] step(x(A,B),C) = x(step(A,C),step(B,C)).
% 0.70/1.09 0 (wt=-1) [] step(y(A,B),C) = aux2(C,A,B,eps2(A)).
% 0.70/1.09 0 (wt=-1) [] step(star(A),B) = y(step(A,B),star(A)).
% 0.70/1.09 0 (wt=-1) [] step(nil4,A) = nil4.
% 0.70/1.09 0 (wt=-1) [] step(eps,A) = nil4.
% 0.70/1.09 0 (wt=-1) [] rec(A,nil2) = eps2(A).
% 0.70/1.09 0 (wt=-1) [] rec(A,cons2(B,C)) = rec(step(A,B),C).
% 0.70/1.09 0 (wt=-1) [] reck(A,B,nil) = nil3.
% 0.70/1.09 0 (wt=-1) [] reck(A,B,cons(pair2(C,D),E)) = cons3(andb(reck2(A,C),rec(B,D)),reck(A,B,E)).
% 0.70/1.09 0 (wt=-1) [] reck2(nil4,A) = bfalse.
% 0.70/1.09 0 (wt=-1) [] reck2(eps,nil2) = btrue.
% 0.70/1.09 0 (wt=-1) [] reck2(eps,cons2(A,B)) = bfalse.
% 0.70/1.09 0 (wt=-1) [] reck2(atom(A),nil2) = bfalse.
% 0.70/1.09 0 (wt=-1) [] reck2(atom(A),cons2(B,nil2)) = eq(A,B).
% 0.70/1.09 0 (wt=-1) [] reck2(atom(A),cons2(B,cons2(C,D))) = bfalse.
% 0.70/1.09 0 (wt=-1) [] reck2(x(A,B),C) = orb(reck2(A,C),reck2(B,C)).
% 0.70/1.09 0 (wt=-1) [] reck2(y(A,B),C) = or2(reck(A,B,splits2(C))).
% 0.70/1.09 0 (wt=-1) [] reck2(star(A),nil2) = btrue.
% 0.70/1.09 0 (wt=-1) [] reck2(star(A),cons2(B,C)) = aux3(A,B,C,notb(eps2(A))).
% 0.70/1.09 0 (wt=-1) [] prop_same(A,B) = eq2(rec(A,B),reck2(A,B)).
% 0.70/1.09 0 (wt=-1) [] eq(a,b) = bfalse.
% 0.70/1.09 0 (wt=-1) [] eq(a,c) = bfalse.
% 0.70/1.09 0 (wt=-1) [] eq(b,a) = bfalse.
% 0.70/1.09 0 (wt=-1) [] eq(b,c) = bfalse.
% 0.70/1.09 0 (wt=-1) [] eq(c,a) = bfalse.
% 0.70/1.09 0 (wt=-1) [] eq(c,b) = bfalse.
% 0.70/1.09 0 (wt=-1) [] eq2(bfalse,btrue) = bfalse.
% 0.70/1.09 0 (wt=-1) [] eq2(btrue,bfalse) = bfalse.
% 0.70/1.09 0 (wt=-1) [] eq(A,A) = btrue.
% 0.70/1.09 0 (wt=-1) [] eq2(A,A) = btrue.
% 0.70/1.09 0 (wt=-1) [] -(eq2(prop_same(A,B),bfalse) = btrue).
% 0.70/1.09 end_of_list.
% 0.70/1.09
% 0.70/1.09 Demodulators:
% 0.70/1.09 end_of_list.
% 0.70/1.09
% 0.70/1.09 Passive:
% 0.70/1.09 end_of_list.
% 0.70/1.09
% 0.70/1.09 Starting to process input.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 1 (wt=6) [] aux(A,B,btrue) = eps.
% 0.70/1.09 1 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 2 (wt=6) [] aux(A,B,bfalse) = nil4.
% 0.70/1.09 2 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 3 (wt=15) [flip(1)] x(y(step(A,B),C),step(C,B)) = aux2(B,A,C,btrue).
% 0.70/1.09 3 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 4 (wt=13) [flip(1)] x(y(step(A,B),C),nil4) = aux2(B,A,C,bfalse).
% 0.70/1.09 4 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 5 (wt=14) [flip(1)] rec(y(A,star(A)),cons2(B,C)) = aux3(A,B,C,btrue).
% 0.70/1.09 5 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 6 (wt=7) [] aux3(A,B,C,bfalse) = bfalse.
% 0.70/1.09 6 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 7 (wt=5) [] z(nil4,A) = nil4.
% 0.70/1.09 7 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 8 (wt=5) [] z(eps,A) = A.
% 0.70/1.09 8 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 9 (wt=6) [] z(atom(A),nil4) = nil4.
% 0.70/1.09 9 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 10 (wt=7) [] z(atom(A),eps) = atom(A).
% 0.70/1.09 10 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 11 (wt=11) [] z(atom(A),atom(B)) = y(atom(A),atom(B)).
% 0.70/1.09 11 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 12 (wt=13) [] z(atom(A),x(B,C)) = y(atom(A),x(B,C)).
% 0.70/1.09 12 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 13 (wt=13) [] z(atom(A),y(B,C)) = y(atom(A),y(B,C)).
% 0.70/1.09 13 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 14 (wt=11) [] z(atom(A),star(B)) = y(atom(A),star(B)).
% 0.70/1.09 14 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 15 (wt=7) [] z(x(A,B),nil4) = nil4.
% 0.70/1.09 15 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 16 (wt=9) [] z(x(A,B),eps) = x(A,B).
% 0.70/1.09 16 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 17 (wt=13) [] z(x(A,B),atom(C)) = y(x(A,B),atom(C)).
% 0.70/1.09 17 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 18 (wt=15) [] z(x(A,B),x(C,D)) = y(x(A,B),x(C,D)).
% 0.70/1.09 18 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 19 (wt=15) [] z(x(A,B),y(C,D)) = y(x(A,B),y(C,D)).
% 0.70/1.09 19 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 20 (wt=13) [] z(x(A,B),star(C)) = y(x(A,B),star(C)).
% 0.70/1.09 20 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 21 (wt=7) [] z(y(A,B),nil4) = nil4.
% 0.70/1.09 21 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 22 (wt=9) [] z(y(A,B),eps) = y(A,B).
% 0.70/1.09 22 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 23 (wt=13) [] z(y(A,B),atom(C)) = y(y(A,B),atom(C)).
% 0.70/1.09 23 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 24 (wt=15) [] z(y(A,B),x(C,D)) = y(y(A,B),x(C,D)).
% 0.70/1.09 24 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 25 (wt=15) [] z(y(A,B),y(C,D)) = y(y(A,B),y(C,D)).
% 0.70/1.09 25 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 26 (wt=13) [] z(y(A,B),star(C)) = y(y(A,B),star(C)).
% 0.70/1.09 26 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 27 (wt=6) [] z(star(A),nil4) = nil4.
% 0.70/1.09 27 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 28 (wt=7) [] z(star(A),eps) = star(A).
% 0.70/1.09 28 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 29 (wt=11) [] z(star(A),atom(B)) = y(star(A),atom(B)).
% 0.70/1.09 29 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 30 (wt=13) [] z(star(A),x(B,C)) = y(star(A),x(B,C)).
% 0.70/1.09 30 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 31 (wt=13) [] z(star(A),y(B,C)) = y(star(A),y(B,C)).
% 0.70/1.09 31 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 32 (wt=11) [] z(star(A),star(B)) = y(star(A),star(B)).
% 0.70/1.09 32 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 33 (wt=5) [] x2(nil4,A) = A.
% 0.70/1.09 33 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 34 (wt=5) [] x2(eps,nil4) = eps.
% 0.70/1.09 34 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 35 (wt=7) [] x2(eps,eps) = x(eps,eps).
% 0.70/1.09 35 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 36 (wt=9) [] x2(eps,atom(A)) = x(eps,atom(A)).
% 0.70/1.09 36 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 37 (wt=11) [] x2(eps,x(A,B)) = x(eps,x(A,B)).
% 0.70/1.09 37 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 38 (wt=11) [] x2(eps,y(A,B)) = x(eps,y(A,B)).
% 0.70/1.09 38 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 39 (wt=9) [] x2(eps,star(A)) = x(eps,star(A)).
% 0.70/1.09 39 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 40 (wt=7) [] x2(atom(A),nil4) = atom(A).
% 0.70/1.09 40 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 41 (wt=9) [] x2(atom(A),eps) = x(atom(A),eps).
% 0.70/1.09 41 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 42 (wt=11) [] x2(atom(A),atom(B)) = x(atom(A),atom(B)).
% 0.70/1.09 42 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 43 (wt=13) [] x2(atom(A),x(B,C)) = x(atom(A),x(B,C)).
% 0.70/1.09 43 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 44 (wt=13) [] x2(atom(A),y(B,C)) = x(atom(A),y(B,C)).
% 0.70/1.09 44 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 45 (wt=11) [] x2(atom(A),star(B)) = x(atom(A),star(B)).
% 0.70/1.09 45 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 46 (wt=9) [] x2(x(A,B),nil4) = x(A,B).
% 0.70/1.09 46 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 47 (wt=11) [] x2(x(A,B),eps) = x(x(A,B),eps).
% 0.70/1.09 47 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 48 (wt=13) [] x2(x(A,B),atom(C)) = x(x(A,B),atom(C)).
% 0.70/1.09 48 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 49 (wt=15) [] x2(x(A,B),x(C,D)) = x(x(A,B),x(C,D)).
% 0.70/1.09 49 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 50 (wt=15) [] x2(x(A,B),y(C,D)) = x(x(A,B),y(C,D)).
% 0.70/1.09 50 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 51 (wt=13) [] x2(x(A,B),star(C)) = x(x(A,B),star(C)).
% 0.70/1.09 51 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 52 (wt=9) [] x2(y(A,B),nil4) = y(A,B).
% 0.70/1.09 52 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 53 (wt=11) [] x2(y(A,B),eps) = x(y(A,B),eps).
% 0.70/1.09 53 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 54 (wt=13) [] x2(y(A,B),atom(C)) = x(y(A,B),atom(C)).
% 0.70/1.09 54 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 55 (wt=15) [] x2(y(A,B),x(C,D)) = x(y(A,B),x(C,D)).
% 0.70/1.09 55 is a new demodulator.
% 0.70/1.09
% 0.70/1.09 ** KEPT: 56 (wt=15) [] x2(y(A,B),y(C,D)) = x(y(A,B),y(C,D)).
% 0.70/1.10 56 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 57 (wt=13) [] x2(y(A,B),star(C)) = x(y(A,B),star(C)).
% 0.70/1.10 57 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 58 (wt=7) [] x2(star(A),nil4) = star(A).
% 0.70/1.10 58 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 59 (wt=9) [] x2(star(A),eps) = x(star(A),eps).
% 0.70/1.10 59 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 60 (wt=11) [] x2(star(A),atom(B)) = x(star(A),atom(B)).
% 0.70/1.10 60 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 61 (wt=13) [] x2(star(A),x(B,C)) = x(star(A),x(B,C)).
% 0.70/1.10 61 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 62 (wt=13) [] x2(star(A),y(B,C)) = x(star(A),y(B,C)).
% 0.70/1.10 62 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 63 (wt=11) [] x2(star(A),star(B)) = x(star(A),star(B)).
% 0.70/1.10 63 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 64 (wt=5) [] splits(A,nil) = nil.
% 0.70/1.10 64 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 65 (wt=17) [] splits(A,cons(pair2(B,C),D)) = cons(pair2(cons2(A,B),C),splits(A,D)).
% 0.70/1.10 65 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 66 (wt=8) [] splits2(nil2) = cons(pair2(nil2,nil2),nil).
% 0.70/1.10 66 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 67 (wt=15) [] splits2(cons2(A,B)) = cons(pair2(nil2,cons2(A,B)),splits(A,splits2(B))).
% 0.70/1.10 67 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 68 (wt=5) [] orb(btrue,A) = btrue.
% 0.70/1.10 68 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 69 (wt=5) [] orb(bfalse,A) = A.
% 0.70/1.10 69 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 70 (wt=4) [] or2(nil3) = bfalse.
% 0.70/1.10 70 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 71 (wt=9) [] or2(cons3(A,B)) = orb(A,or2(B)).
% 0.70/1.10 71 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 72 (wt=4) [] notb(btrue) = bfalse.
% 0.70/1.10 72 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 73 (wt=4) [] notb(bfalse) = btrue.
% 0.70/1.10 73 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 74 (wt=5) [] andb(btrue,A) = A.
% 0.70/1.10 74 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 75 (wt=5) [] andb(bfalse,A) = bfalse.
% 0.70/1.10 75 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 76 (wt=4) [] eps2(eps) = btrue.
% 0.70/1.10 76 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 77 (wt=10) [] eps2(x(A,B)) = orb(eps2(A),eps2(B)).
% 0.70/1.10 77 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 78 (wt=10) [] eps2(y(A,B)) = andb(eps2(A),eps2(B)).
% 0.70/1.10 78 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 79 (wt=5) [] eps2(star(A)) = btrue.
% 0.70/1.10 79 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 80 (wt=4) [] eps2(nil4) = bfalse.
% 0.70/1.10 80 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 81 (wt=5) [] eps2(atom(A)) = bfalse.
% 0.70/1.10 81 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 82 (wt=11) [] step(atom(A),B) = aux(B,A,eq(A,B)).
% 0.70/1.10 82 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 83 (wt=13) [flip(1)] x(step(A,B),step(C,B)) = step(x(A,C),B).
% 0.70/1.10 83 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 84 (wt=12) [] step(y(A,B),C) = aux2(C,A,B,eps2(A)).
% 0.70/1.10
% 0.70/1.10 ** KEPT: 85 (wt=12) [flip(84)] aux2(A,B,C,eps2(B)) = step(y(B,C),A).
% 0.70/1.10 clause forward subsumed: 0 (wt=12) [flip(85)] step(y(B,C),A) = aux2(A,B,C,eps2(B)).
% 0.70/1.10
% 0.70/1.10 ** KEPT: 86 (wt=11) [flip(1)] y(step(A,B),star(A)) = step(star(A),B).
% 0.70/1.10 86 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 87 (wt=5) [] step(nil4,A) = nil4.
% 0.70/1.10 87 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 88 (wt=5) [] step(eps,A) = nil4.
% 0.70/1.10 88 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 89 (wt=6) [flip(1)] eps2(A) = rec(A,nil2).
% 0.70/1.10 89 is a new demodulator.
% 0.70/1.10 -> 89 back demodulating 85.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 90 (wt=13) [back_demod(85),demod([89]),flip(1)] step(y(A,B),C) = aux2(C,A,B,rec(A,nil2)).
% 0.70/1.10 90 is a new demodulator.
% 0.70/1.10 -> 90 back demodulating 84.
% 0.70/1.10 clause forward subsumed: 0 (wt=15) [back_demod(84),demod([90,89])] aux2(C,A,B,rec(A,nil2)) = aux2(C,A,B,rec(A,nil2)).
% 0.70/1.10 -> 89 back demodulating 81.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 91 (wt=6) [back_demod(81),demod([89])] rec(atom(A),nil2) = bfalse.
% 0.70/1.10 91 is a new demodulator.
% 0.70/1.10 -> 89 back demodulating 80.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 92 (wt=5) [back_demod(80),demod([89])] rec(nil4,nil2) = bfalse.
% 0.70/1.10 92 is a new demodulator.
% 0.70/1.10 -> 89 back demodulating 79.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 93 (wt=6) [back_demod(79),demod([89])] rec(star(A),nil2) = btrue.
% 0.70/1.10 93 is a new demodulator.
% 0.70/1.10 -> 89 back demodulating 78.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 94 (wt=13) [back_demod(78),demod([89,89,89])] rec(y(A,B),nil2) = andb(rec(A,nil2),rec(B,nil2)).
% 0.70/1.10 94 is a new demodulator.
% 0.70/1.10 -> 89 back demodulating 77.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 95 (wt=13) [back_demod(77),demod([89,89,89])] rec(x(A,B),nil2) = orb(rec(A,nil2),rec(B,nil2)).
% 0.70/1.10 95 is a new demodulator.
% 0.70/1.10 -> 89 back demodulating 76.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 96 (wt=5) [back_demod(76),demod([89])] rec(eps,nil2) = btrue.
% 0.70/1.10 96 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 97 (wt=11) [flip(1)] rec(step(A,B),C) = rec(A,cons2(B,C)).
% 0.70/1.10 97 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 98 (wt=6) [] reck(A,B,nil) = nil3.
% 0.70/1.10 98 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 99 (wt=21) [] reck(A,B,cons(pair2(C,D),E)) = cons3(andb(reck2(A,C),rec(B,D)),reck(A,B,E)).
% 0.70/1.10
% 0.70/1.10 ** KEPT: 100 (wt=21) [flip(99)] cons3(andb(reck2(A,B),rec(C,D)),reck(A,C,E)) = reck(A,C,cons(pair2(B,D),E)).
% 0.70/1.10 clause forward subsumed: 0 (wt=21) [flip(100)] reck(A,C,cons(pair2(B,D),E)) = cons3(andb(reck2(A,B),rec(C,D)),reck(A,C,E)).
% 0.70/1.10
% 0.70/1.10 ** KEPT: 101 (wt=5) [] reck2(nil4,A) = bfalse.
% 0.70/1.10 101 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 102 (wt=5) [] reck2(eps,nil2) = btrue.
% 0.70/1.10 102 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 103 (wt=7) [] reck2(eps,cons2(A,B)) = bfalse.
% 0.70/1.10 103 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 104 (wt=6) [] reck2(atom(A),nil2) = bfalse.
% 0.70/1.10 104 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 105 (wt=10) [] reck2(atom(A),cons2(B,nil2)) = eq(A,B).
% 0.70/1.10 105 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 106 (wt=10) [] reck2(atom(A),cons2(B,cons2(C,D))) = bfalse.
% 0.70/1.10 106 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 107 (wt=13) [] reck2(x(A,B),C) = orb(reck2(A,C),reck2(B,C)).
% 0.70/1.10 107 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 108 (wt=12) [flip(1)] or2(reck(A,B,splits2(C))) = reck2(y(A,B),C).
% 0.70/1.10 108 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 109 (wt=6) [] reck2(star(A),nil2) = btrue.
% 0.70/1.10 109 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 110 (wt=15) [demod([89])] reck2(star(A),cons2(B,C)) = aux3(A,B,C,notb(rec(A,nil2))).
% 0.70/1.10 110 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 111 (wt=11) [flip(1)] eq2(rec(A,B),reck2(A,B)) = prop_same(A,B).
% 0.70/1.10 111 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 112 (wt=5) [] eq(a,b) = bfalse.
% 0.70/1.10 112 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 113 (wt=5) [] eq(a,c) = bfalse.
% 0.70/1.10 113 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 114 (wt=5) [] eq(b,a) = bfalse.
% 0.70/1.10 114 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 115 (wt=5) [] eq(b,c) = bfalse.
% 0.70/1.10 115 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 116 (wt=5) [] eq(c,a) = bfalse.
% 0.70/1.10 116 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 117 (wt=5) [] eq(c,b) = bfalse.
% 0.70/1.10 117 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 118 (wt=5) [] eq2(bfalse,btrue) = bfalse.
% 0.70/1.10 118 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 119 (wt=5) [] eq2(btrue,bfalse) = bfalse.
% 0.70/1.10 119 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 120 (wt=5) [] eq(A,A) = btrue.
% 0.70/1.10 120 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 121 (wt=5) [] eq2(A,A) = btrue.
% 0.70/1.10 121 is a new demodulator.
% 0.70/1.10
% 0.70/1.10 ** KEPT: 122 (wt=7) [] -(eq2(prop_same(A,B),bfalse) = btrue).
% 0.70/1.10
% 0.70/1.10 After processing input:
% 0.70/1.10
% 0.70/1.10 Usable:
% 0.70/1.10 end_of_list.
% 0.70/1.10
% 0.70/1.10 Sos:
% 0.70/1.10 70 (wt=4) [] or2(nil3) = bfalse.
% 0.70/1.10 72 (wt=4) [] notb(btrue) = bfalse.
% 0.70/1.10 73 (wt=4) [] notb(bfalse) = btrue.
% 0.70/1.10 7 (wt=5) [] z(nil4,A) = nil4.
% 0.70/1.10 8 (wt=5) [] z(eps,A) = A.
% 0.70/1.10 33 (wt=5) [] x2(nil4,A) = A.
% 0.70/1.10 34 (wt=5) [] x2(eps,nil4) = eps.
% 0.70/1.10 64 (wt=5) [] splits(A,nil) = nil.
% 0.70/1.10 68 (wt=5) [] orb(btrue,A) = btrue.
% 0.70/1.10 69 (wt=5) [] orb(bfalse,A) = A.
% 0.70/1.10 74 (wt=5) [] andb(btrue,A) = A.
% 0.70/1.10 75 (wt=5) [] andb(bfalse,A) = bfalse.
% 0.70/1.10 87 (wt=5) [] step(nil4,A) = nil4.
% 0.70/1.10 88 (wt=5) [] step(eps,A) = nil4.
% 0.70/1.10 92 (wt=5) [back_demod(80),demod([89])] rec(nil4,nil2) = bfalse.
% 0.70/1.10 96 (wt=5) [back_demod(76),demod([89])] rec(eps,nil2) = btrue.
% 0.70/1.10 101 (wt=5) [] reck2(nil4,A) = bfalse.
% 0.70/1.10 102 (wt=5) [] reck2(eps,nil2) = btrue.
% 0.70/1.10 112 (wt=5) [] eq(a,b) = bfalse.
% 0.70/1.10 113 (wt=5) [] eq(a,c) = bfalse.
% 0.70/1.10 114 (wt=5) [] eq(b,a) = bfalse.
% 0.70/1.10 115 (wt=5) [] eq(b,c) = bfalse.
% 0.70/1.10 116 (wt=5) [] eq(c,a) = bfalse.
% 0.70/1.10 117 (wt=5) [] eq(c,b) = bfalse.
% 0.70/1.10 118 (wt=5) [] eq2(bfalse,btrue) = bfalse.
% 0.70/1.10 119 (wt=5) [] eq2(btrue,bfalse) = bfalse.
% 0.70/1.10 120 (wt=5) [] eq(A,A) = btrue.
% 0.70/1.10 121 (wt=5) [] eq2(A,A) = btrue.
% 0.70/1.10 1 (wt=6) [] aux(A,B,btrue) = eps.
% 0.70/1.10 2 (wt=6) [] aux(A,B,bfalse) = nil4.
% 0.70/1.10 9 (wt=6) [] z(atom(A),nil4) = nil4.
% 0.70/1.10 27 (wt=6) [] z(star(A),nil4) = nil4.
% 0.70/1.10 89 (wt=6) [flip(1)] eps2(A) = rec(A,nil2).
% 0.70/1.10 91 (wt=6) [back_demod(81),demod([89])] rec(atom(A),nil2) = bfalse.
% 0.70/1.10 93 (wt=6) [back_demod(79),demod([89])] rec(star(A),nil2) = btrue.
% 0.70/1.10 98 (wt=6) [] reck(A,B,nil) = nil3.
% 0.70/1.10 104 (wt=6) [] reck2(atom(A),nil2) = bfalse.
% 0.70/1.10 109 (wt=6) [] reck2(star(A),nil2) = btrue.
% 0.70/1.10 6 (wt=7) [] aux3(A,B,C,bfalse) = bfalse.
% 0.70/1.10 10 (wt=7) [] z(atom(A),eps) = atom(A).
% 0.70/1.10 15 (wt=7) [] z(x(A,B),nil4) = nil4.
% 0.70/1.10 21 (wt=7) [] z(y(A,B),nil4) = nil4.
% 0.70/1.10 28 (wt=7) [] z(star(A),eps) = star(A).
% 0.70/1.10 35 (wt=7) [] x2(eps,eps) = x(eps,eps).
% 0.70/1.10 40 (wt=7) [] x2(atom(A),nil4) = atom(A).
% 0.70/1.10 58 (wt=7) [] x2(star(A),nil4) = star(A).
% 0.70/1.10 103 (wt=7) [] reck2(eps,cons2(A,B)) = bfalse.
% 0.70/1.10 122 (wt=7) [] -(eq2(prop_same(A,B),bfalse) = btrue).
% 0.70/1.10 66 (wt=8) [] splits2(nil2) = cons(pair2(nil2,nil2),nil).
% 0.70/1.10 16 (wt=9) [] z(x(A,B),eps) = x(A,B).
% 0.70/1.10 22 (wt=9) [] z(y(A,B),eps) = y(A,B).
% 0.70/1.10 36 (wt=9) [] x2(eps,atom(A)) = x(eps,atom(A)).
% 0.70/1.10 39 (wt=9) [] x2(eps,star(A)) = x(eps,star(A)).
% 0.70/1.10 41 (wt=9) [] x2(atom(A),eps) = x(atom(A),eps).
% 0.70/1.10 46 (wt=9) [] x2(x(A,B),nil4) = x(A,B).
% 0.70/1.10 52 (wt=9) [] x2(y(A,B),nil4) = y(A,B).
% 0.70/1.10 59 (wt=9) [] x2(star(A),eps) = x(star(A),eps).
% 0.70/1.10 71 (wt=9) [] or2(cons3(A,B)) = orb(A,or2(B)).
% 0.70/1.10 105 (wt=10) [] reck2(atom(A),cons2(B,nil2)) = eq(A,B).
% 0.70/1.10 106 (wt=10) [] reck2(atom(A),cons2(B,cons2(C,D))) = bfalse.
% 0.70/1.10 11 (wt=11) [] z(atom(A),atom(B)) = y(atom(A),atom(B)).
% 0.70/1.10 14 (wt=11) [] z(atom(A),star(B)) = y(atom(A),star(B)).
% 0.70/1.10 29 (wt=11) [] z(star(A),atom(B)) = y(star(A),atom(B)).
% 0.70/1.10 32 (wt=11) [] z(star(A),star(B)) = y(star(A),star(B)).
% 0.70/1.10 37 (wt=11) [] x2(eps,x(A,B)) = x(eps,x(A,B)).
% 0.70/1.10 38 (wt=11) [] x2(eps,y(A,B)) = x(eps,y(A,B)).
% 0.70/1.10 42 (wt=11) [] x2(atom(A),atom(B)) = x(atom(A),atom(B)).
% 0.70/1.10 45 (wt=11) [] x2(atom(A),star(B)) = x(atom(A),star(B)).
% 0.70/1.10 47 (wt=11) [] x2(x(A,B),eps) = x(x(A,B),eps).
% 0.70/1.10 53 (wt=11) [] x2(y(A,B),eps) = x(y(A,B),eps).
% 0.70/1.10 60 (wt=11) [] x2(star(A),atom(B)) = x(star(A),atom(B)).
% 0.70/1.10 63 (wt=11) [] x2(star(A),star(B)) = x(star(A),star(B)).
% 0.70/1.10 82 (wt=11) [] step(atom(A),B) = aux(B,A,eq(A,B)).
% 0.70/1.10 86 (wt=11) [flip(1)] y(step(A,B),star(A)) = step(star(A),B).
% 0.70/1.10 97 (wt=11) [flip(1)] rec(step(A,B),C) = rec(A,cons2(B,C)).
% 0.70/1.10 111 (wt=11) [flip(1)] eq2(rec(A,B),reck2(A,B)) = prop_same(A,B).
% 0.70/1.10 108 (wt=12) [flip(1)] or2(reck(A,B,splits2(C))) = reck2(y(A,B),C).
% 0.70/1.10 4 (wt=13) [flip(1)] x(y(step(A,B),C),nil4) = aux2(B,A,C,bfalse).
% 0.70/1.10 12 (wt=13) [] z(atom(A),x(B,C)) = y(atom(A),x(B,C)).
% 0.70/1.10 13 (wt=13) [] z(atom(A),y(B,C)) = y(atom(A),y(B,C)).
% 0.70/1.10 17 (wt=13) [] z(x(A,B),atom(C)) = y(x(A,B),atom(C)).
% 0.70/1.10 20 (wt=13) [] z(x(A,B),star(C)) = y(x(A,B),star(C)).
% 0.70/1.10 23 (wt=13) [] z(y(A,B),atom(C)) = y(y(A,B),atom(C)).
% 0.70/1.10 26 (wt=13) [] z(y(A,B),star(C)) = y(y(A,B),star(C)).
% 0.70/1.10 30 (wt=13) [] z(star(A),x(B,C)) = y(star(A),x(B,C)).
% 0.70/1.10 31 (wt=13) [] z(star(A),y(B,C)) = y(star(A),y(B,C)).
% 0.70/1.10 43 (wt=13) [] x2(atom(A),x(B,C)) = x(atom(A),x(B,C)).
% 0.70/1.10 44 (wt=13) [] x2(atom(A),y(B,C)) = x(atom(A),y(B,C)).
% 0.70/1.10 48 (wt=13) [] x2(x(A,B),atom(C)) = x(x(A,B),atom(C)).
% 0.70/1.10 51 (wt=13) [] x2(x(A,B),star(C)) = x(x(A,B),star(C)).
% 0.70/1.10 54 (wt=13) [] x2(y(A,B),atom(C)) = x(y(A,B),atom(C)).
% 0.70/1.10 57 (wt=13) [] x2(y(A,B),star(C)) = x(y(A,B),star(C)).
% 0.70/1.10 61 (wt=13) [] x2(star(A),x(B,C)) = x(star(A),x(B,C)).
% 0.70/1.10 62 (wt=13) [] x2(star(A),y(B,C)) = x(star(A),y(B,C)).
% 0.70/1.10 83 (wt=13) [flip(1)] x(step(A,B),step(C,B)) = step(x(A,C),B).
% 0.70/1.10 90 (wt=13) [back_demod(85),demod([89]),flip(1)] step(y(A,B),C) = aux2(C,A,B,rec(A,nil2)).
% 0.70/1.10 94 (wt=13) [back_demod(78),demod([89,89,89])] rec(y(A,B),nil2) = andb(rec(A,nil2),rec(B,nil2)).
% 0.70/1.10 95 (wt=13) [back_demod(77),demod([89,89,89])] rec(x(A,B),nil2) = orb(rec(A,nil2),rec(B,nil2)).
% 0.70/1.10 107 (wt=13) [] reck2(x(A,B),C) = orb(reck2(A,C),reck2(B,C)).
% 0.70/1.10 5 (wt=14) [flip(1)] rec(y(A,star(A)),cons2(B,C)) = aux3(A,B,C,btrue).
% 0.70/1.10 3 (wt=15) [flip(1)] x(y(step(A,B),C),step(C,B)) = aux2(B,A,C,btrue).
% 0.70/1.10 18 (wt=15) [] z(x(A,B),x(C,D)) = y(x(A,B),x(C,D)).
% 0.70/1.10 19 (wt=15) [] z(x(A,B),y(C,D)) = y(x(A,B),y(C,D)).
% 0.70/1.10 24 (wt=15) [] z(y(A,B),x(C,D)) = y(y(A,B),x(C,D)).
% 0.70/1.10 25 (wt=15) [] z(y(A,B),y(C,D)) = y(y(A,B),y(C,D)).
% 0.70/1.10 49 (wt=15) [] x2(x(A,B),x(C,D)) = x(x(A,B),x(C,D)).
% 0.70/1.10 50 (wt=15) [] x2(x(A,B),y(C,D)) = x(x(A,B),y(C,D)).
% 0.70/1.10 55 (wt=15) [] x2(y(A,B),x(C,D)) = x(y(A,B),x(C,D)).
% 0.70/1.10 56 (wt=15) [] x2(y(A,B),y(C,D)) = x(y(A,B),y(C,D)).
% 0.70/1.10 67 (wt=15) [] splits2(cons2(A,B)) = cons(pair2(nil2,cons2(A,B)),splits(A,splits2(B))).
% 0.70/1.10 110 (wt=15) [demod([89])] reck2(star(A),cons2(B,C)) = aux3(A,B,C,notb(rec(A,nil2))).
% 0.70/1.10 65 (wt=17) [] splits(A,cons(pair2(B,C),D)) = cons(pair2(cons2(A,B),C),splits(A,D)).
% 0.70/1.10 99 (wt=21) [] reck(A,B,cons(pair2(C,D),E)) = cons3(andb(reck2(A,C),rec(B,D)),reck(A,B,E)).
% 0.70/1.10 100 (wt=21) [flip(99)] cons3(andb(reck2(A,B),rec(C,D)),reck(A,C,E)) = reck(A,C,cons(pair2(B,D),E)).
% 0.70/1.10 end_of_list.
% 0.70/1.10
% 0.70/1.10 Demodulators:
% 0.70/1.10 1 (wt=6) [] aux(A,B,btrue) = eps.
% 0.70/1.10 2 (wt=6) [] aux(A,B,bfalse) = nil4.
% 0.70/1.10 3 (wt=15) [flip(1)] x(y(step(A,B),C),step(C,B)) = aux2(B,A,C,btrue).
% 0.70/1.10 4 (wt=13) [flip(1)] x(y(step(A,B),C),nil4) = aux2(B,A,C,bfalse).
% 0.70/1.10 5 (wt=14) [flip(1)] rec(y(A,star(A)),cons2(B,C)) = aux3(A,B,C,btrue).
% 0.70/1.10 6 (wt=7) [] aux3(A,B,C,bfalse) = bfalse.
% 0.70/1.10 7 (wt=5) [] z(nil4,A) = nil4.
% 0.70/1.10 8 (wt=5) [] z(eps,A) = A.
% 0.70/1.10 9 (wt=6) [] z(atom(A),nil4) = nil4.
% 0.70/1.10 10 (wt=7) [] z(atom(A),eps) = atom(A).
% 0.70/1.10 11 (wt=11) [] z(atom(A),atom(B)) = y(atom(A),atom(B)).
% 0.70/1.10 12 (wt=13) [] z(atom(A),x(B,C)) = y(atom(A),x(B,C)).
% 0.70/1.10 13 (wt=13) [] z(atom(A),y(B,C)) = y(atom(A),y(B,C)).
% 0.70/1.10 14 (wt=11) [] z(atom(A),star(B)) = y(atom(A),star(B)).
% 0.70/1.10 15 (wt=7) [] z(x(A,B),nil4) = nil4.
% 0.70/1.10 16 (wt=9) [] z(x(A,B),eps) = x(A,B).
% 0.70/1.10 17 (wt=13) [] z(x(A,B),atom(C)) = y(x(A,B),atom(C)).
% 0.70/1.10 18 (wt=15) [] z(x(A,B),x(C,D)) = y(x(A,B),x(C,D)).
% 0.70/1.10 19 (wt=15) [] z(x(A,B),y(C,D)) = y(x(A,B),y(C,D)).
% 0.70/1.10 20 (wt=13) [] z(x(A,B),star(C)) = y(x(A,B),star(C)).
% 0.70/1.10 21 (wt=7) [] z(y(A,B),nil4) = nil4.
% 0.70/1.10 22 (wt=9) [] z(y(A,B),eps) = y(A,B).
% 0.70/1.10 23 (wt=13) [] z(y(A,B),atom(C)) = y(y(A,B),atom(C)).
% 0.70/1.10 24 (wt=15) [] z(y(A,B),x(C,D)) = y(y(A,B),x(C,D)).
% 0.70/1.10 25 (wt=15) [] z(y(A,B),y(C,D)) = y(y(A,B),y(C,D)).
% 0.70/1.10 26 (wt=13) [] z(y(A,B),star(C)) = y(y(A,B),star(C)).
% 0.70/1.10 27 (wt=6) [] z(star(A),nil4) = nil4.
% 0.70/1.10 28 (wt=7) [] z(star(A),eps) = star(A).
% 0.70/1.10 29 (wt=11) [] z(star(A),atom(B)) = y(star(A),atom(B)).
% 0.70/1.10 30 (wt=13) [] z(star(A),x(B,C)) = y(star(A),x(B,C)).
% 0.70/1.10 31 (wt=13) [] z(star(A),y(B,C)) = y(star(A),y(B,C)).
% 0.70/1.10 32 (wt=11) [] z(star(A),star(B)) = y(star(A),star(B)).
% 0.70/1.10 33 (wt=5) [] x2(nil4,A) = A.
% 0.70/1.10 34 (wt=5) [] x2(eps,nil4) = eps.
% 0.70/1.10 35 (wt=7) [] x2(eps,eps) = x(eps,eps).
% 0.70/1.10 36 (wt=9) [] x2(eps,atom(A)) = x(eps,atom(A)).
% 0.70/1.10 37 (wt=11) [] x2(eps,x(A,B)) = x(eps,x(A,B)).
% 0.70/1.10 38 (wt=11) [] x2(eps,y(A,B)) = x(eps,y(A,B)).
% 0.70/1.10 39 (wt=9) [] x2(eps,star(A)) = x(eps,star(A)).
% 0.70/1.10 40 (wt=7) [] x2(atom(A),nil4) = atom(A).
% 0.70/1.10 41 (wt=9) [] x2(atom(A),eps) = x(atom(A),eps).
% 0.70/1.10 42 (wt=11) [] x2(atom(A),atom(B)) = x(atom(A),atom(B)).
% 0.70/1.10 43 (wt=13) [] x2(atom(A),x(B,C)) = x(atom(A),x(B,C)).
% 0.70/1.10 44 (wt=13) [] x2(atom(A),y(B,C)) = x(atom(A),y(B,C)).
% 0.70/1.10 45 (wt=11) [] x2(atom(A),star(B)) = x(atom(A),star(B)).
% 0.70/1.10 46 (wt=9) [] x2(x(A,B),nil4) = x(A,B).
% 0.70/1.10 47 (wt=11) [] x2(x(A,B),eps) = x(x(A,B),eps).
% 0.70/1.10 48 (wt=13) [] x2(x(A,B),atom(C)) = x(x(A,B),atom(C)).
% 0.70/1.10 49 (wt=15) [] x2(x(A,B),x(C,D)) = x(x(A,B),x(C,D)).
% 0.70/1.10 50 (wt=15) [] x2(x(A,B),y(C,D)) = x(x(A,B),y(C,D)).
% 0.70/1.10 51 (wt=13) [] x2(x(A,B),star(C)) = x(x(A,B),star(C)).
% 15.45/15.85 52 (wt=9) [] x2(y(A,B),nil4) = y(A,B).
% 15.45/15.85 ---------------- PROOF FOUND ----------------
% 15.45/15.85 % SZS status Unsatisfiable
% 15.45/15.85
% 15.45/15.85 53 (wt=11) [] x2(y(A,B),eps) = x(y(A,B),eps).
% 15.45/15.85 54 (wt=13) [] x2(y(A,B),atom(C)) = x(y(A,B),atom(C)).
% 15.45/15.85 55 (wt=15) [] x2(y(A,B),x(C,D)) = x(y(A,B),x(C,D)).
% 15.45/15.85 56 (wt=15) [] x2(y(A,B),y(C,D)) = x(y(A,B),y(C,D)).
% 15.45/15.85 57 (wt=13) [] x2(y(A,B),star(C)) = x(y(A,B),star(C)).
% 15.45/15.85 58 (wt=7) [] x2(star(A),nil4) = star(A).
% 15.45/15.85 59 (wt=9) [] x2(star(A),eps) = x(star(A),eps).
% 15.45/15.85 60 (wt=11) [] x2(star(A),atom(B)) = x(star(A),atom(B)).
% 15.45/15.85 61 (wt=13) [] x2(star(A),x(B,C)) = x(star(A),x(B,C)).
% 15.45/15.85 62 (wt=13) [] x2(star(A),y(B,C)) = x(star(A),y(B,C)).
% 15.45/15.85 63 (wt=11) [] x2(star(A),star(B)) = x(star(A),star(B)).
% 15.45/15.85 64 (wt=5) [] splits(A,nil) = nil.
% 15.45/15.85 65 (wt=17) [] splits(A,cons(pair2(B,C),D)) = cons(pair2(cons2(A,B),C),splits(A,D)).
% 15.45/15.85 66 (wt=8) [] splits2(nil2) = cons(pair2(nil2,nil2),nil).
% 15.45/15.85 67 (wt=15) [] splits2(cons2(A,B)) = cons(pair2(nil2,cons2(A,B)),splits(A,splits2(B))).
% 15.45/15.85 68 (wt=5) [] orb(btrue,A) = btrue.
% 15.45/15.85 69 (wt=5) [] orb(bfalse,A) = A.
% 15.45/15.85 70 (wt=4) [] or2(nil3) = bfalse.
% 15.45/15.85 71 (wt=9) [] or2(cons3(A,B)) = orb(A,or2(B)).
% 15.45/15.85 72 (wt=4) [] notb(btrue) = bfalse.
% 15.45/15.85 73 (wt=4) [] notb(bfalse) = btrue.
% 15.45/15.85 74 (wt=5) [] andb(btrue,A) = A.
% 15.45/15.85 75 (wt=5) [] andb(bfalse,A) = bfalse.
% 15.45/15.85 82 (wt=11) [] step(atom(A),B) = aux(B,A,eq(A,B)).
% 15.45/15.85 83 (wt=13) [flip(1)] x(step(A,B),step(C,B)) = step(x(A,C),B).
% 15.45/15.85 86 (wt=11) [flip(1)] y(step(A,B),star(A)) = step(star(A),B).
% 15.45/15.85 87 (wt=5) [] step(nil4,A) = nil4.
% 15.45/15.85 88 (wt=5) [] step(eps,A) = nil4.
% 15.45/15.85 89 (wt=6) [flip(1)] eps2(A) = rec(A,nil2).
% 15.45/15.85 90 (wt=13) [back_demod(85),demod([89]),flip(1)] step(y(A,B),C) = aux2(C,A,B,rec(A,nil2)).
% 15.45/15.85 91 (wt=6) [back_demod(81),demod([89])] rec(atom(A),nil2) = bfalse.
% 15.45/15.85 92 (wt=5) [back_demod(80),demod([89])] rec(nil4,nil2) = bfalse.
% 15.45/15.85 93 (wt=6) [back_demod(79),demod([89])] rec(star(A),nil2) = btrue.
% 15.45/15.85 94 (wt=13) [back_demod(78),demod([89,89,89])] rec(y(A,B),nil2) = andb(rec(A,nil2),rec(B,nil2)).
% 15.45/15.85 95 (wt=13) [back_demod(77),demod([89,89,89])] rec(x(A,B),nil2) = orb(rec(A,nil2),rec(B,nil2)).
% 15.45/15.85 96 (wt=5) [back_demod(76),demod([89])] rec(eps,nil2) = btrue.
% 15.45/15.85 97 (wt=11) [flip(1)] rec(step(A,B),C) = rec(A,cons2(B,C)).
% 15.45/15.85 98 (wt=6) [] reck(A,B,nil) = nil3.
% 15.45/15.85 101 (wt=5) [] reck2(nil4,A) = bfalse.
% 15.45/15.85 102 (wt=5) [] reck2(eps,nil2) = btrue.
% 15.45/15.85 103 (wt=7) [] reck2(eps,cons2(A,B)) = bfalse.
% 15.45/15.85 104 (wt=6) [] reck2(atom(A),nil2) = bfalse.
% 15.45/15.85 105 (wt=10) [] reck2(atom(A),cons2(B,nil2)) = eq(A,B).
% 15.45/15.85 106 (wt=10) [] reck2(atom(A),cons2(B,cons2(C,D))) = bfalse.
% 15.45/15.85 107 (wt=13) [] reck2(x(A,B),C) = orb(reck2(A,C),reck2(B,C)).
% 15.45/15.85 108 (wt=12) [flip(1)] or2(reck(A,B,splits2(C))) = reck2(y(A,B),C).
% 15.45/15.85 109 (wt=6) [] reck2(star(A),nil2) = btrue.
% 15.45/15.85 110 (wt=15) [demod([89])] reck2(star(A),cons2(B,C)) = aux3(A,B,C,notb(rec(A,nil2))).
% 15.45/15.85 111 (wt=11) [flip(1)] eq2(rec(A,B),reck2(A,B)) = prop_same(A,B).
% 15.45/15.85 112 (wt=5) [] eq(a,b) = bfalse.
% 15.45/15.85 113 (wt=5) [] eq(a,c) = bfalse.
% 15.45/15.85 114 (wt=5) [] eq(b,a) = bfalse.
% 15.45/15.85 115 (wt=5) [] eq(b,c) = bfalse.
% 15.45/15.85 116 (wt=5) [] eq(c,a) = bfalse.
% 15.45/15.85 117 (wt=5) [] eq(c,b) = bfalse.
% 15.45/15.85 118 (wt=5) [] eq2(bfalse,btrue) = bfalse.
% 15.45/15.85 119 (wt=5) [] eq2(btrue,bfalse) = bfalse.
% 15.45/15.85 120 (wt=5) [] eq(A,A) = btrue.
% 15.45/15.85 121 (wt=5) [] eq2(A,A) = btrue.
% 15.45/15.85 end_of_list.
% 15.45/15.85
% 15.45/15.85 Passive:
% 15.45/15.85 end_of_list.
% 15.45/15.85
% 15.45/15.85 UNIT CONFLICT from 28742 and x=x at 9.71 seconds.
% 15.45/15.85
% 15.45/15.85 ---------------- PROOF ----------------
% 15.45/15.85 % SZS output start Refutation
% See solution above
% 15.45/15.85 ------------ end of proof -------------
% 15.45/15.85
% 15.45/15.85
% 15.45/15.85 ------------- memory usage ------------
% 15.45/15.85 Memory dynamically allocated (tp_alloc): 52734.
% 15.45/15.85 type (bytes each) gets frees in use avail bytes
% 15.45/15.85 sym_ent ( 96) 106 0 106 0 9.9 K
% 15.45/15.85 term ( 16) 4055024 3264183 790841 62 15335.1 K
% 15.45/15.85 gen_ptr ( 8) 3849880 443235 3406645 28 26614.6 K
% 15.45/15.85 context ( 808) 22080208 22080206 2 8 7.9 K
% 15.45/15.85 trail ( 12) 21393 21393 0 7 0.1 K
% 15.45/15.85 bt_node ( 68) 10599229 10599224 5 17 1.5 K
% 15.45/15.85 ac_position (285432) 0 0 0 0 0.0 K
% 15.45/15.85 ac_match_pos (14044) 0 0 0 0 0.0 K
% 15.45/15.85 ac_match_free_vars_pos (4020)
% 15.45/15.85 0 0 0 0 0.0 K
% 15.45/15.85 discrim ( 12) 527496 12867 514629 0 6030.8 K
% 15.45/15.85 flat ( 40) 9010652 9010652 0 66 2.6 K
% 15.45/15.85 discrim_pos ( 12) 151295 151295 0 1 0.0 K
% 15.45/15.85 fpa_head ( 12) 45960 0 45960 0 538.6 K
% 15.45/15.85 fpa_tree ( 28) 58490 58490 0 25 0.7 K
% 15.45/15.85 fpa_pos ( 36) 35825 35825 0 1 0.0 K
% 15.45/15.85 literal ( 12) 201524 172782 28742 1 336.8 K
% 15.45/15.85 clause ( 24) 201524 172782 28742 1 673.7 K
% 15.45/15.85 list ( 12) 7143 7087 56 4 0.7 K
% 15.45/15.85 list_pos ( 20) 95558 4991 90567 0 1768.9 K
% 15.45/15.85 pair_index ( 40) 2 0 2 0 0.1 K
% 15.45/15.85
% 15.45/15.85 -------------- statistics -------------
% 15.45/15.85 Clauses input 113
% 15.45/15.85 Usable input 0
% 15.45/15.85 Sos input 113
% 15.45/15.85 Demodulators input 0
% 15.45/15.85 Passive input 0
% 15.45/15.85
% 15.45/15.85 Processed BS (before search) 125
% 15.45/15.85 Forward subsumed BS 3
% 15.45/15.85 Kept BS 122
% 15.45/15.85 New demodulators BS 117
% 15.45/15.85 Back demodulated BS 8
% 15.45/15.85
% 15.45/15.85 Clauses or pairs given 1635442
% 15.45/15.85 Clauses generated 99464
% 15.45/15.85 Forward subsumed 70844
% 15.45/15.85 Deleted by weight 0
% 15.45/15.85 Deleted by variable count 0
% 15.45/15.85 Kept 28620
% 15.45/15.85 New demodulators 6967
% 15.45/15.85 Back demodulated 1049
% 15.45/15.85 Ordered paramod prunes 0
% 15.45/15.85 Basic paramod prunes 6036676
% 15.45/15.85 Prime paramod prunes 2
% 15.45/15.85 Semantic prunes 0
% 15.45/15.85
% 15.45/15.85 Rewrite attmepts 2113352
% 15.45/15.85 Rewrites 107479
% 15.45/15.85
% 15.45/15.85 FPA overloads 0
% 15.45/15.85 FPA underloads 0
% 15.45/15.85
% 15.45/15.85 Usable size 0
% 15.45/15.85 Sos size 27684
% 15.45/15.85 Demodulators size 6458
% 15.45/15.85 Passive size 0
% 15.45/15.85 Disabled size 1057
% 15.45/15.85
% 15.45/15.85 Proofs found 1
% 15.45/15.85
% 15.45/15.85 ----------- times (seconds) ----------- Tue May 5 13:19:11 2026
% 15.45/15.85
% 15.45/15.85 user CPU time 9.71 (0 hr, 0 min, 9 sec)
% 15.45/15.86 system CPU time 5.05 (0 hr, 0 min, 5 sec)
% 15.45/15.86 wall-clock time 15 (0 hr, 0 min, 15 sec)
% 15.45/15.86 input time 0.00
% 15.45/15.86 paramodulation time 1.45
% 15.45/15.86 demodulation time 0.27
% 15.45/15.86 orient time 0.19
% 15.45/15.86 weigh time 0.04
% 15.45/15.86 forward subsume time 0.10
% 15.45/15.86 back demod find time 0.05
% 15.45/15.86 conflict time 0.02
% 15.45/15.86 LRPO time 0.08
% 15.45/15.86 store clause time 5.83
% 15.45/15.86 disable clause time 0.12
% 15.45/15.86 prime paramod time 0.08
% 15.45/15.86 semantics time 0.00
% 15.45/15.86
% 15.45/15.86 EQP interrupted
%------------------------------------------------------------------------------