%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : LCL982+1 : TPTP v9.3.1. Released v9.1.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:43:54 PM UTC 2026
% Result : Theorem 0.12s 0.38s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 3
% Syntax : Number of formulae : 35 ( 22 unt; 0 def)
% Number of atoms : 54 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 42 ( 23 ~; 19 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 16 ( 3 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 184 ( 40 sgn 30 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(condensed_detachment,axiom,
! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) ).
fof(a5,axiom,
! [A,B,C,D,E] : is_a_theorem(implies(implies(A,B),implies(implies(implies(C,implies(D,E)),implies(B,implies(not(D),not(A)))),implies(A,D)))) ).
fof(prove_cn_1,conjecture,
! [A,B,C] : is_a_theorem(implies(implies(A,B),implies(implies(B,C),implies(A,C)))) ).
fof(subgoal_0,plain,
! [A,B,C] : is_a_theorem(implies(implies(A,B),implies(implies(B,C),implies(A,C)))),
inference(strip,[],[prove_cn_1]) ).
fof(negate_0_0,plain,
~ ! [A,B,C] : is_a_theorem(implies(implies(A,B),implies(implies(B,C),implies(A,C)))),
inference(negate,[],[subgoal_0]) ).
fof(normalize_0_0,plain,
? [A,B,C] : ~ is_a_theorem(implies(implies(A,B),implies(implies(B,C),implies(A,C)))),
inference(canonicalize,[],[negate_0_0]) ).
fof(normalize_0_1,plain,
~ is_a_theorem(implies(implies(skolemFOFtoCNF_A,skolemFOFtoCNF_B),implies(implies(skolemFOFtoCNF_B,skolemFOFtoCNF_C),implies(skolemFOFtoCNF_A,skolemFOFtoCNF_C)))),
inference(skolemize,[],[normalize_0_0]) ).
fof(normalize_0_2,plain,
! [X,Y] :
( ~ is_a_theorem(X)
| ~ is_a_theorem(implies(X,Y))
| is_a_theorem(Y) ),
inference(canonicalize,[],[condensed_detachment]) ).
fof(normalize_0_3,plain,
! [X,Y] :
( ~ is_a_theorem(X)
| ~ is_a_theorem(implies(X,Y))
| is_a_theorem(Y) ),
inference(specialize,[],[normalize_0_2]) ).
fof(normalize_0_4,plain,
! [A,B,C,D,E] : is_a_theorem(implies(implies(A,B),implies(implies(implies(C,implies(D,E)),implies(B,implies(not(D),not(A)))),implies(A,D)))),
inference(canonicalize,[],[a5]) ).
fof(normalize_0_5,plain,
! [A,B,C,D,E] : is_a_theorem(implies(implies(A,B),implies(implies(implies(C,implies(D,E)),implies(B,implies(not(D),not(A)))),implies(A,D)))),
inference(specialize,[],[normalize_0_4]) ).
cnf(refute_0_0,plain,
~ is_a_theorem(implies(implies(skolemFOFtoCNF_A,skolemFOFtoCNF_B),implies(implies(skolemFOFtoCNF_B,skolemFOFtoCNF_C),implies(skolemFOFtoCNF_A,skolemFOFtoCNF_C)))),
inference(canonicalize,[],[normalize_0_1]) ).
cnf(refute_0_1,plain,
( ~ is_a_theorem(X)
| ~ is_a_theorem(implies(X,Y))
| is_a_theorem(Y) ),
inference(canonicalize,[],[normalize_0_3]) ).
cnf(refute_0_2,plain,
( ~ is_a_theorem(implies(implies(X_19,implies(X_17,X_18)),implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),implies(not(X_17),not(implies(X_12,X_13))))))
| ~ is_a_theorem(implies(implies(implies(X_19,implies(X_17,X_18)),implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),implies(not(X_17),not(implies(X_12,X_13))))),implies(implies(X_12,X_13),X_17)))
| is_a_theorem(implies(implies(X_12,X_13),X_17)) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(implies(implies(X_19,implies(X_17,X_18)),implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),implies(not(X_17),not(implies(X_12,X_13))))))),bind(Y,$fot(implies(implies(X_12,X_13),X_17)))]]) ).
cnf(refute_0_3,plain,
is_a_theorem(implies(implies(A,B),implies(implies(implies(C,implies(D,E)),implies(B,implies(not(D),not(A)))),implies(A,D)))),
inference(canonicalize,[],[normalize_0_5]) ).
cnf(refute_0_4,plain,
( ~ is_a_theorem(implies(X_2,X_3))
| ~ is_a_theorem(implies(implies(X_2,X_3),implies(implies(implies(X_4,implies(X_5,X_6)),implies(X_3,implies(not(X_5),not(X_2)))),implies(X_2,X_5))))
| is_a_theorem(implies(implies(implies(X_4,implies(X_5,X_6)),implies(X_3,implies(not(X_5),not(X_2)))),implies(X_2,X_5))) ),
inference(subst,[],[refute_0_1:[bind(X,$fot(implies(X_2,X_3))),bind(Y,$fot(implies(implies(implies(X_4,implies(X_5,X_6)),implies(X_3,implies(not(X_5),not(X_2)))),implies(X_2,X_5))))]]) ).
cnf(refute_0_5,plain,
is_a_theorem(implies(implies(X_2,X_3),implies(implies(implies(X_4,implies(X_5,X_6)),implies(X_3,implies(not(X_5),not(X_2)))),implies(X_2,X_5)))),
inference(subst,[],[refute_0_3:[bind(A,$fot(X_2)),bind(B,$fot(X_3)),bind(C,$fot(X_4)),bind(D,$fot(X_5)),bind(E,$fot(X_6))]]) ).
cnf(refute_0_6,plain,
( ~ is_a_theorem(implies(X_2,X_3))
| is_a_theorem(implies(implies(implies(X_4,implies(X_5,X_6)),implies(X_3,implies(not(X_5),not(X_2)))),implies(X_2,X_5))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_2,X_3),implies(implies(implies(X_4,implies(X_5,X_6)),implies(X_3,implies(not(X_5),not(X_2)))),implies(X_2,X_5)))) )],[refute_0_5,refute_0_4]) ).
cnf(refute_0_7,plain,
( ~ is_a_theorem(implies(implies(A,B),implies(implies(implies(C,implies(D,E)),implies(B,implies(not(D),not(A)))),implies(A,D))))
| is_a_theorem(implies(implies(implies(X_9,implies(X_10,X_11)),implies(implies(implies(implies(C,implies(D,E)),implies(B,implies(not(D),not(A)))),implies(A,D)),implies(not(X_10),not(implies(A,B))))),implies(implies(A,B),X_10))) ),
inference(subst,[],[refute_0_6:[bind(X_2,$fot(implies(A,B))),bind(X_3,$fot(implies(implies(implies(C,implies(D,E)),implies(B,implies(not(D),not(A)))),implies(A,D)))),bind(X_4,$fot(X_9)),bind(X_5,$fot(X_10)),bind(X_6,$fot(X_11))]]) ).
cnf(refute_0_8,plain,
is_a_theorem(implies(implies(implies(X_9,implies(X_10,X_11)),implies(implies(implies(implies(C,implies(D,E)),implies(B,implies(not(D),not(A)))),implies(A,D)),implies(not(X_10),not(implies(A,B))))),implies(implies(A,B),X_10))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(A,B),implies(implies(implies(C,implies(D,E)),implies(B,implies(not(D),not(A)))),implies(A,D)))) )],[refute_0_3,refute_0_7]) ).
cnf(refute_0_9,plain,
is_a_theorem(implies(implies(implies(X_19,implies(X_17,X_18)),implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),implies(not(X_17),not(implies(X_12,X_13))))),implies(implies(X_12,X_13),X_17))),
inference(subst,[],[refute_0_8:[bind(A,$fot(X_12)),bind(B,$fot(X_13)),bind(C,$fot(X_14)),bind(D,$fot(X_15)),bind(E,$fot(X_16)),bind(X_10,$fot(X_17)),bind(X_11,$fot(X_18)),bind(X_9,$fot(X_19))]]) ).
cnf(refute_0_10,plain,
( ~ is_a_theorem(implies(implies(X_19,implies(X_17,X_18)),implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),implies(not(X_17),not(implies(X_12,X_13))))))
| is_a_theorem(implies(implies(X_12,X_13),X_17)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_19,implies(X_17,X_18)),implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),implies(not(X_17),not(implies(X_12,X_13))))),implies(implies(X_12,X_13),X_17))) )],[refute_0_9,refute_0_2]) ).
cnf(refute_0_11,plain,
( ~ is_a_theorem(implies(implies(implies(X_54,implies(implies(not(implies(implies(X_53,X_55),implies(X_12,X_55))),not(implies(X_12,X_53))),X_61)),implies(implies(implies(X_53,X_55),implies(X_12,X_55)),implies(not(implies(not(implies(implies(X_53,X_55),implies(X_12,X_55))),not(implies(X_12,X_53)))),not(implies(implies(implies(implies(X_56,implies(implies(not(X_55),not(X_12)),X_58)),implies(X_55,implies(not(implies(not(X_55),not(X_12))),not(X_53)))),implies(X_53,implies(not(X_55),not(X_12)))),implies(X_12,X_55)))))),implies(implies(implies(implies(implies(X_56,implies(implies(not(X_55),not(X_12)),X_58)),implies(X_55,implies(not(implies(not(X_55),not(X_12))),not(X_53)))),implies(X_53,implies(not(X_55),not(X_12)))),implies(X_12,X_55)),implies(not(implies(implies(X_53,X_55),implies(X_12,X_55))),not(implies(X_12,X_53))))))
| is_a_theorem(implies(implies(X_12,X_53),implies(implies(X_53,X_55),implies(X_12,X_55)))) ),
inference(subst,[],[refute_0_10:[bind(X_13,$fot(X_53)),bind(X_14,$fot(implies(X_56,implies(implies(not(X_55),not(X_12)),X_58)))),bind(X_15,$fot(X_55)),bind(X_16,$fot(implies(not(implies(not(X_55),not(X_12))),not(X_53)))),bind(X_17,$fot(implies(implies(X_53,X_55),implies(X_12,X_55)))),bind(X_18,$fot(implies(not(implies(not(implies(implies(X_53,X_55),implies(X_12,X_55))),not(implies(X_12,X_53)))),not(implies(implies(implies(implies(X_56,implies(implies(not(X_55),not(X_12)),X_58)),implies(X_55,implies(not(implies(not(X_55),not(X_12))),not(X_53)))),implies(X_53,implies(not(X_55),not(X_12)))),implies(X_12,X_55)))))),bind(X_19,$fot(implies(X_54,implies(implies(not(implies(implies(X_53,X_55),implies(X_12,X_55))),not(implies(X_12,X_53))),X_61))))]]) ).
cnf(refute_0_12,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(X_41,implies(X_42,X_43)),implies(X_40,implies(not(X_42),not(X_39)))),implies(X_39,X_42)),X_44),implies(implies(X_39,X_40),X_44)))
| is_a_theorem(implies(implies(implies(X_4,implies(X_5,X_6)),implies(implies(implies(X_39,X_40),X_44),implies(not(X_5),not(implies(implies(implies(implies(X_41,implies(X_42,X_43)),implies(X_40,implies(not(X_42),not(X_39)))),implies(X_39,X_42)),X_44))))),implies(implies(implies(implies(implies(X_41,implies(X_42,X_43)),implies(X_40,implies(not(X_42),not(X_39)))),implies(X_39,X_42)),X_44),X_5))) ),
inference(subst,[],[refute_0_6:[bind(X_2,$fot(implies(implies(implies(implies(X_41,implies(X_42,X_43)),implies(X_40,implies(not(X_42),not(X_39)))),implies(X_39,X_42)),X_44))),bind(X_3,$fot(implies(implies(X_39,X_40),X_44)))]]) ).
cnf(refute_0_13,plain,
( ~ is_a_theorem(implies(implies(implies(X_19,implies(X_17,X_18)),implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),implies(not(X_17),not(implies(X_12,X_13))))),implies(implies(X_12,X_13),X_17)))
| is_a_theorem(implies(implies(implies(X_4,implies(X_5,X_6)),implies(implies(implies(X_12,X_13),X_17),implies(not(X_5),not(implies(implies(X_19,implies(X_17,X_18)),implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),implies(not(X_17),not(implies(X_12,X_13))))))))),implies(implies(implies(X_19,implies(X_17,X_18)),implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),implies(not(X_17),not(implies(X_12,X_13))))),X_5))) ),
inference(subst,[],[refute_0_6:[bind(X_2,$fot(implies(implies(X_19,implies(X_17,X_18)),implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),implies(not(X_17),not(implies(X_12,X_13))))))),bind(X_3,$fot(implies(implies(X_12,X_13),X_17)))]]) ).
cnf(refute_0_14,plain,
is_a_theorem(implies(implies(implies(X_4,implies(X_5,X_6)),implies(implies(implies(X_12,X_13),X_17),implies(not(X_5),not(implies(implies(X_19,implies(X_17,X_18)),implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),implies(not(X_17),not(implies(X_12,X_13))))))))),implies(implies(implies(X_19,implies(X_17,X_18)),implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),implies(not(X_17),not(implies(X_12,X_13))))),X_5))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_19,implies(X_17,X_18)),implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),implies(not(X_17),not(implies(X_12,X_13))))),implies(implies(X_12,X_13),X_17))) )],[refute_0_9,refute_0_13]) ).
cnf(refute_0_15,plain,
is_a_theorem(implies(implies(implies(X_4,implies(implies(not(implies(implies(X_12,X_13),X_32)),not(implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),X_32))),X_6)),implies(implies(implies(X_12,X_13),X_32),implies(not(implies(not(implies(implies(X_12,X_13),X_32)),not(implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),X_32)))),not(implies(implies(implies(X_33,implies(implies(not(X_32),not(implies(X_12,X_13))),X_35)),implies(X_32,implies(not(implies(not(X_32),not(implies(X_12,X_13)))),not(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)))))),implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),implies(not(X_32),not(implies(X_12,X_13))))))))),implies(implies(implies(implies(X_33,implies(implies(not(X_32),not(implies(X_12,X_13))),X_35)),implies(X_32,implies(not(implies(not(X_32),not(implies(X_12,X_13)))),not(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)))))),implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),implies(not(X_32),not(implies(X_12,X_13))))),implies(not(implies(implies(X_12,X_13),X_32)),not(implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),X_32)))))),
inference(subst,[],[refute_0_14:[bind(X_17,$fot(X_32)),bind(X_18,$fot(implies(not(implies(not(X_32),not(implies(X_12,X_13)))),not(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)))))),bind(X_19,$fot(implies(X_33,implies(implies(not(X_32),not(implies(X_12,X_13))),X_35)))),bind(X_5,$fot(implies(not(implies(implies(X_12,X_13),X_32)),not(implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),X_32)))))]]) ).
cnf(refute_0_16,plain,
( ~ is_a_theorem(implies(implies(implies(X_4,implies(implies(not(implies(implies(X_12,X_13),X_32)),not(implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),X_32))),X_6)),implies(implies(implies(X_12,X_13),X_32),implies(not(implies(not(implies(implies(X_12,X_13),X_32)),not(implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),X_32)))),not(implies(implies(implies(X_33,implies(implies(not(X_32),not(implies(X_12,X_13))),X_35)),implies(X_32,implies(not(implies(not(X_32),not(implies(X_12,X_13)))),not(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)))))),implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),implies(not(X_32),not(implies(X_12,X_13))))))))),implies(implies(implies(implies(X_33,implies(implies(not(X_32),not(implies(X_12,X_13))),X_35)),implies(X_32,implies(not(implies(not(X_32),not(implies(X_12,X_13)))),not(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)))))),implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),implies(not(X_32),not(implies(X_12,X_13))))),implies(not(implies(implies(X_12,X_13),X_32)),not(implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),X_32))))))
| is_a_theorem(implies(implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),X_32),implies(implies(X_12,X_13),X_32))) ),
inference(subst,[],[refute_0_10:[bind(X_12,$fot(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)))),bind(X_13,$fot(X_32)),bind(X_14,$fot(X_33)),bind(X_15,$fot(implies(not(X_32),not(implies(X_12,X_13))))),bind(X_16,$fot(X_35)),bind(X_17,$fot(implies(implies(X_12,X_13),X_32))),bind(X_18,$fot(implies(not(implies(not(implies(implies(X_12,X_13),X_32)),not(implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),X_32)))),not(implies(implies(implies(X_33,implies(implies(not(X_32),not(implies(X_12,X_13))),X_35)),implies(X_32,implies(not(implies(not(X_32),not(implies(X_12,X_13)))),not(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)))))),implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),implies(not(X_32),not(implies(X_12,X_13))))))))),bind(X_19,$fot(implies(X_4,implies(implies(not(implies(implies(X_12,X_13),X_32)),not(implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),X_32))),X_6))))]]) ).
cnf(refute_0_17,plain,
is_a_theorem(implies(implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),X_32),implies(implies(X_12,X_13),X_32))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_4,implies(implies(not(implies(implies(X_12,X_13),X_32)),not(implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),X_32))),X_6)),implies(implies(implies(X_12,X_13),X_32),implies(not(implies(not(implies(implies(X_12,X_13),X_32)),not(implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),X_32)))),not(implies(implies(implies(X_33,implies(implies(not(X_32),not(implies(X_12,X_13))),X_35)),implies(X_32,implies(not(implies(not(X_32),not(implies(X_12,X_13)))),not(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)))))),implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),implies(not(X_32),not(implies(X_12,X_13))))))))),implies(implies(implies(implies(X_33,implies(implies(not(X_32),not(implies(X_12,X_13))),X_35)),implies(X_32,implies(not(implies(not(X_32),not(implies(X_12,X_13)))),not(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)))))),implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),implies(not(X_32),not(implies(X_12,X_13))))),implies(not(implies(implies(X_12,X_13),X_32)),not(implies(implies(implies(implies(X_14,implies(X_15,X_16)),implies(X_13,implies(not(X_15),not(X_12)))),implies(X_12,X_15)),X_32)))))) )],[refute_0_15,refute_0_16]) ).
cnf(refute_0_18,plain,
is_a_theorem(implies(implies(implies(implies(implies(X_41,implies(X_42,X_43)),implies(X_40,implies(not(X_42),not(X_39)))),implies(X_39,X_42)),X_44),implies(implies(X_39,X_40),X_44))),
inference(subst,[],[refute_0_17:[bind(X_12,$fot(X_39)),bind(X_13,$fot(X_40)),bind(X_14,$fot(X_41)),bind(X_15,$fot(X_42)),bind(X_16,$fot(X_43)),bind(X_32,$fot(X_44))]]) ).
cnf(refute_0_19,plain,
is_a_theorem(implies(implies(implies(X_4,implies(X_5,X_6)),implies(implies(implies(X_39,X_40),X_44),implies(not(X_5),not(implies(implies(implies(implies(X_41,implies(X_42,X_43)),implies(X_40,implies(not(X_42),not(X_39)))),implies(X_39,X_42)),X_44))))),implies(implies(implies(implies(implies(X_41,implies(X_42,X_43)),implies(X_40,implies(not(X_42),not(X_39)))),implies(X_39,X_42)),X_44),X_5))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(X_41,implies(X_42,X_43)),implies(X_40,implies(not(X_42),not(X_39)))),implies(X_39,X_42)),X_44),implies(implies(X_39,X_40),X_44))) )],[refute_0_18,refute_0_12]) ).
cnf(refute_0_20,plain,
is_a_theorem(implies(implies(implies(X_54,implies(implies(not(implies(implies(X_53,X_55),implies(X_12,X_55))),not(implies(X_12,X_53))),X_61)),implies(implies(implies(X_53,X_55),implies(X_12,X_55)),implies(not(implies(not(implies(implies(X_53,X_55),implies(X_12,X_55))),not(implies(X_12,X_53)))),not(implies(implies(implies(implies(X_56,implies(implies(not(X_55),not(X_12)),X_58)),implies(X_55,implies(not(implies(not(X_55),not(X_12))),not(X_53)))),implies(X_53,implies(not(X_55),not(X_12)))),implies(X_12,X_55)))))),implies(implies(implies(implies(implies(X_56,implies(implies(not(X_55),not(X_12)),X_58)),implies(X_55,implies(not(implies(not(X_55),not(X_12))),not(X_53)))),implies(X_53,implies(not(X_55),not(X_12)))),implies(X_12,X_55)),implies(not(implies(implies(X_53,X_55),implies(X_12,X_55))),not(implies(X_12,X_53)))))),
inference(subst,[],[refute_0_19:[bind(X_39,$fot(X_53)),bind(X_4,$fot(X_54)),bind(X_40,$fot(X_55)),bind(X_41,$fot(X_56)),bind(X_42,$fot(implies(not(X_55),not(X_12)))),bind(X_43,$fot(X_58)),bind(X_44,$fot(implies(X_12,X_55))),bind(X_5,$fot(implies(not(implies(implies(X_53,X_55),implies(X_12,X_55))),not(implies(X_12,X_53))))),bind(X_6,$fot(X_61))]]) ).
cnf(refute_0_21,plain,
is_a_theorem(implies(implies(X_12,X_53),implies(implies(X_53,X_55),implies(X_12,X_55)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_54,implies(implies(not(implies(implies(X_53,X_55),implies(X_12,X_55))),not(implies(X_12,X_53))),X_61)),implies(implies(implies(X_53,X_55),implies(X_12,X_55)),implies(not(implies(not(implies(implies(X_53,X_55),implies(X_12,X_55))),not(implies(X_12,X_53)))),not(implies(implies(implies(implies(X_56,implies(implies(not(X_55),not(X_12)),X_58)),implies(X_55,implies(not(implies(not(X_55),not(X_12))),not(X_53)))),implies(X_53,implies(not(X_55),not(X_12)))),implies(X_12,X_55)))))),implies(implies(implies(implies(implies(X_56,implies(implies(not(X_55),not(X_12)),X_58)),implies(X_55,implies(not(implies(not(X_55),not(X_12))),not(X_53)))),implies(X_53,implies(not(X_55),not(X_12)))),implies(X_12,X_55)),implies(not(implies(implies(X_53,X_55),implies(X_12,X_55))),not(implies(X_12,X_53)))))) )],[refute_0_20,refute_0_11]) ).
cnf(refute_0_22,plain,
is_a_theorem(implies(implies(skolemFOFtoCNF_A,skolemFOFtoCNF_B),implies(implies(skolemFOFtoCNF_B,skolemFOFtoCNF_C),implies(skolemFOFtoCNF_A,skolemFOFtoCNF_C)))),
inference(subst,[],[refute_0_21:[bind(X_12,$fot(skolemFOFtoCNF_A)),bind(X_53,$fot(skolemFOFtoCNF_B)),bind(X_55,$fot(skolemFOFtoCNF_C))]]) ).
cnf(refute_0_23,plain,
$false,
inference(resolve,[$cnf( is_a_theorem(implies(implies(skolemFOFtoCNF_A,skolemFOFtoCNF_B),implies(implies(skolemFOFtoCNF_B,skolemFOFtoCNF_C),implies(skolemFOFtoCNF_A,skolemFOFtoCNF_C)))) )],[refute_0_22,refute_0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL982+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.03 % Command : metis --show proof --show saturation %s
% 0.08/0.35 % Computer : n004.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 5 16:13:29 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.12/0.38 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.38
% 0.12/0.38 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 0.12/0.40
%------------------------------------------------------------------------------