%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : LCL382+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n013.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:33 PM UTC 2026
% Result : Theorem 114.25s 114.52s
% Output : CNFRefutation 114.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 62
% Number of leaves : 5
% Syntax : Number of formulae : 205 ( 123 unt; 0 def)
% Number of atoms : 306 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 203 ( 102 ~; 99 |; 1 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 500 ( 95 sgn 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(condensed_detachment,axiom,
! [X,Y] :
( ( is_a_theorem(implies(X,Y))
& is_a_theorem(X) )
=> is_a_theorem(Y) ) ).
fof(cn_1,axiom,
! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) ).
fof(cn_2,axiom,
! [X] : is_a_theorem(implies(implies(not(X),X),X)) ).
fof(cn_3,axiom,
! [X,Y] : is_a_theorem(implies(X,implies(not(X),Y))) ).
fof(prove_cn_43,conjecture,
is_a_theorem(implies(implies(x,y),implies(implies(y,not(x)),not(x)))) ).
fof(subgoal_0,plain,
is_a_theorem(implies(implies(x,y),implies(implies(y,not(x)),not(x)))),
inference(strip,[],[prove_cn_43]) ).
fof(negate_0_0,plain,
~ is_a_theorem(implies(implies(x,y),implies(implies(y,not(x)),not(x)))),
inference(negate,[],[subgoal_0]) ).
fof(normalize_0_0,plain,
~ is_a_theorem(implies(implies(x,y),implies(implies(y,not(x)),not(x)))),
inference(canonicalize,[],[negate_0_0]) ).
fof(normalize_0_1,plain,
! [X,Y] :
( ~ is_a_theorem(X)
| ~ is_a_theorem(implies(X,Y))
| is_a_theorem(Y) ),
inference(canonicalize,[],[condensed_detachment]) ).
fof(normalize_0_2,plain,
! [X,Y] :
( ~ is_a_theorem(X)
| ~ is_a_theorem(implies(X,Y))
| is_a_theorem(Y) ),
inference(specialize,[],[normalize_0_1]) ).
fof(normalize_0_3,plain,
! [X] : is_a_theorem(implies(implies(not(X),X),X)),
inference(canonicalize,[],[cn_2]) ).
fof(normalize_0_4,plain,
! [X] : is_a_theorem(implies(implies(not(X),X),X)),
inference(specialize,[],[normalize_0_3]) ).
fof(normalize_0_5,plain,
! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))),
inference(canonicalize,[],[cn_1]) ).
fof(normalize_0_6,plain,
! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))),
inference(specialize,[],[normalize_0_5]) ).
fof(normalize_0_7,plain,
! [X,Y] : is_a_theorem(implies(X,implies(not(X),Y))),
inference(canonicalize,[],[cn_3]) ).
fof(normalize_0_8,plain,
! [X,Y] : is_a_theorem(implies(X,implies(not(X),Y))),
inference(specialize,[],[normalize_0_7]) ).
cnf(refute_0_0,plain,
~ is_a_theorem(implies(implies(x,y),implies(implies(y,not(x)),not(x)))),
inference(canonicalize,[],[normalize_0_0]) ).
cnf(refute_0_1,plain,
( ~ is_a_theorem(X)
| ~ is_a_theorem(implies(X,Y))
| is_a_theorem(Y) ),
inference(canonicalize,[],[normalize_0_2]) ).
cnf(refute_0_2,plain,
( ~ is_a_theorem(implies(X_2106,implies(not(X_2107),X_2107)))
| ~ is_a_theorem(implies(implies(X_2106,implies(not(X_2107),X_2107)),implies(X_2106,X_2107)))
| is_a_theorem(implies(X_2106,X_2107)) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(implies(X_2106,implies(not(X_2107),X_2107)))),bind(Y,$fot(implies(X_2106,X_2107)))]]) ).
cnf(refute_0_3,plain,
( ~ is_a_theorem(implies(implies(implies(not(not(X_361)),X_362),X_361),X_361))
| ~ is_a_theorem(implies(implies(not(not(X_361)),X_362),X_361))
| is_a_theorem(X_361) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(implies(implies(not(not(X_361)),X_362),X_361))),bind(Y,$fot(X_361))]]) ).
cnf(refute_0_4,plain,
is_a_theorem(implies(implies(not(X),X),X)),
inference(canonicalize,[],[normalize_0_4]) ).
cnf(refute_0_5,plain,
is_a_theorem(implies(implies(not(X_357),X_357),X_357)),
inference(subst,[],[refute_0_4:[bind(X,$fot(X_357))]]) ).
cnf(refute_0_6,plain,
( ~ is_a_theorem(implies(implies(X_154,X_155),X_152))
| ~ is_a_theorem(implies(implies(implies(X_154,X_155),X_152),implies(implies(implies(not(X_154),X_153),X_155),X_152)))
| is_a_theorem(implies(implies(implies(not(X_154),X_153),X_155),X_152)) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(implies(implies(X_154,X_155),X_152))),bind(Y,$fot(implies(implies(implies(not(X_154),X_153),X_155),X_152)))]]) ).
cnf(refute_0_7,plain,
is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))),
inference(canonicalize,[],[normalize_0_6]) ).
cnf(refute_0_8,plain,
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))))
| is_a_theorem(implies(implies(Y,Z),implies(X,Z))) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(implies(X,Y))),bind(Y,$fot(implies(implies(Y,Z),implies(X,Z))))]]) ).
cnf(refute_0_9,plain,
( ~ is_a_theorem(implies(X,Y))
| is_a_theorem(implies(implies(Y,Z),implies(X,Z))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )],[refute_0_7,refute_0_8]) ).
cnf(refute_0_10,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_33),X_32),X_34),implies(X_33,X_34)))
| is_a_theorem(implies(implies(implies(X_33,X_34),Z),implies(implies(implies(not(X_33),X_32),X_34),Z))) ),
inference(subst,[],[refute_0_9:[bind(X,$fot(implies(implies(not(X_33),X_32),X_34))),bind(Y,$fot(implies(X_33,X_34)))]]) ).
cnf(refute_0_11,plain,
is_a_theorem(implies(X,implies(not(X),Y))),
inference(canonicalize,[],[normalize_0_8]) ).
cnf(refute_0_12,plain,
is_a_theorem(implies(X_27,implies(not(X_27),Y))),
inference(subst,[],[refute_0_11:[bind(X,$fot(X_27))]]) ).
cnf(refute_0_13,plain,
( ~ is_a_theorem(implies(X_27,implies(not(X_27),Y)))
| is_a_theorem(implies(implies(implies(not(X_27),Y),X_29),implies(X_27,X_29))) ),
inference(subst,[],[refute_0_9:[bind(X,$fot(X_27)),bind(Y,$fot(implies(not(X_27),Y))),bind(Z,$fot(X_29))]]) ).
cnf(refute_0_14,plain,
is_a_theorem(implies(implies(implies(not(X_27),Y),X_29),implies(X_27,X_29))),
inference(resolve,[$cnf( is_a_theorem(implies(X_27,implies(not(X_27),Y))) )],[refute_0_12,refute_0_13]) ).
cnf(refute_0_15,plain,
is_a_theorem(implies(implies(implies(not(X_33),X_32),X_34),implies(X_33,X_34))),
inference(subst,[],[refute_0_14:[bind(Y,$fot(X_32)),bind(X_27,$fot(X_33)),bind(X_29,$fot(X_34))]]) ).
cnf(refute_0_16,plain,
is_a_theorem(implies(implies(implies(X_33,X_34),Z),implies(implies(implies(not(X_33),X_32),X_34),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_33),X_32),X_34),implies(X_33,X_34))) )],[refute_0_15,refute_0_10]) ).
cnf(refute_0_17,plain,
is_a_theorem(implies(implies(implies(X_154,X_155),X_152),implies(implies(implies(not(X_154),X_153),X_155),X_152))),
inference(subst,[],[refute_0_16:[bind(Z,$fot(X_152)),bind(X_32,$fot(X_153)),bind(X_33,$fot(X_154)),bind(X_34,$fot(X_155))]]) ).
cnf(refute_0_18,plain,
( ~ is_a_theorem(implies(implies(X_154,X_155),X_152))
| is_a_theorem(implies(implies(implies(not(X_154),X_153),X_155),X_152)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_154,X_155),X_152),implies(implies(implies(not(X_154),X_153),X_155),X_152))) )],[refute_0_17,refute_0_6]) ).
cnf(refute_0_19,plain,
( ~ is_a_theorem(implies(implies(not(X_357),X_357),X_357))
| is_a_theorem(implies(implies(implies(not(not(X_357)),X_358),X_357),X_357)) ),
inference(subst,[],[refute_0_18:[bind(X_152,$fot(X_357)),bind(X_153,$fot(X_358)),bind(X_154,$fot(not(X_357))),bind(X_155,$fot(X_357))]]) ).
cnf(refute_0_20,plain,
is_a_theorem(implies(implies(implies(not(not(X_357)),X_358),X_357),X_357)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_357),X_357),X_357)) )],[refute_0_5,refute_0_19]) ).
cnf(refute_0_21,plain,
is_a_theorem(implies(implies(implies(not(not(X_361)),X_362),X_361),X_361)),
inference(subst,[],[refute_0_20:[bind(X_357,$fot(X_361)),bind(X_358,$fot(X_362))]]) ).
cnf(refute_0_22,plain,
( ~ is_a_theorem(implies(implies(not(not(X_361)),X_362),X_361))
| is_a_theorem(X_361) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(not(X_361)),X_362),X_361),X_361)) )],[refute_0_21,refute_0_3]) ).
cnf(refute_0_23,plain,
( ~ is_a_theorem(implies(implies(not(not(implies(implies(implies(implies(not(X_1820),X_1820),X_1820),X_1821),X_1821))),X_362),implies(implies(implies(implies(not(X_1820),X_1820),X_1820),X_1821),X_1821)))
| is_a_theorem(implies(implies(implies(implies(not(X_1820),X_1820),X_1820),X_1821),X_1821)) ),
inference(subst,[],[refute_0_22:[bind(X_361,$fot(implies(implies(implies(implies(not(X_1820),X_1820),X_1820),X_1821),X_1821)))]]) ).
cnf(refute_0_24,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(X_47),X_47),X_48),X_46),implies(implies(X_47,X_48),X_46)))
| ~ is_a_theorem(implies(implies(implies(not(X_47),X_47),X_48),X_46))
| is_a_theorem(implies(implies(X_47,X_48),X_46)) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(implies(implies(implies(not(X_47),X_47),X_48),X_46))),bind(Y,$fot(implies(implies(X_47,X_48),X_46)))]]) ).
cnf(refute_0_25,plain,
( ~ is_a_theorem(implies(implies(X_30,X_31),implies(implies(not(X_30),X_30),X_31)))
| is_a_theorem(implies(implies(implies(implies(not(X_30),X_30),X_31),Z),implies(implies(X_30,X_31),Z))) ),
inference(subst,[],[refute_0_9:[bind(X,$fot(implies(X_30,X_31))),bind(Y,$fot(implies(implies(not(X_30),X_30),X_31)))]]) ).
cnf(refute_0_26,plain,
is_a_theorem(implies(implies(not(X_28),X_28),X_28)),
inference(subst,[],[refute_0_4:[bind(X,$fot(X_28))]]) ).
cnf(refute_0_27,plain,
( ~ is_a_theorem(implies(implies(not(X_28),X_28),X_28))
| is_a_theorem(implies(implies(X_28,X_29),implies(implies(not(X_28),X_28),X_29))) ),
inference(subst,[],[refute_0_9:[bind(X,$fot(implies(not(X_28),X_28))),bind(Y,$fot(X_28)),bind(Z,$fot(X_29))]]) ).
cnf(refute_0_28,plain,
is_a_theorem(implies(implies(X_28,X_29),implies(implies(not(X_28),X_28),X_29))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_28),X_28),X_28)) )],[refute_0_26,refute_0_27]) ).
cnf(refute_0_29,plain,
is_a_theorem(implies(implies(X_30,X_31),implies(implies(not(X_30),X_30),X_31))),
inference(subst,[],[refute_0_28:[bind(X_28,$fot(X_30)),bind(X_29,$fot(X_31))]]) ).
cnf(refute_0_30,plain,
is_a_theorem(implies(implies(implies(implies(not(X_30),X_30),X_31),Z),implies(implies(X_30,X_31),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_30,X_31),implies(implies(not(X_30),X_30),X_31))) )],[refute_0_29,refute_0_25]) ).
cnf(refute_0_31,plain,
is_a_theorem(implies(implies(implies(implies(not(X_47),X_47),X_48),X_46),implies(implies(X_47,X_48),X_46))),
inference(subst,[],[refute_0_30:[bind(Z,$fot(X_46)),bind(X_30,$fot(X_47)),bind(X_31,$fot(X_48))]]) ).
cnf(refute_0_32,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_47),X_47),X_48),X_46))
| is_a_theorem(implies(implies(X_47,X_48),X_46)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(X_47),X_47),X_48),X_46),implies(implies(X_47,X_48),X_46))) )],[refute_0_31,refute_0_24]) ).
cnf(refute_0_33,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_1329),X_1329),X_1328),implies(implies(implies(implies(not(X_1330),X_1330),X_1330),X_1329),X_1328)))
| is_a_theorem(implies(implies(X_1329,X_1328),implies(implies(implies(implies(not(X_1330),X_1330),X_1330),X_1329),X_1328))) ),
inference(subst,[],[refute_0_32:[bind(X_46,$fot(implies(implies(implies(implies(not(X_1330),X_1330),X_1330),X_1329),X_1328))),bind(X_47,$fot(X_1329)),bind(X_48,$fot(X_1328))]]) ).
cnf(refute_0_34,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(X_1317),X_1317),X_1317),X_1316),implies(X_1318,X_1316)))
| is_a_theorem(implies(implies(implies(X_1318,X_1316),Z),implies(implies(implies(implies(not(X_1317),X_1317),X_1317),X_1316),Z))) ),
inference(subst,[],[refute_0_9:[bind(X,$fot(implies(implies(implies(not(X_1317),X_1317),X_1317),X_1316))),bind(Y,$fot(implies(X_1318,X_1316)))]]) ).
cnf(refute_0_35,plain,
( ~ is_a_theorem(implies(X_248,implies(not(implies(implies(not(X_246),X_246),X_246)),X_247)))
| is_a_theorem(implies(implies(implies(not(implies(implies(not(X_246),X_246),X_246)),X_247),Z),implies(X_248,Z))) ),
inference(subst,[],[refute_0_9:[bind(X,$fot(X_248)),bind(Y,$fot(implies(not(implies(implies(not(X_246),X_246),X_246)),X_247)))]]) ).
cnf(refute_0_36,plain,
is_a_theorem(implies(X_6,implies(not(X_6),Y))),
inference(subst,[],[refute_0_11:[bind(X,$fot(X_6))]]) ).
cnf(refute_0_37,plain,
( ~ is_a_theorem(X_6)
| ~ is_a_theorem(implies(X_6,implies(not(X_6),Y)))
| is_a_theorem(implies(not(X_6),Y)) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(X_6)),bind(Y,$fot(implies(not(X_6),Y)))]]) ).
cnf(refute_0_38,plain,
( ~ is_a_theorem(X_6)
| is_a_theorem(implies(not(X_6),Y)) ),
inference(resolve,[$cnf( is_a_theorem(implies(X_6,implies(not(X_6),Y))) )],[refute_0_36,refute_0_37]) ).
cnf(refute_0_39,plain,
( ~ is_a_theorem(implies(implies(not(X),X),X))
| is_a_theorem(implies(not(implies(implies(not(X),X),X)),X_9)) ),
inference(subst,[],[refute_0_38:[bind(Y,$fot(X_9)),bind(X_6,$fot(implies(implies(not(X),X),X)))]]) ).
cnf(refute_0_40,plain,
is_a_theorem(implies(not(implies(implies(not(X),X),X)),X_9)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X),X),X)) )],[refute_0_4,refute_0_39]) ).
cnf(refute_0_41,plain,
is_a_theorem(implies(not(implies(implies(not(X),X),X)),X_28)),
inference(subst,[],[refute_0_40:[bind(X_9,$fot(X_28))]]) ).
cnf(refute_0_42,plain,
( ~ is_a_theorem(implies(not(implies(implies(not(X),X),X)),X_28))
| is_a_theorem(implies(implies(X_28,X_29),implies(not(implies(implies(not(X),X),X)),X_29))) ),
inference(subst,[],[refute_0_9:[bind(X,$fot(not(implies(implies(not(X),X),X)))),bind(Y,$fot(X_28)),bind(Z,$fot(X_29))]]) ).
cnf(refute_0_43,plain,
is_a_theorem(implies(implies(X_28,X_29),implies(not(implies(implies(not(X),X),X)),X_29))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(implies(not(X),X),X)),X_28)) )],[refute_0_41,refute_0_42]) ).
cnf(refute_0_44,plain,
is_a_theorem(implies(implies(not(X_239),X_238),implies(not(implies(implies(not(X),X),X)),X_238))),
inference(subst,[],[refute_0_43:[bind(X_28,$fot(not(X_239))),bind(X_29,$fot(X_238))]]) ).
cnf(refute_0_45,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_33),X_32),X_34),implies(X_33,X_34)))
| ~ is_a_theorem(implies(implies(not(X_33),X_32),X_34))
| is_a_theorem(implies(X_33,X_34)) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(implies(implies(not(X_33),X_32),X_34))),bind(Y,$fot(implies(X_33,X_34)))]]) ).
cnf(refute_0_46,plain,
( ~ is_a_theorem(implies(implies(not(X_33),X_32),X_34))
| is_a_theorem(implies(X_33,X_34)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_33),X_32),X_34),implies(X_33,X_34))) )],[refute_0_15,refute_0_45]) ).
cnf(refute_0_47,plain,
( ~ is_a_theorem(implies(implies(not(X_239),X_238),implies(not(implies(implies(not(X),X),X)),X_238)))
| is_a_theorem(implies(X_239,implies(not(implies(implies(not(X),X),X)),X_238))) ),
inference(subst,[],[refute_0_46:[bind(X_32,$fot(X_238)),bind(X_33,$fot(X_239)),bind(X_34,$fot(implies(not(implies(implies(not(X),X),X)),X_238)))]]) ).
cnf(refute_0_48,plain,
is_a_theorem(implies(X_239,implies(not(implies(implies(not(X),X),X)),X_238))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_239),X_238),implies(not(implies(implies(not(X),X),X)),X_238))) )],[refute_0_44,refute_0_47]) ).
cnf(refute_0_49,plain,
is_a_theorem(implies(X_248,implies(not(implies(implies(not(X_246),X_246),X_246)),X_247))),
inference(subst,[],[refute_0_48:[bind(X,$fot(X_246)),bind(X_238,$fot(X_247)),bind(X_239,$fot(X_248))]]) ).
cnf(refute_0_50,plain,
is_a_theorem(implies(implies(implies(not(implies(implies(not(X_246),X_246),X_246)),X_247),Z),implies(X_248,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_248,implies(not(implies(implies(not(X_246),X_246),X_246)),X_247))) )],[refute_0_49,refute_0_35]) ).
cnf(refute_0_51,plain,
is_a_theorem(implies(implies(implies(not(implies(implies(not(X_246),X_246),X_246)),implies(implies(not(X_246),X_246),X_246)),X_1290),implies(X_248,X_1290))),
inference(subst,[],[refute_0_50:[bind(Z,$fot(X_1290)),bind(X_247,$fot(implies(implies(not(X_246),X_246),X_246)))]]) ).
cnf(refute_0_52,plain,
( ~ is_a_theorem(implies(implies(implies(not(implies(implies(not(X_246),X_246),X_246)),implies(implies(not(X_246),X_246),X_246)),X_1290),implies(X_248,X_1290)))
| is_a_theorem(implies(implies(implies(implies(not(X_246),X_246),X_246),X_1290),implies(X_248,X_1290))) ),
inference(subst,[],[refute_0_32:[bind(X_46,$fot(implies(X_248,X_1290))),bind(X_47,$fot(implies(implies(not(X_246),X_246),X_246))),bind(X_48,$fot(X_1290))]]) ).
cnf(refute_0_53,plain,
is_a_theorem(implies(implies(implies(implies(not(X_246),X_246),X_246),X_1290),implies(X_248,X_1290))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(implies(implies(not(X_246),X_246),X_246)),implies(implies(not(X_246),X_246),X_246)),X_1290),implies(X_248,X_1290))) )],[refute_0_51,refute_0_52]) ).
cnf(refute_0_54,plain,
is_a_theorem(implies(implies(implies(implies(not(X_1317),X_1317),X_1317),X_1316),implies(X_1318,X_1316))),
inference(subst,[],[refute_0_53:[bind(X_1290,$fot(X_1316)),bind(X_246,$fot(X_1317)),bind(X_248,$fot(X_1318))]]) ).
cnf(refute_0_55,plain,
is_a_theorem(implies(implies(implies(X_1318,X_1316),Z),implies(implies(implies(implies(not(X_1317),X_1317),X_1317),X_1316),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(X_1317),X_1317),X_1317),X_1316),implies(X_1318,X_1316))) )],[refute_0_54,refute_0_34]) ).
cnf(refute_0_56,plain,
is_a_theorem(implies(implies(implies(not(X_1329),X_1329),X_1328),implies(implies(implies(implies(not(X_1330),X_1330),X_1330),X_1329),X_1328))),
inference(subst,[],[refute_0_55:[bind(Z,$fot(X_1328)),bind(X_1316,$fot(X_1329)),bind(X_1317,$fot(X_1330)),bind(X_1318,$fot(not(X_1329)))]]) ).
cnf(refute_0_57,plain,
is_a_theorem(implies(implies(X_1329,X_1328),implies(implies(implies(implies(not(X_1330),X_1330),X_1330),X_1329),X_1328))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_1329),X_1329),X_1328),implies(implies(implies(implies(not(X_1330),X_1330),X_1330),X_1329),X_1328))) )],[refute_0_56,refute_0_33]) ).
cnf(refute_0_58,plain,
is_a_theorem(implies(implies(X_1548,X_1548),implies(implies(implies(implies(not(X_1330),X_1330),X_1330),X_1548),X_1548))),
inference(subst,[],[refute_0_57:[bind(X_1328,$fot(X_1548)),bind(X_1329,$fot(X_1548))]]) ).
cnf(refute_0_59,plain,
( ~ is_a_theorem(implies(implies(X_1292,X_1292),X_1291))
| ~ is_a_theorem(implies(implies(implies(X_1292,X_1292),X_1291),implies(X_1293,X_1291)))
| is_a_theorem(implies(X_1293,X_1291)) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(implies(implies(X_1292,X_1292),X_1291))),bind(Y,$fot(implies(X_1293,X_1291)))]]) ).
cnf(refute_0_60,plain,
( ~ is_a_theorem(implies(X_297,implies(not(implies(X_296,X_296)),X_295)))
| is_a_theorem(implies(implies(implies(not(implies(X_296,X_296)),X_295),Z),implies(X_297,Z))) ),
inference(subst,[],[refute_0_9:[bind(X,$fot(X_297)),bind(Y,$fot(implies(not(implies(X_296,X_296)),X_295)))]]) ).
cnf(refute_0_61,plain,
( ~ is_a_theorem(implies(implies(not(X_33),X_292),implies(not(implies(X_294,X_294)),X_292)))
| is_a_theorem(implies(X_33,implies(not(implies(X_294,X_294)),X_292))) ),
inference(subst,[],[refute_0_46:[bind(X_32,$fot(X_292)),bind(X_34,$fot(implies(not(implies(X_294,X_294)),X_292)))]]) ).
cnf(refute_0_62,plain,
( ~ is_a_theorem(implies(not(implies(X_243,X_243)),X_242))
| is_a_theorem(implies(implies(X_242,Z),implies(not(implies(X_243,X_243)),Z))) ),
inference(subst,[],[refute_0_9:[bind(X,$fot(not(implies(X_243,X_243)))),bind(Y,$fot(X_242))]]) ).
cnf(refute_0_63,plain,
( ~ is_a_theorem(implies(X_241,X_241))
| is_a_theorem(implies(not(implies(X_241,X_241)),Y)) ),
inference(subst,[],[refute_0_38:[bind(X_6,$fot(implies(X_241,X_241)))]]) ).
cnf(refute_0_64,plain,
is_a_theorem(implies(implies(not(X_240),X_240),X_240)),
inference(subst,[],[refute_0_4:[bind(X,$fot(X_240))]]) ).
cnf(refute_0_65,plain,
( ~ is_a_theorem(implies(implies(not(X_240),X_240),X_240))
| is_a_theorem(implies(X_240,X_240)) ),
inference(subst,[],[refute_0_46:[bind(X_32,$fot(X_240)),bind(X_33,$fot(X_240)),bind(X_34,$fot(X_240))]]) ).
cnf(refute_0_66,plain,
is_a_theorem(implies(X_240,X_240)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_240),X_240),X_240)) )],[refute_0_64,refute_0_65]) ).
cnf(refute_0_67,plain,
is_a_theorem(implies(X_241,X_241)),
inference(subst,[],[refute_0_66:[bind(X_240,$fot(X_241))]]) ).
cnf(refute_0_68,plain,
is_a_theorem(implies(not(implies(X_241,X_241)),Y)),
inference(resolve,[$cnf( is_a_theorem(implies(X_241,X_241)) )],[refute_0_67,refute_0_63]) ).
cnf(refute_0_69,plain,
is_a_theorem(implies(not(implies(X_243,X_243)),X_242)),
inference(subst,[],[refute_0_68:[bind(Y,$fot(X_242)),bind(X_241,$fot(X_243))]]) ).
cnf(refute_0_70,plain,
is_a_theorem(implies(implies(X_242,Z),implies(not(implies(X_243,X_243)),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(X_243,X_243)),X_242)) )],[refute_0_69,refute_0_62]) ).
cnf(refute_0_71,plain,
is_a_theorem(implies(implies(not(X_33),X_292),implies(not(implies(X_294,X_294)),X_292))),
inference(subst,[],[refute_0_70:[bind(Z,$fot(X_292)),bind(X_242,$fot(not(X_33))),bind(X_243,$fot(X_294))]]) ).
cnf(refute_0_72,plain,
is_a_theorem(implies(X_33,implies(not(implies(X_294,X_294)),X_292))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_33),X_292),implies(not(implies(X_294,X_294)),X_292))) )],[refute_0_71,refute_0_61]) ).
cnf(refute_0_73,plain,
is_a_theorem(implies(X_297,implies(not(implies(X_296,X_296)),X_295))),
inference(subst,[],[refute_0_72:[bind(X_292,$fot(X_295)),bind(X_294,$fot(X_296)),bind(X_33,$fot(X_297))]]) ).
cnf(refute_0_74,plain,
is_a_theorem(implies(implies(implies(not(implies(X_296,X_296)),X_295),Z),implies(X_297,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_297,implies(not(implies(X_296,X_296)),X_295))) )],[refute_0_73,refute_0_60]) ).
cnf(refute_0_75,plain,
is_a_theorem(implies(implies(implies(not(implies(X_296,X_296)),implies(X_296,X_296)),X_1290),implies(X_297,X_1290))),
inference(subst,[],[refute_0_74:[bind(Z,$fot(X_1290)),bind(X_295,$fot(implies(X_296,X_296)))]]) ).
cnf(refute_0_76,plain,
( ~ is_a_theorem(implies(implies(implies(not(implies(X_296,X_296)),implies(X_296,X_296)),X_1290),implies(X_297,X_1290)))
| is_a_theorem(implies(implies(implies(X_296,X_296),X_1290),implies(X_297,X_1290))) ),
inference(subst,[],[refute_0_32:[bind(X_46,$fot(implies(X_297,X_1290))),bind(X_47,$fot(implies(X_296,X_296))),bind(X_48,$fot(X_1290))]]) ).
cnf(refute_0_77,plain,
is_a_theorem(implies(implies(implies(X_296,X_296),X_1290),implies(X_297,X_1290))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(implies(X_296,X_296)),implies(X_296,X_296)),X_1290),implies(X_297,X_1290))) )],[refute_0_75,refute_0_76]) ).
cnf(refute_0_78,plain,
is_a_theorem(implies(implies(implies(X_1292,X_1292),X_1291),implies(X_1293,X_1291))),
inference(subst,[],[refute_0_77:[bind(X_1290,$fot(X_1291)),bind(X_296,$fot(X_1292)),bind(X_297,$fot(X_1293))]]) ).
cnf(refute_0_79,plain,
( ~ is_a_theorem(implies(implies(X_1292,X_1292),X_1291))
| is_a_theorem(implies(X_1293,X_1291)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_1292,X_1292),X_1291),implies(X_1293,X_1291))) )],[refute_0_78,refute_0_59]) ).
cnf(refute_0_80,plain,
( ~ is_a_theorem(implies(implies(X_1548,X_1548),implies(implies(implies(implies(not(X_1330),X_1330),X_1330),X_1548),X_1548)))
| is_a_theorem(implies(X_1549,implies(implies(implies(implies(not(X_1330),X_1330),X_1330),X_1548),X_1548))) ),
inference(subst,[],[refute_0_79:[bind(X_1291,$fot(implies(implies(implies(implies(not(X_1330),X_1330),X_1330),X_1548),X_1548))),bind(X_1292,$fot(X_1548)),bind(X_1293,$fot(X_1549))]]) ).
cnf(refute_0_81,plain,
is_a_theorem(implies(X_1549,implies(implies(implies(implies(not(X_1330),X_1330),X_1330),X_1548),X_1548))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_1548,X_1548),implies(implies(implies(implies(not(X_1330),X_1330),X_1330),X_1548),X_1548))) )],[refute_0_58,refute_0_80]) ).
cnf(refute_0_82,plain,
is_a_theorem(implies(implies(not(not(implies(implies(implies(implies(not(X_1820),X_1820),X_1820),X_1821),X_1821))),X_362),implies(implies(implies(implies(not(X_1820),X_1820),X_1820),X_1821),X_1821))),
inference(subst,[],[refute_0_81:[bind(X_1330,$fot(X_1820)),bind(X_1548,$fot(X_1821)),bind(X_1549,$fot(implies(not(not(implies(implies(implies(implies(not(X_1820),X_1820),X_1820),X_1821),X_1821))),X_362)))]]) ).
cnf(refute_0_83,plain,
is_a_theorem(implies(implies(implies(implies(not(X_1820),X_1820),X_1820),X_1821),X_1821)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(not(implies(implies(implies(implies(not(X_1820),X_1820),X_1820),X_1821),X_1821))),X_362),implies(implies(implies(implies(not(X_1820),X_1820),X_1820),X_1821),X_1821))) )],[refute_0_82,refute_0_23]) ).
cnf(refute_0_84,plain,
is_a_theorem(implies(implies(implies(implies(not(X_2082),X_2082),X_2082),implies(X_2080,X_2082)),implies(X_2080,X_2082))),
inference(subst,[],[refute_0_83:[bind(X_1820,$fot(X_2082)),bind(X_1821,$fot(implies(X_2080,X_2082)))]]) ).
cnf(refute_0_85,plain,
( ~ is_a_theorem(implies(implies(implies(X_36,X_37),implies(X_35,X_37)),X_38))
| ~ is_a_theorem(implies(implies(implies(implies(X_36,X_37),implies(X_35,X_37)),X_38),implies(implies(X_35,X_36),X_38)))
| is_a_theorem(implies(implies(X_35,X_36),X_38)) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(implies(implies(implies(X_36,X_37),implies(X_35,X_37)),X_38))),bind(Y,$fot(implies(implies(X_35,X_36),X_38)))]]) ).
cnf(refute_0_86,plain,
( ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))))
| is_a_theorem(implies(implies(implies(implies(Y,Z),implies(X,Z)),X_29),implies(implies(X,Y),X_29))) ),
inference(subst,[],[refute_0_9:[bind(X,$fot(implies(X,Y))),bind(Y,$fot(implies(implies(Y,Z),implies(X,Z)))),bind(Z,$fot(X_29))]]) ).
cnf(refute_0_87,plain,
is_a_theorem(implies(implies(implies(implies(Y,Z),implies(X,Z)),X_29),implies(implies(X,Y),X_29))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )],[refute_0_7,refute_0_86]) ).
cnf(refute_0_88,plain,
is_a_theorem(implies(implies(implies(implies(X_36,X_37),implies(X_35,X_37)),X_38),implies(implies(X_35,X_36),X_38))),
inference(subst,[],[refute_0_87:[bind(X,$fot(X_35)),bind(Y,$fot(X_36)),bind(Z,$fot(X_37)),bind(X_29,$fot(X_38))]]) ).
cnf(refute_0_89,plain,
( ~ is_a_theorem(implies(implies(implies(X_36,X_37),implies(X_35,X_37)),X_38))
| is_a_theorem(implies(implies(X_35,X_36),X_38)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_36,X_37),implies(X_35,X_37)),X_38),implies(implies(X_35,X_36),X_38))) )],[refute_0_88,refute_0_85]) ).
cnf(refute_0_90,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(X_2082),X_2082),X_2082),implies(X_2080,X_2082)),implies(X_2080,X_2082)))
| is_a_theorem(implies(implies(X_2080,implies(not(X_2082),X_2082)),implies(X_2080,X_2082))) ),
inference(subst,[],[refute_0_89:[bind(X_35,$fot(X_2080)),bind(X_36,$fot(implies(not(X_2082),X_2082))),bind(X_37,$fot(X_2082)),bind(X_38,$fot(implies(X_2080,X_2082)))]]) ).
cnf(refute_0_91,plain,
is_a_theorem(implies(implies(X_2080,implies(not(X_2082),X_2082)),implies(X_2080,X_2082))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(X_2082),X_2082),X_2082),implies(X_2080,X_2082)),implies(X_2080,X_2082))) )],[refute_0_84,refute_0_90]) ).
cnf(refute_0_92,plain,
is_a_theorem(implies(implies(X_2106,implies(not(X_2107),X_2107)),implies(X_2106,X_2107))),
inference(subst,[],[refute_0_91:[bind(X_2080,$fot(X_2106)),bind(X_2082,$fot(X_2107))]]) ).
cnf(refute_0_93,plain,
( ~ is_a_theorem(implies(X_2106,implies(not(X_2107),X_2107)))
| is_a_theorem(implies(X_2106,X_2107)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_2106,implies(not(X_2107),X_2107)),implies(X_2106,X_2107))) )],[refute_0_92,refute_0_2]) ).
cnf(refute_0_94,plain,
( ~ is_a_theorem(implies(implies(X_31730,X_31731),implies(not(implies(implies(X_31731,not(X_31730)),not(X_31730))),implies(implies(X_31731,not(X_31730)),not(X_31730)))))
| is_a_theorem(implies(implies(X_31730,X_31731),implies(implies(X_31731,not(X_31730)),not(X_31730)))) ),
inference(subst,[],[refute_0_93:[bind(X_2106,$fot(implies(X_31730,X_31731))),bind(X_2107,$fot(implies(implies(X_31731,not(X_31730)),not(X_31730))))]]) ).
cnf(refute_0_95,plain,
( ~ is_a_theorem(implies(implies(implies(X_36,not(X_31727)),implies(X_31727,not(X_31727))),implies(X_31726,implies(implies(X_36,not(X_31727)),not(X_31727)))))
| is_a_theorem(implies(implies(X_31727,X_36),implies(X_31726,implies(implies(X_36,not(X_31727)),not(X_31727))))) ),
inference(subst,[],[refute_0_89:[bind(X_35,$fot(X_31727)),bind(X_37,$fot(not(X_31727))),bind(X_38,$fot(implies(X_31726,implies(implies(X_36,not(X_31727)),not(X_31727)))))]]) ).
cnf(refute_0_96,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_23247,not(X_23247)),not(X_23247)),implies(X_35,not(X_23247))),implies(X_23246,implies(X_35,not(X_23247)))))
| is_a_theorem(implies(implies(X_35,implies(X_23247,not(X_23247))),implies(X_23246,implies(X_35,not(X_23247))))) ),
inference(subst,[],[refute_0_89:[bind(X_36,$fot(implies(X_23247,not(X_23247)))),bind(X_37,$fot(not(X_23247))),bind(X_38,$fot(implies(X_23246,implies(X_35,not(X_23247)))))]]) ).
cnf(refute_0_97,plain,
( ~ is_a_theorem(implies(implies(not(X_2110),X_2111),implies(implies(X_2111,X_2110),X_2110)))
| ~ is_a_theorem(implies(not(X_2110),X_2111))
| is_a_theorem(implies(implies(X_2111,X_2110),X_2110)) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(implies(not(X_2110),X_2111))),bind(Y,$fot(implies(implies(X_2111,X_2110),X_2110)))]]) ).
cnf(refute_0_98,plain,
( ~ is_a_theorem(implies(implies(implies(X_36,X_2107),implies(not(X_2107),X_2107)),implies(implies(X_36,X_2107),X_2107)))
| is_a_theorem(implies(implies(not(X_2107),X_36),implies(implies(X_36,X_2107),X_2107))) ),
inference(subst,[],[refute_0_89:[bind(X_35,$fot(not(X_2107))),bind(X_37,$fot(X_2107)),bind(X_38,$fot(implies(implies(X_36,X_2107),X_2107)))]]) ).
cnf(refute_0_99,plain,
is_a_theorem(implies(implies(implies(X_36,X_2107),implies(not(X_2107),X_2107)),implies(implies(X_36,X_2107),X_2107))),
inference(subst,[],[refute_0_91:[bind(X_2080,$fot(implies(X_36,X_2107))),bind(X_2082,$fot(X_2107))]]) ).
cnf(refute_0_100,plain,
is_a_theorem(implies(implies(not(X_2107),X_36),implies(implies(X_36,X_2107),X_2107))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_36,X_2107),implies(not(X_2107),X_2107)),implies(implies(X_36,X_2107),X_2107))) )],[refute_0_99,refute_0_98]) ).
cnf(refute_0_101,plain,
is_a_theorem(implies(implies(not(X_2110),X_2111),implies(implies(X_2111,X_2110),X_2110))),
inference(subst,[],[refute_0_100:[bind(X_2107,$fot(X_2110)),bind(X_36,$fot(X_2111))]]) ).
cnf(refute_0_102,plain,
( ~ is_a_theorem(implies(not(X_2110),X_2111))
| is_a_theorem(implies(implies(X_2111,X_2110),X_2110)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_2110),X_2111),implies(implies(X_2111,X_2110),X_2110))) )],[refute_0_101,refute_0_97]) ).
cnf(refute_0_103,plain,
( ~ is_a_theorem(implies(not(not(X_4659)),X_4659))
| is_a_theorem(implies(implies(X_4659,not(X_4659)),not(X_4659))) ),
inference(subst,[],[refute_0_102:[bind(X_2110,$fot(not(X_4659))),bind(X_2111,$fot(X_4659))]]) ).
cnf(refute_0_104,plain,
( ~ is_a_theorem(implies(implies(implies(not(implies(not(X_279),X_278)),X_277),X_276),implies(X_279,X_276)))
| ~ is_a_theorem(implies(implies(not(implies(not(X_279),X_278)),X_277),X_276))
| is_a_theorem(implies(X_279,X_276)) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(implies(implies(not(implies(not(X_279),X_278)),X_277),X_276))),bind(Y,$fot(implies(X_279,X_276)))]]) ).
cnf(refute_0_105,plain,
( ~ is_a_theorem(implies(X_256,implies(not(implies(not(X_256),X_255)),X_254)))
| is_a_theorem(implies(implies(implies(not(implies(not(X_256),X_255)),X_254),Z),implies(X_256,Z))) ),
inference(subst,[],[refute_0_9:[bind(X,$fot(X_256)),bind(Y,$fot(implies(not(implies(not(X_256),X_255)),X_254)))]]) ).
cnf(refute_0_106,plain,
is_a_theorem(implies(implies(not(X_239),X_238),implies(not(implies(not(X_239),X_238)),Y))),
inference(subst,[],[refute_0_11:[bind(X,$fot(implies(not(X_239),X_238)))]]) ).
cnf(refute_0_107,plain,
( ~ is_a_theorem(implies(implies(not(X_239),X_238),implies(not(implies(not(X_239),X_238)),Y)))
| is_a_theorem(implies(X_239,implies(not(implies(not(X_239),X_238)),Y))) ),
inference(subst,[],[refute_0_46:[bind(X_32,$fot(X_238)),bind(X_33,$fot(X_239)),bind(X_34,$fot(implies(not(implies(not(X_239),X_238)),Y)))]]) ).
cnf(refute_0_108,plain,
is_a_theorem(implies(X_239,implies(not(implies(not(X_239),X_238)),Y))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_239),X_238),implies(not(implies(not(X_239),X_238)),Y))) )],[refute_0_106,refute_0_107]) ).
cnf(refute_0_109,plain,
is_a_theorem(implies(X_256,implies(not(implies(not(X_256),X_255)),X_254))),
inference(subst,[],[refute_0_108:[bind(Y,$fot(X_254)),bind(X_238,$fot(X_255)),bind(X_239,$fot(X_256))]]) ).
cnf(refute_0_110,plain,
is_a_theorem(implies(implies(implies(not(implies(not(X_256),X_255)),X_254),Z),implies(X_256,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_256,implies(not(implies(not(X_256),X_255)),X_254))) )],[refute_0_109,refute_0_105]) ).
cnf(refute_0_111,plain,
is_a_theorem(implies(implies(implies(not(implies(not(X_279),X_278)),X_277),X_276),implies(X_279,X_276))),
inference(subst,[],[refute_0_110:[bind(Z,$fot(X_276)),bind(X_254,$fot(X_277)),bind(X_255,$fot(X_278)),bind(X_256,$fot(X_279))]]) ).
cnf(refute_0_112,plain,
( ~ is_a_theorem(implies(implies(not(implies(not(X_279),X_278)),X_277),X_276))
| is_a_theorem(implies(X_279,X_276)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(implies(not(X_279),X_278)),X_277),X_276),implies(X_279,X_276))) )],[refute_0_111,refute_0_104]) ).
cnf(refute_0_113,plain,
( ~ is_a_theorem(implies(implies(not(implies(not(not(not(X_4658))),not(not(X_4658)))),X_4658),X_4658))
| is_a_theorem(implies(not(not(X_4658)),X_4658)) ),
inference(subst,[],[refute_0_112:[bind(X_276,$fot(X_4658)),bind(X_277,$fot(X_4658)),bind(X_278,$fot(not(not(X_4658)))),bind(X_279,$fot(not(not(X_4658))))]]) ).
cnf(refute_0_114,plain,
( ~ is_a_theorem(implies(not(X_2110),not(implies(not(not(not(X_2110))),not(not(X_2110))))))
| is_a_theorem(implies(implies(not(implies(not(not(not(X_2110))),not(not(X_2110)))),X_2110),X_2110)) ),
inference(subst,[],[refute_0_102:[bind(X_2111,$fot(not(implies(not(not(not(X_2110))),not(not(X_2110))))))]]) ).
cnf(refute_0_115,plain,
( ~ is_a_theorem(implies(implies(not(X_33),not(implies(not(not(X_33)),not(X_33)))),not(implies(not(not(X_33)),not(X_33)))))
| is_a_theorem(implies(X_33,not(implies(not(not(X_33)),not(X_33))))) ),
inference(subst,[],[refute_0_46:[bind(X_32,$fot(not(implies(not(not(X_33)),not(X_33))))),bind(X_34,$fot(not(implies(not(not(X_33)),not(X_33)))))]]) ).
cnf(refute_0_116,plain,
( ~ is_a_theorem(implies(not(not(implies(not(X_4654),X_4654))),X_4654))
| is_a_theorem(implies(implies(X_4654,not(implies(not(X_4654),X_4654))),not(implies(not(X_4654),X_4654)))) ),
inference(subst,[],[refute_0_102:[bind(X_2110,$fot(not(implies(not(X_4654),X_4654)))),bind(X_2111,$fot(X_4654))]]) ).
cnf(refute_0_117,plain,
( ~ is_a_theorem(implies(implies(implies(X_290,X_289),implies(not(X_291),X_289)),X_288))
| ~ is_a_theorem(implies(implies(implies(implies(X_290,X_289),implies(not(X_291),X_289)),X_288),implies(X_291,X_288)))
| is_a_theorem(implies(X_291,X_288)) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(implies(implies(implies(X_290,X_289),implies(not(X_291),X_289)),X_288))),bind(Y,$fot(implies(X_291,X_288)))]]) ).
cnf(refute_0_118,plain,
( ~ is_a_theorem(implies(X_251,implies(implies(X_250,X_249),implies(not(X_251),X_249))))
| is_a_theorem(implies(implies(implies(implies(X_250,X_249),implies(not(X_251),X_249)),Z),implies(X_251,Z))) ),
inference(subst,[],[refute_0_9:[bind(X,$fot(X_251)),bind(Y,$fot(implies(implies(X_250,X_249),implies(not(X_251),X_249))))]]) ).
cnf(refute_0_119,plain,
is_a_theorem(implies(implies(not(X_239),X_238),implies(implies(X_238,Z),implies(not(X_239),Z)))),
inference(subst,[],[refute_0_7:[bind(X,$fot(not(X_239))),bind(Y,$fot(X_238))]]) ).
cnf(refute_0_120,plain,
( ~ is_a_theorem(implies(implies(not(X_239),X_238),implies(implies(X_238,Z),implies(not(X_239),Z))))
| is_a_theorem(implies(X_239,implies(implies(X_238,Z),implies(not(X_239),Z)))) ),
inference(subst,[],[refute_0_46:[bind(X_32,$fot(X_238)),bind(X_33,$fot(X_239)),bind(X_34,$fot(implies(implies(X_238,Z),implies(not(X_239),Z))))]]) ).
cnf(refute_0_121,plain,
is_a_theorem(implies(X_239,implies(implies(X_238,Z),implies(not(X_239),Z)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_239),X_238),implies(implies(X_238,Z),implies(not(X_239),Z)))) )],[refute_0_119,refute_0_120]) ).
cnf(refute_0_122,plain,
is_a_theorem(implies(X_251,implies(implies(X_250,X_249),implies(not(X_251),X_249)))),
inference(subst,[],[refute_0_121:[bind(Z,$fot(X_249)),bind(X_238,$fot(X_250)),bind(X_239,$fot(X_251))]]) ).
cnf(refute_0_123,plain,
is_a_theorem(implies(implies(implies(implies(X_250,X_249),implies(not(X_251),X_249)),Z),implies(X_251,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_251,implies(implies(X_250,X_249),implies(not(X_251),X_249)))) )],[refute_0_122,refute_0_118]) ).
cnf(refute_0_124,plain,
is_a_theorem(implies(implies(implies(implies(X_290,X_289),implies(not(X_291),X_289)),X_288),implies(X_291,X_288))),
inference(subst,[],[refute_0_123:[bind(Z,$fot(X_288)),bind(X_249,$fot(X_289)),bind(X_250,$fot(X_290)),bind(X_251,$fot(X_291))]]) ).
cnf(refute_0_125,plain,
( ~ is_a_theorem(implies(implies(implies(X_290,X_289),implies(not(X_291),X_289)),X_288))
| is_a_theorem(implies(X_291,X_288)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_290,X_289),implies(not(X_291),X_289)),X_288),implies(X_291,X_288))) )],[refute_0_124,refute_0_117]) ).
cnf(refute_0_126,plain,
( ~ is_a_theorem(implies(implies(implies(not(not(X_4653)),not(not(implies(not(X_4653),X_4653)))),implies(not(not(not(implies(not(X_4653),X_4653)))),not(not(implies(not(X_4653),X_4653))))),X_4653))
| is_a_theorem(implies(not(not(implies(not(X_4653),X_4653))),X_4653)) ),
inference(subst,[],[refute_0_125:[bind(X_288,$fot(X_4653)),bind(X_289,$fot(not(not(implies(not(X_4653),X_4653))))),bind(X_290,$fot(not(not(X_4653)))),bind(X_291,$fot(not(not(implies(not(X_4653),X_4653)))))]]) ).
cnf(refute_0_127,plain,
( ~ is_a_theorem(implies(implies(not(X_3215),implies(not(not(not(implies(not(X_3215),X_3215)))),not(not(implies(not(X_3215),X_3215))))),X_3215))
| is_a_theorem(implies(implies(implies(not(not(X_3215)),X_153),implies(not(not(not(implies(not(X_3215),X_3215)))),not(not(implies(not(X_3215),X_3215))))),X_3215)) ),
inference(subst,[],[refute_0_18:[bind(X_152,$fot(X_3215)),bind(X_154,$fot(not(X_3215))),bind(X_155,$fot(implies(not(not(not(implies(not(X_3215),X_3215)))),not(not(implies(not(X_3215),X_3215))))))]]) ).
cnf(refute_0_128,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(not(not(implies(not(X_3185),X_3185)))),not(not(implies(not(X_3185),X_3185)))),X_3185),implies(not(X_3185),X_3185)),X_3185))
| is_a_theorem(implies(implies(not(X_3185),implies(not(not(not(implies(not(X_3185),X_3185)))),not(not(implies(not(X_3185),X_3185))))),X_3185)) ),
inference(subst,[],[refute_0_89:[bind(X_35,$fot(not(X_3185))),bind(X_36,$fot(implies(not(not(not(implies(not(X_3185),X_3185)))),not(not(implies(not(X_3185),X_3185)))))),bind(X_37,$fot(X_3185)),bind(X_38,$fot(X_3185))]]) ).
cnf(refute_0_129,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(not(not(implies(not(X_2107),X_2107)))),not(not(implies(not(X_2107),X_2107)))),X_2677),implies(not(X_2107),X_2107)),implies(not(X_2107),X_2107)))
| is_a_theorem(implies(implies(implies(implies(not(not(not(implies(not(X_2107),X_2107)))),not(not(implies(not(X_2107),X_2107)))),X_2677),implies(not(X_2107),X_2107)),X_2107)) ),
inference(subst,[],[refute_0_93:[bind(X_2106,$fot(implies(implies(implies(not(not(not(implies(not(X_2107),X_2107)))),not(not(implies(not(X_2107),X_2107)))),X_2677),implies(not(X_2107),X_2107))))]]) ).
cnf(refute_0_130,plain,
( ~ is_a_theorem(implies(X_258,implies(implies(not(not(X_258)),not(X_258)),X_257)))
| is_a_theorem(implies(implies(implies(implies(not(not(X_258)),not(X_258)),X_257),Z),implies(X_258,Z))) ),
inference(subst,[],[refute_0_9:[bind(X,$fot(X_258)),bind(Y,$fot(implies(implies(not(not(X_258)),not(X_258)),X_257)))]]) ).
cnf(refute_0_131,plain,
is_a_theorem(implies(implies(not(X_239),X_238),implies(implies(not(not(X_239)),not(X_239)),X_238))),
inference(subst,[],[refute_0_28:[bind(X_28,$fot(not(X_239))),bind(X_29,$fot(X_238))]]) ).
cnf(refute_0_132,plain,
( ~ is_a_theorem(implies(implies(not(X_239),X_238),implies(implies(not(not(X_239)),not(X_239)),X_238)))
| is_a_theorem(implies(X_239,implies(implies(not(not(X_239)),not(X_239)),X_238))) ),
inference(subst,[],[refute_0_46:[bind(X_32,$fot(X_238)),bind(X_33,$fot(X_239)),bind(X_34,$fot(implies(implies(not(not(X_239)),not(X_239)),X_238)))]]) ).
cnf(refute_0_133,plain,
is_a_theorem(implies(X_239,implies(implies(not(not(X_239)),not(X_239)),X_238))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_239),X_238),implies(implies(not(not(X_239)),not(X_239)),X_238))) )],[refute_0_131,refute_0_132]) ).
cnf(refute_0_134,plain,
is_a_theorem(implies(X_258,implies(implies(not(not(X_258)),not(X_258)),X_257))),
inference(subst,[],[refute_0_133:[bind(X_238,$fot(X_257)),bind(X_239,$fot(X_258))]]) ).
cnf(refute_0_135,plain,
is_a_theorem(implies(implies(implies(implies(not(not(X_258)),not(X_258)),X_257),Z),implies(X_258,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_258,implies(implies(not(not(X_258)),not(X_258)),X_257))) )],[refute_0_134,refute_0_130]) ).
cnf(refute_0_136,plain,
is_a_theorem(implies(implies(implies(implies(not(not(not(X_2669))),not(not(X_2669))),X_257),X_2669),implies(not(X_2669),X_2669))),
inference(subst,[],[refute_0_135:[bind(Z,$fot(X_2669)),bind(X_258,$fot(not(X_2669)))]]) ).
cnf(refute_0_137,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(not(not(X_2669))),not(not(X_2669))),X_257),X_2669),implies(not(X_2669),X_2669)))
| is_a_theorem(implies(implies(implies(implies(not(not(not(X_2669))),not(not(X_2669))),X_257),X_2669),X_2669)) ),
inference(subst,[],[refute_0_93:[bind(X_2106,$fot(implies(implies(implies(not(not(not(X_2669))),not(not(X_2669))),X_257),X_2669))),bind(X_2107,$fot(X_2669))]]) ).
cnf(refute_0_138,plain,
is_a_theorem(implies(implies(implies(implies(not(not(not(X_2669))),not(not(X_2669))),X_257),X_2669),X_2669)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(not(not(X_2669))),not(not(X_2669))),X_257),X_2669),implies(not(X_2669),X_2669))) )],[refute_0_136,refute_0_137]) ).
cnf(refute_0_139,plain,
is_a_theorem(implies(implies(implies(implies(not(not(not(implies(not(X_2107),X_2107)))),not(not(implies(not(X_2107),X_2107)))),X_2677),implies(not(X_2107),X_2107)),implies(not(X_2107),X_2107))),
inference(subst,[],[refute_0_138:[bind(X_257,$fot(X_2677)),bind(X_2669,$fot(implies(not(X_2107),X_2107)))]]) ).
cnf(refute_0_140,plain,
is_a_theorem(implies(implies(implies(implies(not(not(not(implies(not(X_2107),X_2107)))),not(not(implies(not(X_2107),X_2107)))),X_2677),implies(not(X_2107),X_2107)),X_2107)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(not(not(implies(not(X_2107),X_2107)))),not(not(implies(not(X_2107),X_2107)))),X_2677),implies(not(X_2107),X_2107)),implies(not(X_2107),X_2107))) )],[refute_0_139,refute_0_129]) ).
cnf(refute_0_141,plain,
is_a_theorem(implies(implies(implies(implies(not(not(not(implies(not(X_3185),X_3185)))),not(not(implies(not(X_3185),X_3185)))),X_3185),implies(not(X_3185),X_3185)),X_3185)),
inference(subst,[],[refute_0_140:[bind(X_2107,$fot(X_3185)),bind(X_2677,$fot(X_3185))]]) ).
cnf(refute_0_142,plain,
is_a_theorem(implies(implies(not(X_3185),implies(not(not(not(implies(not(X_3185),X_3185)))),not(not(implies(not(X_3185),X_3185))))),X_3185)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(not(not(implies(not(X_3185),X_3185)))),not(not(implies(not(X_3185),X_3185)))),X_3185),implies(not(X_3185),X_3185)),X_3185)) )],[refute_0_141,refute_0_128]) ).
cnf(refute_0_143,plain,
is_a_theorem(implies(implies(not(X_3215),implies(not(not(not(implies(not(X_3215),X_3215)))),not(not(implies(not(X_3215),X_3215))))),X_3215)),
inference(subst,[],[refute_0_142:[bind(X_3185,$fot(X_3215))]]) ).
cnf(refute_0_144,plain,
is_a_theorem(implies(implies(implies(not(not(X_3215)),X_153),implies(not(not(not(implies(not(X_3215),X_3215)))),not(not(implies(not(X_3215),X_3215))))),X_3215)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_3215),implies(not(not(not(implies(not(X_3215),X_3215)))),not(not(implies(not(X_3215),X_3215))))),X_3215)) )],[refute_0_143,refute_0_127]) ).
cnf(refute_0_145,plain,
is_a_theorem(implies(implies(implies(not(not(X_4653)),not(not(implies(not(X_4653),X_4653)))),implies(not(not(not(implies(not(X_4653),X_4653)))),not(not(implies(not(X_4653),X_4653))))),X_4653)),
inference(subst,[],[refute_0_144:[bind(X_153,$fot(not(not(implies(not(X_4653),X_4653))))),bind(X_3215,$fot(X_4653))]]) ).
cnf(refute_0_146,plain,
is_a_theorem(implies(not(not(implies(not(X_4653),X_4653))),X_4653)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(not(X_4653)),not(not(implies(not(X_4653),X_4653)))),implies(not(not(not(implies(not(X_4653),X_4653)))),not(not(implies(not(X_4653),X_4653))))),X_4653)) )],[refute_0_145,refute_0_126]) ).
cnf(refute_0_147,plain,
is_a_theorem(implies(not(not(implies(not(X_4654),X_4654))),X_4654)),
inference(subst,[],[refute_0_146:[bind(X_4653,$fot(X_4654))]]) ).
cnf(refute_0_148,plain,
is_a_theorem(implies(implies(X_4654,not(implies(not(X_4654),X_4654))),not(implies(not(X_4654),X_4654)))),
inference(resolve,[$cnf( is_a_theorem(implies(not(not(implies(not(X_4654),X_4654))),X_4654)) )],[refute_0_147,refute_0_116]) ).
cnf(refute_0_149,plain,
is_a_theorem(implies(implies(not(X_33),not(implies(not(not(X_33)),not(X_33)))),not(implies(not(not(X_33)),not(X_33))))),
inference(subst,[],[refute_0_148:[bind(X_4654,$fot(not(X_33)))]]) ).
cnf(refute_0_150,plain,
is_a_theorem(implies(X_33,not(implies(not(not(X_33)),not(X_33))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_33),not(implies(not(not(X_33)),not(X_33)))),not(implies(not(not(X_33)),not(X_33))))) )],[refute_0_149,refute_0_115]) ).
cnf(refute_0_151,plain,
is_a_theorem(implies(not(X_2110),not(implies(not(not(not(X_2110))),not(not(X_2110)))))),
inference(subst,[],[refute_0_150:[bind(X_33,$fot(not(X_2110)))]]) ).
cnf(refute_0_152,plain,
is_a_theorem(implies(implies(not(implies(not(not(not(X_2110))),not(not(X_2110)))),X_2110),X_2110)),
inference(resolve,[$cnf( is_a_theorem(implies(not(X_2110),not(implies(not(not(not(X_2110))),not(not(X_2110)))))) )],[refute_0_151,refute_0_114]) ).
cnf(refute_0_153,plain,
is_a_theorem(implies(implies(not(implies(not(not(not(X_4658))),not(not(X_4658)))),X_4658),X_4658)),
inference(subst,[],[refute_0_152:[bind(X_2110,$fot(X_4658))]]) ).
cnf(refute_0_154,plain,
is_a_theorem(implies(not(not(X_4658)),X_4658)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(implies(not(not(not(X_4658))),not(not(X_4658)))),X_4658),X_4658)) )],[refute_0_153,refute_0_113]) ).
cnf(refute_0_155,plain,
is_a_theorem(implies(not(not(X_4659)),X_4659)),
inference(subst,[],[refute_0_154:[bind(X_4658,$fot(X_4659))]]) ).
cnf(refute_0_156,plain,
is_a_theorem(implies(implies(X_4659,not(X_4659)),not(X_4659))),
inference(resolve,[$cnf( is_a_theorem(implies(not(not(X_4659)),X_4659)) )],[refute_0_155,refute_0_103]) ).
cnf(refute_0_157,plain,
( ~ is_a_theorem(X_2280)
| ~ is_a_theorem(implies(X_2280,implies(X_2281,implies(X_2279,X_2280))))
| is_a_theorem(implies(X_2281,implies(X_2279,X_2280))) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(X_2280)),bind(Y,$fot(implies(X_2281,implies(X_2279,X_2280))))]]) ).
cnf(refute_0_158,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_2276),X_2277),implies(not(X_2277),X_2277)),implies(X_2278,implies(X_2276,X_2277))))
| is_a_theorem(implies(X_2277,implies(X_2278,implies(X_2276,X_2277)))) ),
inference(subst,[],[refute_0_125:[bind(X_288,$fot(implies(X_2278,implies(X_2276,X_2277)))),bind(X_289,$fot(X_2277)),bind(X_290,$fot(not(X_2276))),bind(X_291,$fot(X_2277))]]) ).
cnf(refute_0_159,plain,
( ~ is_a_theorem(implies(implies(X_2151,implies(not(X_2152),X_2152)),implies(X_2153,implies(X_2151,X_2152))))
| is_a_theorem(implies(implies(implies(not(X_2151),X_153),implies(not(X_2152),X_2152)),implies(X_2153,implies(X_2151,X_2152)))) ),
inference(subst,[],[refute_0_18:[bind(X_152,$fot(implies(X_2153,implies(X_2151,X_2152)))),bind(X_154,$fot(X_2151)),bind(X_155,$fot(implies(not(X_2152),X_2152)))]]) ).
cnf(refute_0_160,plain,
is_a_theorem(implies(implies(implies(implies(not(X_2082),X_2082),X_2082),implies(X_2080,X_2082)),implies(X_248,implies(X_2080,X_2082)))),
inference(subst,[],[refute_0_53:[bind(X_1290,$fot(implies(X_2080,X_2082))),bind(X_246,$fot(X_2082))]]) ).
cnf(refute_0_161,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(X_2082),X_2082),X_2082),implies(X_2080,X_2082)),implies(X_248,implies(X_2080,X_2082))))
| is_a_theorem(implies(implies(X_2080,implies(not(X_2082),X_2082)),implies(X_248,implies(X_2080,X_2082)))) ),
inference(subst,[],[refute_0_89:[bind(X_35,$fot(X_2080)),bind(X_36,$fot(implies(not(X_2082),X_2082))),bind(X_37,$fot(X_2082)),bind(X_38,$fot(implies(X_248,implies(X_2080,X_2082))))]]) ).
cnf(refute_0_162,plain,
is_a_theorem(implies(implies(X_2080,implies(not(X_2082),X_2082)),implies(X_248,implies(X_2080,X_2082)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(X_2082),X_2082),X_2082),implies(X_2080,X_2082)),implies(X_248,implies(X_2080,X_2082)))) )],[refute_0_160,refute_0_161]) ).
cnf(refute_0_163,plain,
is_a_theorem(implies(implies(X_2151,implies(not(X_2152),X_2152)),implies(X_2153,implies(X_2151,X_2152)))),
inference(subst,[],[refute_0_162:[bind(X_2080,$fot(X_2151)),bind(X_2082,$fot(X_2152)),bind(X_248,$fot(X_2153))]]) ).
cnf(refute_0_164,plain,
is_a_theorem(implies(implies(implies(not(X_2151),X_153),implies(not(X_2152),X_2152)),implies(X_2153,implies(X_2151,X_2152)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_2151,implies(not(X_2152),X_2152)),implies(X_2153,implies(X_2151,X_2152)))) )],[refute_0_163,refute_0_159]) ).
cnf(refute_0_165,plain,
is_a_theorem(implies(implies(implies(not(X_2276),X_2277),implies(not(X_2277),X_2277)),implies(X_2278,implies(X_2276,X_2277)))),
inference(subst,[],[refute_0_164:[bind(X_153,$fot(X_2277)),bind(X_2151,$fot(X_2276)),bind(X_2152,$fot(X_2277)),bind(X_2153,$fot(X_2278))]]) ).
cnf(refute_0_166,plain,
is_a_theorem(implies(X_2277,implies(X_2278,implies(X_2276,X_2277)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_2276),X_2277),implies(not(X_2277),X_2277)),implies(X_2278,implies(X_2276,X_2277)))) )],[refute_0_165,refute_0_158]) ).
cnf(refute_0_167,plain,
is_a_theorem(implies(X_2280,implies(X_2281,implies(X_2279,X_2280)))),
inference(subst,[],[refute_0_166:[bind(X_2276,$fot(X_2279)),bind(X_2277,$fot(X_2280)),bind(X_2278,$fot(X_2281))]]) ).
cnf(refute_0_168,plain,
( ~ is_a_theorem(X_2280)
| is_a_theorem(implies(X_2281,implies(X_2279,X_2280))) ),
inference(resolve,[$cnf( is_a_theorem(implies(X_2280,implies(X_2281,implies(X_2279,X_2280)))) )],[refute_0_167,refute_0_157]) ).
cnf(refute_0_169,plain,
( ~ is_a_theorem(implies(implies(X_4659,not(X_4659)),not(X_4659)))
| is_a_theorem(implies(X_9637,implies(X_9635,implies(implies(X_4659,not(X_4659)),not(X_4659))))) ),
inference(subst,[],[refute_0_168:[bind(X_2279,$fot(X_9635)),bind(X_2280,$fot(implies(implies(X_4659,not(X_4659)),not(X_4659)))),bind(X_2281,$fot(X_9637))]]) ).
cnf(refute_0_170,plain,
is_a_theorem(implies(X_9637,implies(X_9635,implies(implies(X_4659,not(X_4659)),not(X_4659))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_4659,not(X_4659)),not(X_4659))) )],[refute_0_156,refute_0_169]) ).
cnf(refute_0_171,plain,
is_a_theorem(implies(not(implies(X_23235,implies(implies(X_4659,not(X_4659)),not(X_4659)))),implies(X_23235,implies(implies(X_4659,not(X_4659)),not(X_4659))))),
inference(subst,[],[refute_0_170:[bind(X_9635,$fot(X_23235)),bind(X_9637,$fot(not(implies(X_23235,implies(implies(X_4659,not(X_4659)),not(X_4659))))))]]) ).
cnf(refute_0_172,plain,
( ~ is_a_theorem(implies(implies(not(implies(X_98,X_99)),implies(X_98,X_99)),implies(implies(X_99,X_100),implies(X_98,X_100))))
| ~ is_a_theorem(implies(not(implies(X_98,X_99)),implies(X_98,X_99)))
| is_a_theorem(implies(implies(X_99,X_100),implies(X_98,X_100))) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(implies(not(implies(X_98,X_99)),implies(X_98,X_99)))),bind(Y,$fot(implies(implies(X_99,X_100),implies(X_98,X_100))))]]) ).
cnf(refute_0_173,plain,
( ~ is_a_theorem(implies(X_30,X_31))
| ~ is_a_theorem(implies(implies(X_30,X_31),implies(implies(not(X_30),X_30),X_31)))
| is_a_theorem(implies(implies(not(X_30),X_30),X_31)) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(implies(X_30,X_31))),bind(Y,$fot(implies(implies(not(X_30),X_30),X_31)))]]) ).
cnf(refute_0_174,plain,
( ~ is_a_theorem(implies(X_30,X_31))
| is_a_theorem(implies(implies(not(X_30),X_30),X_31)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_30,X_31),implies(implies(not(X_30),X_30),X_31))) )],[refute_0_29,refute_0_173]) ).
cnf(refute_0_175,plain,
( ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))))
| is_a_theorem(implies(implies(not(implies(X,Y)),implies(X,Y)),implies(implies(Y,Z),implies(X,Z)))) ),
inference(subst,[],[refute_0_174:[bind(X_30,$fot(implies(X,Y))),bind(X_31,$fot(implies(implies(Y,Z),implies(X,Z))))]]) ).
cnf(refute_0_176,plain,
is_a_theorem(implies(implies(not(implies(X,Y)),implies(X,Y)),implies(implies(Y,Z),implies(X,Z)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )],[refute_0_7,refute_0_175]) ).
cnf(refute_0_177,plain,
is_a_theorem(implies(implies(not(implies(X_98,X_99)),implies(X_98,X_99)),implies(implies(X_99,X_100),implies(X_98,X_100)))),
inference(subst,[],[refute_0_176:[bind(X,$fot(X_98)),bind(Y,$fot(X_99)),bind(Z,$fot(X_100))]]) ).
cnf(refute_0_178,plain,
( ~ is_a_theorem(implies(not(implies(X_98,X_99)),implies(X_98,X_99)))
| is_a_theorem(implies(implies(X_99,X_100),implies(X_98,X_100))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(implies(X_98,X_99)),implies(X_98,X_99)),implies(implies(X_99,X_100),implies(X_98,X_100)))) )],[refute_0_177,refute_0_172]) ).
cnf(refute_0_179,plain,
( ~ is_a_theorem(implies(not(implies(X_23235,implies(implies(X_4659,not(X_4659)),not(X_4659)))),implies(X_23235,implies(implies(X_4659,not(X_4659)),not(X_4659)))))
| is_a_theorem(implies(implies(implies(implies(X_4659,not(X_4659)),not(X_4659)),X_23234),implies(X_23235,X_23234))) ),
inference(subst,[],[refute_0_178:[bind(X_100,$fot(X_23234)),bind(X_98,$fot(X_23235)),bind(X_99,$fot(implies(implies(X_4659,not(X_4659)),not(X_4659))))]]) ).
cnf(refute_0_180,plain,
is_a_theorem(implies(implies(implies(implies(X_4659,not(X_4659)),not(X_4659)),X_23234),implies(X_23235,X_23234))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(X_23235,implies(implies(X_4659,not(X_4659)),not(X_4659)))),implies(X_23235,implies(implies(X_4659,not(X_4659)),not(X_4659))))) )],[refute_0_171,refute_0_179]) ).
cnf(refute_0_181,plain,
is_a_theorem(implies(implies(implies(implies(X_23247,not(X_23247)),not(X_23247)),implies(X_35,not(X_23247))),implies(X_23246,implies(X_35,not(X_23247))))),
inference(subst,[],[refute_0_180:[bind(X_23234,$fot(implies(X_35,not(X_23247)))),bind(X_23235,$fot(X_23246)),bind(X_4659,$fot(X_23247))]]) ).
cnf(refute_0_182,plain,
is_a_theorem(implies(implies(X_35,implies(X_23247,not(X_23247))),implies(X_23246,implies(X_35,not(X_23247))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_23247,not(X_23247)),not(X_23247)),implies(X_35,not(X_23247))),implies(X_23246,implies(X_35,not(X_23247))))) )],[refute_0_181,refute_0_96]) ).
cnf(refute_0_183,plain,
is_a_theorem(implies(implies(implies(X_36,not(X_31727)),implies(X_31727,not(X_31727))),implies(X_31726,implies(implies(X_36,not(X_31727)),not(X_31727))))),
inference(subst,[],[refute_0_182:[bind(X_23246,$fot(X_31726)),bind(X_23247,$fot(X_31727)),bind(X_35,$fot(implies(X_36,not(X_31727))))]]) ).
cnf(refute_0_184,plain,
is_a_theorem(implies(implies(X_31727,X_36),implies(X_31726,implies(implies(X_36,not(X_31727)),not(X_31727))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_36,not(X_31727)),implies(X_31727,not(X_31727))),implies(X_31726,implies(implies(X_36,not(X_31727)),not(X_31727))))) )],[refute_0_183,refute_0_95]) ).
cnf(refute_0_185,plain,
is_a_theorem(implies(implies(X_31730,X_31731),implies(not(implies(implies(X_31731,not(X_31730)),not(X_31730))),implies(implies(X_31731,not(X_31730)),not(X_31730))))),
inference(subst,[],[refute_0_184:[bind(X_31726,$fot(not(implies(implies(X_31731,not(X_31730)),not(X_31730))))),bind(X_31727,$fot(X_31730)),bind(X_36,$fot(X_31731))]]) ).
cnf(refute_0_186,plain,
is_a_theorem(implies(implies(X_31730,X_31731),implies(implies(X_31731,not(X_31730)),not(X_31730)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_31730,X_31731),implies(not(implies(implies(X_31731,not(X_31730)),not(X_31730))),implies(implies(X_31731,not(X_31730)),not(X_31730))))) )],[refute_0_185,refute_0_94]) ).
cnf(refute_0_187,plain,
is_a_theorem(implies(implies(x,y),implies(implies(y,not(x)),not(x)))),
inference(subst,[],[refute_0_186:[bind(X_31730,$fot(x)),bind(X_31731,$fot(y))]]) ).
cnf(refute_0_188,plain,
$false,
inference(resolve,[$cnf( is_a_theorem(implies(implies(x,y),implies(implies(y,not(x)),not(x)))) )],[refute_0_187,refute_0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL382+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.04 % Command : metis --show proof --show saturation %s
% 0.10/0.37 % Computer : n013.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Fri Sep 4 14:54:04 UTC 2026
% 0.15/0.37 % CPUTime :
% 0.15/0.38 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 114.25/114.52 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 114.25/114.52
% 114.25/114.52 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 114.25/114.56
%------------------------------------------------------------------------------