%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : HEN010-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:32:02 AM UTC 2026
% Result : Unsatisfiable 5.22s 1.11s
% Output : CNFRefutation 5.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 12
% Syntax : Number of formulae : 137 ( 77 unt; 0 def)
% Number of atoms : 261 ( 44 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 254 ( 130 ~; 124 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% Number of variables : 243 ( 45 sgn 21 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(quotient_less_equal,axiom,
! [VAR_0,VAR_1] :
( quotient(VAR_0,VAR_1,zero)
| ~ less_equal(VAR_0,VAR_1) ),
file('theBenchmark.p',quotient_less_equal) ).
cnf(c_1,plain,
( quotient(A,B,zero)
| ~ less_equal(A,B) ),
inference(clausify,[status(thm)],[quotient_less_equal]) ).
fof(less_equal_quotient,axiom,
! [VAR_0,VAR_1] :
( less_equal(VAR_0,VAR_1)
| ~ quotient(VAR_0,VAR_1,zero) ),
file('theBenchmark.p',less_equal_quotient) ).
cnf(c_2,plain,
( less_equal(A,B)
| ~ quotient(A,B,zero) ),
inference(clausify,[status(thm)],[less_equal_quotient]) ).
fof(divisor_existence,axiom,
! [VAR_0,VAR_1,VAR_2] :
( less_equal(VAR_2,VAR_0)
| ~ quotient(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',divisor_existence) ).
cnf(c_3,plain,
( less_equal(C,A)
| ~ quotient(A,B,C) ),
inference(clausify,[status(thm)],[divisor_existence]) ).
fof(quotient_property,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7] :
( less_equal(VAR_6,VAR_7)
| ~ quotient(VAR_2,VAR_3,VAR_7)
| ~ quotient(VAR_5,VAR_4,VAR_6)
| ~ quotient(VAR_0,VAR_3,VAR_5)
| ~ quotient(VAR_1,VAR_3,VAR_4)
| ~ quotient(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',quotient_property) ).
cnf(c_4,plain,
( less_equal(V6,V7)
| ~ quotient(C,D,V7)
| ~ quotient(F,E,V6)
| ~ quotient(A,D,F)
| ~ quotient(B,D,E)
| ~ quotient(A,B,C) ),
inference(clausify,[status(thm)],[quotient_property]) ).
fof(zero_is_smallest,axiom,
! [VAR_0] : less_equal(zero,VAR_0),
file('theBenchmark.p',zero_is_smallest) ).
cnf(c_5,plain,
less_equal(zero,A),
inference(clausify,[status(thm)],[zero_is_smallest]) ).
fof(less_equal_and_equal,axiom,
! [VAR_0,VAR_1] :
( VAR_0 = VAR_1
| ~ less_equal(VAR_1,VAR_0)
| ~ less_equal(VAR_0,VAR_1) ),
file('theBenchmark.p',less_equal_and_equal) ).
cnf(c_6,plain,
( A = B
| ~ less_equal(B,A)
| ~ less_equal(A,B) ),
inference(clausify,[status(thm)],[less_equal_and_equal]) ).
fof(identity_is_largest,axiom,
! [VAR_0] : less_equal(VAR_0,identity),
file('theBenchmark.p',identity_is_largest) ).
cnf(c_7,plain,
less_equal(A,identity),
inference(clausify,[status(thm)],[identity_is_largest]) ).
fof(closure,axiom,
! [VAR_0,VAR_1] : quotient(VAR_0,VAR_1,divide(VAR_0,VAR_1)),
file('theBenchmark.p',closure) ).
cnf(c_8,plain,
quotient(A,B,divide(A,B)),
inference(clausify,[status(thm)],[closure]) ).
fof(identity_divide_a,axiom,
quotient(identity,a,idQa),
file('theBenchmark.p',identity_divide_a) ).
cnf(c_10,plain,
quotient(identity,a,idQa),
inference(clausify,[status(thm)],[identity_divide_a]) ).
fof(identity_divide_idQa,axiom,
quotient(identity,idQa,idQ_idQa),
file('theBenchmark.p',identity_divide_idQa) ).
cnf(c_11,plain,
quotient(identity,idQa,idQ_idQa),
inference(clausify,[status(thm)],[identity_divide_idQa]) ).
fof(identity_divide_idQ_idQa,axiom,
quotient(idQa,idQ_idQa,idQa_Q__idQ_idQa),
file('theBenchmark.p',identity_divide_idQ_idQa) ).
cnf(c_12,plain,
quotient(idQa,idQ_idQa,idQa_Q__idQ_idQa),
inference(clausify,[status(thm)],[identity_divide_idQ_idQa]) ).
fof(prove_idQa_equals_idQa_Q__idQ_idQa,axiom,
idQa != idQa_Q__idQ_idQa,
file('theBenchmark.p',prove_idQa_equals_idQa_Q__idQ_idQa) ).
cnf(c_13,plain,
idQa != idQa_Q__idQ_idQa,
inference(clausify,[status(thm)],[prove_idQa_equals_idQa_Q__idQ_idQa]) ).
cnf(c_14,plain,
idQa_Q__idQ_idQa != idQa,
inference(copy,[status(thm)],[c_13]) ).
cnf(c_15,plain,
quotient(zero,A,zero),
inference(resolve,[status(thm)],[c_1,c_5]) ).
cnf(c_16,plain,
quotient(A,identity,zero),
inference(resolve,[status(thm)],[c_1,c_7]) ).
cnf(c_916,plain,
( less_equal(F,V6)
| ~ quotient(divide(D,A),B,V6)
| ~ quotient(E,C,F)
| ~ quotient(D,B,E)
| ~ quotient(A,B,C) ),
inference(resolve,[status(thm)],[c_4,c_8]) ).
cnf(c_917,plain,
( less_equal(E,F)
| ~ quotient(divide(A,D),B,F)
| ~ quotient(C,divide(D,B),E)
| ~ quotient(A,B,C) ),
inference(resolve,[status(thm)],[c_916,c_8]) ).
cnf(c_918,plain,
( less_equal(D,E)
| ~ quotient(divide(A,C),B,E)
| ~ quotient(divide(A,B),divide(C,B),D) ),
inference(resolve,[status(thm)],[c_917,c_8]) ).
cnf(c_919,plain,
( less_equal(divide(divide(A,C),divide(B,C)),D)
| ~ quotient(divide(A,B),C,D) ),
inference(resolve,[status(thm)],[c_918,c_8]) ).
cnf(c_17,plain,
less_equal(divide(divide(A,B),divide(C,B)),divide(divide(A,C),B)),
inference(resolve,[status(thm)],[c_919,c_8]) ).
cnf(c_18,plain,
less_equal(divide(A,B),A),
inference(resolve,[status(thm)],[c_3,c_8]) ).
cnf(c_920,plain,
( less_equal(D,E)
| ~ quotient(idQa,A,E)
| ~ quotient(C,B,D)
| ~ quotient(identity,A,C)
| ~ quotient(a,A,B) ),
inference(resolve,[status(thm)],[c_4,c_10]) ).
cnf(c_921,plain,
( less_equal(C,D)
| ~ quotient(idQa,A,D)
| ~ quotient(B,divide(a,A),C)
| ~ quotient(identity,A,B) ),
inference(resolve,[status(thm)],[c_920,c_8]) ).
cnf(c_922,plain,
( less_equal(A,B)
| ~ quotient(idQa,idQa,B)
| ~ quotient(idQ_idQa,divide(a,idQa),A) ),
inference(resolve,[status(thm)],[c_921,c_11]) ).
cnf(c_923,plain,
( less_equal(divide(idQ_idQa,divide(a,idQa)),A)
| ~ quotient(idQa,idQa,A) ),
inference(resolve,[status(thm)],[c_922,c_8]) ).
cnf(c_27,plain,
less_equal(divide(idQ_idQa,divide(a,idQa)),divide(idQa,idQa)),
inference(resolve,[status(thm)],[c_923,c_8]) ).
cnf(c_924,plain,
( less_equal(F,V6)
| ~ quotient(divide(D,A),B,V6)
| ~ quotient(E,C,F)
| ~ quotient(D,B,E)
| ~ quotient(A,B,C) ),
inference(resolve,[status(thm)],[c_4,c_8]) ).
cnf(c_925,plain,
( less_equal(C,D)
| ~ quotient(divide(A,idQa),idQ_idQa,D)
| ~ quotient(B,idQa_Q__idQ_idQa,C)
| ~ quotient(A,idQ_idQa,B) ),
inference(resolve,[status(thm)],[c_924,c_12]) ).
cnf(c_926,plain,
( less_equal(B,C)
| ~ quotient(divide(A,idQa),idQ_idQa,C)
| ~ quotient(divide(A,idQ_idQa),idQa_Q__idQ_idQa,B) ),
inference(resolve,[status(thm)],[c_925,c_8]) ).
cnf(c_927,plain,
( less_equal(divide(divide(A,idQ_idQa),idQa_Q__idQ_idQa),B)
| ~ quotient(divide(A,idQa),idQ_idQa,B) ),
inference(resolve,[status(thm)],[c_926,c_8]) ).
cnf(c_39,plain,
less_equal(divide(divide(A,idQ_idQa),idQa_Q__idQ_idQa),divide(divide(A,idQa),idQ_idQa)),
inference(resolve,[status(thm)],[c_927,c_8]) ).
cnf(c_41,plain,
less_equal(idQa_Q__idQ_idQa,idQa),
inference(resolve,[status(thm)],[c_3,c_12]) ).
cnf(c_928,plain,
( less_equal(E,F)
| ~ quotient(zero,A,F)
| ~ quotient(D,B,E)
| ~ quotient(C,A,D)
| ~ quotient(identity,A,B) ),
inference(resolve,[status(thm)],[c_4,c_16]) ).
cnf(c_929,plain,
( less_equal(C,D)
| ~ quotient(zero,idQa,D)
| ~ quotient(B,idQ_idQa,C)
| ~ quotient(A,idQa,B) ),
inference(resolve,[status(thm)],[c_928,c_11]) ).
cnf(c_930,plain,
( less_equal(B,C)
| ~ quotient(zero,idQa,C)
| ~ quotient(divide(A,idQa),idQ_idQa,B) ),
inference(resolve,[status(thm)],[c_929,c_8]) ).
cnf(c_931,plain,
( less_equal(divide(divide(B,idQa),idQ_idQa),A)
| ~ quotient(zero,idQa,A) ),
inference(resolve,[status(thm)],[c_930,c_8]) ).
cnf(c_51,plain,
less_equal(divide(divide(A,idQa),idQ_idQa),zero),
inference(resolve,[status(thm)],[c_931,c_15]) ).
cnf(c_932,plain,
( less_equal(E,F)
| ~ quotient(zero,A,F)
| ~ quotient(D,B,E)
| ~ quotient(C,A,D)
| ~ quotient(identity,A,B) ),
inference(resolve,[status(thm)],[c_4,c_16]) ).
cnf(c_933,plain,
( less_equal(C,D)
| ~ quotient(zero,a,D)
| ~ quotient(B,idQa,C)
| ~ quotient(A,a,B) ),
inference(resolve,[status(thm)],[c_932,c_10]) ).
cnf(c_934,plain,
( less_equal(A,B)
| ~ quotient(zero,a,B)
| ~ quotient(idQa,idQa,A) ),
inference(resolve,[status(thm)],[c_933,c_10]) ).
cnf(c_935,plain,
( less_equal(divide(idQa,idQa),A)
| ~ quotient(zero,a,A) ),
inference(resolve,[status(thm)],[c_934,c_8]) ).
cnf(c_52,plain,
less_equal(divide(idQa,idQa),zero),
inference(resolve,[status(thm)],[c_935,c_15]) ).
cnf(c_936,plain,
( less_equal(E,F)
| ~ quotient(zero,A,F)
| ~ quotient(D,B,E)
| ~ quotient(C,A,D)
| ~ quotient(identity,A,B) ),
inference(resolve,[status(thm)],[c_4,c_16]) ).
cnf(c_937,plain,
( less_equal(C,D)
| ~ quotient(zero,a,D)
| ~ quotient(B,idQa,C)
| ~ quotient(A,a,B) ),
inference(resolve,[status(thm)],[c_936,c_10]) ).
cnf(c_938,plain,
( less_equal(B,C)
| ~ quotient(zero,a,C)
| ~ quotient(divide(A,a),idQa,B) ),
inference(resolve,[status(thm)],[c_937,c_8]) ).
cnf(c_939,plain,
( less_equal(divide(divide(B,a),idQa),A)
| ~ quotient(zero,a,A) ),
inference(resolve,[status(thm)],[c_938,c_8]) ).
cnf(c_53,plain,
less_equal(divide(divide(A,a),idQa),zero),
inference(resolve,[status(thm)],[c_939,c_15]) ).
cnf(c_940,plain,
( less_equal(E,F)
| ~ quotient(zero,A,F)
| ~ quotient(D,B,E)
| ~ quotient(C,A,D)
| ~ quotient(identity,A,B) ),
inference(resolve,[status(thm)],[c_4,c_16]) ).
cnf(c_941,plain,
( less_equal(D,E)
| ~ quotient(zero,B,E)
| ~ quotient(C,divide(identity,B),D)
| ~ quotient(A,B,C) ),
inference(resolve,[status(thm)],[c_940,c_8]) ).
cnf(c_942,plain,
( less_equal(C,D)
| ~ quotient(zero,B,D)
| ~ quotient(divide(A,B),divide(identity,B),C) ),
inference(resolve,[status(thm)],[c_941,c_8]) ).
cnf(c_943,plain,
( less_equal(divide(divide(C,A),divide(identity,A)),B)
| ~ quotient(zero,A,B) ),
inference(resolve,[status(thm)],[c_942,c_8]) ).
cnf(c_55,plain,
less_equal(divide(divide(A,B),divide(identity,B)),zero),
inference(resolve,[status(thm)],[c_943,c_15]) ).
cnf(c_944,plain,
( idQa = idQa_Q__idQ_idQa
| ~ less_equal(idQa,idQa_Q__idQ_idQa) ),
inference(resolve,[status(thm)],[c_6,c_41]) ).
cnf(c_945,plain,
idQa != idQa_Q__idQ_idQa,
inference(copy,[status(thm)],[c_14]) ).
cnf(c_58,plain,
~ less_equal(idQa,idQa_Q__idQ_idQa),
inference(resolve,[status(thm)],[c_944,c_945]) ).
cnf(c_65,plain,
quotient(divide(A,B),A,zero),
inference(resolve,[status(thm)],[c_1,c_18]) ).
cnf(c_67,plain,
~ quotient(idQa_Q__idQ_idQa,A,idQa),
inference(resolve,[status(thm)],[c_3,c_58]) ).
cnf(c_946,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_947,plain,
zero = divide(idQa,idQa),
inference(resolve,[status(thm)],[c_946,c_52]) ).
cnf(c_75,plain,
divide(idQa,idQa) = zero,
inference(copy,[status(thm)],[c_947]) ).
cnf(c_77,plain,
less_equal(divide(idQ_idQa,divide(a,idQa)),zero),
inference(paramod,[status(thm)],[c_75,c_27]) ).
cnf(c_948,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_949,plain,
zero = divide(divide(A,idQa),idQ_idQa),
inference(resolve,[status(thm)],[c_948,c_51]) ).
cnf(c_125,plain,
divide(divide(A,idQa),idQ_idQa) = zero,
inference(copy,[status(thm)],[c_949]) ).
cnf(c_127,plain,
less_equal(divide(divide(A,idQ_idQa),idQa_Q__idQ_idQa),zero),
inference(paramod,[status(thm)],[c_125,c_39]) ).
cnf(c_950,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_951,plain,
zero = divide(divide(A,a),idQa),
inference(resolve,[status(thm)],[c_950,c_53]) ).
cnf(c_128,plain,
divide(divide(A,a),idQa) = zero,
inference(copy,[status(thm)],[c_951]) ).
cnf(c_952,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_953,plain,
zero = divide(idQ_idQa,divide(a,idQa)),
inference(resolve,[status(thm)],[c_952,c_77]) ).
cnf(c_132,plain,
divide(idQ_idQa,divide(a,idQa)) = zero,
inference(copy,[status(thm)],[c_953]) ).
cnf(c_134,plain,
quotient(divide(A,idQa),idQ_idQa,zero),
inference(paramod,[status(thm)],[c_125,c_8]) ).
cnf(c_139,plain,
less_equal(divide(A,idQa),idQ_idQa),
inference(resolve,[status(thm)],[c_2,c_134]) ).
cnf(c_954,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_955,plain,
zero = divide(divide(A,B),divide(identity,B)),
inference(resolve,[status(thm)],[c_954,c_55]) ).
cnf(c_140,plain,
divide(divide(A,B),divide(identity,B)) = zero,
inference(copy,[status(thm)],[c_955]) ).
cnf(c_956,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_957,plain,
zero = divide(divide(A,idQ_idQa),idQa_Q__idQ_idQa),
inference(resolve,[status(thm)],[c_956,c_127]) ).
cnf(c_162,plain,
divide(divide(A,idQ_idQa),idQa_Q__idQ_idQa) = zero,
inference(copy,[status(thm)],[c_957]) ).
cnf(c_163,plain,
quotient(divide(A,a),idQa,zero),
inference(paramod,[status(thm)],[c_128,c_8]) ).
cnf(c_172,plain,
less_equal(divide(A,a),idQa),
inference(resolve,[status(thm)],[c_2,c_163]) ).
cnf(c_187,plain,
quotient(idQ_idQa,divide(a,idQa),zero),
inference(paramod,[status(thm)],[c_132,c_8]) ).
cnf(c_197,plain,
less_equal(idQ_idQa,divide(a,idQa)),
inference(resolve,[status(thm)],[c_2,c_187]) ).
cnf(c_958,plain,
( divide(A,idQa) = idQ_idQa
| ~ less_equal(idQ_idQa,divide(A,idQa)) ),
inference(resolve,[status(thm)],[c_6,c_139]) ).
cnf(c_198,plain,
divide(a,idQa) = idQ_idQa,
inference(resolve,[status(thm)],[c_958,c_197]) ).
cnf(c_203,plain,
quotient(idQ_idQa,a,zero),
inference(paramod,[status(thm)],[c_198,c_65]) ).
cnf(c_959,plain,
( less_equal(D,E)
| ~ quotient(zero,A,E)
| ~ quotient(C,B,D)
| ~ quotient(idQ_idQa,A,C)
| ~ quotient(a,A,B) ),
inference(resolve,[status(thm)],[c_4,c_203]) ).
cnf(c_960,plain,
( less_equal(C,D)
| ~ quotient(zero,A,D)
| ~ quotient(B,divide(a,A),C)
| ~ quotient(idQ_idQa,A,B) ),
inference(resolve,[status(thm)],[c_959,c_8]) ).
cnf(c_961,plain,
( less_equal(B,C)
| ~ quotient(zero,A,C)
| ~ quotient(divide(idQ_idQa,A),divide(a,A),B) ),
inference(resolve,[status(thm)],[c_960,c_8]) ).
cnf(c_962,plain,
( less_equal(divide(divide(idQ_idQa,A),divide(a,A)),B)
| ~ quotient(zero,A,B) ),
inference(resolve,[status(thm)],[c_961,c_8]) ).
cnf(c_240,plain,
less_equal(divide(divide(idQ_idQa,A),divide(a,A)),zero),
inference(resolve,[status(thm)],[c_962,c_15]) ).
cnf(c_280,plain,
less_equal(divide(divide(A,idQa_Q__idQ_idQa),divide(idQ_idQa,idQa_Q__idQ_idQa)),zero),
inference(paramod,[status(thm)],[c_162,c_17]) ).
cnf(c_489,plain,
quotient(divide(A,B),divide(identity,B),zero),
inference(paramod,[status(thm)],[c_140,c_8]) ).
cnf(c_516,plain,
less_equal(divide(A,B),divide(identity,B)),
inference(resolve,[status(thm)],[c_2,c_489]) ).
cnf(c_963,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_964,plain,
zero = divide(divide(idQ_idQa,A),divide(a,A)),
inference(resolve,[status(thm)],[c_963,c_240]) ).
cnf(c_532,plain,
divide(divide(idQ_idQa,A),divide(a,A)) = zero,
inference(copy,[status(thm)],[c_964]) ).
cnf(c_965,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_966,plain,
zero = divide(divide(A,idQa_Q__idQ_idQa),divide(idQ_idQa,idQa_Q__idQ_idQa)),
inference(resolve,[status(thm)],[c_965,c_280]) ).
cnf(c_567,plain,
divide(divide(A,idQa_Q__idQ_idQa),divide(idQ_idQa,idQa_Q__idQ_idQa)) = zero,
inference(copy,[status(thm)],[c_966]) ).
cnf(c_574,plain,
quotient(divide(idQ_idQa,A),divide(a,A),zero),
inference(paramod,[status(thm)],[c_532,c_8]) ).
cnf(c_588,plain,
less_equal(divide(idQ_idQa,A),divide(a,A)),
inference(resolve,[status(thm)],[c_2,c_574]) ).
cnf(c_589,plain,
quotient(divide(A,idQa_Q__idQ_idQa),divide(idQ_idQa,idQa_Q__idQ_idQa),zero),
inference(paramod,[status(thm)],[c_567,c_8]) ).
cnf(c_695,plain,
less_equal(divide(A,idQa_Q__idQ_idQa),divide(idQ_idQa,idQa_Q__idQ_idQa)),
inference(resolve,[status(thm)],[c_2,c_589]) ).
cnf(c_967,plain,
( divide(idQ_idQa,A) = divide(a,A)
| ~ less_equal(divide(a,A),divide(idQ_idQa,A)) ),
inference(resolve,[status(thm)],[c_6,c_588]) ).
cnf(c_968,plain,
divide(idQ_idQa,idQa_Q__idQ_idQa) = divide(a,idQa_Q__idQ_idQa),
inference(resolve,[status(thm)],[c_967,c_695]) ).
cnf(c_696,plain,
divide(a,idQa_Q__idQ_idQa) = divide(idQ_idQa,idQa_Q__idQ_idQa),
inference(copy,[status(thm)],[c_968]) ).
cnf(c_969,plain,
( divide(B,A) = divide(identity,A)
| ~ less_equal(divide(identity,A),divide(B,A)) ),
inference(resolve,[status(thm)],[c_6,c_516]) ).
cnf(c_697,plain,
divide(idQ_idQa,idQa_Q__idQ_idQa) = divide(identity,idQa_Q__idQ_idQa),
inference(resolve,[status(thm)],[c_969,c_695]) ).
cnf(c_698,plain,
divide(a,idQa_Q__idQ_idQa) = divide(identity,idQa_Q__idQ_idQa),
inference(paramod,[status(thm)],[c_697,c_696]) ).
cnf(c_805,plain,
quotient(divide(identity,idQa_Q__idQ_idQa),a,zero),
inference(paramod,[status(thm)],[c_698,c_65]) ).
cnf(c_970,plain,
( less_equal(F,V6)
| ~ quotient(divide(D,A),B,V6)
| ~ quotient(E,C,F)
| ~ quotient(D,B,E)
| ~ quotient(A,B,C) ),
inference(resolve,[status(thm)],[c_4,c_8]) ).
cnf(c_971,plain,
( less_equal(E,F)
| ~ quotient(divide(A,D),B,F)
| ~ quotient(C,divide(D,B),E)
| ~ quotient(A,B,C) ),
inference(resolve,[status(thm)],[c_970,c_8]) ).
cnf(c_972,plain,
( less_equal(B,C)
| ~ quotient(divide(identity,A),a,C)
| ~ quotient(idQa,divide(A,a),B) ),
inference(resolve,[status(thm)],[c_971,c_10]) ).
cnf(c_973,plain,
( less_equal(divide(idQa,divide(A,a)),B)
| ~ quotient(divide(identity,A),a,B) ),
inference(resolve,[status(thm)],[c_972,c_8]) ).
cnf(c_820,plain,
less_equal(divide(idQa,divide(idQa_Q__idQ_idQa,a)),zero),
inference(resolve,[status(thm)],[c_973,c_805]) ).
cnf(c_974,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_975,plain,
zero = divide(idQa,divide(idQa_Q__idQ_idQa,a)),
inference(resolve,[status(thm)],[c_974,c_820]) ).
cnf(c_858,plain,
divide(idQa,divide(idQa_Q__idQ_idQa,a)) = zero,
inference(copy,[status(thm)],[c_975]) ).
cnf(c_889,plain,
quotient(idQa,divide(idQa_Q__idQ_idQa,a),zero),
inference(paramod,[status(thm)],[c_858,c_8]) ).
cnf(c_912,plain,
less_equal(idQa,divide(idQa_Q__idQ_idQa,a)),
inference(resolve,[status(thm)],[c_2,c_889]) ).
cnf(c_976,plain,
( divide(A,a) = idQa
| ~ less_equal(idQa,divide(A,a)) ),
inference(resolve,[status(thm)],[c_6,c_172]) ).
cnf(c_913,plain,
divide(idQa_Q__idQ_idQa,a) = idQa,
inference(resolve,[status(thm)],[c_976,c_912]) ).
cnf(c_914,plain,
quotient(idQa_Q__idQ_idQa,a,idQa),
inference(paramod,[status(thm)],[c_913,c_8]) ).
cnf(c_915,plain,
$false,
inference(resolve,[status(thm)],[c_914,c_67]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : HEN010-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.42 % Computer : n015.cluster.edu
% 0.13/0.42 % Model : x86_64 x86_64
% 0.13/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.42 % Memory : 8046.5625MB
% 0.13/0.42 % OS : Linux 6.8.0-71-generic
% 0.13/0.42 % CPULimit : 300
% 0.13/0.42 % WCLimit : 300
% 0.13/0.42 % DateTime : Fri Sep 25 16:00:57 UTC 2026
% 0.13/0.43 % CPUTime :
% 0.13/0.43 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.43 % Process 1778184 was started by sandbox2 on n015,
% 0.13/0.43 % Fri Sep 25 16:00:57 2026
% 0.13/0.43 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.13/0.44
% 0.13/0.44 % From the command line: assign(max_seconds, 300).
% 5.22/1.11
% 5.22/1.11 % SZS status Unsatisfiable for theBenchmark
% 5.22/1.11
% 5.22/1.11 % Proof 1 at 0.52 (+ 0.15) seconds.
% 5.22/1.11 % Length of proof is 64.
% 5.22/1.11 % Level of proof is 23.
% 5.22/1.11 % Maximum clause weight is 43.000.
% 5.22/1.11 % Given clauses 214.
% 5.22/1.11
% 5.22/1.11 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------