%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : LCL044-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:43 PM UTC 2026
% Result : Unsatisfiable 3.79s 4.06s
% Output : CNFRefutation 3.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 7
% Syntax : Number of clauses : 38 ( 21 unt; 0 nHn; 16 RR)
% Number of literals : 61 ( 0 equ; 24 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 3 ( 3 usr; 1 con; 0-2 aty)
% Number of variables : 74 ( 10 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) ).
cnf(cn_3,axiom,
is_a_theorem(implies(X,implies(not(X),Y))) ).
cnf(cn_18,axiom,
is_a_theorem(implies(X,implies(Y,X))) ).
cnf(cn_21,axiom,
is_a_theorem(implies(implies(X,implies(Y,Z)),implies(Y,implies(X,Z)))) ).
cnf(cn_22,axiom,
is_a_theorem(implies(implies(Y,Z),implies(implies(X,Y),implies(X,Z)))) ).
cnf(cn_54,axiom,
is_a_theorem(implies(implies(X,Y),implies(implies(not(X),Y),Y))) ).
cnf(prove_cn_40,negated_conjecture,
~ is_a_theorem(implies(a,not(not(a)))) ).
cnf(refute_0_0,plain,
( ~ is_a_theorem(implies(implies(not(X_37),implies(X_36,X_37)),implies(X_36,X_37)))
| ~ is_a_theorem(implies(not(X_37),implies(X_36,X_37)))
| is_a_theorem(implies(X_36,X_37)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(not(X_37),implies(X_36,X_37)))),bind(Y,$fot(implies(X_36,X_37)))]]) ).
cnf(refute_0_1,plain,
is_a_theorem(implies(X_34,implies(Y,X_34))),
inference(subst,[],[cn_18:[bind(X,$fot(X_34))]]) ).
cnf(refute_0_2,plain,
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(implies(implies(X,Y),implies(implies(not(X),Y),Y)))
| is_a_theorem(implies(implies(not(X),Y),Y)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X,Y))),bind(Y,$fot(implies(implies(not(X),Y),Y)))]]) ).
cnf(refute_0_3,plain,
( ~ is_a_theorem(implies(X,Y))
| is_a_theorem(implies(implies(not(X),Y),Y)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X,Y),implies(implies(not(X),Y),Y))) )],[cn_54,refute_0_2]) ).
cnf(refute_0_4,plain,
( ~ is_a_theorem(implies(X_34,implies(Y,X_34)))
| is_a_theorem(implies(implies(not(X_34),implies(Y,X_34)),implies(Y,X_34))) ),
inference(subst,[],[refute_0_3:[bind(X,$fot(X_34)),bind(Y,$fot(implies(Y,X_34)))]]) ).
cnf(refute_0_5,plain,
is_a_theorem(implies(implies(not(X_34),implies(Y,X_34)),implies(Y,X_34))),
inference(resolve,[$cnf( is_a_theorem(implies(X_34,implies(Y,X_34))) )],[refute_0_1,refute_0_4]) ).
cnf(refute_0_6,plain,
is_a_theorem(implies(implies(not(X_37),implies(X_36,X_37)),implies(X_36,X_37))),
inference(subst,[],[refute_0_5:[bind(Y,$fot(X_36)),bind(X_34,$fot(X_37))]]) ).
cnf(refute_0_7,plain,
( ~ is_a_theorem(implies(not(X_37),implies(X_36,X_37)))
| is_a_theorem(implies(X_36,X_37)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_37),implies(X_36,X_37)),implies(X_36,X_37))) )],[refute_0_6,refute_0_0]) ).
cnf(refute_0_8,plain,
( ~ is_a_theorem(implies(not(not(not(X_3058))),implies(X_3058,not(not(X_3058)))))
| is_a_theorem(implies(X_3058,not(not(X_3058)))) ),
inference(subst,[],[refute_0_7:[bind(X_36,$fot(X_3058)),bind(X_37,$fot(not(not(X_3058))))]]) ).
cnf(refute_0_9,plain,
is_a_theorem(implies(not(X_693),implies(not(not(X_693)),X_693))),
inference(subst,[],[cn_3:[bind(X,$fot(not(X_693))),bind(Y,$fot(X_693))]]) ).
cnf(refute_0_10,plain,
( ~ is_a_theorem(implies(not(X_693),implies(not(not(X_693)),X_693)))
| is_a_theorem(implies(not(not(X_693)),X_693)) ),
inference(subst,[],[refute_0_7:[bind(X_36,$fot(not(not(X_693)))),bind(X_37,$fot(X_693))]]) ).
cnf(refute_0_11,plain,
is_a_theorem(implies(not(not(X_693)),X_693)),
inference(resolve,[$cnf( is_a_theorem(implies(not(X_693),implies(not(not(X_693)),X_693))) )],[refute_0_9,refute_0_10]) ).
cnf(refute_0_12,plain,
is_a_theorem(implies(not(not(not(X_3046))),not(X_3046))),
inference(subst,[],[refute_0_11:[bind(X_693,$fot(not(X_3046)))]]) ).
cnf(refute_0_13,plain,
( ~ is_a_theorem(implies(X_188,not(X_189)))
| ~ is_a_theorem(implies(implies(X_188,not(X_189)),implies(X_188,implies(X_189,X_190))))
| is_a_theorem(implies(X_188,implies(X_189,X_190))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X_188,not(X_189)))),bind(Y,$fot(implies(X_188,implies(X_189,X_190))))]]) ).
cnf(refute_0_14,plain,
is_a_theorem(implies(X_70,implies(not(X_70),X_72))),
inference(subst,[],[cn_3:[bind(X,$fot(X_70)),bind(Y,$fot(X_72))]]) ).
cnf(refute_0_15,plain,
( ~ is_a_theorem(implies(X,implies(Y,Z)))
| ~ is_a_theorem(implies(implies(X,implies(Y,Z)),implies(Y,implies(X,Z))))
| is_a_theorem(implies(Y,implies(X,Z))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X,implies(Y,Z)))),bind(Y,$fot(implies(Y,implies(X,Z))))]]) ).
cnf(refute_0_16,plain,
( ~ is_a_theorem(implies(X,implies(Y,Z)))
| is_a_theorem(implies(Y,implies(X,Z))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X,implies(Y,Z)),implies(Y,implies(X,Z)))) )],[cn_21,refute_0_15]) ).
cnf(refute_0_17,plain,
( ~ is_a_theorem(implies(X_70,implies(not(X_70),X_72)))
| is_a_theorem(implies(not(X_70),implies(X_70,X_72))) ),
inference(subst,[],[refute_0_16:[bind(X,$fot(X_70)),bind(Y,$fot(not(X_70))),bind(Z,$fot(X_72))]]) ).
cnf(refute_0_18,plain,
is_a_theorem(implies(not(X_70),implies(X_70,X_72))),
inference(resolve,[$cnf( is_a_theorem(implies(X_70,implies(not(X_70),X_72))) )],[refute_0_14,refute_0_17]) ).
cnf(refute_0_19,plain,
( ~ is_a_theorem(implies(Y,Z))
| ~ is_a_theorem(implies(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(Y,Z))),bind(Y,$fot(implies(implies(X,Y),implies(X,Z))))]]) ).
cnf(refute_0_20,plain,
( ~ is_a_theorem(implies(Y,Z))
| is_a_theorem(implies(implies(X,Y),implies(X,Z))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(Y,Z),implies(implies(X,Y),implies(X,Z)))) )],[cn_22,refute_0_19]) ).
cnf(refute_0_21,plain,
( ~ is_a_theorem(implies(not(X_70),implies(X_70,X_72)))
| is_a_theorem(implies(implies(X_163,not(X_70)),implies(X_163,implies(X_70,X_72)))) ),
inference(subst,[],[refute_0_20:[bind(X,$fot(X_163)),bind(Y,$fot(not(X_70))),bind(Z,$fot(implies(X_70,X_72)))]]) ).
cnf(refute_0_22,plain,
is_a_theorem(implies(implies(X_163,not(X_70)),implies(X_163,implies(X_70,X_72)))),
inference(resolve,[$cnf( is_a_theorem(implies(not(X_70),implies(X_70,X_72))) )],[refute_0_18,refute_0_21]) ).
cnf(refute_0_23,plain,
is_a_theorem(implies(implies(X_188,not(X_189)),implies(X_188,implies(X_189,X_190)))),
inference(subst,[],[refute_0_22:[bind(X_163,$fot(X_188)),bind(X_70,$fot(X_189)),bind(X_72,$fot(X_190))]]) ).
cnf(refute_0_24,plain,
( ~ is_a_theorem(implies(X_188,not(X_189)))
| is_a_theorem(implies(X_188,implies(X_189,X_190))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_188,not(X_189)),implies(X_188,implies(X_189,X_190)))) )],[refute_0_23,refute_0_13]) ).
cnf(refute_0_25,plain,
( ~ is_a_theorem(implies(not(not(not(X_3046))),not(X_3046)))
| is_a_theorem(implies(not(not(not(X_3046))),implies(X_3046,X_3047))) ),
inference(subst,[],[refute_0_24:[bind(X_188,$fot(not(not(not(X_3046))))),bind(X_189,$fot(X_3046)),bind(X_190,$fot(X_3047))]]) ).
cnf(refute_0_26,plain,
is_a_theorem(implies(not(not(not(X_3046))),implies(X_3046,X_3047))),
inference(resolve,[$cnf( is_a_theorem(implies(not(not(not(X_3046))),not(X_3046))) )],[refute_0_12,refute_0_25]) ).
cnf(refute_0_27,plain,
is_a_theorem(implies(not(not(not(X_3058))),implies(X_3058,not(not(X_3058))))),
inference(subst,[],[refute_0_26:[bind(X_3046,$fot(X_3058)),bind(X_3047,$fot(not(not(X_3058))))]]) ).
cnf(refute_0_28,plain,
is_a_theorem(implies(X_3058,not(not(X_3058)))),
inference(resolve,[$cnf( is_a_theorem(implies(not(not(not(X_3058))),implies(X_3058,not(not(X_3058))))) )],[refute_0_27,refute_0_8]) ).
cnf(refute_0_29,plain,
is_a_theorem(implies(a,not(not(a)))),
inference(subst,[],[refute_0_28:[bind(X_3058,$fot(a))]]) ).
cnf(refute_0_30,plain,
$false,
inference(resolve,[$cnf( is_a_theorem(implies(a,not(not(a)))) )],[refute_0_29,prove_cn_40]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL044-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : metis --show proof --show saturation %s
% 0.09/0.35 % Computer : n018.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 5 05:24:03 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.13/0.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 3.79/4.06 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.79/4.06
% 3.79/4.06 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 3.79/4.07
%------------------------------------------------------------------------------