%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : LCL256-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n007.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:21 PM UTC 2026
% Result : Unsatisfiable 6.16s 6.47s
% Output : CNFRefutation 6.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 5
% Syntax : Number of clauses : 173 ( 104 unt; 0 nHn; 46 RR)
% Number of literals : 254 ( 0 equ; 82 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 3 ( 3 usr; 1 con; 0-2 aty)
% Number of variables : 439 ( 79 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) ).
cnf(cn_1,axiom,
is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) ).
cnf(cn_2,axiom,
is_a_theorem(implies(implies(not(X),X),X)) ).
cnf(cn_3,axiom,
is_a_theorem(implies(X,implies(not(X),Y))) ).
cnf(prove_not_not_implies,negated_conjecture,
~ is_a_theorem(not(not(implies(p,p)))) ).
cnf(refute_0_0,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_26),X_25),X_27),implies(X_26,X_27)))
| ~ is_a_theorem(implies(implies(not(X_26),X_25),X_27))
| is_a_theorem(implies(X_26,X_27)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(not(X_26),X_25),X_27))),bind(Y,$fot(implies(X_26,X_27)))]]) ).
cnf(refute_0_1,plain,
is_a_theorem(implies(X_20,implies(not(X_20),Y))),
inference(subst,[],[cn_3:[bind(X,$fot(X_20))]]) ).
cnf(refute_0_2,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,[],[condensed_detachment:[bind(X,$fot(implies(X,Y))),bind(Y,$fot(implies(implies(Y,Z),implies(X,Z))))]]) ).
cnf(refute_0_3,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)))) )],[cn_1,refute_0_2]) ).
cnf(refute_0_4,plain,
( ~ is_a_theorem(implies(X_20,implies(not(X_20),Y)))
| is_a_theorem(implies(implies(implies(not(X_20),Y),X_22),implies(X_20,X_22))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(X_20)),bind(Y,$fot(implies(not(X_20),Y))),bind(Z,$fot(X_22))]]) ).
cnf(refute_0_5,plain,
is_a_theorem(implies(implies(implies(not(X_20),Y),X_22),implies(X_20,X_22))),
inference(resolve,[$cnf( is_a_theorem(implies(X_20,implies(not(X_20),Y))) )],[refute_0_1,refute_0_4]) ).
cnf(refute_0_6,plain,
is_a_theorem(implies(implies(implies(not(X_26),X_25),X_27),implies(X_26,X_27))),
inference(subst,[],[refute_0_5:[bind(Y,$fot(X_25)),bind(X_20,$fot(X_26)),bind(X_22,$fot(X_27))]]) ).
cnf(refute_0_7,plain,
( ~ is_a_theorem(implies(implies(not(X_26),X_25),X_27))
| is_a_theorem(implies(X_26,X_27)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_26),X_25),X_27),implies(X_26,X_27))) )],[refute_0_6,refute_0_0]) ).
cnf(refute_0_8,plain,
( ~ is_a_theorem(implies(implies(not(not(not(X_3070))),not(not(X_3070))),X_3070))
| is_a_theorem(implies(not(not(X_3070)),X_3070)) ),
inference(subst,[],[refute_0_7:[bind(X_25,$fot(not(not(X_3070)))),bind(X_26,$fot(not(not(X_3070)))),bind(X_27,$fot(X_3070))]]) ).
cnf(refute_0_9,plain,
( ~ is_a_theorem(implies(implies(not(implies(not(not(not(X_3069))),not(not(X_3069)))),X_3069),X_3069))
| is_a_theorem(implies(implies(not(not(not(X_3069))),not(not(X_3069))),X_3069)) ),
inference(subst,[],[refute_0_7:[bind(X_25,$fot(X_3069)),bind(X_26,$fot(implies(not(not(not(X_3069))),not(not(X_3069))))),bind(X_27,$fot(X_3069))]]) ).
cnf(refute_0_10,plain,
( ~ is_a_theorem(implies(X_2330,implies(not(X_2331),X_2331)))
| ~ is_a_theorem(implies(implies(X_2330,implies(not(X_2331),X_2331)),implies(X_2330,X_2331)))
| is_a_theorem(implies(X_2330,X_2331)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X_2330,implies(not(X_2331),X_2331)))),bind(Y,$fot(implies(X_2330,X_2331)))]]) ).
cnf(refute_0_11,plain,
( ~ is_a_theorem(implies(implies(implies(not(not(X_376)),X_377),X_376),X_376))
| ~ is_a_theorem(implies(implies(not(not(X_376)),X_377),X_376))
| is_a_theorem(X_376) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(not(not(X_376)),X_377),X_376))),bind(Y,$fot(X_376))]]) ).
cnf(refute_0_12,plain,
is_a_theorem(implies(implies(not(X_372),X_372),X_372)),
inference(subst,[],[cn_2:[bind(X,$fot(X_372))]]) ).
cnf(refute_0_13,plain,
( ~ is_a_theorem(implies(implies(X_48,X_49),X_46))
| ~ is_a_theorem(implies(implies(implies(X_48,X_49),X_46),implies(implies(implies(not(X_48),X_47),X_49),X_46)))
| is_a_theorem(implies(implies(implies(not(X_48),X_47),X_49),X_46)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_48,X_49),X_46))),bind(Y,$fot(implies(implies(implies(not(X_48),X_47),X_49),X_46)))]]) ).
cnf(refute_0_14,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_26),X_25),X_27),implies(X_26,X_27)))
| is_a_theorem(implies(implies(implies(X_26,X_27),Z),implies(implies(implies(not(X_26),X_25),X_27),Z))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(implies(implies(not(X_26),X_25),X_27))),bind(Y,$fot(implies(X_26,X_27)))]]) ).
cnf(refute_0_15,plain,
is_a_theorem(implies(implies(implies(X_26,X_27),Z),implies(implies(implies(not(X_26),X_25),X_27),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_26),X_25),X_27),implies(X_26,X_27))) )],[refute_0_6,refute_0_14]) ).
cnf(refute_0_16,plain,
is_a_theorem(implies(implies(implies(X_48,X_49),X_46),implies(implies(implies(not(X_48),X_47),X_49),X_46))),
inference(subst,[],[refute_0_15:[bind(Z,$fot(X_46)),bind(X_25,$fot(X_47)),bind(X_26,$fot(X_48)),bind(X_27,$fot(X_49))]]) ).
cnf(refute_0_17,plain,
( ~ is_a_theorem(implies(implies(X_48,X_49),X_46))
| is_a_theorem(implies(implies(implies(not(X_48),X_47),X_49),X_46)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_48,X_49),X_46),implies(implies(implies(not(X_48),X_47),X_49),X_46))) )],[refute_0_16,refute_0_13]) ).
cnf(refute_0_18,plain,
( ~ is_a_theorem(implies(implies(not(X_372),X_372),X_372))
| is_a_theorem(implies(implies(implies(not(not(X_372)),X_373),X_372),X_372)) ),
inference(subst,[],[refute_0_17:[bind(X_46,$fot(X_372)),bind(X_47,$fot(X_373)),bind(X_48,$fot(not(X_372))),bind(X_49,$fot(X_372))]]) ).
cnf(refute_0_19,plain,
is_a_theorem(implies(implies(implies(not(not(X_372)),X_373),X_372),X_372)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_372),X_372),X_372)) )],[refute_0_12,refute_0_18]) ).
cnf(refute_0_20,plain,
is_a_theorem(implies(implies(implies(not(not(X_376)),X_377),X_376),X_376)),
inference(subst,[],[refute_0_19:[bind(X_372,$fot(X_376)),bind(X_373,$fot(X_377))]]) ).
cnf(refute_0_21,plain,
( ~ is_a_theorem(implies(implies(not(not(X_376)),X_377),X_376))
| is_a_theorem(X_376) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(not(X_376)),X_377),X_376),X_376)) )],[refute_0_20,refute_0_11]) ).
cnf(refute_0_22,plain,
( ~ is_a_theorem(implies(implies(not(not(implies(implies(implies(implies(not(X_1772),X_1772),X_1772),X_1773),X_1773))),X_377),implies(implies(implies(implies(not(X_1772),X_1772),X_1772),X_1773),X_1773)))
| is_a_theorem(implies(implies(implies(implies(not(X_1772),X_1772),X_1772),X_1773),X_1773)) ),
inference(subst,[],[refute_0_21:[bind(X_376,$fot(implies(implies(implies(implies(not(X_1772),X_1772),X_1772),X_1773),X_1773)))]]) ).
cnf(refute_0_23,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(X_72),X_72),X_73),X_71),implies(implies(X_72,X_73),X_71)))
| ~ is_a_theorem(implies(implies(implies(not(X_72),X_72),X_73),X_71))
| is_a_theorem(implies(implies(X_72,X_73),X_71)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(not(X_72),X_72),X_73),X_71))),bind(Y,$fot(implies(implies(X_72,X_73),X_71)))]]) ).
cnf(refute_0_24,plain,
( ~ is_a_theorem(implies(implies(X_23,X_24),implies(implies(not(X_23),X_23),X_24)))
| is_a_theorem(implies(implies(implies(implies(not(X_23),X_23),X_24),Z),implies(implies(X_23,X_24),Z))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(implies(X_23,X_24))),bind(Y,$fot(implies(implies(not(X_23),X_23),X_24)))]]) ).
cnf(refute_0_25,plain,
is_a_theorem(implies(implies(not(X_21),X_21),X_21)),
inference(subst,[],[cn_2:[bind(X,$fot(X_21))]]) ).
cnf(refute_0_26,plain,
( ~ is_a_theorem(implies(implies(not(X_21),X_21),X_21))
| is_a_theorem(implies(implies(X_21,X_22),implies(implies(not(X_21),X_21),X_22))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(implies(not(X_21),X_21))),bind(Y,$fot(X_21)),bind(Z,$fot(X_22))]]) ).
cnf(refute_0_27,plain,
is_a_theorem(implies(implies(X_21,X_22),implies(implies(not(X_21),X_21),X_22))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_21),X_21),X_21)) )],[refute_0_25,refute_0_26]) ).
cnf(refute_0_28,plain,
is_a_theorem(implies(implies(X_23,X_24),implies(implies(not(X_23),X_23),X_24))),
inference(subst,[],[refute_0_27:[bind(X_21,$fot(X_23)),bind(X_22,$fot(X_24))]]) ).
cnf(refute_0_29,plain,
is_a_theorem(implies(implies(implies(implies(not(X_23),X_23),X_24),Z),implies(implies(X_23,X_24),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_23,X_24),implies(implies(not(X_23),X_23),X_24))) )],[refute_0_28,refute_0_24]) ).
cnf(refute_0_30,plain,
is_a_theorem(implies(implies(implies(implies(not(X_72),X_72),X_73),X_71),implies(implies(X_72,X_73),X_71))),
inference(subst,[],[refute_0_29:[bind(Z,$fot(X_71)),bind(X_23,$fot(X_72)),bind(X_24,$fot(X_73))]]) ).
cnf(refute_0_31,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_72),X_72),X_73),X_71))
| is_a_theorem(implies(implies(X_72,X_73),X_71)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(X_72),X_72),X_73),X_71),implies(implies(X_72,X_73),X_71))) )],[refute_0_30,refute_0_23]) ).
cnf(refute_0_32,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_1421),X_1421),X_1420),implies(implies(implies(implies(not(X_1422),X_1422),X_1422),X_1421),X_1420)))
| is_a_theorem(implies(implies(X_1421,X_1420),implies(implies(implies(implies(not(X_1422),X_1422),X_1422),X_1421),X_1420))) ),
inference(subst,[],[refute_0_31:[bind(X_71,$fot(implies(implies(implies(implies(not(X_1422),X_1422),X_1422),X_1421),X_1420))),bind(X_72,$fot(X_1421)),bind(X_73,$fot(X_1420))]]) ).
cnf(refute_0_33,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(X_1395),X_1395),X_1395),X_1394),implies(X_1396,X_1394)))
| is_a_theorem(implies(implies(implies(X_1396,X_1394),Z),implies(implies(implies(implies(not(X_1395),X_1395),X_1395),X_1394),Z))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(implies(implies(implies(not(X_1395),X_1395),X_1395),X_1394))),bind(Y,$fot(implies(X_1396,X_1394)))]]) ).
cnf(refute_0_34,plain,
( ~ is_a_theorem(implies(X_176,implies(not(implies(implies(not(X_174),X_174),X_174)),X_175)))
| is_a_theorem(implies(implies(implies(not(implies(implies(not(X_174),X_174),X_174)),X_175),Z),implies(X_176,Z))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(X_176)),bind(Y,$fot(implies(not(implies(implies(not(X_174),X_174),X_174)),X_175)))]]) ).
cnf(refute_0_35,plain,
is_a_theorem(implies(X_6,implies(not(X_6),Y))),
inference(subst,[],[cn_3:[bind(X,$fot(X_6))]]) ).
cnf(refute_0_36,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,[],[condensed_detachment:[bind(X,$fot(X_6)),bind(Y,$fot(implies(not(X_6),Y)))]]) ).
cnf(refute_0_37,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_35,refute_0_36]) ).
cnf(refute_0_38,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_37:[bind(Y,$fot(X_9)),bind(X_6,$fot(implies(implies(not(X),X),X)))]]) ).
cnf(refute_0_39,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)) )],[cn_2,refute_0_38]) ).
cnf(refute_0_40,plain,
is_a_theorem(implies(not(implies(implies(not(X),X),X)),X_21)),
inference(subst,[],[refute_0_39:[bind(X_9,$fot(X_21))]]) ).
cnf(refute_0_41,plain,
( ~ is_a_theorem(implies(not(implies(implies(not(X),X),X)),X_21))
| is_a_theorem(implies(implies(X_21,X_22),implies(not(implies(implies(not(X),X),X)),X_22))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(not(implies(implies(not(X),X),X)))),bind(Y,$fot(X_21)),bind(Z,$fot(X_22))]]) ).
cnf(refute_0_42,plain,
is_a_theorem(implies(implies(X_21,X_22),implies(not(implies(implies(not(X),X),X)),X_22))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(implies(not(X),X),X)),X_21)) )],[refute_0_40,refute_0_41]) ).
cnf(refute_0_43,plain,
is_a_theorem(implies(implies(not(X_169),X_168),implies(not(implies(implies(not(X),X),X)),X_168))),
inference(subst,[],[refute_0_42:[bind(X_21,$fot(not(X_169))),bind(X_22,$fot(X_168))]]) ).
cnf(refute_0_44,plain,
( ~ is_a_theorem(implies(implies(not(X_169),X_168),implies(not(implies(implies(not(X),X),X)),X_168)))
| is_a_theorem(implies(X_169,implies(not(implies(implies(not(X),X),X)),X_168))) ),
inference(subst,[],[refute_0_7:[bind(X_25,$fot(X_168)),bind(X_26,$fot(X_169)),bind(X_27,$fot(implies(not(implies(implies(not(X),X),X)),X_168)))]]) ).
cnf(refute_0_45,plain,
is_a_theorem(implies(X_169,implies(not(implies(implies(not(X),X),X)),X_168))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_169),X_168),implies(not(implies(implies(not(X),X),X)),X_168))) )],[refute_0_43,refute_0_44]) ).
cnf(refute_0_46,plain,
is_a_theorem(implies(X_176,implies(not(implies(implies(not(X_174),X_174),X_174)),X_175))),
inference(subst,[],[refute_0_45:[bind(X,$fot(X_174)),bind(X_168,$fot(X_175)),bind(X_169,$fot(X_176))]]) ).
cnf(refute_0_47,plain,
is_a_theorem(implies(implies(implies(not(implies(implies(not(X_174),X_174),X_174)),X_175),Z),implies(X_176,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_176,implies(not(implies(implies(not(X_174),X_174),X_174)),X_175))) )],[refute_0_46,refute_0_34]) ).
cnf(refute_0_48,plain,
is_a_theorem(implies(implies(implies(not(implies(implies(not(X_174),X_174),X_174)),implies(implies(not(X_174),X_174),X_174)),X_1387),implies(X_176,X_1387))),
inference(subst,[],[refute_0_47:[bind(Z,$fot(X_1387)),bind(X_175,$fot(implies(implies(not(X_174),X_174),X_174)))]]) ).
cnf(refute_0_49,plain,
( ~ is_a_theorem(implies(implies(implies(not(implies(implies(not(X_174),X_174),X_174)),implies(implies(not(X_174),X_174),X_174)),X_1387),implies(X_176,X_1387)))
| is_a_theorem(implies(implies(implies(implies(not(X_174),X_174),X_174),X_1387),implies(X_176,X_1387))) ),
inference(subst,[],[refute_0_31:[bind(X_71,$fot(implies(X_176,X_1387))),bind(X_72,$fot(implies(implies(not(X_174),X_174),X_174))),bind(X_73,$fot(X_1387))]]) ).
cnf(refute_0_50,plain,
is_a_theorem(implies(implies(implies(implies(not(X_174),X_174),X_174),X_1387),implies(X_176,X_1387))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(implies(implies(not(X_174),X_174),X_174)),implies(implies(not(X_174),X_174),X_174)),X_1387),implies(X_176,X_1387))) )],[refute_0_48,refute_0_49]) ).
cnf(refute_0_51,plain,
is_a_theorem(implies(implies(implies(implies(not(X_1395),X_1395),X_1395),X_1394),implies(X_1396,X_1394))),
inference(subst,[],[refute_0_50:[bind(X_1387,$fot(X_1394)),bind(X_174,$fot(X_1395)),bind(X_176,$fot(X_1396))]]) ).
cnf(refute_0_52,plain,
is_a_theorem(implies(implies(implies(X_1396,X_1394),Z),implies(implies(implies(implies(not(X_1395),X_1395),X_1395),X_1394),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(X_1395),X_1395),X_1395),X_1394),implies(X_1396,X_1394))) )],[refute_0_51,refute_0_33]) ).
cnf(refute_0_53,plain,
is_a_theorem(implies(implies(implies(not(X_1421),X_1421),X_1420),implies(implies(implies(implies(not(X_1422),X_1422),X_1422),X_1421),X_1420))),
inference(subst,[],[refute_0_52:[bind(Z,$fot(X_1420)),bind(X_1394,$fot(X_1421)),bind(X_1395,$fot(X_1422)),bind(X_1396,$fot(not(X_1421)))]]) ).
cnf(refute_0_54,plain,
is_a_theorem(implies(implies(X_1421,X_1420),implies(implies(implies(implies(not(X_1422),X_1422),X_1422),X_1421),X_1420))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_1421),X_1421),X_1420),implies(implies(implies(implies(not(X_1422),X_1422),X_1422),X_1421),X_1420))) )],[refute_0_53,refute_0_32]) ).
cnf(refute_0_55,plain,
is_a_theorem(implies(implies(X_1763,X_1763),implies(implies(implies(implies(not(X_1422),X_1422),X_1422),X_1763),X_1763))),
inference(subst,[],[refute_0_54:[bind(X_1420,$fot(X_1763)),bind(X_1421,$fot(X_1763))]]) ).
cnf(refute_0_56,plain,
( ~ is_a_theorem(implies(implies(X_1392,X_1392),X_1391))
| ~ is_a_theorem(implies(implies(implies(X_1392,X_1392),X_1391),implies(X_1393,X_1391)))
| is_a_theorem(implies(X_1393,X_1391)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_1392,X_1392),X_1391))),bind(Y,$fot(implies(X_1393,X_1391)))]]) ).
cnf(refute_0_57,plain,
( ~ is_a_theorem(implies(X_224,implies(not(implies(X_223,X_223)),X_222)))
| is_a_theorem(implies(implies(implies(not(implies(X_223,X_223)),X_222),Z),implies(X_224,Z))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(X_224)),bind(Y,$fot(implies(not(implies(X_223,X_223)),X_222)))]]) ).
cnf(refute_0_58,plain,
( ~ is_a_theorem(implies(implies(not(X_26),X_219),implies(not(implies(X_221,X_221)),X_219)))
| is_a_theorem(implies(X_26,implies(not(implies(X_221,X_221)),X_219))) ),
inference(subst,[],[refute_0_7:[bind(X_25,$fot(X_219)),bind(X_27,$fot(implies(not(implies(X_221,X_221)),X_219)))]]) ).
cnf(refute_0_59,plain,
( ~ is_a_theorem(implies(not(implies(X_173,X_173)),X_172))
| is_a_theorem(implies(implies(X_172,Z),implies(not(implies(X_173,X_173)),Z))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(not(implies(X_173,X_173)))),bind(Y,$fot(X_172))]]) ).
cnf(refute_0_60,plain,
( ~ is_a_theorem(implies(X_171,X_171))
| is_a_theorem(implies(not(implies(X_171,X_171)),Y)) ),
inference(subst,[],[refute_0_37:[bind(X_6,$fot(implies(X_171,X_171)))]]) ).
cnf(refute_0_61,plain,
is_a_theorem(implies(implies(not(X_170),X_170),X_170)),
inference(subst,[],[cn_2:[bind(X,$fot(X_170))]]) ).
cnf(refute_0_62,plain,
( ~ is_a_theorem(implies(implies(not(X_170),X_170),X_170))
| is_a_theorem(implies(X_170,X_170)) ),
inference(subst,[],[refute_0_7:[bind(X_25,$fot(X_170)),bind(X_26,$fot(X_170)),bind(X_27,$fot(X_170))]]) ).
cnf(refute_0_63,plain,
is_a_theorem(implies(X_170,X_170)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_170),X_170),X_170)) )],[refute_0_61,refute_0_62]) ).
cnf(refute_0_64,plain,
is_a_theorem(implies(X_171,X_171)),
inference(subst,[],[refute_0_63:[bind(X_170,$fot(X_171))]]) ).
cnf(refute_0_65,plain,
is_a_theorem(implies(not(implies(X_171,X_171)),Y)),
inference(resolve,[$cnf( is_a_theorem(implies(X_171,X_171)) )],[refute_0_64,refute_0_60]) ).
cnf(refute_0_66,plain,
is_a_theorem(implies(not(implies(X_173,X_173)),X_172)),
inference(subst,[],[refute_0_65:[bind(Y,$fot(X_172)),bind(X_171,$fot(X_173))]]) ).
cnf(refute_0_67,plain,
is_a_theorem(implies(implies(X_172,Z),implies(not(implies(X_173,X_173)),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(X_173,X_173)),X_172)) )],[refute_0_66,refute_0_59]) ).
cnf(refute_0_68,plain,
is_a_theorem(implies(implies(not(X_26),X_219),implies(not(implies(X_221,X_221)),X_219))),
inference(subst,[],[refute_0_67:[bind(Z,$fot(X_219)),bind(X_172,$fot(not(X_26))),bind(X_173,$fot(X_221))]]) ).
cnf(refute_0_69,plain,
is_a_theorem(implies(X_26,implies(not(implies(X_221,X_221)),X_219))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_26),X_219),implies(not(implies(X_221,X_221)),X_219))) )],[refute_0_68,refute_0_58]) ).
cnf(refute_0_70,plain,
is_a_theorem(implies(X_224,implies(not(implies(X_223,X_223)),X_222))),
inference(subst,[],[refute_0_69:[bind(X_219,$fot(X_222)),bind(X_221,$fot(X_223)),bind(X_26,$fot(X_224))]]) ).
cnf(refute_0_71,plain,
is_a_theorem(implies(implies(implies(not(implies(X_223,X_223)),X_222),Z),implies(X_224,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_224,implies(not(implies(X_223,X_223)),X_222))) )],[refute_0_70,refute_0_57]) ).
cnf(refute_0_72,plain,
is_a_theorem(implies(implies(implies(not(implies(X_223,X_223)),implies(X_223,X_223)),X_1387),implies(X_224,X_1387))),
inference(subst,[],[refute_0_71:[bind(Z,$fot(X_1387)),bind(X_222,$fot(implies(X_223,X_223)))]]) ).
cnf(refute_0_73,plain,
( ~ is_a_theorem(implies(implies(implies(not(implies(X_223,X_223)),implies(X_223,X_223)),X_1387),implies(X_224,X_1387)))
| is_a_theorem(implies(implies(implies(X_223,X_223),X_1387),implies(X_224,X_1387))) ),
inference(subst,[],[refute_0_31:[bind(X_71,$fot(implies(X_224,X_1387))),bind(X_72,$fot(implies(X_223,X_223))),bind(X_73,$fot(X_1387))]]) ).
cnf(refute_0_74,plain,
is_a_theorem(implies(implies(implies(X_223,X_223),X_1387),implies(X_224,X_1387))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(implies(X_223,X_223)),implies(X_223,X_223)),X_1387),implies(X_224,X_1387))) )],[refute_0_72,refute_0_73]) ).
cnf(refute_0_75,plain,
is_a_theorem(implies(implies(implies(X_1392,X_1392),X_1391),implies(X_1393,X_1391))),
inference(subst,[],[refute_0_74:[bind(X_1387,$fot(X_1391)),bind(X_223,$fot(X_1392)),bind(X_224,$fot(X_1393))]]) ).
cnf(refute_0_76,plain,
( ~ is_a_theorem(implies(implies(X_1392,X_1392),X_1391))
| is_a_theorem(implies(X_1393,X_1391)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_1392,X_1392),X_1391),implies(X_1393,X_1391))) )],[refute_0_75,refute_0_56]) ).
cnf(refute_0_77,plain,
( ~ is_a_theorem(implies(implies(X_1763,X_1763),implies(implies(implies(implies(not(X_1422),X_1422),X_1422),X_1763),X_1763)))
| is_a_theorem(implies(X_1764,implies(implies(implies(implies(not(X_1422),X_1422),X_1422),X_1763),X_1763))) ),
inference(subst,[],[refute_0_76:[bind(X_1391,$fot(implies(implies(implies(implies(not(X_1422),X_1422),X_1422),X_1763),X_1763))),bind(X_1392,$fot(X_1763)),bind(X_1393,$fot(X_1764))]]) ).
cnf(refute_0_78,plain,
is_a_theorem(implies(X_1764,implies(implies(implies(implies(not(X_1422),X_1422),X_1422),X_1763),X_1763))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_1763,X_1763),implies(implies(implies(implies(not(X_1422),X_1422),X_1422),X_1763),X_1763))) )],[refute_0_55,refute_0_77]) ).
cnf(refute_0_79,plain,
is_a_theorem(implies(implies(not(not(implies(implies(implies(implies(not(X_1772),X_1772),X_1772),X_1773),X_1773))),X_377),implies(implies(implies(implies(not(X_1772),X_1772),X_1772),X_1773),X_1773))),
inference(subst,[],[refute_0_78:[bind(X_1422,$fot(X_1772)),bind(X_1763,$fot(X_1773)),bind(X_1764,$fot(implies(not(not(implies(implies(implies(implies(not(X_1772),X_1772),X_1772),X_1773),X_1773))),X_377)))]]) ).
cnf(refute_0_80,plain,
is_a_theorem(implies(implies(implies(implies(not(X_1772),X_1772),X_1772),X_1773),X_1773)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(not(implies(implies(implies(implies(not(X_1772),X_1772),X_1772),X_1773),X_1773))),X_377),implies(implies(implies(implies(not(X_1772),X_1772),X_1772),X_1773),X_1773))) )],[refute_0_79,refute_0_22]) ).
cnf(refute_0_81,plain,
is_a_theorem(implies(implies(implies(implies(not(X_2328),X_2328),X_2328),implies(X_2326,X_2328)),implies(X_2326,X_2328))),
inference(subst,[],[refute_0_80:[bind(X_1772,$fot(X_2328)),bind(X_1773,$fot(implies(X_2326,X_2328)))]]) ).
cnf(refute_0_82,plain,
( ~ is_a_theorem(implies(implies(implies(X_115,X_116),implies(X_114,X_116)),X_117))
| ~ is_a_theorem(implies(implies(implies(implies(X_115,X_116),implies(X_114,X_116)),X_117),implies(implies(X_114,X_115),X_117)))
| is_a_theorem(implies(implies(X_114,X_115),X_117)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(X_115,X_116),implies(X_114,X_116)),X_117))),bind(Y,$fot(implies(implies(X_114,X_115),X_117)))]]) ).
cnf(refute_0_83,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_22),implies(implies(X,Y),X_22))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(implies(X,Y))),bind(Y,$fot(implies(implies(Y,Z),implies(X,Z)))),bind(Z,$fot(X_22))]]) ).
cnf(refute_0_84,plain,
is_a_theorem(implies(implies(implies(implies(Y,Z),implies(X,Z)),X_22),implies(implies(X,Y),X_22))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )],[cn_1,refute_0_83]) ).
cnf(refute_0_85,plain,
is_a_theorem(implies(implies(implies(implies(X_115,X_116),implies(X_114,X_116)),X_117),implies(implies(X_114,X_115),X_117))),
inference(subst,[],[refute_0_84:[bind(X,$fot(X_114)),bind(Y,$fot(X_115)),bind(Z,$fot(X_116)),bind(X_22,$fot(X_117))]]) ).
cnf(refute_0_86,plain,
( ~ is_a_theorem(implies(implies(implies(X_115,X_116),implies(X_114,X_116)),X_117))
| is_a_theorem(implies(implies(X_114,X_115),X_117)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_115,X_116),implies(X_114,X_116)),X_117),implies(implies(X_114,X_115),X_117))) )],[refute_0_85,refute_0_82]) ).
cnf(refute_0_87,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(X_2328),X_2328),X_2328),implies(X_2326,X_2328)),implies(X_2326,X_2328)))
| is_a_theorem(implies(implies(X_2326,implies(not(X_2328),X_2328)),implies(X_2326,X_2328))) ),
inference(subst,[],[refute_0_86:[bind(X_114,$fot(X_2326)),bind(X_115,$fot(implies(not(X_2328),X_2328))),bind(X_116,$fot(X_2328)),bind(X_117,$fot(implies(X_2326,X_2328)))]]) ).
cnf(refute_0_88,plain,
is_a_theorem(implies(implies(X_2326,implies(not(X_2328),X_2328)),implies(X_2326,X_2328))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(X_2328),X_2328),X_2328),implies(X_2326,X_2328)),implies(X_2326,X_2328))) )],[refute_0_81,refute_0_87]) ).
cnf(refute_0_89,plain,
is_a_theorem(implies(implies(X_2330,implies(not(X_2331),X_2331)),implies(X_2330,X_2331))),
inference(subst,[],[refute_0_88:[bind(X_2326,$fot(X_2330)),bind(X_2328,$fot(X_2331))]]) ).
cnf(refute_0_90,plain,
( ~ is_a_theorem(implies(X_2330,implies(not(X_2331),X_2331)))
| is_a_theorem(implies(X_2330,X_2331)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_2330,implies(not(X_2331),X_2331)),implies(X_2330,X_2331))) )],[refute_0_89,refute_0_10]) ).
cnf(refute_0_91,plain,
( ~ is_a_theorem(implies(implies(not(implies(not(not(not(X_3067))),not(not(X_3067)))),X_3067),implies(not(X_3067),X_3067)))
| is_a_theorem(implies(implies(not(implies(not(not(not(X_3067))),not(not(X_3067)))),X_3067),X_3067)) ),
inference(subst,[],[refute_0_90:[bind(X_2330,$fot(implies(not(implies(not(not(not(X_3067))),not(not(X_3067)))),X_3067))),bind(X_2331,$fot(X_3067))]]) ).
cnf(refute_0_92,plain,
( ~ is_a_theorem(implies(X_3061,not(implies(not(not(X_3061)),not(X_3061)))))
| is_a_theorem(implies(implies(not(implies(not(not(X_3061)),not(X_3061))),Z),implies(X_3061,Z))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(X_3061)),bind(Y,$fot(not(implies(not(not(X_3061)),not(X_3061)))))]]) ).
cnf(refute_0_93,plain,
( ~ is_a_theorem(implies(implies(not(X_26),not(implies(not(not(X_26)),not(X_26)))),not(implies(not(not(X_26)),not(X_26)))))
| is_a_theorem(implies(X_26,not(implies(not(not(X_26)),not(X_26))))) ),
inference(subst,[],[refute_0_7:[bind(X_25,$fot(not(implies(not(not(X_26)),not(X_26))))),bind(X_27,$fot(not(implies(not(not(X_26)),not(X_26)))))]]) ).
cnf(refute_0_94,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_3059),X_3059),not(implies(not(X_3059),X_3059))),not(implies(not(X_3059),X_3059))))
| is_a_theorem(implies(implies(X_3059,not(implies(not(X_3059),X_3059))),not(implies(not(X_3059),X_3059)))) ),
inference(subst,[],[refute_0_31:[bind(X_71,$fot(not(implies(not(X_3059),X_3059)))),bind(X_72,$fot(X_3059)),bind(X_73,$fot(not(implies(not(X_3059),X_3059))))]]) ).
cnf(refute_0_95,plain,
( ~ is_a_theorem(implies(implies(implies(not(implies(X_2994,X_2995)),implies(X_2994,X_2995)),not(implies(X_2994,X_2995))),not(implies(X_2994,X_2995))))
| is_a_theorem(implies(implies(implies(X_2994,X_2995),not(implies(X_2994,X_2995))),not(implies(X_2994,X_2995)))) ),
inference(subst,[],[refute_0_31:[bind(X_71,$fot(not(implies(X_2994,X_2995)))),bind(X_72,$fot(implies(X_2994,X_2995))),bind(X_73,$fot(not(implies(X_2994,X_2995))))]]) ).
cnf(refute_0_96,plain,
( ~ is_a_theorem(implies(not(X_2779),implies(X_2779,implies(X_2780,X_2781))))
| is_a_theorem(implies(implies(implies(X_2779,implies(X_2780,X_2781)),Z),implies(not(X_2779),Z))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(not(X_2779))),bind(Y,$fot(implies(X_2779,implies(X_2780,X_2781))))]]) ).
cnf(refute_0_97,plain,
( ~ is_a_theorem(implies(implies(implies(X_217,X_216),implies(not(X_218),X_216)),X_215))
| ~ is_a_theorem(implies(implies(implies(implies(X_217,X_216),implies(not(X_218),X_216)),X_215),implies(X_218,X_215)))
| is_a_theorem(implies(X_218,X_215)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(X_217,X_216),implies(not(X_218),X_216)),X_215))),bind(Y,$fot(implies(X_218,X_215)))]]) ).
cnf(refute_0_98,plain,
( ~ is_a_theorem(implies(X_214,implies(implies(X_213,X_212),implies(not(X_214),X_212))))
| is_a_theorem(implies(implies(implies(implies(X_213,X_212),implies(not(X_214),X_212)),Z),implies(X_214,Z))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(X_214)),bind(Y,$fot(implies(implies(X_213,X_212),implies(not(X_214),X_212))))]]) ).
cnf(refute_0_99,plain,
is_a_theorem(implies(implies(not(X_169),X_168),implies(implies(X_168,Z),implies(not(X_169),Z)))),
inference(subst,[],[cn_1:[bind(X,$fot(not(X_169))),bind(Y,$fot(X_168))]]) ).
cnf(refute_0_100,plain,
( ~ is_a_theorem(implies(implies(not(X_169),X_168),implies(implies(X_168,Z),implies(not(X_169),Z))))
| is_a_theorem(implies(X_169,implies(implies(X_168,Z),implies(not(X_169),Z)))) ),
inference(subst,[],[refute_0_7:[bind(X_25,$fot(X_168)),bind(X_26,$fot(X_169)),bind(X_27,$fot(implies(implies(X_168,Z),implies(not(X_169),Z))))]]) ).
cnf(refute_0_101,plain,
is_a_theorem(implies(X_169,implies(implies(X_168,Z),implies(not(X_169),Z)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_169),X_168),implies(implies(X_168,Z),implies(not(X_169),Z)))) )],[refute_0_99,refute_0_100]) ).
cnf(refute_0_102,plain,
is_a_theorem(implies(X_214,implies(implies(X_213,X_212),implies(not(X_214),X_212)))),
inference(subst,[],[refute_0_101:[bind(Z,$fot(X_212)),bind(X_168,$fot(X_213)),bind(X_169,$fot(X_214))]]) ).
cnf(refute_0_103,plain,
is_a_theorem(implies(implies(implies(implies(X_213,X_212),implies(not(X_214),X_212)),Z),implies(X_214,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_214,implies(implies(X_213,X_212),implies(not(X_214),X_212)))) )],[refute_0_102,refute_0_98]) ).
cnf(refute_0_104,plain,
is_a_theorem(implies(implies(implies(implies(X_217,X_216),implies(not(X_218),X_216)),X_215),implies(X_218,X_215))),
inference(subst,[],[refute_0_103:[bind(Z,$fot(X_215)),bind(X_212,$fot(X_216)),bind(X_213,$fot(X_217)),bind(X_214,$fot(X_218))]]) ).
cnf(refute_0_105,plain,
( ~ is_a_theorem(implies(implies(implies(X_217,X_216),implies(not(X_218),X_216)),X_215))
| is_a_theorem(implies(X_218,X_215)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_217,X_216),implies(not(X_218),X_216)),X_215),implies(X_218,X_215))) )],[refute_0_104,refute_0_97]) ).
cnf(refute_0_106,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_2776),not(X_2775)),implies(not(not(X_2775)),not(X_2775))),implies(X_2775,implies(X_2776,X_2777))))
| is_a_theorem(implies(not(X_2775),implies(X_2775,implies(X_2776,X_2777)))) ),
inference(subst,[],[refute_0_105:[bind(X_215,$fot(implies(X_2775,implies(X_2776,X_2777)))),bind(X_216,$fot(not(X_2775))),bind(X_217,$fot(not(X_2776))),bind(X_218,$fot(not(X_2775)))]]) ).
cnf(refute_0_107,plain,
( ~ is_a_theorem(implies(implies(X_2375,implies(not(not(X_2374)),not(X_2374))),implies(X_2374,implies(X_2375,X_2376))))
| is_a_theorem(implies(implies(implies(not(X_2375),X_47),implies(not(not(X_2374)),not(X_2374))),implies(X_2374,implies(X_2375,X_2376)))) ),
inference(subst,[],[refute_0_17:[bind(X_46,$fot(implies(X_2374,implies(X_2375,X_2376)))),bind(X_48,$fot(X_2375)),bind(X_49,$fot(implies(not(not(X_2374)),not(X_2374))))]]) ).
cnf(refute_0_108,plain,
( ~ is_a_theorem(implies(X_178,implies(implies(not(not(X_178)),not(X_178)),X_177)))
| is_a_theorem(implies(implies(implies(implies(not(not(X_178)),not(X_178)),X_177),Z),implies(X_178,Z))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(X_178)),bind(Y,$fot(implies(implies(not(not(X_178)),not(X_178)),X_177)))]]) ).
cnf(refute_0_109,plain,
is_a_theorem(implies(implies(not(X_169),X_168),implies(implies(not(not(X_169)),not(X_169)),X_168))),
inference(subst,[],[refute_0_27:[bind(X_21,$fot(not(X_169))),bind(X_22,$fot(X_168))]]) ).
cnf(refute_0_110,plain,
( ~ is_a_theorem(implies(implies(not(X_169),X_168),implies(implies(not(not(X_169)),not(X_169)),X_168)))
| is_a_theorem(implies(X_169,implies(implies(not(not(X_169)),not(X_169)),X_168))) ),
inference(subst,[],[refute_0_7:[bind(X_25,$fot(X_168)),bind(X_26,$fot(X_169)),bind(X_27,$fot(implies(implies(not(not(X_169)),not(X_169)),X_168)))]]) ).
cnf(refute_0_111,plain,
is_a_theorem(implies(X_169,implies(implies(not(not(X_169)),not(X_169)),X_168))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_169),X_168),implies(implies(not(not(X_169)),not(X_169)),X_168))) )],[refute_0_109,refute_0_110]) ).
cnf(refute_0_112,plain,
is_a_theorem(implies(X_178,implies(implies(not(not(X_178)),not(X_178)),X_177))),
inference(subst,[],[refute_0_111:[bind(X_168,$fot(X_177)),bind(X_169,$fot(X_178))]]) ).
cnf(refute_0_113,plain,
is_a_theorem(implies(implies(implies(implies(not(not(X_178)),not(X_178)),X_177),Z),implies(X_178,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_178,implies(implies(not(not(X_178)),not(X_178)),X_177))) )],[refute_0_112,refute_0_108]) ).
cnf(refute_0_114,plain,
is_a_theorem(implies(implies(implies(implies(not(not(X_178)),not(X_178)),X_2328),implies(X_2326,X_2328)),implies(X_178,implies(X_2326,X_2328)))),
inference(subst,[],[refute_0_113:[bind(Z,$fot(implies(X_2326,X_2328))),bind(X_177,$fot(X_2328))]]) ).
cnf(refute_0_115,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(not(X_178)),not(X_178)),X_2328),implies(X_2326,X_2328)),implies(X_178,implies(X_2326,X_2328))))
| is_a_theorem(implies(implies(X_2326,implies(not(not(X_178)),not(X_178))),implies(X_178,implies(X_2326,X_2328)))) ),
inference(subst,[],[refute_0_86:[bind(X_114,$fot(X_2326)),bind(X_115,$fot(implies(not(not(X_178)),not(X_178)))),bind(X_116,$fot(X_2328)),bind(X_117,$fot(implies(X_178,implies(X_2326,X_2328))))]]) ).
cnf(refute_0_116,plain,
is_a_theorem(implies(implies(X_2326,implies(not(not(X_178)),not(X_178))),implies(X_178,implies(X_2326,X_2328)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(not(X_178)),not(X_178)),X_2328),implies(X_2326,X_2328)),implies(X_178,implies(X_2326,X_2328)))) )],[refute_0_114,refute_0_115]) ).
cnf(refute_0_117,plain,
is_a_theorem(implies(implies(X_2375,implies(not(not(X_2374)),not(X_2374))),implies(X_2374,implies(X_2375,X_2376)))),
inference(subst,[],[refute_0_116:[bind(X_178,$fot(X_2374)),bind(X_2326,$fot(X_2375)),bind(X_2328,$fot(X_2376))]]) ).
cnf(refute_0_118,plain,
is_a_theorem(implies(implies(implies(not(X_2375),X_47),implies(not(not(X_2374)),not(X_2374))),implies(X_2374,implies(X_2375,X_2376)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_2375,implies(not(not(X_2374)),not(X_2374))),implies(X_2374,implies(X_2375,X_2376)))) )],[refute_0_117,refute_0_107]) ).
cnf(refute_0_119,plain,
is_a_theorem(implies(implies(implies(not(X_2776),not(X_2775)),implies(not(not(X_2775)),not(X_2775))),implies(X_2775,implies(X_2776,X_2777)))),
inference(subst,[],[refute_0_118:[bind(X_2374,$fot(X_2775)),bind(X_2375,$fot(X_2776)),bind(X_2376,$fot(X_2777)),bind(X_47,$fot(not(X_2775)))]]) ).
cnf(refute_0_120,plain,
is_a_theorem(implies(not(X_2775),implies(X_2775,implies(X_2776,X_2777)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_2776),not(X_2775)),implies(not(not(X_2775)),not(X_2775))),implies(X_2775,implies(X_2776,X_2777)))) )],[refute_0_119,refute_0_106]) ).
cnf(refute_0_121,plain,
is_a_theorem(implies(not(X_2779),implies(X_2779,implies(X_2780,X_2781)))),
inference(subst,[],[refute_0_120:[bind(X_2775,$fot(X_2779)),bind(X_2776,$fot(X_2780)),bind(X_2777,$fot(X_2781))]]) ).
cnf(refute_0_122,plain,
is_a_theorem(implies(implies(implies(X_2779,implies(X_2780,X_2781)),Z),implies(not(X_2779),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(not(X_2779),implies(X_2779,implies(X_2780,X_2781)))) )],[refute_0_121,refute_0_96]) ).
cnf(refute_0_123,plain,
is_a_theorem(implies(implies(implies(X_2979,implies(X_2780,X_2781)),X_2979),implies(not(X_2979),X_2979))),
inference(subst,[],[refute_0_122:[bind(Z,$fot(X_2979)),bind(X_2779,$fot(X_2979))]]) ).
cnf(refute_0_124,plain,
( ~ is_a_theorem(implies(implies(implies(X_2979,implies(X_2780,X_2781)),X_2979),implies(not(X_2979),X_2979)))
| is_a_theorem(implies(implies(implies(X_2979,implies(X_2780,X_2781)),X_2979),X_2979)) ),
inference(subst,[],[refute_0_90:[bind(X_2330,$fot(implies(implies(X_2979,implies(X_2780,X_2781)),X_2979))),bind(X_2331,$fot(X_2979))]]) ).
cnf(refute_0_125,plain,
is_a_theorem(implies(implies(implies(X_2979,implies(X_2780,X_2781)),X_2979),X_2979)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_2979,implies(X_2780,X_2781)),X_2979),implies(not(X_2979),X_2979))) )],[refute_0_123,refute_0_124]) ).
cnf(refute_0_126,plain,
is_a_theorem(implies(implies(implies(not(implies(X_2994,X_2995)),implies(X_2994,X_2995)),not(implies(X_2994,X_2995))),not(implies(X_2994,X_2995)))),
inference(subst,[],[refute_0_125:[bind(X_2780,$fot(X_2994)),bind(X_2781,$fot(X_2995)),bind(X_2979,$fot(not(implies(X_2994,X_2995))))]]) ).
cnf(refute_0_127,plain,
is_a_theorem(implies(implies(implies(X_2994,X_2995),not(implies(X_2994,X_2995))),not(implies(X_2994,X_2995)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(implies(X_2994,X_2995)),implies(X_2994,X_2995)),not(implies(X_2994,X_2995))),not(implies(X_2994,X_2995)))) )],[refute_0_126,refute_0_95]) ).
cnf(refute_0_128,plain,
is_a_theorem(implies(implies(implies(not(X_3059),X_3059),not(implies(not(X_3059),X_3059))),not(implies(not(X_3059),X_3059)))),
inference(subst,[],[refute_0_127:[bind(X_2994,$fot(not(X_3059))),bind(X_2995,$fot(X_3059))]]) ).
cnf(refute_0_129,plain,
is_a_theorem(implies(implies(X_3059,not(implies(not(X_3059),X_3059))),not(implies(not(X_3059),X_3059)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_3059),X_3059),not(implies(not(X_3059),X_3059))),not(implies(not(X_3059),X_3059)))) )],[refute_0_128,refute_0_94]) ).
cnf(refute_0_130,plain,
is_a_theorem(implies(implies(not(X_26),not(implies(not(not(X_26)),not(X_26)))),not(implies(not(not(X_26)),not(X_26))))),
inference(subst,[],[refute_0_129:[bind(X_3059,$fot(not(X_26)))]]) ).
cnf(refute_0_131,plain,
is_a_theorem(implies(X_26,not(implies(not(not(X_26)),not(X_26))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_26),not(implies(not(not(X_26)),not(X_26)))),not(implies(not(not(X_26)),not(X_26))))) )],[refute_0_130,refute_0_93]) ).
cnf(refute_0_132,plain,
is_a_theorem(implies(X_3061,not(implies(not(not(X_3061)),not(X_3061))))),
inference(subst,[],[refute_0_131:[bind(X_26,$fot(X_3061))]]) ).
cnf(refute_0_133,plain,
is_a_theorem(implies(implies(not(implies(not(not(X_3061)),not(X_3061))),Z),implies(X_3061,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_3061,not(implies(not(not(X_3061)),not(X_3061))))) )],[refute_0_132,refute_0_92]) ).
cnf(refute_0_134,plain,
is_a_theorem(implies(implies(not(implies(not(not(not(X_3067))),not(not(X_3067)))),X_3067),implies(not(X_3067),X_3067))),
inference(subst,[],[refute_0_133:[bind(Z,$fot(X_3067)),bind(X_3061,$fot(not(X_3067)))]]) ).
cnf(refute_0_135,plain,
is_a_theorem(implies(implies(not(implies(not(not(not(X_3067))),not(not(X_3067)))),X_3067),X_3067)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(implies(not(not(not(X_3067))),not(not(X_3067)))),X_3067),implies(not(X_3067),X_3067))) )],[refute_0_134,refute_0_91]) ).
cnf(refute_0_136,plain,
is_a_theorem(implies(implies(not(implies(not(not(not(X_3069))),not(not(X_3069)))),X_3069),X_3069)),
inference(subst,[],[refute_0_135:[bind(X_3067,$fot(X_3069))]]) ).
cnf(refute_0_137,plain,
is_a_theorem(implies(implies(not(not(not(X_3069))),not(not(X_3069))),X_3069)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(implies(not(not(not(X_3069))),not(not(X_3069)))),X_3069),X_3069)) )],[refute_0_136,refute_0_9]) ).
cnf(refute_0_138,plain,
is_a_theorem(implies(implies(not(not(not(X_3070))),not(not(X_3070))),X_3070)),
inference(subst,[],[refute_0_137:[bind(X_3069,$fot(X_3070))]]) ).
cnf(refute_0_139,plain,
is_a_theorem(implies(not(not(X_3070)),X_3070)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(not(not(X_3070))),not(not(X_3070))),X_3070)) )],[refute_0_138,refute_0_8]) ).
cnf(refute_0_140,plain,
is_a_theorem(implies(not(not(not(implies(X_3983,X_3983)))),not(implies(X_3983,X_3983)))),
inference(subst,[],[refute_0_139:[bind(X_3070,$fot(not(implies(X_3983,X_3983))))]]) ).
cnf(refute_0_141,plain,
( ~ is_a_theorem(implies(implies(not(X_2340),not(implies(X_2339,X_2339))),X_2340))
| ~ is_a_theorem(implies(not(X_2340),not(implies(X_2339,X_2339))))
| is_a_theorem(X_2340) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(not(X_2340),not(implies(X_2339,X_2339))))),bind(Y,$fot(X_2340))]]) ).
cnf(refute_0_142,plain,
( ~ is_a_theorem(implies(implies(implies(X_1928,X_1928),implies(not(X_1929),X_1929)),X_1929))
| is_a_theorem(implies(implies(implies(not(implies(X_1928,X_1928)),X_47),implies(not(X_1929),X_1929)),X_1929)) ),
inference(subst,[],[refute_0_17:[bind(X_46,$fot(X_1929)),bind(X_48,$fot(implies(X_1928,X_1928))),bind(X_49,$fot(implies(not(X_1929),X_1929)))]]) ).
cnf(refute_0_143,plain,
( ~ is_a_theorem(implies(implies(not(not(implies(implies(implies(X_1925,X_1925),implies(not(X_1926),X_1926)),X_1926))),X_377),implies(implies(implies(X_1925,X_1925),implies(not(X_1926),X_1926)),X_1926)))
| is_a_theorem(implies(implies(implies(X_1925,X_1925),implies(not(X_1926),X_1926)),X_1926)) ),
inference(subst,[],[refute_0_21:[bind(X_376,$fot(implies(implies(implies(X_1925,X_1925),implies(not(X_1926),X_1926)),X_1926)))]]) ).
cnf(refute_0_144,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_72),X_72),X_1745),implies(implies(implies(X_1747,X_1747),implies(not(X_72),X_72)),X_1745)))
| is_a_theorem(implies(implies(X_72,X_1745),implies(implies(implies(X_1747,X_1747),implies(not(X_72),X_72)),X_1745))) ),
inference(subst,[],[refute_0_31:[bind(X_71,$fot(implies(implies(implies(X_1747,X_1747),implies(not(X_72),X_72)),X_1745))),bind(X_73,$fot(X_1745))]]) ).
cnf(refute_0_145,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_1742),X_1742),X_1741),implies(implies(implies(X_1743,X_1743),X_1742),X_1741)))
| is_a_theorem(implies(implies(X_1742,X_1741),implies(implies(implies(X_1743,X_1743),X_1742),X_1741))) ),
inference(subst,[],[refute_0_31:[bind(X_71,$fot(implies(implies(implies(X_1743,X_1743),X_1742),X_1741))),bind(X_72,$fot(X_1742)),bind(X_73,$fot(X_1741))]]) ).
cnf(refute_0_146,plain,
( ~ is_a_theorem(implies(implies(implies(X_1392,X_1392),X_1391),implies(X_1393,X_1391)))
| is_a_theorem(implies(implies(implies(X_1393,X_1391),Z),implies(implies(implies(X_1392,X_1392),X_1391),Z))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(implies(implies(X_1392,X_1392),X_1391))),bind(Y,$fot(implies(X_1393,X_1391)))]]) ).
cnf(refute_0_147,plain,
is_a_theorem(implies(implies(implies(X_1393,X_1391),Z),implies(implies(implies(X_1392,X_1392),X_1391),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_1392,X_1392),X_1391),implies(X_1393,X_1391))) )],[refute_0_75,refute_0_146]) ).
cnf(refute_0_148,plain,
is_a_theorem(implies(implies(implies(not(X_1742),X_1742),X_1741),implies(implies(implies(X_1743,X_1743),X_1742),X_1741))),
inference(subst,[],[refute_0_147:[bind(Z,$fot(X_1741)),bind(X_1391,$fot(X_1742)),bind(X_1392,$fot(X_1743)),bind(X_1393,$fot(not(X_1742)))]]) ).
cnf(refute_0_149,plain,
is_a_theorem(implies(implies(X_1742,X_1741),implies(implies(implies(X_1743,X_1743),X_1742),X_1741))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_1742),X_1742),X_1741),implies(implies(implies(X_1743,X_1743),X_1742),X_1741))) )],[refute_0_148,refute_0_145]) ).
cnf(refute_0_150,plain,
is_a_theorem(implies(implies(implies(not(X_72),X_72),X_1745),implies(implies(implies(X_1747,X_1747),implies(not(X_72),X_72)),X_1745))),
inference(subst,[],[refute_0_149:[bind(X_1741,$fot(X_1745)),bind(X_1742,$fot(implies(not(X_72),X_72))),bind(X_1743,$fot(X_1747))]]) ).
cnf(refute_0_151,plain,
is_a_theorem(implies(implies(X_72,X_1745),implies(implies(implies(X_1747,X_1747),implies(not(X_72),X_72)),X_1745))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_72),X_72),X_1745),implies(implies(implies(X_1747,X_1747),implies(not(X_72),X_72)),X_1745))) )],[refute_0_150,refute_0_144]) ).
cnf(refute_0_152,plain,
is_a_theorem(implies(implies(X_1763,X_1763),implies(implies(implies(X_1747,X_1747),implies(not(X_1763),X_1763)),X_1763))),
inference(subst,[],[refute_0_151:[bind(X_1745,$fot(X_1763)),bind(X_72,$fot(X_1763))]]) ).
cnf(refute_0_153,plain,
( ~ is_a_theorem(implies(implies(X_1763,X_1763),implies(implies(implies(X_1747,X_1747),implies(not(X_1763),X_1763)),X_1763)))
| is_a_theorem(implies(X_1764,implies(implies(implies(X_1747,X_1747),implies(not(X_1763),X_1763)),X_1763))) ),
inference(subst,[],[refute_0_76:[bind(X_1391,$fot(implies(implies(implies(X_1747,X_1747),implies(not(X_1763),X_1763)),X_1763))),bind(X_1392,$fot(X_1763)),bind(X_1393,$fot(X_1764))]]) ).
cnf(refute_0_154,plain,
is_a_theorem(implies(X_1764,implies(implies(implies(X_1747,X_1747),implies(not(X_1763),X_1763)),X_1763))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_1763,X_1763),implies(implies(implies(X_1747,X_1747),implies(not(X_1763),X_1763)),X_1763))) )],[refute_0_152,refute_0_153]) ).
cnf(refute_0_155,plain,
is_a_theorem(implies(implies(not(not(implies(implies(implies(X_1925,X_1925),implies(not(X_1926),X_1926)),X_1926))),X_377),implies(implies(implies(X_1925,X_1925),implies(not(X_1926),X_1926)),X_1926))),
inference(subst,[],[refute_0_154:[bind(X_1747,$fot(X_1925)),bind(X_1763,$fot(X_1926)),bind(X_1764,$fot(implies(not(not(implies(implies(implies(X_1925,X_1925),implies(not(X_1926),X_1926)),X_1926))),X_377)))]]) ).
cnf(refute_0_156,plain,
is_a_theorem(implies(implies(implies(X_1925,X_1925),implies(not(X_1926),X_1926)),X_1926)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(not(implies(implies(implies(X_1925,X_1925),implies(not(X_1926),X_1926)),X_1926))),X_377),implies(implies(implies(X_1925,X_1925),implies(not(X_1926),X_1926)),X_1926))) )],[refute_0_155,refute_0_143]) ).
cnf(refute_0_157,plain,
is_a_theorem(implies(implies(implies(X_1928,X_1928),implies(not(X_1929),X_1929)),X_1929)),
inference(subst,[],[refute_0_156:[bind(X_1925,$fot(X_1928)),bind(X_1926,$fot(X_1929))]]) ).
cnf(refute_0_158,plain,
is_a_theorem(implies(implies(implies(not(implies(X_1928,X_1928)),X_47),implies(not(X_1929),X_1929)),X_1929)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_1928,X_1928),implies(not(X_1929),X_1929)),X_1929)) )],[refute_0_157,refute_0_142]) ).
cnf(refute_0_159,plain,
is_a_theorem(implies(implies(implies(not(implies(X_1928,X_1928)),X_2329),implies(not(X_2329),X_2329)),X_2329)),
inference(subst,[],[refute_0_158:[bind(X_1929,$fot(X_2329)),bind(X_47,$fot(X_2329))]]) ).
cnf(refute_0_160,plain,
( ~ is_a_theorem(implies(implies(implies(not(implies(X_1928,X_1928)),X_2329),implies(not(X_2329),X_2329)),X_2329))
| is_a_theorem(implies(implies(not(X_2329),not(implies(X_1928,X_1928))),X_2329)) ),
inference(subst,[],[refute_0_86:[bind(X_114,$fot(not(X_2329))),bind(X_115,$fot(not(implies(X_1928,X_1928)))),bind(X_116,$fot(X_2329)),bind(X_117,$fot(X_2329))]]) ).
cnf(refute_0_161,plain,
is_a_theorem(implies(implies(not(X_2329),not(implies(X_1928,X_1928))),X_2329)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(implies(X_1928,X_1928)),X_2329),implies(not(X_2329),X_2329)),X_2329)) )],[refute_0_159,refute_0_160]) ).
cnf(refute_0_162,plain,
is_a_theorem(implies(implies(not(X_2340),not(implies(X_2339,X_2339))),X_2340)),
inference(subst,[],[refute_0_161:[bind(X_1928,$fot(X_2339)),bind(X_2329,$fot(X_2340))]]) ).
cnf(refute_0_163,plain,
( ~ is_a_theorem(implies(not(X_2340),not(implies(X_2339,X_2339))))
| is_a_theorem(X_2340) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_2340),not(implies(X_2339,X_2339))),X_2340)) )],[refute_0_162,refute_0_141]) ).
cnf(refute_0_164,plain,
( ~ is_a_theorem(implies(not(not(not(implies(X_3983,X_3983)))),not(implies(X_3983,X_3983))))
| is_a_theorem(not(not(implies(X_3983,X_3983)))) ),
inference(subst,[],[refute_0_163:[bind(X_2339,$fot(X_3983)),bind(X_2340,$fot(not(not(implies(X_3983,X_3983)))))]]) ).
cnf(refute_0_165,plain,
is_a_theorem(not(not(implies(X_3983,X_3983)))),
inference(resolve,[$cnf( is_a_theorem(implies(not(not(not(implies(X_3983,X_3983)))),not(implies(X_3983,X_3983)))) )],[refute_0_140,refute_0_164]) ).
cnf(refute_0_166,plain,
is_a_theorem(not(not(implies(p,p)))),
inference(subst,[],[refute_0_165:[bind(X_3983,$fot(p))]]) ).
cnf(refute_0_167,plain,
$false,
inference(resolve,[$cnf( is_a_theorem(not(not(implies(p,p)))) )],[refute_0_166,prove_not_not_implies]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL256-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.04 % Command : metis --show proof --show saturation %s
% 0.08/0.35 % Computer : n007.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 5 23:23:54 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 6.16/6.47 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.16/6.47
% 6.16/6.47 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 6.26/6.50
%------------------------------------------------------------------------------