%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : HEN010-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n006.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:25 PM UTC 2026
% Result : Unsatisfiable 3.22s 2.65s
% Output : CNFRefutation 3.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 17
% Syntax : Number of formulae : 117 ( 117 unt; 0 def)
% Number of atoms : 117 ( 116 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 2 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 7 con; 0-4 aty)
% Number of variables : 172 ( 0 sgn 172 !; 0 ?; 106 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : ifeq2(X0,X0,X1,X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ifeq_axiom) ).
fof(f2,axiom,
! [X2,X0,X1] : ifeq(X0,X0,X1,X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ifeq_axiom_001) ).
fof(f3,axiom,
! [X0,X1] : ifeq(less_equal(X0,X1),true,quotient(X0,X1,zero),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',quotient_less_equal) ).
fof(f4,plain,
! [X0,X1] : true = ifeq(less_equal(X0,X1),true,quotient(X0,X1,zero),true),
inference(reorient_equations,[],[f3]) ).
fof(f5,axiom,
! [X0,X1] : ifeq(quotient(X0,X1,zero),true,less_equal(X0,X1),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less_equal_quotient) ).
fof(f6,plain,
! [X0,X1] : true = ifeq(quotient(X0,X1,zero),true,less_equal(X0,X1),true),
inference(reorient_equations,[],[f5]) ).
fof(f7,axiom,
! [X2,X0,X1] : ifeq(quotient(X0,X1,X2),true,less_equal(X2,X0),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',divisor_existence) ).
fof(f8,plain,
! [X2,X0,X1] : true = ifeq(quotient(X0,X1,X2),true,less_equal(X2,X0),true),
inference(reorient_equations,[],[f7]) ).
fof(f9,axiom,
! [X2,X3,X0,X1,X6,X7,X4,X5] : ifeq(quotient(X0,X1,X2),true,ifeq(quotient(X3,X4,X5),true,ifeq(quotient(X6,X4,X1),true,ifeq(quotient(X7,X4,X0),true,ifeq(quotient(X7,X6,X3),true,less_equal(X2,X5),true),true),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',quotient_property) ).
fof(f10,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : true = ifeq(quotient(X0,X1,X2),true,ifeq(quotient(X3,X4,X5),true,ifeq(quotient(X6,X4,X1),true,ifeq(quotient(X7,X4,X0),true,ifeq(quotient(X7,X6,X3),true,less_equal(X2,X5),true),true),true),true),true),
inference(reorient_equations,[],[f9]) ).
fof(f11,axiom,
! [X0] : less_equal(zero,X0) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',zero_is_smallest) ).
fof(f12,plain,
! [X0] : true = less_equal(zero,X0),
inference(reorient_equations,[],[f11]) ).
fof(f13,axiom,
! [X0,X1] : ifeq2(less_equal(X0,X1),true,ifeq2(less_equal(X1,X0),true,X1,X0),X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less_equal_and_equal) ).
fof(f16,axiom,
! [X0,X1] : quotient(X0,X1,divide(X0,X1)) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',closure) ).
fof(f17,plain,
! [X0,X1] : true = quotient(X0,X1,divide(X0,X1)),
inference(reorient_equations,[],[f16]) ).
fof(f18,axiom,
! [X2,X3,X0,X1] : ifeq2(quotient(X0,X1,X2),true,ifeq2(quotient(X0,X1,X3),true,X3,X2),X2) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',well_defined) ).
fof(f23,axiom,
! [X0] : quotient(X0,X0,zero) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',x_divide_x_is_zero) ).
fof(f24,plain,
! [X0] : true = quotient(X0,X0,zero),
inference(reorient_equations,[],[f23]) ).
fof(f27,axiom,
! [X2,X0,X1] : ifeq(less_equal(X0,X1),true,ifeq(less_equal(X2,X0),true,less_equal(X2,X1),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',transitivity_of_less_equal) ).
fof(f28,plain,
! [X2,X0,X1] : true = ifeq(less_equal(X0,X1),true,ifeq(less_equal(X2,X0),true,less_equal(X2,X1),true),true),
inference(reorient_equations,[],[f27]) ).
fof(f29,axiom,
! [X2,X3,X0,X1,X4] : ifeq(quotient(X0,X1,X2),true,ifeq(quotient(X0,X3,X4),true,ifeq(less_equal(X4,X1),true,less_equal(X2,X3),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',xQyLEz_implies_xQzLEy) ).
fof(f30,plain,
! [X2,X3,X0,X1,X4] : true = ifeq(quotient(X0,X1,X2),true,ifeq(quotient(X0,X3,X4),true,ifeq(less_equal(X4,X1),true,less_equal(X2,X3),true),true),true),
inference(reorient_equations,[],[f29]) ).
fof(f35,axiom,
quotient(identity,a,idQa) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity_divide_a) ).
fof(f36,plain,
true = quotient(identity,a,idQa),
inference(reorient_equations,[],[f35]) ).
fof(f37,axiom,
quotient(identity,idQa,idQ_idQa) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity_divide_idQa) ).
fof(f38,plain,
true = quotient(identity,idQa,idQ_idQa),
inference(reorient_equations,[],[f37]) ).
fof(f39,axiom,
quotient(idQa,idQ_idQa,idQa_Q__idQ_idQa) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity_divide_idQ_idQa) ).
fof(f40,plain,
true = quotient(idQa,idQ_idQa,idQa_Q__idQ_idQa),
inference(reorient_equations,[],[f39]) ).
fof(f41,negated_conjecture,
idQa != idQa_Q__idQ_idQa,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_idQa_equals_idQa_Q__idQ_idQa) ).
tcf(c_72,plain,
! [X0: $i,X1: $i,X2: $i] : ifeq2(X0,X0,X1,X2) = X1,
inference(cnf_transformation,[],[f1]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i,X2: $i] : ifeq(X0,X0,X1,X2) = X1,
inference(cnf_transformation,[],[f2]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i] : ifeq(less_equal(X0,X1),true,quotient(X0,X1,zero),true) = true,
inference(cnf_transformation,[],[f4]) ).
tcf(c_75,plain,
! [X0: $i,X1: $i] : ifeq(quotient(X0,X1,zero),true,less_equal(X0,X1),true) = true,
inference(cnf_transformation,[],[f6]) ).
tcf(c_76,plain,
! [X0: $i,X1: $i,X2: $i] : ifeq(quotient(X0,X1,X2),true,less_equal(X2,X0),true) = true,
inference(cnf_transformation,[],[f8]) ).
tcf(c_77,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] : ifeq(quotient(X0,X1,X2),true,ifeq(quotient(X3,X4,X5),true,ifeq(quotient(X6,X4,X1),true,ifeq(quotient(X7,X4,X0),true,ifeq(quotient(X7,X6,X3),true,less_equal(X2,X5),true),true),true),true),true) = true,
inference(cnf_transformation,[],[f10]) ).
tcf(c_78,plain,
! [X0: $i] : less_equal(zero,X0) = true,
inference(cnf_transformation,[],[f12]) ).
tcf(c_79,plain,
! [X0: $i,X1: $i] : ifeq2(less_equal(X0,X1),true,ifeq2(less_equal(X1,X0),true,X1,X0),X0) = X0,
inference(cnf_transformation,[],[f13]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i] : quotient(X0,X1,divide(X0,X1)) = true,
inference(cnf_transformation,[],[f17]) ).
tcf(c_82,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : ifeq2(quotient(X0,X1,X2),true,ifeq2(quotient(X0,X1,X3),true,X3,X2),X2) = X2,
inference(cnf_transformation,[],[f18]) ).
tcf(c_85,plain,
! [X0: $i] : quotient(X0,X0,zero) = true,
inference(cnf_transformation,[],[f24]) ).
tcf(c_87,plain,
! [X0: $i,X1: $i,X2: $i] : ifeq(less_equal(X0,X1),true,ifeq(less_equal(X2,X0),true,less_equal(X2,X1),true),true) = true,
inference(cnf_transformation,[],[f28]) ).
tcf(c_88,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : ifeq(quotient(X0,X1,X2),true,ifeq(quotient(X0,X3,X4),true,ifeq(less_equal(X4,X1),true,less_equal(X2,X3),true),true),true) = true,
inference(cnf_transformation,[],[f30]) ).
tcf(c_91,plain,
quotient(identity,a,idQa) = true,
inference(cnf_transformation,[],[f36]) ).
tcf(c_92,plain,
quotient(identity,idQa,idQ_idQa) = true,
inference(cnf_transformation,[],[f38]) ).
tcf(c_93,plain,
quotient(idQa,idQ_idQa,idQa_Q__idQ_idQa) = true,
inference(cnf_transformation,[],[f40]) ).
tcf(c_94,negated_conjecture,
idQa != idQa_Q__idQ_idQa,
inference(cnf_transformation,[],[f41]) ).
tcf(c_268,plain,
ifeq(true,true,less_equal(idQa_Q__idQ_idQa,idQa),true) = true,
inference(superposition,[status(thm)],[c_93,c_76]) ).
tcf(c_270,plain,
less_equal(idQa_Q__idQ_idQa,idQa) = true,
inference(demodulation,[status(thm)],[c_268,c_73]) ).
tcf(c_290,plain,
! [X0: $i] : ifeq(true,true,less_equal(X0,X0),true) = true,
inference(superposition,[status(thm)],[c_85,c_75]) ).
tcf(c_313,plain,
! [X0: $i,X1: $i] : ifeq(true,true,ifeq(quotient(identity,X0,X1),true,ifeq(less_equal(X1,idQa),true,less_equal(idQ_idQa,X0),true),true),true) = true,
inference(superposition,[status(thm)],[c_92,c_88]) ).
tcf(c_314,plain,
! [X0: $i,X1: $i] : ifeq(true,true,ifeq(quotient(idQa,X0,X1),true,ifeq(less_equal(X1,idQ_idQa),true,less_equal(idQa_Q__idQ_idQa,X0),true),true),true) = true,
inference(superposition,[status(thm)],[c_93,c_88]) ).
tcf(c_319,plain,
! [X0: $i,X1: $i] : ifeq(quotient(identity,X0,X1),true,ifeq(true,true,ifeq(less_equal(idQa,X0),true,less_equal(X1,a),true),true),true) = true,
inference(superposition,[status(thm)],[c_91,c_88]) ).
tcf(c_321,plain,
! [X0: $i,X1: $i] : ifeq(quotient(idQa,X0,X1),true,ifeq(true,true,ifeq(less_equal(idQa_Q__idQ_idQa,X0),true,less_equal(X1,idQ_idQa),true),true),true) = true,
inference(superposition,[status(thm)],[c_93,c_88]) ).
tcf(c_376,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : ifeq(quotient(X0,X1,X2),true,ifeq(true,true,ifeq(less_equal(divide(X0,X3),X1),true,less_equal(X2,X3),true),true),true) = true,
inference(superposition,[status(thm)],[c_81,c_88]) ).
tcf(c_383,plain,
! [X0: $i] : less_equal(X0,X0) = true,
inference(demodulation,[status(thm)],[c_290,c_73]) ).
tcf(c_567,plain,
! [X0: $i,X1: $i] : ifeq(quotient(identity,X0,X1),true,ifeq(less_equal(X1,idQa),true,less_equal(idQ_idQa,X0),true),true) = true,
inference(demodulation,[status(thm)],[c_313,c_73]) ).
tcf(c_576,plain,
! [X0: $i] : ifeq(quotient(identity,X0,idQa),true,ifeq(true,true,less_equal(idQ_idQa,X0),true),true) = true,
inference(superposition,[status(thm)],[c_383,c_567]) ).
tcf(c_652,plain,
! [X0: $i] : ifeq2(true,true,ifeq2(less_equal(X0,zero),true,X0,zero),zero) = zero,
inference(superposition,[status(thm)],[c_78,c_79]) ).
tcf(c_659,plain,
ifeq2(less_equal(idQa,idQa_Q__idQ_idQa),true,ifeq2(true,true,idQa_Q__idQ_idQa,idQa),idQa) = idQa,
inference(superposition,[status(thm)],[c_270,c_79]) ).
tcf(c_695,plain,
! [X0: $i] : ifeq(quotient(identity,X0,idQa),true,less_equal(idQ_idQa,X0),true) = true,
inference(demodulation,[status(thm)],[c_576,c_73]) ).
tcf(c_696,plain,
ifeq(true,true,less_equal(idQ_idQa,a),true) = true,
inference(superposition,[status(thm)],[c_91,c_695]) ).
tcf(c_709,plain,
less_equal(idQ_idQa,a) = true,
inference(demodulation,[status(thm)],[c_696,c_73]) ).
tcf(c_760,plain,
! [X0: $i] : ifeq2(true,true,ifeq2(quotient(identity,idQa,X0),true,X0,idQ_idQa),idQ_idQa) = idQ_idQa,
inference(superposition,[status(thm)],[c_92,c_82]) ).
tcf(c_868,plain,
! [X0: $i] : ifeq(true,true,ifeq(less_equal(X0,idQ_idQa),true,less_equal(X0,a),true),true) = true,
inference(superposition,[status(thm)],[c_709,c_87]) ).
tcf(c_910,plain,
! [X0: $i,X1: $i] : ifeq(quotient(idQa,X0,X1),true,ifeq(less_equal(X1,idQ_idQa),true,less_equal(idQa_Q__idQ_idQa,X0),true),true) = true,
inference(demodulation,[status(thm)],[c_314,c_73]) ).
tcf(c_916,plain,
! [X0: $i] : ifeq(quotient(idQa,X0,zero),true,ifeq(true,true,less_equal(idQa_Q__idQ_idQa,X0),true),true) = true,
inference(superposition,[status(thm)],[c_78,c_910]) ).
tcf(c_960,plain,
! [X0: $i] : ifeq(quotient(idQa,X0,zero),true,less_equal(idQa_Q__idQ_idQa,X0),true) = true,
inference(demodulation,[status(thm)],[c_916,c_73]) ).
tcf(c_1130,plain,
! [X0: $i] : ifeq2(less_equal(X0,zero),true,X0,zero) = zero,
inference(demodulation,[status(thm)],[c_652,c_72]) ).
tcf(c_1318,plain,
! [X0: $i,X1: $i] : ifeq(quotient(identity,X0,X1),true,ifeq(less_equal(idQa,X0),true,less_equal(X1,a),true),true) = true,
inference(demodulation,[status(thm)],[c_319,c_73]) ).
tcf(c_1326,plain,
! [X0: $i] : ifeq(quotient(identity,idQa,X0),true,ifeq(true,true,less_equal(X0,a),true),true) = true,
inference(superposition,[status(thm)],[c_383,c_1318]) ).
tcf(c_1351,plain,
! [X0: $i] : ifeq(quotient(identity,idQa,X0),true,less_equal(X0,a),true) = true,
inference(demodulation,[status(thm)],[c_1326,c_73]) ).
tcf(c_1352,plain,
ifeq(true,true,less_equal(divide(identity,idQa),a),true) = true,
inference(superposition,[status(thm)],[c_81,c_1351]) ).
tcf(c_1360,plain,
less_equal(divide(identity,idQa),a) = true,
inference(demodulation,[status(thm)],[c_1352,c_73]) ).
tcf(c_1365,plain,
ifeq(true,true,quotient(divide(identity,idQa),a,zero),true) = true,
inference(superposition,[status(thm)],[c_1360,c_74]) ).
tcf(c_1394,plain,
quotient(divide(identity,idQa),a,zero) = true,
inference(demodulation,[status(thm)],[c_1365,c_73]) ).
tcf(c_1397,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : ifeq(quotient(X0,X1,X2),true,ifeq(true,true,ifeq(quotient(X3,a,X1),true,ifeq(quotient(X4,a,X0),true,ifeq(quotient(X4,X3,divide(identity,idQa)),true,less_equal(X2,zero),true),true),true),true),true) = true,
inference(superposition,[status(thm)],[c_1394,c_77]) ).
tcf(c_1430,plain,
ifeq2(less_equal(idQa,idQa_Q__idQ_idQa),true,idQa_Q__idQ_idQa,idQa) = idQa,
inference(demodulation,[status(thm)],[c_659,c_72]) ).
tcf(c_1609,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : ifeq(quotient(X0,X1,X2),true,ifeq(quotient(X3,a,X1),true,ifeq(quotient(X4,a,X0),true,ifeq(quotient(X4,X3,divide(identity,idQa)),true,less_equal(X2,zero),true),true),true),true) = true,
inference(demodulation,[status(thm)],[c_1397,c_73]) ).
tcf(c_1632,plain,
! [X0: $i,X1: $i,X2: $i] : ifeq(quotient(idQa,X0,X1),true,ifeq(quotient(X2,a,X0),true,ifeq(true,true,ifeq(quotient(identity,X2,divide(identity,idQa)),true,less_equal(X1,zero),true),true),true),true) = true,
inference(superposition,[status(thm)],[c_91,c_1609]) ).
tcf(c_2007,plain,
! [X0: $i,X1: $i] : ifeq(quotient(idQa,X0,X1),true,ifeq(less_equal(idQa_Q__idQ_idQa,X0),true,less_equal(X1,idQ_idQa),true),true) = true,
inference(demodulation,[status(thm)],[c_321,c_73]) ).
tcf(c_2015,plain,
! [X0: $i] : ifeq(quotient(idQa,idQa_Q__idQ_idQa,X0),true,ifeq(true,true,less_equal(X0,idQ_idQa),true),true) = true,
inference(superposition,[status(thm)],[c_383,c_2007]) ).
tcf(c_2311,plain,
! [X0: $i] : ifeq2(quotient(identity,idQa,X0),true,X0,idQ_idQa) = idQ_idQa,
inference(demodulation,[status(thm)],[c_760,c_72]) ).
tcf(c_2312,plain,
ifeq2(true,true,divide(identity,idQa),idQ_idQa) = idQ_idQa,
inference(superposition,[status(thm)],[c_81,c_2311]) ).
tcf(c_2315,plain,
divide(identity,idQa) = idQ_idQa,
inference(demodulation,[status(thm)],[c_2312,c_72]) ).
tcf(c_3108,plain,
! [X0: $i,X1: $i,X2: $i] : ifeq(quotient(idQa,X0,X1),true,ifeq(quotient(X2,a,X0),true,ifeq(true,true,ifeq(quotient(identity,X2,idQ_idQa),true,less_equal(X1,zero),true),true),true),true) = true,
inference(light_normalisation,[status(thm)],[c_1632,c_2315]) ).
tcf(c_3109,plain,
! [X0: $i,X1: $i,X2: $i] : ifeq(quotient(idQa,X0,X1),true,ifeq(quotient(X2,a,X0),true,ifeq(quotient(identity,X2,idQ_idQa),true,less_equal(X1,zero),true),true),true) = true,
inference(demodulation,[status(thm)],[c_3108,c_73]) ).
tcf(c_3110,plain,
! [X0: $i,X1: $i] : ifeq(true,true,ifeq(quotient(X0,a,X1),true,ifeq(quotient(identity,X0,idQ_idQa),true,less_equal(divide(idQa,X1),zero),true),true),true) = true,
inference(superposition,[status(thm)],[c_81,c_3109]) ).
tcf(c_3150,plain,
! [X0: $i,X1: $i] : ifeq(quotient(X0,a,X1),true,ifeq(quotient(identity,X0,idQ_idQa),true,less_equal(divide(idQa,X1),zero),true),true) = true,
inference(demodulation,[status(thm)],[c_3110,c_73]) ).
tcf(c_3151,plain,
! [X0: $i] : ifeq(true,true,ifeq(quotient(identity,X0,idQ_idQa),true,less_equal(divide(idQa,divide(X0,a)),zero),true),true) = true,
inference(superposition,[status(thm)],[c_81,c_3150]) ).
tcf(c_3172,plain,
! [X0: $i] : ifeq(quotient(identity,X0,idQ_idQa),true,less_equal(divide(idQa,divide(X0,a)),zero),true) = true,
inference(demodulation,[status(thm)],[c_3151,c_73]) ).
tcf(c_3173,plain,
ifeq(true,true,less_equal(divide(idQa,divide(idQa,a)),zero),true) = true,
inference(superposition,[status(thm)],[c_92,c_3172]) ).
tcf(c_3233,plain,
less_equal(divide(idQa,divide(idQa,a)),zero) = true,
inference(demodulation,[status(thm)],[c_3173,c_73]) ).
tcf(c_3264,plain,
ifeq2(true,true,divide(idQa,divide(idQa,a)),zero) = zero,
inference(superposition,[status(thm)],[c_3233,c_1130]) ).
tcf(c_3316,plain,
divide(idQa,divide(idQa,a)) = zero,
inference(demodulation,[status(thm)],[c_3264,c_72]) ).
tcf(c_3320,plain,
quotient(idQa,divide(idQa,a),zero) = true,
inference(superposition,[status(thm)],[c_3316,c_81]) ).
tcf(c_3327,plain,
ifeq(true,true,less_equal(idQa,divide(idQa,a)),true) = true,
inference(superposition,[status(thm)],[c_3320,c_75]) ).
tcf(c_3350,plain,
ifeq(true,true,less_equal(idQa_Q__idQ_idQa,divide(idQa,a)),true) = true,
inference(superposition,[status(thm)],[c_3320,c_960]) ).
tcf(c_3393,plain,
less_equal(idQa,divide(idQa,a)) = true,
inference(demodulation,[status(thm)],[c_3327,c_73]) ).
tcf(c_3438,plain,
less_equal(idQa_Q__idQ_idQa,divide(idQa,a)) = true,
inference(demodulation,[status(thm)],[c_3350,c_73]) ).
tcf(c_4294,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : ifeq(quotient(X0,X1,X2),true,ifeq(less_equal(divide(X0,X3),X1),true,less_equal(X2,X3),true),true) = true,
inference(demodulation,[status(thm)],[c_376,c_73]) ).
tcf(c_4993,plain,
! [X0: $i] : ifeq(less_equal(X0,idQ_idQa),true,less_equal(X0,a),true) = true,
inference(demodulation,[status(thm)],[c_868,c_73]) ).
tcf(c_9166,plain,
! [X0: $i] : ifeq(quotient(idQa,idQa_Q__idQ_idQa,X0),true,less_equal(X0,idQ_idQa),true) = true,
inference(demodulation,[status(thm)],[c_2015,c_73]) ).
tcf(c_9167,plain,
ifeq(true,true,less_equal(divide(idQa,idQa_Q__idQ_idQa),idQ_idQa),true) = true,
inference(superposition,[status(thm)],[c_81,c_9166]) ).
tcf(c_9177,plain,
less_equal(divide(idQa,idQa_Q__idQ_idQa),idQ_idQa) = true,
inference(demodulation,[status(thm)],[c_9167,c_73]) ).
tcf(c_9216,plain,
ifeq(true,true,less_equal(divide(idQa,idQa_Q__idQ_idQa),a),true) = true,
inference(superposition,[status(thm)],[c_9177,c_4993]) ).
tcf(c_9255,plain,
less_equal(divide(idQa,idQa_Q__idQ_idQa),a) = true,
inference(demodulation,[status(thm)],[c_9216,c_73]) ).
tcf(c_9292,plain,
! [X0: $i] : ifeq(quotient(idQa,a,X0),true,ifeq(true,true,less_equal(X0,idQa_Q__idQ_idQa),true),true) = true,
inference(superposition,[status(thm)],[c_9255,c_4294]) ).
tcf(c_13380,plain,
! [X0: $i] : ifeq(quotient(idQa,a,X0),true,less_equal(X0,idQa_Q__idQ_idQa),true) = true,
inference(demodulation,[status(thm)],[c_9292,c_73]) ).
tcf(c_13381,plain,
ifeq(true,true,less_equal(divide(idQa,a),idQa_Q__idQ_idQa),true) = true,
inference(superposition,[status(thm)],[c_81,c_13380]) ).
tcf(c_13450,plain,
less_equal(divide(idQa,a),idQa_Q__idQ_idQa) = true,
inference(demodulation,[status(thm)],[c_13381,c_73]) ).
tcf(c_13468,plain,
ifeq2(less_equal(idQa_Q__idQ_idQa,divide(idQa,a)),true,ifeq2(true,true,divide(idQa,a),idQa_Q__idQ_idQa),idQa_Q__idQ_idQa) = idQa_Q__idQ_idQa,
inference(superposition,[status(thm)],[c_13450,c_79]) ).
tcf(c_13502,plain,
ifeq2(true,true,ifeq2(true,true,divide(idQa,a),idQa_Q__idQ_idQa),idQa_Q__idQ_idQa) = idQa_Q__idQ_idQa,
inference(light_normalisation,[status(thm)],[c_13468,c_3438]) ).
tcf(c_13693,plain,
divide(idQa,a) = idQa_Q__idQ_idQa,
inference(demodulation,[status(thm)],[c_13502,c_72]) ).
tcf(c_13772,plain,
less_equal(idQa,idQa_Q__idQ_idQa) = true,
inference(demodulation,[status(thm)],[c_3393,c_13693]) ).
tcf(c_13775,plain,
ifeq2(true,true,idQa_Q__idQ_idQa,idQa) = idQa,
inference(demodulation,[status(thm)],[c_1430,c_13772]) ).
tcf(c_14604,plain,
idQa = idQa_Q__idQ_idQa,
inference(demodulation,[status(thm)],[c_13775,c_72]) ).
tcf(c_14605,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_14604,c_94]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HEN010-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.37 % Computer : n006.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Wed Sep 23 16:15:56 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.41 Running UEQ theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s ueq_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.42
% 0.11/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.42
% 0.11/0.42 % Detected problem language: tptp
% 0.11/0.43 % Proving...
% 3.22/2.65 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 3.22/2.65 % SZS status Started for theBenchmark.p
% 3.22/2.65 % SZS status Unsatisfiable for theBenchmark.p
% 3.22/2.65
% 3.22/2.65 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.22/2.65
% 3.22/2.65 % ------ iProver source info
% 3.22/2.65
% 3.22/2.65 % git: date: 2026-07-19 20:42:38 +0200
% 3.22/2.65 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.22/2.65 % git: non_committed_changes: false
% 3.22/2.65
% 3.22/2.65 % ------ Parsing...% successful
% 3.22/2.65
% 3.22/2.65
% 3.22/2.65 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 3.22/2.65
% 3.22/2.65 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 3.22/2.65
% 3.22/2.65 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 3.22/2.65
% 3.22/2.65 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 3.22/2.65 % ------ Proving...
% 3.22/2.65 % ------ Problem Properties
% 3.22/2.65
% 3.22/2.65 %
% 3.22/2.65 % clauses 23
% 3.22/2.65 % conjectures 1
% 3.22/2.65 % EPR 1
% 3.22/2.65 % Horn 23
% 3.22/2.65 % unary 23
% 3.22/2.65 % binary 0
% 3.22/2.65 % lits 23
% 3.22/2.65 % lits eq 23
% 3.22/2.65 % fd_pure 0
% 3.22/2.65 % fd_pseudo 0
% 3.22/2.65 % fd_cond 0
% 3.22/2.65 % fd_pseudo_cond 0
% 3.22/2.65 % AC symbols 0
% 3.22/2.65
% 3.22/2.65 % ------ Input Options Time Limit: Unbounded
% 3.22/2.65
% 3.22/2.65
% 3.22/2.65 % ------
% 3.22/2.65 % Current options:
% 3.22/2.65 % ------
% 3.22/2.65
% 3.22/2.65
% 3.22/2.65 %
% 3.22/2.65
% 3.22/2.65 % ------ Proving...
% 3.22/2.65 %
% 3.22/2.65
% 3.22/2.65 % SZS status Unsatisfiable for theBenchmark.p
% 3.22/2.65
% 3.22/2.65 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 3.22/2.66
% 3.22/2.66
%------------------------------------------------------------------------------