%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : HEN006-2 : TPTP v9.2.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 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 : Tue May 5 04:28:31 PM UTC 2026
% Result : Unsatisfiable 135.88s 92.91s
% Output : CNFRefutation 139.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 26
% Syntax : Number of clauses : 336 ( 305 unt; 0 nHn; 84 RR)
% Number of literals : 399 ( 31 equ; 96 neg)
% Maximal clause size : 6 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 7 con; 0-2 aty)
% Number of variables : 442 ( 72 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(quotient_property,axiom,
( less_equal(X7,X8)
| ~ quotient(X1,X2,X3)
| ~ quotient(X2,X4,X5)
| ~ quotient(X1,X4,X6)
| ~ quotient(X6,X5,X7)
| ~ quotient(X3,X4,X8) ),
file('/export/starexec/sandbox/benchmark/Axioms/HEN001-0.ax',quotient_property) ).
cnf(well_defined,axiom,
( X3 = X4
| ~ quotient(X1,X2,X3)
| ~ quotient(X1,X2,X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/HEN001-0.ax',well_defined) ).
cnf(divisor_existence,axiom,
( less_equal(X3,X1)
| ~ quotient(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/HEN001-0.ax',divisor_existence) ).
cnf(less_equal_quotient,axiom,
( less_equal(X1,X2)
| ~ quotient(X1,X2,zero) ),
file('/export/starexec/sandbox/benchmark/Axioms/HEN001-0.ax',less_equal_quotient) ).
cnf(closure,axiom,
quotient(X1,X2,divide(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/HEN001-0.ax',closure) ).
cnf(quotient_less_equal,axiom,
( quotient(X1,X2,zero)
| ~ less_equal(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/HEN001-0.ax',quotient_less_equal) ).
cnf(transitivity_of_less_equal,axiom,
( less_equal(X1,X3)
| ~ less_equal(X1,X2)
| ~ less_equal(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity_of_less_equal) ).
cnf(x_divde_zero_is_x,axiom,
quotient(X1,zero,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',x_divde_zero_is_x) ).
cnf(x_divide_x_is_zero,axiom,
quotient(X1,X1,zero),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',x_divide_x_is_zero) ).
cnf(zero_divide_anything_is_zero,axiom,
quotient(zero,X1,zero),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',zero_divide_anything_is_zero) ).
cnf(everything_divide_identity_is_zero,axiom,
quotient(X1,identity,zero),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',everything_divide_identity_is_zero) ).
cnf(xQz,hypothesis,
quotient(x,z,xQz),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',xQz) ).
cnf(xQy,hypothesis,
quotient(x,y,xQy),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',xQy) ).
cnf(less_equal_and_equal,axiom,
( X1 = X2
| ~ less_equal(X1,X2)
| ~ less_equal(X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HEN001-0.ax',less_equal_and_equal) ).
cnf(prove_xQzLEy,negated_conjecture,
~ less_equal(xQz,y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_xQzLEy) ).
cnf(zero_is_smallest,axiom,
less_equal(zero,X1),
file('/export/starexec/sandbox/benchmark/Axioms/HEN001-0.ax',zero_is_smallest) ).
cnf(identity_is_largest,axiom,
less_equal(X1,identity),
file('/export/starexec/sandbox/benchmark/Axioms/HEN001-0.ax',identity_is_largest) ).
cnf(xQyLEz,hypothesis,
less_equal(xQy,z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',xQyLEz) ).
cnf(i_0_18,axiom,
( less_equal(X7,X8)
| ~ quotient(X1,X2,X3)
| ~ quotient(X2,X4,X5)
| ~ quotient(X1,X4,X6)
| ~ quotient(X6,X5,X7)
| ~ quotient(X3,X4,X8) ),
quotient_property,
[final] ).
cnf(i_0_19,axiom,
( X3 = X4
| ~ quotient(X1,X2,X3)
| ~ quotient(X1,X2,X4) ),
well_defined,
[final] ).
cnf(i_0_20,axiom,
( less_equal(X3,X1)
| ~ quotient(X1,X2,X3) ),
divisor_existence,
[final] ).
cnf(i_0_21,axiom,
( less_equal(X1,X2)
| ~ quotient(X1,X2,zero) ),
less_equal_quotient,
[final] ).
cnf(i_0_22,axiom,
quotient(X1,X2,divide(X1,X2)),
closure,
[final] ).
cnf(i_0_23,axiom,
( quotient(X1,X2,zero)
| ~ less_equal(X1,X2) ),
quotient_less_equal,
[final] ).
cnf(i_0_24,axiom,
( less_equal(X1,X3)
| ~ less_equal(X1,X2)
| ~ less_equal(X2,X3) ),
transitivity_of_less_equal,
[final] ).
cnf(i_0_25,axiom,
quotient(X1,zero,X1),
x_divde_zero_is_x,
[final] ).
cnf(i_0_26,axiom,
quotient(X1,X1,zero),
x_divide_x_is_zero,
[final] ).
cnf(i_0_27,axiom,
quotient(zero,X1,zero),
zero_divide_anything_is_zero,
[final] ).
cnf(i_0_28,axiom,
quotient(X1,identity,zero),
everything_divide_identity_is_zero,
[final] ).
cnf(i_0_29,hypothesis,
quotient(x,z,xQz),
xQz,
[final] ).
cnf(i_0_30,hypothesis,
quotient(x,y,xQy),
xQy,
[final] ).
cnf(i_0_31,axiom,
( X1 = X2
| ~ less_equal(X1,X2)
| ~ less_equal(X2,X1) ),
less_equal_and_equal,
[final] ).
cnf(i_0_32,negated_conjecture,
~ less_equal(xQz,y),
prove_xQzLEy,
[final] ).
cnf(i_0_33,axiom,
less_equal(zero,X1),
zero_is_smallest,
[final] ).
cnf(i_0_34,axiom,
less_equal(X1,identity),
identity_is_largest,
[final] ).
cnf(i_0_35,hypothesis,
less_equal(xQy,z),
xQyLEz,
[final] ).
cnf(i_0_36,axiom,
X1 = X1 ).
cnf(i_0_37,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_38,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_39,axiom,
( X1 != X2
| ~ less_equal(X1,X3)
| less_equal(X2,X3) ) ).
cnf(i_0_40,axiom,
( X1 != X2
| ~ less_equal(X3,X1)
| less_equal(X3,X2) ) ).
cnf(i_0_41,axiom,
( X1 != X2
| ~ quotient(X1,X3,X4)
| quotient(X2,X3,X4) ) ).
cnf(i_0_42,axiom,
( X1 != X2
| ~ quotient(X3,X1,X4)
| quotient(X3,X2,X4) ) ).
cnf(i_0_43,axiom,
( X1 != X2
| ~ quotient(X3,X4,X1)
| quotient(X3,X4,X2) ) ).
cnf(i_0_44,plain,
~ quotient(y,X1,xQz),
inference(scs_inference,[],[i_0_32,i_0_20]) ).
cnf(i_0_46,plain,
less_equal(X1,X1),
inference(scs_inference,[],[i_0_32,i_0_26,i_0_20,i_0_21]) ).
cnf(i_0_48,plain,
~ less_equal(xQz,zero),
inference(scs_inference,[],[i_0_32,i_0_26,i_0_33,i_0_20,i_0_21,i_0_24]) ).
cnf(i_0_49,plain,
less_equal(zero,X1),
inference(rename_variables,[],[i_0_33]) ).
cnf(i_0_52,plain,
less_equal(zero,X1),
inference(rename_variables,[],[i_0_33]) ).
cnf(i_0_54,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_57,plain,
less_equal(X1,identity),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_59,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_61,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_63,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_65,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_66,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_67,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_68,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_69,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_78,plain,
less_equal(zero,X1),
inference(rename_variables,[],[i_0_33]) ).
cnf(i_0_95,plain,
quotient(zero,X1,zero),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_98,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_113,plain,
quotient(X1,identity,zero),
inference(rename_variables,[],[i_0_28]) ).
cnf(i_0_116,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_118,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_122,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_123,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_124,plain,
quotient(zero,X1,zero),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_147,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_149,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_153,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_156,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_161,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_164,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_169,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_172,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_177,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_187,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_193,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_197,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_201,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_208,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_211,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_214,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_217,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_219,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_221,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_224,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_227,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_228,plain,
less_equal(divide(xQz,zero),xQz),
inference(scs_inference,[],[i_0_29,i_0_27,i_0_25,i_0_22,i_0_18]) ).
cnf(i_0_229,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_230,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_231,plain,
quotient(zero,X1,zero),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_239,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_242,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_243,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_244,plain,
quotient(zero,X1,zero),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_249,plain,
quotient(X1,identity,zero),
inference(rename_variables,[],[i_0_28]) ).
cnf(i_0_250,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_253,plain,
less_equal(X1,identity),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_257,plain,
less_equal(X1,identity),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_264,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_268,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_272,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_274,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_276,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_280,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_290,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_302,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_306,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_310,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_320,plain,
less_equal(X1,identity),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_323,plain,
less_equal(X1,identity),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_329,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_334,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_335,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_336,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_350,plain,
less_equal(zero,X1),
inference(rename_variables,[],[i_0_33]) ).
cnf(i_0_375,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_393,plain,
less_equal(X1,identity),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_396,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_405,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_422,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_436,plain,
less_equal(X1,identity),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_439,plain,
less_equal(zero,X1),
inference(rename_variables,[],[i_0_33]) ).
cnf(i_0_442,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_448,plain,
quotient(X1,identity,zero),
inference(rename_variables,[],[i_0_28]) ).
cnf(i_0_449,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_463,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_470,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_472,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_476,plain,
quotient(xQy,z,zero),
inference(scs_inference,[],[i_0_35,i_0_23]) ).
cnf(i_0_482,plain,
less_equal(X1,identity),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_503,plain,
less_equal(zero,X1),
inference(rename_variables,[],[i_0_33]) ).
cnf(i_0_506,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_512,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_524,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_530,plain,
less_equal(X1,identity),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_553,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_615,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_670,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_691,plain,
less_equal(X1,identity),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_735,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_788,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_795,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_815,plain,
quotient(X1,identity,zero),
inference(rename_variables,[],[i_0_28]) ).
cnf(i_0_818,plain,
less_equal(X1,identity),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_840,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_845,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_848,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_854,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_921,plain,
less_equal(zero,X1),
inference(rename_variables,[],[i_0_33]) ).
cnf(i_0_937,plain,
less_equal(zero,X1),
inference(rename_variables,[],[i_0_33]) ).
cnf(i_0_940,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_947,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_948,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_955,plain,
less_equal(zero,X1),
inference(rename_variables,[],[i_0_33]) ).
cnf(i_0_962,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_966,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_971,plain,
quotient(X1,identity,zero),
inference(rename_variables,[],[i_0_28]) ).
cnf(i_0_977,plain,
less_equal(zero,X1),
inference(rename_variables,[],[i_0_33]) ).
cnf(i_0_1023,plain,
less_equal(zero,X1),
inference(rename_variables,[],[i_0_33]) ).
cnf(i_0_1036,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1104,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1202,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_1241,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1244,plain,
quotient(zero,X1,zero),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_1372,plain,
less_equal(zero,X1),
inference(rename_variables,[],[i_0_33]) ).
cnf(i_0_1421,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1431,plain,
less_equal(zero,X1),
inference(rename_variables,[],[i_0_33]) ).
cnf(i_0_1514,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_1515,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1541,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1547,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1550,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1551,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1552,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1565,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1573,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1574,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1575,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1583,plain,
less_equal(X1,identity),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_1591,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1595,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1603,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1609,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1620,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1633,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1642,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1648,plain,
less_equal(X1,identity),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_1657,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_1658,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1669,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1670,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1671,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1697,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1703,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1708,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1709,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1749,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1759,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1761,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1762,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1781,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1786,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1815,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1839,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_1841,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_1842,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_1843,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_1860,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_1879,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_1885,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_1889,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_1890,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_1891,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_1908,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_1944,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_1955,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_1977,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_1988,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_1989,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_1990,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_2011,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_2013,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_2014,plain,
quotient(zero,X1,zero),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_2031,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_2040,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_2042,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_2043,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_2044,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_2066,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_2067,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_2084,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_2089,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_2108,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_2109,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_2110,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_2119,plain,
less_equal(zero,X1),
inference(rename_variables,[],[i_0_33]) ).
cnf(i_0_2123,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_2135,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_2155,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_2184,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_2185,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_2198,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_2199,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_2200,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_2226,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_2227,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_2228,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_2247,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_2250,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_2272,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_2283,plain,
less_equal(zero,X1),
inference(rename_variables,[],[i_0_33]) ).
cnf(i_0_2295,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_2346,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_2347,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_2348,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_2349,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_2374,plain,
quotient(zero,X1,zero),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_2419,plain,
quotient(zero,X1,zero),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_2438,plain,
quotient(zero,X1,zero),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_2439,plain,
quotient(zero,X1,zero),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_2450,plain,
quotient(zero,X1,zero),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_2451,plain,
quotient(zero,X1,zero),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_2452,plain,
quotient(zero,X1,zero),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_2518,plain,
quotient(zero,X1,zero),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_2519,plain,
quotient(zero,X1,zero),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_2520,plain,
quotient(zero,X1,zero),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_51,plain,
zero != xQz,
inference(scs_inference,[],[i_0_32,i_0_26,i_0_33,i_0_49,i_0_20,i_0_21,i_0_24,i_0_39]) ).
cnf(i_0_53,plain,
~ quotient(xQz,zero,zero),
inference(scs_inference,[],[i_0_32,i_0_25,i_0_26,i_0_33,i_0_49,i_0_20,i_0_21,i_0_24,i_0_39,i_0_19]) ).
cnf(i_0_56,plain,
identity != y,
inference(scs_inference,[],[i_0_32,i_0_25,i_0_26,i_0_33,i_0_49,i_0_34,i_0_20,i_0_21,i_0_24,i_0_39,i_0_19,i_0_40]) ).
cnf(i_0_58,plain,
xQz != y,
inference(scs_inference,[],[i_0_32,i_0_25,i_0_54,i_0_26,i_0_33,i_0_49,i_0_34,i_0_20,i_0_21,i_0_24,i_0_39,i_0_19,i_0_40,i_0_41]) ).
cnf(i_0_60,plain,
xQz != zero,
inference(scs_inference,[],[i_0_32,i_0_25,i_0_54,i_0_26,i_0_33,i_0_49,i_0_34,i_0_20,i_0_21,i_0_24,i_0_39,i_0_19,i_0_40,i_0_41,i_0_42]) ).
cnf(i_0_62,plain,
y != xQz,
inference(scs_inference,[],[i_0_32,i_0_25,i_0_54,i_0_59,i_0_26,i_0_33,i_0_49,i_0_34,i_0_20,i_0_21,i_0_24,i_0_39,i_0_19,i_0_40,i_0_41,i_0_42,i_0_43]) ).
cnf(i_0_64,plain,
less_equal(divide(zero,zero),zero),
inference(scs_inference,[],[i_0_32,i_0_25,i_0_54,i_0_59,i_0_63,i_0_26,i_0_22,i_0_33,i_0_49,i_0_34,i_0_20,i_0_21,i_0_24,i_0_39,i_0_19,i_0_40,i_0_41,i_0_42,i_0_43,i_0_18]) ).
cnf(i_0_73,plain,
~ quotient(zero,X1,xQz),
inference(scs_inference,[],[i_0_48,i_0_20]) ).
cnf(i_0_84,plain,
less_equal(X1,X1),
inference(rename_variables,[],[i_0_46]) ).
cnf(i_0_86,plain,
~ quotient(y,X1,xQz),
inference(rename_variables,[],[i_0_44]) ).
cnf(i_0_105,plain,
less_equal(X1,X1),
inference(rename_variables,[],[i_0_46]) ).
cnf(i_0_107,plain,
less_equal(X1,X1),
inference(rename_variables,[],[i_0_46]) ).
cnf(i_0_120,plain,
less_equal(X1,X1),
inference(rename_variables,[],[i_0_46]) ).
cnf(i_0_131,plain,
less_equal(X1,X1),
inference(rename_variables,[],[i_0_46]) ).
cnf(i_0_182,plain,
less_equal(X1,X1),
inference(rename_variables,[],[i_0_46]) ).
cnf(i_0_209,plain,
divide(y,X1) != xQz,
inference(scs_inference,[],[i_0_22,i_0_44,i_0_43]) ).
cnf(i_0_210,plain,
~ quotient(y,X1,xQz),
inference(rename_variables,[],[i_0_44]) ).
cnf(i_0_236,plain,
less_equal(X1,X1),
inference(rename_variables,[],[i_0_46]) ).
cnf(i_0_246,plain,
less_equal(X1,X1),
inference(rename_variables,[],[i_0_46]) ).
cnf(i_0_247,plain,
less_equal(X1,X1),
inference(rename_variables,[],[i_0_46]) ).
cnf(i_0_285,plain,
less_equal(X1,X1),
inference(rename_variables,[],[i_0_46]) ).
cnf(i_0_296,plain,
less_equal(X1,X1),
inference(rename_variables,[],[i_0_46]) ).
cnf(i_0_311,plain,
quotient(divide(xQz,zero),xQz,zero),
inference(scs_inference,[],[i_0_228,i_0_23]) ).
cnf(i_0_313,plain,
~ quotient(xQz,y,zero),
inference(scs_inference,[],[i_0_32,i_0_228,i_0_23,i_0_21]) ).
cnf(i_0_420,plain,
less_equal(X1,X1),
inference(rename_variables,[],[i_0_46]) ).
cnf(i_0_1528,plain,
less_equal(X1,X1),
inference(rename_variables,[],[i_0_46]) ).
cnf(i_0_75,plain,
~ less_equal(xQz,divide(zero,zero)),
inference(scs_inference,[],[i_0_64,i_0_48,i_0_20,i_0_24]) ).
cnf(i_0_77,plain,
divide(zero,zero) = zero,
inference(scs_inference,[],[i_0_64,i_0_48,i_0_33,i_0_20,i_0_24,i_0_31]) ).
cnf(i_0_80,plain,
~ quotient(X1,identity,xQz),
inference(scs_inference,[],[i_0_64,i_0_48,i_0_28,i_0_60,i_0_33,i_0_20,i_0_24,i_0_31,i_0_19]) ).
cnf(i_0_82,plain,
divide(zero,zero) != xQz,
inference(scs_inference,[],[i_0_64,i_0_48,i_0_28,i_0_60,i_0_33,i_0_20,i_0_24,i_0_31,i_0_19,i_0_39]) ).
cnf(i_0_83,plain,
xQz != divide(zero,zero),
inference(scs_inference,[],[i_0_64,i_0_46,i_0_48,i_0_28,i_0_60,i_0_33,i_0_20,i_0_24,i_0_31,i_0_19,i_0_39,i_0_40]) ).
cnf(i_0_85,plain,
x != y,
inference(scs_inference,[],[i_0_64,i_0_46,i_0_48,i_0_44,i_0_28,i_0_29,i_0_60,i_0_33,i_0_20,i_0_24,i_0_31,i_0_19,i_0_39,i_0_40,i_0_41]) ).
cnf(i_0_87,plain,
~ quotient(xQz,divide(zero,zero),zero),
inference(scs_inference,[],[i_0_64,i_0_46,i_0_48,i_0_44,i_0_28,i_0_29,i_0_53,i_0_60,i_0_33,i_0_20,i_0_24,i_0_31,i_0_19,i_0_39,i_0_40,i_0_41,i_0_42]) ).
cnf(i_0_88,plain,
~ quotient(xQz,zero,divide(zero,zero)),
inference(scs_inference,[],[i_0_64,i_0_46,i_0_48,i_0_44,i_0_28,i_0_29,i_0_53,i_0_60,i_0_33,i_0_20,i_0_24,i_0_31,i_0_19,i_0_39,i_0_40,i_0_41,i_0_42,i_0_43]) ).
cnf(i_0_89,plain,
zero = divide(zero,zero),
inference(scs_inference,[],[i_0_64,i_0_46,i_0_48,i_0_44,i_0_28,i_0_29,i_0_53,i_0_60,i_0_33,i_0_20,i_0_24,i_0_31,i_0_19,i_0_39,i_0_40,i_0_41,i_0_42,i_0_43,i_0_37]) ).
cnf(i_0_146,plain,
~ quotient(zero,X1,xQz),
inference(rename_variables,[],[i_0_73]) ).
cnf(i_0_263,plain,
~ quotient(y,zero,identity),
inference(scs_inference,[],[i_0_56,i_0_25,i_0_19]) ).
cnf(i_0_275,plain,
~ quotient(xQz,zero,y),
inference(scs_inference,[],[i_0_62,i_0_25,i_0_19]) ).
cnf(i_0_287,plain,
~ quotient(x,z,y),
inference(scs_inference,[],[i_0_62,i_0_29,i_0_19]) ).
cnf(i_0_289,plain,
divide(x,z) != y,
inference(scs_inference,[],[i_0_62,i_0_22,i_0_29,i_0_19,i_0_43]) ).
cnf(i_0_90,plain,
~ quotient(divide(zero,zero),X1,xQz),
inference(scs_inference,[],[i_0_75,i_0_20]) ).
cnf(i_0_92,plain,
~ quotient(x,z,zero),
inference(scs_inference,[],[i_0_75,i_0_51,i_0_29,i_0_20,i_0_19]) ).
cnf(i_0_94,plain,
zero != x,
inference(scs_inference,[],[i_0_75,i_0_51,i_0_27,i_0_29,i_0_20,i_0_19,i_0_41]) ).
cnf(i_0_96,plain,
zero != identity,
inference(scs_inference,[],[i_0_75,i_0_51,i_0_27,i_0_80,i_0_25,i_0_29,i_0_20,i_0_19,i_0_41,i_0_42]) ).
cnf(i_0_97,plain,
~ quotient(X1,identity,xQz),
inference(rename_variables,[],[i_0_80]) ).
cnf(c_0_488,axiom,
( less_equal(X1,X2)
| ~ quotient(X3,X4,X5)
| ~ quotient(X4,X6,X7)
| ~ quotient(X3,X6,X8)
| ~ quotient(X8,X7,X1)
| ~ quotient(X5,X6,X2) ),
i_0_18 ).
cnf(c_0_489,axiom,
quotient(X1,X2,divide(X1,X2)),
i_0_22 ).
cnf(c_0_490,plain,
( less_equal(divide(X1,X2),X3)
| ~ quotient(X4,X5,X3)
| ~ quotient(X6,X5,X2)
| ~ quotient(X7,X5,X1)
| ~ quotient(X7,X6,X4) ),
inference(spm,[status(thm)],[c_0_488,c_0_489]) ).
cnf(c_0_491,plain,
quotient(xQy,z,zero),
i_0_476 ).
cnf(c_0_492,plain,
( less_equal(divide(X1,X2),zero)
| ~ quotient(X3,z,X2)
| ~ quotient(X4,z,X1)
| ~ quotient(X4,X3,xQy) ),
inference(spm,[status(thm)],[c_0_490,c_0_491]) ).
cnf(c_0_493,plain,
( less_equal(divide(X1,divide(X2,z)),zero)
| ~ quotient(X3,z,X1)
| ~ quotient(X3,X2,xQy) ),
inference(spm,[status(thm)],[c_0_492,c_0_489]) ).
cnf(c_0_494,hypothesis,
quotient(x,z,xQz),
i_0_29 ).
cnf(c_0_495,hypothesis,
( less_equal(divide(xQz,divide(X1,z)),zero)
| ~ quotient(x,X1,xQy) ),
inference(spm,[status(thm)],[c_0_493,c_0_494]) ).
cnf(c_0_496,hypothesis,
quotient(x,y,xQy),
i_0_30 ).
cnf(c_0_497,axiom,
( X1 = X2
| ~ less_equal(X1,X2)
| ~ less_equal(X2,X1) ),
i_0_31 ).
cnf(c_0_498,hypothesis,
less_equal(divide(xQz,divide(y,z)),zero),
inference(spm,[status(thm)],[c_0_495,c_0_496]) ).
cnf(c_0_499,axiom,
less_equal(zero,X1),
i_0_33 ).
cnf(c_0_500,axiom,
( less_equal(X1,X2)
| ~ quotient(X2,X3,X1) ),
i_0_20 ).
cnf(c_0_501,hypothesis,
divide(xQz,divide(y,z)) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_497,c_0_498]),c_0_499])]) ).
cnf(c_0_502,axiom,
( less_equal(X1,X2)
| ~ less_equal(X1,X3)
| ~ less_equal(X3,X2) ),
i_0_24 ).
cnf(c_0_503,plain,
less_equal(divide(X1,X2),X1),
inference(spm,[status(thm)],[c_0_500,c_0_489]) ).
cnf(c_0_504,axiom,
( less_equal(X1,X2)
| ~ quotient(X1,X2,zero) ),
i_0_21 ).
cnf(c_0_505,hypothesis,
quotient(xQz,divide(y,z),zero),
inference(spm,[status(thm)],[c_0_489,c_0_501]) ).
cnf(c_0_506,plain,
( less_equal(X1,X2)
| ~ less_equal(X1,divide(X2,X3)) ),
inference(spm,[status(thm)],[c_0_502,c_0_503]) ).
cnf(c_0_507,hypothesis,
less_equal(xQz,divide(y,z)),
inference(spm,[status(thm)],[c_0_504,c_0_505]) ).
cnf(c_0_508,negated_conjecture,
~ less_equal(xQz,y),
i_0_32 ).
cnf(c_0_509,hypothesis,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_506,c_0_507]),c_0_508]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : HEN006-2 : TPTP v9.2.1. Released v1.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n005.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Mon May 4 19:09:00 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 135.88/92.91 % Version : CSE_E---1.7
% 135.88/92.91 % Problem : theBenchmark.p
% 135.88/92.91 % SZS status Unsatisfiable for theBenchmark.p
% 135.88/92.91 % SZS output start CNFRefutation
% See solution above
% 139.28/96.35 % Total time : 92.458s
%------------------------------------------------------------------------------