%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : HEN011-3 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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:04 AM UTC 2026
% Result : Unsatisfiable 10.49s 1.79s
% Output : CNFRefutation 10.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 12
% Syntax : Number of formulae : 230 ( 185 unt; 0 def)
% Number of atoms : 277 ( 129 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 100 ( 53 ~; 47 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 8 con; 0-2 aty)
% Number of variables : 206 ( 70 sgn 13 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(quotient_less_equal1,axiom,
! [VAR_0,VAR_1] :
( divide(VAR_0,VAR_1) = zero
| ~ less_equal(VAR_0,VAR_1) ),
file('theBenchmark.p',quotient_less_equal1) ).
cnf(c_1,plain,
( divide(A,B) = zero
| ~ less_equal(A,B) ),
inference(clausify,[status(thm)],[quotient_less_equal1]) ).
fof(quotient_less_equal2,axiom,
! [VAR_0,VAR_1] :
( less_equal(VAR_0,VAR_1)
| divide(VAR_0,VAR_1) != zero ),
file('theBenchmark.p',quotient_less_equal2) ).
cnf(c_2,plain,
( less_equal(A,B)
| divide(A,B) != zero ),
inference(clausify,[status(thm)],[quotient_less_equal2]) ).
fof(quotient_smaller_than_numerator,axiom,
! [VAR_0,VAR_1] : less_equal(divide(VAR_0,VAR_1),VAR_0),
file('theBenchmark.p',quotient_smaller_than_numerator) ).
cnf(c_3,plain,
less_equal(divide(A,B),A),
inference(clausify,[status(thm)],[quotient_smaller_than_numerator]) ).
fof(quotient_property,axiom,
! [VAR_0,VAR_1,VAR_2] : less_equal(divide(divide(VAR_0,VAR_1),divide(VAR_2,VAR_1)),divide(divide(VAR_0,VAR_2),VAR_1)),
file('theBenchmark.p',quotient_property) ).
cnf(c_4,plain,
less_equal(divide(divide(A,B),divide(C,B)),divide(divide(A,C),B)),
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(identity_divide_a,axiom,
divide(identity,a) = c,
file('theBenchmark.p',identity_divide_a) ).
cnf(c_10,plain,
divide(identity,a) = c,
inference(clausify,[status(thm)],[identity_divide_a]) ).
fof(identity_divide_b,axiom,
divide(identity,b) = d,
file('theBenchmark.p',identity_divide_b) ).
cnf(c_11,plain,
divide(identity,b) = d,
inference(clausify,[status(thm)],[identity_divide_b]) ).
fof(identity_divide_c,axiom,
divide(identity,c) = e,
file('theBenchmark.p',identity_divide_c) ).
cnf(c_12,plain,
divide(identity,c) = e,
inference(clausify,[status(thm)],[identity_divide_c]) ).
fof(identity_divide_d,axiom,
divide(identity,d) = g,
file('theBenchmark.p',identity_divide_d) ).
cnf(c_13,plain,
divide(identity,d) = g,
inference(clausify,[status(thm)],[identity_divide_d]) ).
fof(prove_commutativity,axiom,
divide(c,g) != divide(d,e),
file('theBenchmark.p',prove_commutativity) ).
cnf(c_14,plain,
divide(c,g) != divide(d,e),
inference(clausify,[status(thm)],[prove_commutativity]) ).
cnf(c_15,plain,
divide(d,e) != divide(c,g),
inference(copy,[status(thm)],[c_14]) ).
cnf(c_16,plain,
divide(divide(A,B),A) = zero,
inference(resolve,[status(thm)],[c_1,c_3]) ).
cnf(c_17,plain,
divide(zero,A) = zero,
inference(resolve,[status(thm)],[c_1,c_5]) ).
cnf(c_18,plain,
divide(A,identity) = zero,
inference(resolve,[status(thm)],[c_1,c_7]) ).
cnf(c_20,plain,
less_equal(divide(c,divide(A,a)),divide(divide(identity,A),a)),
inference(paramod,[status(thm)],[c_10,c_4]) ).
cnf(c_2629,plain,
less_equal(divide(divide(A,a),c),divide(divide(A,identity),a)),
inference(paramod,[status(thm)],[c_10,c_4]) ).
cnf(c_2630,plain,
less_equal(divide(divide(A,a),c),divide(zero,a)),
inference(paramod,[status(thm)],[c_18,c_2629]) ).
cnf(c_21,plain,
less_equal(divide(divide(A,a),c),zero),
inference(paramod,[status(thm)],[c_17,c_2630]) ).
cnf(c_22,plain,
less_equal(divide(divide(identity,A),divide(a,A)),divide(c,A)),
inference(paramod,[status(thm)],[c_10,c_4]) ).
cnf(c_24,plain,
less_equal(divide(d,divide(A,b)),divide(divide(identity,A),b)),
inference(paramod,[status(thm)],[c_11,c_4]) ).
cnf(c_2631,plain,
less_equal(divide(divide(A,b),d),divide(divide(A,identity),b)),
inference(paramod,[status(thm)],[c_11,c_4]) ).
cnf(c_2632,plain,
less_equal(divide(divide(A,b),d),divide(zero,b)),
inference(paramod,[status(thm)],[c_18,c_2631]) ).
cnf(c_25,plain,
less_equal(divide(divide(A,b),d),zero),
inference(paramod,[status(thm)],[c_17,c_2632]) ).
cnf(c_26,plain,
less_equal(divide(divide(identity,A),divide(b,A)),divide(d,A)),
inference(paramod,[status(thm)],[c_11,c_4]) ).
cnf(c_2633,plain,
less_equal(divide(divide(A,c),e),divide(divide(A,identity),c)),
inference(paramod,[status(thm)],[c_12,c_4]) ).
cnf(c_2634,plain,
less_equal(divide(divide(A,c),e),divide(zero,c)),
inference(paramod,[status(thm)],[c_18,c_2633]) ).
cnf(c_29,plain,
less_equal(divide(divide(A,c),e),zero),
inference(paramod,[status(thm)],[c_17,c_2634]) ).
cnf(c_30,plain,
less_equal(divide(divide(identity,A),divide(c,A)),divide(e,A)),
inference(paramod,[status(thm)],[c_12,c_4]) ).
cnf(c_2635,plain,
less_equal(divide(divide(A,d),g),divide(divide(A,identity),d)),
inference(paramod,[status(thm)],[c_13,c_4]) ).
cnf(c_2636,plain,
less_equal(divide(divide(A,d),g),divide(zero,d)),
inference(paramod,[status(thm)],[c_18,c_2635]) ).
cnf(c_33,plain,
less_equal(divide(divide(A,d),g),zero),
inference(paramod,[status(thm)],[c_17,c_2636]) ).
cnf(c_35,plain,
less_equal(divide(divide(A,B),zero),divide(divide(A,divide(B,C)),B)),
inference(paramod,[status(thm)],[c_16,c_4]) ).
cnf(c_2637,plain,
less_equal(divide(divide(divide(A,B),C),divide(A,C)),divide(zero,C)),
inference(paramod,[status(thm)],[c_16,c_4]) ).
cnf(c_36,plain,
less_equal(divide(divide(divide(A,B),C),divide(A,C)),zero),
inference(paramod,[status(thm)],[c_17,c_2637]) ).
cnf(c_38,plain,
less_equal(divide(divide(A,B),zero),divide(divide(A,zero),B)),
inference(paramod,[status(thm)],[c_17,c_4]) ).
cnf(c_2638,plain,
less_equal(divide(divide(A,B),divide(identity,B)),divide(zero,B)),
inference(paramod,[status(thm)],[c_18,c_4]) ).
cnf(c_39,plain,
less_equal(divide(divide(A,B),divide(identity,B)),zero),
inference(paramod,[status(thm)],[c_17,c_2638]) ).
cnf(c_2639,plain,
less_equal(divide(c,c),divide(divide(identity,identity),a)),
inference(paramod,[status(thm)],[c_10,c_20]) ).
cnf(c_2640,plain,
less_equal(divide(c,c),divide(zero,a)),
inference(paramod,[status(thm)],[c_18,c_2639]) ).
cnf(c_41,plain,
less_equal(divide(c,c),zero),
inference(paramod,[status(thm)],[c_17,c_2640]) ).
cnf(c_44,plain,
less_equal(divide(c,divide(c,a)),divide(e,a)),
inference(paramod,[status(thm)],[c_12,c_20]) ).
cnf(c_2641,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2642,plain,
zero = divide(divide(A,a),c),
inference(resolve,[status(thm)],[c_2641,c_21]) ).
cnf(c_48,plain,
divide(divide(A,a),c) = zero,
inference(copy,[status(thm)],[c_2642]) ).
cnf(c_2643,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2644,plain,
zero = divide(c,c),
inference(resolve,[status(thm)],[c_2643,c_41]) ).
cnf(c_49,plain,
divide(c,c) = zero,
inference(copy,[status(thm)],[c_2644]) ).
cnf(c_2645,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2646,plain,
zero = divide(divide(A,b),d),
inference(resolve,[status(thm)],[c_2645,c_25]) ).
cnf(c_53,plain,
divide(divide(A,b),d) = zero,
inference(copy,[status(thm)],[c_2646]) ).
cnf(c_54,plain,
less_equal(divide(d,d),zero),
inference(paramod,[status(thm)],[c_11,c_25]) ).
cnf(c_2647,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2648,plain,
zero = divide(d,d),
inference(resolve,[status(thm)],[c_2647,c_54]) ).
cnf(c_55,plain,
divide(d,d) = zero,
inference(copy,[status(thm)],[c_2648]) ).
cnf(c_2649,plain,
less_equal(divide(e,divide(a,c)),divide(c,c)),
inference(paramod,[status(thm)],[c_12,c_22]) ).
cnf(c_58,plain,
less_equal(divide(e,divide(a,c)),zero),
inference(paramod,[status(thm)],[c_49,c_2649]) ).
cnf(c_63,plain,
less_equal(divide(d,divide(d,b)),divide(g,b)),
inference(paramod,[status(thm)],[c_13,c_24]) ).
cnf(c_2650,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2651,plain,
zero = divide(divide(A,c),e),
inference(resolve,[status(thm)],[c_2650,c_29]) ).
cnf(c_69,plain,
divide(divide(A,c),e) = zero,
inference(copy,[status(thm)],[c_2651]) ).
cnf(c_2652,plain,
less_equal(divide(g,divide(b,d)),divide(d,d)),
inference(paramod,[status(thm)],[c_13,c_26]) ).
cnf(c_77,plain,
less_equal(divide(g,divide(b,d)),zero),
inference(paramod,[status(thm)],[c_55,c_2652]) ).
cnf(c_2653,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2654,plain,
zero = divide(divide(A,d),g),
inference(resolve,[status(thm)],[c_2653,c_33]) ).
cnf(c_84,plain,
divide(divide(A,d),g) = zero,
inference(copy,[status(thm)],[c_2654]) ).
cnf(c_90,plain,
divide(divide(divide(identity,A),divide(c,A)),divide(e,A)) = zero,
inference(resolve,[status(thm)],[c_1,c_30]) ).
cnf(c_98,plain,
less_equal(divide(A,a),c),
inference(resolve,[status(thm)],[c_2,c_48]) ).
cnf(c_103,plain,
less_equal(divide(A,b),d),
inference(resolve,[status(thm)],[c_2,c_53]) ).
cnf(c_111,plain,
less_equal(divide(divide(A,A),zero),zero),
inference(paramod,[status(thm)],[c_16,c_35]) ).
cnf(c_2655,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2656,plain,
zero = divide(e,divide(a,c)),
inference(resolve,[status(thm)],[c_2655,c_58]) ).
cnf(c_112,plain,
divide(e,divide(a,c)) = zero,
inference(copy,[status(thm)],[c_2656]) ).
cnf(c_113,plain,
less_equal(divide(A,c),e),
inference(resolve,[status(thm)],[c_2,c_69]) ).
cnf(c_116,plain,
less_equal(divide(divide(A,e),divide(c,e)),zero),
inference(paramod,[status(thm)],[c_69,c_4]) ).
cnf(c_2657,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2658,plain,
zero = divide(g,divide(b,d)),
inference(resolve,[status(thm)],[c_2657,c_77]) ).
cnf(c_117,plain,
divide(g,divide(b,d)) = zero,
inference(copy,[status(thm)],[c_2658]) ).
cnf(c_2659,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2660,plain,
zero = divide(divide(divide(A,B),C),divide(A,C)),
inference(resolve,[status(thm)],[c_2659,c_36]) ).
cnf(c_118,plain,
divide(divide(divide(A,B),C),divide(A,C)) = zero,
inference(copy,[status(thm)],[c_2660]) ).
cnf(c_123,plain,
less_equal(divide(A,d),g),
inference(resolve,[status(thm)],[c_2,c_84]) ).
cnf(c_126,plain,
less_equal(divide(divide(A,g),divide(d,g)),zero),
inference(paramod,[status(thm)],[c_84,c_4]) ).
cnf(c_2661,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2662,plain,
zero = divide(divide(A,A),zero),
inference(resolve,[status(thm)],[c_2661,c_111]) ).
cnf(c_127,plain,
divide(divide(A,A),zero) = zero,
inference(copy,[status(thm)],[c_2662]) ).
cnf(c_128,plain,
less_equal(e,divide(a,c)),
inference(resolve,[status(thm)],[c_2,c_112]) ).
cnf(c_2663,plain,
( divide(A,c) = e
| ~ less_equal(e,divide(A,c)) ),
inference(resolve,[status(thm)],[c_6,c_113]) ).
cnf(c_132,plain,
divide(a,c) = e,
inference(resolve,[status(thm)],[c_2663,c_128]) ).
cnf(c_2664,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2665,plain,
zero = divide(divide(A,B),divide(identity,B)),
inference(resolve,[status(thm)],[c_2664,c_39]) ).
cnf(c_134,plain,
divide(divide(A,B),divide(identity,B)) = zero,
inference(copy,[status(thm)],[c_2665]) ).
cnf(c_139,plain,
divide(e,a) = zero,
inference(paramod,[status(thm)],[c_132,c_16]) ).
cnf(c_141,plain,
less_equal(divide(divide(A,a),zero),divide(divide(A,e),a)),
inference(paramod,[status(thm)],[c_132,c_35]) ).
cnf(c_143,plain,
less_equal(divide(c,divide(c,a)),zero),
inference(paramod,[status(thm)],[c_139,c_44]) ).
cnf(c_146,plain,
less_equal(g,divide(b,d)),
inference(resolve,[status(thm)],[c_2,c_117]) ).
cnf(c_2666,plain,
( divide(A,d) = g
| ~ less_equal(g,divide(A,d)) ),
inference(resolve,[status(thm)],[c_6,c_123]) ).
cnf(c_156,plain,
divide(b,d) = g,
inference(resolve,[status(thm)],[c_2666,c_146]) ).
cnf(c_161,plain,
divide(g,b) = zero,
inference(paramod,[status(thm)],[c_156,c_16]) ).
cnf(c_163,plain,
less_equal(divide(divide(A,b),zero),divide(divide(A,g),b)),
inference(paramod,[status(thm)],[c_156,c_35]) ).
cnf(c_165,plain,
less_equal(divide(d,divide(d,b)),zero),
inference(paramod,[status(thm)],[c_161,c_63]) ).
cnf(c_168,plain,
less_equal(divide(A,A),zero),
inference(resolve,[status(thm)],[c_2,c_127]) ).
cnf(c_2667,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2668,plain,
zero = divide(A,A),
inference(resolve,[status(thm)],[c_2667,c_168]) ).
cnf(c_171,plain,
divide(A,A) = zero,
inference(copy,[status(thm)],[c_2668]) ).
cnf(c_178,plain,
less_equal(divide(divide(A,divide(A,zero)),zero),zero),
inference(paramod,[status(thm)],[c_171,c_38]) ).
cnf(c_2669,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2670,plain,
zero = divide(c,divide(c,a)),
inference(resolve,[status(thm)],[c_2669,c_143]) ).
cnf(c_180,plain,
divide(c,divide(c,a)) = zero,
inference(copy,[status(thm)],[c_2670]) ).
cnf(c_2671,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2672,plain,
zero = divide(d,divide(d,b)),
inference(resolve,[status(thm)],[c_2671,c_165]) ).
cnf(c_181,plain,
divide(d,divide(d,b)) = zero,
inference(copy,[status(thm)],[c_2672]) ).
cnf(c_182,plain,
less_equal(c,divide(c,a)),
inference(resolve,[status(thm)],[c_2,c_180]) ).
cnf(c_2673,plain,
( divide(A,a) = c
| ~ less_equal(c,divide(A,a)) ),
inference(resolve,[status(thm)],[c_6,c_98]) ).
cnf(c_186,plain,
divide(c,a) = c,
inference(resolve,[status(thm)],[c_2673,c_182]) ).
cnf(c_192,plain,
less_equal(divide(c,zero),divide(divide(c,zero),a)),
inference(paramod,[status(thm)],[c_186,c_38]) ).
cnf(c_193,plain,
less_equal(d,divide(d,b)),
inference(resolve,[status(thm)],[c_2,c_181]) ).
cnf(c_2674,plain,
( divide(A,b) = d
| ~ less_equal(d,divide(A,b)) ),
inference(resolve,[status(thm)],[c_6,c_103]) ).
cnf(c_197,plain,
divide(d,b) = d,
inference(resolve,[status(thm)],[c_2674,c_193]) ).
cnf(c_201,plain,
less_equal(divide(d,zero),divide(divide(d,zero),b)),
inference(paramod,[status(thm)],[c_197,c_38]) ).
cnf(c_2675,plain,
( divide(A,B) = A
| ~ less_equal(A,divide(A,B)) ),
inference(resolve,[status(thm)],[c_6,c_3]) ).
cnf(c_212,plain,
divide(divide(c,zero),a) = divide(c,zero),
inference(resolve,[status(thm)],[c_2675,c_192]) ).
cnf(c_2676,plain,
( divide(A,B) = A
| ~ less_equal(A,divide(A,B)) ),
inference(resolve,[status(thm)],[c_6,c_3]) ).
cnf(c_213,plain,
divide(divide(d,zero),b) = divide(d,zero),
inference(resolve,[status(thm)],[c_2676,c_201]) ).
cnf(c_2677,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2678,plain,
zero = divide(divide(A,e),divide(c,e)),
inference(resolve,[status(thm)],[c_2677,c_116]) ).
cnf(c_225,plain,
divide(divide(A,e),divide(c,e)) = zero,
inference(copy,[status(thm)],[c_2678]) ).
cnf(c_2679,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2680,plain,
zero = divide(divide(A,g),divide(d,g)),
inference(resolve,[status(thm)],[c_2679,c_126]) ).
cnf(c_226,plain,
divide(divide(A,g),divide(d,g)) = zero,
inference(copy,[status(thm)],[c_2680]) ).
cnf(c_227,plain,
less_equal(divide(A,B),divide(identity,B)),
inference(resolve,[status(thm)],[c_2,c_134]) ).
cnf(c_235,plain,
less_equal(divide(A,e),divide(c,e)),
inference(resolve,[status(thm)],[c_2,c_225]) ).
cnf(c_2681,plain,
less_equal(divide(divide(divide(A,e),c),zero),divide(zero,c)),
inference(paramod,[status(thm)],[c_225,c_35]) ).
cnf(c_238,plain,
less_equal(divide(divide(divide(A,e),c),zero),zero),
inference(paramod,[status(thm)],[c_17,c_2681]) ).
cnf(c_2682,plain,
( divide(B,A) = divide(identity,A)
| ~ less_equal(divide(identity,A),divide(B,A)) ),
inference(resolve,[status(thm)],[c_6,c_227]) ).
cnf(c_239,plain,
divide(c,e) = divide(identity,e),
inference(resolve,[status(thm)],[c_2682,c_235]) ).
cnf(c_242,plain,
less_equal(divide(divide(identity,e),divide(A,e)),divide(divide(c,A),e)),
inference(paramod,[status(thm)],[c_239,c_4]) ).
cnf(c_268,plain,
less_equal(divide(A,g),divide(d,g)),
inference(resolve,[status(thm)],[c_2,c_226]) ).
cnf(c_2683,plain,
less_equal(divide(divide(divide(A,g),d),zero),divide(zero,d)),
inference(paramod,[status(thm)],[c_226,c_35]) ).
cnf(c_271,plain,
less_equal(divide(divide(divide(A,g),d),zero),zero),
inference(paramod,[status(thm)],[c_17,c_2683]) ).
cnf(c_2684,plain,
( divide(B,A) = divide(identity,A)
| ~ less_equal(divide(identity,A),divide(B,A)) ),
inference(resolve,[status(thm)],[c_6,c_227]) ).
cnf(c_276,plain,
divide(d,g) = divide(identity,g),
inference(resolve,[status(thm)],[c_2684,c_268]) ).
cnf(c_302,plain,
less_equal(divide(divide(A,B),C),divide(A,C)),
inference(resolve,[status(thm)],[c_2,c_118]) ).
cnf(c_316,plain,
less_equal(divide(divide(divide(A,B),C),A),zero),
inference(paramod,[status(thm)],[c_16,c_302]) ).
cnf(c_367,plain,
less_equal(divide(divide(c,zero),zero),divide(divide(divide(c,zero),e),a)),
inference(paramod,[status(thm)],[c_212,c_141]) ).
cnf(c_378,plain,
less_equal(divide(divide(d,zero),zero),divide(divide(divide(d,zero),g),b)),
inference(paramod,[status(thm)],[c_213,c_163]) ).
cnf(c_2685,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2686,plain,
zero = divide(divide(A,divide(A,zero)),zero),
inference(resolve,[status(thm)],[c_2685,c_178]) ).
cnf(c_382,plain,
divide(divide(A,divide(A,zero)),zero) = zero,
inference(copy,[status(thm)],[c_2686]) ).
cnf(c_2687,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2688,plain,
zero = divide(divide(divide(A,e),c),zero),
inference(resolve,[status(thm)],[c_2687,c_238]) ).
cnf(c_390,plain,
divide(divide(divide(A,e),c),zero) = zero,
inference(copy,[status(thm)],[c_2688]) ).
cnf(c_2689,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2690,plain,
zero = divide(divide(divide(A,g),d),zero),
inference(resolve,[status(thm)],[c_2689,c_271]) ).
cnf(c_399,plain,
divide(divide(divide(A,g),d),zero) = zero,
inference(copy,[status(thm)],[c_2690]) ).
cnf(c_2691,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2692,plain,
zero = divide(divide(divide(A,B),C),A),
inference(resolve,[status(thm)],[c_2691,c_316]) ).
cnf(c_405,plain,
divide(divide(divide(A,B),C),A) = zero,
inference(copy,[status(thm)],[c_2692]) ).
cnf(c_419,plain,
less_equal(divide(A,divide(A,zero)),zero),
inference(resolve,[status(thm)],[c_2,c_382]) ).
cnf(c_2693,plain,
( zero = A
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2694,plain,
zero = divide(A,divide(A,zero)),
inference(resolve,[status(thm)],[c_2693,c_419]) ).
cnf(c_421,plain,
divide(A,divide(A,zero)) = zero,
inference(copy,[status(thm)],[c_2694]) ).
cnf(c_425,plain,
less_equal(A,divide(A,zero)),
inference(resolve,[status(thm)],[c_2,c_421]) ).
cnf(c_2695,plain,
( divide(A,B) = A
| ~ less_equal(A,divide(A,B)) ),
inference(resolve,[status(thm)],[c_6,c_3]) ).
cnf(c_459,plain,
divide(A,zero) = A,
inference(resolve,[status(thm)],[c_2695,c_425]) ).
cnf(c_2696,plain,
less_equal(divide(d,zero),divide(divide(divide(d,zero),g),b)),
inference(paramod,[status(thm)],[c_459,c_378]) ).
cnf(c_2697,plain,
less_equal(d,divide(divide(divide(d,zero),g),b)),
inference(paramod,[status(thm)],[c_459,c_2696]) ).
cnf(c_2698,plain,
less_equal(d,divide(divide(d,g),b)),
inference(paramod,[status(thm)],[c_459,c_2697]) ).
cnf(c_460,plain,
less_equal(d,divide(divide(identity,g),b)),
inference(paramod,[status(thm)],[c_276,c_2698]) ).
cnf(c_2699,plain,
less_equal(divide(c,zero),divide(divide(divide(c,zero),e),a)),
inference(paramod,[status(thm)],[c_459,c_367]) ).
cnf(c_2700,plain,
less_equal(c,divide(divide(divide(c,zero),e),a)),
inference(paramod,[status(thm)],[c_459,c_2699]) ).
cnf(c_2701,plain,
less_equal(c,divide(divide(c,e),a)),
inference(paramod,[status(thm)],[c_459,c_2700]) ).
cnf(c_461,plain,
less_equal(c,divide(divide(identity,e),a)),
inference(paramod,[status(thm)],[c_239,c_2701]) ).
cnf(c_468,plain,
divide(divide(A,g),d) = zero,
inference(paramod,[status(thm)],[c_459,c_399]) ).
cnf(c_473,plain,
divide(divide(A,e),c) = zero,
inference(paramod,[status(thm)],[c_459,c_390]) ).
cnf(c_520,plain,
less_equal(divide(A,B),divide(divide(A,divide(B,C)),B)),
inference(paramod,[status(thm)],[c_459,c_35]) ).
cnf(c_2702,plain,
( divide(A,b) = d
| ~ less_equal(d,divide(A,b)) ),
inference(resolve,[status(thm)],[c_6,c_103]) ).
cnf(c_522,plain,
divide(divide(identity,g),b) = d,
inference(resolve,[status(thm)],[c_2702,c_460]) ).
cnf(c_2703,plain,
( divide(A,a) = c
| ~ less_equal(c,divide(A,a)) ),
inference(resolve,[status(thm)],[c_6,c_98]) ).
cnf(c_523,plain,
divide(divide(identity,e),a) = c,
inference(resolve,[status(thm)],[c_2703,c_461]) ).
cnf(c_539,plain,
less_equal(divide(A,g),d),
inference(resolve,[status(thm)],[c_2,c_468]) ).
cnf(c_548,plain,
less_equal(divide(A,e),c),
inference(resolve,[status(thm)],[c_2,c_473]) ).
cnf(c_559,plain,
less_equal(d,divide(identity,g)),
inference(paramod,[status(thm)],[c_522,c_3]) ).
cnf(c_2704,plain,
( divide(A,g) = d
| ~ less_equal(d,divide(A,g)) ),
inference(resolve,[status(thm)],[c_6,c_539]) ).
cnf(c_565,plain,
divide(identity,g) = d,
inference(resolve,[status(thm)],[c_2704,c_559]) ).
cnf(c_573,plain,
less_equal(divide(divide(identity,A),divide(g,A)),divide(d,A)),
inference(paramod,[status(thm)],[c_565,c_4]) ).
cnf(c_581,plain,
divide(divide(d,divide(c,g)),divide(e,g)) = zero,
inference(paramod,[status(thm)],[c_565,c_90]) ).
cnf(c_583,plain,
less_equal(c,divide(identity,e)),
inference(paramod,[status(thm)],[c_523,c_3]) ).
cnf(c_2705,plain,
( divide(A,e) = c
| ~ less_equal(c,divide(A,e)) ),
inference(resolve,[status(thm)],[c_6,c_548]) ).
cnf(c_588,plain,
divide(identity,e) = c,
inference(resolve,[status(thm)],[c_2705,c_583]) ).
cnf(c_591,plain,
less_equal(divide(c,divide(A,e)),divide(divide(c,A),e)),
inference(paramod,[status(thm)],[c_588,c_242]) ).
cnf(c_692,plain,
less_equal(divide(divide(A,B),C),A),
inference(resolve,[status(thm)],[c_2,c_405]) ).
cnf(c_2706,plain,
( divide(divide(A,C),B) = divide(A,B)
| ~ less_equal(divide(A,B),divide(divide(A,C),B)) ),
inference(resolve,[status(thm)],[c_6,c_302]) ).
cnf(c_788,plain,
divide(divide(A,divide(B,C)),B) = divide(A,B),
inference(resolve,[status(thm)],[c_2706,c_520]) ).
cnf(c_855,plain,
less_equal(divide(c,divide(g,e)),divide(d,e)),
inference(paramod,[status(thm)],[c_588,c_573]) ).
cnf(c_1466,plain,
less_equal(divide(A,B),divide(A,divide(B,C))),
inference(paramod,[status(thm)],[c_788,c_3]) ).
cnf(c_1489,plain,
less_equal(divide(divide(A,B),C),divide(A,divide(B,D))),
inference(paramod,[status(thm)],[c_788,c_692]) ).
cnf(c_2707,plain,
divide(zero,e) = divide(divide(d,divide(c,g)),e),
inference(paramod,[status(thm)],[c_581,c_788]) ).
cnf(c_2708,plain,
zero = divide(divide(d,divide(c,g)),e),
inference(paramod,[status(thm)],[c_17,c_2707]) ).
cnf(c_1497,plain,
divide(divide(d,divide(c,g)),e) = zero,
inference(copy,[status(thm)],[c_2708]) ).
cnf(c_2709,plain,
( divide(c,divide(A,e)) = divide(divide(c,A),e)
| ~ less_equal(divide(divide(c,A),e),divide(c,divide(A,e))) ),
inference(resolve,[status(thm)],[c_6,c_591]) ).
cnf(c_2710,plain,
divide(c,divide(A,e)) = divide(divide(c,A),e),
inference(resolve,[status(thm)],[c_2709,c_1489]) ).
cnf(c_2119,plain,
divide(divide(c,A),e) = divide(c,divide(A,e)),
inference(copy,[status(thm)],[c_2710]) ).
cnf(c_2711,plain,
less_equal(divide(divide(d,e),divide(divide(c,g),e)),zero),
inference(paramod,[status(thm)],[c_1497,c_4]) ).
cnf(c_2197,plain,
less_equal(divide(divide(d,e),divide(c,divide(g,e))),zero),
inference(paramod,[status(thm)],[c_2119,c_2711]) ).
cnf(c_2542,plain,
less_equal(divide(c,divide(A,e)),divide(c,A)),
inference(paramod,[status(thm)],[c_2119,c_3]) ).
cnf(c_2712,plain,
( divide(A,B) = divide(A,divide(B,C))
| ~ less_equal(divide(A,divide(B,C)),divide(A,B)) ),
inference(resolve,[status(thm)],[c_6,c_1466]) ).
cnf(c_2713,plain,
divide(c,A) = divide(c,divide(A,e)),
inference(resolve,[status(thm)],[c_2712,c_2542]) ).
cnf(c_2585,plain,
divide(c,divide(A,e)) = divide(c,A),
inference(copy,[status(thm)],[c_2713]) ).
cnf(c_2607,plain,
less_equal(divide(divide(d,e),divide(c,g)),zero),
inference(paramod,[status(thm)],[c_2585,c_2197]) ).
cnf(c_2617,plain,
less_equal(divide(c,g),divide(d,e)),
inference(paramod,[status(thm)],[c_2585,c_855]) ).
cnf(c_2714,plain,
( divide(d,e) = divide(c,g)
| ~ less_equal(divide(d,e),divide(c,g)) ),
inference(resolve,[status(thm)],[c_6,c_2617]) ).
cnf(c_2623,plain,
~ less_equal(divide(d,e),divide(c,g)),
inference(resolve,[status(thm)],[c_2714,c_15]) ).
cnf(c_2624,plain,
divide(divide(d,e),divide(c,g)) != zero,
inference(resolve,[status(thm)],[c_2,c_2623]) ).
cnf(c_2715,plain,
( A = zero
| ~ less_equal(A,zero) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_2627,plain,
~ less_equal(divide(divide(d,e),divide(c,g)),zero),
inference(resolve,[status(thm)],[c_2715,c_2624]) ).
cnf(c_2628,plain,
$false,
inference(resolve,[status(thm)],[c_2627,c_2607]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HEN011-3 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n007.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Fri Sep 25 15:56:08 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/0.35 % Process 1414357 was started by sandbox on n007,
% 0.07/0.35 % Fri Sep 25 15:56:08 2026
% 0.07/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.07/0.36
% 0.07/0.36 % From the command line: assign(max_seconds, 300).
% 10.49/1.79
% 10.49/1.79 % given #500 (T,wt=21): 948 less_equal(divide(divide(a,divide(a,e)),A),e). [para(881(a,1),692(a,1,1))].
% 10.49/1.79
% 10.49/1.79 % given #1000 (A,wt=29): 1101 less_equal(divide(A,B),divide(divide(A,divide(C,divide(identity,B))),B)). [para(1068(a,1),4(a,1,2)),rewrite([459(3)])].
% 10.49/1.79
% 10.49/1.79 % SZS status Unsatisfiable for theBenchmark
% 10.49/1.79
% 10.49/1.79 % Proof 1 at 0.88 (+ 0.45) seconds.
% 10.49/1.79 % Length of proof is 131.
% 10.49/1.79 % Level of proof is 28.
% 10.49/1.79 % Maximum clause weight is 29.000.
% 10.49/1.79 % Given clauses 1002.
% 10.49/1.79
% 10.49/1.79 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------