%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUM850+1 : TPTP v8.1.2. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.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 4.92s 5.10s
% Output : Refutation 4.92s
% 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/sandbox2/benchmark/theBenchmark.p','holds(antec(302), 472, 0)') ).
cnf(c185,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/sandbox2/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,
( X148 != X147
| ~ greater(X148,X147) ),
inference(split_conjunct,[status(thm)],[c70]) ).
cnf(c192,plain,
vd470 != vd471,
inference(resolution,[status(thm)],[c71,c185]) ).
fof('ass(cond(goal(130), 0), 1)',axiom,
! [Vd203,Vd204] :
( Vd203 != Vd204
| ~ less(Vd203,Vd204) ),
file('/export/starexec/sandbox2/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,
( X156 != X157
| ~ less(X156,X157) ),
inference(split_conjunct,[status(thm)],[c76]) ).
fof('ass(cond(189, 0), 0)',axiom,
! [Vd295,Vd296] : greater(vplus(Vd295,Vd296),Vd295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(189, 0), 0)') ).
fof(c119,plain,
! [X84,X85] : greater(vplus(X84,X85),X84),
inference(variable_rename,[status(thm)],['ass(cond(189, 0), 0)']) ).
cnf(c120,plain,
greater(vplus(X146,X145),X146),
inference(split_conjunct,[status(thm)],[c119]) ).
fof('ass(cond(140, 0), 0)',axiom,
! [Vd208,Vd209] :
( greater(Vd208,Vd209)
=> less(Vd209,Vd208) ),
file('/export/starexec/sandbox2/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(X159,X158)
| less(X158,X159) ),
inference(split_conjunct,[status(thm)],[c81]) ).
cnf(c195,plain,
less(X165,vplus(X165,X164)),
inference(resolution,[status(thm)],[c82,c120]) ).
cnf(c196,plain,
less(vd471,vd470),
inference(resolution,[status(thm)],[c82,c185]) ).
fof('ass(cond(168, 0), 0)',axiom,
! [Vd262,Vd263,Vd265] :
( ( less(Vd263,Vd265)
& less(Vd262,Vd263) )
=> less(Vd262,Vd265) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(168, 0), 0)') ).
fof(c108,plain,
! [Vd262,Vd263,Vd265] :
( ~ less(Vd263,Vd265)
| ~ less(Vd262,Vd263)
| less(Vd262,Vd265) ),
inference(fof_nnf,[status(thm)],['ass(cond(168, 0), 0)']) ).
fof(c109,plain,
! [X75,X76,X77] :
( ~ less(X76,X77)
| ~ less(X75,X76)
| less(X75,X77) ),
inference(variable_rename,[status(thm)],[c108]) ).
cnf(c110,plain,
( ~ less(X402,X401)
| ~ less(X400,X402)
| less(X400,X401) ),
inference(split_conjunct,[status(thm)],[c109]) ).
cnf(c627,plain,
( ~ less(vd470,X624)
| less(vd471,X624) ),
inference(resolution,[status(thm)],[c110,c196]) ).
cnf(c1154,plain,
less(vd471,vplus(vd470,X635)),
inference(resolution,[status(thm)],[c627,c195]) ).
cnf(c1276,plain,
vd471 != vplus(vd470,X651),
inference(resolution,[status(thm)],[c1154,c77]) ).
fof('qe(conseq_conjunct1(conseq(302)))',conjecture,
? [Vd473] : vd470 = vplus(vd471,Vd473),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qe(conseq_conjunct1(conseq(302)))') ).
fof(c186,negated_conjecture,
~ ? [Vd473] : vd470 = vplus(vd471,Vd473),
inference(assume_negation,[status(cth)],['qe(conseq_conjunct1(conseq(302)))']) ).
fof(c187,negated_conjecture,
! [Vd473] : vd470 != vplus(vd471,Vd473),
inference(fof_nnf,[status(thm)],[c186]) ).
fof(c188,negated_conjecture,
! [X135] : vd470 != vplus(vd471,X135),
inference(variable_rename,[status(thm)],[c187]) ).
cnf(c189,negated_conjecture,
vd470 != vplus(vd471,X259),
inference(split_conjunct,[status(thm)],[c188]) ).
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/sandbox2/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,
( X326 = X325
| X326 = vplus(X325,skolem0001(X326,X325))
| X325 = vplus(X326,skolem0002(X326,X325)) ),
inference(split_conjunct,[status(thm)],[c53]) ).
cnf(c455,plain,
( vd470 = vd471
| vd471 = vplus(vd470,skolem0002(vd470,vd471)) ),
inference(resolution,[status(thm)],[c54,c189]) ).
cnf(c15400,plain,
vd470 = vd471,
inference(resolution,[status(thm)],[c455,c1276]) ).
cnf(c15526,plain,
$false,
inference(resolution,[status(thm)],[c15400,c192]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : NUM850+1 : TPTP v8.1.2. Released v4.1.0.
% 0.04/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n013.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 15:56:38 EDT 2024
% 0.14/0.36 % CPUTime :
% 4.92/5.10 % Version: 1.5
% 4.92/5.10 % SZS status Theorem
% 4.92/5.10 % SZS output start CNFRefutation
% See solution above
% 4.92/5.10
% 4.92/5.10 % Initial clauses : 73
% 4.92/5.10 % Processed clauses : 622
% 4.92/5.10 % Factors computed : 15
% 4.92/5.10 % Resolvents computed: 15344
% 4.92/5.10 % Tautologies deleted: 9
% 4.92/5.10 % Forward subsumed : 666
% 4.92/5.10 % Backward subsumed : 2
% 4.92/5.10 % -------- CPU Time ---------
% 4.92/5.10 % User time : 4.687 s
% 4.92/5.10 % System time : 0.043 s
% 4.92/5.10 % Total time : 4.730 s
%------------------------------------------------------------------------------