%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : LCL082-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 12:41:48 PM UTC 2026
% Result : Unsatisfiable 0.42s 0.68s
% Output : CNFRefutation 0.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 3
% Syntax : Number of clauses : 59 ( 31 unt; 0 nHn; 13 RR)
% Number of literals : 95 ( 0 equ; 37 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 3 ( 3 usr; 2 con; 0-2 aty)
% Number of variables : 217 ( 79 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(prove_ic_2,negated_conjecture,
~ is_a_theorem(implies(a,implies(b,a))) ).
cnf(refute_0_0,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_1,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_0]) ).
cnf(refute_0_2,plain,
( ~ is_a_theorem(implies(implies(X_220,X_221),implies(implies(implies(implies(X_222,X_222),implies(implies(X_223,X_222),implies(X_222,X_222))),X_221),implies(X_220,X_221))))
| is_a_theorem(implies(implies(implies(implies(implies(implies(X_222,X_222),implies(implies(X_223,X_222),implies(X_222,X_222))),X_221),implies(X_220,X_221)),X_220),implies(U,X_220))) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(X_220)),bind(Y,$fot(X_221)),bind(Z,$fot(implies(implies(implies(implies(X_222,X_222),implies(implies(X_223,X_222),implies(X_222,X_222))),X_221),implies(X_220,X_221))))]]) ).
cnf(refute_0_3,plain,
( ~ is_a_theorem(implies(implies(X,Y),implies(implies(X_29,X_29),implies(implies(X_30,X_29),implies(X_29,X_29)))))
| is_a_theorem(implies(implies(implies(implies(X_29,X_29),implies(implies(X_30,X_29),implies(X_29,X_29))),X),implies(U,X))) ),
inference(subst,[],[refute_0_1:[bind(Z,$fot(implies(implies(X_29,X_29),implies(implies(X_30,X_29),implies(X_29,X_29)))))]]) ).
cnf(refute_0_4,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_14,X_11),implies(X_10,X_11)),implies(X_11,X_12)),implies(X_13,implies(X_11,X_12))))
| is_a_theorem(implies(implies(implies(X_13,implies(X_11,X_12)),implies(implies(X_14,X_11),implies(X_10,X_11))),implies(U,implies(implies(X_14,X_11),implies(X_10,X_11))))) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(implies(implies(X_14,X_11),implies(X_10,X_11)))),bind(Y,$fot(implies(X_11,X_12))),bind(Z,$fot(implies(X_13,implies(X_11,X_12))))]]) ).
cnf(refute_0_5,plain,
is_a_theorem(implies(implies(implies(X,Y),X_8),implies(implies(X_8,X),implies(U,X)))),
inference(subst,[],[ic_JLukasiewicz:[bind(Z,$fot(X_8))]]) ).
cnf(refute_0_6,plain,
( ~ is_a_theorem(implies(implies(implies(X,Y),X_8),implies(implies(X_8,X),implies(U,X))))
| is_a_theorem(implies(implies(implies(implies(X_8,X),implies(U,X)),implies(X,Y)),implies(X_6,implies(X,Y)))) ),
inference(subst,[],[refute_0_1:[bind(U,$fot(X_6)),bind(X,$fot(implies(X,Y))),bind(Y,$fot(X_8)),bind(Z,$fot(implies(implies(X_8,X),implies(U,X))))]]) ).
cnf(refute_0_7,plain,
is_a_theorem(implies(implies(implies(implies(X_8,X),implies(U,X)),implies(X,Y)),implies(X_6,implies(X,Y)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X,Y),X_8),implies(implies(X_8,X),implies(U,X)))) )],[refute_0_5,refute_0_6]) ).
cnf(refute_0_8,plain,
is_a_theorem(implies(implies(implies(implies(X_14,X_11),implies(X_10,X_11)),implies(X_11,X_12)),implies(X_13,implies(X_11,X_12)))),
inference(subst,[],[refute_0_7:[bind(U,$fot(X_10)),bind(X,$fot(X_11)),bind(Y,$fot(X_12)),bind(X_6,$fot(X_13)),bind(X_8,$fot(X_14))]]) ).
cnf(refute_0_9,plain,
is_a_theorem(implies(implies(implies(X_13,implies(X_11,X_12)),implies(implies(X_14,X_11),implies(X_10,X_11))),implies(U,implies(implies(X_14,X_11),implies(X_10,X_11))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_14,X_11),implies(X_10,X_11)),implies(X_11,X_12)),implies(X_13,implies(X_11,X_12)))) )],[refute_0_8,refute_0_4]) ).
cnf(refute_0_10,plain,
is_a_theorem(implies(implies(implies(X_25,implies(X_12,X_12)),implies(implies(X_14,X_12),implies(X_12,X_12))),implies(implies(X_12,X_12),implies(implies(X_14,X_12),implies(X_12,X_12))))),
inference(subst,[],[refute_0_9:[bind(U,$fot(implies(X_12,X_12))),bind(X_10,$fot(X_12)),bind(X_11,$fot(X_12)),bind(X_13,$fot(X_25))]]) ).
cnf(refute_0_11,plain,
( ~ is_a_theorem(implies(implies(implies(X_14,X_11),implies(X_10,X_11)),implies(X_11,X_12)))
| ~ is_a_theorem(implies(implies(implies(implies(X_14,X_11),implies(X_10,X_11)),implies(X_11,X_12)),implies(X_13,implies(X_11,X_12))))
| is_a_theorem(implies(X_13,implies(X_11,X_12))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(X_14,X_11),implies(X_10,X_11)),implies(X_11,X_12)))),bind(Y,$fot(implies(X_13,implies(X_11,X_12))))]]) ).
cnf(refute_0_12,plain,
( ~ is_a_theorem(implies(implies(implies(X_14,X_11),implies(X_10,X_11)),implies(X_11,X_12)))
| is_a_theorem(implies(X_13,implies(X_11,X_12))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_14,X_11),implies(X_10,X_11)),implies(X_11,X_12)),implies(X_13,implies(X_11,X_12)))) )],[refute_0_8,refute_0_11]) ).
cnf(refute_0_13,plain,
( ~ is_a_theorem(implies(implies(implies(X_25,implies(X_12,X_12)),implies(implies(X_14,X_12),implies(X_12,X_12))),implies(implies(X_12,X_12),implies(implies(X_14,X_12),implies(X_12,X_12)))))
| is_a_theorem(implies(X_24,implies(implies(X_12,X_12),implies(implies(X_14,X_12),implies(X_12,X_12))))) ),
inference(subst,[],[refute_0_12:[bind(X_10,$fot(implies(X_14,X_12))),bind(X_11,$fot(implies(X_12,X_12))),bind(X_12,$fot(implies(implies(X_14,X_12),implies(X_12,X_12)))),bind(X_13,$fot(X_24)),bind(X_14,$fot(X_25))]]) ).
cnf(refute_0_14,plain,
is_a_theorem(implies(X_24,implies(implies(X_12,X_12),implies(implies(X_14,X_12),implies(X_12,X_12))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_25,implies(X_12,X_12)),implies(implies(X_14,X_12),implies(X_12,X_12))),implies(implies(X_12,X_12),implies(implies(X_14,X_12),implies(X_12,X_12))))) )],[refute_0_10,refute_0_13]) ).
cnf(refute_0_15,plain,
is_a_theorem(implies(implies(X,Y),implies(implies(X_29,X_29),implies(implies(X_30,X_29),implies(X_29,X_29))))),
inference(subst,[],[refute_0_14:[bind(X_12,$fot(X_29)),bind(X_14,$fot(X_30)),bind(X_24,$fot(implies(X,Y)))]]) ).
cnf(refute_0_16,plain,
is_a_theorem(implies(implies(implies(implies(X_29,X_29),implies(implies(X_30,X_29),implies(X_29,X_29))),X),implies(U,X))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X,Y),implies(implies(X_29,X_29),implies(implies(X_30,X_29),implies(X_29,X_29))))) )],[refute_0_15,refute_0_3]) ).
cnf(refute_0_17,plain,
( ~ is_a_theorem(implies(X_47,X_48))
| ~ is_a_theorem(implies(implies(X_47,X_48),implies(X_48,implies(X_47,X_48))))
| is_a_theorem(implies(X_48,implies(X_47,X_48))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X_47,X_48))),bind(Y,$fot(implies(X_48,implies(X_47,X_48))))]]) ).
cnf(refute_0_18,plain,
( ~ is_a_theorem(X_28)
| ~ is_a_theorem(implies(X_28,implies(implies(X_26,X_27),implies(X_27,implies(X_26,X_27)))))
| is_a_theorem(implies(implies(X_26,X_27),implies(X_27,implies(X_26,X_27)))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(X_28)),bind(Y,$fot(implies(implies(X_26,X_27),implies(X_27,implies(X_26,X_27)))))]]) ).
cnf(refute_0_19,plain,
is_a_theorem(implies(implies(implies(implies(X_8,X_21),implies(U,X_21)),implies(X_21,implies(U,X_21))),implies(implies(U,X_21),implies(X_21,implies(U,X_21))))),
inference(subst,[],[refute_0_7:[bind(X,$fot(X_21)),bind(Y,$fot(implies(U,X_21))),bind(X_6,$fot(implies(U,X_21)))]]) ).
cnf(refute_0_20,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_8,X_21),implies(U,X_21)),implies(X_21,implies(U,X_21))),implies(implies(U,X_21),implies(X_21,implies(U,X_21)))))
| is_a_theorem(implies(X_24,implies(implies(U,X_21),implies(X_21,implies(U,X_21))))) ),
inference(subst,[],[refute_0_12:[bind(X_10,$fot(X_21)),bind(X_11,$fot(implies(U,X_21))),bind(X_12,$fot(implies(X_21,implies(U,X_21)))),bind(X_13,$fot(X_24)),bind(X_14,$fot(implies(X_8,X_21)))]]) ).
cnf(refute_0_21,plain,
is_a_theorem(implies(X_24,implies(implies(U,X_21),implies(X_21,implies(U,X_21))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_8,X_21),implies(U,X_21)),implies(X_21,implies(U,X_21))),implies(implies(U,X_21),implies(X_21,implies(U,X_21))))) )],[refute_0_19,refute_0_20]) ).
cnf(refute_0_22,plain,
is_a_theorem(implies(X_28,implies(implies(X_26,X_27),implies(X_27,implies(X_26,X_27))))),
inference(subst,[],[refute_0_21:[bind(U,$fot(X_26)),bind(X_21,$fot(X_27)),bind(X_24,$fot(X_28))]]) ).
cnf(refute_0_23,plain,
( ~ is_a_theorem(X_28)
| is_a_theorem(implies(implies(X_26,X_27),implies(X_27,implies(X_26,X_27)))) ),
inference(resolve,[$cnf( is_a_theorem(implies(X_28,implies(implies(X_26,X_27),implies(X_27,implies(X_26,X_27))))) )],[refute_0_22,refute_0_18]) ).
cnf(refute_0_24,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_29,X_29),implies(implies(X_30,X_29),implies(X_29,X_29))),X),implies(U,X)))
| is_a_theorem(implies(implies(X_44,X_45),implies(X_45,implies(X_44,X_45)))) ),
inference(subst,[],[refute_0_23:[bind(X_26,$fot(X_44)),bind(X_27,$fot(X_45)),bind(X_28,$fot(implies(implies(implies(implies(X_29,X_29),implies(implies(X_30,X_29),implies(X_29,X_29))),X),implies(U,X))))]]) ).
cnf(refute_0_25,plain,
is_a_theorem(implies(implies(X_44,X_45),implies(X_45,implies(X_44,X_45)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_29,X_29),implies(implies(X_30,X_29),implies(X_29,X_29))),X),implies(U,X))) )],[refute_0_16,refute_0_24]) ).
cnf(refute_0_26,plain,
is_a_theorem(implies(implies(X_47,X_48),implies(X_48,implies(X_47,X_48)))),
inference(subst,[],[refute_0_25:[bind(X_44,$fot(X_47)),bind(X_45,$fot(X_48))]]) ).
cnf(refute_0_27,plain,
( ~ is_a_theorem(implies(X_47,X_48))
| is_a_theorem(implies(X_48,implies(X_47,X_48))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_47,X_48),implies(X_48,implies(X_47,X_48)))) )],[refute_0_26,refute_0_17]) ).
cnf(refute_0_28,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_29,X_29),implies(implies(X_30,X_29),implies(X_29,X_29))),X),implies(U,X)))
| is_a_theorem(implies(implies(U,X),implies(implies(implies(implies(X_29,X_29),implies(implies(X_30,X_29),implies(X_29,X_29))),X),implies(U,X)))) ),
inference(subst,[],[refute_0_27:[bind(X_47,$fot(implies(implies(implies(X_29,X_29),implies(implies(X_30,X_29),implies(X_29,X_29))),X))),bind(X_48,$fot(implies(U,X)))]]) ).
cnf(refute_0_29,plain,
is_a_theorem(implies(implies(U,X),implies(implies(implies(implies(X_29,X_29),implies(implies(X_30,X_29),implies(X_29,X_29))),X),implies(U,X)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_29,X_29),implies(implies(X_30,X_29),implies(X_29,X_29))),X),implies(U,X))) )],[refute_0_16,refute_0_28]) ).
cnf(refute_0_30,plain,
is_a_theorem(implies(implies(X_220,X_221),implies(implies(implies(implies(X_222,X_222),implies(implies(X_223,X_222),implies(X_222,X_222))),X_221),implies(X_220,X_221)))),
inference(subst,[],[refute_0_29:[bind(U,$fot(X_220)),bind(X,$fot(X_221)),bind(X_29,$fot(X_222)),bind(X_30,$fot(X_223))]]) ).
cnf(refute_0_31,plain,
is_a_theorem(implies(implies(implies(implies(implies(implies(X_222,X_222),implies(implies(X_223,X_222),implies(X_222,X_222))),X_221),implies(X_220,X_221)),X_220),implies(U,X_220))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_220,X_221),implies(implies(implies(implies(X_222,X_222),implies(implies(X_223,X_222),implies(X_222,X_222))),X_221),implies(X_220,X_221)))) )],[refute_0_30,refute_0_2]) ).
cnf(refute_0_32,plain,
( ~ is_a_theorem(X_471)
| ~ is_a_theorem(implies(X_471,implies(X_472,implies(X_470,X_472))))
| is_a_theorem(implies(X_472,implies(X_470,X_472))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(X_471)),bind(Y,$fot(implies(X_472,implies(X_470,X_472))))]]) ).
cnf(refute_0_33,plain,
( ~ is_a_theorem(implies(implies(implies(X_467,X_467),implies(X_10,X_467)),implies(X_467,implies(X_10,X_467))))
| is_a_theorem(implies(X_13,implies(X_467,implies(X_10,X_467)))) ),
inference(subst,[],[refute_0_12:[bind(X_11,$fot(X_467)),bind(X_12,$fot(implies(X_10,X_467))),bind(X_14,$fot(X_467))]]) ).
cnf(refute_0_34,plain,
( ~ is_a_theorem(implies(implies(X_466,X_465),implies(X_465,X_465)))
| is_a_theorem(implies(implies(implies(X_465,X_465),X_466),implies(U,X_466))) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(X_466)),bind(Y,$fot(X_465)),bind(Z,$fot(implies(X_465,X_465)))]]) ).
cnf(refute_0_35,plain,
( ~ is_a_theorem(X_451)
| ~ is_a_theorem(implies(X_451,implies(implies(X_453,X_452),implies(X_452,X_452))))
| is_a_theorem(implies(implies(X_453,X_452),implies(X_452,X_452))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(X_451)),bind(Y,$fot(implies(implies(X_453,X_452),implies(X_452,X_452))))]]) ).
cnf(refute_0_36,plain,
is_a_theorem(implies(implies(implies(implies(implies(implies(X_222,X_222),implies(implies(X_223,X_222),implies(X_222,X_222))),X_221),implies(implies(X_446,X_446),X_221)),implies(X_446,X_446)),implies(implies(X_450,X_446),implies(X_446,X_446)))),
inference(subst,[],[refute_0_31:[bind(U,$fot(implies(X_450,X_446))),bind(X_220,$fot(implies(X_446,X_446)))]]) ).
cnf(refute_0_37,plain,
( ~ is_a_theorem(implies(implies(X_19,implies(X_17,X_18)),implies(implies(X_20,X_17),implies(X_16,X_17))))
| ~ is_a_theorem(implies(implies(implies(X_19,implies(X_17,X_18)),implies(implies(X_20,X_17),implies(X_16,X_17))),implies(X_15,implies(implies(X_20,X_17),implies(X_16,X_17)))))
| is_a_theorem(implies(X_15,implies(implies(X_20,X_17),implies(X_16,X_17)))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_19,implies(X_17,X_18)),implies(implies(X_20,X_17),implies(X_16,X_17))))),bind(Y,$fot(implies(X_15,implies(implies(X_20,X_17),implies(X_16,X_17)))))]]) ).
cnf(refute_0_38,plain,
is_a_theorem(implies(implies(implies(X_19,implies(X_17,X_18)),implies(implies(X_20,X_17),implies(X_16,X_17))),implies(X_15,implies(implies(X_20,X_17),implies(X_16,X_17))))),
inference(subst,[],[refute_0_9:[bind(U,$fot(X_15)),bind(X_10,$fot(X_16)),bind(X_11,$fot(X_17)),bind(X_12,$fot(X_18)),bind(X_13,$fot(X_19)),bind(X_14,$fot(X_20))]]) ).
cnf(refute_0_39,plain,
( ~ is_a_theorem(implies(implies(X_19,implies(X_17,X_18)),implies(implies(X_20,X_17),implies(X_16,X_17))))
| is_a_theorem(implies(X_15,implies(implies(X_20,X_17),implies(X_16,X_17)))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_19,implies(X_17,X_18)),implies(implies(X_20,X_17),implies(X_16,X_17))),implies(X_15,implies(implies(X_20,X_17),implies(X_16,X_17))))) )],[refute_0_38,refute_0_37]) ).
cnf(refute_0_40,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(implies(X_222,X_222),implies(implies(X_223,X_222),implies(X_222,X_222))),X_221),implies(implies(X_446,X_446),X_221)),implies(X_446,X_446)),implies(implies(X_450,X_446),implies(X_446,X_446))))
| is_a_theorem(implies(X_445,implies(implies(X_450,X_446),implies(X_446,X_446)))) ),
inference(subst,[],[refute_0_39:[bind(X_15,$fot(X_445)),bind(X_16,$fot(X_446)),bind(X_17,$fot(X_446)),bind(X_18,$fot(X_446)),bind(X_19,$fot(implies(implies(implies(implies(X_222,X_222),implies(implies(X_223,X_222),implies(X_222,X_222))),X_221),implies(implies(X_446,X_446),X_221)))),bind(X_20,$fot(X_450))]]) ).
cnf(refute_0_41,plain,
is_a_theorem(implies(X_445,implies(implies(X_450,X_446),implies(X_446,X_446)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(implies(X_222,X_222),implies(implies(X_223,X_222),implies(X_222,X_222))),X_221),implies(implies(X_446,X_446),X_221)),implies(X_446,X_446)),implies(implies(X_450,X_446),implies(X_446,X_446)))) )],[refute_0_36,refute_0_40]) ).
cnf(refute_0_42,plain,
is_a_theorem(implies(X_451,implies(implies(X_453,X_452),implies(X_452,X_452)))),
inference(subst,[],[refute_0_41:[bind(X_445,$fot(X_451)),bind(X_446,$fot(X_452)),bind(X_450,$fot(X_453))]]) ).
cnf(refute_0_43,plain,
( ~ is_a_theorem(X_451)
| is_a_theorem(implies(implies(X_453,X_452),implies(X_452,X_452))) ),
inference(resolve,[$cnf( is_a_theorem(implies(X_451,implies(implies(X_453,X_452),implies(X_452,X_452)))) )],[refute_0_42,refute_0_35]) ).
cnf(refute_0_44,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(implies(X_222,X_222),implies(implies(X_223,X_222),implies(X_222,X_222))),X_221),implies(X_220,X_221)),X_220),implies(U,X_220)))
| is_a_theorem(implies(implies(X_464,X_463),implies(X_463,X_463))) ),
inference(subst,[],[refute_0_43:[bind(X_451,$fot(implies(implies(implies(implies(implies(implies(X_222,X_222),implies(implies(X_223,X_222),implies(X_222,X_222))),X_221),implies(X_220,X_221)),X_220),implies(U,X_220)))),bind(X_452,$fot(X_463)),bind(X_453,$fot(X_464))]]) ).
cnf(refute_0_45,plain,
is_a_theorem(implies(implies(X_464,X_463),implies(X_463,X_463))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(implies(X_222,X_222),implies(implies(X_223,X_222),implies(X_222,X_222))),X_221),implies(X_220,X_221)),X_220),implies(U,X_220))) )],[refute_0_31,refute_0_44]) ).
cnf(refute_0_46,plain,
is_a_theorem(implies(implies(X_466,X_465),implies(X_465,X_465))),
inference(subst,[],[refute_0_45:[bind(X_463,$fot(X_465)),bind(X_464,$fot(X_466))]]) ).
cnf(refute_0_47,plain,
is_a_theorem(implies(implies(implies(X_465,X_465),X_466),implies(U,X_466))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_466,X_465),implies(X_465,X_465))) )],[refute_0_46,refute_0_34]) ).
cnf(refute_0_48,plain,
is_a_theorem(implies(implies(implies(X_467,X_467),implies(X_10,X_467)),implies(X_467,implies(X_10,X_467)))),
inference(subst,[],[refute_0_47:[bind(U,$fot(X_467)),bind(X_465,$fot(X_467)),bind(X_466,$fot(implies(X_10,X_467)))]]) ).
cnf(refute_0_49,plain,
is_a_theorem(implies(X_13,implies(X_467,implies(X_10,X_467)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_467,X_467),implies(X_10,X_467)),implies(X_467,implies(X_10,X_467)))) )],[refute_0_48,refute_0_33]) ).
cnf(refute_0_50,plain,
is_a_theorem(implies(X_471,implies(X_472,implies(X_470,X_472)))),
inference(subst,[],[refute_0_49:[bind(X_10,$fot(X_470)),bind(X_13,$fot(X_471)),bind(X_467,$fot(X_472))]]) ).
cnf(refute_0_51,plain,
( ~ is_a_theorem(X_471)
| is_a_theorem(implies(X_472,implies(X_470,X_472))) ),
inference(resolve,[$cnf( is_a_theorem(implies(X_471,implies(X_472,implies(X_470,X_472)))) )],[refute_0_50,refute_0_32]) ).
cnf(refute_0_52,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(implies(X_222,X_222),implies(implies(X_223,X_222),implies(X_222,X_222))),X_221),implies(X_220,X_221)),X_220),implies(U,X_220)))
| is_a_theorem(implies(X_537,implies(X_535,X_537))) ),
inference(subst,[],[refute_0_51:[bind(X_470,$fot(X_535)),bind(X_471,$fot(implies(implies(implies(implies(implies(implies(X_222,X_222),implies(implies(X_223,X_222),implies(X_222,X_222))),X_221),implies(X_220,X_221)),X_220),implies(U,X_220)))),bind(X_472,$fot(X_537))]]) ).
cnf(refute_0_53,plain,
is_a_theorem(implies(X_537,implies(X_535,X_537))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(implies(X_222,X_222),implies(implies(X_223,X_222),implies(X_222,X_222))),X_221),implies(X_220,X_221)),X_220),implies(U,X_220))) )],[refute_0_31,refute_0_52]) ).
cnf(refute_0_54,plain,
is_a_theorem(implies(a,implies(b,a))),
inference(subst,[],[refute_0_53:[bind(X_535,$fot(b)),bind(X_537,$fot(a))]]) ).
cnf(refute_0_55,plain,
$false,
inference(resolve,[$cnf( is_a_theorem(implies(a,implies(b,a))) )],[refute_0_54,prove_ic_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LCL082-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.05 % Command : metis --show proof --show saturation %s
% 0.16/0.40 % Computer : n004.cluster.edu
% 0.16/0.40 % Model : x86_64 x86_64
% 0.16/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.40 % Memory : 8046.5625MB
% 0.16/0.40 % OS : Linux 6.8.0-71-generic
% 0.16/0.40 % CPULimit : 300
% 0.16/0.40 % WCLimit : 300
% 0.16/0.40 % DateTime : Sat Sep 5 16:31:14 UTC 2026
% 0.16/0.40 % CPUTime :
% 0.19/0.41 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.42/0.68 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.42/0.68
% 0.42/0.68 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 0.47/0.72
%------------------------------------------------------------------------------