%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : LCL162-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 12:42:02 PM UTC 2026
% Result : Unsatisfiable 50.79s 51.13s
% Output : CNFRefutation 50.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 59
% Number of leaves : 119
% Syntax : Number of clauses : 446 ( 224 unt; 0 nHn; 234 RR)
% Number of literals : 768 ( 767 equ; 325 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 : 9 ( 9 usr; 5 con; 0-2 aty)
% Number of variables : 854 ( 19 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(axiom_1,axiom,
not(X) = xor(X,truth) ).
cnf(axiom_2,axiom,
xor(X,falsehood) = X ).
cnf(axiom_5,axiom,
and_star(X,falsehood) = falsehood ).
cnf(axiom_6,axiom,
and_star(xor(truth,X),X) = falsehood ).
cnf(axiom_7,axiom,
xor(X,xor(truth,Y)) = xor(xor(X,truth),Y) ).
cnf(axiom_8,axiom,
and_star(xor(and_star(xor(truth,X),Y),truth),Y) = and_star(xor(and_star(xor(truth,Y),X),truth),X) ).
cnf(xor_commutativity,axiom,
xor(X,Y) = xor(Y,X) ).
cnf(and_star_associativity,axiom,
and_star(and_star(X,Y),Z) = and_star(X,and_star(Y,Z)) ).
cnf(and_star_commutativity,axiom,
and_star(X,Y) = and_star(Y,X) ).
cnf(false_definition,axiom,
not(truth) = falsehood ).
cnf(implies_definition,axiom,
implies(X,Y) = xor(truth,and_star(X,xor(truth,Y))) ).
cnf(prove_wajsberg_axiom,negated_conjecture,
implies(implies(x,y),implies(implies(y,z),implies(x,z))) != truth ).
cnf(refute_0_0,plain,
X0 = X0,
introduced(tautology,[refl,[$fot(X0)]]) ).
cnf(refute_0_1,plain,
( X0 != X0
| X0 != Y0
| Y0 = X0 ),
introduced(tautology,[equality,[$cnf( $equal(X0,X0) ),[0],$fot(Y0)]]) ).
cnf(refute_0_2,plain,
( X0 != Y0
| Y0 = X0 ),
inference(resolve,[$cnf( $equal(X0,X0) )],[refute_0_0,refute_0_1]) ).
cnf(refute_0_3,plain,
( not(X) != xor(X,truth)
| xor(X,truth) = not(X) ),
inference(subst,[],[refute_0_2:[bind(X0,$fot(not(X))),bind(Y0,$fot(xor(X,truth)))]]) ).
cnf(refute_0_4,plain,
xor(X,truth) = not(X),
inference(resolve,[$cnf( $equal(not(X),xor(X,truth)) )],[axiom_1,refute_0_3]) ).
cnf(refute_0_5,plain,
xor(xor(X,truth),Y) = xor(xor(X,truth),Y),
introduced(tautology,[refl,[$fot(xor(xor(X,truth),Y))]]) ).
cnf(refute_0_6,plain,
( xor(X,truth) != not(X)
| xor(xor(X,truth),Y) != xor(xor(X,truth),Y)
| xor(xor(X,truth),Y) = xor(not(X),Y) ),
introduced(tautology,[equality,[$cnf( $equal(xor(xor(X,truth),Y),xor(xor(X,truth),Y)) ),[1,0],$fot(not(X))]]) ).
cnf(refute_0_7,plain,
( xor(X,truth) != not(X)
| xor(xor(X,truth),Y) = xor(not(X),Y) ),
inference(resolve,[$cnf( $equal(xor(xor(X,truth),Y),xor(xor(X,truth),Y)) )],[refute_0_5,refute_0_6]) ).
cnf(refute_0_8,plain,
xor(xor(X,truth),Y) = xor(not(X),Y),
inference(resolve,[$cnf( $equal(xor(X,truth),not(X)) )],[refute_0_4,refute_0_7]) ).
cnf(refute_0_9,plain,
( xor(X,xor(truth,Y)) != xor(xor(X,truth),Y)
| xor(xor(X,truth),Y) != xor(not(X),Y)
| xor(X,xor(truth,Y)) = xor(not(X),Y) ),
introduced(tautology,[equality,[$cnf( ~ $equal(xor(X,xor(truth,Y)),xor(not(X),Y)) ),[0],$fot(xor(xor(X,truth),Y))]]) ).
cnf(refute_0_10,plain,
( xor(X,xor(truth,Y)) != xor(xor(X,truth),Y)
| xor(X,xor(truth,Y)) = xor(not(X),Y) ),
inference(resolve,[$cnf( $equal(xor(xor(X,truth),Y),xor(not(X),Y)) )],[refute_0_8,refute_0_9]) ).
cnf(refute_0_11,plain,
xor(X,xor(truth,Y)) = xor(not(X),Y),
inference(resolve,[$cnf( $equal(xor(X,xor(truth,Y)),xor(xor(X,truth),Y)) )],[axiom_7,refute_0_10]) ).
cnf(refute_0_12,plain,
xor(X_6,xor(truth,truth)) = xor(not(X_6),truth),
inference(subst,[],[refute_0_11:[bind(X,$fot(X_6)),bind(Y,$fot(truth))]]) ).
cnf(refute_0_13,plain,
not(not(X_6)) = xor(not(X_6),truth),
inference(subst,[],[axiom_1:[bind(X,$fot(not(X_6)))]]) ).
cnf(refute_0_14,plain,
( not(not(X_6)) != xor(not(X_6),truth)
| xor(not(X_6),truth) = not(not(X_6)) ),
inference(subst,[],[refute_0_2:[bind(X0,$fot(not(not(X_6)))),bind(Y0,$fot(xor(not(X_6),truth)))]]) ).
cnf(refute_0_15,plain,
xor(not(X_6),truth) = not(not(X_6)),
inference(resolve,[$cnf( $equal(not(not(X_6)),xor(not(X_6),truth)) )],[refute_0_13,refute_0_14]) ).
cnf(refute_0_16,plain,
( xor(X_6,xor(truth,truth)) != xor(not(X_6),truth)
| xor(not(X_6),truth) != not(not(X_6))
| xor(X_6,xor(truth,truth)) = not(not(X_6)) ),
introduced(tautology,[equality,[$cnf( ~ $equal(xor(X_6,xor(truth,truth)),not(not(X_6))) ),[0],$fot(xor(not(X_6),truth))]]) ).
cnf(refute_0_17,plain,
( xor(X_6,xor(truth,truth)) != xor(not(X_6),truth)
| xor(X_6,xor(truth,truth)) = not(not(X_6)) ),
inference(resolve,[$cnf( $equal(xor(not(X_6),truth),not(not(X_6))) )],[refute_0_15,refute_0_16]) ).
cnf(refute_0_18,plain,
xor(X_6,xor(truth,truth)) = not(not(X_6)),
inference(resolve,[$cnf( $equal(xor(X_6,xor(truth,truth)),xor(not(X_6),truth)) )],[refute_0_12,refute_0_17]) ).
cnf(refute_0_19,plain,
not(truth) = xor(truth,truth),
inference(subst,[],[axiom_1:[bind(X,$fot(truth))]]) ).
cnf(refute_0_20,plain,
( not(truth) != xor(truth,truth)
| xor(truth,truth) = not(truth) ),
inference(subst,[],[refute_0_2:[bind(X0,$fot(not(truth))),bind(Y0,$fot(xor(truth,truth)))]]) ).
cnf(refute_0_21,plain,
xor(truth,truth) = not(truth),
inference(resolve,[$cnf( $equal(not(truth),xor(truth,truth)) )],[refute_0_19,refute_0_20]) ).
cnf(refute_0_22,plain,
( xor(X_6,xor(truth,truth)) != xor(not(X_6),truth)
| xor(truth,truth) != not(truth)
| xor(X_6,not(truth)) = xor(not(X_6),truth) ),
introduced(tautology,[equality,[$cnf( $equal(xor(X_6,xor(truth,truth)),xor(not(X_6),truth)) ),[0,1],$fot(not(truth))]]) ).
cnf(refute_0_23,plain,
( xor(X_6,xor(truth,truth)) != xor(not(X_6),truth)
| xor(X_6,not(truth)) = xor(not(X_6),truth) ),
inference(resolve,[$cnf( $equal(xor(truth,truth),not(truth)) )],[refute_0_21,refute_0_22]) ).
cnf(refute_0_24,plain,
xor(X_6,not(truth)) = xor(not(X_6),truth),
inference(resolve,[$cnf( $equal(xor(X_6,xor(truth,truth)),xor(not(X_6),truth)) )],[refute_0_12,refute_0_23]) ).
cnf(refute_0_25,plain,
xor(X_6,falsehood) = X_6,
inference(subst,[],[axiom_2:[bind(X,$fot(X_6))]]) ).
cnf(refute_0_26,plain,
xor(X_6,not(truth)) = xor(X_6,not(truth)),
introduced(tautology,[refl,[$fot(xor(X_6,not(truth)))]]) ).
cnf(refute_0_27,plain,
( not(truth) != falsehood
| xor(X_6,not(truth)) != xor(X_6,not(truth))
| xor(X_6,not(truth)) = xor(X_6,falsehood) ),
introduced(tautology,[equality,[$cnf( $equal(xor(X_6,not(truth)),xor(X_6,not(truth))) ),[1,1],$fot(falsehood)]]) ).
cnf(refute_0_28,plain,
( not(truth) != falsehood
| xor(X_6,not(truth)) = xor(X_6,falsehood) ),
inference(resolve,[$cnf( $equal(xor(X_6,not(truth)),xor(X_6,not(truth))) )],[refute_0_26,refute_0_27]) ).
cnf(refute_0_29,plain,
xor(X_6,not(truth)) = xor(X_6,falsehood),
inference(resolve,[$cnf( $equal(not(truth),falsehood) )],[false_definition,refute_0_28]) ).
cnf(refute_0_30,plain,
( Y0 != X0
| Y0 != Z0
| X0 = Z0 ),
introduced(tautology,[equality,[$cnf( $equal(Y0,Z0) ),[0],$fot(X0)]]) ).
cnf(refute_0_31,plain,
( X0 != Y0
| Y0 != Z0
| X0 = Z0 ),
inference(resolve,[$cnf( $equal(Y0,X0) )],[refute_0_2,refute_0_30]) ).
cnf(refute_0_32,plain,
( xor(X_6,falsehood) != X_6
| xor(X_6,not(truth)) != xor(X_6,falsehood)
| xor(X_6,not(truth)) = X_6 ),
inference(subst,[],[refute_0_31:[bind(X0,$fot(xor(X_6,not(truth)))),bind(Y0,$fot(xor(X_6,falsehood))),bind(Z0,$fot(X_6))]]) ).
cnf(refute_0_33,plain,
( xor(X_6,falsehood) != X_6
| xor(X_6,not(truth)) = X_6 ),
inference(resolve,[$cnf( $equal(xor(X_6,not(truth)),xor(X_6,falsehood)) )],[refute_0_29,refute_0_32]) ).
cnf(refute_0_34,plain,
xor(X_6,not(truth)) = X_6,
inference(resolve,[$cnf( $equal(xor(X_6,falsehood),X_6) )],[refute_0_25,refute_0_33]) ).
cnf(refute_0_35,plain,
( xor(X_6,not(truth)) != X_6
| xor(X_6,not(truth)) != xor(not(X_6),truth)
| X_6 = xor(not(X_6),truth) ),
introduced(tautology,[equality,[$cnf( $equal(xor(X_6,not(truth)),xor(not(X_6),truth)) ),[0],$fot(X_6)]]) ).
cnf(refute_0_36,plain,
( xor(X_6,not(truth)) != xor(not(X_6),truth)
| X_6 = xor(not(X_6),truth) ),
inference(resolve,[$cnf( $equal(xor(X_6,not(truth)),X_6) )],[refute_0_34,refute_0_35]) ).
cnf(refute_0_37,plain,
( xor(X,Y) != xor(Y,X)
| xor(Y,X) = xor(X,Y) ),
inference(subst,[],[refute_0_2:[bind(X0,$fot(xor(X,Y))),bind(Y0,$fot(xor(Y,X)))]]) ).
cnf(refute_0_38,plain,
xor(Y,X) = xor(X,Y),
inference(resolve,[$cnf( $equal(xor(X,Y),xor(Y,X)) )],[xor_commutativity,refute_0_37]) ).
cnf(refute_0_39,plain,
xor(not(X_6),truth) = xor(truth,not(X_6)),
inference(subst,[],[refute_0_38:[bind(X,$fot(truth)),bind(Y,$fot(not(X_6)))]]) ).
cnf(refute_0_40,plain,
( X_6 != xor(not(X_6),truth)
| xor(not(X_6),truth) != xor(truth,not(X_6))
| X_6 = xor(truth,not(X_6)) ),
introduced(tautology,[equality,[$cnf( ~ $equal(X_6,xor(truth,not(X_6))) ),[0],$fot(xor(not(X_6),truth))]]) ).
cnf(refute_0_41,plain,
( X_6 != xor(not(X_6),truth)
| X_6 = xor(truth,not(X_6)) ),
inference(resolve,[$cnf( $equal(xor(not(X_6),truth),xor(truth,not(X_6))) )],[refute_0_39,refute_0_40]) ).
cnf(refute_0_42,plain,
( xor(X_6,not(truth)) != xor(not(X_6),truth)
| X_6 = xor(truth,not(X_6)) ),
inference(resolve,[$cnf( $equal(X_6,xor(not(X_6),truth)) )],[refute_0_36,refute_0_41]) ).
cnf(refute_0_43,plain,
X_6 = xor(truth,not(X_6)),
inference(resolve,[$cnf( $equal(xor(X_6,not(truth)),xor(not(X_6),truth)) )],[refute_0_24,refute_0_42]) ).
cnf(refute_0_44,plain,
( X_6 != xor(truth,not(X_6))
| xor(truth,not(X_6)) = X_6 ),
inference(subst,[],[refute_0_2:[bind(X0,$fot(X_6)),bind(Y0,$fot(xor(truth,not(X_6))))]]) ).
cnf(refute_0_45,plain,
xor(truth,not(X_6)) = X_6,
inference(resolve,[$cnf( $equal(X_6,xor(truth,not(X_6))) )],[refute_0_43,refute_0_44]) ).
cnf(refute_0_46,plain,
( xor(not(X_6),truth) != xor(truth,not(X_6))
| xor(truth,not(X_6)) != X_6
| xor(not(X_6),truth) = X_6 ),
inference(subst,[],[refute_0_31:[bind(X0,$fot(xor(not(X_6),truth))),bind(Y0,$fot(xor(truth,not(X_6)))),bind(Z0,$fot(X_6))]]) ).
cnf(refute_0_47,plain,
( xor(truth,not(X_6)) != X_6
| xor(not(X_6),truth) = X_6 ),
inference(resolve,[$cnf( $equal(xor(not(X_6),truth),xor(truth,not(X_6))) )],[refute_0_39,refute_0_46]) ).
cnf(refute_0_48,plain,
xor(not(X_6),truth) = X_6,
inference(resolve,[$cnf( $equal(xor(truth,not(X_6)),X_6) )],[refute_0_45,refute_0_47]) ).
cnf(refute_0_49,plain,
( xor(X_6,xor(truth,truth)) != xor(not(X_6),truth)
| xor(not(X_6),truth) != X_6
| xor(X_6,xor(truth,truth)) = X_6 ),
inference(subst,[],[refute_0_31:[bind(X0,$fot(xor(X_6,xor(truth,truth)))),bind(Y0,$fot(xor(not(X_6),truth))),bind(Z0,$fot(X_6))]]) ).
cnf(refute_0_50,plain,
( xor(not(X_6),truth) != X_6
| xor(X_6,xor(truth,truth)) = X_6 ),
inference(resolve,[$cnf( $equal(xor(X_6,xor(truth,truth)),xor(not(X_6),truth)) )],[refute_0_12,refute_0_49]) ).
cnf(refute_0_51,plain,
xor(X_6,xor(truth,truth)) = X_6,
inference(resolve,[$cnf( $equal(xor(not(X_6),truth),X_6) )],[refute_0_48,refute_0_50]) ).
cnf(refute_0_52,plain,
( xor(X_6,xor(truth,truth)) != X_6
| xor(X_6,xor(truth,truth)) != not(not(X_6))
| X_6 = not(not(X_6)) ),
introduced(tautology,[equality,[$cnf( $equal(xor(X_6,xor(truth,truth)),not(not(X_6))) ),[0],$fot(X_6)]]) ).
cnf(refute_0_53,plain,
( xor(X_6,xor(truth,truth)) != not(not(X_6))
| X_6 = not(not(X_6)) ),
inference(resolve,[$cnf( $equal(xor(X_6,xor(truth,truth)),X_6) )],[refute_0_51,refute_0_52]) ).
cnf(refute_0_54,plain,
X_6 = not(not(X_6)),
inference(resolve,[$cnf( $equal(xor(X_6,xor(truth,truth)),not(not(X_6))) )],[refute_0_18,refute_0_53]) ).
cnf(refute_0_55,plain,
implies(X_84,implies(X_83,X_82)) = not(not(implies(X_84,implies(X_83,X_82)))),
inference(subst,[],[refute_0_54:[bind(X_6,$fot(implies(X_84,implies(X_83,X_82))))]]) ).
cnf(refute_0_56,plain,
and_star(and_star(not(X_29),X_43),X_44) = and_star(not(X_29),and_star(X_43,X_44)),
inference(subst,[],[and_star_associativity:[bind(X,$fot(not(X_29))),bind(Y,$fot(X_43)),bind(Z,$fot(X_44))]]) ).
cnf(refute_0_57,plain,
and_star(not(X_29),Y) = and_star(Y,not(X_29)),
inference(subst,[],[and_star_commutativity:[bind(X,$fot(not(X_29)))]]) ).
cnf(refute_0_58,plain,
and_star(X_21,not(X_22)) = not(not(and_star(X_21,not(X_22)))),
inference(subst,[],[refute_0_54:[bind(X_6,$fot(and_star(X_21,not(X_22))))]]) ).
cnf(refute_0_59,plain,
not(X_9) = xor(truth,not(not(X_9))),
inference(subst,[],[refute_0_43:[bind(X_6,$fot(not(X_9)))]]) ).
cnf(refute_0_60,plain,
X_9 = not(not(X_9)),
inference(subst,[],[refute_0_54:[bind(X_6,$fot(X_9))]]) ).
cnf(refute_0_61,plain,
( X_9 != not(not(X_9))
| not(not(X_9)) = X_9 ),
inference(subst,[],[refute_0_2:[bind(X0,$fot(X_9)),bind(Y0,$fot(not(not(X_9))))]]) ).
cnf(refute_0_62,plain,
not(not(X_9)) = X_9,
inference(resolve,[$cnf( $equal(X_9,not(not(X_9))) )],[refute_0_60,refute_0_61]) ).
cnf(refute_0_63,plain,
( not(X_9) != xor(truth,not(not(X_9)))
| not(not(X_9)) != X_9
| not(X_9) = xor(truth,X_9) ),
introduced(tautology,[equality,[$cnf( $equal(not(X_9),xor(truth,not(not(X_9)))) ),[1,1],$fot(X_9)]]) ).
cnf(refute_0_64,plain,
( not(X_9) != xor(truth,not(not(X_9)))
| not(X_9) = xor(truth,X_9) ),
inference(resolve,[$cnf( $equal(not(not(X_9)),X_9) )],[refute_0_62,refute_0_63]) ).
cnf(refute_0_65,plain,
not(X_9) = xor(truth,X_9),
inference(resolve,[$cnf( $equal(not(X_9),xor(truth,not(not(X_9)))) )],[refute_0_59,refute_0_64]) ).
cnf(refute_0_66,plain,
( not(X_9) != xor(truth,X_9)
| xor(truth,X_9) = not(X_9) ),
inference(subst,[],[refute_0_2:[bind(X0,$fot(not(X_9))),bind(Y0,$fot(xor(truth,X_9)))]]) ).
cnf(refute_0_67,plain,
xor(truth,X_9) = not(X_9),
inference(resolve,[$cnf( $equal(not(X_9),xor(truth,X_9)) )],[refute_0_65,refute_0_66]) ).
cnf(refute_0_68,plain,
xor(truth,Y) = not(Y),
inference(subst,[],[refute_0_67:[bind(X_9,$fot(Y))]]) ).
cnf(refute_0_69,plain,
and_star(X,xor(truth,Y)) = and_star(X,xor(truth,Y)),
introduced(tautology,[refl,[$fot(and_star(X,xor(truth,Y)))]]) ).
cnf(refute_0_70,plain,
( and_star(X,xor(truth,Y)) != and_star(X,xor(truth,Y))
| xor(truth,Y) != not(Y)
| and_star(X,xor(truth,Y)) = and_star(X,not(Y)) ),
introduced(tautology,[equality,[$cnf( $equal(and_star(X,xor(truth,Y)),and_star(X,xor(truth,Y))) ),[1,1],$fot(not(Y))]]) ).
cnf(refute_0_71,plain,
( xor(truth,Y) != not(Y)
| and_star(X,xor(truth,Y)) = and_star(X,not(Y)) ),
inference(resolve,[$cnf( $equal(and_star(X,xor(truth,Y)),and_star(X,xor(truth,Y))) )],[refute_0_69,refute_0_70]) ).
cnf(refute_0_72,plain,
and_star(X,xor(truth,Y)) = and_star(X,not(Y)),
inference(resolve,[$cnf( $equal(xor(truth,Y),not(Y)) )],[refute_0_68,refute_0_71]) ).
cnf(refute_0_73,plain,
not(and_star(X,xor(truth,Y))) = not(and_star(X,xor(truth,Y))),
introduced(tautology,[refl,[$fot(not(and_star(X,xor(truth,Y))))]]) ).
cnf(refute_0_74,plain,
( and_star(X,xor(truth,Y)) != and_star(X,not(Y))
| not(and_star(X,xor(truth,Y))) != not(and_star(X,xor(truth,Y)))
| not(and_star(X,xor(truth,Y))) = not(and_star(X,not(Y))) ),
introduced(tautology,[equality,[$cnf( $equal(not(and_star(X,xor(truth,Y))),not(and_star(X,xor(truth,Y)))) ),[1,0],$fot(and_star(X,not(Y)))]]) ).
cnf(refute_0_75,plain,
( and_star(X,xor(truth,Y)) != and_star(X,not(Y))
| not(and_star(X,xor(truth,Y))) = not(and_star(X,not(Y))) ),
inference(resolve,[$cnf( $equal(not(and_star(X,xor(truth,Y))),not(and_star(X,xor(truth,Y)))) )],[refute_0_73,refute_0_74]) ).
cnf(refute_0_76,plain,
not(and_star(X,xor(truth,Y))) = not(and_star(X,not(Y))),
inference(resolve,[$cnf( $equal(and_star(X,xor(truth,Y)),and_star(X,not(Y))) )],[refute_0_72,refute_0_75]) ).
cnf(refute_0_77,plain,
xor(truth,and_star(X,xor(truth,Y))) = not(and_star(X,xor(truth,Y))),
inference(subst,[],[refute_0_67:[bind(X_9,$fot(and_star(X,xor(truth,Y))))]]) ).
cnf(refute_0_78,plain,
( not(and_star(X,xor(truth,Y))) != not(and_star(X,not(Y)))
| xor(truth,and_star(X,xor(truth,Y))) != not(and_star(X,xor(truth,Y)))
| xor(truth,and_star(X,xor(truth,Y))) = not(and_star(X,not(Y))) ),
inference(subst,[],[refute_0_31:[bind(X0,$fot(xor(truth,and_star(X,xor(truth,Y))))),bind(Y0,$fot(not(and_star(X,xor(truth,Y))))),bind(Z0,$fot(not(and_star(X,not(Y)))))]]) ).
cnf(refute_0_79,plain,
( not(and_star(X,xor(truth,Y))) != not(and_star(X,not(Y)))
| xor(truth,and_star(X,xor(truth,Y))) = not(and_star(X,not(Y))) ),
inference(resolve,[$cnf( $equal(xor(truth,and_star(X,xor(truth,Y))),not(and_star(X,xor(truth,Y)))) )],[refute_0_77,refute_0_78]) ).
cnf(refute_0_80,plain,
xor(truth,and_star(X,xor(truth,Y))) = not(and_star(X,not(Y))),
inference(resolve,[$cnf( $equal(not(and_star(X,xor(truth,Y))),not(and_star(X,not(Y)))) )],[refute_0_76,refute_0_79]) ).
cnf(refute_0_81,plain,
( implies(X,Y) != xor(truth,and_star(X,xor(truth,Y)))
| xor(truth,and_star(X,xor(truth,Y))) != not(and_star(X,not(Y)))
| implies(X,Y) = not(and_star(X,not(Y))) ),
introduced(tautology,[equality,[$cnf( ~ $equal(implies(X,Y),not(and_star(X,not(Y)))) ),[0],$fot(xor(truth,and_star(X,xor(truth,Y))))]]) ).
cnf(refute_0_82,plain,
( implies(X,Y) != xor(truth,and_star(X,xor(truth,Y)))
| implies(X,Y) = not(and_star(X,not(Y))) ),
inference(resolve,[$cnf( $equal(xor(truth,and_star(X,xor(truth,Y))),not(and_star(X,not(Y)))) )],[refute_0_80,refute_0_81]) ).
cnf(refute_0_83,plain,
implies(X,Y) = not(and_star(X,not(Y))),
inference(resolve,[$cnf( $equal(implies(X,Y),xor(truth,and_star(X,xor(truth,Y)))) )],[implies_definition,refute_0_82]) ).
cnf(refute_0_84,plain,
implies(X_21,X_22) = not(and_star(X_21,not(X_22))),
inference(subst,[],[refute_0_83:[bind(X,$fot(X_21)),bind(Y,$fot(X_22))]]) ).
cnf(refute_0_85,plain,
( implies(X_21,X_22) != not(and_star(X_21,not(X_22)))
| not(and_star(X_21,not(X_22))) = implies(X_21,X_22) ),
inference(subst,[],[refute_0_2:[bind(X0,$fot(implies(X_21,X_22))),bind(Y0,$fot(not(and_star(X_21,not(X_22)))))]]) ).
cnf(refute_0_86,plain,
not(and_star(X_21,not(X_22))) = implies(X_21,X_22),
inference(resolve,[$cnf( $equal(implies(X_21,X_22),not(and_star(X_21,not(X_22)))) )],[refute_0_84,refute_0_85]) ).
cnf(refute_0_87,plain,
( and_star(X_21,not(X_22)) != not(not(and_star(X_21,not(X_22))))
| not(and_star(X_21,not(X_22))) != implies(X_21,X_22)
| and_star(X_21,not(X_22)) = not(implies(X_21,X_22)) ),
introduced(tautology,[equality,[$cnf( $equal(and_star(X_21,not(X_22)),not(not(and_star(X_21,not(X_22))))) ),[1,0],$fot(implies(X_21,X_22))]]) ).
cnf(refute_0_88,plain,
( and_star(X_21,not(X_22)) != not(not(and_star(X_21,not(X_22))))
| and_star(X_21,not(X_22)) = not(implies(X_21,X_22)) ),
inference(resolve,[$cnf( $equal(not(and_star(X_21,not(X_22))),implies(X_21,X_22)) )],[refute_0_86,refute_0_87]) ).
cnf(refute_0_89,plain,
and_star(X_21,not(X_22)) = not(implies(X_21,X_22)),
inference(resolve,[$cnf( $equal(and_star(X_21,not(X_22)),not(not(and_star(X_21,not(X_22))))) )],[refute_0_58,refute_0_88]) ).
cnf(refute_0_90,plain,
and_star(Y,not(X_29)) = not(implies(Y,X_29)),
inference(subst,[],[refute_0_89:[bind(X_21,$fot(Y)),bind(X_22,$fot(X_29))]]) ).
cnf(refute_0_91,plain,
( and_star(Y,not(X_29)) != not(implies(Y,X_29))
| and_star(not(X_29),Y) != and_star(Y,not(X_29))
| and_star(not(X_29),Y) = not(implies(Y,X_29)) ),
introduced(tautology,[equality,[$cnf( $equal(and_star(not(X_29),Y),and_star(Y,not(X_29))) ),[1],$fot(not(implies(Y,X_29)))]]) ).
cnf(refute_0_92,plain,
( and_star(not(X_29),Y) != and_star(Y,not(X_29))
| and_star(not(X_29),Y) = not(implies(Y,X_29)) ),
inference(resolve,[$cnf( $equal(and_star(Y,not(X_29)),not(implies(Y,X_29))) )],[refute_0_90,refute_0_91]) ).
cnf(refute_0_93,plain,
and_star(not(X_29),Y) = not(implies(Y,X_29)),
inference(resolve,[$cnf( $equal(and_star(not(X_29),Y),and_star(Y,not(X_29))) )],[refute_0_57,refute_0_92]) ).
cnf(refute_0_94,plain,
and_star(not(X_29),X_43) = not(implies(X_43,X_29)),
inference(subst,[],[refute_0_93:[bind(Y,$fot(X_43))]]) ).
cnf(refute_0_95,plain,
( and_star(and_star(not(X_29),X_43),X_44) != and_star(not(X_29),and_star(X_43,X_44))
| and_star(not(X_29),X_43) != not(implies(X_43,X_29))
| and_star(not(implies(X_43,X_29)),X_44) = and_star(not(X_29),and_star(X_43,X_44)) ),
introduced(tautology,[equality,[$cnf( $equal(and_star(and_star(not(X_29),X_43),X_44),and_star(not(X_29),and_star(X_43,X_44))) ),[0,0],$fot(not(implies(X_43,X_29)))]]) ).
cnf(refute_0_96,plain,
( and_star(and_star(not(X_29),X_43),X_44) != and_star(not(X_29),and_star(X_43,X_44))
| and_star(not(implies(X_43,X_29)),X_44) = and_star(not(X_29),and_star(X_43,X_44)) ),
inference(resolve,[$cnf( $equal(and_star(not(X_29),X_43),not(implies(X_43,X_29))) )],[refute_0_94,refute_0_95]) ).
cnf(refute_0_97,plain,
and_star(not(implies(X_43,X_29)),X_44) = and_star(not(X_29),and_star(X_43,X_44)),
inference(resolve,[$cnf( $equal(and_star(and_star(not(X_29),X_43),X_44),and_star(not(X_29),and_star(X_43,X_44))) )],[refute_0_56,refute_0_96]) ).
cnf(refute_0_98,plain,
and_star(not(implies(X_43,X_29)),X_44) = not(implies(X_44,implies(X_43,X_29))),
inference(subst,[],[refute_0_93:[bind(Y,$fot(X_44)),bind(X_29,$fot(implies(X_43,X_29)))]]) ).
cnf(refute_0_99,plain,
( and_star(not(implies(X_43,X_29)),X_44) != and_star(not(X_29),and_star(X_43,X_44))
| and_star(not(implies(X_43,X_29)),X_44) != not(implies(X_44,implies(X_43,X_29)))
| not(implies(X_44,implies(X_43,X_29))) = and_star(not(X_29),and_star(X_43,X_44)) ),
introduced(tautology,[equality,[$cnf( $equal(and_star(not(implies(X_43,X_29)),X_44),and_star(not(X_29),and_star(X_43,X_44))) ),[0],$fot(not(implies(X_44,implies(X_43,X_29))))]]) ).
cnf(refute_0_100,plain,
( and_star(not(implies(X_43,X_29)),X_44) != and_star(not(X_29),and_star(X_43,X_44))
| not(implies(X_44,implies(X_43,X_29))) = and_star(not(X_29),and_star(X_43,X_44)) ),
inference(resolve,[$cnf( $equal(and_star(not(implies(X_43,X_29)),X_44),not(implies(X_44,implies(X_43,X_29)))) )],[refute_0_98,refute_0_99]) ).
cnf(refute_0_101,plain,
and_star(and_star(X_42,X_43),not(X_22)) = not(implies(and_star(X_42,X_43),X_22)),
inference(subst,[],[refute_0_89:[bind(X_21,$fot(and_star(X_42,X_43)))]]) ).
cnf(refute_0_102,plain,
and_star(and_star(X_42,X_43),not(X_22)) = and_star(X_42,and_star(X_43,not(X_22))),
inference(subst,[],[and_star_associativity:[bind(X,$fot(X_42)),bind(Y,$fot(X_43)),bind(Z,$fot(not(X_22)))]]) ).
cnf(refute_0_103,plain,
( and_star(and_star(X_42,X_43),not(X_22)) != and_star(X_42,and_star(X_43,not(X_22)))
| and_star(and_star(X_42,X_43),not(X_22)) != not(implies(and_star(X_42,X_43),X_22))
| and_star(X_42,and_star(X_43,not(X_22))) = not(implies(and_star(X_42,X_43),X_22)) ),
introduced(tautology,[equality,[$cnf( $equal(and_star(and_star(X_42,X_43),not(X_22)),not(implies(and_star(X_42,X_43),X_22))) ),[0],$fot(and_star(X_42,and_star(X_43,not(X_22))))]]) ).
cnf(refute_0_104,plain,
( and_star(and_star(X_42,X_43),not(X_22)) != not(implies(and_star(X_42,X_43),X_22))
| and_star(X_42,and_star(X_43,not(X_22))) = not(implies(and_star(X_42,X_43),X_22)) ),
inference(resolve,[$cnf( $equal(and_star(and_star(X_42,X_43),not(X_22)),and_star(X_42,and_star(X_43,not(X_22)))) )],[refute_0_102,refute_0_103]) ).
cnf(refute_0_105,plain,
and_star(X_42,and_star(X_43,not(X_22))) = not(implies(and_star(X_42,X_43),X_22)),
inference(resolve,[$cnf( $equal(and_star(and_star(X_42,X_43),not(X_22)),not(implies(and_star(X_42,X_43),X_22))) )],[refute_0_101,refute_0_104]) ).
cnf(refute_0_106,plain,
and_star(X_42,not(implies(X_43,X_22))) = not(implies(X_42,implies(X_43,X_22))),
inference(subst,[],[refute_0_89:[bind(X_21,$fot(X_42)),bind(X_22,$fot(implies(X_43,X_22)))]]) ).
cnf(refute_0_107,plain,
and_star(X_43,not(X_22)) = not(implies(X_43,X_22)),
inference(subst,[],[refute_0_89:[bind(X_21,$fot(X_43))]]) ).
cnf(refute_0_108,plain,
and_star(X_42,and_star(X_43,not(X_22))) = and_star(X_42,and_star(X_43,not(X_22))),
introduced(tautology,[refl,[$fot(and_star(X_42,and_star(X_43,not(X_22))))]]) ).
cnf(refute_0_109,plain,
( and_star(X_42,and_star(X_43,not(X_22))) != and_star(X_42,and_star(X_43,not(X_22)))
| and_star(X_43,not(X_22)) != not(implies(X_43,X_22))
| and_star(X_42,and_star(X_43,not(X_22))) = and_star(X_42,not(implies(X_43,X_22))) ),
introduced(tautology,[equality,[$cnf( $equal(and_star(X_42,and_star(X_43,not(X_22))),and_star(X_42,and_star(X_43,not(X_22)))) ),[1,1],$fot(not(implies(X_43,X_22)))]]) ).
cnf(refute_0_110,plain,
( and_star(X_43,not(X_22)) != not(implies(X_43,X_22))
| and_star(X_42,and_star(X_43,not(X_22))) = and_star(X_42,not(implies(X_43,X_22))) ),
inference(resolve,[$cnf( $equal(and_star(X_42,and_star(X_43,not(X_22))),and_star(X_42,and_star(X_43,not(X_22)))) )],[refute_0_108,refute_0_109]) ).
cnf(refute_0_111,plain,
and_star(X_42,and_star(X_43,not(X_22))) = and_star(X_42,not(implies(X_43,X_22))),
inference(resolve,[$cnf( $equal(and_star(X_43,not(X_22)),not(implies(X_43,X_22))) )],[refute_0_107,refute_0_110]) ).
cnf(refute_0_112,plain,
( and_star(X_42,and_star(X_43,not(X_22))) != and_star(X_42,not(implies(X_43,X_22)))
| and_star(X_42,not(implies(X_43,X_22))) != not(implies(X_42,implies(X_43,X_22)))
| and_star(X_42,and_star(X_43,not(X_22))) = not(implies(X_42,implies(X_43,X_22))) ),
inference(subst,[],[refute_0_31:[bind(X0,$fot(and_star(X_42,and_star(X_43,not(X_22))))),bind(Y0,$fot(and_star(X_42,not(implies(X_43,X_22))))),bind(Z0,$fot(not(implies(X_42,implies(X_43,X_22)))))]]) ).
cnf(refute_0_113,plain,
( and_star(X_42,not(implies(X_43,X_22))) != not(implies(X_42,implies(X_43,X_22)))
| and_star(X_42,and_star(X_43,not(X_22))) = not(implies(X_42,implies(X_43,X_22))) ),
inference(resolve,[$cnf( $equal(and_star(X_42,and_star(X_43,not(X_22))),and_star(X_42,not(implies(X_43,X_22)))) )],[refute_0_111,refute_0_112]) ).
cnf(refute_0_114,plain,
and_star(X_42,and_star(X_43,not(X_22))) = not(implies(X_42,implies(X_43,X_22))),
inference(resolve,[$cnf( $equal(and_star(X_42,not(implies(X_43,X_22))),not(implies(X_42,implies(X_43,X_22)))) )],[refute_0_106,refute_0_113]) ).
cnf(refute_0_115,plain,
( and_star(X_42,and_star(X_43,not(X_22))) != not(implies(X_42,implies(X_43,X_22)))
| and_star(X_42,and_star(X_43,not(X_22))) != not(implies(and_star(X_42,X_43),X_22))
| not(implies(X_42,implies(X_43,X_22))) = not(implies(and_star(X_42,X_43),X_22)) ),
introduced(tautology,[equality,[$cnf( $equal(and_star(X_42,and_star(X_43,not(X_22))),not(implies(and_star(X_42,X_43),X_22))) ),[0],$fot(not(implies(X_42,implies(X_43,X_22))))]]) ).
cnf(refute_0_116,plain,
( and_star(X_42,and_star(X_43,not(X_22))) != not(implies(and_star(X_42,X_43),X_22))
| not(implies(X_42,implies(X_43,X_22))) = not(implies(and_star(X_42,X_43),X_22)) ),
inference(resolve,[$cnf( $equal(and_star(X_42,and_star(X_43,not(X_22))),not(implies(X_42,implies(X_43,X_22)))) )],[refute_0_114,refute_0_115]) ).
cnf(refute_0_117,plain,
not(implies(X_42,implies(X_43,X_22))) = not(implies(and_star(X_42,X_43),X_22)),
inference(resolve,[$cnf( $equal(and_star(X_42,and_star(X_43,not(X_22))),not(implies(and_star(X_42,X_43),X_22))) )],[refute_0_105,refute_0_116]) ).
cnf(refute_0_118,plain,
( not(implies(X_42,implies(X_43,X_22))) != not(implies(and_star(X_42,X_43),X_22))
| not(implies(and_star(X_42,X_43),X_22)) = not(implies(X_42,implies(X_43,X_22))) ),
inference(subst,[],[refute_0_2:[bind(X0,$fot(not(implies(X_42,implies(X_43,X_22))))),bind(Y0,$fot(not(implies(and_star(X_42,X_43),X_22))))]]) ).
cnf(refute_0_119,plain,
not(implies(and_star(X_42,X_43),X_22)) = not(implies(X_42,implies(X_43,X_22))),
inference(resolve,[$cnf( $equal(not(implies(X_42,implies(X_43,X_22))),not(implies(and_star(X_42,X_43),X_22))) )],[refute_0_117,refute_0_118]) ).
cnf(refute_0_120,plain,
not(implies(and_star(X_43,X_44),X_29)) = not(implies(X_43,implies(X_44,X_29))),
inference(subst,[],[refute_0_119:[bind(X_22,$fot(X_29)),bind(X_42,$fot(X_43)),bind(X_43,$fot(X_44))]]) ).
cnf(refute_0_121,plain,
and_star(not(X_29),and_star(X_43,X_44)) = not(implies(and_star(X_43,X_44),X_29)),
inference(subst,[],[refute_0_93:[bind(Y,$fot(and_star(X_43,X_44)))]]) ).
cnf(refute_0_122,plain,
( and_star(not(X_29),and_star(X_43,X_44)) != not(implies(and_star(X_43,X_44),X_29))
| not(implies(and_star(X_43,X_44),X_29)) != not(implies(X_43,implies(X_44,X_29)))
| and_star(not(X_29),and_star(X_43,X_44)) = not(implies(X_43,implies(X_44,X_29))) ),
inference(subst,[],[refute_0_31:[bind(X0,$fot(and_star(not(X_29),and_star(X_43,X_44)))),bind(Y0,$fot(not(implies(and_star(X_43,X_44),X_29)))),bind(Z0,$fot(not(implies(X_43,implies(X_44,X_29)))))]]) ).
cnf(refute_0_123,plain,
( not(implies(and_star(X_43,X_44),X_29)) != not(implies(X_43,implies(X_44,X_29)))
| and_star(not(X_29),and_star(X_43,X_44)) = not(implies(X_43,implies(X_44,X_29))) ),
inference(resolve,[$cnf( $equal(and_star(not(X_29),and_star(X_43,X_44)),not(implies(and_star(X_43,X_44),X_29))) )],[refute_0_121,refute_0_122]) ).
cnf(refute_0_124,plain,
and_star(not(X_29),and_star(X_43,X_44)) = not(implies(X_43,implies(X_44,X_29))),
inference(resolve,[$cnf( $equal(not(implies(and_star(X_43,X_44),X_29)),not(implies(X_43,implies(X_44,X_29)))) )],[refute_0_120,refute_0_123]) ).
cnf(refute_0_125,plain,
( and_star(not(X_29),and_star(X_43,X_44)) != not(implies(X_43,implies(X_44,X_29)))
| not(implies(X_44,implies(X_43,X_29))) != and_star(not(X_29),and_star(X_43,X_44))
| not(implies(X_44,implies(X_43,X_29))) = not(implies(X_43,implies(X_44,X_29))) ),
introduced(tautology,[equality,[$cnf( $equal(not(implies(X_44,implies(X_43,X_29))),and_star(not(X_29),and_star(X_43,X_44))) ),[1],$fot(not(implies(X_43,implies(X_44,X_29))))]]) ).
cnf(refute_0_126,plain,
( not(implies(X_44,implies(X_43,X_29))) != and_star(not(X_29),and_star(X_43,X_44))
| not(implies(X_44,implies(X_43,X_29))) = not(implies(X_43,implies(X_44,X_29))) ),
inference(resolve,[$cnf( $equal(and_star(not(X_29),and_star(X_43,X_44)),not(implies(X_43,implies(X_44,X_29)))) )],[refute_0_124,refute_0_125]) ).
cnf(refute_0_127,plain,
( and_star(not(implies(X_43,X_29)),X_44) != and_star(not(X_29),and_star(X_43,X_44))
| not(implies(X_44,implies(X_43,X_29))) = not(implies(X_43,implies(X_44,X_29))) ),
inference(resolve,[$cnf( $equal(not(implies(X_44,implies(X_43,X_29))),and_star(not(X_29),and_star(X_43,X_44))) )],[refute_0_100,refute_0_126]) ).
cnf(refute_0_128,plain,
not(implies(X_44,implies(X_43,X_29))) = not(implies(X_43,implies(X_44,X_29))),
inference(resolve,[$cnf( $equal(and_star(not(implies(X_43,X_29)),X_44),and_star(not(X_29),and_star(X_43,X_44))) )],[refute_0_97,refute_0_127]) ).
cnf(refute_0_129,plain,
not(implies(X_84,implies(X_83,X_82))) = not(implies(X_83,implies(X_84,X_82))),
inference(subst,[],[refute_0_128:[bind(X_29,$fot(X_82)),bind(X_43,$fot(X_83)),bind(X_44,$fot(X_84))]]) ).
cnf(refute_0_130,plain,
( implies(X_84,implies(X_83,X_82)) != not(not(implies(X_84,implies(X_83,X_82))))
| not(implies(X_84,implies(X_83,X_82))) != not(implies(X_83,implies(X_84,X_82)))
| implies(X_84,implies(X_83,X_82)) = not(not(implies(X_83,implies(X_84,X_82)))) ),
introduced(tautology,[equality,[$cnf( $equal(implies(X_84,implies(X_83,X_82)),not(not(implies(X_84,implies(X_83,X_82))))) ),[1,0],$fot(not(implies(X_83,implies(X_84,X_82))))]]) ).
cnf(refute_0_131,plain,
( implies(X_84,implies(X_83,X_82)) != not(not(implies(X_84,implies(X_83,X_82))))
| implies(X_84,implies(X_83,X_82)) = not(not(implies(X_83,implies(X_84,X_82)))) ),
inference(resolve,[$cnf( $equal(not(implies(X_84,implies(X_83,X_82))),not(implies(X_83,implies(X_84,X_82)))) )],[refute_0_129,refute_0_130]) ).
cnf(refute_0_132,plain,
implies(X_84,implies(X_83,X_82)) = not(not(implies(X_83,implies(X_84,X_82)))),
inference(resolve,[$cnf( $equal(implies(X_84,implies(X_83,X_82)),not(not(implies(X_84,implies(X_83,X_82))))) )],[refute_0_55,refute_0_131]) ).
cnf(refute_0_133,plain,
( X_6 != not(not(X_6))
| not(not(X_6)) = X_6 ),
inference(subst,[],[refute_0_2:[bind(X0,$fot(X_6)),bind(Y0,$fot(not(not(X_6))))]]) ).
cnf(refute_0_134,plain,
not(not(X_6)) = X_6,
inference(resolve,[$cnf( $equal(X_6,not(not(X_6))) )],[refute_0_54,refute_0_133]) ).
cnf(refute_0_135,plain,
not(not(implies(X_83,implies(X_84,X_82)))) = implies(X_83,implies(X_84,X_82)),
inference(subst,[],[refute_0_134:[bind(X_6,$fot(implies(X_83,implies(X_84,X_82))))]]) ).
cnf(refute_0_136,plain,
( implies(X_84,implies(X_83,X_82)) != not(not(implies(X_83,implies(X_84,X_82))))
| not(not(implies(X_83,implies(X_84,X_82)))) != implies(X_83,implies(X_84,X_82))
| implies(X_84,implies(X_83,X_82)) = implies(X_83,implies(X_84,X_82)) ),
introduced(tautology,[equality,[$cnf( ~ $equal(implies(X_84,implies(X_83,X_82)),implies(X_83,implies(X_84,X_82))) ),[0],$fot(not(not(implies(X_83,implies(X_84,X_82)))))]]) ).
cnf(refute_0_137,plain,
( implies(X_84,implies(X_83,X_82)) != not(not(implies(X_83,implies(X_84,X_82))))
| implies(X_84,implies(X_83,X_82)) = implies(X_83,implies(X_84,X_82)) ),
inference(resolve,[$cnf( $equal(not(not(implies(X_83,implies(X_84,X_82)))),implies(X_83,implies(X_84,X_82))) )],[refute_0_135,refute_0_136]) ).
cnf(refute_0_138,plain,
implies(X_84,implies(X_83,X_82)) = implies(X_83,implies(X_84,X_82)),
inference(resolve,[$cnf( $equal(implies(X_84,implies(X_83,X_82)),not(not(implies(X_83,implies(X_84,X_82))))) )],[refute_0_132,refute_0_137]) ).
cnf(refute_0_139,plain,
( implies(X_84,implies(X_83,X_82)) != implies(X_83,implies(X_84,X_82))
| implies(X_83,implies(X_84,X_82)) = implies(X_84,implies(X_83,X_82)) ),
inference(subst,[],[refute_0_2:[bind(X0,$fot(implies(X_84,implies(X_83,X_82)))),bind(Y0,$fot(implies(X_83,implies(X_84,X_82))))]]) ).
cnf(refute_0_140,plain,
implies(X_83,implies(X_84,X_82)) = implies(X_84,implies(X_83,X_82)),
inference(resolve,[$cnf( $equal(implies(X_84,implies(X_83,X_82)),implies(X_83,implies(X_84,X_82))) )],[refute_0_138,refute_0_139]) ).
cnf(refute_0_141,plain,
implies(implies(x,y),implies(x,implies(implies(y,z),z))) = implies(x,implies(implies(x,y),implies(implies(y,z),z))),
inference(subst,[],[refute_0_140:[bind(X_82,$fot(implies(implies(y,z),z))),bind(X_83,$fot(implies(x,y))),bind(X_84,$fot(x))]]) ).
cnf(refute_0_142,plain,
implies(implies(y,z),implies(x,z)) = implies(x,implies(implies(y,z),z)),
inference(subst,[],[refute_0_140:[bind(X_82,$fot(z)),bind(X_83,$fot(implies(y,z))),bind(X_84,$fot(x))]]) ).
cnf(refute_0_143,plain,
implies(implies(x,y),implies(implies(y,z),implies(x,z))) = implies(implies(x,y),implies(implies(y,z),implies(x,z))),
introduced(tautology,[refl,[$fot(implies(implies(x,y),implies(implies(y,z),implies(x,z))))]]) ).
cnf(refute_0_144,plain,
( implies(implies(x,y),implies(implies(y,z),implies(x,z))) != implies(implies(x,y),implies(implies(y,z),implies(x,z)))
| implies(implies(y,z),implies(x,z)) != implies(x,implies(implies(y,z),z))
| implies(implies(x,y),implies(implies(y,z),implies(x,z))) = implies(implies(x,y),implies(x,implies(implies(y,z),z))) ),
introduced(tautology,[equality,[$cnf( $equal(implies(implies(x,y),implies(implies(y,z),implies(x,z))),implies(implies(x,y),implies(implies(y,z),implies(x,z)))) ),[1,1],$fot(implies(x,implies(implies(y,z),z)))]]) ).
cnf(refute_0_145,plain,
( implies(implies(y,z),implies(x,z)) != implies(x,implies(implies(y,z),z))
| implies(implies(x,y),implies(implies(y,z),implies(x,z))) = implies(implies(x,y),implies(x,implies(implies(y,z),z))) ),
inference(resolve,[$cnf( $equal(implies(implies(x,y),implies(implies(y,z),implies(x,z))),implies(implies(x,y),implies(implies(y,z),implies(x,z)))) )],[refute_0_143,refute_0_144]) ).
cnf(refute_0_146,plain,
implies(implies(x,y),implies(implies(y,z),implies(x,z))) = implies(implies(x,y),implies(x,implies(implies(y,z),z))),
inference(resolve,[$cnf( $equal(implies(implies(y,z),implies(x,z)),implies(x,implies(implies(y,z),z))) )],[refute_0_142,refute_0_145]) ).
cnf(refute_0_147,plain,
( implies(implies(x,y),implies(implies(y,z),implies(x,z))) != implies(implies(x,y),implies(x,implies(implies(y,z),z)))
| implies(implies(x,y),implies(x,implies(implies(y,z),z))) != implies(x,implies(implies(x,y),implies(implies(y,z),z)))
| implies(implies(x,y),implies(implies(y,z),implies(x,z))) = implies(x,implies(implies(x,y),implies(implies(y,z),z))) ),
inference(subst,[],[refute_0_31:[bind(X0,$fot(implies(implies(x,y),implies(implies(y,z),implies(x,z))))),bind(Y0,$fot(implies(implies(x,y),implies(x,implies(implies(y,z),z))))),bind(Z0,$fot(implies(x,implies(implies(x,y),implies(implies(y,z),z)))))]]) ).
cnf(refute_0_148,plain,
( implies(implies(x,y),implies(x,implies(implies(y,z),z))) != implies(x,implies(implies(x,y),implies(implies(y,z),z)))
| implies(implies(x,y),implies(implies(y,z),implies(x,z))) = implies(x,implies(implies(x,y),implies(implies(y,z),z))) ),
inference(resolve,[$cnf( $equal(implies(implies(x,y),implies(implies(y,z),implies(x,z))),implies(implies(x,y),implies(x,implies(implies(y,z),z)))) )],[refute_0_146,refute_0_147]) ).
cnf(refute_0_149,plain,
implies(implies(x,y),implies(implies(y,z),implies(x,z))) = implies(x,implies(implies(x,y),implies(implies(y,z),z))),
inference(resolve,[$cnf( $equal(implies(implies(x,y),implies(x,implies(implies(y,z),z))),implies(x,implies(implies(x,y),implies(implies(y,z),z)))) )],[refute_0_141,refute_0_148]) ).
cnf(refute_0_150,plain,
( implies(implies(x,y),implies(implies(y,z),implies(x,z))) != implies(x,implies(implies(x,y),implies(implies(y,z),z)))
| implies(x,implies(implies(x,y),implies(implies(y,z),z))) != truth
| implies(implies(x,y),implies(implies(y,z),implies(x,z))) = truth ),
introduced(tautology,[equality,[$cnf( ~ $equal(implies(implies(x,y),implies(implies(y,z),implies(x,z))),truth) ),[0],$fot(implies(x,implies(implies(x,y),implies(implies(y,z),z))))]]) ).
cnf(refute_0_151,plain,
( implies(x,implies(implies(x,y),implies(implies(y,z),z))) != truth
| implies(implies(x,y),implies(implies(y,z),implies(x,z))) = truth ),
inference(resolve,[$cnf( $equal(implies(implies(x,y),implies(implies(y,z),implies(x,z))),implies(x,implies(implies(x,y),implies(implies(y,z),z)))) )],[refute_0_149,refute_0_150]) ).
cnf(refute_0_152,plain,
implies(x,implies(implies(x,y),implies(implies(y,z),z))) != truth,
inference(resolve,[$cnf( $equal(implies(implies(x,y),implies(implies(y,z),implies(x,z))),truth) )],[refute_0_151,prove_wajsberg_axiom]) ).
cnf(refute_0_153,plain,
implies(X_21,not(X_6)) = not(and_star(X_21,not(not(X_6)))),
inference(subst,[],[refute_0_83:[bind(X,$fot(X_21)),bind(Y,$fot(not(X_6)))]]) ).
cnf(refute_0_154,plain,
( implies(X_21,not(X_6)) != not(and_star(X_21,not(not(X_6))))
| not(not(X_6)) != X_6
| implies(X_21,not(X_6)) = not(and_star(X_21,X_6)) ),
introduced(tautology,[equality,[$cnf( $equal(implies(X_21,not(X_6)),not(and_star(X_21,not(not(X_6))))) ),[1,0,1],$fot(X_6)]]) ).
cnf(refute_0_155,plain,
( implies(X_21,not(X_6)) != not(and_star(X_21,not(not(X_6))))
| implies(X_21,not(X_6)) = not(and_star(X_21,X_6)) ),
inference(resolve,[$cnf( $equal(not(not(X_6)),X_6) )],[refute_0_134,refute_0_154]) ).
cnf(refute_0_156,plain,
implies(X_21,not(X_6)) = not(and_star(X_21,X_6)),
inference(resolve,[$cnf( $equal(implies(X_21,not(X_6)),not(and_star(X_21,not(not(X_6))))) )],[refute_0_153,refute_0_155]) ).
cnf(refute_0_157,plain,
implies(X_21,not(and_star(X_36,implies(X_36,X_37)))) = not(and_star(X_21,and_star(X_36,implies(X_36,X_37)))),
inference(subst,[],[refute_0_156:[bind(X_6,$fot(and_star(X_36,implies(X_36,X_37))))]]) ).
cnf(refute_0_158,plain,
implies(X_21,not(implies(X_21,X_34))) = not(and_star(X_21,implies(X_21,X_34))),
inference(subst,[],[refute_0_156:[bind(X_6,$fot(implies(X_21,X_34)))]]) ).
cnf(refute_0_159,plain,
xor(and_star(xor(truth,X),Y),truth) = not(and_star(xor(truth,X),Y)),
inference(subst,[],[refute_0_4:[bind(X,$fot(and_star(xor(truth,X),Y)))]]) ).
cnf(refute_0_160,plain,
and_star(xor(and_star(xor(truth,X),Y),truth),Y) = and_star(xor(and_star(xor(truth,X),Y),truth),Y),
introduced(tautology,[refl,[$fot(and_star(xor(and_star(xor(truth,X),Y),truth),Y))]]) ).
cnf(refute_0_161,plain,
( and_star(xor(and_star(xor(truth,X),Y),truth),Y) != and_star(xor(and_star(xor(truth,X),Y),truth),Y)
| xor(and_star(xor(truth,X),Y),truth) != not(and_star(xor(truth,X),Y))
| and_star(xor(and_star(xor(truth,X),Y),truth),Y) = and_star(not(and_star(xor(truth,X),Y)),Y) ),
introduced(tautology,[equality,[$cnf( $equal(and_star(xor(and_star(xor(truth,X),Y),truth),Y),and_star(xor(and_star(xor(truth,X),Y),truth),Y)) ),[1,0],$fot(not(and_star(xor(truth,X),Y)))]]) ).
cnf(refute_0_162,plain,
( xor(and_star(xor(truth,X),Y),truth) != not(and_star(xor(truth,X),Y))
| and_star(xor(and_star(xor(truth,X),Y),truth),Y) = and_star(not(and_star(xor(truth,X),Y)),Y) ),
inference(resolve,[$cnf( $equal(and_star(xor(and_star(xor(truth,X),Y),truth),Y),and_star(xor(and_star(xor(truth,X),Y),truth),Y)) )],[refute_0_160,refute_0_161]) ).
cnf(refute_0_163,plain,
and_star(xor(and_star(xor(truth,X),Y),truth),Y) = and_star(not(and_star(xor(truth,X),Y)),Y),
inference(resolve,[$cnf( $equal(xor(and_star(xor(truth,X),Y),truth),not(and_star(xor(truth,X),Y))) )],[refute_0_159,refute_0_162]) ).
cnf(refute_0_164,plain,
( and_star(xor(and_star(xor(truth,X),Y),truth),Y) != and_star(not(and_star(xor(truth,X),Y)),Y)
| and_star(xor(and_star(xor(truth,X),Y),truth),Y) != and_star(xor(and_star(xor(truth,Y),X),truth),X)
| and_star(not(and_star(xor(truth,X),Y)),Y) = and_star(xor(and_star(xor(truth,Y),X),truth),X) ),
introduced(tautology,[equality,[$cnf( $equal(and_star(xor(and_star(xor(truth,X),Y),truth),Y),and_star(xor(and_star(xor(truth,Y),X),truth),X)) ),[0],$fot(and_star(not(and_star(xor(truth,X),Y)),Y))]]) ).
cnf(refute_0_165,plain,
( and_star(xor(and_star(xor(truth,X),Y),truth),Y) != and_star(xor(and_star(xor(truth,Y),X),truth),X)
| and_star(not(and_star(xor(truth,X),Y)),Y) = and_star(xor(and_star(xor(truth,Y),X),truth),X) ),
inference(resolve,[$cnf( $equal(and_star(xor(and_star(xor(truth,X),Y),truth),Y),and_star(not(and_star(xor(truth,X),Y)),Y)) )],[refute_0_163,refute_0_164]) ).
cnf(refute_0_166,plain,
xor(and_star(xor(truth,Y),X),truth) = not(and_star(xor(truth,Y),X)),
inference(subst,[],[refute_0_4:[bind(X,$fot(and_star(xor(truth,Y),X)))]]) ).
cnf(refute_0_167,plain,
and_star(xor(and_star(xor(truth,Y),X),truth),X) = and_star(xor(and_star(xor(truth,Y),X),truth),X),
introduced(tautology,[refl,[$fot(and_star(xor(and_star(xor(truth,Y),X),truth),X))]]) ).
cnf(refute_0_168,plain,
( and_star(xor(and_star(xor(truth,Y),X),truth),X) != and_star(xor(and_star(xor(truth,Y),X),truth),X)
| xor(and_star(xor(truth,Y),X),truth) != not(and_star(xor(truth,Y),X))
| and_star(xor(and_star(xor(truth,Y),X),truth),X) = and_star(not(and_star(xor(truth,Y),X)),X) ),
introduced(tautology,[equality,[$cnf( $equal(and_star(xor(and_star(xor(truth,Y),X),truth),X),and_star(xor(and_star(xor(truth,Y),X),truth),X)) ),[1,0],$fot(not(and_star(xor(truth,Y),X)))]]) ).
cnf(refute_0_169,plain,
( xor(and_star(xor(truth,Y),X),truth) != not(and_star(xor(truth,Y),X))
| and_star(xor(and_star(xor(truth,Y),X),truth),X) = and_star(not(and_star(xor(truth,Y),X)),X) ),
inference(resolve,[$cnf( $equal(and_star(xor(and_star(xor(truth,Y),X),truth),X),and_star(xor(and_star(xor(truth,Y),X),truth),X)) )],[refute_0_167,refute_0_168]) ).
cnf(refute_0_170,plain,
and_star(xor(and_star(xor(truth,Y),X),truth),X) = and_star(not(and_star(xor(truth,Y),X)),X),
inference(resolve,[$cnf( $equal(xor(and_star(xor(truth,Y),X),truth),not(and_star(xor(truth,Y),X))) )],[refute_0_166,refute_0_169]) ).
cnf(refute_0_171,plain,
( and_star(not(and_star(xor(truth,X),Y)),Y) != and_star(xor(and_star(xor(truth,Y),X),truth),X)
| and_star(xor(and_star(xor(truth,Y),X),truth),X) != and_star(not(and_star(xor(truth,Y),X)),X)
| and_star(not(and_star(xor(truth,X),Y)),Y) = and_star(not(and_star(xor(truth,Y),X)),X) ),
introduced(tautology,[equality,[$cnf( ~ $equal(and_star(not(and_star(xor(truth,X),Y)),Y),and_star(not(and_star(xor(truth,Y),X)),X)) ),[0],$fot(and_star(xor(and_star(xor(truth,Y),X),truth),X))]]) ).
cnf(refute_0_172,plain,
( and_star(not(and_star(xor(truth,X),Y)),Y) != and_star(xor(and_star(xor(truth,Y),X),truth),X)
| and_star(not(and_star(xor(truth,X),Y)),Y) = and_star(not(and_star(xor(truth,Y),X)),X) ),
inference(resolve,[$cnf( $equal(and_star(xor(and_star(xor(truth,Y),X),truth),X),and_star(not(and_star(xor(truth,Y),X)),X)) )],[refute_0_170,refute_0_171]) ).
cnf(refute_0_173,plain,
( and_star(xor(and_star(xor(truth,X),Y),truth),Y) != and_star(xor(and_star(xor(truth,Y),X),truth),X)
| and_star(not(and_star(xor(truth,X),Y)),Y) = and_star(not(and_star(xor(truth,Y),X)),X) ),
inference(resolve,[$cnf( $equal(and_star(not(and_star(xor(truth,X),Y)),Y),and_star(xor(and_star(xor(truth,Y),X),truth),X)) )],[refute_0_165,refute_0_172]) ).
cnf(refute_0_174,plain,
and_star(not(and_star(xor(truth,X),Y)),Y) = and_star(not(and_star(xor(truth,Y),X)),X),
inference(resolve,[$cnf( $equal(and_star(xor(and_star(xor(truth,X),Y),truth),Y),and_star(xor(and_star(xor(truth,Y),X),truth),X)) )],[axiom_8,refute_0_173]) ).
cnf(refute_0_175,plain,
( and_star(X,Y) != and_star(Y,X)
| and_star(Y,X) = and_star(X,Y) ),
inference(subst,[],[refute_0_2:[bind(X0,$fot(and_star(X,Y))),bind(Y0,$fot(and_star(Y,X)))]]) ).
cnf(refute_0_176,plain,
and_star(Y,X) = and_star(X,Y),
inference(resolve,[$cnf( $equal(and_star(X,Y),and_star(Y,X)) )],[and_star_commutativity,refute_0_175]) ).
cnf(refute_0_177,plain,
and_star(not(and_star(xor(truth,X),Y)),Y) = and_star(Y,not(and_star(xor(truth,X),Y))),
inference(subst,[],[refute_0_176:[bind(X,$fot(Y)),bind(Y,$fot(not(and_star(xor(truth,X),Y))))]]) ).
cnf(refute_0_178,plain,
( and_star(not(and_star(xor(truth,X),Y)),Y) != and_star(Y,not(and_star(xor(truth,X),Y)))
| and_star(not(and_star(xor(truth,X),Y)),Y) != and_star(not(and_star(xor(truth,Y),X)),X)
| and_star(Y,not(and_star(xor(truth,X),Y))) = and_star(not(and_star(xor(truth,Y),X)),X) ),
introduced(tautology,[equality,[$cnf( $equal(and_star(not(and_star(xor(truth,X),Y)),Y),and_star(not(and_star(xor(truth,Y),X)),X)) ),[0],$fot(and_star(Y,not(and_star(xor(truth,X),Y))))]]) ).
cnf(refute_0_179,plain,
( and_star(not(and_star(xor(truth,X),Y)),Y) != and_star(not(and_star(xor(truth,Y),X)),X)
| and_star(Y,not(and_star(xor(truth,X),Y))) = and_star(not(and_star(xor(truth,Y),X)),X) ),
inference(resolve,[$cnf( $equal(and_star(not(and_star(xor(truth,X),Y)),Y),and_star(Y,not(and_star(xor(truth,X),Y)))) )],[refute_0_177,refute_0_178]) ).
cnf(refute_0_180,plain,
and_star(not(and_star(xor(truth,Y),X)),X) = and_star(X,not(and_star(xor(truth,Y),X))),
inference(subst,[],[refute_0_176:[bind(Y,$fot(not(and_star(xor(truth,Y),X))))]]) ).
cnf(refute_0_181,plain,
( and_star(Y,not(and_star(xor(truth,X),Y))) != and_star(not(and_star(xor(truth,Y),X)),X)
| and_star(not(and_star(xor(truth,Y),X)),X) != and_star(X,not(and_star(xor(truth,Y),X)))
| and_star(Y,not(and_star(xor(truth,X),Y))) = and_star(X,not(and_star(xor(truth,Y),X))) ),
introduced(tautology,[equality,[$cnf( ~ $equal(and_star(Y,not(and_star(xor(truth,X),Y))),and_star(X,not(and_star(xor(truth,Y),X)))) ),[0],$fot(and_star(not(and_star(xor(truth,Y),X)),X))]]) ).
cnf(refute_0_182,plain,
( and_star(Y,not(and_star(xor(truth,X),Y))) != and_star(not(and_star(xor(truth,Y),X)),X)
| and_star(Y,not(and_star(xor(truth,X),Y))) = and_star(X,not(and_star(xor(truth,Y),X))) ),
inference(resolve,[$cnf( $equal(and_star(not(and_star(xor(truth,Y),X)),X),and_star(X,not(and_star(xor(truth,Y),X)))) )],[refute_0_180,refute_0_181]) ).
cnf(refute_0_183,plain,
( and_star(not(and_star(xor(truth,X),Y)),Y) != and_star(not(and_star(xor(truth,Y),X)),X)
| and_star(Y,not(and_star(xor(truth,X),Y))) = and_star(X,not(and_star(xor(truth,Y),X))) ),
inference(resolve,[$cnf( $equal(and_star(Y,not(and_star(xor(truth,X),Y))),and_star(not(and_star(xor(truth,Y),X)),X)) )],[refute_0_179,refute_0_182]) ).
cnf(refute_0_184,plain,
and_star(Y,not(and_star(xor(truth,X),Y))) = and_star(X,not(and_star(xor(truth,Y),X))),
inference(resolve,[$cnf( $equal(and_star(not(and_star(xor(truth,X),Y)),Y),and_star(not(and_star(xor(truth,Y),X)),X)) )],[refute_0_174,refute_0_183]) ).
cnf(refute_0_185,plain,
xor(truth,X) = not(X),
inference(subst,[],[refute_0_67:[bind(X_9,$fot(X))]]) ).
cnf(refute_0_186,plain,
and_star(xor(truth,X),Y) = and_star(xor(truth,X),Y),
introduced(tautology,[refl,[$fot(and_star(xor(truth,X),Y))]]) ).
cnf(refute_0_187,plain,
( and_star(xor(truth,X),Y) != and_star(xor(truth,X),Y)
| xor(truth,X) != not(X)
| and_star(xor(truth,X),Y) = and_star(not(X),Y) ),
introduced(tautology,[equality,[$cnf( $equal(and_star(xor(truth,X),Y),and_star(xor(truth,X),Y)) ),[1,0],$fot(not(X))]]) ).
cnf(refute_0_188,plain,
( xor(truth,X) != not(X)
| and_star(xor(truth,X),Y) = and_star(not(X),Y) ),
inference(resolve,[$cnf( $equal(and_star(xor(truth,X),Y),and_star(xor(truth,X),Y)) )],[refute_0_186,refute_0_187]) ).
cnf(refute_0_189,plain,
and_star(xor(truth,X),Y) = and_star(not(X),Y),
inference(resolve,[$cnf( $equal(xor(truth,X),not(X)) )],[refute_0_185,refute_0_188]) ).
cnf(refute_0_190,plain,
not(and_star(xor(truth,X),Y)) = not(and_star(xor(truth,X),Y)),
introduced(tautology,[refl,[$fot(not(and_star(xor(truth,X),Y)))]]) ).
cnf(refute_0_191,plain,
( and_star(xor(truth,X),Y) != and_star(not(X),Y)
| not(and_star(xor(truth,X),Y)) != not(and_star(xor(truth,X),Y))
| not(and_star(xor(truth,X),Y)) = not(and_star(not(X),Y)) ),
introduced(tautology,[equality,[$cnf( $equal(not(and_star(xor(truth,X),Y)),not(and_star(xor(truth,X),Y))) ),[1,0],$fot(and_star(not(X),Y))]]) ).
cnf(refute_0_192,plain,
( and_star(xor(truth,X),Y) != and_star(not(X),Y)
| not(and_star(xor(truth,X),Y)) = not(and_star(not(X),Y)) ),
inference(resolve,[$cnf( $equal(not(and_star(xor(truth,X),Y)),not(and_star(xor(truth,X),Y))) )],[refute_0_190,refute_0_191]) ).
cnf(refute_0_193,plain,
not(and_star(xor(truth,X),Y)) = not(and_star(not(X),Y)),
inference(resolve,[$cnf( $equal(and_star(xor(truth,X),Y),and_star(not(X),Y)) )],[refute_0_189,refute_0_192]) ).
cnf(refute_0_194,plain,
and_star(Y,not(and_star(xor(truth,X),Y))) = and_star(Y,not(and_star(xor(truth,X),Y))),
introduced(tautology,[refl,[$fot(and_star(Y,not(and_star(xor(truth,X),Y))))]]) ).
cnf(refute_0_195,plain,
( and_star(Y,not(and_star(xor(truth,X),Y))) != and_star(Y,not(and_star(xor(truth,X),Y)))
| not(and_star(xor(truth,X),Y)) != not(and_star(not(X),Y))
| and_star(Y,not(and_star(xor(truth,X),Y))) = and_star(Y,not(and_star(not(X),Y))) ),
introduced(tautology,[equality,[$cnf( $equal(and_star(Y,not(and_star(xor(truth,X),Y))),and_star(Y,not(and_star(xor(truth,X),Y)))) ),[1,1],$fot(not(and_star(not(X),Y)))]]) ).
cnf(refute_0_196,plain,
( not(and_star(xor(truth,X),Y)) != not(and_star(not(X),Y))
| and_star(Y,not(and_star(xor(truth,X),Y))) = and_star(Y,not(and_star(not(X),Y))) ),
inference(resolve,[$cnf( $equal(and_star(Y,not(and_star(xor(truth,X),Y))),and_star(Y,not(and_star(xor(truth,X),Y)))) )],[refute_0_194,refute_0_195]) ).
cnf(refute_0_197,plain,
and_star(Y,not(and_star(xor(truth,X),Y))) = and_star(Y,not(and_star(not(X),Y))),
inference(resolve,[$cnf( $equal(not(and_star(xor(truth,X),Y)),not(and_star(not(X),Y))) )],[refute_0_193,refute_0_196]) ).
cnf(refute_0_198,plain,
( and_star(Y,not(and_star(xor(truth,X),Y))) != and_star(X,not(and_star(xor(truth,Y),X)))
| and_star(Y,not(and_star(xor(truth,X),Y))) != and_star(Y,not(and_star(not(X),Y)))
| and_star(Y,not(and_star(not(X),Y))) = and_star(X,not(and_star(xor(truth,Y),X))) ),
introduced(tautology,[equality,[$cnf( $equal(and_star(Y,not(and_star(xor(truth,X),Y))),and_star(X,not(and_star(xor(truth,Y),X)))) ),[0],$fot(and_star(Y,not(and_star(not(X),Y))))]]) ).
cnf(refute_0_199,plain,
( and_star(Y,not(and_star(xor(truth,X),Y))) != and_star(X,not(and_star(xor(truth,Y),X)))
| and_star(Y,not(and_star(not(X),Y))) = and_star(X,not(and_star(xor(truth,Y),X))) ),
inference(resolve,[$cnf( $equal(and_star(Y,not(and_star(xor(truth,X),Y))),and_star(Y,not(and_star(not(X),Y)))) )],[refute_0_197,refute_0_198]) ).
cnf(refute_0_200,plain,
and_star(xor(truth,Y),X) = and_star(xor(truth,Y),X),
introduced(tautology,[refl,[$fot(and_star(xor(truth,Y),X))]]) ).
cnf(refute_0_201,plain,
( and_star(xor(truth,Y),X) != and_star(xor(truth,Y),X)
| xor(truth,Y) != not(Y)
| and_star(xor(truth,Y),X) = and_star(not(Y),X) ),
introduced(tautology,[equality,[$cnf( $equal(and_star(xor(truth,Y),X),and_star(xor(truth,Y),X)) ),[1,0],$fot(not(Y))]]) ).
cnf(refute_0_202,plain,
( xor(truth,Y) != not(Y)
| and_star(xor(truth,Y),X) = and_star(not(Y),X) ),
inference(resolve,[$cnf( $equal(and_star(xor(truth,Y),X),and_star(xor(truth,Y),X)) )],[refute_0_200,refute_0_201]) ).
cnf(refute_0_203,plain,
and_star(xor(truth,Y),X) = and_star(not(Y),X),
inference(resolve,[$cnf( $equal(xor(truth,Y),not(Y)) )],[refute_0_68,refute_0_202]) ).
cnf(refute_0_204,plain,
not(and_star(xor(truth,Y),X)) = not(and_star(xor(truth,Y),X)),
introduced(tautology,[refl,[$fot(not(and_star(xor(truth,Y),X)))]]) ).
cnf(refute_0_205,plain,
( and_star(xor(truth,Y),X) != and_star(not(Y),X)
| not(and_star(xor(truth,Y),X)) != not(and_star(xor(truth,Y),X))
| not(and_star(xor(truth,Y),X)) = not(and_star(not(Y),X)) ),
introduced(tautology,[equality,[$cnf( $equal(not(and_star(xor(truth,Y),X)),not(and_star(xor(truth,Y),X))) ),[1,0],$fot(and_star(not(Y),X))]]) ).
cnf(refute_0_206,plain,
( and_star(xor(truth,Y),X) != and_star(not(Y),X)
| not(and_star(xor(truth,Y),X)) = not(and_star(not(Y),X)) ),
inference(resolve,[$cnf( $equal(not(and_star(xor(truth,Y),X)),not(and_star(xor(truth,Y),X))) )],[refute_0_204,refute_0_205]) ).
cnf(refute_0_207,plain,
not(and_star(xor(truth,Y),X)) = not(and_star(not(Y),X)),
inference(resolve,[$cnf( $equal(and_star(xor(truth,Y),X),and_star(not(Y),X)) )],[refute_0_203,refute_0_206]) ).
cnf(refute_0_208,plain,
and_star(X,not(and_star(xor(truth,Y),X))) = and_star(X,not(and_star(xor(truth,Y),X))),
introduced(tautology,[refl,[$fot(and_star(X,not(and_star(xor(truth,Y),X))))]]) ).
cnf(refute_0_209,plain,
( and_star(X,not(and_star(xor(truth,Y),X))) != and_star(X,not(and_star(xor(truth,Y),X)))
| not(and_star(xor(truth,Y),X)) != not(and_star(not(Y),X))
| and_star(X,not(and_star(xor(truth,Y),X))) = and_star(X,not(and_star(not(Y),X))) ),
introduced(tautology,[equality,[$cnf( $equal(and_star(X,not(and_star(xor(truth,Y),X))),and_star(X,not(and_star(xor(truth,Y),X)))) ),[1,1],$fot(not(and_star(not(Y),X)))]]) ).
cnf(refute_0_210,plain,
( not(and_star(xor(truth,Y),X)) != not(and_star(not(Y),X))
| and_star(X,not(and_star(xor(truth,Y),X))) = and_star(X,not(and_star(not(Y),X))) ),
inference(resolve,[$cnf( $equal(and_star(X,not(and_star(xor(truth,Y),X))),and_star(X,not(and_star(xor(truth,Y),X)))) )],[refute_0_208,refute_0_209]) ).
cnf(refute_0_211,plain,
and_star(X,not(and_star(xor(truth,Y),X))) = and_star(X,not(and_star(not(Y),X))),
inference(resolve,[$cnf( $equal(not(and_star(xor(truth,Y),X)),not(and_star(not(Y),X))) )],[refute_0_207,refute_0_210]) ).
cnf(refute_0_212,plain,
( and_star(X,not(and_star(xor(truth,Y),X))) != and_star(X,not(and_star(not(Y),X)))
| and_star(Y,not(and_star(not(X),Y))) != and_star(X,not(and_star(xor(truth,Y),X)))
| and_star(Y,not(and_star(not(X),Y))) = and_star(X,not(and_star(not(Y),X))) ),
introduced(tautology,[equality,[$cnf( $equal(and_star(Y,not(and_star(not(X),Y))),and_star(X,not(and_star(xor(truth,Y),X)))) ),[1],$fot(and_star(X,not(and_star(not(Y),X))))]]) ).
cnf(refute_0_213,plain,
( and_star(Y,not(and_star(not(X),Y))) != and_star(X,not(and_star(xor(truth,Y),X)))
| and_star(Y,not(and_star(not(X),Y))) = and_star(X,not(and_star(not(Y),X))) ),
inference(resolve,[$cnf( $equal(and_star(X,not(and_star(xor(truth,Y),X))),and_star(X,not(and_star(not(Y),X)))) )],[refute_0_211,refute_0_212]) ).
cnf(refute_0_214,plain,
( and_star(Y,not(and_star(xor(truth,X),Y))) != and_star(X,not(and_star(xor(truth,Y),X)))
| and_star(Y,not(and_star(not(X),Y))) = and_star(X,not(and_star(not(Y),X))) ),
inference(resolve,[$cnf( $equal(and_star(Y,not(and_star(not(X),Y))),and_star(X,not(and_star(xor(truth,Y),X)))) )],[refute_0_199,refute_0_213]) ).
cnf(refute_0_215,plain,
and_star(Y,not(and_star(not(X),Y))) = and_star(X,not(and_star(not(Y),X))),
inference(resolve,[$cnf( $equal(and_star(Y,not(and_star(xor(truth,X),Y))),and_star(X,not(and_star(xor(truth,Y),X)))) )],[refute_0_184,refute_0_214]) ).
cnf(refute_0_216,plain,
and_star(Y,not(and_star(not(X),Y))) = not(implies(Y,and_star(not(X),Y))),
inference(subst,[],[refute_0_89:[bind(X_21,$fot(Y)),bind(X_22,$fot(and_star(not(X),Y)))]]) ).
cnf(refute_0_217,plain,
( and_star(Y,not(and_star(not(X),Y))) != and_star(X,not(and_star(not(Y),X)))
| and_star(Y,not(and_star(not(X),Y))) != not(implies(Y,and_star(not(X),Y)))
| not(implies(Y,and_star(not(X),Y))) = and_star(X,not(and_star(not(Y),X))) ),
introduced(tautology,[equality,[$cnf( $equal(and_star(Y,not(and_star(not(X),Y))),and_star(X,not(and_star(not(Y),X)))) ),[0],$fot(not(implies(Y,and_star(not(X),Y))))]]) ).
cnf(refute_0_218,plain,
( and_star(Y,not(and_star(not(X),Y))) != and_star(X,not(and_star(not(Y),X)))
| not(implies(Y,and_star(not(X),Y))) = and_star(X,not(and_star(not(Y),X))) ),
inference(resolve,[$cnf( $equal(and_star(Y,not(and_star(not(X),Y))),not(implies(Y,and_star(not(X),Y)))) )],[refute_0_216,refute_0_217]) ).
cnf(refute_0_219,plain,
and_star(X,not(and_star(not(Y),X))) = not(implies(X,and_star(not(Y),X))),
inference(subst,[],[refute_0_89:[bind(X_21,$fot(X)),bind(X_22,$fot(and_star(not(Y),X)))]]) ).
cnf(refute_0_220,plain,
( and_star(X,not(and_star(not(Y),X))) != not(implies(X,and_star(not(Y),X)))
| not(implies(Y,and_star(not(X),Y))) != and_star(X,not(and_star(not(Y),X)))
| not(implies(Y,and_star(not(X),Y))) = not(implies(X,and_star(not(Y),X))) ),
introduced(tautology,[equality,[$cnf( $equal(not(implies(Y,and_star(not(X),Y))),and_star(X,not(and_star(not(Y),X)))) ),[1],$fot(not(implies(X,and_star(not(Y),X))))]]) ).
cnf(refute_0_221,plain,
( not(implies(Y,and_star(not(X),Y))) != and_star(X,not(and_star(not(Y),X)))
| not(implies(Y,and_star(not(X),Y))) = not(implies(X,and_star(not(Y),X))) ),
inference(resolve,[$cnf( $equal(and_star(X,not(and_star(not(Y),X))),not(implies(X,and_star(not(Y),X)))) )],[refute_0_219,refute_0_220]) ).
cnf(refute_0_222,plain,
( and_star(Y,not(and_star(not(X),Y))) != and_star(X,not(and_star(not(Y),X)))
| not(implies(Y,and_star(not(X),Y))) = not(implies(X,and_star(not(Y),X))) ),
inference(resolve,[$cnf( $equal(not(implies(Y,and_star(not(X),Y))),and_star(X,not(and_star(not(Y),X)))) )],[refute_0_218,refute_0_221]) ).
cnf(refute_0_223,plain,
not(implies(Y,and_star(not(X),Y))) = not(implies(X,and_star(not(Y),X))),
inference(resolve,[$cnf( $equal(and_star(Y,not(and_star(not(X),Y))),and_star(X,not(and_star(not(Y),X)))) )],[refute_0_215,refute_0_222]) ).
cnf(refute_0_224,plain,
not(not(and_star(Y,implies(Y,X)))) = and_star(Y,implies(Y,X)),
inference(subst,[],[refute_0_134:[bind(X_6,$fot(and_star(Y,implies(Y,X))))]]) ).
cnf(refute_0_225,plain,
implies(Y,not(implies(Y,X))) = not(and_star(Y,implies(Y,X))),
inference(subst,[],[refute_0_156:[bind(X_21,$fot(Y)),bind(X_6,$fot(implies(Y,X)))]]) ).
cnf(refute_0_226,plain,
and_star(not(X),Y) = not(implies(Y,X)),
inference(subst,[],[refute_0_93:[bind(X_29,$fot(X))]]) ).
cnf(refute_0_227,plain,
implies(Y,and_star(not(X),Y)) = implies(Y,and_star(not(X),Y)),
introduced(tautology,[refl,[$fot(implies(Y,and_star(not(X),Y)))]]) ).
cnf(refute_0_228,plain,
( and_star(not(X),Y) != not(implies(Y,X))
| implies(Y,and_star(not(X),Y)) != implies(Y,and_star(not(X),Y))
| implies(Y,and_star(not(X),Y)) = implies(Y,not(implies(Y,X))) ),
introduced(tautology,[equality,[$cnf( $equal(implies(Y,and_star(not(X),Y)),implies(Y,and_star(not(X),Y))) ),[1,1],$fot(not(implies(Y,X)))]]) ).
cnf(refute_0_229,plain,
( and_star(not(X),Y) != not(implies(Y,X))
| implies(Y,and_star(not(X),Y)) = implies(Y,not(implies(Y,X))) ),
inference(resolve,[$cnf( $equal(implies(Y,and_star(not(X),Y)),implies(Y,and_star(not(X),Y))) )],[refute_0_227,refute_0_228]) ).
cnf(refute_0_230,plain,
implies(Y,and_star(not(X),Y)) = implies(Y,not(implies(Y,X))),
inference(resolve,[$cnf( $equal(and_star(not(X),Y),not(implies(Y,X))) )],[refute_0_226,refute_0_229]) ).
cnf(refute_0_231,plain,
( implies(Y,and_star(not(X),Y)) != implies(Y,not(implies(Y,X)))
| implies(Y,not(implies(Y,X))) != not(and_star(Y,implies(Y,X)))
| implies(Y,and_star(not(X),Y)) = not(and_star(Y,implies(Y,X))) ),
inference(subst,[],[refute_0_31:[bind(X0,$fot(implies(Y,and_star(not(X),Y)))),bind(Y0,$fot(implies(Y,not(implies(Y,X))))),bind(Z0,$fot(not(and_star(Y,implies(Y,X)))))]]) ).
cnf(refute_0_232,plain,
( implies(Y,not(implies(Y,X))) != not(and_star(Y,implies(Y,X)))
| implies(Y,and_star(not(X),Y)) = not(and_star(Y,implies(Y,X))) ),
inference(resolve,[$cnf( $equal(implies(Y,and_star(not(X),Y)),implies(Y,not(implies(Y,X)))) )],[refute_0_230,refute_0_231]) ).
cnf(refute_0_233,plain,
implies(Y,and_star(not(X),Y)) = not(and_star(Y,implies(Y,X))),
inference(resolve,[$cnf( $equal(implies(Y,not(implies(Y,X))),not(and_star(Y,implies(Y,X)))) )],[refute_0_225,refute_0_232]) ).
cnf(refute_0_234,plain,
not(implies(Y,and_star(not(X),Y))) = not(implies(Y,and_star(not(X),Y))),
introduced(tautology,[refl,[$fot(not(implies(Y,and_star(not(X),Y))))]]) ).
cnf(refute_0_235,plain,
( implies(Y,and_star(not(X),Y)) != not(and_star(Y,implies(Y,X)))
| not(implies(Y,and_star(not(X),Y))) != not(implies(Y,and_star(not(X),Y)))
| not(implies(Y,and_star(not(X),Y))) = not(not(and_star(Y,implies(Y,X)))) ),
introduced(tautology,[equality,[$cnf( $equal(not(implies(Y,and_star(not(X),Y))),not(implies(Y,and_star(not(X),Y)))) ),[1,0],$fot(not(and_star(Y,implies(Y,X))))]]) ).
cnf(refute_0_236,plain,
( implies(Y,and_star(not(X),Y)) != not(and_star(Y,implies(Y,X)))
| not(implies(Y,and_star(not(X),Y))) = not(not(and_star(Y,implies(Y,X)))) ),
inference(resolve,[$cnf( $equal(not(implies(Y,and_star(not(X),Y))),not(implies(Y,and_star(not(X),Y)))) )],[refute_0_234,refute_0_235]) ).
cnf(refute_0_237,plain,
not(implies(Y,and_star(not(X),Y))) = not(not(and_star(Y,implies(Y,X)))),
inference(resolve,[$cnf( $equal(implies(Y,and_star(not(X),Y)),not(and_star(Y,implies(Y,X)))) )],[refute_0_233,refute_0_236]) ).
cnf(refute_0_238,plain,
( not(implies(Y,and_star(not(X),Y))) != not(not(and_star(Y,implies(Y,X))))
| not(not(and_star(Y,implies(Y,X)))) != and_star(Y,implies(Y,X))
| not(implies(Y,and_star(not(X),Y))) = and_star(Y,implies(Y,X)) ),
inference(subst,[],[refute_0_31:[bind(X0,$fot(not(implies(Y,and_star(not(X),Y))))),bind(Y0,$fot(not(not(and_star(Y,implies(Y,X)))))),bind(Z0,$fot(and_star(Y,implies(Y,X))))]]) ).
cnf(refute_0_239,plain,
( not(not(and_star(Y,implies(Y,X)))) != and_star(Y,implies(Y,X))
| not(implies(Y,and_star(not(X),Y))) = and_star(Y,implies(Y,X)) ),
inference(resolve,[$cnf( $equal(not(implies(Y,and_star(not(X),Y))),not(not(and_star(Y,implies(Y,X))))) )],[refute_0_237,refute_0_238]) ).
cnf(refute_0_240,plain,
not(implies(Y,and_star(not(X),Y))) = and_star(Y,implies(Y,X)),
inference(resolve,[$cnf( $equal(not(not(and_star(Y,implies(Y,X)))),and_star(Y,implies(Y,X))) )],[refute_0_224,refute_0_239]) ).
cnf(refute_0_241,plain,
( not(implies(Y,and_star(not(X),Y))) != and_star(Y,implies(Y,X))
| not(implies(Y,and_star(not(X),Y))) != not(implies(X,and_star(not(Y),X)))
| and_star(Y,implies(Y,X)) = not(implies(X,and_star(not(Y),X))) ),
introduced(tautology,[equality,[$cnf( $equal(not(implies(Y,and_star(not(X),Y))),not(implies(X,and_star(not(Y),X)))) ),[0],$fot(and_star(Y,implies(Y,X)))]]) ).
cnf(refute_0_242,plain,
( not(implies(Y,and_star(not(X),Y))) != not(implies(X,and_star(not(Y),X)))
| and_star(Y,implies(Y,X)) = not(implies(X,and_star(not(Y),X))) ),
inference(resolve,[$cnf( $equal(not(implies(Y,and_star(not(X),Y))),and_star(Y,implies(Y,X))) )],[refute_0_240,refute_0_241]) ).
cnf(refute_0_243,plain,
not(not(and_star(X,implies(X,Y)))) = and_star(X,implies(X,Y)),
inference(subst,[],[refute_0_134:[bind(X_6,$fot(and_star(X,implies(X,Y))))]]) ).
cnf(refute_0_244,plain,
implies(X,not(implies(X,Y))) = not(and_star(X,implies(X,Y))),
inference(subst,[],[refute_0_156:[bind(X_21,$fot(X)),bind(X_6,$fot(implies(X,Y)))]]) ).
cnf(refute_0_245,plain,
and_star(not(Y),X) = not(implies(X,Y)),
inference(subst,[],[refute_0_93:[bind(Y,$fot(X)),bind(X_29,$fot(Y))]]) ).
cnf(refute_0_246,plain,
implies(X,and_star(not(Y),X)) = implies(X,and_star(not(Y),X)),
introduced(tautology,[refl,[$fot(implies(X,and_star(not(Y),X)))]]) ).
cnf(refute_0_247,plain,
( and_star(not(Y),X) != not(implies(X,Y))
| implies(X,and_star(not(Y),X)) != implies(X,and_star(not(Y),X))
| implies(X,and_star(not(Y),X)) = implies(X,not(implies(X,Y))) ),
introduced(tautology,[equality,[$cnf( $equal(implies(X,and_star(not(Y),X)),implies(X,and_star(not(Y),X))) ),[1,1],$fot(not(implies(X,Y)))]]) ).
cnf(refute_0_248,plain,
( and_star(not(Y),X) != not(implies(X,Y))
| implies(X,and_star(not(Y),X)) = implies(X,not(implies(X,Y))) ),
inference(resolve,[$cnf( $equal(implies(X,and_star(not(Y),X)),implies(X,and_star(not(Y),X))) )],[refute_0_246,refute_0_247]) ).
cnf(refute_0_249,plain,
implies(X,and_star(not(Y),X)) = implies(X,not(implies(X,Y))),
inference(resolve,[$cnf( $equal(and_star(not(Y),X),not(implies(X,Y))) )],[refute_0_245,refute_0_248]) ).
cnf(refute_0_250,plain,
( implies(X,and_star(not(Y),X)) != implies(X,not(implies(X,Y)))
| implies(X,not(implies(X,Y))) != not(and_star(X,implies(X,Y)))
| implies(X,and_star(not(Y),X)) = not(and_star(X,implies(X,Y))) ),
inference(subst,[],[refute_0_31:[bind(X0,$fot(implies(X,and_star(not(Y),X)))),bind(Y0,$fot(implies(X,not(implies(X,Y))))),bind(Z0,$fot(not(and_star(X,implies(X,Y)))))]]) ).
cnf(refute_0_251,plain,
( implies(X,not(implies(X,Y))) != not(and_star(X,implies(X,Y)))
| implies(X,and_star(not(Y),X)) = not(and_star(X,implies(X,Y))) ),
inference(resolve,[$cnf( $equal(implies(X,and_star(not(Y),X)),implies(X,not(implies(X,Y)))) )],[refute_0_249,refute_0_250]) ).
cnf(refute_0_252,plain,
implies(X,and_star(not(Y),X)) = not(and_star(X,implies(X,Y))),
inference(resolve,[$cnf( $equal(implies(X,not(implies(X,Y))),not(and_star(X,implies(X,Y)))) )],[refute_0_244,refute_0_251]) ).
cnf(refute_0_253,plain,
not(implies(X,and_star(not(Y),X))) = not(implies(X,and_star(not(Y),X))),
introduced(tautology,[refl,[$fot(not(implies(X,and_star(not(Y),X))))]]) ).
cnf(refute_0_254,plain,
( implies(X,and_star(not(Y),X)) != not(and_star(X,implies(X,Y)))
| not(implies(X,and_star(not(Y),X))) != not(implies(X,and_star(not(Y),X)))
| not(implies(X,and_star(not(Y),X))) = not(not(and_star(X,implies(X,Y)))) ),
introduced(tautology,[equality,[$cnf( $equal(not(implies(X,and_star(not(Y),X))),not(implies(X,and_star(not(Y),X)))) ),[1,0],$fot(not(and_star(X,implies(X,Y))))]]) ).
cnf(refute_0_255,plain,
( implies(X,and_star(not(Y),X)) != not(and_star(X,implies(X,Y)))
| not(implies(X,and_star(not(Y),X))) = not(not(and_star(X,implies(X,Y)))) ),
inference(resolve,[$cnf( $equal(not(implies(X,and_star(not(Y),X))),not(implies(X,and_star(not(Y),X)))) )],[refute_0_253,refute_0_254]) ).
cnf(refute_0_256,plain,
not(implies(X,and_star(not(Y),X))) = not(not(and_star(X,implies(X,Y)))),
inference(resolve,[$cnf( $equal(implies(X,and_star(not(Y),X)),not(and_star(X,implies(X,Y)))) )],[refute_0_252,refute_0_255]) ).
cnf(refute_0_257,plain,
( not(implies(X,and_star(not(Y),X))) != not(not(and_star(X,implies(X,Y))))
| not(not(and_star(X,implies(X,Y)))) != and_star(X,implies(X,Y))
| not(implies(X,and_star(not(Y),X))) = and_star(X,implies(X,Y)) ),
inference(subst,[],[refute_0_31:[bind(X0,$fot(not(implies(X,and_star(not(Y),X))))),bind(Y0,$fot(not(not(and_star(X,implies(X,Y)))))),bind(Z0,$fot(and_star(X,implies(X,Y))))]]) ).
cnf(refute_0_258,plain,
( not(not(and_star(X,implies(X,Y)))) != and_star(X,implies(X,Y))
| not(implies(X,and_star(not(Y),X))) = and_star(X,implies(X,Y)) ),
inference(resolve,[$cnf( $equal(not(implies(X,and_star(not(Y),X))),not(not(and_star(X,implies(X,Y))))) )],[refute_0_256,refute_0_257]) ).
cnf(refute_0_259,plain,
not(implies(X,and_star(not(Y),X))) = and_star(X,implies(X,Y)),
inference(resolve,[$cnf( $equal(not(not(and_star(X,implies(X,Y)))),and_star(X,implies(X,Y))) )],[refute_0_243,refute_0_258]) ).
cnf(refute_0_260,plain,
( and_star(Y,implies(Y,X)) != not(implies(X,and_star(not(Y),X)))
| not(implies(X,and_star(not(Y),X))) != and_star(X,implies(X,Y))
| and_star(Y,implies(Y,X)) = and_star(X,implies(X,Y)) ),
introduced(tautology,[equality,[$cnf( ~ $equal(and_star(Y,implies(Y,X)),and_star(X,implies(X,Y))) ),[0],$fot(not(implies(X,and_star(not(Y),X))))]]) ).
cnf(refute_0_261,plain,
( and_star(Y,implies(Y,X)) != not(implies(X,and_star(not(Y),X)))
| and_star(Y,implies(Y,X)) = and_star(X,implies(X,Y)) ),
inference(resolve,[$cnf( $equal(not(implies(X,and_star(not(Y),X))),and_star(X,implies(X,Y))) )],[refute_0_259,refute_0_260]) ).
cnf(refute_0_262,plain,
( not(implies(Y,and_star(not(X),Y))) != not(implies(X,and_star(not(Y),X)))
| and_star(Y,implies(Y,X)) = and_star(X,implies(X,Y)) ),
inference(resolve,[$cnf( $equal(and_star(Y,implies(Y,X)),not(implies(X,and_star(not(Y),X)))) )],[refute_0_242,refute_0_261]) ).
cnf(refute_0_263,plain,
and_star(Y,implies(Y,X)) = and_star(X,implies(X,Y)),
inference(resolve,[$cnf( $equal(not(implies(Y,and_star(not(X),Y))),not(implies(X,and_star(not(Y),X)))) )],[refute_0_223,refute_0_262]) ).
cnf(refute_0_264,plain,
and_star(X_21,implies(X_21,X_34)) = and_star(X_34,implies(X_34,X_21)),
inference(subst,[],[refute_0_263:[bind(X,$fot(X_34)),bind(Y,$fot(X_21))]]) ).
cnf(refute_0_265,plain,
( and_star(X_21,implies(X_21,X_34)) != and_star(X_34,implies(X_34,X_21))
| implies(X_21,not(implies(X_21,X_34))) != not(and_star(X_21,implies(X_21,X_34)))
| implies(X_21,not(implies(X_21,X_34))) = not(and_star(X_34,implies(X_34,X_21))) ),
introduced(tautology,[equality,[$cnf( $equal(implies(X_21,not(implies(X_21,X_34))),not(and_star(X_21,implies(X_21,X_34)))) ),[1,0],$fot(and_star(X_34,implies(X_34,X_21)))]]) ).
cnf(refute_0_266,plain,
( implies(X_21,not(implies(X_21,X_34))) != not(and_star(X_21,implies(X_21,X_34)))
| implies(X_21,not(implies(X_21,X_34))) = not(and_star(X_34,implies(X_34,X_21))) ),
inference(resolve,[$cnf( $equal(and_star(X_21,implies(X_21,X_34)),and_star(X_34,implies(X_34,X_21))) )],[refute_0_264,refute_0_265]) ).
cnf(refute_0_267,plain,
implies(X_21,not(implies(X_21,X_34))) = not(and_star(X_34,implies(X_34,X_21))),
inference(resolve,[$cnf( $equal(implies(X_21,not(implies(X_21,X_34))),not(and_star(X_21,implies(X_21,X_34)))) )],[refute_0_158,refute_0_266]) ).
cnf(refute_0_268,plain,
( implies(X_21,not(implies(X_21,X_34))) != not(and_star(X_21,implies(X_21,X_34)))
| implies(X_21,not(implies(X_21,X_34))) != not(and_star(X_34,implies(X_34,X_21)))
| not(and_star(X_21,implies(X_21,X_34))) = not(and_star(X_34,implies(X_34,X_21))) ),
introduced(tautology,[equality,[$cnf( $equal(implies(X_21,not(implies(X_21,X_34))),not(and_star(X_34,implies(X_34,X_21)))) ),[0],$fot(not(and_star(X_21,implies(X_21,X_34))))]]) ).
cnf(refute_0_269,plain,
( implies(X_21,not(implies(X_21,X_34))) != not(and_star(X_34,implies(X_34,X_21)))
| not(and_star(X_21,implies(X_21,X_34))) = not(and_star(X_34,implies(X_34,X_21))) ),
inference(resolve,[$cnf( $equal(implies(X_21,not(implies(X_21,X_34))),not(and_star(X_21,implies(X_21,X_34)))) )],[refute_0_158,refute_0_268]) ).
cnf(refute_0_270,plain,
not(and_star(X_21,implies(X_21,X_34))) = not(and_star(X_34,implies(X_34,X_21))),
inference(resolve,[$cnf( $equal(implies(X_21,not(implies(X_21,X_34))),not(and_star(X_34,implies(X_34,X_21)))) )],[refute_0_267,refute_0_269]) ).
cnf(refute_0_271,plain,
not(and_star(X_36,implies(X_36,X_37))) = not(and_star(X_37,implies(X_37,X_36))),
inference(subst,[],[refute_0_270:[bind(X_21,$fot(X_36)),bind(X_34,$fot(X_37))]]) ).
cnf(refute_0_272,plain,
( implies(X_21,not(and_star(X_36,implies(X_36,X_37)))) != not(and_star(X_21,and_star(X_36,implies(X_36,X_37))))
| not(and_star(X_36,implies(X_36,X_37))) != not(and_star(X_37,implies(X_37,X_36)))
| implies(X_21,not(and_star(X_37,implies(X_37,X_36)))) = not(and_star(X_21,and_star(X_36,implies(X_36,X_37)))) ),
introduced(tautology,[equality,[$cnf( $equal(implies(X_21,not(and_star(X_36,implies(X_36,X_37)))),not(and_star(X_21,and_star(X_36,implies(X_36,X_37))))) ),[0,1],$fot(not(and_star(X_37,implies(X_37,X_36))))]]) ).
cnf(refute_0_273,plain,
( implies(X_21,not(and_star(X_36,implies(X_36,X_37)))) != not(and_star(X_21,and_star(X_36,implies(X_36,X_37))))
| implies(X_21,not(and_star(X_37,implies(X_37,X_36)))) = not(and_star(X_21,and_star(X_36,implies(X_36,X_37)))) ),
inference(resolve,[$cnf( $equal(not(and_star(X_36,implies(X_36,X_37))),not(and_star(X_37,implies(X_37,X_36)))) )],[refute_0_271,refute_0_272]) ).
cnf(refute_0_274,plain,
implies(X_21,not(and_star(X_37,implies(X_37,X_36)))) = not(and_star(X_21,and_star(X_36,implies(X_36,X_37)))),
inference(resolve,[$cnf( $equal(implies(X_21,not(and_star(X_36,implies(X_36,X_37)))),not(and_star(X_21,and_star(X_36,implies(X_36,X_37))))) )],[refute_0_157,refute_0_273]) ).
cnf(refute_0_275,plain,
implies(X_21,not(and_star(X_37,implies(X_37,X_36)))) = not(and_star(X_21,and_star(X_37,implies(X_37,X_36)))),
inference(subst,[],[refute_0_156:[bind(X_6,$fot(and_star(X_37,implies(X_37,X_36))))]]) ).
cnf(refute_0_276,plain,
( implies(X_21,not(and_star(X_37,implies(X_37,X_36)))) != not(and_star(X_21,and_star(X_36,implies(X_36,X_37))))
| implies(X_21,not(and_star(X_37,implies(X_37,X_36)))) != not(and_star(X_21,and_star(X_37,implies(X_37,X_36))))
| not(and_star(X_21,and_star(X_37,implies(X_37,X_36)))) = not(and_star(X_21,and_star(X_36,implies(X_36,X_37)))) ),
introduced(tautology,[equality,[$cnf( $equal(implies(X_21,not(and_star(X_37,implies(X_37,X_36)))),not(and_star(X_21,and_star(X_36,implies(X_36,X_37))))) ),[0],$fot(not(and_star(X_21,and_star(X_37,implies(X_37,X_36)))))]]) ).
cnf(refute_0_277,plain,
( implies(X_21,not(and_star(X_37,implies(X_37,X_36)))) != not(and_star(X_21,and_star(X_36,implies(X_36,X_37))))
| not(and_star(X_21,and_star(X_37,implies(X_37,X_36)))) = not(and_star(X_21,and_star(X_36,implies(X_36,X_37)))) ),
inference(resolve,[$cnf( $equal(implies(X_21,not(and_star(X_37,implies(X_37,X_36)))),not(and_star(X_21,and_star(X_37,implies(X_37,X_36))))) )],[refute_0_275,refute_0_276]) ).
cnf(refute_0_278,plain,
not(and_star(X_21,and_star(X_37,implies(X_37,X_36)))) = not(and_star(X_21,and_star(X_36,implies(X_36,X_37)))),
inference(resolve,[$cnf( $equal(implies(X_21,not(and_star(X_37,implies(X_37,X_36)))),not(and_star(X_21,and_star(X_36,implies(X_36,X_37))))) )],[refute_0_274,refute_0_277]) ).
cnf(refute_0_279,plain,
not(and_star(not(X_29),and_star(X_143,implies(X_143,X_142)))) = not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143)))),
inference(subst,[],[refute_0_278:[bind(X_21,$fot(not(X_29))),bind(X_36,$fot(X_142)),bind(X_37,$fot(X_143))]]) ).
cnf(refute_0_280,plain,
and_star(not(X_29),and_star(X_143,implies(X_143,X_142))) = not(implies(and_star(X_143,implies(X_143,X_142)),X_29)),
inference(subst,[],[refute_0_93:[bind(Y,$fot(and_star(X_143,implies(X_143,X_142))))]]) ).
cnf(refute_0_281,plain,
( and_star(not(X_29),and_star(X_143,implies(X_143,X_142))) != not(implies(and_star(X_143,implies(X_143,X_142)),X_29))
| not(and_star(not(X_29),and_star(X_143,implies(X_143,X_142)))) != not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143))))
| not(not(implies(and_star(X_143,implies(X_143,X_142)),X_29))) = not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143)))) ),
introduced(tautology,[equality,[$cnf( $equal(not(and_star(not(X_29),and_star(X_143,implies(X_143,X_142)))),not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143))))) ),[0,0],$fot(not(implies(and_star(X_143,implies(X_143,X_142)),X_29)))]]) ).
cnf(refute_0_282,plain,
( not(and_star(not(X_29),and_star(X_143,implies(X_143,X_142)))) != not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143))))
| not(not(implies(and_star(X_143,implies(X_143,X_142)),X_29))) = not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143)))) ),
inference(resolve,[$cnf( $equal(and_star(not(X_29),and_star(X_143,implies(X_143,X_142))),not(implies(and_star(X_143,implies(X_143,X_142)),X_29))) )],[refute_0_280,refute_0_281]) ).
cnf(refute_0_283,plain,
not(not(implies(and_star(X_143,implies(X_143,X_142)),X_29))) = not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143)))),
inference(resolve,[$cnf( $equal(not(and_star(not(X_29),and_star(X_143,implies(X_143,X_142)))),not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143))))) )],[refute_0_279,refute_0_282]) ).
cnf(refute_0_284,plain,
implies(and_star(X_58,X_59),X_57) = not(not(implies(and_star(X_58,X_59),X_57))),
inference(subst,[],[refute_0_54:[bind(X_6,$fot(implies(and_star(X_58,X_59),X_57)))]]) ).
cnf(refute_0_285,plain,
not(implies(X_58,implies(X_59,X_57))) = not(implies(and_star(X_58,X_59),X_57)),
inference(subst,[],[refute_0_117:[bind(X_22,$fot(X_57)),bind(X_42,$fot(X_58)),bind(X_43,$fot(X_59))]]) ).
cnf(refute_0_286,plain,
( not(implies(X_58,implies(X_59,X_57))) != not(implies(and_star(X_58,X_59),X_57))
| not(implies(and_star(X_58,X_59),X_57)) = not(implies(X_58,implies(X_59,X_57))) ),
inference(subst,[],[refute_0_2:[bind(X0,$fot(not(implies(X_58,implies(X_59,X_57))))),bind(Y0,$fot(not(implies(and_star(X_58,X_59),X_57))))]]) ).
cnf(refute_0_287,plain,
not(implies(and_star(X_58,X_59),X_57)) = not(implies(X_58,implies(X_59,X_57))),
inference(resolve,[$cnf( $equal(not(implies(X_58,implies(X_59,X_57))),not(implies(and_star(X_58,X_59),X_57))) )],[refute_0_285,refute_0_286]) ).
cnf(refute_0_288,plain,
( implies(and_star(X_58,X_59),X_57) != not(not(implies(and_star(X_58,X_59),X_57)))
| not(implies(and_star(X_58,X_59),X_57)) != not(implies(X_58,implies(X_59,X_57)))
| implies(and_star(X_58,X_59),X_57) = not(not(implies(X_58,implies(X_59,X_57)))) ),
introduced(tautology,[equality,[$cnf( $equal(implies(and_star(X_58,X_59),X_57),not(not(implies(and_star(X_58,X_59),X_57)))) ),[1,0],$fot(not(implies(X_58,implies(X_59,X_57))))]]) ).
cnf(refute_0_289,plain,
( implies(and_star(X_58,X_59),X_57) != not(not(implies(and_star(X_58,X_59),X_57)))
| implies(and_star(X_58,X_59),X_57) = not(not(implies(X_58,implies(X_59,X_57)))) ),
inference(resolve,[$cnf( $equal(not(implies(and_star(X_58,X_59),X_57)),not(implies(X_58,implies(X_59,X_57)))) )],[refute_0_287,refute_0_288]) ).
cnf(refute_0_290,plain,
implies(and_star(X_58,X_59),X_57) = not(not(implies(X_58,implies(X_59,X_57)))),
inference(resolve,[$cnf( $equal(implies(and_star(X_58,X_59),X_57),not(not(implies(and_star(X_58,X_59),X_57)))) )],[refute_0_284,refute_0_289]) ).
cnf(refute_0_291,plain,
not(not(implies(X_58,implies(X_59,X_57)))) = implies(X_58,implies(X_59,X_57)),
inference(subst,[],[refute_0_134:[bind(X_6,$fot(implies(X_58,implies(X_59,X_57))))]]) ).
cnf(refute_0_292,plain,
( implies(and_star(X_58,X_59),X_57) != not(not(implies(X_58,implies(X_59,X_57))))
| not(not(implies(X_58,implies(X_59,X_57)))) != implies(X_58,implies(X_59,X_57))
| implies(and_star(X_58,X_59),X_57) = implies(X_58,implies(X_59,X_57)) ),
introduced(tautology,[equality,[$cnf( ~ $equal(implies(and_star(X_58,X_59),X_57),implies(X_58,implies(X_59,X_57))) ),[0],$fot(not(not(implies(X_58,implies(X_59,X_57)))))]]) ).
cnf(refute_0_293,plain,
( implies(and_star(X_58,X_59),X_57) != not(not(implies(X_58,implies(X_59,X_57))))
| implies(and_star(X_58,X_59),X_57) = implies(X_58,implies(X_59,X_57)) ),
inference(resolve,[$cnf( $equal(not(not(implies(X_58,implies(X_59,X_57)))),implies(X_58,implies(X_59,X_57))) )],[refute_0_291,refute_0_292]) ).
cnf(refute_0_294,plain,
implies(and_star(X_58,X_59),X_57) = implies(X_58,implies(X_59,X_57)),
inference(resolve,[$cnf( $equal(implies(and_star(X_58,X_59),X_57),not(not(implies(X_58,implies(X_59,X_57))))) )],[refute_0_290,refute_0_293]) ).
cnf(refute_0_295,plain,
implies(and_star(X_143,implies(X_143,X_142)),X_29) = implies(X_143,implies(implies(X_143,X_142),X_29)),
inference(subst,[],[refute_0_294:[bind(X_57,$fot(X_29)),bind(X_58,$fot(X_143)),bind(X_59,$fot(implies(X_143,X_142)))]]) ).
cnf(refute_0_296,plain,
not(not(implies(and_star(X_143,implies(X_143,X_142)),X_29))) = implies(and_star(X_143,implies(X_143,X_142)),X_29),
inference(subst,[],[refute_0_134:[bind(X_6,$fot(implies(and_star(X_143,implies(X_143,X_142)),X_29)))]]) ).
cnf(refute_0_297,plain,
( implies(and_star(X_143,implies(X_143,X_142)),X_29) != implies(X_143,implies(implies(X_143,X_142),X_29))
| not(not(implies(and_star(X_143,implies(X_143,X_142)),X_29))) != implies(and_star(X_143,implies(X_143,X_142)),X_29)
| not(not(implies(and_star(X_143,implies(X_143,X_142)),X_29))) = implies(X_143,implies(implies(X_143,X_142),X_29)) ),
inference(subst,[],[refute_0_31:[bind(X0,$fot(not(not(implies(and_star(X_143,implies(X_143,X_142)),X_29))))),bind(Y0,$fot(implies(and_star(X_143,implies(X_143,X_142)),X_29))),bind(Z0,$fot(implies(X_143,implies(implies(X_143,X_142),X_29))))]]) ).
cnf(refute_0_298,plain,
( implies(and_star(X_143,implies(X_143,X_142)),X_29) != implies(X_143,implies(implies(X_143,X_142),X_29))
| not(not(implies(and_star(X_143,implies(X_143,X_142)),X_29))) = implies(X_143,implies(implies(X_143,X_142),X_29)) ),
inference(resolve,[$cnf( $equal(not(not(implies(and_star(X_143,implies(X_143,X_142)),X_29))),implies(and_star(X_143,implies(X_143,X_142)),X_29)) )],[refute_0_296,refute_0_297]) ).
cnf(refute_0_299,plain,
not(not(implies(and_star(X_143,implies(X_143,X_142)),X_29))) = implies(X_143,implies(implies(X_143,X_142),X_29)),
inference(resolve,[$cnf( $equal(implies(and_star(X_143,implies(X_143,X_142)),X_29),implies(X_143,implies(implies(X_143,X_142),X_29))) )],[refute_0_295,refute_0_298]) ).
cnf(refute_0_300,plain,
( not(not(implies(and_star(X_143,implies(X_143,X_142)),X_29))) != implies(X_143,implies(implies(X_143,X_142),X_29))
| not(not(implies(and_star(X_143,implies(X_143,X_142)),X_29))) != not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143))))
| implies(X_143,implies(implies(X_143,X_142),X_29)) = not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143)))) ),
introduced(tautology,[equality,[$cnf( $equal(not(not(implies(and_star(X_143,implies(X_143,X_142)),X_29))),not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143))))) ),[0],$fot(implies(X_143,implies(implies(X_143,X_142),X_29)))]]) ).
cnf(refute_0_301,plain,
( not(not(implies(and_star(X_143,implies(X_143,X_142)),X_29))) != not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143))))
| implies(X_143,implies(implies(X_143,X_142),X_29)) = not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143)))) ),
inference(resolve,[$cnf( $equal(not(not(implies(and_star(X_143,implies(X_143,X_142)),X_29))),implies(X_143,implies(implies(X_143,X_142),X_29))) )],[refute_0_299,refute_0_300]) ).
cnf(refute_0_302,plain,
not(not(implies(X_142,implies(implies(X_142,X_143),X_29)))) = implies(X_142,implies(implies(X_142,X_143),X_29)),
inference(subst,[],[refute_0_134:[bind(X_6,$fot(implies(X_142,implies(implies(X_142,X_143),X_29))))]]) ).
cnf(refute_0_303,plain,
implies(and_star(X_142,implies(X_142,X_143)),X_29) = implies(X_142,implies(implies(X_142,X_143),X_29)),
inference(subst,[],[refute_0_294:[bind(X_57,$fot(X_29)),bind(X_58,$fot(X_142)),bind(X_59,$fot(implies(X_142,X_143)))]]) ).
cnf(refute_0_304,plain,
not(implies(and_star(X_142,implies(X_142,X_143)),X_29)) = not(implies(and_star(X_142,implies(X_142,X_143)),X_29)),
introduced(tautology,[refl,[$fot(not(implies(and_star(X_142,implies(X_142,X_143)),X_29)))]]) ).
cnf(refute_0_305,plain,
( implies(and_star(X_142,implies(X_142,X_143)),X_29) != implies(X_142,implies(implies(X_142,X_143),X_29))
| not(implies(and_star(X_142,implies(X_142,X_143)),X_29)) != not(implies(and_star(X_142,implies(X_142,X_143)),X_29))
| not(implies(and_star(X_142,implies(X_142,X_143)),X_29)) = not(implies(X_142,implies(implies(X_142,X_143),X_29))) ),
introduced(tautology,[equality,[$cnf( $equal(not(implies(and_star(X_142,implies(X_142,X_143)),X_29)),not(implies(and_star(X_142,implies(X_142,X_143)),X_29))) ),[1,0],$fot(implies(X_142,implies(implies(X_142,X_143),X_29)))]]) ).
cnf(refute_0_306,plain,
( implies(and_star(X_142,implies(X_142,X_143)),X_29) != implies(X_142,implies(implies(X_142,X_143),X_29))
| not(implies(and_star(X_142,implies(X_142,X_143)),X_29)) = not(implies(X_142,implies(implies(X_142,X_143),X_29))) ),
inference(resolve,[$cnf( $equal(not(implies(and_star(X_142,implies(X_142,X_143)),X_29)),not(implies(and_star(X_142,implies(X_142,X_143)),X_29))) )],[refute_0_304,refute_0_305]) ).
cnf(refute_0_307,plain,
not(implies(and_star(X_142,implies(X_142,X_143)),X_29)) = not(implies(X_142,implies(implies(X_142,X_143),X_29))),
inference(resolve,[$cnf( $equal(implies(and_star(X_142,implies(X_142,X_143)),X_29),implies(X_142,implies(implies(X_142,X_143),X_29))) )],[refute_0_303,refute_0_306]) ).
cnf(refute_0_308,plain,
and_star(not(X_29),and_star(X_142,implies(X_142,X_143))) = not(implies(and_star(X_142,implies(X_142,X_143)),X_29)),
inference(subst,[],[refute_0_93:[bind(Y,$fot(and_star(X_142,implies(X_142,X_143))))]]) ).
cnf(refute_0_309,plain,
( and_star(not(X_29),and_star(X_142,implies(X_142,X_143))) != not(implies(and_star(X_142,implies(X_142,X_143)),X_29))
| not(implies(and_star(X_142,implies(X_142,X_143)),X_29)) != not(implies(X_142,implies(implies(X_142,X_143),X_29)))
| and_star(not(X_29),and_star(X_142,implies(X_142,X_143))) = not(implies(X_142,implies(implies(X_142,X_143),X_29))) ),
inference(subst,[],[refute_0_31:[bind(X0,$fot(and_star(not(X_29),and_star(X_142,implies(X_142,X_143))))),bind(Y0,$fot(not(implies(and_star(X_142,implies(X_142,X_143)),X_29)))),bind(Z0,$fot(not(implies(X_142,implies(implies(X_142,X_143),X_29)))))]]) ).
cnf(refute_0_310,plain,
( not(implies(and_star(X_142,implies(X_142,X_143)),X_29)) != not(implies(X_142,implies(implies(X_142,X_143),X_29)))
| and_star(not(X_29),and_star(X_142,implies(X_142,X_143))) = not(implies(X_142,implies(implies(X_142,X_143),X_29))) ),
inference(resolve,[$cnf( $equal(and_star(not(X_29),and_star(X_142,implies(X_142,X_143))),not(implies(and_star(X_142,implies(X_142,X_143)),X_29))) )],[refute_0_308,refute_0_309]) ).
cnf(refute_0_311,plain,
and_star(not(X_29),and_star(X_142,implies(X_142,X_143))) = not(implies(X_142,implies(implies(X_142,X_143),X_29))),
inference(resolve,[$cnf( $equal(not(implies(and_star(X_142,implies(X_142,X_143)),X_29)),not(implies(X_142,implies(implies(X_142,X_143),X_29)))) )],[refute_0_307,refute_0_310]) ).
cnf(refute_0_312,plain,
not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143)))) = not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143)))),
introduced(tautology,[refl,[$fot(not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143)))))]]) ).
cnf(refute_0_313,plain,
( and_star(not(X_29),and_star(X_142,implies(X_142,X_143))) != not(implies(X_142,implies(implies(X_142,X_143),X_29)))
| not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143)))) != not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143))))
| not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143)))) = not(not(implies(X_142,implies(implies(X_142,X_143),X_29)))) ),
introduced(tautology,[equality,[$cnf( $equal(not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143)))),not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143))))) ),[1,0],$fot(not(implies(X_142,implies(implies(X_142,X_143),X_29))))]]) ).
cnf(refute_0_314,plain,
( and_star(not(X_29),and_star(X_142,implies(X_142,X_143))) != not(implies(X_142,implies(implies(X_142,X_143),X_29)))
| not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143)))) = not(not(implies(X_142,implies(implies(X_142,X_143),X_29)))) ),
inference(resolve,[$cnf( $equal(not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143)))),not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143))))) )],[refute_0_312,refute_0_313]) ).
cnf(refute_0_315,plain,
not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143)))) = not(not(implies(X_142,implies(implies(X_142,X_143),X_29)))),
inference(resolve,[$cnf( $equal(and_star(not(X_29),and_star(X_142,implies(X_142,X_143))),not(implies(X_142,implies(implies(X_142,X_143),X_29)))) )],[refute_0_311,refute_0_314]) ).
cnf(refute_0_316,plain,
( not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143)))) != not(not(implies(X_142,implies(implies(X_142,X_143),X_29))))
| not(not(implies(X_142,implies(implies(X_142,X_143),X_29)))) != implies(X_142,implies(implies(X_142,X_143),X_29))
| not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143)))) = implies(X_142,implies(implies(X_142,X_143),X_29)) ),
inference(subst,[],[refute_0_31:[bind(X0,$fot(not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143)))))),bind(Y0,$fot(not(not(implies(X_142,implies(implies(X_142,X_143),X_29)))))),bind(Z0,$fot(implies(X_142,implies(implies(X_142,X_143),X_29))))]]) ).
cnf(refute_0_317,plain,
( not(not(implies(X_142,implies(implies(X_142,X_143),X_29)))) != implies(X_142,implies(implies(X_142,X_143),X_29))
| not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143)))) = implies(X_142,implies(implies(X_142,X_143),X_29)) ),
inference(resolve,[$cnf( $equal(not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143)))),not(not(implies(X_142,implies(implies(X_142,X_143),X_29))))) )],[refute_0_315,refute_0_316]) ).
cnf(refute_0_318,plain,
not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143)))) = implies(X_142,implies(implies(X_142,X_143),X_29)),
inference(resolve,[$cnf( $equal(not(not(implies(X_142,implies(implies(X_142,X_143),X_29)))),implies(X_142,implies(implies(X_142,X_143),X_29))) )],[refute_0_302,refute_0_317]) ).
cnf(refute_0_319,plain,
( implies(X_143,implies(implies(X_143,X_142),X_29)) != not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143))))
| not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143)))) != implies(X_142,implies(implies(X_142,X_143),X_29))
| implies(X_143,implies(implies(X_143,X_142),X_29)) = implies(X_142,implies(implies(X_142,X_143),X_29)) ),
introduced(tautology,[equality,[$cnf( ~ $equal(implies(X_143,implies(implies(X_143,X_142),X_29)),implies(X_142,implies(implies(X_142,X_143),X_29))) ),[0],$fot(not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143)))))]]) ).
cnf(refute_0_320,plain,
( implies(X_143,implies(implies(X_143,X_142),X_29)) != not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143))))
| implies(X_143,implies(implies(X_143,X_142),X_29)) = implies(X_142,implies(implies(X_142,X_143),X_29)) ),
inference(resolve,[$cnf( $equal(not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143)))),implies(X_142,implies(implies(X_142,X_143),X_29))) )],[refute_0_318,refute_0_319]) ).
cnf(refute_0_321,plain,
( not(not(implies(and_star(X_143,implies(X_143,X_142)),X_29))) != not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143))))
| implies(X_143,implies(implies(X_143,X_142),X_29)) = implies(X_142,implies(implies(X_142,X_143),X_29)) ),
inference(resolve,[$cnf( $equal(implies(X_143,implies(implies(X_143,X_142),X_29)),not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143))))) )],[refute_0_301,refute_0_320]) ).
cnf(refute_0_322,plain,
implies(X_143,implies(implies(X_143,X_142),X_29)) = implies(X_142,implies(implies(X_142,X_143),X_29)),
inference(resolve,[$cnf( $equal(not(not(implies(and_star(X_143,implies(X_143,X_142)),X_29))),not(and_star(not(X_29),and_star(X_142,implies(X_142,X_143))))) )],[refute_0_283,refute_0_321]) ).
cnf(refute_0_323,plain,
implies(X_143,implies(implies(X_143,X_142),implies(implies(X_142,X_229),X_229))) = implies(X_142,implies(implies(X_142,X_143),implies(implies(X_142,X_229),X_229))),
inference(subst,[],[refute_0_322:[bind(X_29,$fot(implies(implies(X_142,X_229),X_229)))]]) ).
cnf(refute_0_324,plain,
implies(X_85,implies(X_86,X_85)) = not(not(implies(X_85,implies(X_86,X_85)))),
inference(subst,[],[refute_0_54:[bind(X_6,$fot(implies(X_85,implies(X_86,X_85))))]]) ).
cnf(refute_0_325,plain,
not(implies(X_84,implies(X_82,X_82))) = not(implies(X_82,implies(X_84,X_82))),
inference(subst,[],[refute_0_128:[bind(X_29,$fot(X_82)),bind(X_43,$fot(X_82)),bind(X_44,$fot(X_84))]]) ).
cnf(refute_0_326,plain,
implies(X_22,X_22) = not(and_star(X_22,not(X_22))),
inference(subst,[],[refute_0_83:[bind(X,$fot(X_22)),bind(Y,$fot(X_22))]]) ).
cnf(refute_0_327,plain,
and_star(xor(truth,X),X) = and_star(X,xor(truth,X)),
inference(subst,[],[refute_0_176:[bind(Y,$fot(xor(truth,X)))]]) ).
cnf(refute_0_328,plain,
( and_star(xor(truth,X),X) != and_star(X,xor(truth,X))
| and_star(xor(truth,X),X) != falsehood
| and_star(X,xor(truth,X)) = falsehood ),
introduced(tautology,[equality,[$cnf( $equal(and_star(xor(truth,X),X),falsehood) ),[0],$fot(and_star(X,xor(truth,X)))]]) ).
cnf(refute_0_329,plain,
( and_star(xor(truth,X),X) != falsehood
| and_star(X,xor(truth,X)) = falsehood ),
inference(resolve,[$cnf( $equal(and_star(xor(truth,X),X),and_star(X,xor(truth,X))) )],[refute_0_327,refute_0_328]) ).
cnf(refute_0_330,plain,
and_star(X,xor(truth,X)) = falsehood,
inference(resolve,[$cnf( $equal(and_star(xor(truth,X),X),falsehood) )],[axiom_6,refute_0_329]) ).
cnf(refute_0_331,plain,
and_star(not(X_8),xor(truth,not(X_8))) = falsehood,
inference(subst,[],[refute_0_330:[bind(X,$fot(not(X_8)))]]) ).
cnf(refute_0_332,plain,
X_8 = xor(truth,not(X_8)),
inference(subst,[],[refute_0_43:[bind(X_6,$fot(X_8))]]) ).
cnf(refute_0_333,plain,
( X_8 != xor(truth,not(X_8))
| xor(truth,not(X_8)) = X_8 ),
inference(subst,[],[refute_0_2:[bind(X0,$fot(X_8)),bind(Y0,$fot(xor(truth,not(X_8))))]]) ).
cnf(refute_0_334,plain,
xor(truth,not(X_8)) = X_8,
inference(resolve,[$cnf( $equal(X_8,xor(truth,not(X_8))) )],[refute_0_332,refute_0_333]) ).
cnf(refute_0_335,plain,
( and_star(not(X_8),xor(truth,not(X_8))) != falsehood
| xor(truth,not(X_8)) != X_8
| and_star(not(X_8),X_8) = falsehood ),
introduced(tautology,[equality,[$cnf( $equal(and_star(not(X_8),xor(truth,not(X_8))),falsehood) ),[0,1],$fot(X_8)]]) ).
cnf(refute_0_336,plain,
( and_star(not(X_8),xor(truth,not(X_8))) != falsehood
| and_star(not(X_8),X_8) = falsehood ),
inference(resolve,[$cnf( $equal(xor(truth,not(X_8)),X_8) )],[refute_0_334,refute_0_335]) ).
cnf(refute_0_337,plain,
and_star(not(X_8),X_8) = falsehood,
inference(resolve,[$cnf( $equal(and_star(not(X_8),xor(truth,not(X_8))),falsehood) )],[refute_0_331,refute_0_336]) ).
cnf(refute_0_338,plain,
and_star(not(X_8),X_8) = and_star(X_8,not(X_8)),
inference(subst,[],[refute_0_176:[bind(X,$fot(X_8)),bind(Y,$fot(not(X_8)))]]) ).
cnf(refute_0_339,plain,
( and_star(not(X_8),X_8) != and_star(X_8,not(X_8))
| and_star(not(X_8),X_8) != falsehood
| and_star(X_8,not(X_8)) = falsehood ),
introduced(tautology,[equality,[$cnf( $equal(and_star(not(X_8),X_8),falsehood) ),[0],$fot(and_star(X_8,not(X_8)))]]) ).
cnf(refute_0_340,plain,
( and_star(not(X_8),X_8) != falsehood
| and_star(X_8,not(X_8)) = falsehood ),
inference(resolve,[$cnf( $equal(and_star(not(X_8),X_8),and_star(X_8,not(X_8))) )],[refute_0_338,refute_0_339]) ).
cnf(refute_0_341,plain,
and_star(X_8,not(X_8)) = falsehood,
inference(resolve,[$cnf( $equal(and_star(not(X_8),X_8),falsehood) )],[refute_0_337,refute_0_340]) ).
cnf(refute_0_342,plain,
and_star(X_22,not(X_22)) = falsehood,
inference(subst,[],[refute_0_341:[bind(X_8,$fot(X_22))]]) ).
cnf(refute_0_343,plain,
( and_star(X_22,not(X_22)) != falsehood
| implies(X_22,X_22) != not(and_star(X_22,not(X_22)))
| implies(X_22,X_22) = not(falsehood) ),
introduced(tautology,[equality,[$cnf( $equal(implies(X_22,X_22),not(and_star(X_22,not(X_22)))) ),[1,0],$fot(falsehood)]]) ).
cnf(refute_0_344,plain,
( implies(X_22,X_22) != not(and_star(X_22,not(X_22)))
| implies(X_22,X_22) = not(falsehood) ),
inference(resolve,[$cnf( $equal(and_star(X_22,not(X_22)),falsehood) )],[refute_0_342,refute_0_343]) ).
cnf(refute_0_345,plain,
implies(X_22,X_22) = not(falsehood),
inference(resolve,[$cnf( $equal(implies(X_22,X_22),not(and_star(X_22,not(X_22)))) )],[refute_0_326,refute_0_344]) ).
cnf(refute_0_346,plain,
truth = xor(truth,not(truth)),
inference(subst,[],[refute_0_43:[bind(X_6,$fot(truth))]]) ).
cnf(refute_0_347,plain,
( not(truth) != falsehood
| truth != xor(truth,not(truth))
| truth = xor(truth,falsehood) ),
introduced(tautology,[equality,[$cnf( $equal(truth,xor(truth,not(truth))) ),[1,1],$fot(falsehood)]]) ).
cnf(refute_0_348,plain,
( truth != xor(truth,not(truth))
| truth = xor(truth,falsehood) ),
inference(resolve,[$cnf( $equal(not(truth),falsehood) )],[false_definition,refute_0_347]) ).
cnf(refute_0_349,plain,
truth = xor(truth,falsehood),
inference(resolve,[$cnf( $equal(truth,xor(truth,not(truth))) )],[refute_0_346,refute_0_348]) ).
cnf(refute_0_350,plain,
xor(falsehood,truth) = not(falsehood),
inference(subst,[],[refute_0_4:[bind(X,$fot(falsehood))]]) ).
cnf(refute_0_351,plain,
xor(truth,falsehood) = xor(falsehood,truth),
inference(subst,[],[refute_0_38:[bind(X,$fot(falsehood)),bind(Y,$fot(truth))]]) ).
cnf(refute_0_352,plain,
( xor(falsehood,truth) != not(falsehood)
| xor(truth,falsehood) != xor(falsehood,truth)
| xor(truth,falsehood) = not(falsehood) ),
inference(subst,[],[refute_0_31:[bind(X0,$fot(xor(truth,falsehood))),bind(Y0,$fot(xor(falsehood,truth))),bind(Z0,$fot(not(falsehood)))]]) ).
cnf(refute_0_353,plain,
( xor(falsehood,truth) != not(falsehood)
| xor(truth,falsehood) = not(falsehood) ),
inference(resolve,[$cnf( $equal(xor(truth,falsehood),xor(falsehood,truth)) )],[refute_0_351,refute_0_352]) ).
cnf(refute_0_354,plain,
xor(truth,falsehood) = not(falsehood),
inference(resolve,[$cnf( $equal(xor(falsehood,truth),not(falsehood)) )],[refute_0_350,refute_0_353]) ).
cnf(refute_0_355,plain,
( truth != xor(truth,falsehood)
| xor(truth,falsehood) != not(falsehood)
| truth = not(falsehood) ),
introduced(tautology,[equality,[$cnf( ~ $equal(truth,not(falsehood)) ),[0],$fot(xor(truth,falsehood))]]) ).
cnf(refute_0_356,plain,
( truth != xor(truth,falsehood)
| truth = not(falsehood) ),
inference(resolve,[$cnf( $equal(xor(truth,falsehood),not(falsehood)) )],[refute_0_354,refute_0_355]) ).
cnf(refute_0_357,plain,
truth = not(falsehood),
inference(resolve,[$cnf( $equal(truth,xor(truth,falsehood)) )],[refute_0_349,refute_0_356]) ).
cnf(refute_0_358,plain,
( truth != not(falsehood)
| not(falsehood) = truth ),
inference(subst,[],[refute_0_2:[bind(X0,$fot(truth)),bind(Y0,$fot(not(falsehood)))]]) ).
cnf(refute_0_359,plain,
not(falsehood) = truth,
inference(resolve,[$cnf( $equal(truth,not(falsehood)) )],[refute_0_357,refute_0_358]) ).
cnf(refute_0_360,plain,
( implies(X_22,X_22) != not(falsehood)
| not(falsehood) != truth
| implies(X_22,X_22) = truth ),
introduced(tautology,[equality,[$cnf( ~ $equal(implies(X_22,X_22),truth) ),[0],$fot(not(falsehood))]]) ).
cnf(refute_0_361,plain,
( implies(X_22,X_22) != not(falsehood)
| implies(X_22,X_22) = truth ),
inference(resolve,[$cnf( $equal(not(falsehood),truth) )],[refute_0_359,refute_0_360]) ).
cnf(refute_0_362,plain,
implies(X_22,X_22) = truth,
inference(resolve,[$cnf( $equal(implies(X_22,X_22),not(falsehood)) )],[refute_0_345,refute_0_361]) ).
cnf(refute_0_363,plain,
implies(X_82,X_82) = truth,
inference(subst,[],[refute_0_362:[bind(X_22,$fot(X_82))]]) ).
cnf(refute_0_364,plain,
( implies(X_82,X_82) != truth
| not(implies(X_84,implies(X_82,X_82))) != not(implies(X_82,implies(X_84,X_82)))
| not(implies(X_84,truth)) = not(implies(X_82,implies(X_84,X_82))) ),
introduced(tautology,[equality,[$cnf( $equal(not(implies(X_84,implies(X_82,X_82))),not(implies(X_82,implies(X_84,X_82)))) ),[0,0,1],$fot(truth)]]) ).
cnf(refute_0_365,plain,
( not(implies(X_84,implies(X_82,X_82))) != not(implies(X_82,implies(X_84,X_82)))
| not(implies(X_84,truth)) = not(implies(X_82,implies(X_84,X_82))) ),
inference(resolve,[$cnf( $equal(implies(X_82,X_82),truth) )],[refute_0_363,refute_0_364]) ).
cnf(refute_0_366,plain,
not(implies(X_84,truth)) = not(implies(X_82,implies(X_84,X_82))),
inference(resolve,[$cnf( $equal(not(implies(X_84,implies(X_82,X_82))),not(implies(X_82,implies(X_84,X_82)))) )],[refute_0_325,refute_0_365]) ).
cnf(refute_0_367,plain,
implies(X_21,truth) = not(and_star(X_21,not(truth))),
inference(subst,[],[refute_0_83:[bind(X,$fot(X_21)),bind(Y,$fot(truth))]]) ).
cnf(refute_0_368,plain,
( implies(X_21,truth) != not(and_star(X_21,not(truth)))
| not(truth) != falsehood
| implies(X_21,truth) = not(and_star(X_21,falsehood)) ),
introduced(tautology,[equality,[$cnf( $equal(implies(X_21,truth),not(and_star(X_21,not(truth)))) ),[1,0,1],$fot(falsehood)]]) ).
cnf(refute_0_369,plain,
( implies(X_21,truth) != not(and_star(X_21,not(truth)))
| implies(X_21,truth) = not(and_star(X_21,falsehood)) ),
inference(resolve,[$cnf( $equal(not(truth),falsehood) )],[false_definition,refute_0_368]) ).
cnf(refute_0_370,plain,
implies(X_21,truth) = not(and_star(X_21,falsehood)),
inference(resolve,[$cnf( $equal(implies(X_21,truth),not(and_star(X_21,not(truth)))) )],[refute_0_367,refute_0_369]) ).
cnf(refute_0_371,plain,
and_star(X_21,falsehood) = falsehood,
inference(subst,[],[axiom_5:[bind(X,$fot(X_21))]]) ).
cnf(refute_0_372,plain,
not(and_star(X_21,falsehood)) = not(and_star(X_21,falsehood)),
introduced(tautology,[refl,[$fot(not(and_star(X_21,falsehood)))]]) ).
cnf(refute_0_373,plain,
( and_star(X_21,falsehood) != falsehood
| not(and_star(X_21,falsehood)) != not(and_star(X_21,falsehood))
| not(and_star(X_21,falsehood)) = not(falsehood) ),
introduced(tautology,[equality,[$cnf( $equal(not(and_star(X_21,falsehood)),not(and_star(X_21,falsehood))) ),[1,0],$fot(falsehood)]]) ).
cnf(refute_0_374,plain,
( and_star(X_21,falsehood) != falsehood
| not(and_star(X_21,falsehood)) = not(falsehood) ),
inference(resolve,[$cnf( $equal(not(and_star(X_21,falsehood)),not(and_star(X_21,falsehood))) )],[refute_0_372,refute_0_373]) ).
cnf(refute_0_375,plain,
not(and_star(X_21,falsehood)) = not(falsehood),
inference(resolve,[$cnf( $equal(and_star(X_21,falsehood),falsehood) )],[refute_0_371,refute_0_374]) ).
cnf(refute_0_376,plain,
( not(and_star(X_21,falsehood)) != not(falsehood)
| not(falsehood) != truth
| not(and_star(X_21,falsehood)) = truth ),
inference(subst,[],[refute_0_31:[bind(X0,$fot(not(and_star(X_21,falsehood)))),bind(Y0,$fot(not(falsehood))),bind(Z0,$fot(truth))]]) ).
cnf(refute_0_377,plain,
( not(falsehood) != truth
| not(and_star(X_21,falsehood)) = truth ),
inference(resolve,[$cnf( $equal(not(and_star(X_21,falsehood)),not(falsehood)) )],[refute_0_375,refute_0_376]) ).
cnf(refute_0_378,plain,
not(and_star(X_21,falsehood)) = truth,
inference(resolve,[$cnf( $equal(not(falsehood),truth) )],[refute_0_359,refute_0_377]) ).
cnf(refute_0_379,plain,
( implies(X_21,truth) != not(and_star(X_21,falsehood))
| not(and_star(X_21,falsehood)) != truth
| implies(X_21,truth) = truth ),
introduced(tautology,[equality,[$cnf( ~ $equal(implies(X_21,truth),truth) ),[0],$fot(not(and_star(X_21,falsehood)))]]) ).
cnf(refute_0_380,plain,
( implies(X_21,truth) != not(and_star(X_21,falsehood))
| implies(X_21,truth) = truth ),
inference(resolve,[$cnf( $equal(not(and_star(X_21,falsehood)),truth) )],[refute_0_378,refute_0_379]) ).
cnf(refute_0_381,plain,
implies(X_21,truth) = truth,
inference(resolve,[$cnf( $equal(implies(X_21,truth),not(and_star(X_21,falsehood))) )],[refute_0_370,refute_0_380]) ).
cnf(refute_0_382,plain,
implies(X_84,truth) = truth,
inference(subst,[],[refute_0_381:[bind(X_21,$fot(X_84))]]) ).
cnf(refute_0_383,plain,
not(implies(X_84,truth)) = not(implies(X_84,truth)),
introduced(tautology,[refl,[$fot(not(implies(X_84,truth)))]]) ).
cnf(refute_0_384,plain,
( implies(X_84,truth) != truth
| not(implies(X_84,truth)) != not(implies(X_84,truth))
| not(implies(X_84,truth)) = not(truth) ),
introduced(tautology,[equality,[$cnf( $equal(not(implies(X_84,truth)),not(implies(X_84,truth))) ),[1,0],$fot(truth)]]) ).
cnf(refute_0_385,plain,
( implies(X_84,truth) != truth
| not(implies(X_84,truth)) = not(truth) ),
inference(resolve,[$cnf( $equal(not(implies(X_84,truth)),not(implies(X_84,truth))) )],[refute_0_383,refute_0_384]) ).
cnf(refute_0_386,plain,
not(implies(X_84,truth)) = not(truth),
inference(resolve,[$cnf( $equal(implies(X_84,truth),truth) )],[refute_0_382,refute_0_385]) ).
cnf(refute_0_387,plain,
( not(implies(X_84,truth)) != not(truth)
| not(truth) != falsehood
| not(implies(X_84,truth)) = falsehood ),
inference(subst,[],[refute_0_31:[bind(X0,$fot(not(implies(X_84,truth)))),bind(Y0,$fot(not(truth))),bind(Z0,$fot(falsehood))]]) ).
cnf(refute_0_388,plain,
( not(truth) != falsehood
| not(implies(X_84,truth)) = falsehood ),
inference(resolve,[$cnf( $equal(not(implies(X_84,truth)),not(truth)) )],[refute_0_386,refute_0_387]) ).
cnf(refute_0_389,plain,
not(implies(X_84,truth)) = falsehood,
inference(resolve,[$cnf( $equal(not(truth),falsehood) )],[false_definition,refute_0_388]) ).
cnf(refute_0_390,plain,
( not(implies(X_84,truth)) != falsehood
| not(implies(X_84,truth)) != not(implies(X_82,implies(X_84,X_82)))
| falsehood = not(implies(X_82,implies(X_84,X_82))) ),
introduced(tautology,[equality,[$cnf( $equal(not(implies(X_84,truth)),not(implies(X_82,implies(X_84,X_82)))) ),[0],$fot(falsehood)]]) ).
cnf(refute_0_391,plain,
( not(implies(X_84,truth)) != not(implies(X_82,implies(X_84,X_82)))
| falsehood = not(implies(X_82,implies(X_84,X_82))) ),
inference(resolve,[$cnf( $equal(not(implies(X_84,truth)),falsehood) )],[refute_0_389,refute_0_390]) ).
cnf(refute_0_392,plain,
falsehood = not(implies(X_82,implies(X_84,X_82))),
inference(resolve,[$cnf( $equal(not(implies(X_84,truth)),not(implies(X_82,implies(X_84,X_82)))) )],[refute_0_366,refute_0_391]) ).
cnf(refute_0_393,plain,
falsehood = not(implies(X_85,implies(X_86,X_85))),
inference(subst,[],[refute_0_392:[bind(X_82,$fot(X_85)),bind(X_84,$fot(X_86))]]) ).
cnf(refute_0_394,plain,
( falsehood != not(implies(X_85,implies(X_86,X_85)))
| not(implies(X_85,implies(X_86,X_85))) = falsehood ),
inference(subst,[],[refute_0_2:[bind(X0,$fot(falsehood)),bind(Y0,$fot(not(implies(X_85,implies(X_86,X_85)))))]]) ).
cnf(refute_0_395,plain,
not(implies(X_85,implies(X_86,X_85))) = falsehood,
inference(resolve,[$cnf( $equal(falsehood,not(implies(X_85,implies(X_86,X_85)))) )],[refute_0_393,refute_0_394]) ).
cnf(refute_0_396,plain,
( implies(X_85,implies(X_86,X_85)) != not(not(implies(X_85,implies(X_86,X_85))))
| not(implies(X_85,implies(X_86,X_85))) != falsehood
| implies(X_85,implies(X_86,X_85)) = not(falsehood) ),
introduced(tautology,[equality,[$cnf( $equal(implies(X_85,implies(X_86,X_85)),not(not(implies(X_85,implies(X_86,X_85))))) ),[1,0],$fot(falsehood)]]) ).
cnf(refute_0_397,plain,
( implies(X_85,implies(X_86,X_85)) != not(not(implies(X_85,implies(X_86,X_85))))
| implies(X_85,implies(X_86,X_85)) = not(falsehood) ),
inference(resolve,[$cnf( $equal(not(implies(X_85,implies(X_86,X_85))),falsehood) )],[refute_0_395,refute_0_396]) ).
cnf(refute_0_398,plain,
implies(X_85,implies(X_86,X_85)) = not(falsehood),
inference(resolve,[$cnf( $equal(implies(X_85,implies(X_86,X_85)),not(not(implies(X_85,implies(X_86,X_85))))) )],[refute_0_324,refute_0_397]) ).
cnf(refute_0_399,plain,
( implies(X_85,implies(X_86,X_85)) != not(falsehood)
| not(falsehood) != truth
| implies(X_85,implies(X_86,X_85)) = truth ),
introduced(tautology,[equality,[$cnf( ~ $equal(implies(X_85,implies(X_86,X_85)),truth) ),[0],$fot(not(falsehood))]]) ).
cnf(refute_0_400,plain,
( implies(X_85,implies(X_86,X_85)) != not(falsehood)
| implies(X_85,implies(X_86,X_85)) = truth ),
inference(resolve,[$cnf( $equal(not(falsehood),truth) )],[refute_0_359,refute_0_399]) ).
cnf(refute_0_401,plain,
implies(X_85,implies(X_86,X_85)) = truth,
inference(resolve,[$cnf( $equal(implies(X_85,implies(X_86,X_85)),not(falsehood)) )],[refute_0_398,refute_0_400]) ).
cnf(refute_0_402,plain,
implies(implies(X_139,X_138),implies(X_86,implies(X_139,X_138))) = truth,
inference(subst,[],[refute_0_401:[bind(X_85,$fot(implies(X_139,X_138)))]]) ).
cnf(refute_0_403,plain,
implies(X_86,implies(X_139,X_138)) = implies(X_139,implies(X_86,X_138)),
inference(subst,[],[refute_0_138:[bind(X_82,$fot(X_138)),bind(X_83,$fot(X_139)),bind(X_84,$fot(X_86))]]) ).
cnf(refute_0_404,plain,
( implies(X_86,implies(X_139,X_138)) != implies(X_139,implies(X_86,X_138))
| implies(implies(X_139,X_138),implies(X_86,implies(X_139,X_138))) != truth
| implies(implies(X_139,X_138),implies(X_139,implies(X_86,X_138))) = truth ),
introduced(tautology,[equality,[$cnf( $equal(implies(implies(X_139,X_138),implies(X_86,implies(X_139,X_138))),truth) ),[0,1],$fot(implies(X_139,implies(X_86,X_138)))]]) ).
cnf(refute_0_405,plain,
( implies(implies(X_139,X_138),implies(X_86,implies(X_139,X_138))) != truth
| implies(implies(X_139,X_138),implies(X_139,implies(X_86,X_138))) = truth ),
inference(resolve,[$cnf( $equal(implies(X_86,implies(X_139,X_138)),implies(X_139,implies(X_86,X_138))) )],[refute_0_403,refute_0_404]) ).
cnf(refute_0_406,plain,
implies(implies(X_139,X_138),implies(X_139,implies(X_86,X_138))) = truth,
inference(resolve,[$cnf( $equal(implies(implies(X_139,X_138),implies(X_86,implies(X_139,X_138))),truth) )],[refute_0_402,refute_0_405]) ).
cnf(refute_0_407,plain,
implies(and_star(X_58,X_59),implies(X_139,X_138)) = implies(X_58,implies(X_59,implies(X_139,X_138))),
inference(subst,[],[refute_0_294:[bind(X_57,$fot(implies(X_139,X_138)))]]) ).
cnf(refute_0_408,plain,
implies(and_star(X_58,X_59),implies(X_139,X_138)) = implies(X_139,implies(and_star(X_58,X_59),X_138)),
inference(subst,[],[refute_0_138:[bind(X_82,$fot(X_138)),bind(X_83,$fot(X_139)),bind(X_84,$fot(and_star(X_58,X_59)))]]) ).
cnf(refute_0_409,plain,
( implies(and_star(X_58,X_59),implies(X_139,X_138)) != implies(X_139,implies(and_star(X_58,X_59),X_138))
| implies(and_star(X_58,X_59),implies(X_139,X_138)) != implies(X_58,implies(X_59,implies(X_139,X_138)))
| implies(X_139,implies(and_star(X_58,X_59),X_138)) = implies(X_58,implies(X_59,implies(X_139,X_138))) ),
introduced(tautology,[equality,[$cnf( $equal(implies(and_star(X_58,X_59),implies(X_139,X_138)),implies(X_58,implies(X_59,implies(X_139,X_138)))) ),[0],$fot(implies(X_139,implies(and_star(X_58,X_59),X_138)))]]) ).
cnf(refute_0_410,plain,
( implies(and_star(X_58,X_59),implies(X_139,X_138)) != implies(X_58,implies(X_59,implies(X_139,X_138)))
| implies(X_139,implies(and_star(X_58,X_59),X_138)) = implies(X_58,implies(X_59,implies(X_139,X_138))) ),
inference(resolve,[$cnf( $equal(implies(and_star(X_58,X_59),implies(X_139,X_138)),implies(X_139,implies(and_star(X_58,X_59),X_138))) )],[refute_0_408,refute_0_409]) ).
cnf(refute_0_411,plain,
implies(X_139,implies(and_star(X_58,X_59),X_138)) = implies(X_58,implies(X_59,implies(X_139,X_138))),
inference(resolve,[$cnf( $equal(implies(and_star(X_58,X_59),implies(X_139,X_138)),implies(X_58,implies(X_59,implies(X_139,X_138)))) )],[refute_0_407,refute_0_410]) ).
cnf(refute_0_412,plain,
implies(and_star(X_58,X_59),X_138) = implies(X_58,implies(X_59,X_138)),
inference(subst,[],[refute_0_294:[bind(X_57,$fot(X_138))]]) ).
cnf(refute_0_413,plain,
implies(X_139,implies(and_star(X_58,X_59),X_138)) = implies(X_139,implies(and_star(X_58,X_59),X_138)),
introduced(tautology,[refl,[$fot(implies(X_139,implies(and_star(X_58,X_59),X_138)))]]) ).
cnf(refute_0_414,plain,
( implies(X_139,implies(and_star(X_58,X_59),X_138)) != implies(X_139,implies(and_star(X_58,X_59),X_138))
| implies(and_star(X_58,X_59),X_138) != implies(X_58,implies(X_59,X_138))
| implies(X_139,implies(and_star(X_58,X_59),X_138)) = implies(X_139,implies(X_58,implies(X_59,X_138))) ),
introduced(tautology,[equality,[$cnf( $equal(implies(X_139,implies(and_star(X_58,X_59),X_138)),implies(X_139,implies(and_star(X_58,X_59),X_138))) ),[1,1],$fot(implies(X_58,implies(X_59,X_138)))]]) ).
cnf(refute_0_415,plain,
( implies(and_star(X_58,X_59),X_138) != implies(X_58,implies(X_59,X_138))
| implies(X_139,implies(and_star(X_58,X_59),X_138)) = implies(X_139,implies(X_58,implies(X_59,X_138))) ),
inference(resolve,[$cnf( $equal(implies(X_139,implies(and_star(X_58,X_59),X_138)),implies(X_139,implies(and_star(X_58,X_59),X_138))) )],[refute_0_413,refute_0_414]) ).
cnf(refute_0_416,plain,
implies(X_139,implies(and_star(X_58,X_59),X_138)) = implies(X_139,implies(X_58,implies(X_59,X_138))),
inference(resolve,[$cnf( $equal(implies(and_star(X_58,X_59),X_138),implies(X_58,implies(X_59,X_138))) )],[refute_0_412,refute_0_415]) ).
cnf(refute_0_417,plain,
( implies(X_139,implies(and_star(X_58,X_59),X_138)) != implies(X_139,implies(X_58,implies(X_59,X_138)))
| implies(X_139,implies(and_star(X_58,X_59),X_138)) != implies(X_58,implies(X_59,implies(X_139,X_138)))
| implies(X_139,implies(X_58,implies(X_59,X_138))) = implies(X_58,implies(X_59,implies(X_139,X_138))) ),
introduced(tautology,[equality,[$cnf( $equal(implies(X_139,implies(and_star(X_58,X_59),X_138)),implies(X_58,implies(X_59,implies(X_139,X_138)))) ),[0],$fot(implies(X_139,implies(X_58,implies(X_59,X_138))))]]) ).
cnf(refute_0_418,plain,
( implies(X_139,implies(and_star(X_58,X_59),X_138)) != implies(X_58,implies(X_59,implies(X_139,X_138)))
| implies(X_139,implies(X_58,implies(X_59,X_138))) = implies(X_58,implies(X_59,implies(X_139,X_138))) ),
inference(resolve,[$cnf( $equal(implies(X_139,implies(and_star(X_58,X_59),X_138)),implies(X_139,implies(X_58,implies(X_59,X_138)))) )],[refute_0_416,refute_0_417]) ).
cnf(refute_0_419,plain,
implies(X_139,implies(X_58,implies(X_59,X_138))) = implies(X_58,implies(X_59,implies(X_139,X_138))),
inference(resolve,[$cnf( $equal(implies(X_139,implies(and_star(X_58,X_59),X_138)),implies(X_58,implies(X_59,implies(X_139,X_138)))) )],[refute_0_411,refute_0_418]) ).
cnf(refute_0_420,plain,
implies(implies(X_139,X_138),implies(X_139,implies(X_86,X_138))) = implies(X_139,implies(X_86,implies(implies(X_139,X_138),X_138))),
inference(subst,[],[refute_0_419:[bind(X_139,$fot(implies(X_139,X_138))),bind(X_58,$fot(X_139)),bind(X_59,$fot(X_86))]]) ).
cnf(refute_0_421,plain,
( implies(implies(X_139,X_138),implies(X_139,implies(X_86,X_138))) != implies(X_139,implies(X_86,implies(implies(X_139,X_138),X_138)))
| implies(implies(X_139,X_138),implies(X_139,implies(X_86,X_138))) != truth
| implies(X_139,implies(X_86,implies(implies(X_139,X_138),X_138))) = truth ),
introduced(tautology,[equality,[$cnf( $equal(implies(implies(X_139,X_138),implies(X_139,implies(X_86,X_138))),truth) ),[0],$fot(implies(X_139,implies(X_86,implies(implies(X_139,X_138),X_138))))]]) ).
cnf(refute_0_422,plain,
( implies(implies(X_139,X_138),implies(X_139,implies(X_86,X_138))) != truth
| implies(X_139,implies(X_86,implies(implies(X_139,X_138),X_138))) = truth ),
inference(resolve,[$cnf( $equal(implies(implies(X_139,X_138),implies(X_139,implies(X_86,X_138))),implies(X_139,implies(X_86,implies(implies(X_139,X_138),X_138)))) )],[refute_0_420,refute_0_421]) ).
cnf(refute_0_423,plain,
implies(X_139,implies(X_86,implies(implies(X_139,X_138),X_138))) = truth,
inference(resolve,[$cnf( $equal(implies(implies(X_139,X_138),implies(X_139,implies(X_86,X_138))),truth) )],[refute_0_406,refute_0_422]) ).
cnf(refute_0_424,plain,
implies(X_142,implies(implies(X_142,X_143),implies(implies(X_142,X_229),X_229))) = truth,
inference(subst,[],[refute_0_423:[bind(X_138,$fot(X_229)),bind(X_139,$fot(X_142)),bind(X_86,$fot(implies(X_142,X_143)))]]) ).
cnf(refute_0_425,plain,
( implies(X_142,implies(implies(X_142,X_143),implies(implies(X_142,X_229),X_229))) != truth
| implies(X_143,implies(implies(X_143,X_142),implies(implies(X_142,X_229),X_229))) != implies(X_142,implies(implies(X_142,X_143),implies(implies(X_142,X_229),X_229)))
| implies(X_143,implies(implies(X_143,X_142),implies(implies(X_142,X_229),X_229))) = truth ),
introduced(tautology,[equality,[$cnf( $equal(implies(X_143,implies(implies(X_143,X_142),implies(implies(X_142,X_229),X_229))),implies(X_142,implies(implies(X_142,X_143),implies(implies(X_142,X_229),X_229)))) ),[1],$fot(truth)]]) ).
cnf(refute_0_426,plain,
( implies(X_143,implies(implies(X_143,X_142),implies(implies(X_142,X_229),X_229))) != implies(X_142,implies(implies(X_142,X_143),implies(implies(X_142,X_229),X_229)))
| implies(X_143,implies(implies(X_143,X_142),implies(implies(X_142,X_229),X_229))) = truth ),
inference(resolve,[$cnf( $equal(implies(X_142,implies(implies(X_142,X_143),implies(implies(X_142,X_229),X_229))),truth) )],[refute_0_424,refute_0_425]) ).
cnf(refute_0_427,plain,
implies(X_143,implies(implies(X_143,X_142),implies(implies(X_142,X_229),X_229))) = truth,
inference(resolve,[$cnf( $equal(implies(X_143,implies(implies(X_143,X_142),implies(implies(X_142,X_229),X_229))),implies(X_142,implies(implies(X_142,X_143),implies(implies(X_142,X_229),X_229)))) )],[refute_0_323,refute_0_426]) ).
cnf(refute_0_428,plain,
implies(x,implies(implies(x,y),implies(implies(y,z),z))) = truth,
inference(subst,[],[refute_0_427:[bind(X_142,$fot(y)),bind(X_143,$fot(x)),bind(X_229,$fot(z))]]) ).
cnf(refute_0_429,plain,
( implies(x,implies(implies(x,y),implies(implies(y,z),z))) != truth
| truth != truth
| implies(x,implies(implies(x,y),implies(implies(y,z),z))) = truth ),
introduced(tautology,[equality,[$cnf( ~ $equal(implies(x,implies(implies(x,y),implies(implies(y,z),z))),truth) ),[0],$fot(truth)]]) ).
cnf(refute_0_430,plain,
( truth != truth
| implies(x,implies(implies(x,y),implies(implies(y,z),z))) = truth ),
inference(resolve,[$cnf( $equal(implies(x,implies(implies(x,y),implies(implies(y,z),z))),truth) )],[refute_0_428,refute_0_429]) ).
cnf(refute_0_431,plain,
truth != truth,
inference(resolve,[$cnf( $equal(implies(x,implies(implies(x,y),implies(implies(y,z),z))),truth) )],[refute_0_430,refute_0_152]) ).
cnf(refute_0_432,plain,
truth = truth,
introduced(tautology,[refl,[$fot(truth)]]) ).
cnf(refute_0_433,plain,
$false,
inference(resolve,[$cnf( $equal(truth,truth) )],[refute_0_432,refute_0_431]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL162-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : metis --show proof --show saturation %s
% 0.10/0.37 % Computer : n015.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Fri Sep 4 19:23:26 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 50.79/51.13 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 50.79/51.13
% 50.79/51.13 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 50.95/51.28
%------------------------------------------------------------------------------