%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : LCL050-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n020.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:43 PM UTC 2026
% Result : Unsatisfiable 85.94s 86.25s
% Output : CNFRefutation 86.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 70
% Number of leaves : 5
% Syntax : Number of clauses : 249 ( 145 unt; 0 nHn; 63 RR)
% Number of literals : 373 ( 0 equ; 125 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 : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 731 ( 163 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_cn_21,negated_conjecture,
~ is_a_theorem(implies(implies(a,implies(b,c)),implies(b,implies(a,c)))) ).
cnf(refute_0_0,plain,
( ~ is_a_theorem(implies(implies(implies(X_129,X_130),implies(X_128,X_130)),X_131))
| ~ is_a_theorem(implies(implies(implies(implies(X_129,X_130),implies(X_128,X_130)),X_131),implies(implies(X_128,X_129),X_131)))
| is_a_theorem(implies(implies(X_128,X_129),X_131)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(X_129,X_130),implies(X_128,X_130)),X_131))),bind(Y,$fot(implies(implies(X_128,X_129),X_131)))]]) ).
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)))) )],[cn_1,refute_0_1]) ).
cnf(refute_0_3,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_43),implies(implies(X,Y),X_43))) ),
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_43))]]) ).
cnf(refute_0_4,plain,
is_a_theorem(implies(implies(implies(implies(Y,Z),implies(X,Z)),X_43),implies(implies(X,Y),X_43))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )],[cn_1,refute_0_3]) ).
cnf(refute_0_5,plain,
is_a_theorem(implies(implies(implies(implies(X_129,X_130),implies(X_128,X_130)),X_131),implies(implies(X_128,X_129),X_131))),
inference(subst,[],[refute_0_4:[bind(X,$fot(X_128)),bind(Y,$fot(X_129)),bind(Z,$fot(X_130)),bind(X_43,$fot(X_131))]]) ).
cnf(refute_0_6,plain,
( ~ is_a_theorem(implies(implies(implies(X_129,X_130),implies(X_128,X_130)),X_131))
| is_a_theorem(implies(implies(X_128,X_129),X_131)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_129,X_130),implies(X_128,X_130)),X_131),implies(implies(X_128,X_129),X_131))) )],[refute_0_5,refute_0_0]) ).
cnf(refute_0_7,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_36169,X_36170),X_36170),implies(X_128,X_36170)),implies(X_36169,implies(X_128,X_36170))))
| is_a_theorem(implies(implies(X_128,implies(X_36169,X_36170)),implies(X_36169,implies(X_128,X_36170)))) ),
inference(subst,[],[refute_0_6:[bind(X_129,$fot(implies(X_36169,X_36170))),bind(X_130,$fot(X_36170)),bind(X_131,$fot(implies(X_36169,implies(X_128,X_36170))))]]) ).
cnf(refute_0_8,plain,
( ~ is_a_theorem(implies(X_36144,implies(implies(X_36144,X_36145),X_36145)))
| is_a_theorem(implies(implies(implies(implies(X_36144,X_36145),X_36145),Z),implies(X_36144,Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(X_36144)),bind(Y,$fot(implies(implies(X_36144,X_36145),X_36145)))]]) ).
cnf(refute_0_9,plain,
( ~ is_a_theorem(implies(implies(X_371,implies(not(X_372),X_370)),X_369))
| ~ is_a_theorem(implies(implies(implies(X_371,implies(not(X_372),X_370)),X_369),implies(X_372,X_369)))
| is_a_theorem(implies(X_372,X_369)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_371,implies(not(X_372),X_370)),X_369))),bind(Y,$fot(implies(X_372,X_369)))]]) ).
cnf(refute_0_10,plain,
( ~ is_a_theorem(implies(X_326,implies(X_325,implies(not(X_326),X_324))))
| is_a_theorem(implies(implies(implies(X_325,implies(not(X_326),X_324)),Z),implies(X_326,Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(X_326)),bind(Y,$fot(implies(X_325,implies(not(X_326),X_324))))]]) ).
cnf(refute_0_11,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_47),X_46),X_48),implies(X_47,X_48)))
| ~ is_a_theorem(implies(implies(not(X_47),X_46),X_48))
| is_a_theorem(implies(X_47,X_48)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(not(X_47),X_46),X_48))),bind(Y,$fot(implies(X_47,X_48)))]]) ).
cnf(refute_0_12,plain,
is_a_theorem(implies(X_41,implies(not(X_41),Y))),
inference(subst,[],[cn_3:[bind(X,$fot(X_41))]]) ).
cnf(refute_0_13,plain,
( ~ is_a_theorem(implies(X_41,implies(not(X_41),Y)))
| is_a_theorem(implies(implies(implies(not(X_41),Y),X_43),implies(X_41,X_43))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(X_41)),bind(Y,$fot(implies(not(X_41),Y))),bind(Z,$fot(X_43))]]) ).
cnf(refute_0_14,plain,
is_a_theorem(implies(implies(implies(not(X_41),Y),X_43),implies(X_41,X_43))),
inference(resolve,[$cnf( is_a_theorem(implies(X_41,implies(not(X_41),Y))) )],[refute_0_12,refute_0_13]) ).
cnf(refute_0_15,plain,
is_a_theorem(implies(implies(implies(not(X_47),X_46),X_48),implies(X_47,X_48))),
inference(subst,[],[refute_0_14:[bind(Y,$fot(X_46)),bind(X_41,$fot(X_47)),bind(X_43,$fot(X_48))]]) ).
cnf(refute_0_16,plain,
( ~ is_a_theorem(implies(implies(not(X_47),X_46),X_48))
| is_a_theorem(implies(X_47,X_48)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_47),X_46),X_48),implies(X_47,X_48))) )],[refute_0_15,refute_0_11]) ).
cnf(refute_0_17,plain,
( ~ is_a_theorem(implies(implies(not(X_47),not(X_323)),implies(X_323,implies(not(X_47),X_322))))
| is_a_theorem(implies(X_47,implies(X_323,implies(not(X_47),X_322)))) ),
inference(subst,[],[refute_0_16:[bind(X_46,$fot(not(X_323))),bind(X_48,$fot(implies(X_323,implies(not(X_47),X_322))))]]) ).
cnf(refute_0_18,plain,
is_a_theorem(implies(implies(implies(not(X_41),X_319),implies(X_317,X_319)),implies(X_41,implies(X_317,X_319)))),
inference(subst,[],[refute_0_14:[bind(Y,$fot(X_319)),bind(X_43,$fot(implies(X_317,X_319)))]]) ).
cnf(refute_0_19,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_41),X_319),implies(X_317,X_319)),implies(X_41,implies(X_317,X_319))))
| is_a_theorem(implies(implies(X_317,not(X_41)),implies(X_41,implies(X_317,X_319)))) ),
inference(subst,[],[refute_0_6:[bind(X_128,$fot(X_317)),bind(X_129,$fot(not(X_41))),bind(X_130,$fot(X_319)),bind(X_131,$fot(implies(X_41,implies(X_317,X_319))))]]) ).
cnf(refute_0_20,plain,
is_a_theorem(implies(implies(X_317,not(X_41)),implies(X_41,implies(X_317,X_319)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_41),X_319),implies(X_317,X_319)),implies(X_41,implies(X_317,X_319)))) )],[refute_0_18,refute_0_19]) ).
cnf(refute_0_21,plain,
is_a_theorem(implies(implies(not(X_47),not(X_323)),implies(X_323,implies(not(X_47),X_322)))),
inference(subst,[],[refute_0_20:[bind(X_317,$fot(not(X_47))),bind(X_319,$fot(X_322)),bind(X_41,$fot(X_323))]]) ).
cnf(refute_0_22,plain,
is_a_theorem(implies(X_47,implies(X_323,implies(not(X_47),X_322)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_47),not(X_323)),implies(X_323,implies(not(X_47),X_322)))) )],[refute_0_21,refute_0_17]) ).
cnf(refute_0_23,plain,
is_a_theorem(implies(X_326,implies(X_325,implies(not(X_326),X_324)))),
inference(subst,[],[refute_0_22:[bind(X_322,$fot(X_324)),bind(X_323,$fot(X_325)),bind(X_47,$fot(X_326))]]) ).
cnf(refute_0_24,plain,
is_a_theorem(implies(implies(implies(X_325,implies(not(X_326),X_324)),Z),implies(X_326,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_326,implies(X_325,implies(not(X_326),X_324)))) )],[refute_0_23,refute_0_10]) ).
cnf(refute_0_25,plain,
is_a_theorem(implies(implies(implies(X_371,implies(not(X_372),X_370)),X_369),implies(X_372,X_369))),
inference(subst,[],[refute_0_24:[bind(Z,$fot(X_369)),bind(X_324,$fot(X_370)),bind(X_325,$fot(X_371)),bind(X_326,$fot(X_372))]]) ).
cnf(refute_0_26,plain,
( ~ is_a_theorem(implies(implies(X_371,implies(not(X_372),X_370)),X_369))
| is_a_theorem(implies(X_372,X_369)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_371,implies(not(X_372),X_370)),X_369),implies(X_372,X_369))) )],[refute_0_25,refute_0_9]) ).
cnf(refute_0_27,plain,
( ~ is_a_theorem(implies(implies(not(X_36143),implies(not(X_36142),X_36142)),implies(implies(X_36142,X_36143),X_36143)))
| is_a_theorem(implies(X_36142,implies(implies(X_36142,X_36143),X_36143))) ),
inference(subst,[],[refute_0_26:[bind(X_369,$fot(implies(implies(X_36142,X_36143),X_36143))),bind(X_370,$fot(X_36142)),bind(X_371,$fot(not(X_36143))),bind(X_372,$fot(X_36142))]]) ).
cnf(refute_0_28,plain,
( ~ is_a_theorem(implies(implies(implies(not(not(X_525)),X_526),X_525),X_525))
| ~ is_a_theorem(implies(implies(not(not(X_525)),X_526),X_525))
| is_a_theorem(X_525) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(not(not(X_525)),X_526),X_525))),bind(Y,$fot(X_525))]]) ).
cnf(refute_0_29,plain,
is_a_theorem(implies(implies(not(X_521),X_521),X_521)),
inference(subst,[],[cn_2:[bind(X,$fot(X_521))]]) ).
cnf(refute_0_30,plain,
( ~ is_a_theorem(implies(implies(X_234,X_235),X_232))
| ~ is_a_theorem(implies(implies(implies(X_234,X_235),X_232),implies(implies(implies(not(X_234),X_233),X_235),X_232)))
| is_a_theorem(implies(implies(implies(not(X_234),X_233),X_235),X_232)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_234,X_235),X_232))),bind(Y,$fot(implies(implies(implies(not(X_234),X_233),X_235),X_232)))]]) ).
cnf(refute_0_31,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_47),X_46),X_48),implies(X_47,X_48)))
| is_a_theorem(implies(implies(implies(X_47,X_48),Z),implies(implies(implies(not(X_47),X_46),X_48),Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(implies(implies(not(X_47),X_46),X_48))),bind(Y,$fot(implies(X_47,X_48)))]]) ).
cnf(refute_0_32,plain,
is_a_theorem(implies(implies(implies(X_47,X_48),Z),implies(implies(implies(not(X_47),X_46),X_48),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_47),X_46),X_48),implies(X_47,X_48))) )],[refute_0_15,refute_0_31]) ).
cnf(refute_0_33,plain,
is_a_theorem(implies(implies(implies(X_234,X_235),X_232),implies(implies(implies(not(X_234),X_233),X_235),X_232))),
inference(subst,[],[refute_0_32:[bind(Z,$fot(X_232)),bind(X_46,$fot(X_233)),bind(X_47,$fot(X_234)),bind(X_48,$fot(X_235))]]) ).
cnf(refute_0_34,plain,
( ~ is_a_theorem(implies(implies(X_234,X_235),X_232))
| is_a_theorem(implies(implies(implies(not(X_234),X_233),X_235),X_232)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_234,X_235),X_232),implies(implies(implies(not(X_234),X_233),X_235),X_232))) )],[refute_0_33,refute_0_30]) ).
cnf(refute_0_35,plain,
( ~ is_a_theorem(implies(implies(not(X_521),X_521),X_521))
| is_a_theorem(implies(implies(implies(not(not(X_521)),X_522),X_521),X_521)) ),
inference(subst,[],[refute_0_34:[bind(X_232,$fot(X_521)),bind(X_233,$fot(X_522)),bind(X_234,$fot(not(X_521))),bind(X_235,$fot(X_521))]]) ).
cnf(refute_0_36,plain,
is_a_theorem(implies(implies(implies(not(not(X_521)),X_522),X_521),X_521)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_521),X_521),X_521)) )],[refute_0_29,refute_0_35]) ).
cnf(refute_0_37,plain,
is_a_theorem(implies(implies(implies(not(not(X_525)),X_526),X_525),X_525)),
inference(subst,[],[refute_0_36:[bind(X_521,$fot(X_525)),bind(X_522,$fot(X_526))]]) ).
cnf(refute_0_38,plain,
( ~ is_a_theorem(implies(implies(not(not(X_525)),X_526),X_525))
| is_a_theorem(X_525) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(not(X_525)),X_526),X_525),X_525)) )],[refute_0_37,refute_0_28]) ).
cnf(refute_0_39,plain,
( ~ is_a_theorem(implies(implies(not(not(implies(implies(not(X_36141),implies(not(X_36140),X_36140)),implies(implies(X_36140,X_36141),X_36141)))),X_526),implies(implies(not(X_36141),implies(not(X_36140),X_36140)),implies(implies(X_36140,X_36141),X_36141))))
| is_a_theorem(implies(implies(not(X_36141),implies(not(X_36140),X_36140)),implies(implies(X_36140,X_36141),X_36141))) ),
inference(subst,[],[refute_0_38:[bind(X_525,$fot(implies(implies(not(X_36141),implies(not(X_36140),X_36140)),implies(implies(X_36140,X_36141),X_36141))))]]) ).
cnf(refute_0_40,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_15818,X_15819),X_15819),implies(X_128,X_15819)),implies(implies(not(X_15819),X_15818),implies(X_128,X_15819))))
| is_a_theorem(implies(implies(X_128,implies(X_15818,X_15819)),implies(implies(not(X_15819),X_15818),implies(X_128,X_15819)))) ),
inference(subst,[],[refute_0_6:[bind(X_129,$fot(implies(X_15818,X_15819))),bind(X_130,$fot(X_15819)),bind(X_131,$fot(implies(implies(not(X_15819),X_15818),implies(X_128,X_15819))))]]) ).
cnf(refute_0_41,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_3306),X_3305),X_3307),implies(implies(X_3307,X_3304),implies(X_3306,X_3304))))
| ~ is_a_theorem(implies(implies(not(X_3306),X_3305),X_3307))
| is_a_theorem(implies(implies(X_3307,X_3304),implies(X_3306,X_3304))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(not(X_3306),X_3305),X_3307))),bind(Y,$fot(implies(implies(X_3307,X_3304),implies(X_3306,X_3304))))]]) ).
cnf(refute_0_42,plain,
is_a_theorem(implies(implies(X_523,X_524),implies(implies(X_524,Z),implies(X_523,Z)))),
inference(subst,[],[cn_1:[bind(X,$fot(X_523)),bind(Y,$fot(X_524))]]) ).
cnf(refute_0_43,plain,
( ~ is_a_theorem(implies(implies(X_523,X_524),implies(implies(X_524,Z),implies(X_523,Z))))
| is_a_theorem(implies(implies(implies(not(X_523),X_522),X_524),implies(implies(X_524,Z),implies(X_523,Z)))) ),
inference(subst,[],[refute_0_34:[bind(X_232,$fot(implies(implies(X_524,Z),implies(X_523,Z)))),bind(X_233,$fot(X_522)),bind(X_234,$fot(X_523)),bind(X_235,$fot(X_524))]]) ).
cnf(refute_0_44,plain,
is_a_theorem(implies(implies(implies(not(X_523),X_522),X_524),implies(implies(X_524,Z),implies(X_523,Z)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_523,X_524),implies(implies(X_524,Z),implies(X_523,Z)))) )],[refute_0_42,refute_0_43]) ).
cnf(refute_0_45,plain,
is_a_theorem(implies(implies(implies(not(X_3306),X_3305),X_3307),implies(implies(X_3307,X_3304),implies(X_3306,X_3304)))),
inference(subst,[],[refute_0_44:[bind(Z,$fot(X_3304)),bind(X_522,$fot(X_3305)),bind(X_523,$fot(X_3306)),bind(X_524,$fot(X_3307))]]) ).
cnf(refute_0_46,plain,
( ~ is_a_theorem(implies(implies(not(X_3306),X_3305),X_3307))
| is_a_theorem(implies(implies(X_3307,X_3304),implies(X_3306,X_3304))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_3306),X_3305),X_3307),implies(implies(X_3307,X_3304),implies(X_3306,X_3304)))) )],[refute_0_45,refute_0_41]) ).
cnf(refute_0_47,plain,
( ~ is_a_theorem(implies(implies(not(implies(not(X_15811),X_15810)),implies(not(X_15811),X_15810)),implies(implies(X_15810,X_15811),X_15811)))
| is_a_theorem(implies(implies(implies(implies(X_15810,X_15811),X_15811),X_3304),implies(implies(not(X_15811),X_15810),X_3304))) ),
inference(subst,[],[refute_0_46:[bind(X_3305,$fot(implies(not(X_15811),X_15810))),bind(X_3306,$fot(implies(not(X_15811),X_15810))),bind(X_3307,$fot(implies(implies(X_15810,X_15811),X_15811)))]]) ).
cnf(refute_0_48,plain,
( ~ is_a_theorem(implies(implies(not(X_3546),X_3546),implies(X_3547,X_3546)))
| ~ is_a_theorem(implies(not(X_3546),X_3546))
| is_a_theorem(implies(X_3547,X_3546)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(not(X_3546),X_3546))),bind(Y,$fot(implies(X_3547,X_3546)))]]) ).
cnf(refute_0_49,plain,
( ~ is_a_theorem(implies(implies(not(implies(X_84,X_85)),implies(X_84,X_85)),implies(implies(not(X_84),X_84),X_85)))
| ~ is_a_theorem(implies(not(implies(X_84,X_85)),implies(X_84,X_85)))
| is_a_theorem(implies(implies(not(X_84),X_84),X_85)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(not(implies(X_84,X_85)),implies(X_84,X_85)))),bind(Y,$fot(implies(implies(not(X_84),X_84),X_85)))]]) ).
cnf(refute_0_50,plain,
is_a_theorem(implies(implies(not(X_42),X_42),X_42)),
inference(subst,[],[cn_2:[bind(X,$fot(X_42))]]) ).
cnf(refute_0_51,plain,
( ~ is_a_theorem(implies(implies(not(X_42),X_42),X_42))
| is_a_theorem(implies(implies(X_42,X_43),implies(implies(not(X_42),X_42),X_43))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(implies(not(X_42),X_42))),bind(Y,$fot(X_42)),bind(Z,$fot(X_43))]]) ).
cnf(refute_0_52,plain,
is_a_theorem(implies(implies(X_42,X_43),implies(implies(not(X_42),X_42),X_43))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_42),X_42),X_42)) )],[refute_0_50,refute_0_51]) ).
cnf(refute_0_53,plain,
( ~ is_a_theorem(implies(X_44,X_45))
| ~ is_a_theorem(implies(implies(X_44,X_45),implies(implies(not(X_44),X_44),X_45)))
| is_a_theorem(implies(implies(not(X_44),X_44),X_45)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X_44,X_45))),bind(Y,$fot(implies(implies(not(X_44),X_44),X_45)))]]) ).
cnf(refute_0_54,plain,
is_a_theorem(implies(implies(X_44,X_45),implies(implies(not(X_44),X_44),X_45))),
inference(subst,[],[refute_0_52:[bind(X_42,$fot(X_44)),bind(X_43,$fot(X_45))]]) ).
cnf(refute_0_55,plain,
( ~ is_a_theorem(implies(X_44,X_45))
| is_a_theorem(implies(implies(not(X_44),X_44),X_45)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_44,X_45),implies(implies(not(X_44),X_44),X_45))) )],[refute_0_54,refute_0_53]) ).
cnf(refute_0_56,plain,
( ~ is_a_theorem(implies(implies(X_42,X_43),implies(implies(not(X_42),X_42),X_43)))
| is_a_theorem(implies(implies(not(implies(X_42,X_43)),implies(X_42,X_43)),implies(implies(not(X_42),X_42),X_43))) ),
inference(subst,[],[refute_0_55:[bind(X_44,$fot(implies(X_42,X_43))),bind(X_45,$fot(implies(implies(not(X_42),X_42),X_43)))]]) ).
cnf(refute_0_57,plain,
is_a_theorem(implies(implies(not(implies(X_42,X_43)),implies(X_42,X_43)),implies(implies(not(X_42),X_42),X_43))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_42,X_43),implies(implies(not(X_42),X_42),X_43))) )],[refute_0_52,refute_0_56]) ).
cnf(refute_0_58,plain,
is_a_theorem(implies(implies(not(implies(X_84,X_85)),implies(X_84,X_85)),implies(implies(not(X_84),X_84),X_85))),
inference(subst,[],[refute_0_57:[bind(X_42,$fot(X_84)),bind(X_43,$fot(X_85))]]) ).
cnf(refute_0_59,plain,
( ~ is_a_theorem(implies(not(implies(X_84,X_85)),implies(X_84,X_85)))
| is_a_theorem(implies(implies(not(X_84),X_84),X_85)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(implies(X_84,X_85)),implies(X_84,X_85)),implies(implies(not(X_84),X_84),X_85))) )],[refute_0_58,refute_0_49]) ).
cnf(refute_0_60,plain,
( ~ is_a_theorem(implies(not(implies(X_3541,implies(X_3542,X_3541))),implies(X_3541,implies(X_3542,X_3541))))
| is_a_theorem(implies(implies(not(X_3541),X_3541),implies(X_3542,X_3541))) ),
inference(subst,[],[refute_0_59:[bind(X_84,$fot(X_3541)),bind(X_85,$fot(implies(X_3542,X_3541)))]]) ).
cnf(refute_0_61,plain,
( ~ is_a_theorem(implies(implies(implies(X_2679,X_2680),implies(X_128,X_2680)),implies(X_2680,implies(X_128,X_2680))))
| is_a_theorem(implies(implies(X_128,X_2679),implies(X_2680,implies(X_128,X_2680)))) ),
inference(subst,[],[refute_0_6:[bind(X_129,$fot(X_2679)),bind(X_130,$fot(X_2680)),bind(X_131,$fot(implies(X_2680,implies(X_128,X_2680))))]]) ).
cnf(refute_0_62,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(X_65),X_65),X_66),X_64),implies(implies(X_65,X_66),X_64)))
| ~ is_a_theorem(implies(implies(implies(not(X_65),X_65),X_66),X_64))
| is_a_theorem(implies(implies(X_65,X_66),X_64)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(not(X_65),X_65),X_66),X_64))),bind(Y,$fot(implies(implies(X_65,X_66),X_64)))]]) ).
cnf(refute_0_63,plain,
( ~ is_a_theorem(implies(implies(X_44,X_45),implies(implies(not(X_44),X_44),X_45)))
| is_a_theorem(implies(implies(implies(implies(not(X_44),X_44),X_45),Z),implies(implies(X_44,X_45),Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(implies(X_44,X_45))),bind(Y,$fot(implies(implies(not(X_44),X_44),X_45)))]]) ).
cnf(refute_0_64,plain,
is_a_theorem(implies(implies(implies(implies(not(X_44),X_44),X_45),Z),implies(implies(X_44,X_45),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_44,X_45),implies(implies(not(X_44),X_44),X_45))) )],[refute_0_54,refute_0_63]) ).
cnf(refute_0_65,plain,
is_a_theorem(implies(implies(implies(implies(not(X_65),X_65),X_66),X_64),implies(implies(X_65,X_66),X_64))),
inference(subst,[],[refute_0_64:[bind(Z,$fot(X_64)),bind(X_44,$fot(X_65)),bind(X_45,$fot(X_66))]]) ).
cnf(refute_0_66,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_65),X_65),X_66),X_64))
| is_a_theorem(implies(implies(X_65,X_66),X_64)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(X_65),X_65),X_66),X_64),implies(implies(X_65,X_66),X_64))) )],[refute_0_65,refute_0_62]) ).
cnf(refute_0_67,plain,
( ~ is_a_theorem(implies(implies(implies(not(implies(X_2529,X_2530)),implies(X_2529,X_2530)),X_2528),implies(X_2530,X_2528)))
| is_a_theorem(implies(implies(implies(X_2529,X_2530),X_2528),implies(X_2530,X_2528))) ),
inference(subst,[],[refute_0_66:[bind(X_64,$fot(implies(X_2530,X_2528))),bind(X_65,$fot(implies(X_2529,X_2530))),bind(X_66,$fot(X_2528))]]) ).
cnf(refute_0_68,plain,
( ~ is_a_theorem(implies(X_2481,implies(X_2482,implies(X_2480,X_2481))))
| is_a_theorem(implies(implies(implies(X_2482,implies(X_2480,X_2481)),Z),implies(X_2481,Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(X_2481)),bind(Y,$fot(implies(X_2482,implies(X_2480,X_2481))))]]) ).
cnf(refute_0_69,plain,
( ~ is_a_theorem(implies(implies(not(X_2478),not(X_2477)),implies(X_2479,implies(X_2477,X_2478))))
| is_a_theorem(implies(X_2478,implies(X_2479,implies(X_2477,X_2478)))) ),
inference(subst,[],[refute_0_16:[bind(X_46,$fot(not(X_2477))),bind(X_47,$fot(X_2478)),bind(X_48,$fot(implies(X_2479,implies(X_2477,X_2478))))]]) ).
cnf(refute_0_70,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_2473),X_2474),implies(not(X_2474),X_2474)),implies(X_2475,implies(X_2473,X_2474))))
| is_a_theorem(implies(implies(not(X_2474),not(X_2473)),implies(X_2475,implies(X_2473,X_2474)))) ),
inference(subst,[],[refute_0_6:[bind(X_128,$fot(not(X_2474))),bind(X_129,$fot(not(X_2473))),bind(X_130,$fot(X_2474)),bind(X_131,$fot(implies(X_2475,implies(X_2473,X_2474))))]]) ).
cnf(refute_0_71,plain,
( ~ is_a_theorem(implies(implies(X_2288,implies(not(X_2289),X_2289)),implies(X_2290,implies(X_2288,X_2289))))
| is_a_theorem(implies(implies(implies(not(X_2288),X_233),implies(not(X_2289),X_2289)),implies(X_2290,implies(X_2288,X_2289)))) ),
inference(subst,[],[refute_0_34:[bind(X_232,$fot(implies(X_2290,implies(X_2288,X_2289)))),bind(X_234,$fot(X_2288)),bind(X_235,$fot(implies(not(X_2289),X_2289)))]]) ).
cnf(refute_0_72,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(X_2285),X_2285),X_2285),implies(X_128,X_2285)),implies(X_2286,implies(X_128,X_2285))))
| is_a_theorem(implies(implies(X_128,implies(not(X_2285),X_2285)),implies(X_2286,implies(X_128,X_2285)))) ),
inference(subst,[],[refute_0_6:[bind(X_129,$fot(implies(not(X_2285),X_2285))),bind(X_130,$fot(X_2285)),bind(X_131,$fot(implies(X_2286,implies(X_128,X_2285))))]]) ).
cnf(refute_0_73,plain,
( ~ is_a_theorem(implies(X_151,implies(not(implies(implies(not(X_149),X_149),X_149)),X_150)))
| is_a_theorem(implies(implies(implies(not(implies(implies(not(X_149),X_149),X_149)),X_150),Z),implies(X_151,Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(X_151)),bind(Y,$fot(implies(not(implies(implies(not(X_149),X_149),X_149)),X_150)))]]) ).
cnf(refute_0_74,plain,
is_a_theorem(implies(X_6,implies(not(X_6),Y))),
inference(subst,[],[cn_3:[bind(X,$fot(X_6))]]) ).
cnf(refute_0_75,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_76,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_74,refute_0_75]) ).
cnf(refute_0_77,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_76:[bind(Y,$fot(X_9)),bind(X_6,$fot(implies(implies(not(X),X),X)))]]) ).
cnf(refute_0_78,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_77]) ).
cnf(refute_0_79,plain,
is_a_theorem(implies(not(implies(implies(not(X),X),X)),X_42)),
inference(subst,[],[refute_0_78:[bind(X_9,$fot(X_42))]]) ).
cnf(refute_0_80,plain,
( ~ is_a_theorem(implies(not(implies(implies(not(X),X),X)),X_42))
| is_a_theorem(implies(implies(X_42,X_43),implies(not(implies(implies(not(X),X),X)),X_43))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(not(implies(implies(not(X),X),X)))),bind(Y,$fot(X_42)),bind(Z,$fot(X_43))]]) ).
cnf(refute_0_81,plain,
is_a_theorem(implies(implies(X_42,X_43),implies(not(implies(implies(not(X),X),X)),X_43))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(implies(not(X),X),X)),X_42)) )],[refute_0_79,refute_0_80]) ).
cnf(refute_0_82,plain,
is_a_theorem(implies(implies(not(X_133),X_132),implies(not(implies(implies(not(X),X),X)),X_132))),
inference(subst,[],[refute_0_81:[bind(X_42,$fot(not(X_133))),bind(X_43,$fot(X_132))]]) ).
cnf(refute_0_83,plain,
( ~ is_a_theorem(implies(implies(not(X_133),X_132),implies(not(implies(implies(not(X),X),X)),X_132)))
| is_a_theorem(implies(X_133,implies(not(implies(implies(not(X),X),X)),X_132))) ),
inference(subst,[],[refute_0_16:[bind(X_46,$fot(X_132)),bind(X_47,$fot(X_133)),bind(X_48,$fot(implies(not(implies(implies(not(X),X),X)),X_132)))]]) ).
cnf(refute_0_84,plain,
is_a_theorem(implies(X_133,implies(not(implies(implies(not(X),X),X)),X_132))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_133),X_132),implies(not(implies(implies(not(X),X),X)),X_132))) )],[refute_0_82,refute_0_83]) ).
cnf(refute_0_85,plain,
is_a_theorem(implies(X_151,implies(not(implies(implies(not(X_149),X_149),X_149)),X_150))),
inference(subst,[],[refute_0_84:[bind(X,$fot(X_149)),bind(X_132,$fot(X_150)),bind(X_133,$fot(X_151))]]) ).
cnf(refute_0_86,plain,
is_a_theorem(implies(implies(implies(not(implies(implies(not(X_149),X_149),X_149)),X_150),Z),implies(X_151,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_151,implies(not(implies(implies(not(X_149),X_149),X_149)),X_150))) )],[refute_0_85,refute_0_73]) ).
cnf(refute_0_87,plain,
is_a_theorem(implies(implies(implies(not(implies(implies(not(X_149),X_149),X_149)),implies(implies(not(X_149),X_149),X_149)),X_2244),implies(X_151,X_2244))),
inference(subst,[],[refute_0_86:[bind(Z,$fot(X_2244)),bind(X_150,$fot(implies(implies(not(X_149),X_149),X_149)))]]) ).
cnf(refute_0_88,plain,
( ~ is_a_theorem(implies(implies(implies(not(implies(implies(not(X_149),X_149),X_149)),implies(implies(not(X_149),X_149),X_149)),X_2244),implies(X_151,X_2244)))
| is_a_theorem(implies(implies(implies(implies(not(X_149),X_149),X_149),X_2244),implies(X_151,X_2244))) ),
inference(subst,[],[refute_0_66:[bind(X_64,$fot(implies(X_151,X_2244))),bind(X_65,$fot(implies(implies(not(X_149),X_149),X_149))),bind(X_66,$fot(X_2244))]]) ).
cnf(refute_0_89,plain,
is_a_theorem(implies(implies(implies(implies(not(X_149),X_149),X_149),X_2244),implies(X_151,X_2244))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(implies(implies(not(X_149),X_149),X_149)),implies(implies(not(X_149),X_149),X_149)),X_2244),implies(X_151,X_2244))) )],[refute_0_87,refute_0_88]) ).
cnf(refute_0_90,plain,
is_a_theorem(implies(implies(implies(implies(not(X_2285),X_2285),X_2285),implies(X_128,X_2285)),implies(X_2286,implies(X_128,X_2285)))),
inference(subst,[],[refute_0_89:[bind(X_149,$fot(X_2285)),bind(X_151,$fot(X_2286)),bind(X_2244,$fot(implies(X_128,X_2285)))]]) ).
cnf(refute_0_91,plain,
is_a_theorem(implies(implies(X_128,implies(not(X_2285),X_2285)),implies(X_2286,implies(X_128,X_2285)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(X_2285),X_2285),X_2285),implies(X_128,X_2285)),implies(X_2286,implies(X_128,X_2285)))) )],[refute_0_90,refute_0_72]) ).
cnf(refute_0_92,plain,
is_a_theorem(implies(implies(X_2288,implies(not(X_2289),X_2289)),implies(X_2290,implies(X_2288,X_2289)))),
inference(subst,[],[refute_0_91:[bind(X_128,$fot(X_2288)),bind(X_2285,$fot(X_2289)),bind(X_2286,$fot(X_2290))]]) ).
cnf(refute_0_93,plain,
is_a_theorem(implies(implies(implies(not(X_2288),X_233),implies(not(X_2289),X_2289)),implies(X_2290,implies(X_2288,X_2289)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_2288,implies(not(X_2289),X_2289)),implies(X_2290,implies(X_2288,X_2289)))) )],[refute_0_92,refute_0_71]) ).
cnf(refute_0_94,plain,
is_a_theorem(implies(implies(implies(not(X_2473),X_2474),implies(not(X_2474),X_2474)),implies(X_2475,implies(X_2473,X_2474)))),
inference(subst,[],[refute_0_93:[bind(X_2288,$fot(X_2473)),bind(X_2289,$fot(X_2474)),bind(X_2290,$fot(X_2475)),bind(X_233,$fot(X_2474))]]) ).
cnf(refute_0_95,plain,
is_a_theorem(implies(implies(not(X_2474),not(X_2473)),implies(X_2475,implies(X_2473,X_2474)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_2473),X_2474),implies(not(X_2474),X_2474)),implies(X_2475,implies(X_2473,X_2474)))) )],[refute_0_94,refute_0_70]) ).
cnf(refute_0_96,plain,
is_a_theorem(implies(implies(not(X_2478),not(X_2477)),implies(X_2479,implies(X_2477,X_2478)))),
inference(subst,[],[refute_0_95:[bind(X_2473,$fot(X_2477)),bind(X_2474,$fot(X_2478)),bind(X_2475,$fot(X_2479))]]) ).
cnf(refute_0_97,plain,
is_a_theorem(implies(X_2478,implies(X_2479,implies(X_2477,X_2478)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_2478),not(X_2477)),implies(X_2479,implies(X_2477,X_2478)))) )],[refute_0_96,refute_0_69]) ).
cnf(refute_0_98,plain,
is_a_theorem(implies(X_2481,implies(X_2482,implies(X_2480,X_2481)))),
inference(subst,[],[refute_0_97:[bind(X_2477,$fot(X_2480)),bind(X_2478,$fot(X_2481)),bind(X_2479,$fot(X_2482))]]) ).
cnf(refute_0_99,plain,
is_a_theorem(implies(implies(implies(X_2482,implies(X_2480,X_2481)),Z),implies(X_2481,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_2481,implies(X_2482,implies(X_2480,X_2481)))) )],[refute_0_98,refute_0_68]) ).
cnf(refute_0_100,plain,
is_a_theorem(implies(implies(implies(not(implies(X_2529,X_2530)),implies(X_2529,X_2530)),X_2528),implies(X_2530,X_2528))),
inference(subst,[],[refute_0_99:[bind(Z,$fot(X_2528)),bind(X_2480,$fot(X_2529)),bind(X_2481,$fot(X_2530)),bind(X_2482,$fot(not(implies(X_2529,X_2530))))]]) ).
cnf(refute_0_101,plain,
is_a_theorem(implies(implies(implies(X_2529,X_2530),X_2528),implies(X_2530,X_2528))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(implies(X_2529,X_2530)),implies(X_2529,X_2530)),X_2528),implies(X_2530,X_2528))) )],[refute_0_100,refute_0_67]) ).
cnf(refute_0_102,plain,
is_a_theorem(implies(implies(implies(X_2679,X_2680),implies(X_128,X_2680)),implies(X_2680,implies(X_128,X_2680)))),
inference(subst,[],[refute_0_101:[bind(X_2528,$fot(implies(X_128,X_2680))),bind(X_2529,$fot(X_2679)),bind(X_2530,$fot(X_2680))]]) ).
cnf(refute_0_103,plain,
is_a_theorem(implies(implies(X_128,X_2679),implies(X_2680,implies(X_128,X_2680)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_2679,X_2680),implies(X_128,X_2680)),implies(X_2680,implies(X_128,X_2680)))) )],[refute_0_102,refute_0_61]) ).
cnf(refute_0_104,plain,
is_a_theorem(implies(implies(X_3537,implies(not(X_3537),X_3538)),implies(X_2680,implies(X_3537,X_2680)))),
inference(subst,[],[refute_0_103:[bind(X_128,$fot(X_3537)),bind(X_2679,$fot(implies(not(X_3537),X_3538)))]]) ).
cnf(refute_0_105,plain,
( ~ is_a_theorem(implies(implies(X_2250,implies(not(X_2250),X_2251)),X_2253))
| ~ is_a_theorem(implies(implies(implies(X_2250,implies(not(X_2250),X_2251)),X_2253),implies(X_2252,X_2253)))
| is_a_theorem(implies(X_2252,X_2253)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_2250,implies(not(X_2250),X_2251)),X_2253))),bind(Y,$fot(implies(X_2252,X_2253)))]]) ).
cnf(refute_0_106,plain,
( ~ is_a_theorem(implies(X_155,implies(not(implies(X_152,implies(not(X_152),X_153))),X_154)))
| is_a_theorem(implies(implies(implies(not(implies(X_152,implies(not(X_152),X_153))),X_154),Z),implies(X_155,Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(X_155)),bind(Y,$fot(implies(not(implies(X_152,implies(not(X_152),X_153))),X_154)))]]) ).
cnf(refute_0_107,plain,
( ~ is_a_theorem(implies(X,implies(not(X),Y)))
| is_a_theorem(implies(not(implies(X,implies(not(X),Y))),X_9)) ),
inference(subst,[],[refute_0_76:[bind(Y,$fot(X_9)),bind(X_6,$fot(implies(X,implies(not(X),Y))))]]) ).
cnf(refute_0_108,plain,
is_a_theorem(implies(not(implies(X,implies(not(X),Y))),X_9)),
inference(resolve,[$cnf( is_a_theorem(implies(X,implies(not(X),Y))) )],[cn_3,refute_0_107]) ).
cnf(refute_0_109,plain,
is_a_theorem(implies(not(implies(X,implies(not(X),Y))),X_42)),
inference(subst,[],[refute_0_108:[bind(X_9,$fot(X_42))]]) ).
cnf(refute_0_110,plain,
( ~ is_a_theorem(implies(not(implies(X,implies(not(X),Y))),X_42))
| is_a_theorem(implies(implies(X_42,X_43),implies(not(implies(X,implies(not(X),Y))),X_43))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(not(implies(X,implies(not(X),Y))))),bind(Y,$fot(X_42)),bind(Z,$fot(X_43))]]) ).
cnf(refute_0_111,plain,
is_a_theorem(implies(implies(X_42,X_43),implies(not(implies(X,implies(not(X),Y))),X_43))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(X,implies(not(X),Y))),X_42)) )],[refute_0_109,refute_0_110]) ).
cnf(refute_0_112,plain,
is_a_theorem(implies(implies(not(X_133),X_132),implies(not(implies(X,implies(not(X),Y))),X_132))),
inference(subst,[],[refute_0_111:[bind(X_42,$fot(not(X_133))),bind(X_43,$fot(X_132))]]) ).
cnf(refute_0_113,plain,
( ~ is_a_theorem(implies(implies(not(X_133),X_132),implies(not(implies(X,implies(not(X),Y))),X_132)))
| is_a_theorem(implies(X_133,implies(not(implies(X,implies(not(X),Y))),X_132))) ),
inference(subst,[],[refute_0_16:[bind(X_46,$fot(X_132)),bind(X_47,$fot(X_133)),bind(X_48,$fot(implies(not(implies(X,implies(not(X),Y))),X_132)))]]) ).
cnf(refute_0_114,plain,
is_a_theorem(implies(X_133,implies(not(implies(X,implies(not(X),Y))),X_132))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_133),X_132),implies(not(implies(X,implies(not(X),Y))),X_132))) )],[refute_0_112,refute_0_113]) ).
cnf(refute_0_115,plain,
is_a_theorem(implies(X_155,implies(not(implies(X_152,implies(not(X_152),X_153))),X_154))),
inference(subst,[],[refute_0_114:[bind(X,$fot(X_152)),bind(Y,$fot(X_153)),bind(X_132,$fot(X_154)),bind(X_133,$fot(X_155))]]) ).
cnf(refute_0_116,plain,
is_a_theorem(implies(implies(implies(not(implies(X_152,implies(not(X_152),X_153))),X_154),Z),implies(X_155,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_155,implies(not(implies(X_152,implies(not(X_152),X_153))),X_154))) )],[refute_0_115,refute_0_106]) ).
cnf(refute_0_117,plain,
is_a_theorem(implies(implies(implies(not(implies(X_152,implies(not(X_152),X_153))),implies(X_152,implies(not(X_152),X_153))),X_2244),implies(X_155,X_2244))),
inference(subst,[],[refute_0_116:[bind(Z,$fot(X_2244)),bind(X_154,$fot(implies(X_152,implies(not(X_152),X_153))))]]) ).
cnf(refute_0_118,plain,
( ~ is_a_theorem(implies(implies(implies(not(implies(X_152,implies(not(X_152),X_153))),implies(X_152,implies(not(X_152),X_153))),X_2244),implies(X_155,X_2244)))
| is_a_theorem(implies(implies(implies(X_152,implies(not(X_152),X_153)),X_2244),implies(X_155,X_2244))) ),
inference(subst,[],[refute_0_66:[bind(X_64,$fot(implies(X_155,X_2244))),bind(X_65,$fot(implies(X_152,implies(not(X_152),X_153)))),bind(X_66,$fot(X_2244))]]) ).
cnf(refute_0_119,plain,
is_a_theorem(implies(implies(implies(X_152,implies(not(X_152),X_153)),X_2244),implies(X_155,X_2244))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(implies(X_152,implies(not(X_152),X_153))),implies(X_152,implies(not(X_152),X_153))),X_2244),implies(X_155,X_2244))) )],[refute_0_117,refute_0_118]) ).
cnf(refute_0_120,plain,
is_a_theorem(implies(implies(implies(X_2250,implies(not(X_2250),X_2251)),X_2253),implies(X_2252,X_2253))),
inference(subst,[],[refute_0_119:[bind(X_152,$fot(X_2250)),bind(X_153,$fot(X_2251)),bind(X_155,$fot(X_2252)),bind(X_2244,$fot(X_2253))]]) ).
cnf(refute_0_121,plain,
( ~ is_a_theorem(implies(implies(X_2250,implies(not(X_2250),X_2251)),X_2253))
| is_a_theorem(implies(X_2252,X_2253)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_2250,implies(not(X_2250),X_2251)),X_2253),implies(X_2252,X_2253))) )],[refute_0_120,refute_0_105]) ).
cnf(refute_0_122,plain,
( ~ is_a_theorem(implies(implies(X_3537,implies(not(X_3537),X_3538)),implies(X_2680,implies(X_3537,X_2680))))
| is_a_theorem(implies(X_3539,implies(X_2680,implies(X_3537,X_2680)))) ),
inference(subst,[],[refute_0_121:[bind(X_2250,$fot(X_3537)),bind(X_2251,$fot(X_3538)),bind(X_2252,$fot(X_3539)),bind(X_2253,$fot(implies(X_2680,implies(X_3537,X_2680))))]]) ).
cnf(refute_0_123,plain,
is_a_theorem(implies(X_3539,implies(X_2680,implies(X_3537,X_2680)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_3537,implies(not(X_3537),X_3538)),implies(X_2680,implies(X_3537,X_2680)))) )],[refute_0_104,refute_0_122]) ).
cnf(refute_0_124,plain,
is_a_theorem(implies(not(implies(X_3541,implies(X_3542,X_3541))),implies(X_3541,implies(X_3542,X_3541)))),
inference(subst,[],[refute_0_123:[bind(X_2680,$fot(X_3541)),bind(X_3537,$fot(X_3542)),bind(X_3539,$fot(not(implies(X_3541,implies(X_3542,X_3541)))))]]) ).
cnf(refute_0_125,plain,
is_a_theorem(implies(implies(not(X_3541),X_3541),implies(X_3542,X_3541))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(X_3541,implies(X_3542,X_3541))),implies(X_3541,implies(X_3542,X_3541)))) )],[refute_0_124,refute_0_60]) ).
cnf(refute_0_126,plain,
is_a_theorem(implies(implies(not(X_3546),X_3546),implies(X_3547,X_3546))),
inference(subst,[],[refute_0_125:[bind(X_3541,$fot(X_3546)),bind(X_3542,$fot(X_3547))]]) ).
cnf(refute_0_127,plain,
( ~ is_a_theorem(implies(not(X_3546),X_3546))
| is_a_theorem(implies(X_3547,X_3546)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_3546),X_3546),implies(X_3547,X_3546))) )],[refute_0_126,refute_0_48]) ).
cnf(refute_0_128,plain,
( ~ is_a_theorem(implies(not(implies(not(implies(implies(not(X_12194),X_12193),implies(implies(X_12193,X_12194),X_12194))),X_12192)),implies(not(implies(implies(not(X_12194),X_12193),implies(implies(X_12193,X_12194),X_12194))),X_12192)))
| is_a_theorem(implies(X_3547,implies(not(implies(implies(not(X_12194),X_12193),implies(implies(X_12193,X_12194),X_12194))),X_12192))) ),
inference(subst,[],[refute_0_127:[bind(X_3546,$fot(implies(not(implies(implies(not(X_12194),X_12193),implies(implies(X_12193,X_12194),X_12194))),X_12192)))]]) ).
cnf(refute_0_129,plain,
( ~ is_a_theorem(implies(implies(not(X_7701),X_7700),implies(implies(X_7700,X_7701),X_7701)))
| is_a_theorem(implies(not(implies(implies(not(X_7701),X_7700),implies(implies(X_7700,X_7701),X_7701))),Y)) ),
inference(subst,[],[refute_0_76:[bind(X_6,$fot(implies(implies(not(X_7701),X_7700),implies(implies(X_7700,X_7701),X_7701))))]]) ).
cnf(refute_0_130,plain,
( ~ is_a_theorem(implies(implies(implies(X_129,X_6636),implies(not(X_6636),X_6636)),implies(implies(X_129,X_6636),X_6636)))
| is_a_theorem(implies(implies(not(X_6636),X_129),implies(implies(X_129,X_6636),X_6636))) ),
inference(subst,[],[refute_0_6:[bind(X_128,$fot(not(X_6636))),bind(X_130,$fot(X_6636)),bind(X_131,$fot(implies(implies(X_129,X_6636),X_6636)))]]) ).
cnf(refute_0_131,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(X_6633),X_6633),X_6633),implies(X_128,X_6633)),implies(X_128,X_6633)))
| is_a_theorem(implies(implies(X_128,implies(not(X_6633),X_6633)),implies(X_128,X_6633))) ),
inference(subst,[],[refute_0_6:[bind(X_129,$fot(implies(not(X_6633),X_6633))),bind(X_130,$fot(X_6633)),bind(X_131,$fot(implies(X_128,X_6633)))]]) ).
cnf(refute_0_132,plain,
( ~ is_a_theorem(implies(implies(not(not(implies(implies(implies(implies(not(X_6630),X_6630),X_6630),X_6631),X_6631))),X_526),implies(implies(implies(implies(not(X_6630),X_6630),X_6630),X_6631),X_6631)))
| is_a_theorem(implies(implies(implies(implies(not(X_6630),X_6630),X_6630),X_6631),X_6631)) ),
inference(subst,[],[refute_0_38:[bind(X_525,$fot(implies(implies(implies(implies(not(X_6630),X_6630),X_6630),X_6631),X_6631)))]]) ).
cnf(refute_0_133,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_4087),X_4087),X_4085),implies(implies(implies(implies(not(X_4084),X_4084),X_4084),X_4087),X_4085)))
| is_a_theorem(implies(implies(X_4087,X_4085),implies(implies(implies(implies(not(X_4084),X_4084),X_4084),X_4087),X_4085))) ),
inference(subst,[],[refute_0_66:[bind(X_64,$fot(implies(implies(implies(implies(not(X_4084),X_4084),X_4084),X_4087),X_4085))),bind(X_65,$fot(X_4087)),bind(X_66,$fot(X_4085))]]) ).
cnf(refute_0_134,plain,
( ~ is_a_theorem(X_3544)
| ~ is_a_theorem(implies(X_3544,implies(X_3545,X_3544)))
| is_a_theorem(implies(X_3545,X_3544)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(X_3544)),bind(Y,$fot(implies(X_3545,X_3544)))]]) ).
cnf(refute_0_135,plain,
( ~ is_a_theorem(implies(implies(not(not(implies(X_3541,implies(X_3542,X_3541)))),X_526),implies(X_3541,implies(X_3542,X_3541))))
| is_a_theorem(implies(X_3541,implies(X_3542,X_3541))) ),
inference(subst,[],[refute_0_38:[bind(X_525,$fot(implies(X_3541,implies(X_3542,X_3541))))]]) ).
cnf(refute_0_136,plain,
is_a_theorem(implies(implies(not(not(implies(X_3541,implies(X_3542,X_3541)))),X_526),implies(X_3541,implies(X_3542,X_3541)))),
inference(subst,[],[refute_0_123:[bind(X_2680,$fot(X_3541)),bind(X_3537,$fot(X_3542)),bind(X_3539,$fot(implies(not(not(implies(X_3541,implies(X_3542,X_3541)))),X_526)))]]) ).
cnf(refute_0_137,plain,
is_a_theorem(implies(X_3541,implies(X_3542,X_3541))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(not(implies(X_3541,implies(X_3542,X_3541)))),X_526),implies(X_3541,implies(X_3542,X_3541)))) )],[refute_0_136,refute_0_135]) ).
cnf(refute_0_138,plain,
is_a_theorem(implies(X_3544,implies(X_3545,X_3544))),
inference(subst,[],[refute_0_137:[bind(X_3541,$fot(X_3544)),bind(X_3542,$fot(X_3545))]]) ).
cnf(refute_0_139,plain,
( ~ is_a_theorem(X_3544)
| is_a_theorem(implies(X_3545,X_3544)) ),
inference(resolve,[$cnf( is_a_theorem(implies(X_3544,implies(X_3545,X_3544))) )],[refute_0_138,refute_0_134]) ).
cnf(refute_0_140,plain,
( ~ is_a_theorem(implies(implies(not(X),X),X))
| is_a_theorem(implies(X_3555,implies(implies(not(X),X),X))) ),
inference(subst,[],[refute_0_139:[bind(X_3544,$fot(implies(implies(not(X),X),X))),bind(X_3545,$fot(X_3555))]]) ).
cnf(refute_0_141,plain,
is_a_theorem(implies(X_3555,implies(implies(not(X),X),X))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X),X),X)) )],[cn_2,refute_0_140]) ).
cnf(refute_0_142,plain,
is_a_theorem(implies(X_4063,implies(implies(not(X),X),X))),
inference(subst,[],[refute_0_141:[bind(X_3555,$fot(X_4063))]]) ).
cnf(refute_0_143,plain,
( ~ is_a_theorem(implies(X_351,X_352))
| ~ is_a_theorem(implies(implies(X_351,X_352),implies(implies(implies(X_351,X_353),X_350),implies(implies(X_352,X_353),X_350))))
| is_a_theorem(implies(implies(implies(X_351,X_353),X_350),implies(implies(X_352,X_353),X_350))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X_351,X_352))),bind(Y,$fot(implies(implies(implies(X_351,X_353),X_350),implies(implies(X_352,X_353),X_350))))]]) ).
cnf(refute_0_144,plain,
is_a_theorem(implies(implies(implies(X_318,X_319),implies(X_317,X_319)),implies(implies(implies(X_317,X_319),Z),implies(implies(X_318,X_319),Z)))),
inference(subst,[],[cn_1:[bind(X,$fot(implies(X_318,X_319))),bind(Y,$fot(implies(X_317,X_319)))]]) ).
cnf(refute_0_145,plain,
( ~ is_a_theorem(implies(implies(implies(X_318,X_319),implies(X_317,X_319)),implies(implies(implies(X_317,X_319),Z),implies(implies(X_318,X_319),Z))))
| is_a_theorem(implies(implies(X_317,X_318),implies(implies(implies(X_317,X_319),Z),implies(implies(X_318,X_319),Z)))) ),
inference(subst,[],[refute_0_6:[bind(X_128,$fot(X_317)),bind(X_129,$fot(X_318)),bind(X_130,$fot(X_319)),bind(X_131,$fot(implies(implies(implies(X_317,X_319),Z),implies(implies(X_318,X_319),Z))))]]) ).
cnf(refute_0_146,plain,
is_a_theorem(implies(implies(X_317,X_318),implies(implies(implies(X_317,X_319),Z),implies(implies(X_318,X_319),Z)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_318,X_319),implies(X_317,X_319)),implies(implies(implies(X_317,X_319),Z),implies(implies(X_318,X_319),Z)))) )],[refute_0_144,refute_0_145]) ).
cnf(refute_0_147,plain,
is_a_theorem(implies(implies(X_351,X_352),implies(implies(implies(X_351,X_353),X_350),implies(implies(X_352,X_353),X_350)))),
inference(subst,[],[refute_0_146:[bind(Z,$fot(X_350)),bind(X_317,$fot(X_351)),bind(X_318,$fot(X_352)),bind(X_319,$fot(X_353))]]) ).
cnf(refute_0_148,plain,
( ~ is_a_theorem(implies(X_351,X_352))
| is_a_theorem(implies(implies(implies(X_351,X_353),X_350),implies(implies(X_352,X_353),X_350))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_351,X_352),implies(implies(implies(X_351,X_353),X_350),implies(implies(X_352,X_353),X_350)))) )],[refute_0_147,refute_0_143]) ).
cnf(refute_0_149,plain,
( ~ is_a_theorem(implies(X_4063,implies(implies(not(X),X),X)))
| is_a_theorem(implies(implies(implies(X_4063,X_4065),X_4062),implies(implies(implies(implies(not(X),X),X),X_4065),X_4062))) ),
inference(subst,[],[refute_0_148:[bind(X_350,$fot(X_4062)),bind(X_351,$fot(X_4063)),bind(X_352,$fot(implies(implies(not(X),X),X))),bind(X_353,$fot(X_4065))]]) ).
cnf(refute_0_150,plain,
is_a_theorem(implies(implies(implies(X_4063,X_4065),X_4062),implies(implies(implies(implies(not(X),X),X),X_4065),X_4062))),
inference(resolve,[$cnf( is_a_theorem(implies(X_4063,implies(implies(not(X),X),X))) )],[refute_0_142,refute_0_149]) ).
cnf(refute_0_151,plain,
is_a_theorem(implies(implies(implies(not(X_4087),X_4087),X_4085),implies(implies(implies(implies(not(X_4084),X_4084),X_4084),X_4087),X_4085))),
inference(subst,[],[refute_0_150:[bind(X,$fot(X_4084)),bind(X_4062,$fot(X_4085)),bind(X_4063,$fot(not(X_4087))),bind(X_4065,$fot(X_4087))]]) ).
cnf(refute_0_152,plain,
is_a_theorem(implies(implies(X_4087,X_4085),implies(implies(implies(implies(not(X_4084),X_4084),X_4084),X_4087),X_4085))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_4087),X_4087),X_4085),implies(implies(implies(implies(not(X_4084),X_4084),X_4084),X_4087),X_4085))) )],[refute_0_151,refute_0_133]) ).
cnf(refute_0_153,plain,
is_a_theorem(implies(implies(X_6035,X_6035),implies(implies(implies(implies(not(X_4084),X_4084),X_4084),X_6035),X_6035))),
inference(subst,[],[refute_0_152:[bind(X_4085,$fot(X_6035)),bind(X_4087,$fot(X_6035))]]) ).
cnf(refute_0_154,plain,
( ~ is_a_theorem(implies(implies(X_2245,X_2245),X_2247))
| ~ is_a_theorem(implies(implies(implies(X_2245,X_2245),X_2247),implies(X_2246,X_2247)))
| is_a_theorem(implies(X_2246,X_2247)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_2245,X_2245),X_2247))),bind(Y,$fot(implies(X_2246,X_2247)))]]) ).
cnf(refute_0_155,plain,
( ~ is_a_theorem(implies(X_184,implies(not(implies(X_183,X_183)),X_182)))
| is_a_theorem(implies(implies(implies(not(implies(X_183,X_183)),X_182),Z),implies(X_184,Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(X_184)),bind(Y,$fot(implies(not(implies(X_183,X_183)),X_182)))]]) ).
cnf(refute_0_156,plain,
( ~ is_a_theorem(implies(implies(not(X_47),X_160),implies(not(implies(X_162,X_162)),X_160)))
| is_a_theorem(implies(X_47,implies(not(implies(X_162,X_162)),X_160))) ),
inference(subst,[],[refute_0_16:[bind(X_46,$fot(X_160)),bind(X_48,$fot(implies(not(implies(X_162,X_162)),X_160)))]]) ).
cnf(refute_0_157,plain,
( ~ is_a_theorem(implies(not(implies(X_137,X_137)),X_136))
| is_a_theorem(implies(implies(X_136,Z),implies(not(implies(X_137,X_137)),Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(not(implies(X_137,X_137)))),bind(Y,$fot(X_136))]]) ).
cnf(refute_0_158,plain,
( ~ is_a_theorem(implies(X_135,X_135))
| is_a_theorem(implies(not(implies(X_135,X_135)),Y)) ),
inference(subst,[],[refute_0_76:[bind(X_6,$fot(implies(X_135,X_135)))]]) ).
cnf(refute_0_159,plain,
is_a_theorem(implies(implies(not(X_134),X_134),X_134)),
inference(subst,[],[cn_2:[bind(X,$fot(X_134))]]) ).
cnf(refute_0_160,plain,
( ~ is_a_theorem(implies(implies(not(X_134),X_134),X_134))
| is_a_theorem(implies(X_134,X_134)) ),
inference(subst,[],[refute_0_16:[bind(X_46,$fot(X_134)),bind(X_47,$fot(X_134)),bind(X_48,$fot(X_134))]]) ).
cnf(refute_0_161,plain,
is_a_theorem(implies(X_134,X_134)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_134),X_134),X_134)) )],[refute_0_159,refute_0_160]) ).
cnf(refute_0_162,plain,
is_a_theorem(implies(X_135,X_135)),
inference(subst,[],[refute_0_161:[bind(X_134,$fot(X_135))]]) ).
cnf(refute_0_163,plain,
is_a_theorem(implies(not(implies(X_135,X_135)),Y)),
inference(resolve,[$cnf( is_a_theorem(implies(X_135,X_135)) )],[refute_0_162,refute_0_158]) ).
cnf(refute_0_164,plain,
is_a_theorem(implies(not(implies(X_137,X_137)),X_136)),
inference(subst,[],[refute_0_163:[bind(Y,$fot(X_136)),bind(X_135,$fot(X_137))]]) ).
cnf(refute_0_165,plain,
is_a_theorem(implies(implies(X_136,Z),implies(not(implies(X_137,X_137)),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(X_137,X_137)),X_136)) )],[refute_0_164,refute_0_157]) ).
cnf(refute_0_166,plain,
is_a_theorem(implies(implies(not(X_47),X_160),implies(not(implies(X_162,X_162)),X_160))),
inference(subst,[],[refute_0_165:[bind(Z,$fot(X_160)),bind(X_136,$fot(not(X_47))),bind(X_137,$fot(X_162))]]) ).
cnf(refute_0_167,plain,
is_a_theorem(implies(X_47,implies(not(implies(X_162,X_162)),X_160))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_47),X_160),implies(not(implies(X_162,X_162)),X_160))) )],[refute_0_166,refute_0_156]) ).
cnf(refute_0_168,plain,
is_a_theorem(implies(X_184,implies(not(implies(X_183,X_183)),X_182))),
inference(subst,[],[refute_0_167:[bind(X_160,$fot(X_182)),bind(X_162,$fot(X_183)),bind(X_47,$fot(X_184))]]) ).
cnf(refute_0_169,plain,
is_a_theorem(implies(implies(implies(not(implies(X_183,X_183)),X_182),Z),implies(X_184,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_184,implies(not(implies(X_183,X_183)),X_182))) )],[refute_0_168,refute_0_155]) ).
cnf(refute_0_170,plain,
is_a_theorem(implies(implies(implies(not(implies(X_183,X_183)),implies(X_183,X_183)),X_2244),implies(X_184,X_2244))),
inference(subst,[],[refute_0_169:[bind(Z,$fot(X_2244)),bind(X_182,$fot(implies(X_183,X_183)))]]) ).
cnf(refute_0_171,plain,
( ~ is_a_theorem(implies(implies(implies(not(implies(X_183,X_183)),implies(X_183,X_183)),X_2244),implies(X_184,X_2244)))
| is_a_theorem(implies(implies(implies(X_183,X_183),X_2244),implies(X_184,X_2244))) ),
inference(subst,[],[refute_0_66:[bind(X_64,$fot(implies(X_184,X_2244))),bind(X_65,$fot(implies(X_183,X_183))),bind(X_66,$fot(X_2244))]]) ).
cnf(refute_0_172,plain,
is_a_theorem(implies(implies(implies(X_183,X_183),X_2244),implies(X_184,X_2244))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(implies(X_183,X_183)),implies(X_183,X_183)),X_2244),implies(X_184,X_2244))) )],[refute_0_170,refute_0_171]) ).
cnf(refute_0_173,plain,
is_a_theorem(implies(implies(implies(X_2245,X_2245),X_2247),implies(X_2246,X_2247))),
inference(subst,[],[refute_0_172:[bind(X_183,$fot(X_2245)),bind(X_184,$fot(X_2246)),bind(X_2244,$fot(X_2247))]]) ).
cnf(refute_0_174,plain,
( ~ is_a_theorem(implies(implies(X_2245,X_2245),X_2247))
| is_a_theorem(implies(X_2246,X_2247)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_2245,X_2245),X_2247),implies(X_2246,X_2247))) )],[refute_0_173,refute_0_154]) ).
cnf(refute_0_175,plain,
( ~ is_a_theorem(implies(implies(X_6035,X_6035),implies(implies(implies(implies(not(X_4084),X_4084),X_4084),X_6035),X_6035)))
| is_a_theorem(implies(X_6036,implies(implies(implies(implies(not(X_4084),X_4084),X_4084),X_6035),X_6035))) ),
inference(subst,[],[refute_0_174:[bind(X_2245,$fot(X_6035)),bind(X_2246,$fot(X_6036)),bind(X_2247,$fot(implies(implies(implies(implies(not(X_4084),X_4084),X_4084),X_6035),X_6035)))]]) ).
cnf(refute_0_176,plain,
is_a_theorem(implies(X_6036,implies(implies(implies(implies(not(X_4084),X_4084),X_4084),X_6035),X_6035))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_6035,X_6035),implies(implies(implies(implies(not(X_4084),X_4084),X_4084),X_6035),X_6035))) )],[refute_0_153,refute_0_175]) ).
cnf(refute_0_177,plain,
is_a_theorem(implies(implies(not(not(implies(implies(implies(implies(not(X_6630),X_6630),X_6630),X_6631),X_6631))),X_526),implies(implies(implies(implies(not(X_6630),X_6630),X_6630),X_6631),X_6631))),
inference(subst,[],[refute_0_176:[bind(X_4084,$fot(X_6630)),bind(X_6035,$fot(X_6631)),bind(X_6036,$fot(implies(not(not(implies(implies(implies(implies(not(X_6630),X_6630),X_6630),X_6631),X_6631))),X_526)))]]) ).
cnf(refute_0_178,plain,
is_a_theorem(implies(implies(implies(implies(not(X_6630),X_6630),X_6630),X_6631),X_6631)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(not(implies(implies(implies(implies(not(X_6630),X_6630),X_6630),X_6631),X_6631))),X_526),implies(implies(implies(implies(not(X_6630),X_6630),X_6630),X_6631),X_6631))) )],[refute_0_177,refute_0_132]) ).
cnf(refute_0_179,plain,
is_a_theorem(implies(implies(implies(implies(not(X_6633),X_6633),X_6633),implies(X_128,X_6633)),implies(X_128,X_6633))),
inference(subst,[],[refute_0_178:[bind(X_6630,$fot(X_6633)),bind(X_6631,$fot(implies(X_128,X_6633)))]]) ).
cnf(refute_0_180,plain,
is_a_theorem(implies(implies(X_128,implies(not(X_6633),X_6633)),implies(X_128,X_6633))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(X_6633),X_6633),X_6633),implies(X_128,X_6633)),implies(X_128,X_6633))) )],[refute_0_179,refute_0_131]) ).
cnf(refute_0_181,plain,
is_a_theorem(implies(implies(implies(X_129,X_6636),implies(not(X_6636),X_6636)),implies(implies(X_129,X_6636),X_6636))),
inference(subst,[],[refute_0_180:[bind(X_128,$fot(implies(X_129,X_6636))),bind(X_6633,$fot(X_6636))]]) ).
cnf(refute_0_182,plain,
is_a_theorem(implies(implies(not(X_6636),X_129),implies(implies(X_129,X_6636),X_6636))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_129,X_6636),implies(not(X_6636),X_6636)),implies(implies(X_129,X_6636),X_6636))) )],[refute_0_181,refute_0_130]) ).
cnf(refute_0_183,plain,
is_a_theorem(implies(implies(not(X_7701),X_7700),implies(implies(X_7700,X_7701),X_7701))),
inference(subst,[],[refute_0_182:[bind(X_129,$fot(X_7700)),bind(X_6636,$fot(X_7701))]]) ).
cnf(refute_0_184,plain,
is_a_theorem(implies(not(implies(implies(not(X_7701),X_7700),implies(implies(X_7700,X_7701),X_7701))),Y)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_7701),X_7700),implies(implies(X_7700,X_7701),X_7701))) )],[refute_0_183,refute_0_129]) ).
cnf(refute_0_185,plain,
is_a_theorem(implies(not(implies(implies(not(X_7701),X_7700),implies(implies(X_7700,X_7701),X_7701))),implies(implies(not(X_7701),X_7700),implies(implies(X_7700,X_7701),X_7701)))),
inference(subst,[],[refute_0_184:[bind(Y,$fot(implies(implies(not(X_7701),X_7700),implies(implies(X_7700,X_7701),X_7701))))]]) ).
cnf(refute_0_186,plain,
( ~ is_a_theorem(implies(implies(not(X_208),X_208),implies(not(implies(not(X_208),X_207)),X_206)))
| ~ is_a_theorem(implies(not(X_208),X_208))
| is_a_theorem(implies(not(implies(not(X_208),X_207)),X_206)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(not(X_208),X_208))),bind(Y,$fot(implies(not(implies(not(X_208),X_207)),X_206)))]]) ).
cnf(refute_0_187,plain,
( ~ is_a_theorem(implies(X_140,implies(not(implies(not(X_140),X_139)),X_138)))
| is_a_theorem(implies(implies(not(X_140),X_140),implies(not(implies(not(X_140),X_139)),X_138))) ),
inference(subst,[],[refute_0_55:[bind(X_44,$fot(X_140)),bind(X_45,$fot(implies(not(implies(not(X_140),X_139)),X_138)))]]) ).
cnf(refute_0_188,plain,
is_a_theorem(implies(implies(not(X_133),X_132),implies(not(implies(not(X_133),X_132)),Y))),
inference(subst,[],[cn_3:[bind(X,$fot(implies(not(X_133),X_132)))]]) ).
cnf(refute_0_189,plain,
( ~ is_a_theorem(implies(implies(not(X_133),X_132),implies(not(implies(not(X_133),X_132)),Y)))
| is_a_theorem(implies(X_133,implies(not(implies(not(X_133),X_132)),Y))) ),
inference(subst,[],[refute_0_16:[bind(X_46,$fot(X_132)),bind(X_47,$fot(X_133)),bind(X_48,$fot(implies(not(implies(not(X_133),X_132)),Y)))]]) ).
cnf(refute_0_190,plain,
is_a_theorem(implies(X_133,implies(not(implies(not(X_133),X_132)),Y))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_133),X_132),implies(not(implies(not(X_133),X_132)),Y))) )],[refute_0_188,refute_0_189]) ).
cnf(refute_0_191,plain,
is_a_theorem(implies(X_140,implies(not(implies(not(X_140),X_139)),X_138))),
inference(subst,[],[refute_0_190:[bind(Y,$fot(X_138)),bind(X_132,$fot(X_139)),bind(X_133,$fot(X_140))]]) ).
cnf(refute_0_192,plain,
is_a_theorem(implies(implies(not(X_140),X_140),implies(not(implies(not(X_140),X_139)),X_138))),
inference(resolve,[$cnf( is_a_theorem(implies(X_140,implies(not(implies(not(X_140),X_139)),X_138))) )],[refute_0_191,refute_0_187]) ).
cnf(refute_0_193,plain,
is_a_theorem(implies(implies(not(X_208),X_208),implies(not(implies(not(X_208),X_207)),X_206))),
inference(subst,[],[refute_0_192:[bind(X_138,$fot(X_206)),bind(X_139,$fot(X_207)),bind(X_140,$fot(X_208))]]) ).
cnf(refute_0_194,plain,
( ~ is_a_theorem(implies(not(X_208),X_208))
| is_a_theorem(implies(not(implies(not(X_208),X_207)),X_206)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_208),X_208),implies(not(implies(not(X_208),X_207)),X_206))) )],[refute_0_193,refute_0_186]) ).
cnf(refute_0_195,plain,
( ~ is_a_theorem(implies(not(implies(implies(not(X_7701),X_7700),implies(implies(X_7700,X_7701),X_7701))),implies(implies(not(X_7701),X_7700),implies(implies(X_7700,X_7701),X_7701))))
| is_a_theorem(implies(not(implies(not(implies(implies(not(X_7701),X_7700),implies(implies(X_7700,X_7701),X_7701))),X_12042)),X_12041)) ),
inference(subst,[],[refute_0_194:[bind(X_206,$fot(X_12041)),bind(X_207,$fot(X_12042)),bind(X_208,$fot(implies(implies(not(X_7701),X_7700),implies(implies(X_7700,X_7701),X_7701))))]]) ).
cnf(refute_0_196,plain,
is_a_theorem(implies(not(implies(not(implies(implies(not(X_7701),X_7700),implies(implies(X_7700,X_7701),X_7701))),X_12042)),X_12041)),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(implies(not(X_7701),X_7700),implies(implies(X_7700,X_7701),X_7701))),implies(implies(not(X_7701),X_7700),implies(implies(X_7700,X_7701),X_7701)))) )],[refute_0_185,refute_0_195]) ).
cnf(refute_0_197,plain,
is_a_theorem(implies(not(implies(not(implies(implies(not(X_12194),X_12193),implies(implies(X_12193,X_12194),X_12194))),X_12192)),implies(not(implies(implies(not(X_12194),X_12193),implies(implies(X_12193,X_12194),X_12194))),X_12192))),
inference(subst,[],[refute_0_196:[bind(X_12041,$fot(implies(not(implies(implies(not(X_12194),X_12193),implies(implies(X_12193,X_12194),X_12194))),X_12192))),bind(X_12042,$fot(X_12192)),bind(X_7700,$fot(X_12193)),bind(X_7701,$fot(X_12194))]]) ).
cnf(refute_0_198,plain,
is_a_theorem(implies(X_3547,implies(not(implies(implies(not(X_12194),X_12193),implies(implies(X_12193,X_12194),X_12194))),X_12192))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(not(implies(implies(not(X_12194),X_12193),implies(implies(X_12193,X_12194),X_12194))),X_12192)),implies(not(implies(implies(not(X_12194),X_12193),implies(implies(X_12193,X_12194),X_12194))),X_12192))) )],[refute_0_197,refute_0_128]) ).
cnf(refute_0_199,plain,
is_a_theorem(implies(not(implies(not(implies(implies(not(X_12194),X_12193),implies(implies(X_12193,X_12194),X_12194))),implies(implies(not(X_12194),X_12193),implies(implies(X_12193,X_12194),X_12194)))),implies(not(implies(implies(not(X_12194),X_12193),implies(implies(X_12193,X_12194),X_12194))),implies(implies(not(X_12194),X_12193),implies(implies(X_12193,X_12194),X_12194))))),
inference(subst,[],[refute_0_198:[bind(X_12192,$fot(implies(implies(not(X_12194),X_12193),implies(implies(X_12193,X_12194),X_12194)))),bind(X_3547,$fot(not(implies(not(implies(implies(not(X_12194),X_12193),implies(implies(X_12193,X_12194),X_12194))),implies(implies(not(X_12194),X_12193),implies(implies(X_12193,X_12194),X_12194))))))]]) ).
cnf(refute_0_200,plain,
( ~ is_a_theorem(implies(implies(not(implies(not(implies(X_761,X_762)),implies(X_761,X_762))),implies(not(implies(X_761,X_762)),implies(X_761,X_762))),implies(implies(not(X_761),X_761),X_762)))
| ~ is_a_theorem(implies(not(implies(not(implies(X_761,X_762)),implies(X_761,X_762))),implies(not(implies(X_761,X_762)),implies(X_761,X_762))))
| is_a_theorem(implies(implies(not(X_761),X_761),X_762)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(not(implies(not(implies(X_761,X_762)),implies(X_761,X_762))),implies(not(implies(X_761,X_762)),implies(X_761,X_762))))),bind(Y,$fot(implies(implies(not(X_761),X_761),X_762)))]]) ).
cnf(refute_0_201,plain,
( ~ is_a_theorem(implies(not(implies(implies(not(implies(X_759,X_760)),implies(X_759,X_760)),implies(implies(not(X_759),X_759),X_760))),implies(implies(not(implies(X_759,X_760)),implies(X_759,X_760)),implies(implies(not(X_759),X_759),X_760))))
| is_a_theorem(implies(implies(not(implies(not(implies(X_759,X_760)),implies(X_759,X_760))),implies(not(implies(X_759,X_760)),implies(X_759,X_760))),implies(implies(not(X_759),X_759),X_760))) ),
inference(subst,[],[refute_0_59:[bind(X_84,$fot(implies(not(implies(X_759,X_760)),implies(X_759,X_760)))),bind(X_85,$fot(implies(implies(not(X_759),X_759),X_760)))]]) ).
cnf(refute_0_202,plain,
( ~ is_a_theorem(implies(implies(not(implies(X_84,X_85)),implies(X_84,X_85)),implies(implies(not(X_84),X_84),X_85)))
| is_a_theorem(implies(not(implies(implies(not(implies(X_84,X_85)),implies(X_84,X_85)),implies(implies(not(X_84),X_84),X_85))),Y)) ),
inference(subst,[],[refute_0_76:[bind(X_6,$fot(implies(implies(not(implies(X_84,X_85)),implies(X_84,X_85)),implies(implies(not(X_84),X_84),X_85))))]]) ).
cnf(refute_0_203,plain,
is_a_theorem(implies(not(implies(implies(not(implies(X_84,X_85)),implies(X_84,X_85)),implies(implies(not(X_84),X_84),X_85))),Y)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(implies(X_84,X_85)),implies(X_84,X_85)),implies(implies(not(X_84),X_84),X_85))) )],[refute_0_58,refute_0_202]) ).
cnf(refute_0_204,plain,
is_a_theorem(implies(not(implies(implies(not(implies(X_759,X_760)),implies(X_759,X_760)),implies(implies(not(X_759),X_759),X_760))),implies(implies(not(implies(X_759,X_760)),implies(X_759,X_760)),implies(implies(not(X_759),X_759),X_760)))),
inference(subst,[],[refute_0_203:[bind(Y,$fot(implies(implies(not(implies(X_759,X_760)),implies(X_759,X_760)),implies(implies(not(X_759),X_759),X_760)))),bind(X_84,$fot(X_759)),bind(X_85,$fot(X_760))]]) ).
cnf(refute_0_205,plain,
is_a_theorem(implies(implies(not(implies(not(implies(X_759,X_760)),implies(X_759,X_760))),implies(not(implies(X_759,X_760)),implies(X_759,X_760))),implies(implies(not(X_759),X_759),X_760))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(implies(not(implies(X_759,X_760)),implies(X_759,X_760)),implies(implies(not(X_759),X_759),X_760))),implies(implies(not(implies(X_759,X_760)),implies(X_759,X_760)),implies(implies(not(X_759),X_759),X_760)))) )],[refute_0_204,refute_0_201]) ).
cnf(refute_0_206,plain,
is_a_theorem(implies(implies(not(implies(not(implies(X_761,X_762)),implies(X_761,X_762))),implies(not(implies(X_761,X_762)),implies(X_761,X_762))),implies(implies(not(X_761),X_761),X_762))),
inference(subst,[],[refute_0_205:[bind(X_759,$fot(X_761)),bind(X_760,$fot(X_762))]]) ).
cnf(refute_0_207,plain,
( ~ is_a_theorem(implies(not(implies(not(implies(X_761,X_762)),implies(X_761,X_762))),implies(not(implies(X_761,X_762)),implies(X_761,X_762))))
| is_a_theorem(implies(implies(not(X_761),X_761),X_762)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(implies(not(implies(X_761,X_762)),implies(X_761,X_762))),implies(not(implies(X_761,X_762)),implies(X_761,X_762))),implies(implies(not(X_761),X_761),X_762))) )],[refute_0_206,refute_0_200]) ).
cnf(refute_0_208,plain,
( ~ is_a_theorem(implies(not(implies(not(implies(implies(not(X_12194),X_12193),implies(implies(X_12193,X_12194),X_12194))),implies(implies(not(X_12194),X_12193),implies(implies(X_12193,X_12194),X_12194)))),implies(not(implies(implies(not(X_12194),X_12193),implies(implies(X_12193,X_12194),X_12194))),implies(implies(not(X_12194),X_12193),implies(implies(X_12193,X_12194),X_12194)))))
| is_a_theorem(implies(implies(not(implies(not(X_12194),X_12193)),implies(not(X_12194),X_12193)),implies(implies(X_12193,X_12194),X_12194))) ),
inference(subst,[],[refute_0_207:[bind(X_761,$fot(implies(not(X_12194),X_12193))),bind(X_762,$fot(implies(implies(X_12193,X_12194),X_12194)))]]) ).
cnf(refute_0_209,plain,
is_a_theorem(implies(implies(not(implies(not(X_12194),X_12193)),implies(not(X_12194),X_12193)),implies(implies(X_12193,X_12194),X_12194))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(not(implies(implies(not(X_12194),X_12193),implies(implies(X_12193,X_12194),X_12194))),implies(implies(not(X_12194),X_12193),implies(implies(X_12193,X_12194),X_12194)))),implies(not(implies(implies(not(X_12194),X_12193),implies(implies(X_12193,X_12194),X_12194))),implies(implies(not(X_12194),X_12193),implies(implies(X_12193,X_12194),X_12194))))) )],[refute_0_199,refute_0_208]) ).
cnf(refute_0_210,plain,
is_a_theorem(implies(implies(not(implies(not(X_15811),X_15810)),implies(not(X_15811),X_15810)),implies(implies(X_15810,X_15811),X_15811))),
inference(subst,[],[refute_0_209:[bind(X_12193,$fot(X_15810)),bind(X_12194,$fot(X_15811))]]) ).
cnf(refute_0_211,plain,
is_a_theorem(implies(implies(implies(implies(X_15810,X_15811),X_15811),X_3304),implies(implies(not(X_15811),X_15810),X_3304))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(implies(not(X_15811),X_15810)),implies(not(X_15811),X_15810)),implies(implies(X_15810,X_15811),X_15811))) )],[refute_0_210,refute_0_47]) ).
cnf(refute_0_212,plain,
is_a_theorem(implies(implies(implies(implies(X_15818,X_15819),X_15819),implies(X_128,X_15819)),implies(implies(not(X_15819),X_15818),implies(X_128,X_15819)))),
inference(subst,[],[refute_0_211:[bind(X_15810,$fot(X_15818)),bind(X_15811,$fot(X_15819)),bind(X_3304,$fot(implies(X_128,X_15819)))]]) ).
cnf(refute_0_213,plain,
is_a_theorem(implies(implies(X_128,implies(X_15818,X_15819)),implies(implies(not(X_15819),X_15818),implies(X_128,X_15819)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_15818,X_15819),X_15819),implies(X_128,X_15819)),implies(implies(not(X_15819),X_15818),implies(X_128,X_15819)))) )],[refute_0_212,refute_0_40]) ).
cnf(refute_0_214,plain,
is_a_theorem(implies(implies(implies(X_35909,X_35910),implies(implies(not(X_35909),X_35909),X_35910)),implies(implies(not(X_35910),implies(not(X_35909),X_35909)),implies(implies(X_35909,X_35910),X_35910)))),
inference(subst,[],[refute_0_213:[bind(X_128,$fot(implies(X_35909,X_35910))),bind(X_15818,$fot(implies(not(X_35909),X_35909))),bind(X_15819,$fot(X_35910))]]) ).
cnf(refute_0_215,plain,
( ~ is_a_theorem(implies(implies(implies(X_2322,X_2323),implies(implies(not(X_2322),X_2322),X_2323)),X_2320))
| ~ is_a_theorem(implies(implies(implies(implies(X_2322,X_2323),implies(implies(not(X_2322),X_2322),X_2323)),X_2320),implies(X_2321,X_2320)))
| is_a_theorem(implies(X_2321,X_2320)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(X_2322,X_2323),implies(implies(not(X_2322),X_2322),X_2323)),X_2320))),bind(Y,$fot(implies(X_2321,X_2320)))]]) ).
cnf(refute_0_216,plain,
( ~ is_a_theorem(implies(X_949,implies(not(implies(implies(X_951,X_952),implies(implies(not(X_951),X_951),X_952))),X_950)))
| is_a_theorem(implies(implies(implies(not(implies(implies(X_951,X_952),implies(implies(not(X_951),X_951),X_952))),X_950),Z),implies(X_949,Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(X_949)),bind(Y,$fot(implies(not(implies(implies(X_951,X_952),implies(implies(not(X_951),X_951),X_952))),X_950)))]]) ).
cnf(refute_0_217,plain,
( ~ is_a_theorem(implies(implies(not(X_47),X_945),implies(not(implies(implies(X_947,X_948),implies(implies(not(X_947),X_947),X_948))),X_945)))
| is_a_theorem(implies(X_47,implies(not(implies(implies(X_947,X_948),implies(implies(not(X_947),X_947),X_948))),X_945))) ),
inference(subst,[],[refute_0_16:[bind(X_46,$fot(X_945)),bind(X_48,$fot(implies(not(implies(implies(X_947,X_948),implies(implies(not(X_947),X_947),X_948))),X_945)))]]) ).
cnf(refute_0_218,plain,
( ~ is_a_theorem(implies(not(implies(implies(X_68,X_69),implies(implies(not(X_68),X_68),X_69))),X_67))
| is_a_theorem(implies(implies(X_67,Z),implies(not(implies(implies(X_68,X_69),implies(implies(not(X_68),X_68),X_69))),Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(not(implies(implies(X_68,X_69),implies(implies(not(X_68),X_68),X_69))))),bind(Y,$fot(X_67))]]) ).
cnf(refute_0_219,plain,
( ~ is_a_theorem(implies(implies(X_44,X_45),implies(implies(not(X_44),X_44),X_45)))
| is_a_theorem(implies(not(implies(implies(X_44,X_45),implies(implies(not(X_44),X_44),X_45))),Y)) ),
inference(subst,[],[refute_0_76:[bind(X_6,$fot(implies(implies(X_44,X_45),implies(implies(not(X_44),X_44),X_45))))]]) ).
cnf(refute_0_220,plain,
is_a_theorem(implies(not(implies(implies(X_44,X_45),implies(implies(not(X_44),X_44),X_45))),Y)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_44,X_45),implies(implies(not(X_44),X_44),X_45))) )],[refute_0_54,refute_0_219]) ).
cnf(refute_0_221,plain,
is_a_theorem(implies(not(implies(implies(X_68,X_69),implies(implies(not(X_68),X_68),X_69))),X_67)),
inference(subst,[],[refute_0_220:[bind(Y,$fot(X_67)),bind(X_44,$fot(X_68)),bind(X_45,$fot(X_69))]]) ).
cnf(refute_0_222,plain,
is_a_theorem(implies(implies(X_67,Z),implies(not(implies(implies(X_68,X_69),implies(implies(not(X_68),X_68),X_69))),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(implies(X_68,X_69),implies(implies(not(X_68),X_68),X_69))),X_67)) )],[refute_0_221,refute_0_218]) ).
cnf(refute_0_223,plain,
is_a_theorem(implies(implies(not(X_47),X_945),implies(not(implies(implies(X_947,X_948),implies(implies(not(X_947),X_947),X_948))),X_945))),
inference(subst,[],[refute_0_222:[bind(Z,$fot(X_945)),bind(X_67,$fot(not(X_47))),bind(X_68,$fot(X_947)),bind(X_69,$fot(X_948))]]) ).
cnf(refute_0_224,plain,
is_a_theorem(implies(X_47,implies(not(implies(implies(X_947,X_948),implies(implies(not(X_947),X_947),X_948))),X_945))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_47),X_945),implies(not(implies(implies(X_947,X_948),implies(implies(not(X_947),X_947),X_948))),X_945))) )],[refute_0_223,refute_0_217]) ).
cnf(refute_0_225,plain,
is_a_theorem(implies(X_949,implies(not(implies(implies(X_951,X_952),implies(implies(not(X_951),X_951),X_952))),X_950))),
inference(subst,[],[refute_0_224:[bind(X_47,$fot(X_949)),bind(X_945,$fot(X_950)),bind(X_947,$fot(X_951)),bind(X_948,$fot(X_952))]]) ).
cnf(refute_0_226,plain,
is_a_theorem(implies(implies(implies(not(implies(implies(X_951,X_952),implies(implies(not(X_951),X_951),X_952))),X_950),Z),implies(X_949,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_949,implies(not(implies(implies(X_951,X_952),implies(implies(not(X_951),X_951),X_952))),X_950))) )],[refute_0_225,refute_0_216]) ).
cnf(refute_0_227,plain,
is_a_theorem(implies(implies(implies(not(implies(implies(X_951,X_952),implies(implies(not(X_951),X_951),X_952))),implies(implies(X_951,X_952),implies(implies(not(X_951),X_951),X_952))),X_2244),implies(X_949,X_2244))),
inference(subst,[],[refute_0_226:[bind(Z,$fot(X_2244)),bind(X_950,$fot(implies(implies(X_951,X_952),implies(implies(not(X_951),X_951),X_952))))]]) ).
cnf(refute_0_228,plain,
( ~ is_a_theorem(implies(implies(implies(not(implies(implies(X_951,X_952),implies(implies(not(X_951),X_951),X_952))),implies(implies(X_951,X_952),implies(implies(not(X_951),X_951),X_952))),X_2244),implies(X_949,X_2244)))
| is_a_theorem(implies(implies(implies(implies(X_951,X_952),implies(implies(not(X_951),X_951),X_952)),X_2244),implies(X_949,X_2244))) ),
inference(subst,[],[refute_0_66:[bind(X_64,$fot(implies(X_949,X_2244))),bind(X_65,$fot(implies(implies(X_951,X_952),implies(implies(not(X_951),X_951),X_952)))),bind(X_66,$fot(X_2244))]]) ).
cnf(refute_0_229,plain,
is_a_theorem(implies(implies(implies(implies(X_951,X_952),implies(implies(not(X_951),X_951),X_952)),X_2244),implies(X_949,X_2244))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(implies(implies(X_951,X_952),implies(implies(not(X_951),X_951),X_952))),implies(implies(X_951,X_952),implies(implies(not(X_951),X_951),X_952))),X_2244),implies(X_949,X_2244))) )],[refute_0_227,refute_0_228]) ).
cnf(refute_0_230,plain,
is_a_theorem(implies(implies(implies(implies(X_2322,X_2323),implies(implies(not(X_2322),X_2322),X_2323)),X_2320),implies(X_2321,X_2320))),
inference(subst,[],[refute_0_229:[bind(X_2244,$fot(X_2320)),bind(X_949,$fot(X_2321)),bind(X_951,$fot(X_2322)),bind(X_952,$fot(X_2323))]]) ).
cnf(refute_0_231,plain,
( ~ is_a_theorem(implies(implies(implies(X_2322,X_2323),implies(implies(not(X_2322),X_2322),X_2323)),X_2320))
| is_a_theorem(implies(X_2321,X_2320)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_2322,X_2323),implies(implies(not(X_2322),X_2322),X_2323)),X_2320),implies(X_2321,X_2320))) )],[refute_0_230,refute_0_215]) ).
cnf(refute_0_232,plain,
( ~ is_a_theorem(implies(implies(implies(X_35909,X_35910),implies(implies(not(X_35909),X_35909),X_35910)),implies(implies(not(X_35910),implies(not(X_35909),X_35909)),implies(implies(X_35909,X_35910),X_35910))))
| is_a_theorem(implies(X_35908,implies(implies(not(X_35910),implies(not(X_35909),X_35909)),implies(implies(X_35909,X_35910),X_35910)))) ),
inference(subst,[],[refute_0_231:[bind(X_2320,$fot(implies(implies(not(X_35910),implies(not(X_35909),X_35909)),implies(implies(X_35909,X_35910),X_35910)))),bind(X_2321,$fot(X_35908)),bind(X_2322,$fot(X_35909)),bind(X_2323,$fot(X_35910))]]) ).
cnf(refute_0_233,plain,
is_a_theorem(implies(X_35908,implies(implies(not(X_35910),implies(not(X_35909),X_35909)),implies(implies(X_35909,X_35910),X_35910)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_35909,X_35910),implies(implies(not(X_35909),X_35909),X_35910)),implies(implies(not(X_35910),implies(not(X_35909),X_35909)),implies(implies(X_35909,X_35910),X_35910)))) )],[refute_0_214,refute_0_232]) ).
cnf(refute_0_234,plain,
is_a_theorem(implies(implies(not(not(implies(implies(not(X_36141),implies(not(X_36140),X_36140)),implies(implies(X_36140,X_36141),X_36141)))),X_526),implies(implies(not(X_36141),implies(not(X_36140),X_36140)),implies(implies(X_36140,X_36141),X_36141)))),
inference(subst,[],[refute_0_233:[bind(X_35908,$fot(implies(not(not(implies(implies(not(X_36141),implies(not(X_36140),X_36140)),implies(implies(X_36140,X_36141),X_36141)))),X_526))),bind(X_35909,$fot(X_36140)),bind(X_35910,$fot(X_36141))]]) ).
cnf(refute_0_235,plain,
is_a_theorem(implies(implies(not(X_36141),implies(not(X_36140),X_36140)),implies(implies(X_36140,X_36141),X_36141))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(not(implies(implies(not(X_36141),implies(not(X_36140),X_36140)),implies(implies(X_36140,X_36141),X_36141)))),X_526),implies(implies(not(X_36141),implies(not(X_36140),X_36140)),implies(implies(X_36140,X_36141),X_36141)))) )],[refute_0_234,refute_0_39]) ).
cnf(refute_0_236,plain,
is_a_theorem(implies(implies(not(X_36143),implies(not(X_36142),X_36142)),implies(implies(X_36142,X_36143),X_36143))),
inference(subst,[],[refute_0_235:[bind(X_36140,$fot(X_36142)),bind(X_36141,$fot(X_36143))]]) ).
cnf(refute_0_237,plain,
is_a_theorem(implies(X_36142,implies(implies(X_36142,X_36143),X_36143))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_36143),implies(not(X_36142),X_36142)),implies(implies(X_36142,X_36143),X_36143))) )],[refute_0_236,refute_0_27]) ).
cnf(refute_0_238,plain,
is_a_theorem(implies(X_36144,implies(implies(X_36144,X_36145),X_36145))),
inference(subst,[],[refute_0_237:[bind(X_36142,$fot(X_36144)),bind(X_36143,$fot(X_36145))]]) ).
cnf(refute_0_239,plain,
is_a_theorem(implies(implies(implies(implies(X_36144,X_36145),X_36145),Z),implies(X_36144,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_36144,implies(implies(X_36144,X_36145),X_36145))) )],[refute_0_238,refute_0_8]) ).
cnf(refute_0_240,plain,
is_a_theorem(implies(implies(implies(implies(X_36169,X_36170),X_36170),implies(X_128,X_36170)),implies(X_36169,implies(X_128,X_36170)))),
inference(subst,[],[refute_0_239:[bind(Z,$fot(implies(X_128,X_36170))),bind(X_36144,$fot(X_36169)),bind(X_36145,$fot(X_36170))]]) ).
cnf(refute_0_241,plain,
is_a_theorem(implies(implies(X_128,implies(X_36169,X_36170)),implies(X_36169,implies(X_128,X_36170)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_36169,X_36170),X_36170),implies(X_128,X_36170)),implies(X_36169,implies(X_128,X_36170)))) )],[refute_0_240,refute_0_7]) ).
cnf(refute_0_242,plain,
is_a_theorem(implies(implies(a,implies(b,c)),implies(b,implies(a,c)))),
inference(subst,[],[refute_0_241:[bind(X_128,$fot(a)),bind(X_36169,$fot(b)),bind(X_36170,$fot(c))]]) ).
cnf(refute_0_243,plain,
$false,
inference(resolve,[$cnf( is_a_theorem(implies(implies(a,implies(b,c)),implies(b,implies(a,c)))) )],[refute_0_242,prove_cn_21]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL050-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : metis --show proof --show saturation %s
% 0.07/0.35 % Computer : n020.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sat Sep 5 21:42:57 UTC 2026
% 0.07/0.36 % CPUTime :
% 0.07/0.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 85.94/86.25 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 85.94/86.25
% 85.94/86.25 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 86.03/86.32
%------------------------------------------------------------------------------