%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : LCL030-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n003.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:41:41 PM UTC 2026
% Result : Unsatisfiable 216.33s 216.67s
% Output : CNFRefutation 216.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 6
% Syntax : Number of clauses : 149 ( 84 unt; 0 nHn; 42 RR)
% Number of literals : 229 ( 0 equ; 81 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 454 ( 97 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) ).
cnf(c0_1,axiom,
is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) ).
cnf(c0_2,axiom,
is_a_theorem(implies(X,implies(Y,X))) ).
cnf(c0_3,axiom,
is_a_theorem(implies(implies(implies(X,Y),X),X)) ).
cnf(c0_4,axiom,
is_a_theorem(implies(falsehood,X)) ).
cnf(prove_c0_6,negated_conjecture,
~ is_a_theorem(implies(implies(a,implies(b,c)),implies(implies(a,b),implies(a,c)))) ).
cnf(refute_0_0,plain,
( ~ is_a_theorem(implies(X_3087,implies(X_3089,X_3088)))
| ~ is_a_theorem(implies(implies(X_3087,implies(X_3089,X_3088)),implies(X_3089,implies(X_3087,X_3088))))
| is_a_theorem(implies(X_3089,implies(X_3087,X_3088))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X_3087,implies(X_3089,X_3088)))),bind(Y,$fot(implies(X_3089,implies(X_3087,X_3088))))]]) ).
cnf(refute_0_1,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_2,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)))) )],[c0_1,refute_0_1]) ).
cnf(refute_0_3,plain,
( ~ is_a_theorem(implies(X_664,implies(implies(X_664,X_665),X_665)))
| is_a_theorem(implies(implies(implies(implies(X_664,X_665),X_665),Z),implies(X_664,Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(X_664)),bind(Y,$fot(implies(implies(X_664,X_665),X_665)))]]) ).
cnf(refute_0_4,plain,
( ~ is_a_theorem(implies(implies(implies(X_390,X_388),implies(X_389,X_388)),X_387))
| ~ is_a_theorem(implies(implies(implies(implies(X_390,X_388),implies(X_389,X_388)),X_387),implies(X_390,X_387)))
| is_a_theorem(implies(X_390,X_387)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(X_390,X_388),implies(X_389,X_388)),X_387))),bind(Y,$fot(implies(X_390,X_387)))]]) ).
cnf(refute_0_5,plain,
( ~ is_a_theorem(implies(X_244,implies(implies(X_244,X_242),implies(X_243,X_242))))
| is_a_theorem(implies(implies(implies(implies(X_244,X_242),implies(X_243,X_242)),Z),implies(X_244,Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(X_244)),bind(Y,$fot(implies(implies(X_244,X_242),implies(X_243,X_242))))]]) ).
cnf(refute_0_6,plain,
is_a_theorem(implies(implies(X_232,X_233),implies(implies(X_233,Z),implies(X_232,Z)))),
inference(subst,[],[c0_1:[bind(X,$fot(X_232)),bind(Y,$fot(X_233))]]) ).
cnf(refute_0_7,plain,
( ~ is_a_theorem(implies(implies(X_49,X_50),X_51))
| ~ is_a_theorem(implies(implies(implies(X_49,X_50),X_51),implies(X_50,X_51)))
| is_a_theorem(implies(X_50,X_51)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_49,X_50),X_51))),bind(Y,$fot(implies(X_50,X_51)))]]) ).
cnf(refute_0_8,plain,
is_a_theorem(implies(X_42,implies(Y,X_42))),
inference(subst,[],[c0_2:[bind(X,$fot(X_42))]]) ).
cnf(refute_0_9,plain,
( ~ is_a_theorem(implies(X_42,implies(Y,X_42)))
| is_a_theorem(implies(implies(implies(Y,X_42),X_44),implies(X_42,X_44))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(X_42)),bind(Y,$fot(implies(Y,X_42))),bind(Z,$fot(X_44))]]) ).
cnf(refute_0_10,plain,
is_a_theorem(implies(implies(implies(Y,X_42),X_44),implies(X_42,X_44))),
inference(resolve,[$cnf( is_a_theorem(implies(X_42,implies(Y,X_42))) )],[refute_0_8,refute_0_9]) ).
cnf(refute_0_11,plain,
is_a_theorem(implies(implies(implies(X_49,X_50),X_51),implies(X_50,X_51))),
inference(subst,[],[refute_0_10:[bind(Y,$fot(X_49)),bind(X_42,$fot(X_50)),bind(X_44,$fot(X_51))]]) ).
cnf(refute_0_12,plain,
( ~ is_a_theorem(implies(implies(X_49,X_50),X_51))
| is_a_theorem(implies(X_50,X_51)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_49,X_50),X_51),implies(X_50,X_51))) )],[refute_0_11,refute_0_7]) ).
cnf(refute_0_13,plain,
( ~ is_a_theorem(implies(implies(X_232,X_233),implies(implies(X_233,Z),implies(X_232,Z))))
| is_a_theorem(implies(X_233,implies(implies(X_233,Z),implies(X_232,Z)))) ),
inference(subst,[],[refute_0_12:[bind(X_49,$fot(X_232)),bind(X_50,$fot(X_233)),bind(X_51,$fot(implies(implies(X_233,Z),implies(X_232,Z))))]]) ).
cnf(refute_0_14,plain,
is_a_theorem(implies(X_233,implies(implies(X_233,Z),implies(X_232,Z)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_232,X_233),implies(implies(X_233,Z),implies(X_232,Z)))) )],[refute_0_6,refute_0_13]) ).
cnf(refute_0_15,plain,
is_a_theorem(implies(X_244,implies(implies(X_244,X_242),implies(X_243,X_242)))),
inference(subst,[],[refute_0_14:[bind(Z,$fot(X_242)),bind(X_232,$fot(X_243)),bind(X_233,$fot(X_244))]]) ).
cnf(refute_0_16,plain,
is_a_theorem(implies(implies(implies(implies(X_244,X_242),implies(X_243,X_242)),Z),implies(X_244,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_244,implies(implies(X_244,X_242),implies(X_243,X_242)))) )],[refute_0_15,refute_0_5]) ).
cnf(refute_0_17,plain,
is_a_theorem(implies(implies(implies(implies(X_390,X_388),implies(X_389,X_388)),X_387),implies(X_390,X_387))),
inference(subst,[],[refute_0_16:[bind(Z,$fot(X_387)),bind(X_242,$fot(X_388)),bind(X_243,$fot(X_389)),bind(X_244,$fot(X_390))]]) ).
cnf(refute_0_18,plain,
( ~ is_a_theorem(implies(implies(implies(X_390,X_388),implies(X_389,X_388)),X_387))
| is_a_theorem(implies(X_390,X_387)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_390,X_388),implies(X_389,X_388)),X_387),implies(X_390,X_387))) )],[refute_0_17,refute_0_4]) ).
cnf(refute_0_19,plain,
( ~ is_a_theorem(implies(implies(implies(X_390,X_662),implies(implies(X_390,X_662),X_662)),implies(implies(X_390,X_662),X_662)))
| is_a_theorem(implies(X_390,implies(implies(X_390,X_662),X_662))) ),
inference(subst,[],[refute_0_18:[bind(X_387,$fot(implies(implies(X_390,X_662),X_662))),bind(X_388,$fot(X_662)),bind(X_389,$fot(implies(X_390,X_662)))]]) ).
cnf(refute_0_20,plain,
( ~ is_a_theorem(implies(implies(X_59,X_60),implies(implies(implies(X_59,X_58),X_59),X_60)))
| is_a_theorem(implies(implies(implies(implies(implies(X_59,X_58),X_59),X_60),Z),implies(implies(X_59,X_60),Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(implies(X_59,X_60))),bind(Y,$fot(implies(implies(implies(X_59,X_58),X_59),X_60)))]]) ).
cnf(refute_0_21,plain,
is_a_theorem(implies(implies(implies(X_43,Y),X_43),X_43)),
inference(subst,[],[c0_3:[bind(X,$fot(X_43))]]) ).
cnf(refute_0_22,plain,
( ~ is_a_theorem(implies(implies(implies(X_43,Y),X_43),X_43))
| is_a_theorem(implies(implies(X_43,X_44),implies(implies(implies(X_43,Y),X_43),X_44))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(implies(implies(X_43,Y),X_43))),bind(Y,$fot(X_43)),bind(Z,$fot(X_44))]]) ).
cnf(refute_0_23,plain,
is_a_theorem(implies(implies(X_43,X_44),implies(implies(implies(X_43,Y),X_43),X_44))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_43,Y),X_43),X_43)) )],[refute_0_21,refute_0_22]) ).
cnf(refute_0_24,plain,
is_a_theorem(implies(implies(X_59,X_60),implies(implies(implies(X_59,X_58),X_59),X_60))),
inference(subst,[],[refute_0_23:[bind(Y,$fot(X_58)),bind(X_43,$fot(X_59)),bind(X_44,$fot(X_60))]]) ).
cnf(refute_0_25,plain,
is_a_theorem(implies(implies(implies(implies(implies(X_59,X_58),X_59),X_60),Z),implies(implies(X_59,X_60),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_59,X_60),implies(implies(implies(X_59,X_58),X_59),X_60))) )],[refute_0_24,refute_0_20]) ).
cnf(refute_0_26,plain,
is_a_theorem(implies(implies(implies(implies(implies(X_661,X_58),X_661),implies(X_661,X_58)),implies(X_661,X_58)),implies(implies(X_661,implies(X_661,X_58)),implies(X_661,X_58)))),
inference(subst,[],[refute_0_25:[bind(Z,$fot(implies(X_661,X_58))),bind(X_59,$fot(X_661)),bind(X_60,$fot(implies(X_661,X_58)))]]) ).
cnf(refute_0_27,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_562,X_563),X_562),X_562),X_561))
| ~ is_a_theorem(implies(implies(implies(implies(implies(X_562,X_563),X_562),X_562),X_561),X_561))
| is_a_theorem(X_561) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(implies(X_562,X_563),X_562),X_562),X_561))),bind(Y,$fot(X_561))]]) ).
cnf(refute_0_28,plain,
is_a_theorem(implies(implies(implies(X_9,Y),X_9),X_9)),
inference(subst,[],[c0_3:[bind(X,$fot(X_9))]]) ).
cnf(refute_0_29,plain,
( ~ is_a_theorem(implies(implies(X_9,Y),X_9))
| ~ is_a_theorem(implies(implies(implies(X_9,Y),X_9),X_9))
| is_a_theorem(X_9) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_9,Y),X_9))),bind(Y,$fot(X_9))]]) ).
cnf(refute_0_30,plain,
( ~ is_a_theorem(implies(implies(X_9,Y),X_9))
| is_a_theorem(X_9) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_9,Y),X_9),X_9)) )],[refute_0_28,refute_0_29]) ).
cnf(refute_0_31,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(implies(implies(X_557,X_558),X_557),X_557),X_556),X_556),X_556),implies(implies(implies(implies(implies(X_557,X_558),X_557),X_557),X_556),X_556)))
| is_a_theorem(implies(implies(implies(implies(implies(X_557,X_558),X_557),X_557),X_556),X_556)) ),
inference(subst,[],[refute_0_30:[bind(Y,$fot(X_556)),bind(X_9,$fot(implies(implies(implies(implies(implies(X_557,X_558),X_557),X_557),X_556),X_556)))]]) ).
cnf(refute_0_32,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(X_130,X_131),X_130),X_130),X_133),implies(X_132,X_133)))
| is_a_theorem(implies(implies(implies(X_132,X_133),Z),implies(implies(implies(implies(implies(X_130,X_131),X_130),X_130),X_133),Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(implies(implies(implies(implies(X_130,X_131),X_130),X_130),X_133))),bind(Y,$fot(implies(X_132,X_133)))]]) ).
cnf(refute_0_33,plain,
is_a_theorem(implies(X_8,implies(Y,X_8))),
inference(subst,[],[c0_2:[bind(X,$fot(X_8))]]) ).
cnf(refute_0_34,plain,
( ~ is_a_theorem(X_8)
| ~ is_a_theorem(implies(X_8,implies(Y,X_8)))
| is_a_theorem(implies(Y,X_8)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(X_8)),bind(Y,$fot(implies(Y,X_8)))]]) ).
cnf(refute_0_35,plain,
( ~ is_a_theorem(X_8)
| is_a_theorem(implies(Y,X_8)) ),
inference(resolve,[$cnf( is_a_theorem(implies(X_8,implies(Y,X_8))) )],[refute_0_33,refute_0_34]) ).
cnf(refute_0_36,plain,
( ~ is_a_theorem(implies(implies(implies(X,Y),X),X))
| is_a_theorem(implies(X_11,implies(implies(implies(X,Y),X),X))) ),
inference(subst,[],[refute_0_35:[bind(Y,$fot(X_11)),bind(X_8,$fot(implies(implies(implies(X,Y),X),X)))]]) ).
cnf(refute_0_37,plain,
is_a_theorem(implies(X_11,implies(implies(implies(X,Y),X),X))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X,Y),X),X)) )],[c0_3,refute_0_36]) ).
cnf(refute_0_38,plain,
is_a_theorem(implies(X_42,implies(implies(implies(X,Y),X),X))),
inference(subst,[],[refute_0_37:[bind(X_11,$fot(X_42))]]) ).
cnf(refute_0_39,plain,
( ~ is_a_theorem(implies(X_42,implies(implies(implies(X,Y),X),X)))
| is_a_theorem(implies(implies(implies(implies(implies(X,Y),X),X),X_44),implies(X_42,X_44))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(X_42)),bind(Y,$fot(implies(implies(implies(X,Y),X),X))),bind(Z,$fot(X_44))]]) ).
cnf(refute_0_40,plain,
is_a_theorem(implies(implies(implies(implies(implies(X,Y),X),X),X_44),implies(X_42,X_44))),
inference(resolve,[$cnf( is_a_theorem(implies(X_42,implies(implies(implies(X,Y),X),X))) )],[refute_0_38,refute_0_39]) ).
cnf(refute_0_41,plain,
is_a_theorem(implies(implies(implies(implies(implies(X_130,X_131),X_130),X_130),X_133),implies(X_132,X_133))),
inference(subst,[],[refute_0_40:[bind(X,$fot(X_130)),bind(Y,$fot(X_131)),bind(X_42,$fot(X_132)),bind(X_44,$fot(X_133))]]) ).
cnf(refute_0_42,plain,
is_a_theorem(implies(implies(implies(X_132,X_133),Z),implies(implies(implies(implies(implies(X_130,X_131),X_130),X_130),X_133),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(X_130,X_131),X_130),X_130),X_133),implies(X_132,X_133))) )],[refute_0_41,refute_0_32]) ).
cnf(refute_0_43,plain,
is_a_theorem(implies(implies(implies(implies(implies(implies(implies(X_557,X_558),X_557),X_557),X_556),X_556),X_556),implies(implies(implies(implies(implies(X_557,X_558),X_557),X_557),X_556),X_556))),
inference(subst,[],[refute_0_42:[bind(Z,$fot(X_556)),bind(X_130,$fot(X_557)),bind(X_131,$fot(X_558)),bind(X_132,$fot(implies(implies(implies(implies(X_557,X_558),X_557),X_557),X_556))),bind(X_133,$fot(X_556))]]) ).
cnf(refute_0_44,plain,
is_a_theorem(implies(implies(implies(implies(implies(X_557,X_558),X_557),X_557),X_556),X_556)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(implies(implies(X_557,X_558),X_557),X_557),X_556),X_556),X_556),implies(implies(implies(implies(implies(X_557,X_558),X_557),X_557),X_556),X_556))) )],[refute_0_43,refute_0_31]) ).
cnf(refute_0_45,plain,
is_a_theorem(implies(implies(implies(implies(implies(X_562,X_563),X_562),X_562),X_561),X_561)),
inference(subst,[],[refute_0_44:[bind(X_556,$fot(X_561)),bind(X_557,$fot(X_562)),bind(X_558,$fot(X_563))]]) ).
cnf(refute_0_46,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_562,X_563),X_562),X_562),X_561))
| is_a_theorem(X_561) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(X_562,X_563),X_562),X_562),X_561),X_561)) )],[refute_0_45,refute_0_27]) ).
cnf(refute_0_47,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(X_661,X_58),X_661),implies(X_661,X_58)),implies(X_661,X_58)),implies(implies(X_661,implies(X_661,X_58)),implies(X_661,X_58))))
| is_a_theorem(implies(implies(X_661,implies(X_661,X_58)),implies(X_661,X_58))) ),
inference(subst,[],[refute_0_46:[bind(X_561,$fot(implies(implies(X_661,implies(X_661,X_58)),implies(X_661,X_58)))),bind(X_562,$fot(implies(X_661,X_58))),bind(X_563,$fot(X_661))]]) ).
cnf(refute_0_48,plain,
is_a_theorem(implies(implies(X_661,implies(X_661,X_58)),implies(X_661,X_58))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(X_661,X_58),X_661),implies(X_661,X_58)),implies(X_661,X_58)),implies(implies(X_661,implies(X_661,X_58)),implies(X_661,X_58)))) )],[refute_0_26,refute_0_47]) ).
cnf(refute_0_49,plain,
is_a_theorem(implies(implies(implies(X_390,X_662),implies(implies(X_390,X_662),X_662)),implies(implies(X_390,X_662),X_662))),
inference(subst,[],[refute_0_48:[bind(X_58,$fot(X_662)),bind(X_661,$fot(implies(X_390,X_662)))]]) ).
cnf(refute_0_50,plain,
is_a_theorem(implies(X_390,implies(implies(X_390,X_662),X_662))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_390,X_662),implies(implies(X_390,X_662),X_662)),implies(implies(X_390,X_662),X_662))) )],[refute_0_49,refute_0_19]) ).
cnf(refute_0_51,plain,
is_a_theorem(implies(X_664,implies(implies(X_664,X_665),X_665))),
inference(subst,[],[refute_0_50:[bind(X_390,$fot(X_664)),bind(X_662,$fot(X_665))]]) ).
cnf(refute_0_52,plain,
is_a_theorem(implies(implies(implies(implies(X_664,X_665),X_665),Z),implies(X_664,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_664,implies(implies(X_664,X_665),X_665))) )],[refute_0_51,refute_0_3]) ).
cnf(refute_0_53,plain,
is_a_theorem(implies(implies(implies(implies(X_664,X_2973),X_2973),implies(X_2971,X_2973)),implies(X_664,implies(X_2971,X_2973)))),
inference(subst,[],[refute_0_52:[bind(Z,$fot(implies(X_2971,X_2973))),bind(X_665,$fot(X_2973))]]) ).
cnf(refute_0_54,plain,
( ~ is_a_theorem(implies(implies(implies(X_69,X_70),implies(X_68,X_70)),X_71))
| ~ is_a_theorem(implies(implies(implies(implies(X_69,X_70),implies(X_68,X_70)),X_71),implies(implies(X_68,X_69),X_71)))
| is_a_theorem(implies(implies(X_68,X_69),X_71)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(X_69,X_70),implies(X_68,X_70)),X_71))),bind(Y,$fot(implies(implies(X_68,X_69),X_71)))]]) ).
cnf(refute_0_55,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_44),implies(implies(X,Y),X_44))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(implies(X,Y))),bind(Y,$fot(implies(implies(Y,Z),implies(X,Z)))),bind(Z,$fot(X_44))]]) ).
cnf(refute_0_56,plain,
is_a_theorem(implies(implies(implies(implies(Y,Z),implies(X,Z)),X_44),implies(implies(X,Y),X_44))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )],[c0_1,refute_0_55]) ).
cnf(refute_0_57,plain,
is_a_theorem(implies(implies(implies(implies(X_69,X_70),implies(X_68,X_70)),X_71),implies(implies(X_68,X_69),X_71))),
inference(subst,[],[refute_0_56:[bind(X,$fot(X_68)),bind(Y,$fot(X_69)),bind(Z,$fot(X_70)),bind(X_44,$fot(X_71))]]) ).
cnf(refute_0_58,plain,
( ~ is_a_theorem(implies(implies(implies(X_69,X_70),implies(X_68,X_70)),X_71))
| is_a_theorem(implies(implies(X_68,X_69),X_71)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_69,X_70),implies(X_68,X_70)),X_71),implies(implies(X_68,X_69),X_71))) )],[refute_0_57,refute_0_54]) ).
cnf(refute_0_59,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_664,X_2973),X_2973),implies(X_2971,X_2973)),implies(X_664,implies(X_2971,X_2973))))
| is_a_theorem(implies(implies(X_2971,implies(X_664,X_2973)),implies(X_664,implies(X_2971,X_2973)))) ),
inference(subst,[],[refute_0_58:[bind(X_68,$fot(X_2971)),bind(X_69,$fot(implies(X_664,X_2973))),bind(X_70,$fot(X_2973)),bind(X_71,$fot(implies(X_664,implies(X_2971,X_2973))))]]) ).
cnf(refute_0_60,plain,
is_a_theorem(implies(implies(X_2971,implies(X_664,X_2973)),implies(X_664,implies(X_2971,X_2973)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_664,X_2973),X_2973),implies(X_2971,X_2973)),implies(X_664,implies(X_2971,X_2973)))) )],[refute_0_53,refute_0_59]) ).
cnf(refute_0_61,plain,
is_a_theorem(implies(implies(X_3087,implies(X_3089,X_3088)),implies(X_3089,implies(X_3087,X_3088)))),
inference(subst,[],[refute_0_60:[bind(X_2971,$fot(X_3087)),bind(X_2973,$fot(X_3088)),bind(X_664,$fot(X_3089))]]) ).
cnf(refute_0_62,plain,
( ~ is_a_theorem(implies(X_3087,implies(X_3089,X_3088)))
| is_a_theorem(implies(X_3089,implies(X_3087,X_3088))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_3087,implies(X_3089,X_3088)),implies(X_3089,implies(X_3087,X_3088)))) )],[refute_0_61,refute_0_0]) ).
cnf(refute_0_63,plain,
( ~ is_a_theorem(implies(implies(X_15576,X_15577),implies(implies(X_15576,implies(X_15577,X_15575)),implies(X_15576,X_15575))))
| is_a_theorem(implies(implies(X_15576,implies(X_15577,X_15575)),implies(implies(X_15576,X_15577),implies(X_15576,X_15575)))) ),
inference(subst,[],[refute_0_62:[bind(X_3087,$fot(implies(X_15576,X_15577))),bind(X_3088,$fot(implies(X_15576,X_15575))),bind(X_3089,$fot(implies(X_15576,implies(X_15577,X_15575))))]]) ).
cnf(refute_0_64,plain,
( ~ is_a_theorem(implies(implies(implies(X_69,X_15572),implies(X_15573,X_15572)),implies(implies(X_15573,implies(X_69,X_15572)),implies(X_15573,X_15572))))
| is_a_theorem(implies(implies(X_15573,X_69),implies(implies(X_15573,implies(X_69,X_15572)),implies(X_15573,X_15572)))) ),
inference(subst,[],[refute_0_58:[bind(X_68,$fot(X_15573)),bind(X_70,$fot(X_15572)),bind(X_71,$fot(implies(implies(X_15573,implies(X_69,X_15572)),implies(X_15573,X_15572))))]]) ).
cnf(refute_0_65,plain,
( ~ is_a_theorem(implies(X_3144,implies(implies(falsehood,X_3146),X_3145)))
| ~ is_a_theorem(implies(implies(X_3144,implies(implies(falsehood,X_3146),X_3145)),implies(X_3144,X_3145)))
| is_a_theorem(implies(X_3144,X_3145)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X_3144,implies(implies(falsehood,X_3146),X_3145)))),bind(Y,$fot(implies(X_3144,X_3145)))]]) ).
cnf(refute_0_66,plain,
( ~ is_a_theorem(implies(X_82,implies(implies(implies(falsehood,X_84),X_83),X_83)))
| is_a_theorem(implies(implies(implies(implies(implies(falsehood,X_84),X_83),X_83),Z),implies(X_82,Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(X_82)),bind(Y,$fot(implies(implies(implies(falsehood,X_84),X_83),X_83)))]]) ).
cnf(refute_0_67,plain,
( ~ is_a_theorem(implies(implies(implies(falsehood,X_77),X_76),X_76))
| is_a_theorem(implies(Y,implies(implies(implies(falsehood,X_77),X_76),X_76))) ),
inference(subst,[],[refute_0_35:[bind(X_8,$fot(implies(implies(implies(falsehood,X_77),X_76),X_76)))]]) ).
cnf(refute_0_68,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(falsehood,X_73),X_72),X_72),X_72),implies(implies(implies(falsehood,X_73),X_72),X_72)))
| is_a_theorem(implies(implies(implies(falsehood,X_73),X_72),X_72)) ),
inference(subst,[],[refute_0_30:[bind(Y,$fot(X_72)),bind(X_9,$fot(implies(implies(implies(falsehood,X_73),X_72),X_72)))]]) ).
cnf(refute_0_69,plain,
( ~ is_a_theorem(implies(implies(implies(falsehood,X_55),X_57),implies(X_56,X_57)))
| is_a_theorem(implies(implies(implies(X_56,X_57),Z),implies(implies(implies(falsehood,X_55),X_57),Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(implies(implies(falsehood,X_55),X_57))),bind(Y,$fot(implies(X_56,X_57)))]]) ).
cnf(refute_0_70,plain,
( ~ is_a_theorem(implies(falsehood,X))
| is_a_theorem(implies(X_11,implies(falsehood,X))) ),
inference(subst,[],[refute_0_35:[bind(Y,$fot(X_11)),bind(X_8,$fot(implies(falsehood,X)))]]) ).
cnf(refute_0_71,plain,
is_a_theorem(implies(X_11,implies(falsehood,X))),
inference(resolve,[$cnf( is_a_theorem(implies(falsehood,X)) )],[c0_4,refute_0_70]) ).
cnf(refute_0_72,plain,
is_a_theorem(implies(X_42,implies(falsehood,X))),
inference(subst,[],[refute_0_71:[bind(X_11,$fot(X_42))]]) ).
cnf(refute_0_73,plain,
( ~ is_a_theorem(implies(X_42,implies(falsehood,X)))
| is_a_theorem(implies(implies(implies(falsehood,X),X_44),implies(X_42,X_44))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(X_42)),bind(Y,$fot(implies(falsehood,X))),bind(Z,$fot(X_44))]]) ).
cnf(refute_0_74,plain,
is_a_theorem(implies(implies(implies(falsehood,X),X_44),implies(X_42,X_44))),
inference(resolve,[$cnf( is_a_theorem(implies(X_42,implies(falsehood,X))) )],[refute_0_72,refute_0_73]) ).
cnf(refute_0_75,plain,
is_a_theorem(implies(implies(implies(falsehood,X_55),X_57),implies(X_56,X_57))),
inference(subst,[],[refute_0_74:[bind(X,$fot(X_55)),bind(X_42,$fot(X_56)),bind(X_44,$fot(X_57))]]) ).
cnf(refute_0_76,plain,
is_a_theorem(implies(implies(implies(X_56,X_57),Z),implies(implies(implies(falsehood,X_55),X_57),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(falsehood,X_55),X_57),implies(X_56,X_57))) )],[refute_0_75,refute_0_69]) ).
cnf(refute_0_77,plain,
is_a_theorem(implies(implies(implies(implies(implies(falsehood,X_73),X_72),X_72),X_72),implies(implies(implies(falsehood,X_73),X_72),X_72))),
inference(subst,[],[refute_0_76:[bind(Z,$fot(X_72)),bind(X_55,$fot(X_73)),bind(X_56,$fot(implies(implies(falsehood,X_73),X_72))),bind(X_57,$fot(X_72))]]) ).
cnf(refute_0_78,plain,
is_a_theorem(implies(implies(implies(falsehood,X_73),X_72),X_72)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(falsehood,X_73),X_72),X_72),X_72),implies(implies(implies(falsehood,X_73),X_72),X_72))) )],[refute_0_77,refute_0_68]) ).
cnf(refute_0_79,plain,
is_a_theorem(implies(implies(implies(falsehood,X_77),X_76),X_76)),
inference(subst,[],[refute_0_78:[bind(X_72,$fot(X_76)),bind(X_73,$fot(X_77))]]) ).
cnf(refute_0_80,plain,
is_a_theorem(implies(Y,implies(implies(implies(falsehood,X_77),X_76),X_76))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(falsehood,X_77),X_76),X_76)) )],[refute_0_79,refute_0_67]) ).
cnf(refute_0_81,plain,
is_a_theorem(implies(X_82,implies(implies(implies(falsehood,X_84),X_83),X_83))),
inference(subst,[],[refute_0_80:[bind(Y,$fot(X_82)),bind(X_76,$fot(X_83)),bind(X_77,$fot(X_84))]]) ).
cnf(refute_0_82,plain,
is_a_theorem(implies(implies(implies(implies(implies(falsehood,X_84),X_83),X_83),Z),implies(X_82,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_82,implies(implies(implies(falsehood,X_84),X_83),X_83))) )],[refute_0_81,refute_0_66]) ).
cnf(refute_0_83,plain,
is_a_theorem(implies(implies(implies(implies(implies(falsehood,X_84),X_83),X_83),X_1405),implies(implies(implies(implies(implies(falsehood,X_84),X_83),X_83),X_1405),X_1405))),
inference(subst,[],[refute_0_82:[bind(Z,$fot(X_1405)),bind(X_82,$fot(implies(implies(implies(implies(falsehood,X_84),X_83),X_83),X_1405)))]]) ).
cnf(refute_0_84,plain,
( ~ is_a_theorem(implies(X_663,implies(X_663,X_662)))
| ~ is_a_theorem(implies(implies(X_663,implies(X_663,X_662)),implies(X_663,X_662)))
| is_a_theorem(implies(X_663,X_662)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X_663,implies(X_663,X_662)))),bind(Y,$fot(implies(X_663,X_662)))]]) ).
cnf(refute_0_85,plain,
is_a_theorem(implies(implies(X_663,implies(X_663,X_662)),implies(X_663,X_662))),
inference(subst,[],[refute_0_48:[bind(X_58,$fot(X_662)),bind(X_661,$fot(X_663))]]) ).
cnf(refute_0_86,plain,
( ~ is_a_theorem(implies(X_663,implies(X_663,X_662)))
| is_a_theorem(implies(X_663,X_662)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_663,implies(X_663,X_662)),implies(X_663,X_662))) )],[refute_0_85,refute_0_84]) ).
cnf(refute_0_87,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(falsehood,X_84),X_83),X_83),X_1405),implies(implies(implies(implies(implies(falsehood,X_84),X_83),X_83),X_1405),X_1405)))
| is_a_theorem(implies(implies(implies(implies(implies(falsehood,X_84),X_83),X_83),X_1405),X_1405)) ),
inference(subst,[],[refute_0_86:[bind(X_662,$fot(X_1405)),bind(X_663,$fot(implies(implies(implies(implies(falsehood,X_84),X_83),X_83),X_1405)))]]) ).
cnf(refute_0_88,plain,
is_a_theorem(implies(implies(implies(implies(implies(falsehood,X_84),X_83),X_83),X_1405),X_1405)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(falsehood,X_84),X_83),X_83),X_1405),implies(implies(implies(implies(implies(falsehood,X_84),X_83),X_83),X_1405),X_1405))) )],[refute_0_83,refute_0_87]) ).
cnf(refute_0_89,plain,
is_a_theorem(implies(implies(implies(implies(implies(falsehood,X_84),X_2973),X_2973),implies(X_2971,X_2973)),implies(X_2971,X_2973))),
inference(subst,[],[refute_0_88:[bind(X_1405,$fot(implies(X_2971,X_2973))),bind(X_83,$fot(X_2973))]]) ).
cnf(refute_0_90,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(falsehood,X_84),X_2973),X_2973),implies(X_2971,X_2973)),implies(X_2971,X_2973)))
| is_a_theorem(implies(implies(X_2971,implies(implies(falsehood,X_84),X_2973)),implies(X_2971,X_2973))) ),
inference(subst,[],[refute_0_58:[bind(X_68,$fot(X_2971)),bind(X_69,$fot(implies(implies(falsehood,X_84),X_2973))),bind(X_70,$fot(X_2973)),bind(X_71,$fot(implies(X_2971,X_2973)))]]) ).
cnf(refute_0_91,plain,
is_a_theorem(implies(implies(X_2971,implies(implies(falsehood,X_84),X_2973)),implies(X_2971,X_2973))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(falsehood,X_84),X_2973),X_2973),implies(X_2971,X_2973)),implies(X_2971,X_2973))) )],[refute_0_89,refute_0_90]) ).
cnf(refute_0_92,plain,
is_a_theorem(implies(implies(X_3144,implies(implies(falsehood,X_3146),X_3145)),implies(X_3144,X_3145))),
inference(subst,[],[refute_0_91:[bind(X_2971,$fot(X_3144)),bind(X_2973,$fot(X_3145)),bind(X_84,$fot(X_3146))]]) ).
cnf(refute_0_93,plain,
( ~ is_a_theorem(implies(X_3144,implies(implies(falsehood,X_3146),X_3145)))
| is_a_theorem(implies(X_3144,X_3145)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_3144,implies(implies(falsehood,X_3146),X_3145)),implies(X_3144,X_3145))) )],[refute_0_92,refute_0_65]) ).
cnf(refute_0_94,plain,
( ~ is_a_theorem(implies(implies(X_5858,X_5859),implies(implies(falsehood,X_3146),implies(implies(X_5859,implies(X_5858,X_5857)),implies(X_5858,X_5857)))))
| is_a_theorem(implies(implies(X_5858,X_5859),implies(implies(X_5859,implies(X_5858,X_5857)),implies(X_5858,X_5857)))) ),
inference(subst,[],[refute_0_93:[bind(X_3144,$fot(implies(X_5858,X_5859))),bind(X_3145,$fot(implies(implies(X_5859,implies(X_5858,X_5857)),implies(X_5858,X_5857))))]]) ).
cnf(refute_0_95,plain,
( ~ is_a_theorem(implies(implies(implies(X_69,implies(X_5854,X_5853)),implies(X_5854,implies(X_5854,X_5853))),implies(X_5852,implies(implies(X_69,implies(X_5854,X_5853)),implies(X_5854,X_5853)))))
| is_a_theorem(implies(implies(X_5854,X_69),implies(X_5852,implies(implies(X_69,implies(X_5854,X_5853)),implies(X_5854,X_5853))))) ),
inference(subst,[],[refute_0_58:[bind(X_68,$fot(X_5854)),bind(X_70,$fot(implies(X_5854,X_5853))),bind(X_71,$fot(implies(X_5852,implies(implies(X_69,implies(X_5854,X_5853)),implies(X_5854,X_5853)))))]]) ).
cnf(refute_0_96,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_5851,implies(X_5851,X_5850)),implies(X_5851,X_5850)),implies(X_68,implies(X_5851,X_5850))),implies(X_5849,implies(X_68,implies(X_5851,X_5850)))))
| is_a_theorem(implies(implies(X_68,implies(X_5851,implies(X_5851,X_5850))),implies(X_5849,implies(X_68,implies(X_5851,X_5850))))) ),
inference(subst,[],[refute_0_58:[bind(X_69,$fot(implies(X_5851,implies(X_5851,X_5850)))),bind(X_70,$fot(implies(X_5851,X_5850))),bind(X_71,$fot(implies(X_5849,implies(X_68,implies(X_5851,X_5850)))))]]) ).
cnf(refute_0_97,plain,
( ~ is_a_theorem(implies(implies(X_541,X_540),X_541))
| ~ is_a_theorem(implies(implies(implies(X_541,X_540),X_541),implies(implies(X_541,X_538),implies(X_539,X_538))))
| is_a_theorem(implies(implies(X_541,X_538),implies(X_539,X_538))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_541,X_540),X_541))),bind(Y,$fot(implies(implies(X_541,X_538),implies(X_539,X_538))))]]) ).
cnf(refute_0_98,plain,
is_a_theorem(implies(X_262,implies(implies(X_262,Z),implies(X_232,Z)))),
inference(subst,[],[refute_0_14:[bind(X_233,$fot(X_262))]]) ).
cnf(refute_0_99,plain,
( ~ is_a_theorem(implies(X_59,X_60))
| ~ is_a_theorem(implies(implies(X_59,X_60),implies(implies(implies(X_59,X_58),X_59),X_60)))
| is_a_theorem(implies(implies(implies(X_59,X_58),X_59),X_60)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X_59,X_60))),bind(Y,$fot(implies(implies(implies(X_59,X_58),X_59),X_60)))]]) ).
cnf(refute_0_100,plain,
( ~ is_a_theorem(implies(X_59,X_60))
| is_a_theorem(implies(implies(implies(X_59,X_58),X_59),X_60)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_59,X_60),implies(implies(implies(X_59,X_58),X_59),X_60))) )],[refute_0_24,refute_0_99]) ).
cnf(refute_0_101,plain,
( ~ is_a_theorem(implies(X_262,implies(implies(X_262,Z),implies(X_232,Z))))
| is_a_theorem(implies(implies(implies(X_262,X_261),X_262),implies(implies(X_262,Z),implies(X_232,Z)))) ),
inference(subst,[],[refute_0_100:[bind(X_58,$fot(X_261)),bind(X_59,$fot(X_262)),bind(X_60,$fot(implies(implies(X_262,Z),implies(X_232,Z))))]]) ).
cnf(refute_0_102,plain,
is_a_theorem(implies(implies(implies(X_262,X_261),X_262),implies(implies(X_262,Z),implies(X_232,Z)))),
inference(resolve,[$cnf( is_a_theorem(implies(X_262,implies(implies(X_262,Z),implies(X_232,Z)))) )],[refute_0_98,refute_0_101]) ).
cnf(refute_0_103,plain,
is_a_theorem(implies(implies(implies(X_541,X_540),X_541),implies(implies(X_541,X_538),implies(X_539,X_538)))),
inference(subst,[],[refute_0_102:[bind(Z,$fot(X_538)),bind(X_232,$fot(X_539)),bind(X_261,$fot(X_540)),bind(X_262,$fot(X_541))]]) ).
cnf(refute_0_104,plain,
( ~ is_a_theorem(implies(implies(X_541,X_540),X_541))
| is_a_theorem(implies(implies(X_541,X_538),implies(X_539,X_538))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_541,X_540),X_541),implies(implies(X_541,X_538),implies(X_539,X_538)))) )],[refute_0_103,refute_0_97]) ).
cnf(refute_0_105,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_5846,implies(X_5846,X_5845)),implies(X_5846,X_5845)),implies(X_5846,X_5845)),implies(implies(X_5846,implies(X_5846,X_5845)),implies(X_5846,X_5845))))
| is_a_theorem(implies(implies(implies(implies(X_5846,implies(X_5846,X_5845)),implies(X_5846,X_5845)),X_538),implies(X_539,X_538))) ),
inference(subst,[],[refute_0_104:[bind(X_540,$fot(implies(X_5846,X_5845))),bind(X_541,$fot(implies(implies(X_5846,implies(X_5846,X_5845)),implies(X_5846,X_5845))))]]) ).
cnf(refute_0_106,plain,
( ~ is_a_theorem(implies(implies(X_855,implies(X_855,X_854)),implies(X_856,implies(X_855,X_854))))
| is_a_theorem(implies(implies(implies(X_856,implies(X_855,X_854)),Z),implies(implies(X_855,implies(X_855,X_854)),Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(implies(X_855,implies(X_855,X_854)))),bind(Y,$fot(implies(X_856,implies(X_855,X_854))))]]) ).
cnf(refute_0_107,plain,
( ~ is_a_theorem(implies(implies(falsehood,X_77),X_76))
| ~ is_a_theorem(implies(implies(implies(falsehood,X_77),X_76),X_76))
| is_a_theorem(X_76) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(falsehood,X_77),X_76))),bind(Y,$fot(X_76))]]) ).
cnf(refute_0_108,plain,
( ~ is_a_theorem(implies(implies(falsehood,X_77),X_76))
| is_a_theorem(X_76) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(falsehood,X_77),X_76),X_76)) )],[refute_0_79,refute_0_107]) ).
cnf(refute_0_109,plain,
( ~ is_a_theorem(implies(implies(falsehood,X_77),implies(implies(X_851,implies(X_851,X_850)),implies(X_852,implies(X_851,X_850)))))
| is_a_theorem(implies(implies(X_851,implies(X_851,X_850)),implies(X_852,implies(X_851,X_850)))) ),
inference(subst,[],[refute_0_108:[bind(X_76,$fot(implies(implies(X_851,implies(X_851,X_850)),implies(X_852,implies(X_851,X_850)))))]]) ).
cnf(refute_0_110,plain,
( ~ is_a_theorem(implies(implies(X_663,implies(X_663,X_662)),implies(X_663,X_662)))
| is_a_theorem(implies(implies(implies(X_663,X_662),Z),implies(implies(X_663,implies(X_663,X_662)),Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(implies(X_663,implies(X_663,X_662)))),bind(Y,$fot(implies(X_663,X_662)))]]) ).
cnf(refute_0_111,plain,
is_a_theorem(implies(implies(implies(X_663,X_662),Z),implies(implies(X_663,implies(X_663,X_662)),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_663,implies(X_663,X_662)),implies(X_663,X_662))) )],[refute_0_85,refute_0_110]) ).
cnf(refute_0_112,plain,
is_a_theorem(implies(implies(implies(X_663,X_662),implies(X_847,implies(X_663,X_662))),implies(implies(X_663,implies(X_663,X_662)),implies(X_847,implies(X_663,X_662))))),
inference(subst,[],[refute_0_111:[bind(Z,$fot(implies(X_847,implies(X_663,X_662))))]]) ).
cnf(refute_0_113,plain,
( ~ is_a_theorem(implies(implies(X_45,implies(X_46,X_45)),X_48))
| ~ is_a_theorem(implies(implies(implies(X_45,implies(X_46,X_45)),X_48),implies(X_47,X_48)))
| is_a_theorem(implies(X_47,X_48)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_45,implies(X_46,X_45)),X_48))),bind(Y,$fot(implies(X_47,X_48)))]]) ).
cnf(refute_0_114,plain,
( ~ is_a_theorem(implies(X,implies(Y,X)))
| is_a_theorem(implies(X_11,implies(X,implies(Y,X)))) ),
inference(subst,[],[refute_0_35:[bind(Y,$fot(X_11)),bind(X_8,$fot(implies(X,implies(Y,X))))]]) ).
cnf(refute_0_115,plain,
is_a_theorem(implies(X_11,implies(X,implies(Y,X)))),
inference(resolve,[$cnf( is_a_theorem(implies(X,implies(Y,X))) )],[c0_2,refute_0_114]) ).
cnf(refute_0_116,plain,
is_a_theorem(implies(X_42,implies(X,implies(Y,X)))),
inference(subst,[],[refute_0_115:[bind(X_11,$fot(X_42))]]) ).
cnf(refute_0_117,plain,
( ~ is_a_theorem(implies(X_42,implies(X,implies(Y,X))))
| is_a_theorem(implies(implies(implies(X,implies(Y,X)),X_44),implies(X_42,X_44))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(X_42)),bind(Y,$fot(implies(X,implies(Y,X)))),bind(Z,$fot(X_44))]]) ).
cnf(refute_0_118,plain,
is_a_theorem(implies(implies(implies(X,implies(Y,X)),X_44),implies(X_42,X_44))),
inference(resolve,[$cnf( is_a_theorem(implies(X_42,implies(X,implies(Y,X)))) )],[refute_0_116,refute_0_117]) ).
cnf(refute_0_119,plain,
is_a_theorem(implies(implies(implies(X_45,implies(X_46,X_45)),X_48),implies(X_47,X_48))),
inference(subst,[],[refute_0_118:[bind(X,$fot(X_45)),bind(Y,$fot(X_46)),bind(X_42,$fot(X_47)),bind(X_44,$fot(X_48))]]) ).
cnf(refute_0_120,plain,
( ~ is_a_theorem(implies(implies(X_45,implies(X_46,X_45)),X_48))
| is_a_theorem(implies(X_47,X_48)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_45,implies(X_46,X_45)),X_48),implies(X_47,X_48))) )],[refute_0_119,refute_0_113]) ).
cnf(refute_0_121,plain,
( ~ is_a_theorem(implies(implies(implies(X_663,X_662),implies(X_847,implies(X_663,X_662))),implies(implies(X_663,implies(X_663,X_662)),implies(X_847,implies(X_663,X_662)))))
| is_a_theorem(implies(X_848,implies(implies(X_663,implies(X_663,X_662)),implies(X_847,implies(X_663,X_662))))) ),
inference(subst,[],[refute_0_120:[bind(X_45,$fot(implies(X_663,X_662))),bind(X_46,$fot(X_847)),bind(X_47,$fot(X_848)),bind(X_48,$fot(implies(implies(X_663,implies(X_663,X_662)),implies(X_847,implies(X_663,X_662)))))]]) ).
cnf(refute_0_122,plain,
is_a_theorem(implies(X_848,implies(implies(X_663,implies(X_663,X_662)),implies(X_847,implies(X_663,X_662))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_663,X_662),implies(X_847,implies(X_663,X_662))),implies(implies(X_663,implies(X_663,X_662)),implies(X_847,implies(X_663,X_662))))) )],[refute_0_112,refute_0_121]) ).
cnf(refute_0_123,plain,
is_a_theorem(implies(implies(falsehood,X_77),implies(implies(X_851,implies(X_851,X_850)),implies(X_852,implies(X_851,X_850))))),
inference(subst,[],[refute_0_122:[bind(X_662,$fot(X_850)),bind(X_663,$fot(X_851)),bind(X_847,$fot(X_852)),bind(X_848,$fot(implies(falsehood,X_77)))]]) ).
cnf(refute_0_124,plain,
is_a_theorem(implies(implies(X_851,implies(X_851,X_850)),implies(X_852,implies(X_851,X_850)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(falsehood,X_77),implies(implies(X_851,implies(X_851,X_850)),implies(X_852,implies(X_851,X_850))))) )],[refute_0_123,refute_0_109]) ).
cnf(refute_0_125,plain,
is_a_theorem(implies(implies(X_855,implies(X_855,X_854)),implies(X_856,implies(X_855,X_854)))),
inference(subst,[],[refute_0_124:[bind(X_850,$fot(X_854)),bind(X_851,$fot(X_855)),bind(X_852,$fot(X_856))]]) ).
cnf(refute_0_126,plain,
is_a_theorem(implies(implies(implies(X_856,implies(X_855,X_854)),Z),implies(implies(X_855,implies(X_855,X_854)),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_855,implies(X_855,X_854)),implies(X_856,implies(X_855,X_854)))) )],[refute_0_125,refute_0_106]) ).
cnf(refute_0_127,plain,
is_a_theorem(implies(implies(implies(implies(X_5846,implies(X_5846,X_5845)),implies(X_5846,X_5845)),implies(X_5846,X_5845)),implies(implies(X_5846,implies(X_5846,X_5845)),implies(X_5846,X_5845)))),
inference(subst,[],[refute_0_126:[bind(Z,$fot(implies(X_5846,X_5845))),bind(X_854,$fot(X_5845)),bind(X_855,$fot(X_5846)),bind(X_856,$fot(implies(X_5846,implies(X_5846,X_5845))))]]) ).
cnf(refute_0_128,plain,
is_a_theorem(implies(implies(implies(implies(X_5846,implies(X_5846,X_5845)),implies(X_5846,X_5845)),X_538),implies(X_539,X_538))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_5846,implies(X_5846,X_5845)),implies(X_5846,X_5845)),implies(X_5846,X_5845)),implies(implies(X_5846,implies(X_5846,X_5845)),implies(X_5846,X_5845)))) )],[refute_0_127,refute_0_105]) ).
cnf(refute_0_129,plain,
is_a_theorem(implies(implies(implies(implies(X_5851,implies(X_5851,X_5850)),implies(X_5851,X_5850)),implies(X_68,implies(X_5851,X_5850))),implies(X_5849,implies(X_68,implies(X_5851,X_5850))))),
inference(subst,[],[refute_0_128:[bind(X_538,$fot(implies(X_68,implies(X_5851,X_5850)))),bind(X_539,$fot(X_5849)),bind(X_5845,$fot(X_5850)),bind(X_5846,$fot(X_5851))]]) ).
cnf(refute_0_130,plain,
is_a_theorem(implies(implies(X_68,implies(X_5851,implies(X_5851,X_5850))),implies(X_5849,implies(X_68,implies(X_5851,X_5850))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_5851,implies(X_5851,X_5850)),implies(X_5851,X_5850)),implies(X_68,implies(X_5851,X_5850))),implies(X_5849,implies(X_68,implies(X_5851,X_5850))))) )],[refute_0_129,refute_0_96]) ).
cnf(refute_0_131,plain,
is_a_theorem(implies(implies(implies(X_69,implies(X_5854,X_5853)),implies(X_5854,implies(X_5854,X_5853))),implies(X_5852,implies(implies(X_69,implies(X_5854,X_5853)),implies(X_5854,X_5853))))),
inference(subst,[],[refute_0_130:[bind(X_5849,$fot(X_5852)),bind(X_5850,$fot(X_5853)),bind(X_5851,$fot(X_5854)),bind(X_68,$fot(implies(X_69,implies(X_5854,X_5853))))]]) ).
cnf(refute_0_132,plain,
is_a_theorem(implies(implies(X_5854,X_69),implies(X_5852,implies(implies(X_69,implies(X_5854,X_5853)),implies(X_5854,X_5853))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_69,implies(X_5854,X_5853)),implies(X_5854,implies(X_5854,X_5853))),implies(X_5852,implies(implies(X_69,implies(X_5854,X_5853)),implies(X_5854,X_5853))))) )],[refute_0_131,refute_0_95]) ).
cnf(refute_0_133,plain,
is_a_theorem(implies(implies(X_5858,X_5859),implies(implies(falsehood,X_3146),implies(implies(X_5859,implies(X_5858,X_5857)),implies(X_5858,X_5857))))),
inference(subst,[],[refute_0_132:[bind(X_5852,$fot(implies(falsehood,X_3146))),bind(X_5853,$fot(X_5857)),bind(X_5854,$fot(X_5858)),bind(X_69,$fot(X_5859))]]) ).
cnf(refute_0_134,plain,
is_a_theorem(implies(implies(X_5858,X_5859),implies(implies(X_5859,implies(X_5858,X_5857)),implies(X_5858,X_5857)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_5858,X_5859),implies(implies(falsehood,X_3146),implies(implies(X_5859,implies(X_5858,X_5857)),implies(X_5858,X_5857))))) )],[refute_0_133,refute_0_94]) ).
cnf(refute_0_135,plain,
( ~ is_a_theorem(implies(implies(X_5858,X_5859),implies(implies(X_5859,implies(X_5858,X_5857)),implies(X_5858,X_5857))))
| is_a_theorem(implies(implies(X_5859,implies(X_5858,X_5857)),implies(implies(X_5858,X_5859),implies(X_5858,X_5857)))) ),
inference(subst,[],[refute_0_62:[bind(X_3087,$fot(implies(X_5858,X_5859))),bind(X_3088,$fot(implies(X_5858,X_5857))),bind(X_3089,$fot(implies(X_5859,implies(X_5858,X_5857))))]]) ).
cnf(refute_0_136,plain,
is_a_theorem(implies(implies(X_5859,implies(X_5858,X_5857)),implies(implies(X_5858,X_5859),implies(X_5858,X_5857)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_5858,X_5859),implies(implies(X_5859,implies(X_5858,X_5857)),implies(X_5858,X_5857)))) )],[refute_0_134,refute_0_135]) ).
cnf(refute_0_137,plain,
is_a_theorem(implies(implies(implies(X_69,X_15572),implies(X_15573,X_15572)),implies(implies(X_15573,implies(X_69,X_15572)),implies(X_15573,X_15572)))),
inference(subst,[],[refute_0_136:[bind(X_5857,$fot(X_15572)),bind(X_5858,$fot(X_15573)),bind(X_5859,$fot(implies(X_69,X_15572)))]]) ).
cnf(refute_0_138,plain,
is_a_theorem(implies(implies(X_15573,X_69),implies(implies(X_15573,implies(X_69,X_15572)),implies(X_15573,X_15572)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_69,X_15572),implies(X_15573,X_15572)),implies(implies(X_15573,implies(X_69,X_15572)),implies(X_15573,X_15572)))) )],[refute_0_137,refute_0_64]) ).
cnf(refute_0_139,plain,
is_a_theorem(implies(implies(X_15576,X_15577),implies(implies(X_15576,implies(X_15577,X_15575)),implies(X_15576,X_15575)))),
inference(subst,[],[refute_0_138:[bind(X_15572,$fot(X_15575)),bind(X_15573,$fot(X_15576)),bind(X_69,$fot(X_15577))]]) ).
cnf(refute_0_140,plain,
is_a_theorem(implies(implies(X_15576,implies(X_15577,X_15575)),implies(implies(X_15576,X_15577),implies(X_15576,X_15575)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_15576,X_15577),implies(implies(X_15576,implies(X_15577,X_15575)),implies(X_15576,X_15575)))) )],[refute_0_139,refute_0_63]) ).
cnf(refute_0_141,plain,
is_a_theorem(implies(implies(a,implies(b,c)),implies(implies(a,b),implies(a,c)))),
inference(subst,[],[refute_0_140:[bind(X_15575,$fot(c)),bind(X_15576,$fot(a)),bind(X_15577,$fot(b))]]) ).
cnf(refute_0_142,plain,
$false,
inference(resolve,[$cnf( is_a_theorem(implies(implies(a,implies(b,c)),implies(implies(a,b),implies(a,c)))) )],[refute_0_141,prove_c0_6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL030-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : metis --show proof --show saturation %s
% 0.12/0.36 % Computer : n003.cluster.edu
% 0.12/0.36 % Model : x86_64 x86_64
% 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.36 % Memory : 8046.5625MB
% 0.12/0.36 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sat Sep 5 16:07:51 UTC 2026
% 0.15/0.37 % CPUTime :
% 0.15/0.37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 216.33/216.67 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 216.33/216.67
% 216.33/216.67 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 216.43/216.74
%------------------------------------------------------------------------------