%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : HEN011-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n002.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 : Fri Sep 25 01:37:26 PM UTC 2026
% Result : Unsatisfiable 28.03s 6.02s
% Output : CNFRefutation 28.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 16
% Syntax : Number of formulae : 310 ( 212 unt; 0 def)
% Number of atoms : 1335 ( 193 equ)
% Maximal formula atoms : 6 ( 4 avg)
% Number of connectives : 234 ( 118 ~; 116 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 10 con; 0-0 aty)
% Number of variables : 261 ( 0 sgn 261 !; 0 ?; 242 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( quotient(X0,X1,zero)
| ~ less_equal(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',quotient_less_equal) ).
fof(f2,axiom,
! [X0,X1] :
( less_equal(X0,X1)
| ~ quotient(X0,X1,zero) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',less_equal_quotient) ).
fof(f3,axiom,
! [X2,X0,X1] :
( less_equal(X2,X0)
| ~ quotient(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',divisor_existence) ).
fof(f4,axiom,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( less_equal(X6,X7)
| ~ quotient(X2,X3,X7)
| ~ quotient(X5,X4,X6)
| ~ quotient(X0,X3,X5)
| ~ quotient(X1,X3,X4)
| ~ quotient(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',quotient_property) ).
fof(f5,axiom,
! [X0] : less_equal(zero,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',zero_is_smallest) ).
fof(f6,axiom,
! [X0,X1] :
( X0 = X1
| ~ less_equal(X1,X0)
| ~ less_equal(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',less_equal_and_equal) ).
fof(f7,axiom,
! [X0] : less_equal(X0,identity),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',identity_is_largest) ).
fof(f10,axiom,
quotient(identity,a,idQa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity_divide_a) ).
fof(f11,axiom,
quotient(identity,b,idQb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity_divide_b) ).
fof(f12,axiom,
quotient(identity,idQb,idQ_idQb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity_divide_idQb) ).
fof(f13,axiom,
quotient(idQa,idQ_idQb,idQa_Q__idQ_idQb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idQa_divide_idQ_idQb) ).
fof(f14,axiom,
quotient(identity,idQa,idQ_idQa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity_divide_idQa) ).
fof(f15,axiom,
quotient(idQb,idQ_idQa,idQb_Q__idQ_idQa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idQb_divide_idQ_idQa) ).
fof(f16,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) ).
tcf(c_65,plain,
! [X0: $i,X1: $i] :
( quotient(X0,X1,zero)
| ~ less_equal(X0,X1) ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i] :
( less_equal(X0,X1)
| ~ quotient(X0,X1,zero) ),
inference(cnf_transformation,[],[f2]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i,X2: $i] :
( less_equal(X2,X0)
| ~ quotient(X0,X1,X2) ),
inference(cnf_transformation,[],[f3]) ).
tcf(c_68,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( less_equal(X7,X6)
| ~ quotient(X4,X5,X7)
| ~ quotient(X2,X3,X6)
| ~ quotient(X1,X3,X5)
| ~ quotient(X0,X3,X4)
| ~ quotient(X0,X1,X2) ),
inference(cnf_transformation,[],[f4]) ).
tcf(c_69,plain,
! [X0: $i] : less_equal(zero,X0),
inference(cnf_transformation,[],[f5]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ less_equal(X1,X0)
| ~ less_equal(X0,X1) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_71,plain,
! [X0: $i] : less_equal(X0,identity),
inference(cnf_transformation,[],[f7]) ).
tcf(c_74,plain,
quotient(identity,a,idQa),
inference(cnf_transformation,[],[f10]) ).
tcf(c_75,plain,
quotient(identity,b,idQb),
inference(cnf_transformation,[],[f11]) ).
tcf(c_76,plain,
quotient(identity,idQb,idQ_idQb),
inference(cnf_transformation,[],[f12]) ).
tcf(c_77,plain,
quotient(idQa,idQ_idQb,idQa_Q__idQ_idQb),
inference(cnf_transformation,[],[f13]) ).
tcf(c_78,plain,
quotient(identity,idQa,idQ_idQa),
inference(cnf_transformation,[],[f14]) ).
tcf(c_79,plain,
quotient(idQb,idQ_idQa,idQb_Q__idQ_idQa),
inference(cnf_transformation,[],[f15]) ).
tcf(c_80,negated_conjecture,
idQa_Q__idQ_idQb != idQb_Q__idQ_idQa,
inference(cnf_transformation,[],[f16]) ).
tcf(c_87,plain,
divide(identity,a) = idQa,
inference(well_definedness,[status(thm)],[c_74]) ).
tcf(c_88,plain,
divide(identity,b) = idQb,
inference(well_definedness,[status(thm)],[c_75]) ).
tcf(c_89,plain,
divide(identity,idQb) = idQ_idQb,
inference(well_definedness,[status(thm)],[c_76]) ).
tcf(c_90,plain,
divide(idQa,idQ_idQb) = idQa_Q__idQ_idQb,
inference(well_definedness,[status(thm)],[c_77]) ).
tcf(c_91,plain,
divide(identity,idQa) = idQ_idQa,
inference(well_definedness,[status(thm)],[c_78]) ).
tcf(c_92,plain,
divide(idQb,idQ_idQa) = idQb_Q__idQ_idQa,
inference(well_definedness,[status(thm)],[c_79]) ).
tcf(c_93,plain,
! [X0: $i,X1: $i] :
( ( divide(X0,X1) = zero )
| ~ less_equal(X0,X1) ),
inference(well_definedness,[status(thm)],[c_65]) ).
tcf(c_94,plain,
! [X0: $i,X1: $i] :
( less_equal(X0,X1)
| ( divide(X0,X1) != zero ) ),
inference(well_definedness,[status(thm)],[c_66]) ).
tcf(c_95,plain,
! [X0: $i,X1: $i,X2: $i] :
( less_equal(X2,X0)
| ( divide(X0,X1) != X2 ) ),
inference(well_definedness,[status(thm)],[c_67]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( less_equal(X7,X6)
| ( divide(X4,X5) != X7 )
| ( divide(X2,X3) != X6 )
| ( divide(X1,X3) != X5 )
| ( divide(X0,X3) != X4 )
| ( divide(X0,X1) != X2 ) ),
inference(well_definedness,[status(thm)],[c_68]) ).
tcf(c_107,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( divide(X0,X1) != X2 )
| less_equal(X2,X0) ),
inference(prop_impl_just,[status(thm)],[c_95]) ).
tcf(c_108,plain,
! [X0: $i,X1: $i,X2: $i] :
( less_equal(X2,X0)
| ( divide(X0,X1) != X2 ) ),
inference(renaming,[status(thm)],[c_107]) ).
tcf(c_196,plain,
! [X0: $i,X1: $i] : less_equal(divide(X0,X1),X0),
inference(unflattening,[status(thm)],[c_108]) ).
tcf(c_210,plain,
! [X0: $i,X1: $i,X2: $i] : less_equal(divide(divide(X0,X1),divide(X2,X1)),divide(divide(X0,X2),X1)),
inference(unflattening,[status(thm)],[c_97]) ).
tcf(c_218,plain,
! [X0: $i,X1: $i] :
( ( divide(X0,X1) != zero )
| less_equal(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_94]) ).
tcf(c_219,plain,
! [X0: $i,X1: $i] :
( less_equal(X0,X1)
| ( divide(X0,X1) != zero ) ),
inference(renaming,[status(thm)],[c_218]) ).
tcf(c_220,plain,
! [X0: $i,X1: $i] :
( ( divide(X0,X1) = zero )
| ~ less_equal(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_93]) ).
tcf(c_295,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_297,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_486,plain,
less_equal(idQa_Q__idQ_idQb,idQa),
inference(superposition,[status(thm)],[c_90,c_196]) ).
tcf(c_487,plain,
less_equal(idQb_Q__idQ_idQa,idQb),
inference(superposition,[status(thm)],[c_92,c_196]) ).
tcf(c_490,plain,
! [X0: $i] : divide(zero,X0) = zero,
inference(superposition,[status(thm)],[c_69,c_220]) ).
tcf(c_491,plain,
! [X0: $i] : divide(X0,identity) = zero,
inference(superposition,[status(thm)],[c_71,c_220]) ).
tcf(c_492,plain,
! [X0: $i,X1: $i] : divide(divide(X0,X1),X0) = zero,
inference(superposition,[status(thm)],[c_196,c_220]) ).
tcf(c_502,plain,
! [X0: $i] :
( ( X0 = zero )
| ~ less_equal(X0,zero) ),
inference(superposition,[status(thm)],[c_69,c_70]) ).
tcf(c_504,plain,
! [X0: $i,X1: $i] :
( ( divide(X0,X1) = X0 )
| ~ less_equal(X0,divide(X0,X1)) ),
inference(superposition,[status(thm)],[c_196,c_70]) ).
tcf(c_516,plain,
divide(idQa_Q__idQ_idQb,idQa) = zero,
inference(superposition,[status(thm)],[c_486,c_220]) ).
tcf(c_520,plain,
divide(idQb_Q__idQ_idQa,idQb) = zero,
inference(superposition,[status(thm)],[c_487,c_220]) ).
tcf(c_590,plain,
! [X0: $i] :
( ( idQa_Q__idQ_idQb = idQb_Q__idQ_idQa )
| ( idQb_Q__idQ_idQa != X0 )
| ( idQa_Q__idQ_idQb != X0 ) ),
inference(instantiation,[status(thm)],[c_297]) ).
tcf(c_636,plain,
( less_equal(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa)
| ( divide(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa) != zero ) ),
inference(instantiation,[status(thm)],[c_219]) ).
tcf(c_641,plain,
( ( idQa_Q__idQ_idQb = idQb_Q__idQ_idQa )
| ( idQb_Q__idQ_idQa != idQa_Q__idQ_idQb )
| ( idQa_Q__idQ_idQb != idQa_Q__idQ_idQb ) ),
inference(instantiation,[status(thm)],[c_590]) ).
tcf(c_642,plain,
idQa_Q__idQ_idQb = idQa_Q__idQ_idQb,
inference(instantiation,[status(thm)],[c_295]) ).
tcf(c_645,plain,
! [X0: $i] : less_equal(divide(idQa,divide(X0,a)),divide(divide(identity,X0),a)),
inference(superposition,[status(thm)],[c_87,c_210]) ).
tcf(c_646,plain,
! [X0: $i] : less_equal(divide(idQb,divide(X0,b)),divide(divide(identity,X0),b)),
inference(superposition,[status(thm)],[c_88,c_210]) ).
tcf(c_648,plain,
! [X0: $i] : less_equal(divide(idQa_Q__idQ_idQb,divide(X0,idQ_idQb)),divide(divide(idQa,X0),idQ_idQb)),
inference(superposition,[status(thm)],[c_90,c_210]) ).
tcf(c_650,plain,
! [X0: $i] : less_equal(divide(idQb_Q__idQ_idQa,divide(X0,idQ_idQa)),divide(divide(idQb,X0),idQ_idQa)),
inference(superposition,[status(thm)],[c_92,c_210]) ).
tcf(c_656,plain,
! [X0: $i] : less_equal(divide(divide(X0,a),idQa),divide(divide(X0,identity),a)),
inference(superposition,[status(thm)],[c_87,c_210]) ).
tcf(c_657,plain,
! [X0: $i] : less_equal(divide(divide(X0,b),idQb),divide(divide(X0,identity),b)),
inference(superposition,[status(thm)],[c_88,c_210]) ).
tcf(c_658,plain,
! [X0: $i] : less_equal(divide(divide(X0,idQb),idQ_idQb),divide(divide(X0,identity),idQb)),
inference(superposition,[status(thm)],[c_89,c_210]) ).
tcf(c_659,plain,
! [X0: $i] : less_equal(divide(divide(X0,idQ_idQb),idQa_Q__idQ_idQb),divide(divide(X0,idQa),idQ_idQb)),
inference(superposition,[status(thm)],[c_90,c_210]) ).
tcf(c_660,plain,
! [X0: $i] : less_equal(divide(divide(X0,idQa),idQ_idQa),divide(divide(X0,identity),idQa)),
inference(superposition,[status(thm)],[c_91,c_210]) ).
tcf(c_661,plain,
! [X0: $i] : less_equal(divide(divide(X0,idQ_idQa),idQb_Q__idQ_idQa),divide(divide(X0,idQb),idQ_idQa)),
inference(superposition,[status(thm)],[c_92,c_210]) ).
tcf(c_662,plain,
! [X0: $i,X1: $i] : less_equal(divide(divide(X0,X1),zero),divide(divide(X0,zero),X1)),
inference(superposition,[status(thm)],[c_490,c_210]) ).
tcf(c_665,plain,
! [X0: $i] : less_equal(divide(divide(X0,idQa),zero),divide(divide(X0,idQa_Q__idQ_idQb),idQa)),
inference(superposition,[status(thm)],[c_516,c_210]) ).
tcf(c_666,plain,
! [X0: $i] : less_equal(divide(divide(X0,idQb),zero),divide(divide(X0,idQb_Q__idQ_idQa),idQb)),
inference(superposition,[status(thm)],[c_520,c_210]) ).
tcf(c_680,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( divide(divide(X0,X2),divide(X1,X2)) = divide(divide(X0,X1),X2) )
| ~ less_equal(divide(divide(X0,X1),X2),divide(divide(X0,X2),divide(X1,X2))) ),
inference(superposition,[status(thm)],[c_210,c_70]) ).
tcf(c_681,plain,
! [X0: $i,X1: $i,X2: $i] : divide(divide(divide(X0,X1),divide(X2,X1)),divide(divide(X0,X2),X1)) = zero,
inference(superposition,[status(thm)],[c_210,c_220]) ).
tcf(c_690,plain,
! [X0: $i] : less_equal(divide(divide(X0,idQa),idQ_idQa),divide(zero,idQa)),
inference(light_normalisation,[status(thm)],[c_660,c_491]) ).
tcf(c_691,plain,
! [X0: $i] : less_equal(divide(divide(X0,idQb),idQ_idQb),divide(zero,idQb)),
inference(light_normalisation,[status(thm)],[c_658,c_491]) ).
tcf(c_692,plain,
! [X0: $i] : less_equal(divide(divide(X0,b),idQb),divide(zero,b)),
inference(light_normalisation,[status(thm)],[c_657,c_491]) ).
tcf(c_693,plain,
! [X0: $i] : less_equal(divide(divide(X0,a),idQa),divide(zero,a)),
inference(light_normalisation,[status(thm)],[c_656,c_491]) ).
tcf(c_736,plain,
( ( idQb_Q__idQ_idQa = idQa_Q__idQ_idQb )
| ~ less_equal(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb)
| ~ less_equal(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_792,plain,
! [X0: $i] : divide(divide(idQa_Q__idQ_idQb,divide(X0,idQ_idQb)),divide(divide(idQa,X0),idQ_idQb)) = zero,
inference(superposition,[status(thm)],[c_90,c_681]) ).
tcf(c_794,plain,
! [X0: $i] : divide(divide(idQb_Q__idQ_idQa,divide(X0,idQ_idQa)),divide(divide(idQb,X0),idQ_idQa)) = zero,
inference(superposition,[status(thm)],[c_92,c_681]) ).
tcf(c_1050,plain,
! [X0: $i,X1: $i] :
( ( divide(divide(X0,X0),divide(X1,X0)) = divide(divide(X0,X1),X0) )
| ~ less_equal(zero,divide(divide(X0,X0),divide(X1,X0))) ),
inference(superposition,[status(thm)],[c_492,c_680]) ).
tcf(c_1059,plain,
! [X0: $i,X1: $i] :
( ( divide(divide(X1,X0),divide(identity,X0)) = divide(divide(X1,identity),X0) )
| ~ less_equal(divide(zero,X0),divide(divide(X1,X0),divide(identity,X0))) ),
inference(superposition,[status(thm)],[c_491,c_680]) ).
tcf(c_1061,plain,
! [X0: $i] :
( ( divide(divide(idQa_Q__idQ_idQb,X0),divide(idQa,X0)) = divide(divide(idQa_Q__idQ_idQb,idQa),X0) )
| ~ less_equal(divide(zero,X0),divide(divide(idQa_Q__idQ_idQb,X0),divide(idQa,X0))) ),
inference(superposition,[status(thm)],[c_516,c_680]) ).
tcf(c_1062,plain,
! [X0: $i] :
( ( divide(divide(idQb_Q__idQ_idQa,X0),divide(idQb,X0)) = divide(divide(idQb_Q__idQ_idQa,idQb),X0) )
| ~ less_equal(divide(zero,X0),divide(divide(idQb_Q__idQ_idQa,X0),divide(idQb,X0))) ),
inference(superposition,[status(thm)],[c_520,c_680]) ).
tcf(c_1089,plain,
! [X0: $i,X1: $i] :
( ( divide(divide(X0,X0),divide(X1,X0)) = zero )
| ~ less_equal(zero,divide(divide(X0,X0),divide(X1,X0))) ),
inference(light_normalisation,[status(thm)],[c_1050,c_492]) ).
tcf(c_1090,plain,
! [X0: $i,X1: $i] : divide(divide(X0,X0),divide(X1,X0)) = zero,
inference(forward_subsumption_resolution,[status(thm)],[c_1089,c_69]) ).
tcf(c_1152,plain,
! [X0: $i] :
( ( divide(divide(idQb_Q__idQ_idQa,X0),divide(idQb,X0)) = zero )
| ~ less_equal(zero,divide(divide(idQb_Q__idQ_idQa,X0),divide(idQb,X0))) ),
inference(light_normalisation,[status(thm)],[c_1062,c_490,c_520]) ).
tcf(c_1153,plain,
! [X0: $i] : divide(divide(idQb_Q__idQ_idQa,X0),divide(idQb,X0)) = zero,
inference(forward_subsumption_resolution,[status(thm)],[c_1152,c_69]) ).
tcf(c_1154,plain,
! [X0: $i] :
( ( divide(divide(idQa_Q__idQ_idQb,X0),divide(idQa,X0)) = zero )
| ~ less_equal(zero,divide(divide(idQa_Q__idQ_idQb,X0),divide(idQa,X0))) ),
inference(light_normalisation,[status(thm)],[c_1061,c_490,c_516]) ).
tcf(c_1155,plain,
! [X0: $i] : divide(divide(idQa_Q__idQ_idQb,X0),divide(idQa,X0)) = zero,
inference(forward_subsumption_resolution,[status(thm)],[c_1154,c_69]) ).
tcf(c_1156,plain,
! [X0: $i,X1: $i] :
( ( divide(divide(X0,X1),divide(identity,X1)) = divide(divide(X0,identity),X1) )
| ~ less_equal(zero,divide(divide(X0,X1),divide(identity,X1))) ),
inference(light_normalisation,[status(thm)],[c_1059,c_490]) ).
tcf(c_1157,plain,
! [X0: $i,X1: $i] :
( ( divide(divide(X0,X1),divide(identity,X1)) = divide(zero,X1) )
| ~ less_equal(zero,divide(divide(X0,X1),divide(identity,X1))) ),
inference(light_normalisation,[status(thm)],[c_1156,c_491]) ).
tcf(c_1158,plain,
! [X0: $i,X1: $i] : divide(divide(X0,X1),divide(identity,X1)) = divide(zero,X1),
inference(forward_subsumption_resolution,[status(thm)],[c_1157,c_69]) ).
tcf(c_1529,plain,
! [X0: $i] : less_equal(divide(divide(X0,idQa),idQ_idQa),zero),
inference(demodulation,[status(thm)],[c_690,c_490]) ).
tcf(c_1531,plain,
less_equal(divide(idQ_idQa,idQ_idQa),zero),
inference(superposition,[status(thm)],[c_91,c_1529]) ).
tcf(c_1537,plain,
! [X0: $i] : divide(divide(X0,idQa),idQ_idQa) = zero,
inference(superposition,[status(thm)],[c_1529,c_502]) ).
tcf(c_1544,plain,
divide(idQ_idQa,idQ_idQa) = zero,
inference(superposition,[status(thm)],[c_1531,c_502]) ).
tcf(c_1610,plain,
! [X0: $i] : less_equal(divide(X0,idQa),idQ_idQa),
inference(superposition,[status(thm)],[c_1537,c_219]) ).
tcf(c_1620,plain,
! [X0: $i] :
( ( divide(divide(X0,idQ_idQa),divide(idQa,idQ_idQa)) = divide(divide(X0,idQa),idQ_idQa) )
| ~ less_equal(zero,divide(divide(X0,idQ_idQa),divide(idQa,idQ_idQa))) ),
inference(superposition,[status(thm)],[c_1537,c_680]) ).
tcf(c_1625,plain,
! [X0: $i] :
( ( divide(divide(X0,idQ_idQa),divide(idQa,idQ_idQa)) = zero )
| ~ less_equal(zero,divide(divide(X0,idQ_idQa),divide(idQa,idQ_idQa))) ),
inference(light_normalisation,[status(thm)],[c_1620,c_1537]) ).
tcf(c_1626,plain,
! [X0: $i] : divide(divide(X0,idQ_idQa),divide(idQa,idQ_idQa)) = zero,
inference(forward_subsumption_resolution,[status(thm)],[c_1625,c_69]) ).
tcf(c_1679,plain,
! [X0: $i] : less_equal(divide(divide(X0,idQb),idQ_idQb),zero),
inference(demodulation,[status(thm)],[c_691,c_490]) ).
tcf(c_1681,plain,
less_equal(divide(idQ_idQb,idQ_idQb),zero),
inference(superposition,[status(thm)],[c_89,c_1679]) ).
tcf(c_1687,plain,
! [X0: $i] : divide(divide(X0,idQb),idQ_idQb) = zero,
inference(superposition,[status(thm)],[c_1679,c_502]) ).
tcf(c_1695,plain,
divide(idQ_idQb,idQ_idQb) = zero,
inference(superposition,[status(thm)],[c_1681,c_502]) ).
tcf(c_1709,plain,
divide(divide(idQa_Q__idQ_idQb,zero),divide(divide(idQa,idQ_idQb),idQ_idQb)) = zero,
inference(superposition,[status(thm)],[c_1695,c_792]) ).
tcf(c_1715,plain,
divide(divide(idQa_Q__idQ_idQb,zero),divide(idQa_Q__idQ_idQb,idQ_idQb)) = zero,
inference(light_normalisation,[status(thm)],[c_1709,c_90]) ).
tcf(c_1773,plain,
! [X0: $i] : less_equal(divide(X0,idQb),idQ_idQb),
inference(superposition,[status(thm)],[c_1687,c_219]) ).
tcf(c_1785,plain,
! [X0: $i] :
( ( divide(divide(X0,idQ_idQb),divide(idQb,idQ_idQb)) = divide(divide(X0,idQb),idQ_idQb) )
| ~ less_equal(zero,divide(divide(X0,idQ_idQb),divide(idQb,idQ_idQb))) ),
inference(superposition,[status(thm)],[c_1687,c_680]) ).
tcf(c_1790,plain,
! [X0: $i] :
( ( divide(divide(X0,idQ_idQb),divide(idQb,idQ_idQb)) = zero )
| ~ less_equal(zero,divide(divide(X0,idQ_idQb),divide(idQb,idQ_idQb))) ),
inference(light_normalisation,[status(thm)],[c_1785,c_1687]) ).
tcf(c_1791,plain,
! [X0: $i] : divide(divide(X0,idQ_idQb),divide(idQb,idQ_idQb)) = zero,
inference(forward_subsumption_resolution,[status(thm)],[c_1790,c_69]) ).
tcf(c_1851,plain,
divide(divide(idQb_Q__idQ_idQa,divide(idQ_idQa,idQ_idQa)),divide(idQb_Q__idQ_idQa,idQ_idQa)) = zero,
inference(superposition,[status(thm)],[c_92,c_794]) ).
tcf(c_1869,plain,
divide(divide(idQb_Q__idQ_idQa,zero),divide(idQb_Q__idQ_idQa,idQ_idQa)) = zero,
inference(light_normalisation,[status(thm)],[c_1851,c_1544]) ).
tcf(c_2019,plain,
! [X0: $i] : less_equal(divide(divide(X0,b),idQb),zero),
inference(demodulation,[status(thm)],[c_692,c_490]) ).
tcf(c_2026,plain,
! [X0: $i] : divide(divide(X0,b),idQb) = zero,
inference(superposition,[status(thm)],[c_2019,c_502]) ).
tcf(c_2109,plain,
! [X0: $i] : less_equal(divide(X0,b),idQb),
inference(superposition,[status(thm)],[c_2026,c_219]) ).
tcf(c_2121,plain,
! [X0: $i] :
( ( divide(divide(X0,idQb),divide(b,idQb)) = divide(divide(X0,b),idQb) )
| ~ less_equal(zero,divide(divide(X0,idQb),divide(b,idQb))) ),
inference(superposition,[status(thm)],[c_2026,c_680]) ).
tcf(c_2126,plain,
! [X0: $i] :
( ( divide(divide(X0,idQb),divide(b,idQb)) = zero )
| ~ less_equal(zero,divide(divide(X0,idQb),divide(b,idQb))) ),
inference(light_normalisation,[status(thm)],[c_2121,c_2026]) ).
tcf(c_2127,plain,
! [X0: $i] : divide(divide(X0,idQb),divide(b,idQb)) = zero,
inference(forward_subsumption_resolution,[status(thm)],[c_2126,c_69]) ).
tcf(c_2168,plain,
! [X0: $i] :
( ( divide(X0,b) = idQb )
| ~ less_equal(idQb,divide(X0,b)) ),
inference(superposition,[status(thm)],[c_2109,c_70]) ).
tcf(c_2173,plain,
! [X0: $i] : less_equal(divide(divide(X0,a),idQa),zero),
inference(demodulation,[status(thm)],[c_693,c_490]) ).
tcf(c_2180,plain,
! [X0: $i] : divide(divide(X0,a),idQa) = zero,
inference(superposition,[status(thm)],[c_2173,c_502]) ).
tcf(c_2315,plain,
! [X0: $i] : less_equal(divide(X0,a),idQa),
inference(superposition,[status(thm)],[c_2180,c_219]) ).
tcf(c_2328,plain,
! [X0: $i] :
( ( divide(divide(X0,idQa),divide(a,idQa)) = divide(divide(X0,a),idQa) )
| ~ less_equal(zero,divide(divide(X0,idQa),divide(a,idQa))) ),
inference(superposition,[status(thm)],[c_2180,c_680]) ).
tcf(c_2334,plain,
! [X0: $i] :
( ( divide(divide(X0,idQa),divide(a,idQa)) = zero )
| ~ less_equal(zero,divide(divide(X0,idQa),divide(a,idQa))) ),
inference(light_normalisation,[status(thm)],[c_2328,c_2180]) ).
tcf(c_2335,plain,
! [X0: $i] : divide(divide(X0,idQa),divide(a,idQa)) = zero,
inference(forward_subsumption_resolution,[status(thm)],[c_2334,c_69]) ).
tcf(c_2529,plain,
! [X0: $i,X1: $i] : less_equal(divide(X0,X0),divide(X1,X0)),
inference(superposition,[status(thm)],[c_1090,c_219]) ).
tcf(c_2603,plain,
! [X0: $i] : less_equal(divide(X0,X0),zero),
inference(superposition,[status(thm)],[c_492,c_2529]) ).
tcf(c_2639,plain,
! [X0: $i] : divide(X0,X0) = zero,
inference(superposition,[status(thm)],[c_2603,c_502]) ).
tcf(c_2718,plain,
! [X0: $i,X1: $i] :
( ( divide(divide(divide(idQb_Q__idQ_idQa,X1),X0),divide(divide(idQb,X1),X0)) = divide(divide(divide(idQb_Q__idQ_idQa,X1),divide(idQb,X1)),X0) )
| ~ less_equal(divide(zero,X0),divide(divide(divide(idQb_Q__idQ_idQa,X1),X0),divide(divide(idQb,X1),X0))) ),
inference(superposition,[status(thm)],[c_1153,c_680]) ).
tcf(c_2746,plain,
! [X0: $i,X1: $i] :
( ( divide(divide(divide(idQb_Q__idQ_idQa,X0),X1),divide(divide(idQb,X0),X1)) = divide(divide(divide(idQb_Q__idQ_idQa,X0),divide(idQb,X0)),X1) )
| ~ less_equal(zero,divide(divide(divide(idQb_Q__idQ_idQa,X0),X1),divide(divide(idQb,X0),X1))) ),
inference(light_normalisation,[status(thm)],[c_2718,c_490]) ).
tcf(c_2747,plain,
! [X0: $i,X1: $i] :
( ( divide(divide(divide(idQb_Q__idQ_idQa,X0),X1),divide(divide(idQb,X0),X1)) = divide(zero,X1) )
| ~ less_equal(zero,divide(divide(divide(idQb_Q__idQ_idQa,X0),X1),divide(divide(idQb,X0),X1))) ),
inference(light_normalisation,[status(thm)],[c_2746,c_1153]) ).
tcf(c_2748,plain,
! [X0: $i,X1: $i] : divide(divide(divide(idQb_Q__idQ_idQa,X0),X1),divide(divide(idQb,X0),X1)) = divide(zero,X1),
inference(forward_subsumption_resolution,[status(thm)],[c_2747,c_69]) ).
tcf(c_2827,plain,
! [X0: $i,X1: $i] :
( ( divide(divide(divide(idQa_Q__idQ_idQb,X1),X0),divide(divide(idQa,X1),X0)) = divide(divide(divide(idQa_Q__idQ_idQb,X1),divide(idQa,X1)),X0) )
| ~ less_equal(divide(zero,X0),divide(divide(divide(idQa_Q__idQ_idQb,X1),X0),divide(divide(idQa,X1),X0))) ),
inference(superposition,[status(thm)],[c_1155,c_680]) ).
tcf(c_2855,plain,
! [X0: $i,X1: $i] :
( ( divide(divide(divide(idQa_Q__idQ_idQb,X0),X1),divide(divide(idQa,X0),X1)) = divide(divide(divide(idQa_Q__idQ_idQb,X0),divide(idQa,X0)),X1) )
| ~ less_equal(zero,divide(divide(divide(idQa_Q__idQ_idQb,X0),X1),divide(divide(idQa,X0),X1))) ),
inference(light_normalisation,[status(thm)],[c_2827,c_490]) ).
tcf(c_2856,plain,
! [X0: $i,X1: $i] :
( ( divide(divide(divide(idQa_Q__idQ_idQb,X0),X1),divide(divide(idQa,X0),X1)) = divide(zero,X1) )
| ~ less_equal(zero,divide(divide(divide(idQa_Q__idQ_idQb,X0),X1),divide(divide(idQa,X0),X1))) ),
inference(light_normalisation,[status(thm)],[c_2855,c_1155]) ).
tcf(c_2857,plain,
! [X0: $i,X1: $i] : divide(divide(divide(idQa_Q__idQ_idQb,X0),X1),divide(divide(idQa,X0),X1)) = divide(zero,X1),
inference(forward_subsumption_resolution,[status(thm)],[c_2856,c_69]) ).
tcf(c_3111,plain,
divide(idQb_Q__idQ_idQa,divide(idQa,idQ_idQa)) = zero,
inference(superposition,[status(thm)],[c_92,c_1626]) ).
tcf(c_3120,plain,
! [X0: $i] : less_equal(divide(X0,idQ_idQa),divide(idQa,idQ_idQa)),
inference(superposition,[status(thm)],[c_1626,c_219]) ).
tcf(c_3295,plain,
less_equal(divide(idQa_Q__idQ_idQb,zero),divide(idQa_Q__idQ_idQb,idQ_idQb)),
inference(superposition,[status(thm)],[c_1715,c_219]) ).
tcf(c_3365,plain,
( ( divide(idQa_Q__idQ_idQb,idQ_idQb) = divide(idQa_Q__idQ_idQb,zero) )
| ~ less_equal(divide(idQa_Q__idQ_idQb,idQ_idQb),divide(idQa_Q__idQ_idQb,zero)) ),
inference(superposition,[status(thm)],[c_3295,c_70]) ).
tcf(c_3518,plain,
divide(idQa_Q__idQ_idQb,divide(idQb,idQ_idQb)) = zero,
inference(superposition,[status(thm)],[c_90,c_1791]) ).
tcf(c_3527,plain,
! [X0: $i] : less_equal(divide(X0,idQ_idQb),divide(idQb,idQ_idQb)),
inference(superposition,[status(thm)],[c_1791,c_219]) ).
tcf(c_3725,plain,
less_equal(divide(idQb_Q__idQ_idQa,zero),divide(idQb_Q__idQ_idQa,idQ_idQa)),
inference(superposition,[status(thm)],[c_1869,c_219]) ).
tcf(c_3805,plain,
( ( divide(idQb_Q__idQ_idQa,idQ_idQa) = divide(idQb_Q__idQ_idQa,zero) )
| ~ less_equal(divide(idQb_Q__idQ_idQa,idQ_idQa),divide(idQb_Q__idQ_idQa,zero)) ),
inference(superposition,[status(thm)],[c_3725,c_70]) ).
tcf(c_3839,plain,
! [X0: $i] : less_equal(divide(X0,idQb),divide(b,idQb)),
inference(superposition,[status(thm)],[c_2127,c_219]) ).
tcf(c_3926,plain,
! [X0: $i] :
( ( divide(X0,idQb) = divide(b,idQb) )
| ~ less_equal(divide(b,idQb),divide(X0,idQb)) ),
inference(superposition,[status(thm)],[c_3839,c_70]) ).
tcf(c_4214,plain,
( ( divide(identity,idQb) = divide(b,idQb) )
| ~ less_equal(divide(b,idQb),idQ_idQb) ),
inference(superposition,[status(thm)],[c_89,c_3926]) ).
tcf(c_4227,plain,
( ( divide(b,idQb) = idQ_idQb )
| ~ less_equal(divide(b,idQb),idQ_idQb) ),
inference(light_normalisation,[status(thm)],[c_4214,c_89]) ).
tcf(c_4228,plain,
divide(b,idQb) = idQ_idQb,
inference(forward_subsumption_resolution,[status(thm)],[c_4227,c_1773]) ).
tcf(c_4242,plain,
divide(idQ_idQb,b) = zero,
inference(superposition,[status(thm)],[c_4228,c_492]) ).
tcf(c_4284,plain,
! [X0: $i] : less_equal(divide(divide(X0,b),zero),divide(divide(X0,idQ_idQb),b)),
inference(superposition,[status(thm)],[c_4242,c_210]) ).
tcf(c_4334,plain,
! [X0: $i] : less_equal(divide(X0,idQa),divide(a,idQa)),
inference(superposition,[status(thm)],[c_2335,c_219]) ).
tcf(c_4557,plain,
! [X0: $i] :
( ( divide(X0,idQa) = divide(a,idQa) )
| ~ less_equal(divide(a,idQa),divide(X0,idQa)) ),
inference(superposition,[status(thm)],[c_4334,c_70]) ).
tcf(c_4587,plain,
( ( divide(identity,idQa) = divide(a,idQa) )
| ~ less_equal(divide(a,idQa),idQ_idQa) ),
inference(superposition,[status(thm)],[c_91,c_4557]) ).
tcf(c_4600,plain,
( ( divide(a,idQa) = idQ_idQa )
| ~ less_equal(divide(a,idQa),idQ_idQa) ),
inference(light_normalisation,[status(thm)],[c_4587,c_91]) ).
tcf(c_4601,plain,
divide(a,idQa) = idQ_idQa,
inference(forward_subsumption_resolution,[status(thm)],[c_4600,c_1610]) ).
tcf(c_4615,plain,
divide(idQ_idQa,a) = zero,
inference(superposition,[status(thm)],[c_4601,c_492]) ).
tcf(c_4695,plain,
! [X0: $i] : less_equal(divide(divide(X0,a),zero),divide(divide(X0,idQ_idQa),a)),
inference(superposition,[status(thm)],[c_4615,c_210]) ).
tcf(c_5131,plain,
less_equal(divide(idQa,zero),divide(divide(identity,idQ_idQa),a)),
inference(superposition,[status(thm)],[c_4615,c_645]) ).
tcf(c_5135,plain,
less_equal(divide(idQa,divide(idQa,a)),divide(idQ_idQa,a)),
inference(superposition,[status(thm)],[c_91,c_645]) ).
tcf(c_5141,plain,
less_equal(divide(idQa,divide(idQa,a)),zero),
inference(light_normalisation,[status(thm)],[c_5135,c_4615]) ).
tcf(c_5182,plain,
divide(idQa,divide(idQa,a)) = zero,
inference(superposition,[status(thm)],[c_5141,c_502]) ).
tcf(c_5433,plain,
less_equal(idQa,divide(idQa,a)),
inference(superposition,[status(thm)],[c_5182,c_219]) ).
tcf(c_5507,plain,
! [X0: $i] :
( less_equal(idQb_Q__idQ_idQa,X0)
| ( divide(idQb_Q__idQ_idQa,X0) != zero ) ),
inference(instantiation,[status(thm)],[c_219]) ).
tcf(c_5518,plain,
divide(idQa,a) = idQa,
inference(superposition,[status(thm)],[c_5433,c_504]) ).
tcf(c_5625,plain,
( ( divide(divide(identity,idQ_idQa),a) = divide(idQa,zero) )
| ~ less_equal(divide(divide(identity,idQ_idQa),a),divide(idQa,zero)) ),
inference(superposition,[status(thm)],[c_5131,c_70]) ).
tcf(c_5831,plain,
less_equal(divide(idQb,zero),divide(divide(identity,idQ_idQb),b)),
inference(superposition,[status(thm)],[c_4242,c_646]) ).
tcf(c_5834,plain,
less_equal(divide(idQb,divide(idQb,b)),divide(idQ_idQb,b)),
inference(superposition,[status(thm)],[c_89,c_646]) ).
tcf(c_5841,plain,
less_equal(divide(idQb,divide(idQb,b)),zero),
inference(light_normalisation,[status(thm)],[c_5834,c_4242]) ).
tcf(c_5881,plain,
divide(idQb,divide(idQb,b)) = zero,
inference(superposition,[status(thm)],[c_5841,c_502]) ).
tcf(c_5891,plain,
less_equal(idQb,divide(idQb,b)),
inference(superposition,[status(thm)],[c_5881,c_219]) ).
tcf(c_6618,plain,
divide(idQb,b) = idQb,
inference(superposition,[status(thm)],[c_5891,c_504]) ).
tcf(c_6842,plain,
( ( divide(divide(identity,idQ_idQb),b) = divide(idQb,zero) )
| ~ less_equal(divide(divide(identity,idQ_idQb),b),divide(idQb,zero)) ),
inference(superposition,[status(thm)],[c_5831,c_70]) ).
tcf(c_9041,plain,
! [X0: $i] : less_equal(divide(divide(X0,divide(X0,zero)),zero),zero),
inference(superposition,[status(thm)],[c_2639,c_662]) ).
tcf(c_9591,plain,
! [X0: $i] : divide(divide(X0,divide(X0,zero)),zero) = zero,
inference(superposition,[status(thm)],[c_9041,c_502]) ).
tcf(c_10050,plain,
! [X0: $i] :
( ( divide(divide(X0,divide(X0,zero)),zero) = divide(X0,divide(X0,zero)) )
| ~ less_equal(divide(X0,divide(X0,zero)),zero) ),
inference(superposition,[status(thm)],[c_9591,c_504]) ).
tcf(c_10051,plain,
! [X0: $i] : less_equal(divide(X0,divide(X0,zero)),zero),
inference(superposition,[status(thm)],[c_9591,c_219]) ).
tcf(c_10066,plain,
! [X0: $i] : divide(divide(X0,divide(X0,zero)),zero) = divide(X0,divide(X0,zero)),
inference(forward_subsumption_resolution,[status(thm)],[c_10050,c_10051]) ).
tcf(c_10067,plain,
! [X0: $i] : divide(X0,divide(X0,zero)) = zero,
inference(light_normalisation,[status(thm)],[c_10066,c_9591]) ).
tcf(c_10113,plain,
! [X0: $i] : less_equal(X0,divide(X0,zero)),
inference(superposition,[status(thm)],[c_10067,c_219]) ).
tcf(c_10227,plain,
( less_equal(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb)
| ( divide(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb) != zero ) ),
inference(instantiation,[status(thm)],[c_5507]) ).
tcf(c_10424,plain,
! [X0: $i] : divide(X0,zero) = X0,
inference(superposition,[status(thm)],[c_10113,c_504]) ).
tcf(c_10440,plain,
( ( divide(divide(identity,idQ_idQa),a) = idQa )
| ~ less_equal(divide(divide(identity,idQ_idQa),a),idQa) ),
inference(demodulation,[status(thm)],[c_5625,c_10424]) ).
tcf(c_10454,plain,
( ( divide(idQa_Q__idQ_idQb,idQ_idQb) = idQa_Q__idQ_idQb )
| ~ less_equal(divide(idQa_Q__idQ_idQb,idQ_idQb),idQa_Q__idQ_idQb) ),
inference(demodulation,[status(thm)],[c_3365,c_10424]) ).
tcf(c_10461,plain,
( ( divide(idQb_Q__idQ_idQa,idQ_idQa) = idQb_Q__idQ_idQa )
| ~ less_equal(divide(idQb_Q__idQ_idQa,idQ_idQa),idQb_Q__idQ_idQa) ),
inference(demodulation,[status(thm)],[c_3805,c_10424]) ).
tcf(c_10470,plain,
divide(idQb_Q__idQ_idQa,idQ_idQa) = idQb_Q__idQ_idQa,
inference(forward_subsumption_resolution,[status(thm)],[c_10461,c_196]) ).
tcf(c_10472,plain,
divide(idQa_Q__idQ_idQb,idQ_idQb) = idQa_Q__idQ_idQb,
inference(forward_subsumption_resolution,[status(thm)],[c_10454,c_196]) ).
tcf(c_10477,plain,
divide(divide(identity,idQ_idQa),a) = idQa,
inference(forward_subsumption_resolution,[status(thm)],[c_10440,c_2315]) ).
tcf(c_10533,plain,
! [X0: $i,X1: $i] :
( ( divide(divide(X0,zero),divide(X1,zero)) = divide(divide(X0,X1),zero) )
| ~ less_equal(divide(divide(X0,X1),zero),divide(divide(X0,zero),X1)) ),
inference(superposition,[status(thm)],[c_10424,c_680]) ).
tcf(c_10586,plain,
! [X0: $i,X1: $i] :
( ( divide(divide(X0,X1),zero) = divide(X0,divide(X1,zero)) )
| ~ less_equal(divide(divide(X0,X1),zero),divide(X0,X1)) ),
inference(light_normalisation,[status(thm)],[c_10533,c_10424]) ).
tcf(c_10587,plain,
! [X0: $i,X1: $i] : divide(divide(X0,X1),zero) = divide(X0,divide(X1,zero)),
inference(forward_subsumption_resolution,[status(thm)],[c_10586,c_196]) ).
tcf(c_10730,plain,
! [X0: $i] : less_equal(divide(idQb_Q__idQ_idQa,divide(X0,idQ_idQa)),divide(divide(idQb_Q__idQ_idQa,X0),idQ_idQa)),
inference(superposition,[status(thm)],[c_10470,c_210]) ).
tcf(c_10867,plain,
! [X0: $i] : less_equal(divide(idQa_Q__idQ_idQb,divide(X0,idQ_idQb)),divide(divide(idQa_Q__idQ_idQb,X0),idQ_idQb)),
inference(superposition,[status(thm)],[c_10472,c_210]) ).
tcf(c_10987,plain,
( ( divide(divide(identity,idQ_idQb),b) = idQb )
| ~ less_equal(divide(divide(identity,idQ_idQb),b),idQb) ),
inference(demodulation,[status(thm)],[c_6842,c_10424]) ).
tcf(c_10988,plain,
divide(divide(identity,idQ_idQb),b) = idQb,
inference(forward_subsumption_resolution,[status(thm)],[c_10987,c_2109]) ).
tcf(c_10994,plain,
divide(idQb,divide(identity,idQ_idQb)) = zero,
inference(superposition,[status(thm)],[c_10988,c_492]) ).
tcf(c_11258,plain,
divide(idQa,divide(identity,idQ_idQa)) = zero,
inference(superposition,[status(thm)],[c_10477,c_492]) ).
tcf(c_11489,plain,
less_equal(divide(idQb_Q__idQ_idQa,divide(divide(identity,idQ_idQb),idQ_idQa)),divide(zero,idQ_idQa)),
inference(superposition,[status(thm)],[c_10994,c_650]) ).
tcf(c_11794,plain,
less_equal(divide(idQa_Q__idQ_idQb,divide(divide(identity,idQ_idQa),idQ_idQb)),divide(zero,idQ_idQb)),
inference(superposition,[status(thm)],[c_11258,c_648]) ).
tcf(c_12444,plain,
! [X0: $i] : less_equal(divide(X0,idQa),divide(divide(X0,idQa_Q__idQ_idQb),idQa)),
inference(demodulation,[status(thm)],[c_665,c_10424,c_10587]) ).
tcf(c_12457,plain,
! [X0: $i] : less_equal(divide(divide(idQa_Q__idQ_idQb,X0),idQa),divide(zero,idQa)),
inference(superposition,[status(thm)],[c_492,c_12444]) ).
tcf(c_13055,plain,
! [X0: $i] : less_equal(divide(divide(idQa_Q__idQ_idQb,X0),idQa),zero),
inference(demodulation,[status(thm)],[c_12457,c_490]) ).
tcf(c_13068,plain,
! [X0: $i] : divide(divide(idQa_Q__idQ_idQb,X0),idQa) = zero,
inference(superposition,[status(thm)],[c_13055,c_502]) ).
tcf(c_13096,plain,
! [X0: $i] : less_equal(divide(divide(divide(idQa_Q__idQ_idQb,X0),idQ_idQb),idQa_Q__idQ_idQb),divide(zero,idQ_idQb)),
inference(superposition,[status(thm)],[c_13068,c_659]) ).
tcf(c_13956,plain,
! [X0: $i] : less_equal(divide(X0,idQb),divide(divide(X0,idQb_Q__idQ_idQa),idQb)),
inference(demodulation,[status(thm)],[c_666,c_10424,c_10587]) ).
tcf(c_13969,plain,
! [X0: $i] : less_equal(divide(divide(idQb_Q__idQ_idQa,X0),idQb),divide(zero,idQb)),
inference(superposition,[status(thm)],[c_492,c_13956]) ).
tcf(c_14584,plain,
! [X0: $i] : less_equal(divide(divide(idQb_Q__idQ_idQa,X0),idQb),zero),
inference(demodulation,[status(thm)],[c_13969,c_490]) ).
tcf(c_14598,plain,
! [X0: $i] : divide(divide(idQb_Q__idQ_idQa,X0),idQb) = zero,
inference(superposition,[status(thm)],[c_14584,c_502]) ).
tcf(c_14631,plain,
! [X0: $i] : less_equal(divide(divide(divide(idQb_Q__idQ_idQa,X0),idQ_idQa),idQb_Q__idQ_idQa),divide(zero,idQ_idQa)),
inference(superposition,[status(thm)],[c_14598,c_661]) ).
tcf(c_19462,plain,
! [X0: $i] : less_equal(divide(X0,b),divide(divide(X0,idQ_idQb),b)),
inference(demodulation,[status(thm)],[c_4284,c_10424,c_10587]) ).
tcf(c_19468,plain,
less_equal(idQb,divide(divide(idQb,idQ_idQb),b)),
inference(superposition,[status(thm)],[c_6618,c_19462]) ).
tcf(c_19522,plain,
divide(divide(idQb,idQ_idQb),b) = idQb,
inference(superposition,[status(thm)],[c_19468,c_2168]) ).
tcf(c_19560,plain,
( ( divide(divide(idQb,idQ_idQb),b) = divide(idQb,idQ_idQb) )
| ~ less_equal(divide(idQb,idQ_idQb),idQb) ),
inference(superposition,[status(thm)],[c_19522,c_504]) ).
tcf(c_19586,plain,
( ( divide(idQb,idQ_idQb) = idQb )
| ~ less_equal(divide(idQb,idQ_idQb),idQb) ),
inference(light_normalisation,[status(thm)],[c_19560,c_19522]) ).
tcf(c_19587,plain,
divide(idQb,idQ_idQb) = idQb,
inference(forward_subsumption_resolution,[status(thm)],[c_19586,c_196]) ).
tcf(c_19601,plain,
divide(idQa_Q__idQ_idQb,idQb) = zero,
inference(demodulation,[status(thm)],[c_3518,c_19587]) ).
tcf(c_19603,plain,
! [X0: $i] : less_equal(divide(X0,idQ_idQb),idQb),
inference(demodulation,[status(thm)],[c_3527,c_19587]) ).
tcf(c_19604,plain,
! [X0: $i] : divide(divide(X0,idQ_idQb),idQb) = zero,
inference(demodulation,[status(thm)],[c_1791,c_19587]) ).
tcf(c_19795,plain,
! [X0: $i,X1: $i] : divide(divide(divide(idQb_Q__idQ_idQa,X0),X1),divide(divide(idQb,X0),X1)) = zero,
inference(demodulation,[status(thm)],[c_2748,c_490]) ).
tcf(c_19853,plain,
! [X0: $i,X1: $i] : less_equal(divide(divide(idQb_Q__idQ_idQa,X0),X1),divide(divide(idQb,X0),X1)),
inference(superposition,[status(thm)],[c_19795,c_219]) ).
tcf(c_20444,plain,
less_equal(divide(divide(idQa_Q__idQ_idQb,idQ_idQa),idQb_Q__idQ_idQa),divide(zero,idQ_idQa)),
inference(superposition,[status(thm)],[c_19601,c_661]) ).
tcf(c_20710,plain,
! [X0: $i] : less_equal(divide(divide(divide(X0,idQ_idQb),idQ_idQa),idQb_Q__idQ_idQa),divide(zero,idQ_idQa)),
inference(superposition,[status(thm)],[c_19604,c_661]) ).
tcf(c_22214,plain,
less_equal(divide(divide(idQa_Q__idQ_idQb,idQ_idQa),idQb_Q__idQ_idQa),zero),
inference(demodulation,[status(thm)],[c_20444,c_490]) ).
tcf(c_22217,plain,
divide(divide(idQa_Q__idQ_idQb,idQ_idQa),idQb_Q__idQ_idQa) = zero,
inference(superposition,[status(thm)],[c_22214,c_502]) ).
tcf(c_22241,plain,
( ( divide(divide(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa),divide(idQ_idQa,idQb_Q__idQ_idQa)) = divide(divide(idQa_Q__idQ_idQb,idQ_idQa),idQb_Q__idQ_idQa) )
| ~ less_equal(zero,divide(divide(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa),divide(idQ_idQa,idQb_Q__idQ_idQa))) ),
inference(superposition,[status(thm)],[c_22217,c_680]) ).
tcf(c_22257,plain,
( ( divide(divide(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa),divide(idQ_idQa,idQb_Q__idQ_idQa)) = zero )
| ~ less_equal(zero,divide(divide(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa),divide(idQ_idQa,idQb_Q__idQ_idQa))) ),
inference(light_normalisation,[status(thm)],[c_22241,c_22217]) ).
tcf(c_22258,plain,
divide(divide(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa),divide(idQ_idQa,idQb_Q__idQ_idQa)) = zero,
inference(forward_subsumption_resolution,[status(thm)],[c_22257,c_69]) ).
tcf(c_23347,plain,
( ( divide(divide(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa),divide(idQ_idQa,idQb_Q__idQ_idQa)) = divide(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa) )
| ~ less_equal(divide(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa),zero) ),
inference(superposition,[status(thm)],[c_22258,c_504]) ).
tcf(c_23367,plain,
( ( divide(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa) = zero )
| ~ less_equal(divide(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa),zero) ),
inference(light_normalisation,[status(thm)],[c_23347,c_22258]) ).
tcf(c_23985,plain,
! [X0: $i,X1: $i] : divide(divide(divide(idQa_Q__idQ_idQb,X0),X1),divide(divide(idQa,X0),X1)) = zero,
inference(demodulation,[status(thm)],[c_2857,c_490]) ).
tcf(c_24053,plain,
! [X0: $i,X1: $i] : less_equal(divide(divide(idQa_Q__idQ_idQb,X0),X1),divide(divide(idQa,X0),X1)),
inference(superposition,[status(thm)],[c_23985,c_219]) ).
tcf(c_24291,plain,
! [X0: $i] : less_equal(divide(X0,a),divide(divide(X0,idQ_idQa),a)),
inference(demodulation,[status(thm)],[c_4695,c_10424,c_10587]) ).
tcf(c_24311,plain,
! [X0: $i] :
( ( divide(divide(X0,idQ_idQa),a) = divide(X0,a) )
| ~ less_equal(divide(divide(X0,idQ_idQa),a),divide(X0,a)) ),
inference(superposition,[status(thm)],[c_24291,c_70]) ).
tcf(c_24461,plain,
( ( divide(divide(idQa,idQ_idQa),a) = divide(idQa,a) )
| ~ less_equal(divide(divide(idQa,idQ_idQa),a),idQa) ),
inference(superposition,[status(thm)],[c_5518,c_24311]) ).
tcf(c_24470,plain,
( ( divide(divide(idQa,idQ_idQa),a) = idQa )
| ~ less_equal(divide(divide(idQa,idQ_idQa),a),idQa) ),
inference(light_normalisation,[status(thm)],[c_24461,c_5518]) ).
tcf(c_24471,plain,
divide(divide(idQa,idQ_idQa),a) = idQa,
inference(forward_subsumption_resolution,[status(thm)],[c_24470,c_2315]) ).
tcf(c_24583,plain,
( ( divide(divide(idQa,idQ_idQa),a) = divide(idQa,idQ_idQa) )
| ~ less_equal(divide(idQa,idQ_idQa),idQa) ),
inference(superposition,[status(thm)],[c_24471,c_504]) ).
tcf(c_24616,plain,
( ( divide(idQa,idQ_idQa) = idQa )
| ~ less_equal(divide(idQa,idQ_idQa),idQa) ),
inference(light_normalisation,[status(thm)],[c_24583,c_24471]) ).
tcf(c_24617,plain,
divide(idQa,idQ_idQa) = idQa,
inference(forward_subsumption_resolution,[status(thm)],[c_24616,c_196]) ).
tcf(c_24633,plain,
divide(idQb_Q__idQ_idQa,idQa) = zero,
inference(demodulation,[status(thm)],[c_3111,c_24617]) ).
tcf(c_24635,plain,
! [X0: $i] : less_equal(divide(X0,idQ_idQa),idQa),
inference(demodulation,[status(thm)],[c_3120,c_24617]) ).
tcf(c_24636,plain,
! [X0: $i] : divide(divide(X0,idQ_idQa),idQa) = zero,
inference(demodulation,[status(thm)],[c_1626,c_24617]) ).
tcf(c_24774,plain,
less_equal(divide(divide(idQb_Q__idQ_idQa,idQ_idQb),idQa_Q__idQ_idQb),divide(zero,idQ_idQb)),
inference(superposition,[status(thm)],[c_24633,c_659]) ).
tcf(c_25034,plain,
! [X0: $i] : less_equal(divide(divide(divide(X0,idQ_idQa),idQ_idQb),idQa_Q__idQ_idQb),divide(zero,idQ_idQb)),
inference(superposition,[status(thm)],[c_24636,c_659]) ).
tcf(c_26113,plain,
less_equal(divide(divide(idQb_Q__idQ_idQa,idQ_idQb),idQa_Q__idQ_idQb),zero),
inference(demodulation,[status(thm)],[c_24774,c_490]) ).
tcf(c_26116,plain,
divide(divide(idQb_Q__idQ_idQa,idQ_idQb),idQa_Q__idQ_idQb) = zero,
inference(superposition,[status(thm)],[c_26113,c_502]) ).
tcf(c_26133,plain,
( ( divide(divide(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb),divide(idQ_idQb,idQa_Q__idQ_idQb)) = divide(divide(idQb_Q__idQ_idQa,idQ_idQb),idQa_Q__idQ_idQb) )
| ~ less_equal(zero,divide(divide(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb),divide(idQ_idQb,idQa_Q__idQ_idQb))) ),
inference(superposition,[status(thm)],[c_26116,c_680]) ).
tcf(c_26151,plain,
( ( divide(divide(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb),divide(idQ_idQb,idQa_Q__idQ_idQb)) = zero )
| ~ less_equal(zero,divide(divide(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb),divide(idQ_idQb,idQa_Q__idQ_idQb))) ),
inference(light_normalisation,[status(thm)],[c_26133,c_26116]) ).
tcf(c_26152,plain,
divide(divide(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb),divide(idQ_idQb,idQa_Q__idQ_idQb)) = zero,
inference(forward_subsumption_resolution,[status(thm)],[c_26151,c_69]) ).
tcf(c_27801,plain,
( ( divide(divide(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb),divide(idQ_idQb,idQa_Q__idQ_idQb)) = divide(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb) )
| ~ less_equal(divide(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb),zero) ),
inference(superposition,[status(thm)],[c_26152,c_504]) ).
tcf(c_27822,plain,
( ( divide(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb) = zero )
| ~ less_equal(divide(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb),zero) ),
inference(light_normalisation,[status(thm)],[c_27801,c_26152]) ).
tcf(c_35567,plain,
! [X0: $i] : less_equal(divide(idQb_Q__idQ_idQa,zero),divide(divide(idQb_Q__idQ_idQa,divide(idQ_idQa,X0)),idQ_idQa)),
inference(superposition,[status(thm)],[c_492,c_10730]) ).
tcf(c_36163,plain,
! [X0: $i] : less_equal(divide(idQa_Q__idQ_idQb,zero),divide(divide(idQa_Q__idQ_idQb,divide(idQ_idQb,X0)),idQ_idQb)),
inference(superposition,[status(thm)],[c_492,c_10867]) ).
tcf(c_37289,plain,
less_equal(divide(idQb_Q__idQ_idQa,divide(divide(identity,idQ_idQb),idQ_idQa)),zero),
inference(demodulation,[status(thm)],[c_11489,c_490]) ).
tcf(c_37292,plain,
divide(idQb_Q__idQ_idQa,divide(divide(identity,idQ_idQb),idQ_idQa)) = zero,
inference(superposition,[status(thm)],[c_37289,c_502]) ).
tcf(c_37299,plain,
less_equal(idQb_Q__idQ_idQa,divide(divide(identity,idQ_idQb),idQ_idQa)),
inference(superposition,[status(thm)],[c_37292,c_219]) ).
tcf(c_37407,plain,
( ( divide(divide(identity,idQ_idQb),idQ_idQa) = idQb_Q__idQ_idQa )
| ~ less_equal(divide(divide(identity,idQ_idQb),idQ_idQa),idQb_Q__idQ_idQa) ),
inference(superposition,[status(thm)],[c_37299,c_70]) ).
tcf(c_37646,plain,
less_equal(divide(idQa_Q__idQ_idQb,divide(divide(identity,idQ_idQa),idQ_idQb)),zero),
inference(demodulation,[status(thm)],[c_11794,c_490]) ).
tcf(c_37649,plain,
divide(idQa_Q__idQ_idQb,divide(divide(identity,idQ_idQa),idQ_idQb)) = zero,
inference(superposition,[status(thm)],[c_37646,c_502]) ).
tcf(c_37656,plain,
less_equal(idQa_Q__idQ_idQb,divide(divide(identity,idQ_idQa),idQ_idQb)),
inference(superposition,[status(thm)],[c_37649,c_219]) ).
tcf(c_37883,plain,
( ( divide(divide(identity,idQ_idQa),idQ_idQb) = idQa_Q__idQ_idQb )
| ~ less_equal(divide(divide(identity,idQ_idQa),idQ_idQb),idQa_Q__idQ_idQb) ),
inference(superposition,[status(thm)],[c_37656,c_70]) ).
tcf(c_38404,plain,
! [X0: $i] : less_equal(divide(divide(divide(idQa_Q__idQ_idQb,X0),idQ_idQb),idQa_Q__idQ_idQb),zero),
inference(demodulation,[status(thm)],[c_13096,c_490]) ).
tcf(c_38424,plain,
! [X0: $i] : divide(divide(divide(idQa_Q__idQ_idQb,X0),idQ_idQb),idQa_Q__idQ_idQb) = zero,
inference(superposition,[status(thm)],[c_38404,c_502]) ).
tcf(c_38596,plain,
! [X0: $i] : less_equal(divide(divide(idQa_Q__idQ_idQb,X0),idQ_idQb),idQa_Q__idQ_idQb),
inference(superposition,[status(thm)],[c_38424,c_219]) ).
tcf(c_38810,plain,
! [X0: $i] :
( ( divide(divide(idQa_Q__idQ_idQb,X0),idQ_idQb) = idQa_Q__idQ_idQb )
| ~ less_equal(idQa_Q__idQ_idQb,divide(divide(idQa_Q__idQ_idQb,X0),idQ_idQb)) ),
inference(superposition,[status(thm)],[c_38596,c_70]) ).
tcf(c_39423,plain,
! [X0: $i] : less_equal(divide(divide(divide(idQb_Q__idQ_idQa,X0),idQ_idQa),idQb_Q__idQ_idQa),zero),
inference(demodulation,[status(thm)],[c_14631,c_490]) ).
tcf(c_39443,plain,
! [X0: $i] : divide(divide(divide(idQb_Q__idQ_idQa,X0),idQ_idQa),idQb_Q__idQ_idQa) = zero,
inference(superposition,[status(thm)],[c_39423,c_502]) ).
tcf(c_39469,plain,
! [X0: $i] : less_equal(divide(divide(idQb_Q__idQ_idQa,X0),idQ_idQa),idQb_Q__idQ_idQa),
inference(superposition,[status(thm)],[c_39443,c_219]) ).
tcf(c_39613,plain,
! [X0: $i] :
( ( divide(divide(idQb_Q__idQ_idQa,X0),idQ_idQa) = idQb_Q__idQ_idQa )
| ~ less_equal(idQb_Q__idQ_idQa,divide(divide(idQb_Q__idQ_idQa,X0),idQ_idQa)) ),
inference(superposition,[status(thm)],[c_39469,c_70]) ).
tcf(c_47431,plain,
! [X0: $i] : less_equal(divide(divide(divide(X0,idQ_idQb),idQ_idQa),idQb_Q__idQ_idQa),zero),
inference(demodulation,[status(thm)],[c_20710,c_490]) ).
tcf(c_47451,plain,
! [X0: $i] : divide(divide(divide(X0,idQ_idQb),idQ_idQa),idQb_Q__idQ_idQa) = zero,
inference(superposition,[status(thm)],[c_47431,c_502]) ).
tcf(c_47475,plain,
! [X0: $i] : less_equal(divide(divide(X0,idQ_idQb),idQ_idQa),idQb_Q__idQ_idQa),
inference(superposition,[status(thm)],[c_47451,c_219]) ).
tcf(c_47516,plain,
divide(divide(identity,idQ_idQb),idQ_idQa) = idQb_Q__idQ_idQa,
inference(backward_subsumption_resolution,[status(thm)],[c_37407,c_47475]) ).
tcf(c_47743,plain,
less_equal(divide(divide(identity,idQ_idQa),divide(idQ_idQb,idQ_idQa)),idQb_Q__idQ_idQa),
inference(superposition,[status(thm)],[c_47516,c_210]) ).
tcf(c_60625,plain,
! [X0: $i] : less_equal(divide(divide(divide(X0,idQ_idQa),idQ_idQb),idQa_Q__idQ_idQb),zero),
inference(demodulation,[status(thm)],[c_25034,c_490]) ).
tcf(c_60646,plain,
! [X0: $i] : divide(divide(divide(X0,idQ_idQa),idQ_idQb),idQa_Q__idQ_idQb) = zero,
inference(superposition,[status(thm)],[c_60625,c_502]) ).
tcf(c_60672,plain,
! [X0: $i] : less_equal(divide(divide(X0,idQ_idQa),idQ_idQb),idQa_Q__idQ_idQb),
inference(superposition,[status(thm)],[c_60646,c_219]) ).
tcf(c_60722,plain,
divide(divide(identity,idQ_idQa),idQ_idQb) = idQa_Q__idQ_idQb,
inference(backward_subsumption_resolution,[status(thm)],[c_37883,c_60672]) ).
tcf(c_61141,plain,
less_equal(divide(divide(identity,idQ_idQb),divide(idQ_idQa,idQ_idQb)),idQa_Q__idQ_idQb),
inference(superposition,[status(thm)],[c_60722,c_210]) ).
tcf(c_78674,plain,
! [X0: $i] : less_equal(idQb_Q__idQ_idQa,divide(divide(idQb_Q__idQ_idQa,divide(idQ_idQa,X0)),idQ_idQa)),
inference(demodulation,[status(thm)],[c_35567,c_10424]) ).
tcf(c_78702,plain,
! [X0: $i] : divide(divide(idQb_Q__idQ_idQa,divide(idQ_idQa,X0)),idQ_idQa) = idQb_Q__idQ_idQa,
inference(superposition,[status(thm)],[c_78674,c_39613]) ).
tcf(c_78737,plain,
! [X0: $i] :
( ( divide(divide(idQb_Q__idQ_idQa,divide(idQ_idQa,X0)),idQ_idQa) = divide(idQb_Q__idQ_idQa,divide(idQ_idQa,X0)) )
| ~ less_equal(divide(idQb_Q__idQ_idQa,divide(idQ_idQa,X0)),idQb_Q__idQ_idQa) ),
inference(superposition,[status(thm)],[c_78702,c_504]) ).
tcf(c_78794,plain,
! [X0: $i] :
( ( divide(idQb_Q__idQ_idQa,divide(idQ_idQa,X0)) = idQb_Q__idQ_idQa )
| ~ less_equal(divide(idQb_Q__idQ_idQa,divide(idQ_idQa,X0)),idQb_Q__idQ_idQa) ),
inference(light_normalisation,[status(thm)],[c_78737,c_78702]) ).
tcf(c_78795,plain,
! [X0: $i] : divide(idQb_Q__idQ_idQa,divide(idQ_idQa,X0)) = idQb_Q__idQ_idQa,
inference(forward_subsumption_resolution,[status(thm)],[c_78794,c_196]) ).
tcf(c_80324,plain,
! [X0: $i,X1: $i] : less_equal(divide(idQb_Q__idQ_idQa,X0),divide(divide(idQb,divide(idQ_idQa,X1)),X0)),
inference(superposition,[status(thm)],[c_78795,c_19853]) ).
tcf(c_86396,plain,
! [X0: $i] : less_equal(idQa_Q__idQ_idQb,divide(divide(idQa_Q__idQ_idQb,divide(idQ_idQb,X0)),idQ_idQb)),
inference(demodulation,[status(thm)],[c_36163,c_10424]) ).
tcf(c_86424,plain,
! [X0: $i] : divide(divide(idQa_Q__idQ_idQb,divide(idQ_idQb,X0)),idQ_idQb) = idQa_Q__idQ_idQb,
inference(superposition,[status(thm)],[c_86396,c_38810]) ).
tcf(c_86461,plain,
! [X0: $i] :
( ( divide(divide(idQa_Q__idQ_idQb,divide(idQ_idQb,X0)),idQ_idQb) = divide(idQa_Q__idQ_idQb,divide(idQ_idQb,X0)) )
| ~ less_equal(divide(idQa_Q__idQ_idQb,divide(idQ_idQb,X0)),idQa_Q__idQ_idQb) ),
inference(superposition,[status(thm)],[c_86424,c_504]) ).
tcf(c_86517,plain,
! [X0: $i] :
( ( divide(idQa_Q__idQ_idQb,divide(idQ_idQb,X0)) = idQa_Q__idQ_idQb )
| ~ less_equal(divide(idQa_Q__idQ_idQb,divide(idQ_idQb,X0)),idQa_Q__idQ_idQb) ),
inference(light_normalisation,[status(thm)],[c_86461,c_86424]) ).
tcf(c_86518,plain,
! [X0: $i] : divide(idQa_Q__idQ_idQb,divide(idQ_idQb,X0)) = idQa_Q__idQ_idQb,
inference(forward_subsumption_resolution,[status(thm)],[c_86517,c_196]) ).
tcf(c_86766,plain,
! [X0: $i,X1: $i] : less_equal(divide(idQa_Q__idQ_idQb,X0),divide(divide(idQa,divide(idQ_idQb,X1)),X0)),
inference(superposition,[status(thm)],[c_86518,c_24053]) ).
tcf(c_117870,plain,
! [X0: $i,X1: $i] : divide(divide(X0,X1),divide(identity,X1)) = zero,
inference(demodulation,[status(thm)],[c_1158,c_490]) ).
tcf(c_118188,plain,
! [X0: $i,X1: $i] : less_equal(divide(X0,X1),divide(identity,X1)),
inference(superposition,[status(thm)],[c_117870,c_219]) ).
tcf(c_118923,plain,
! [X0: $i,X1: $i] :
( ( divide(X1,X0) = divide(identity,X0) )
| ~ less_equal(divide(identity,X0),divide(X1,X0)) ),
inference(superposition,[status(thm)],[c_118188,c_70]) ).
tcf(c_119016,plain,
( ( divide(identity,idQ_idQa) = divide(idQa,idQ_idQa) )
| ~ less_equal(divide(identity,idQ_idQa),idQa) ),
inference(superposition,[status(thm)],[c_24617,c_118923]) ).
tcf(c_119018,plain,
( ( divide(identity,idQ_idQb) = divide(idQb,idQ_idQb) )
| ~ less_equal(divide(identity,idQ_idQb),idQb) ),
inference(superposition,[status(thm)],[c_19587,c_118923]) ).
tcf(c_119296,plain,
( ( divide(identity,idQ_idQb) = idQb )
| ~ less_equal(divide(identity,idQ_idQb),idQb) ),
inference(light_normalisation,[status(thm)],[c_119018,c_19587]) ).
tcf(c_119297,plain,
divide(identity,idQ_idQb) = idQb,
inference(forward_subsumption_resolution,[status(thm)],[c_119296,c_19603]) ).
tcf(c_119299,plain,
( ( divide(identity,idQ_idQa) = idQa )
| ~ less_equal(divide(identity,idQ_idQa),idQa) ),
inference(light_normalisation,[status(thm)],[c_119016,c_24617]) ).
tcf(c_119300,plain,
divide(identity,idQ_idQa) = idQa,
inference(forward_subsumption_resolution,[status(thm)],[c_119299,c_24635]) ).
tcf(c_119822,plain,
less_equal(divide(idQb,divide(idQ_idQa,idQ_idQb)),idQa_Q__idQ_idQb),
inference(demodulation,[status(thm)],[c_61141,c_119297]) ).
tcf(c_119864,plain,
less_equal(divide(idQa,divide(idQ_idQb,idQ_idQa)),idQb_Q__idQ_idQa),
inference(demodulation,[status(thm)],[c_47743,c_119300]) ).
tcf(c_120632,plain,
divide(divide(idQb,divide(idQ_idQa,idQ_idQb)),idQa_Q__idQ_idQb) = zero,
inference(superposition,[status(thm)],[c_119822,c_220]) ).
tcf(c_120640,plain,
divide(divide(idQa,divide(idQ_idQb,idQ_idQa)),idQb_Q__idQ_idQa) = zero,
inference(superposition,[status(thm)],[c_119864,c_220]) ).
tcf(c_120678,plain,
less_equal(divide(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb),zero),
inference(superposition,[status(thm)],[c_120632,c_80324]) ).
tcf(c_120859,plain,
less_equal(divide(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa),zero),
inference(superposition,[status(thm)],[c_120640,c_86766]) ).
tcf(c_120885,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_120859,c_120678,c_27822,c_23367,c_10227,c_736,c_642,c_641,c_636,c_80]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : HEN011-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.17/0.42 % Computer : n002.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Wed Sep 23 16:20:03 UTC 2026
% 0.17/0.42 % CPUTime :
% 0.17/0.43 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.17/0.49 Running first-order theorem proving
% 0.17/0.49 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.24/0.50
% 0.24/0.50 % ======== iProver multi-core TPTP/SMT =========
% 0.24/0.50
% 0.24/0.50 % Detected problem language: tptp
% 0.24/0.52 % Proving...
% 28.03/6.02 % SZS status Started for theBenchmark.p
% 28.03/6.02 % SZS status Unsatisfiable for theBenchmark.p
% 28.03/6.02
% 28.03/6.02 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 28.03/6.02
% 28.03/6.02 % ------ iProver source info
% 28.03/6.02
% 28.03/6.02 % git: date: 2026-07-19 20:42:38 +0200
% 28.03/6.02 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 28.03/6.02 % git: non_committed_changes: false
% 28.03/6.02
% 28.03/6.02 % ------ Parsing...% successful
% 28.03/6.02
% 28.03/6.02
% 28.03/6.02 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 28.03/6.02
% 28.03/6.02 % ------ Preprocessing... sup_sim: 4 sf_s rm: 1 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 28.03/6.02
% 28.03/6.02 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 28.03/6.02
% 28.03/6.02 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 28.03/6.02 % ------ Proving...
% 28.03/6.02 % ------ Problem Properties
% 28.03/6.02
% 28.03/6.02 %
% 28.03/6.02 % clauses 14
% 28.03/6.02 % conjectures 1
% 28.03/6.02 % EPR 4
% 28.03/6.02 % Horn 14
% 28.03/6.02 % unary 11
% 28.03/6.02 % binary 2
% 28.03/6.02 % lits 18
% 28.03/6.02 % lits eq 10
% 28.03/6.02 % fd_pure 0
% 28.03/6.02 % fd_pseudo 0
% 28.03/6.02 % fd_cond 0
% 28.03/6.02 % fd_pseudo_cond 1
% 28.03/6.02 % AC symbols 0
% 28.03/6.02
% 28.03/6.02 % ------ Schedule dynamic 5 is on
% 28.03/6.02
% 28.03/6.02 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 28.03/6.02
% 28.03/6.02
% 28.03/6.02 % ------
% 28.03/6.02 % Current options:
% 28.03/6.02 % ------
% 28.03/6.02
% 28.03/6.02
% 28.03/6.02 %
% 28.03/6.02
% 28.03/6.02 % ------ Proving...
% 28.03/6.02 %
% 28.03/6.02
% 28.03/6.02 % SZS status Unsatisfiable for theBenchmark.p
% 28.03/6.02
% 28.03/6.02 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 28.03/6.03
% 28.03/6.03
%------------------------------------------------------------------------------