%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUM850+2 : TPTP v8.1.2. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n016.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 : 300s
% DateTime : Thu May 9 17:36:50 EDT 2024
% Result : Theorem 5.09s 5.34s
% Output : Refutation 5.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 8
% Syntax : Number of formulae : 39 ( 17 unt; 0 def)
% Number of atoms : 69 ( 30 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 62 ( 32 ~; 27 |; 1 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 64 ( 5 sgn 39 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof('holds(antec(302), 472, 0)',axiom,
greater(vd470,vd471),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(antec(302), 472, 0)') ).
cnf(c182,plain,
greater(vd470,vd471),
inference(split_conjunct,[status(thm)],['holds(antec(302), 472, 0)']) ).
fof('ass(cond(goal(130), 0), 3)',axiom,
! [Vd203,Vd204] :
( Vd203 != Vd204
| ~ greater(Vd203,Vd204) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 3)') ).
fof(c69,plain,
! [Vd203,Vd204] :
( Vd203 != Vd204
| ~ greater(Vd203,Vd204) ),
inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 3)']) ).
fof(c70,plain,
! [X51,X52] :
( X51 != X52
| ~ greater(X51,X52) ),
inference(variable_rename,[status(thm)],[c69]) ).
cnf(c71,plain,
( X145 != X146
| ~ greater(X145,X146) ),
inference(split_conjunct,[status(thm)],[c70]) ).
cnf(c189,plain,
vd470 != vd471,
inference(resolution,[status(thm)],[c71,c182]) ).
fof('ass(cond(goal(130), 0), 1)',axiom,
! [Vd203,Vd204] :
( Vd203 != Vd204
| ~ less(Vd203,Vd204) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 1)') ).
fof(c75,plain,
! [Vd203,Vd204] :
( Vd203 != Vd204
| ~ less(Vd203,Vd204) ),
inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 1)']) ).
fof(c76,plain,
! [X55,X56] :
( X55 != X56
| ~ less(X55,X56) ),
inference(variable_rename,[status(thm)],[c75]) ).
cnf(c77,plain,
( X154 != X155
| ~ less(X154,X155) ),
inference(split_conjunct,[status(thm)],[c76]) ).
fof('ass(cond(189, 0), 0)',axiom,
! [Vd295,Vd296] : greater(vplus(Vd295,Vd296),Vd295),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(189, 0), 0)') ).
fof(c116,plain,
! [X82,X83] : greater(vplus(X82,X83),X82),
inference(variable_rename,[status(thm)],['ass(cond(189, 0), 0)']) ).
cnf(c117,plain,
greater(vplus(X144,X143),X144),
inference(split_conjunct,[status(thm)],[c116]) ).
fof('ass(cond(140, 0), 0)',axiom,
! [Vd208,Vd209] :
( greater(Vd208,Vd209)
=> less(Vd209,Vd208) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(140, 0), 0)') ).
fof(c80,plain,
! [Vd208,Vd209] :
( ~ greater(Vd208,Vd209)
| less(Vd209,Vd208) ),
inference(fof_nnf,[status(thm)],['ass(cond(140, 0), 0)']) ).
fof(c81,plain,
! [X59,X60] :
( ~ greater(X59,X60)
| less(X60,X59) ),
inference(variable_rename,[status(thm)],[c80]) ).
cnf(c82,plain,
( ~ greater(X157,X156)
| less(X156,X157) ),
inference(split_conjunct,[status(thm)],[c81]) ).
cnf(c192,plain,
less(X162,vplus(X162,X163)),
inference(resolution,[status(thm)],[c82,c117]) ).
cnf(c193,plain,
less(vd471,vd470),
inference(resolution,[status(thm)],[c82,c182]) ).
fof('ass(cond(168, 0), 0)',axiom,
! [Vd262,Vd263,Vd265] :
( ( less(Vd263,Vd265)
& less(Vd262,Vd263) )
=> less(Vd262,Vd265) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(168, 0), 0)') ).
fof(c105,plain,
! [Vd262,Vd263,Vd265] :
( ~ less(Vd263,Vd265)
| ~ less(Vd262,Vd263)
| less(Vd262,Vd265) ),
inference(fof_nnf,[status(thm)],['ass(cond(168, 0), 0)']) ).
fof(c106,plain,
! [X73,X74,X75] :
( ~ less(X74,X75)
| ~ less(X73,X74)
| less(X73,X75) ),
inference(variable_rename,[status(thm)],[c105]) ).
cnf(c107,plain,
( ~ less(X397,X399)
| ~ less(X398,X397)
| less(X398,X399) ),
inference(split_conjunct,[status(thm)],[c106]) ).
cnf(c619,plain,
( ~ less(vd470,X421)
| less(vd471,X421) ),
inference(resolution,[status(thm)],[c107,c193]) ).
cnf(c677,plain,
less(vd471,vplus(vd470,X431)),
inference(resolution,[status(thm)],[c619,c192]) ).
cnf(c738,plain,
vd471 != vplus(vd470,X438),
inference(resolution,[status(thm)],[c677,c77]) ).
fof('qe(conseq_conjunct1(conseq(302)))',conjecture,
? [Vd473] : vd470 = vplus(vd471,Vd473),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qe(conseq_conjunct1(conseq(302)))') ).
fof(c183,negated_conjecture,
~ ? [Vd473] : vd470 = vplus(vd471,Vd473),
inference(assume_negation,[status(cth)],['qe(conseq_conjunct1(conseq(302)))']) ).
fof(c184,negated_conjecture,
! [Vd473] : vd470 != vplus(vd471,Vd473),
inference(fof_nnf,[status(thm)],[c183]) ).
fof(c185,negated_conjecture,
! [X133] : vd470 != vplus(vd471,X133),
inference(variable_rename,[status(thm)],[c184]) ).
cnf(c186,negated_conjecture,
vd470 != vplus(vd471,X243),
inference(split_conjunct,[status(thm)],[c185]) ).
fof('ass(cond(goal(88), 0), 0)',axiom,
! [Vd120,Vd121] :
( Vd120 = Vd121
| ? [Vd123] : Vd120 = vplus(Vd121,Vd123)
| ? [Vd125] : Vd121 = vplus(Vd120,Vd125) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(goal(88), 0), 0)') ).
fof(c52,plain,
! [X35,X36] :
( X35 = X36
| ? [X37] : X35 = vplus(X36,X37)
| ? [X38] : X36 = vplus(X35,X38) ),
inference(variable_rename,[status(thm)],['ass(cond(goal(88), 0), 0)']) ).
fof(c53,plain,
! [X35,X36] :
( X35 = X36
| X35 = vplus(X36,skolem0001(X35,X36))
| X36 = vplus(X35,skolem0002(X35,X36)) ),
inference(skolemize,[status(esa)],[c52]) ).
cnf(c54,plain,
( X330 = X329
| X330 = vplus(X329,skolem0001(X330,X329))
| X329 = vplus(X330,skolem0002(X330,X329)) ),
inference(split_conjunct,[status(thm)],[c53]) ).
cnf(c439,plain,
( vd470 = vd471
| vd471 = vplus(vd470,skolem0002(vd470,vd471)) ),
inference(resolution,[status(thm)],[c54,c186]) ).
cnf(c15704,plain,
vd470 = vd471,
inference(resolution,[status(thm)],[c439,c738]) ).
cnf(c15807,plain,
$false,
inference(resolution,[status(thm)],[c15704,c189]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : NUM850+2 : TPTP v8.1.2. Released v4.1.0.
% 0.04/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n016.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 16:11:38 EDT 2024
% 0.13/0.35 % CPUTime :
% 5.09/5.34 % Version: 1.5
% 5.09/5.34 % SZS status Theorem
% 5.09/5.34 % SZS output start CNFRefutation
% See solution above
% 5.09/5.34
% 5.09/5.34 % Initial clauses : 72
% 5.09/5.34 % Processed clauses : 664
% 5.09/5.34 % Factors computed : 15
% 5.09/5.34 % Resolvents computed: 15616
% 5.09/5.34 % Tautologies deleted: 8
% 5.09/5.34 % Forward subsumed : 607
% 5.09/5.34 % Backward subsumed : 3
% 5.09/5.34 % -------- CPU Time ---------
% 5.09/5.34 % User time : 4.927 s
% 5.09/5.34 % System time : 0.036 s
% 5.09/5.34 % Total time : 4.963 s
%------------------------------------------------------------------------------