%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : HEN011-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 : n005.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:03 AM UTC 2026
% Result : Unsatisfiable 35.36s 5.19s
% Output : CNFRefutation 35.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 16
% Syntax : Number of formulae : 279 ( 155 unt; 0 def)
% Number of atoms : 535 ( 96 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 517 ( 261 ~; 256 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 10 con; 0-2 aty)
% Number of variables : 457 ( 75 sgn 25 !; 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(well_defined,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( VAR_2 = VAR_3
| ~ quotient(VAR_0,VAR_1,VAR_3)
| ~ quotient(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',well_defined) ).
cnf(c_9,plain,
( C = D
| ~ quotient(A,B,D)
| ~ quotient(A,B,C) ),
inference(clausify,[status(thm)],[well_defined]) ).
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_b,axiom,
quotient(identity,b,idQb),
file('theBenchmark.p',identity_divide_b) ).
cnf(c_11,plain,
quotient(identity,b,idQb),
inference(clausify,[status(thm)],[identity_divide_b]) ).
fof(identity_divide_idQb,axiom,
quotient(identity,idQb,idQ_idQb),
file('theBenchmark.p',identity_divide_idQb) ).
cnf(c_12,plain,
quotient(identity,idQb,idQ_idQb),
inference(clausify,[status(thm)],[identity_divide_idQb]) ).
fof(idQa_divide_idQ_idQb,axiom,
quotient(idQa,idQ_idQb,idQa_Q__idQ_idQb),
file('theBenchmark.p',idQa_divide_idQ_idQb) ).
cnf(c_13,plain,
quotient(idQa,idQ_idQb,idQa_Q__idQ_idQb),
inference(clausify,[status(thm)],[idQa_divide_idQ_idQb]) ).
fof(identity_divide_idQa,axiom,
quotient(identity,idQa,idQ_idQa),
file('theBenchmark.p',identity_divide_idQa) ).
cnf(c_14,plain,
quotient(identity,idQa,idQ_idQa),
inference(clausify,[status(thm)],[identity_divide_idQa]) ).
fof(idQb_divide_idQ_idQa,axiom,
quotient(idQb,idQ_idQa,idQb_Q__idQ_idQa),
file('theBenchmark.p',idQb_divide_idQ_idQa) ).
cnf(c_15,plain,
quotient(idQb,idQ_idQa,idQb_Q__idQ_idQa),
inference(clausify,[status(thm)],[idQb_divide_idQ_idQa]) ).
fof(prove_idQa_Q__idQ_idQb_equals_idQb_Q__idQ_idQa,axiom,
idQa_Q__idQ_idQb != idQb_Q__idQ_idQa,
file('theBenchmark.p',prove_idQa_Q__idQ_idQb_equals_idQb_Q__idQ_idQa) ).
cnf(c_16,plain,
idQa_Q__idQ_idQb != idQb_Q__idQ_idQa,
inference(clausify,[status(thm)],[prove_idQa_Q__idQ_idQb_equals_idQb_Q__idQ_idQa]) ).
cnf(c_17,plain,
idQb_Q__idQ_idQa != idQa_Q__idQ_idQb,
inference(copy,[status(thm)],[c_16]) ).
cnf(c_18,plain,
quotient(zero,A,zero),
inference(resolve,[status(thm)],[c_1,c_5]) ).
cnf(c_19,plain,
quotient(A,identity,zero),
inference(resolve,[status(thm)],[c_1,c_7]) ).
cnf(c_2943,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_2944,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_2943,c_8]) ).
cnf(c_2945,plain,
( less_equal(D,E)
| ~ quotient(divide(A,C),B,E)
| ~ quotient(divide(A,B),divide(C,B),D) ),
inference(resolve,[status(thm)],[c_2944,c_8]) ).
cnf(c_2946,plain,
( less_equal(divide(divide(A,C),divide(B,C)),D)
| ~ quotient(divide(A,B),C,D) ),
inference(resolve,[status(thm)],[c_2945,c_8]) ).
cnf(c_20,plain,
less_equal(divide(divide(A,B),divide(C,B)),divide(divide(A,C),B)),
inference(resolve,[status(thm)],[c_2946,c_8]) ).
cnf(c_21,plain,
less_equal(divide(A,B),A),
inference(resolve,[status(thm)],[c_3,c_8]) ).
cnf(c_2947,plain,
( less_equal(D,E)
| ~ quotient(idQb,A,E)
| ~ quotient(C,B,D)
| ~ quotient(identity,A,C)
| ~ quotient(b,A,B) ),
inference(resolve,[status(thm)],[c_4,c_11]) ).
cnf(c_2948,plain,
( less_equal(C,D)
| ~ quotient(idQb,A,D)
| ~ quotient(B,divide(b,A),C)
| ~ quotient(identity,A,B) ),
inference(resolve,[status(thm)],[c_2947,c_8]) ).
cnf(c_2949,plain,
( less_equal(A,B)
| ~ quotient(idQb,idQb,B)
| ~ quotient(idQ_idQb,divide(b,idQb),A) ),
inference(resolve,[status(thm)],[c_2948,c_12]) ).
cnf(c_2950,plain,
( less_equal(divide(idQ_idQb,divide(b,idQb)),A)
| ~ quotient(idQb,idQb,A) ),
inference(resolve,[status(thm)],[c_2949,c_8]) ).
cnf(c_38,plain,
less_equal(divide(idQ_idQb,divide(b,idQb)),divide(idQb,idQb)),
inference(resolve,[status(thm)],[c_2950,c_8]) ).
cnf(c_2951,plain,
( divide(A,B) = C
| ~ quotient(A,B,C) ),
inference(resolve,[status(thm)],[c_9,c_8]) ).
cnf(c_46,plain,
divide(idQa,idQ_idQb) = idQa_Q__idQ_idQb,
inference(resolve,[status(thm)],[c_2951,c_13]) ).
cnf(c_2952,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_2953,plain,
( less_equal(C,D)
| ~ quotient(idQa,A,D)
| ~ quotient(B,divide(a,A),C)
| ~ quotient(identity,A,B) ),
inference(resolve,[status(thm)],[c_2952,c_8]) ).
cnf(c_2954,plain,
( less_equal(A,B)
| ~ quotient(idQa,idQa,B)
| ~ quotient(idQ_idQa,divide(a,idQa),A) ),
inference(resolve,[status(thm)],[c_2953,c_14]) ).
cnf(c_2955,plain,
( less_equal(divide(idQ_idQa,divide(a,idQa)),A)
| ~ quotient(idQa,idQa,A) ),
inference(resolve,[status(thm)],[c_2954,c_8]) ).
cnf(c_58,plain,
less_equal(divide(idQ_idQa,divide(a,idQa)),divide(idQa,idQa)),
inference(resolve,[status(thm)],[c_2955,c_8]) ).
cnf(c_2956,plain,
( less_equal(D,E)
| ~ quotient(idQ_idQa,A,E)
| ~ quotient(C,B,D)
| ~ quotient(identity,A,C)
| ~ quotient(idQa,A,B) ),
inference(resolve,[status(thm)],[c_4,c_14]) ).
cnf(c_2957,plain,
( less_equal(B,C)
| ~ quotient(idQ_idQa,idQ_idQb,C)
| ~ quotient(A,idQa_Q__idQ_idQb,B)
| ~ quotient(identity,idQ_idQb,A) ),
inference(resolve,[status(thm)],[c_2956,c_13]) ).
cnf(c_2958,plain,
( less_equal(A,B)
| ~ quotient(idQ_idQa,idQ_idQb,B)
| ~ quotient(divide(identity,idQ_idQb),idQa_Q__idQ_idQb,A) ),
inference(resolve,[status(thm)],[c_2957,c_8]) ).
cnf(c_2959,plain,
( less_equal(divide(divide(identity,idQ_idQb),idQa_Q__idQ_idQb),A)
| ~ quotient(idQ_idQa,idQ_idQb,A) ),
inference(resolve,[status(thm)],[c_2958,c_8]) ).
cnf(c_62,plain,
less_equal(divide(divide(identity,idQ_idQb),idQa_Q__idQ_idQb),divide(idQ_idQa,idQ_idQb)),
inference(resolve,[status(thm)],[c_2959,c_8]) ).
cnf(c_2960,plain,
( divide(A,B) = C
| ~ quotient(A,B,C) ),
inference(resolve,[status(thm)],[c_9,c_8]) ).
cnf(c_67,plain,
divide(idQb,idQ_idQa) = idQb_Q__idQ_idQa,
inference(resolve,[status(thm)],[c_2960,c_15]) ).
cnf(c_2961,plain,
( less_equal(D,E)
| ~ quotient(idQ_idQb,A,E)
| ~ quotient(C,B,D)
| ~ quotient(identity,A,C)
| ~ quotient(idQb,A,B) ),
inference(resolve,[status(thm)],[c_4,c_12]) ).
cnf(c_2962,plain,
( less_equal(B,C)
| ~ quotient(idQ_idQb,idQ_idQa,C)
| ~ quotient(A,idQb_Q__idQ_idQa,B)
| ~ quotient(identity,idQ_idQa,A) ),
inference(resolve,[status(thm)],[c_2961,c_15]) ).
cnf(c_2963,plain,
( less_equal(A,B)
| ~ quotient(idQ_idQb,idQ_idQa,B)
| ~ quotient(divide(identity,idQ_idQa),idQb_Q__idQ_idQa,A) ),
inference(resolve,[status(thm)],[c_2962,c_8]) ).
cnf(c_2964,plain,
( less_equal(divide(divide(identity,idQ_idQa),idQb_Q__idQ_idQa),A)
| ~ quotient(idQ_idQb,idQ_idQa,A) ),
inference(resolve,[status(thm)],[c_2963,c_8]) ).
cnf(c_72,plain,
less_equal(divide(divide(identity,idQ_idQa),idQb_Q__idQ_idQa),divide(idQ_idQb,idQ_idQa)),
inference(resolve,[status(thm)],[c_2964,c_8]) ).
cnf(c_2965,plain,
( divide(A,B) = C
| ~ quotient(A,B,C) ),
inference(resolve,[status(thm)],[c_9,c_8]) ).
cnf(c_78,plain,
divide(zero,A) = zero,
inference(resolve,[status(thm)],[c_2965,c_18]) ).
cnf(c_2966,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_19]) ).
cnf(c_2967,plain,
( less_equal(C,D)
| ~ quotient(zero,idQa,D)
| ~ quotient(B,idQ_idQa,C)
| ~ quotient(A,idQa,B) ),
inference(resolve,[status(thm)],[c_2966,c_14]) ).
cnf(c_2968,plain,
( less_equal(B,C)
| ~ quotient(zero,idQa,C)
| ~ quotient(divide(A,idQa),idQ_idQa,B) ),
inference(resolve,[status(thm)],[c_2967,c_8]) ).
cnf(c_2969,plain,
( less_equal(divide(divide(B,idQa),idQ_idQa),A)
| ~ quotient(zero,idQa,A) ),
inference(resolve,[status(thm)],[c_2968,c_8]) ).
cnf(c_90,plain,
less_equal(divide(divide(A,idQa),idQ_idQa),zero),
inference(resolve,[status(thm)],[c_2969,c_18]) ).
cnf(c_2970,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_19]) ).
cnf(c_2971,plain,
( less_equal(C,D)
| ~ quotient(zero,idQb,D)
| ~ quotient(B,idQ_idQb,C)
| ~ quotient(A,idQb,B) ),
inference(resolve,[status(thm)],[c_2970,c_12]) ).
cnf(c_2972,plain,
( less_equal(B,C)
| ~ quotient(zero,idQb,C)
| ~ quotient(divide(A,idQb),idQ_idQb,B) ),
inference(resolve,[status(thm)],[c_2971,c_8]) ).
cnf(c_2973,plain,
( less_equal(divide(divide(B,idQb),idQ_idQb),A)
| ~ quotient(zero,idQb,A) ),
inference(resolve,[status(thm)],[c_2972,c_8]) ).
cnf(c_92,plain,
less_equal(divide(divide(A,idQb),idQ_idQb),zero),
inference(resolve,[status(thm)],[c_2973,c_18]) ).
cnf(c_2974,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_19]) ).
cnf(c_2975,plain,
( less_equal(C,D)
| ~ quotient(zero,b,D)
| ~ quotient(B,idQb,C)
| ~ quotient(A,b,B) ),
inference(resolve,[status(thm)],[c_2974,c_11]) ).
cnf(c_2976,plain,
( less_equal(A,B)
| ~ quotient(zero,b,B)
| ~ quotient(idQb,idQb,A) ),
inference(resolve,[status(thm)],[c_2975,c_11]) ).
cnf(c_2977,plain,
( less_equal(divide(idQb,idQb),A)
| ~ quotient(zero,b,A) ),
inference(resolve,[status(thm)],[c_2976,c_8]) ).
cnf(c_93,plain,
less_equal(divide(idQb,idQb),zero),
inference(resolve,[status(thm)],[c_2977,c_18]) ).
cnf(c_2978,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_19]) ).
cnf(c_2979,plain,
( less_equal(C,D)
| ~ quotient(zero,b,D)
| ~ quotient(B,idQb,C)
| ~ quotient(A,b,B) ),
inference(resolve,[status(thm)],[c_2978,c_11]) ).
cnf(c_2980,plain,
( less_equal(B,C)
| ~ quotient(zero,b,C)
| ~ quotient(divide(A,b),idQb,B) ),
inference(resolve,[status(thm)],[c_2979,c_8]) ).
cnf(c_2981,plain,
( less_equal(divide(divide(B,b),idQb),A)
| ~ quotient(zero,b,A) ),
inference(resolve,[status(thm)],[c_2980,c_8]) ).
cnf(c_94,plain,
less_equal(divide(divide(A,b),idQb),zero),
inference(resolve,[status(thm)],[c_2981,c_18]) ).
cnf(c_2982,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_19]) ).
cnf(c_2983,plain,
( less_equal(C,D)
| ~ quotient(zero,a,D)
| ~ quotient(B,idQa,C)
| ~ quotient(A,a,B) ),
inference(resolve,[status(thm)],[c_2982,c_10]) ).
cnf(c_2984,plain,
( less_equal(A,B)
| ~ quotient(zero,a,B)
| ~ quotient(idQa,idQa,A) ),
inference(resolve,[status(thm)],[c_2983,c_10]) ).
cnf(c_2985,plain,
( less_equal(divide(idQa,idQa),A)
| ~ quotient(zero,a,A) ),
inference(resolve,[status(thm)],[c_2984,c_8]) ).
cnf(c_95,plain,
less_equal(divide(idQa,idQa),zero),
inference(resolve,[status(thm)],[c_2985,c_18]) ).
cnf(c_2986,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_19]) ).
cnf(c_2987,plain,
( less_equal(C,D)
| ~ quotient(zero,a,D)
| ~ quotient(B,idQa,C)
| ~ quotient(A,a,B) ),
inference(resolve,[status(thm)],[c_2986,c_10]) ).
cnf(c_2988,plain,
( less_equal(B,C)
| ~ quotient(zero,a,C)
| ~ quotient(divide(A,a),idQa,B) ),
inference(resolve,[status(thm)],[c_2987,c_8]) ).
cnf(c_2989,plain,
( less_equal(divide(divide(B,a),idQa),A)
| ~ quotient(zero,a,A) ),
inference(resolve,[status(thm)],[c_2988,c_8]) ).
cnf(c_96,plain,
less_equal(divide(divide(A,a),idQa),zero),
inference(resolve,[status(thm)],[c_2989,c_18]) ).
cnf(c_106,plain,
quotient(divide(divide(A,B),divide(C,B)),divide(divide(A,C),B),zero),
inference(resolve,[status(thm)],[c_1,c_20]) ).
cnf(c_113,plain,
quotient(divide(A,B),A,zero),
inference(resolve,[status(thm)],[c_1,c_21]) ).
cnf(c_2990,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2991,plain,
zero = divide(idQb,idQb),
inference(resolve,[status(thm)],[c_2990,c_93]) ).
cnf(c_121,plain,
divide(idQb,idQb) = zero,
inference(copy,[status(thm)],[c_2991]) ).
cnf(c_123,plain,
less_equal(divide(idQ_idQb,divide(b,idQb)),zero),
inference(paramod,[status(thm)],[c_121,c_38]) ).
cnf(c_2992,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2993,plain,
zero = divide(idQa,idQa),
inference(resolve,[status(thm)],[c_2992,c_95]) ).
cnf(c_125,plain,
divide(idQa,idQa) = zero,
inference(copy,[status(thm)],[c_2993]) ).
cnf(c_126,plain,
less_equal(divide(idQ_idQa,divide(a,idQa)),zero),
inference(paramod,[status(thm)],[c_125,c_58]) ).
cnf(c_2994,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_2995,plain,
( less_equal(D,F)
| ~ quotient(divide(A,divide(B,E)),B,F)
| ~ quotient(C,zero,D)
| ~ quotient(A,B,C) ),
inference(resolve,[status(thm)],[c_2994,c_113]) ).
cnf(c_2996,plain,
( less_equal(C,E)
| ~ quotient(divide(A,divide(B,D)),B,E)
| ~ quotient(divide(A,B),zero,C) ),
inference(resolve,[status(thm)],[c_2995,c_8]) ).
cnf(c_2997,plain,
( less_equal(divide(divide(A,B),zero),D)
| ~ quotient(divide(A,divide(B,C)),B,D) ),
inference(resolve,[status(thm)],[c_2996,c_8]) ).
cnf(c_166,plain,
less_equal(divide(divide(A,A),zero),zero),
inference(resolve,[status(thm)],[c_2997,c_113]) ).
cnf(c_2998,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_2999,plain,
( less_equal(D,F)
| ~ quotient(divide(A,divide(B,E)),B,F)
| ~ quotient(C,zero,D)
| ~ quotient(A,B,C) ),
inference(resolve,[status(thm)],[c_2998,c_113]) ).
cnf(c_3000,plain,
( less_equal(C,E)
| ~ quotient(divide(A,divide(B,D)),B,E)
| ~ quotient(divide(A,B),zero,C) ),
inference(resolve,[status(thm)],[c_2999,c_8]) ).
cnf(c_3001,plain,
( less_equal(divide(divide(A,B),zero),D)
| ~ quotient(divide(A,divide(B,C)),B,D) ),
inference(resolve,[status(thm)],[c_3000,c_8]) ).
cnf(c_175,plain,
less_equal(divide(divide(A,B),zero),divide(divide(A,divide(B,C)),B)),
inference(resolve,[status(thm)],[c_3001,c_8]) ).
cnf(c_3002,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_3003,plain,
zero = divide(divide(A,idQa),idQ_idQa),
inference(resolve,[status(thm)],[c_3002,c_90]) ).
cnf(c_181,plain,
divide(divide(A,idQa),idQ_idQa) = zero,
inference(copy,[status(thm)],[c_3003]) ).
cnf(c_3004,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_3005,plain,
zero = divide(divide(A,idQb),idQ_idQb),
inference(resolve,[status(thm)],[c_3004,c_92]) ).
cnf(c_182,plain,
divide(divide(A,idQb),idQ_idQb) = zero,
inference(copy,[status(thm)],[c_3005]) ).
cnf(c_3006,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_3007,plain,
zero = divide(divide(A,b),idQb),
inference(resolve,[status(thm)],[c_3006,c_94]) ).
cnf(c_183,plain,
divide(divide(A,b),idQb) = zero,
inference(copy,[status(thm)],[c_3007]) ).
cnf(c_3008,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_3009,plain,
zero = divide(divide(A,a),idQa),
inference(resolve,[status(thm)],[c_3008,c_96]) ).
cnf(c_185,plain,
divide(divide(A,a),idQa) = zero,
inference(copy,[status(thm)],[c_3009]) ).
cnf(c_3010,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_3011,plain,
zero = divide(idQ_idQb,divide(b,idQb)),
inference(resolve,[status(thm)],[c_3010,c_123]) ).
cnf(c_191,plain,
divide(idQ_idQb,divide(b,idQb)) = zero,
inference(copy,[status(thm)],[c_3011]) ).
cnf(c_3012,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_3013,plain,
zero = divide(idQ_idQa,divide(a,idQa)),
inference(resolve,[status(thm)],[c_3012,c_126]) ).
cnf(c_193,plain,
divide(idQ_idQa,divide(a,idQa)) = zero,
inference(copy,[status(thm)],[c_3013]) ).
cnf(c_3014,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_3015,plain,
zero = divide(divide(A,A),zero),
inference(resolve,[status(thm)],[c_3014,c_166]) ).
cnf(c_196,plain,
divide(divide(A,A),zero) = zero,
inference(copy,[status(thm)],[c_3015]) ).
cnf(c_197,plain,
quotient(divide(A,idQa),idQ_idQa,zero),
inference(paramod,[status(thm)],[c_181,c_8]) ).
cnf(c_200,plain,
less_equal(divide(divide(A,idQ_idQa),divide(idQa,idQ_idQa)),zero),
inference(paramod,[status(thm)],[c_181,c_20]) ).
cnf(c_205,plain,
less_equal(divide(A,idQa),idQ_idQa),
inference(resolve,[status(thm)],[c_2,c_197]) ).
cnf(c_206,plain,
quotient(divide(A,idQb),idQ_idQb,zero),
inference(paramod,[status(thm)],[c_182,c_8]) ).
cnf(c_209,plain,
less_equal(divide(divide(A,idQ_idQb),divide(idQb,idQ_idQb)),zero),
inference(paramod,[status(thm)],[c_182,c_20]) ).
cnf(c_213,plain,
less_equal(divide(A,idQb),idQ_idQb),
inference(resolve,[status(thm)],[c_2,c_206]) ).
cnf(c_215,plain,
quotient(divide(A,b),idQb,zero),
inference(paramod,[status(thm)],[c_183,c_8]) ).
cnf(c_222,plain,
less_equal(divide(A,b),idQb),
inference(resolve,[status(thm)],[c_2,c_215]) ).
cnf(c_224,plain,
quotient(divide(A,a),idQa,zero),
inference(paramod,[status(thm)],[c_185,c_8]) ).
cnf(c_231,plain,
less_equal(divide(A,a),idQa),
inference(resolve,[status(thm)],[c_2,c_224]) ).
cnf(c_246,plain,
quotient(idQ_idQb,divide(b,idQb),zero),
inference(paramod,[status(thm)],[c_191,c_8]) ).
cnf(c_254,plain,
less_equal(idQ_idQb,divide(b,idQb)),
inference(resolve,[status(thm)],[c_2,c_246]) ).
cnf(c_3016,plain,
( divide(A,idQb) = idQ_idQb
| ~ less_equal(idQ_idQb,divide(A,idQb)) ),
inference(resolve,[status(thm)],[c_6,c_213]) ).
cnf(c_255,plain,
divide(b,idQb) = idQ_idQb,
inference(resolve,[status(thm)],[c_3016,c_254]) ).
cnf(c_261,plain,
quotient(idQ_idQb,b,zero),
inference(paramod,[status(thm)],[c_255,c_113]) ).
cnf(c_3017,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_3018,plain,
( less_equal(C,D)
| ~ quotient(divide(A,idQ_idQb),b,D)
| ~ quotient(B,zero,C)
| ~ quotient(A,b,B) ),
inference(resolve,[status(thm)],[c_3017,c_261]) ).
cnf(c_3019,plain,
( less_equal(A,B)
| ~ quotient(divide(identity,idQ_idQb),b,B)
| ~ quotient(idQb,zero,A) ),
inference(resolve,[status(thm)],[c_3018,c_11]) ).
cnf(c_3020,plain,
( less_equal(divide(idQb,zero),A)
| ~ quotient(divide(identity,idQ_idQb),b,A) ),
inference(resolve,[status(thm)],[c_3019,c_8]) ).
cnf(c_273,plain,
less_equal(divide(idQb,zero),divide(divide(identity,idQ_idQb),b)),
inference(resolve,[status(thm)],[c_3020,c_8]) ).
cnf(c_277,plain,
quotient(idQ_idQa,divide(a,idQa),zero),
inference(paramod,[status(thm)],[c_193,c_8]) ).
cnf(c_285,plain,
less_equal(idQ_idQa,divide(a,idQa)),
inference(resolve,[status(thm)],[c_2,c_277]) ).
cnf(c_3021,plain,
( divide(A,idQa) = idQ_idQa
| ~ less_equal(idQ_idQa,divide(A,idQa)) ),
inference(resolve,[status(thm)],[c_6,c_205]) ).
cnf(c_286,plain,
divide(a,idQa) = idQ_idQa,
inference(resolve,[status(thm)],[c_3021,c_285]) ).
cnf(c_292,plain,
quotient(idQ_idQa,a,zero),
inference(paramod,[status(thm)],[c_286,c_113]) ).
cnf(c_3022,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_3023,plain,
( less_equal(C,D)
| ~ quotient(divide(A,idQ_idQa),a,D)
| ~ quotient(B,zero,C)
| ~ quotient(A,a,B) ),
inference(resolve,[status(thm)],[c_3022,c_292]) ).
cnf(c_3024,plain,
( less_equal(A,B)
| ~ quotient(divide(identity,idQ_idQa),a,B)
| ~ quotient(idQa,zero,A) ),
inference(resolve,[status(thm)],[c_3023,c_10]) ).
cnf(c_3025,plain,
( less_equal(divide(idQa,zero),A)
| ~ quotient(divide(identity,idQ_idQa),a,A) ),
inference(resolve,[status(thm)],[c_3024,c_8]) ).
cnf(c_303,plain,
less_equal(divide(idQa,zero),divide(divide(identity,idQ_idQa),a)),
inference(resolve,[status(thm)],[c_3025,c_8]) ).
cnf(c_306,plain,
quotient(divide(divide(identity,idQ_idQb),idQa_Q__idQ_idQb),divide(idQ_idQa,idQ_idQb),zero),
inference(resolve,[status(thm)],[c_1,c_62]) ).
cnf(c_307,plain,
quotient(divide(A,A),zero,zero),
inference(paramod,[status(thm)],[c_196,c_8]) ).
cnf(c_312,plain,
less_equal(divide(A,A),zero),
inference(resolve,[status(thm)],[c_2,c_307]) ).
cnf(c_3026,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_3027,plain,
zero = divide(A,A),
inference(resolve,[status(thm)],[c_3026,c_312]) ).
cnf(c_313,plain,
divide(A,A) = zero,
inference(copy,[status(thm)],[c_3027]) ).
cnf(c_319,plain,
quotient(A,A,zero),
inference(paramod,[status(thm)],[c_313,c_8]) ).
cnf(c_3028,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_3029,plain,
( less_equal(D,E)
| ~ quotient(divide(A,zero),B,E)
| ~ quotient(C,zero,D)
| ~ quotient(A,B,C) ),
inference(resolve,[status(thm)],[c_3028,c_18]) ).
cnf(c_3030,plain,
( less_equal(C,D)
| ~ quotient(divide(A,zero),B,D)
| ~ quotient(divide(A,B),zero,C) ),
inference(resolve,[status(thm)],[c_3029,c_8]) ).
cnf(c_3031,plain,
( less_equal(divide(divide(A,B),zero),C)
| ~ quotient(divide(A,zero),B,C) ),
inference(resolve,[status(thm)],[c_3030,c_8]) ).
cnf(c_322,plain,
less_equal(divide(divide(A,divide(A,zero)),zero),zero),
inference(resolve,[status(thm)],[c_3031,c_319]) ).
cnf(c_364,plain,
quotient(divide(divide(identity,idQ_idQa),idQb_Q__idQ_idQa),divide(idQ_idQb,idQ_idQa),zero),
inference(resolve,[status(thm)],[c_1,c_72]) ).
cnf(c_3032,plain,
( divide(A,B) = C
| ~ quotient(A,B,C) ),
inference(resolve,[status(thm)],[c_9,c_8]) ).
cnf(c_477,plain,
divide(divide(divide(A,B),divide(C,B)),divide(divide(A,C),B)) = zero,
inference(resolve,[status(thm)],[c_3032,c_106]) ).
cnf(c_3033,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_3034,plain,
zero = divide(divide(A,idQ_idQa),divide(idQa,idQ_idQa)),
inference(resolve,[status(thm)],[c_3033,c_200]) ).
cnf(c_531,plain,
divide(divide(A,idQ_idQa),divide(idQa,idQ_idQa)) = zero,
inference(copy,[status(thm)],[c_3034]) ).
cnf(c_3035,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_3036,plain,
zero = divide(divide(A,idQ_idQb),divide(idQb,idQ_idQb)),
inference(resolve,[status(thm)],[c_3035,c_209]) ).
cnf(c_532,plain,
divide(divide(A,idQ_idQb),divide(idQb,idQ_idQb)) = zero,
inference(copy,[status(thm)],[c_3036]) ).
cnf(c_3037,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_3038,plain,
zero = divide(divide(A,divide(A,zero)),zero),
inference(resolve,[status(thm)],[c_3037,c_322]) ).
cnf(c_582,plain,
divide(divide(A,divide(A,zero)),zero) = zero,
inference(copy,[status(thm)],[c_3038]) ).
cnf(c_3039,plain,
less_equal(divide(divide(divide(A,idQ_idQa),idQa),zero),divide(zero,idQa)),
inference(paramod,[status(thm)],[c_531,c_175]) ).
cnf(c_787,plain,
less_equal(divide(divide(divide(A,idQ_idQa),idQa),zero),zero),
inference(paramod,[status(thm)],[c_78,c_3039]) ).
cnf(c_3040,plain,
less_equal(divide(divide(divide(A,idQ_idQb),idQb),zero),divide(zero,idQb)),
inference(paramod,[status(thm)],[c_532,c_175]) ).
cnf(c_869,plain,
less_equal(divide(divide(divide(A,idQ_idQb),idQb),zero),zero),
inference(paramod,[status(thm)],[c_78,c_3040]) ).
cnf(c_1083,plain,
quotient(divide(A,divide(A,zero)),zero,zero),
inference(paramod,[status(thm)],[c_582,c_8]) ).
cnf(c_1100,plain,
less_equal(divide(A,divide(A,zero)),zero),
inference(resolve,[status(thm)],[c_2,c_1083]) ).
cnf(c_3041,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_3042,plain,
zero = divide(A,divide(A,zero)),
inference(resolve,[status(thm)],[c_3041,c_1100]) ).
cnf(c_1101,plain,
divide(A,divide(A,zero)) = zero,
inference(copy,[status(thm)],[c_3042]) ).
cnf(c_1102,plain,
quotient(A,divide(A,zero),zero),
inference(paramod,[status(thm)],[c_1101,c_8]) ).
cnf(c_1214,plain,
less_equal(A,divide(A,zero)),
inference(resolve,[status(thm)],[c_2,c_1102]) ).
cnf(c_3043,plain,
( divide(A,B) = A
| ~ less_equal(A,divide(A,B)) ),
inference(resolve,[status(thm)],[c_6,c_21]) ).
cnf(c_1216,plain,
divide(A,zero) = A,
inference(resolve,[status(thm)],[c_3043,c_1214]) ).
cnf(c_1299,plain,
less_equal(divide(divide(A,idQ_idQb),idQb),zero),
inference(paramod,[status(thm)],[c_1216,c_869]) ).
cnf(c_1322,plain,
less_equal(divide(divide(A,idQ_idQa),idQa),zero),
inference(paramod,[status(thm)],[c_1216,c_787]) ).
cnf(c_1459,plain,
less_equal(idQa,divide(divide(identity,idQ_idQa),a)),
inference(paramod,[status(thm)],[c_1216,c_303]) ).
cnf(c_1465,plain,
less_equal(idQb,divide(divide(identity,idQ_idQb),b)),
inference(paramod,[status(thm)],[c_1216,c_273]) ).
cnf(c_1495,plain,
quotient(A,zero,A),
inference(paramod,[status(thm)],[c_1216,c_8]) ).
cnf(c_3044,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_3045,plain,
zero = divide(divide(A,idQ_idQb),idQb),
inference(resolve,[status(thm)],[c_3044,c_1299]) ).
cnf(c_1534,plain,
divide(divide(A,idQ_idQb),idQb) = zero,
inference(copy,[status(thm)],[c_3045]) ).
cnf(c_3046,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_3047,plain,
zero = divide(divide(A,idQ_idQa),idQa),
inference(resolve,[status(thm)],[c_3046,c_1322]) ).
cnf(c_1545,plain,
divide(divide(A,idQ_idQa),idQa) = zero,
inference(copy,[status(thm)],[c_3047]) ).
cnf(c_3048,plain,
( divide(A,a) = idQa
| ~ less_equal(idQa,divide(A,a)) ),
inference(resolve,[status(thm)],[c_6,c_231]) ).
cnf(c_1585,plain,
divide(divide(identity,idQ_idQa),a) = idQa,
inference(resolve,[status(thm)],[c_3048,c_1459]) ).
cnf(c_3049,plain,
( divide(A,b) = idQb
| ~ less_equal(idQb,divide(A,b)) ),
inference(resolve,[status(thm)],[c_6,c_222]) ).
cnf(c_1594,plain,
divide(divide(identity,idQ_idQb),b) = idQb,
inference(resolve,[status(thm)],[c_3049,c_1465]) ).
cnf(c_3050,plain,
( less_equal(D,E)
| ~ quotient(zero,A,E)
| ~ quotient(C,B,D)
| ~ quotient(divide(divide(identity,idQ_idQb),idQa_Q__idQ_idQb),A,C)
| ~ quotient(divide(idQ_idQa,idQ_idQb),A,B) ),
inference(resolve,[status(thm)],[c_4,c_306]) ).
cnf(c_3051,plain,
( less_equal(B,C)
| ~ quotient(zero,idQ_idQa,C)
| ~ quotient(A,zero,B)
| ~ quotient(divide(divide(identity,idQ_idQb),idQa_Q__idQ_idQb),idQ_idQa,A) ),
inference(resolve,[status(thm)],[c_3050,c_113]) ).
cnf(c_3052,plain,
( less_equal(A,B)
| ~ quotient(zero,idQ_idQa,B)
| ~ quotient(divide(divide(divide(identity,idQ_idQb),idQa_Q__idQ_idQb),idQ_idQa),zero,A) ),
inference(resolve,[status(thm)],[c_3051,c_8]) ).
cnf(c_3053,plain,
( less_equal(divide(divide(divide(identity,idQ_idQb),idQa_Q__idQ_idQb),idQ_idQa),A)
| ~ quotient(zero,idQ_idQa,A) ),
inference(resolve,[status(thm)],[c_3052,c_1495]) ).
cnf(c_1682,plain,
less_equal(divide(divide(divide(identity,idQ_idQb),idQa_Q__idQ_idQb),idQ_idQa),zero),
inference(resolve,[status(thm)],[c_3053,c_18]) ).
cnf(c_1781,plain,
quotient(divide(A,idQ_idQb),idQb,zero),
inference(paramod,[status(thm)],[c_1534,c_8]) ).
cnf(c_1793,plain,
less_equal(divide(A,idQ_idQb),idQb),
inference(resolve,[status(thm)],[c_2,c_1781]) ).
cnf(c_3054,plain,
( less_equal(D,E)
| ~ quotient(zero,A,E)
| ~ quotient(C,B,D)
| ~ quotient(divide(divide(identity,idQ_idQa),idQb_Q__idQ_idQa),A,C)
| ~ quotient(divide(idQ_idQb,idQ_idQa),A,B) ),
inference(resolve,[status(thm)],[c_4,c_364]) ).
cnf(c_3055,plain,
( less_equal(B,C)
| ~ quotient(zero,idQ_idQb,C)
| ~ quotient(A,zero,B)
| ~ quotient(divide(divide(identity,idQ_idQa),idQb_Q__idQ_idQa),idQ_idQb,A) ),
inference(resolve,[status(thm)],[c_3054,c_113]) ).
cnf(c_3056,plain,
( less_equal(A,B)
| ~ quotient(zero,idQ_idQb,B)
| ~ quotient(divide(divide(divide(identity,idQ_idQa),idQb_Q__idQ_idQa),idQ_idQb),zero,A) ),
inference(resolve,[status(thm)],[c_3055,c_8]) ).
cnf(c_3057,plain,
( less_equal(divide(divide(divide(identity,idQ_idQa),idQb_Q__idQ_idQa),idQ_idQb),A)
| ~ quotient(zero,idQ_idQb,A) ),
inference(resolve,[status(thm)],[c_3056,c_1495]) ).
cnf(c_1930,plain,
less_equal(divide(divide(divide(identity,idQ_idQa),idQb_Q__idQ_idQa),idQ_idQb),zero),
inference(resolve,[status(thm)],[c_3057,c_18]) ).
cnf(c_1954,plain,
quotient(divide(A,idQ_idQa),idQa,zero),
inference(paramod,[status(thm)],[c_1545,c_8]) ).
cnf(c_1966,plain,
less_equal(divide(A,idQ_idQa),idQa),
inference(resolve,[status(thm)],[c_2,c_1954]) ).
cnf(c_2066,plain,
less_equal(idQa,divide(identity,idQ_idQa)),
inference(paramod,[status(thm)],[c_1585,c_21]) ).
cnf(c_3058,plain,
( divide(A,idQ_idQa) = idQa
| ~ less_equal(idQa,divide(A,idQ_idQa)) ),
inference(resolve,[status(thm)],[c_6,c_1966]) ).
cnf(c_2072,plain,
divide(identity,idQ_idQa) = idQa,
inference(resolve,[status(thm)],[c_3058,c_2066]) ).
cnf(c_2075,plain,
less_equal(divide(divide(idQa,idQb_Q__idQ_idQa),idQ_idQb),zero),
inference(paramod,[status(thm)],[c_2072,c_1930]) ).
cnf(c_2287,plain,
less_equal(idQb,divide(identity,idQ_idQb)),
inference(paramod,[status(thm)],[c_1594,c_21]) ).
cnf(c_3059,plain,
( divide(A,idQ_idQb) = idQb
| ~ less_equal(idQb,divide(A,idQ_idQb)) ),
inference(resolve,[status(thm)],[c_6,c_1793]) ).
cnf(c_2305,plain,
divide(identity,idQ_idQb) = idQb,
inference(resolve,[status(thm)],[c_3059,c_2287]) ).
cnf(c_2312,plain,
less_equal(divide(divide(idQb,idQa_Q__idQ_idQb),idQ_idQa),zero),
inference(paramod,[status(thm)],[c_2305,c_1682]) ).
cnf(c_3060,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_3061,plain,
zero = divide(divide(idQa,idQb_Q__idQ_idQa),idQ_idQb),
inference(resolve,[status(thm)],[c_3060,c_2075]) ).
cnf(c_2622,plain,
divide(divide(idQa,idQb_Q__idQ_idQa),idQ_idQb) = zero,
inference(copy,[status(thm)],[c_3061]) ).
cnf(c_3062,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_3063,plain,
zero = divide(divide(idQb,idQa_Q__idQ_idQb),idQ_idQa),
inference(resolve,[status(thm)],[c_3062,c_2312]) ).
cnf(c_2637,plain,
divide(divide(idQb,idQa_Q__idQ_idQb),idQ_idQa) = zero,
inference(copy,[status(thm)],[c_3063]) ).
cnf(c_3064,plain,
divide(divide(divide(idQa,idQ_idQb),divide(idQb_Q__idQ_idQa,idQ_idQb)),zero) = zero,
inference(paramod,[status(thm)],[c_2622,c_477]) ).
cnf(c_3065,plain,
divide(divide(idQa_Q__idQ_idQb,divide(idQb_Q__idQ_idQa,idQ_idQb)),zero) = zero,
inference(paramod,[status(thm)],[c_46,c_3064]) ).
cnf(c_2672,plain,
divide(idQa_Q__idQ_idQb,divide(idQb_Q__idQ_idQa,idQ_idQb)) = zero,
inference(paramod,[status(thm)],[c_1216,c_3065]) ).
cnf(c_3066,plain,
divide(divide(divide(idQb,idQ_idQa),divide(idQa_Q__idQ_idQb,idQ_idQa)),zero) = zero,
inference(paramod,[status(thm)],[c_2637,c_477]) ).
cnf(c_3067,plain,
divide(divide(idQb_Q__idQ_idQa,divide(idQa_Q__idQ_idQb,idQ_idQa)),zero) = zero,
inference(paramod,[status(thm)],[c_67,c_3066]) ).
cnf(c_2732,plain,
divide(idQb_Q__idQ_idQa,divide(idQa_Q__idQ_idQb,idQ_idQa)) = zero,
inference(paramod,[status(thm)],[c_1216,c_3067]) ).
cnf(c_2817,plain,
quotient(idQa_Q__idQ_idQb,divide(idQb_Q__idQ_idQa,idQ_idQb),zero),
inference(paramod,[status(thm)],[c_2672,c_8]) ).
cnf(c_3068,plain,
( less_equal(D,E)
| ~ quotient(zero,A,E)
| ~ quotient(C,B,D)
| ~ quotient(idQa_Q__idQ_idQb,A,C)
| ~ quotient(divide(idQb_Q__idQ_idQa,idQ_idQb),A,B) ),
inference(resolve,[status(thm)],[c_4,c_2817]) ).
cnf(c_3069,plain,
( less_equal(B,C)
| ~ quotient(zero,idQb_Q__idQ_idQa,C)
| ~ quotient(A,zero,B)
| ~ quotient(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa,A) ),
inference(resolve,[status(thm)],[c_3068,c_113]) ).
cnf(c_3070,plain,
( less_equal(A,B)
| ~ quotient(zero,idQb_Q__idQ_idQa,B)
| ~ quotient(divide(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa),zero,A) ),
inference(resolve,[status(thm)],[c_3069,c_8]) ).
cnf(c_3071,plain,
( less_equal(divide(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa),A)
| ~ quotient(zero,idQb_Q__idQ_idQa,A) ),
inference(resolve,[status(thm)],[c_3070,c_1495]) ).
cnf(c_2830,plain,
less_equal(divide(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa),zero),
inference(resolve,[status(thm)],[c_3071,c_18]) ).
cnf(c_3072,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_3073,plain,
zero = divide(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa),
inference(resolve,[status(thm)],[c_3072,c_2830]) ).
cnf(c_2834,plain,
divide(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa) = zero,
inference(copy,[status(thm)],[c_3073]) ).
cnf(c_2846,plain,
quotient(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa,zero),
inference(paramod,[status(thm)],[c_2834,c_8]) ).
cnf(c_2857,plain,
less_equal(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa),
inference(resolve,[status(thm)],[c_2,c_2846]) ).
cnf(c_3074,plain,
( idQb_Q__idQ_idQa = idQa_Q__idQ_idQb
| ~ less_equal(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb) ),
inference(resolve,[status(thm)],[c_6,c_2857]) ).
cnf(c_2858,plain,
~ less_equal(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb),
inference(resolve,[status(thm)],[c_3074,c_17]) ).
cnf(c_2880,plain,
~ quotient(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb,zero),
inference(resolve,[status(thm)],[c_2,c_2858]) ).
cnf(c_2909,plain,
quotient(idQb_Q__idQ_idQa,divide(idQa_Q__idQ_idQb,idQ_idQa),zero),
inference(paramod,[status(thm)],[c_2732,c_8]) ).
cnf(c_3075,plain,
( less_equal(D,E)
| ~ quotient(zero,A,E)
| ~ quotient(C,B,D)
| ~ quotient(idQb_Q__idQ_idQa,A,C)
| ~ quotient(divide(idQa_Q__idQ_idQb,idQ_idQa),A,B) ),
inference(resolve,[status(thm)],[c_4,c_2909]) ).
cnf(c_3076,plain,
( less_equal(B,C)
| ~ quotient(zero,idQa_Q__idQ_idQb,C)
| ~ quotient(A,zero,B)
| ~ quotient(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb,A) ),
inference(resolve,[status(thm)],[c_3075,c_113]) ).
cnf(c_3077,plain,
( less_equal(A,B)
| ~ quotient(zero,idQa_Q__idQ_idQb,B)
| ~ quotient(divide(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb),zero,A) ),
inference(resolve,[status(thm)],[c_3076,c_8]) ).
cnf(c_3078,plain,
( less_equal(divide(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb),A)
| ~ quotient(zero,idQa_Q__idQ_idQb,A) ),
inference(resolve,[status(thm)],[c_3077,c_1495]) ).
cnf(c_2923,plain,
less_equal(divide(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb),zero),
inference(resolve,[status(thm)],[c_3078,c_18]) ).
cnf(c_3079,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_3080,plain,
zero = divide(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb),
inference(resolve,[status(thm)],[c_3079,c_2923]) ).
cnf(c_2939,plain,
divide(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb) = zero,
inference(copy,[status(thm)],[c_3080]) ).
cnf(c_2941,plain,
quotient(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb,zero),
inference(paramod,[status(thm)],[c_2939,c_8]) ).
cnf(c_2942,plain,
$false,
inference(resolve,[status(thm)],[c_2941,c_2880]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HEN011-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.53 % Computer : n005.cluster.edu
% 0.11/0.53 % Model : x86_64 x86_64
% 0.11/0.53 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.53 % Memory : 8046.5625MB
% 0.11/0.53 % OS : Linux 6.8.0-71-generic
% 0.11/0.53 % CPULimit : 300
% 0.11/0.53 % WCLimit : 300
% 0.11/0.53 % DateTime : Fri Sep 25 15:58:02 UTC 2026
% 0.11/0.54 % CPUTime :
% 0.11/0.54 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.54 % Process 3884863 was started by sandbox2 on n005,
% 0.11/0.54 % Fri Sep 25 15:58:02 2026
% 0.11/0.54 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.11/0.54
% 0.11/0.54 % From the command line: assign(max_seconds, 300).
% 35.36/5.19
% 35.36/5.19 % given #500 (T,wt=6): 1838 quotient(idQ_idQa,divide(a,idQb_Q__idQ_idQa),zero). [para(1813(a,1),1072(a,1))].
% 35.36/5.19
% 35.36/5.19 % SZS status Unsatisfiable for theBenchmark
% 35.36/5.19
% 35.36/5.19 % Proof 1 at 3.58 (+ 0.94) seconds.
% 35.36/5.19 % Length of proof is 125.
% 35.36/5.19 % Level of proof is 32.
% 35.36/5.19 % Maximum clause weight is 23.000.
% 35.36/5.19 % Given clauses 644.
% 35.36/5.19
% 35.36/5.19 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------