%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : HEN004-6 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n019.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 169.56s 169.80s
% Output : Refutation 169.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 13
% Syntax : Number of clauses : 45 ( 26 unt; 0 nHn; 18 RR)
% Number of literals : 72 ( 45 equ; 28 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 : 92 ( 23 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_x_divide_zero_is_x,negated_conjecture,
divide(a,zero) != a,
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/Axioms/HEN002-0.ax',less_equal_and_equal) ).
cnf(c20,plain,
( ~ less_equal(X85,divide(X85,X86))
| X85 = divide(X85,X86) ),
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/sandbox2/benchmark/Axioms/HEN002-0.ax',quotient_less_equal2) ).
cnf(zero_is_smallest,axiom,
less_equal(zero,X3),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN002-0.ax',zero_is_smallest) ).
cnf(c17,plain,
( ~ less_equal(X36,zero)
| X36 = zero ),
inference(resolution,[status(thm)],[less_equal_and_equal,zero_is_smallest]) ).
cnf(zero_divide_anything_is_zero,axiom,
divide(zero,X13) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',zero_divide_anything_is_zero) ).
cnf(transitivity,axiom,
( X39 != X41
| X41 != X40
| X39 = X40 ),
theory(equality) ).
cnf(c26,plain,
( X68 != divide(zero,X69)
| X68 = zero ),
inference(resolution,[status(thm)],[transitivity,zero_divide_anything_is_zero]) ).
cnf(c7,plain,
zero = divide(zero,X21),
inference(resolution,[status(thm)],[zero_divide_anything_is_zero,symmetry]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c1,axiom,
( X63 != X64
| X65 != X62
| ~ less_equal(X63,X65)
| less_equal(X64,X62) ),
theory(equality) ).
cnf(c53,plain,
( zero != X120
| X121 != X119
| less_equal(X120,X119) ),
inference(resolution,[status(thm)],[c1,zero_is_smallest]) ).
cnf(c110,plain,
( zero != X125
| less_equal(X125,X126) ),
inference(resolution,[status(thm)],[c53,reflexivity]) ).
cnf(c132,plain,
less_equal(divide(zero,X129),X128),
inference(resolution,[status(thm)],[c110,c7]) ).
cnf(c137,plain,
( ~ less_equal(X645,divide(zero,X644))
| X645 = divide(zero,X644) ),
inference(resolution,[status(thm)],[c132,less_equal_and_equal]) ).
cnf(quotient_less_equal1,axiom,
( ~ less_equal(X9,X10)
| divide(X9,X10) = zero ),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN002-0.ax',quotient_less_equal1) ).
cnf(c5,plain,
divide(divide(X27,X28),X27) = zero,
inference(resolution,[status(thm)],[quotient_less_equal1,quotient_smaller_than_numerator]) ).
cnf(c13,plain,
zero = divide(divide(X32,X31),X32),
inference(resolution,[status(thm)],[c5,symmetry]) ).
cnf(c134,plain,
less_equal(divide(divide(X147,X146),X147),X145),
inference(resolution,[status(thm)],[c110,c13]) ).
cnf(c177,plain,
( divide(divide(X1048,X1047),X1048) != X1046
| X1050 != X1049
| less_equal(X1046,X1049) ),
inference(resolution,[status(thm)],[c134,c1]) ).
cnf(quotient_property,axiom,
less_equal(divide(divide(X23,X24),divide(X25,X24)),divide(divide(X23,X25),X24)),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN002-0.ax',quotient_property) ).
cnf(c18,plain,
( ~ less_equal(divide(divide(X80,X79),X81),divide(divide(X80,X81),divide(X79,X81)))
| divide(divide(X80,X79),X81) = divide(divide(X80,X81),divide(X79,X81)) ),
inference(resolution,[status(thm)],[less_equal_and_equal,quotient_property]) ).
cnf(c178,plain,
divide(divide(X1054,X1053),X1054) = divide(divide(X1054,X1054),divide(X1053,X1054)),
inference(resolution,[status(thm)],[c134,c18]) ).
cnf(c2140,plain,
( X3094 != X3093
| less_equal(divide(divide(X3095,X3095),divide(X3092,X3095)),X3093) ),
inference(resolution,[status(thm)],[c178,c177]) ).
cnf(c6641,plain,
less_equal(divide(divide(X3101,X3101),divide(X3100,X3101)),X3102),
inference(resolution,[status(thm)],[c2140,reflexivity]) ).
cnf(c6787,plain,
divide(divide(X3131,X3131),divide(X3132,X3131)) = zero,
inference(resolution,[status(thm)],[c6641,c17]) ).
cnf(c6889,plain,
less_equal(divide(X3142,X3142),divide(X3141,X3142)),
inference(resolution,[status(thm)],[c6787,quotient_less_equal2]) ).
cnf(c6936,plain,
divide(X3143,X3143) = divide(zero,X3143),
inference(resolution,[status(thm)],[c6889,c137]) ).
cnf(c6966,plain,
divide(X3144,X3144) = zero,
inference(resolution,[status(thm)],[c6936,c26]) ).
cnf(c54,plain,
( divide(divide(X284,X287),divide(X285,X287)) != X283
| divide(divide(X284,X285),X287) != X286
| less_equal(X283,X286) ),
inference(resolution,[status(thm)],[c1,quotient_property]) ).
cnf(c0,axiom,
( X50 != X51
| X52 != X49
| divide(X50,X52) = divide(X51,X49) ),
theory(equality) ).
cnf(c38,plain,
( X142 != X143
| divide(X142,divide(zero,X141)) = divide(X143,zero) ),
inference(resolution,[status(thm)],[c0,zero_divide_anything_is_zero]) ).
cnf(c168,plain,
divide(X548,divide(zero,X547)) = divide(X548,zero),
inference(resolution,[status(thm)],[c38,reflexivity]) ).
cnf(c921,plain,
( divide(divide(X8188,zero),X8187) != X8186
| less_equal(divide(divide(X8188,X8187),zero),X8186) ),
inference(resolution,[status(thm)],[c168,c54]) ).
cnf(c30094,plain,
less_equal(divide(divide(X15921,divide(X15921,zero)),zero),zero),
inference(resolution,[status(thm)],[c921,c6966]) ).
cnf(c79353,plain,
divide(divide(X20110,divide(X20110,zero)),zero) = zero,
inference(resolution,[status(thm)],[c30094,c17]) ).
cnf(c108970,plain,
less_equal(divide(X20125,divide(X20125,zero)),zero),
inference(resolution,[status(thm)],[c79353,quotient_less_equal2]) ).
cnf(c109362,plain,
divide(X20126,divide(X20126,zero)) = zero,
inference(resolution,[status(thm)],[c108970,c17]) ).
cnf(c109461,plain,
less_equal(X20132,divide(X20132,zero)),
inference(resolution,[status(thm)],[c109362,quotient_less_equal2]) ).
cnf(c109495,plain,
X20133 = divide(X20133,zero),
inference(resolution,[status(thm)],[c109461,c20]) ).
cnf(c109599,plain,
divide(X20140,zero) = X20140,
inference(resolution,[status(thm)],[c109495,symmetry]) ).
cnf(c109691,plain,
$false,
inference(resolution,[status(thm)],[c109599,prove_x_divide_zero_is_x]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : HEN004-6 : TPTP v8.1.2. Released v1.0.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n019.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 13:51:23 EDT 2024
% 0.13/0.34 % CPUTime :
% 169.56/169.80 % Version: 1.5
% 169.56/169.80 % SZS status Unsatisfiable
% 169.56/169.80 % SZS output start CNFRefutation
% See solution above
% 169.56/169.80
% 169.56/169.80 % Initial clauses : 15
% 169.56/169.80 % Processed clauses : 1348
% 169.56/169.80 % Factors computed : 13
% 169.56/169.80 % Resolvents computed: 109894
% 169.56/169.80 % Tautologies deleted: 2
% 169.56/169.80 % Forward subsumed : 7788
% 169.56/169.80 % Backward subsumed : 380
% 169.56/169.80 % -------- CPU Time ---------
% 169.56/169.80 % User time : 169.165 s
% 169.56/169.80 % System time : 0.275 s
% 169.56/169.80 % Total time : 169.440 s
%------------------------------------------------------------------------------