%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : LCL265-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n018.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:22 PM UTC 2026
% Result : Unsatisfiable 49.14s 49.41s
% Output : CNFRefutation 49.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 55
% Number of leaves : 111
% Syntax : Number of clauses : 413 ( 228 unt; 0 nHn; 187 RR)
% Number of literals : 686 ( 685 equ; 275 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 3 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 2 con; 0-4 aty)
% Number of variables : 811 ( 9 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(ifeq_axiom,axiom,
ifeq(A,A,B,C) = B ).
cnf(axiom_1_2,axiom,
axiom(implies(or(A,A),A)) = true ).
cnf(axiom_1_3,axiom,
axiom(implies(A,or(B,A))) = true ).
cnf(axiom_1_4,axiom,
axiom(implies(or(A,B),or(B,A))) = true ).
cnf(axiom_1_5,axiom,
axiom(implies(or(A,or(B,C)),or(B,or(A,C)))) = true ).
cnf(axiom_1_6,axiom,
axiom(implies(implies(A,B),implies(or(C,A),or(C,B)))) = true ).
cnf(implies_definition,axiom,
implies(X,Y) = or(not(X),Y) ).
cnf(rule_1,axiom,
ifeq(axiom(X),true,theorem(X),true) = true ).
cnf(rule_2,axiom,
ifeq(theorem(implies(Y,X)),true,ifeq(theorem(Y),true,theorem(X),true),true) = true ).
cnf(and_defn,axiom,
and(P,Q) = not(or(not(P),not(Q))) ).
cnf(equivalent_defn,axiom,
equivalent(P,Q) = and(implies(P,Q),implies(Q,P)) ).
cnf(prove_this,negated_conjecture,
theorem(equivalent(p,not(not(p)))) != true ).
cnf(refute_0_0,plain,
ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(theorem(implies(X_153,not(not(X_153)))),true,theorem(X),true),true) = true,
inference(subst,[],[rule_2:[bind(Y,$fot(implies(X_153,not(not(X_153)))))]]) ).
cnf(refute_0_1,plain,
ifeq(theorem(implies(or(X_34,not(X_33)),implies(X_33,X_34))),true,ifeq(theorem(or(X_34,not(X_33))),true,theorem(implies(X_33,X_34)),true),true) = true,
inference(subst,[],[rule_2:[bind(X,$fot(implies(X_33,X_34))),bind(Y,$fot(or(X_34,not(X_33))))]]) ).
cnf(refute_0_2,plain,
ifeq(axiom(implies(or(X_6,X_7),or(X_7,X_6))),true,theorem(implies(or(X_6,X_7),or(X_7,X_6))),true) = true,
inference(subst,[],[rule_1:[bind(X,$fot(implies(or(X_6,X_7),or(X_7,X_6))))]]) ).
cnf(refute_0_3,plain,
axiom(implies(or(X_6,X_7),or(X_7,X_6))) = true,
inference(subst,[],[axiom_1_4:[bind(A,$fot(X_6)),bind(B,$fot(X_7))]]) ).
cnf(refute_0_4,plain,
( axiom(implies(or(X_6,X_7),or(X_7,X_6))) != true
| ifeq(axiom(implies(or(X_6,X_7),or(X_7,X_6))),true,theorem(implies(or(X_6,X_7),or(X_7,X_6))),true) != true
| ifeq(true,true,theorem(implies(or(X_6,X_7),or(X_7,X_6))),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(axiom(implies(or(X_6,X_7),or(X_7,X_6))),true,theorem(implies(or(X_6,X_7),or(X_7,X_6))),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_5,plain,
( ifeq(axiom(implies(or(X_6,X_7),or(X_7,X_6))),true,theorem(implies(or(X_6,X_7),or(X_7,X_6))),true) != true
| ifeq(true,true,theorem(implies(or(X_6,X_7),or(X_7,X_6))),true) = true ),
inference(resolve,[$cnf( $equal(axiom(implies(or(X_6,X_7),or(X_7,X_6))),true) )],[refute_0_3,refute_0_4]) ).
cnf(refute_0_6,plain,
ifeq(true,true,theorem(implies(or(X_6,X_7),or(X_7,X_6))),true) = true,
inference(resolve,[$cnf( $equal(ifeq(axiom(implies(or(X_6,X_7),or(X_7,X_6))),true,theorem(implies(or(X_6,X_7),or(X_7,X_6))),true),true) )],[refute_0_2,refute_0_5]) ).
cnf(refute_0_7,plain,
ifeq(true,true,theorem(implies(or(X_6,X_7),or(X_7,X_6))),true) = theorem(implies(or(X_6,X_7),or(X_7,X_6))),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(theorem(implies(or(X_6,X_7),or(X_7,X_6))))),bind(C,$fot(true))]]) ).
cnf(refute_0_8,plain,
( ifeq(true,true,theorem(implies(or(X_6,X_7),or(X_7,X_6))),true) != theorem(implies(or(X_6,X_7),or(X_7,X_6)))
| ifeq(true,true,theorem(implies(or(X_6,X_7),or(X_7,X_6))),true) != true
| theorem(implies(or(X_6,X_7),or(X_7,X_6))) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,theorem(implies(or(X_6,X_7),or(X_7,X_6))),true),true) ),[0],$fot(theorem(implies(or(X_6,X_7),or(X_7,X_6))))]]) ).
cnf(refute_0_9,plain,
( ifeq(true,true,theorem(implies(or(X_6,X_7),or(X_7,X_6))),true) != true
| theorem(implies(or(X_6,X_7),or(X_7,X_6))) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(implies(or(X_6,X_7),or(X_7,X_6))),true),theorem(implies(or(X_6,X_7),or(X_7,X_6)))) )],[refute_0_7,refute_0_8]) ).
cnf(refute_0_10,plain,
theorem(implies(or(X_6,X_7),or(X_7,X_6))) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(implies(or(X_6,X_7),or(X_7,X_6))),true),true) )],[refute_0_6,refute_0_9]) ).
cnf(refute_0_11,plain,
theorem(implies(or(X_6,not(X_16)),or(not(X_16),X_6))) = true,
inference(subst,[],[refute_0_10:[bind(X_7,$fot(not(X_16)))]]) ).
cnf(refute_0_12,plain,
implies(X_16,X_6) = or(not(X_16),X_6),
inference(subst,[],[implies_definition:[bind(X,$fot(X_16)),bind(Y,$fot(X_6))]]) ).
cnf(refute_0_13,plain,
X0 = X0,
introduced(tautology,[refl,[$fot(X0)]]) ).
cnf(refute_0_14,plain,
( X0 != X0
| X0 != Y0
| Y0 = X0 ),
introduced(tautology,[equality,[$cnf( $equal(X0,X0) ),[0],$fot(Y0)]]) ).
cnf(refute_0_15,plain,
( X0 != Y0
| Y0 = X0 ),
inference(resolve,[$cnf( $equal(X0,X0) )],[refute_0_13,refute_0_14]) ).
cnf(refute_0_16,plain,
( implies(X_16,X_6) != or(not(X_16),X_6)
| or(not(X_16),X_6) = implies(X_16,X_6) ),
inference(subst,[],[refute_0_15:[bind(X0,$fot(implies(X_16,X_6))),bind(Y0,$fot(or(not(X_16),X_6)))]]) ).
cnf(refute_0_17,plain,
or(not(X_16),X_6) = implies(X_16,X_6),
inference(resolve,[$cnf( $equal(implies(X_16,X_6),or(not(X_16),X_6)) )],[refute_0_12,refute_0_16]) ).
cnf(refute_0_18,plain,
( or(not(X_16),X_6) != implies(X_16,X_6)
| theorem(implies(or(X_6,not(X_16)),or(not(X_16),X_6))) != true
| theorem(implies(or(X_6,not(X_16)),implies(X_16,X_6))) = true ),
introduced(tautology,[equality,[$cnf( $equal(theorem(implies(or(X_6,not(X_16)),or(not(X_16),X_6))),true) ),[0,0,1],$fot(implies(X_16,X_6))]]) ).
cnf(refute_0_19,plain,
( theorem(implies(or(X_6,not(X_16)),or(not(X_16),X_6))) != true
| theorem(implies(or(X_6,not(X_16)),implies(X_16,X_6))) = true ),
inference(resolve,[$cnf( $equal(or(not(X_16),X_6),implies(X_16,X_6)) )],[refute_0_17,refute_0_18]) ).
cnf(refute_0_20,plain,
theorem(implies(or(X_6,not(X_16)),implies(X_16,X_6))) = true,
inference(resolve,[$cnf( $equal(theorem(implies(or(X_6,not(X_16)),or(not(X_16),X_6))),true) )],[refute_0_11,refute_0_19]) ).
cnf(refute_0_21,plain,
theorem(implies(or(X_34,not(X_33)),implies(X_33,X_34))) = true,
inference(subst,[],[refute_0_20:[bind(X_16,$fot(X_33)),bind(X_6,$fot(X_34))]]) ).
cnf(refute_0_22,plain,
( ifeq(theorem(implies(or(X_34,not(X_33)),implies(X_33,X_34))),true,ifeq(theorem(or(X_34,not(X_33))),true,theorem(implies(X_33,X_34)),true),true) != true
| theorem(implies(or(X_34,not(X_33)),implies(X_33,X_34))) != true
| ifeq(true,true,ifeq(theorem(or(X_34,not(X_33))),true,theorem(implies(X_33,X_34)),true),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(implies(or(X_34,not(X_33)),implies(X_33,X_34))),true,ifeq(theorem(or(X_34,not(X_33))),true,theorem(implies(X_33,X_34)),true),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_23,plain,
( ifeq(theorem(implies(or(X_34,not(X_33)),implies(X_33,X_34))),true,ifeq(theorem(or(X_34,not(X_33))),true,theorem(implies(X_33,X_34)),true),true) != true
| ifeq(true,true,ifeq(theorem(or(X_34,not(X_33))),true,theorem(implies(X_33,X_34)),true),true) = true ),
inference(resolve,[$cnf( $equal(theorem(implies(or(X_34,not(X_33)),implies(X_33,X_34))),true) )],[refute_0_21,refute_0_22]) ).
cnf(refute_0_24,plain,
ifeq(true,true,ifeq(theorem(or(X_34,not(X_33))),true,theorem(implies(X_33,X_34)),true),true) = true,
inference(resolve,[$cnf( $equal(ifeq(theorem(implies(or(X_34,not(X_33)),implies(X_33,X_34))),true,ifeq(theorem(or(X_34,not(X_33))),true,theorem(implies(X_33,X_34)),true),true),true) )],[refute_0_1,refute_0_23]) ).
cnf(refute_0_25,plain,
ifeq(true,true,ifeq(theorem(or(X_34,not(X_33))),true,theorem(implies(X_33,X_34)),true),true) = ifeq(theorem(or(X_34,not(X_33))),true,theorem(implies(X_33,X_34)),true),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(ifeq(theorem(or(X_34,not(X_33))),true,theorem(implies(X_33,X_34)),true))),bind(C,$fot(true))]]) ).
cnf(refute_0_26,plain,
( ifeq(true,true,ifeq(theorem(or(X_34,not(X_33))),true,theorem(implies(X_33,X_34)),true),true) != ifeq(theorem(or(X_34,not(X_33))),true,theorem(implies(X_33,X_34)),true)
| ifeq(true,true,ifeq(theorem(or(X_34,not(X_33))),true,theorem(implies(X_33,X_34)),true),true) != true
| ifeq(theorem(or(X_34,not(X_33))),true,theorem(implies(X_33,X_34)),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,ifeq(theorem(or(X_34,not(X_33))),true,theorem(implies(X_33,X_34)),true),true),true) ),[0],$fot(ifeq(theorem(or(X_34,not(X_33))),true,theorem(implies(X_33,X_34)),true))]]) ).
cnf(refute_0_27,plain,
( ifeq(true,true,ifeq(theorem(or(X_34,not(X_33))),true,theorem(implies(X_33,X_34)),true),true) != true
| ifeq(theorem(or(X_34,not(X_33))),true,theorem(implies(X_33,X_34)),true) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,ifeq(theorem(or(X_34,not(X_33))),true,theorem(implies(X_33,X_34)),true),true),ifeq(theorem(or(X_34,not(X_33))),true,theorem(implies(X_33,X_34)),true)) )],[refute_0_25,refute_0_26]) ).
cnf(refute_0_28,plain,
ifeq(theorem(or(X_34,not(X_33))),true,theorem(implies(X_33,X_34)),true) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,ifeq(theorem(or(X_34,not(X_33))),true,theorem(implies(X_33,X_34)),true),true),true) )],[refute_0_24,refute_0_27]) ).
cnf(refute_0_29,plain,
ifeq(theorem(or(not(X),not(X_116))),true,theorem(implies(X_116,not(X))),true) = true,
inference(subst,[],[refute_0_28:[bind(X_33,$fot(X_116)),bind(X_34,$fot(not(X)))]]) ).
cnf(refute_0_30,plain,
implies(X,not(X_116)) = or(not(X),not(X_116)),
inference(subst,[],[implies_definition:[bind(Y,$fot(not(X_116)))]]) ).
cnf(refute_0_31,plain,
( implies(X,not(X_116)) != or(not(X),not(X_116))
| or(not(X),not(X_116)) = implies(X,not(X_116)) ),
inference(subst,[],[refute_0_15:[bind(X0,$fot(implies(X,not(X_116)))),bind(Y0,$fot(or(not(X),not(X_116))))]]) ).
cnf(refute_0_32,plain,
or(not(X),not(X_116)) = implies(X,not(X_116)),
inference(resolve,[$cnf( $equal(implies(X,not(X_116)),or(not(X),not(X_116))) )],[refute_0_30,refute_0_31]) ).
cnf(refute_0_33,plain,
( ifeq(theorem(or(not(X),not(X_116))),true,theorem(implies(X_116,not(X))),true) != true
| or(not(X),not(X_116)) != implies(X,not(X_116))
| ifeq(theorem(implies(X,not(X_116))),true,theorem(implies(X_116,not(X))),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(or(not(X),not(X_116))),true,theorem(implies(X_116,not(X))),true),true) ),[0,0,0],$fot(implies(X,not(X_116)))]]) ).
cnf(refute_0_34,plain,
( ifeq(theorem(or(not(X),not(X_116))),true,theorem(implies(X_116,not(X))),true) != true
| ifeq(theorem(implies(X,not(X_116))),true,theorem(implies(X_116,not(X))),true) = true ),
inference(resolve,[$cnf( $equal(or(not(X),not(X_116)),implies(X,not(X_116))) )],[refute_0_32,refute_0_33]) ).
cnf(refute_0_35,plain,
ifeq(theorem(implies(X,not(X_116))),true,theorem(implies(X_116,not(X))),true) = true,
inference(resolve,[$cnf( $equal(ifeq(theorem(or(not(X),not(X_116))),true,theorem(implies(X_116,not(X))),true),true) )],[refute_0_29,refute_0_34]) ).
cnf(refute_0_36,plain,
ifeq(theorem(implies(not(X_116),not(X_116))),true,theorem(implies(X_116,not(not(X_116)))),true) = true,
inference(subst,[],[refute_0_35:[bind(X,$fot(not(X_116)))]]) ).
cnf(refute_0_37,plain,
ifeq(theorem(implies(or(X_28,X_28),X_28)),true,ifeq(theorem(or(X_28,X_28)),true,theorem(X_28),true),true) = true,
inference(subst,[],[rule_2:[bind(X,$fot(X_28)),bind(Y,$fot(or(X_28,X_28)))]]) ).
cnf(refute_0_38,plain,
ifeq(axiom(implies(or(A,A),A)),true,theorem(implies(or(A,A),A)),true) = true,
inference(subst,[],[rule_1:[bind(X,$fot(implies(or(A,A),A)))]]) ).
cnf(refute_0_39,plain,
( axiom(implies(or(A,A),A)) != true
| ifeq(axiom(implies(or(A,A),A)),true,theorem(implies(or(A,A),A)),true) != true
| ifeq(true,true,theorem(implies(or(A,A),A)),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(axiom(implies(or(A,A),A)),true,theorem(implies(or(A,A),A)),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_40,plain,
( ifeq(axiom(implies(or(A,A),A)),true,theorem(implies(or(A,A),A)),true) != true
| ifeq(true,true,theorem(implies(or(A,A),A)),true) = true ),
inference(resolve,[$cnf( $equal(axiom(implies(or(A,A),A)),true) )],[axiom_1_2,refute_0_39]) ).
cnf(refute_0_41,plain,
ifeq(true,true,theorem(implies(or(A,A),A)),true) = true,
inference(resolve,[$cnf( $equal(ifeq(axiom(implies(or(A,A),A)),true,theorem(implies(or(A,A),A)),true),true) )],[refute_0_38,refute_0_40]) ).
cnf(refute_0_42,plain,
ifeq(true,true,theorem(implies(or(A,A),A)),true) = theorem(implies(or(A,A),A)),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(theorem(implies(or(A,A),A)))),bind(C,$fot(true))]]) ).
cnf(refute_0_43,plain,
( ifeq(true,true,theorem(implies(or(A,A),A)),true) != theorem(implies(or(A,A),A))
| ifeq(true,true,theorem(implies(or(A,A),A)),true) != true
| theorem(implies(or(A,A),A)) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,theorem(implies(or(A,A),A)),true),true) ),[0],$fot(theorem(implies(or(A,A),A)))]]) ).
cnf(refute_0_44,plain,
( ifeq(true,true,theorem(implies(or(A,A),A)),true) != true
| theorem(implies(or(A,A),A)) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(implies(or(A,A),A)),true),theorem(implies(or(A,A),A))) )],[refute_0_42,refute_0_43]) ).
cnf(refute_0_45,plain,
theorem(implies(or(A,A),A)) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(implies(or(A,A),A)),true),true) )],[refute_0_41,refute_0_44]) ).
cnf(refute_0_46,plain,
theorem(implies(or(X_28,X_28),X_28)) = true,
inference(subst,[],[refute_0_45:[bind(A,$fot(X_28))]]) ).
cnf(refute_0_47,plain,
( ifeq(theorem(implies(or(X_28,X_28),X_28)),true,ifeq(theorem(or(X_28,X_28)),true,theorem(X_28),true),true) != true
| theorem(implies(or(X_28,X_28),X_28)) != true
| ifeq(true,true,ifeq(theorem(or(X_28,X_28)),true,theorem(X_28),true),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(implies(or(X_28,X_28),X_28)),true,ifeq(theorem(or(X_28,X_28)),true,theorem(X_28),true),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_48,plain,
( ifeq(theorem(implies(or(X_28,X_28),X_28)),true,ifeq(theorem(or(X_28,X_28)),true,theorem(X_28),true),true) != true
| ifeq(true,true,ifeq(theorem(or(X_28,X_28)),true,theorem(X_28),true),true) = true ),
inference(resolve,[$cnf( $equal(theorem(implies(or(X_28,X_28),X_28)),true) )],[refute_0_46,refute_0_47]) ).
cnf(refute_0_49,plain,
ifeq(true,true,ifeq(theorem(or(X_28,X_28)),true,theorem(X_28),true),true) = true,
inference(resolve,[$cnf( $equal(ifeq(theorem(implies(or(X_28,X_28),X_28)),true,ifeq(theorem(or(X_28,X_28)),true,theorem(X_28),true),true),true) )],[refute_0_37,refute_0_48]) ).
cnf(refute_0_50,plain,
ifeq(true,true,ifeq(theorem(or(X_28,X_28)),true,theorem(X_28),true),true) = ifeq(theorem(or(X_28,X_28)),true,theorem(X_28),true),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(ifeq(theorem(or(X_28,X_28)),true,theorem(X_28),true))),bind(C,$fot(true))]]) ).
cnf(refute_0_51,plain,
( ifeq(true,true,ifeq(theorem(or(X_28,X_28)),true,theorem(X_28),true),true) != ifeq(theorem(or(X_28,X_28)),true,theorem(X_28),true)
| ifeq(true,true,ifeq(theorem(or(X_28,X_28)),true,theorem(X_28),true),true) != true
| ifeq(theorem(or(X_28,X_28)),true,theorem(X_28),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,ifeq(theorem(or(X_28,X_28)),true,theorem(X_28),true),true),true) ),[0],$fot(ifeq(theorem(or(X_28,X_28)),true,theorem(X_28),true))]]) ).
cnf(refute_0_52,plain,
( ifeq(true,true,ifeq(theorem(or(X_28,X_28)),true,theorem(X_28),true),true) != true
| ifeq(theorem(or(X_28,X_28)),true,theorem(X_28),true) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,ifeq(theorem(or(X_28,X_28)),true,theorem(X_28),true),true),ifeq(theorem(or(X_28,X_28)),true,theorem(X_28),true)) )],[refute_0_50,refute_0_51]) ).
cnf(refute_0_53,plain,
ifeq(theorem(or(X_28,X_28)),true,theorem(X_28),true) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,ifeq(theorem(or(X_28,X_28)),true,theorem(X_28),true),true),true) )],[refute_0_49,refute_0_52]) ).
cnf(refute_0_54,plain,
ifeq(theorem(or(implies(X_149,X_149),implies(X_149,X_149))),true,theorem(implies(X_149,X_149)),true) = true,
inference(subst,[],[refute_0_53:[bind(X_28,$fot(implies(X_149,X_149)))]]) ).
cnf(refute_0_55,plain,
ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(theorem(implies(X_10,or(X_11,X_10))),true,theorem(X_28),true),true) = true,
inference(subst,[],[rule_2:[bind(X,$fot(X_28)),bind(Y,$fot(implies(X_10,or(X_11,X_10))))]]) ).
cnf(refute_0_56,plain,
ifeq(axiom(implies(X_10,or(X_11,X_10))),true,theorem(implies(X_10,or(X_11,X_10))),true) = true,
inference(subst,[],[rule_1:[bind(X,$fot(implies(X_10,or(X_11,X_10))))]]) ).
cnf(refute_0_57,plain,
axiom(implies(X_10,or(X_11,X_10))) = true,
inference(subst,[],[axiom_1_3:[bind(A,$fot(X_10)),bind(B,$fot(X_11))]]) ).
cnf(refute_0_58,plain,
( axiom(implies(X_10,or(X_11,X_10))) != true
| ifeq(axiom(implies(X_10,or(X_11,X_10))),true,theorem(implies(X_10,or(X_11,X_10))),true) != true
| ifeq(true,true,theorem(implies(X_10,or(X_11,X_10))),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(axiom(implies(X_10,or(X_11,X_10))),true,theorem(implies(X_10,or(X_11,X_10))),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_59,plain,
( ifeq(axiom(implies(X_10,or(X_11,X_10))),true,theorem(implies(X_10,or(X_11,X_10))),true) != true
| ifeq(true,true,theorem(implies(X_10,or(X_11,X_10))),true) = true ),
inference(resolve,[$cnf( $equal(axiom(implies(X_10,or(X_11,X_10))),true) )],[refute_0_57,refute_0_58]) ).
cnf(refute_0_60,plain,
ifeq(true,true,theorem(implies(X_10,or(X_11,X_10))),true) = true,
inference(resolve,[$cnf( $equal(ifeq(axiom(implies(X_10,or(X_11,X_10))),true,theorem(implies(X_10,or(X_11,X_10))),true),true) )],[refute_0_56,refute_0_59]) ).
cnf(refute_0_61,plain,
ifeq(true,true,theorem(implies(X_10,or(X_11,X_10))),true) = theorem(implies(X_10,or(X_11,X_10))),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(theorem(implies(X_10,or(X_11,X_10))))),bind(C,$fot(true))]]) ).
cnf(refute_0_62,plain,
( ifeq(true,true,theorem(implies(X_10,or(X_11,X_10))),true) != theorem(implies(X_10,or(X_11,X_10)))
| ifeq(true,true,theorem(implies(X_10,or(X_11,X_10))),true) != true
| theorem(implies(X_10,or(X_11,X_10))) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,theorem(implies(X_10,or(X_11,X_10))),true),true) ),[0],$fot(theorem(implies(X_10,or(X_11,X_10))))]]) ).
cnf(refute_0_63,plain,
( ifeq(true,true,theorem(implies(X_10,or(X_11,X_10))),true) != true
| theorem(implies(X_10,or(X_11,X_10))) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(implies(X_10,or(X_11,X_10))),true),theorem(implies(X_10,or(X_11,X_10)))) )],[refute_0_61,refute_0_62]) ).
cnf(refute_0_64,plain,
theorem(implies(X_10,or(X_11,X_10))) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(implies(X_10,or(X_11,X_10))),true),true) )],[refute_0_60,refute_0_63]) ).
cnf(refute_0_65,plain,
( ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(theorem(implies(X_10,or(X_11,X_10))),true,theorem(X_28),true),true) != true
| theorem(implies(X_10,or(X_11,X_10))) != true
| ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(true,true,theorem(X_28),true),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(theorem(implies(X_10,or(X_11,X_10))),true,theorem(X_28),true),true),true) ),[0,2,0],$fot(true)]]) ).
cnf(refute_0_66,plain,
( ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(theorem(implies(X_10,or(X_11,X_10))),true,theorem(X_28),true),true) != true
| ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(true,true,theorem(X_28),true),true) = true ),
inference(resolve,[$cnf( $equal(theorem(implies(X_10,or(X_11,X_10))),true) )],[refute_0_64,refute_0_65]) ).
cnf(refute_0_67,plain,
ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(true,true,theorem(X_28),true),true) = true,
inference(resolve,[$cnf( $equal(ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(theorem(implies(X_10,or(X_11,X_10))),true,theorem(X_28),true),true),true) )],[refute_0_55,refute_0_66]) ).
cnf(refute_0_68,plain,
ifeq(true,true,theorem(X_28),true) = theorem(X_28),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(theorem(X_28))),bind(C,$fot(true))]]) ).
cnf(refute_0_69,plain,
ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(true,true,theorem(X_28),true),true) = ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(true,true,theorem(X_28),true),true),
introduced(tautology,[refl,[$fot(ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(true,true,theorem(X_28),true),true))]]) ).
cnf(refute_0_70,plain,
( ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(true,true,theorem(X_28),true),true) != ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(true,true,theorem(X_28),true),true)
| ifeq(true,true,theorem(X_28),true) != theorem(X_28)
| ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(true,true,theorem(X_28),true),true) = ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,theorem(X_28),true) ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(true,true,theorem(X_28),true),true),ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(true,true,theorem(X_28),true),true)) ),[1,2],$fot(theorem(X_28))]]) ).
cnf(refute_0_71,plain,
( ifeq(true,true,theorem(X_28),true) != theorem(X_28)
| ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(true,true,theorem(X_28),true),true) = ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,theorem(X_28),true) ),
inference(resolve,[$cnf( $equal(ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(true,true,theorem(X_28),true),true),ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(true,true,theorem(X_28),true),true)) )],[refute_0_69,refute_0_70]) ).
cnf(refute_0_72,plain,
ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(true,true,theorem(X_28),true),true) = ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,theorem(X_28),true),
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(X_28),true),theorem(X_28)) )],[refute_0_68,refute_0_71]) ).
cnf(refute_0_73,plain,
( ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(true,true,theorem(X_28),true),true) != ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,theorem(X_28),true)
| ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(true,true,theorem(X_28),true),true) != true
| ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,theorem(X_28),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(true,true,theorem(X_28),true),true),true) ),[0],$fot(ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,theorem(X_28),true))]]) ).
cnf(refute_0_74,plain,
( ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(true,true,theorem(X_28),true),true) != true
| ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,theorem(X_28),true) = true ),
inference(resolve,[$cnf( $equal(ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(true,true,theorem(X_28),true),true),ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,theorem(X_28),true)) )],[refute_0_72,refute_0_73]) ).
cnf(refute_0_75,plain,
ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,theorem(X_28),true) = true,
inference(resolve,[$cnf( $equal(ifeq(theorem(implies(implies(X_10,or(X_11,X_10)),X_28)),true,ifeq(true,true,theorem(X_28),true),true),true) )],[refute_0_67,refute_0_74]) ).
cnf(refute_0_76,plain,
ifeq(theorem(implies(implies(X_146,or(X_147,X_146)),or(X_147,implies(X_146,X_146)))),true,theorem(or(X_147,implies(X_146,X_146))),true) = true,
inference(subst,[],[refute_0_75:[bind(X_10,$fot(X_146)),bind(X_11,$fot(X_147)),bind(X_28,$fot(or(X_147,implies(X_146,X_146))))]]) ).
cnf(refute_0_77,plain,
ifeq(axiom(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))),true,theorem(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))),true) = true,
inference(subst,[],[rule_1:[bind(X,$fot(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))))]]) ).
cnf(refute_0_78,plain,
axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,or(not(X),X_24)))) = true,
inference(subst,[],[axiom_1_5:[bind(A,$fot(not(X))),bind(B,$fot(X_23)),bind(C,$fot(X_24))]]) ).
cnf(refute_0_79,plain,
implies(X,X_24) = or(not(X),X_24),
inference(subst,[],[implies_definition:[bind(Y,$fot(X_24))]]) ).
cnf(refute_0_80,plain,
( implies(X,X_24) != or(not(X),X_24)
| or(not(X),X_24) = implies(X,X_24) ),
inference(subst,[],[refute_0_15:[bind(X0,$fot(implies(X,X_24))),bind(Y0,$fot(or(not(X),X_24)))]]) ).
cnf(refute_0_81,plain,
or(not(X),X_24) = implies(X,X_24),
inference(resolve,[$cnf( $equal(implies(X,X_24),or(not(X),X_24)) )],[refute_0_79,refute_0_80]) ).
cnf(refute_0_82,plain,
( axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,or(not(X),X_24)))) != true
| or(not(X),X_24) != implies(X,X_24)
| axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24)))) = true ),
introduced(tautology,[equality,[$cnf( $equal(axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,or(not(X),X_24)))),true) ),[0,0,1,1],$fot(implies(X,X_24))]]) ).
cnf(refute_0_83,plain,
( axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,or(not(X),X_24)))) != true
| axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24)))) = true ),
inference(resolve,[$cnf( $equal(or(not(X),X_24),implies(X,X_24)) )],[refute_0_81,refute_0_82]) ).
cnf(refute_0_84,plain,
axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24)))) = true,
inference(resolve,[$cnf( $equal(axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,or(not(X),X_24)))),true) )],[refute_0_78,refute_0_83]) ).
cnf(refute_0_85,plain,
( implies(X,Y) != or(not(X),Y)
| or(not(X),Y) = implies(X,Y) ),
inference(subst,[],[refute_0_15:[bind(X0,$fot(implies(X,Y))),bind(Y0,$fot(or(not(X),Y)))]]) ).
cnf(refute_0_86,plain,
or(not(X),Y) = implies(X,Y),
inference(resolve,[$cnf( $equal(implies(X,Y),or(not(X),Y)) )],[implies_definition,refute_0_85]) ).
cnf(refute_0_87,plain,
or(not(X),or(X_23,X_24)) = implies(X,or(X_23,X_24)),
inference(subst,[],[refute_0_86:[bind(Y,$fot(or(X_23,X_24)))]]) ).
cnf(refute_0_88,plain,
implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24))) = implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24))),
introduced(tautology,[refl,[$fot(implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24))))]]) ).
cnf(refute_0_89,plain,
( implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24))) != implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24)))
| or(not(X),or(X_23,X_24)) != implies(X,or(X_23,X_24))
| implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24))) = implies(implies(X,or(X_23,X_24)),or(X_23,implies(X,X_24))) ),
introduced(tautology,[equality,[$cnf( $equal(implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24))),implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24)))) ),[1,0],$fot(implies(X,or(X_23,X_24)))]]) ).
cnf(refute_0_90,plain,
( or(not(X),or(X_23,X_24)) != implies(X,or(X_23,X_24))
| implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24))) = implies(implies(X,or(X_23,X_24)),or(X_23,implies(X,X_24))) ),
inference(resolve,[$cnf( $equal(implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24))),implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24)))) )],[refute_0_88,refute_0_89]) ).
cnf(refute_0_91,plain,
implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24))) = implies(implies(X,or(X_23,X_24)),or(X_23,implies(X,X_24))),
inference(resolve,[$cnf( $equal(or(not(X),or(X_23,X_24)),implies(X,or(X_23,X_24))) )],[refute_0_87,refute_0_90]) ).
cnf(refute_0_92,plain,
axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24)))) = axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24)))),
introduced(tautology,[refl,[$fot(axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24)))))]]) ).
cnf(refute_0_93,plain,
( axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24)))) != axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24))))
| implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24))) != implies(implies(X,or(X_23,X_24)),or(X_23,implies(X,X_24)))
| axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24)))) = axiom(implies(implies(X,or(X_23,X_24)),or(X_23,implies(X,X_24)))) ),
introduced(tautology,[equality,[$cnf( $equal(axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24)))),axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24))))) ),[1,0],$fot(implies(implies(X,or(X_23,X_24)),or(X_23,implies(X,X_24))))]]) ).
cnf(refute_0_94,plain,
( implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24))) != implies(implies(X,or(X_23,X_24)),or(X_23,implies(X,X_24)))
| axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24)))) = axiom(implies(implies(X,or(X_23,X_24)),or(X_23,implies(X,X_24)))) ),
inference(resolve,[$cnf( $equal(axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24)))),axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24))))) )],[refute_0_92,refute_0_93]) ).
cnf(refute_0_95,plain,
axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24)))) = axiom(implies(implies(X,or(X_23,X_24)),or(X_23,implies(X,X_24)))),
inference(resolve,[$cnf( $equal(implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24))),implies(implies(X,or(X_23,X_24)),or(X_23,implies(X,X_24)))) )],[refute_0_91,refute_0_94]) ).
cnf(refute_0_96,plain,
( axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24)))) != axiom(implies(implies(X,or(X_23,X_24)),or(X_23,implies(X,X_24))))
| axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24)))) != true
| axiom(implies(implies(X,or(X_23,X_24)),or(X_23,implies(X,X_24)))) = true ),
introduced(tautology,[equality,[$cnf( $equal(axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24)))),true) ),[0],$fot(axiom(implies(implies(X,or(X_23,X_24)),or(X_23,implies(X,X_24)))))]]) ).
cnf(refute_0_97,plain,
( axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24)))) != true
| axiom(implies(implies(X,or(X_23,X_24)),or(X_23,implies(X,X_24)))) = true ),
inference(resolve,[$cnf( $equal(axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24)))),axiom(implies(implies(X,or(X_23,X_24)),or(X_23,implies(X,X_24))))) )],[refute_0_95,refute_0_96]) ).
cnf(refute_0_98,plain,
axiom(implies(implies(X,or(X_23,X_24)),or(X_23,implies(X,X_24)))) = true,
inference(resolve,[$cnf( $equal(axiom(implies(or(not(X),or(X_23,X_24)),or(X_23,implies(X,X_24)))),true) )],[refute_0_84,refute_0_97]) ).
cnf(refute_0_99,plain,
axiom(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))) = true,
inference(subst,[],[refute_0_98:[bind(X,$fot(X_64)),bind(X_23,$fot(X_65)),bind(X_24,$fot(X_66))]]) ).
cnf(refute_0_100,plain,
( axiom(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))) != true
| ifeq(axiom(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))),true,theorem(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))),true) != true
| ifeq(true,true,theorem(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(axiom(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))),true,theorem(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_101,plain,
( ifeq(axiom(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))),true,theorem(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))),true) != true
| ifeq(true,true,theorem(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))),true) = true ),
inference(resolve,[$cnf( $equal(axiom(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))),true) )],[refute_0_99,refute_0_100]) ).
cnf(refute_0_102,plain,
ifeq(true,true,theorem(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))),true) = true,
inference(resolve,[$cnf( $equal(ifeq(axiom(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))),true,theorem(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))),true),true) )],[refute_0_77,refute_0_101]) ).
cnf(refute_0_103,plain,
ifeq(true,true,theorem(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))),true) = theorem(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(theorem(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))))),bind(C,$fot(true))]]) ).
cnf(refute_0_104,plain,
( ifeq(true,true,theorem(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))),true) != theorem(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66))))
| ifeq(true,true,theorem(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))),true) != true
| theorem(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,theorem(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))),true),true) ),[0],$fot(theorem(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))))]]) ).
cnf(refute_0_105,plain,
( ifeq(true,true,theorem(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))),true) != true
| theorem(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))),true),theorem(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66))))) )],[refute_0_103,refute_0_104]) ).
cnf(refute_0_106,plain,
theorem(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(implies(implies(X_64,or(X_65,X_66)),or(X_65,implies(X_64,X_66)))),true),true) )],[refute_0_102,refute_0_105]) ).
cnf(refute_0_107,plain,
theorem(implies(implies(X_146,or(X_147,X_146)),or(X_147,implies(X_146,X_146)))) = true,
inference(subst,[],[refute_0_106:[bind(X_64,$fot(X_146)),bind(X_65,$fot(X_147)),bind(X_66,$fot(X_146))]]) ).
cnf(refute_0_108,plain,
( ifeq(theorem(implies(implies(X_146,or(X_147,X_146)),or(X_147,implies(X_146,X_146)))),true,theorem(or(X_147,implies(X_146,X_146))),true) != true
| theorem(implies(implies(X_146,or(X_147,X_146)),or(X_147,implies(X_146,X_146)))) != true
| ifeq(true,true,theorem(or(X_147,implies(X_146,X_146))),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(implies(implies(X_146,or(X_147,X_146)),or(X_147,implies(X_146,X_146)))),true,theorem(or(X_147,implies(X_146,X_146))),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_109,plain,
( ifeq(theorem(implies(implies(X_146,or(X_147,X_146)),or(X_147,implies(X_146,X_146)))),true,theorem(or(X_147,implies(X_146,X_146))),true) != true
| ifeq(true,true,theorem(or(X_147,implies(X_146,X_146))),true) = true ),
inference(resolve,[$cnf( $equal(theorem(implies(implies(X_146,or(X_147,X_146)),or(X_147,implies(X_146,X_146)))),true) )],[refute_0_107,refute_0_108]) ).
cnf(refute_0_110,plain,
ifeq(true,true,theorem(or(X_147,implies(X_146,X_146))),true) = true,
inference(resolve,[$cnf( $equal(ifeq(theorem(implies(implies(X_146,or(X_147,X_146)),or(X_147,implies(X_146,X_146)))),true,theorem(or(X_147,implies(X_146,X_146))),true),true) )],[refute_0_76,refute_0_109]) ).
cnf(refute_0_111,plain,
ifeq(true,true,theorem(or(X_147,implies(X_146,X_146))),true) = theorem(or(X_147,implies(X_146,X_146))),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(theorem(or(X_147,implies(X_146,X_146))))),bind(C,$fot(true))]]) ).
cnf(refute_0_112,plain,
( ifeq(true,true,theorem(or(X_147,implies(X_146,X_146))),true) != theorem(or(X_147,implies(X_146,X_146)))
| ifeq(true,true,theorem(or(X_147,implies(X_146,X_146))),true) != true
| theorem(or(X_147,implies(X_146,X_146))) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,theorem(or(X_147,implies(X_146,X_146))),true),true) ),[0],$fot(theorem(or(X_147,implies(X_146,X_146))))]]) ).
cnf(refute_0_113,plain,
( ifeq(true,true,theorem(or(X_147,implies(X_146,X_146))),true) != true
| theorem(or(X_147,implies(X_146,X_146))) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(or(X_147,implies(X_146,X_146))),true),theorem(or(X_147,implies(X_146,X_146)))) )],[refute_0_111,refute_0_112]) ).
cnf(refute_0_114,plain,
theorem(or(X_147,implies(X_146,X_146))) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(or(X_147,implies(X_146,X_146))),true),true) )],[refute_0_110,refute_0_113]) ).
cnf(refute_0_115,plain,
theorem(or(implies(X_149,X_149),implies(X_149,X_149))) = true,
inference(subst,[],[refute_0_114:[bind(X_146,$fot(X_149)),bind(X_147,$fot(implies(X_149,X_149)))]]) ).
cnf(refute_0_116,plain,
( ifeq(theorem(or(implies(X_149,X_149),implies(X_149,X_149))),true,theorem(implies(X_149,X_149)),true) != true
| theorem(or(implies(X_149,X_149),implies(X_149,X_149))) != true
| ifeq(true,true,theorem(implies(X_149,X_149)),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(or(implies(X_149,X_149),implies(X_149,X_149))),true,theorem(implies(X_149,X_149)),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_117,plain,
( ifeq(theorem(or(implies(X_149,X_149),implies(X_149,X_149))),true,theorem(implies(X_149,X_149)),true) != true
| ifeq(true,true,theorem(implies(X_149,X_149)),true) = true ),
inference(resolve,[$cnf( $equal(theorem(or(implies(X_149,X_149),implies(X_149,X_149))),true) )],[refute_0_115,refute_0_116]) ).
cnf(refute_0_118,plain,
ifeq(true,true,theorem(implies(X_149,X_149)),true) = true,
inference(resolve,[$cnf( $equal(ifeq(theorem(or(implies(X_149,X_149),implies(X_149,X_149))),true,theorem(implies(X_149,X_149)),true),true) )],[refute_0_54,refute_0_117]) ).
cnf(refute_0_119,plain,
ifeq(true,true,theorem(implies(X_149,X_149)),true) = theorem(implies(X_149,X_149)),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(theorem(implies(X_149,X_149)))),bind(C,$fot(true))]]) ).
cnf(refute_0_120,plain,
( ifeq(true,true,theorem(implies(X_149,X_149)),true) != theorem(implies(X_149,X_149))
| ifeq(true,true,theorem(implies(X_149,X_149)),true) != true
| theorem(implies(X_149,X_149)) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,theorem(implies(X_149,X_149)),true),true) ),[0],$fot(theorem(implies(X_149,X_149)))]]) ).
cnf(refute_0_121,plain,
( ifeq(true,true,theorem(implies(X_149,X_149)),true) != true
| theorem(implies(X_149,X_149)) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(implies(X_149,X_149)),true),theorem(implies(X_149,X_149))) )],[refute_0_119,refute_0_120]) ).
cnf(refute_0_122,plain,
theorem(implies(X_149,X_149)) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(implies(X_149,X_149)),true),true) )],[refute_0_118,refute_0_121]) ).
cnf(refute_0_123,plain,
theorem(implies(not(X_116),not(X_116))) = true,
inference(subst,[],[refute_0_122:[bind(X_149,$fot(not(X_116)))]]) ).
cnf(refute_0_124,plain,
( ifeq(theorem(implies(not(X_116),not(X_116))),true,theorem(implies(X_116,not(not(X_116)))),true) != true
| theorem(implies(not(X_116),not(X_116))) != true
| ifeq(true,true,theorem(implies(X_116,not(not(X_116)))),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(implies(not(X_116),not(X_116))),true,theorem(implies(X_116,not(not(X_116)))),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_125,plain,
( ifeq(theorem(implies(not(X_116),not(X_116))),true,theorem(implies(X_116,not(not(X_116)))),true) != true
| ifeq(true,true,theorem(implies(X_116,not(not(X_116)))),true) = true ),
inference(resolve,[$cnf( $equal(theorem(implies(not(X_116),not(X_116))),true) )],[refute_0_123,refute_0_124]) ).
cnf(refute_0_126,plain,
ifeq(true,true,theorem(implies(X_116,not(not(X_116)))),true) = true,
inference(resolve,[$cnf( $equal(ifeq(theorem(implies(not(X_116),not(X_116))),true,theorem(implies(X_116,not(not(X_116)))),true),true) )],[refute_0_36,refute_0_125]) ).
cnf(refute_0_127,plain,
ifeq(true,true,theorem(implies(X_116,not(not(X_116)))),true) = theorem(implies(X_116,not(not(X_116)))),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(theorem(implies(X_116,not(not(X_116)))))),bind(C,$fot(true))]]) ).
cnf(refute_0_128,plain,
( ifeq(true,true,theorem(implies(X_116,not(not(X_116)))),true) != theorem(implies(X_116,not(not(X_116))))
| ifeq(true,true,theorem(implies(X_116,not(not(X_116)))),true) != true
| theorem(implies(X_116,not(not(X_116)))) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,theorem(implies(X_116,not(not(X_116)))),true),true) ),[0],$fot(theorem(implies(X_116,not(not(X_116)))))]]) ).
cnf(refute_0_129,plain,
( ifeq(true,true,theorem(implies(X_116,not(not(X_116)))),true) != true
| theorem(implies(X_116,not(not(X_116)))) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(implies(X_116,not(not(X_116)))),true),theorem(implies(X_116,not(not(X_116))))) )],[refute_0_127,refute_0_128]) ).
cnf(refute_0_130,plain,
theorem(implies(X_116,not(not(X_116)))) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(implies(X_116,not(not(X_116)))),true),true) )],[refute_0_126,refute_0_129]) ).
cnf(refute_0_131,plain,
theorem(implies(X_153,not(not(X_153)))) = true,
inference(subst,[],[refute_0_130:[bind(X_116,$fot(X_153))]]) ).
cnf(refute_0_132,plain,
( ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(theorem(implies(X_153,not(not(X_153)))),true,theorem(X),true),true) != true
| theorem(implies(X_153,not(not(X_153)))) != true
| ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(theorem(implies(X_153,not(not(X_153)))),true,theorem(X),true),true),true) ),[0,2,0],$fot(true)]]) ).
cnf(refute_0_133,plain,
( ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(theorem(implies(X_153,not(not(X_153)))),true,theorem(X),true),true) != true
| ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true) = true ),
inference(resolve,[$cnf( $equal(theorem(implies(X_153,not(not(X_153)))),true) )],[refute_0_131,refute_0_132]) ).
cnf(refute_0_134,plain,
ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true) = true,
inference(resolve,[$cnf( $equal(ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(theorem(implies(X_153,not(not(X_153)))),true,theorem(X),true),true),true) )],[refute_0_0,refute_0_133]) ).
cnf(refute_0_135,plain,
ifeq(true,true,theorem(X),true) = theorem(X),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(theorem(X))),bind(C,$fot(true))]]) ).
cnf(refute_0_136,plain,
ifeq(theorem(or(and(X_153,not(X_153)),X)),true,ifeq(true,true,theorem(X),true),true) = ifeq(theorem(or(and(X_153,not(X_153)),X)),true,ifeq(true,true,theorem(X),true),true),
introduced(tautology,[refl,[$fot(ifeq(theorem(or(and(X_153,not(X_153)),X)),true,ifeq(true,true,theorem(X),true),true))]]) ).
cnf(refute_0_137,plain,
( ifeq(theorem(or(and(X_153,not(X_153)),X)),true,ifeq(true,true,theorem(X),true),true) != ifeq(theorem(or(and(X_153,not(X_153)),X)),true,ifeq(true,true,theorem(X),true),true)
| ifeq(true,true,theorem(X),true) != theorem(X)
| ifeq(theorem(or(and(X_153,not(X_153)),X)),true,ifeq(true,true,theorem(X),true),true) = ifeq(theorem(or(and(X_153,not(X_153)),X)),true,theorem(X),true) ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(or(and(X_153,not(X_153)),X)),true,ifeq(true,true,theorem(X),true),true),ifeq(theorem(or(and(X_153,not(X_153)),X)),true,ifeq(true,true,theorem(X),true),true)) ),[1,2],$fot(theorem(X))]]) ).
cnf(refute_0_138,plain,
( ifeq(true,true,theorem(X),true) != theorem(X)
| ifeq(theorem(or(and(X_153,not(X_153)),X)),true,ifeq(true,true,theorem(X),true),true) = ifeq(theorem(or(and(X_153,not(X_153)),X)),true,theorem(X),true) ),
inference(resolve,[$cnf( $equal(ifeq(theorem(or(and(X_153,not(X_153)),X)),true,ifeq(true,true,theorem(X),true),true),ifeq(theorem(or(and(X_153,not(X_153)),X)),true,ifeq(true,true,theorem(X),true),true)) )],[refute_0_136,refute_0_137]) ).
cnf(refute_0_139,plain,
ifeq(theorem(or(and(X_153,not(X_153)),X)),true,ifeq(true,true,theorem(X),true),true) = ifeq(theorem(or(and(X_153,not(X_153)),X)),true,theorem(X),true),
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(X),true),theorem(X)) )],[refute_0_135,refute_0_138]) ).
cnf(refute_0_140,plain,
implies(implies(P,not(Q)),X_17) = or(not(implies(P,not(Q))),X_17),
inference(subst,[],[implies_definition:[bind(X,$fot(implies(P,not(Q)))),bind(Y,$fot(X_17))]]) ).
cnf(refute_0_141,plain,
or(not(P),not(Q)) = implies(P,not(Q)),
inference(subst,[],[refute_0_86:[bind(X,$fot(P)),bind(Y,$fot(not(Q)))]]) ).
cnf(refute_0_142,plain,
not(or(not(P),not(Q))) = not(or(not(P),not(Q))),
introduced(tautology,[refl,[$fot(not(or(not(P),not(Q))))]]) ).
cnf(refute_0_143,plain,
( not(or(not(P),not(Q))) != not(or(not(P),not(Q)))
| or(not(P),not(Q)) != implies(P,not(Q))
| not(or(not(P),not(Q))) = not(implies(P,not(Q))) ),
introduced(tautology,[equality,[$cnf( $equal(not(or(not(P),not(Q))),not(or(not(P),not(Q)))) ),[1,0],$fot(implies(P,not(Q)))]]) ).
cnf(refute_0_144,plain,
( or(not(P),not(Q)) != implies(P,not(Q))
| not(or(not(P),not(Q))) = not(implies(P,not(Q))) ),
inference(resolve,[$cnf( $equal(not(or(not(P),not(Q))),not(or(not(P),not(Q)))) )],[refute_0_142,refute_0_143]) ).
cnf(refute_0_145,plain,
not(or(not(P),not(Q))) = not(implies(P,not(Q))),
inference(resolve,[$cnf( $equal(or(not(P),not(Q)),implies(P,not(Q))) )],[refute_0_141,refute_0_144]) ).
cnf(refute_0_146,plain,
( and(P,Q) != not(or(not(P),not(Q)))
| not(or(not(P),not(Q))) != not(implies(P,not(Q)))
| and(P,Q) = not(implies(P,not(Q))) ),
introduced(tautology,[equality,[$cnf( ~ $equal(and(P,Q),not(implies(P,not(Q)))) ),[0],$fot(not(or(not(P),not(Q))))]]) ).
cnf(refute_0_147,plain,
( and(P,Q) != not(or(not(P),not(Q)))
| and(P,Q) = not(implies(P,not(Q))) ),
inference(resolve,[$cnf( $equal(not(or(not(P),not(Q))),not(implies(P,not(Q)))) )],[refute_0_145,refute_0_146]) ).
cnf(refute_0_148,plain,
and(P,Q) = not(implies(P,not(Q))),
inference(resolve,[$cnf( $equal(and(P,Q),not(or(not(P),not(Q)))) )],[and_defn,refute_0_147]) ).
cnf(refute_0_149,plain,
( and(P,Q) != not(implies(P,not(Q)))
| not(implies(P,not(Q))) = and(P,Q) ),
inference(subst,[],[refute_0_15:[bind(X0,$fot(and(P,Q))),bind(Y0,$fot(not(implies(P,not(Q)))))]]) ).
cnf(refute_0_150,plain,
not(implies(P,not(Q))) = and(P,Q),
inference(resolve,[$cnf( $equal(and(P,Q),not(implies(P,not(Q)))) )],[refute_0_148,refute_0_149]) ).
cnf(refute_0_151,plain,
( implies(implies(P,not(Q)),X_17) != or(not(implies(P,not(Q))),X_17)
| not(implies(P,not(Q))) != and(P,Q)
| implies(implies(P,not(Q)),X_17) = or(and(P,Q),X_17) ),
introduced(tautology,[equality,[$cnf( $equal(implies(implies(P,not(Q)),X_17),or(not(implies(P,not(Q))),X_17)) ),[1,0],$fot(and(P,Q))]]) ).
cnf(refute_0_152,plain,
( implies(implies(P,not(Q)),X_17) != or(not(implies(P,not(Q))),X_17)
| implies(implies(P,not(Q)),X_17) = or(and(P,Q),X_17) ),
inference(resolve,[$cnf( $equal(not(implies(P,not(Q))),and(P,Q)) )],[refute_0_150,refute_0_151]) ).
cnf(refute_0_153,plain,
implies(implies(P,not(Q)),X_17) = or(and(P,Q),X_17),
inference(resolve,[$cnf( $equal(implies(implies(P,not(Q)),X_17),or(not(implies(P,not(Q))),X_17)) )],[refute_0_140,refute_0_152]) ).
cnf(refute_0_154,plain,
implies(implies(X_153,not(not(X_153))),X) = or(and(X_153,not(X_153)),X),
inference(subst,[],[refute_0_153:[bind(P,$fot(X_153)),bind(Q,$fot(not(X_153))),bind(X_17,$fot(X))]]) ).
cnf(refute_0_155,plain,
theorem(implies(implies(X_153,not(not(X_153))),X)) = theorem(implies(implies(X_153,not(not(X_153))),X)),
introduced(tautology,[refl,[$fot(theorem(implies(implies(X_153,not(not(X_153))),X)))]]) ).
cnf(refute_0_156,plain,
( implies(implies(X_153,not(not(X_153))),X) != or(and(X_153,not(X_153)),X)
| theorem(implies(implies(X_153,not(not(X_153))),X)) != theorem(implies(implies(X_153,not(not(X_153))),X))
| theorem(implies(implies(X_153,not(not(X_153))),X)) = theorem(or(and(X_153,not(X_153)),X)) ),
introduced(tautology,[equality,[$cnf( $equal(theorem(implies(implies(X_153,not(not(X_153))),X)),theorem(implies(implies(X_153,not(not(X_153))),X))) ),[1,0],$fot(or(and(X_153,not(X_153)),X))]]) ).
cnf(refute_0_157,plain,
( implies(implies(X_153,not(not(X_153))),X) != or(and(X_153,not(X_153)),X)
| theorem(implies(implies(X_153,not(not(X_153))),X)) = theorem(or(and(X_153,not(X_153)),X)) ),
inference(resolve,[$cnf( $equal(theorem(implies(implies(X_153,not(not(X_153))),X)),theorem(implies(implies(X_153,not(not(X_153))),X))) )],[refute_0_155,refute_0_156]) ).
cnf(refute_0_158,plain,
theorem(implies(implies(X_153,not(not(X_153))),X)) = theorem(or(and(X_153,not(X_153)),X)),
inference(resolve,[$cnf( $equal(implies(implies(X_153,not(not(X_153))),X),or(and(X_153,not(X_153)),X)) )],[refute_0_154,refute_0_157]) ).
cnf(refute_0_159,plain,
ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true) = ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true),
introduced(tautology,[refl,[$fot(ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true))]]) ).
cnf(refute_0_160,plain,
( ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true) != ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true)
| theorem(implies(implies(X_153,not(not(X_153))),X)) != theorem(or(and(X_153,not(X_153)),X))
| ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true) = ifeq(theorem(or(and(X_153,not(X_153)),X)),true,ifeq(true,true,theorem(X),true),true) ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true),ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true)) ),[1,0],$fot(theorem(or(and(X_153,not(X_153)),X)))]]) ).
cnf(refute_0_161,plain,
( theorem(implies(implies(X_153,not(not(X_153))),X)) != theorem(or(and(X_153,not(X_153)),X))
| ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true) = ifeq(theorem(or(and(X_153,not(X_153)),X)),true,ifeq(true,true,theorem(X),true),true) ),
inference(resolve,[$cnf( $equal(ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true),ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true)) )],[refute_0_159,refute_0_160]) ).
cnf(refute_0_162,plain,
ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true) = ifeq(theorem(or(and(X_153,not(X_153)),X)),true,ifeq(true,true,theorem(X),true),true),
inference(resolve,[$cnf( $equal(theorem(implies(implies(X_153,not(not(X_153))),X)),theorem(or(and(X_153,not(X_153)),X))) )],[refute_0_158,refute_0_161]) ).
cnf(refute_0_163,plain,
( Y0 != X0
| Y0 != Z
| X0 = Z ),
introduced(tautology,[equality,[$cnf( $equal(Y0,Z) ),[0],$fot(X0)]]) ).
cnf(refute_0_164,plain,
( X0 != Y0
| Y0 != Z
| X0 = Z ),
inference(resolve,[$cnf( $equal(Y0,X0) )],[refute_0_15,refute_0_163]) ).
cnf(refute_0_165,plain,
( ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true) != ifeq(theorem(or(and(X_153,not(X_153)),X)),true,ifeq(true,true,theorem(X),true),true)
| ifeq(theorem(or(and(X_153,not(X_153)),X)),true,ifeq(true,true,theorem(X),true),true) != ifeq(theorem(or(and(X_153,not(X_153)),X)),true,theorem(X),true)
| ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true) = ifeq(theorem(or(and(X_153,not(X_153)),X)),true,theorem(X),true) ),
inference(subst,[],[refute_0_164:[bind(X0,$fot(ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true))),bind(Y0,$fot(ifeq(theorem(or(and(X_153,not(X_153)),X)),true,ifeq(true,true,theorem(X),true),true))),bind(Z,$fot(ifeq(theorem(or(and(X_153,not(X_153)),X)),true,theorem(X),true)))]]) ).
cnf(refute_0_166,plain,
( ifeq(theorem(or(and(X_153,not(X_153)),X)),true,ifeq(true,true,theorem(X),true),true) != ifeq(theorem(or(and(X_153,not(X_153)),X)),true,theorem(X),true)
| ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true) = ifeq(theorem(or(and(X_153,not(X_153)),X)),true,theorem(X),true) ),
inference(resolve,[$cnf( $equal(ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true),ifeq(theorem(or(and(X_153,not(X_153)),X)),true,ifeq(true,true,theorem(X),true),true)) )],[refute_0_162,refute_0_165]) ).
cnf(refute_0_167,plain,
ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true) = ifeq(theorem(or(and(X_153,not(X_153)),X)),true,theorem(X),true),
inference(resolve,[$cnf( $equal(ifeq(theorem(or(and(X_153,not(X_153)),X)),true,ifeq(true,true,theorem(X),true),true),ifeq(theorem(or(and(X_153,not(X_153)),X)),true,theorem(X),true)) )],[refute_0_139,refute_0_166]) ).
cnf(refute_0_168,plain,
( ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true) != ifeq(theorem(or(and(X_153,not(X_153)),X)),true,theorem(X),true)
| ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true) != true
| ifeq(theorem(or(and(X_153,not(X_153)),X)),true,theorem(X),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true),true) ),[0],$fot(ifeq(theorem(or(and(X_153,not(X_153)),X)),true,theorem(X),true))]]) ).
cnf(refute_0_169,plain,
( ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true) != true
| ifeq(theorem(or(and(X_153,not(X_153)),X)),true,theorem(X),true) = true ),
inference(resolve,[$cnf( $equal(ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true),ifeq(theorem(or(and(X_153,not(X_153)),X)),true,theorem(X),true)) )],[refute_0_167,refute_0_168]) ).
cnf(refute_0_170,plain,
ifeq(theorem(or(and(X_153,not(X_153)),X)),true,theorem(X),true) = true,
inference(resolve,[$cnf( $equal(ifeq(theorem(implies(implies(X_153,not(not(X_153))),X)),true,ifeq(true,true,theorem(X),true),true),true) )],[refute_0_134,refute_0_169]) ).
cnf(refute_0_171,plain,
ifeq(theorem(or(and(X_2323,not(X_2323)),equivalent(X_2323,not(not(X_2323))))),true,theorem(equivalent(X_2323,not(not(X_2323)))),true) = true,
inference(subst,[],[refute_0_170:[bind(X,$fot(equivalent(X_2323,not(not(X_2323))))),bind(X_153,$fot(X_2323))]]) ).
cnf(refute_0_172,plain,
ifeq(theorem(implies(or(X_6,X_7),or(X_7,X_6))),true,ifeq(theorem(or(X_6,X_7)),true,theorem(or(X_7,X_6)),true),true) = true,
inference(subst,[],[rule_2:[bind(X,$fot(or(X_7,X_6))),bind(Y,$fot(or(X_6,X_7)))]]) ).
cnf(refute_0_173,plain,
( ifeq(theorem(implies(or(X_6,X_7),or(X_7,X_6))),true,ifeq(theorem(or(X_6,X_7)),true,theorem(or(X_7,X_6)),true),true) != true
| theorem(implies(or(X_6,X_7),or(X_7,X_6))) != true
| ifeq(true,true,ifeq(theorem(or(X_6,X_7)),true,theorem(or(X_7,X_6)),true),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(implies(or(X_6,X_7),or(X_7,X_6))),true,ifeq(theorem(or(X_6,X_7)),true,theorem(or(X_7,X_6)),true),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_174,plain,
( ifeq(theorem(implies(or(X_6,X_7),or(X_7,X_6))),true,ifeq(theorem(or(X_6,X_7)),true,theorem(or(X_7,X_6)),true),true) != true
| ifeq(true,true,ifeq(theorem(or(X_6,X_7)),true,theorem(or(X_7,X_6)),true),true) = true ),
inference(resolve,[$cnf( $equal(theorem(implies(or(X_6,X_7),or(X_7,X_6))),true) )],[refute_0_10,refute_0_173]) ).
cnf(refute_0_175,plain,
ifeq(true,true,ifeq(theorem(or(X_6,X_7)),true,theorem(or(X_7,X_6)),true),true) = true,
inference(resolve,[$cnf( $equal(ifeq(theorem(implies(or(X_6,X_7),or(X_7,X_6))),true,ifeq(theorem(or(X_6,X_7)),true,theorem(or(X_7,X_6)),true),true),true) )],[refute_0_172,refute_0_174]) ).
cnf(refute_0_176,plain,
ifeq(true,true,ifeq(theorem(or(X_6,X_7)),true,theorem(or(X_7,X_6)),true),true) = ifeq(theorem(or(X_6,X_7)),true,theorem(or(X_7,X_6)),true),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(ifeq(theorem(or(X_6,X_7)),true,theorem(or(X_7,X_6)),true))),bind(C,$fot(true))]]) ).
cnf(refute_0_177,plain,
( ifeq(true,true,ifeq(theorem(or(X_6,X_7)),true,theorem(or(X_7,X_6)),true),true) != ifeq(theorem(or(X_6,X_7)),true,theorem(or(X_7,X_6)),true)
| ifeq(true,true,ifeq(theorem(or(X_6,X_7)),true,theorem(or(X_7,X_6)),true),true) != true
| ifeq(theorem(or(X_6,X_7)),true,theorem(or(X_7,X_6)),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,ifeq(theorem(or(X_6,X_7)),true,theorem(or(X_7,X_6)),true),true),true) ),[0],$fot(ifeq(theorem(or(X_6,X_7)),true,theorem(or(X_7,X_6)),true))]]) ).
cnf(refute_0_178,plain,
( ifeq(true,true,ifeq(theorem(or(X_6,X_7)),true,theorem(or(X_7,X_6)),true),true) != true
| ifeq(theorem(or(X_6,X_7)),true,theorem(or(X_7,X_6)),true) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,ifeq(theorem(or(X_6,X_7)),true,theorem(or(X_7,X_6)),true),true),ifeq(theorem(or(X_6,X_7)),true,theorem(or(X_7,X_6)),true)) )],[refute_0_176,refute_0_177]) ).
cnf(refute_0_179,plain,
ifeq(theorem(or(X_6,X_7)),true,theorem(or(X_7,X_6)),true) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,ifeq(theorem(or(X_6,X_7)),true,theorem(or(X_7,X_6)),true),true),true) )],[refute_0_175,refute_0_178]) ).
cnf(refute_0_180,plain,
ifeq(theorem(or(equivalent(X_1959,not(not(X_1959))),and(X_1959,not(X_1959)))),true,theorem(or(and(X_1959,not(X_1959)),equivalent(X_1959,not(not(X_1959))))),true) = true,
inference(subst,[],[refute_0_179:[bind(X_6,$fot(equivalent(X_1959,not(not(X_1959))))),bind(X_7,$fot(and(X_1959,not(X_1959))))]]) ).
cnf(refute_0_181,plain,
ifeq(theorem(implies(implies(not(X_347),X_348),or(equivalent(X_348,not(X_347)),and(X_348,X_347)))),true,ifeq(theorem(implies(not(X_347),X_348)),true,theorem(or(equivalent(X_348,not(X_347)),and(X_348,X_347))),true),true) = true,
inference(subst,[],[rule_2:[bind(X,$fot(or(equivalent(X_348,not(X_347)),and(X_348,X_347)))),bind(Y,$fot(implies(not(X_347),X_348)))]]) ).
cnf(refute_0_182,plain,
ifeq(theorem(implies(or(X_71,implies(X_70,X_72)),implies(X_70,or(X_71,X_72)))),true,ifeq(theorem(or(X_71,implies(X_70,X_72))),true,theorem(implies(X_70,or(X_71,X_72))),true),true) = true,
inference(subst,[],[rule_2:[bind(X,$fot(implies(X_70,or(X_71,X_72)))),bind(Y,$fot(or(X_71,implies(X_70,X_72))))]]) ).
cnf(refute_0_183,plain,
ifeq(axiom(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))),true,theorem(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))),true) = true,
inference(subst,[],[rule_1:[bind(X,$fot(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))))]]) ).
cnf(refute_0_184,plain,
axiom(implies(or(X_22,or(not(X),X_24)),or(not(X),or(X_22,X_24)))) = true,
inference(subst,[],[axiom_1_5:[bind(A,$fot(X_22)),bind(B,$fot(not(X))),bind(C,$fot(X_24))]]) ).
cnf(refute_0_185,plain,
implies(X,or(X_22,X_24)) = or(not(X),or(X_22,X_24)),
inference(subst,[],[implies_definition:[bind(Y,$fot(or(X_22,X_24)))]]) ).
cnf(refute_0_186,plain,
( implies(X,or(X_22,X_24)) != or(not(X),or(X_22,X_24))
| or(not(X),or(X_22,X_24)) = implies(X,or(X_22,X_24)) ),
inference(subst,[],[refute_0_15:[bind(X0,$fot(implies(X,or(X_22,X_24)))),bind(Y0,$fot(or(not(X),or(X_22,X_24))))]]) ).
cnf(refute_0_187,plain,
or(not(X),or(X_22,X_24)) = implies(X,or(X_22,X_24)),
inference(resolve,[$cnf( $equal(implies(X,or(X_22,X_24)),or(not(X),or(X_22,X_24))) )],[refute_0_185,refute_0_186]) ).
cnf(refute_0_188,plain,
( axiom(implies(or(X_22,or(not(X),X_24)),or(not(X),or(X_22,X_24)))) != true
| or(not(X),or(X_22,X_24)) != implies(X,or(X_22,X_24))
| axiom(implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24)))) = true ),
introduced(tautology,[equality,[$cnf( $equal(axiom(implies(or(X_22,or(not(X),X_24)),or(not(X),or(X_22,X_24)))),true) ),[0,0,1],$fot(implies(X,or(X_22,X_24)))]]) ).
cnf(refute_0_189,plain,
( axiom(implies(or(X_22,or(not(X),X_24)),or(not(X),or(X_22,X_24)))) != true
| axiom(implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24)))) = true ),
inference(resolve,[$cnf( $equal(or(not(X),or(X_22,X_24)),implies(X,or(X_22,X_24))) )],[refute_0_187,refute_0_188]) ).
cnf(refute_0_190,plain,
axiom(implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24)))) = true,
inference(resolve,[$cnf( $equal(axiom(implies(or(X_22,or(not(X),X_24)),or(not(X),or(X_22,X_24)))),true) )],[refute_0_184,refute_0_189]) ).
cnf(refute_0_191,plain,
or(X_22,or(not(X),X_24)) = or(X_22,or(not(X),X_24)),
introduced(tautology,[refl,[$fot(or(X_22,or(not(X),X_24)))]]) ).
cnf(refute_0_192,plain,
( or(X_22,or(not(X),X_24)) != or(X_22,or(not(X),X_24))
| or(not(X),X_24) != implies(X,X_24)
| or(X_22,or(not(X),X_24)) = or(X_22,implies(X,X_24)) ),
introduced(tautology,[equality,[$cnf( $equal(or(X_22,or(not(X),X_24)),or(X_22,or(not(X),X_24))) ),[1,1],$fot(implies(X,X_24))]]) ).
cnf(refute_0_193,plain,
( or(not(X),X_24) != implies(X,X_24)
| or(X_22,or(not(X),X_24)) = or(X_22,implies(X,X_24)) ),
inference(resolve,[$cnf( $equal(or(X_22,or(not(X),X_24)),or(X_22,or(not(X),X_24))) )],[refute_0_191,refute_0_192]) ).
cnf(refute_0_194,plain,
or(X_22,or(not(X),X_24)) = or(X_22,implies(X,X_24)),
inference(resolve,[$cnf( $equal(or(not(X),X_24),implies(X,X_24)) )],[refute_0_81,refute_0_193]) ).
cnf(refute_0_195,plain,
implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24))) = implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24))),
introduced(tautology,[refl,[$fot(implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24))))]]) ).
cnf(refute_0_196,plain,
( implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24))) != implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24)))
| or(X_22,or(not(X),X_24)) != or(X_22,implies(X,X_24))
| implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24))) = implies(or(X_22,implies(X,X_24)),implies(X,or(X_22,X_24))) ),
introduced(tautology,[equality,[$cnf( $equal(implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24))),implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24)))) ),[1,0],$fot(or(X_22,implies(X,X_24)))]]) ).
cnf(refute_0_197,plain,
( or(X_22,or(not(X),X_24)) != or(X_22,implies(X,X_24))
| implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24))) = implies(or(X_22,implies(X,X_24)),implies(X,or(X_22,X_24))) ),
inference(resolve,[$cnf( $equal(implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24))),implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24)))) )],[refute_0_195,refute_0_196]) ).
cnf(refute_0_198,plain,
implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24))) = implies(or(X_22,implies(X,X_24)),implies(X,or(X_22,X_24))),
inference(resolve,[$cnf( $equal(or(X_22,or(not(X),X_24)),or(X_22,implies(X,X_24))) )],[refute_0_194,refute_0_197]) ).
cnf(refute_0_199,plain,
axiom(implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24)))) = axiom(implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24)))),
introduced(tautology,[refl,[$fot(axiom(implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24)))))]]) ).
cnf(refute_0_200,plain,
( axiom(implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24)))) != axiom(implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24))))
| implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24))) != implies(or(X_22,implies(X,X_24)),implies(X,or(X_22,X_24)))
| axiom(implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24)))) = axiom(implies(or(X_22,implies(X,X_24)),implies(X,or(X_22,X_24)))) ),
introduced(tautology,[equality,[$cnf( $equal(axiom(implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24)))),axiom(implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24))))) ),[1,0],$fot(implies(or(X_22,implies(X,X_24)),implies(X,or(X_22,X_24))))]]) ).
cnf(refute_0_201,plain,
( implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24))) != implies(or(X_22,implies(X,X_24)),implies(X,or(X_22,X_24)))
| axiom(implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24)))) = axiom(implies(or(X_22,implies(X,X_24)),implies(X,or(X_22,X_24)))) ),
inference(resolve,[$cnf( $equal(axiom(implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24)))),axiom(implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24))))) )],[refute_0_199,refute_0_200]) ).
cnf(refute_0_202,plain,
axiom(implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24)))) = axiom(implies(or(X_22,implies(X,X_24)),implies(X,or(X_22,X_24)))),
inference(resolve,[$cnf( $equal(implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24))),implies(or(X_22,implies(X,X_24)),implies(X,or(X_22,X_24)))) )],[refute_0_198,refute_0_201]) ).
cnf(refute_0_203,plain,
( axiom(implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24)))) != axiom(implies(or(X_22,implies(X,X_24)),implies(X,or(X_22,X_24))))
| axiom(implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24)))) != true
| axiom(implies(or(X_22,implies(X,X_24)),implies(X,or(X_22,X_24)))) = true ),
introduced(tautology,[equality,[$cnf( $equal(axiom(implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24)))),true) ),[0],$fot(axiom(implies(or(X_22,implies(X,X_24)),implies(X,or(X_22,X_24)))))]]) ).
cnf(refute_0_204,plain,
( axiom(implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24)))) != true
| axiom(implies(or(X_22,implies(X,X_24)),implies(X,or(X_22,X_24)))) = true ),
inference(resolve,[$cnf( $equal(axiom(implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24)))),axiom(implies(or(X_22,implies(X,X_24)),implies(X,or(X_22,X_24))))) )],[refute_0_202,refute_0_203]) ).
cnf(refute_0_205,plain,
axiom(implies(or(X_22,implies(X,X_24)),implies(X,or(X_22,X_24)))) = true,
inference(resolve,[$cnf( $equal(axiom(implies(or(X_22,or(not(X),X_24)),implies(X,or(X_22,X_24)))),true) )],[refute_0_190,refute_0_204]) ).
cnf(refute_0_206,plain,
axiom(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))) = true,
inference(subst,[],[refute_0_205:[bind(X,$fot(X_67)),bind(X_22,$fot(X_68)),bind(X_24,$fot(X_69))]]) ).
cnf(refute_0_207,plain,
( axiom(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))) != true
| ifeq(axiom(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))),true,theorem(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))),true) != true
| ifeq(true,true,theorem(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(axiom(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))),true,theorem(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_208,plain,
( ifeq(axiom(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))),true,theorem(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))),true) != true
| ifeq(true,true,theorem(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))),true) = true ),
inference(resolve,[$cnf( $equal(axiom(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))),true) )],[refute_0_206,refute_0_207]) ).
cnf(refute_0_209,plain,
ifeq(true,true,theorem(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))),true) = true,
inference(resolve,[$cnf( $equal(ifeq(axiom(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))),true,theorem(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))),true),true) )],[refute_0_183,refute_0_208]) ).
cnf(refute_0_210,plain,
ifeq(true,true,theorem(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))),true) = theorem(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(theorem(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))))),bind(C,$fot(true))]]) ).
cnf(refute_0_211,plain,
( ifeq(true,true,theorem(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))),true) != theorem(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69))))
| ifeq(true,true,theorem(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))),true) != true
| theorem(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,theorem(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))),true),true) ),[0],$fot(theorem(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))))]]) ).
cnf(refute_0_212,plain,
( ifeq(true,true,theorem(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))),true) != true
| theorem(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))),true),theorem(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69))))) )],[refute_0_210,refute_0_211]) ).
cnf(refute_0_213,plain,
theorem(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(implies(or(X_68,implies(X_67,X_69)),implies(X_67,or(X_68,X_69)))),true),true) )],[refute_0_209,refute_0_212]) ).
cnf(refute_0_214,plain,
theorem(implies(or(X_71,implies(X_70,X_72)),implies(X_70,or(X_71,X_72)))) = true,
inference(subst,[],[refute_0_213:[bind(X_67,$fot(X_70)),bind(X_68,$fot(X_71)),bind(X_69,$fot(X_72))]]) ).
cnf(refute_0_215,plain,
( ifeq(theorem(implies(or(X_71,implies(X_70,X_72)),implies(X_70,or(X_71,X_72)))),true,ifeq(theorem(or(X_71,implies(X_70,X_72))),true,theorem(implies(X_70,or(X_71,X_72))),true),true) != true
| theorem(implies(or(X_71,implies(X_70,X_72)),implies(X_70,or(X_71,X_72)))) != true
| ifeq(true,true,ifeq(theorem(or(X_71,implies(X_70,X_72))),true,theorem(implies(X_70,or(X_71,X_72))),true),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(implies(or(X_71,implies(X_70,X_72)),implies(X_70,or(X_71,X_72)))),true,ifeq(theorem(or(X_71,implies(X_70,X_72))),true,theorem(implies(X_70,or(X_71,X_72))),true),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_216,plain,
( ifeq(theorem(implies(or(X_71,implies(X_70,X_72)),implies(X_70,or(X_71,X_72)))),true,ifeq(theorem(or(X_71,implies(X_70,X_72))),true,theorem(implies(X_70,or(X_71,X_72))),true),true) != true
| ifeq(true,true,ifeq(theorem(or(X_71,implies(X_70,X_72))),true,theorem(implies(X_70,or(X_71,X_72))),true),true) = true ),
inference(resolve,[$cnf( $equal(theorem(implies(or(X_71,implies(X_70,X_72)),implies(X_70,or(X_71,X_72)))),true) )],[refute_0_214,refute_0_215]) ).
cnf(refute_0_217,plain,
ifeq(true,true,ifeq(theorem(or(X_71,implies(X_70,X_72))),true,theorem(implies(X_70,or(X_71,X_72))),true),true) = true,
inference(resolve,[$cnf( $equal(ifeq(theorem(implies(or(X_71,implies(X_70,X_72)),implies(X_70,or(X_71,X_72)))),true,ifeq(theorem(or(X_71,implies(X_70,X_72))),true,theorem(implies(X_70,or(X_71,X_72))),true),true),true) )],[refute_0_182,refute_0_216]) ).
cnf(refute_0_218,plain,
ifeq(true,true,ifeq(theorem(or(X_71,implies(X_70,X_72))),true,theorem(implies(X_70,or(X_71,X_72))),true),true) = ifeq(theorem(or(X_71,implies(X_70,X_72))),true,theorem(implies(X_70,or(X_71,X_72))),true),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(ifeq(theorem(or(X_71,implies(X_70,X_72))),true,theorem(implies(X_70,or(X_71,X_72))),true))),bind(C,$fot(true))]]) ).
cnf(refute_0_219,plain,
( ifeq(true,true,ifeq(theorem(or(X_71,implies(X_70,X_72))),true,theorem(implies(X_70,or(X_71,X_72))),true),true) != ifeq(theorem(or(X_71,implies(X_70,X_72))),true,theorem(implies(X_70,or(X_71,X_72))),true)
| ifeq(true,true,ifeq(theorem(or(X_71,implies(X_70,X_72))),true,theorem(implies(X_70,or(X_71,X_72))),true),true) != true
| ifeq(theorem(or(X_71,implies(X_70,X_72))),true,theorem(implies(X_70,or(X_71,X_72))),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,ifeq(theorem(or(X_71,implies(X_70,X_72))),true,theorem(implies(X_70,or(X_71,X_72))),true),true),true) ),[0],$fot(ifeq(theorem(or(X_71,implies(X_70,X_72))),true,theorem(implies(X_70,or(X_71,X_72))),true))]]) ).
cnf(refute_0_220,plain,
( ifeq(true,true,ifeq(theorem(or(X_71,implies(X_70,X_72))),true,theorem(implies(X_70,or(X_71,X_72))),true),true) != true
| ifeq(theorem(or(X_71,implies(X_70,X_72))),true,theorem(implies(X_70,or(X_71,X_72))),true) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,ifeq(theorem(or(X_71,implies(X_70,X_72))),true,theorem(implies(X_70,or(X_71,X_72))),true),true),ifeq(theorem(or(X_71,implies(X_70,X_72))),true,theorem(implies(X_70,or(X_71,X_72))),true)) )],[refute_0_218,refute_0_219]) ).
cnf(refute_0_221,plain,
ifeq(theorem(or(X_71,implies(X_70,X_72))),true,theorem(implies(X_70,or(X_71,X_72))),true) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,ifeq(theorem(or(X_71,implies(X_70,X_72))),true,theorem(implies(X_70,or(X_71,X_72))),true),true),true) )],[refute_0_217,refute_0_220]) ).
cnf(refute_0_222,plain,
ifeq(theorem(or(equivalent(X_83,not(Q)),implies(implies(not(Q),X_83),and(X_83,Q)))),true,theorem(implies(implies(not(Q),X_83),or(equivalent(X_83,not(Q)),and(X_83,Q)))),true) = true,
inference(subst,[],[refute_0_221:[bind(X_70,$fot(implies(not(Q),X_83))),bind(X_71,$fot(equivalent(X_83,not(Q)))),bind(X_72,$fot(and(X_83,Q)))]]) ).
cnf(refute_0_223,plain,
ifeq(axiom(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))),true,theorem(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))),true) = true,
inference(subst,[],[rule_1:[bind(X,$fot(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))))]]) ).
cnf(refute_0_224,plain,
axiom(implies(or(A,not(X_16)),or(not(X_16),A))) = true,
inference(subst,[],[axiom_1_4:[bind(B,$fot(not(X_16)))]]) ).
cnf(refute_0_225,plain,
implies(X_16,A) = or(not(X_16),A),
inference(subst,[],[implies_definition:[bind(X,$fot(X_16)),bind(Y,$fot(A))]]) ).
cnf(refute_0_226,plain,
( implies(X_16,A) != or(not(X_16),A)
| or(not(X_16),A) = implies(X_16,A) ),
inference(subst,[],[refute_0_15:[bind(X0,$fot(implies(X_16,A))),bind(Y0,$fot(or(not(X_16),A)))]]) ).
cnf(refute_0_227,plain,
or(not(X_16),A) = implies(X_16,A),
inference(resolve,[$cnf( $equal(implies(X_16,A),or(not(X_16),A)) )],[refute_0_225,refute_0_226]) ).
cnf(refute_0_228,plain,
( axiom(implies(or(A,not(X_16)),or(not(X_16),A))) != true
| or(not(X_16),A) != implies(X_16,A)
| axiom(implies(or(A,not(X_16)),implies(X_16,A))) = true ),
introduced(tautology,[equality,[$cnf( $equal(axiom(implies(or(A,not(X_16)),or(not(X_16),A))),true) ),[0,0,1],$fot(implies(X_16,A))]]) ).
cnf(refute_0_229,plain,
( axiom(implies(or(A,not(X_16)),or(not(X_16),A))) != true
| axiom(implies(or(A,not(X_16)),implies(X_16,A))) = true ),
inference(resolve,[$cnf( $equal(or(not(X_16),A),implies(X_16,A)) )],[refute_0_227,refute_0_228]) ).
cnf(refute_0_230,plain,
axiom(implies(or(A,not(X_16)),implies(X_16,A))) = true,
inference(resolve,[$cnf( $equal(axiom(implies(or(A,not(X_16)),or(not(X_16),A))),true) )],[refute_0_224,refute_0_229]) ).
cnf(refute_0_231,plain,
axiom(implies(or(not(X),not(X_36)),implies(X_36,not(X)))) = true,
inference(subst,[],[refute_0_230:[bind(A,$fot(not(X))),bind(X_16,$fot(X_36))]]) ).
cnf(refute_0_232,plain,
implies(X,not(X_36)) = or(not(X),not(X_36)),
inference(subst,[],[implies_definition:[bind(Y,$fot(not(X_36)))]]) ).
cnf(refute_0_233,plain,
( implies(X,not(X_36)) != or(not(X),not(X_36))
| or(not(X),not(X_36)) = implies(X,not(X_36)) ),
inference(subst,[],[refute_0_15:[bind(X0,$fot(implies(X,not(X_36)))),bind(Y0,$fot(or(not(X),not(X_36))))]]) ).
cnf(refute_0_234,plain,
or(not(X),not(X_36)) = implies(X,not(X_36)),
inference(resolve,[$cnf( $equal(implies(X,not(X_36)),or(not(X),not(X_36))) )],[refute_0_232,refute_0_233]) ).
cnf(refute_0_235,plain,
( axiom(implies(or(not(X),not(X_36)),implies(X_36,not(X)))) != true
| or(not(X),not(X_36)) != implies(X,not(X_36))
| axiom(implies(implies(X,not(X_36)),implies(X_36,not(X)))) = true ),
introduced(tautology,[equality,[$cnf( $equal(axiom(implies(or(not(X),not(X_36)),implies(X_36,not(X)))),true) ),[0,0,0],$fot(implies(X,not(X_36)))]]) ).
cnf(refute_0_236,plain,
( axiom(implies(or(not(X),not(X_36)),implies(X_36,not(X)))) != true
| axiom(implies(implies(X,not(X_36)),implies(X_36,not(X)))) = true ),
inference(resolve,[$cnf( $equal(or(not(X),not(X_36)),implies(X,not(X_36))) )],[refute_0_234,refute_0_235]) ).
cnf(refute_0_237,plain,
axiom(implies(implies(X,not(X_36)),implies(X_36,not(X)))) = true,
inference(resolve,[$cnf( $equal(axiom(implies(or(not(X),not(X_36)),implies(X_36,not(X)))),true) )],[refute_0_231,refute_0_236]) ).
cnf(refute_0_238,plain,
implies(implies(X,not(X_36)),implies(X_36,not(X))) = or(and(X,X_36),implies(X_36,not(X))),
inference(subst,[],[refute_0_153:[bind(P,$fot(X)),bind(Q,$fot(X_36)),bind(X_17,$fot(implies(X_36,not(X))))]]) ).
cnf(refute_0_239,plain,
axiom(implies(implies(X,not(X_36)),implies(X_36,not(X)))) = axiom(implies(implies(X,not(X_36)),implies(X_36,not(X)))),
introduced(tautology,[refl,[$fot(axiom(implies(implies(X,not(X_36)),implies(X_36,not(X)))))]]) ).
cnf(refute_0_240,plain,
( axiom(implies(implies(X,not(X_36)),implies(X_36,not(X)))) != axiom(implies(implies(X,not(X_36)),implies(X_36,not(X))))
| implies(implies(X,not(X_36)),implies(X_36,not(X))) != or(and(X,X_36),implies(X_36,not(X)))
| axiom(implies(implies(X,not(X_36)),implies(X_36,not(X)))) = axiom(or(and(X,X_36),implies(X_36,not(X)))) ),
introduced(tautology,[equality,[$cnf( $equal(axiom(implies(implies(X,not(X_36)),implies(X_36,not(X)))),axiom(implies(implies(X,not(X_36)),implies(X_36,not(X))))) ),[1,0],$fot(or(and(X,X_36),implies(X_36,not(X))))]]) ).
cnf(refute_0_241,plain,
( implies(implies(X,not(X_36)),implies(X_36,not(X))) != or(and(X,X_36),implies(X_36,not(X)))
| axiom(implies(implies(X,not(X_36)),implies(X_36,not(X)))) = axiom(or(and(X,X_36),implies(X_36,not(X)))) ),
inference(resolve,[$cnf( $equal(axiom(implies(implies(X,not(X_36)),implies(X_36,not(X)))),axiom(implies(implies(X,not(X_36)),implies(X_36,not(X))))) )],[refute_0_239,refute_0_240]) ).
cnf(refute_0_242,plain,
axiom(implies(implies(X,not(X_36)),implies(X_36,not(X)))) = axiom(or(and(X,X_36),implies(X_36,not(X)))),
inference(resolve,[$cnf( $equal(implies(implies(X,not(X_36)),implies(X_36,not(X))),or(and(X,X_36),implies(X_36,not(X)))) )],[refute_0_238,refute_0_241]) ).
cnf(refute_0_243,plain,
( axiom(implies(implies(X,not(X_36)),implies(X_36,not(X)))) != axiom(or(and(X,X_36),implies(X_36,not(X))))
| axiom(implies(implies(X,not(X_36)),implies(X_36,not(X)))) != true
| axiom(or(and(X,X_36),implies(X_36,not(X)))) = true ),
introduced(tautology,[equality,[$cnf( $equal(axiom(implies(implies(X,not(X_36)),implies(X_36,not(X)))),true) ),[0],$fot(axiom(or(and(X,X_36),implies(X_36,not(X)))))]]) ).
cnf(refute_0_244,plain,
( axiom(implies(implies(X,not(X_36)),implies(X_36,not(X)))) != true
| axiom(or(and(X,X_36),implies(X_36,not(X)))) = true ),
inference(resolve,[$cnf( $equal(axiom(implies(implies(X,not(X_36)),implies(X_36,not(X)))),axiom(or(and(X,X_36),implies(X_36,not(X))))) )],[refute_0_242,refute_0_243]) ).
cnf(refute_0_245,plain,
axiom(or(and(X,X_36),implies(X_36,not(X)))) = true,
inference(resolve,[$cnf( $equal(axiom(implies(implies(X,not(X_36)),implies(X_36,not(X)))),true) )],[refute_0_237,refute_0_244]) ).
cnf(refute_0_246,plain,
axiom(or(and(implies(X_42,X_43),implies(X_43,X_42)),implies(implies(X_43,X_42),not(implies(X_42,X_43))))) = true,
inference(subst,[],[refute_0_245:[bind(X,$fot(implies(X_42,X_43))),bind(X_36,$fot(implies(X_43,X_42)))]]) ).
cnf(refute_0_247,plain,
equivalent(X_42,X_43) = and(implies(X_42,X_43),implies(X_43,X_42)),
inference(subst,[],[equivalent_defn:[bind(P,$fot(X_42)),bind(Q,$fot(X_43))]]) ).
cnf(refute_0_248,plain,
( equivalent(X_42,X_43) != and(implies(X_42,X_43),implies(X_43,X_42))
| and(implies(X_42,X_43),implies(X_43,X_42)) = equivalent(X_42,X_43) ),
inference(subst,[],[refute_0_15:[bind(X0,$fot(equivalent(X_42,X_43))),bind(Y0,$fot(and(implies(X_42,X_43),implies(X_43,X_42))))]]) ).
cnf(refute_0_249,plain,
and(implies(X_42,X_43),implies(X_43,X_42)) = equivalent(X_42,X_43),
inference(resolve,[$cnf( $equal(equivalent(X_42,X_43),and(implies(X_42,X_43),implies(X_43,X_42))) )],[refute_0_247,refute_0_248]) ).
cnf(refute_0_250,plain,
( and(implies(X_42,X_43),implies(X_43,X_42)) != equivalent(X_42,X_43)
| axiom(or(and(implies(X_42,X_43),implies(X_43,X_42)),implies(implies(X_43,X_42),not(implies(X_42,X_43))))) != true
| axiom(or(equivalent(X_42,X_43),implies(implies(X_43,X_42),not(implies(X_42,X_43))))) = true ),
introduced(tautology,[equality,[$cnf( $equal(axiom(or(and(implies(X_42,X_43),implies(X_43,X_42)),implies(implies(X_43,X_42),not(implies(X_42,X_43))))),true) ),[0,0,0],$fot(equivalent(X_42,X_43))]]) ).
cnf(refute_0_251,plain,
( axiom(or(and(implies(X_42,X_43),implies(X_43,X_42)),implies(implies(X_43,X_42),not(implies(X_42,X_43))))) != true
| axiom(or(equivalent(X_42,X_43),implies(implies(X_43,X_42),not(implies(X_42,X_43))))) = true ),
inference(resolve,[$cnf( $equal(and(implies(X_42,X_43),implies(X_43,X_42)),equivalent(X_42,X_43)) )],[refute_0_249,refute_0_250]) ).
cnf(refute_0_252,plain,
axiom(or(equivalent(X_42,X_43),implies(implies(X_43,X_42),not(implies(X_42,X_43))))) = true,
inference(resolve,[$cnf( $equal(axiom(or(and(implies(X_42,X_43),implies(X_43,X_42)),implies(implies(X_43,X_42),not(implies(X_42,X_43))))),true) )],[refute_0_246,refute_0_251]) ).
cnf(refute_0_253,plain,
axiom(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))) = true,
inference(subst,[],[refute_0_252:[bind(X_42,$fot(X_52)),bind(X_43,$fot(X_53))]]) ).
cnf(refute_0_254,plain,
( axiom(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))) != true
| ifeq(axiom(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))),true,theorem(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))),true) != true
| ifeq(true,true,theorem(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(axiom(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))),true,theorem(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_255,plain,
( ifeq(axiom(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))),true,theorem(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))),true) != true
| ifeq(true,true,theorem(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))),true) = true ),
inference(resolve,[$cnf( $equal(axiom(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))),true) )],[refute_0_253,refute_0_254]) ).
cnf(refute_0_256,plain,
ifeq(true,true,theorem(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))),true) = true,
inference(resolve,[$cnf( $equal(ifeq(axiom(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))),true,theorem(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))),true),true) )],[refute_0_223,refute_0_255]) ).
cnf(refute_0_257,plain,
ifeq(true,true,theorem(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))),true) = theorem(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(theorem(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))))),bind(C,$fot(true))]]) ).
cnf(refute_0_258,plain,
( ifeq(true,true,theorem(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))),true) != theorem(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53)))))
| ifeq(true,true,theorem(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))),true) != true
| theorem(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,theorem(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))),true),true) ),[0],$fot(theorem(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))))]]) ).
cnf(refute_0_259,plain,
( ifeq(true,true,theorem(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))),true) != true
| theorem(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))),true),theorem(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53)))))) )],[refute_0_257,refute_0_258]) ).
cnf(refute_0_260,plain,
theorem(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(or(equivalent(X_52,X_53),implies(implies(X_53,X_52),not(implies(X_52,X_53))))),true),true) )],[refute_0_256,refute_0_259]) ).
cnf(refute_0_261,plain,
theorem(or(equivalent(X_83,not(Q)),implies(implies(not(Q),X_83),not(implies(X_83,not(Q)))))) = true,
inference(subst,[],[refute_0_260:[bind(X_52,$fot(X_83)),bind(X_53,$fot(not(Q)))]]) ).
cnf(refute_0_262,plain,
and(X_83,Q) = not(implies(X_83,not(Q))),
inference(subst,[],[refute_0_148:[bind(P,$fot(X_83))]]) ).
cnf(refute_0_263,plain,
( and(X_83,Q) != not(implies(X_83,not(Q)))
| not(implies(X_83,not(Q))) = and(X_83,Q) ),
inference(subst,[],[refute_0_15:[bind(X0,$fot(and(X_83,Q))),bind(Y0,$fot(not(implies(X_83,not(Q)))))]]) ).
cnf(refute_0_264,plain,
not(implies(X_83,not(Q))) = and(X_83,Q),
inference(resolve,[$cnf( $equal(and(X_83,Q),not(implies(X_83,not(Q)))) )],[refute_0_262,refute_0_263]) ).
cnf(refute_0_265,plain,
( not(implies(X_83,not(Q))) != and(X_83,Q)
| theorem(or(equivalent(X_83,not(Q)),implies(implies(not(Q),X_83),not(implies(X_83,not(Q)))))) != true
| theorem(or(equivalent(X_83,not(Q)),implies(implies(not(Q),X_83),and(X_83,Q)))) = true ),
introduced(tautology,[equality,[$cnf( $equal(theorem(or(equivalent(X_83,not(Q)),implies(implies(not(Q),X_83),not(implies(X_83,not(Q)))))),true) ),[0,0,1,1],$fot(and(X_83,Q))]]) ).
cnf(refute_0_266,plain,
( theorem(or(equivalent(X_83,not(Q)),implies(implies(not(Q),X_83),not(implies(X_83,not(Q)))))) != true
| theorem(or(equivalent(X_83,not(Q)),implies(implies(not(Q),X_83),and(X_83,Q)))) = true ),
inference(resolve,[$cnf( $equal(not(implies(X_83,not(Q))),and(X_83,Q)) )],[refute_0_264,refute_0_265]) ).
cnf(refute_0_267,plain,
theorem(or(equivalent(X_83,not(Q)),implies(implies(not(Q),X_83),and(X_83,Q)))) = true,
inference(resolve,[$cnf( $equal(theorem(or(equivalent(X_83,not(Q)),implies(implies(not(Q),X_83),not(implies(X_83,not(Q)))))),true) )],[refute_0_261,refute_0_266]) ).
cnf(refute_0_268,plain,
( ifeq(theorem(or(equivalent(X_83,not(Q)),implies(implies(not(Q),X_83),and(X_83,Q)))),true,theorem(implies(implies(not(Q),X_83),or(equivalent(X_83,not(Q)),and(X_83,Q)))),true) != true
| theorem(or(equivalent(X_83,not(Q)),implies(implies(not(Q),X_83),and(X_83,Q)))) != true
| ifeq(true,true,theorem(implies(implies(not(Q),X_83),or(equivalent(X_83,not(Q)),and(X_83,Q)))),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(or(equivalent(X_83,not(Q)),implies(implies(not(Q),X_83),and(X_83,Q)))),true,theorem(implies(implies(not(Q),X_83),or(equivalent(X_83,not(Q)),and(X_83,Q)))),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_269,plain,
( ifeq(theorem(or(equivalent(X_83,not(Q)),implies(implies(not(Q),X_83),and(X_83,Q)))),true,theorem(implies(implies(not(Q),X_83),or(equivalent(X_83,not(Q)),and(X_83,Q)))),true) != true
| ifeq(true,true,theorem(implies(implies(not(Q),X_83),or(equivalent(X_83,not(Q)),and(X_83,Q)))),true) = true ),
inference(resolve,[$cnf( $equal(theorem(or(equivalent(X_83,not(Q)),implies(implies(not(Q),X_83),and(X_83,Q)))),true) )],[refute_0_267,refute_0_268]) ).
cnf(refute_0_270,plain,
ifeq(true,true,theorem(implies(implies(not(Q),X_83),or(equivalent(X_83,not(Q)),and(X_83,Q)))),true) = true,
inference(resolve,[$cnf( $equal(ifeq(theorem(or(equivalent(X_83,not(Q)),implies(implies(not(Q),X_83),and(X_83,Q)))),true,theorem(implies(implies(not(Q),X_83),or(equivalent(X_83,not(Q)),and(X_83,Q)))),true),true) )],[refute_0_222,refute_0_269]) ).
cnf(refute_0_271,plain,
ifeq(true,true,theorem(implies(implies(not(Q),X_83),or(equivalent(X_83,not(Q)),and(X_83,Q)))),true) = theorem(implies(implies(not(Q),X_83),or(equivalent(X_83,not(Q)),and(X_83,Q)))),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(theorem(implies(implies(not(Q),X_83),or(equivalent(X_83,not(Q)),and(X_83,Q)))))),bind(C,$fot(true))]]) ).
cnf(refute_0_272,plain,
( ifeq(true,true,theorem(implies(implies(not(Q),X_83),or(equivalent(X_83,not(Q)),and(X_83,Q)))),true) != theorem(implies(implies(not(Q),X_83),or(equivalent(X_83,not(Q)),and(X_83,Q))))
| ifeq(true,true,theorem(implies(implies(not(Q),X_83),or(equivalent(X_83,not(Q)),and(X_83,Q)))),true) != true
| theorem(implies(implies(not(Q),X_83),or(equivalent(X_83,not(Q)),and(X_83,Q)))) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,theorem(implies(implies(not(Q),X_83),or(equivalent(X_83,not(Q)),and(X_83,Q)))),true),true) ),[0],$fot(theorem(implies(implies(not(Q),X_83),or(equivalent(X_83,not(Q)),and(X_83,Q)))))]]) ).
cnf(refute_0_273,plain,
( ifeq(true,true,theorem(implies(implies(not(Q),X_83),or(equivalent(X_83,not(Q)),and(X_83,Q)))),true) != true
| theorem(implies(implies(not(Q),X_83),or(equivalent(X_83,not(Q)),and(X_83,Q)))) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(implies(implies(not(Q),X_83),or(equivalent(X_83,not(Q)),and(X_83,Q)))),true),theorem(implies(implies(not(Q),X_83),or(equivalent(X_83,not(Q)),and(X_83,Q))))) )],[refute_0_271,refute_0_272]) ).
cnf(refute_0_274,plain,
theorem(implies(implies(not(Q),X_83),or(equivalent(X_83,not(Q)),and(X_83,Q)))) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(implies(implies(not(Q),X_83),or(equivalent(X_83,not(Q)),and(X_83,Q)))),true),true) )],[refute_0_270,refute_0_273]) ).
cnf(refute_0_275,plain,
theorem(implies(implies(not(X_347),X_348),or(equivalent(X_348,not(X_347)),and(X_348,X_347)))) = true,
inference(subst,[],[refute_0_274:[bind(Q,$fot(X_347)),bind(X_83,$fot(X_348))]]) ).
cnf(refute_0_276,plain,
( ifeq(theorem(implies(implies(not(X_347),X_348),or(equivalent(X_348,not(X_347)),and(X_348,X_347)))),true,ifeq(theorem(implies(not(X_347),X_348)),true,theorem(or(equivalent(X_348,not(X_347)),and(X_348,X_347))),true),true) != true
| theorem(implies(implies(not(X_347),X_348),or(equivalent(X_348,not(X_347)),and(X_348,X_347)))) != true
| ifeq(true,true,ifeq(theorem(implies(not(X_347),X_348)),true,theorem(or(equivalent(X_348,not(X_347)),and(X_348,X_347))),true),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(implies(implies(not(X_347),X_348),or(equivalent(X_348,not(X_347)),and(X_348,X_347)))),true,ifeq(theorem(implies(not(X_347),X_348)),true,theorem(or(equivalent(X_348,not(X_347)),and(X_348,X_347))),true),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_277,plain,
( ifeq(theorem(implies(implies(not(X_347),X_348),or(equivalent(X_348,not(X_347)),and(X_348,X_347)))),true,ifeq(theorem(implies(not(X_347),X_348)),true,theorem(or(equivalent(X_348,not(X_347)),and(X_348,X_347))),true),true) != true
| ifeq(true,true,ifeq(theorem(implies(not(X_347),X_348)),true,theorem(or(equivalent(X_348,not(X_347)),and(X_348,X_347))),true),true) = true ),
inference(resolve,[$cnf( $equal(theorem(implies(implies(not(X_347),X_348),or(equivalent(X_348,not(X_347)),and(X_348,X_347)))),true) )],[refute_0_275,refute_0_276]) ).
cnf(refute_0_278,plain,
ifeq(true,true,ifeq(theorem(implies(not(X_347),X_348)),true,theorem(or(equivalent(X_348,not(X_347)),and(X_348,X_347))),true),true) = true,
inference(resolve,[$cnf( $equal(ifeq(theorem(implies(implies(not(X_347),X_348),or(equivalent(X_348,not(X_347)),and(X_348,X_347)))),true,ifeq(theorem(implies(not(X_347),X_348)),true,theorem(or(equivalent(X_348,not(X_347)),and(X_348,X_347))),true),true),true) )],[refute_0_181,refute_0_277]) ).
cnf(refute_0_279,plain,
ifeq(true,true,ifeq(theorem(implies(not(X_347),X_348)),true,theorem(or(equivalent(X_348,not(X_347)),and(X_348,X_347))),true),true) = ifeq(theorem(implies(not(X_347),X_348)),true,theorem(or(equivalent(X_348,not(X_347)),and(X_348,X_347))),true),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(ifeq(theorem(implies(not(X_347),X_348)),true,theorem(or(equivalent(X_348,not(X_347)),and(X_348,X_347))),true))),bind(C,$fot(true))]]) ).
cnf(refute_0_280,plain,
( ifeq(true,true,ifeq(theorem(implies(not(X_347),X_348)),true,theorem(or(equivalent(X_348,not(X_347)),and(X_348,X_347))),true),true) != ifeq(theorem(implies(not(X_347),X_348)),true,theorem(or(equivalent(X_348,not(X_347)),and(X_348,X_347))),true)
| ifeq(true,true,ifeq(theorem(implies(not(X_347),X_348)),true,theorem(or(equivalent(X_348,not(X_347)),and(X_348,X_347))),true),true) != true
| ifeq(theorem(implies(not(X_347),X_348)),true,theorem(or(equivalent(X_348,not(X_347)),and(X_348,X_347))),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,ifeq(theorem(implies(not(X_347),X_348)),true,theorem(or(equivalent(X_348,not(X_347)),and(X_348,X_347))),true),true),true) ),[0],$fot(ifeq(theorem(implies(not(X_347),X_348)),true,theorem(or(equivalent(X_348,not(X_347)),and(X_348,X_347))),true))]]) ).
cnf(refute_0_281,plain,
( ifeq(true,true,ifeq(theorem(implies(not(X_347),X_348)),true,theorem(or(equivalent(X_348,not(X_347)),and(X_348,X_347))),true),true) != true
| ifeq(theorem(implies(not(X_347),X_348)),true,theorem(or(equivalent(X_348,not(X_347)),and(X_348,X_347))),true) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,ifeq(theorem(implies(not(X_347),X_348)),true,theorem(or(equivalent(X_348,not(X_347)),and(X_348,X_347))),true),true),ifeq(theorem(implies(not(X_347),X_348)),true,theorem(or(equivalent(X_348,not(X_347)),and(X_348,X_347))),true)) )],[refute_0_279,refute_0_280]) ).
cnf(refute_0_282,plain,
ifeq(theorem(implies(not(X_347),X_348)),true,theorem(or(equivalent(X_348,not(X_347)),and(X_348,X_347))),true) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,ifeq(theorem(implies(not(X_347),X_348)),true,theorem(or(equivalent(X_348,not(X_347)),and(X_348,X_347))),true),true),true) )],[refute_0_278,refute_0_281]) ).
cnf(refute_0_283,plain,
ifeq(theorem(implies(not(not(X_1958)),X_1958)),true,theorem(or(equivalent(X_1958,not(not(X_1958))),and(X_1958,not(X_1958)))),true) = true,
inference(subst,[],[refute_0_282:[bind(X_347,$fot(not(X_1958))),bind(X_348,$fot(X_1958))]]) ).
cnf(refute_0_284,plain,
ifeq(theorem(or(X_6,not(not(not(X_6))))),true,theorem(or(not(not(not(X_6))),X_6)),true) = true,
inference(subst,[],[refute_0_179:[bind(X_7,$fot(not(not(not(X_6)))))]]) ).
cnf(refute_0_285,plain,
ifeq(theorem(implies(or(X_245,X_244),or(X_245,not(not(X_244))))),true,ifeq(theorem(or(X_245,X_244)),true,theorem(or(X_245,not(not(X_244)))),true),true) = true,
inference(subst,[],[rule_2:[bind(X,$fot(or(X_245,not(not(X_244))))),bind(Y,$fot(or(X_245,X_244)))]]) ).
cnf(refute_0_286,plain,
ifeq(theorem(implies(implies(X_54,X_55),implies(or(X_56,X_54),or(X_56,X_55)))),true,ifeq(theorem(implies(X_54,X_55)),true,theorem(implies(or(X_56,X_54),or(X_56,X_55))),true),true) = true,
inference(subst,[],[rule_2:[bind(X,$fot(implies(or(X_56,X_54),or(X_56,X_55)))),bind(Y,$fot(implies(X_54,X_55)))]]) ).
cnf(refute_0_287,plain,
ifeq(axiom(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))),true,theorem(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))),true) = true,
inference(subst,[],[rule_1:[bind(X,$fot(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))))]]) ).
cnf(refute_0_288,plain,
axiom(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))) = true,
inference(subst,[],[axiom_1_6:[bind(A,$fot(X_25)),bind(B,$fot(X_26)),bind(C,$fot(X_27))]]) ).
cnf(refute_0_289,plain,
( axiom(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))) != true
| ifeq(axiom(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))),true,theorem(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))),true) != true
| ifeq(true,true,theorem(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(axiom(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))),true,theorem(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_290,plain,
( ifeq(axiom(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))),true,theorem(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))),true) != true
| ifeq(true,true,theorem(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))),true) = true ),
inference(resolve,[$cnf( $equal(axiom(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))),true) )],[refute_0_288,refute_0_289]) ).
cnf(refute_0_291,plain,
ifeq(true,true,theorem(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))),true) = true,
inference(resolve,[$cnf( $equal(ifeq(axiom(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))),true,theorem(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))),true),true) )],[refute_0_287,refute_0_290]) ).
cnf(refute_0_292,plain,
ifeq(true,true,theorem(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))),true) = theorem(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(theorem(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))))),bind(C,$fot(true))]]) ).
cnf(refute_0_293,plain,
( ifeq(true,true,theorem(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))),true) != theorem(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26))))
| ifeq(true,true,theorem(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))),true) != true
| theorem(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,theorem(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))),true),true) ),[0],$fot(theorem(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))))]]) ).
cnf(refute_0_294,plain,
( ifeq(true,true,theorem(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))),true) != true
| theorem(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))),true),theorem(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26))))) )],[refute_0_292,refute_0_293]) ).
cnf(refute_0_295,plain,
theorem(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(implies(implies(X_25,X_26),implies(or(X_27,X_25),or(X_27,X_26)))),true),true) )],[refute_0_291,refute_0_294]) ).
cnf(refute_0_296,plain,
theorem(implies(implies(X_54,X_55),implies(or(X_56,X_54),or(X_56,X_55)))) = true,
inference(subst,[],[refute_0_295:[bind(X_25,$fot(X_54)),bind(X_26,$fot(X_55)),bind(X_27,$fot(X_56))]]) ).
cnf(refute_0_297,plain,
( ifeq(theorem(implies(implies(X_54,X_55),implies(or(X_56,X_54),or(X_56,X_55)))),true,ifeq(theorem(implies(X_54,X_55)),true,theorem(implies(or(X_56,X_54),or(X_56,X_55))),true),true) != true
| theorem(implies(implies(X_54,X_55),implies(or(X_56,X_54),or(X_56,X_55)))) != true
| ifeq(true,true,ifeq(theorem(implies(X_54,X_55)),true,theorem(implies(or(X_56,X_54),or(X_56,X_55))),true),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(implies(implies(X_54,X_55),implies(or(X_56,X_54),or(X_56,X_55)))),true,ifeq(theorem(implies(X_54,X_55)),true,theorem(implies(or(X_56,X_54),or(X_56,X_55))),true),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_298,plain,
( ifeq(theorem(implies(implies(X_54,X_55),implies(or(X_56,X_54),or(X_56,X_55)))),true,ifeq(theorem(implies(X_54,X_55)),true,theorem(implies(or(X_56,X_54),or(X_56,X_55))),true),true) != true
| ifeq(true,true,ifeq(theorem(implies(X_54,X_55)),true,theorem(implies(or(X_56,X_54),or(X_56,X_55))),true),true) = true ),
inference(resolve,[$cnf( $equal(theorem(implies(implies(X_54,X_55),implies(or(X_56,X_54),or(X_56,X_55)))),true) )],[refute_0_296,refute_0_297]) ).
cnf(refute_0_299,plain,
ifeq(true,true,ifeq(theorem(implies(X_54,X_55)),true,theorem(implies(or(X_56,X_54),or(X_56,X_55))),true),true) = true,
inference(resolve,[$cnf( $equal(ifeq(theorem(implies(implies(X_54,X_55),implies(or(X_56,X_54),or(X_56,X_55)))),true,ifeq(theorem(implies(X_54,X_55)),true,theorem(implies(or(X_56,X_54),or(X_56,X_55))),true),true),true) )],[refute_0_286,refute_0_298]) ).
cnf(refute_0_300,plain,
ifeq(true,true,ifeq(theorem(implies(X_54,X_55)),true,theorem(implies(or(X_56,X_54),or(X_56,X_55))),true),true) = ifeq(theorem(implies(X_54,X_55)),true,theorem(implies(or(X_56,X_54),or(X_56,X_55))),true),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(ifeq(theorem(implies(X_54,X_55)),true,theorem(implies(or(X_56,X_54),or(X_56,X_55))),true))),bind(C,$fot(true))]]) ).
cnf(refute_0_301,plain,
( ifeq(true,true,ifeq(theorem(implies(X_54,X_55)),true,theorem(implies(or(X_56,X_54),or(X_56,X_55))),true),true) != ifeq(theorem(implies(X_54,X_55)),true,theorem(implies(or(X_56,X_54),or(X_56,X_55))),true)
| ifeq(true,true,ifeq(theorem(implies(X_54,X_55)),true,theorem(implies(or(X_56,X_54),or(X_56,X_55))),true),true) != true
| ifeq(theorem(implies(X_54,X_55)),true,theorem(implies(or(X_56,X_54),or(X_56,X_55))),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,ifeq(theorem(implies(X_54,X_55)),true,theorem(implies(or(X_56,X_54),or(X_56,X_55))),true),true),true) ),[0],$fot(ifeq(theorem(implies(X_54,X_55)),true,theorem(implies(or(X_56,X_54),or(X_56,X_55))),true))]]) ).
cnf(refute_0_302,plain,
( ifeq(true,true,ifeq(theorem(implies(X_54,X_55)),true,theorem(implies(or(X_56,X_54),or(X_56,X_55))),true),true) != true
| ifeq(theorem(implies(X_54,X_55)),true,theorem(implies(or(X_56,X_54),or(X_56,X_55))),true) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,ifeq(theorem(implies(X_54,X_55)),true,theorem(implies(or(X_56,X_54),or(X_56,X_55))),true),true),ifeq(theorem(implies(X_54,X_55)),true,theorem(implies(or(X_56,X_54),or(X_56,X_55))),true)) )],[refute_0_300,refute_0_301]) ).
cnf(refute_0_303,plain,
ifeq(theorem(implies(X_54,X_55)),true,theorem(implies(or(X_56,X_54),or(X_56,X_55))),true) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,ifeq(theorem(implies(X_54,X_55)),true,theorem(implies(or(X_56,X_54),or(X_56,X_55))),true),true),true) )],[refute_0_299,refute_0_302]) ).
cnf(refute_0_304,plain,
ifeq(theorem(implies(X_239,not(not(X_239)))),true,theorem(implies(or(X_241,X_239),or(X_241,not(not(X_239))))),true) = true,
inference(subst,[],[refute_0_303:[bind(X_54,$fot(X_239)),bind(X_55,$fot(not(not(X_239)))),bind(X_56,$fot(X_241))]]) ).
cnf(refute_0_305,plain,
theorem(implies(X_239,not(not(X_239)))) = true,
inference(subst,[],[refute_0_130:[bind(X_116,$fot(X_239))]]) ).
cnf(refute_0_306,plain,
( ifeq(theorem(implies(X_239,not(not(X_239)))),true,theorem(implies(or(X_241,X_239),or(X_241,not(not(X_239))))),true) != true
| theorem(implies(X_239,not(not(X_239)))) != true
| ifeq(true,true,theorem(implies(or(X_241,X_239),or(X_241,not(not(X_239))))),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(implies(X_239,not(not(X_239)))),true,theorem(implies(or(X_241,X_239),or(X_241,not(not(X_239))))),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_307,plain,
( ifeq(theorem(implies(X_239,not(not(X_239)))),true,theorem(implies(or(X_241,X_239),or(X_241,not(not(X_239))))),true) != true
| ifeq(true,true,theorem(implies(or(X_241,X_239),or(X_241,not(not(X_239))))),true) = true ),
inference(resolve,[$cnf( $equal(theorem(implies(X_239,not(not(X_239)))),true) )],[refute_0_305,refute_0_306]) ).
cnf(refute_0_308,plain,
ifeq(true,true,theorem(implies(or(X_241,X_239),or(X_241,not(not(X_239))))),true) = true,
inference(resolve,[$cnf( $equal(ifeq(theorem(implies(X_239,not(not(X_239)))),true,theorem(implies(or(X_241,X_239),or(X_241,not(not(X_239))))),true),true) )],[refute_0_304,refute_0_307]) ).
cnf(refute_0_309,plain,
ifeq(true,true,theorem(implies(or(X_241,X_239),or(X_241,not(not(X_239))))),true) = theorem(implies(or(X_241,X_239),or(X_241,not(not(X_239))))),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(theorem(implies(or(X_241,X_239),or(X_241,not(not(X_239))))))),bind(C,$fot(true))]]) ).
cnf(refute_0_310,plain,
( ifeq(true,true,theorem(implies(or(X_241,X_239),or(X_241,not(not(X_239))))),true) != theorem(implies(or(X_241,X_239),or(X_241,not(not(X_239)))))
| ifeq(true,true,theorem(implies(or(X_241,X_239),or(X_241,not(not(X_239))))),true) != true
| theorem(implies(or(X_241,X_239),or(X_241,not(not(X_239))))) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,theorem(implies(or(X_241,X_239),or(X_241,not(not(X_239))))),true),true) ),[0],$fot(theorem(implies(or(X_241,X_239),or(X_241,not(not(X_239))))))]]) ).
cnf(refute_0_311,plain,
( ifeq(true,true,theorem(implies(or(X_241,X_239),or(X_241,not(not(X_239))))),true) != true
| theorem(implies(or(X_241,X_239),or(X_241,not(not(X_239))))) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(implies(or(X_241,X_239),or(X_241,not(not(X_239))))),true),theorem(implies(or(X_241,X_239),or(X_241,not(not(X_239)))))) )],[refute_0_309,refute_0_310]) ).
cnf(refute_0_312,plain,
theorem(implies(or(X_241,X_239),or(X_241,not(not(X_239))))) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(implies(or(X_241,X_239),or(X_241,not(not(X_239))))),true),true) )],[refute_0_308,refute_0_311]) ).
cnf(refute_0_313,plain,
theorem(implies(or(X_245,X_244),or(X_245,not(not(X_244))))) = true,
inference(subst,[],[refute_0_312:[bind(X_239,$fot(X_244)),bind(X_241,$fot(X_245))]]) ).
cnf(refute_0_314,plain,
( ifeq(theorem(implies(or(X_245,X_244),or(X_245,not(not(X_244))))),true,ifeq(theorem(or(X_245,X_244)),true,theorem(or(X_245,not(not(X_244)))),true),true) != true
| theorem(implies(or(X_245,X_244),or(X_245,not(not(X_244))))) != true
| ifeq(true,true,ifeq(theorem(or(X_245,X_244)),true,theorem(or(X_245,not(not(X_244)))),true),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(implies(or(X_245,X_244),or(X_245,not(not(X_244))))),true,ifeq(theorem(or(X_245,X_244)),true,theorem(or(X_245,not(not(X_244)))),true),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_315,plain,
( ifeq(theorem(implies(or(X_245,X_244),or(X_245,not(not(X_244))))),true,ifeq(theorem(or(X_245,X_244)),true,theorem(or(X_245,not(not(X_244)))),true),true) != true
| ifeq(true,true,ifeq(theorem(or(X_245,X_244)),true,theorem(or(X_245,not(not(X_244)))),true),true) = true ),
inference(resolve,[$cnf( $equal(theorem(implies(or(X_245,X_244),or(X_245,not(not(X_244))))),true) )],[refute_0_313,refute_0_314]) ).
cnf(refute_0_316,plain,
ifeq(true,true,ifeq(theorem(or(X_245,X_244)),true,theorem(or(X_245,not(not(X_244)))),true),true) = true,
inference(resolve,[$cnf( $equal(ifeq(theorem(implies(or(X_245,X_244),or(X_245,not(not(X_244))))),true,ifeq(theorem(or(X_245,X_244)),true,theorem(or(X_245,not(not(X_244)))),true),true),true) )],[refute_0_285,refute_0_315]) ).
cnf(refute_0_317,plain,
ifeq(true,true,ifeq(theorem(or(X_245,X_244)),true,theorem(or(X_245,not(not(X_244)))),true),true) = ifeq(theorem(or(X_245,X_244)),true,theorem(or(X_245,not(not(X_244)))),true),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(ifeq(theorem(or(X_245,X_244)),true,theorem(or(X_245,not(not(X_244)))),true))),bind(C,$fot(true))]]) ).
cnf(refute_0_318,plain,
( ifeq(true,true,ifeq(theorem(or(X_245,X_244)),true,theorem(or(X_245,not(not(X_244)))),true),true) != ifeq(theorem(or(X_245,X_244)),true,theorem(or(X_245,not(not(X_244)))),true)
| ifeq(true,true,ifeq(theorem(or(X_245,X_244)),true,theorem(or(X_245,not(not(X_244)))),true),true) != true
| ifeq(theorem(or(X_245,X_244)),true,theorem(or(X_245,not(not(X_244)))),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,ifeq(theorem(or(X_245,X_244)),true,theorem(or(X_245,not(not(X_244)))),true),true),true) ),[0],$fot(ifeq(theorem(or(X_245,X_244)),true,theorem(or(X_245,not(not(X_244)))),true))]]) ).
cnf(refute_0_319,plain,
( ifeq(true,true,ifeq(theorem(or(X_245,X_244)),true,theorem(or(X_245,not(not(X_244)))),true),true) != true
| ifeq(theorem(or(X_245,X_244)),true,theorem(or(X_245,not(not(X_244)))),true) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,ifeq(theorem(or(X_245,X_244)),true,theorem(or(X_245,not(not(X_244)))),true),true),ifeq(theorem(or(X_245,X_244)),true,theorem(or(X_245,not(not(X_244)))),true)) )],[refute_0_317,refute_0_318]) ).
cnf(refute_0_320,plain,
ifeq(theorem(or(X_245,X_244)),true,theorem(or(X_245,not(not(X_244)))),true) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,ifeq(theorem(or(X_245,X_244)),true,theorem(or(X_245,not(not(X_244)))),true),true),true) )],[refute_0_316,refute_0_319]) ).
cnf(refute_0_321,plain,
ifeq(theorem(or(X_997,not(X_997))),true,theorem(or(X_997,not(not(not(X_997))))),true) = true,
inference(subst,[],[refute_0_320:[bind(X_244,$fot(not(X_997))),bind(X_245,$fot(X_997))]]) ).
cnf(refute_0_322,plain,
ifeq(theorem(implies(implies(X_31,X_32),or(X_32,not(X_31)))),true,ifeq(theorem(implies(X_31,X_32)),true,theorem(or(X_32,not(X_31))),true),true) = true,
inference(subst,[],[rule_2:[bind(X,$fot(or(X_32,not(X_31)))),bind(Y,$fot(implies(X_31,X_32)))]]) ).
cnf(refute_0_323,plain,
theorem(implies(or(not(X_16),X_7),or(X_7,not(X_16)))) = true,
inference(subst,[],[refute_0_10:[bind(X_6,$fot(not(X_16)))]]) ).
cnf(refute_0_324,plain,
implies(X_16,X_7) = or(not(X_16),X_7),
inference(subst,[],[implies_definition:[bind(X,$fot(X_16)),bind(Y,$fot(X_7))]]) ).
cnf(refute_0_325,plain,
( implies(X_16,X_7) != or(not(X_16),X_7)
| or(not(X_16),X_7) = implies(X_16,X_7) ),
inference(subst,[],[refute_0_15:[bind(X0,$fot(implies(X_16,X_7))),bind(Y0,$fot(or(not(X_16),X_7)))]]) ).
cnf(refute_0_326,plain,
or(not(X_16),X_7) = implies(X_16,X_7),
inference(resolve,[$cnf( $equal(implies(X_16,X_7),or(not(X_16),X_7)) )],[refute_0_324,refute_0_325]) ).
cnf(refute_0_327,plain,
( or(not(X_16),X_7) != implies(X_16,X_7)
| theorem(implies(or(not(X_16),X_7),or(X_7,not(X_16)))) != true
| theorem(implies(implies(X_16,X_7),or(X_7,not(X_16)))) = true ),
introduced(tautology,[equality,[$cnf( $equal(theorem(implies(or(not(X_16),X_7),or(X_7,not(X_16)))),true) ),[0,0,0],$fot(implies(X_16,X_7))]]) ).
cnf(refute_0_328,plain,
( theorem(implies(or(not(X_16),X_7),or(X_7,not(X_16)))) != true
| theorem(implies(implies(X_16,X_7),or(X_7,not(X_16)))) = true ),
inference(resolve,[$cnf( $equal(or(not(X_16),X_7),implies(X_16,X_7)) )],[refute_0_326,refute_0_327]) ).
cnf(refute_0_329,plain,
theorem(implies(implies(X_16,X_7),or(X_7,not(X_16)))) = true,
inference(resolve,[$cnf( $equal(theorem(implies(or(not(X_16),X_7),or(X_7,not(X_16)))),true) )],[refute_0_323,refute_0_328]) ).
cnf(refute_0_330,plain,
theorem(implies(implies(X_31,X_32),or(X_32,not(X_31)))) = true,
inference(subst,[],[refute_0_329:[bind(X_16,$fot(X_31)),bind(X_7,$fot(X_32))]]) ).
cnf(refute_0_331,plain,
( ifeq(theorem(implies(implies(X_31,X_32),or(X_32,not(X_31)))),true,ifeq(theorem(implies(X_31,X_32)),true,theorem(or(X_32,not(X_31))),true),true) != true
| theorem(implies(implies(X_31,X_32),or(X_32,not(X_31)))) != true
| ifeq(true,true,ifeq(theorem(implies(X_31,X_32)),true,theorem(or(X_32,not(X_31))),true),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(implies(implies(X_31,X_32),or(X_32,not(X_31)))),true,ifeq(theorem(implies(X_31,X_32)),true,theorem(or(X_32,not(X_31))),true),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_332,plain,
( ifeq(theorem(implies(implies(X_31,X_32),or(X_32,not(X_31)))),true,ifeq(theorem(implies(X_31,X_32)),true,theorem(or(X_32,not(X_31))),true),true) != true
| ifeq(true,true,ifeq(theorem(implies(X_31,X_32)),true,theorem(or(X_32,not(X_31))),true),true) = true ),
inference(resolve,[$cnf( $equal(theorem(implies(implies(X_31,X_32),or(X_32,not(X_31)))),true) )],[refute_0_330,refute_0_331]) ).
cnf(refute_0_333,plain,
ifeq(true,true,ifeq(theorem(implies(X_31,X_32)),true,theorem(or(X_32,not(X_31))),true),true) = true,
inference(resolve,[$cnf( $equal(ifeq(theorem(implies(implies(X_31,X_32),or(X_32,not(X_31)))),true,ifeq(theorem(implies(X_31,X_32)),true,theorem(or(X_32,not(X_31))),true),true),true) )],[refute_0_322,refute_0_332]) ).
cnf(refute_0_334,plain,
ifeq(true,true,ifeq(theorem(implies(X_31,X_32)),true,theorem(or(X_32,not(X_31))),true),true) = ifeq(theorem(implies(X_31,X_32)),true,theorem(or(X_32,not(X_31))),true),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(ifeq(theorem(implies(X_31,X_32)),true,theorem(or(X_32,not(X_31))),true))),bind(C,$fot(true))]]) ).
cnf(refute_0_335,plain,
( ifeq(true,true,ifeq(theorem(implies(X_31,X_32)),true,theorem(or(X_32,not(X_31))),true),true) != ifeq(theorem(implies(X_31,X_32)),true,theorem(or(X_32,not(X_31))),true)
| ifeq(true,true,ifeq(theorem(implies(X_31,X_32)),true,theorem(or(X_32,not(X_31))),true),true) != true
| ifeq(theorem(implies(X_31,X_32)),true,theorem(or(X_32,not(X_31))),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,ifeq(theorem(implies(X_31,X_32)),true,theorem(or(X_32,not(X_31))),true),true),true) ),[0],$fot(ifeq(theorem(implies(X_31,X_32)),true,theorem(or(X_32,not(X_31))),true))]]) ).
cnf(refute_0_336,plain,
( ifeq(true,true,ifeq(theorem(implies(X_31,X_32)),true,theorem(or(X_32,not(X_31))),true),true) != true
| ifeq(theorem(implies(X_31,X_32)),true,theorem(or(X_32,not(X_31))),true) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,ifeq(theorem(implies(X_31,X_32)),true,theorem(or(X_32,not(X_31))),true),true),ifeq(theorem(implies(X_31,X_32)),true,theorem(or(X_32,not(X_31))),true)) )],[refute_0_334,refute_0_335]) ).
cnf(refute_0_337,plain,
ifeq(theorem(implies(X_31,X_32)),true,theorem(or(X_32,not(X_31))),true) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,ifeq(theorem(implies(X_31,X_32)),true,theorem(or(X_32,not(X_31))),true),true),true) )],[refute_0_333,refute_0_336]) ).
cnf(refute_0_338,plain,
ifeq(theorem(implies(X_32,X_32)),true,theorem(or(X_32,not(X_32))),true) = true,
inference(subst,[],[refute_0_337:[bind(X_31,$fot(X_32))]]) ).
cnf(refute_0_339,plain,
theorem(implies(X_32,X_32)) = true,
inference(subst,[],[refute_0_122:[bind(X_149,$fot(X_32))]]) ).
cnf(refute_0_340,plain,
( ifeq(theorem(implies(X_32,X_32)),true,theorem(or(X_32,not(X_32))),true) != true
| theorem(implies(X_32,X_32)) != true
| ifeq(true,true,theorem(or(X_32,not(X_32))),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(implies(X_32,X_32)),true,theorem(or(X_32,not(X_32))),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_341,plain,
( ifeq(theorem(implies(X_32,X_32)),true,theorem(or(X_32,not(X_32))),true) != true
| ifeq(true,true,theorem(or(X_32,not(X_32))),true) = true ),
inference(resolve,[$cnf( $equal(theorem(implies(X_32,X_32)),true) )],[refute_0_339,refute_0_340]) ).
cnf(refute_0_342,plain,
ifeq(true,true,theorem(or(X_32,not(X_32))),true) = true,
inference(resolve,[$cnf( $equal(ifeq(theorem(implies(X_32,X_32)),true,theorem(or(X_32,not(X_32))),true),true) )],[refute_0_338,refute_0_341]) ).
cnf(refute_0_343,plain,
ifeq(true,true,theorem(or(X_32,not(X_32))),true) = theorem(or(X_32,not(X_32))),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(theorem(or(X_32,not(X_32))))),bind(C,$fot(true))]]) ).
cnf(refute_0_344,plain,
( ifeq(true,true,theorem(or(X_32,not(X_32))),true) != theorem(or(X_32,not(X_32)))
| ifeq(true,true,theorem(or(X_32,not(X_32))),true) != true
| theorem(or(X_32,not(X_32))) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,theorem(or(X_32,not(X_32))),true),true) ),[0],$fot(theorem(or(X_32,not(X_32))))]]) ).
cnf(refute_0_345,plain,
( ifeq(true,true,theorem(or(X_32,not(X_32))),true) != true
| theorem(or(X_32,not(X_32))) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(or(X_32,not(X_32))),true),theorem(or(X_32,not(X_32)))) )],[refute_0_343,refute_0_344]) ).
cnf(refute_0_346,plain,
theorem(or(X_32,not(X_32))) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(or(X_32,not(X_32))),true),true) )],[refute_0_342,refute_0_345]) ).
cnf(refute_0_347,plain,
theorem(or(X_997,not(X_997))) = true,
inference(subst,[],[refute_0_346:[bind(X_32,$fot(X_997))]]) ).
cnf(refute_0_348,plain,
( ifeq(theorem(or(X_997,not(X_997))),true,theorem(or(X_997,not(not(not(X_997))))),true) != true
| theorem(or(X_997,not(X_997))) != true
| ifeq(true,true,theorem(or(X_997,not(not(not(X_997))))),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(or(X_997,not(X_997))),true,theorem(or(X_997,not(not(not(X_997))))),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_349,plain,
( ifeq(theorem(or(X_997,not(X_997))),true,theorem(or(X_997,not(not(not(X_997))))),true) != true
| ifeq(true,true,theorem(or(X_997,not(not(not(X_997))))),true) = true ),
inference(resolve,[$cnf( $equal(theorem(or(X_997,not(X_997))),true) )],[refute_0_347,refute_0_348]) ).
cnf(refute_0_350,plain,
ifeq(true,true,theorem(or(X_997,not(not(not(X_997))))),true) = true,
inference(resolve,[$cnf( $equal(ifeq(theorem(or(X_997,not(X_997))),true,theorem(or(X_997,not(not(not(X_997))))),true),true) )],[refute_0_321,refute_0_349]) ).
cnf(refute_0_351,plain,
ifeq(true,true,theorem(or(X_997,not(not(not(X_997))))),true) = theorem(or(X_997,not(not(not(X_997))))),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(theorem(or(X_997,not(not(not(X_997))))))),bind(C,$fot(true))]]) ).
cnf(refute_0_352,plain,
( ifeq(true,true,theorem(or(X_997,not(not(not(X_997))))),true) != theorem(or(X_997,not(not(not(X_997)))))
| ifeq(true,true,theorem(or(X_997,not(not(not(X_997))))),true) != true
| theorem(or(X_997,not(not(not(X_997))))) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,theorem(or(X_997,not(not(not(X_997))))),true),true) ),[0],$fot(theorem(or(X_997,not(not(not(X_997))))))]]) ).
cnf(refute_0_353,plain,
( ifeq(true,true,theorem(or(X_997,not(not(not(X_997))))),true) != true
| theorem(or(X_997,not(not(not(X_997))))) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(or(X_997,not(not(not(X_997))))),true),theorem(or(X_997,not(not(not(X_997)))))) )],[refute_0_351,refute_0_352]) ).
cnf(refute_0_354,plain,
theorem(or(X_997,not(not(not(X_997))))) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(or(X_997,not(not(not(X_997))))),true),true) )],[refute_0_350,refute_0_353]) ).
cnf(refute_0_355,plain,
theorem(or(X_6,not(not(not(X_6))))) = true,
inference(subst,[],[refute_0_354:[bind(X_997,$fot(X_6))]]) ).
cnf(refute_0_356,plain,
( ifeq(theorem(or(X_6,not(not(not(X_6))))),true,theorem(or(not(not(not(X_6))),X_6)),true) != true
| theorem(or(X_6,not(not(not(X_6))))) != true
| ifeq(true,true,theorem(or(not(not(not(X_6))),X_6)),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(or(X_6,not(not(not(X_6))))),true,theorem(or(not(not(not(X_6))),X_6)),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_357,plain,
( ifeq(theorem(or(X_6,not(not(not(X_6))))),true,theorem(or(not(not(not(X_6))),X_6)),true) != true
| ifeq(true,true,theorem(or(not(not(not(X_6))),X_6)),true) = true ),
inference(resolve,[$cnf( $equal(theorem(or(X_6,not(not(not(X_6))))),true) )],[refute_0_355,refute_0_356]) ).
cnf(refute_0_358,plain,
ifeq(true,true,theorem(or(not(not(not(X_6))),X_6)),true) = true,
inference(resolve,[$cnf( $equal(ifeq(theorem(or(X_6,not(not(not(X_6))))),true,theorem(or(not(not(not(X_6))),X_6)),true),true) )],[refute_0_284,refute_0_357]) ).
cnf(refute_0_359,plain,
or(not(not(not(X_6))),X_6) = implies(not(not(X_6)),X_6),
inference(subst,[],[refute_0_86:[bind(X,$fot(not(not(X_6)))),bind(Y,$fot(X_6))]]) ).
cnf(refute_0_360,plain,
theorem(or(not(not(not(X_6))),X_6)) = theorem(or(not(not(not(X_6))),X_6)),
introduced(tautology,[refl,[$fot(theorem(or(not(not(not(X_6))),X_6)))]]) ).
cnf(refute_0_361,plain,
( or(not(not(not(X_6))),X_6) != implies(not(not(X_6)),X_6)
| theorem(or(not(not(not(X_6))),X_6)) != theorem(or(not(not(not(X_6))),X_6))
| theorem(or(not(not(not(X_6))),X_6)) = theorem(implies(not(not(X_6)),X_6)) ),
introduced(tautology,[equality,[$cnf( $equal(theorem(or(not(not(not(X_6))),X_6)),theorem(or(not(not(not(X_6))),X_6))) ),[1,0],$fot(implies(not(not(X_6)),X_6))]]) ).
cnf(refute_0_362,plain,
( or(not(not(not(X_6))),X_6) != implies(not(not(X_6)),X_6)
| theorem(or(not(not(not(X_6))),X_6)) = theorem(implies(not(not(X_6)),X_6)) ),
inference(resolve,[$cnf( $equal(theorem(or(not(not(not(X_6))),X_6)),theorem(or(not(not(not(X_6))),X_6))) )],[refute_0_360,refute_0_361]) ).
cnf(refute_0_363,plain,
theorem(or(not(not(not(X_6))),X_6)) = theorem(implies(not(not(X_6)),X_6)),
inference(resolve,[$cnf( $equal(or(not(not(not(X_6))),X_6),implies(not(not(X_6)),X_6)) )],[refute_0_359,refute_0_362]) ).
cnf(refute_0_364,plain,
ifeq(true,true,theorem(or(not(not(not(X_6))),X_6)),true) = theorem(or(not(not(not(X_6))),X_6)),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(theorem(or(not(not(not(X_6))),X_6)))),bind(C,$fot(true))]]) ).
cnf(refute_0_365,plain,
( ifeq(true,true,theorem(or(not(not(not(X_6))),X_6)),true) != theorem(or(not(not(not(X_6))),X_6))
| theorem(or(not(not(not(X_6))),X_6)) != theorem(implies(not(not(X_6)),X_6))
| ifeq(true,true,theorem(or(not(not(not(X_6))),X_6)),true) = theorem(implies(not(not(X_6)),X_6)) ),
inference(subst,[],[refute_0_164:[bind(X0,$fot(ifeq(true,true,theorem(or(not(not(not(X_6))),X_6)),true))),bind(Y0,$fot(theorem(or(not(not(not(X_6))),X_6)))),bind(Z,$fot(theorem(implies(not(not(X_6)),X_6))))]]) ).
cnf(refute_0_366,plain,
( theorem(or(not(not(not(X_6))),X_6)) != theorem(implies(not(not(X_6)),X_6))
| ifeq(true,true,theorem(or(not(not(not(X_6))),X_6)),true) = theorem(implies(not(not(X_6)),X_6)) ),
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(or(not(not(not(X_6))),X_6)),true),theorem(or(not(not(not(X_6))),X_6))) )],[refute_0_364,refute_0_365]) ).
cnf(refute_0_367,plain,
ifeq(true,true,theorem(or(not(not(not(X_6))),X_6)),true) = theorem(implies(not(not(X_6)),X_6)),
inference(resolve,[$cnf( $equal(theorem(or(not(not(not(X_6))),X_6)),theorem(implies(not(not(X_6)),X_6))) )],[refute_0_363,refute_0_366]) ).
cnf(refute_0_368,plain,
( ifeq(true,true,theorem(or(not(not(not(X_6))),X_6)),true) != theorem(implies(not(not(X_6)),X_6))
| ifeq(true,true,theorem(or(not(not(not(X_6))),X_6)),true) != true
| theorem(implies(not(not(X_6)),X_6)) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,theorem(or(not(not(not(X_6))),X_6)),true),true) ),[0],$fot(theorem(implies(not(not(X_6)),X_6)))]]) ).
cnf(refute_0_369,plain,
( ifeq(true,true,theorem(or(not(not(not(X_6))),X_6)),true) != true
| theorem(implies(not(not(X_6)),X_6)) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(or(not(not(not(X_6))),X_6)),true),theorem(implies(not(not(X_6)),X_6))) )],[refute_0_367,refute_0_368]) ).
cnf(refute_0_370,plain,
theorem(implies(not(not(X_6)),X_6)) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(or(not(not(not(X_6))),X_6)),true),true) )],[refute_0_358,refute_0_369]) ).
cnf(refute_0_371,plain,
theorem(implies(not(not(X_1958)),X_1958)) = true,
inference(subst,[],[refute_0_370:[bind(X_6,$fot(X_1958))]]) ).
cnf(refute_0_372,plain,
( ifeq(theorem(implies(not(not(X_1958)),X_1958)),true,theorem(or(equivalent(X_1958,not(not(X_1958))),and(X_1958,not(X_1958)))),true) != true
| theorem(implies(not(not(X_1958)),X_1958)) != true
| ifeq(true,true,theorem(or(equivalent(X_1958,not(not(X_1958))),and(X_1958,not(X_1958)))),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(implies(not(not(X_1958)),X_1958)),true,theorem(or(equivalent(X_1958,not(not(X_1958))),and(X_1958,not(X_1958)))),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_373,plain,
( ifeq(theorem(implies(not(not(X_1958)),X_1958)),true,theorem(or(equivalent(X_1958,not(not(X_1958))),and(X_1958,not(X_1958)))),true) != true
| ifeq(true,true,theorem(or(equivalent(X_1958,not(not(X_1958))),and(X_1958,not(X_1958)))),true) = true ),
inference(resolve,[$cnf( $equal(theorem(implies(not(not(X_1958)),X_1958)),true) )],[refute_0_371,refute_0_372]) ).
cnf(refute_0_374,plain,
ifeq(true,true,theorem(or(equivalent(X_1958,not(not(X_1958))),and(X_1958,not(X_1958)))),true) = true,
inference(resolve,[$cnf( $equal(ifeq(theorem(implies(not(not(X_1958)),X_1958)),true,theorem(or(equivalent(X_1958,not(not(X_1958))),and(X_1958,not(X_1958)))),true),true) )],[refute_0_283,refute_0_373]) ).
cnf(refute_0_375,plain,
ifeq(true,true,theorem(or(equivalent(X_1958,not(not(X_1958))),and(X_1958,not(X_1958)))),true) = theorem(or(equivalent(X_1958,not(not(X_1958))),and(X_1958,not(X_1958)))),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(theorem(or(equivalent(X_1958,not(not(X_1958))),and(X_1958,not(X_1958)))))),bind(C,$fot(true))]]) ).
cnf(refute_0_376,plain,
( ifeq(true,true,theorem(or(equivalent(X_1958,not(not(X_1958))),and(X_1958,not(X_1958)))),true) != theorem(or(equivalent(X_1958,not(not(X_1958))),and(X_1958,not(X_1958))))
| ifeq(true,true,theorem(or(equivalent(X_1958,not(not(X_1958))),and(X_1958,not(X_1958)))),true) != true
| theorem(or(equivalent(X_1958,not(not(X_1958))),and(X_1958,not(X_1958)))) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,theorem(or(equivalent(X_1958,not(not(X_1958))),and(X_1958,not(X_1958)))),true),true) ),[0],$fot(theorem(or(equivalent(X_1958,not(not(X_1958))),and(X_1958,not(X_1958)))))]]) ).
cnf(refute_0_377,plain,
( ifeq(true,true,theorem(or(equivalent(X_1958,not(not(X_1958))),and(X_1958,not(X_1958)))),true) != true
| theorem(or(equivalent(X_1958,not(not(X_1958))),and(X_1958,not(X_1958)))) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(or(equivalent(X_1958,not(not(X_1958))),and(X_1958,not(X_1958)))),true),theorem(or(equivalent(X_1958,not(not(X_1958))),and(X_1958,not(X_1958))))) )],[refute_0_375,refute_0_376]) ).
cnf(refute_0_378,plain,
theorem(or(equivalent(X_1958,not(not(X_1958))),and(X_1958,not(X_1958)))) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(or(equivalent(X_1958,not(not(X_1958))),and(X_1958,not(X_1958)))),true),true) )],[refute_0_374,refute_0_377]) ).
cnf(refute_0_379,plain,
theorem(or(equivalent(X_1959,not(not(X_1959))),and(X_1959,not(X_1959)))) = true,
inference(subst,[],[refute_0_378:[bind(X_1958,$fot(X_1959))]]) ).
cnf(refute_0_380,plain,
( ifeq(theorem(or(equivalent(X_1959,not(not(X_1959))),and(X_1959,not(X_1959)))),true,theorem(or(and(X_1959,not(X_1959)),equivalent(X_1959,not(not(X_1959))))),true) != true
| theorem(or(equivalent(X_1959,not(not(X_1959))),and(X_1959,not(X_1959)))) != true
| ifeq(true,true,theorem(or(and(X_1959,not(X_1959)),equivalent(X_1959,not(not(X_1959))))),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(or(equivalent(X_1959,not(not(X_1959))),and(X_1959,not(X_1959)))),true,theorem(or(and(X_1959,not(X_1959)),equivalent(X_1959,not(not(X_1959))))),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_381,plain,
( ifeq(theorem(or(equivalent(X_1959,not(not(X_1959))),and(X_1959,not(X_1959)))),true,theorem(or(and(X_1959,not(X_1959)),equivalent(X_1959,not(not(X_1959))))),true) != true
| ifeq(true,true,theorem(or(and(X_1959,not(X_1959)),equivalent(X_1959,not(not(X_1959))))),true) = true ),
inference(resolve,[$cnf( $equal(theorem(or(equivalent(X_1959,not(not(X_1959))),and(X_1959,not(X_1959)))),true) )],[refute_0_379,refute_0_380]) ).
cnf(refute_0_382,plain,
ifeq(true,true,theorem(or(and(X_1959,not(X_1959)),equivalent(X_1959,not(not(X_1959))))),true) = true,
inference(resolve,[$cnf( $equal(ifeq(theorem(or(equivalent(X_1959,not(not(X_1959))),and(X_1959,not(X_1959)))),true,theorem(or(and(X_1959,not(X_1959)),equivalent(X_1959,not(not(X_1959))))),true),true) )],[refute_0_180,refute_0_381]) ).
cnf(refute_0_383,plain,
ifeq(true,true,theorem(or(and(X_1959,not(X_1959)),equivalent(X_1959,not(not(X_1959))))),true) = theorem(or(and(X_1959,not(X_1959)),equivalent(X_1959,not(not(X_1959))))),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(theorem(or(and(X_1959,not(X_1959)),equivalent(X_1959,not(not(X_1959))))))),bind(C,$fot(true))]]) ).
cnf(refute_0_384,plain,
( ifeq(true,true,theorem(or(and(X_1959,not(X_1959)),equivalent(X_1959,not(not(X_1959))))),true) != theorem(or(and(X_1959,not(X_1959)),equivalent(X_1959,not(not(X_1959)))))
| ifeq(true,true,theorem(or(and(X_1959,not(X_1959)),equivalent(X_1959,not(not(X_1959))))),true) != true
| theorem(or(and(X_1959,not(X_1959)),equivalent(X_1959,not(not(X_1959))))) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,theorem(or(and(X_1959,not(X_1959)),equivalent(X_1959,not(not(X_1959))))),true),true) ),[0],$fot(theorem(or(and(X_1959,not(X_1959)),equivalent(X_1959,not(not(X_1959))))))]]) ).
cnf(refute_0_385,plain,
( ifeq(true,true,theorem(or(and(X_1959,not(X_1959)),equivalent(X_1959,not(not(X_1959))))),true) != true
| theorem(or(and(X_1959,not(X_1959)),equivalent(X_1959,not(not(X_1959))))) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(or(and(X_1959,not(X_1959)),equivalent(X_1959,not(not(X_1959))))),true),theorem(or(and(X_1959,not(X_1959)),equivalent(X_1959,not(not(X_1959)))))) )],[refute_0_383,refute_0_384]) ).
cnf(refute_0_386,plain,
theorem(or(and(X_1959,not(X_1959)),equivalent(X_1959,not(not(X_1959))))) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(or(and(X_1959,not(X_1959)),equivalent(X_1959,not(not(X_1959))))),true),true) )],[refute_0_382,refute_0_385]) ).
cnf(refute_0_387,plain,
theorem(or(and(X_2323,not(X_2323)),equivalent(X_2323,not(not(X_2323))))) = true,
inference(subst,[],[refute_0_386:[bind(X_1959,$fot(X_2323))]]) ).
cnf(refute_0_388,plain,
( ifeq(theorem(or(and(X_2323,not(X_2323)),equivalent(X_2323,not(not(X_2323))))),true,theorem(equivalent(X_2323,not(not(X_2323)))),true) != true
| theorem(or(and(X_2323,not(X_2323)),equivalent(X_2323,not(not(X_2323))))) != true
| ifeq(true,true,theorem(equivalent(X_2323,not(not(X_2323)))),true) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(theorem(or(and(X_2323,not(X_2323)),equivalent(X_2323,not(not(X_2323))))),true,theorem(equivalent(X_2323,not(not(X_2323)))),true),true) ),[0,0],$fot(true)]]) ).
cnf(refute_0_389,plain,
( ifeq(theorem(or(and(X_2323,not(X_2323)),equivalent(X_2323,not(not(X_2323))))),true,theorem(equivalent(X_2323,not(not(X_2323)))),true) != true
| ifeq(true,true,theorem(equivalent(X_2323,not(not(X_2323)))),true) = true ),
inference(resolve,[$cnf( $equal(theorem(or(and(X_2323,not(X_2323)),equivalent(X_2323,not(not(X_2323))))),true) )],[refute_0_387,refute_0_388]) ).
cnf(refute_0_390,plain,
ifeq(true,true,theorem(equivalent(X_2323,not(not(X_2323)))),true) = true,
inference(resolve,[$cnf( $equal(ifeq(theorem(or(and(X_2323,not(X_2323)),equivalent(X_2323,not(not(X_2323))))),true,theorem(equivalent(X_2323,not(not(X_2323)))),true),true) )],[refute_0_171,refute_0_389]) ).
cnf(refute_0_391,plain,
ifeq(true,true,theorem(equivalent(X_2323,not(not(X_2323)))),true) = theorem(equivalent(X_2323,not(not(X_2323)))),
inference(subst,[],[ifeq_axiom:[bind(A,$fot(true)),bind(B,$fot(theorem(equivalent(X_2323,not(not(X_2323)))))),bind(C,$fot(true))]]) ).
cnf(refute_0_392,plain,
( ifeq(true,true,theorem(equivalent(X_2323,not(not(X_2323)))),true) != theorem(equivalent(X_2323,not(not(X_2323))))
| ifeq(true,true,theorem(equivalent(X_2323,not(not(X_2323)))),true) != true
| theorem(equivalent(X_2323,not(not(X_2323)))) = true ),
introduced(tautology,[equality,[$cnf( $equal(ifeq(true,true,theorem(equivalent(X_2323,not(not(X_2323)))),true),true) ),[0],$fot(theorem(equivalent(X_2323,not(not(X_2323)))))]]) ).
cnf(refute_0_393,plain,
( ifeq(true,true,theorem(equivalent(X_2323,not(not(X_2323)))),true) != true
| theorem(equivalent(X_2323,not(not(X_2323)))) = true ),
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(equivalent(X_2323,not(not(X_2323)))),true),theorem(equivalent(X_2323,not(not(X_2323))))) )],[refute_0_391,refute_0_392]) ).
cnf(refute_0_394,plain,
theorem(equivalent(X_2323,not(not(X_2323)))) = true,
inference(resolve,[$cnf( $equal(ifeq(true,true,theorem(equivalent(X_2323,not(not(X_2323)))),true),true) )],[refute_0_390,refute_0_393]) ).
cnf(refute_0_395,plain,
theorem(equivalent(p,not(not(p)))) = true,
inference(subst,[],[refute_0_394:[bind(X_2323,$fot(p))]]) ).
cnf(refute_0_396,plain,
( theorem(equivalent(p,not(not(p)))) != true
| true != true
| theorem(equivalent(p,not(not(p)))) = true ),
introduced(tautology,[equality,[$cnf( ~ $equal(theorem(equivalent(p,not(not(p)))),true) ),[0],$fot(true)]]) ).
cnf(refute_0_397,plain,
( true != true
| theorem(equivalent(p,not(not(p)))) = true ),
inference(resolve,[$cnf( $equal(theorem(equivalent(p,not(not(p)))),true) )],[refute_0_395,refute_0_396]) ).
cnf(refute_0_398,plain,
true != true,
inference(resolve,[$cnf( $equal(theorem(equivalent(p,not(not(p)))),true) )],[refute_0_397,prove_this]) ).
cnf(refute_0_399,plain,
true = true,
introduced(tautology,[refl,[$fot(true)]]) ).
cnf(refute_0_400,plain,
$false,
inference(resolve,[$cnf( $equal(true,true) )],[refute_0_399,refute_0_398]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL265-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : metis --show proof --show saturation %s
% 0.10/0.36 % Computer : n018.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 5 00:53:03 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 49.14/49.41 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 49.14/49.41
% 49.14/49.41 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 49.44/49.76
%------------------------------------------------------------------------------