%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : HEN004-3 : TPTP v8.1.2. Released v1.0.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:24:47 EDT 2024
% Result : Unsatisfiable 238.12s 238.37s
% Output : Refutation 238.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 12
% Syntax : Number of clauses : 40 ( 23 unt; 0 nHn; 17 RR)
% Number of literals : 64 ( 40 equ; 25 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 3 ( 3 usr; 2 con; 0-2 aty)
% Number of variables : 76 ( 15 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_x_divide_zero_is_x,negated_conjecture,
divide(a,zero) != a,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_x_divide_zero_is_x) ).
cnf(symmetry,axiom,
( X7 != X8
| X8 = X7 ),
theory(equality) ).
cnf(quotient_smaller_than_numerator,axiom,
less_equal(divide(X5,X6),X5),
file('/export/starexec/sandbox/benchmark/Axioms/HEN002-0.ax',quotient_smaller_than_numerator) ).
cnf(less_equal_and_equal,axiom,
( ~ less_equal(X33,X34)
| ~ less_equal(X34,X33)
| X33 = X34 ),
file('/export/starexec/sandbox/benchmark/Axioms/HEN002-0.ax',less_equal_and_equal) ).
cnf(c17,plain,
( ~ less_equal(X70,divide(X70,X71))
| X70 = divide(X70,X71) ),
inference(resolution,[status(thm)],[less_equal_and_equal,quotient_smaller_than_numerator]) ).
cnf(quotient_less_equal2,axiom,
( divide(X16,X17) != zero
| less_equal(X16,X17) ),
file('/export/starexec/sandbox/benchmark/Axioms/HEN002-0.ax',quotient_less_equal2) ).
cnf(zero_is_smallest,axiom,
less_equal(zero,X3),
file('/export/starexec/sandbox/benchmark/Axioms/HEN002-0.ax',zero_is_smallest) ).
cnf(c18,plain,
( ~ less_equal(X42,zero)
| X42 = zero ),
inference(resolution,[status(thm)],[less_equal_and_equal,zero_is_smallest]) ).
cnf(quotient_less_equal1,axiom,
( ~ less_equal(X9,X10)
| divide(X9,X10) = zero ),
file('/export/starexec/sandbox/benchmark/Axioms/HEN002-0.ax',quotient_less_equal1) ).
cnf(c4,plain,
divide(zero,X12) = zero,
inference(resolution,[status(thm)],[quotient_less_equal1,zero_is_smallest]) ).
cnf(transitivity,axiom,
( X35 != X36
| X36 != X37
| X35 = X37 ),
theory(equality) ).
cnf(c28,plain,
( X104 != divide(zero,X103)
| X104 = zero ),
inference(resolution,[status(thm)],[transitivity,c4]) ).
cnf(c6,plain,
zero = divide(zero,X14),
inference(resolution,[status(thm)],[c4,symmetry]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c1,axiom,
( X54 != X52
| X51 != X53
| ~ less_equal(X54,X51)
| less_equal(X52,X53) ),
theory(equality) ).
cnf(c45,plain,
( zero != X118
| X117 != X119
| less_equal(X118,X119) ),
inference(resolution,[status(thm)],[c1,zero_is_smallest]) ).
cnf(c128,plain,
( zero != X121
| less_equal(X121,X122) ),
inference(resolution,[status(thm)],[c45,reflexivity]) ).
cnf(c138,plain,
less_equal(divide(zero,X129),X130),
inference(resolution,[status(thm)],[c128,c6]) ).
cnf(c161,plain,
( ~ less_equal(X947,divide(zero,X946))
| X947 = divide(zero,X946) ),
inference(resolution,[status(thm)],[c138,less_equal_and_equal]) ).
cnf(c3,plain,
divide(divide(X25,X26),X25) = zero,
inference(resolution,[status(thm)],[quotient_less_equal1,quotient_smaller_than_numerator]) ).
cnf(quotient_property,axiom,
less_equal(divide(divide(X22,X24),divide(X23,X24)),divide(divide(X22,X23),X24)),
file('/export/starexec/sandbox/benchmark/Axioms/HEN002-0.ax',quotient_property) ).
cnf(c46,plain,
( divide(divide(X203,X205),divide(X201,X205)) != X204
| divide(divide(X203,X201),X205) != X202
| less_equal(X204,X202) ),
inference(resolution,[status(thm)],[c1,quotient_property]) ).
cnf(c316,plain,
( divide(divide(X2215,X2217),X2216) != X2214
| less_equal(divide(divide(X2215,X2216),divide(X2217,X2216)),X2214) ),
inference(resolution,[status(thm)],[c46,reflexivity]) ).
cnf(c4678,plain,
less_equal(divide(divide(X2219,X2219),divide(X2218,X2219)),zero),
inference(resolution,[status(thm)],[c316,c3]) ).
cnf(c4704,plain,
divide(divide(X2220,X2220),divide(X2221,X2220)) = zero,
inference(resolution,[status(thm)],[c4678,c18]) ).
cnf(c4708,plain,
less_equal(divide(X2230,X2230),divide(X2231,X2230)),
inference(resolution,[status(thm)],[c4704,quotient_less_equal2]) ).
cnf(c4746,plain,
divide(X2232,X2232) = divide(zero,X2232),
inference(resolution,[status(thm)],[c4708,c161]) ).
cnf(c4787,plain,
divide(X2233,X2233) = zero,
inference(resolution,[status(thm)],[c4746,c28]) ).
cnf(c0,axiom,
( X46 != X44
| X43 != X45
| divide(X46,X43) = divide(X44,X45) ),
theory(equality) ).
cnf(c38,plain,
( X179 != X177
| divide(X179,divide(zero,X178)) = divide(X177,zero) ),
inference(resolution,[status(thm)],[c0,c4]) ).
cnf(c293,plain,
divide(X593,divide(zero,X594)) = divide(X593,zero),
inference(resolution,[status(thm)],[c38,reflexivity]) ).
cnf(c1260,plain,
( divide(divide(X11827,zero),X11828) != X11829
| less_equal(divide(divide(X11827,X11828),zero),X11829) ),
inference(resolution,[status(thm)],[c293,c46]) ).
cnf(c55662,plain,
less_equal(divide(divide(X20397,divide(X20397,zero)),zero),zero),
inference(resolution,[status(thm)],[c1260,c4787]) ).
cnf(c114630,plain,
divide(divide(X22647,divide(X22647,zero)),zero) = zero,
inference(resolution,[status(thm)],[c55662,c18]) ).
cnf(c129000,plain,
less_equal(divide(X22660,divide(X22660,zero)),zero),
inference(resolution,[status(thm)],[c114630,quotient_less_equal2]) ).
cnf(c129186,plain,
divide(X22666,divide(X22666,zero)) = zero,
inference(resolution,[status(thm)],[c129000,c18]) ).
cnf(c130110,plain,
less_equal(X22671,divide(X22671,zero)),
inference(resolution,[status(thm)],[c129186,quotient_less_equal2]) ).
cnf(c130333,plain,
X22673 = divide(X22673,zero),
inference(resolution,[status(thm)],[c130110,c17]) ).
cnf(c130414,plain,
divide(X22681,zero) = X22681,
inference(resolution,[status(thm)],[c130333,symmetry]) ).
cnf(c130666,plain,
$false,
inference(resolution,[status(thm)],[c130414,prove_x_divide_zero_is_x]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : HEN004-3 : TPTP v8.1.2. Released v1.0.0.
% 0.08/0.15 % 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 13:50:53 EDT 2024
% 0.14/0.36 % CPUTime :
% 238.12/238.37 % Version: 1.5
% 238.12/238.37 % SZS status Unsatisfiable
% 238.12/238.37 % SZS output start CNFRefutation
% See solution above
% 238.12/238.37
% 238.12/238.37 % Initial clauses : 13
% 238.12/238.37 % Processed clauses : 1439
% 238.12/238.37 % Factors computed : 15
% 238.12/238.37 % Resolvents computed: 130772
% 238.12/238.37 % Tautologies deleted: 2
% 238.12/238.37 % Forward subsumed : 8757
% 238.12/238.37 % Backward subsumed : 308
% 238.12/238.37 % -------- CPU Time ---------
% 238.12/238.37 % User time : 237.626 s
% 238.12/238.37 % System time : 0.333 s
% 238.12/238.37 % Total time : 237.959 s
%------------------------------------------------------------------------------