%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : HEN009-2 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n029.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:50 EDT 2024
% Result : Unsatisfiable 2.34s 2.50s
% Output : Refutation 2.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 9
% Syntax : Number of clauses : 22 ( 11 unt; 0 nHn; 20 RR)
% Number of literals : 41 ( 4 equ; 20 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 22 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_one_inversion_equals_three,negated_conjecture,
idQa != idQ__idQ_idQa,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_one_inversion_equals_three) ).
cnf(x_divide_x_is_zero,axiom,
quotient(X5,X5,zero),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',x_divide_x_is_zero) ).
cnf(less_equal_quotient,axiom,
( ~ quotient(X14,X13,zero)
| less_equal(X14,X13) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',less_equal_quotient) ).
cnf(c6,plain,
less_equal(X15,X15),
inference(resolution,[status(thm)],[less_equal_quotient,x_divide_x_is_zero]) ).
cnf(identity_divide_a,plain,
quotient(identity,a,idQa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity_divide_a) ).
cnf(identity_divide_idQa,plain,
quotient(identity,idQa,idQ_idQa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity_divide_idQa) ).
cnf(xQyLEz_implies_xQzLEy,axiom,
( ~ quotient(X68,X70,X67)
| ~ less_equal(X67,X71)
| ~ quotient(X68,X71,X69)
| less_equal(X69,X70) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',xQyLEz_implies_xQzLEy) ).
cnf(c63,plain,
( ~ quotient(identity,X338,X339)
| ~ less_equal(X339,idQa)
| less_equal(idQ_idQa,X338) ),
inference(resolution,[status(thm)],[xQyLEz_implies_xQzLEy,identity_divide_idQa]) ).
cnf(c516,plain,
( ~ less_equal(idQa,idQa)
| less_equal(idQ_idQa,a) ),
inference(resolution,[status(thm)],[c63,identity_divide_a]) ).
cnf(c1689,plain,
less_equal(idQ_idQa,a),
inference(resolution,[status(thm)],[c516,c6]) ).
cnf(identity_divide_idQ_idQa,plain,
quotient(identity,idQ_idQa,idQ__idQ_idQa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity_divide_idQ_idQa) ).
cnf(xLEy_implies_zQyLEzQx,axiom,
( ~ less_equal(X80,X82)
| ~ quotient(X83,X82,X79)
| ~ quotient(X83,X80,X81)
| less_equal(X79,X81) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',xLEy_implies_zQyLEzQx) ).
cnf(c85,plain,
( ~ less_equal(idQ_idQa,X481)
| ~ quotient(identity,X481,X482)
| less_equal(X482,idQ__idQ_idQa) ),
inference(resolution,[status(thm)],[xLEy_implies_zQyLEzQx,identity_divide_idQ_idQa]) ).
cnf(c749,plain,
( ~ less_equal(idQ_idQa,a)
| less_equal(idQa,idQ__idQ_idQa) ),
inference(resolution,[status(thm)],[c85,identity_divide_a]) ).
cnf(c3458,plain,
less_equal(idQa,idQ__idQ_idQa),
inference(resolution,[status(thm)],[c749,c1689]) ).
cnf(less_equal_and_equal,axiom,
( ~ less_equal(X38,X37)
| ~ less_equal(X37,X38)
| X38 = X37 ),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',less_equal_and_equal) ).
cnf(c67,plain,
( ~ quotient(identity,X360,X361)
| ~ less_equal(X361,idQ_idQa)
| less_equal(idQ__idQ_idQa,X360) ),
inference(resolution,[status(thm)],[xQyLEz_implies_xQzLEy,identity_divide_idQ_idQa]) ).
cnf(c588,plain,
( ~ less_equal(idQ_idQa,idQ_idQa)
| less_equal(idQ__idQ_idQa,idQa) ),
inference(resolution,[status(thm)],[c67,identity_divide_idQa]) ).
cnf(c2283,plain,
less_equal(idQ__idQ_idQa,idQa),
inference(resolution,[status(thm)],[c588,c6]) ).
cnf(c2285,plain,
( ~ less_equal(idQa,idQ__idQ_idQa)
| idQa = idQ__idQ_idQa ),
inference(resolution,[status(thm)],[c2283,less_equal_and_equal]) ).
cnf(c4627,plain,
idQa = idQ__idQ_idQa,
inference(resolution,[status(thm)],[c2285,c3458]) ).
cnf(c4664,plain,
$false,
inference(resolution,[status(thm)],[c4627,prove_one_inversion_equals_three]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : HEN009-2 : TPTP v8.1.2. Released v1.0.0.
% 0.03/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n029.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:53:53 EDT 2024
% 0.14/0.36 % CPUTime :
% 2.34/2.50 % Version: 1.5
% 2.34/2.50 % SZS status Unsatisfiable
% 2.34/2.50 % SZS output start CNFRefutation
% See solution above
% 2.34/2.50
% 2.34/2.50 % Initial clauses : 27
% 2.34/2.50 % Processed clauses : 356
% 2.34/2.50 % Factors computed : 142
% 2.34/2.50 % Resolvents computed: 4533
% 2.34/2.50 % Tautologies deleted: 15
% 2.34/2.50 % Forward subsumed : 980
% 2.34/2.50 % Backward subsumed : 15
% 2.34/2.50 % -------- CPU Time ---------
% 2.34/2.50 % User time : 2.124 s
% 2.34/2.50 % System time : 0.014 s
% 2.34/2.50 % Total time : 2.138 s
%------------------------------------------------------------------------------