%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : LCL048-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n029.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 6.06s 6.34s
% Output : CNFRefutation 6.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 47
% Number of leaves : 5
% Syntax : Number of clauses : 106 ( 62 unt; 0 nHn; 27 RR)
% Number of literals : 160 ( 0 equ; 55 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 6 ( 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 : 272 ( 42 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_19,negated_conjecture,
~ is_a_theorem(implies(implies(implies(a,b),c),implies(b,c))) ).
cnf(refute_0_0,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_1,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_0]) ).
cnf(refute_0_2,plain,
( ~ is_a_theorem(implies(X_4574,implies(X_4575,X_4574)))
| is_a_theorem(implies(implies(implies(X_4575,X_4574),Z),implies(X_4574,Z))) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(X_4574)),bind(Y,$fot(implies(X_4575,X_4574)))]]) ).
cnf(refute_0_3,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_29),X_28),X_30),implies(X_29,X_30)))
| ~ is_a_theorem(implies(implies(not(X_29),X_28),X_30))
| is_a_theorem(implies(X_29,X_30)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(not(X_29),X_28),X_30))),bind(Y,$fot(implies(X_29,X_30)))]]) ).
cnf(refute_0_4,plain,
is_a_theorem(implies(X_23,implies(not(X_23),Y))),
inference(subst,[],[cn_3:[bind(X,$fot(X_23))]]) ).
cnf(refute_0_5,plain,
( ~ is_a_theorem(implies(X_23,implies(not(X_23),Y)))
| is_a_theorem(implies(implies(implies(not(X_23),Y),X_25),implies(X_23,X_25))) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(X_23)),bind(Y,$fot(implies(not(X_23),Y))),bind(Z,$fot(X_25))]]) ).
cnf(refute_0_6,plain,
is_a_theorem(implies(implies(implies(not(X_23),Y),X_25),implies(X_23,X_25))),
inference(resolve,[$cnf( is_a_theorem(implies(X_23,implies(not(X_23),Y))) )],[refute_0_4,refute_0_5]) ).
cnf(refute_0_7,plain,
is_a_theorem(implies(implies(implies(not(X_29),X_28),X_30),implies(X_29,X_30))),
inference(subst,[],[refute_0_6:[bind(Y,$fot(X_28)),bind(X_23,$fot(X_29)),bind(X_25,$fot(X_30))]]) ).
cnf(refute_0_8,plain,
( ~ is_a_theorem(implies(implies(not(X_29),X_28),X_30))
| is_a_theorem(implies(X_29,X_30)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_29),X_28),X_30),implies(X_29,X_30))) )],[refute_0_7,refute_0_3]) ).
cnf(refute_0_9,plain,
( ~ is_a_theorem(implies(implies(not(X_4572),not(X_4573)),implies(X_4573,X_4572)))
| is_a_theorem(implies(X_4572,implies(X_4573,X_4572))) ),
inference(subst,[],[refute_0_8:[bind(X_28,$fot(not(X_4573))),bind(X_29,$fot(X_4572)),bind(X_30,$fot(implies(X_4573,X_4572)))]]) ).
cnf(refute_0_10,plain,
( ~ is_a_theorem(implies(implies(implies(X_32,X_33),implies(X_31,X_33)),X_34))
| ~ is_a_theorem(implies(implies(implies(implies(X_32,X_33),implies(X_31,X_33)),X_34),implies(implies(X_31,X_32),X_34)))
| is_a_theorem(implies(implies(X_31,X_32),X_34)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(X_32,X_33),implies(X_31,X_33)),X_34))),bind(Y,$fot(implies(implies(X_31,X_32),X_34)))]]) ).
cnf(refute_0_11,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_25),implies(implies(X,Y),X_25))) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(implies(X,Y))),bind(Y,$fot(implies(implies(Y,Z),implies(X,Z)))),bind(Z,$fot(X_25))]]) ).
cnf(refute_0_12,plain,
is_a_theorem(implies(implies(implies(implies(Y,Z),implies(X,Z)),X_25),implies(implies(X,Y),X_25))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )],[cn_1,refute_0_11]) ).
cnf(refute_0_13,plain,
is_a_theorem(implies(implies(implies(implies(X_32,X_33),implies(X_31,X_33)),X_34),implies(implies(X_31,X_32),X_34))),
inference(subst,[],[refute_0_12:[bind(X,$fot(X_31)),bind(Y,$fot(X_32)),bind(Z,$fot(X_33)),bind(X_25,$fot(X_34))]]) ).
cnf(refute_0_14,plain,
( ~ is_a_theorem(implies(implies(implies(X_32,X_33),implies(X_31,X_33)),X_34))
| is_a_theorem(implies(implies(X_31,X_32),X_34)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_32,X_33),implies(X_31,X_33)),X_34),implies(implies(X_31,X_32),X_34))) )],[refute_0_13,refute_0_10]) ).
cnf(refute_0_15,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_4567),X_4565),implies(not(X_4565),X_4565)),implies(X_4567,X_4565)))
| is_a_theorem(implies(implies(not(X_4565),not(X_4567)),implies(X_4567,X_4565))) ),
inference(subst,[],[refute_0_14:[bind(X_31,$fot(not(X_4565))),bind(X_32,$fot(not(X_4567))),bind(X_33,$fot(X_4565)),bind(X_34,$fot(implies(X_4567,X_4565)))]]) ).
cnf(refute_0_16,plain,
( ~ is_a_theorem(implies(X_4288,implies(X_4289,X_4289)))
| ~ is_a_theorem(implies(implies(X_4288,implies(X_4289,X_4289)),implies(implies(X_4289,implies(not(X_4290),X_4290)),implies(X_4289,X_4290))))
| is_a_theorem(implies(implies(X_4289,implies(not(X_4290),X_4290)),implies(X_4289,X_4290))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X_4288,implies(X_4289,X_4289)))),bind(Y,$fot(implies(implies(X_4289,implies(not(X_4290),X_4290)),implies(X_4289,X_4290))))]]) ).
cnf(refute_0_17,plain,
( ~ is_a_theorem(implies(implies(implies(not(implies(X_151,X_151)),X_149),X_148),implies(implies(X_150,X_149),X_148)))
| ~ is_a_theorem(implies(implies(not(implies(X_151,X_151)),X_149),X_148))
| is_a_theorem(implies(implies(X_150,X_149),X_148)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(not(implies(X_151,X_151)),X_149),X_148))),bind(Y,$fot(implies(implies(X_150,X_149),X_148)))]]) ).
cnf(refute_0_18,plain,
( ~ is_a_theorem(implies(implies(X_94,X_93),implies(not(implies(X_95,X_95)),X_93)))
| is_a_theorem(implies(implies(implies(not(implies(X_95,X_95)),X_93),Z),implies(implies(X_94,X_93),Z))) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(implies(X_94,X_93))),bind(Y,$fot(implies(not(implies(X_95,X_95)),X_93)))]]) ).
cnf(refute_0_19,plain,
( ~ is_a_theorem(implies(not(implies(X_76,X_76)),X_75))
| is_a_theorem(implies(implies(X_75,Z),implies(not(implies(X_76,X_76)),Z))) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(not(implies(X_76,X_76)))),bind(Y,$fot(X_75))]]) ).
cnf(refute_0_20,plain,
is_a_theorem(implies(X_6,implies(not(X_6),Y))),
inference(subst,[],[cn_3:[bind(X,$fot(X_6))]]) ).
cnf(refute_0_21,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_22,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_20,refute_0_21]) ).
cnf(refute_0_23,plain,
( ~ is_a_theorem(implies(X_74,X_74))
| is_a_theorem(implies(not(implies(X_74,X_74)),Y)) ),
inference(subst,[],[refute_0_22:[bind(X_6,$fot(implies(X_74,X_74)))]]) ).
cnf(refute_0_24,plain,
is_a_theorem(implies(implies(not(X_73),X_73),X_73)),
inference(subst,[],[cn_2:[bind(X,$fot(X_73))]]) ).
cnf(refute_0_25,plain,
( ~ is_a_theorem(implies(implies(not(X_73),X_73),X_73))
| is_a_theorem(implies(X_73,X_73)) ),
inference(subst,[],[refute_0_8:[bind(X_28,$fot(X_73)),bind(X_29,$fot(X_73)),bind(X_30,$fot(X_73))]]) ).
cnf(refute_0_26,plain,
is_a_theorem(implies(X_73,X_73)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_73),X_73),X_73)) )],[refute_0_24,refute_0_25]) ).
cnf(refute_0_27,plain,
is_a_theorem(implies(X_74,X_74)),
inference(subst,[],[refute_0_26:[bind(X_73,$fot(X_74))]]) ).
cnf(refute_0_28,plain,
is_a_theorem(implies(not(implies(X_74,X_74)),Y)),
inference(resolve,[$cnf( is_a_theorem(implies(X_74,X_74)) )],[refute_0_27,refute_0_23]) ).
cnf(refute_0_29,plain,
is_a_theorem(implies(not(implies(X_76,X_76)),X_75)),
inference(subst,[],[refute_0_28:[bind(Y,$fot(X_75)),bind(X_74,$fot(X_76))]]) ).
cnf(refute_0_30,plain,
is_a_theorem(implies(implies(X_75,Z),implies(not(implies(X_76,X_76)),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(X_76,X_76)),X_75)) )],[refute_0_29,refute_0_19]) ).
cnf(refute_0_31,plain,
is_a_theorem(implies(implies(X_94,X_93),implies(not(implies(X_95,X_95)),X_93))),
inference(subst,[],[refute_0_30:[bind(Z,$fot(X_93)),bind(X_75,$fot(X_94)),bind(X_76,$fot(X_95))]]) ).
cnf(refute_0_32,plain,
is_a_theorem(implies(implies(implies(not(implies(X_95,X_95)),X_93),Z),implies(implies(X_94,X_93),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_94,X_93),implies(not(implies(X_95,X_95)),X_93))) )],[refute_0_31,refute_0_18]) ).
cnf(refute_0_33,plain,
is_a_theorem(implies(implies(implies(not(implies(X_151,X_151)),X_149),X_148),implies(implies(X_150,X_149),X_148))),
inference(subst,[],[refute_0_32:[bind(Z,$fot(X_148)),bind(X_93,$fot(X_149)),bind(X_94,$fot(X_150)),bind(X_95,$fot(X_151))]]) ).
cnf(refute_0_34,plain,
( ~ is_a_theorem(implies(implies(not(implies(X_151,X_151)),X_149),X_148))
| is_a_theorem(implies(implies(X_150,X_149),X_148)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(implies(X_151,X_151)),X_149),X_148),implies(implies(X_150,X_149),X_148))) )],[refute_0_33,refute_0_17]) ).
cnf(refute_0_35,plain,
( ~ is_a_theorem(implies(implies(not(implies(X_4285,X_4285)),implies(X_4285,X_4285)),implies(implies(X_4285,implies(not(X_4286),X_4286)),implies(X_4285,X_4286))))
| is_a_theorem(implies(implies(X_150,implies(X_4285,X_4285)),implies(implies(X_4285,implies(not(X_4286),X_4286)),implies(X_4285,X_4286)))) ),
inference(subst,[],[refute_0_34:[bind(X_148,$fot(implies(implies(X_4285,implies(not(X_4286),X_4286)),implies(X_4285,X_4286)))),bind(X_149,$fot(implies(X_4285,X_4285))),bind(X_151,$fot(X_4285))]]) ).
cnf(refute_0_36,plain,
( ~ is_a_theorem(implies(X_26,X_27))
| ~ is_a_theorem(implies(implies(X_26,X_27),implies(implies(not(X_26),X_26),X_27)))
| is_a_theorem(implies(implies(not(X_26),X_26),X_27)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X_26,X_27))),bind(Y,$fot(implies(implies(not(X_26),X_26),X_27)))]]) ).
cnf(refute_0_37,plain,
is_a_theorem(implies(implies(not(X_24),X_24),X_24)),
inference(subst,[],[cn_2:[bind(X,$fot(X_24))]]) ).
cnf(refute_0_38,plain,
( ~ is_a_theorem(implies(implies(not(X_24),X_24),X_24))
| is_a_theorem(implies(implies(X_24,X_25),implies(implies(not(X_24),X_24),X_25))) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(implies(not(X_24),X_24))),bind(Y,$fot(X_24)),bind(Z,$fot(X_25))]]) ).
cnf(refute_0_39,plain,
is_a_theorem(implies(implies(X_24,X_25),implies(implies(not(X_24),X_24),X_25))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_24),X_24),X_24)) )],[refute_0_37,refute_0_38]) ).
cnf(refute_0_40,plain,
is_a_theorem(implies(implies(X_26,X_27),implies(implies(not(X_26),X_26),X_27))),
inference(subst,[],[refute_0_39:[bind(X_24,$fot(X_26)),bind(X_25,$fot(X_27))]]) ).
cnf(refute_0_41,plain,
( ~ is_a_theorem(implies(X_26,X_27))
| is_a_theorem(implies(implies(not(X_26),X_26),X_27)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_26,X_27),implies(implies(not(X_26),X_26),X_27))) )],[refute_0_40,refute_0_36]) ).
cnf(refute_0_42,plain,
( ~ is_a_theorem(implies(implies(X_3274,X_3272),implies(implies(X_3272,implies(not(X_3273),X_3273)),implies(X_3274,X_3273))))
| is_a_theorem(implies(implies(not(implies(X_3274,X_3272)),implies(X_3274,X_3272)),implies(implies(X_3272,implies(not(X_3273),X_3273)),implies(X_3274,X_3273)))) ),
inference(subst,[],[refute_0_41:[bind(X_26,$fot(implies(X_3274,X_3272))),bind(X_27,$fot(implies(implies(X_3272,implies(not(X_3273),X_3273)),implies(X_3274,X_3273))))]]) ).
cnf(refute_0_43,plain,
( ~ is_a_theorem(implies(implies(implies(X_2340,X_2341),implies(X_31,X_2341)),implies(implies(X_2340,implies(not(X_2341),X_2341)),implies(X_31,X_2341))))
| is_a_theorem(implies(implies(X_31,X_2340),implies(implies(X_2340,implies(not(X_2341),X_2341)),implies(X_31,X_2341)))) ),
inference(subst,[],[refute_0_14:[bind(X_32,$fot(X_2340)),bind(X_33,$fot(X_2341)),bind(X_34,$fot(implies(implies(X_2340,implies(not(X_2341),X_2341)),implies(X_31,X_2341))))]]) ).
cnf(refute_0_44,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(X_64),X_64),X_65),X_63),implies(implies(X_64,X_65),X_63)))
| ~ is_a_theorem(implies(implies(implies(not(X_64),X_64),X_65),X_63))
| is_a_theorem(implies(implies(X_64,X_65),X_63)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(not(X_64),X_64),X_65),X_63))),bind(Y,$fot(implies(implies(X_64,X_65),X_63)))]]) ).
cnf(refute_0_45,plain,
( ~ is_a_theorem(implies(implies(X_26,X_27),implies(implies(not(X_26),X_26),X_27)))
| is_a_theorem(implies(implies(implies(implies(not(X_26),X_26),X_27),Z),implies(implies(X_26,X_27),Z))) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(implies(X_26,X_27))),bind(Y,$fot(implies(implies(not(X_26),X_26),X_27)))]]) ).
cnf(refute_0_46,plain,
is_a_theorem(implies(implies(implies(implies(not(X_26),X_26),X_27),Z),implies(implies(X_26,X_27),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_26,X_27),implies(implies(not(X_26),X_26),X_27))) )],[refute_0_40,refute_0_45]) ).
cnf(refute_0_47,plain,
is_a_theorem(implies(implies(implies(implies(not(X_64),X_64),X_65),X_63),implies(implies(X_64,X_65),X_63))),
inference(subst,[],[refute_0_46:[bind(Z,$fot(X_63)),bind(X_26,$fot(X_64)),bind(X_27,$fot(X_65))]]) ).
cnf(refute_0_48,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_64),X_64),X_65),X_63))
| is_a_theorem(implies(implies(X_64,X_65),X_63)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(X_64),X_64),X_65),X_63),implies(implies(X_64,X_65),X_63))) )],[refute_0_47,refute_0_44]) ).
cnf(refute_0_49,plain,
( ~ is_a_theorem(implies(implies(implies(not(implies(X_2099,X_2100)),implies(X_2099,X_2100)),X_2098),implies(implies(X_2099,implies(not(X_2100),X_2100)),X_2098)))
| is_a_theorem(implies(implies(implies(X_2099,X_2100),X_2098),implies(implies(X_2099,implies(not(X_2100),X_2100)),X_2098))) ),
inference(subst,[],[refute_0_48:[bind(X_63,$fot(implies(implies(X_2099,implies(not(X_2100),X_2100)),X_2098))),bind(X_64,$fot(implies(X_2099,X_2100))),bind(X_65,$fot(X_2098))]]) ).
cnf(refute_0_50,plain,
( ~ is_a_theorem(implies(implies(X_1915,implies(not(X_1916),X_1916)),implies(X_1917,implies(X_1915,X_1916))))
| is_a_theorem(implies(implies(implies(X_1917,implies(X_1915,X_1916)),Z),implies(implies(X_1915,implies(not(X_1916),X_1916)),Z))) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(implies(X_1915,implies(not(X_1916),X_1916)))),bind(Y,$fot(implies(X_1917,implies(X_1915,X_1916))))]]) ).
cnf(refute_0_51,plain,
( ~ is_a_theorem(implies(X_982,implies(implies(not(X_983),X_983),X_983)))
| is_a_theorem(implies(implies(implies(implies(not(X_983),X_983),X_983),Z),implies(X_982,Z))) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(X_982)),bind(Y,$fot(implies(implies(not(X_983),X_983),X_983)))]]) ).
cnf(refute_0_52,plain,
( ~ is_a_theorem(implies(implies(not(X_29),implies(X_981,X_981)),implies(implies(not(X_981),X_981),X_981)))
| is_a_theorem(implies(X_29,implies(implies(not(X_981),X_981),X_981))) ),
inference(subst,[],[refute_0_8:[bind(X_28,$fot(implies(X_981,X_981))),bind(X_30,$fot(implies(implies(not(X_981),X_981),X_981)))]]) ).
cnf(refute_0_53,plain,
( ~ is_a_theorem(implies(implies(X_24,X_25),implies(implies(not(X_24),X_24),X_25)))
| is_a_theorem(implies(implies(not(implies(X_24,X_25)),implies(X_24,X_25)),implies(implies(not(X_24),X_24),X_25))) ),
inference(subst,[],[refute_0_41:[bind(X_26,$fot(implies(X_24,X_25))),bind(X_27,$fot(implies(implies(not(X_24),X_24),X_25)))]]) ).
cnf(refute_0_54,plain,
is_a_theorem(implies(implies(not(implies(X_24,X_25)),implies(X_24,X_25)),implies(implies(not(X_24),X_24),X_25))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_24,X_25),implies(implies(not(X_24),X_24),X_25))) )],[refute_0_39,refute_0_53]) ).
cnf(refute_0_55,plain,
is_a_theorem(implies(implies(not(implies(X_979,X_979)),implies(X_979,X_979)),implies(implies(not(X_979),X_979),X_979))),
inference(subst,[],[refute_0_54:[bind(X_24,$fot(X_979)),bind(X_25,$fot(X_979))]]) ).
cnf(refute_0_56,plain,
( ~ is_a_theorem(implies(implies(not(implies(X_979,X_979)),implies(X_979,X_979)),implies(implies(not(X_979),X_979),X_979)))
| is_a_theorem(implies(implies(X_978,implies(X_979,X_979)),implies(implies(not(X_979),X_979),X_979))) ),
inference(subst,[],[refute_0_34:[bind(X_148,$fot(implies(implies(not(X_979),X_979),X_979))),bind(X_149,$fot(implies(X_979,X_979))),bind(X_150,$fot(X_978)),bind(X_151,$fot(X_979))]]) ).
cnf(refute_0_57,plain,
is_a_theorem(implies(implies(X_978,implies(X_979,X_979)),implies(implies(not(X_979),X_979),X_979))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(implies(X_979,X_979)),implies(X_979,X_979)),implies(implies(not(X_979),X_979),X_979))) )],[refute_0_55,refute_0_56]) ).
cnf(refute_0_58,plain,
is_a_theorem(implies(implies(not(X_29),implies(X_981,X_981)),implies(implies(not(X_981),X_981),X_981))),
inference(subst,[],[refute_0_57:[bind(X_978,$fot(not(X_29))),bind(X_979,$fot(X_981))]]) ).
cnf(refute_0_59,plain,
is_a_theorem(implies(X_29,implies(implies(not(X_981),X_981),X_981))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_29),implies(X_981,X_981)),implies(implies(not(X_981),X_981),X_981))) )],[refute_0_58,refute_0_52]) ).
cnf(refute_0_60,plain,
is_a_theorem(implies(X_982,implies(implies(not(X_983),X_983),X_983))),
inference(subst,[],[refute_0_59:[bind(X_29,$fot(X_982)),bind(X_981,$fot(X_983))]]) ).
cnf(refute_0_61,plain,
is_a_theorem(implies(implies(implies(implies(not(X_983),X_983),X_983),Z),implies(X_982,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_982,implies(implies(not(X_983),X_983),X_983))) )],[refute_0_60,refute_0_51]) ).
cnf(refute_0_62,plain,
is_a_theorem(implies(implies(implies(implies(not(X_1902),X_1902),X_1902),implies(X_1900,X_1902)),implies(X_982,implies(X_1900,X_1902)))),
inference(subst,[],[refute_0_61:[bind(Z,$fot(implies(X_1900,X_1902))),bind(X_983,$fot(X_1902))]]) ).
cnf(refute_0_63,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(X_1902),X_1902),X_1902),implies(X_1900,X_1902)),implies(X_982,implies(X_1900,X_1902))))
| is_a_theorem(implies(implies(X_1900,implies(not(X_1902),X_1902)),implies(X_982,implies(X_1900,X_1902)))) ),
inference(subst,[],[refute_0_14:[bind(X_31,$fot(X_1900)),bind(X_32,$fot(implies(not(X_1902),X_1902))),bind(X_33,$fot(X_1902)),bind(X_34,$fot(implies(X_982,implies(X_1900,X_1902))))]]) ).
cnf(refute_0_64,plain,
is_a_theorem(implies(implies(X_1900,implies(not(X_1902),X_1902)),implies(X_982,implies(X_1900,X_1902)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(X_1902),X_1902),X_1902),implies(X_1900,X_1902)),implies(X_982,implies(X_1900,X_1902)))) )],[refute_0_62,refute_0_63]) ).
cnf(refute_0_65,plain,
is_a_theorem(implies(implies(X_1915,implies(not(X_1916),X_1916)),implies(X_1917,implies(X_1915,X_1916)))),
inference(subst,[],[refute_0_64:[bind(X_1900,$fot(X_1915)),bind(X_1902,$fot(X_1916)),bind(X_982,$fot(X_1917))]]) ).
cnf(refute_0_66,plain,
is_a_theorem(implies(implies(implies(X_1917,implies(X_1915,X_1916)),Z),implies(implies(X_1915,implies(not(X_1916),X_1916)),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_1915,implies(not(X_1916),X_1916)),implies(X_1917,implies(X_1915,X_1916)))) )],[refute_0_65,refute_0_50]) ).
cnf(refute_0_67,plain,
is_a_theorem(implies(implies(implies(not(implies(X_2099,X_2100)),implies(X_2099,X_2100)),X_2098),implies(implies(X_2099,implies(not(X_2100),X_2100)),X_2098))),
inference(subst,[],[refute_0_66:[bind(Z,$fot(X_2098)),bind(X_1915,$fot(X_2099)),bind(X_1916,$fot(X_2100)),bind(X_1917,$fot(not(implies(X_2099,X_2100))))]]) ).
cnf(refute_0_68,plain,
is_a_theorem(implies(implies(implies(X_2099,X_2100),X_2098),implies(implies(X_2099,implies(not(X_2100),X_2100)),X_2098))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(implies(X_2099,X_2100)),implies(X_2099,X_2100)),X_2098),implies(implies(X_2099,implies(not(X_2100),X_2100)),X_2098))) )],[refute_0_67,refute_0_49]) ).
cnf(refute_0_69,plain,
is_a_theorem(implies(implies(implies(X_2340,X_2341),implies(X_31,X_2341)),implies(implies(X_2340,implies(not(X_2341),X_2341)),implies(X_31,X_2341)))),
inference(subst,[],[refute_0_68:[bind(X_2098,$fot(implies(X_31,X_2341))),bind(X_2099,$fot(X_2340)),bind(X_2100,$fot(X_2341))]]) ).
cnf(refute_0_70,plain,
is_a_theorem(implies(implies(X_31,X_2340),implies(implies(X_2340,implies(not(X_2341),X_2341)),implies(X_31,X_2341)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_2340,X_2341),implies(X_31,X_2341)),implies(implies(X_2340,implies(not(X_2341),X_2341)),implies(X_31,X_2341)))) )],[refute_0_69,refute_0_43]) ).
cnf(refute_0_71,plain,
is_a_theorem(implies(implies(X_3274,X_3272),implies(implies(X_3272,implies(not(X_3273),X_3273)),implies(X_3274,X_3273)))),
inference(subst,[],[refute_0_70:[bind(X_2340,$fot(X_3272)),bind(X_2341,$fot(X_3273)),bind(X_31,$fot(X_3274))]]) ).
cnf(refute_0_72,plain,
is_a_theorem(implies(implies(not(implies(X_3274,X_3272)),implies(X_3274,X_3272)),implies(implies(X_3272,implies(not(X_3273),X_3273)),implies(X_3274,X_3273)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_3274,X_3272),implies(implies(X_3272,implies(not(X_3273),X_3273)),implies(X_3274,X_3273)))) )],[refute_0_71,refute_0_42]) ).
cnf(refute_0_73,plain,
is_a_theorem(implies(implies(not(implies(X_4285,X_4285)),implies(X_4285,X_4285)),implies(implies(X_4285,implies(not(X_4286),X_4286)),implies(X_4285,X_4286)))),
inference(subst,[],[refute_0_72:[bind(X_3272,$fot(X_4285)),bind(X_3273,$fot(X_4286)),bind(X_3274,$fot(X_4285))]]) ).
cnf(refute_0_74,plain,
is_a_theorem(implies(implies(X_150,implies(X_4285,X_4285)),implies(implies(X_4285,implies(not(X_4286),X_4286)),implies(X_4285,X_4286)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(implies(X_4285,X_4285)),implies(X_4285,X_4285)),implies(implies(X_4285,implies(not(X_4286),X_4286)),implies(X_4285,X_4286)))) )],[refute_0_73,refute_0_35]) ).
cnf(refute_0_75,plain,
is_a_theorem(implies(implies(X_4288,implies(X_4289,X_4289)),implies(implies(X_4289,implies(not(X_4290),X_4290)),implies(X_4289,X_4290)))),
inference(subst,[],[refute_0_74:[bind(X_150,$fot(X_4288)),bind(X_4285,$fot(X_4289)),bind(X_4286,$fot(X_4290))]]) ).
cnf(refute_0_76,plain,
( ~ is_a_theorem(implies(X_4288,implies(X_4289,X_4289)))
| is_a_theorem(implies(implies(X_4289,implies(not(X_4290),X_4290)),implies(X_4289,X_4290))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_4288,implies(X_4289,X_4289)),implies(implies(X_4289,implies(not(X_4290),X_4290)),implies(X_4289,X_4290)))) )],[refute_0_75,refute_0_16]) ).
cnf(refute_0_77,plain,
( ~ is_a_theorem(implies(implies(not(X_29),implies(X_985,X_985)),implies(X_985,X_985)))
| is_a_theorem(implies(X_29,implies(X_985,X_985))) ),
inference(subst,[],[refute_0_8:[bind(X_28,$fot(implies(X_985,X_985))),bind(X_30,$fot(implies(X_985,X_985)))]]) ).
cnf(refute_0_78,plain,
is_a_theorem(implies(implies(not(implies(X_979,X_979)),implies(X_979,X_979)),implies(X_979,X_979))),
inference(subst,[],[cn_2:[bind(X,$fot(implies(X_979,X_979)))]]) ).
cnf(refute_0_79,plain,
( ~ is_a_theorem(implies(implies(not(implies(X_979,X_979)),implies(X_979,X_979)),implies(X_979,X_979)))
| is_a_theorem(implies(implies(X_978,implies(X_979,X_979)),implies(X_979,X_979))) ),
inference(subst,[],[refute_0_34:[bind(X_148,$fot(implies(X_979,X_979))),bind(X_149,$fot(implies(X_979,X_979))),bind(X_150,$fot(X_978)),bind(X_151,$fot(X_979))]]) ).
cnf(refute_0_80,plain,
is_a_theorem(implies(implies(X_978,implies(X_979,X_979)),implies(X_979,X_979))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(implies(X_979,X_979)),implies(X_979,X_979)),implies(X_979,X_979))) )],[refute_0_78,refute_0_79]) ).
cnf(refute_0_81,plain,
is_a_theorem(implies(implies(not(X_29),implies(X_985,X_985)),implies(X_985,X_985))),
inference(subst,[],[refute_0_80:[bind(X_978,$fot(not(X_29))),bind(X_979,$fot(X_985))]]) ).
cnf(refute_0_82,plain,
is_a_theorem(implies(X_29,implies(X_985,X_985))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_29),implies(X_985,X_985)),implies(X_985,X_985))) )],[refute_0_81,refute_0_77]) ).
cnf(refute_0_83,plain,
is_a_theorem(implies(X_4288,implies(X_4289,X_4289))),
inference(subst,[],[refute_0_82:[bind(X_29,$fot(X_4288)),bind(X_985,$fot(X_4289))]]) ).
cnf(refute_0_84,plain,
is_a_theorem(implies(implies(X_4289,implies(not(X_4290),X_4290)),implies(X_4289,X_4290))),
inference(resolve,[$cnf( is_a_theorem(implies(X_4288,implies(X_4289,X_4289))) )],[refute_0_83,refute_0_76]) ).
cnf(refute_0_85,plain,
is_a_theorem(implies(implies(X_4544,implies(not(X_4290),X_4290)),implies(X_4544,X_4290))),
inference(subst,[],[refute_0_84:[bind(X_4289,$fot(X_4544))]]) ).
cnf(refute_0_86,plain,
( ~ is_a_theorem(implies(implies(X_44,X_45),X_42))
| ~ is_a_theorem(implies(implies(implies(X_44,X_45),X_42),implies(implies(implies(not(X_44),X_43),X_45),X_42)))
| is_a_theorem(implies(implies(implies(not(X_44),X_43),X_45),X_42)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_44,X_45),X_42))),bind(Y,$fot(implies(implies(implies(not(X_44),X_43),X_45),X_42)))]]) ).
cnf(refute_0_87,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_29),X_28),X_30),implies(X_29,X_30)))
| is_a_theorem(implies(implies(implies(X_29,X_30),Z),implies(implies(implies(not(X_29),X_28),X_30),Z))) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(implies(implies(not(X_29),X_28),X_30))),bind(Y,$fot(implies(X_29,X_30)))]]) ).
cnf(refute_0_88,plain,
is_a_theorem(implies(implies(implies(X_29,X_30),Z),implies(implies(implies(not(X_29),X_28),X_30),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_29),X_28),X_30),implies(X_29,X_30))) )],[refute_0_7,refute_0_87]) ).
cnf(refute_0_89,plain,
is_a_theorem(implies(implies(implies(X_44,X_45),X_42),implies(implies(implies(not(X_44),X_43),X_45),X_42))),
inference(subst,[],[refute_0_88:[bind(Z,$fot(X_42)),bind(X_28,$fot(X_43)),bind(X_29,$fot(X_44)),bind(X_30,$fot(X_45))]]) ).
cnf(refute_0_90,plain,
( ~ is_a_theorem(implies(implies(X_44,X_45),X_42))
| is_a_theorem(implies(implies(implies(not(X_44),X_43),X_45),X_42)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_44,X_45),X_42),implies(implies(implies(not(X_44),X_43),X_45),X_42))) )],[refute_0_89,refute_0_86]) ).
cnf(refute_0_91,plain,
( ~ is_a_theorem(implies(implies(X_4544,implies(not(X_4290),X_4290)),implies(X_4544,X_4290)))
| is_a_theorem(implies(implies(implies(not(X_4544),X_4543),implies(not(X_4290),X_4290)),implies(X_4544,X_4290))) ),
inference(subst,[],[refute_0_90:[bind(X_42,$fot(implies(X_4544,X_4290))),bind(X_43,$fot(X_4543)),bind(X_44,$fot(X_4544)),bind(X_45,$fot(implies(not(X_4290),X_4290)))]]) ).
cnf(refute_0_92,plain,
is_a_theorem(implies(implies(implies(not(X_4544),X_4543),implies(not(X_4290),X_4290)),implies(X_4544,X_4290))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_4544,implies(not(X_4290),X_4290)),implies(X_4544,X_4290))) )],[refute_0_85,refute_0_91]) ).
cnf(refute_0_93,plain,
is_a_theorem(implies(implies(implies(not(X_4567),X_4565),implies(not(X_4565),X_4565)),implies(X_4567,X_4565))),
inference(subst,[],[refute_0_92:[bind(X_4290,$fot(X_4565)),bind(X_4543,$fot(X_4565)),bind(X_4544,$fot(X_4567))]]) ).
cnf(refute_0_94,plain,
is_a_theorem(implies(implies(not(X_4565),not(X_4567)),implies(X_4567,X_4565))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_4567),X_4565),implies(not(X_4565),X_4565)),implies(X_4567,X_4565))) )],[refute_0_93,refute_0_15]) ).
cnf(refute_0_95,plain,
is_a_theorem(implies(implies(not(X_4572),not(X_4573)),implies(X_4573,X_4572))),
inference(subst,[],[refute_0_94:[bind(X_4565,$fot(X_4572)),bind(X_4567,$fot(X_4573))]]) ).
cnf(refute_0_96,plain,
is_a_theorem(implies(X_4572,implies(X_4573,X_4572))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_4572),not(X_4573)),implies(X_4573,X_4572))) )],[refute_0_95,refute_0_9]) ).
cnf(refute_0_97,plain,
is_a_theorem(implies(X_4574,implies(X_4575,X_4574))),
inference(subst,[],[refute_0_96:[bind(X_4572,$fot(X_4574)),bind(X_4573,$fot(X_4575))]]) ).
cnf(refute_0_98,plain,
is_a_theorem(implies(implies(implies(X_4575,X_4574),Z),implies(X_4574,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_4574,implies(X_4575,X_4574))) )],[refute_0_97,refute_0_2]) ).
cnf(refute_0_99,plain,
is_a_theorem(implies(implies(implies(a,b),c),implies(b,c))),
inference(subst,[],[refute_0_98:[bind(Z,$fot(c)),bind(X_4574,$fot(b)),bind(X_4575,$fot(a))]]) ).
cnf(refute_0_100,plain,
$false,
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(a,b),c),implies(b,c))) )],[refute_0_99,prove_cn_19]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL048-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : metis --show proof --show saturation %s
% 0.08/0.35 % Computer : n029.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 17:11:10 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 6.06/6.34 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.06/6.34
% 6.06/6.34 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 6.06/6.39
%------------------------------------------------------------------------------