%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : HEN011-3 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n008.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.62s 4.73s
% Output : CNFRefutation 28.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 14
% Syntax : Number of formulae : 257 ( 218 unt; 2 def)
% Number of atoms : 468 ( 115 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 86 ( 45 ~; 41 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 3 usr; 3 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 8 con; 0-2 aty)
% Number of variables : 136 ( 0 sgn 136 !; 0 ?; 123 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( divide(X0,X1) = zero
| ~ less_equal(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HEN002-0.ax',quotient_less_equal1) ).
fof(f2,axiom,
! [X0,X1] :
( less_equal(X0,X1)
| divide(X0,X1) != zero ),
file('/export/starexec/sandbox/benchmark/Axioms/HEN002-0.ax',quotient_less_equal2) ).
fof(f3,axiom,
! [X0,X1] : less_equal(divide(X0,X1),X0),
file('/export/starexec/sandbox/benchmark/Axioms/HEN002-0.ax',quotient_smaller_than_numerator) ).
fof(f4,axiom,
! [X2,X0,X1] : less_equal(divide(divide(X0,X1),divide(X2,X1)),divide(divide(X0,X2),X1)),
file('/export/starexec/sandbox/benchmark/Axioms/HEN002-0.ax',quotient_property) ).
fof(f5,axiom,
! [X0] : less_equal(zero,X0),
file('/export/starexec/sandbox/benchmark/Axioms/HEN002-0.ax',zero_is_smallest) ).
fof(f6,axiom,
! [X0,X1] :
( X0 = X1
| ~ less_equal(X1,X0)
| ~ less_equal(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HEN002-0.ax',less_equal_and_equal) ).
fof(f7,axiom,
! [X0] : less_equal(X0,identity),
file('/export/starexec/sandbox/benchmark/Axioms/HEN002-0.ax',identity_is_largest) ).
fof(f9,axiom,
divide(identity,a) = c,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_divide_a) ).
fof(f10,axiom,
divide(identity,b) = d,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_divide_b) ).
fof(f11,axiom,
divide(identity,c) = e,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_divide_c) ).
fof(f12,axiom,
divide(identity,d) = g,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_divide_d) ).
fof(f13,negated_conjecture,
divide(c,g) != divide(d,e),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_commutativity) ).
tcf(c_62,plain,
! [X0: $i,X1: $i] :
( ( divide(X0,X1) = zero )
| ~ less_equal(X0,X1) ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i] :
( less_equal(X0,X1)
| ( divide(X0,X1) != zero ) ),
inference(cnf_transformation,[],[f2]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i] : less_equal(divide(X0,X1),X0),
inference(cnf_transformation,[],[f3]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i] : less_equal(divide(divide(X0,X1),divide(X2,X1)),divide(divide(X0,X2),X1)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_66,plain,
! [X0: $i] : less_equal(zero,X0),
inference(cnf_transformation,[],[f5]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ less_equal(X1,X0)
| ~ less_equal(X0,X1) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_68,plain,
! [X0: $i] : less_equal(X0,identity),
inference(cnf_transformation,[],[f7]) ).
tcf(c_70,plain,
divide(identity,a) = c,
inference(cnf_transformation,[],[f9]) ).
tcf(c_71,plain,
divide(identity,b) = d,
inference(cnf_transformation,[],[f10]) ).
tcf(c_72,plain,
divide(identity,c) = e,
inference(cnf_transformation,[],[f11]) ).
tcf(c_73,plain,
divide(identity,d) = g,
inference(cnf_transformation,[],[f12]) ).
tcf(c_74,negated_conjecture,
divide(c,g) != divide(d,e),
inference(cnf_transformation,[],[f13]) ).
tcf(c_225,definition,
iPr_def_10 = divide(c,g),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_226,definition,
iPr_def_11 = divide(d,e),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_227,negated_conjecture,
iPr_def_10 != iPr_def_11,
inference(demodulation,[status(thm)],[c_74,c_226,c_225]) ).
tcf(c_421,plain,
less_equal(iPr_def_10,c),
inference(superposition,[status(thm)],[c_225,c_64]) ).
tcf(c_422,plain,
less_equal(iPr_def_11,d),
inference(superposition,[status(thm)],[c_226,c_64]) ).
tcf(c_425,plain,
! [X0: $i,X1: $i] : divide(divide(X0,X1),X0) = zero,
inference(superposition,[status(thm)],[c_64,c_62]) ).
tcf(c_426,plain,
! [X0: $i] : divide(zero,X0) = zero,
inference(superposition,[status(thm)],[c_66,c_62]) ).
tcf(c_427,plain,
! [X0: $i] : divide(X0,identity) = zero,
inference(superposition,[status(thm)],[c_68,c_62]) ).
tcf(c_459,plain,
! [X0: $i,X1: $i] :
( ( divide(X0,X1) = X0 )
| ~ less_equal(X0,divide(X0,X1)) ),
inference(superposition,[status(thm)],[c_64,c_67]) ).
tcf(c_460,plain,
! [X0: $i] :
( ( X0 = zero )
| ~ less_equal(X0,zero) ),
inference(superposition,[status(thm)],[c_66,c_67]) ).
tcf(c_471,plain,
divide(iPr_def_10,c) = zero,
inference(superposition,[status(thm)],[c_421,c_62]) ).
tcf(c_475,plain,
divide(iPr_def_11,d) = zero,
inference(superposition,[status(thm)],[c_422,c_62]) ).
tcf(c_524,plain,
! [X0: $i] : less_equal(divide(c,divide(X0,a)),divide(divide(identity,X0),a)),
inference(superposition,[status(thm)],[c_70,c_65]) ).
tcf(c_525,plain,
! [X0: $i] : less_equal(divide(d,divide(X0,b)),divide(divide(identity,X0),b)),
inference(superposition,[status(thm)],[c_71,c_65]) ).
tcf(c_526,plain,
! [X0: $i] : less_equal(divide(e,divide(X0,c)),divide(divide(identity,X0),c)),
inference(superposition,[status(thm)],[c_72,c_65]) ).
tcf(c_527,plain,
! [X0: $i] : less_equal(divide(g,divide(X0,d)),divide(divide(identity,X0),d)),
inference(superposition,[status(thm)],[c_73,c_65]) ).
tcf(c_528,plain,
! [X0: $i] : less_equal(divide(iPr_def_10,divide(X0,g)),divide(divide(c,X0),g)),
inference(superposition,[status(thm)],[c_225,c_65]) ).
tcf(c_529,plain,
! [X0: $i] : less_equal(divide(iPr_def_11,divide(X0,e)),divide(divide(d,X0),e)),
inference(superposition,[status(thm)],[c_226,c_65]) ).
tcf(c_535,plain,
! [X0: $i] : less_equal(divide(divide(X0,a),c),divide(divide(X0,identity),a)),
inference(superposition,[status(thm)],[c_70,c_65]) ).
tcf(c_536,plain,
! [X0: $i] : less_equal(divide(divide(X0,b),d),divide(divide(X0,identity),b)),
inference(superposition,[status(thm)],[c_71,c_65]) ).
tcf(c_537,plain,
! [X0: $i] : less_equal(divide(divide(X0,c),e),divide(divide(X0,identity),c)),
inference(superposition,[status(thm)],[c_72,c_65]) ).
tcf(c_538,plain,
! [X0: $i] : less_equal(divide(divide(X0,d),g),divide(divide(X0,identity),d)),
inference(superposition,[status(thm)],[c_73,c_65]) ).
tcf(c_539,plain,
! [X0: $i] : less_equal(divide(divide(X0,g),iPr_def_10),divide(divide(X0,c),g)),
inference(superposition,[status(thm)],[c_225,c_65]) ).
tcf(c_540,plain,
! [X0: $i] : less_equal(divide(divide(X0,e),iPr_def_11),divide(divide(X0,d),e)),
inference(superposition,[status(thm)],[c_226,c_65]) ).
tcf(c_542,plain,
! [X0: $i,X1: $i] : less_equal(divide(divide(X0,X1),zero),divide(divide(X0,zero),X1)),
inference(superposition,[status(thm)],[c_426,c_65]) ).
tcf(c_546,plain,
! [X0: $i,X1: $i] : less_equal(divide(divide(X0,X0),divide(X1,X0)),zero),
inference(superposition,[status(thm)],[c_425,c_65]) ).
tcf(c_550,plain,
! [X0: $i] : less_equal(divide(divide(identity,X0),divide(c,X0)),divide(e,X0)),
inference(superposition,[status(thm)],[c_72,c_65]) ).
tcf(c_551,plain,
! [X0: $i] : less_equal(divide(divide(identity,X0),divide(d,X0)),divide(g,X0)),
inference(superposition,[status(thm)],[c_73,c_65]) ).
tcf(c_560,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_65,c_62]) ).
tcf(c_569,plain,
! [X0: $i] : less_equal(divide(divide(X0,d),g),divide(zero,d)),
inference(light_normalisation,[status(thm)],[c_538,c_427]) ).
tcf(c_570,plain,
! [X0: $i] : less_equal(divide(divide(X0,c),e),divide(zero,c)),
inference(light_normalisation,[status(thm)],[c_537,c_427]) ).
tcf(c_571,plain,
! [X0: $i] : less_equal(divide(divide(X0,b),d),divide(zero,b)),
inference(light_normalisation,[status(thm)],[c_536,c_427]) ).
tcf(c_572,plain,
! [X0: $i] : less_equal(divide(divide(X0,a),c),divide(zero,a)),
inference(light_normalisation,[status(thm)],[c_535,c_427]) ).
tcf(c_691,plain,
! [X0: $i] : less_equal(divide(divide(X0,X0),zero),zero),
inference(superposition,[status(thm)],[c_425,c_546]) ).
tcf(c_776,plain,
! [X0: $i] : divide(divide(X0,X0),zero) = zero,
inference(superposition,[status(thm)],[c_691,c_460]) ).
tcf(c_863,plain,
! [X0: $i,X1: $i,X2: $i] : divide(divide(divide(divide(X0,X1),X2),divide(X0,X2)),divide(zero,X2)) = zero,
inference(superposition,[status(thm)],[c_425,c_560]) ).
tcf(c_1308,plain,
! [X0: $i] : less_equal(divide(X0,X0),zero),
inference(superposition,[status(thm)],[c_776,c_63]) ).
tcf(c_1339,plain,
! [X0: $i] : divide(X0,X0) = zero,
inference(superposition,[status(thm)],[c_1308,c_460]) ).
tcf(c_1355,plain,
! [X0: $i] : less_equal(divide(divide(X0,d),g),zero),
inference(demodulation,[status(thm)],[c_569,c_426]) ).
tcf(c_1363,plain,
! [X0: $i] : divide(divide(X0,d),g) = zero,
inference(superposition,[status(thm)],[c_1355,c_460]) ).
tcf(c_1403,plain,
! [X0: $i] : less_equal(divide(X0,d),g),
inference(superposition,[status(thm)],[c_1363,c_63]) ).
tcf(c_1410,plain,
! [X0: $i] : less_equal(divide(divide(X0,g),divide(d,g)),zero),
inference(superposition,[status(thm)],[c_1363,c_65]) ).
tcf(c_1439,plain,
! [X0: $i] : less_equal(divide(divide(X0,c),e),zero),
inference(demodulation,[status(thm)],[c_570,c_426]) ).
tcf(c_1448,plain,
! [X0: $i] : divide(divide(X0,c),e) = zero,
inference(superposition,[status(thm)],[c_1439,c_460]) ).
tcf(c_1461,plain,
! [X0: $i] : less_equal(divide(X0,c),e),
inference(superposition,[status(thm)],[c_1448,c_63]) ).
tcf(c_1468,plain,
! [X0: $i] : less_equal(divide(divide(X0,e),divide(c,e)),zero),
inference(superposition,[status(thm)],[c_1448,c_65]) ).
tcf(c_1516,plain,
! [X0: $i] : less_equal(divide(divide(X0,b),d),zero),
inference(demodulation,[status(thm)],[c_571,c_426]) ).
tcf(c_1524,plain,
! [X0: $i] : divide(divide(X0,b),d) = zero,
inference(superposition,[status(thm)],[c_1516,c_460]) ).
tcf(c_1550,plain,
! [X0: $i] : less_equal(divide(X0,b),d),
inference(superposition,[status(thm)],[c_1524,c_63]) ).
tcf(c_1557,plain,
! [X0: $i] : less_equal(divide(divide(X0,d),divide(b,d)),zero),
inference(superposition,[status(thm)],[c_1524,c_65]) ).
tcf(c_1591,plain,
! [X0: $i] : less_equal(divide(divide(X0,a),c),zero),
inference(demodulation,[status(thm)],[c_572,c_426]) ).
tcf(c_1599,plain,
! [X0: $i] : divide(divide(X0,a),c) = zero,
inference(superposition,[status(thm)],[c_1591,c_460]) ).
tcf(c_1613,plain,
! [X0: $i] : less_equal(divide(X0,a),c),
inference(superposition,[status(thm)],[c_1599,c_63]) ).
tcf(c_1620,plain,
! [X0: $i] : less_equal(divide(divide(X0,c),divide(a,c)),zero),
inference(superposition,[status(thm)],[c_1599,c_65]) ).
tcf(c_1653,plain,
less_equal(divide(iPr_def_10,divide(d,g)),zero),
inference(superposition,[status(thm)],[c_225,c_1410]) ).
tcf(c_1660,plain,
! [X0: $i] : divide(divide(X0,g),divide(d,g)) = zero,
inference(superposition,[status(thm)],[c_1410,c_460]) ).
tcf(c_1679,plain,
divide(iPr_def_10,divide(d,g)) = zero,
inference(superposition,[status(thm)],[c_1653,c_460]) ).
tcf(c_1687,plain,
! [X0: $i] : less_equal(divide(divide(iPr_def_10,X0),divide(divide(d,g),X0)),divide(zero,X0)),
inference(superposition,[status(thm)],[c_1679,c_65]) ).
tcf(c_1690,plain,
! [X0: $i] : less_equal(divide(divide(iPr_def_10,X0),divide(divide(d,g),X0)),zero),
inference(light_normalisation,[status(thm)],[c_1687,c_426]) ).
tcf(c_1704,plain,
less_equal(divide(iPr_def_11,divide(c,e)),zero),
inference(superposition,[status(thm)],[c_226,c_1468]) ).
tcf(c_1711,plain,
! [X0: $i] : divide(divide(X0,e),divide(c,e)) = zero,
inference(superposition,[status(thm)],[c_1468,c_460]) ).
tcf(c_1716,plain,
divide(iPr_def_11,divide(c,e)) = zero,
inference(superposition,[status(thm)],[c_1704,c_460]) ).
tcf(c_1720,plain,
less_equal(divide(g,divide(b,d)),zero),
inference(superposition,[status(thm)],[c_73,c_1557]) ).
tcf(c_1733,plain,
divide(g,divide(b,d)) = zero,
inference(superposition,[status(thm)],[c_1720,c_460]) ).
tcf(c_1737,plain,
less_equal(divide(e,divide(a,c)),zero),
inference(superposition,[status(thm)],[c_72,c_1620]) ).
tcf(c_1750,plain,
divide(e,divide(a,c)) = zero,
inference(superposition,[status(thm)],[c_1737,c_460]) ).
tcf(c_1758,plain,
! [X0: $i] : less_equal(divide(divide(iPr_def_11,X0),divide(divide(c,e),X0)),divide(zero,X0)),
inference(superposition,[status(thm)],[c_1716,c_65]) ).
tcf(c_1761,plain,
! [X0: $i] : less_equal(divide(divide(iPr_def_11,X0),divide(divide(c,e),X0)),zero),
inference(light_normalisation,[status(thm)],[c_1758,c_426]) ).
tcf(c_1803,plain,
less_equal(g,divide(b,d)),
inference(superposition,[status(thm)],[c_1733,c_63]) ).
tcf(c_1837,plain,
( ( divide(b,d) = g )
| ~ less_equal(divide(b,d),g) ),
inference(superposition,[status(thm)],[c_1803,c_67]) ).
tcf(c_1839,plain,
divide(b,d) = g,
inference(forward_subsumption_resolution,[status(thm)],[c_1837,c_1403]) ).
tcf(c_1848,plain,
divide(g,b) = zero,
inference(superposition,[status(thm)],[c_1839,c_425]) ).
tcf(c_1901,plain,
! [X0: $i] : less_equal(divide(divide(X0,b),zero),divide(divide(X0,g),b)),
inference(superposition,[status(thm)],[c_1848,c_65]) ).
tcf(c_1948,plain,
less_equal(e,divide(a,c)),
inference(superposition,[status(thm)],[c_1750,c_63]) ).
tcf(c_2014,plain,
( ( divide(a,c) = e )
| ~ less_equal(divide(a,c),e) ),
inference(superposition,[status(thm)],[c_1948,c_67]) ).
tcf(c_2016,plain,
divide(a,c) = e,
inference(forward_subsumption_resolution,[status(thm)],[c_2014,c_1461]) ).
tcf(c_2021,plain,
divide(e,a) = zero,
inference(superposition,[status(thm)],[c_2016,c_425]) ).
tcf(c_2376,plain,
! [X0: $i] : less_equal(divide(X0,g),divide(d,g)),
inference(superposition,[status(thm)],[c_1660,c_63]) ).
tcf(c_2450,plain,
! [X0: $i] : less_equal(divide(X0,e),divide(c,e)),
inference(superposition,[status(thm)],[c_1711,c_63]) ).
tcf(c_2893,plain,
less_equal(divide(c,zero),divide(divide(identity,e),a)),
inference(superposition,[status(thm)],[c_2021,c_524]) ).
tcf(c_3149,plain,
less_equal(divide(d,zero),divide(divide(identity,g),b)),
inference(superposition,[status(thm)],[c_1848,c_525]) ).
tcf(c_3153,plain,
less_equal(divide(d,divide(d,b)),divide(g,b)),
inference(superposition,[status(thm)],[c_73,c_525]) ).
tcf(c_3159,plain,
less_equal(divide(d,divide(d,b)),zero),
inference(light_normalisation,[status(thm)],[c_3153,c_1848]) ).
tcf(c_3204,plain,
divide(d,divide(d,b)) = zero,
inference(superposition,[status(thm)],[c_3159,c_460]) ).
tcf(c_3213,plain,
less_equal(d,divide(d,b)),
inference(superposition,[status(thm)],[c_3204,c_63]) ).
tcf(c_3233,plain,
( ( divide(d,b) = d )
| ~ less_equal(divide(d,b),d) ),
inference(superposition,[status(thm)],[c_3213,c_67]) ).
tcf(c_3235,plain,
divide(d,b) = d,
inference(forward_subsumption_resolution,[status(thm)],[c_3233,c_1550]) ).
tcf(c_3379,plain,
less_equal(divide(e,zero),divide(divide(identity,iPr_def_10),c)),
inference(superposition,[status(thm)],[c_471,c_526]) ).
tcf(c_3381,plain,
less_equal(divide(e,zero),divide(divide(identity,c),c)),
inference(superposition,[status(thm)],[c_1339,c_526]) ).
tcf(c_3395,plain,
less_equal(divide(e,zero),divide(e,c)),
inference(light_normalisation,[status(thm)],[c_3381,c_72]) ).
tcf(c_3529,plain,
less_equal(divide(g,zero),divide(divide(identity,iPr_def_11),d)),
inference(superposition,[status(thm)],[c_475,c_527]) ).
tcf(c_3531,plain,
less_equal(divide(g,zero),divide(divide(identity,d),d)),
inference(superposition,[status(thm)],[c_1339,c_527]) ).
tcf(c_3545,plain,
less_equal(divide(g,zero),divide(g,d)),
inference(light_normalisation,[status(thm)],[c_3531,c_73]) ).
tcf(c_3706,plain,
less_equal(divide(iPr_def_10,zero),divide(divide(c,g),g)),
inference(superposition,[status(thm)],[c_1339,c_528]) ).
tcf(c_3716,plain,
less_equal(divide(iPr_def_10,zero),divide(iPr_def_10,g)),
inference(light_normalisation,[status(thm)],[c_3706,c_225]) ).
tcf(c_3734,plain,
less_equal(divide(iPr_def_11,zero),divide(divide(d,e),e)),
inference(superposition,[status(thm)],[c_1339,c_529]) ).
tcf(c_3744,plain,
less_equal(divide(iPr_def_11,zero),divide(iPr_def_11,e)),
inference(light_normalisation,[status(thm)],[c_3734,c_226]) ).
tcf(c_3985,plain,
less_equal(divide(divide(identity,g),iPr_def_10),divide(e,g)),
inference(superposition,[status(thm)],[c_72,c_539]) ).
tcf(c_4073,plain,
less_equal(divide(divide(identity,e),iPr_def_11),divide(g,e)),
inference(superposition,[status(thm)],[c_73,c_540]) ).
tcf(c_4153,plain,
! [X0: $i] : less_equal(divide(divide(X0,divide(X0,zero)),zero),zero),
inference(superposition,[status(thm)],[c_1339,c_542]) ).
tcf(c_4512,plain,
! [X0: $i] : divide(divide(X0,divide(X0,zero)),zero) = zero,
inference(superposition,[status(thm)],[c_4153,c_460]) ).
tcf(c_6245,plain,
! [X0: $i] : less_equal(divide(X0,divide(X0,zero)),zero),
inference(superposition,[status(thm)],[c_4512,c_63]) ).
tcf(c_6302,plain,
! [X0: $i] : divide(X0,divide(X0,zero)) = zero,
inference(superposition,[status(thm)],[c_6245,c_460]) ).
tcf(c_6311,plain,
! [X0: $i] : less_equal(X0,divide(X0,zero)),
inference(superposition,[status(thm)],[c_6302,c_63]) ).
tcf(c_6615,plain,
! [X0: $i] :
( ( divide(X0,zero) = X0 )
| ~ less_equal(divide(X0,zero),X0) ),
inference(superposition,[status(thm)],[c_6311,c_67]) ).
tcf(c_6619,plain,
! [X0: $i] : divide(X0,zero) = X0,
inference(forward_subsumption_resolution,[status(thm)],[c_6615,c_64]) ).
tcf(c_6628,plain,
less_equal(c,divide(divide(identity,e),a)),
inference(demodulation,[status(thm)],[c_2893,c_6619]) ).
tcf(c_6631,plain,
less_equal(d,divide(divide(identity,g),b)),
inference(demodulation,[status(thm)],[c_3149,c_6619]) ).
tcf(c_6634,plain,
less_equal(e,divide(divide(identity,iPr_def_10),c)),
inference(demodulation,[status(thm)],[c_3379,c_6619]) ).
tcf(c_6635,plain,
less_equal(e,divide(e,c)),
inference(demodulation,[status(thm)],[c_3395,c_6619]) ).
tcf(c_6638,plain,
less_equal(g,divide(divide(identity,iPr_def_11),d)),
inference(demodulation,[status(thm)],[c_3529,c_6619]) ).
tcf(c_6639,plain,
less_equal(g,divide(g,d)),
inference(demodulation,[status(thm)],[c_3545,c_6619]) ).
tcf(c_6645,plain,
less_equal(iPr_def_10,divide(iPr_def_10,g)),
inference(demodulation,[status(thm)],[c_3716,c_6619]) ).
tcf(c_6647,plain,
less_equal(iPr_def_11,divide(iPr_def_11,e)),
inference(demodulation,[status(thm)],[c_3744,c_6619]) ).
tcf(c_6664,plain,
( ( divide(e,c) = e )
| ~ less_equal(divide(e,c),e) ),
inference(superposition,[status(thm)],[c_6635,c_67]) ).
tcf(c_6666,plain,
divide(e,c) = e,
inference(forward_subsumption_resolution,[status(thm)],[c_6664,c_1461]) ).
tcf(c_6668,plain,
( ( divide(g,d) = g )
| ~ less_equal(divide(g,d),g) ),
inference(superposition,[status(thm)],[c_6639,c_67]) ).
tcf(c_6670,plain,
divide(g,d) = g,
inference(forward_subsumption_resolution,[status(thm)],[c_6668,c_1403]) ).
tcf(c_6892,plain,
! [X0: $i] : less_equal(divide(e,divide(X0,c)),divide(divide(e,X0),c)),
inference(superposition,[status(thm)],[c_6666,c_65]) ).
tcf(c_6918,plain,
! [X0: $i] : less_equal(divide(g,divide(X0,d)),divide(divide(g,X0),d)),
inference(superposition,[status(thm)],[c_6670,c_65]) ).
tcf(c_6999,plain,
( ( divide(iPr_def_10,g) = iPr_def_10 )
| ~ less_equal(divide(iPr_def_10,g),iPr_def_10) ),
inference(superposition,[status(thm)],[c_6645,c_67]) ).
tcf(c_7001,plain,
divide(iPr_def_10,g) = iPr_def_10,
inference(forward_subsumption_resolution,[status(thm)],[c_6999,c_64]) ).
tcf(c_7003,plain,
( ( divide(iPr_def_11,e) = iPr_def_11 )
| ~ less_equal(divide(iPr_def_11,e),iPr_def_11) ),
inference(superposition,[status(thm)],[c_6647,c_67]) ).
tcf(c_7005,plain,
divide(iPr_def_11,e) = iPr_def_11,
inference(forward_subsumption_resolution,[status(thm)],[c_7003,c_64]) ).
tcf(c_7023,plain,
! [X0: $i] : less_equal(divide(divide(X0,g),iPr_def_10),divide(divide(X0,iPr_def_10),g)),
inference(superposition,[status(thm)],[c_7001,c_65]) ).
tcf(c_7052,plain,
! [X0: $i] : less_equal(divide(divide(X0,e),iPr_def_11),divide(divide(X0,iPr_def_11),e)),
inference(superposition,[status(thm)],[c_7005,c_65]) ).
tcf(c_7241,plain,
( ( divide(divide(identity,e),a) = c )
| ~ less_equal(divide(divide(identity,e),a),c) ),
inference(superposition,[status(thm)],[c_6628,c_67]) ).
tcf(c_7243,plain,
divide(divide(identity,e),a) = c,
inference(forward_subsumption_resolution,[status(thm)],[c_7241,c_1613]) ).
tcf(c_7245,plain,
( ( divide(divide(identity,g),b) = d )
| ~ less_equal(divide(divide(identity,g),b),d) ),
inference(superposition,[status(thm)],[c_6631,c_67]) ).
tcf(c_7247,plain,
divide(divide(identity,g),b) = d,
inference(forward_subsumption_resolution,[status(thm)],[c_7245,c_1550]) ).
tcf(c_7253,plain,
( ( divide(divide(identity,iPr_def_10),c) = e )
| ~ less_equal(divide(divide(identity,iPr_def_10),c),e) ),
inference(superposition,[status(thm)],[c_6634,c_67]) ).
tcf(c_7255,plain,
divide(divide(identity,iPr_def_10),c) = e,
inference(forward_subsumption_resolution,[status(thm)],[c_7253,c_1461]) ).
tcf(c_7261,plain,
( ( divide(divide(identity,iPr_def_11),d) = g )
| ~ less_equal(divide(divide(identity,iPr_def_11),d),g) ),
inference(superposition,[status(thm)],[c_6638,c_67]) ).
tcf(c_7263,plain,
divide(divide(identity,iPr_def_11),d) = g,
inference(forward_subsumption_resolution,[status(thm)],[c_7261,c_1403]) ).
tcf(c_7399,plain,
less_equal(c,divide(identity,e)),
inference(superposition,[status(thm)],[c_7243,c_64]) ).
tcf(c_7446,plain,
( ( divide(identity,e) = c )
| ~ less_equal(divide(identity,e),c) ),
inference(superposition,[status(thm)],[c_7399,c_67]) ).
tcf(c_7454,plain,
less_equal(d,divide(identity,g)),
inference(superposition,[status(thm)],[c_7247,c_64]) ).
tcf(c_7509,plain,
( ( divide(identity,g) = d )
| ~ less_equal(divide(identity,g),d) ),
inference(superposition,[status(thm)],[c_7454,c_67]) ).
tcf(c_10970,plain,
less_equal(divide(divide(iPr_def_10,d),zero),zero),
inference(superposition,[status(thm)],[c_425,c_1690]) ).
tcf(c_11096,plain,
less_equal(divide(divide(iPr_def_11,c),zero),zero),
inference(superposition,[status(thm)],[c_425,c_1761]) ).
tcf(c_11189,plain,
less_equal(divide(iPr_def_10,d),zero),
inference(demodulation,[status(thm)],[c_10970,c_6619]) ).
tcf(c_11192,plain,
divide(iPr_def_10,d) = zero,
inference(superposition,[status(thm)],[c_11189,c_460]) ).
tcf(c_11371,plain,
less_equal(divide(iPr_def_11,c),zero),
inference(demodulation,[status(thm)],[c_11096,c_6619]) ).
tcf(c_11374,plain,
divide(iPr_def_11,c) = zero,
inference(superposition,[status(thm)],[c_11371,c_460]) ).
tcf(c_11385,plain,
! [X0: $i] : less_equal(divide(divide(iPr_def_11,X0),divide(c,X0)),divide(zero,X0)),
inference(superposition,[status(thm)],[c_11374,c_65]) ).
tcf(c_11403,plain,
! [X0: $i] : less_equal(divide(divide(iPr_def_11,X0),divide(c,X0)),zero),
inference(light_normalisation,[status(thm)],[c_11385,c_426]) ).
tcf(c_11496,plain,
! [X0: $i,X1: $i,X2: $i] : divide(divide(divide(X0,X1),X2),divide(X0,X2)) = zero,
inference(demodulation,[status(thm)],[c_863,c_426,c_6619]) ).
tcf(c_11710,plain,
! [X0: $i,X1: $i,X2: $i] : less_equal(divide(divide(X0,X1),X2),divide(X0,X2)),
inference(superposition,[status(thm)],[c_11496,c_63]) ).
tcf(c_12108,plain,
less_equal(divide(divide(iPr_def_11,g),iPr_def_10),zero),
inference(superposition,[status(thm)],[c_225,c_11403]) ).
tcf(c_12137,plain,
divide(divide(iPr_def_11,g),iPr_def_10) = zero,
inference(superposition,[status(thm)],[c_12108,c_460]) ).
tcf(c_12227,plain,
less_equal(divide(iPr_def_11,g),iPr_def_10),
inference(superposition,[status(thm)],[c_12137,c_63]) ).
tcf(c_12599,plain,
! [X0: $i] : less_equal(divide(g,X0),divide(divide(identity,iPr_def_11),X0)),
inference(superposition,[status(thm)],[c_7263,c_11710]) ).
tcf(c_12600,plain,
! [X0: $i] : less_equal(divide(e,X0),divide(divide(identity,iPr_def_10),X0)),
inference(superposition,[status(thm)],[c_7255,c_11710]) ).
tcf(c_12634,plain,
! [X0: $i] : less_equal(divide(c,X0),divide(divide(identity,e),X0)),
inference(superposition,[status(thm)],[c_7243,c_11710]) ).
tcf(c_12663,plain,
! [X0: $i,X1: $i,X2: $i] : less_equal(divide(divide(divide(X0,X1),X2),X0),zero),
inference(superposition,[status(thm)],[c_425,c_11710]) ).
tcf(c_16313,plain,
! [X0: $i] : less_equal(divide(X0,b),divide(divide(X0,g),b)),
inference(demodulation,[status(thm)],[c_1901,c_6619]) ).
tcf(c_16334,plain,
! [X0: $i] :
( ( divide(divide(X0,g),b) = divide(X0,b) )
| ~ less_equal(divide(divide(X0,g),b),divide(X0,b)) ),
inference(superposition,[status(thm)],[c_16313,c_67]) ).
tcf(c_16340,plain,
! [X0: $i] : divide(divide(X0,g),b) = divide(X0,b),
inference(forward_subsumption_resolution,[status(thm)],[c_16334,c_11710]) ).
tcf(c_18950,plain,
! [X0: $i] : less_equal(divide(X0,b),divide(X0,g)),
inference(superposition,[status(thm)],[c_16340,c_64]) ).
tcf(c_19133,plain,
less_equal(d,divide(d,g)),
inference(superposition,[status(thm)],[c_3235,c_18950]) ).
tcf(c_19234,plain,
( ( divide(d,g) = d )
| ~ less_equal(divide(d,g),d) ),
inference(superposition,[status(thm)],[c_19133,c_67]) ).
tcf(c_19236,plain,
divide(d,g) = d,
inference(forward_subsumption_resolution,[status(thm)],[c_19234,c_64]) ).
tcf(c_19238,plain,
! [X0: $i] : less_equal(divide(X0,g),d),
inference(demodulation,[status(thm)],[c_2376,c_19236]) ).
tcf(c_19242,plain,
less_equal(divide(identity,g),d),
inference(instantiation,[status(thm)],[c_19238]) ).
tcf(c_22808,plain,
less_equal(divide(c,divide(c,e)),zero),
inference(superposition,[status(thm)],[c_1711,c_12634]) ).
tcf(c_23413,plain,
divide(c,divide(c,e)) = zero,
inference(superposition,[status(thm)],[c_22808,c_460]) ).
tcf(c_23425,plain,
less_equal(c,divide(c,e)),
inference(superposition,[status(thm)],[c_23413,c_63]) ).
tcf(c_23512,plain,
( ( divide(c,e) = c )
| ~ less_equal(divide(c,e),c) ),
inference(superposition,[status(thm)],[c_23425,c_67]) ).
tcf(c_23514,plain,
divide(c,e) = c,
inference(forward_subsumption_resolution,[status(thm)],[c_23512,c_64]) ).
tcf(c_23517,plain,
! [X0: $i] : less_equal(divide(X0,e),c),
inference(demodulation,[status(thm)],[c_2450,c_23514]) ).
tcf(c_23521,plain,
less_equal(divide(identity,e),c),
inference(instantiation,[status(thm)],[c_23517]) ).
tcf(c_24543,plain,
! [X0: $i,X1: $i,X2: $i] : divide(divide(divide(X0,X1),X2),X0) = zero,
inference(superposition,[status(thm)],[c_12663,c_460]) ).
tcf(c_25219,plain,
less_equal(divide(e,zero),divide(divide(e,iPr_def_11),c)),
inference(superposition,[status(thm)],[c_11374,c_6892]) ).
tcf(c_25271,plain,
less_equal(divide(g,zero),divide(divide(g,iPr_def_10),d)),
inference(superposition,[status(thm)],[c_11192,c_6918]) ).
tcf(c_29455,plain,
less_equal(e,divide(divide(e,iPr_def_11),c)),
inference(demodulation,[status(thm)],[c_25219,c_6619]) ).
tcf(c_29456,plain,
( ( divide(divide(e,iPr_def_11),c) = e )
| ~ less_equal(divide(divide(e,iPr_def_11),c),e) ),
inference(superposition,[status(thm)],[c_29455,c_67]) ).
tcf(c_29458,plain,
divide(divide(e,iPr_def_11),c) = e,
inference(forward_subsumption_resolution,[status(thm)],[c_29456,c_1461]) ).
tcf(c_29471,plain,
less_equal(e,divide(e,iPr_def_11)),
inference(superposition,[status(thm)],[c_29458,c_64]) ).
tcf(c_29593,plain,
( ( divide(e,iPr_def_11) = e )
| ~ less_equal(divide(e,iPr_def_11),e) ),
inference(superposition,[status(thm)],[c_29471,c_67]) ).
tcf(c_29595,plain,
divide(e,iPr_def_11) = e,
inference(forward_subsumption_resolution,[status(thm)],[c_29593,c_64]) ).
tcf(c_29625,plain,
! [X0: $i] : less_equal(divide(divide(X0,iPr_def_11),e),divide(divide(X0,e),iPr_def_11)),
inference(superposition,[status(thm)],[c_29595,c_65]) ).
tcf(c_29924,plain,
less_equal(g,divide(divide(g,iPr_def_10),d)),
inference(demodulation,[status(thm)],[c_25271,c_6619]) ).
tcf(c_29925,plain,
( ( divide(divide(g,iPr_def_10),d) = g )
| ~ less_equal(divide(divide(g,iPr_def_10),d),g) ),
inference(superposition,[status(thm)],[c_29924,c_67]) ).
tcf(c_29927,plain,
divide(divide(g,iPr_def_10),d) = g,
inference(forward_subsumption_resolution,[status(thm)],[c_29925,c_1403]) ).
tcf(c_29941,plain,
less_equal(g,divide(g,iPr_def_10)),
inference(superposition,[status(thm)],[c_29927,c_64]) ).
tcf(c_30672,plain,
( ( divide(g,iPr_def_10) = g )
| ~ less_equal(divide(g,iPr_def_10),g) ),
inference(superposition,[status(thm)],[c_29941,c_67]) ).
tcf(c_30674,plain,
divide(g,iPr_def_10) = g,
inference(forward_subsumption_resolution,[status(thm)],[c_30672,c_64]) ).
tcf(c_30704,plain,
! [X0: $i] : less_equal(divide(divide(X0,iPr_def_10),g),divide(divide(X0,g),iPr_def_10)),
inference(superposition,[status(thm)],[c_30674,c_65]) ).
tcf(c_36183,plain,
! [X0: $i] :
( ( divide(divide(X0,e),iPr_def_11) = divide(divide(X0,iPr_def_11),e) )
| ~ less_equal(divide(divide(X0,e),iPr_def_11),divide(divide(X0,iPr_def_11),e)) ),
inference(superposition,[status(thm)],[c_29625,c_67]) ).
tcf(c_36194,plain,
! [X0: $i] : divide(divide(X0,e),iPr_def_11) = divide(divide(X0,iPr_def_11),e),
inference(forward_subsumption_resolution,[status(thm)],[c_36183,c_7052]) ).
tcf(c_36195,plain,
less_equal(divide(divide(identity,iPr_def_11),e),divide(g,e)),
inference(demodulation,[status(thm)],[c_4073,c_36194]) ).
tcf(c_36210,plain,
( ( divide(divide(identity,iPr_def_11),e) = divide(g,e) )
| ~ less_equal(divide(g,e),divide(divide(identity,iPr_def_11),e)) ),
inference(superposition,[status(thm)],[c_36195,c_67]) ).
tcf(c_36212,plain,
divide(divide(identity,iPr_def_11),e) = divide(g,e),
inference(forward_subsumption_resolution,[status(thm)],[c_36210,c_12599]) ).
tcf(c_36820,plain,
! [X0: $i] :
( ( divide(divide(X0,g),iPr_def_10) = divide(divide(X0,iPr_def_10),g) )
| ~ less_equal(divide(divide(X0,g),iPr_def_10),divide(divide(X0,iPr_def_10),g)) ),
inference(superposition,[status(thm)],[c_30704,c_67]) ).
tcf(c_36831,plain,
! [X0: $i] : divide(divide(X0,g),iPr_def_10) = divide(divide(X0,iPr_def_10),g),
inference(forward_subsumption_resolution,[status(thm)],[c_36820,c_7023]) ).
tcf(c_36832,plain,
less_equal(divide(divide(identity,iPr_def_10),g),divide(e,g)),
inference(demodulation,[status(thm)],[c_3985,c_36831]) ).
tcf(c_36847,plain,
( ( divide(divide(identity,iPr_def_10),g) = divide(e,g) )
| ~ less_equal(divide(e,g),divide(divide(identity,iPr_def_10),g)) ),
inference(superposition,[status(thm)],[c_36832,c_67]) ).
tcf(c_36849,plain,
divide(divide(identity,iPr_def_10),g) = divide(e,g),
inference(forward_subsumption_resolution,[status(thm)],[c_36847,c_12600]) ).
tcf(c_46924,plain,
! [X0: $i,X1: $i,X2: $i] : less_equal(divide(divide(X0,X1),X2),X0),
inference(superposition,[status(thm)],[c_24543,c_63]) ).
tcf(c_68227,plain,
divide(identity,e) = c,
inference(global_subsumption_just,[status(thm)],[c_7446,c_7446,c_23521]) ).
tcf(c_68273,plain,
! [X0: $i] : less_equal(divide(divide(identity,X0),divide(e,X0)),divide(c,X0)),
inference(superposition,[status(thm)],[c_68227,c_65]) ).
tcf(c_68284,plain,
less_equal(divide(c,divide(d,e)),divide(g,e)),
inference(superposition,[status(thm)],[c_68227,c_551]) ).
tcf(c_68326,plain,
less_equal(divide(c,iPr_def_11),divide(g,e)),
inference(light_normalisation,[status(thm)],[c_68284,c_226]) ).
tcf(c_69949,plain,
less_equal(divide(divide(identity,iPr_def_11),e),divide(c,iPr_def_11)),
inference(superposition,[status(thm)],[c_29595,c_68273]) ).
tcf(c_69972,plain,
less_equal(divide(g,e),divide(c,iPr_def_11)),
inference(light_normalisation,[status(thm)],[c_69949,c_36212]) ).
tcf(c_70156,plain,
( ( divide(c,iPr_def_11) = divide(g,e) )
| ~ less_equal(divide(c,iPr_def_11),divide(g,e)) ),
inference(superposition,[status(thm)],[c_69972,c_67]) ).
tcf(c_70158,plain,
divide(c,iPr_def_11) = divide(g,e),
inference(forward_subsumption_resolution,[status(thm)],[c_70156,c_68326]) ).
tcf(c_70177,plain,
divide(divide(c,iPr_def_11),g) = zero,
inference(superposition,[status(thm)],[c_70158,c_425]) ).
tcf(c_70854,plain,
less_equal(divide(iPr_def_10,divide(iPr_def_11,g)),zero),
inference(superposition,[status(thm)],[c_70177,c_528]) ).
tcf(c_71083,plain,
divide(iPr_def_10,divide(iPr_def_11,g)) = zero,
inference(superposition,[status(thm)],[c_70854,c_460]) ).
tcf(c_71197,plain,
less_equal(iPr_def_10,divide(iPr_def_11,g)),
inference(superposition,[status(thm)],[c_71083,c_63]) ).
tcf(c_71254,plain,
( ( divide(iPr_def_11,g) = iPr_def_10 )
| ~ less_equal(divide(iPr_def_11,g),iPr_def_10) ),
inference(superposition,[status(thm)],[c_71197,c_67]) ).
tcf(c_71256,plain,
divide(iPr_def_11,g) = iPr_def_10,
inference(forward_subsumption_resolution,[status(thm)],[c_71254,c_12227]) ).
tcf(c_71263,plain,
! [X0: $i] : less_equal(divide(iPr_def_10,X0),iPr_def_11),
inference(superposition,[status(thm)],[c_71256,c_46924]) ).
tcf(c_71267,plain,
( ( divide(iPr_def_11,g) = iPr_def_11 )
| ~ less_equal(iPr_def_11,iPr_def_10) ),
inference(superposition,[status(thm)],[c_71256,c_459]) ).
tcf(c_71330,plain,
( ( iPr_def_10 = iPr_def_11 )
| ~ less_equal(iPr_def_11,iPr_def_10) ),
inference(light_normalisation,[status(thm)],[c_71267,c_71256]) ).
tcf(c_71331,plain,
~ less_equal(iPr_def_11,iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_71330,c_227]) ).
tcf(c_75031,plain,
divide(identity,g) = d,
inference(global_subsumption_just,[status(thm)],[c_7509,c_7509,c_19242]) ).
tcf(c_75078,plain,
! [X0: $i] : less_equal(divide(divide(identity,X0),divide(g,X0)),divide(d,X0)),
inference(superposition,[status(thm)],[c_75031,c_65]) ).
tcf(c_75092,plain,
less_equal(divide(d,divide(c,g)),divide(e,g)),
inference(superposition,[status(thm)],[c_75031,c_550]) ).
tcf(c_75134,plain,
less_equal(divide(d,iPr_def_10),divide(e,g)),
inference(light_normalisation,[status(thm)],[c_75092,c_225]) ).
tcf(c_77929,plain,
less_equal(divide(divide(identity,iPr_def_10),g),divide(d,iPr_def_10)),
inference(superposition,[status(thm)],[c_30674,c_75078]) ).
tcf(c_77952,plain,
less_equal(divide(e,g),divide(d,iPr_def_10)),
inference(light_normalisation,[status(thm)],[c_77929,c_36849]) ).
tcf(c_78000,plain,
( ( divide(d,iPr_def_10) = divide(e,g) )
| ~ less_equal(divide(d,iPr_def_10),divide(e,g)) ),
inference(superposition,[status(thm)],[c_77952,c_67]) ).
tcf(c_78002,plain,
divide(d,iPr_def_10) = divide(e,g),
inference(forward_subsumption_resolution,[status(thm)],[c_78000,c_75134]) ).
tcf(c_78025,plain,
divide(divide(d,iPr_def_10),e) = zero,
inference(superposition,[status(thm)],[c_78002,c_425]) ).
tcf(c_80017,plain,
less_equal(divide(iPr_def_11,divide(iPr_def_10,e)),zero),
inference(superposition,[status(thm)],[c_78025,c_529]) ).
tcf(c_80245,plain,
divide(iPr_def_11,divide(iPr_def_10,e)) = zero,
inference(superposition,[status(thm)],[c_80017,c_460]) ).
tcf(c_81138,plain,
less_equal(iPr_def_11,divide(iPr_def_10,e)),
inference(superposition,[status(thm)],[c_80245,c_63]) ).
tcf(c_81235,plain,
( ( divide(iPr_def_10,e) = iPr_def_11 )
| ~ less_equal(divide(iPr_def_10,e),iPr_def_11) ),
inference(superposition,[status(thm)],[c_81138,c_67]) ).
tcf(c_81237,plain,
divide(iPr_def_10,e) = iPr_def_11,
inference(forward_subsumption_resolution,[status(thm)],[c_81235,c_71263]) ).
tcf(c_81258,plain,
less_equal(iPr_def_11,iPr_def_10),
inference(superposition,[status(thm)],[c_81237,c_64]) ).
tcf(c_81306,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_81258,c_71331]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HEN011-3 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.38 % Computer : n008.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Wed Sep 23 16:18:09 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.44
% 0.12/0.44 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.44
% 0.12/0.44 % Detected problem language: tptp
% 0.12/0.45 % Proving...
% 28.62/4.73 % SZS status Started for theBenchmark.p
% 28.62/4.73 % SZS status Unsatisfiable for theBenchmark.p
% 28.62/4.73
% 28.62/4.73 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 28.62/4.73
% 28.62/4.73 % ------ iProver source info
% 28.62/4.73
% 28.62/4.73 % git: date: 2026-07-19 20:42:38 +0200
% 28.62/4.73 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 28.62/4.73 % git: non_committed_changes: false
% 28.62/4.73
% 28.62/4.73 % ------ Parsing...% successful
% 28.62/4.73
% 28.62/4.73
% 28.62/4.73 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 28.62/4.73
% 28.62/4.73 % ------ Preprocessing... sup_sim: 1 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.62/4.73
% 28.62/4.73 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 28.62/4.73
% 28.62/4.73 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 28.62/4.73 % ------ Proving...
% 28.62/4.73 % ------ Problem Properties
% 28.62/4.73
% 28.62/4.73 %
% 28.62/4.73 % clauses 14
% 28.62/4.73 % conjectures 1
% 28.62/4.73 % EPR 4
% 28.62/4.73 % Horn 14
% 28.62/4.73 % unary 11
% 28.62/4.73 % binary 2
% 28.62/4.73 % lits 18
% 28.62/4.73 % lits eq 10
% 28.62/4.73 % fd_pure 0
% 28.62/4.73 % fd_pseudo 0
% 28.62/4.73 % fd_cond 0
% 28.62/4.73 % fd_pseudo_cond 1
% 28.62/4.73 % AC symbols 0
% 28.62/4.73
% 28.62/4.73 % ------ Schedule dynamic 5 is on
% 28.62/4.73
% 28.62/4.73 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 28.62/4.73
% 28.62/4.73
% 28.62/4.73 % ------
% 28.62/4.73 % Current options:
% 28.62/4.73 % ------
% 28.62/4.73
% 28.62/4.73
% 28.62/4.73 %
% 28.62/4.73
% 28.62/4.73 % ------ Proving...
% 28.62/4.73 %
% 28.62/4.73
% 28.62/4.73 % SZS status Unsatisfiable for theBenchmark.p
% 28.62/4.73
% 28.62/4.73 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 28.62/4.73
% 28.62/4.73
%------------------------------------------------------------------------------