%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : LCL083-2 : TPTP v9.3.1. Bugfixed v1.2.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 0.23s 0.53s
% Output : CNFRefutation 0.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 4
% Syntax : Number of clauses : 103 ( 57 unt; 0 nHn; 20 RR)
% Number of literals : 161 ( 0 equ; 59 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 3 ( 3 usr; 2 con; 0-2 aty)
% Number of variables : 383 ( 143 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) ).
cnf(ic_JLukasiewicz,axiom,
is_a_theorem(implies(implies(implies(X,Y),Z),implies(implies(Z,X),implies(U,X)))) ).
cnf(ic_1,axiom,
is_a_theorem(implies(X,X)) ).
cnf(prove_ic_3,negated_conjecture,
~ is_a_theorem(implies(implies(implies(a,b),a),a)) ).
cnf(refute_0_0,plain,
( ~ is_a_theorem(implies(implies(X_264,X_264),X_263))
| ~ is_a_theorem(implies(implies(implies(X_264,X_264),X_263),X_263))
| is_a_theorem(X_263) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_264,X_264),X_263))),bind(Y,$fot(X_263))]]) ).
cnf(refute_0_1,plain,
( ~ is_a_theorem(implies(implies(X,Y),Z))
| ~ is_a_theorem(implies(implies(implies(X,Y),Z),implies(implies(Z,X),implies(U,X))))
| is_a_theorem(implies(implies(Z,X),implies(U,X))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X,Y),Z))),bind(Y,$fot(implies(implies(Z,X),implies(U,X))))]]) ).
cnf(refute_0_2,plain,
( ~ is_a_theorem(implies(implies(X,Y),Z))
| is_a_theorem(implies(implies(Z,X),implies(U,X))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X,Y),Z),implies(implies(Z,X),implies(U,X)))) )],[ic_JLukasiewicz,refute_0_1]) ).
cnf(refute_0_3,plain,
( ~ is_a_theorem(implies(implies(X,Y),implies(implies(implies(implies(X_192,X_193),X_195),X_193),implies(X_192,X_193))))
| is_a_theorem(implies(implies(implies(implies(implies(implies(X_192,X_193),X_195),X_193),implies(X_192,X_193)),X),implies(U,X))) ),
inference(subst,[],[refute_0_2:[bind(Z,$fot(implies(implies(implies(implies(X_192,X_193),X_195),X_193),implies(X_192,X_193))))]]) ).
cnf(refute_0_4,plain,
is_a_theorem(implies(implies(implies(X,Y),implies(implies(U,X),X_191)),implies(implies(implies(implies(U,X),X_191),X),implies(U,X)))),
inference(subst,[],[ic_JLukasiewicz:[bind(Z,$fot(implies(implies(U,X),X_191)))]]) ).
cnf(refute_0_5,plain,
( ~ is_a_theorem(implies(implies(X_53,implies(X_55,X_56)),implies(X_54,X_55)))
| ~ is_a_theorem(implies(implies(implies(X_53,implies(X_55,X_56)),implies(X_54,X_55)),implies(X_52,implies(X_54,X_55))))
| is_a_theorem(implies(X_52,implies(X_54,X_55))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_53,implies(X_55,X_56)),implies(X_54,X_55)))),bind(Y,$fot(implies(X_52,implies(X_54,X_55))))]]) ).
cnf(refute_0_6,plain,
( ~ is_a_theorem(implies(implies(implies(X_23,X_24),implies(X_24,X_25)),implies(X_22,implies(X_24,X_25))))
| is_a_theorem(implies(implies(implies(X_22,implies(X_24,X_25)),implies(X_23,X_24)),implies(U,implies(X_23,X_24)))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(implies(X_23,X_24))),bind(Y,$fot(implies(X_24,X_25))),bind(Z,$fot(implies(X_22,implies(X_24,X_25))))]]) ).
cnf(refute_0_7,plain,
( ~ is_a_theorem(implies(implies(implies(X_12,X_13),X_12),implies(X_11,X_12)))
| is_a_theorem(implies(implies(implies(X_11,X_12),implies(X_12,X_13)),implies(U,implies(X_12,X_13)))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(implies(X_12,X_13))),bind(Y,$fot(X_12)),bind(Z,$fot(implies(X_11,X_12)))]]) ).
cnf(refute_0_8,plain,
is_a_theorem(implies(implies(X_8,X_9),implies(X_8,X_9))),
inference(subst,[],[ic_1:[bind(X,$fot(implies(X_8,X_9)))]]) ).
cnf(refute_0_9,plain,
( ~ is_a_theorem(implies(implies(X_8,X_9),implies(X_8,X_9)))
| is_a_theorem(implies(implies(implies(X_8,X_9),X_8),implies(X_7,X_8))) ),
inference(subst,[],[refute_0_2:[bind(U,$fot(X_7)),bind(X,$fot(X_8)),bind(Y,$fot(X_9)),bind(Z,$fot(implies(X_8,X_9)))]]) ).
cnf(refute_0_10,plain,
is_a_theorem(implies(implies(implies(X_8,X_9),X_8),implies(X_7,X_8))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_8,X_9),implies(X_8,X_9))) )],[refute_0_8,refute_0_9]) ).
cnf(refute_0_11,plain,
is_a_theorem(implies(implies(implies(X_12,X_13),X_12),implies(X_11,X_12))),
inference(subst,[],[refute_0_10:[bind(X_7,$fot(X_11)),bind(X_8,$fot(X_12)),bind(X_9,$fot(X_13))]]) ).
cnf(refute_0_12,plain,
is_a_theorem(implies(implies(implies(X_11,X_12),implies(X_12,X_13)),implies(U,implies(X_12,X_13)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_12,X_13),X_12),implies(X_11,X_12))) )],[refute_0_11,refute_0_7]) ).
cnf(refute_0_13,plain,
is_a_theorem(implies(implies(implies(X_23,X_24),implies(X_24,X_25)),implies(X_22,implies(X_24,X_25)))),
inference(subst,[],[refute_0_12:[bind(U,$fot(X_22)),bind(X_11,$fot(X_23)),bind(X_12,$fot(X_24)),bind(X_13,$fot(X_25))]]) ).
cnf(refute_0_14,plain,
is_a_theorem(implies(implies(implies(X_22,implies(X_24,X_25)),implies(X_23,X_24)),implies(U,implies(X_23,X_24)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_23,X_24),implies(X_24,X_25)),implies(X_22,implies(X_24,X_25)))) )],[refute_0_13,refute_0_6]) ).
cnf(refute_0_15,plain,
is_a_theorem(implies(implies(implies(X_53,implies(X_55,X_56)),implies(X_54,X_55)),implies(X_52,implies(X_54,X_55)))),
inference(subst,[],[refute_0_14:[bind(U,$fot(X_52)),bind(X_22,$fot(X_53)),bind(X_23,$fot(X_54)),bind(X_24,$fot(X_55)),bind(X_25,$fot(X_56))]]) ).
cnf(refute_0_16,plain,
( ~ is_a_theorem(implies(implies(X_53,implies(X_55,X_56)),implies(X_54,X_55)))
| is_a_theorem(implies(X_52,implies(X_54,X_55))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_53,implies(X_55,X_56)),implies(X_54,X_55)),implies(X_52,implies(X_54,X_55)))) )],[refute_0_15,refute_0_5]) ).
cnf(refute_0_17,plain,
( ~ is_a_theorem(implies(implies(implies(X,Y),implies(implies(U,X),X_191)),implies(implies(implies(implies(U,X),X_191),X),implies(U,X))))
| is_a_theorem(implies(X_187,implies(implies(implies(implies(U,X),X_191),X),implies(U,X)))) ),
inference(subst,[],[refute_0_16:[bind(X_52,$fot(X_187)),bind(X_53,$fot(implies(X,Y))),bind(X_54,$fot(implies(implies(implies(U,X),X_191),X))),bind(X_55,$fot(implies(U,X))),bind(X_56,$fot(X_191))]]) ).
cnf(refute_0_18,plain,
is_a_theorem(implies(X_187,implies(implies(implies(implies(U,X),X_191),X),implies(U,X)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X,Y),implies(implies(U,X),X_191)),implies(implies(implies(implies(U,X),X_191),X),implies(U,X)))) )],[refute_0_4,refute_0_17]) ).
cnf(refute_0_19,plain,
is_a_theorem(implies(implies(X,Y),implies(implies(implies(implies(X_192,X_193),X_195),X_193),implies(X_192,X_193)))),
inference(subst,[],[refute_0_18:[bind(U,$fot(X_192)),bind(X,$fot(X_193)),bind(X_187,$fot(implies(X,Y))),bind(X_191,$fot(X_195))]]) ).
cnf(refute_0_20,plain,
is_a_theorem(implies(implies(implies(implies(implies(implies(X_192,X_193),X_195),X_193),implies(X_192,X_193)),X),implies(U,X))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X,Y),implies(implies(implies(implies(X_192,X_193),X_195),X_193),implies(X_192,X_193)))) )],[refute_0_19,refute_0_3]) ).
cnf(refute_0_21,plain,
( ~ is_a_theorem(X_251)
| ~ is_a_theorem(implies(X_251,implies(implies(implies(X_252,X_252),X_250),X_250)))
| is_a_theorem(implies(implies(implies(X_252,X_252),X_250),X_250)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(X_251)),bind(Y,$fot(implies(implies(implies(X_252,X_252),X_250),X_250)))]]) ).
cnf(refute_0_22,plain,
( ~ is_a_theorem(implies(implies(implies(X_205,X_206),X_207),X_206))
| ~ is_a_theorem(implies(implies(implies(implies(X_205,X_206),X_207),X_206),implies(X_205,X_206)))
| is_a_theorem(implies(X_205,X_206)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(X_205,X_206),X_207),X_206))),bind(Y,$fot(implies(X_205,X_206)))]]) ).
cnf(refute_0_23,plain,
( ~ is_a_theorem(implies(implies(X,Y),implies(implies(implies(X_49,X_50),X_49),implies(X_48,X_49))))
| is_a_theorem(implies(implies(implies(implies(implies(X_49,X_50),X_49),implies(X_48,X_49)),X),implies(U,X))) ),
inference(subst,[],[refute_0_2:[bind(Z,$fot(implies(implies(implies(X_49,X_50),X_49),implies(X_48,X_49))))]]) ).
cnf(refute_0_24,plain,
is_a_theorem(implies(implies(implies(X,Y),implies(X,Y)),implies(implies(implies(X,Y),X),implies(U,X)))),
inference(subst,[],[ic_JLukasiewicz:[bind(Z,$fot(implies(X,Y)))]]) ).
cnf(refute_0_25,plain,
( ~ is_a_theorem(implies(implies(X_21,X_21),X_20))
| ~ is_a_theorem(implies(implies(implies(X_21,X_21),X_20),implies(X_19,X_20)))
| is_a_theorem(implies(X_19,X_20)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_21,X_21),X_20))),bind(Y,$fot(implies(X_19,X_20)))]]) ).
cnf(refute_0_26,plain,
( ~ is_a_theorem(implies(implies(X,Y),implies(X_18,X_18)))
| is_a_theorem(implies(implies(implies(X_18,X_18),X),implies(U,X))) ),
inference(subst,[],[refute_0_2:[bind(Z,$fot(implies(X_18,X_18)))]]) ).
cnf(refute_0_27,plain,
is_a_theorem(implies(implies(implies(X_9,X_9),X_9),implies(X_9,X_9))),
inference(subst,[],[refute_0_10:[bind(X_7,$fot(X_9)),bind(X_8,$fot(X_9))]]) ).
cnf(refute_0_28,plain,
( ~ is_a_theorem(implies(implies(X_12,X_13),X_12))
| ~ is_a_theorem(implies(implies(implies(X_12,X_13),X_12),implies(X_11,X_12)))
| is_a_theorem(implies(X_11,X_12)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_12,X_13),X_12))),bind(Y,$fot(implies(X_11,X_12)))]]) ).
cnf(refute_0_29,plain,
( ~ is_a_theorem(implies(implies(X_12,X_13),X_12))
| is_a_theorem(implies(X_11,X_12)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_12,X_13),X_12),implies(X_11,X_12))) )],[refute_0_11,refute_0_28]) ).
cnf(refute_0_30,plain,
( ~ is_a_theorem(implies(implies(implies(X_9,X_9),X_9),implies(X_9,X_9)))
| is_a_theorem(implies(X_14,implies(X_9,X_9))) ),
inference(subst,[],[refute_0_29:[bind(X_11,$fot(X_14)),bind(X_12,$fot(implies(X_9,X_9))),bind(X_13,$fot(X_9))]]) ).
cnf(refute_0_31,plain,
is_a_theorem(implies(X_14,implies(X_9,X_9))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_9,X_9),X_9),implies(X_9,X_9))) )],[refute_0_27,refute_0_30]) ).
cnf(refute_0_32,plain,
is_a_theorem(implies(implies(X,Y),implies(X_18,X_18))),
inference(subst,[],[refute_0_31:[bind(X_14,$fot(implies(X,Y))),bind(X_9,$fot(X_18))]]) ).
cnf(refute_0_33,plain,
is_a_theorem(implies(implies(implies(X_18,X_18),X),implies(U,X))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X,Y),implies(X_18,X_18))) )],[refute_0_32,refute_0_26]) ).
cnf(refute_0_34,plain,
is_a_theorem(implies(implies(implies(X_21,X_21),X_20),implies(X_19,X_20))),
inference(subst,[],[refute_0_33:[bind(U,$fot(X_19)),bind(X,$fot(X_20)),bind(X_18,$fot(X_21))]]) ).
cnf(refute_0_35,plain,
( ~ is_a_theorem(implies(implies(X_21,X_21),X_20))
| is_a_theorem(implies(X_19,X_20)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_21,X_21),X_20),implies(X_19,X_20))) )],[refute_0_34,refute_0_25]) ).
cnf(refute_0_36,plain,
( ~ is_a_theorem(implies(implies(implies(X,Y),implies(X,Y)),implies(implies(implies(X,Y),X),implies(U,X))))
| is_a_theorem(implies(X_38,implies(implies(implies(X,Y),X),implies(U,X)))) ),
inference(subst,[],[refute_0_35:[bind(X_19,$fot(X_38)),bind(X_20,$fot(implies(implies(implies(X,Y),X),implies(U,X)))),bind(X_21,$fot(implies(X,Y)))]]) ).
cnf(refute_0_37,plain,
is_a_theorem(implies(X_38,implies(implies(implies(X,Y),X),implies(U,X)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X,Y),implies(X,Y)),implies(implies(implies(X,Y),X),implies(U,X)))) )],[refute_0_24,refute_0_36]) ).
cnf(refute_0_38,plain,
is_a_theorem(implies(implies(X,Y),implies(implies(implies(X_49,X_50),X_49),implies(X_48,X_49)))),
inference(subst,[],[refute_0_37:[bind(U,$fot(X_48)),bind(X,$fot(X_49)),bind(Y,$fot(X_50)),bind(X_38,$fot(implies(X,Y)))]]) ).
cnf(refute_0_39,plain,
is_a_theorem(implies(implies(implies(implies(implies(X_49,X_50),X_49),implies(X_48,X_49)),X),implies(U,X))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X,Y),implies(implies(implies(X_49,X_50),X_49),implies(X_48,X_49)))) )],[refute_0_38,refute_0_23]) ).
cnf(refute_0_40,plain,
( ~ is_a_theorem(X_194)
| ~ is_a_theorem(implies(X_194,implies(implies(implies(implies(X_192,X_193),X_195),X_193),implies(X_192,X_193))))
| is_a_theorem(implies(implies(implies(implies(X_192,X_193),X_195),X_193),implies(X_192,X_193))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(X_194)),bind(Y,$fot(implies(implies(implies(implies(X_192,X_193),X_195),X_193),implies(X_192,X_193))))]]) ).
cnf(refute_0_41,plain,
is_a_theorem(implies(X_194,implies(implies(implies(implies(X_192,X_193),X_195),X_193),implies(X_192,X_193)))),
inference(subst,[],[refute_0_18:[bind(U,$fot(X_192)),bind(X,$fot(X_193)),bind(X_187,$fot(X_194)),bind(X_191,$fot(X_195))]]) ).
cnf(refute_0_42,plain,
( ~ is_a_theorem(X_194)
| is_a_theorem(implies(implies(implies(implies(X_192,X_193),X_195),X_193),implies(X_192,X_193))) ),
inference(resolve,[$cnf( is_a_theorem(implies(X_194,implies(implies(implies(implies(X_192,X_193),X_195),X_193),implies(X_192,X_193)))) )],[refute_0_41,refute_0_40]) ).
cnf(refute_0_43,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(X_49,X_50),X_49),implies(X_48,X_49)),X),implies(U,X)))
| is_a_theorem(implies(implies(implies(implies(X_201,X_202),X_204),X_202),implies(X_201,X_202))) ),
inference(subst,[],[refute_0_42:[bind(X_192,$fot(X_201)),bind(X_193,$fot(X_202)),bind(X_194,$fot(implies(implies(implies(implies(implies(X_49,X_50),X_49),implies(X_48,X_49)),X),implies(U,X)))),bind(X_195,$fot(X_204))]]) ).
cnf(refute_0_44,plain,
is_a_theorem(implies(implies(implies(implies(X_201,X_202),X_204),X_202),implies(X_201,X_202))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(X_49,X_50),X_49),implies(X_48,X_49)),X),implies(U,X))) )],[refute_0_39,refute_0_43]) ).
cnf(refute_0_45,plain,
is_a_theorem(implies(implies(implies(implies(X_205,X_206),X_207),X_206),implies(X_205,X_206))),
inference(subst,[],[refute_0_44:[bind(X_201,$fot(X_205)),bind(X_202,$fot(X_206)),bind(X_204,$fot(X_207))]]) ).
cnf(refute_0_46,plain,
( ~ is_a_theorem(implies(implies(implies(X_205,X_206),X_207),X_206))
| is_a_theorem(implies(X_205,X_206)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_205,X_206),X_207),X_206),implies(X_205,X_206))) )],[refute_0_45,refute_0_22]) ).
cnf(refute_0_47,plain,
( ~ is_a_theorem(implies(implies(implies(X_247,implies(implies(implies(X_249,X_249),X_246),X_246)),X_246),implies(implies(implies(X_249,X_249),X_246),X_246)))
| is_a_theorem(implies(X_247,implies(implies(implies(X_249,X_249),X_246),X_246))) ),
inference(subst,[],[refute_0_46:[bind(X_205,$fot(X_247)),bind(X_206,$fot(implies(implies(implies(X_249,X_249),X_246),X_246))),bind(X_207,$fot(X_246))]]) ).
cnf(refute_0_48,plain,
( ~ is_a_theorem(implies(implies(X,Y),implies(X_212,implies(implies(implies(X_215,X_215),X_213),X_213))))
| is_a_theorem(implies(implies(implies(X_212,implies(implies(implies(X_215,X_215),X_213),X_213)),X),implies(U,X))) ),
inference(subst,[],[refute_0_2:[bind(Z,$fot(implies(X_212,implies(implies(implies(X_215,X_215),X_213),X_213))))]]) ).
cnf(refute_0_49,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_76,X_76),X_77),implies(X_75,X_77)),X_74))
| ~ is_a_theorem(implies(implies(implies(implies(implies(X_76,X_76),X_77),implies(X_75,X_77)),X_74),implies(X_73,X_74)))
| is_a_theorem(implies(X_73,X_74)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(implies(X_76,X_76),X_77),implies(X_75,X_77)),X_74))),bind(Y,$fot(implies(X_73,X_74)))]]) ).
cnf(refute_0_50,plain,
( ~ is_a_theorem(implies(implies(X,Y),implies(implies(implies(X_63,X_63),X_64),implies(X_61,X_64))))
| is_a_theorem(implies(implies(implies(implies(implies(X_63,X_63),X_64),implies(X_61,X_64)),X),implies(U,X))) ),
inference(subst,[],[refute_0_2:[bind(Z,$fot(implies(implies(implies(X_63,X_63),X_64),implies(X_61,X_64))))]]) ).
cnf(refute_0_51,plain,
is_a_theorem(implies(implies(implies(X_60,X_59),implies(X_59,X_59)),implies(implies(implies(X_59,X_59),X_60),implies(U,X_60)))),
inference(subst,[],[ic_JLukasiewicz:[bind(X,$fot(X_60)),bind(Y,$fot(X_59)),bind(Z,$fot(implies(X_59,X_59)))]]) ).
cnf(refute_0_52,plain,
( ~ is_a_theorem(implies(implies(implies(X_37,X_36),implies(X_36,X_36)),X_35))
| ~ is_a_theorem(implies(implies(implies(implies(X_37,X_36),implies(X_36,X_36)),X_35),implies(X_34,X_35)))
| is_a_theorem(implies(X_34,X_35)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(X_37,X_36),implies(X_36,X_36)),X_35))),bind(Y,$fot(implies(X_34,X_35)))]]) ).
cnf(refute_0_53,plain,
( ~ is_a_theorem(implies(implies(X,Y),implies(implies(X_33,X_32),implies(X_32,X_32))))
| is_a_theorem(implies(implies(implies(implies(X_33,X_32),implies(X_32,X_32)),X),implies(U,X))) ),
inference(subst,[],[refute_0_2:[bind(Z,$fot(implies(implies(X_33,X_32),implies(X_32,X_32))))]]) ).
cnf(refute_0_54,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_30,X_28),implies(X_28,X_28)),implies(X_28,X_28)),implies(implies(X_30,X_28),implies(X_28,X_28))))
| is_a_theorem(implies(X_11,implies(implies(X_30,X_28),implies(X_28,X_28)))) ),
inference(subst,[],[refute_0_29:[bind(X_12,$fot(implies(implies(X_30,X_28),implies(X_28,X_28)))),bind(X_13,$fot(implies(X_28,X_28)))]]) ).
cnf(refute_0_55,plain,
is_a_theorem(implies(implies(implies(X,Y),X_9),implies(implies(X_9,X),implies(U,X)))),
inference(subst,[],[ic_JLukasiewicz:[bind(Z,$fot(X_9))]]) ).
cnf(refute_0_56,plain,
( ~ is_a_theorem(implies(implies(implies(X,Y),X_9),implies(implies(X_9,X),implies(U,X))))
| is_a_theorem(implies(implies(implies(implies(X_9,X),implies(U,X)),implies(X,Y)),implies(X_7,implies(X,Y)))) ),
inference(subst,[],[refute_0_2:[bind(U,$fot(X_7)),bind(X,$fot(implies(X,Y))),bind(Y,$fot(X_9)),bind(Z,$fot(implies(implies(X_9,X),implies(U,X))))]]) ).
cnf(refute_0_57,plain,
is_a_theorem(implies(implies(implies(implies(X_9,X),implies(U,X)),implies(X,Y)),implies(X_7,implies(X,Y)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X,Y),X_9),implies(implies(X_9,X),implies(U,X)))) )],[refute_0_55,refute_0_56]) ).
cnf(refute_0_58,plain,
is_a_theorem(implies(implies(implies(implies(X_30,X_28),implies(X_28,X_28)),implies(X_28,X_28)),implies(implies(X_30,X_28),implies(X_28,X_28)))),
inference(subst,[],[refute_0_57:[bind(U,$fot(X_28)),bind(X,$fot(X_28)),bind(Y,$fot(X_28)),bind(X_7,$fot(implies(X_30,X_28))),bind(X_9,$fot(X_30))]]) ).
cnf(refute_0_59,plain,
is_a_theorem(implies(X_11,implies(implies(X_30,X_28),implies(X_28,X_28)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_30,X_28),implies(X_28,X_28)),implies(X_28,X_28)),implies(implies(X_30,X_28),implies(X_28,X_28)))) )],[refute_0_58,refute_0_54]) ).
cnf(refute_0_60,plain,
is_a_theorem(implies(implies(X,Y),implies(implies(X_33,X_32),implies(X_32,X_32)))),
inference(subst,[],[refute_0_59:[bind(X_11,$fot(implies(X,Y))),bind(X_28,$fot(X_32)),bind(X_30,$fot(X_33))]]) ).
cnf(refute_0_61,plain,
is_a_theorem(implies(implies(implies(implies(X_33,X_32),implies(X_32,X_32)),X),implies(U,X))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X,Y),implies(implies(X_33,X_32),implies(X_32,X_32)))) )],[refute_0_60,refute_0_53]) ).
cnf(refute_0_62,plain,
is_a_theorem(implies(implies(implies(implies(X_37,X_36),implies(X_36,X_36)),X_35),implies(X_34,X_35))),
inference(subst,[],[refute_0_61:[bind(U,$fot(X_34)),bind(X,$fot(X_35)),bind(X_32,$fot(X_36)),bind(X_33,$fot(X_37))]]) ).
cnf(refute_0_63,plain,
( ~ is_a_theorem(implies(implies(implies(X_37,X_36),implies(X_36,X_36)),X_35))
| is_a_theorem(implies(X_34,X_35)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_37,X_36),implies(X_36,X_36)),X_35),implies(X_34,X_35))) )],[refute_0_62,refute_0_52]) ).
cnf(refute_0_64,plain,
( ~ is_a_theorem(implies(implies(implies(X_60,X_59),implies(X_59,X_59)),implies(implies(implies(X_59,X_59),X_60),implies(U,X_60))))
| is_a_theorem(implies(X_57,implies(implies(implies(X_59,X_59),X_60),implies(U,X_60)))) ),
inference(subst,[],[refute_0_63:[bind(X_34,$fot(X_57)),bind(X_35,$fot(implies(implies(implies(X_59,X_59),X_60),implies(U,X_60)))),bind(X_36,$fot(X_59)),bind(X_37,$fot(X_60))]]) ).
cnf(refute_0_65,plain,
is_a_theorem(implies(X_57,implies(implies(implies(X_59,X_59),X_60),implies(U,X_60)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_60,X_59),implies(X_59,X_59)),implies(implies(implies(X_59,X_59),X_60),implies(U,X_60)))) )],[refute_0_51,refute_0_64]) ).
cnf(refute_0_66,plain,
is_a_theorem(implies(implies(X,Y),implies(implies(implies(X_63,X_63),X_64),implies(X_61,X_64)))),
inference(subst,[],[refute_0_65:[bind(U,$fot(X_61)),bind(X_57,$fot(implies(X,Y))),bind(X_59,$fot(X_63)),bind(X_60,$fot(X_64))]]) ).
cnf(refute_0_67,plain,
is_a_theorem(implies(implies(implies(implies(implies(X_63,X_63),X_64),implies(X_61,X_64)),X),implies(U,X))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X,Y),implies(implies(implies(X_63,X_63),X_64),implies(X_61,X_64)))) )],[refute_0_66,refute_0_50]) ).
cnf(refute_0_68,plain,
is_a_theorem(implies(implies(implies(implies(implies(X_76,X_76),X_77),implies(X_75,X_77)),X_74),implies(X_73,X_74))),
inference(subst,[],[refute_0_67:[bind(U,$fot(X_73)),bind(X,$fot(X_74)),bind(X_61,$fot(X_75)),bind(X_63,$fot(X_76)),bind(X_64,$fot(X_77))]]) ).
cnf(refute_0_69,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_76,X_76),X_77),implies(X_75,X_77)),X_74))
| is_a_theorem(implies(X_73,X_74)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(X_76,X_76),X_77),implies(X_75,X_77)),X_74),implies(X_73,X_74))) )],[refute_0_68,refute_0_49]) ).
cnf(refute_0_70,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_76,X_76),X_211),implies(implies(implies(X_76,X_76),X_211),X_211)),implies(X_208,implies(implies(implies(X_76,X_76),X_211),X_211))))
| is_a_theorem(implies(X_73,implies(X_208,implies(implies(implies(X_76,X_76),X_211),X_211)))) ),
inference(subst,[],[refute_0_69:[bind(X_74,$fot(implies(X_208,implies(implies(implies(X_76,X_76),X_211),X_211)))),bind(X_75,$fot(implies(implies(X_76,X_76),X_211))),bind(X_77,$fot(X_211))]]) ).
cnf(refute_0_71,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_205,X_206),X_207),X_206),implies(X_205,X_206)))
| is_a_theorem(implies(implies(implies(X_205,X_206),implies(implies(X_205,X_206),X_207)),implies(U,implies(implies(X_205,X_206),X_207)))) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(implies(implies(X_205,X_206),X_207))),bind(Y,$fot(X_206)),bind(Z,$fot(implies(X_205,X_206)))]]) ).
cnf(refute_0_72,plain,
is_a_theorem(implies(implies(implies(X_205,X_206),implies(implies(X_205,X_206),X_207)),implies(U,implies(implies(X_205,X_206),X_207)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_205,X_206),X_207),X_206),implies(X_205,X_206))) )],[refute_0_45,refute_0_71]) ).
cnf(refute_0_73,plain,
is_a_theorem(implies(implies(implies(implies(X_76,X_76),X_211),implies(implies(implies(X_76,X_76),X_211),X_211)),implies(X_208,implies(implies(implies(X_76,X_76),X_211),X_211)))),
inference(subst,[],[refute_0_72:[bind(U,$fot(X_208)),bind(X_205,$fot(implies(X_76,X_76))),bind(X_206,$fot(X_211)),bind(X_207,$fot(X_211))]]) ).
cnf(refute_0_74,plain,
is_a_theorem(implies(X_73,implies(X_208,implies(implies(implies(X_76,X_76),X_211),X_211)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_76,X_76),X_211),implies(implies(implies(X_76,X_76),X_211),X_211)),implies(X_208,implies(implies(implies(X_76,X_76),X_211),X_211)))) )],[refute_0_73,refute_0_70]) ).
cnf(refute_0_75,plain,
is_a_theorem(implies(implies(X,Y),implies(X_212,implies(implies(implies(X_215,X_215),X_213),X_213)))),
inference(subst,[],[refute_0_74:[bind(X_208,$fot(X_212)),bind(X_211,$fot(X_213)),bind(X_73,$fot(implies(X,Y))),bind(X_76,$fot(X_215))]]) ).
cnf(refute_0_76,plain,
is_a_theorem(implies(implies(implies(X_212,implies(implies(implies(X_215,X_215),X_213),X_213)),X),implies(U,X))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X,Y),implies(X_212,implies(implies(implies(X_215,X_215),X_213),X_213)))) )],[refute_0_75,refute_0_48]) ).
cnf(refute_0_77,plain,
is_a_theorem(implies(implies(implies(X_247,implies(implies(implies(X_249,X_249),X_246),X_246)),X_246),implies(implies(implies(X_249,X_249),X_246),X_246))),
inference(subst,[],[refute_0_76:[bind(U,$fot(implies(implies(X_249,X_249),X_246))),bind(X,$fot(X_246)),bind(X_212,$fot(X_247)),bind(X_213,$fot(X_246)),bind(X_215,$fot(X_249))]]) ).
cnf(refute_0_78,plain,
is_a_theorem(implies(X_247,implies(implies(implies(X_249,X_249),X_246),X_246))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_247,implies(implies(implies(X_249,X_249),X_246),X_246)),X_246),implies(implies(implies(X_249,X_249),X_246),X_246))) )],[refute_0_77,refute_0_47]) ).
cnf(refute_0_79,plain,
is_a_theorem(implies(X_251,implies(implies(implies(X_252,X_252),X_250),X_250))),
inference(subst,[],[refute_0_78:[bind(X_246,$fot(X_250)),bind(X_247,$fot(X_251)),bind(X_249,$fot(X_252))]]) ).
cnf(refute_0_80,plain,
( ~ is_a_theorem(X_251)
| is_a_theorem(implies(implies(implies(X_252,X_252),X_250),X_250)) ),
inference(resolve,[$cnf( is_a_theorem(implies(X_251,implies(implies(implies(X_252,X_252),X_250),X_250))) )],[refute_0_79,refute_0_21]) ).
cnf(refute_0_81,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(implies(X_192,X_193),X_195),X_193),implies(X_192,X_193)),X),implies(U,X)))
| is_a_theorem(implies(implies(implies(X_262,X_262),X_260),X_260)) ),
inference(subst,[],[refute_0_80:[bind(X_250,$fot(X_260)),bind(X_251,$fot(implies(implies(implies(implies(implies(implies(X_192,X_193),X_195),X_193),implies(X_192,X_193)),X),implies(U,X)))),bind(X_252,$fot(X_262))]]) ).
cnf(refute_0_82,plain,
is_a_theorem(implies(implies(implies(X_262,X_262),X_260),X_260)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(implies(X_192,X_193),X_195),X_193),implies(X_192,X_193)),X),implies(U,X))) )],[refute_0_20,refute_0_81]) ).
cnf(refute_0_83,plain,
is_a_theorem(implies(implies(implies(X_264,X_264),X_263),X_263)),
inference(subst,[],[refute_0_82:[bind(X_260,$fot(X_263)),bind(X_262,$fot(X_264))]]) ).
cnf(refute_0_84,plain,
( ~ is_a_theorem(implies(implies(X_264,X_264),X_263))
| is_a_theorem(X_263) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_264,X_264),X_263),X_263)) )],[refute_0_83,refute_0_0]) ).
cnf(refute_0_85,plain,
( ~ is_a_theorem(implies(implies(X_264,X_264),implies(implies(implies(X_453,X_454),X_453),X_453)))
| is_a_theorem(implies(implies(implies(X_453,X_454),X_453),X_453)) ),
inference(subst,[],[refute_0_84:[bind(X_263,$fot(implies(implies(implies(X_453,X_454),X_453),X_453)))]]) ).
cnf(refute_0_86,plain,
( ~ is_a_theorem(implies(implies(X_264,X_264),implies(X_448,implies(implies(implies(X_450,X_451),X_450),X_450))))
| is_a_theorem(implies(X_448,implies(implies(implies(X_450,X_451),X_450),X_450))) ),
inference(subst,[],[refute_0_84:[bind(X_263,$fot(implies(X_448,implies(implies(implies(X_450,X_451),X_450),X_450))))]]) ).
cnf(refute_0_87,plain,
is_a_theorem(implies(implies(implies(implies(X_446,X_447),X_446),implies(implies(implies(X_446,X_447),X_446),X_446)),implies(U,implies(implies(implies(X_446,X_447),X_446),X_446)))),
inference(subst,[],[refute_0_72:[bind(X_205,$fot(implies(X_446,X_447))),bind(X_206,$fot(X_446)),bind(X_207,$fot(X_446))]]) ).
cnf(refute_0_88,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_86,X_87),X_86),implies(X_85,X_86)),X_84))
| ~ is_a_theorem(implies(implies(implies(implies(implies(X_86,X_87),X_86),implies(X_85,X_86)),X_84),implies(X_83,X_84)))
| is_a_theorem(implies(X_83,X_84)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(implies(X_86,X_87),X_86),implies(X_85,X_86)),X_84))),bind(Y,$fot(implies(X_83,X_84)))]]) ).
cnf(refute_0_89,plain,
is_a_theorem(implies(implies(implies(implies(implies(X_86,X_87),X_86),implies(X_85,X_86)),X_84),implies(X_83,X_84))),
inference(subst,[],[refute_0_39:[bind(U,$fot(X_83)),bind(X,$fot(X_84)),bind(X_48,$fot(X_85)),bind(X_49,$fot(X_86)),bind(X_50,$fot(X_87))]]) ).
cnf(refute_0_90,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_86,X_87),X_86),implies(X_85,X_86)),X_84))
| is_a_theorem(implies(X_83,X_84)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(X_86,X_87),X_86),implies(X_85,X_86)),X_84),implies(X_83,X_84))) )],[refute_0_89,refute_0_88]) ).
cnf(refute_0_91,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_446,X_447),X_446),implies(implies(implies(X_446,X_447),X_446),X_446)),implies(U,implies(implies(implies(X_446,X_447),X_446),X_446))))
| is_a_theorem(implies(X_443,implies(U,implies(implies(implies(X_446,X_447),X_446),X_446)))) ),
inference(subst,[],[refute_0_90:[bind(X_83,$fot(X_443)),bind(X_84,$fot(implies(U,implies(implies(implies(X_446,X_447),X_446),X_446)))),bind(X_85,$fot(implies(implies(X_446,X_447),X_446))),bind(X_86,$fot(X_446)),bind(X_87,$fot(X_447))]]) ).
cnf(refute_0_92,plain,
is_a_theorem(implies(X_443,implies(U,implies(implies(implies(X_446,X_447),X_446),X_446)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_446,X_447),X_446),implies(implies(implies(X_446,X_447),X_446),X_446)),implies(U,implies(implies(implies(X_446,X_447),X_446),X_446)))) )],[refute_0_87,refute_0_91]) ).
cnf(refute_0_93,plain,
is_a_theorem(implies(implies(X_264,X_264),implies(X_448,implies(implies(implies(X_450,X_451),X_450),X_450)))),
inference(subst,[],[refute_0_92:[bind(U,$fot(X_448)),bind(X_443,$fot(implies(X_264,X_264))),bind(X_446,$fot(X_450)),bind(X_447,$fot(X_451))]]) ).
cnf(refute_0_94,plain,
is_a_theorem(implies(X_448,implies(implies(implies(X_450,X_451),X_450),X_450))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_264,X_264),implies(X_448,implies(implies(implies(X_450,X_451),X_450),X_450)))) )],[refute_0_93,refute_0_86]) ).
cnf(refute_0_95,plain,
is_a_theorem(implies(implies(X_264,X_264),implies(implies(implies(X_453,X_454),X_453),X_453))),
inference(subst,[],[refute_0_94:[bind(X_448,$fot(implies(X_264,X_264))),bind(X_450,$fot(X_453)),bind(X_451,$fot(X_454))]]) ).
cnf(refute_0_96,plain,
is_a_theorem(implies(implies(implies(X_453,X_454),X_453),X_453)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_264,X_264),implies(implies(implies(X_453,X_454),X_453),X_453))) )],[refute_0_95,refute_0_85]) ).
cnf(refute_0_97,plain,
is_a_theorem(implies(implies(implies(a,b),a),a)),
inference(subst,[],[refute_0_96:[bind(X_453,$fot(a)),bind(X_454,$fot(b))]]) ).
cnf(refute_0_98,plain,
$false,
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(a,b),a),a)) )],[refute_0_97,prove_ic_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL083-2 : TPTP v9.3.1. Bugfixed v1.2.0.
% 0.00/0.04 % Command : metis --show proof --show saturation %s
% 0.11/0.37 % Computer : n006.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sat Sep 5 13:56:46 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.38 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.23/0.53 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.23/0.53
% 0.23/0.53 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 0.23/0.56
%------------------------------------------------------------------------------