%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : LCL379-1 : TPTP v9.3.1. Released v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 12:42:33 PM UTC 2026
% Result : Unsatisfiable 6.26s 6.58s
% Output : CNFRefutation 6.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 54
% Number of leaves : 5
% Syntax : Number of clauses : 159 ( 91 unt; 0 nHn; 46 RR)
% Number of literals : 242 ( 0 equ; 84 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 : 3 ( 3 usr; 1 con; 0-2 aty)
% Number of variables : 383 ( 59 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_38,negated_conjecture,
~ is_a_theorem(implies(implies(x,not(x)),not(x))) ).
cnf(refute_0_0,plain,
( ~ is_a_theorem(implies(implies(not(X_1304),X_1305),implies(implies(X_1305,X_1304),X_1304)))
| ~ is_a_theorem(implies(not(X_1304),X_1305))
| is_a_theorem(implies(implies(X_1305,X_1304),X_1304)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(not(X_1304),X_1305))),bind(Y,$fot(implies(implies(X_1305,X_1304),X_1304)))]]) ).
cnf(refute_0_1,plain,
( ~ is_a_theorem(implies(implies(implies(X_80,X_81),implies(X_79,X_81)),X_82))
| ~ is_a_theorem(implies(implies(implies(implies(X_80,X_81),implies(X_79,X_81)),X_82),implies(implies(X_79,X_80),X_82)))
| is_a_theorem(implies(implies(X_79,X_80),X_82)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(X_80,X_81),implies(X_79,X_81)),X_82))),bind(Y,$fot(implies(implies(X_79,X_80),X_82)))]]) ).
cnf(refute_0_2,plain,
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))))
| is_a_theorem(implies(implies(Y,Z),implies(X,Z))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X,Y))),bind(Y,$fot(implies(implies(Y,Z),implies(X,Z))))]]) ).
cnf(refute_0_3,plain,
( ~ is_a_theorem(implies(X,Y))
| is_a_theorem(implies(implies(Y,Z),implies(X,Z))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )],[cn_1,refute_0_2]) ).
cnf(refute_0_4,plain,
( ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))))
| is_a_theorem(implies(implies(implies(implies(Y,Z),implies(X,Z)),X_27),implies(implies(X,Y),X_27))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(implies(X,Y))),bind(Y,$fot(implies(implies(Y,Z),implies(X,Z)))),bind(Z,$fot(X_27))]]) ).
cnf(refute_0_5,plain,
is_a_theorem(implies(implies(implies(implies(Y,Z),implies(X,Z)),X_27),implies(implies(X,Y),X_27))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )],[cn_1,refute_0_4]) ).
cnf(refute_0_6,plain,
is_a_theorem(implies(implies(implies(implies(X_80,X_81),implies(X_79,X_81)),X_82),implies(implies(X_79,X_80),X_82))),
inference(subst,[],[refute_0_5:[bind(X,$fot(X_79)),bind(Y,$fot(X_80)),bind(Z,$fot(X_81)),bind(X_27,$fot(X_82))]]) ).
cnf(refute_0_7,plain,
( ~ is_a_theorem(implies(implies(implies(X_80,X_81),implies(X_79,X_81)),X_82))
| is_a_theorem(implies(implies(X_79,X_80),X_82)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_80,X_81),implies(X_79,X_81)),X_82),implies(implies(X_79,X_80),X_82))) )],[refute_0_6,refute_0_1]) ).
cnf(refute_0_8,plain,
( ~ is_a_theorem(implies(implies(implies(X_80,X_1274),implies(not(X_1274),X_1274)),implies(implies(X_80,X_1274),X_1274)))
| is_a_theorem(implies(implies(not(X_1274),X_80),implies(implies(X_80,X_1274),X_1274))) ),
inference(subst,[],[refute_0_7:[bind(X_79,$fot(not(X_1274))),bind(X_81,$fot(X_1274)),bind(X_82,$fot(implies(implies(X_80,X_1274),X_1274)))]]) ).
cnf(refute_0_9,plain,
is_a_theorem(implies(implies(not(X_7),X_7),X_7)),
inference(subst,[],[cn_2:[bind(X,$fot(X_7))]]) ).
cnf(refute_0_10,plain,
( ~ is_a_theorem(implies(implies(not(X_7),X_7),X_7))
| ~ is_a_theorem(implies(not(X_7),X_7))
| is_a_theorem(X_7) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(not(X_7),X_7))),bind(Y,$fot(X_7))]]) ).
cnf(refute_0_11,plain,
( ~ is_a_theorem(implies(not(X_7),X_7))
| is_a_theorem(X_7) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_7),X_7),X_7)) )],[refute_0_9,refute_0_10]) ).
cnf(refute_0_12,plain,
( ~ is_a_theorem(implies(not(implies(implies(implies(implies(not(X_936),X_936),X_936),X_937),X_937)),implies(implies(implies(implies(not(X_936),X_936),X_936),X_937),X_937)))
| is_a_theorem(implies(implies(implies(implies(not(X_936),X_936),X_936),X_937),X_937)) ),
inference(subst,[],[refute_0_11:[bind(X_7,$fot(implies(implies(implies(implies(not(X_936),X_936),X_936),X_937),X_937)))]]) ).
cnf(refute_0_13,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(X_70),X_70),X_71),X_69),implies(implies(X_70,X_71),X_69)))
| ~ is_a_theorem(implies(implies(implies(not(X_70),X_70),X_71),X_69))
| is_a_theorem(implies(implies(X_70,X_71),X_69)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(not(X_70),X_70),X_71),X_69))),bind(Y,$fot(implies(implies(X_70,X_71),X_69)))]]) ).
cnf(refute_0_14,plain,
( ~ is_a_theorem(implies(implies(X_28,X_29),implies(implies(not(X_28),X_28),X_29)))
| is_a_theorem(implies(implies(implies(implies(not(X_28),X_28),X_29),Z),implies(implies(X_28,X_29),Z))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(implies(X_28,X_29))),bind(Y,$fot(implies(implies(not(X_28),X_28),X_29)))]]) ).
cnf(refute_0_15,plain,
is_a_theorem(implies(implies(not(X_26),X_26),X_26)),
inference(subst,[],[cn_2:[bind(X,$fot(X_26))]]) ).
cnf(refute_0_16,plain,
( ~ is_a_theorem(implies(implies(not(X_26),X_26),X_26))
| is_a_theorem(implies(implies(X_26,X_27),implies(implies(not(X_26),X_26),X_27))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(implies(not(X_26),X_26))),bind(Y,$fot(X_26)),bind(Z,$fot(X_27))]]) ).
cnf(refute_0_17,plain,
is_a_theorem(implies(implies(X_26,X_27),implies(implies(not(X_26),X_26),X_27))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_26),X_26),X_26)) )],[refute_0_15,refute_0_16]) ).
cnf(refute_0_18,plain,
is_a_theorem(implies(implies(X_28,X_29),implies(implies(not(X_28),X_28),X_29))),
inference(subst,[],[refute_0_17:[bind(X_26,$fot(X_28)),bind(X_27,$fot(X_29))]]) ).
cnf(refute_0_19,plain,
is_a_theorem(implies(implies(implies(implies(not(X_28),X_28),X_29),Z),implies(implies(X_28,X_29),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_28,X_29),implies(implies(not(X_28),X_28),X_29))) )],[refute_0_18,refute_0_14]) ).
cnf(refute_0_20,plain,
is_a_theorem(implies(implies(implies(implies(not(X_70),X_70),X_71),X_69),implies(implies(X_70,X_71),X_69))),
inference(subst,[],[refute_0_19:[bind(Z,$fot(X_69)),bind(X_28,$fot(X_70)),bind(X_29,$fot(X_71))]]) ).
cnf(refute_0_21,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_70),X_70),X_71),X_69))
| is_a_theorem(implies(implies(X_70,X_71),X_69)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(X_70),X_70),X_71),X_69),implies(implies(X_70,X_71),X_69))) )],[refute_0_20,refute_0_13]) ).
cnf(refute_0_22,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_746),X_746),X_743),implies(implies(implies(implies(not(X_744),X_744),X_744),X_746),X_743)))
| is_a_theorem(implies(implies(X_746,X_743),implies(implies(implies(implies(not(X_744),X_744),X_744),X_746),X_743))) ),
inference(subst,[],[refute_0_21:[bind(X_69,$fot(implies(implies(implies(implies(not(X_744),X_744),X_744),X_746),X_743))),bind(X_70,$fot(X_746)),bind(X_71,$fot(X_743))]]) ).
cnf(refute_0_23,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(X_731),X_731),X_731),X_733),implies(X_732,X_733)))
| is_a_theorem(implies(implies(implies(X_732,X_733),Z),implies(implies(implies(implies(not(X_731),X_731),X_731),X_733),Z))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(implies(implies(implies(not(X_731),X_731),X_731),X_733))),bind(Y,$fot(implies(X_732,X_733)))]]) ).
cnf(refute_0_24,plain,
( ~ is_a_theorem(implies(X_137,implies(not(implies(implies(not(X_135),X_135),X_135)),X_136)))
| is_a_theorem(implies(implies(implies(not(implies(implies(not(X_135),X_135),X_135)),X_136),Z),implies(X_137,Z))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(X_137)),bind(Y,$fot(implies(not(implies(implies(not(X_135),X_135),X_135)),X_136)))]]) ).
cnf(refute_0_25,plain,
is_a_theorem(implies(X_6,implies(not(X_6),Y))),
inference(subst,[],[cn_3:[bind(X,$fot(X_6))]]) ).
cnf(refute_0_26,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_27,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_25,refute_0_26]) ).
cnf(refute_0_28,plain,
( ~ is_a_theorem(implies(implies(not(X),X),X))
| is_a_theorem(implies(not(implies(implies(not(X),X),X)),X_8)) ),
inference(subst,[],[refute_0_27:[bind(Y,$fot(X_8)),bind(X_6,$fot(implies(implies(not(X),X),X)))]]) ).
cnf(refute_0_29,plain,
is_a_theorem(implies(not(implies(implies(not(X),X),X)),X_8)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X),X),X)) )],[cn_2,refute_0_28]) ).
cnf(refute_0_30,plain,
is_a_theorem(implies(not(implies(implies(not(X),X),X)),X_26)),
inference(subst,[],[refute_0_29:[bind(X_8,$fot(X_26))]]) ).
cnf(refute_0_31,plain,
( ~ is_a_theorem(implies(not(implies(implies(not(X),X),X)),X_26))
| is_a_theorem(implies(implies(X_26,X_27),implies(not(implies(implies(not(X),X),X)),X_27))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(not(implies(implies(not(X),X),X)))),bind(Y,$fot(X_26)),bind(Z,$fot(X_27))]]) ).
cnf(refute_0_32,plain,
is_a_theorem(implies(implies(X_26,X_27),implies(not(implies(implies(not(X),X),X)),X_27))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(implies(not(X),X),X)),X_26)) )],[refute_0_30,refute_0_31]) ).
cnf(refute_0_33,plain,
is_a_theorem(implies(implies(not(X_108),X_107),implies(not(implies(implies(not(X),X),X)),X_107))),
inference(subst,[],[refute_0_32:[bind(X_26,$fot(not(X_108))),bind(X_27,$fot(X_107))]]) ).
cnf(refute_0_34,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_31),X_30),X_32),implies(X_31,X_32)))
| ~ is_a_theorem(implies(implies(not(X_31),X_30),X_32))
| is_a_theorem(implies(X_31,X_32)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(not(X_31),X_30),X_32))),bind(Y,$fot(implies(X_31,X_32)))]]) ).
cnf(refute_0_35,plain,
is_a_theorem(implies(X_25,implies(not(X_25),Y))),
inference(subst,[],[cn_3:[bind(X,$fot(X_25))]]) ).
cnf(refute_0_36,plain,
( ~ is_a_theorem(implies(X_25,implies(not(X_25),Y)))
| is_a_theorem(implies(implies(implies(not(X_25),Y),X_27),implies(X_25,X_27))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(X_25)),bind(Y,$fot(implies(not(X_25),Y))),bind(Z,$fot(X_27))]]) ).
cnf(refute_0_37,plain,
is_a_theorem(implies(implies(implies(not(X_25),Y),X_27),implies(X_25,X_27))),
inference(resolve,[$cnf( is_a_theorem(implies(X_25,implies(not(X_25),Y))) )],[refute_0_35,refute_0_36]) ).
cnf(refute_0_38,plain,
is_a_theorem(implies(implies(implies(not(X_31),X_30),X_32),implies(X_31,X_32))),
inference(subst,[],[refute_0_37:[bind(Y,$fot(X_30)),bind(X_25,$fot(X_31)),bind(X_27,$fot(X_32))]]) ).
cnf(refute_0_39,plain,
( ~ is_a_theorem(implies(implies(not(X_31),X_30),X_32))
| is_a_theorem(implies(X_31,X_32)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_31),X_30),X_32),implies(X_31,X_32))) )],[refute_0_38,refute_0_34]) ).
cnf(refute_0_40,plain,
( ~ is_a_theorem(implies(implies(not(X_108),X_107),implies(not(implies(implies(not(X),X),X)),X_107)))
| is_a_theorem(implies(X_108,implies(not(implies(implies(not(X),X),X)),X_107))) ),
inference(subst,[],[refute_0_39:[bind(X_30,$fot(X_107)),bind(X_31,$fot(X_108)),bind(X_32,$fot(implies(not(implies(implies(not(X),X),X)),X_107)))]]) ).
cnf(refute_0_41,plain,
is_a_theorem(implies(X_108,implies(not(implies(implies(not(X),X),X)),X_107))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_108),X_107),implies(not(implies(implies(not(X),X),X)),X_107))) )],[refute_0_33,refute_0_40]) ).
cnf(refute_0_42,plain,
is_a_theorem(implies(X_137,implies(not(implies(implies(not(X_135),X_135),X_135)),X_136))),
inference(subst,[],[refute_0_41:[bind(X,$fot(X_135)),bind(X_107,$fot(X_136)),bind(X_108,$fot(X_137))]]) ).
cnf(refute_0_43,plain,
is_a_theorem(implies(implies(implies(not(implies(implies(not(X_135),X_135),X_135)),X_136),Z),implies(X_137,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_137,implies(not(implies(implies(not(X_135),X_135),X_135)),X_136))) )],[refute_0_42,refute_0_24]) ).
cnf(refute_0_44,plain,
is_a_theorem(implies(implies(implies(not(implies(implies(not(X_135),X_135),X_135)),implies(implies(not(X_135),X_135),X_135)),X_730),implies(X_137,X_730))),
inference(subst,[],[refute_0_43:[bind(Z,$fot(X_730)),bind(X_136,$fot(implies(implies(not(X_135),X_135),X_135)))]]) ).
cnf(refute_0_45,plain,
( ~ is_a_theorem(implies(implies(implies(not(implies(implies(not(X_135),X_135),X_135)),implies(implies(not(X_135),X_135),X_135)),X_730),implies(X_137,X_730)))
| is_a_theorem(implies(implies(implies(implies(not(X_135),X_135),X_135),X_730),implies(X_137,X_730))) ),
inference(subst,[],[refute_0_21:[bind(X_69,$fot(implies(X_137,X_730))),bind(X_70,$fot(implies(implies(not(X_135),X_135),X_135))),bind(X_71,$fot(X_730))]]) ).
cnf(refute_0_46,plain,
is_a_theorem(implies(implies(implies(implies(not(X_135),X_135),X_135),X_730),implies(X_137,X_730))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(implies(implies(not(X_135),X_135),X_135)),implies(implies(not(X_135),X_135),X_135)),X_730),implies(X_137,X_730))) )],[refute_0_44,refute_0_45]) ).
cnf(refute_0_47,plain,
is_a_theorem(implies(implies(implies(implies(not(X_731),X_731),X_731),X_733),implies(X_732,X_733))),
inference(subst,[],[refute_0_46:[bind(X_135,$fot(X_731)),bind(X_137,$fot(X_732)),bind(X_730,$fot(X_733))]]) ).
cnf(refute_0_48,plain,
is_a_theorem(implies(implies(implies(X_732,X_733),Z),implies(implies(implies(implies(not(X_731),X_731),X_731),X_733),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(X_731),X_731),X_731),X_733),implies(X_732,X_733))) )],[refute_0_47,refute_0_23]) ).
cnf(refute_0_49,plain,
is_a_theorem(implies(implies(implies(not(X_746),X_746),X_743),implies(implies(implies(implies(not(X_744),X_744),X_744),X_746),X_743))),
inference(subst,[],[refute_0_48:[bind(Z,$fot(X_743)),bind(X_731,$fot(X_744)),bind(X_732,$fot(not(X_746))),bind(X_733,$fot(X_746))]]) ).
cnf(refute_0_50,plain,
is_a_theorem(implies(implies(X_746,X_743),implies(implies(implies(implies(not(X_744),X_744),X_744),X_746),X_743))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_746),X_746),X_743),implies(implies(implies(implies(not(X_744),X_744),X_744),X_746),X_743))) )],[refute_0_49,refute_0_22]) ).
cnf(refute_0_51,plain,
is_a_theorem(implies(implies(X_840,X_840),implies(implies(implies(implies(not(X_744),X_744),X_744),X_840),X_840))),
inference(subst,[],[refute_0_50:[bind(X_743,$fot(X_840)),bind(X_746,$fot(X_840))]]) ).
cnf(refute_0_52,plain,
( ~ is_a_theorem(implies(implies(X_734,X_734),X_736))
| ~ is_a_theorem(implies(implies(implies(X_734,X_734),X_736),implies(X_735,X_736)))
| is_a_theorem(implies(X_735,X_736)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_734,X_734),X_736))),bind(Y,$fot(implies(X_735,X_736)))]]) ).
cnf(refute_0_53,plain,
( ~ is_a_theorem(implies(X_140,implies(not(implies(X_139,X_139)),X_138)))
| is_a_theorem(implies(implies(implies(not(implies(X_139,X_139)),X_138),Z),implies(X_140,Z))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(X_140)),bind(Y,$fot(implies(not(implies(X_139,X_139)),X_138)))]]) ).
cnf(refute_0_54,plain,
( ~ is_a_theorem(implies(implies(not(X_31),X_129),implies(not(implies(X_131,X_131)),X_129)))
| is_a_theorem(implies(X_31,implies(not(implies(X_131,X_131)),X_129))) ),
inference(subst,[],[refute_0_39:[bind(X_30,$fot(X_129)),bind(X_32,$fot(implies(not(implies(X_131,X_131)),X_129)))]]) ).
cnf(refute_0_55,plain,
( ~ is_a_theorem(implies(not(implies(X_112,X_112)),X_111))
| is_a_theorem(implies(implies(X_111,Z),implies(not(implies(X_112,X_112)),Z))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(not(implies(X_112,X_112)))),bind(Y,$fot(X_111))]]) ).
cnf(refute_0_56,plain,
( ~ is_a_theorem(implies(X_110,X_110))
| is_a_theorem(implies(not(implies(X_110,X_110)),Y)) ),
inference(subst,[],[refute_0_27:[bind(X_6,$fot(implies(X_110,X_110)))]]) ).
cnf(refute_0_57,plain,
is_a_theorem(implies(implies(not(X_109),X_109),X_109)),
inference(subst,[],[cn_2:[bind(X,$fot(X_109))]]) ).
cnf(refute_0_58,plain,
( ~ is_a_theorem(implies(implies(not(X_109),X_109),X_109))
| is_a_theorem(implies(X_109,X_109)) ),
inference(subst,[],[refute_0_39:[bind(X_30,$fot(X_109)),bind(X_31,$fot(X_109)),bind(X_32,$fot(X_109))]]) ).
cnf(refute_0_59,plain,
is_a_theorem(implies(X_109,X_109)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_109),X_109),X_109)) )],[refute_0_57,refute_0_58]) ).
cnf(refute_0_60,plain,
is_a_theorem(implies(X_110,X_110)),
inference(subst,[],[refute_0_59:[bind(X_109,$fot(X_110))]]) ).
cnf(refute_0_61,plain,
is_a_theorem(implies(not(implies(X_110,X_110)),Y)),
inference(resolve,[$cnf( is_a_theorem(implies(X_110,X_110)) )],[refute_0_60,refute_0_56]) ).
cnf(refute_0_62,plain,
is_a_theorem(implies(not(implies(X_112,X_112)),X_111)),
inference(subst,[],[refute_0_61:[bind(Y,$fot(X_111)),bind(X_110,$fot(X_112))]]) ).
cnf(refute_0_63,plain,
is_a_theorem(implies(implies(X_111,Z),implies(not(implies(X_112,X_112)),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(X_112,X_112)),X_111)) )],[refute_0_62,refute_0_55]) ).
cnf(refute_0_64,plain,
is_a_theorem(implies(implies(not(X_31),X_129),implies(not(implies(X_131,X_131)),X_129))),
inference(subst,[],[refute_0_63:[bind(Z,$fot(X_129)),bind(X_111,$fot(not(X_31))),bind(X_112,$fot(X_131))]]) ).
cnf(refute_0_65,plain,
is_a_theorem(implies(X_31,implies(not(implies(X_131,X_131)),X_129))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_31),X_129),implies(not(implies(X_131,X_131)),X_129))) )],[refute_0_64,refute_0_54]) ).
cnf(refute_0_66,plain,
is_a_theorem(implies(X_140,implies(not(implies(X_139,X_139)),X_138))),
inference(subst,[],[refute_0_65:[bind(X_129,$fot(X_138)),bind(X_131,$fot(X_139)),bind(X_31,$fot(X_140))]]) ).
cnf(refute_0_67,plain,
is_a_theorem(implies(implies(implies(not(implies(X_139,X_139)),X_138),Z),implies(X_140,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_140,implies(not(implies(X_139,X_139)),X_138))) )],[refute_0_66,refute_0_53]) ).
cnf(refute_0_68,plain,
is_a_theorem(implies(implies(implies(not(implies(X_139,X_139)),implies(X_139,X_139)),X_730),implies(X_140,X_730))),
inference(subst,[],[refute_0_67:[bind(Z,$fot(X_730)),bind(X_138,$fot(implies(X_139,X_139)))]]) ).
cnf(refute_0_69,plain,
( ~ is_a_theorem(implies(implies(implies(not(implies(X_139,X_139)),implies(X_139,X_139)),X_730),implies(X_140,X_730)))
| is_a_theorem(implies(implies(implies(X_139,X_139),X_730),implies(X_140,X_730))) ),
inference(subst,[],[refute_0_21:[bind(X_69,$fot(implies(X_140,X_730))),bind(X_70,$fot(implies(X_139,X_139))),bind(X_71,$fot(X_730))]]) ).
cnf(refute_0_70,plain,
is_a_theorem(implies(implies(implies(X_139,X_139),X_730),implies(X_140,X_730))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(implies(X_139,X_139)),implies(X_139,X_139)),X_730),implies(X_140,X_730))) )],[refute_0_68,refute_0_69]) ).
cnf(refute_0_71,plain,
is_a_theorem(implies(implies(implies(X_734,X_734),X_736),implies(X_735,X_736))),
inference(subst,[],[refute_0_70:[bind(X_139,$fot(X_734)),bind(X_140,$fot(X_735)),bind(X_730,$fot(X_736))]]) ).
cnf(refute_0_72,plain,
( ~ is_a_theorem(implies(implies(X_734,X_734),X_736))
| is_a_theorem(implies(X_735,X_736)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_734,X_734),X_736),implies(X_735,X_736))) )],[refute_0_71,refute_0_52]) ).
cnf(refute_0_73,plain,
( ~ is_a_theorem(implies(implies(X_840,X_840),implies(implies(implies(implies(not(X_744),X_744),X_744),X_840),X_840)))
| is_a_theorem(implies(X_841,implies(implies(implies(implies(not(X_744),X_744),X_744),X_840),X_840))) ),
inference(subst,[],[refute_0_72:[bind(X_734,$fot(X_840)),bind(X_735,$fot(X_841)),bind(X_736,$fot(implies(implies(implies(implies(not(X_744),X_744),X_744),X_840),X_840)))]]) ).
cnf(refute_0_74,plain,
is_a_theorem(implies(X_841,implies(implies(implies(implies(not(X_744),X_744),X_744),X_840),X_840))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_840,X_840),implies(implies(implies(implies(not(X_744),X_744),X_744),X_840),X_840))) )],[refute_0_51,refute_0_73]) ).
cnf(refute_0_75,plain,
is_a_theorem(implies(not(implies(implies(implies(implies(not(X_936),X_936),X_936),X_937),X_937)),implies(implies(implies(implies(not(X_936),X_936),X_936),X_937),X_937))),
inference(subst,[],[refute_0_74:[bind(X_744,$fot(X_936)),bind(X_840,$fot(X_937)),bind(X_841,$fot(not(implies(implies(implies(implies(not(X_936),X_936),X_936),X_937),X_937))))]]) ).
cnf(refute_0_76,plain,
is_a_theorem(implies(implies(implies(implies(not(X_936),X_936),X_936),X_937),X_937)),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(implies(implies(implies(not(X_936),X_936),X_936),X_937),X_937)),implies(implies(implies(implies(not(X_936),X_936),X_936),X_937),X_937))) )],[refute_0_75,refute_0_12]) ).
cnf(refute_0_77,plain,
is_a_theorem(implies(implies(implies(implies(not(X_1264),X_1264),X_1264),implies(X_1262,X_1264)),implies(X_1262,X_1264))),
inference(subst,[],[refute_0_76:[bind(X_936,$fot(X_1264)),bind(X_937,$fot(implies(X_1262,X_1264)))]]) ).
cnf(refute_0_78,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(X_1264),X_1264),X_1264),implies(X_1262,X_1264)),implies(X_1262,X_1264)))
| is_a_theorem(implies(implies(X_1262,implies(not(X_1264),X_1264)),implies(X_1262,X_1264))) ),
inference(subst,[],[refute_0_7:[bind(X_79,$fot(X_1262)),bind(X_80,$fot(implies(not(X_1264),X_1264))),bind(X_81,$fot(X_1264)),bind(X_82,$fot(implies(X_1262,X_1264)))]]) ).
cnf(refute_0_79,plain,
is_a_theorem(implies(implies(X_1262,implies(not(X_1264),X_1264)),implies(X_1262,X_1264))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(X_1264),X_1264),X_1264),implies(X_1262,X_1264)),implies(X_1262,X_1264))) )],[refute_0_77,refute_0_78]) ).
cnf(refute_0_80,plain,
is_a_theorem(implies(implies(implies(X_80,X_1274),implies(not(X_1274),X_1274)),implies(implies(X_80,X_1274),X_1274))),
inference(subst,[],[refute_0_79:[bind(X_1262,$fot(implies(X_80,X_1274))),bind(X_1264,$fot(X_1274))]]) ).
cnf(refute_0_81,plain,
is_a_theorem(implies(implies(not(X_1274),X_80),implies(implies(X_80,X_1274),X_1274))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_80,X_1274),implies(not(X_1274),X_1274)),implies(implies(X_80,X_1274),X_1274))) )],[refute_0_80,refute_0_8]) ).
cnf(refute_0_82,plain,
is_a_theorem(implies(implies(not(X_1304),X_1305),implies(implies(X_1305,X_1304),X_1304))),
inference(subst,[],[refute_0_81:[bind(X_1274,$fot(X_1304)),bind(X_80,$fot(X_1305))]]) ).
cnf(refute_0_83,plain,
( ~ is_a_theorem(implies(not(X_1304),X_1305))
| is_a_theorem(implies(implies(X_1305,X_1304),X_1304)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_1304),X_1305),implies(implies(X_1305,X_1304),X_1304))) )],[refute_0_82,refute_0_0]) ).
cnf(refute_0_84,plain,
( ~ is_a_theorem(implies(not(not(X_3971)),X_3971))
| is_a_theorem(implies(implies(X_3971,not(X_3971)),not(X_3971))) ),
inference(subst,[],[refute_0_83:[bind(X_1304,$fot(not(X_3971))),bind(X_1305,$fot(X_3971))]]) ).
cnf(refute_0_85,plain,
( ~ is_a_theorem(implies(implies(not(not(not(X_3970))),not(not(X_3970))),X_3970))
| is_a_theorem(implies(not(not(X_3970)),X_3970)) ),
inference(subst,[],[refute_0_39:[bind(X_30,$fot(not(not(X_3970)))),bind(X_31,$fot(not(not(X_3970)))),bind(X_32,$fot(X_3970))]]) ).
cnf(refute_0_86,plain,
( ~ is_a_theorem(implies(implies(implies(not(not(X_3968)),not(not(X_3968))),implies(not(not(not(X_3968))),not(not(X_3968)))),X_3968))
| is_a_theorem(implies(implies(not(not(not(X_3968))),not(not(X_3968))),X_3968)) ),
inference(subst,[],[refute_0_7:[bind(X_79,$fot(not(not(not(X_3968))))),bind(X_80,$fot(not(not(X_3968)))),bind(X_81,$fot(not(not(X_3968)))),bind(X_82,$fot(X_3968))]]) ).
cnf(refute_0_87,plain,
( ~ is_a_theorem(implies(X_114,implies(implies(not(not(X_114)),not(X_114)),X_113)))
| is_a_theorem(implies(implies(implies(implies(not(not(X_114)),not(X_114)),X_113),Z),implies(X_114,Z))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(X_114)),bind(Y,$fot(implies(implies(not(not(X_114)),not(X_114)),X_113)))]]) ).
cnf(refute_0_88,plain,
is_a_theorem(implies(implies(not(X_108),X_107),implies(implies(not(not(X_108)),not(X_108)),X_107))),
inference(subst,[],[refute_0_17:[bind(X_26,$fot(not(X_108))),bind(X_27,$fot(X_107))]]) ).
cnf(refute_0_89,plain,
( ~ is_a_theorem(implies(implies(not(X_108),X_107),implies(implies(not(not(X_108)),not(X_108)),X_107)))
| is_a_theorem(implies(X_108,implies(implies(not(not(X_108)),not(X_108)),X_107))) ),
inference(subst,[],[refute_0_39:[bind(X_30,$fot(X_107)),bind(X_31,$fot(X_108)),bind(X_32,$fot(implies(implies(not(not(X_108)),not(X_108)),X_107)))]]) ).
cnf(refute_0_90,plain,
is_a_theorem(implies(X_108,implies(implies(not(not(X_108)),not(X_108)),X_107))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_108),X_107),implies(implies(not(not(X_108)),not(X_108)),X_107))) )],[refute_0_88,refute_0_89]) ).
cnf(refute_0_91,plain,
is_a_theorem(implies(X_114,implies(implies(not(not(X_114)),not(X_114)),X_113))),
inference(subst,[],[refute_0_90:[bind(X_107,$fot(X_113)),bind(X_108,$fot(X_114))]]) ).
cnf(refute_0_92,plain,
is_a_theorem(implies(implies(implies(implies(not(not(X_114)),not(X_114)),X_113),Z),implies(X_114,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_114,implies(implies(not(not(X_114)),not(X_114)),X_113))) )],[refute_0_91,refute_0_87]) ).
cnf(refute_0_93,plain,
is_a_theorem(implies(implies(implies(implies(not(not(X_114)),not(X_114)),X_1264),implies(X_1262,X_1264)),implies(X_114,implies(X_1262,X_1264)))),
inference(subst,[],[refute_0_92:[bind(Z,$fot(implies(X_1262,X_1264))),bind(X_113,$fot(X_1264))]]) ).
cnf(refute_0_94,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(not(X_114)),not(X_114)),X_1264),implies(X_1262,X_1264)),implies(X_114,implies(X_1262,X_1264))))
| is_a_theorem(implies(implies(X_1262,implies(not(not(X_114)),not(X_114))),implies(X_114,implies(X_1262,X_1264)))) ),
inference(subst,[],[refute_0_7:[bind(X_79,$fot(X_1262)),bind(X_80,$fot(implies(not(not(X_114)),not(X_114)))),bind(X_81,$fot(X_1264)),bind(X_82,$fot(implies(X_114,implies(X_1262,X_1264))))]]) ).
cnf(refute_0_95,plain,
is_a_theorem(implies(implies(X_1262,implies(not(not(X_114)),not(X_114))),implies(X_114,implies(X_1262,X_1264)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(not(X_114)),not(X_114)),X_1264),implies(X_1262,X_1264)),implies(X_114,implies(X_1262,X_1264)))) )],[refute_0_93,refute_0_94]) ).
cnf(refute_0_96,plain,
is_a_theorem(implies(implies(not(X_2602),implies(not(not(not(X_2602))),not(not(X_2602)))),implies(not(X_2602),implies(not(X_2602),X_2602)))),
inference(subst,[],[refute_0_95:[bind(X_114,$fot(not(X_2602))),bind(X_1262,$fot(not(X_2602))),bind(X_1264,$fot(X_2602))]]) ).
cnf(refute_0_97,plain,
( ~ is_a_theorem(implies(X_2521,implies(not(X_2520),implies(not(X_2520),X_2520))))
| ~ is_a_theorem(implies(implies(X_2521,implies(not(X_2520),implies(not(X_2520),X_2520))),implies(X_2521,X_2520)))
| is_a_theorem(implies(X_2521,X_2520)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X_2521,implies(not(X_2520),implies(not(X_2520),X_2520))))),bind(Y,$fot(implies(X_2521,X_2520)))]]) ).
cnf(refute_0_98,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(X_2502),implies(not(X_2502),X_2502)),X_2502),implies(X_79,X_2502)),implies(X_79,X_2502)))
| is_a_theorem(implies(implies(X_79,implies(not(X_2502),implies(not(X_2502),X_2502))),implies(X_79,X_2502))) ),
inference(subst,[],[refute_0_7:[bind(X_80,$fot(implies(not(X_2502),implies(not(X_2502),X_2502)))),bind(X_81,$fot(X_2502)),bind(X_82,$fot(implies(X_79,X_2502)))]]) ).
cnf(refute_0_99,plain,
( ~ is_a_theorem(implies(X_1273,implies(not(X_1274),X_1274)))
| ~ is_a_theorem(implies(implies(X_1273,implies(not(X_1274),X_1274)),implies(X_1273,X_1274)))
| is_a_theorem(implies(X_1273,X_1274)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X_1273,implies(not(X_1274),X_1274)))),bind(Y,$fot(implies(X_1273,X_1274)))]]) ).
cnf(refute_0_100,plain,
is_a_theorem(implies(implies(X_1273,implies(not(X_1274),X_1274)),implies(X_1273,X_1274))),
inference(subst,[],[refute_0_79:[bind(X_1262,$fot(X_1273)),bind(X_1264,$fot(X_1274))]]) ).
cnf(refute_0_101,plain,
( ~ is_a_theorem(implies(X_1273,implies(not(X_1274),X_1274)))
| is_a_theorem(implies(X_1273,X_1274)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_1273,implies(not(X_1274),X_1274)),implies(X_1273,X_1274))) )],[refute_0_100,refute_0_99]) ).
cnf(refute_0_102,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(X_2499),implies(not(X_2499),X_2499)),X_2499),X_2501),implies(not(X_2501),X_2501)))
| is_a_theorem(implies(implies(implies(implies(not(X_2499),implies(not(X_2499),X_2499)),X_2499),X_2501),X_2501)) ),
inference(subst,[],[refute_0_101:[bind(X_1273,$fot(implies(implies(implies(not(X_2499),implies(not(X_2499),X_2499)),X_2499),X_2501))),bind(X_1274,$fot(X_2501))]]) ).
cnf(refute_0_103,plain,
( ~ is_a_theorem(implies(implies(X_1473,X_1473),implies(implies(not(X_1473),implies(not(X_1473),X_1473)),X_1473)))
| is_a_theorem(implies(X_735,implies(implies(not(X_1473),implies(not(X_1473),X_1473)),X_1473))) ),
inference(subst,[],[refute_0_72:[bind(X_734,$fot(X_1473)),bind(X_736,$fot(implies(implies(not(X_1473),implies(not(X_1473),X_1473)),X_1473)))]]) ).
cnf(refute_0_104,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_1472),X_1472),X_1470),implies(implies(not(X_1472),implies(not(X_1472),X_1472)),X_1470)))
| is_a_theorem(implies(implies(X_1472,X_1470),implies(implies(not(X_1472),implies(not(X_1472),X_1472)),X_1470))) ),
inference(subst,[],[refute_0_21:[bind(X_69,$fot(implies(implies(not(X_1472),implies(not(X_1472),X_1472)),X_1470))),bind(X_70,$fot(X_1472)),bind(X_71,$fot(X_1470))]]) ).
cnf(refute_0_105,plain,
( ~ is_a_theorem(implies(implies(X_1273,implies(not(X_1274),X_1274)),implies(X_1273,X_1274)))
| is_a_theorem(implies(implies(implies(X_1273,X_1274),Z),implies(implies(X_1273,implies(not(X_1274),X_1274)),Z))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(implies(X_1273,implies(not(X_1274),X_1274)))),bind(Y,$fot(implies(X_1273,X_1274)))]]) ).
cnf(refute_0_106,plain,
is_a_theorem(implies(implies(implies(X_1273,X_1274),Z),implies(implies(X_1273,implies(not(X_1274),X_1274)),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_1273,implies(not(X_1274),X_1274)),implies(X_1273,X_1274))) )],[refute_0_100,refute_0_105]) ).
cnf(refute_0_107,plain,
is_a_theorem(implies(implies(implies(not(X_1472),X_1472),X_1470),implies(implies(not(X_1472),implies(not(X_1472),X_1472)),X_1470))),
inference(subst,[],[refute_0_106:[bind(Z,$fot(X_1470)),bind(X_1273,$fot(not(X_1472))),bind(X_1274,$fot(X_1472))]]) ).
cnf(refute_0_108,plain,
is_a_theorem(implies(implies(X_1472,X_1470),implies(implies(not(X_1472),implies(not(X_1472),X_1472)),X_1470))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_1472),X_1472),X_1470),implies(implies(not(X_1472),implies(not(X_1472),X_1472)),X_1470))) )],[refute_0_107,refute_0_104]) ).
cnf(refute_0_109,plain,
is_a_theorem(implies(implies(X_1473,X_1473),implies(implies(not(X_1473),implies(not(X_1473),X_1473)),X_1473))),
inference(subst,[],[refute_0_108:[bind(X_1470,$fot(X_1473)),bind(X_1472,$fot(X_1473))]]) ).
cnf(refute_0_110,plain,
is_a_theorem(implies(X_735,implies(implies(not(X_1473),implies(not(X_1473),X_1473)),X_1473))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_1473,X_1473),implies(implies(not(X_1473),implies(not(X_1473),X_1473)),X_1473))) )],[refute_0_109,refute_0_103]) ).
cnf(refute_0_111,plain,
is_a_theorem(implies(X_1962,implies(implies(not(X_1473),implies(not(X_1473),X_1473)),X_1473))),
inference(subst,[],[refute_0_110:[bind(X_735,$fot(X_1962))]]) ).
cnf(refute_0_112,plain,
( ~ is_a_theorem(implies(X_1282,X_1283))
| ~ is_a_theorem(implies(implies(X_1282,X_1283),implies(X_1284,implies(X_1282,X_1283))))
| is_a_theorem(implies(X_1284,implies(X_1282,X_1283))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X_1282,X_1283))),bind(Y,$fot(implies(X_1284,implies(X_1282,X_1283))))]]) ).
cnf(refute_0_113,plain,
is_a_theorem(implies(implies(implies(X_1264,X_1264),implies(X_1262,X_1264)),implies(X_140,implies(X_1262,X_1264)))),
inference(subst,[],[refute_0_70:[bind(X_139,$fot(X_1264)),bind(X_730,$fot(implies(X_1262,X_1264)))]]) ).
cnf(refute_0_114,plain,
( ~ is_a_theorem(implies(implies(implies(X_1264,X_1264),implies(X_1262,X_1264)),implies(X_140,implies(X_1262,X_1264))))
| is_a_theorem(implies(implies(X_1262,X_1264),implies(X_140,implies(X_1262,X_1264)))) ),
inference(subst,[],[refute_0_7:[bind(X_79,$fot(X_1262)),bind(X_80,$fot(X_1264)),bind(X_81,$fot(X_1264)),bind(X_82,$fot(implies(X_140,implies(X_1262,X_1264))))]]) ).
cnf(refute_0_115,plain,
is_a_theorem(implies(implies(X_1262,X_1264),implies(X_140,implies(X_1262,X_1264)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_1264,X_1264),implies(X_1262,X_1264)),implies(X_140,implies(X_1262,X_1264)))) )],[refute_0_113,refute_0_114]) ).
cnf(refute_0_116,plain,
is_a_theorem(implies(implies(X_1282,X_1283),implies(X_1284,implies(X_1282,X_1283)))),
inference(subst,[],[refute_0_115:[bind(X_1262,$fot(X_1282)),bind(X_1264,$fot(X_1283)),bind(X_140,$fot(X_1284))]]) ).
cnf(refute_0_117,plain,
( ~ is_a_theorem(implies(X_1282,X_1283))
| is_a_theorem(implies(X_1284,implies(X_1282,X_1283))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_1282,X_1283),implies(X_1284,implies(X_1282,X_1283)))) )],[refute_0_116,refute_0_112]) ).
cnf(refute_0_118,plain,
( ~ is_a_theorem(implies(X_1962,implies(implies(not(X_1473),implies(not(X_1473),X_1473)),X_1473)))
| is_a_theorem(implies(X_1964,implies(X_1962,implies(implies(not(X_1473),implies(not(X_1473),X_1473)),X_1473)))) ),
inference(subst,[],[refute_0_117:[bind(X_1282,$fot(X_1962)),bind(X_1283,$fot(implies(implies(not(X_1473),implies(not(X_1473),X_1473)),X_1473))),bind(X_1284,$fot(X_1964))]]) ).
cnf(refute_0_119,plain,
is_a_theorem(implies(X_1964,implies(X_1962,implies(implies(not(X_1473),implies(not(X_1473),X_1473)),X_1473)))),
inference(resolve,[$cnf( is_a_theorem(implies(X_1962,implies(implies(not(X_1473),implies(not(X_1473),X_1473)),X_1473))) )],[refute_0_111,refute_0_118]) ).
cnf(refute_0_120,plain,
is_a_theorem(implies(not(implies(X_2460,implies(implies(not(X_1473),implies(not(X_1473),X_1473)),X_1473))),implies(X_2460,implies(implies(not(X_1473),implies(not(X_1473),X_1473)),X_1473)))),
inference(subst,[],[refute_0_119:[bind(X_1962,$fot(X_2460)),bind(X_1964,$fot(not(implies(X_2460,implies(implies(not(X_1473),implies(not(X_1473),X_1473)),X_1473)))))]]) ).
cnf(refute_0_121,plain,
( ~ is_a_theorem(implies(implies(not(implies(X_251,X_252)),implies(X_251,X_252)),implies(implies(X_252,X_253),implies(X_251,X_253))))
| ~ is_a_theorem(implies(not(implies(X_251,X_252)),implies(X_251,X_252)))
| is_a_theorem(implies(implies(X_252,X_253),implies(X_251,X_253))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(not(implies(X_251,X_252)),implies(X_251,X_252)))),bind(Y,$fot(implies(implies(X_252,X_253),implies(X_251,X_253))))]]) ).
cnf(refute_0_122,plain,
( ~ is_a_theorem(implies(X_28,X_29))
| ~ is_a_theorem(implies(implies(X_28,X_29),implies(implies(not(X_28),X_28),X_29)))
| is_a_theorem(implies(implies(not(X_28),X_28),X_29)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X_28,X_29))),bind(Y,$fot(implies(implies(not(X_28),X_28),X_29)))]]) ).
cnf(refute_0_123,plain,
( ~ is_a_theorem(implies(X_28,X_29))
| is_a_theorem(implies(implies(not(X_28),X_28),X_29)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_28,X_29),implies(implies(not(X_28),X_28),X_29))) )],[refute_0_18,refute_0_122]) ).
cnf(refute_0_124,plain,
( ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))))
| is_a_theorem(implies(implies(not(implies(X,Y)),implies(X,Y)),implies(implies(Y,Z),implies(X,Z)))) ),
inference(subst,[],[refute_0_123:[bind(X_28,$fot(implies(X,Y))),bind(X_29,$fot(implies(implies(Y,Z),implies(X,Z))))]]) ).
cnf(refute_0_125,plain,
is_a_theorem(implies(implies(not(implies(X,Y)),implies(X,Y)),implies(implies(Y,Z),implies(X,Z)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )],[cn_1,refute_0_124]) ).
cnf(refute_0_126,plain,
is_a_theorem(implies(implies(not(implies(X_251,X_252)),implies(X_251,X_252)),implies(implies(X_252,X_253),implies(X_251,X_253)))),
inference(subst,[],[refute_0_125:[bind(X,$fot(X_251)),bind(Y,$fot(X_252)),bind(Z,$fot(X_253))]]) ).
cnf(refute_0_127,plain,
( ~ is_a_theorem(implies(not(implies(X_251,X_252)),implies(X_251,X_252)))
| is_a_theorem(implies(implies(X_252,X_253),implies(X_251,X_253))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(implies(X_251,X_252)),implies(X_251,X_252)),implies(implies(X_252,X_253),implies(X_251,X_253)))) )],[refute_0_126,refute_0_121]) ).
cnf(refute_0_128,plain,
( ~ is_a_theorem(implies(not(implies(X_2460,implies(implies(not(X_1473),implies(not(X_1473),X_1473)),X_1473))),implies(X_2460,implies(implies(not(X_1473),implies(not(X_1473),X_1473)),X_1473))))
| is_a_theorem(implies(implies(implies(implies(not(X_1473),implies(not(X_1473),X_1473)),X_1473),X_2462),implies(X_2460,X_2462))) ),
inference(subst,[],[refute_0_127:[bind(X_251,$fot(X_2460)),bind(X_252,$fot(implies(implies(not(X_1473),implies(not(X_1473),X_1473)),X_1473))),bind(X_253,$fot(X_2462))]]) ).
cnf(refute_0_129,plain,
is_a_theorem(implies(implies(implies(implies(not(X_1473),implies(not(X_1473),X_1473)),X_1473),X_2462),implies(X_2460,X_2462))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(X_2460,implies(implies(not(X_1473),implies(not(X_1473),X_1473)),X_1473))),implies(X_2460,implies(implies(not(X_1473),implies(not(X_1473),X_1473)),X_1473)))) )],[refute_0_120,refute_0_128]) ).
cnf(refute_0_130,plain,
is_a_theorem(implies(implies(implies(implies(not(X_2499),implies(not(X_2499),X_2499)),X_2499),X_2501),implies(not(X_2501),X_2501))),
inference(subst,[],[refute_0_129:[bind(X_1473,$fot(X_2499)),bind(X_2460,$fot(not(X_2501))),bind(X_2462,$fot(X_2501))]]) ).
cnf(refute_0_131,plain,
is_a_theorem(implies(implies(implies(implies(not(X_2499),implies(not(X_2499),X_2499)),X_2499),X_2501),X_2501)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(X_2499),implies(not(X_2499),X_2499)),X_2499),X_2501),implies(not(X_2501),X_2501))) )],[refute_0_130,refute_0_102]) ).
cnf(refute_0_132,plain,
is_a_theorem(implies(implies(implies(implies(not(X_2502),implies(not(X_2502),X_2502)),X_2502),implies(X_79,X_2502)),implies(X_79,X_2502))),
inference(subst,[],[refute_0_131:[bind(X_2499,$fot(X_2502)),bind(X_2501,$fot(implies(X_79,X_2502)))]]) ).
cnf(refute_0_133,plain,
is_a_theorem(implies(implies(X_79,implies(not(X_2502),implies(not(X_2502),X_2502))),implies(X_79,X_2502))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(X_2502),implies(not(X_2502),X_2502)),X_2502),implies(X_79,X_2502)),implies(X_79,X_2502))) )],[refute_0_132,refute_0_98]) ).
cnf(refute_0_134,plain,
is_a_theorem(implies(implies(X_2521,implies(not(X_2520),implies(not(X_2520),X_2520))),implies(X_2521,X_2520))),
inference(subst,[],[refute_0_133:[bind(X_2502,$fot(X_2520)),bind(X_79,$fot(X_2521))]]) ).
cnf(refute_0_135,plain,
( ~ is_a_theorem(implies(X_2521,implies(not(X_2520),implies(not(X_2520),X_2520))))
| is_a_theorem(implies(X_2521,X_2520)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_2521,implies(not(X_2520),implies(not(X_2520),X_2520))),implies(X_2521,X_2520))) )],[refute_0_134,refute_0_97]) ).
cnf(refute_0_136,plain,
( ~ is_a_theorem(implies(implies(not(X_2602),implies(not(not(not(X_2602))),not(not(X_2602)))),implies(not(X_2602),implies(not(X_2602),X_2602))))
| is_a_theorem(implies(implies(not(X_2602),implies(not(not(not(X_2602))),not(not(X_2602)))),X_2602)) ),
inference(subst,[],[refute_0_135:[bind(X_2520,$fot(X_2602)),bind(X_2521,$fot(implies(not(X_2602),implies(not(not(not(X_2602))),not(not(X_2602))))))]]) ).
cnf(refute_0_137,plain,
is_a_theorem(implies(implies(not(X_2602),implies(not(not(not(X_2602))),not(not(X_2602)))),X_2602)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_2602),implies(not(not(not(X_2602))),not(not(X_2602)))),implies(not(X_2602),implies(not(X_2602),X_2602)))) )],[refute_0_96,refute_0_136]) ).
cnf(refute_0_138,plain,
is_a_theorem(implies(implies(not(X_3929),implies(not(not(not(X_3929))),not(not(X_3929)))),X_3929)),
inference(subst,[],[refute_0_137:[bind(X_2602,$fot(X_3929))]]) ).
cnf(refute_0_139,plain,
( ~ is_a_theorem(implies(implies(X_105,X_106),X_103))
| ~ is_a_theorem(implies(implies(implies(X_105,X_106),X_103),implies(implies(implies(not(X_105),X_104),X_106),X_103)))
| is_a_theorem(implies(implies(implies(not(X_105),X_104),X_106),X_103)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_105,X_106),X_103))),bind(Y,$fot(implies(implies(implies(not(X_105),X_104),X_106),X_103)))]]) ).
cnf(refute_0_140,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_31),X_30),X_32),implies(X_31,X_32)))
| is_a_theorem(implies(implies(implies(X_31,X_32),Z),implies(implies(implies(not(X_31),X_30),X_32),Z))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(implies(implies(not(X_31),X_30),X_32))),bind(Y,$fot(implies(X_31,X_32)))]]) ).
cnf(refute_0_141,plain,
is_a_theorem(implies(implies(implies(X_31,X_32),Z),implies(implies(implies(not(X_31),X_30),X_32),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_31),X_30),X_32),implies(X_31,X_32))) )],[refute_0_38,refute_0_140]) ).
cnf(refute_0_142,plain,
is_a_theorem(implies(implies(implies(X_105,X_106),X_103),implies(implies(implies(not(X_105),X_104),X_106),X_103))),
inference(subst,[],[refute_0_141:[bind(Z,$fot(X_103)),bind(X_30,$fot(X_104)),bind(X_31,$fot(X_105)),bind(X_32,$fot(X_106))]]) ).
cnf(refute_0_143,plain,
( ~ is_a_theorem(implies(implies(X_105,X_106),X_103))
| is_a_theorem(implies(implies(implies(not(X_105),X_104),X_106),X_103)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_105,X_106),X_103),implies(implies(implies(not(X_105),X_104),X_106),X_103))) )],[refute_0_142,refute_0_139]) ).
cnf(refute_0_144,plain,
( ~ is_a_theorem(implies(implies(not(X_3929),implies(not(not(not(X_3929))),not(not(X_3929)))),X_3929))
| is_a_theorem(implies(implies(implies(not(not(X_3929)),X_3930),implies(not(not(not(X_3929))),not(not(X_3929)))),X_3929)) ),
inference(subst,[],[refute_0_143:[bind(X_103,$fot(X_3929)),bind(X_104,$fot(X_3930)),bind(X_105,$fot(not(X_3929))),bind(X_106,$fot(implies(not(not(not(X_3929))),not(not(X_3929)))))]]) ).
cnf(refute_0_145,plain,
is_a_theorem(implies(implies(implies(not(not(X_3929)),X_3930),implies(not(not(not(X_3929))),not(not(X_3929)))),X_3929)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_3929),implies(not(not(not(X_3929))),not(not(X_3929)))),X_3929)) )],[refute_0_138,refute_0_144]) ).
cnf(refute_0_146,plain,
is_a_theorem(implies(implies(implies(not(not(X_3968)),not(not(X_3968))),implies(not(not(not(X_3968))),not(not(X_3968)))),X_3968)),
inference(subst,[],[refute_0_145:[bind(X_3929,$fot(X_3968)),bind(X_3930,$fot(not(not(X_3968))))]]) ).
cnf(refute_0_147,plain,
is_a_theorem(implies(implies(not(not(not(X_3968))),not(not(X_3968))),X_3968)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(not(X_3968)),not(not(X_3968))),implies(not(not(not(X_3968))),not(not(X_3968)))),X_3968)) )],[refute_0_146,refute_0_86]) ).
cnf(refute_0_148,plain,
is_a_theorem(implies(implies(not(not(not(X_3970))),not(not(X_3970))),X_3970)),
inference(subst,[],[refute_0_147:[bind(X_3968,$fot(X_3970))]]) ).
cnf(refute_0_149,plain,
is_a_theorem(implies(not(not(X_3970)),X_3970)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(not(not(X_3970))),not(not(X_3970))),X_3970)) )],[refute_0_148,refute_0_85]) ).
cnf(refute_0_150,plain,
is_a_theorem(implies(not(not(X_3971)),X_3971)),
inference(subst,[],[refute_0_149:[bind(X_3970,$fot(X_3971))]]) ).
cnf(refute_0_151,plain,
is_a_theorem(implies(implies(X_3971,not(X_3971)),not(X_3971))),
inference(resolve,[$cnf( is_a_theorem(implies(not(not(X_3971)),X_3971)) )],[refute_0_150,refute_0_84]) ).
cnf(refute_0_152,plain,
is_a_theorem(implies(implies(x,not(x)),not(x))),
inference(subst,[],[refute_0_151:[bind(X_3971,$fot(x))]]) ).
cnf(refute_0_153,plain,
$false,
inference(resolve,[$cnf( is_a_theorem(implies(implies(x,not(x)),not(x))) )],[refute_0_152,prove_cn_38]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL379-1 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.04 % Command : metis --show proof --show saturation %s
% 0.08/0.35 % Computer : n004.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 5 01:09:59 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 6.26/6.58 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.26/6.58
% 6.26/6.58 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 6.36/6.68
%------------------------------------------------------------------------------