%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : HEN009-5 : TPTP v8.1.2. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n005.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 225.13s 225.38s
% Output : Refutation 225.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 6
% Syntax : Number of clauses : 16 ( 9 unt; 0 nHn; 8 RR)
% Number of literals : 25 ( 24 equ; 10 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% Number of variables : 32 ( 4 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_this,negated_conjecture,
divide(identity,a) != divide(identity,divide(identity,divide(identity,a))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this) ).
cnf(property_of_divide2,axiom,
( divide(X54,X55) != zero
| divide(divide(X56,X55),divide(X56,X54)) = zero ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',property_of_divide2) ).
cnf(property_of_divide1,axiom,
( divide(divide(X44,X45),X46) != zero
| divide(divide(X44,X46),X45) = zero ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',property_of_divide1) ).
cnf(quotient_smaller_than_numerator,axiom,
divide(divide(X8,X9),X8) = zero,
file('/export/starexec/sandbox2/benchmark/Axioms/HEN003-0.ax',quotient_smaller_than_numerator) ).
cnf(transitivity,axiom,
( X21 != X22
| X22 != X23
| X21 = X23 ),
theory(equality) ).
cnf(c12,plain,
( X94 != divide(divide(X92,X93),X92)
| X94 = zero ),
inference(resolution,[status(thm)],[transitivity,quotient_smaller_than_numerator]) ).
cnf(c44,plain,
divide(divide(X48,X48),X49) = zero,
inference(resolution,[status(thm)],[property_of_divide1,quotient_smaller_than_numerator]) ).
cnf(divide_and_equal,axiom,
( divide(X29,X30) != zero
| divide(X30,X29) != zero
| X29 = X30 ),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN003-0.ax',divide_and_equal) ).
cnf(c24,plain,
( divide(X115,divide(X115,X116)) != zero
| X115 = divide(X115,X116) ),
inference(resolution,[status(thm)],[divide_and_equal,quotient_smaller_than_numerator]) ).
cnf(c128,plain,
divide(X118,X118) = divide(divide(X118,X118),X119),
inference(resolution,[status(thm)],[c24,c44]) ).
cnf(c131,plain,
divide(X120,X120) = zero,
inference(resolution,[status(thm)],[c128,c12]) ).
cnf(c137,plain,
divide(divide(X649,divide(X649,X650)),X650) = zero,
inference(resolution,[status(thm)],[c131,property_of_divide1]) ).
cnf(c1398,plain,
divide(divide(X12685,X12687),divide(X12685,divide(X12686,divide(X12686,X12687)))) = zero,
inference(resolution,[status(thm)],[c137,property_of_divide2]) ).
cnf(c1418,plain,
( divide(X12924,divide(X12925,divide(X12925,X12924))) != zero
| X12924 = divide(X12925,divide(X12925,X12924)) ),
inference(resolution,[status(thm)],[c137,divide_and_equal]) ).
cnf(c60600,plain,
divide(X20502,X20503) = divide(X20502,divide(X20502,divide(X20502,X20503))),
inference(resolution,[status(thm)],[c1418,c1398]) ).
cnf(c107889,plain,
$false,
inference(resolution,[status(thm)],[c60600,prove_this]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.14 % Problem : HEN009-5 : TPTP v8.1.2. Bugfixed v1.2.1.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n005.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:51:08 EDT 2024
% 0.14/0.36 % CPUTime :
% 225.13/225.38 % Version: 1.5
% 225.13/225.38 % SZS status Unsatisfiable
% 225.13/225.38 % SZS output start CNFRefutation
% See solution above
% 225.13/225.38
% 225.13/225.38 % Initial clauses : 13
% 225.13/225.38 % Processed clauses : 1405
% 225.13/225.38 % Factors computed : 4
% 225.13/225.38 % Resolvents computed: 108033
% 225.13/225.38 % Tautologies deleted: 5
% 225.13/225.38 % Forward subsumed : 8508
% 225.13/225.38 % Backward subsumed : 78
% 225.13/225.38 % -------- CPU Time ---------
% 225.13/225.38 % User time : 224.679 s
% 225.13/225.38 % System time : 0.310 s
% 225.13/225.38 % Total time : 224.989 s
%------------------------------------------------------------------------------