%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : SWX239-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n014.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:04:38 PM UTC 2026
% Result : Unsatisfiable 0.86s 1.12s
% Output : CNFRefutation 0.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 48
% Syntax : Number of clauses : 161 ( 90 unt; 0 nHn; 79 RR)
% Number of literals : 265 ( 264 equ; 108 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 3 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 4 con; 0-4 aty)
% Number of variables : 228 ( 22 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(axiom,axiom,
aux(Y,B,btrue) = eps ).
cnf(axiom_005,axiom,
aux3(P2,X6,X7,bfalse) = bfalse ).
cnf(axiom_071,axiom,
notb(btrue) = bfalse ).
cnf(axiom_073,axiom,
andb(btrue,Q) = Q ).
cnf(axiom_075,axiom,
eps2(eps) = btrue ).
cnf(axiom_077,axiom,
eps2(y(R,Q2)) = andb(eps2(R),eps2(Q2)) ).
cnf(axiom_078,axiom,
eps2(star(Y)) = btrue ).
cnf(axiom_081,axiom,
step(atom(B),Y) = aux(Y,B,eq(B,Y)) ).
cnf(axiom_084,axiom,
step(star(P2),Y) = y(step(P2,Y),star(P2)) ).
cnf(axiom_087,axiom,
rec(X,nil2) = eps2(X) ).
cnf(axiom_088,axiom,
rec(X,cons2(Z,Xs)) = rec(step(X,Z),Xs) ).
cnf(axiom_100,axiom,
reck2(star(P2),cons2(X6,X7)) = aux3(P2,X6,X7,notb(eps2(P2))) ).
cnf(axiom_101,axiom,
prop_same(X,Y) = eq2(rec(X,Y),reck2(X,Y)) ).
cnf(axiom_109,axiom,
eq2(btrue,bfalse) = bfalse ).
cnf(axiom_110,axiom,
eq(X,X) = btrue ).
cnf(axiom_111,axiom,
eq2(X,X) = btrue ).
cnf(goal,negated_conjecture,
eq2(prop_same(X,Y),bfalse) != btrue ).
cnf(refute_0_0,plain,
eq2(prop_same(star(star(atom(X_343))),cons2(X_343,nil2)),bfalse) != btrue,
inference(subst,[],[goal:[bind(X,$fot(star(star(atom(X_343))))),bind(Y,$fot(cons2(X_343,nil2)))]]) ).
cnf(refute_0_1,plain,
prop_same(star(star(atom(X_342))),cons2(X_342,nil2)) = eq2(rec(star(star(atom(X_342))),cons2(X_342,nil2)),reck2(star(star(atom(X_342))),cons2(X_342,nil2))),
inference(subst,[],[axiom_101:[bind(X,$fot(star(star(atom(X_342))))),bind(Y,$fot(cons2(X_342,nil2)))]]) ).
cnf(refute_0_2,plain,
rec(step(star(star(atom(X_243))),X_243),nil2) = eps2(step(star(star(atom(X_243))),X_243)),
inference(subst,[],[axiom_087:[bind(X,$fot(step(star(star(atom(X_243))),X_243)))]]) ).
cnf(refute_0_3,plain,
eps2(y(X_41,eps)) = andb(eps2(X_41),eps2(eps)),
inference(subst,[],[axiom_077:[bind(Q2,$fot(eps)),bind(R,$fot(X_41))]]) ).
cnf(refute_0_4,plain,
( eps2(eps) != btrue
| eps2(y(X_41,eps)) != andb(eps2(X_41),eps2(eps))
| eps2(y(X_41,eps)) = andb(eps2(X_41),btrue) ),
introduced(tautology,[equality,[$cnf( $equal(eps2(y(X_41,eps)),andb(eps2(X_41),eps2(eps))) ),[1,1],$fot(btrue)]]) ).
cnf(refute_0_5,plain,
( eps2(y(X_41,eps)) != andb(eps2(X_41),eps2(eps))
| eps2(y(X_41,eps)) = andb(eps2(X_41),btrue) ),
inference(resolve,[$cnf( $equal(eps2(eps),btrue) )],[axiom_075,refute_0_4]) ).
cnf(refute_0_6,plain,
eps2(y(X_41,eps)) = andb(eps2(X_41),btrue),
inference(resolve,[$cnf( $equal(eps2(y(X_41,eps)),andb(eps2(X_41),eps2(eps))) )],[refute_0_3,refute_0_5]) ).
cnf(refute_0_7,plain,
eps2(y(step(star(atom(X_242)),X_242),eps)) = andb(eps2(step(star(atom(X_242)),X_242)),btrue),
inference(subst,[],[refute_0_6:[bind(X_41,$fot(step(star(atom(X_242)),X_242)))]]) ).
cnf(refute_0_8,plain,
eps2(y(eps,star(atom(X_241)))) = andb(eps2(eps),eps2(star(atom(X_241)))),
inference(subst,[],[axiom_077:[bind(Q2,$fot(star(atom(X_241)))),bind(R,$fot(eps))]]) ).
cnf(refute_0_9,plain,
step(star(atom(Y)),Y) = y(step(atom(Y),Y),star(atom(Y))),
inference(subst,[],[axiom_084:[bind(P2,$fot(atom(Y)))]]) ).
cnf(refute_0_10,plain,
step(atom(X_232),X_232) = aux(X_232,X_232,eq(X_232,X_232)),
inference(subst,[],[axiom_081:[bind(B,$fot(X_232)),bind(Y,$fot(X_232))]]) ).
cnf(refute_0_11,plain,
eq(X_232,X_232) = btrue,
inference(subst,[],[axiom_110:[bind(X,$fot(X_232))]]) ).
cnf(refute_0_12,plain,
( eq(X_232,X_232) != btrue
| step(atom(X_232),X_232) != aux(X_232,X_232,eq(X_232,X_232))
| step(atom(X_232),X_232) = aux(X_232,X_232,btrue) ),
introduced(tautology,[equality,[$cnf( $equal(step(atom(X_232),X_232),aux(X_232,X_232,eq(X_232,X_232))) ),[1,2],$fot(btrue)]]) ).
cnf(refute_0_13,plain,
( step(atom(X_232),X_232) != aux(X_232,X_232,eq(X_232,X_232))
| step(atom(X_232),X_232) = aux(X_232,X_232,btrue) ),
inference(resolve,[$cnf( $equal(eq(X_232,X_232),btrue) )],[refute_0_11,refute_0_12]) ).
cnf(refute_0_14,plain,
step(atom(X_232),X_232) = aux(X_232,X_232,btrue),
inference(resolve,[$cnf( $equal(step(atom(X_232),X_232),aux(X_232,X_232,eq(X_232,X_232))) )],[refute_0_10,refute_0_13]) ).
cnf(refute_0_15,plain,
aux(X_232,X_232,btrue) = eps,
inference(subst,[],[axiom:[bind(B,$fot(X_232)),bind(Y,$fot(X_232))]]) ).
cnf(refute_0_16,plain,
( aux(X_232,X_232,btrue) != eps
| step(atom(X_232),X_232) != aux(X_232,X_232,btrue)
| step(atom(X_232),X_232) = eps ),
introduced(tautology,[equality,[$cnf( $equal(step(atom(X_232),X_232),aux(X_232,X_232,btrue)) ),[1],$fot(eps)]]) ).
cnf(refute_0_17,plain,
( step(atom(X_232),X_232) != aux(X_232,X_232,btrue)
| step(atom(X_232),X_232) = eps ),
inference(resolve,[$cnf( $equal(aux(X_232,X_232,btrue),eps) )],[refute_0_15,refute_0_16]) ).
cnf(refute_0_18,plain,
step(atom(X_232),X_232) = eps,
inference(resolve,[$cnf( $equal(step(atom(X_232),X_232),aux(X_232,X_232,btrue)) )],[refute_0_14,refute_0_17]) ).
cnf(refute_0_19,plain,
step(atom(Y),Y) = eps,
inference(subst,[],[refute_0_18:[bind(X_232,$fot(Y))]]) ).
cnf(refute_0_20,plain,
( step(atom(Y),Y) != eps
| step(star(atom(Y)),Y) != y(step(atom(Y),Y),star(atom(Y)))
| step(star(atom(Y)),Y) = y(eps,star(atom(Y))) ),
introduced(tautology,[equality,[$cnf( $equal(step(star(atom(Y)),Y),y(step(atom(Y),Y),star(atom(Y)))) ),[1,0],$fot(eps)]]) ).
cnf(refute_0_21,plain,
( step(star(atom(Y)),Y) != y(step(atom(Y),Y),star(atom(Y)))
| step(star(atom(Y)),Y) = y(eps,star(atom(Y))) ),
inference(resolve,[$cnf( $equal(step(atom(Y),Y),eps) )],[refute_0_19,refute_0_20]) ).
cnf(refute_0_22,plain,
step(star(atom(Y)),Y) = y(eps,star(atom(Y))),
inference(resolve,[$cnf( $equal(step(star(atom(Y)),Y),y(step(atom(Y),Y),star(atom(Y)))) )],[refute_0_9,refute_0_21]) ).
cnf(refute_0_23,plain,
step(star(atom(X_241)),X_241) = y(eps,star(atom(X_241))),
inference(subst,[],[refute_0_22:[bind(Y,$fot(X_241))]]) ).
cnf(refute_0_24,plain,
X0 = X0,
introduced(tautology,[refl,[$fot(X0)]]) ).
cnf(refute_0_25,plain,
( X0 != X0
| X0 != Y0
| Y0 = X0 ),
introduced(tautology,[equality,[$cnf( $equal(X0,X0) ),[0],$fot(Y0)]]) ).
cnf(refute_0_26,plain,
( X0 != Y0
| Y0 = X0 ),
inference(resolve,[$cnf( $equal(X0,X0) )],[refute_0_24,refute_0_25]) ).
cnf(refute_0_27,plain,
( step(star(atom(X_241)),X_241) != y(eps,star(atom(X_241)))
| y(eps,star(atom(X_241))) = step(star(atom(X_241)),X_241) ),
inference(subst,[],[refute_0_26:[bind(X0,$fot(step(star(atom(X_241)),X_241))),bind(Y0,$fot(y(eps,star(atom(X_241)))))]]) ).
cnf(refute_0_28,plain,
y(eps,star(atom(X_241))) = step(star(atom(X_241)),X_241),
inference(resolve,[$cnf( $equal(step(star(atom(X_241)),X_241),y(eps,star(atom(X_241)))) )],[refute_0_23,refute_0_27]) ).
cnf(refute_0_29,plain,
( eps2(y(eps,star(atom(X_241)))) != andb(eps2(eps),eps2(star(atom(X_241))))
| y(eps,star(atom(X_241))) != step(star(atom(X_241)),X_241)
| eps2(step(star(atom(X_241)),X_241)) = andb(eps2(eps),eps2(star(atom(X_241)))) ),
introduced(tautology,[equality,[$cnf( $equal(eps2(y(eps,star(atom(X_241)))),andb(eps2(eps),eps2(star(atom(X_241))))) ),[0,0],$fot(step(star(atom(X_241)),X_241))]]) ).
cnf(refute_0_30,plain,
( eps2(y(eps,star(atom(X_241)))) != andb(eps2(eps),eps2(star(atom(X_241))))
| eps2(step(star(atom(X_241)),X_241)) = andb(eps2(eps),eps2(star(atom(X_241)))) ),
inference(resolve,[$cnf( $equal(y(eps,star(atom(X_241))),step(star(atom(X_241)),X_241)) )],[refute_0_28,refute_0_29]) ).
cnf(refute_0_31,plain,
eps2(step(star(atom(X_241)),X_241)) = andb(eps2(eps),eps2(star(atom(X_241)))),
inference(resolve,[$cnf( $equal(eps2(y(eps,star(atom(X_241)))),andb(eps2(eps),eps2(star(atom(X_241))))) )],[refute_0_8,refute_0_30]) ).
cnf(refute_0_32,plain,
eps2(star(atom(X_241))) = btrue,
inference(subst,[],[axiom_078:[bind(Y,$fot(atom(X_241)))]]) ).
cnf(refute_0_33,plain,
eps2(y(eps,X_40)) = andb(eps2(eps),eps2(X_40)),
inference(subst,[],[axiom_077:[bind(Q2,$fot(X_40)),bind(R,$fot(eps))]]) ).
cnf(refute_0_34,plain,
( eps2(eps) != btrue
| eps2(y(eps,X_40)) != andb(eps2(eps),eps2(X_40))
| eps2(y(eps,X_40)) = andb(btrue,eps2(X_40)) ),
introduced(tautology,[equality,[$cnf( $equal(eps2(y(eps,X_40)),andb(eps2(eps),eps2(X_40))) ),[1,0],$fot(btrue)]]) ).
cnf(refute_0_35,plain,
( eps2(y(eps,X_40)) != andb(eps2(eps),eps2(X_40))
| eps2(y(eps,X_40)) = andb(btrue,eps2(X_40)) ),
inference(resolve,[$cnf( $equal(eps2(eps),btrue) )],[axiom_075,refute_0_34]) ).
cnf(refute_0_36,plain,
eps2(y(eps,X_40)) = andb(btrue,eps2(X_40)),
inference(resolve,[$cnf( $equal(eps2(y(eps,X_40)),andb(eps2(eps),eps2(X_40))) )],[refute_0_33,refute_0_35]) ).
cnf(refute_0_37,plain,
andb(btrue,eps2(X_40)) = eps2(X_40),
inference(subst,[],[axiom_073:[bind(Q,$fot(eps2(X_40)))]]) ).
cnf(refute_0_38,plain,
( andb(btrue,eps2(X_40)) != eps2(X_40)
| eps2(y(eps,X_40)) != andb(btrue,eps2(X_40))
| eps2(y(eps,X_40)) = eps2(X_40) ),
introduced(tautology,[equality,[$cnf( $equal(eps2(y(eps,X_40)),andb(btrue,eps2(X_40))) ),[1],$fot(eps2(X_40))]]) ).
cnf(refute_0_39,plain,
( eps2(y(eps,X_40)) != andb(btrue,eps2(X_40))
| eps2(y(eps,X_40)) = eps2(X_40) ),
inference(resolve,[$cnf( $equal(andb(btrue,eps2(X_40)),eps2(X_40)) )],[refute_0_37,refute_0_38]) ).
cnf(refute_0_40,plain,
eps2(y(eps,X_40)) = eps2(X_40),
inference(resolve,[$cnf( $equal(eps2(y(eps,X_40)),andb(btrue,eps2(X_40))) )],[refute_0_36,refute_0_39]) ).
cnf(refute_0_41,plain,
eps2(y(eps,star(atom(X_241)))) = eps2(star(atom(X_241))),
inference(subst,[],[refute_0_40:[bind(X_40,$fot(star(atom(X_241))))]]) ).
cnf(refute_0_42,plain,
( Y0 != X0
| Y0 != Z0
| X0 = Z0 ),
introduced(tautology,[equality,[$cnf( $equal(Y0,Z0) ),[0],$fot(X0)]]) ).
cnf(refute_0_43,plain,
( X0 != Y0
| Y0 != Z0
| X0 = Z0 ),
inference(resolve,[$cnf( $equal(Y0,X0) )],[refute_0_26,refute_0_42]) ).
cnf(refute_0_44,plain,
( eps2(star(atom(X_241))) != btrue
| eps2(y(eps,star(atom(X_241)))) != eps2(star(atom(X_241)))
| eps2(y(eps,star(atom(X_241)))) = btrue ),
inference(subst,[],[refute_0_43:[bind(X0,$fot(eps2(y(eps,star(atom(X_241)))))),bind(Y0,$fot(eps2(star(atom(X_241))))),bind(Z0,$fot(btrue))]]) ).
cnf(refute_0_45,plain,
( eps2(star(atom(X_241))) != btrue
| eps2(y(eps,star(atom(X_241)))) = btrue ),
inference(resolve,[$cnf( $equal(eps2(y(eps,star(atom(X_241)))),eps2(star(atom(X_241)))) )],[refute_0_41,refute_0_44]) ).
cnf(refute_0_46,plain,
eps2(y(eps,star(atom(X_241)))) = btrue,
inference(resolve,[$cnf( $equal(eps2(star(atom(X_241))),btrue) )],[refute_0_32,refute_0_45]) ).
cnf(refute_0_47,plain,
( eps2(y(R,Q2)) != andb(eps2(R),eps2(Q2))
| andb(eps2(R),eps2(Q2)) = eps2(y(R,Q2)) ),
inference(subst,[],[refute_0_26:[bind(X0,$fot(eps2(y(R,Q2)))),bind(Y0,$fot(andb(eps2(R),eps2(Q2))))]]) ).
cnf(refute_0_48,plain,
andb(eps2(R),eps2(Q2)) = eps2(y(R,Q2)),
inference(resolve,[$cnf( $equal(eps2(y(R,Q2)),andb(eps2(R),eps2(Q2))) )],[axiom_077,refute_0_47]) ).
cnf(refute_0_49,plain,
andb(eps2(eps),eps2(star(atom(X_241)))) = eps2(y(eps,star(atom(X_241)))),
inference(subst,[],[refute_0_48:[bind(Q2,$fot(star(atom(X_241)))),bind(R,$fot(eps))]]) ).
cnf(refute_0_50,plain,
( andb(eps2(eps),eps2(star(atom(X_241)))) != eps2(y(eps,star(atom(X_241))))
| eps2(y(eps,star(atom(X_241)))) != btrue
| andb(eps2(eps),eps2(star(atom(X_241)))) = btrue ),
inference(subst,[],[refute_0_43:[bind(X0,$fot(andb(eps2(eps),eps2(star(atom(X_241)))))),bind(Y0,$fot(eps2(y(eps,star(atom(X_241)))))),bind(Z0,$fot(btrue))]]) ).
cnf(refute_0_51,plain,
( eps2(y(eps,star(atom(X_241)))) != btrue
| andb(eps2(eps),eps2(star(atom(X_241)))) = btrue ),
inference(resolve,[$cnf( $equal(andb(eps2(eps),eps2(star(atom(X_241)))),eps2(y(eps,star(atom(X_241))))) )],[refute_0_49,refute_0_50]) ).
cnf(refute_0_52,plain,
andb(eps2(eps),eps2(star(atom(X_241)))) = btrue,
inference(resolve,[$cnf( $equal(eps2(y(eps,star(atom(X_241)))),btrue) )],[refute_0_46,refute_0_51]) ).
cnf(refute_0_53,plain,
( andb(eps2(eps),eps2(star(atom(X_241)))) != btrue
| eps2(step(star(atom(X_241)),X_241)) != andb(eps2(eps),eps2(star(atom(X_241))))
| eps2(step(star(atom(X_241)),X_241)) = btrue ),
introduced(tautology,[equality,[$cnf( $equal(eps2(step(star(atom(X_241)),X_241)),andb(eps2(eps),eps2(star(atom(X_241))))) ),[1],$fot(btrue)]]) ).
cnf(refute_0_54,plain,
( eps2(step(star(atom(X_241)),X_241)) != andb(eps2(eps),eps2(star(atom(X_241))))
| eps2(step(star(atom(X_241)),X_241)) = btrue ),
inference(resolve,[$cnf( $equal(andb(eps2(eps),eps2(star(atom(X_241)))),btrue) )],[refute_0_52,refute_0_53]) ).
cnf(refute_0_55,plain,
eps2(step(star(atom(X_241)),X_241)) = btrue,
inference(resolve,[$cnf( $equal(eps2(step(star(atom(X_241)),X_241)),andb(eps2(eps),eps2(star(atom(X_241))))) )],[refute_0_31,refute_0_54]) ).
cnf(refute_0_56,plain,
eps2(step(star(atom(X_242)),X_242)) = btrue,
inference(subst,[],[refute_0_55:[bind(X_241,$fot(X_242))]]) ).
cnf(refute_0_57,plain,
( eps2(step(star(atom(X_242)),X_242)) != btrue
| eps2(y(step(star(atom(X_242)),X_242),eps)) != andb(eps2(step(star(atom(X_242)),X_242)),btrue)
| eps2(y(step(star(atom(X_242)),X_242),eps)) = andb(btrue,btrue) ),
introduced(tautology,[equality,[$cnf( $equal(eps2(y(step(star(atom(X_242)),X_242),eps)),andb(eps2(step(star(atom(X_242)),X_242)),btrue)) ),[1,0],$fot(btrue)]]) ).
cnf(refute_0_58,plain,
( eps2(y(step(star(atom(X_242)),X_242),eps)) != andb(eps2(step(star(atom(X_242)),X_242)),btrue)
| eps2(y(step(star(atom(X_242)),X_242),eps)) = andb(btrue,btrue) ),
inference(resolve,[$cnf( $equal(eps2(step(star(atom(X_242)),X_242)),btrue) )],[refute_0_56,refute_0_57]) ).
cnf(refute_0_59,plain,
eps2(y(step(star(atom(X_242)),X_242),eps)) = andb(btrue,btrue),
inference(resolve,[$cnf( $equal(eps2(y(step(star(atom(X_242)),X_242),eps)),andb(eps2(step(star(atom(X_242)),X_242)),btrue)) )],[refute_0_7,refute_0_58]) ).
cnf(refute_0_60,plain,
eps2(y(step(X_86,X_87),star(X_86))) = andb(eps2(step(X_86,X_87)),eps2(star(X_86))),
inference(subst,[],[axiom_077:[bind(Q2,$fot(star(X_86))),bind(R,$fot(step(X_86,X_87)))]]) ).
cnf(refute_0_61,plain,
step(star(X_86),X_87) = y(step(X_86,X_87),star(X_86)),
inference(subst,[],[axiom_084:[bind(P2,$fot(X_86)),bind(Y,$fot(X_87))]]) ).
cnf(refute_0_62,plain,
( step(star(X_86),X_87) != y(step(X_86,X_87),star(X_86))
| y(step(X_86,X_87),star(X_86)) = step(star(X_86),X_87) ),
inference(subst,[],[refute_0_26:[bind(X0,$fot(step(star(X_86),X_87))),bind(Y0,$fot(y(step(X_86,X_87),star(X_86))))]]) ).
cnf(refute_0_63,plain,
y(step(X_86,X_87),star(X_86)) = step(star(X_86),X_87),
inference(resolve,[$cnf( $equal(step(star(X_86),X_87),y(step(X_86,X_87),star(X_86))) )],[refute_0_61,refute_0_62]) ).
cnf(refute_0_64,plain,
( eps2(y(step(X_86,X_87),star(X_86))) != andb(eps2(step(X_86,X_87)),eps2(star(X_86)))
| y(step(X_86,X_87),star(X_86)) != step(star(X_86),X_87)
| eps2(step(star(X_86),X_87)) = andb(eps2(step(X_86,X_87)),eps2(star(X_86))) ),
introduced(tautology,[equality,[$cnf( $equal(eps2(y(step(X_86,X_87),star(X_86))),andb(eps2(step(X_86,X_87)),eps2(star(X_86)))) ),[0,0],$fot(step(star(X_86),X_87))]]) ).
cnf(refute_0_65,plain,
( eps2(y(step(X_86,X_87),star(X_86))) != andb(eps2(step(X_86,X_87)),eps2(star(X_86)))
| eps2(step(star(X_86),X_87)) = andb(eps2(step(X_86,X_87)),eps2(star(X_86))) ),
inference(resolve,[$cnf( $equal(y(step(X_86,X_87),star(X_86)),step(star(X_86),X_87)) )],[refute_0_63,refute_0_64]) ).
cnf(refute_0_66,plain,
eps2(step(star(X_86),X_87)) = andb(eps2(step(X_86,X_87)),eps2(star(X_86))),
inference(resolve,[$cnf( $equal(eps2(y(step(X_86,X_87),star(X_86))),andb(eps2(step(X_86,X_87)),eps2(star(X_86)))) )],[refute_0_60,refute_0_65]) ).
cnf(refute_0_67,plain,
eps2(y(X_41,star(Y))) = andb(eps2(X_41),eps2(star(Y))),
inference(subst,[],[axiom_077:[bind(Q2,$fot(star(Y))),bind(R,$fot(X_41))]]) ).
cnf(refute_0_68,plain,
( eps2(star(Y)) != btrue
| eps2(y(X_41,star(Y))) != andb(eps2(X_41),eps2(star(Y)))
| eps2(y(X_41,star(Y))) = andb(eps2(X_41),btrue) ),
introduced(tautology,[equality,[$cnf( $equal(eps2(y(X_41,star(Y))),andb(eps2(X_41),eps2(star(Y)))) ),[1,1],$fot(btrue)]]) ).
cnf(refute_0_69,plain,
( eps2(y(X_41,star(Y))) != andb(eps2(X_41),eps2(star(Y)))
| eps2(y(X_41,star(Y))) = andb(eps2(X_41),btrue) ),
inference(resolve,[$cnf( $equal(eps2(star(Y)),btrue) )],[axiom_078,refute_0_68]) ).
cnf(refute_0_70,plain,
eps2(y(X_41,star(Y))) = andb(eps2(X_41),btrue),
inference(resolve,[$cnf( $equal(eps2(y(X_41,star(Y))),andb(eps2(X_41),eps2(star(Y)))) )],[refute_0_67,refute_0_69]) ).
cnf(refute_0_71,plain,
( eps2(y(X_41,eps)) != andb(eps2(X_41),btrue)
| andb(eps2(X_41),btrue) = eps2(y(X_41,eps)) ),
inference(subst,[],[refute_0_26:[bind(X0,$fot(eps2(y(X_41,eps)))),bind(Y0,$fot(andb(eps2(X_41),btrue)))]]) ).
cnf(refute_0_72,plain,
andb(eps2(X_41),btrue) = eps2(y(X_41,eps)),
inference(resolve,[$cnf( $equal(eps2(y(X_41,eps)),andb(eps2(X_41),btrue)) )],[refute_0_6,refute_0_71]) ).
cnf(refute_0_73,plain,
( andb(eps2(X_41),btrue) != eps2(y(X_41,eps))
| eps2(y(X_41,star(Y))) != andb(eps2(X_41),btrue)
| eps2(y(X_41,star(Y))) = eps2(y(X_41,eps)) ),
introduced(tautology,[equality,[$cnf( $equal(eps2(y(X_41,star(Y))),andb(eps2(X_41),btrue)) ),[1],$fot(eps2(y(X_41,eps)))]]) ).
cnf(refute_0_74,plain,
( eps2(y(X_41,star(Y))) != andb(eps2(X_41),btrue)
| eps2(y(X_41,star(Y))) = eps2(y(X_41,eps)) ),
inference(resolve,[$cnf( $equal(andb(eps2(X_41),btrue),eps2(y(X_41,eps))) )],[refute_0_72,refute_0_73]) ).
cnf(refute_0_75,plain,
eps2(y(X_41,star(Y))) = eps2(y(X_41,eps)),
inference(resolve,[$cnf( $equal(eps2(y(X_41,star(Y))),andb(eps2(X_41),btrue)) )],[refute_0_70,refute_0_74]) ).
cnf(refute_0_76,plain,
eps2(y(step(X_86,X_87),star(X_86))) = eps2(y(step(X_86,X_87),eps)),
inference(subst,[],[refute_0_75:[bind(Y,$fot(X_86)),bind(X_41,$fot(step(X_86,X_87)))]]) ).
cnf(refute_0_77,plain,
andb(eps2(step(X_86,X_87)),eps2(star(X_86))) = eps2(y(step(X_86,X_87),star(X_86))),
inference(subst,[],[refute_0_48:[bind(Q2,$fot(star(X_86))),bind(R,$fot(step(X_86,X_87)))]]) ).
cnf(refute_0_78,plain,
( andb(eps2(step(X_86,X_87)),eps2(star(X_86))) != eps2(y(step(X_86,X_87),star(X_86)))
| eps2(y(step(X_86,X_87),star(X_86))) != eps2(y(step(X_86,X_87),eps))
| andb(eps2(step(X_86,X_87)),eps2(star(X_86))) = eps2(y(step(X_86,X_87),eps)) ),
inference(subst,[],[refute_0_43:[bind(X0,$fot(andb(eps2(step(X_86,X_87)),eps2(star(X_86))))),bind(Y0,$fot(eps2(y(step(X_86,X_87),star(X_86))))),bind(Z0,$fot(eps2(y(step(X_86,X_87),eps))))]]) ).
cnf(refute_0_79,plain,
( eps2(y(step(X_86,X_87),star(X_86))) != eps2(y(step(X_86,X_87),eps))
| andb(eps2(step(X_86,X_87)),eps2(star(X_86))) = eps2(y(step(X_86,X_87),eps)) ),
inference(resolve,[$cnf( $equal(andb(eps2(step(X_86,X_87)),eps2(star(X_86))),eps2(y(step(X_86,X_87),star(X_86)))) )],[refute_0_77,refute_0_78]) ).
cnf(refute_0_80,plain,
andb(eps2(step(X_86,X_87)),eps2(star(X_86))) = eps2(y(step(X_86,X_87),eps)),
inference(resolve,[$cnf( $equal(eps2(y(step(X_86,X_87),star(X_86))),eps2(y(step(X_86,X_87),eps))) )],[refute_0_76,refute_0_79]) ).
cnf(refute_0_81,plain,
( andb(eps2(step(X_86,X_87)),eps2(star(X_86))) != eps2(y(step(X_86,X_87),eps))
| eps2(step(star(X_86),X_87)) != andb(eps2(step(X_86,X_87)),eps2(star(X_86)))
| eps2(step(star(X_86),X_87)) = eps2(y(step(X_86,X_87),eps)) ),
introduced(tautology,[equality,[$cnf( $equal(eps2(step(star(X_86),X_87)),andb(eps2(step(X_86,X_87)),eps2(star(X_86)))) ),[1],$fot(eps2(y(step(X_86,X_87),eps)))]]) ).
cnf(refute_0_82,plain,
( eps2(step(star(X_86),X_87)) != andb(eps2(step(X_86,X_87)),eps2(star(X_86)))
| eps2(step(star(X_86),X_87)) = eps2(y(step(X_86,X_87),eps)) ),
inference(resolve,[$cnf( $equal(andb(eps2(step(X_86,X_87)),eps2(star(X_86))),eps2(y(step(X_86,X_87),eps))) )],[refute_0_80,refute_0_81]) ).
cnf(refute_0_83,plain,
eps2(step(star(X_86),X_87)) = eps2(y(step(X_86,X_87),eps)),
inference(resolve,[$cnf( $equal(eps2(step(star(X_86),X_87)),andb(eps2(step(X_86,X_87)),eps2(star(X_86)))) )],[refute_0_66,refute_0_82]) ).
cnf(refute_0_84,plain,
( eps2(step(star(X_86),X_87)) != eps2(y(step(X_86,X_87),eps))
| eps2(y(step(X_86,X_87),eps)) = eps2(step(star(X_86),X_87)) ),
inference(subst,[],[refute_0_26:[bind(X0,$fot(eps2(step(star(X_86),X_87)))),bind(Y0,$fot(eps2(y(step(X_86,X_87),eps))))]]) ).
cnf(refute_0_85,plain,
eps2(y(step(X_86,X_87),eps)) = eps2(step(star(X_86),X_87)),
inference(resolve,[$cnf( $equal(eps2(step(star(X_86),X_87)),eps2(y(step(X_86,X_87),eps))) )],[refute_0_83,refute_0_84]) ).
cnf(refute_0_86,plain,
eps2(y(step(star(atom(X_242)),X_242),eps)) = eps2(step(star(star(atom(X_242))),X_242)),
inference(subst,[],[refute_0_85:[bind(X_86,$fot(star(atom(X_242)))),bind(X_87,$fot(X_242))]]) ).
cnf(refute_0_87,plain,
( eps2(y(step(star(atom(X_242)),X_242),eps)) != andb(btrue,btrue)
| eps2(y(step(star(atom(X_242)),X_242),eps)) != eps2(step(star(star(atom(X_242))),X_242))
| eps2(step(star(star(atom(X_242))),X_242)) = andb(btrue,btrue) ),
introduced(tautology,[equality,[$cnf( $equal(eps2(y(step(star(atom(X_242)),X_242),eps)),andb(btrue,btrue)) ),[0],$fot(eps2(step(star(star(atom(X_242))),X_242)))]]) ).
cnf(refute_0_88,plain,
( eps2(y(step(star(atom(X_242)),X_242),eps)) != andb(btrue,btrue)
| eps2(step(star(star(atom(X_242))),X_242)) = andb(btrue,btrue) ),
inference(resolve,[$cnf( $equal(eps2(y(step(star(atom(X_242)),X_242),eps)),eps2(step(star(star(atom(X_242))),X_242))) )],[refute_0_86,refute_0_87]) ).
cnf(refute_0_89,plain,
andb(btrue,btrue) = btrue,
inference(subst,[],[axiom_073:[bind(Q,$fot(btrue))]]) ).
cnf(refute_0_90,plain,
( andb(btrue,btrue) != btrue
| eps2(step(star(star(atom(X_242))),X_242)) != andb(btrue,btrue)
| eps2(step(star(star(atom(X_242))),X_242)) = btrue ),
introduced(tautology,[equality,[$cnf( $equal(eps2(step(star(star(atom(X_242))),X_242)),andb(btrue,btrue)) ),[1],$fot(btrue)]]) ).
cnf(refute_0_91,plain,
( eps2(step(star(star(atom(X_242))),X_242)) != andb(btrue,btrue)
| eps2(step(star(star(atom(X_242))),X_242)) = btrue ),
inference(resolve,[$cnf( $equal(andb(btrue,btrue),btrue) )],[refute_0_89,refute_0_90]) ).
cnf(refute_0_92,plain,
( eps2(y(step(star(atom(X_242)),X_242),eps)) != andb(btrue,btrue)
| eps2(step(star(star(atom(X_242))),X_242)) = btrue ),
inference(resolve,[$cnf( $equal(eps2(step(star(star(atom(X_242))),X_242)),andb(btrue,btrue)) )],[refute_0_88,refute_0_91]) ).
cnf(refute_0_93,plain,
eps2(step(star(star(atom(X_242))),X_242)) = btrue,
inference(resolve,[$cnf( $equal(eps2(y(step(star(atom(X_242)),X_242),eps)),andb(btrue,btrue)) )],[refute_0_59,refute_0_92]) ).
cnf(refute_0_94,plain,
eps2(step(star(star(atom(X_243))),X_243)) = btrue,
inference(subst,[],[refute_0_93:[bind(X_242,$fot(X_243))]]) ).
cnf(refute_0_95,plain,
( eps2(step(star(star(atom(X_243))),X_243)) != btrue
| rec(step(star(star(atom(X_243))),X_243),nil2) != eps2(step(star(star(atom(X_243))),X_243))
| rec(step(star(star(atom(X_243))),X_243),nil2) = btrue ),
introduced(tautology,[equality,[$cnf( $equal(rec(step(star(star(atom(X_243))),X_243),nil2),eps2(step(star(star(atom(X_243))),X_243))) ),[1],$fot(btrue)]]) ).
cnf(refute_0_96,plain,
( rec(step(star(star(atom(X_243))),X_243),nil2) != eps2(step(star(star(atom(X_243))),X_243))
| rec(step(star(star(atom(X_243))),X_243),nil2) = btrue ),
inference(resolve,[$cnf( $equal(eps2(step(star(star(atom(X_243))),X_243)),btrue) )],[refute_0_94,refute_0_95]) ).
cnf(refute_0_97,plain,
rec(step(star(star(atom(X_243))),X_243),nil2) = btrue,
inference(resolve,[$cnf( $equal(rec(step(star(star(atom(X_243))),X_243),nil2),eps2(step(star(star(atom(X_243))),X_243))) )],[refute_0_2,refute_0_96]) ).
cnf(refute_0_98,plain,
( rec(X,cons2(Z,Xs)) != rec(step(X,Z),Xs)
| rec(step(X,Z),Xs) = rec(X,cons2(Z,Xs)) ),
inference(subst,[],[refute_0_26:[bind(X0,$fot(rec(X,cons2(Z,Xs)))),bind(Y0,$fot(rec(step(X,Z),Xs)))]]) ).
cnf(refute_0_99,plain,
rec(step(X,Z),Xs) = rec(X,cons2(Z,Xs)),
inference(resolve,[$cnf( $equal(rec(X,cons2(Z,Xs)),rec(step(X,Z),Xs)) )],[axiom_088,refute_0_98]) ).
cnf(refute_0_100,plain,
rec(step(star(star(atom(X_243))),X_243),nil2) = rec(star(star(atom(X_243))),cons2(X_243,nil2)),
inference(subst,[],[refute_0_99:[bind(X,$fot(star(star(atom(X_243))))),bind(Xs,$fot(nil2)),bind(Z,$fot(X_243))]]) ).
cnf(refute_0_101,plain,
( rec(step(star(star(atom(X_243))),X_243),nil2) != btrue
| rec(step(star(star(atom(X_243))),X_243),nil2) != rec(star(star(atom(X_243))),cons2(X_243,nil2))
| rec(star(star(atom(X_243))),cons2(X_243,nil2)) = btrue ),
introduced(tautology,[equality,[$cnf( $equal(rec(step(star(star(atom(X_243))),X_243),nil2),btrue) ),[0],$fot(rec(star(star(atom(X_243))),cons2(X_243,nil2)))]]) ).
cnf(refute_0_102,plain,
( rec(step(star(star(atom(X_243))),X_243),nil2) != btrue
| rec(star(star(atom(X_243))),cons2(X_243,nil2)) = btrue ),
inference(resolve,[$cnf( $equal(rec(step(star(star(atom(X_243))),X_243),nil2),rec(star(star(atom(X_243))),cons2(X_243,nil2))) )],[refute_0_100,refute_0_101]) ).
cnf(refute_0_103,plain,
rec(star(star(atom(X_243))),cons2(X_243,nil2)) = btrue,
inference(resolve,[$cnf( $equal(rec(step(star(star(atom(X_243))),X_243),nil2),btrue) )],[refute_0_97,refute_0_102]) ).
cnf(refute_0_104,plain,
rec(star(star(atom(X_342))),cons2(X_342,nil2)) = btrue,
inference(subst,[],[refute_0_103:[bind(X_243,$fot(X_342))]]) ).
cnf(refute_0_105,plain,
( prop_same(star(star(atom(X_342))),cons2(X_342,nil2)) != eq2(rec(star(star(atom(X_342))),cons2(X_342,nil2)),reck2(star(star(atom(X_342))),cons2(X_342,nil2)))
| rec(star(star(atom(X_342))),cons2(X_342,nil2)) != btrue
| prop_same(star(star(atom(X_342))),cons2(X_342,nil2)) = eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2))) ),
introduced(tautology,[equality,[$cnf( $equal(prop_same(star(star(atom(X_342))),cons2(X_342,nil2)),eq2(rec(star(star(atom(X_342))),cons2(X_342,nil2)),reck2(star(star(atom(X_342))),cons2(X_342,nil2)))) ),[1,0],$fot(btrue)]]) ).
cnf(refute_0_106,plain,
( prop_same(star(star(atom(X_342))),cons2(X_342,nil2)) != eq2(rec(star(star(atom(X_342))),cons2(X_342,nil2)),reck2(star(star(atom(X_342))),cons2(X_342,nil2)))
| prop_same(star(star(atom(X_342))),cons2(X_342,nil2)) = eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2))) ),
inference(resolve,[$cnf( $equal(rec(star(star(atom(X_342))),cons2(X_342,nil2)),btrue) )],[refute_0_104,refute_0_105]) ).
cnf(refute_0_107,plain,
prop_same(star(star(atom(X_342))),cons2(X_342,nil2)) = eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2))),
inference(resolve,[$cnf( $equal(prop_same(star(star(atom(X_342))),cons2(X_342,nil2)),eq2(rec(star(star(atom(X_342))),cons2(X_342,nil2)),reck2(star(star(atom(X_342))),cons2(X_342,nil2)))) )],[refute_0_1,refute_0_106]) ).
cnf(refute_0_108,plain,
reck2(star(star(Y)),cons2(X_184,X_185)) = aux3(star(Y),X_184,X_185,notb(eps2(star(Y)))),
inference(subst,[],[axiom_100:[bind(P2,$fot(star(Y))),bind(X6,$fot(X_184)),bind(X7,$fot(X_185))]]) ).
cnf(refute_0_109,plain,
( eps2(star(Y)) != btrue
| reck2(star(star(Y)),cons2(X_184,X_185)) != aux3(star(Y),X_184,X_185,notb(eps2(star(Y))))
| reck2(star(star(Y)),cons2(X_184,X_185)) = aux3(star(Y),X_184,X_185,notb(btrue)) ),
introduced(tautology,[equality,[$cnf( $equal(reck2(star(star(Y)),cons2(X_184,X_185)),aux3(star(Y),X_184,X_185,notb(eps2(star(Y))))) ),[1,3,0],$fot(btrue)]]) ).
cnf(refute_0_110,plain,
( reck2(star(star(Y)),cons2(X_184,X_185)) != aux3(star(Y),X_184,X_185,notb(eps2(star(Y))))
| reck2(star(star(Y)),cons2(X_184,X_185)) = aux3(star(Y),X_184,X_185,notb(btrue)) ),
inference(resolve,[$cnf( $equal(eps2(star(Y)),btrue) )],[axiom_078,refute_0_109]) ).
cnf(refute_0_111,plain,
reck2(star(star(Y)),cons2(X_184,X_185)) = aux3(star(Y),X_184,X_185,notb(btrue)),
inference(resolve,[$cnf( $equal(reck2(star(star(Y)),cons2(X_184,X_185)),aux3(star(Y),X_184,X_185,notb(eps2(star(Y))))) )],[refute_0_108,refute_0_110]) ).
cnf(refute_0_112,plain,
aux3(star(Y),X_184,X_185,bfalse) = bfalse,
inference(subst,[],[axiom_005:[bind(P2,$fot(star(Y))),bind(X6,$fot(X_184)),bind(X7,$fot(X_185))]]) ).
cnf(refute_0_113,plain,
aux3(star(Y),X_184,X_185,notb(btrue)) = aux3(star(Y),X_184,X_185,notb(btrue)),
introduced(tautology,[refl,[$fot(aux3(star(Y),X_184,X_185,notb(btrue)))]]) ).
cnf(refute_0_114,plain,
( aux3(star(Y),X_184,X_185,notb(btrue)) != aux3(star(Y),X_184,X_185,notb(btrue))
| notb(btrue) != bfalse
| aux3(star(Y),X_184,X_185,notb(btrue)) = aux3(star(Y),X_184,X_185,bfalse) ),
introduced(tautology,[equality,[$cnf( $equal(aux3(star(Y),X_184,X_185,notb(btrue)),aux3(star(Y),X_184,X_185,notb(btrue))) ),[1,3],$fot(bfalse)]]) ).
cnf(refute_0_115,plain,
( notb(btrue) != bfalse
| aux3(star(Y),X_184,X_185,notb(btrue)) = aux3(star(Y),X_184,X_185,bfalse) ),
inference(resolve,[$cnf( $equal(aux3(star(Y),X_184,X_185,notb(btrue)),aux3(star(Y),X_184,X_185,notb(btrue))) )],[refute_0_113,refute_0_114]) ).
cnf(refute_0_116,plain,
aux3(star(Y),X_184,X_185,notb(btrue)) = aux3(star(Y),X_184,X_185,bfalse),
inference(resolve,[$cnf( $equal(notb(btrue),bfalse) )],[axiom_071,refute_0_115]) ).
cnf(refute_0_117,plain,
( aux3(star(Y),X_184,X_185,bfalse) != bfalse
| aux3(star(Y),X_184,X_185,notb(btrue)) != aux3(star(Y),X_184,X_185,bfalse)
| aux3(star(Y),X_184,X_185,notb(btrue)) = bfalse ),
inference(subst,[],[refute_0_43:[bind(X0,$fot(aux3(star(Y),X_184,X_185,notb(btrue)))),bind(Y0,$fot(aux3(star(Y),X_184,X_185,bfalse))),bind(Z0,$fot(bfalse))]]) ).
cnf(refute_0_118,plain,
( aux3(star(Y),X_184,X_185,bfalse) != bfalse
| aux3(star(Y),X_184,X_185,notb(btrue)) = bfalse ),
inference(resolve,[$cnf( $equal(aux3(star(Y),X_184,X_185,notb(btrue)),aux3(star(Y),X_184,X_185,bfalse)) )],[refute_0_116,refute_0_117]) ).
cnf(refute_0_119,plain,
aux3(star(Y),X_184,X_185,notb(btrue)) = bfalse,
inference(resolve,[$cnf( $equal(aux3(star(Y),X_184,X_185,bfalse),bfalse) )],[refute_0_112,refute_0_118]) ).
cnf(refute_0_120,plain,
( aux3(star(Y),X_184,X_185,notb(btrue)) != bfalse
| reck2(star(star(Y)),cons2(X_184,X_185)) != aux3(star(Y),X_184,X_185,notb(btrue))
| reck2(star(star(Y)),cons2(X_184,X_185)) = bfalse ),
introduced(tautology,[equality,[$cnf( $equal(reck2(star(star(Y)),cons2(X_184,X_185)),aux3(star(Y),X_184,X_185,notb(btrue))) ),[1],$fot(bfalse)]]) ).
cnf(refute_0_121,plain,
( reck2(star(star(Y)),cons2(X_184,X_185)) != aux3(star(Y),X_184,X_185,notb(btrue))
| reck2(star(star(Y)),cons2(X_184,X_185)) = bfalse ),
inference(resolve,[$cnf( $equal(aux3(star(Y),X_184,X_185,notb(btrue)),bfalse) )],[refute_0_119,refute_0_120]) ).
cnf(refute_0_122,plain,
reck2(star(star(Y)),cons2(X_184,X_185)) = bfalse,
inference(resolve,[$cnf( $equal(reck2(star(star(Y)),cons2(X_184,X_185)),aux3(star(Y),X_184,X_185,notb(btrue))) )],[refute_0_111,refute_0_121]) ).
cnf(refute_0_123,plain,
reck2(star(star(atom(X_342))),cons2(X_342,nil2)) = bfalse,
inference(subst,[],[refute_0_122:[bind(Y,$fot(atom(X_342))),bind(X_184,$fot(X_342)),bind(X_185,$fot(nil2))]]) ).
cnf(refute_0_124,plain,
eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2))) = eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2))),
introduced(tautology,[refl,[$fot(eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2))))]]) ).
cnf(refute_0_125,plain,
( eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2))) != eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2)))
| reck2(star(star(atom(X_342))),cons2(X_342,nil2)) != bfalse
| eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2))) = eq2(btrue,bfalse) ),
introduced(tautology,[equality,[$cnf( $equal(eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2))),eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2)))) ),[1,1],$fot(bfalse)]]) ).
cnf(refute_0_126,plain,
( reck2(star(star(atom(X_342))),cons2(X_342,nil2)) != bfalse
| eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2))) = eq2(btrue,bfalse) ),
inference(resolve,[$cnf( $equal(eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2))),eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2)))) )],[refute_0_124,refute_0_125]) ).
cnf(refute_0_127,plain,
eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2))) = eq2(btrue,bfalse),
inference(resolve,[$cnf( $equal(reck2(star(star(atom(X_342))),cons2(X_342,nil2)),bfalse) )],[refute_0_123,refute_0_126]) ).
cnf(refute_0_128,plain,
( eq2(btrue,bfalse) != bfalse
| eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2))) != eq2(btrue,bfalse)
| eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2))) = bfalse ),
inference(subst,[],[refute_0_43:[bind(X0,$fot(eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2))))),bind(Y0,$fot(eq2(btrue,bfalse))),bind(Z0,$fot(bfalse))]]) ).
cnf(refute_0_129,plain,
( eq2(btrue,bfalse) != bfalse
| eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2))) = bfalse ),
inference(resolve,[$cnf( $equal(eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2))),eq2(btrue,bfalse)) )],[refute_0_127,refute_0_128]) ).
cnf(refute_0_130,plain,
eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2))) = bfalse,
inference(resolve,[$cnf( $equal(eq2(btrue,bfalse),bfalse) )],[axiom_109,refute_0_129]) ).
cnf(refute_0_131,plain,
( eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2))) != bfalse
| prop_same(star(star(atom(X_342))),cons2(X_342,nil2)) != eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2)))
| prop_same(star(star(atom(X_342))),cons2(X_342,nil2)) = bfalse ),
introduced(tautology,[equality,[$cnf( $equal(prop_same(star(star(atom(X_342))),cons2(X_342,nil2)),eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2)))) ),[1],$fot(bfalse)]]) ).
cnf(refute_0_132,plain,
( prop_same(star(star(atom(X_342))),cons2(X_342,nil2)) != eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2)))
| prop_same(star(star(atom(X_342))),cons2(X_342,nil2)) = bfalse ),
inference(resolve,[$cnf( $equal(eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2))),bfalse) )],[refute_0_130,refute_0_131]) ).
cnf(refute_0_133,plain,
prop_same(star(star(atom(X_342))),cons2(X_342,nil2)) = bfalse,
inference(resolve,[$cnf( $equal(prop_same(star(star(atom(X_342))),cons2(X_342,nil2)),eq2(btrue,reck2(star(star(atom(X_342))),cons2(X_342,nil2)))) )],[refute_0_107,refute_0_132]) ).
cnf(refute_0_134,plain,
prop_same(star(star(atom(X_343))),cons2(X_343,nil2)) = bfalse,
inference(subst,[],[refute_0_133:[bind(X_342,$fot(X_343))]]) ).
cnf(refute_0_135,plain,
( eq2(bfalse,bfalse) != btrue
| prop_same(star(star(atom(X_343))),cons2(X_343,nil2)) != bfalse
| eq2(prop_same(star(star(atom(X_343))),cons2(X_343,nil2)),bfalse) = btrue ),
introduced(tautology,[equality,[$cnf( ~ $equal(eq2(prop_same(star(star(atom(X_343))),cons2(X_343,nil2)),bfalse),btrue) ),[0,0],$fot(bfalse)]]) ).
cnf(refute_0_136,plain,
( eq2(bfalse,bfalse) != btrue
| eq2(prop_same(star(star(atom(X_343))),cons2(X_343,nil2)),bfalse) = btrue ),
inference(resolve,[$cnf( $equal(prop_same(star(star(atom(X_343))),cons2(X_343,nil2)),bfalse) )],[refute_0_134,refute_0_135]) ).
cnf(refute_0_137,plain,
eq2(bfalse,bfalse) != btrue,
inference(resolve,[$cnf( $equal(eq2(prop_same(star(star(atom(X_343))),cons2(X_343,nil2)),bfalse),btrue) )],[refute_0_136,refute_0_0]) ).
cnf(refute_0_138,plain,
eq2(bfalse,bfalse) = btrue,
inference(subst,[],[axiom_111:[bind(X,$fot(bfalse))]]) ).
cnf(refute_0_139,plain,
( btrue != btrue
| eq2(bfalse,bfalse) != btrue
| eq2(bfalse,bfalse) = btrue ),
introduced(tautology,[equality,[$cnf( $equal(eq2(bfalse,bfalse),btrue) ),[1],$fot(btrue)]]) ).
cnf(refute_0_140,plain,
( btrue != btrue
| eq2(bfalse,bfalse) = btrue ),
inference(resolve,[$cnf( $equal(eq2(bfalse,bfalse),btrue) )],[refute_0_138,refute_0_139]) ).
cnf(refute_0_141,plain,
btrue != btrue,
inference(resolve,[$cnf( $equal(eq2(bfalse,bfalse),btrue) )],[refute_0_140,refute_0_137]) ).
cnf(refute_0_142,plain,
btrue = btrue,
introduced(tautology,[refl,[$fot(btrue)]]) ).
cnf(refute_0_143,plain,
$false,
inference(resolve,[$cnf( $equal(btrue,btrue) )],[refute_0_142,refute_0_141]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX239-1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : metis --show proof --show saturation %s
% 0.15/0.34 % Computer : n014.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Tue May 5 13:19:51 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.86/1.12 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.86/1.12
% 0.86/1.12 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 0.97/1.13
%------------------------------------------------------------------------------