%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : HEN008-3 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.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:49 EDT 2024
% Result : Unsatisfiable 243.92s 244.10s
% Output : Refutation 243.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 10
% Syntax : Number of clauses : 23 ( 13 unt; 0 nHn; 14 RR)
% Number of literals : 38 ( 19 equ; 16 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 37 ( 5 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_a_divide_c_LE_b_divide_c,negated_conjecture,
~ less_equal(divide(a,c),divide(b,c)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_a_divide_c_LE_b_divide_c) ).
cnf(quotient_less_equal2,axiom,
( divide(X15,X16) != zero
| less_equal(X15,X16) ),
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(less_equal_and_equal,axiom,
( ~ less_equal(X27,X28)
| ~ less_equal(X28,X27)
| X27 = X28 ),
file('/export/starexec/sandbox/benchmark/Axioms/HEN002-0.ax',less_equal_and_equal) ).
cnf(c22,plain,
( ~ less_equal(X33,zero)
| X33 = zero ),
inference(resolution,[status(thm)],[less_equal_and_equal,zero_is_smallest]) ).
cnf(quotient_less_equal1,axiom,
( ~ less_equal(X7,X8)
| divide(X7,X8) = zero ),
file('/export/starexec/sandbox/benchmark/Axioms/HEN002-0.ax',quotient_less_equal1) ).
cnf(symmetry,axiom,
( X9 != X10
| X10 = X9 ),
theory(equality) ).
cnf(a_LE_b,plain,
less_equal(a,b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_LE_b) ).
cnf(c3,plain,
divide(a,b) = zero,
inference(resolution,[status(thm)],[quotient_less_equal1,a_LE_b]) ).
cnf(c14,plain,
zero = divide(a,b),
inference(resolution,[status(thm)],[c3,symmetry]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c1,axiom,
( X53 != X52
| X54 != X55
| ~ less_equal(X53,X54)
| less_equal(X52,X55) ),
theory(equality) ).
cnf(c56,plain,
( zero != X128
| X126 != X127
| less_equal(X128,X127) ),
inference(resolution,[status(thm)],[c1,zero_is_smallest]) ).
cnf(c163,plain,
( zero != X130
| less_equal(X130,X131) ),
inference(resolution,[status(thm)],[c56,reflexivity]) ).
cnf(c181,plain,
less_equal(divide(a,b),X141),
inference(resolution,[status(thm)],[c163,c14]) ).
cnf(c208,plain,
divide(divide(a,b),X293) = zero,
inference(resolution,[status(thm)],[c181,quotient_less_equal1]) ).
cnf(quotient_property,axiom,
less_equal(divide(divide(X22,X23),divide(X24,X23)),divide(divide(X22,X24),X23)),
file('/export/starexec/sandbox/benchmark/Axioms/HEN002-0.ax',quotient_property) ).
cnf(c55,plain,
( divide(divide(X220,X222),divide(X223,X222)) != X221
| divide(divide(X220,X223),X222) != X224
| less_equal(X221,X224) ),
inference(resolution,[status(thm)],[c1,quotient_property]) ).
cnf(c463,plain,
( divide(divide(X3287,X3285),X3288) != X3286
| less_equal(divide(divide(X3287,X3288),divide(X3285,X3288)),X3286) ),
inference(resolution,[status(thm)],[c55,reflexivity]) ).
cnf(c9920,plain,
less_equal(divide(divide(a,X11537),divide(b,X11537)),zero),
inference(resolution,[status(thm)],[c463,c208]) ).
cnf(c57064,plain,
divide(divide(a,X20322),divide(b,X20322)) = zero,
inference(resolution,[status(thm)],[c9920,c22]) ).
cnf(c142092,plain,
less_equal(divide(a,X20331),divide(b,X20331)),
inference(resolution,[status(thm)],[c57064,quotient_less_equal2]) ).
cnf(c142274,plain,
$false,
inference(resolution,[status(thm)],[c142092,prove_a_divide_c_LE_b_divide_c]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : HEN008-3 : TPTP v8.1.2. Released v1.0.0.
% 0.08/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.16/0.36 % Computer : n014.cluster.edu
% 0.16/0.36 % Model : x86_64 x86_64
% 0.16/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.36 % Memory : 8042.1875MB
% 0.16/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.36 % CPULimit : 300
% 0.16/0.36 % WCLimit : 300
% 0.16/0.36 % DateTime : Wed May 8 13:48:53 EDT 2024
% 0.16/0.37 % CPUTime :
% 243.92/244.10 % Version: 1.5
% 243.92/244.10 % SZS status Unsatisfiable
% 243.92/244.10 % SZS output start CNFRefutation
% See solution above
% 243.92/244.10
% 243.92/244.10 % Initial clauses : 14
% 243.92/244.10 % Processed clauses : 1599
% 243.92/244.10 % Factors computed : 15
% 243.92/244.10 % Resolvents computed: 142259
% 243.92/244.10 % Tautologies deleted: 2
% 243.92/244.10 % Forward subsumed : 8764
% 243.92/244.10 % Backward subsumed : 464
% 243.92/244.10 % -------- CPU Time ---------
% 243.92/244.10 % User time : 243.383 s
% 243.92/244.10 % System time : 0.349 s
% 243.92/244.10 % Total time : 243.732 s
%------------------------------------------------------------------------------