%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : LCL494+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n010.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:42:49 PM UTC 2026
% Result : Theorem 1.05s 1.37s
% Output : CNFRefutation 1.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 24
% Syntax : Number of formulae : 113 ( 57 unt; 0 def)
% Number of atoms : 201 ( 58 equ)
% Maximal formula atoms : 10 ( 1 avg)
% Number of connectives : 165 ( 77 ~; 67 |; 9 &)
% ( 8 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 11 ( 8 usr; 8 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 8 con; 0-2 aty)
% Number of variables : 184 ( 7 sgn 40 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(modus_ponens,axiom,
( modus_ponens
<=> ! [X,Y] :
( ( is_a_theorem(X)
& is_a_theorem(implies(X,Y)) )
=> is_a_theorem(Y) ) ) ).
fof(equivalence_2,axiom,
( equivalence_2
<=> ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(Y,X))) ) ).
fof(r2,axiom,
( r2
<=> ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ) ).
fof(r3,axiom,
( r3
<=> ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) ) ).
fof(op_implies_and,axiom,
( op_implies_and
=> ! [X,Y] : implies(X,Y) = not(and(X,not(Y))) ) ).
fof(op_implies_or,axiom,
( op_implies_or
=> ! [X,Y] : implies(X,Y) = or(not(X),Y) ) ).
fof(op_equiv,axiom,
( op_equiv
=> ! [X,Y] : equiv(X,Y) = and(implies(X,Y),implies(Y,X)) ) ).
fof(principia_op_implies_or,axiom,
op_implies_or ).
fof(principia_op_equiv,axiom,
op_equiv ).
fof(principia_modus_ponens,axiom,
modus_ponens ).
fof(principia_r2,axiom,
r2 ).
fof(principia_r3,axiom,
r3 ).
fof(hilbert_op_implies_and,axiom,
op_implies_and ).
fof(hilbert_op_equiv,axiom,
op_equiv ).
fof(hilbert_equivalence_2,conjecture,
equivalence_2 ).
fof(subgoal_0,plain,
equivalence_2,
inference(strip,[],[hilbert_equivalence_2]) ).
fof(negate_0_0,plain,
~ equivalence_2,
inference(negate,[],[subgoal_0]) ).
fof(normalize_0_0,plain,
( ~ equivalence_2
<=> ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(Y,X))) ),
inference(canonicalize,[],[equivalence_2]) ).
fof(normalize_0_1,plain,
! [X,Y] :
( ( ~ equivalence_2
| is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( ~ is_a_theorem(implies(equiv(skolemFOFtoCNF_X_13,skolemFOFtoCNF_Y_13),implies(skolemFOFtoCNF_Y_13,skolemFOFtoCNF_X_13)))
| equivalence_2 ) ),
inference(clausify,[],[normalize_0_0]) ).
fof(normalize_0_2,plain,
( ~ is_a_theorem(implies(equiv(skolemFOFtoCNF_X_13,skolemFOFtoCNF_Y_13),implies(skolemFOFtoCNF_Y_13,skolemFOFtoCNF_X_13)))
| equivalence_2 ),
inference(conjunct,[],[normalize_0_1]) ).
fof(normalize_0_3,plain,
~ equivalence_2,
inference(canonicalize,[],[negate_0_0]) ).
fof(normalize_0_4,plain,
( ~ r2
<=> ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) ),
inference(canonicalize,[],[r2]) ).
fof(normalize_0_5,plain,
! [P,Q] :
( ( ~ is_a_theorem(implies(skolemFOFtoCNF_Q_4,or(skolemFOFtoCNF_P_7,skolemFOFtoCNF_Q_4)))
| r2 )
& ( ~ r2
| is_a_theorem(implies(Q,or(P,Q))) ) ),
inference(clausify,[],[normalize_0_4]) ).
fof(normalize_0_6,plain,
! [P,Q] :
( ~ r2
| is_a_theorem(implies(Q,or(P,Q))) ),
inference(conjunct,[],[normalize_0_5]) ).
fof(normalize_0_7,plain,
r2,
inference(canonicalize,[],[principia_r2]) ).
fof(normalize_0_8,plain,
( ~ op_implies_or
| ! [X,Y] : implies(X,Y) = or(not(X),Y) ),
inference(canonicalize,[],[op_implies_or]) ).
fof(normalize_0_9,plain,
! [X,Y] :
( ~ op_implies_or
| implies(X,Y) = or(not(X),Y) ),
inference(clausify,[],[normalize_0_8]) ).
fof(normalize_0_10,plain,
op_implies_or,
inference(canonicalize,[],[principia_op_implies_or]) ).
fof(normalize_0_11,plain,
( ~ op_implies_and
| ! [X,Y] : implies(X,Y) = not(and(X,not(Y))) ),
inference(canonicalize,[],[op_implies_and]) ).
fof(normalize_0_12,plain,
! [X,Y] :
( ~ op_implies_and
| implies(X,Y) = not(and(X,not(Y))) ),
inference(clausify,[],[normalize_0_11]) ).
fof(normalize_0_13,plain,
op_implies_and,
inference(canonicalize,[],[hilbert_op_implies_and]) ).
fof(normalize_0_14,plain,
( ~ op_equiv
| ! [X,Y] : equiv(X,Y) = and(implies(X,Y),implies(Y,X)) ),
inference(canonicalize,[],[op_equiv]) ).
fof(normalize_0_15,plain,
! [X,Y] :
( ~ op_equiv
| equiv(X,Y) = and(implies(X,Y),implies(Y,X)) ),
inference(clausify,[],[normalize_0_14]) ).
fof(normalize_0_16,plain,
op_equiv,
inference(canonicalize,[],[hilbert_op_equiv]) ).
fof(normalize_0_17,plain,
( ~ r3
<=> ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) ),
inference(canonicalize,[],[r3]) ).
fof(normalize_0_18,plain,
! [P,Q] :
( ( ~ is_a_theorem(implies(or(skolemFOFtoCNF_P_8,skolemFOFtoCNF_Q_5),or(skolemFOFtoCNF_Q_5,skolemFOFtoCNF_P_8)))
| r3 )
& ( ~ r3
| is_a_theorem(implies(or(P,Q),or(Q,P))) ) ),
inference(clausify,[],[normalize_0_17]) ).
fof(normalize_0_19,plain,
! [P,Q] :
( ~ r3
| is_a_theorem(implies(or(P,Q),or(Q,P))) ),
inference(conjunct,[],[normalize_0_18]) ).
fof(normalize_0_20,plain,
r3,
inference(canonicalize,[],[principia_r3]) ).
fof(normalize_0_21,plain,
( ~ modus_ponens
<=> ? [X,Y] :
( ~ is_a_theorem(Y)
& is_a_theorem(X)
& is_a_theorem(implies(X,Y)) ) ),
inference(canonicalize,[],[modus_ponens]) ).
fof(normalize_0_22,plain,
! [X,Y] :
( ( ~ is_a_theorem(skolemFOFtoCNF_Y)
| modus_ponens )
& ( is_a_theorem(implies(skolemFOFtoCNF_X,skolemFOFtoCNF_Y))
| modus_ponens )
& ( is_a_theorem(skolemFOFtoCNF_X)
| modus_ponens )
& ( ~ is_a_theorem(X)
| ~ is_a_theorem(implies(X,Y))
| ~ modus_ponens
| is_a_theorem(Y) ) ),
inference(clausify,[],[normalize_0_21]) ).
fof(normalize_0_23,plain,
! [X,Y] :
( ~ is_a_theorem(X)
| ~ is_a_theorem(implies(X,Y))
| ~ modus_ponens
| is_a_theorem(Y) ),
inference(conjunct,[],[normalize_0_22]) ).
fof(normalize_0_24,plain,
modus_ponens,
inference(canonicalize,[],[principia_modus_ponens]) ).
cnf(refute_0_0,plain,
( ~ is_a_theorem(implies(equiv(skolemFOFtoCNF_X_13,skolemFOFtoCNF_Y_13),implies(skolemFOFtoCNF_Y_13,skolemFOFtoCNF_X_13)))
| equivalence_2 ),
inference(canonicalize,[],[normalize_0_2]) ).
cnf(refute_0_1,plain,
~ equivalence_2,
inference(canonicalize,[],[normalize_0_3]) ).
cnf(refute_0_2,plain,
~ is_a_theorem(implies(equiv(skolemFOFtoCNF_X_13,skolemFOFtoCNF_Y_13),implies(skolemFOFtoCNF_Y_13,skolemFOFtoCNF_X_13))),
inference(resolve,[$cnf( equivalence_2 )],[refute_0_0,refute_0_1]) ).
cnf(refute_0_3,plain,
( ~ r2
| is_a_theorem(implies(Q,or(P,Q))) ),
inference(canonicalize,[],[normalize_0_6]) ).
cnf(refute_0_4,plain,
r2,
inference(canonicalize,[],[normalize_0_7]) ).
cnf(refute_0_5,plain,
is_a_theorem(implies(Q,or(P,Q))),
inference(resolve,[$cnf( r2 )],[refute_0_4,refute_0_3]) ).
cnf(refute_0_6,plain,
is_a_theorem(implies(Q,or(not(X_7),Q))),
inference(subst,[],[refute_0_5:[bind(P,$fot(not(X_7)))]]) ).
cnf(refute_0_7,plain,
( ~ op_implies_or
| implies(X,Y) = or(not(X),Y) ),
inference(canonicalize,[],[normalize_0_9]) ).
cnf(refute_0_8,plain,
op_implies_or,
inference(canonicalize,[],[normalize_0_10]) ).
cnf(refute_0_9,plain,
implies(X,Y) = or(not(X),Y),
inference(resolve,[$cnf( op_implies_or )],[refute_0_8,refute_0_7]) ).
cnf(refute_0_10,plain,
implies(X_7,Q) = or(not(X_7),Q),
inference(subst,[],[refute_0_9:[bind(X,$fot(X_7)),bind(Y,$fot(Q))]]) ).
cnf(refute_0_11,plain,
X0 = X0,
introduced(tautology,[refl,[$fot(X0)]]) ).
cnf(refute_0_12,plain,
( X0 != X0
| X0 != Y0
| Y0 = X0 ),
introduced(tautology,[equality,[$cnf( $equal(X0,X0) ),[0],$fot(Y0)]]) ).
cnf(refute_0_13,plain,
( X0 != Y0
| Y0 = X0 ),
inference(resolve,[$cnf( $equal(X0,X0) )],[refute_0_11,refute_0_12]) ).
cnf(refute_0_14,plain,
( implies(X_7,Q) != or(not(X_7),Q)
| or(not(X_7),Q) = implies(X_7,Q) ),
inference(subst,[],[refute_0_13:[bind(X0,$fot(implies(X_7,Q))),bind(Y0,$fot(or(not(X_7),Q)))]]) ).
cnf(refute_0_15,plain,
or(not(X_7),Q) = implies(X_7,Q),
inference(resolve,[$cnf( $equal(implies(X_7,Q),or(not(X_7),Q)) )],[refute_0_10,refute_0_14]) ).
cnf(refute_0_16,plain,
( or(not(X_7),Q) != implies(X_7,Q)
| ~ is_a_theorem(implies(Q,or(not(X_7),Q)))
| is_a_theorem(implies(Q,implies(X_7,Q))) ),
introduced(tautology,[equality,[$cnf( is_a_theorem(implies(Q,or(not(X_7),Q))) ),[0,1],$fot(implies(X_7,Q))]]) ).
cnf(refute_0_17,plain,
( ~ is_a_theorem(implies(Q,or(not(X_7),Q)))
| is_a_theorem(implies(Q,implies(X_7,Q))) ),
inference(resolve,[$cnf( $equal(or(not(X_7),Q),implies(X_7,Q)) )],[refute_0_15,refute_0_16]) ).
cnf(refute_0_18,plain,
is_a_theorem(implies(Q,implies(X_7,Q))),
inference(resolve,[$cnf( is_a_theorem(implies(Q,or(not(X_7),Q))) )],[refute_0_6,refute_0_17]) ).
cnf(refute_0_19,plain,
is_a_theorem(implies(and(X_51,not(X_52)),implies(X_7,and(X_51,not(X_52))))),
inference(subst,[],[refute_0_18:[bind(Q,$fot(and(X_51,not(X_52))))]]) ).
cnf(refute_0_20,plain,
( ~ op_implies_and
| implies(X,Y) = not(and(X,not(Y))) ),
inference(canonicalize,[],[normalize_0_12]) ).
cnf(refute_0_21,plain,
op_implies_and,
inference(canonicalize,[],[normalize_0_13]) ).
cnf(refute_0_22,plain,
implies(X,Y) = not(and(X,not(Y))),
inference(resolve,[$cnf( op_implies_and )],[refute_0_21,refute_0_20]) ).
cnf(refute_0_23,plain,
implies(X,and(X_10,not(X_11))) = not(and(X,not(and(X_10,not(X_11))))),
inference(subst,[],[refute_0_22:[bind(Y,$fot(and(X_10,not(X_11))))]]) ).
cnf(refute_0_24,plain,
implies(X_10,X_11) = not(and(X_10,not(X_11))),
inference(subst,[],[refute_0_22:[bind(X,$fot(X_10)),bind(Y,$fot(X_11))]]) ).
cnf(refute_0_25,plain,
( implies(X_10,X_11) != not(and(X_10,not(X_11)))
| not(and(X_10,not(X_11))) = implies(X_10,X_11) ),
inference(subst,[],[refute_0_13:[bind(X0,$fot(implies(X_10,X_11))),bind(Y0,$fot(not(and(X_10,not(X_11)))))]]) ).
cnf(refute_0_26,plain,
not(and(X_10,not(X_11))) = implies(X_10,X_11),
inference(resolve,[$cnf( $equal(implies(X_10,X_11),not(and(X_10,not(X_11)))) )],[refute_0_24,refute_0_25]) ).
cnf(refute_0_27,plain,
( implies(X,and(X_10,not(X_11))) != not(and(X,not(and(X_10,not(X_11)))))
| not(and(X_10,not(X_11))) != implies(X_10,X_11)
| implies(X,and(X_10,not(X_11))) = not(and(X,implies(X_10,X_11))) ),
introduced(tautology,[equality,[$cnf( $equal(implies(X,and(X_10,not(X_11))),not(and(X,not(and(X_10,not(X_11)))))) ),[1,0,1],$fot(implies(X_10,X_11))]]) ).
cnf(refute_0_28,plain,
( implies(X,and(X_10,not(X_11))) != not(and(X,not(and(X_10,not(X_11)))))
| implies(X,and(X_10,not(X_11))) = not(and(X,implies(X_10,X_11))) ),
inference(resolve,[$cnf( $equal(not(and(X_10,not(X_11))),implies(X_10,X_11)) )],[refute_0_26,refute_0_27]) ).
cnf(refute_0_29,plain,
implies(X,and(X_10,not(X_11))) = not(and(X,implies(X_10,X_11))),
inference(resolve,[$cnf( $equal(implies(X,and(X_10,not(X_11))),not(and(X,not(and(X_10,not(X_11)))))) )],[refute_0_23,refute_0_28]) ).
cnf(refute_0_30,plain,
implies(X_7,and(X_51,not(X_52))) = not(and(X_7,implies(X_51,X_52))),
inference(subst,[],[refute_0_29:[bind(X,$fot(X_7)),bind(X_10,$fot(X_51)),bind(X_11,$fot(X_52))]]) ).
cnf(refute_0_31,plain,
( implies(X_7,and(X_51,not(X_52))) != not(and(X_7,implies(X_51,X_52)))
| ~ is_a_theorem(implies(and(X_51,not(X_52)),implies(X_7,and(X_51,not(X_52)))))
| is_a_theorem(implies(and(X_51,not(X_52)),not(and(X_7,implies(X_51,X_52))))) ),
introduced(tautology,[equality,[$cnf( is_a_theorem(implies(and(X_51,not(X_52)),implies(X_7,and(X_51,not(X_52))))) ),[0,1],$fot(not(and(X_7,implies(X_51,X_52))))]]) ).
cnf(refute_0_32,plain,
( ~ is_a_theorem(implies(and(X_51,not(X_52)),implies(X_7,and(X_51,not(X_52)))))
| is_a_theorem(implies(and(X_51,not(X_52)),not(and(X_7,implies(X_51,X_52))))) ),
inference(resolve,[$cnf( $equal(implies(X_7,and(X_51,not(X_52))),not(and(X_7,implies(X_51,X_52)))) )],[refute_0_30,refute_0_31]) ).
cnf(refute_0_33,plain,
is_a_theorem(implies(and(X_51,not(X_52)),not(and(X_7,implies(X_51,X_52))))),
inference(resolve,[$cnf( is_a_theorem(implies(and(X_51,not(X_52)),implies(X_7,and(X_51,not(X_52))))) )],[refute_0_19,refute_0_32]) ).
cnf(refute_0_34,plain,
implies(and(X_10,not(X_11)),Y) = or(not(and(X_10,not(X_11))),Y),
inference(subst,[],[refute_0_9:[bind(X,$fot(and(X_10,not(X_11))))]]) ).
cnf(refute_0_35,plain,
( implies(and(X_10,not(X_11)),Y) != or(not(and(X_10,not(X_11))),Y)
| not(and(X_10,not(X_11))) != implies(X_10,X_11)
| implies(and(X_10,not(X_11)),Y) = or(implies(X_10,X_11),Y) ),
introduced(tautology,[equality,[$cnf( $equal(implies(and(X_10,not(X_11)),Y),or(not(and(X_10,not(X_11))),Y)) ),[1,0],$fot(implies(X_10,X_11))]]) ).
cnf(refute_0_36,plain,
( implies(and(X_10,not(X_11)),Y) != or(not(and(X_10,not(X_11))),Y)
| implies(and(X_10,not(X_11)),Y) = or(implies(X_10,X_11),Y) ),
inference(resolve,[$cnf( $equal(not(and(X_10,not(X_11))),implies(X_10,X_11)) )],[refute_0_26,refute_0_35]) ).
cnf(refute_0_37,plain,
implies(and(X_10,not(X_11)),Y) = or(implies(X_10,X_11),Y),
inference(resolve,[$cnf( $equal(implies(and(X_10,not(X_11)),Y),or(not(and(X_10,not(X_11))),Y)) )],[refute_0_34,refute_0_36]) ).
cnf(refute_0_38,plain,
implies(and(X_51,not(X_52)),not(and(X_7,implies(X_51,X_52)))) = or(implies(X_51,X_52),not(and(X_7,implies(X_51,X_52)))),
inference(subst,[],[refute_0_37:[bind(Y,$fot(not(and(X_7,implies(X_51,X_52))))),bind(X_10,$fot(X_51)),bind(X_11,$fot(X_52))]]) ).
cnf(refute_0_39,plain,
( implies(and(X_51,not(X_52)),not(and(X_7,implies(X_51,X_52)))) != or(implies(X_51,X_52),not(and(X_7,implies(X_51,X_52))))
| ~ is_a_theorem(implies(and(X_51,not(X_52)),not(and(X_7,implies(X_51,X_52)))))
| is_a_theorem(or(implies(X_51,X_52),not(and(X_7,implies(X_51,X_52))))) ),
introduced(tautology,[equality,[$cnf( is_a_theorem(implies(and(X_51,not(X_52)),not(and(X_7,implies(X_51,X_52))))) ),[0],$fot(or(implies(X_51,X_52),not(and(X_7,implies(X_51,X_52)))))]]) ).
cnf(refute_0_40,plain,
( ~ is_a_theorem(implies(and(X_51,not(X_52)),not(and(X_7,implies(X_51,X_52)))))
| is_a_theorem(or(implies(X_51,X_52),not(and(X_7,implies(X_51,X_52))))) ),
inference(resolve,[$cnf( $equal(implies(and(X_51,not(X_52)),not(and(X_7,implies(X_51,X_52)))),or(implies(X_51,X_52),not(and(X_7,implies(X_51,X_52))))) )],[refute_0_38,refute_0_39]) ).
cnf(refute_0_41,plain,
is_a_theorem(or(implies(X_51,X_52),not(and(X_7,implies(X_51,X_52))))),
inference(resolve,[$cnf( is_a_theorem(implies(and(X_51,not(X_52)),not(and(X_7,implies(X_51,X_52))))) )],[refute_0_33,refute_0_40]) ).
cnf(refute_0_42,plain,
is_a_theorem(or(implies(X_208,X_209),not(and(implies(X_209,X_208),implies(X_208,X_209))))),
inference(subst,[],[refute_0_41:[bind(X_51,$fot(X_208)),bind(X_52,$fot(X_209)),bind(X_7,$fot(implies(X_209,X_208)))]]) ).
cnf(refute_0_43,plain,
( ~ op_equiv
| equiv(X,Y) = and(implies(X,Y),implies(Y,X)) ),
inference(canonicalize,[],[normalize_0_15]) ).
cnf(refute_0_44,plain,
op_equiv,
inference(canonicalize,[],[normalize_0_16]) ).
cnf(refute_0_45,plain,
equiv(X,Y) = and(implies(X,Y),implies(Y,X)),
inference(resolve,[$cnf( op_equiv )],[refute_0_44,refute_0_43]) ).
cnf(refute_0_46,plain,
equiv(X_209,X_208) = and(implies(X_209,X_208),implies(X_208,X_209)),
inference(subst,[],[refute_0_45:[bind(X,$fot(X_209)),bind(Y,$fot(X_208))]]) ).
cnf(refute_0_47,plain,
( equiv(X_209,X_208) != and(implies(X_209,X_208),implies(X_208,X_209))
| and(implies(X_209,X_208),implies(X_208,X_209)) = equiv(X_209,X_208) ),
inference(subst,[],[refute_0_13:[bind(X0,$fot(equiv(X_209,X_208))),bind(Y0,$fot(and(implies(X_209,X_208),implies(X_208,X_209))))]]) ).
cnf(refute_0_48,plain,
and(implies(X_209,X_208),implies(X_208,X_209)) = equiv(X_209,X_208),
inference(resolve,[$cnf( $equal(equiv(X_209,X_208),and(implies(X_209,X_208),implies(X_208,X_209))) )],[refute_0_46,refute_0_47]) ).
cnf(refute_0_49,plain,
( and(implies(X_209,X_208),implies(X_208,X_209)) != equiv(X_209,X_208)
| ~ is_a_theorem(or(implies(X_208,X_209),not(and(implies(X_209,X_208),implies(X_208,X_209)))))
| is_a_theorem(or(implies(X_208,X_209),not(equiv(X_209,X_208)))) ),
introduced(tautology,[equality,[$cnf( is_a_theorem(or(implies(X_208,X_209),not(and(implies(X_209,X_208),implies(X_208,X_209))))) ),[0,1,0],$fot(equiv(X_209,X_208))]]) ).
cnf(refute_0_50,plain,
( ~ is_a_theorem(or(implies(X_208,X_209),not(and(implies(X_209,X_208),implies(X_208,X_209)))))
| is_a_theorem(or(implies(X_208,X_209),not(equiv(X_209,X_208)))) ),
inference(resolve,[$cnf( $equal(and(implies(X_209,X_208),implies(X_208,X_209)),equiv(X_209,X_208)) )],[refute_0_48,refute_0_49]) ).
cnf(refute_0_51,plain,
is_a_theorem(or(implies(X_208,X_209),not(equiv(X_209,X_208)))),
inference(resolve,[$cnf( is_a_theorem(or(implies(X_208,X_209),not(and(implies(X_209,X_208),implies(X_208,X_209))))) )],[refute_0_42,refute_0_50]) ).
cnf(refute_0_52,plain,
( ~ r3
| is_a_theorem(implies(or(P,Q),or(Q,P))) ),
inference(canonicalize,[],[normalize_0_19]) ).
cnf(refute_0_53,plain,
r3,
inference(canonicalize,[],[normalize_0_20]) ).
cnf(refute_0_54,plain,
is_a_theorem(implies(or(P,Q),or(Q,P))),
inference(resolve,[$cnf( r3 )],[refute_0_53,refute_0_52]) ).
cnf(refute_0_55,plain,
is_a_theorem(implies(or(P,not(X_7)),or(not(X_7),P))),
inference(subst,[],[refute_0_54:[bind(Q,$fot(not(X_7)))]]) ).
cnf(refute_0_56,plain,
implies(X_7,P) = or(not(X_7),P),
inference(subst,[],[refute_0_9:[bind(X,$fot(X_7)),bind(Y,$fot(P))]]) ).
cnf(refute_0_57,plain,
( implies(X_7,P) != or(not(X_7),P)
| or(not(X_7),P) = implies(X_7,P) ),
inference(subst,[],[refute_0_13:[bind(X0,$fot(implies(X_7,P))),bind(Y0,$fot(or(not(X_7),P)))]]) ).
cnf(refute_0_58,plain,
or(not(X_7),P) = implies(X_7,P),
inference(resolve,[$cnf( $equal(implies(X_7,P),or(not(X_7),P)) )],[refute_0_56,refute_0_57]) ).
cnf(refute_0_59,plain,
( or(not(X_7),P) != implies(X_7,P)
| ~ is_a_theorem(implies(or(P,not(X_7)),or(not(X_7),P)))
| is_a_theorem(implies(or(P,not(X_7)),implies(X_7,P))) ),
introduced(tautology,[equality,[$cnf( is_a_theorem(implies(or(P,not(X_7)),or(not(X_7),P))) ),[0,1],$fot(implies(X_7,P))]]) ).
cnf(refute_0_60,plain,
( ~ is_a_theorem(implies(or(P,not(X_7)),or(not(X_7),P)))
| is_a_theorem(implies(or(P,not(X_7)),implies(X_7,P))) ),
inference(resolve,[$cnf( $equal(or(not(X_7),P),implies(X_7,P)) )],[refute_0_58,refute_0_59]) ).
cnf(refute_0_61,plain,
is_a_theorem(implies(or(P,not(X_7)),implies(X_7,P))),
inference(resolve,[$cnf( is_a_theorem(implies(or(P,not(X_7)),or(not(X_7),P))) )],[refute_0_55,refute_0_60]) ).
cnf(refute_0_62,plain,
( ~ is_a_theorem(X)
| ~ is_a_theorem(implies(X,Y))
| ~ modus_ponens
| is_a_theorem(Y) ),
inference(canonicalize,[],[normalize_0_23]) ).
cnf(refute_0_63,plain,
modus_ponens,
inference(canonicalize,[],[normalize_0_24]) ).
cnf(refute_0_64,plain,
( ~ is_a_theorem(X)
| ~ is_a_theorem(implies(X,Y))
| is_a_theorem(Y) ),
inference(resolve,[$cnf( modus_ponens )],[refute_0_63,refute_0_62]) ).
cnf(refute_0_65,plain,
( ~ is_a_theorem(implies(or(P,not(X_7)),implies(X_7,P)))
| ~ is_a_theorem(or(P,not(X_7)))
| is_a_theorem(implies(X_7,P)) ),
inference(subst,[],[refute_0_64:[bind(X,$fot(or(P,not(X_7)))),bind(Y,$fot(implies(X_7,P)))]]) ).
cnf(refute_0_66,plain,
( ~ is_a_theorem(or(P,not(X_7)))
| is_a_theorem(implies(X_7,P)) ),
inference(resolve,[$cnf( is_a_theorem(implies(or(P,not(X_7)),implies(X_7,P))) )],[refute_0_61,refute_0_65]) ).
cnf(refute_0_67,plain,
( ~ is_a_theorem(or(implies(X_208,X_209),not(equiv(X_209,X_208))))
| is_a_theorem(implies(equiv(X_209,X_208),implies(X_208,X_209))) ),
inference(subst,[],[refute_0_66:[bind(P,$fot(implies(X_208,X_209))),bind(X_7,$fot(equiv(X_209,X_208)))]]) ).
cnf(refute_0_68,plain,
is_a_theorem(implies(equiv(X_209,X_208),implies(X_208,X_209))),
inference(resolve,[$cnf( is_a_theorem(or(implies(X_208,X_209),not(equiv(X_209,X_208)))) )],[refute_0_51,refute_0_67]) ).
cnf(refute_0_69,plain,
is_a_theorem(implies(equiv(skolemFOFtoCNF_X_13,skolemFOFtoCNF_Y_13),implies(skolemFOFtoCNF_Y_13,skolemFOFtoCNF_X_13))),
inference(subst,[],[refute_0_68:[bind(X_208,$fot(skolemFOFtoCNF_Y_13)),bind(X_209,$fot(skolemFOFtoCNF_X_13))]]) ).
cnf(refute_0_70,plain,
$false,
inference(resolve,[$cnf( is_a_theorem(implies(equiv(skolemFOFtoCNF_X_13,skolemFOFtoCNF_Y_13),implies(skolemFOFtoCNF_Y_13,skolemFOFtoCNF_X_13))) )],[refute_0_69,refute_0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL494+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : metis --show proof --show saturation %s
% 0.08/0.35 % Computer : n010.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 : Fri Sep 4 19:01:08 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 1.05/1.37 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.05/1.37
% 1.05/1.37 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 1.15/1.40
%------------------------------------------------------------------------------