%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : LCL080-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n006.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:48 PM UTC 2026
% Result : Unsatisfiable 278.24s 278.52s
% Output : CNFRefutation 278.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 5
% Syntax : Number of clauses : 156 ( 89 unt; 0 nHn; 40 RR)
% Number of literals : 238 ( 0 equ; 83 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 530 ( 109 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) ).
cnf(ic_2,axiom,
is_a_theorem(implies(X,implies(Y,X))) ).
cnf(ic_3,axiom,
is_a_theorem(implies(implies(implies(X,Y),X),X)) ).
cnf(ic_4,axiom,
is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) ).
cnf(prove_ic_JLukasiewicz,negated_conjecture,
~ is_a_theorem(implies(implies(implies(a,b),c),implies(implies(c,a),implies(e,a)))) ).
cnf(refute_0_0,plain,
( ~ is_a_theorem(implies(implies(implies(X_37,X_38),implies(X_36,X_38)),X_39))
| ~ is_a_theorem(implies(implies(implies(implies(X_37,X_38),implies(X_36,X_38)),X_39),implies(implies(X_36,X_37),X_39)))
| is_a_theorem(implies(implies(X_36,X_37),X_39)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(X_37,X_38),implies(X_36,X_38)),X_39))),bind(Y,$fot(implies(implies(X_36,X_37),X_39)))]]) ).
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)))) )],[ic_4,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_29),implies(implies(X,Y),X_29))) ),
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_29))]]) ).
cnf(refute_0_4,plain,
is_a_theorem(implies(implies(implies(implies(Y,Z),implies(X,Z)),X_29),implies(implies(X,Y),X_29))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )],[ic_4,refute_0_3]) ).
cnf(refute_0_5,plain,
is_a_theorem(implies(implies(implies(implies(X_37,X_38),implies(X_36,X_38)),X_39),implies(implies(X_36,X_37),X_39))),
inference(subst,[],[refute_0_4:[bind(X,$fot(X_36)),bind(Y,$fot(X_37)),bind(Z,$fot(X_38)),bind(X_29,$fot(X_39))]]) ).
cnf(refute_0_6,plain,
( ~ is_a_theorem(implies(implies(implies(X_37,X_38),implies(X_36,X_38)),X_39))
| is_a_theorem(implies(implies(X_36,X_37),X_39)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_37,X_38),implies(X_36,X_38)),X_39),implies(implies(X_36,X_37),X_39))) )],[refute_0_5,refute_0_0]) ).
cnf(refute_0_7,plain,
( ~ is_a_theorem(implies(implies(implies(X_37,X_9416),implies(implies(X_9416,X_9415),X_9416)),implies(implies(X_37,X_9416),implies(X_9413,X_9416))))
| is_a_theorem(implies(implies(implies(X_9416,X_9415),X_37),implies(implies(X_37,X_9416),implies(X_9413,X_9416)))) ),
inference(subst,[],[refute_0_6:[bind(X_36,$fot(implies(X_9416,X_9415))),bind(X_38,$fot(X_9416)),bind(X_39,$fot(implies(implies(X_37,X_9416),implies(X_9413,X_9416))))]]) ).
cnf(refute_0_8,plain,
( ~ is_a_theorem(implies(implies(X_125,implies(X_126,X_125)),X_124))
| ~ is_a_theorem(implies(implies(implies(X_125,implies(X_126,X_125)),X_124),X_124))
| is_a_theorem(X_124) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_125,implies(X_126,X_125)),X_124))),bind(Y,$fot(X_124))]]) ).
cnf(refute_0_9,plain,
is_a_theorem(implies(implies(implies(X_8,Y),X_8),X_8)),
inference(subst,[],[ic_3:[bind(X,$fot(X_8))]]) ).
cnf(refute_0_10,plain,
( ~ is_a_theorem(implies(implies(X_8,Y),X_8))
| ~ is_a_theorem(implies(implies(implies(X_8,Y),X_8),X_8))
| is_a_theorem(X_8) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_8,Y),X_8))),bind(Y,$fot(X_8))]]) ).
cnf(refute_0_11,plain,
( ~ is_a_theorem(implies(implies(X_8,Y),X_8))
| is_a_theorem(X_8) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_8,Y),X_8),X_8)) )],[refute_0_9,refute_0_10]) ).
cnf(refute_0_12,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(X_120,implies(X_121,X_120)),X_119),X_119),X_119),implies(implies(implies(X_120,implies(X_121,X_120)),X_119),X_119)))
| is_a_theorem(implies(implies(implies(X_120,implies(X_121,X_120)),X_119),X_119)) ),
inference(subst,[],[refute_0_11:[bind(Y,$fot(X_119)),bind(X_8,$fot(implies(implies(implies(X_120,implies(X_121,X_120)),X_119),X_119)))]]) ).
cnf(refute_0_13,plain,
( ~ is_a_theorem(implies(implies(implies(X_62,implies(X_63,X_62)),X_65),implies(X_64,X_65)))
| is_a_theorem(implies(implies(implies(X_64,X_65),Z),implies(implies(implies(X_62,implies(X_63,X_62)),X_65),Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(implies(implies(X_62,implies(X_63,X_62)),X_65))),bind(Y,$fot(implies(X_64,X_65)))]]) ).
cnf(refute_0_14,plain,
is_a_theorem(implies(X_7,implies(Y,X_7))),
inference(subst,[],[ic_2:[bind(X,$fot(X_7))]]) ).
cnf(refute_0_15,plain,
( ~ is_a_theorem(X_7)
| ~ is_a_theorem(implies(X_7,implies(Y,X_7)))
| is_a_theorem(implies(Y,X_7)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(X_7)),bind(Y,$fot(implies(Y,X_7)))]]) ).
cnf(refute_0_16,plain,
( ~ is_a_theorem(X_7)
| is_a_theorem(implies(Y,X_7)) ),
inference(resolve,[$cnf( is_a_theorem(implies(X_7,implies(Y,X_7))) )],[refute_0_14,refute_0_15]) ).
cnf(refute_0_17,plain,
( ~ is_a_theorem(implies(X,implies(Y,X)))
| is_a_theorem(implies(X_9,implies(X,implies(Y,X)))) ),
inference(subst,[],[refute_0_16:[bind(Y,$fot(X_9)),bind(X_7,$fot(implies(X,implies(Y,X))))]]) ).
cnf(refute_0_18,plain,
is_a_theorem(implies(X_9,implies(X,implies(Y,X)))),
inference(resolve,[$cnf( is_a_theorem(implies(X,implies(Y,X))) )],[ic_2,refute_0_17]) ).
cnf(refute_0_19,plain,
is_a_theorem(implies(X_27,implies(X,implies(Y,X)))),
inference(subst,[],[refute_0_18:[bind(X_9,$fot(X_27))]]) ).
cnf(refute_0_20,plain,
( ~ is_a_theorem(implies(X_27,implies(X,implies(Y,X))))
| is_a_theorem(implies(implies(implies(X,implies(Y,X)),X_29),implies(X_27,X_29))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(X_27)),bind(Y,$fot(implies(X,implies(Y,X)))),bind(Z,$fot(X_29))]]) ).
cnf(refute_0_21,plain,
is_a_theorem(implies(implies(implies(X,implies(Y,X)),X_29),implies(X_27,X_29))),
inference(resolve,[$cnf( is_a_theorem(implies(X_27,implies(X,implies(Y,X)))) )],[refute_0_19,refute_0_20]) ).
cnf(refute_0_22,plain,
is_a_theorem(implies(implies(implies(X_62,implies(X_63,X_62)),X_65),implies(X_64,X_65))),
inference(subst,[],[refute_0_21:[bind(X,$fot(X_62)),bind(Y,$fot(X_63)),bind(X_27,$fot(X_64)),bind(X_29,$fot(X_65))]]) ).
cnf(refute_0_23,plain,
is_a_theorem(implies(implies(implies(X_64,X_65),Z),implies(implies(implies(X_62,implies(X_63,X_62)),X_65),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_62,implies(X_63,X_62)),X_65),implies(X_64,X_65))) )],[refute_0_22,refute_0_13]) ).
cnf(refute_0_24,plain,
is_a_theorem(implies(implies(implies(implies(implies(X_120,implies(X_121,X_120)),X_119),X_119),X_119),implies(implies(implies(X_120,implies(X_121,X_120)),X_119),X_119))),
inference(subst,[],[refute_0_23:[bind(Z,$fot(X_119)),bind(X_62,$fot(X_120)),bind(X_63,$fot(X_121)),bind(X_64,$fot(implies(implies(X_120,implies(X_121,X_120)),X_119))),bind(X_65,$fot(X_119))]]) ).
cnf(refute_0_25,plain,
is_a_theorem(implies(implies(implies(X_120,implies(X_121,X_120)),X_119),X_119)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(X_120,implies(X_121,X_120)),X_119),X_119),X_119),implies(implies(implies(X_120,implies(X_121,X_120)),X_119),X_119))) )],[refute_0_24,refute_0_12]) ).
cnf(refute_0_26,plain,
is_a_theorem(implies(implies(implies(X_125,implies(X_126,X_125)),X_124),X_124)),
inference(subst,[],[refute_0_25:[bind(X_119,$fot(X_124)),bind(X_120,$fot(X_125)),bind(X_121,$fot(X_126))]]) ).
cnf(refute_0_27,plain,
( ~ is_a_theorem(implies(implies(X_125,implies(X_126,X_125)),X_124))
| is_a_theorem(X_124) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_125,implies(X_126,X_125)),X_124),X_124)) )],[refute_0_26,refute_0_8]) ).
cnf(refute_0_28,plain,
( ~ is_a_theorem(implies(implies(X_8367,implies(X_126,X_8367)),implies(implies(X_8365,implies(implies(X_8367,X_8366),X_8367)),implies(X_8365,implies(X_126,X_8367)))))
| is_a_theorem(implies(implies(X_8365,implies(implies(X_8367,X_8366),X_8367)),implies(X_8365,implies(X_126,X_8367)))) ),
inference(subst,[],[refute_0_27:[bind(X_124,$fot(implies(implies(X_8365,implies(implies(X_8367,X_8366),X_8367)),implies(X_8365,implies(X_126,X_8367))))),bind(X_125,$fot(X_8367))]]) ).
cnf(refute_0_29,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_3210,implies(X_3211,X_3210)),X_3208),X_3208),X_3209))
| ~ is_a_theorem(implies(implies(implies(implies(implies(X_3210,implies(X_3211,X_3210)),X_3208),X_3208),X_3209),X_3209))
| is_a_theorem(X_3209) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(implies(X_3210,implies(X_3211,X_3210)),X_3208),X_3208),X_3209))),bind(Y,$fot(X_3209))]]) ).
cnf(refute_0_30,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_187,X_188),X_187),X_187),X_186))
| ~ is_a_theorem(implies(implies(implies(implies(implies(X_187,X_188),X_187),X_187),X_186),X_186))
| is_a_theorem(X_186) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(implies(X_187,X_188),X_187),X_187),X_186))),bind(Y,$fot(X_186))]]) ).
cnf(refute_0_31,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(implies(implies(X_182,X_183),X_182),X_182),X_181),X_181),X_181),implies(implies(implies(implies(implies(X_182,X_183),X_182),X_182),X_181),X_181)))
| is_a_theorem(implies(implies(implies(implies(implies(X_182,X_183),X_182),X_182),X_181),X_181)) ),
inference(subst,[],[refute_0_11:[bind(Y,$fot(X_181)),bind(X_8,$fot(implies(implies(implies(implies(implies(X_182,X_183),X_182),X_182),X_181),X_181)))]]) ).
cnf(refute_0_32,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(X_71,X_72),X_71),X_71),X_74),implies(X_73,X_74)))
| is_a_theorem(implies(implies(implies(X_73,X_74),Z),implies(implies(implies(implies(implies(X_71,X_72),X_71),X_71),X_74),Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(implies(implies(implies(implies(X_71,X_72),X_71),X_71),X_74))),bind(Y,$fot(implies(X_73,X_74)))]]) ).
cnf(refute_0_33,plain,
( ~ is_a_theorem(implies(implies(implies(X,Y),X),X))
| is_a_theorem(implies(X_9,implies(implies(implies(X,Y),X),X))) ),
inference(subst,[],[refute_0_16:[bind(Y,$fot(X_9)),bind(X_7,$fot(implies(implies(implies(X,Y),X),X)))]]) ).
cnf(refute_0_34,plain,
is_a_theorem(implies(X_9,implies(implies(implies(X,Y),X),X))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X,Y),X),X)) )],[ic_3,refute_0_33]) ).
cnf(refute_0_35,plain,
is_a_theorem(implies(X_27,implies(implies(implies(X,Y),X),X))),
inference(subst,[],[refute_0_34:[bind(X_9,$fot(X_27))]]) ).
cnf(refute_0_36,plain,
( ~ is_a_theorem(implies(X_27,implies(implies(implies(X,Y),X),X)))
| is_a_theorem(implies(implies(implies(implies(implies(X,Y),X),X),X_29),implies(X_27,X_29))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(X_27)),bind(Y,$fot(implies(implies(implies(X,Y),X),X))),bind(Z,$fot(X_29))]]) ).
cnf(refute_0_37,plain,
is_a_theorem(implies(implies(implies(implies(implies(X,Y),X),X),X_29),implies(X_27,X_29))),
inference(resolve,[$cnf( is_a_theorem(implies(X_27,implies(implies(implies(X,Y),X),X))) )],[refute_0_35,refute_0_36]) ).
cnf(refute_0_38,plain,
is_a_theorem(implies(implies(implies(implies(implies(X_71,X_72),X_71),X_71),X_74),implies(X_73,X_74))),
inference(subst,[],[refute_0_37:[bind(X,$fot(X_71)),bind(Y,$fot(X_72)),bind(X_27,$fot(X_73)),bind(X_29,$fot(X_74))]]) ).
cnf(refute_0_39,plain,
is_a_theorem(implies(implies(implies(X_73,X_74),Z),implies(implies(implies(implies(implies(X_71,X_72),X_71),X_71),X_74),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(X_71,X_72),X_71),X_71),X_74),implies(X_73,X_74))) )],[refute_0_38,refute_0_32]) ).
cnf(refute_0_40,plain,
is_a_theorem(implies(implies(implies(implies(implies(implies(implies(X_182,X_183),X_182),X_182),X_181),X_181),X_181),implies(implies(implies(implies(implies(X_182,X_183),X_182),X_182),X_181),X_181))),
inference(subst,[],[refute_0_39:[bind(Z,$fot(X_181)),bind(X_71,$fot(X_182)),bind(X_72,$fot(X_183)),bind(X_73,$fot(implies(implies(implies(implies(X_182,X_183),X_182),X_182),X_181))),bind(X_74,$fot(X_181))]]) ).
cnf(refute_0_41,plain,
is_a_theorem(implies(implies(implies(implies(implies(X_182,X_183),X_182),X_182),X_181),X_181)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(implies(implies(X_182,X_183),X_182),X_182),X_181),X_181),X_181),implies(implies(implies(implies(implies(X_182,X_183),X_182),X_182),X_181),X_181))) )],[refute_0_40,refute_0_31]) ).
cnf(refute_0_42,plain,
is_a_theorem(implies(implies(implies(implies(implies(X_187,X_188),X_187),X_187),X_186),X_186)),
inference(subst,[],[refute_0_41:[bind(X_181,$fot(X_186)),bind(X_182,$fot(X_187)),bind(X_183,$fot(X_188))]]) ).
cnf(refute_0_43,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_187,X_188),X_187),X_187),X_186))
| is_a_theorem(X_186) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(X_187,X_188),X_187),X_187),X_186),X_186)) )],[refute_0_42,refute_0_30]) ).
cnf(refute_0_44,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_187,X_188),X_187),X_187),implies(implies(implies(implies(implies(X_3205,implies(X_3206,X_3205)),X_3203),X_3203),X_3204),X_3204)))
| is_a_theorem(implies(implies(implies(implies(implies(X_3205,implies(X_3206,X_3205)),X_3203),X_3203),X_3204),X_3204)) ),
inference(subst,[],[refute_0_43:[bind(X_186,$fot(implies(implies(implies(implies(implies(X_3205,implies(X_3206,X_3205)),X_3203),X_3203),X_3204),X_3204)))]]) ).
cnf(refute_0_45,plain,
( ~ is_a_theorem(implies(implies(X_300,X_299),X_298))
| ~ is_a_theorem(implies(implies(implies(X_300,X_299),X_298),implies(implies(implies(X_301,X_301),X_299),X_298)))
| is_a_theorem(implies(implies(implies(X_301,X_301),X_299),X_298)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_300,X_299),X_298))),bind(Y,$fot(implies(implies(implies(X_301,X_301),X_299),X_298)))]]) ).
cnf(refute_0_46,plain,
( ~ is_a_theorem(implies(implies(implies(X_56,X_56),X_54),implies(X_55,X_54)))
| is_a_theorem(implies(implies(implies(X_55,X_54),Z),implies(implies(implies(X_56,X_56),X_54),Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(implies(implies(X_56,X_56),X_54))),bind(Y,$fot(implies(X_55,X_54)))]]) ).
cnf(refute_0_47,plain,
( ~ is_a_theorem(implies(X_34,implies(X_35,X_35)))
| is_a_theorem(implies(implies(implies(X_35,X_35),Z),implies(X_34,Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(X_34)),bind(Y,$fot(implies(X_35,X_35)))]]) ).
cnf(refute_0_48,plain,
( ~ is_a_theorem(implies(X_33,X_33))
| is_a_theorem(implies(Y,implies(X_33,X_33))) ),
inference(subst,[],[refute_0_16:[bind(X_7,$fot(implies(X_33,X_33)))]]) ).
cnf(refute_0_49,plain,
( ~ is_a_theorem(implies(implies(implies(X_32,X_32),X_32),implies(X_32,X_32)))
| is_a_theorem(implies(X_32,X_32)) ),
inference(subst,[],[refute_0_11:[bind(Y,$fot(X_32)),bind(X_8,$fot(implies(X_32,X_32)))]]) ).
cnf(refute_0_50,plain,
is_a_theorem(implies(X_27,implies(Y,X_27))),
inference(subst,[],[ic_2:[bind(X,$fot(X_27))]]) ).
cnf(refute_0_51,plain,
( ~ is_a_theorem(implies(X_27,implies(Y,X_27)))
| is_a_theorem(implies(implies(implies(Y,X_27),X_29),implies(X_27,X_29))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(X_27)),bind(Y,$fot(implies(Y,X_27))),bind(Z,$fot(X_29))]]) ).
cnf(refute_0_52,plain,
is_a_theorem(implies(implies(implies(Y,X_27),X_29),implies(X_27,X_29))),
inference(resolve,[$cnf( is_a_theorem(implies(X_27,implies(Y,X_27))) )],[refute_0_50,refute_0_51]) ).
cnf(refute_0_53,plain,
is_a_theorem(implies(implies(implies(X_32,X_32),X_32),implies(X_32,X_32))),
inference(subst,[],[refute_0_52:[bind(Y,$fot(X_32)),bind(X_27,$fot(X_32)),bind(X_29,$fot(X_32))]]) ).
cnf(refute_0_54,plain,
is_a_theorem(implies(X_32,X_32)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_32,X_32),X_32),implies(X_32,X_32))) )],[refute_0_53,refute_0_49]) ).
cnf(refute_0_55,plain,
is_a_theorem(implies(X_33,X_33)),
inference(subst,[],[refute_0_54:[bind(X_32,$fot(X_33))]]) ).
cnf(refute_0_56,plain,
is_a_theorem(implies(Y,implies(X_33,X_33))),
inference(resolve,[$cnf( is_a_theorem(implies(X_33,X_33)) )],[refute_0_55,refute_0_48]) ).
cnf(refute_0_57,plain,
is_a_theorem(implies(X_34,implies(X_35,X_35))),
inference(subst,[],[refute_0_56:[bind(Y,$fot(X_34)),bind(X_33,$fot(X_35))]]) ).
cnf(refute_0_58,plain,
is_a_theorem(implies(implies(implies(X_35,X_35),Z),implies(X_34,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_34,implies(X_35,X_35))) )],[refute_0_57,refute_0_47]) ).
cnf(refute_0_59,plain,
is_a_theorem(implies(implies(implies(X_56,X_56),X_54),implies(X_55,X_54))),
inference(subst,[],[refute_0_58:[bind(Z,$fot(X_54)),bind(X_34,$fot(X_55)),bind(X_35,$fot(X_56))]]) ).
cnf(refute_0_60,plain,
is_a_theorem(implies(implies(implies(X_55,X_54),Z),implies(implies(implies(X_56,X_56),X_54),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_56,X_56),X_54),implies(X_55,X_54))) )],[refute_0_59,refute_0_46]) ).
cnf(refute_0_61,plain,
is_a_theorem(implies(implies(implies(X_300,X_299),X_298),implies(implies(implies(X_301,X_301),X_299),X_298))),
inference(subst,[],[refute_0_60:[bind(Z,$fot(X_298)),bind(X_54,$fot(X_299)),bind(X_55,$fot(X_300)),bind(X_56,$fot(X_301))]]) ).
cnf(refute_0_62,plain,
( ~ is_a_theorem(implies(implies(X_300,X_299),X_298))
| is_a_theorem(implies(implies(implies(X_301,X_301),X_299),X_298)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_300,X_299),X_298),implies(implies(implies(X_301,X_301),X_299),X_298))) )],[refute_0_61,refute_0_45]) ).
cnf(refute_0_63,plain,
( ~ is_a_theorem(implies(implies(implies(X_2040,X_2041),X_2040),implies(implies(implies(implies(X_2040,X_2038),X_2038),X_2039),X_2039)))
| is_a_theorem(implies(implies(implies(X_301,X_301),X_2040),implies(implies(implies(implies(X_2040,X_2038),X_2038),X_2039),X_2039))) ),
inference(subst,[],[refute_0_62:[bind(X_298,$fot(implies(implies(implies(implies(X_2040,X_2038),X_2038),X_2039),X_2039))),bind(X_299,$fot(X_2040)),bind(X_300,$fot(implies(X_2040,X_2041)))]]) ).
cnf(refute_0_64,plain,
( ~ is_a_theorem(implies(X_41,X_42))
| ~ is_a_theorem(implies(implies(X_41,X_42),implies(implies(implies(X_41,X_40),X_41),X_42)))
| is_a_theorem(implies(implies(implies(X_41,X_40),X_41),X_42)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X_41,X_42))),bind(Y,$fot(implies(implies(implies(X_41,X_40),X_41),X_42)))]]) ).
cnf(refute_0_65,plain,
is_a_theorem(implies(implies(implies(X_28,Y),X_28),X_28)),
inference(subst,[],[ic_3:[bind(X,$fot(X_28))]]) ).
cnf(refute_0_66,plain,
( ~ is_a_theorem(implies(implies(implies(X_28,Y),X_28),X_28))
| is_a_theorem(implies(implies(X_28,X_29),implies(implies(implies(X_28,Y),X_28),X_29))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(implies(implies(X_28,Y),X_28))),bind(Y,$fot(X_28)),bind(Z,$fot(X_29))]]) ).
cnf(refute_0_67,plain,
is_a_theorem(implies(implies(X_28,X_29),implies(implies(implies(X_28,Y),X_28),X_29))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_28,Y),X_28),X_28)) )],[refute_0_65,refute_0_66]) ).
cnf(refute_0_68,plain,
is_a_theorem(implies(implies(X_41,X_42),implies(implies(implies(X_41,X_40),X_41),X_42))),
inference(subst,[],[refute_0_67:[bind(Y,$fot(X_40)),bind(X_28,$fot(X_41)),bind(X_29,$fot(X_42))]]) ).
cnf(refute_0_69,plain,
( ~ is_a_theorem(implies(X_41,X_42))
| is_a_theorem(implies(implies(implies(X_41,X_40),X_41),X_42)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_41,X_42),implies(implies(implies(X_41,X_40),X_41),X_42))) )],[refute_0_68,refute_0_64]) ).
cnf(refute_0_70,plain,
( ~ is_a_theorem(implies(X_1886,implies(implies(implies(implies(X_1886,X_1884),X_1884),X_1885),X_1885)))
| is_a_theorem(implies(implies(implies(X_1886,X_40),X_1886),implies(implies(implies(implies(X_1886,X_1884),X_1884),X_1885),X_1885))) ),
inference(subst,[],[refute_0_69:[bind(X_41,$fot(X_1886)),bind(X_42,$fot(implies(implies(implies(implies(X_1886,X_1884),X_1884),X_1885),X_1885)))]]) ).
cnf(refute_0_71,plain,
( ~ is_a_theorem(implies(implies(implies(X_365,X_363),implies(X_364,X_363)),X_362))
| ~ is_a_theorem(implies(implies(implies(implies(X_365,X_363),implies(X_364,X_363)),X_362),implies(X_365,X_362)))
| is_a_theorem(implies(X_365,X_362)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(X_365,X_363),implies(X_364,X_363)),X_362))),bind(Y,$fot(implies(X_365,X_362)))]]) ).
cnf(refute_0_72,plain,
( ~ is_a_theorem(implies(X_148,implies(implies(X_148,X_146),implies(X_147,X_146))))
| is_a_theorem(implies(implies(implies(implies(X_148,X_146),implies(X_147,X_146)),Z),implies(X_148,Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(X_148)),bind(Y,$fot(implies(implies(X_148,X_146),implies(X_147,X_146))))]]) ).
cnf(refute_0_73,plain,
is_a_theorem(implies(implies(X_140,X_141),implies(implies(X_141,Z),implies(X_140,Z)))),
inference(subst,[],[ic_4:[bind(X,$fot(X_140)),bind(Y,$fot(X_141))]]) ).
cnf(refute_0_74,plain,
( ~ is_a_theorem(implies(implies(X_30,X_31),X_32))
| ~ is_a_theorem(implies(implies(implies(X_30,X_31),X_32),implies(X_31,X_32)))
| is_a_theorem(implies(X_31,X_32)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_30,X_31),X_32))),bind(Y,$fot(implies(X_31,X_32)))]]) ).
cnf(refute_0_75,plain,
is_a_theorem(implies(implies(implies(X_30,X_31),X_32),implies(X_31,X_32))),
inference(subst,[],[refute_0_52:[bind(Y,$fot(X_30)),bind(X_27,$fot(X_31)),bind(X_29,$fot(X_32))]]) ).
cnf(refute_0_76,plain,
( ~ is_a_theorem(implies(implies(X_30,X_31),X_32))
| is_a_theorem(implies(X_31,X_32)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_30,X_31),X_32),implies(X_31,X_32))) )],[refute_0_75,refute_0_74]) ).
cnf(refute_0_77,plain,
( ~ is_a_theorem(implies(implies(X_140,X_141),implies(implies(X_141,Z),implies(X_140,Z))))
| is_a_theorem(implies(X_141,implies(implies(X_141,Z),implies(X_140,Z)))) ),
inference(subst,[],[refute_0_76:[bind(X_30,$fot(X_140)),bind(X_31,$fot(X_141)),bind(X_32,$fot(implies(implies(X_141,Z),implies(X_140,Z))))]]) ).
cnf(refute_0_78,plain,
is_a_theorem(implies(X_141,implies(implies(X_141,Z),implies(X_140,Z)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_140,X_141),implies(implies(X_141,Z),implies(X_140,Z)))) )],[refute_0_73,refute_0_77]) ).
cnf(refute_0_79,plain,
is_a_theorem(implies(X_148,implies(implies(X_148,X_146),implies(X_147,X_146)))),
inference(subst,[],[refute_0_78:[bind(Z,$fot(X_146)),bind(X_140,$fot(X_147)),bind(X_141,$fot(X_148))]]) ).
cnf(refute_0_80,plain,
is_a_theorem(implies(implies(implies(implies(X_148,X_146),implies(X_147,X_146)),Z),implies(X_148,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_148,implies(implies(X_148,X_146),implies(X_147,X_146)))) )],[refute_0_79,refute_0_72]) ).
cnf(refute_0_81,plain,
is_a_theorem(implies(implies(implies(implies(X_365,X_363),implies(X_364,X_363)),X_362),implies(X_365,X_362))),
inference(subst,[],[refute_0_80:[bind(Z,$fot(X_362)),bind(X_146,$fot(X_363)),bind(X_147,$fot(X_364)),bind(X_148,$fot(X_365))]]) ).
cnf(refute_0_82,plain,
( ~ is_a_theorem(implies(implies(implies(X_365,X_363),implies(X_364,X_363)),X_362))
| is_a_theorem(implies(X_365,X_362)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_365,X_363),implies(X_364,X_363)),X_362),implies(X_365,X_362))) )],[refute_0_81,refute_0_71]) ).
cnf(refute_0_83,plain,
( ~ is_a_theorem(implies(implies(implies(X_365,X_1805),implies(implies(X_365,X_1805),X_1805)),implies(implies(implies(implies(X_365,X_1805),X_1805),X_1806),X_1806)))
| is_a_theorem(implies(X_365,implies(implies(implies(implies(X_365,X_1805),X_1805),X_1806),X_1806))) ),
inference(subst,[],[refute_0_82:[bind(X_362,$fot(implies(implies(implies(implies(X_365,X_1805),X_1805),X_1806),X_1806))),bind(X_363,$fot(X_1805)),bind(X_364,$fot(implies(X_365,X_1805)))]]) ).
cnf(refute_0_84,plain,
( ~ is_a_theorem(implies(X_744,implies(implies(X_744,X_745),X_745)))
| is_a_theorem(implies(implies(implies(X_744,X_40),X_744),implies(implies(X_744,X_745),X_745))) ),
inference(subst,[],[refute_0_69:[bind(X_41,$fot(X_744)),bind(X_42,$fot(implies(implies(X_744,X_745),X_745)))]]) ).
cnf(refute_0_85,plain,
( ~ is_a_theorem(implies(implies(implies(X_365,X_742),implies(implies(X_365,X_742),X_742)),implies(implies(X_365,X_742),X_742)))
| is_a_theorem(implies(X_365,implies(implies(X_365,X_742),X_742))) ),
inference(subst,[],[refute_0_82:[bind(X_362,$fot(implies(implies(X_365,X_742),X_742))),bind(X_363,$fot(X_742)),bind(X_364,$fot(implies(X_365,X_742)))]]) ).
cnf(refute_0_86,plain,
( ~ is_a_theorem(implies(implies(X_41,X_42),implies(implies(implies(X_41,X_40),X_41),X_42)))
| is_a_theorem(implies(implies(implies(implies(implies(X_41,X_40),X_41),X_42),Z),implies(implies(X_41,X_42),Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(implies(X_41,X_42))),bind(Y,$fot(implies(implies(implies(X_41,X_40),X_41),X_42)))]]) ).
cnf(refute_0_87,plain,
is_a_theorem(implies(implies(implies(implies(implies(X_41,X_40),X_41),X_42),Z),implies(implies(X_41,X_42),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_41,X_42),implies(implies(implies(X_41,X_40),X_41),X_42))) )],[refute_0_68,refute_0_86]) ).
cnf(refute_0_88,plain,
is_a_theorem(implies(implies(implies(implies(implies(X_741,X_40),X_741),implies(X_741,X_40)),implies(X_741,X_40)),implies(implies(X_741,implies(X_741,X_40)),implies(X_741,X_40)))),
inference(subst,[],[refute_0_87:[bind(Z,$fot(implies(X_741,X_40))),bind(X_41,$fot(X_741)),bind(X_42,$fot(implies(X_741,X_40)))]]) ).
cnf(refute_0_89,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(X_741,X_40),X_741),implies(X_741,X_40)),implies(X_741,X_40)),implies(implies(X_741,implies(X_741,X_40)),implies(X_741,X_40))))
| is_a_theorem(implies(implies(X_741,implies(X_741,X_40)),implies(X_741,X_40))) ),
inference(subst,[],[refute_0_43:[bind(X_186,$fot(implies(implies(X_741,implies(X_741,X_40)),implies(X_741,X_40)))),bind(X_187,$fot(implies(X_741,X_40))),bind(X_188,$fot(X_741))]]) ).
cnf(refute_0_90,plain,
is_a_theorem(implies(implies(X_741,implies(X_741,X_40)),implies(X_741,X_40))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(X_741,X_40),X_741),implies(X_741,X_40)),implies(X_741,X_40)),implies(implies(X_741,implies(X_741,X_40)),implies(X_741,X_40)))) )],[refute_0_88,refute_0_89]) ).
cnf(refute_0_91,plain,
is_a_theorem(implies(implies(implies(X_365,X_742),implies(implies(X_365,X_742),X_742)),implies(implies(X_365,X_742),X_742))),
inference(subst,[],[refute_0_90:[bind(X_40,$fot(X_742)),bind(X_741,$fot(implies(X_365,X_742)))]]) ).
cnf(refute_0_92,plain,
is_a_theorem(implies(X_365,implies(implies(X_365,X_742),X_742))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_365,X_742),implies(implies(X_365,X_742),X_742)),implies(implies(X_365,X_742),X_742))) )],[refute_0_91,refute_0_85]) ).
cnf(refute_0_93,plain,
is_a_theorem(implies(X_744,implies(implies(X_744,X_745),X_745))),
inference(subst,[],[refute_0_92:[bind(X_365,$fot(X_744)),bind(X_742,$fot(X_745))]]) ).
cnf(refute_0_94,plain,
is_a_theorem(implies(implies(implies(X_744,X_40),X_744),implies(implies(X_744,X_745),X_745))),
inference(resolve,[$cnf( is_a_theorem(implies(X_744,implies(implies(X_744,X_745),X_745))) )],[refute_0_93,refute_0_84]) ).
cnf(refute_0_95,plain,
is_a_theorem(implies(implies(implies(implies(X_1751,X_1753),X_1753),implies(X_1751,X_1753)),implies(implies(implies(X_1751,X_1753),X_745),X_745))),
inference(subst,[],[refute_0_94:[bind(X_40,$fot(X_1753)),bind(X_744,$fot(implies(X_1751,X_1753)))]]) ).
cnf(refute_0_96,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_1751,X_1753),X_1753),implies(X_1751,X_1753)),implies(implies(implies(X_1751,X_1753),X_745),X_745)))
| is_a_theorem(implies(implies(X_1751,implies(X_1751,X_1753)),implies(implies(implies(X_1751,X_1753),X_745),X_745))) ),
inference(subst,[],[refute_0_6:[bind(X_36,$fot(X_1751)),bind(X_37,$fot(implies(X_1751,X_1753))),bind(X_38,$fot(X_1753)),bind(X_39,$fot(implies(implies(implies(X_1751,X_1753),X_745),X_745)))]]) ).
cnf(refute_0_97,plain,
is_a_theorem(implies(implies(X_1751,implies(X_1751,X_1753)),implies(implies(implies(X_1751,X_1753),X_745),X_745))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_1751,X_1753),X_1753),implies(X_1751,X_1753)),implies(implies(implies(X_1751,X_1753),X_745),X_745))) )],[refute_0_95,refute_0_96]) ).
cnf(refute_0_98,plain,
is_a_theorem(implies(implies(implies(X_365,X_1805),implies(implies(X_365,X_1805),X_1805)),implies(implies(implies(implies(X_365,X_1805),X_1805),X_1806),X_1806))),
inference(subst,[],[refute_0_97:[bind(X_1751,$fot(implies(X_365,X_1805))),bind(X_1753,$fot(X_1805)),bind(X_745,$fot(X_1806))]]) ).
cnf(refute_0_99,plain,
is_a_theorem(implies(X_365,implies(implies(implies(implies(X_365,X_1805),X_1805),X_1806),X_1806))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_365,X_1805),implies(implies(X_365,X_1805),X_1805)),implies(implies(implies(implies(X_365,X_1805),X_1805),X_1806),X_1806))) )],[refute_0_98,refute_0_83]) ).
cnf(refute_0_100,plain,
is_a_theorem(implies(X_1886,implies(implies(implies(implies(X_1886,X_1884),X_1884),X_1885),X_1885))),
inference(subst,[],[refute_0_99:[bind(X_1805,$fot(X_1884)),bind(X_1806,$fot(X_1885)),bind(X_365,$fot(X_1886))]]) ).
cnf(refute_0_101,plain,
is_a_theorem(implies(implies(implies(X_1886,X_40),X_1886),implies(implies(implies(implies(X_1886,X_1884),X_1884),X_1885),X_1885))),
inference(resolve,[$cnf( is_a_theorem(implies(X_1886,implies(implies(implies(implies(X_1886,X_1884),X_1884),X_1885),X_1885))) )],[refute_0_100,refute_0_70]) ).
cnf(refute_0_102,plain,
is_a_theorem(implies(implies(implies(X_2040,X_2041),X_2040),implies(implies(implies(implies(X_2040,X_2038),X_2038),X_2039),X_2039))),
inference(subst,[],[refute_0_101:[bind(X_1884,$fot(X_2038)),bind(X_1885,$fot(X_2039)),bind(X_1886,$fot(X_2040)),bind(X_40,$fot(X_2041))]]) ).
cnf(refute_0_103,plain,
is_a_theorem(implies(implies(implies(X_301,X_301),X_2040),implies(implies(implies(implies(X_2040,X_2038),X_2038),X_2039),X_2039))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_2040,X_2041),X_2040),implies(implies(implies(implies(X_2040,X_2038),X_2038),X_2039),X_2039))) )],[refute_0_102,refute_0_63]) ).
cnf(refute_0_104,plain,
is_a_theorem(implies(implies(implies(X_301,X_301),implies(X_3107,implies(X_3108,X_3107))),implies(implies(implies(implies(implies(X_3107,implies(X_3108,X_3107)),X_2038),X_2038),X_2039),X_2039))),
inference(subst,[],[refute_0_103:[bind(X_2040,$fot(implies(X_3107,implies(X_3108,X_3107))))]]) ).
cnf(refute_0_105,plain,
( ~ is_a_theorem(implies(implies(X_83,implies(X_81,implies(X_82,X_81))),X_85))
| ~ is_a_theorem(implies(implies(implies(X_83,implies(X_81,implies(X_82,X_81))),X_85),implies(X_84,X_85)))
| is_a_theorem(implies(X_84,X_85)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_83,implies(X_81,implies(X_82,X_81))),X_85))),bind(Y,$fot(implies(X_84,X_85)))]]) ).
cnf(refute_0_106,plain,
( ~ is_a_theorem(implies(X_13,implies(X_11,implies(X_12,X_11))))
| is_a_theorem(implies(Y,implies(X_13,implies(X_11,implies(X_12,X_11))))) ),
inference(subst,[],[refute_0_16:[bind(X_7,$fot(implies(X_13,implies(X_11,implies(X_12,X_11)))))]]) ).
cnf(refute_0_107,plain,
is_a_theorem(implies(X_13,implies(X_11,implies(X_12,X_11)))),
inference(subst,[],[refute_0_18:[bind(X,$fot(X_11)),bind(Y,$fot(X_12)),bind(X_9,$fot(X_13))]]) ).
cnf(refute_0_108,plain,
is_a_theorem(implies(Y,implies(X_13,implies(X_11,implies(X_12,X_11))))),
inference(resolve,[$cnf( is_a_theorem(implies(X_13,implies(X_11,implies(X_12,X_11)))) )],[refute_0_107,refute_0_106]) ).
cnf(refute_0_109,plain,
is_a_theorem(implies(X_27,implies(X_13,implies(X_11,implies(X_12,X_11))))),
inference(subst,[],[refute_0_108:[bind(Y,$fot(X_27))]]) ).
cnf(refute_0_110,plain,
( ~ is_a_theorem(implies(X_27,implies(X_13,implies(X_11,implies(X_12,X_11)))))
| is_a_theorem(implies(implies(implies(X_13,implies(X_11,implies(X_12,X_11))),X_29),implies(X_27,X_29))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(X_27)),bind(Y,$fot(implies(X_13,implies(X_11,implies(X_12,X_11))))),bind(Z,$fot(X_29))]]) ).
cnf(refute_0_111,plain,
is_a_theorem(implies(implies(implies(X_13,implies(X_11,implies(X_12,X_11))),X_29),implies(X_27,X_29))),
inference(resolve,[$cnf( is_a_theorem(implies(X_27,implies(X_13,implies(X_11,implies(X_12,X_11))))) )],[refute_0_109,refute_0_110]) ).
cnf(refute_0_112,plain,
is_a_theorem(implies(implies(implies(X_83,implies(X_81,implies(X_82,X_81))),X_85),implies(X_84,X_85))),
inference(subst,[],[refute_0_111:[bind(X_11,$fot(X_81)),bind(X_12,$fot(X_82)),bind(X_13,$fot(X_83)),bind(X_27,$fot(X_84)),bind(X_29,$fot(X_85))]]) ).
cnf(refute_0_113,plain,
( ~ is_a_theorem(implies(implies(X_83,implies(X_81,implies(X_82,X_81))),X_85))
| is_a_theorem(implies(X_84,X_85)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_83,implies(X_81,implies(X_82,X_81))),X_85),implies(X_84,X_85))) )],[refute_0_112,refute_0_105]) ).
cnf(refute_0_114,plain,
( ~ is_a_theorem(implies(implies(implies(X_301,X_301),implies(X_3107,implies(X_3108,X_3107))),implies(implies(implies(implies(implies(X_3107,implies(X_3108,X_3107)),X_2038),X_2038),X_2039),X_2039)))
| is_a_theorem(implies(X_3110,implies(implies(implies(implies(implies(X_3107,implies(X_3108,X_3107)),X_2038),X_2038),X_2039),X_2039))) ),
inference(subst,[],[refute_0_113:[bind(X_81,$fot(X_3107)),bind(X_82,$fot(X_3108)),bind(X_83,$fot(implies(X_301,X_301))),bind(X_84,$fot(X_3110)),bind(X_85,$fot(implies(implies(implies(implies(implies(X_3107,implies(X_3108,X_3107)),X_2038),X_2038),X_2039),X_2039)))]]) ).
cnf(refute_0_115,plain,
is_a_theorem(implies(X_3110,implies(implies(implies(implies(implies(X_3107,implies(X_3108,X_3107)),X_2038),X_2038),X_2039),X_2039))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_301,X_301),implies(X_3107,implies(X_3108,X_3107))),implies(implies(implies(implies(implies(X_3107,implies(X_3108,X_3107)),X_2038),X_2038),X_2039),X_2039))) )],[refute_0_104,refute_0_114]) ).
cnf(refute_0_116,plain,
is_a_theorem(implies(implies(implies(implies(X_187,X_188),X_187),X_187),implies(implies(implies(implies(implies(X_3205,implies(X_3206,X_3205)),X_3203),X_3203),X_3204),X_3204))),
inference(subst,[],[refute_0_115:[bind(X_2038,$fot(X_3203)),bind(X_2039,$fot(X_3204)),bind(X_3107,$fot(X_3205)),bind(X_3108,$fot(X_3206)),bind(X_3110,$fot(implies(implies(implies(X_187,X_188),X_187),X_187)))]]) ).
cnf(refute_0_117,plain,
is_a_theorem(implies(implies(implies(implies(implies(X_3205,implies(X_3206,X_3205)),X_3203),X_3203),X_3204),X_3204)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_187,X_188),X_187),X_187),implies(implies(implies(implies(implies(X_3205,implies(X_3206,X_3205)),X_3203),X_3203),X_3204),X_3204))) )],[refute_0_116,refute_0_44]) ).
cnf(refute_0_118,plain,
is_a_theorem(implies(implies(implies(implies(implies(X_3210,implies(X_3211,X_3210)),X_3208),X_3208),X_3209),X_3209)),
inference(subst,[],[refute_0_117:[bind(X_3203,$fot(X_3208)),bind(X_3204,$fot(X_3209)),bind(X_3205,$fot(X_3210)),bind(X_3206,$fot(X_3211))]]) ).
cnf(refute_0_119,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_3210,implies(X_3211,X_3210)),X_3208),X_3208),X_3209))
| is_a_theorem(X_3209) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(X_3210,implies(X_3211,X_3210)),X_3208),X_3208),X_3209),X_3209)) )],[refute_0_118,refute_0_29]) ).
cnf(refute_0_120,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_3210,implies(X_3211,X_3210)),X_3208),X_3208),implies(implies(X_4855,X_4856),implies(implies(X_4854,X_4855),implies(X_4854,X_4856)))))
| is_a_theorem(implies(implies(X_4855,X_4856),implies(implies(X_4854,X_4855),implies(X_4854,X_4856)))) ),
inference(subst,[],[refute_0_119:[bind(X_3209,$fot(implies(implies(X_4855,X_4856),implies(implies(X_4854,X_4855),implies(X_4854,X_4856)))))]]) ).
cnf(refute_0_121,plain,
( ~ is_a_theorem(implies(X_744,implies(implies(X_744,X_745),X_745)))
| is_a_theorem(implies(implies(implies(implies(X_744,X_745),X_745),Z),implies(X_744,Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(X_744)),bind(Y,$fot(implies(implies(X_744,X_745),X_745)))]]) ).
cnf(refute_0_122,plain,
is_a_theorem(implies(implies(implies(implies(X_744,X_745),X_745),Z),implies(X_744,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_744,implies(implies(X_744,X_745),X_745))) )],[refute_0_93,refute_0_121]) ).
cnf(refute_0_123,plain,
is_a_theorem(implies(implies(implies(implies(X_744,X_1753),X_1753),implies(X_1751,X_1753)),implies(X_744,implies(X_1751,X_1753)))),
inference(subst,[],[refute_0_122:[bind(Z,$fot(implies(X_1751,X_1753))),bind(X_745,$fot(X_1753))]]) ).
cnf(refute_0_124,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_744,X_1753),X_1753),implies(X_1751,X_1753)),implies(X_744,implies(X_1751,X_1753))))
| is_a_theorem(implies(implies(X_1751,implies(X_744,X_1753)),implies(X_744,implies(X_1751,X_1753)))) ),
inference(subst,[],[refute_0_6:[bind(X_36,$fot(X_1751)),bind(X_37,$fot(implies(X_744,X_1753))),bind(X_38,$fot(X_1753)),bind(X_39,$fot(implies(X_744,implies(X_1751,X_1753))))]]) ).
cnf(refute_0_125,plain,
is_a_theorem(implies(implies(X_1751,implies(X_744,X_1753)),implies(X_744,implies(X_1751,X_1753)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_744,X_1753),X_1753),implies(X_1751,X_1753)),implies(X_744,implies(X_1751,X_1753)))) )],[refute_0_123,refute_0_124]) ).
cnf(refute_0_126,plain,
is_a_theorem(implies(implies(implies(X_4805,X_4806),implies(implies(X_4806,X_4807),implies(X_4805,X_4807))),implies(implies(X_4806,X_4807),implies(implies(X_4805,X_4806),implies(X_4805,X_4807))))),
inference(subst,[],[refute_0_125:[bind(X_1751,$fot(implies(X_4805,X_4806))),bind(X_1753,$fot(implies(X_4805,X_4807))),bind(X_744,$fot(implies(X_4806,X_4807)))]]) ).
cnf(refute_0_127,plain,
( ~ is_a_theorem(implies(implies(implies(X_91,X_92),implies(implies(X_92,X_93),implies(X_91,X_93))),X_90))
| ~ is_a_theorem(implies(implies(implies(implies(X_91,X_92),implies(implies(X_92,X_93),implies(X_91,X_93))),X_90),implies(X_94,X_90)))
| is_a_theorem(implies(X_94,X_90)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(X_91,X_92),implies(implies(X_92,X_93),implies(X_91,X_93))),X_90))),bind(Y,$fot(implies(X_94,X_90)))]]) ).
cnf(refute_0_128,plain,
( ~ is_a_theorem(implies(X_53,implies(implies(X_50,X_51),implies(implies(X_51,X_52),implies(X_50,X_52)))))
| is_a_theorem(implies(implies(implies(implies(X_50,X_51),implies(implies(X_51,X_52),implies(X_50,X_52))),Z),implies(X_53,Z))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(X_53)),bind(Y,$fot(implies(implies(X_50,X_51),implies(implies(X_51,X_52),implies(X_50,X_52)))))]]) ).
cnf(refute_0_129,plain,
( ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))))
| is_a_theorem(implies(X_9,implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))))) ),
inference(subst,[],[refute_0_16:[bind(Y,$fot(X_9)),bind(X_7,$fot(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))))]]) ).
cnf(refute_0_130,plain,
is_a_theorem(implies(X_9,implies(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)))) )],[ic_4,refute_0_129]) ).
cnf(refute_0_131,plain,
is_a_theorem(implies(X_53,implies(implies(X_50,X_51),implies(implies(X_51,X_52),implies(X_50,X_52))))),
inference(subst,[],[refute_0_130:[bind(X,$fot(X_50)),bind(Y,$fot(X_51)),bind(Z,$fot(X_52)),bind(X_9,$fot(X_53))]]) ).
cnf(refute_0_132,plain,
is_a_theorem(implies(implies(implies(implies(X_50,X_51),implies(implies(X_51,X_52),implies(X_50,X_52))),Z),implies(X_53,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_53,implies(implies(X_50,X_51),implies(implies(X_51,X_52),implies(X_50,X_52))))) )],[refute_0_131,refute_0_128]) ).
cnf(refute_0_133,plain,
is_a_theorem(implies(implies(implies(implies(X_91,X_92),implies(implies(X_92,X_93),implies(X_91,X_93))),X_90),implies(X_94,X_90))),
inference(subst,[],[refute_0_132:[bind(Z,$fot(X_90)),bind(X_50,$fot(X_91)),bind(X_51,$fot(X_92)),bind(X_52,$fot(X_93)),bind(X_53,$fot(X_94))]]) ).
cnf(refute_0_134,plain,
( ~ is_a_theorem(implies(implies(implies(X_91,X_92),implies(implies(X_92,X_93),implies(X_91,X_93))),X_90))
| is_a_theorem(implies(X_94,X_90)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_91,X_92),implies(implies(X_92,X_93),implies(X_91,X_93))),X_90),implies(X_94,X_90))) )],[refute_0_133,refute_0_127]) ).
cnf(refute_0_135,plain,
( ~ is_a_theorem(implies(implies(implies(X_4805,X_4806),implies(implies(X_4806,X_4807),implies(X_4805,X_4807))),implies(implies(X_4806,X_4807),implies(implies(X_4805,X_4806),implies(X_4805,X_4807)))))
| is_a_theorem(implies(X_4808,implies(implies(X_4806,X_4807),implies(implies(X_4805,X_4806),implies(X_4805,X_4807))))) ),
inference(subst,[],[refute_0_134:[bind(X_90,$fot(implies(implies(X_4806,X_4807),implies(implies(X_4805,X_4806),implies(X_4805,X_4807))))),bind(X_91,$fot(X_4805)),bind(X_92,$fot(X_4806)),bind(X_93,$fot(X_4807)),bind(X_94,$fot(X_4808))]]) ).
cnf(refute_0_136,plain,
is_a_theorem(implies(X_4808,implies(implies(X_4806,X_4807),implies(implies(X_4805,X_4806),implies(X_4805,X_4807))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_4805,X_4806),implies(implies(X_4806,X_4807),implies(X_4805,X_4807))),implies(implies(X_4806,X_4807),implies(implies(X_4805,X_4806),implies(X_4805,X_4807))))) )],[refute_0_126,refute_0_135]) ).
cnf(refute_0_137,plain,
is_a_theorem(implies(implies(implies(implies(X_3210,implies(X_3211,X_3210)),X_3208),X_3208),implies(implies(X_4855,X_4856),implies(implies(X_4854,X_4855),implies(X_4854,X_4856))))),
inference(subst,[],[refute_0_136:[bind(X_4805,$fot(X_4854)),bind(X_4806,$fot(X_4855)),bind(X_4807,$fot(X_4856)),bind(X_4808,$fot(implies(implies(implies(X_3210,implies(X_3211,X_3210)),X_3208),X_3208)))]]) ).
cnf(refute_0_138,plain,
is_a_theorem(implies(implies(X_4855,X_4856),implies(implies(X_4854,X_4855),implies(X_4854,X_4856)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_3210,implies(X_3211,X_3210)),X_3208),X_3208),implies(implies(X_4855,X_4856),implies(implies(X_4854,X_4855),implies(X_4854,X_4856))))) )],[refute_0_137,refute_0_120]) ).
cnf(refute_0_139,plain,
is_a_theorem(implies(implies(implies(implies(X_7897,X_7896),X_7897),X_7898),implies(implies(X_4854,implies(implies(X_7897,X_7896),X_7897)),implies(X_4854,X_7898)))),
inference(subst,[],[refute_0_138:[bind(X_4855,$fot(implies(implies(X_7897,X_7896),X_7897))),bind(X_4856,$fot(X_7898))]]) ).
cnf(refute_0_140,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_179,X_178),X_179),X_180),X_177))
| ~ is_a_theorem(implies(implies(implies(implies(implies(X_179,X_178),X_179),X_180),X_177),implies(implies(X_179,X_180),X_177)))
| is_a_theorem(implies(implies(X_179,X_180),X_177)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(implies(X_179,X_178),X_179),X_180),X_177))),bind(Y,$fot(implies(implies(X_179,X_180),X_177)))]]) ).
cnf(refute_0_141,plain,
is_a_theorem(implies(implies(implies(implies(implies(X_179,X_178),X_179),X_180),X_177),implies(implies(X_179,X_180),X_177))),
inference(subst,[],[refute_0_87:[bind(Z,$fot(X_177)),bind(X_40,$fot(X_178)),bind(X_41,$fot(X_179)),bind(X_42,$fot(X_180))]]) ).
cnf(refute_0_142,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_179,X_178),X_179),X_180),X_177))
| is_a_theorem(implies(implies(X_179,X_180),X_177)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(X_179,X_178),X_179),X_180),X_177),implies(implies(X_179,X_180),X_177))) )],[refute_0_141,refute_0_140]) ).
cnf(refute_0_143,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_7897,X_7896),X_7897),X_7898),implies(implies(X_4854,implies(implies(X_7897,X_7896),X_7897)),implies(X_4854,X_7898))))
| is_a_theorem(implies(implies(X_7897,X_7898),implies(implies(X_4854,implies(implies(X_7897,X_7896),X_7897)),implies(X_4854,X_7898)))) ),
inference(subst,[],[refute_0_142:[bind(X_177,$fot(implies(implies(X_4854,implies(implies(X_7897,X_7896),X_7897)),implies(X_4854,X_7898)))),bind(X_178,$fot(X_7896)),bind(X_179,$fot(X_7897)),bind(X_180,$fot(X_7898))]]) ).
cnf(refute_0_144,plain,
is_a_theorem(implies(implies(X_7897,X_7898),implies(implies(X_4854,implies(implies(X_7897,X_7896),X_7897)),implies(X_4854,X_7898)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_7897,X_7896),X_7897),X_7898),implies(implies(X_4854,implies(implies(X_7897,X_7896),X_7897)),implies(X_4854,X_7898)))) )],[refute_0_139,refute_0_143]) ).
cnf(refute_0_145,plain,
is_a_theorem(implies(implies(X_8367,implies(X_126,X_8367)),implies(implies(X_8365,implies(implies(X_8367,X_8366),X_8367)),implies(X_8365,implies(X_126,X_8367))))),
inference(subst,[],[refute_0_144:[bind(X_4854,$fot(X_8365)),bind(X_7896,$fot(X_8366)),bind(X_7897,$fot(X_8367)),bind(X_7898,$fot(implies(X_126,X_8367)))]]) ).
cnf(refute_0_146,plain,
is_a_theorem(implies(implies(X_8365,implies(implies(X_8367,X_8366),X_8367)),implies(X_8365,implies(X_126,X_8367)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_8367,implies(X_126,X_8367)),implies(implies(X_8365,implies(implies(X_8367,X_8366),X_8367)),implies(X_8365,implies(X_126,X_8367))))) )],[refute_0_145,refute_0_28]) ).
cnf(refute_0_147,plain,
is_a_theorem(implies(implies(implies(X_37,X_9416),implies(implies(X_9416,X_9415),X_9416)),implies(implies(X_37,X_9416),implies(X_9413,X_9416)))),
inference(subst,[],[refute_0_146:[bind(X_126,$fot(X_9413)),bind(X_8365,$fot(implies(X_37,X_9416))),bind(X_8366,$fot(X_9415)),bind(X_8367,$fot(X_9416))]]) ).
cnf(refute_0_148,plain,
is_a_theorem(implies(implies(implies(X_9416,X_9415),X_37),implies(implies(X_37,X_9416),implies(X_9413,X_9416)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_37,X_9416),implies(implies(X_9416,X_9415),X_9416)),implies(implies(X_37,X_9416),implies(X_9413,X_9416)))) )],[refute_0_147,refute_0_7]) ).
cnf(refute_0_149,plain,
is_a_theorem(implies(implies(implies(a,b),c),implies(implies(c,a),implies(e,a)))),
inference(subst,[],[refute_0_148:[bind(X_37,$fot(c)),bind(X_9413,$fot(e)),bind(X_9415,$fot(b)),bind(X_9416,$fot(a))]]) ).
cnf(refute_0_150,plain,
$false,
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(a,b),c),implies(implies(c,a),implies(e,a)))) )],[refute_0_149,prove_ic_JLukasiewicz]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL080-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : metis --show proof --show saturation %s
% 0.08/0.34 % Computer : n006.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Sat Sep 5 15:17:31 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 278.24/278.52 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 278.24/278.52
% 278.24/278.52 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 278.24/278.55
%------------------------------------------------------------------------------