%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : HEN011-1 : TPTP v9.2.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n021.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:35 PM UTC 2026
% Result : Unsatisfiable 164.74s 110.46s
% Output : CNFRefutation 165.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 24
% Syntax : Number of clauses : 367 ( 294 unt; 0 nHn; 187 RR)
% Number of literals : 495 ( 80 equ; 133 neg)
% Maximal clause size : 6 ( 1 avg)
% Maximal term depth : 5 ( 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 : 520 ( 81 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/sandbox2/benchmark/Axioms/HEN001-0.ax',quotient_property) ).
cnf(well_defined,axiom,
( X3 = X4
| ~ quotient(X1,X2,X3)
| ~ quotient(X1,X2,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',well_defined) ).
cnf(divisor_existence,axiom,
( less_equal(X3,X1)
| ~ quotient(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',divisor_existence) ).
cnf(less_equal_quotient,axiom,
( less_equal(X1,X2)
| ~ quotient(X1,X2,zero) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',less_equal_quotient) ).
cnf(closure,axiom,
quotient(X1,X2,divide(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',closure) ).
cnf(quotient_less_equal,axiom,
( quotient(X1,X2,zero)
| ~ less_equal(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',quotient_less_equal) ).
cnf(idQb_divide_idQ_idQa,hypothesis,
quotient(idQb,idQ_idQa,idQb_Q__idQ_idQa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idQb_divide_idQ_idQa) ).
cnf(idQa_divide_idQ_idQb,hypothesis,
quotient(idQa,idQ_idQb,idQa_Q__idQ_idQb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idQa_divide_idQ_idQb) ).
cnf(identity_divide_idQb,hypothesis,
quotient(identity,idQb,idQ_idQb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity_divide_idQb) ).
cnf(identity_divide_b,hypothesis,
quotient(identity,b,idQb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity_divide_b) ).
cnf(identity_divide_idQa,hypothesis,
quotient(identity,idQa,idQ_idQa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity_divide_idQa) ).
cnf(identity_divide_a,hypothesis,
quotient(identity,a,idQa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity_divide_a) ).
cnf(less_equal_and_equal,axiom,
( X1 = X2
| ~ less_equal(X1,X2)
| ~ less_equal(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',less_equal_and_equal) ).
cnf(zero_is_smallest,axiom,
less_equal(zero,X1),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',zero_is_smallest) ).
cnf(identity_is_largest,axiom,
less_equal(X1,identity),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',identity_is_largest) ).
cnf(prove_idQa_Q__idQ_idQb_equals_idQb_Q__idQ_idQa,negated_conjecture,
idQa_Q__idQ_idQb != idQb_Q__idQ_idQa,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_idQa_Q__idQ_idQb_equals_idQb_Q__idQ_idQa) ).
cnf(i_0_16,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_17,axiom,
( X3 = X4
| ~ quotient(X1,X2,X3)
| ~ quotient(X1,X2,X4) ),
well_defined,
[final] ).
cnf(i_0_18,axiom,
( less_equal(X3,X1)
| ~ quotient(X1,X2,X3) ),
divisor_existence,
[final] ).
cnf(i_0_19,axiom,
( less_equal(X1,X2)
| ~ quotient(X1,X2,zero) ),
less_equal_quotient,
[final] ).
cnf(i_0_20,axiom,
quotient(X1,X2,divide(X1,X2)),
closure,
[final] ).
cnf(i_0_21,axiom,
( quotient(X1,X2,zero)
| ~ less_equal(X1,X2) ),
quotient_less_equal,
[final] ).
cnf(i_0_22,hypothesis,
quotient(idQb,idQ_idQa,idQb_Q__idQ_idQa),
idQb_divide_idQ_idQa,
[final] ).
cnf(i_0_23,hypothesis,
quotient(idQa,idQ_idQb,idQa_Q__idQ_idQb),
idQa_divide_idQ_idQb,
[final] ).
cnf(i_0_24,hypothesis,
quotient(identity,idQb,idQ_idQb),
identity_divide_idQb,
[final] ).
cnf(i_0_25,hypothesis,
quotient(identity,b,idQb),
identity_divide_b,
[final] ).
cnf(i_0_26,hypothesis,
quotient(identity,idQa,idQ_idQa),
identity_divide_idQa,
[final] ).
cnf(i_0_27,hypothesis,
quotient(identity,a,idQa),
identity_divide_a,
[final] ).
cnf(i_0_28,axiom,
( X1 = X2
| ~ less_equal(X1,X2)
| ~ less_equal(X2,X1) ),
less_equal_and_equal,
[final] ).
cnf(i_0_29,axiom,
less_equal(zero,X1),
zero_is_smallest,
[final] ).
cnf(i_0_30,axiom,
less_equal(X1,identity),
identity_is_largest,
[final] ).
cnf(i_0_31,negated_conjecture,
idQa_Q__idQ_idQb != idQb_Q__idQ_idQa,
prove_idQa_Q__idQ_idQb_equals_idQb_Q__idQ_idQa,
[final] ).
cnf(i_0_32,axiom,
X1 = X1 ).
cnf(i_0_33,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_34,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_35,axiom,
( X1 != X2
| ~ less_equal(X1,X3)
| less_equal(X2,X3) ) ).
cnf(i_0_36,axiom,
( X1 != X2
| ~ less_equal(X3,X1)
| less_equal(X3,X2) ) ).
cnf(i_0_37,axiom,
( X1 != X2
| ~ quotient(X1,X3,X4)
| quotient(X2,X3,X4) ) ).
cnf(i_0_38,axiom,
( X1 != X2
| ~ quotient(X3,X1,X4)
| quotient(X3,X2,X4) ) ).
cnf(i_0_39,axiom,
( X1 != X2
| ~ quotient(X3,X4,X1)
| quotient(X3,X4,X2) ) ).
cnf(i_0_40,plain,
~ quotient(idQb,idQ_idQa,idQa_Q__idQ_idQb),
inference(scs_inference,[],[i_0_31,i_0_22,i_0_17]) ).
cnf(i_0_42,plain,
divide(idQb,idQ_idQa) != idQa_Q__idQ_idQb,
inference(scs_inference,[],[i_0_31,i_0_20,i_0_22,i_0_17,i_0_39]) ).
cnf(i_0_43,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_46,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_47,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_51,plain,
idQ_idQb = divide(identity,idQb),
inference(scs_inference,[],[i_0_24,i_0_20,i_0_17]) ).
cnf(i_0_52,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_54,plain,
divide(identity,idQb) = idQ_idQb,
inference(scs_inference,[],[i_0_24,i_0_20,i_0_17,i_0_33]) ).
cnf(i_0_57,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_71,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_77,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_95,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_101,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_209,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_211,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_212,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_215,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_217,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_218,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_555,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_557,plain,
less_equal(X1,identity),
inference(rename_variables,[],[i_0_30]) ).
cnf(i_0_558,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_559,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_673,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_675,plain,
less_equal(zero,X1),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_676,plain,
less_equal(X1,identity),
inference(rename_variables,[],[i_0_30]) ).
cnf(i_0_677,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_791,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_793,plain,
less_equal(zero,X1),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_794,plain,
less_equal(X1,identity),
inference(rename_variables,[],[i_0_30]) ).
cnf(i_0_795,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_909,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_911,plain,
less_equal(zero,X1),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_912,plain,
less_equal(X1,identity),
inference(rename_variables,[],[i_0_30]) ).
cnf(i_0_913,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_2707,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_2710,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_2713,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_2714,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_2715,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_2721,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_2722,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_2723,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_10599,plain,
less_equal(divide(X1,X2),X1),
inference(scs_inference,[],[i_0_20,i_0_18]) ).
cnf(i_0_10601,plain,
quotient(zero,X1,zero),
inference(scs_inference,[],[i_0_29,i_0_20,i_0_18,i_0_21]) ).
cnf(i_0_10603,plain,
zero = divide(zero,X1),
inference(scs_inference,[],[i_0_29,i_0_20,i_0_18,i_0_21,i_0_28]) ).
cnf(i_0_10604,plain,
less_equal(zero,X1),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_10608,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_10610,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_10615,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_10649,plain,
less_equal(zero,X1),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_10689,plain,
quotient(X1,identity,zero),
inference(scs_inference,[],[i_0_30,i_0_21]) ).
cnf(i_0_10718,plain,
less_equal(X1,identity),
inference(rename_variables,[],[i_0_30]) ).
cnf(i_0_10752,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_10762,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_10782,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_10833,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_10844,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_10861,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_10876,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_10900,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_10902,plain,
less_equal(X1,identity),
inference(rename_variables,[],[i_0_30]) ).
cnf(i_0_10954,plain,
less_equal(X1,identity),
inference(rename_variables,[],[i_0_30]) ).
cnf(i_0_10960,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11003,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11007,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11021,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11037,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11051,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11055,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11076,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11080,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11102,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11107,plain,
less_equal(X1,identity),
inference(rename_variables,[],[i_0_30]) ).
cnf(i_0_11113,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11120,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11149,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11168,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11174,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11178,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11190,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11192,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11195,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11197,plain,
less_equal(zero,X1),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_11205,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11207,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11209,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11211,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11220,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11223,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11232,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11237,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11243,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11253,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11260,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11266,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11270,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11280,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11311,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11315,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11322,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11330,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11346,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11350,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11357,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11364,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11374,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11383,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11394,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11399,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11424,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_11429,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_20]) ).
cnf(c_0_10708,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_16 ).
cnf(c_0_10709,axiom,
quotient(X1,X2,divide(X1,X2)),
i_0_20 ).
cnf(c_0_10710,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_10708,c_0_10709]) ).
cnf(c_0_10711,plain,
quotient(zero,X1,zero),
i_0_10601 ).
cnf(c_0_10712,plain,
( less_equal(divide(X1,X2),zero)
| ~ quotient(X3,X4,zero)
| ~ quotient(X4,X5,X2)
| ~ quotient(X3,X5,X1) ),
inference(spm,[status(thm)],[c_0_10710,c_0_10711]) ).
cnf(c_0_10713,hypothesis,
quotient(identity,b,idQb),
i_0_25 ).
cnf(c_0_10714,plain,
quotient(X1,identity,zero),
i_0_10689 ).
cnf(c_0_10715,axiom,
( quotient(X1,X2,zero)
| ~ less_equal(X1,X2) ),
i_0_21 ).
cnf(c_0_10716,plain,
less_equal(divide(X1,X2),X1),
i_0_10599 ).
cnf(c_0_10717,hypothesis,
( less_equal(divide(X1,idQb),zero)
| ~ quotient(X2,b,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10712,c_0_10713]),c_0_10714])]) ).
cnf(c_0_10718,plain,
quotient(divide(X1,X2),X1,zero),
inference(spm,[status(thm)],[c_0_10715,c_0_10716]) ).
cnf(c_0_10719,axiom,
( X1 = X2
| ~ less_equal(X1,X2)
| ~ less_equal(X2,X1) ),
i_0_28 ).
cnf(c_0_10720,hypothesis,
less_equal(divide(idQb,idQb),zero),
inference(spm,[status(thm)],[c_0_10717,c_0_10713]) ).
cnf(c_0_10721,axiom,
less_equal(zero,X1),
i_0_29 ).
cnf(c_0_10722,plain,
( less_equal(divide(X1,X2),zero)
| ~ quotient(X3,X4,divide(X5,X6))
| ~ quotient(X4,X5,X2)
| ~ quotient(X3,X5,X1) ),
inference(spm,[status(thm)],[c_0_10710,c_0_10718]) ).
cnf(c_0_10723,hypothesis,
divide(idQb,idQb) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10720]),c_0_10721])]) ).
cnf(c_0_10724,plain,
( less_equal(divide(X1,zero),zero)
| ~ quotient(X2,zero,divide(X3,X4))
| ~ quotient(X2,X3,X1) ),
inference(spm,[status(thm)],[c_0_10722,c_0_10711]) ).
cnf(c_0_10725,hypothesis,
quotient(idQb,idQb,zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10723]) ).
cnf(c_0_10726,plain,
( less_equal(divide(divide(X1,X2),zero),zero)
| ~ quotient(X1,zero,divide(X2,X3)) ),
inference(spm,[status(thm)],[c_0_10724,c_0_10709]) ).
cnf(c_0_10727,hypothesis,
( less_equal(divide(X1,X2),zero)
| ~ quotient(X3,idQb,X2)
| ~ quotient(X4,idQb,X1)
| ~ quotient(X4,X3,idQb) ),
inference(spm,[status(thm)],[c_0_10710,c_0_10725]) ).
cnf(c_0_10728,hypothesis,
quotient(identity,idQa,idQ_idQa),
i_0_26 ).
cnf(c_0_10729,plain,
less_equal(divide(divide(X1,X1),zero),zero),
inference(spm,[status(thm)],[c_0_10726,c_0_10709]) ).
cnf(c_0_10730,hypothesis,
( less_equal(divide(X1,divide(X2,idQb)),zero)
| ~ quotient(X3,idQb,X1)
| ~ quotient(X3,X2,idQb) ),
inference(spm,[status(thm)],[c_0_10727,c_0_10709]) ).
cnf(c_0_10731,hypothesis,
quotient(identity,idQb,idQ_idQb),
i_0_24 ).
cnf(c_0_10732,hypothesis,
( less_equal(divide(X1,idQ_idQa),zero)
| ~ quotient(X2,idQa,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10712,c_0_10728]),c_0_10714])]) ).
cnf(c_0_10733,plain,
( less_equal(divide(X1,X2),divide(X3,X4))
| ~ quotient(X5,X4,X2)
| ~ quotient(X6,X4,X1)
| ~ quotient(X6,X5,X3) ),
inference(spm,[status(thm)],[c_0_10710,c_0_10709]) ).
cnf(c_0_10734,plain,
divide(divide(X1,X1),zero) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10729]),c_0_10721])]) ).
cnf(c_0_10735,hypothesis,
( less_equal(divide(idQ_idQb,divide(X1,idQb)),zero)
| ~ quotient(identity,X1,idQb) ),
inference(spm,[status(thm)],[c_0_10730,c_0_10731]) ).
cnf(c_0_10736,hypothesis,
( less_equal(divide(X1,idQ_idQb),zero)
| ~ quotient(X2,idQb,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10712,c_0_10731]),c_0_10714])]) ).
cnf(c_0_10737,hypothesis,
less_equal(divide(idQ_idQa,idQ_idQa),zero),
inference(spm,[status(thm)],[c_0_10732,c_0_10728]) ).
cnf(c_0_10738,plain,
( less_equal(divide(X1,zero),divide(X2,X3))
| ~ quotient(X4,zero,X2)
| ~ quotient(X4,X3,X1) ),
inference(spm,[status(thm)],[c_0_10733,c_0_10711]) ).
cnf(c_0_10739,axiom,
( less_equal(X1,X2)
| ~ quotient(X1,X2,zero) ),
i_0_19 ).
cnf(c_0_10740,plain,
quotient(divide(X1,X1),zero,zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10734]) ).
cnf(c_0_10741,hypothesis,
less_equal(divide(idQ_idQb,divide(b,idQb)),zero),
inference(spm,[status(thm)],[c_0_10735,c_0_10713]) ).
cnf(c_0_10742,hypothesis,
less_equal(divide(divide(X1,idQb),idQ_idQb),zero),
inference(spm,[status(thm)],[c_0_10736,c_0_10709]) ).
cnf(c_0_10743,hypothesis,
divide(idQ_idQa,idQ_idQa) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10737]),c_0_10721])]) ).
cnf(c_0_10744,plain,
( less_equal(divide(divide(X1,X2),zero),divide(X3,X2))
| ~ quotient(X1,zero,X3) ),
inference(spm,[status(thm)],[c_0_10738,c_0_10709]) ).
cnf(c_0_10745,plain,
less_equal(divide(X1,X1),zero),
inference(spm,[status(thm)],[c_0_10739,c_0_10740]) ).
cnf(c_0_10746,hypothesis,
divide(idQ_idQb,divide(b,idQb)) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10741]),c_0_10721])]) ).
cnf(c_0_10747,hypothesis,
divide(divide(X1,idQb),idQ_idQb) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10742]),c_0_10721])]) ).
cnf(c_0_10748,hypothesis,
quotient(identity,a,idQa),
i_0_27 ).
cnf(c_0_10749,hypothesis,
quotient(idQ_idQa,idQ_idQa,zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10743]) ).
cnf(c_0_10750,plain,
less_equal(divide(divide(X1,X2),zero),divide(divide(X1,zero),X2)),
inference(spm,[status(thm)],[c_0_10744,c_0_10709]) ).
cnf(c_0_10751,plain,
divide(X1,X1) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10745]),c_0_10721])]) ).
cnf(c_0_10752,axiom,
( X1 = X2
| ~ quotient(X3,X4,X1)
| ~ quotient(X3,X4,X2) ),
i_0_17 ).
cnf(c_0_10753,hypothesis,
quotient(idQ_idQb,divide(b,idQb),zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10746]) ).
cnf(c_0_10754,hypothesis,
quotient(divide(X1,idQb),idQ_idQb,zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10747]) ).
cnf(c_0_10755,plain,
( less_equal(divide(X1,divide(X2,X3)),zero)
| ~ quotient(X4,X2,zero)
| ~ quotient(X4,X3,X1) ),
inference(spm,[status(thm)],[c_0_10712,c_0_10709]) ).
cnf(c_0_10756,hypothesis,
quotient(idQb,idQ_idQa,idQb_Q__idQ_idQa),
i_0_22 ).
cnf(c_0_10757,hypothesis,
( less_equal(divide(X1,idQa),zero)
| ~ quotient(X2,a,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10712,c_0_10748]),c_0_10714])]) ).
cnf(c_0_10758,hypothesis,
( less_equal(divide(X1,X2),zero)
| ~ quotient(X3,idQ_idQa,X2)
| ~ quotient(X4,idQ_idQa,X1)
| ~ quotient(X4,X3,idQ_idQa) ),
inference(spm,[status(thm)],[c_0_10710,c_0_10749]) ).
cnf(c_0_10759,plain,
less_equal(divide(divide(X1,divide(X1,zero)),zero),zero),
inference(spm,[status(thm)],[c_0_10750,c_0_10751]) ).
cnf(c_0_10760,plain,
( less_equal(divide(X1,divide(X2,X3)),divide(X4,X3))
| ~ quotient(X5,X3,X1)
| ~ quotient(X5,X2,X4) ),
inference(spm,[status(thm)],[c_0_10733,c_0_10709]) ).
cnf(c_0_10761,plain,
( X1 = divide(X2,X3)
| ~ quotient(X2,X3,X1) ),
inference(spm,[status(thm)],[c_0_10752,c_0_10709]) ).
cnf(c_0_10762,hypothesis,
less_equal(idQ_idQb,divide(b,idQb)),
inference(spm,[status(thm)],[c_0_10739,c_0_10753]) ).
cnf(c_0_10763,hypothesis,
less_equal(divide(X1,idQb),idQ_idQb),
inference(spm,[status(thm)],[c_0_10739,c_0_10754]) ).
cnf(c_0_10764,hypothesis,
( less_equal(divide(idQb_Q__idQ_idQa,divide(X1,idQ_idQa)),zero)
| ~ quotient(idQb,X1,zero) ),
inference(spm,[status(thm)],[c_0_10755,c_0_10756]) ).
cnf(c_0_10765,hypothesis,
less_equal(divide(idQa,idQa),zero),
inference(spm,[status(thm)],[c_0_10757,c_0_10748]) ).
cnf(c_0_10766,hypothesis,
( less_equal(divide(X1,divide(X2,idQ_idQa)),zero)
| ~ quotient(X3,idQ_idQa,X1)
| ~ quotient(X3,X2,idQ_idQa) ),
inference(spm,[status(thm)],[c_0_10758,c_0_10709]) ).
cnf(c_0_10767,plain,
divide(divide(X1,divide(X1,zero)),zero) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10759]),c_0_10721])]) ).
cnf(c_0_10768,hypothesis,
( less_equal(divide(idQb,divide(X1,b)),divide(X2,b))
| ~ quotient(identity,X1,X2) ),
inference(spm,[status(thm)],[c_0_10760,c_0_10713]) ).
cnf(c_0_10769,plain,
divide(divide(X1,X2),X1) = zero,
inference(spm,[status(thm)],[c_0_10761,c_0_10718]) ).
cnf(c_0_10770,hypothesis,
divide(b,idQb) = idQ_idQb,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10762]),c_0_10763])]) ).
cnf(c_0_10771,plain,
less_equal(divide(idQb_Q__idQ_idQa,divide(identity,idQ_idQa)),zero),
inference(spm,[status(thm)],[c_0_10764,c_0_10714]) ).
cnf(c_0_10772,hypothesis,
divide(idQa,idQa) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10765]),c_0_10721])]) ).
cnf(c_0_10773,hypothesis,
( less_equal(divide(divide(X1,idQ_idQa),divide(X2,idQ_idQa)),zero)
| ~ quotient(X1,X2,idQ_idQa) ),
inference(spm,[status(thm)],[c_0_10766,c_0_10709]) ).
cnf(c_0_10774,plain,
( less_equal(divide(divide(X1,X2),divide(X3,X2)),zero)
| ~ quotient(X1,X3,zero) ),
inference(spm,[status(thm)],[c_0_10755,c_0_10709]) ).
cnf(c_0_10775,plain,
quotient(divide(X1,divide(X1,zero)),zero,zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10767]) ).
cnf(c_0_10776,hypothesis,
less_equal(divide(idQb,divide(idQb,b)),divide(idQ_idQb,b)),
inference(spm,[status(thm)],[c_0_10768,c_0_10731]) ).
cnf(c_0_10777,plain,
divide(idQ_idQb,b) = zero,
inference(spm,[status(thm)],[c_0_10769,c_0_10770]) ).
cnf(c_0_10778,plain,
divide(idQb_Q__idQ_idQa,divide(identity,idQ_idQa)) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10771]),c_0_10721])]) ).
cnf(c_0_10779,hypothesis,
quotient(idQa,idQa,zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10772]) ).
cnf(c_0_10780,hypothesis,
less_equal(divide(divide(identity,idQ_idQa),divide(idQa,idQ_idQa)),zero),
inference(spm,[status(thm)],[c_0_10773,c_0_10728]) ).
cnf(c_0_10781,plain,
less_equal(divide(divide(X1,X2),divide(identity,X2)),zero),
inference(spm,[status(thm)],[c_0_10774,c_0_10714]) ).
cnf(c_0_10782,plain,
less_equal(divide(X1,divide(X1,zero)),zero),
inference(spm,[status(thm)],[c_0_10739,c_0_10775]) ).
cnf(c_0_10783,hypothesis,
less_equal(divide(idQb,divide(idQb,b)),zero),
inference(rw,[status(thm)],[c_0_10776,c_0_10777]) ).
cnf(c_0_10784,hypothesis,
less_equal(divide(divide(X1,b),idQb),zero),
inference(spm,[status(thm)],[c_0_10717,c_0_10709]) ).
cnf(c_0_10785,plain,
less_equal(divide(divide(divide(X1,X2),X3),divide(X1,X3)),zero),
inference(spm,[status(thm)],[c_0_10774,c_0_10718]) ).
cnf(c_0_10786,plain,
quotient(idQb_Q__idQ_idQa,divide(identity,idQ_idQa),zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10778]) ).
cnf(c_0_10787,hypothesis,
( less_equal(divide(X1,X2),zero)
| ~ quotient(X3,idQa,X2)
| ~ quotient(X4,idQa,X1)
| ~ quotient(X4,X3,idQa) ),
inference(spm,[status(thm)],[c_0_10710,c_0_10779]) ).
cnf(c_0_10788,hypothesis,
divide(divide(identity,idQ_idQa),divide(idQa,idQ_idQa)) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10780]),c_0_10721])]) ).
cnf(c_0_10789,plain,
divide(divide(X1,X2),divide(identity,X2)) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10781]),c_0_10721])]) ).
cnf(c_0_10790,plain,
divide(X1,divide(X1,zero)) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10782]),c_0_10721])]) ).
cnf(c_0_10791,hypothesis,
divide(idQb,divide(idQb,b)) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10783]),c_0_10721])]) ).
cnf(c_0_10792,hypothesis,
divide(divide(X1,b),idQb) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10784]),c_0_10721])]) ).
cnf(c_0_10793,plain,
divide(divide(divide(X1,X2),X3),divide(X1,X3)) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10785]),c_0_10721])]) ).
cnf(c_0_10794,plain,
less_equal(divide(divide(idQb_Q__idQ_idQa,X1),divide(divide(identity,idQ_idQa),X1)),zero),
inference(spm,[status(thm)],[c_0_10774,c_0_10786]) ).
cnf(c_0_10795,hypothesis,
( less_equal(divide(X1,divide(X2,idQa)),zero)
| ~ quotient(X3,idQa,X1)
| ~ quotient(X3,X2,idQa) ),
inference(spm,[status(thm)],[c_0_10787,c_0_10709]) ).
cnf(c_0_10796,hypothesis,
quotient(divide(identity,idQ_idQa),divide(idQa,idQ_idQa),zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10788]) ).
cnf(c_0_10797,plain,
quotient(divide(X1,X2),divide(identity,X2),zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10789]) ).
cnf(c_0_10798,plain,
quotient(X1,divide(X1,zero),zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10790]) ).
cnf(c_0_10799,hypothesis,
quotient(idQb,divide(idQb,b),zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10791]) ).
cnf(c_0_10800,hypothesis,
quotient(divide(X1,b),idQb,zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10792]) ).
cnf(c_0_10801,plain,
quotient(divide(divide(X1,X2),X3),divide(X1,X3),zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10793]) ).
cnf(c_0_10802,plain,
divide(divide(idQb_Q__idQ_idQa,X1),divide(divide(identity,idQ_idQa),X1)) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10794]),c_0_10721])]) ).
cnf(c_0_10803,hypothesis,
( less_equal(divide(idQ_idQa,divide(X1,idQa)),zero)
| ~ quotient(identity,X1,idQa) ),
inference(spm,[status(thm)],[c_0_10795,c_0_10728]) ).
cnf(c_0_10804,hypothesis,
less_equal(divide(identity,idQ_idQa),divide(idQa,idQ_idQa)),
inference(spm,[status(thm)],[c_0_10739,c_0_10796]) ).
cnf(c_0_10805,plain,
less_equal(divide(X1,X2),divide(identity,X2)),
inference(spm,[status(thm)],[c_0_10739,c_0_10797]) ).
cnf(c_0_10806,plain,
quotient(idQ_idQb,b,zero),
inference(spm,[status(thm)],[c_0_10718,c_0_10770]) ).
cnf(c_0_10807,plain,
less_equal(X1,divide(X1,zero)),
inference(spm,[status(thm)],[c_0_10739,c_0_10798]) ).
cnf(c_0_10808,hypothesis,
less_equal(idQb,divide(idQb,b)),
inference(spm,[status(thm)],[c_0_10739,c_0_10799]) ).
cnf(c_0_10809,hypothesis,
less_equal(divide(X1,b),idQb),
inference(spm,[status(thm)],[c_0_10739,c_0_10800]) ).
cnf(c_0_10810,plain,
less_equal(divide(divide(X1,X2),X3),divide(X1,X3)),
inference(spm,[status(thm)],[c_0_10739,c_0_10801]) ).
cnf(c_0_10811,plain,
quotient(divide(idQb_Q__idQ_idQa,X1),divide(divide(identity,idQ_idQa),X1),zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10802]) ).
cnf(c_0_10812,hypothesis,
less_equal(divide(idQ_idQa,divide(a,idQa)),zero),
inference(spm,[status(thm)],[c_0_10803,c_0_10748]) ).
cnf(c_0_10813,hypothesis,
less_equal(divide(divide(X1,idQa),idQ_idQa),zero),
inference(spm,[status(thm)],[c_0_10732,c_0_10709]) ).
cnf(c_0_10814,hypothesis,
divide(idQa,idQ_idQa) = divide(identity,idQ_idQa),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10804]),c_0_10805])]) ).
cnf(c_0_10815,hypothesis,
less_equal(divide(idQ_idQb,idQ_idQb),zero),
inference(spm,[status(thm)],[c_0_10736,c_0_10731]) ).
cnf(c_0_10816,plain,
( less_equal(divide(X1,zero),divide(X2,b))
| ~ quotient(X3,b,X1)
| ~ quotient(X3,idQ_idQb,X2) ),
inference(spm,[status(thm)],[c_0_10733,c_0_10806]) ).
cnf(c_0_10817,plain,
divide(X1,zero) = X1,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10807]),c_0_10716])]) ).
cnf(c_0_10818,hypothesis,
divide(idQb,b) = idQb,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10808]),c_0_10809])]) ).
cnf(c_0_10819,plain,
less_equal(divide(divide(divide(X1,X2),X3),X1),zero),
inference(spm,[status(thm)],[c_0_10810,c_0_10769]) ).
cnf(c_0_10820,plain,
less_equal(divide(idQb_Q__idQ_idQa,X1),divide(divide(identity,idQ_idQa),X1)),
inference(spm,[status(thm)],[c_0_10739,c_0_10811]) ).
cnf(c_0_10821,hypothesis,
divide(idQ_idQa,divide(a,idQa)) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10812]),c_0_10721])]) ).
cnf(c_0_10822,hypothesis,
divide(divide(X1,idQa),idQ_idQa) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10813]),c_0_10721])]) ).
cnf(c_0_10823,plain,
less_equal(divide(divide(divide(X1,X2),X3),divide(divide(identity,X2),X3)),zero),
inference(spm,[status(thm)],[c_0_10774,c_0_10797]) ).
cnf(c_0_10824,plain,
divide(divide(identity,idQ_idQa),idQa) = zero,
inference(spm,[status(thm)],[c_0_10769,c_0_10814]) ).
cnf(c_0_10825,hypothesis,
divide(idQ_idQb,idQ_idQb) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10815]),c_0_10721])]) ).
cnf(c_0_10826,plain,
( less_equal(X1,divide(X2,b))
| ~ quotient(X3,b,X1)
| ~ quotient(X3,idQ_idQb,X2) ),
inference(rw,[status(thm)],[c_0_10816,c_0_10817]) ).
cnf(c_0_10827,hypothesis,
quotient(idQb,b,idQb),
inference(spm,[status(thm)],[c_0_10709,c_0_10818]) ).
cnf(c_0_10828,plain,
divide(divide(divide(X1,X2),X3),X1) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10819]),c_0_10721])]) ).
cnf(c_0_10829,plain,
less_equal(divide(idQb_Q__idQ_idQa,divide(idQa,idQ_idQa)),zero),
inference(spm,[status(thm)],[c_0_10820,c_0_10788]) ).
cnf(c_0_10830,hypothesis,
quotient(idQ_idQa,divide(a,idQa),zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10821]) ).
cnf(c_0_10831,hypothesis,
quotient(divide(X1,idQa),idQ_idQa,zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10822]) ).
cnf(c_0_10832,plain,
less_equal(divide(divide(divide(X1,idQ_idQa),idQa),zero),zero),
inference(spm,[status(thm)],[c_0_10823,c_0_10824]) ).
cnf(c_0_10833,hypothesis,
quotient(idQ_idQb,idQ_idQb,zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10825]) ).
cnf(c_0_10834,hypothesis,
( less_equal(idQb,divide(X1,b))
| ~ quotient(idQb,idQ_idQb,X1) ),
inference(spm,[status(thm)],[c_0_10826,c_0_10827]) ).
cnf(c_0_10835,plain,
quotient(divide(divide(X1,X2),X3),X1,zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10828]) ).
cnf(c_0_10836,plain,
( less_equal(divide(X1,zero),zero)
| ~ quotient(X2,divide(X3,X4),zero)
| ~ quotient(X2,X3,X1) ),
inference(spm,[status(thm)],[c_0_10712,c_0_10718]) ).
cnf(c_0_10837,plain,
divide(idQb_Q__idQ_idQa,divide(idQa,idQ_idQa)) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10829]),c_0_10721])]) ).
cnf(c_0_10838,hypothesis,
( less_equal(divide(X1,idQb_Q__idQ_idQa),divide(X2,idQ_idQa))
| ~ quotient(X3,idQ_idQa,X1)
| ~ quotient(X3,idQb,X2) ),
inference(spm,[status(thm)],[c_0_10733,c_0_10756]) ).
cnf(c_0_10839,plain,
( less_equal(divide(X1,zero),divide(X2,X3))
| ~ quotient(X4,divide(X3,X5),X2)
| ~ quotient(X4,X3,X1) ),
inference(spm,[status(thm)],[c_0_10733,c_0_10718]) ).
cnf(c_0_10840,hypothesis,
less_equal(idQ_idQa,divide(a,idQa)),
inference(spm,[status(thm)],[c_0_10739,c_0_10830]) ).
cnf(c_0_10841,hypothesis,
less_equal(divide(X1,idQa),idQ_idQa),
inference(spm,[status(thm)],[c_0_10739,c_0_10831]) ).
cnf(c_0_10842,plain,
divide(divide(divide(X1,idQ_idQa),idQa),zero) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10832]),c_0_10721])]) ).
cnf(c_0_10843,hypothesis,
quotient(idQa,idQ_idQb,idQa_Q__idQ_idQb),
i_0_23 ).
cnf(c_0_10844,hypothesis,
( less_equal(divide(X1,X2),zero)
| ~ quotient(X3,idQ_idQb,X2)
| ~ quotient(X4,idQ_idQb,X1)
| ~ quotient(X4,X3,idQ_idQb) ),
inference(spm,[status(thm)],[c_0_10710,c_0_10833]) ).
cnf(c_0_10845,hypothesis,
less_equal(idQb,divide(divide(idQb,idQ_idQb),b)),
inference(spm,[status(thm)],[c_0_10834,c_0_10709]) ).
cnf(c_0_10846,plain,
less_equal(divide(divide(X1,X2),X3),X1),
inference(spm,[status(thm)],[c_0_10739,c_0_10835]) ).
cnf(c_0_10847,plain,
( less_equal(divide(divide(X1,X2),zero),zero)
| ~ quotient(X1,divide(X2,X3),zero) ),
inference(spm,[status(thm)],[c_0_10836,c_0_10709]) ).
cnf(c_0_10848,plain,
quotient(idQb_Q__idQ_idQa,divide(idQa,idQ_idQa),zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10837]) ).
cnf(c_0_10849,hypothesis,
( less_equal(divide(divide(X1,idQ_idQa),idQb_Q__idQ_idQa),divide(X2,idQ_idQa))
| ~ quotient(X1,idQb,X2) ),
inference(spm,[status(thm)],[c_0_10838,c_0_10709]) ).
cnf(c_0_10850,hypothesis,
( less_equal(divide(idQa,zero),divide(X1,a))
| ~ quotient(identity,divide(a,X2),X1) ),
inference(spm,[status(thm)],[c_0_10839,c_0_10748]) ).
cnf(c_0_10851,hypothesis,
divide(a,idQa) = idQ_idQa,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10840]),c_0_10841])]) ).
cnf(c_0_10852,plain,
quotient(divide(divide(X1,idQ_idQa),idQa),zero,zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10842]) ).
cnf(c_0_10853,hypothesis,
( less_equal(divide(X1,idQa_Q__idQ_idQb),divide(X2,idQ_idQb))
| ~ quotient(X3,idQ_idQb,X1)
| ~ quotient(X3,idQa,X2) ),
inference(spm,[status(thm)],[c_0_10733,c_0_10843]) ).
cnf(c_0_10854,hypothesis,
( less_equal(divide(idQb,zero),divide(X1,b))
| ~ quotient(identity,divide(b,X2),X1) ),
inference(spm,[status(thm)],[c_0_10839,c_0_10713]) ).
cnf(c_0_10855,hypothesis,
( less_equal(divide(X1,divide(X2,idQ_idQb)),zero)
| ~ quotient(X3,idQ_idQb,X1)
| ~ quotient(X3,X2,idQ_idQb) ),
inference(spm,[status(thm)],[c_0_10844,c_0_10709]) ).
cnf(c_0_10856,plain,
( divide(X1,X2) = X1
| ~ less_equal(X1,divide(X1,X2)) ),
inference(spm,[status(thm)],[c_0_10719,c_0_10716]) ).
cnf(c_0_10857,hypothesis,
divide(divide(idQb,idQ_idQb),b) = idQb,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10845]),c_0_10846])]) ).
cnf(c_0_10858,plain,
less_equal(divide(divide(idQb_Q__idQ_idQa,idQa),zero),zero),
inference(spm,[status(thm)],[c_0_10847,c_0_10848]) ).
cnf(c_0_10859,hypothesis,
less_equal(divide(divide(identity,idQ_idQa),idQb_Q__idQ_idQa),divide(idQ_idQb,idQ_idQa)),
inference(spm,[status(thm)],[c_0_10849,c_0_10731]) ).
cnf(c_0_10860,hypothesis,
( less_equal(divide(idQa,zero),divide(X1,a))
| ~ quotient(identity,idQ_idQa,X1) ),
inference(spm,[status(thm)],[c_0_10850,c_0_10851]) ).
cnf(c_0_10861,plain,
less_equal(divide(divide(X1,idQ_idQa),idQa),zero),
inference(spm,[status(thm)],[c_0_10739,c_0_10852]) ).
cnf(c_0_10862,hypothesis,
( less_equal(divide(divide(X1,idQ_idQb),idQa_Q__idQ_idQb),divide(X2,idQ_idQb))
| ~ quotient(X1,idQa,X2) ),
inference(spm,[status(thm)],[c_0_10853,c_0_10709]) ).
cnf(c_0_10863,hypothesis,
( less_equal(divide(idQb,zero),divide(X1,b))
| ~ quotient(identity,idQ_idQb,X1) ),
inference(spm,[status(thm)],[c_0_10854,c_0_10770]) ).
cnf(c_0_10864,hypothesis,
( less_equal(divide(divide(X1,idQ_idQb),divide(X2,idQ_idQb)),zero)
| ~ quotient(X1,X2,idQ_idQb) ),
inference(spm,[status(thm)],[c_0_10855,c_0_10709]) ).
cnf(c_0_10865,plain,
divide(idQb,idQ_idQb) = idQb,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10856,c_0_10857]),c_0_10716])]) ).
cnf(c_0_10866,plain,
divide(divide(idQb_Q__idQ_idQa,idQa),zero) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10858]),c_0_10721])]) ).
cnf(c_0_10867,hypothesis,
quotient(divide(divide(identity,idQ_idQa),idQb_Q__idQ_idQa),divide(idQ_idQb,idQ_idQa),zero),
inference(spm,[status(thm)],[c_0_10715,c_0_10859]) ).
cnf(c_0_10868,hypothesis,
less_equal(divide(idQa,zero),divide(divide(identity,idQ_idQa),a)),
inference(spm,[status(thm)],[c_0_10860,c_0_10709]) ).
cnf(c_0_10869,plain,
divide(divide(X1,idQ_idQa),idQa) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10861]),c_0_10721])]) ).
cnf(c_0_10870,hypothesis,
less_equal(divide(divide(identity,idQ_idQb),idQa_Q__idQ_idQb),divide(idQ_idQa,idQ_idQb)),
inference(spm,[status(thm)],[c_0_10862,c_0_10728]) ).
cnf(c_0_10871,hypothesis,
less_equal(divide(idQb,zero),divide(divide(identity,idQ_idQb),b)),
inference(spm,[status(thm)],[c_0_10863,c_0_10709]) ).
cnf(c_0_10872,hypothesis,
less_equal(divide(divide(identity,idQ_idQb),idQb),zero),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10864,c_0_10731]),c_0_10865]) ).
cnf(c_0_10873,plain,
quotient(divide(idQb_Q__idQ_idQa,idQa),zero,zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10866]) ).
cnf(c_0_10874,hypothesis,
less_equal(divide(divide(divide(divide(identity,idQ_idQa),idQb_Q__idQ_idQa),idQ_idQb),zero),zero),
inference(spm,[status(thm)],[c_0_10847,c_0_10867]) ).
cnf(c_0_10875,hypothesis,
less_equal(idQa,divide(divide(identity,idQ_idQa),a)),
inference(rw,[status(thm)],[c_0_10868,c_0_10817]) ).
cnf(c_0_10876,plain,
less_equal(divide(divide(identity,idQ_idQa),X1),idQa),
inference(spm,[status(thm)],[c_0_10846,c_0_10814]) ).
cnf(c_0_10877,plain,
quotient(divide(X1,idQ_idQa),idQa,zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10869]) ).
cnf(c_0_10878,hypothesis,
quotient(divide(divide(identity,idQ_idQb),idQa_Q__idQ_idQb),divide(idQ_idQa,idQ_idQb),zero),
inference(spm,[status(thm)],[c_0_10715,c_0_10870]) ).
cnf(c_0_10879,hypothesis,
less_equal(idQb,divide(divide(identity,idQ_idQb),b)),
inference(rw,[status(thm)],[c_0_10871,c_0_10817]) ).
cnf(c_0_10880,hypothesis,
divide(divide(identity,idQ_idQb),idQb) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10872]),c_0_10721])]) ).
cnf(c_0_10881,plain,
less_equal(divide(idQb_Q__idQ_idQa,idQa),zero),
inference(spm,[status(thm)],[c_0_10739,c_0_10873]) ).
cnf(c_0_10882,hypothesis,
divide(divide(divide(divide(identity,idQ_idQa),idQb_Q__idQ_idQa),idQ_idQb),zero) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10874]),c_0_10721])]) ).
cnf(c_0_10883,hypothesis,
divide(divide(identity,idQ_idQa),a) = idQa,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10875]),c_0_10876])]) ).
cnf(c_0_10884,plain,
less_equal(divide(X1,idQ_idQa),idQa),
inference(spm,[status(thm)],[c_0_10739,c_0_10877]) ).
cnf(c_0_10885,hypothesis,
less_equal(divide(divide(divide(divide(identity,idQ_idQb),idQa_Q__idQ_idQb),idQ_idQa),zero),zero),
inference(spm,[status(thm)],[c_0_10847,c_0_10878]) ).
cnf(c_0_10886,hypothesis,
divide(divide(identity,idQ_idQb),b) = idQb,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10879]),c_0_10809])]) ).
cnf(c_0_10887,hypothesis,
quotient(divide(identity,idQ_idQb),idQb,zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10880]) ).
cnf(c_0_10888,hypothesis,
less_equal(divide(divide(X1,idQ_idQb),idQa_Q__idQ_idQb),divide(divide(X1,idQa),idQ_idQb)),
inference(spm,[status(thm)],[c_0_10862,c_0_10709]) ).
cnf(c_0_10889,plain,
divide(idQb_Q__idQ_idQa,idQa) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10881]),c_0_10721])]) ).
cnf(c_0_10890,plain,
zero = divide(zero,X1),
i_0_10603 ).
cnf(c_0_10891,hypothesis,
( less_equal(divide(idQa_Q__idQ_idQb,divide(X1,idQ_idQb)),divide(X2,idQ_idQb))
| ~ quotient(idQa,X1,X2) ),
inference(spm,[status(thm)],[c_0_10760,c_0_10843]) ).
cnf(c_0_10892,hypothesis,
divide(divide(divide(identity,idQ_idQa),idQb_Q__idQ_idQa),idQ_idQb) = zero,
inference(rw,[status(thm)],[c_0_10882,c_0_10817]) ).
cnf(c_0_10893,plain,
divide(identity,idQ_idQa) = idQa,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10856,c_0_10883]),c_0_10884])]) ).
cnf(c_0_10894,hypothesis,
divide(divide(divide(divide(identity,idQ_idQb),idQa_Q__idQ_idQb),idQ_idQa),zero) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10885]),c_0_10721])]) ).
cnf(c_0_10895,plain,
( divide(identity,idQ_idQb) = idQb
| ~ less_equal(divide(identity,idQ_idQb),idQb) ),
inference(spm,[status(thm)],[c_0_10856,c_0_10886]) ).
cnf(c_0_10896,hypothesis,
less_equal(divide(identity,idQ_idQb),idQb),
inference(spm,[status(thm)],[c_0_10739,c_0_10887]) ).
cnf(c_0_10897,hypothesis,
less_equal(divide(divide(idQb_Q__idQ_idQa,idQ_idQb),idQa_Q__idQ_idQb),zero),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10888,c_0_10889]),c_0_10890]) ).
cnf(c_0_10898,hypothesis,
less_equal(divide(idQa_Q__idQ_idQb,divide(X1,idQ_idQb)),divide(divide(idQa,X1),idQ_idQb)),
inference(spm,[status(thm)],[c_0_10891,c_0_10709]) ).
cnf(c_0_10899,hypothesis,
divide(divide(idQa,idQb_Q__idQ_idQa),idQ_idQb) = zero,
inference(rw,[status(thm)],[c_0_10892,c_0_10893]) ).
cnf(c_0_10900,hypothesis,
( less_equal(divide(idQb_Q__idQ_idQa,divide(X1,idQ_idQa)),divide(X2,idQ_idQa))
| ~ quotient(idQb,X1,X2) ),
inference(spm,[status(thm)],[c_0_10760,c_0_10756]) ).
cnf(c_0_10901,hypothesis,
divide(divide(divide(identity,idQ_idQb),idQa_Q__idQ_idQb),idQ_idQa) = zero,
inference(rw,[status(thm)],[c_0_10894,c_0_10817]) ).
cnf(c_0_10902,plain,
divide(identity,idQ_idQb) = idQb,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_10895,c_0_10896])]) ).
cnf(c_0_10903,hypothesis,
divide(divide(idQb_Q__idQ_idQa,idQ_idQb),idQa_Q__idQ_idQb) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10897]),c_0_10721])]) ).
cnf(c_0_10904,hypothesis,
less_equal(divide(idQa_Q__idQ_idQb,divide(idQb_Q__idQ_idQa,idQ_idQb)),zero),
inference(spm,[status(thm)],[c_0_10898,c_0_10899]) ).
cnf(c_0_10905,hypothesis,
less_equal(divide(idQb_Q__idQ_idQa,divide(X1,idQ_idQa)),divide(divide(idQb,X1),idQ_idQa)),
inference(spm,[status(thm)],[c_0_10900,c_0_10709]) ).
cnf(c_0_10906,hypothesis,
divide(divide(idQb,idQa_Q__idQ_idQb),idQ_idQa) = zero,
inference(rw,[status(thm)],[c_0_10901,c_0_10902]) ).
cnf(c_0_10907,hypothesis,
quotient(divide(idQb_Q__idQ_idQa,idQ_idQb),idQa_Q__idQ_idQb,zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10903]) ).
cnf(c_0_10908,hypothesis,
divide(idQa_Q__idQ_idQb,divide(idQb_Q__idQ_idQa,idQ_idQb)) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10904]),c_0_10721])]) ).
cnf(c_0_10909,hypothesis,
less_equal(divide(idQb_Q__idQ_idQa,divide(idQa_Q__idQ_idQb,idQ_idQa)),zero),
inference(spm,[status(thm)],[c_0_10905,c_0_10906]) ).
cnf(c_0_10910,hypothesis,
less_equal(divide(idQb_Q__idQ_idQa,idQ_idQb),idQa_Q__idQ_idQb),
inference(spm,[status(thm)],[c_0_10739,c_0_10907]) ).
cnf(c_0_10911,hypothesis,
quotient(idQa_Q__idQ_idQb,divide(idQb_Q__idQ_idQa,idQ_idQb),zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10908]) ).
cnf(c_0_10912,hypothesis,
divide(idQb_Q__idQ_idQa,divide(idQa_Q__idQ_idQb,idQ_idQa)) = zero,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10909]),c_0_10721])]) ).
cnf(c_0_10913,hypothesis,
( divide(idQb_Q__idQ_idQa,idQ_idQb) = idQa_Q__idQ_idQb
| ~ less_equal(idQa_Q__idQ_idQb,divide(idQb_Q__idQ_idQa,idQ_idQb)) ),
inference(spm,[status(thm)],[c_0_10719,c_0_10910]) ).
cnf(c_0_10914,hypothesis,
less_equal(idQa_Q__idQ_idQb,divide(idQb_Q__idQ_idQa,idQ_idQb)),
inference(spm,[status(thm)],[c_0_10739,c_0_10911]) ).
cnf(c_0_10915,hypothesis,
quotient(idQb_Q__idQ_idQa,divide(idQa_Q__idQ_idQb,idQ_idQa),zero),
inference(spm,[status(thm)],[c_0_10709,c_0_10912]) ).
cnf(c_0_10916,hypothesis,
divide(idQb_Q__idQ_idQa,idQ_idQb) = idQa_Q__idQ_idQb,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_10913,c_0_10914])]) ).
cnf(c_0_10917,hypothesis,
less_equal(idQb_Q__idQ_idQa,divide(idQa_Q__idQ_idQb,idQ_idQa)),
inference(spm,[status(thm)],[c_0_10739,c_0_10915]) ).
cnf(c_0_10918,plain,
less_equal(divide(idQa_Q__idQ_idQb,X1),idQb_Q__idQ_idQa),
inference(spm,[status(thm)],[c_0_10846,c_0_10916]) ).
cnf(c_0_10919,hypothesis,
divide(idQa_Q__idQ_idQb,idQ_idQa) = idQb_Q__idQ_idQa,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10719,c_0_10917]),c_0_10918])]) ).
cnf(c_0_10920,plain,
less_equal(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa),
inference(spm,[status(thm)],[c_0_10716,c_0_10916]) ).
cnf(c_0_10921,negated_conjecture,
idQa_Q__idQ_idQb != idQb_Q__idQ_idQa,
i_0_31 ).
cnf(c_0_10922,plain,
$false,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10856,c_0_10919]),c_0_10920])]),c_0_10921]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : HEN011-1 : TPTP v9.2.1. Released v1.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n021.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Mon May 4 19:10:10 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 164.74/110.46 % Version : CSE_E---1.7
% 164.74/110.46 % Problem : theBenchmark.p
% 164.74/110.46 % SZS status Unsatisfiable for theBenchmark.p
% 164.74/110.46 % SZS output start CNFRefutation
% See solution above
% 165.84/111.59 % Total time : 109.266s
%------------------------------------------------------------------------------