%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : HEN011-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:31:50 AM UTC 2026
% Result : Unsatisfiable 87.82s 24.97s
% Output : CNFRefutation 87.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 16
% Syntax : Number of clauses : 237 ( 149 unt; 0 nHn; 166 RR)
% Number of literals : 406 ( 62 equ; 172 neg)
% Maximal clause size : 6 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 10 con; 0-2 aty)
% Number of variables : 328 ( 66 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(identity_divide_a,hypothesis,
quotient(identity,a,idQa) ).
cnf(identity_divide_b,hypothesis,
quotient(identity,b,idQb) ).
cnf(identity_divide_idQb,hypothesis,
quotient(identity,idQb,'idQ$uidQb') ).
cnf(idQa_divide_idQ_idQb,hypothesis,
quotient(idQa,'idQ$uidQb','idQa$uQ$u$uidQ$uidQb') ).
cnf(identity_divide_idQa,hypothesis,
quotient(identity,idQa,'idQ$uidQa') ).
cnf(idQb_divide_idQ_idQa,hypothesis,
quotient(idQb,'idQ$uidQa','idQb$uQ$u$uidQ$uidQa') ).
cnf(prove_idQa_Q__idQ_idQb_equals_idQb_Q__idQ_idQa,negated_conjecture,
'idQa$uQ$u$uidQ$uidQb' != 'idQb$uQ$u$uidQ$uidQa' ).
cnf(quotient_less_equal,axiom,
( quotient(X0,X1,zero)
| ~ 'less$uequal'(X0,X1) ) ).
cnf(less_equal_quotient,axiom,
( 'less$uequal'(X0,X1)
| ~ quotient(X0,X1,zero) ) ).
cnf(divisor_existence,axiom,
( 'less$uequal'(X2,X0)
| ~ quotient(X0,X1,X2) ) ).
cnf(quotient_property,axiom,
( 'less$uequal'(X6,X7)
| ~ quotient(X2,X3,X7)
| ~ quotient(X5,X4,X6)
| ~ quotient(X0,X3,X5)
| ~ quotient(X1,X3,X4)
| ~ quotient(X0,X1,X2) ) ).
cnf(zero_is_smallest,axiom,
'less$uequal'(zero,X0) ).
cnf(less_equal_and_equal,axiom,
( X0 = X1
| ~ 'less$uequal'(X1,X0)
| ~ 'less$uequal'(X0,X1) ) ).
cnf(identity_is_largest,axiom,
'less$uequal'(X0,identity) ).
cnf(closure,axiom,
quotient(X0,X1,divide(X0,X1)) ).
cnf(well_defined,axiom,
( X2 = X3
| ~ quotient(X0,X1,X3)
| ~ quotient(X0,X1,X2) ) ).
cnf(c0,plain,
quotient(identity,a,idQa),
inference(clausification,[status(esa)],[identity_divide_a]) ).
cnf(c1,plain,
quotient(identity,b,idQb),
inference(clausification,[status(esa)],[identity_divide_b]) ).
cnf(c2,plain,
quotient(identity,idQb,'idQ$uidQb'),
inference(clausification,[status(esa)],[identity_divide_idQb]) ).
cnf(c3,plain,
quotient(idQa,'idQ$uidQb','idQa$uQ$u$uidQ$uidQb'),
inference(clausification,[status(esa)],[idQa_divide_idQ_idQb]) ).
cnf(c4,plain,
quotient(identity,idQa,'idQ$uidQa'),
inference(clausification,[status(esa)],[identity_divide_idQa]) ).
cnf(c5,plain,
quotient(idQb,'idQ$uidQa','idQb$uQ$u$uidQ$uidQa'),
inference(clausification,[status(esa)],[idQb_divide_idQ_idQa]) ).
cnf(c6,plain,
'idQb$uQ$u$uidQ$uidQa' != 'idQa$uQ$u$uidQ$uidQb',
inference(clausification,[status(esa)],[prove_idQa_Q__idQ_idQb_equals_idQb_Q__idQ_idQa]) ).
cnf(c7,plain,
( quotient(X0,X1,zero)
| ~ 'less$uequal'(X0,X1) ),
inference(clausification,[status(esa)],[quotient_less_equal]) ).
cnf(c8,plain,
( 'less$uequal'(X0,X1)
| ~ quotient(X0,X1,zero) ),
inference(clausification,[status(esa)],[less_equal_quotient]) ).
cnf(c9,plain,
( 'less$uequal'(X2,X0)
| ~ quotient(X0,X1,X2) ),
inference(clausification,[status(esa)],[divisor_existence]) ).
cnf(c10,plain,
( ~ quotient(X7,X5,X3)
| ~ quotient(X6,X5,X2)
| ~ quotient(X6,X7,X4)
| ~ quotient(X4,X5,X1)
| ~ quotient(X2,X3,X0)
| 'less$uequal'(X0,X1) ),
inference(clausification,[status(esa)],[quotient_property]) ).
cnf(c11,plain,
'less$uequal'(zero,X0),
inference(clausification,[status(esa)],[zero_is_smallest]) ).
cnf(c12,plain,
( X0 = X1
| ~ 'less$uequal'(X1,X0)
| ~ 'less$uequal'(X0,X1) ),
inference(clausification,[status(esa)],[less_equal_and_equal]) ).
cnf(c13,plain,
'less$uequal'(X0,identity),
inference(clausification,[status(esa)],[identity_is_largest]) ).
cnf(c14,plain,
quotient(X0,X1,divide(X0,X1)),
inference(clausification,[status(esa)],[closure]) ).
cnf(c15,plain,
( X2 = X3
| ~ quotient(X0,X1,X3)
| ~ quotient(X0,X1,X2) ),
inference(clausification,[status(esa)],[well_defined]) ).
cnf(d0,plain,
'less$uequal'(divide(X0,X1),X0),
inference(resolution,[status(thm)],[c14,c9]) ).
cnf(d1,plain,
( ~ 'less$uequal'(X0,zero)
| X0 = zero ),
inference(resolution,[status(thm)],[c12,c11]) ).
cnf(d2,plain,
divide(zero,X0) = zero,
inference(resolution,[status(thm)],[d1,d0]) ).
cnf(d3,plain,
( 'less$uequal'(X3,X1)
| ~ quotient(X4,'idQ$uidQa',X2)
| ~ quotient(X4,idQb,X0)
| ~ quotient(X2,'idQb$uQ$u$uidQ$uidQa',X3)
| ~ quotient(X0,'idQ$uidQa',X1) ),
inference(resolution,[status(thm)],[c10,c5]) ).
cnf(d4,plain,
( 'less$uequal'(X2,X3)
| ~ quotient(divide(X0,idQb),'idQ$uidQa',X3)
| ~ quotient(X1,'idQb$uQ$u$uidQ$uidQa',X2)
| ~ quotient(X0,'idQ$uidQa',X1) ),
inference(resolution,[status(thm)],[d3,c14]) ).
cnf(d5,plain,
( 'less$uequal'(divide(X1,'idQb$uQ$u$uidQ$uidQa'),X2)
| ~ quotient(divide(X0,idQb),'idQ$uidQa',X2)
| ~ quotient(X0,'idQ$uidQa',X1) ),
inference(resolution,[status(thm)],[d4,c14]) ).
cnf(d6,plain,
( 'less$uequal'(divide(divide(X0,'idQ$uidQa'),'idQb$uQ$u$uidQ$uidQa'),X1)
| ~ quotient(divide(X0,idQb),'idQ$uidQa',X1) ),
inference(resolution,[status(thm)],[d5,c14]) ).
cnf(d7,plain,
'less$uequal'(divide(divide(X0,'idQ$uidQa'),'idQb$uQ$u$uidQ$uidQa'),divide(divide(X0,idQb),'idQ$uidQa')),
inference(resolution,[status(thm)],[d6,c14]) ).
cnf(d8,plain,
( 'less$uequal'(X5,X2)
| ~ quotient(X6,X1,X3)
| ~ quotient(X6,X4,X0)
| ~ quotient(X3,divide(X4,X1),X5)
| ~ quotient(X0,X1,X2) ),
inference(resolution,[status(thm)],[c14,c10]) ).
cnf(d9,plain,
( 'less$uequal'(X4,X5)
| ~ quotient(divide(X0,X3),X1,X5)
| ~ quotient(X2,divide(X3,X1),X4)
| ~ quotient(X0,X1,X2) ),
inference(resolution,[status(thm)],[d8,c14]) ).
cnf(d10,plain,
( 'less$uequal'(divide(X2,divide(X3,X1)),X4)
| ~ quotient(divide(X0,X3),X1,X4)
| ~ quotient(X0,X1,X2) ),
inference(resolution,[status(thm)],[d9,c14]) ).
cnf(d11,plain,
( 'less$uequal'(divide('idQa$uQ$u$uidQ$uidQb',divide(X0,'idQ$uidQb')),X1)
| ~ quotient(divide(idQa,X0),'idQ$uidQb',X1) ),
inference(resolution,[status(thm)],[d10,c3]) ).
cnf(d12,plain,
quotient(zero,X0,zero),
inference(resolution,[status(thm)],[c7,c11]) ).
cnf(d13,plain,
quotient(X0,identity,zero),
inference(resolution,[status(thm)],[c7,c13]) ).
cnf(d14,plain,
( 'less$uequal'(X3,X1)
| ~ quotient(X4,idQb,X2)
| ~ quotient(X4,identity,X0)
| ~ quotient(X2,'idQ$uidQb',X3)
| ~ quotient(X0,idQb,X1) ),
inference(resolution,[status(thm)],[c10,c2]) ).
cnf(d15,plain,
( 'less$uequal'(X2,X3)
| ~ quotient(zero,idQb,X3)
| ~ quotient(X1,'idQ$uidQb',X2)
| ~ quotient(X0,idQb,X1) ),
inference(resolution,[status(thm)],[d14,d13]) ).
cnf(d16,plain,
( 'less$uequal'(divide(X1,'idQ$uidQb'),X2)
| ~ quotient(zero,idQb,X2)
| ~ quotient(X0,idQb,X1) ),
inference(resolution,[status(thm)],[d15,c14]) ).
cnf(d17,plain,
( 'less$uequal'(divide(divide(X1,idQb),'idQ$uidQb'),X0)
| ~ quotient(zero,idQb,X0) ),
inference(resolution,[status(thm)],[d16,c14]) ).
cnf(d18,plain,
'less$uequal'(divide(divide(X0,idQb),'idQ$uidQb'),zero),
inference(resolution,[status(thm)],[d17,d12]) ).
cnf(d19,plain,
divide(divide(X0,idQb),'idQ$uidQb') = zero,
inference(resolution,[status(thm)],[d18,d1]) ).
cnf(d20,plain,
quotient(divide(X0,idQb),'idQ$uidQb',zero),
inference(superposition,[status(thm)],[d19,c14]) ).
cnf(d21,plain,
'less$uequal'(divide('idQa$uQ$u$uidQ$uidQb',divide(idQb,'idQ$uidQb')),zero),
inference(resolution,[status(thm)],[d20,d11]) ).
cnf(d22,plain,
divide('idQa$uQ$u$uidQ$uidQb',divide(idQb,'idQ$uidQb')) = zero,
inference(resolution,[status(thm)],[d21,d1]) ).
cnf(d23,plain,
quotient('idQa$uQ$u$uidQ$uidQb',divide(idQb,'idQ$uidQb'),zero),
inference(superposition,[status(thm)],[d22,c14]) ).
cnf(d24,plain,
quotient(divide(X0,X1),X0,zero),
inference(resolution,[status(thm)],[d0,c7]) ).
cnf(d25,plain,
( 'less$uequal'(X4,X2)
| ~ quotient(X5,X1,X3)
| ~ quotient(X5,divide(X1,X6),X0)
| ~ quotient(X3,zero,X4)
| ~ quotient(X0,X1,X2) ),
inference(resolution,[status(thm)],[d24,c10]) ).
cnf(d26,plain,
( 'less$uequal'(X4,X5)
| ~ quotient(X3,X1,X5)
| ~ quotient(divide(X0,X1),zero,X4)
| ~ quotient(X0,divide(X1,X2),X3) ),
inference(resolution,[status(thm)],[d25,c14]) ).
cnf(d27,plain,
( 'less$uequal'(X3,zero)
| ~ quotient(divide(X0,X1),zero,X3)
| ~ quotient(X0,divide(X1,X2),zero) ),
inference(resolution,[status(thm)],[d26,d12]) ).
cnf(d28,plain,
( 'less$uequal'(X0,zero)
| ~ quotient(divide('idQa$uQ$u$uidQ$uidQb',idQb),zero,X0) ),
inference(resolution,[status(thm)],[d27,d23]) ).
cnf(d29,plain,
'less$uequal'(divide(divide('idQa$uQ$u$uidQ$uidQb',idQb),zero),zero),
inference(resolution,[status(thm)],[d28,c14]) ).
cnf(d30,plain,
divide(divide('idQa$uQ$u$uidQ$uidQb',idQb),zero) = zero,
inference(resolution,[status(thm)],[d29,d1]) ).
cnf(d31,plain,
quotient(divide('idQa$uQ$u$uidQ$uidQb',idQb),zero,zero),
inference(superposition,[status(thm)],[d30,c14]) ).
cnf(d32,plain,
'less$uequal'(divide('idQa$uQ$u$uidQ$uidQb',idQb),zero),
inference(resolution,[status(thm)],[d31,c8]) ).
cnf(d33,plain,
divide('idQa$uQ$u$uidQ$uidQb',idQb) = zero,
inference(resolution,[status(thm)],[d32,d1]) ).
cnf(d34,plain,
'less$uequal'(divide(divide('idQa$uQ$u$uidQ$uidQb','idQ$uidQa'),'idQb$uQ$u$uidQ$uidQa'),divide(zero,'idQ$uidQa')),
inference(superposition,[status(thm)],[d33,d7]) ).
cnf(d35,plain,
'less$uequal'(divide(divide('idQa$uQ$u$uidQ$uidQb','idQ$uidQa'),'idQb$uQ$u$uidQ$uidQa'),zero),
inference(demodulation,[status(thm)],[d34,d2]) ).
cnf(d36,plain,
divide(divide('idQa$uQ$u$uidQ$uidQb','idQ$uidQa'),'idQb$uQ$u$uidQ$uidQa') = zero,
inference(resolution,[status(thm)],[d35,d1]) ).
cnf(d37,plain,
quotient(divide('idQa$uQ$u$uidQ$uidQb','idQ$uidQa'),'idQb$uQ$u$uidQ$uidQa',zero),
inference(superposition,[status(thm)],[d36,c14]) ).
cnf(d38,plain,
'less$uequal'(divide('idQa$uQ$u$uidQ$uidQb','idQ$uidQa'),'idQb$uQ$u$uidQ$uidQa'),
inference(resolution,[status(thm)],[d37,c8]) ).
cnf(d39,plain,
( ~ 'less$uequal'('idQb$uQ$u$uidQ$uidQa',divide('idQa$uQ$u$uidQ$uidQb','idQ$uidQa'))
| 'idQb$uQ$u$uidQ$uidQa' = divide('idQa$uQ$u$uidQ$uidQb','idQ$uidQa') ),
inference(resolution,[status(thm)],[d38,c12]) ).
cnf(d40,plain,
( 'less$uequal'(divide('idQb$uQ$u$uidQ$uidQa',divide(X0,'idQ$uidQa')),X1)
| ~ quotient(divide(idQb,X0),'idQ$uidQa',X1) ),
inference(resolution,[status(thm)],[d10,c5]) ).
cnf(d41,plain,
'less$uequal'(divide('idQb$uQ$u$uidQ$uidQa',divide(X0,'idQ$uidQa')),divide(divide(idQb,X0),'idQ$uidQa')),
inference(resolution,[status(thm)],[d40,c14]) ).
cnf(d42,plain,
( 'less$uequal'(X3,X1)
| ~ quotient(X4,b,X2)
| ~ quotient(X4,identity,X0)
| ~ quotient(X2,idQb,X3)
| ~ quotient(X0,b,X1) ),
inference(resolution,[status(thm)],[c10,c1]) ).
cnf(d43,plain,
( 'less$uequal'(X2,X3)
| ~ quotient(zero,b,X3)
| ~ quotient(X1,idQb,X2)
| ~ quotient(X0,b,X1) ),
inference(resolution,[status(thm)],[d42,d13]) ).
cnf(d44,plain,
( 'less$uequal'(divide(X1,idQb),X2)
| ~ quotient(zero,b,X2)
| ~ quotient(X0,b,X1) ),
inference(resolution,[status(thm)],[d43,c14]) ).
cnf(d45,plain,
( 'less$uequal'(divide(divide(X1,b),idQb),X0)
| ~ quotient(zero,b,X0) ),
inference(resolution,[status(thm)],[d44,c14]) ).
cnf(d46,plain,
'less$uequal'(divide(divide(X0,b),idQb),zero),
inference(resolution,[status(thm)],[d45,d12]) ).
cnf(d47,plain,
divide(divide(X0,b),idQb) = zero,
inference(resolution,[status(thm)],[d46,d1]) ).
cnf(d48,plain,
quotient(divide(X0,b),idQb,zero),
inference(superposition,[status(thm)],[d47,c14]) ).
cnf(d49,plain,
'less$uequal'(divide(X0,b),idQb),
inference(resolution,[status(thm)],[d48,c8]) ).
cnf(d50,plain,
( ~ 'less$uequal'(idQb,divide(X0,b))
| idQb = divide(X0,b) ),
inference(resolution,[status(thm)],[d49,c12]) ).
cnf(d51,plain,
( ~ 'less$uequal'(X0,divide(X0,X1))
| X0 = divide(X0,X1) ),
inference(resolution,[status(thm)],[d0,c12]) ).
cnf(d52,plain,
( 'less$uequal'(X4,X2)
| ~ quotient(X5,X1,X3)
| ~ quotient(X5,zero,X0)
| ~ quotient(X3,zero,X4)
| ~ quotient(X0,X1,X2) ),
inference(resolution,[status(thm)],[d12,c10]) ).
cnf(d53,plain,
( 'less$uequal'(X3,X4)
| ~ quotient(X1,X2,X4)
| ~ quotient(divide(X0,X2),zero,X3)
| ~ quotient(X0,zero,X1) ),
inference(resolution,[status(thm)],[d52,c14]) ).
cnf(d54,plain,
( 'less$uequal'(X3,zero)
| ~ quotient(divide(X0,X1),zero,X3)
| ~ quotient(X0,zero,divide(X1,X2)) ),
inference(resolution,[status(thm)],[d53,d24]) ).
cnf(d55,plain,
( 'less$uequal'(X1,zero)
| ~ quotient(divide(X0,X0),zero,X1) ),
inference(resolution,[status(thm)],[d54,c14]) ).
cnf(d56,plain,
'less$uequal'(divide(divide(X0,X0),zero),zero),
inference(resolution,[status(thm)],[d55,c14]) ).
cnf(d57,plain,
divide(divide(X0,X0),zero) = zero,
inference(resolution,[status(thm)],[d56,d1]) ).
cnf(d58,plain,
quotient(divide(X0,X0),zero,zero),
inference(superposition,[status(thm)],[d57,c14]) ).
cnf(d59,plain,
'less$uequal'(divide(X0,X0),zero),
inference(resolution,[status(thm)],[d58,c8]) ).
cnf(d60,plain,
divide(X0,X0) = zero,
inference(resolution,[status(thm)],[d59,d1]) ).
cnf(d61,plain,
quotient(X0,X0,zero),
inference(superposition,[status(thm)],[d60,c14]) ).
cnf(d62,plain,
( 'less$uequal'(divide(divide(X0,X2),divide(X1,X2)),X3)
| ~ quotient(divide(X0,X1),X2,X3) ),
inference(resolution,[status(thm)],[d10,c14]) ).
cnf(d63,plain,
'less$uequal'(divide(divide(X0,divide(X0,X1)),divide(X1,divide(X0,X1))),zero),
inference(resolution,[status(thm)],[d62,d61]) ).
cnf(d64,plain,
( ~ quotient(X1,X2,X0)
| X0 = divide(X1,X2) ),
inference(resolution,[status(thm)],[c15,c14]) ).
cnf(d65,plain,
zero = divide(zero,X0),
inference(resolution,[status(thm)],[d64,d12]) ).
cnf(d66,plain,
'less$uequal'(divide(divide(X0,divide(X0,zero)),zero),zero),
inference(superposition,[status(thm)],[d65,d63]) ).
cnf(d67,plain,
divide(divide(X0,divide(X0,zero)),zero) = zero,
inference(resolution,[status(thm)],[d66,d1]) ).
cnf(d68,plain,
quotient(divide(X0,divide(X0,zero)),zero,zero),
inference(superposition,[status(thm)],[d67,c14]) ).
cnf(d69,plain,
'less$uequal'(divide(X0,divide(X0,zero)),zero),
inference(resolution,[status(thm)],[d68,c8]) ).
cnf(d70,plain,
divide(X0,divide(X0,zero)) = zero,
inference(resolution,[status(thm)],[d69,d1]) ).
cnf(d71,plain,
quotient(X0,divide(X0,zero),zero),
inference(superposition,[status(thm)],[d70,c14]) ).
cnf(d72,plain,
'less$uequal'(X0,divide(X0,zero)),
inference(resolution,[status(thm)],[d71,c8]) ).
cnf(d73,plain,
X0 = divide(X0,zero),
inference(resolution,[status(thm)],[d72,d51]) ).
cnf(d74,plain,
( 'less$uequal'(divide(idQb,divide(X0,b)),X1)
| ~ quotient(divide(identity,X0),b,X1) ),
inference(resolution,[status(thm)],[d10,c1]) ).
cnf(d75,plain,
'less$uequal'(divide(idQb,divide(X0,b)),divide(divide(identity,X0),b)),
inference(resolution,[status(thm)],[d74,c14]) ).
cnf(d76,plain,
( ~ quotient(divide(X1,X2),X1,X0)
| X0 = zero ),
inference(resolution,[status(thm)],[d24,c15]) ).
cnf(d77,plain,
divide(divide(X0,X1),X0) = zero,
inference(resolution,[status(thm)],[d76,c14]) ).
cnf(d78,plain,
( 'less$uequal'(X2,X3)
| ~ quotient(idQb,X0,X3)
| ~ quotient(X1,divide(b,X0),X2)
| ~ quotient(identity,X0,X1) ),
inference(resolution,[status(thm)],[d8,c1]) ).
cnf(d79,plain,
( 'less$uequal'(divide(X1,divide(b,X0)),X2)
| ~ quotient(idQb,X0,X2)
| ~ quotient(identity,X0,X1) ),
inference(resolution,[status(thm)],[d78,c14]) ).
cnf(d80,plain,
( 'less$uequal'(divide('idQ$uidQb',divide(b,idQb)),X0)
| ~ quotient(idQb,idQb,X0) ),
inference(resolution,[status(thm)],[d79,c2]) ).
cnf(d81,plain,
'less$uequal'(divide('idQ$uidQb',divide(b,idQb)),zero),
inference(resolution,[status(thm)],[d80,d61]) ).
cnf(d82,plain,
divide('idQ$uidQb',divide(b,idQb)) = zero,
inference(resolution,[status(thm)],[d81,d1]) ).
cnf(d83,plain,
quotient('idQ$uidQb',divide(b,idQb),zero),
inference(superposition,[status(thm)],[d82,c14]) ).
cnf(d84,plain,
'less$uequal'('idQ$uidQb',divide(b,idQb)),
inference(resolution,[status(thm)],[d83,c8]) ).
cnf(d85,plain,
'less$uequal'(divide(X0,idQb),'idQ$uidQb'),
inference(resolution,[status(thm)],[d20,c8]) ).
cnf(d86,plain,
( ~ 'less$uequal'('idQ$uidQb',divide(X0,idQb))
| 'idQ$uidQb' = divide(X0,idQb) ),
inference(resolution,[status(thm)],[d85,c12]) ).
cnf(d87,plain,
'idQ$uidQb' = divide(b,idQb),
inference(resolution,[status(thm)],[d86,d84]) ).
cnf(d88,plain,
divide('idQ$uidQb',b) = zero,
inference(superposition,[status(thm)],[d87,d77]) ).
cnf(d89,plain,
'less$uequal'(divide(idQb,zero),divide(divide(identity,'idQ$uidQb'),b)),
inference(superposition,[status(thm)],[d88,d75]) ).
cnf(d90,plain,
'less$uequal'(idQb,divide(divide(identity,'idQ$uidQb'),b)),
inference(demodulation,[status(thm)],[d89,d73]) ).
cnf(d91,plain,
idQb = divide(divide(identity,'idQ$uidQb'),b),
inference(resolution,[status(thm)],[d90,d50]) ).
cnf(d92,plain,
( divide(identity,'idQ$uidQb') = divide(divide(identity,'idQ$uidQb'),b)
| ~ 'less$uequal'(divide(identity,'idQ$uidQb'),idQb) ),
inference(superposition,[status(thm)],[d91,d51]) ).
cnf(d93,plain,
( ~ 'less$uequal'(divide(identity,'idQ$uidQb'),idQb)
| divide(identity,'idQ$uidQb') = idQb ),
inference(demodulation,[status(thm)],[d92,d91]) ).
cnf(d94,plain,
quotient(X0,zero,X0),
inference(superposition,[status(thm)],[d73,c14]) ).
cnf(d95,plain,
'less$uequal'(divide(divide(X0,'idQ$uidQb'),divide(idQb,'idQ$uidQb')),zero),
inference(resolution,[status(thm)],[d20,d62]) ).
cnf(d96,plain,
divide(divide(X0,'idQ$uidQb'),divide(idQb,'idQ$uidQb')) = zero,
inference(resolution,[status(thm)],[d95,d1]) ).
cnf(d97,plain,
quotient(divide(X0,'idQ$uidQb'),divide(idQb,'idQ$uidQb'),zero),
inference(superposition,[status(thm)],[d96,c14]) ).
cnf(d98,plain,
( 'less$uequal'(X1,zero)
| ~ quotient(divide(divide(X0,'idQ$uidQb'),idQb),zero,X1) ),
inference(resolution,[status(thm)],[d97,d27]) ).
cnf(d99,plain,
'less$uequal'(divide(divide(X0,'idQ$uidQb'),idQb),zero),
inference(resolution,[status(thm)],[d98,d94]) ).
cnf(d100,plain,
divide(divide(X0,'idQ$uidQb'),idQb) = zero,
inference(resolution,[status(thm)],[d99,d1]) ).
cnf(d101,plain,
quotient(divide(X0,'idQ$uidQb'),idQb,zero),
inference(superposition,[status(thm)],[d100,c14]) ).
cnf(d102,plain,
'less$uequal'(divide(X0,'idQ$uidQb'),idQb),
inference(resolution,[status(thm)],[d101,c8]) ).
cnf(d103,plain,
divide(identity,'idQ$uidQb') = idQb,
inference(resolution,[status(thm)],[d102,d93]) ).
cnf(d104,plain,
( 'less$uequal'(X3,X1)
| ~ quotient(X4,'idQ$uidQb',X2)
| ~ quotient(X4,idQa,X0)
| ~ quotient(X2,'idQa$uQ$u$uidQ$uidQb',X3)
| ~ quotient(X0,'idQ$uidQb',X1) ),
inference(resolution,[status(thm)],[c10,c3]) ).
cnf(d105,plain,
( 'less$uequal'(X1,X2)
| ~ quotient('idQ$uidQa','idQ$uidQb',X2)
| ~ quotient(X0,'idQa$uQ$u$uidQ$uidQb',X1)
| ~ quotient(identity,'idQ$uidQb',X0) ),
inference(resolution,[status(thm)],[d104,c4]) ).
cnf(d106,plain,
( 'less$uequal'(divide(X0,'idQa$uQ$u$uidQ$uidQb'),X1)
| ~ quotient('idQ$uidQa','idQ$uidQb',X1)
| ~ quotient(identity,'idQ$uidQb',X0) ),
inference(resolution,[status(thm)],[d105,c14]) ).
cnf(d107,plain,
( 'less$uequal'(divide(divide(identity,'idQ$uidQb'),'idQa$uQ$u$uidQ$uidQb'),X0)
| ~ quotient('idQ$uidQa','idQ$uidQb',X0) ),
inference(resolution,[status(thm)],[d106,c14]) ).
cnf(d108,plain,
'less$uequal'(divide(divide(identity,'idQ$uidQb'),'idQa$uQ$u$uidQ$uidQb'),divide('idQ$uidQa','idQ$uidQb')),
inference(resolution,[status(thm)],[d107,c14]) ).
cnf(d109,plain,
quotient(divide(divide(identity,'idQ$uidQb'),'idQa$uQ$u$uidQ$uidQb'),divide('idQ$uidQa','idQ$uidQb'),zero),
inference(resolution,[status(thm)],[d108,c7]) ).
cnf(d110,plain,
( 'less$uequal'(X0,zero)
| ~ quotient(divide(divide(divide(identity,'idQ$uidQb'),'idQa$uQ$u$uidQ$uidQb'),'idQ$uidQa'),zero,X0) ),
inference(resolution,[status(thm)],[d109,d27]) ).
cnf(d111,plain,
'less$uequal'(divide(divide(divide(identity,'idQ$uidQb'),'idQa$uQ$u$uidQ$uidQb'),'idQ$uidQa'),zero),
inference(resolution,[status(thm)],[d110,d94]) ).
cnf(d112,plain,
'less$uequal'(divide(divide(idQb,'idQa$uQ$u$uidQ$uidQb'),'idQ$uidQa'),zero),
inference(demodulation,[status(thm)],[d111,d103]) ).
cnf(d113,plain,
divide(divide(idQb,'idQa$uQ$u$uidQ$uidQb'),'idQ$uidQa') = zero,
inference(resolution,[status(thm)],[d112,d1]) ).
cnf(d114,plain,
'less$uequal'(divide('idQb$uQ$u$uidQ$uidQa',divide('idQa$uQ$u$uidQ$uidQb','idQ$uidQa')),zero),
inference(superposition,[status(thm)],[d113,d41]) ).
cnf(d115,plain,
divide('idQb$uQ$u$uidQ$uidQa',divide('idQa$uQ$u$uidQ$uidQb','idQ$uidQa')) = zero,
inference(resolution,[status(thm)],[d114,d1]) ).
cnf(d116,plain,
quotient('idQb$uQ$u$uidQ$uidQa',divide('idQa$uQ$u$uidQ$uidQb','idQ$uidQa'),zero),
inference(superposition,[status(thm)],[d115,c14]) ).
cnf(d117,plain,
'less$uequal'('idQb$uQ$u$uidQ$uidQa',divide('idQa$uQ$u$uidQ$uidQb','idQ$uidQa')),
inference(resolution,[status(thm)],[d116,c8]) ).
cnf(d118,plain,
'idQb$uQ$u$uidQ$uidQa' = divide('idQa$uQ$u$uidQ$uidQb','idQ$uidQa'),
inference(resolution,[status(thm)],[d117,d39]) ).
cnf(d119,plain,
'less$uequal'('idQb$uQ$u$uidQ$uidQa','idQa$uQ$u$uidQ$uidQb'),
inference(superposition,[status(thm)],[d118,d0]) ).
cnf(d120,plain,
( 'less$uequal'(X2,X3)
| ~ quotient(divide(X0,idQa),'idQ$uidQb',X3)
| ~ quotient(X1,'idQa$uQ$u$uidQ$uidQb',X2)
| ~ quotient(X0,'idQ$uidQb',X1) ),
inference(resolution,[status(thm)],[d104,c14]) ).
cnf(d121,plain,
( 'less$uequal'(divide(X1,'idQa$uQ$u$uidQ$uidQb'),X2)
| ~ quotient(divide(X0,idQa),'idQ$uidQb',X2)
| ~ quotient(X0,'idQ$uidQb',X1) ),
inference(resolution,[status(thm)],[d120,c14]) ).
cnf(d122,plain,
( 'less$uequal'(divide(divide(X0,'idQ$uidQb'),'idQa$uQ$u$uidQ$uidQb'),X1)
| ~ quotient(divide(X0,idQa),'idQ$uidQb',X1) ),
inference(resolution,[status(thm)],[d121,c14]) ).
cnf(d123,plain,
'less$uequal'(divide(divide(X0,'idQ$uidQb'),'idQa$uQ$u$uidQ$uidQb'),divide(divide(X0,idQa),'idQ$uidQb')),
inference(resolution,[status(thm)],[d122,c14]) ).
cnf(d124,plain,
( 'less$uequal'(X3,X1)
| ~ quotient(X4,idQa,X2)
| ~ quotient(X4,identity,X0)
| ~ quotient(X2,'idQ$uidQa',X3)
| ~ quotient(X0,idQa,X1) ),
inference(resolution,[status(thm)],[c10,c4]) ).
cnf(d125,plain,
( 'less$uequal'(X2,X3)
| ~ quotient(zero,idQa,X3)
| ~ quotient(X1,'idQ$uidQa',X2)
| ~ quotient(X0,idQa,X1) ),
inference(resolution,[status(thm)],[d124,d13]) ).
cnf(d126,plain,
( 'less$uequal'(divide(X1,'idQ$uidQa'),X2)
| ~ quotient(zero,idQa,X2)
| ~ quotient(X0,idQa,X1) ),
inference(resolution,[status(thm)],[d125,c14]) ).
cnf(d127,plain,
( 'less$uequal'(divide(divide(X1,idQa),'idQ$uidQa'),X0)
| ~ quotient(zero,idQa,X0) ),
inference(resolution,[status(thm)],[d126,c14]) ).
cnf(d128,plain,
'less$uequal'(divide(divide(X0,idQa),'idQ$uidQa'),zero),
inference(resolution,[status(thm)],[d127,d12]) ).
cnf(d129,plain,
divide(divide(X0,idQa),'idQ$uidQa') = zero,
inference(resolution,[status(thm)],[d128,d1]) ).
cnf(d130,plain,
quotient(divide(X0,idQa),'idQ$uidQa',zero),
inference(superposition,[status(thm)],[d129,c14]) ).
cnf(d131,plain,
'less$uequal'(divide('idQb$uQ$u$uidQ$uidQa',divide(idQa,'idQ$uidQa')),zero),
inference(resolution,[status(thm)],[d130,d40]) ).
cnf(d132,plain,
divide('idQb$uQ$u$uidQ$uidQa',divide(idQa,'idQ$uidQa')) = zero,
inference(resolution,[status(thm)],[d131,d1]) ).
cnf(d133,plain,
quotient('idQb$uQ$u$uidQ$uidQa',divide(idQa,'idQ$uidQa'),zero),
inference(superposition,[status(thm)],[d132,c14]) ).
cnf(d134,plain,
( 'less$uequal'(X0,zero)
| ~ quotient(divide('idQb$uQ$u$uidQ$uidQa',idQa),zero,X0) ),
inference(resolution,[status(thm)],[d27,d133]) ).
cnf(d135,plain,
'less$uequal'(divide(divide('idQb$uQ$u$uidQ$uidQa',idQa),zero),zero),
inference(resolution,[status(thm)],[d134,c14]) ).
cnf(d136,plain,
divide(divide('idQb$uQ$u$uidQ$uidQa',idQa),zero) = zero,
inference(resolution,[status(thm)],[d135,d1]) ).
cnf(d137,plain,
quotient(divide('idQb$uQ$u$uidQ$uidQa',idQa),zero,zero),
inference(superposition,[status(thm)],[d136,c14]) ).
cnf(d138,plain,
'less$uequal'(divide('idQb$uQ$u$uidQ$uidQa',idQa),zero),
inference(resolution,[status(thm)],[d137,c8]) ).
cnf(d139,plain,
divide('idQb$uQ$u$uidQ$uidQa',idQa) = zero,
inference(resolution,[status(thm)],[d138,d1]) ).
cnf(d140,plain,
'less$uequal'(divide(divide('idQb$uQ$u$uidQ$uidQa','idQ$uidQb'),'idQa$uQ$u$uidQ$uidQb'),divide(zero,'idQ$uidQb')),
inference(superposition,[status(thm)],[d139,d123]) ).
cnf(d141,plain,
'less$uequal'(divide(divide('idQb$uQ$u$uidQ$uidQa','idQ$uidQb'),'idQa$uQ$u$uidQ$uidQb'),zero),
inference(demodulation,[status(thm)],[d140,d2]) ).
cnf(d142,plain,
divide(divide('idQb$uQ$u$uidQ$uidQa','idQ$uidQb'),'idQa$uQ$u$uidQ$uidQb') = zero,
inference(resolution,[status(thm)],[d141,d1]) ).
cnf(d143,plain,
quotient(divide('idQb$uQ$u$uidQ$uidQa','idQ$uidQb'),'idQa$uQ$u$uidQ$uidQb',zero),
inference(superposition,[status(thm)],[d142,c14]) ).
cnf(d144,plain,
'less$uequal'(divide('idQb$uQ$u$uidQ$uidQa','idQ$uidQb'),'idQa$uQ$u$uidQ$uidQb'),
inference(resolution,[status(thm)],[d143,c8]) ).
cnf(d145,plain,
( ~ 'less$uequal'('idQa$uQ$u$uidQ$uidQb',divide('idQb$uQ$u$uidQ$uidQa','idQ$uidQb'))
| 'idQa$uQ$u$uidQ$uidQb' = divide('idQb$uQ$u$uidQ$uidQa','idQ$uidQb') ),
inference(resolution,[status(thm)],[d144,c12]) ).
cnf(d146,plain,
'less$uequal'(divide('idQa$uQ$u$uidQ$uidQb',divide(X0,'idQ$uidQb')),divide(divide(idQa,X0),'idQ$uidQb')),
inference(resolution,[status(thm)],[d11,c14]) ).
cnf(d147,plain,
( 'less$uequal'(X3,X1)
| ~ quotient(X4,a,X2)
| ~ quotient(X4,identity,X0)
| ~ quotient(X2,idQa,X3)
| ~ quotient(X0,a,X1) ),
inference(resolution,[status(thm)],[c10,c0]) ).
cnf(d148,plain,
( 'less$uequal'(X2,X3)
| ~ quotient(zero,a,X3)
| ~ quotient(X1,idQa,X2)
| ~ quotient(X0,a,X1) ),
inference(resolution,[status(thm)],[d147,d13]) ).
cnf(d149,plain,
( 'less$uequal'(divide(X1,idQa),X2)
| ~ quotient(zero,a,X2)
| ~ quotient(X0,a,X1) ),
inference(resolution,[status(thm)],[d148,c14]) ).
cnf(d150,plain,
( 'less$uequal'(divide(divide(X1,a),idQa),X0)
| ~ quotient(zero,a,X0) ),
inference(resolution,[status(thm)],[d149,c14]) ).
cnf(d151,plain,
'less$uequal'(divide(divide(X0,a),idQa),zero),
inference(resolution,[status(thm)],[d150,d12]) ).
cnf(d152,plain,
divide(divide(X0,a),idQa) = zero,
inference(resolution,[status(thm)],[d151,d1]) ).
cnf(d153,plain,
quotient(divide(X0,a),idQa,zero),
inference(superposition,[status(thm)],[d152,c14]) ).
cnf(d154,plain,
'less$uequal'(divide(X0,a),idQa),
inference(resolution,[status(thm)],[d153,c8]) ).
cnf(d155,plain,
( ~ 'less$uequal'(idQa,divide(X0,a))
| idQa = divide(X0,a) ),
inference(resolution,[status(thm)],[d154,c12]) ).
cnf(d156,plain,
( 'less$uequal'(divide(idQa,divide(X0,a)),X1)
| ~ quotient(divide(identity,X0),a,X1) ),
inference(resolution,[status(thm)],[d10,c0]) ).
cnf(d157,plain,
'less$uequal'(divide(idQa,divide(X0,a)),divide(divide(identity,X0),a)),
inference(resolution,[status(thm)],[d156,c14]) ).
cnf(d158,plain,
( 'less$uequal'(X2,X3)
| ~ quotient(idQa,X0,X3)
| ~ quotient(X1,divide(a,X0),X2)
| ~ quotient(identity,X0,X1) ),
inference(resolution,[status(thm)],[d8,c0]) ).
cnf(d159,plain,
( 'less$uequal'(divide(X1,divide(a,X0)),X2)
| ~ quotient(idQa,X0,X2)
| ~ quotient(identity,X0,X1) ),
inference(resolution,[status(thm)],[d158,c14]) ).
cnf(d160,plain,
( 'less$uequal'(divide('idQ$uidQa',divide(a,idQa)),X0)
| ~ quotient(idQa,idQa,X0) ),
inference(resolution,[status(thm)],[d159,c4]) ).
cnf(d161,plain,
'less$uequal'(divide('idQ$uidQa',divide(a,idQa)),zero),
inference(resolution,[status(thm)],[d160,d61]) ).
cnf(d162,plain,
divide('idQ$uidQa',divide(a,idQa)) = zero,
inference(resolution,[status(thm)],[d161,d1]) ).
cnf(d163,plain,
quotient('idQ$uidQa',divide(a,idQa),zero),
inference(superposition,[status(thm)],[d162,c14]) ).
cnf(d164,plain,
'less$uequal'('idQ$uidQa',divide(a,idQa)),
inference(resolution,[status(thm)],[d163,c8]) ).
cnf(d165,plain,
'less$uequal'(divide(X0,idQa),'idQ$uidQa'),
inference(resolution,[status(thm)],[d130,c8]) ).
cnf(d166,plain,
( ~ 'less$uequal'('idQ$uidQa',divide(X0,idQa))
| 'idQ$uidQa' = divide(X0,idQa) ),
inference(resolution,[status(thm)],[d165,c12]) ).
cnf(d167,plain,
'idQ$uidQa' = divide(a,idQa),
inference(resolution,[status(thm)],[d166,d164]) ).
cnf(d168,plain,
divide('idQ$uidQa',a) = zero,
inference(superposition,[status(thm)],[d167,d77]) ).
cnf(d169,plain,
'less$uequal'(divide(idQa,zero),divide(divide(identity,'idQ$uidQa'),a)),
inference(superposition,[status(thm)],[d168,d157]) ).
cnf(d170,plain,
'less$uequal'(idQa,divide(divide(identity,'idQ$uidQa'),a)),
inference(demodulation,[status(thm)],[d169,d73]) ).
cnf(d171,plain,
idQa = divide(divide(identity,'idQ$uidQa'),a),
inference(resolution,[status(thm)],[d170,d155]) ).
cnf(d172,plain,
( divide(identity,'idQ$uidQa') = divide(divide(identity,'idQ$uidQa'),a)
| ~ 'less$uequal'(divide(identity,'idQ$uidQa'),idQa) ),
inference(superposition,[status(thm)],[d171,d51]) ).
cnf(d173,plain,
( ~ 'less$uequal'(divide(identity,'idQ$uidQa'),idQa)
| divide(identity,'idQ$uidQa') = idQa ),
inference(demodulation,[status(thm)],[d172,d171]) ).
cnf(d174,plain,
zero = divide(divide(X0,X1),X0),
inference(resolution,[status(thm)],[d24,d64]) ).
cnf(d175,plain,
( 'less$uequal'(X3,X5)
| ~ quotient(divide(X4,divide(X0,X1)),X0,X5)
| ~ quotient(X4,X0,X2)
| ~ quotient(X2,zero,X3) ),
inference(superposition,[status(thm)],[d174,d9]) ).
cnf(d176,plain,
( 'less$uequal'(X2,X4)
| ~ quotient(divide(X0,divide(X1,X3)),X1,X4)
| ~ quotient(divide(X0,X1),zero,X2) ),
inference(resolution,[status(thm)],[d175,c14]) ).
cnf(d177,plain,
( 'less$uequal'(divide(divide(X0,X1),zero),X3)
| ~ quotient(divide(X0,divide(X1,X2)),X1,X3) ),
inference(resolution,[status(thm)],[d176,c14]) ).
cnf(d178,plain,
'less$uequal'(divide(divide(X0,'idQ$uidQa'),divide(idQa,'idQ$uidQa')),zero),
inference(resolution,[status(thm)],[d130,d62]) ).
cnf(d179,plain,
divide(divide(X0,'idQ$uidQa'),divide(idQa,'idQ$uidQa')) = zero,
inference(resolution,[status(thm)],[d178,d1]) ).
cnf(d180,plain,
( 'less$uequal'(divide(divide(divide(X0,'idQ$uidQa'),idQa),zero),X1)
| ~ quotient(zero,idQa,X1) ),
inference(superposition,[status(thm)],[d179,d177]) ).
cnf(d181,plain,
( 'less$uequal'(divide(divide(X0,'idQ$uidQa'),idQa),X1)
| ~ quotient(zero,idQa,X1) ),
inference(demodulation,[status(thm)],[d180,d73]) ).
cnf(d182,plain,
'less$uequal'(divide(divide(X0,'idQ$uidQa'),idQa),zero),
inference(resolution,[status(thm)],[d181,d12]) ).
cnf(d183,plain,
divide(divide(X0,'idQ$uidQa'),idQa) = zero,
inference(resolution,[status(thm)],[d182,d1]) ).
cnf(d184,plain,
quotient(divide(X0,'idQ$uidQa'),idQa,zero),
inference(superposition,[status(thm)],[d183,c14]) ).
cnf(d185,plain,
'less$uequal'(divide(X0,'idQ$uidQa'),idQa),
inference(resolution,[status(thm)],[d184,c8]) ).
cnf(d186,plain,
divide(identity,'idQ$uidQa') = idQa,
inference(resolution,[status(thm)],[d185,d173]) ).
cnf(d187,plain,
( 'less$uequal'(X1,X2)
| ~ quotient('idQ$uidQb','idQ$uidQa',X2)
| ~ quotient(X0,'idQb$uQ$u$uidQ$uidQa',X1)
| ~ quotient(identity,'idQ$uidQa',X0) ),
inference(resolution,[status(thm)],[d3,c2]) ).
cnf(d188,plain,
( 'less$uequal'(divide(X0,'idQb$uQ$u$uidQ$uidQa'),X1)
| ~ quotient('idQ$uidQb','idQ$uidQa',X1)
| ~ quotient(identity,'idQ$uidQa',X0) ),
inference(resolution,[status(thm)],[d187,c14]) ).
cnf(d189,plain,
( 'less$uequal'(divide(divide(identity,'idQ$uidQa'),'idQb$uQ$u$uidQ$uidQa'),X0)
| ~ quotient('idQ$uidQb','idQ$uidQa',X0) ),
inference(resolution,[status(thm)],[d188,c14]) ).
cnf(d190,plain,
'less$uequal'(divide(divide(identity,'idQ$uidQa'),'idQb$uQ$u$uidQ$uidQa'),divide('idQ$uidQb','idQ$uidQa')),
inference(resolution,[status(thm)],[d189,c14]) ).
cnf(d191,plain,
quotient(divide(divide(identity,'idQ$uidQa'),'idQb$uQ$u$uidQ$uidQa'),divide('idQ$uidQb','idQ$uidQa'),zero),
inference(resolution,[status(thm)],[d190,c7]) ).
cnf(d192,plain,
( 'less$uequal'(X0,zero)
| ~ quotient(divide(divide(divide(identity,'idQ$uidQa'),'idQb$uQ$u$uidQ$uidQa'),'idQ$uidQb'),zero,X0) ),
inference(resolution,[status(thm)],[d191,d27]) ).
cnf(d193,plain,
'less$uequal'(divide(divide(divide(identity,'idQ$uidQa'),'idQb$uQ$u$uidQ$uidQa'),'idQ$uidQb'),zero),
inference(resolution,[status(thm)],[d192,d94]) ).
cnf(d194,plain,
'less$uequal'(divide(divide(idQa,'idQb$uQ$u$uidQ$uidQa'),'idQ$uidQb'),zero),
inference(demodulation,[status(thm)],[d193,d186]) ).
cnf(d195,plain,
divide(divide(idQa,'idQb$uQ$u$uidQ$uidQa'),'idQ$uidQb') = zero,
inference(resolution,[status(thm)],[d194,d1]) ).
cnf(d196,plain,
'less$uequal'(divide('idQa$uQ$u$uidQ$uidQb',divide('idQb$uQ$u$uidQ$uidQa','idQ$uidQb')),zero),
inference(superposition,[status(thm)],[d195,d146]) ).
cnf(d197,plain,
divide('idQa$uQ$u$uidQ$uidQb',divide('idQb$uQ$u$uidQ$uidQa','idQ$uidQb')) = zero,
inference(resolution,[status(thm)],[d196,d1]) ).
cnf(d198,plain,
quotient('idQa$uQ$u$uidQ$uidQb',divide('idQb$uQ$u$uidQ$uidQa','idQ$uidQb'),zero),
inference(superposition,[status(thm)],[d197,c14]) ).
cnf(d199,plain,
'less$uequal'('idQa$uQ$u$uidQ$uidQb',divide('idQb$uQ$u$uidQ$uidQa','idQ$uidQb')),
inference(resolution,[status(thm)],[d198,c8]) ).
cnf(d200,plain,
'idQa$uQ$u$uidQ$uidQb' = divide('idQb$uQ$u$uidQ$uidQa','idQ$uidQb'),
inference(resolution,[status(thm)],[d199,d145]) ).
cnf(d201,plain,
'less$uequal'('idQa$uQ$u$uidQ$uidQb','idQb$uQ$u$uidQ$uidQa'),
inference(superposition,[status(thm)],[d200,d0]) ).
cnf(d202,plain,
( ~ 'less$uequal'('idQb$uQ$u$uidQ$uidQa','idQa$uQ$u$uidQ$uidQb')
| 'idQb$uQ$u$uidQ$uidQa' = 'idQa$uQ$u$uidQ$uidQb' ),
inference(resolution,[status(thm)],[d201,c12]) ).
cnf(d203,plain,
~ 'less$uequal'('idQb$uQ$u$uidQ$uidQa','idQa$uQ$u$uidQ$uidQb'),
inference(resolution,[status(thm)],[c6,d202]) ).
cnf(d204,plain,
$false,
inference(resolution,[status(thm)],[d203,d119]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : HEN011-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/5.43 % Computer : n016.cluster.edu
% 0.16/5.43 % Model : x86_64 x86_64
% 0.16/5.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/5.43 % Memory : 8046.5625MB
% 0.16/5.43 % OS : Linux 6.8.0-71-generic
% 0.16/5.43 % CPULimit : 300
% 0.16/5.43 % WCLimit : 300
% 0.16/5.43 % DateTime : Fri Sep 25 16:03:04 UTC 2026
% 0.16/5.44 % CPUTime :
% 0.16/5.44 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 87.82/24.97 % SZS status Unsatisfiable for theBenchmark.p
% 87.82/24.97 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------