%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : LCL039-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n018.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:42 PM UTC 2026
% Result : Unsatisfiable 9.66s 9.92s
% Output : CNFRefutation 9.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 8
% Syntax : Number of clauses : 97 ( 54 unt; 0 nHn; 42 RR)
% Number of literals : 151 ( 0 equ; 55 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 4 ( 4 usr; 1 con; 0-2 aty)
% Number of variables : 187 ( 25 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) ).
cnf(cn_18,axiom,
is_a_theorem(implies(X,implies(Y,X))) ).
cnf(cn_35,axiom,
is_a_theorem(implies(implies(X,implies(Y,Z)),implies(implies(X,Y),implies(X,Z)))) ).
cnf(cn_49,axiom,
is_a_theorem(implies(implies(not(X),not(Y)),implies(Y,X))) ).
cnf(necessitation1,axiom,
is_a_theorem(implies(necessary(implies(X,Y)),implies(necessary(X),necessary(Y)))) ).
cnf(necessitation2,axiom,
is_a_theorem(implies(necessary(X),X)) ).
cnf(axiom_of_necessitation,axiom,
( ~ is_a_theorem(X)
| is_a_theorem(necessary(X)) ) ).
cnf(prove_this,negated_conjecture,
~ is_a_theorem(implies(necessary(a),not(necessary(not(a))))) ).
cnf(refute_0_0,plain,
( ~ is_a_theorem(implies(X_432,necessary(X_433)))
| ~ is_a_theorem(implies(implies(X_432,necessary(X_433)),implies(X_432,X_433)))
| is_a_theorem(implies(X_432,X_433)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X_432,necessary(X_433)))),bind(Y,$fot(implies(X_432,X_433)))]]) ).
cnf(refute_0_1,plain,
is_a_theorem(implies(X_113,implies(Y,X_113))),
inference(subst,[],[cn_18:[bind(X,$fot(X_113))]]) ).
cnf(refute_0_2,plain,
( ~ is_a_theorem(X_113)
| ~ is_a_theorem(implies(X_113,implies(Y,X_113)))
| is_a_theorem(implies(Y,X_113)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(X_113)),bind(Y,$fot(implies(Y,X_113)))]]) ).
cnf(refute_0_3,plain,
( ~ is_a_theorem(X_113)
| is_a_theorem(implies(Y,X_113)) ),
inference(resolve,[$cnf( is_a_theorem(implies(X_113,implies(Y,X_113))) )],[refute_0_1,refute_0_2]) ).
cnf(refute_0_4,plain,
( ~ is_a_theorem(implies(necessary(X),X))
| is_a_theorem(implies(X_116,implies(necessary(X),X))) ),
inference(subst,[],[refute_0_3:[bind(Y,$fot(X_116)),bind(X_113,$fot(implies(necessary(X),X)))]]) ).
cnf(refute_0_5,plain,
is_a_theorem(implies(X_116,implies(necessary(X),X))),
inference(resolve,[$cnf( is_a_theorem(implies(necessary(X),X)) )],[necessitation2,refute_0_4]) ).
cnf(refute_0_6,plain,
is_a_theorem(implies(X_427,implies(necessary(X_429),X_429))),
inference(subst,[],[refute_0_5:[bind(X,$fot(X_429)),bind(X_116,$fot(X_427))]]) ).
cnf(refute_0_7,plain,
( ~ is_a_theorem(implies(X,implies(Y,Z)))
| ~ is_a_theorem(implies(implies(X,implies(Y,Z)),implies(implies(X,Y),implies(X,Z))))
| is_a_theorem(implies(implies(X,Y),implies(X,Z))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X,implies(Y,Z)))),bind(Y,$fot(implies(implies(X,Y),implies(X,Z))))]]) ).
cnf(refute_0_8,plain,
( ~ is_a_theorem(implies(X,implies(Y,Z)))
| is_a_theorem(implies(implies(X,Y),implies(X,Z))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X,implies(Y,Z)),implies(implies(X,Y),implies(X,Z)))) )],[cn_35,refute_0_7]) ).
cnf(refute_0_9,plain,
( ~ is_a_theorem(implies(X_427,implies(necessary(X_429),X_429)))
| is_a_theorem(implies(implies(X_427,necessary(X_429)),implies(X_427,X_429))) ),
inference(subst,[],[refute_0_8:[bind(X,$fot(X_427)),bind(Y,$fot(necessary(X_429))),bind(Z,$fot(X_429))]]) ).
cnf(refute_0_10,plain,
is_a_theorem(implies(implies(X_427,necessary(X_429)),implies(X_427,X_429))),
inference(resolve,[$cnf( is_a_theorem(implies(X_427,implies(necessary(X_429),X_429))) )],[refute_0_6,refute_0_9]) ).
cnf(refute_0_11,plain,
is_a_theorem(implies(implies(X_432,necessary(X_433)),implies(X_432,X_433))),
inference(subst,[],[refute_0_10:[bind(X_427,$fot(X_432)),bind(X_429,$fot(X_433))]]) ).
cnf(refute_0_12,plain,
( ~ is_a_theorem(implies(X_432,necessary(X_433)))
| is_a_theorem(implies(X_432,X_433)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_432,necessary(X_433)),implies(X_432,X_433))) )],[refute_0_11,refute_0_0]) ).
cnf(refute_0_13,plain,
( ~ is_a_theorem(implies(necessary(X_9808),necessary(not(necessary(not(X_9808))))))
| is_a_theorem(implies(necessary(X_9808),not(necessary(not(X_9808))))) ),
inference(subst,[],[refute_0_12:[bind(X_432,$fot(necessary(X_9808))),bind(X_433,$fot(not(necessary(not(X_9808)))))]]) ).
cnf(refute_0_14,plain,
( ~ is_a_theorem(implies(necessary(implies(X,Y)),implies(necessary(X),necessary(Y))))
| ~ is_a_theorem(necessary(implies(X,Y)))
| is_a_theorem(implies(necessary(X),necessary(Y))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(necessary(implies(X,Y)))),bind(Y,$fot(implies(necessary(X),necessary(Y))))]]) ).
cnf(refute_0_15,plain,
( ~ is_a_theorem(necessary(implies(X,Y)))
| is_a_theorem(implies(necessary(X),necessary(Y))) ),
inference(resolve,[$cnf( is_a_theorem(implies(necessary(implies(X,Y)),implies(necessary(X),necessary(Y)))) )],[necessitation1,refute_0_14]) ).
cnf(refute_0_16,plain,
( ~ is_a_theorem(necessary(implies(X_9791,not(necessary(not(X_9791))))))
| is_a_theorem(implies(necessary(X_9791),necessary(not(necessary(not(X_9791)))))) ),
inference(subst,[],[refute_0_15:[bind(X,$fot(X_9791)),bind(Y,$fot(not(necessary(not(X_9791)))))]]) ).
cnf(refute_0_17,plain,
( ~ is_a_theorem(implies(X_9781,not(necessary(not(X_9781)))))
| is_a_theorem(necessary(implies(X_9781,not(necessary(not(X_9781)))))) ),
inference(subst,[],[axiom_of_necessitation:[bind(X,$fot(implies(X_9781,not(necessary(not(X_9781))))))]]) ).
cnf(refute_0_18,plain,
( ~ is_a_theorem(implies(implies(not(X),not(Y)),implies(Y,X)))
| ~ is_a_theorem(implies(not(X),not(Y)))
| is_a_theorem(implies(Y,X)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(not(X),not(Y)))),bind(Y,$fot(implies(Y,X)))]]) ).
cnf(refute_0_19,plain,
( ~ is_a_theorem(implies(not(X),not(Y)))
| is_a_theorem(implies(Y,X)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X),not(Y)),implies(Y,X))) )],[cn_49,refute_0_18]) ).
cnf(refute_0_20,plain,
( ~ is_a_theorem(implies(not(not(necessary(not(Y)))),not(Y)))
| is_a_theorem(implies(Y,not(necessary(not(Y))))) ),
inference(subst,[],[refute_0_19:[bind(X,$fot(not(necessary(not(Y)))))]]) ).
cnf(refute_0_21,plain,
( ~ is_a_theorem(implies(not(not(necessary(X_433))),necessary(X_433)))
| is_a_theorem(implies(not(not(necessary(X_433))),X_433)) ),
inference(subst,[],[refute_0_12:[bind(X_432,$fot(not(not(necessary(X_433)))))]]) ).
cnf(refute_0_22,plain,
( ~ is_a_theorem(implies(necessary(implies(implies(X_2360,X_2360),X_2359)),X_2359))
| ~ is_a_theorem(necessary(implies(implies(X_2360,X_2360),X_2359)))
| is_a_theorem(X_2359) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(necessary(implies(implies(X_2360,X_2360),X_2359)))),bind(Y,$fot(X_2359))]]) ).
cnf(refute_0_23,plain,
( ~ is_a_theorem(implies(X_491,X_491))
| is_a_theorem(implies(Y,implies(X_491,X_491))) ),
inference(subst,[],[refute_0_3:[bind(X_113,$fot(implies(X_491,X_491)))]]) ).
cnf(refute_0_24,plain,
( ~ is_a_theorem(implies(implies(not(X),not(Y)),implies(Y,X)))
| is_a_theorem(implies(X_116,implies(implies(not(X),not(Y)),implies(Y,X)))) ),
inference(subst,[],[refute_0_3:[bind(Y,$fot(X_116)),bind(X_113,$fot(implies(implies(not(X),not(Y)),implies(Y,X))))]]) ).
cnf(refute_0_25,plain,
is_a_theorem(implies(X_116,implies(implies(not(X),not(Y)),implies(Y,X)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X),not(Y)),implies(Y,X))) )],[cn_49,refute_0_24]) ).
cnf(refute_0_26,plain,
is_a_theorem(implies(X_490,implies(implies(not(X),not(Y)),implies(Y,X)))),
inference(subst,[],[refute_0_25:[bind(X_116,$fot(X_490))]]) ).
cnf(refute_0_27,plain,
( ~ is_a_theorem(implies(X_431,X_430))
| ~ is_a_theorem(implies(implies(X_431,X_430),implies(X_431,X_431)))
| is_a_theorem(implies(X_431,X_431)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X_431,X_430))),bind(Y,$fot(implies(X_431,X_431)))]]) ).
cnf(refute_0_28,plain,
is_a_theorem(implies(X_429,implies(X_428,X_429))),
inference(subst,[],[cn_18:[bind(X,$fot(X_429)),bind(Y,$fot(X_428))]]) ).
cnf(refute_0_29,plain,
( ~ is_a_theorem(implies(X_429,implies(X_428,X_429)))
| is_a_theorem(implies(implies(X_429,X_428),implies(X_429,X_429))) ),
inference(subst,[],[refute_0_8:[bind(X,$fot(X_429)),bind(Y,$fot(X_428)),bind(Z,$fot(X_429))]]) ).
cnf(refute_0_30,plain,
is_a_theorem(implies(implies(X_429,X_428),implies(X_429,X_429))),
inference(resolve,[$cnf( is_a_theorem(implies(X_429,implies(X_428,X_429))) )],[refute_0_28,refute_0_29]) ).
cnf(refute_0_31,plain,
is_a_theorem(implies(implies(X_431,X_430),implies(X_431,X_431))),
inference(subst,[],[refute_0_30:[bind(X_428,$fot(X_430)),bind(X_429,$fot(X_431))]]) ).
cnf(refute_0_32,plain,
( ~ is_a_theorem(implies(X_431,X_430))
| is_a_theorem(implies(X_431,X_431)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_431,X_430),implies(X_431,X_431))) )],[refute_0_31,refute_0_27]) ).
cnf(refute_0_33,plain,
( ~ is_a_theorem(implies(X_490,implies(implies(not(X),not(Y)),implies(Y,X))))
| is_a_theorem(implies(X_490,X_490)) ),
inference(subst,[],[refute_0_32:[bind(X_430,$fot(implies(implies(not(X),not(Y)),implies(Y,X)))),bind(X_431,$fot(X_490))]]) ).
cnf(refute_0_34,plain,
is_a_theorem(implies(X_490,X_490)),
inference(resolve,[$cnf( is_a_theorem(implies(X_490,implies(implies(not(X),not(Y)),implies(Y,X)))) )],[refute_0_26,refute_0_33]) ).
cnf(refute_0_35,plain,
is_a_theorem(implies(X_491,X_491)),
inference(subst,[],[refute_0_34:[bind(X_490,$fot(X_491))]]) ).
cnf(refute_0_36,plain,
is_a_theorem(implies(Y,implies(X_491,X_491))),
inference(resolve,[$cnf( is_a_theorem(implies(X_491,X_491)) )],[refute_0_35,refute_0_23]) ).
cnf(refute_0_37,plain,
is_a_theorem(implies(necessary(implies(implies(X_491,X_491),X_2358)),implies(X_491,X_491))),
inference(subst,[],[refute_0_36:[bind(Y,$fot(necessary(implies(implies(X_491,X_491),X_2358))))]]) ).
cnf(refute_0_38,plain,
( ~ is_a_theorem(implies(implies(necessary(implies(X_441,X_442)),X_441),implies(necessary(implies(X_441,X_442)),X_442)))
| ~ is_a_theorem(implies(necessary(implies(X_441,X_442)),X_441))
| is_a_theorem(implies(necessary(implies(X_441,X_442)),X_442)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(necessary(implies(X_441,X_442)),X_441))),bind(Y,$fot(implies(necessary(implies(X_441,X_442)),X_442)))]]) ).
cnf(refute_0_39,plain,
is_a_theorem(implies(necessary(implies(X_428,X_429)),implies(X_428,X_429))),
inference(subst,[],[necessitation2:[bind(X,$fot(implies(X_428,X_429)))]]) ).
cnf(refute_0_40,plain,
( ~ is_a_theorem(implies(necessary(implies(X_428,X_429)),implies(X_428,X_429)))
| is_a_theorem(implies(implies(necessary(implies(X_428,X_429)),X_428),implies(necessary(implies(X_428,X_429)),X_429))) ),
inference(subst,[],[refute_0_8:[bind(X,$fot(necessary(implies(X_428,X_429)))),bind(Y,$fot(X_428)),bind(Z,$fot(X_429))]]) ).
cnf(refute_0_41,plain,
is_a_theorem(implies(implies(necessary(implies(X_428,X_429)),X_428),implies(necessary(implies(X_428,X_429)),X_429))),
inference(resolve,[$cnf( is_a_theorem(implies(necessary(implies(X_428,X_429)),implies(X_428,X_429))) )],[refute_0_39,refute_0_40]) ).
cnf(refute_0_42,plain,
is_a_theorem(implies(implies(necessary(implies(X_441,X_442)),X_441),implies(necessary(implies(X_441,X_442)),X_442))),
inference(subst,[],[refute_0_41:[bind(X_428,$fot(X_441)),bind(X_429,$fot(X_442))]]) ).
cnf(refute_0_43,plain,
( ~ is_a_theorem(implies(necessary(implies(X_441,X_442)),X_441))
| is_a_theorem(implies(necessary(implies(X_441,X_442)),X_442)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(necessary(implies(X_441,X_442)),X_441),implies(necessary(implies(X_441,X_442)),X_442))) )],[refute_0_42,refute_0_38]) ).
cnf(refute_0_44,plain,
( ~ is_a_theorem(implies(necessary(implies(implies(X_491,X_491),X_2358)),implies(X_491,X_491)))
| is_a_theorem(implies(necessary(implies(implies(X_491,X_491),X_2358)),X_2358)) ),
inference(subst,[],[refute_0_43:[bind(X_441,$fot(implies(X_491,X_491))),bind(X_442,$fot(X_2358))]]) ).
cnf(refute_0_45,plain,
is_a_theorem(implies(necessary(implies(implies(X_491,X_491),X_2358)),X_2358)),
inference(resolve,[$cnf( is_a_theorem(implies(necessary(implies(implies(X_491,X_491),X_2358)),implies(X_491,X_491))) )],[refute_0_37,refute_0_44]) ).
cnf(refute_0_46,plain,
is_a_theorem(implies(necessary(implies(implies(X_2360,X_2360),X_2359)),X_2359)),
inference(subst,[],[refute_0_45:[bind(X_2358,$fot(X_2359)),bind(X_491,$fot(X_2360))]]) ).
cnf(refute_0_47,plain,
( ~ is_a_theorem(necessary(implies(implies(X_2360,X_2360),X_2359)))
| is_a_theorem(X_2359) ),
inference(resolve,[$cnf( is_a_theorem(implies(necessary(implies(implies(X_2360,X_2360),X_2359)),X_2359)) )],[refute_0_46,refute_0_22]) ).
cnf(refute_0_48,plain,
( ~ is_a_theorem(necessary(implies(implies(not(not(X_9773)),not(not(X_9773))),implies(not(not(X_9773)),X_9773))))
| is_a_theorem(implies(not(not(X_9773)),X_9773)) ),
inference(subst,[],[refute_0_47:[bind(X_2359,$fot(implies(not(not(X_9773)),X_9773))),bind(X_2360,$fot(not(not(X_9773))))]]) ).
cnf(refute_0_49,plain,
( ~ is_a_theorem(implies(necessary(implies(X_254,implies(X_255,X_256))),necessary(implies(implies(X_254,X_255),implies(X_254,X_256)))))
| ~ is_a_theorem(necessary(implies(X_254,implies(X_255,X_256))))
| is_a_theorem(necessary(implies(implies(X_254,X_255),implies(X_254,X_256)))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(necessary(implies(X_254,implies(X_255,X_256))))),bind(Y,$fot(necessary(implies(implies(X_254,X_255),implies(X_254,X_256)))))]]) ).
cnf(refute_0_50,plain,
( ~ is_a_theorem(implies(implies(X_67,implies(X_68,X_69)),implies(implies(X_67,X_68),implies(X_67,X_69))))
| is_a_theorem(necessary(implies(implies(X_67,implies(X_68,X_69)),implies(implies(X_67,X_68),implies(X_67,X_69))))) ),
inference(subst,[],[axiom_of_necessitation:[bind(X,$fot(implies(implies(X_67,implies(X_68,X_69)),implies(implies(X_67,X_68),implies(X_67,X_69)))))]]) ).
cnf(refute_0_51,plain,
is_a_theorem(implies(implies(X_67,implies(X_68,X_69)),implies(implies(X_67,X_68),implies(X_67,X_69)))),
inference(subst,[],[cn_35:[bind(X,$fot(X_67)),bind(Y,$fot(X_68)),bind(Z,$fot(X_69))]]) ).
cnf(refute_0_52,plain,
is_a_theorem(necessary(implies(implies(X_67,implies(X_68,X_69)),implies(implies(X_67,X_68),implies(X_67,X_69))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_67,implies(X_68,X_69)),implies(implies(X_67,X_68),implies(X_67,X_69)))) )],[refute_0_51,refute_0_50]) ).
cnf(refute_0_53,plain,
( ~ is_a_theorem(necessary(implies(implies(X_67,implies(X_68,X_69)),implies(implies(X_67,X_68),implies(X_67,X_69)))))
| is_a_theorem(implies(necessary(implies(X_67,implies(X_68,X_69))),necessary(implies(implies(X_67,X_68),implies(X_67,X_69))))) ),
inference(subst,[],[refute_0_15:[bind(X,$fot(implies(X_67,implies(X_68,X_69)))),bind(Y,$fot(implies(implies(X_67,X_68),implies(X_67,X_69))))]]) ).
cnf(refute_0_54,plain,
is_a_theorem(implies(necessary(implies(X_67,implies(X_68,X_69))),necessary(implies(implies(X_67,X_68),implies(X_67,X_69))))),
inference(resolve,[$cnf( is_a_theorem(necessary(implies(implies(X_67,implies(X_68,X_69)),implies(implies(X_67,X_68),implies(X_67,X_69))))) )],[refute_0_52,refute_0_53]) ).
cnf(refute_0_55,plain,
is_a_theorem(implies(necessary(implies(X_254,implies(X_255,X_256))),necessary(implies(implies(X_254,X_255),implies(X_254,X_256))))),
inference(subst,[],[refute_0_54:[bind(X_67,$fot(X_254)),bind(X_68,$fot(X_255)),bind(X_69,$fot(X_256))]]) ).
cnf(refute_0_56,plain,
( ~ is_a_theorem(necessary(implies(X_254,implies(X_255,X_256))))
| is_a_theorem(necessary(implies(implies(X_254,X_255),implies(X_254,X_256)))) ),
inference(resolve,[$cnf( is_a_theorem(implies(necessary(implies(X_254,implies(X_255,X_256))),necessary(implies(implies(X_254,X_255),implies(X_254,X_256))))) )],[refute_0_55,refute_0_49]) ).
cnf(refute_0_57,plain,
( ~ is_a_theorem(necessary(implies(not(not(X_9428)),implies(X_9429,X_9428))))
| is_a_theorem(necessary(implies(implies(not(not(X_9428)),X_9429),implies(not(not(X_9428)),X_9428)))) ),
inference(subst,[],[refute_0_56:[bind(X_254,$fot(not(not(X_9428)))),bind(X_255,$fot(X_9429)),bind(X_256,$fot(X_9428))]]) ).
cnf(refute_0_58,plain,
( ~ is_a_theorem(implies(not(not(X_9406)),implies(X_9407,X_9406)))
| is_a_theorem(necessary(implies(not(not(X_9406)),implies(X_9407,X_9406)))) ),
inference(subst,[],[axiom_of_necessitation:[bind(X,$fot(implies(not(not(X_9406)),implies(X_9407,X_9406))))]]) ).
cnf(refute_0_59,plain,
( ~ is_a_theorem(implies(X_481,implies(not(X_479),not(X_480))))
| ~ is_a_theorem(implies(implies(X_481,implies(not(X_479),not(X_480))),implies(X_481,implies(X_480,X_479))))
| is_a_theorem(implies(X_481,implies(X_480,X_479))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X_481,implies(not(X_479),not(X_480))))),bind(Y,$fot(implies(X_481,implies(X_480,X_479))))]]) ).
cnf(refute_0_60,plain,
is_a_theorem(implies(X_427,implies(implies(not(X),not(Y)),implies(Y,X)))),
inference(subst,[],[refute_0_25:[bind(X_116,$fot(X_427))]]) ).
cnf(refute_0_61,plain,
( ~ is_a_theorem(implies(X_427,implies(implies(not(X),not(Y)),implies(Y,X))))
| is_a_theorem(implies(implies(X_427,implies(not(X),not(Y))),implies(X_427,implies(Y,X)))) ),
inference(subst,[],[refute_0_8:[bind(X,$fot(X_427)),bind(Y,$fot(implies(not(X),not(Y)))),bind(Z,$fot(implies(Y,X)))]]) ).
cnf(refute_0_62,plain,
is_a_theorem(implies(implies(X_427,implies(not(X),not(Y))),implies(X_427,implies(Y,X)))),
inference(resolve,[$cnf( is_a_theorem(implies(X_427,implies(implies(not(X),not(Y)),implies(Y,X)))) )],[refute_0_60,refute_0_61]) ).
cnf(refute_0_63,plain,
is_a_theorem(implies(implies(X_481,implies(not(X_479),not(X_480))),implies(X_481,implies(X_480,X_479)))),
inference(subst,[],[refute_0_62:[bind(X,$fot(X_479)),bind(Y,$fot(X_480)),bind(X_427,$fot(X_481))]]) ).
cnf(refute_0_64,plain,
( ~ is_a_theorem(implies(X_481,implies(not(X_479),not(X_480))))
| is_a_theorem(implies(X_481,implies(X_480,X_479))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_481,implies(not(X_479),not(X_480))),implies(X_481,implies(X_480,X_479)))) )],[refute_0_63,refute_0_59]) ).
cnf(refute_0_65,plain,
( ~ is_a_theorem(implies(not(not(X_479)),implies(not(X_479),not(X_480))))
| is_a_theorem(implies(not(not(X_479)),implies(X_480,X_479))) ),
inference(subst,[],[refute_0_64:[bind(X_481,$fot(not(not(X_479))))]]) ).
cnf(refute_0_66,plain,
is_a_theorem(implies(not(X_9396),implies(not(X_9395),not(X_9396)))),
inference(subst,[],[cn_18:[bind(X,$fot(not(X_9396))),bind(Y,$fot(not(X_9395)))]]) ).
cnf(refute_0_67,plain,
( ~ is_a_theorem(implies(not(X_9396),implies(not(X_9395),not(X_9396))))
| is_a_theorem(implies(not(X_9396),implies(X_9396,X_9395))) ),
inference(subst,[],[refute_0_64:[bind(X_479,$fot(X_9395)),bind(X_480,$fot(X_9396)),bind(X_481,$fot(not(X_9396)))]]) ).
cnf(refute_0_68,plain,
is_a_theorem(implies(not(X_9396),implies(X_9396,X_9395))),
inference(resolve,[$cnf( is_a_theorem(implies(not(X_9396),implies(not(X_9395),not(X_9396)))) )],[refute_0_66,refute_0_67]) ).
cnf(refute_0_69,plain,
is_a_theorem(implies(not(not(X_479)),implies(not(X_479),not(X_480)))),
inference(subst,[],[refute_0_68:[bind(X_9395,$fot(not(X_480))),bind(X_9396,$fot(not(X_479)))]]) ).
cnf(refute_0_70,plain,
is_a_theorem(implies(not(not(X_479)),implies(X_480,X_479))),
inference(resolve,[$cnf( is_a_theorem(implies(not(not(X_479)),implies(not(X_479),not(X_480)))) )],[refute_0_69,refute_0_65]) ).
cnf(refute_0_71,plain,
is_a_theorem(implies(not(not(X_9406)),implies(X_9407,X_9406))),
inference(subst,[],[refute_0_70:[bind(X_479,$fot(X_9406)),bind(X_480,$fot(X_9407))]]) ).
cnf(refute_0_72,plain,
is_a_theorem(necessary(implies(not(not(X_9406)),implies(X_9407,X_9406)))),
inference(resolve,[$cnf( is_a_theorem(implies(not(not(X_9406)),implies(X_9407,X_9406))) )],[refute_0_71,refute_0_58]) ).
cnf(refute_0_73,plain,
is_a_theorem(necessary(implies(not(not(X_9428)),implies(X_9429,X_9428)))),
inference(subst,[],[refute_0_72:[bind(X_9406,$fot(X_9428)),bind(X_9407,$fot(X_9429))]]) ).
cnf(refute_0_74,plain,
is_a_theorem(necessary(implies(implies(not(not(X_9428)),X_9429),implies(not(not(X_9428)),X_9428)))),
inference(resolve,[$cnf( is_a_theorem(necessary(implies(not(not(X_9428)),implies(X_9429,X_9428)))) )],[refute_0_73,refute_0_57]) ).
cnf(refute_0_75,plain,
is_a_theorem(necessary(implies(implies(not(not(X_9773)),not(not(X_9773))),implies(not(not(X_9773)),X_9773)))),
inference(subst,[],[refute_0_74:[bind(X_9428,$fot(X_9773)),bind(X_9429,$fot(not(not(X_9773))))]]) ).
cnf(refute_0_76,plain,
is_a_theorem(implies(not(not(X_9773)),X_9773)),
inference(resolve,[$cnf( is_a_theorem(necessary(implies(implies(not(not(X_9773)),not(not(X_9773))),implies(not(not(X_9773)),X_9773)))) )],[refute_0_75,refute_0_48]) ).
cnf(refute_0_77,plain,
is_a_theorem(implies(not(not(necessary(X_433))),necessary(X_433))),
inference(subst,[],[refute_0_76:[bind(X_9773,$fot(necessary(X_433)))]]) ).
cnf(refute_0_78,plain,
is_a_theorem(implies(not(not(necessary(X_433))),X_433)),
inference(resolve,[$cnf( is_a_theorem(implies(not(not(necessary(X_433))),necessary(X_433))) )],[refute_0_77,refute_0_21]) ).
cnf(refute_0_79,plain,
is_a_theorem(implies(not(not(necessary(not(Y)))),not(Y))),
inference(subst,[],[refute_0_78:[bind(X_433,$fot(not(Y)))]]) ).
cnf(refute_0_80,plain,
is_a_theorem(implies(Y,not(necessary(not(Y))))),
inference(resolve,[$cnf( is_a_theorem(implies(not(not(necessary(not(Y)))),not(Y))) )],[refute_0_79,refute_0_20]) ).
cnf(refute_0_81,plain,
is_a_theorem(implies(X_9781,not(necessary(not(X_9781))))),
inference(subst,[],[refute_0_80:[bind(Y,$fot(X_9781))]]) ).
cnf(refute_0_82,plain,
is_a_theorem(necessary(implies(X_9781,not(necessary(not(X_9781)))))),
inference(resolve,[$cnf( is_a_theorem(implies(X_9781,not(necessary(not(X_9781))))) )],[refute_0_81,refute_0_17]) ).
cnf(refute_0_83,plain,
is_a_theorem(necessary(implies(X_9791,not(necessary(not(X_9791)))))),
inference(subst,[],[refute_0_82:[bind(X_9781,$fot(X_9791))]]) ).
cnf(refute_0_84,plain,
is_a_theorem(implies(necessary(X_9791),necessary(not(necessary(not(X_9791)))))),
inference(resolve,[$cnf( is_a_theorem(necessary(implies(X_9791,not(necessary(not(X_9791)))))) )],[refute_0_83,refute_0_16]) ).
cnf(refute_0_85,plain,
is_a_theorem(implies(necessary(X_9808),necessary(not(necessary(not(X_9808)))))),
inference(subst,[],[refute_0_84:[bind(X_9791,$fot(X_9808))]]) ).
cnf(refute_0_86,plain,
is_a_theorem(implies(necessary(X_9808),not(necessary(not(X_9808))))),
inference(resolve,[$cnf( is_a_theorem(implies(necessary(X_9808),necessary(not(necessary(not(X_9808)))))) )],[refute_0_85,refute_0_13]) ).
cnf(refute_0_87,plain,
is_a_theorem(implies(necessary(a),not(necessary(not(a))))),
inference(subst,[],[refute_0_86:[bind(X_9808,$fot(a))]]) ).
cnf(refute_0_88,plain,
$false,
inference(resolve,[$cnf( is_a_theorem(implies(necessary(a),not(necessary(not(a))))) )],[refute_0_87,prove_this]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL039-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : metis --show proof --show saturation %s
% 0.10/0.36 % Computer : n018.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 5 00:14:33 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 9.66/9.92 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.66/9.92
% 9.66/9.92 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 9.66/9.95
%------------------------------------------------------------------------------