%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : NUM836+2 : TPTP v8.1.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Mon Jul 18 12:30:48 EDT 2022
% Result : Theorem 0.44s 0.63s
% Output : CNFRefutation 0.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 10
% Syntax : Number of formulae : 54 ( 22 unt; 0 def)
% Number of atoms : 93 ( 64 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 93 ( 54 ~; 28 |; 3 &)
% ( 6 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 5 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 80 ( 5 sgn 46 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof('dis(ex(cond(conseq(131), 0), 1))',conjecture,
( ~ greater(vd203,vd204)
| ~ less(vd203,vd204) ) ).
fof('def(cond(conseq(axiom(3)), 12), 1)',axiom,
! [Vd198,Vd199] :
( less(Vd199,Vd198)
<=> ? [Vd201] : Vd198 = vplus(Vd199,Vd201) ) ).
fof('def(cond(conseq(axiom(3)), 11), 1)',axiom,
! [Vd193,Vd194] :
( greater(Vd194,Vd193)
<=> ? [Vd196] : Vd194 = vplus(Vd193,Vd196) ) ).
fof('ass(cond(goal(88), 0), 1)',axiom,
! [Vd120,Vd121] :
( Vd120 != Vd121
| ~ ? [Vd125] : Vd121 = vplus(Vd120,Vd125) ) ).
fof('ass(cond(33, 0), 0)',axiom,
! [Vd46,Vd47,Vd48] : vplus(vplus(Vd46,Vd47),Vd48) = vplus(Vd46,vplus(Vd47,Vd48)) ).
fof(subgoal_0,plain,
( ~ ~ greater(vd203,vd204)
=> ~ less(vd203,vd204) ),
inference(strip,[],['dis(ex(cond(conseq(131), 0), 1))']) ).
fof(negate_0_0,plain,
~ ( ~ ~ greater(vd203,vd204)
=> ~ less(vd203,vd204) ),
inference(negate,[],[subgoal_0]) ).
fof(normalize_0_0,plain,
( greater(vd203,vd204)
& less(vd203,vd204) ),
inference(canonicalize,[],[negate_0_0]) ).
fof(normalize_0_1,plain,
greater(vd203,vd204),
inference(conjunct,[],[normalize_0_0]) ).
fof(normalize_0_2,plain,
! [Vd193,Vd194] :
( ~ greater(Vd194,Vd193)
<=> ! [Vd196] : Vd194 != vplus(Vd193,Vd196) ),
inference(canonicalize,[],['def(cond(conseq(axiom(3)), 11), 1)']) ).
fof(normalize_0_3,plain,
! [Vd193,Vd194] :
( ~ greater(Vd194,Vd193)
<=> ! [Vd196] : Vd194 != vplus(Vd193,Vd196) ),
inference(specialize,[],[normalize_0_2]) ).
fof(normalize_0_4,plain,
! [Vd193,Vd194,Vd196] :
( ( Vd194 != vplus(Vd193,Vd196)
| greater(Vd194,Vd193) )
& ( ~ greater(Vd194,Vd193)
| Vd194 = vplus(Vd193,skolemFOFtoCNF_Vd196(Vd193,Vd194)) ) ),
inference(clausify,[],[normalize_0_3]) ).
fof(normalize_0_5,plain,
! [Vd193,Vd194] :
( ~ greater(Vd194,Vd193)
| Vd194 = vplus(Vd193,skolemFOFtoCNF_Vd196(Vd193,Vd194)) ),
inference(conjunct,[],[normalize_0_4]) ).
fof(normalize_0_6,plain,
! [Vd120,Vd121] :
( Vd120 != Vd121
| ! [Vd125] : Vd121 != vplus(Vd120,Vd125) ),
inference(canonicalize,[],['ass(cond(goal(88), 0), 1)']) ).
fof(normalize_0_7,plain,
! [Vd120,Vd121] :
( Vd120 != Vd121
| ! [Vd125] : Vd121 != vplus(Vd120,Vd125) ),
inference(specialize,[],[normalize_0_6]) ).
fof(normalize_0_8,plain,
! [Vd120,Vd121,Vd125] :
( Vd120 != Vd121
| Vd121 != vplus(Vd120,Vd125) ),
inference(clausify,[],[normalize_0_7]) ).
fof(normalize_0_9,plain,
! [Vd46,Vd47,Vd48] : vplus(vplus(Vd46,Vd47),Vd48) = vplus(Vd46,vplus(Vd47,Vd48)),
inference(canonicalize,[],['ass(cond(33, 0), 0)']) ).
fof(normalize_0_10,plain,
! [Vd46,Vd47,Vd48] : vplus(vplus(Vd46,Vd47),Vd48) = vplus(Vd46,vplus(Vd47,Vd48)),
inference(specialize,[],[normalize_0_9]) ).
fof(normalize_0_11,plain,
less(vd203,vd204),
inference(conjunct,[],[normalize_0_0]) ).
fof(normalize_0_12,plain,
! [Vd198,Vd199] :
( ~ less(Vd199,Vd198)
<=> ! [Vd201] : Vd198 != vplus(Vd199,Vd201) ),
inference(canonicalize,[],['def(cond(conseq(axiom(3)), 12), 1)']) ).
fof(normalize_0_13,plain,
! [Vd198,Vd199] :
( ~ less(Vd199,Vd198)
<=> ! [Vd201] : Vd198 != vplus(Vd199,Vd201) ),
inference(specialize,[],[normalize_0_12]) ).
fof(normalize_0_14,plain,
! [Vd198,Vd199,Vd201] :
( ( Vd198 != vplus(Vd199,Vd201)
| less(Vd199,Vd198) )
& ( ~ less(Vd199,Vd198)
| Vd198 = vplus(Vd199,skolemFOFtoCNF_Vd201(Vd198,Vd199)) ) ),
inference(clausify,[],[normalize_0_13]) ).
fof(normalize_0_15,plain,
! [Vd198,Vd199] :
( ~ less(Vd199,Vd198)
| Vd198 = vplus(Vd199,skolemFOFtoCNF_Vd201(Vd198,Vd199)) ),
inference(conjunct,[],[normalize_0_14]) ).
cnf(refute_0_0,plain,
greater(vd203,vd204),
inference(canonicalize,[],[normalize_0_1]) ).
cnf(refute_0_1,plain,
( ~ greater(Vd194,Vd193)
| Vd194 = vplus(Vd193,skolemFOFtoCNF_Vd196(Vd193,Vd194)) ),
inference(canonicalize,[],[normalize_0_5]) ).
cnf(refute_0_2,plain,
( ~ greater(vd203,vd204)
| vd203 = vplus(vd204,skolemFOFtoCNF_Vd196(vd204,vd203)) ),
inference(subst,[],[refute_0_1:[bind(Vd193,$fot(vd204)),bind(Vd194,$fot(vd203))]]) ).
cnf(refute_0_3,plain,
vd203 = vplus(vd204,skolemFOFtoCNF_Vd196(vd204,vd203)),
inference(resolve,[$cnf( greater(vd203,vd204) )],[refute_0_0,refute_0_2]) ).
cnf(refute_0_4,plain,
( Vd120 != Vd121
| Vd121 != vplus(Vd120,Vd125) ),
inference(canonicalize,[],[normalize_0_8]) ).
cnf(refute_0_5,plain,
( Vd121 != Vd121
| Vd121 != vplus(Vd121,Vd125) ),
inference(subst,[],[refute_0_4:[bind(Vd120,$fot(Vd121))]]) ).
cnf(refute_0_6,plain,
Vd121 = Vd121,
introduced(tautology,[refl,[$fot(Vd121)]]) ).
cnf(refute_0_7,plain,
Vd121 != vplus(Vd121,Vd125),
inference(resolve,[$cnf( $equal(Vd121,Vd121) )],[refute_0_6,refute_0_5]) ).
cnf(refute_0_8,plain,
vd203 != vplus(vd203,vplus(skolemFOFtoCNF_Vd201(vd204,vd203),X_110)),
inference(subst,[],[refute_0_7:[bind(Vd121,$fot(vd203)),bind(Vd125,$fot(vplus(skolemFOFtoCNF_Vd201(vd204,vd203),X_110)))]]) ).
cnf(refute_0_9,plain,
vplus(vplus(Vd46,Vd47),Vd48) = vplus(Vd46,vplus(Vd47,Vd48)),
inference(canonicalize,[],[normalize_0_10]) ).
cnf(refute_0_10,plain,
vplus(vplus(vd203,skolemFOFtoCNF_Vd201(vd204,vd203)),Vd48) = vplus(vd203,vplus(skolemFOFtoCNF_Vd201(vd204,vd203),Vd48)),
inference(subst,[],[refute_0_9:[bind(Vd46,$fot(vd203)),bind(Vd47,$fot(skolemFOFtoCNF_Vd201(vd204,vd203)))]]) ).
cnf(refute_0_11,plain,
less(vd203,vd204),
inference(canonicalize,[],[normalize_0_11]) ).
cnf(refute_0_12,plain,
( ~ less(Vd199,Vd198)
| Vd198 = vplus(Vd199,skolemFOFtoCNF_Vd201(Vd198,Vd199)) ),
inference(canonicalize,[],[normalize_0_15]) ).
cnf(refute_0_13,plain,
( ~ less(vd203,vd204)
| vd204 = vplus(vd203,skolemFOFtoCNF_Vd201(vd204,vd203)) ),
inference(subst,[],[refute_0_12:[bind(Vd198,$fot(vd204)),bind(Vd199,$fot(vd203))]]) ).
cnf(refute_0_14,plain,
vd204 = vplus(vd203,skolemFOFtoCNF_Vd201(vd204,vd203)),
inference(resolve,[$cnf( less(vd203,vd204) )],[refute_0_11,refute_0_13]) ).
cnf(refute_0_15,plain,
X = X,
introduced(tautology,[refl,[$fot(X)]]) ).
cnf(refute_0_16,plain,
( X != X
| X != Y
| Y = X ),
introduced(tautology,[equality,[$cnf( $equal(X,X) ),[0],$fot(Y)]]) ).
cnf(refute_0_17,plain,
( X != Y
| Y = X ),
inference(resolve,[$cnf( $equal(X,X) )],[refute_0_15,refute_0_16]) ).
cnf(refute_0_18,plain,
( vd204 != vplus(vd203,skolemFOFtoCNF_Vd201(vd204,vd203))
| vplus(vd203,skolemFOFtoCNF_Vd201(vd204,vd203)) = vd204 ),
inference(subst,[],[refute_0_17:[bind(X,$fot(vd204)),bind(Y,$fot(vplus(vd203,skolemFOFtoCNF_Vd201(vd204,vd203))))]]) ).
cnf(refute_0_19,plain,
vplus(vd203,skolemFOFtoCNF_Vd201(vd204,vd203)) = vd204,
inference(resolve,[$cnf( $equal(vd204,vplus(vd203,skolemFOFtoCNF_Vd201(vd204,vd203))) )],[refute_0_14,refute_0_18]) ).
cnf(refute_0_20,plain,
( vplus(vd203,skolemFOFtoCNF_Vd201(vd204,vd203)) != vd204
| vplus(vplus(vd203,skolemFOFtoCNF_Vd201(vd204,vd203)),Vd48) != vplus(vd203,vplus(skolemFOFtoCNF_Vd201(vd204,vd203),Vd48))
| vplus(vd204,Vd48) = vplus(vd203,vplus(skolemFOFtoCNF_Vd201(vd204,vd203),Vd48)) ),
introduced(tautology,[equality,[$cnf( $equal(vplus(vplus(vd203,skolemFOFtoCNF_Vd201(vd204,vd203)),Vd48),vplus(vd203,vplus(skolemFOFtoCNF_Vd201(vd204,vd203),Vd48))) ),[0,0],$fot(vd204)]]) ).
cnf(refute_0_21,plain,
( vplus(vplus(vd203,skolemFOFtoCNF_Vd201(vd204,vd203)),Vd48) != vplus(vd203,vplus(skolemFOFtoCNF_Vd201(vd204,vd203),Vd48))
| vplus(vd204,Vd48) = vplus(vd203,vplus(skolemFOFtoCNF_Vd201(vd204,vd203),Vd48)) ),
inference(resolve,[$cnf( $equal(vplus(vd203,skolemFOFtoCNF_Vd201(vd204,vd203)),vd204) )],[refute_0_19,refute_0_20]) ).
cnf(refute_0_22,plain,
vplus(vd204,Vd48) = vplus(vd203,vplus(skolemFOFtoCNF_Vd201(vd204,vd203),Vd48)),
inference(resolve,[$cnf( $equal(vplus(vplus(vd203,skolemFOFtoCNF_Vd201(vd204,vd203)),Vd48),vplus(vd203,vplus(skolemFOFtoCNF_Vd201(vd204,vd203),Vd48))) )],[refute_0_10,refute_0_21]) ).
cnf(refute_0_23,plain,
vplus(vd204,X_110) = vplus(vd203,vplus(skolemFOFtoCNF_Vd201(vd204,vd203),X_110)),
inference(subst,[],[refute_0_22:[bind(Vd48,$fot(X_110))]]) ).
cnf(refute_0_24,plain,
( vplus(vd204,X_110) != vplus(vd203,vplus(skolemFOFtoCNF_Vd201(vd204,vd203),X_110))
| vplus(vd203,vplus(skolemFOFtoCNF_Vd201(vd204,vd203),X_110)) = vplus(vd204,X_110) ),
inference(subst,[],[refute_0_17:[bind(X,$fot(vplus(vd204,X_110))),bind(Y,$fot(vplus(vd203,vplus(skolemFOFtoCNF_Vd201(vd204,vd203),X_110))))]]) ).
cnf(refute_0_25,plain,
vplus(vd203,vplus(skolemFOFtoCNF_Vd201(vd204,vd203),X_110)) = vplus(vd204,X_110),
inference(resolve,[$cnf( $equal(vplus(vd204,X_110),vplus(vd203,vplus(skolemFOFtoCNF_Vd201(vd204,vd203),X_110))) )],[refute_0_23,refute_0_24]) ).
cnf(refute_0_26,plain,
( vd203 != vplus(vd204,X_110)
| vplus(vd203,vplus(skolemFOFtoCNF_Vd201(vd204,vd203),X_110)) != vplus(vd204,X_110)
| vd203 = vplus(vd203,vplus(skolemFOFtoCNF_Vd201(vd204,vd203),X_110)) ),
introduced(tautology,[equality,[$cnf( ~ $equal(vd203,vplus(vd203,vplus(skolemFOFtoCNF_Vd201(vd204,vd203),X_110))) ),[1],$fot(vplus(vd204,X_110))]]) ).
cnf(refute_0_27,plain,
( vd203 != vplus(vd204,X_110)
| vd203 = vplus(vd203,vplus(skolemFOFtoCNF_Vd201(vd204,vd203),X_110)) ),
inference(resolve,[$cnf( $equal(vplus(vd203,vplus(skolemFOFtoCNF_Vd201(vd204,vd203),X_110)),vplus(vd204,X_110)) )],[refute_0_25,refute_0_26]) ).
cnf(refute_0_28,plain,
vd203 != vplus(vd204,X_110),
inference(resolve,[$cnf( $equal(vd203,vplus(vd203,vplus(skolemFOFtoCNF_Vd201(vd204,vd203),X_110))) )],[refute_0_27,refute_0_8]) ).
cnf(refute_0_29,plain,
vd203 != vplus(vd204,skolemFOFtoCNF_Vd196(vd204,vd203)),
inference(subst,[],[refute_0_28:[bind(X_110,$fot(skolemFOFtoCNF_Vd196(vd204,vd203)))]]) ).
cnf(refute_0_30,plain,
$false,
inference(resolve,[$cnf( $equal(vd203,vplus(vd204,skolemFOFtoCNF_Vd196(vd204,vd203))) )],[refute_0_3,refute_0_29]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : NUM836+2 : TPTP v8.1.0. Released v4.1.0.
% 0.12/0.13 % Command : metis --show proof --show saturation %s
% 0.12/0.34 % Computer : n017.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Thu Jul 7 11:55:30 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.12/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.44/0.63 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.44/0.63
% 0.44/0.63 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 0.47/0.63
%------------------------------------------------------------------------------