%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : ITP107^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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 : Wed Oct 7 10:24:08 AM UTC 2026
% Result : Theorem 1.78s 0.53s
% Output : CNFRefutation 1.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 17
% Syntax : Number of formulae : 69 ( 69 unt; 0 typ; 0 def)
% Number of atoms : 171 ( 88 equ; 0 cnn)
% Maximal formula atoms : 1 ( 2 avg)
% Number of connectives : 396 ( 2 ~; 0 |; 0 &; 394 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Number of types : 13 ( 12 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 75 ( 72 usr; 13 con; 0-3 aty)
% Number of variables : 24 ( 0 ^; 24 !; 0 ?; 24 :)
% Comments :
%------------------------------------------------------------------------------
thf(tp_a,type,
a: $tType ).
thf(tp_int,type,
int: $tType ).
thf(tp_nat,type,
nat: $tType ).
thf(tp_partia1833973666xt_a_b,type,
partia1833973666xt_a_b: $tType ).
thf(tp_partia1993116613t_unit,type,
partia1993116613t_unit: $tType ).
thf(tp_partia539144763t_unit,type,
partia539144763t_unit: $tType ).
thf(tp_partia96731725t_unit,type,
partia96731725t_unit: $tType ).
thf(tp_product_prod_a_a,type,
product_prod_a_a: $tType ).
thf(tp_set_Product_prod_a_a,type,
set_Product_prod_a_a: $tType ).
thf(tp_set_a,type,
set_a: $tType ).
thf(tp_set_se1596668135od_a_a,type,
set_se1596668135od_a_a: $tType ).
thf(tp_set_set_a,type,
set_set_a: $tType ).
thf(tp_a_RCOSETS_a_b,type,
a_RCOSETS_a_b: partia1833973666xt_a_b > set_a > set_set_a ).
thf(tp_a_l_coset_a_b,type,
a_l_coset_a_b: partia1833973666xt_a_b > a > set_a > set_a ).
thf(tp_a_r_coset_a_b,type,
a_r_coset_a_b: partia1833973666xt_a_b > set_a > a > set_a ).
thf(tp_abelian_monoid_a_b,type,
abelian_monoid_a_b: partia1833973666xt_a_b > $o ).
thf(tp_add_pow_a_b_int,type,
add_pow_a_b_int: partia1833973666xt_a_b > int > a > a ).
thf(tp_add_pow_a_b_nat,type,
add_pow_a_b_nat: partia1833973666xt_a_b > nat > a > a ).
thf(tp_additi2104487374up_a_b,type,
additi2104487374up_a_b: set_a > partia1833973666xt_a_b > $o ).
thf(tp_bot_bo1424703315od_a_a,type,
bot_bo1424703315od_a_a: set_se1596668135od_a_a ).
thf(tp_bot_bo2131659635od_a_a,type,
bot_bo2131659635od_a_a: set_Product_prod_a_a ).
thf(tp_bot_bot_set_a,type,
bot_bot_set_a: set_a ).
thf(tp_bot_bot_set_set_a,type,
bot_bot_set_set_a: set_set_a ).
thf(tp_collec183727474od_a_a,type,
collec183727474od_a_a: ( set_Product_prod_a_a > $o ) > set_se1596668135od_a_a ).
thf(tp_collec645855634od_a_a,type,
collec645855634od_a_a: ( product_prod_a_a > $o ) > set_Product_prod_a_a ).
thf(tp_collect_a,type,
collect_a: ( a > $o ) > set_a ).
thf(tp_collect_set_a,type,
collect_set_a: ( set_a > $o ) > set_set_a ).
thf(tp_equiva2136214035t_unit,type,
equiva2136214035t_unit: partia1993116613t_unit > $o ).
thf(tp_field_a_b,type,
field_a_b: partia1833973666xt_a_b > $o ).
thf(tp_group_52730354t_unit,type,
group_52730354t_unit: partia539144763t_unit > $o ).
thf(tp_group_a_Product_unit,type,
group_a_Product_unit: partia96731725t_unit > $o ).
thf(tp_group_a_ring_ext_a_b,type,
group_a_ring_ext_a_b: partia1833973666xt_a_b > $o ).
thf(tp_insert1116662519od_a_a,type,
insert1116662519od_a_a: product_prod_a_a > set_Product_prod_a_a > set_Product_prod_a_a ).
thf(tp_insert1738756823od_a_a,type,
insert1738756823od_a_a: set_Product_prod_a_a > set_se1596668135od_a_a > set_se1596668135od_a_a ).
thf(tp_insert_a,type,
insert_a: a > set_a > set_a ).
thf(tp_insert_set_a,type,
insert_set_a: set_a > set_set_a > set_set_a ).
thf(tp_locali1170246543t_unit,type,
locali1170246543t_unit: partia1993116613t_unit > a > a > set_Product_prod_a_a ).
thf(tp_locali1488796916t_unit,type,
locali1488796916t_unit: partia539144763t_unit > set_se1596668135od_a_a > $o ).
thf(tp_locali1538946157t_unit,type,
locali1538946157t_unit: partia1993116613t_unit > set_se1596668135od_a_a ).
thf(tp_locali1648887798ac_a_b,type,
locali1648887798ac_a_b: partia1833973666xt_a_b > set_a > $o ).
thf(tp_locali1944243560ac_a_b,type,
locali1944243560ac_a_b: partia1833973666xt_a_b > set_a > partia539144763t_unit ).
thf(tp_locali425460998xt_a_b,type,
locali425460998xt_a_b: partia1833973666xt_a_b > set_a > $o ).
thf(tp_locali807230110ng_a_b,type,
locali807230110ng_a_b: partia1833973666xt_a_b > set_a > $o ).
thf(tp_locali880295127ng_a_b,type,
locali880295127ng_a_b: partia1833973666xt_a_b > set_a > $o ).
thf(tp_member1838126896od_a_a,type,
member1838126896od_a_a: set_Product_prod_a_a > set_se1596668135od_a_a > $o ).
thf(tp_member449909584od_a_a,type,
member449909584od_a_a: product_prod_a_a > set_Product_prod_a_a > $o ).
thf(tp_member_a,type,
member_a: a > set_a > $o ).
thf(tp_member_set_a,type,
member_set_a: set_a > set_set_a > $o ).
thf(tp_minus_minus_set_a,type,
minus_minus_set_a: set_a > set_a > set_a ).
thf(tp_monoid1022105667xt_a_b,type,
monoid1022105667xt_a_b: partia1833973666xt_a_b > $o ).
thf(tp_monoid1242292471t_unit,type,
monoid1242292471t_unit: partia539144763t_unit > $o ).
thf(tp_monoid1447254976t_unit,type,
monoid1447254976t_unit: partia96731725t_unit > $o ).
thf(tp_mult_a_Product_unit,type,
mult_a_Product_unit: partia96731725t_unit > a > a > a ).
thf(tp_mult_a_ring_ext_a_b,type,
mult_a_ring_ext_a_b: partia1833973666xt_a_b > a > a > a ).
thf(tp_mult_s977248631t_unit,type,
mult_s977248631t_unit: partia539144763t_unit > set_Product_prod_a_a > set_Product_prod_a_a > set_Product_prod_a_a ).
thf(tp_one_a_Product_unit,type,
one_a_Product_unit: partia96731725t_unit > a ).
thf(tp_one_a_ring_ext_a_b,type,
one_a_ring_ext_a_b: partia1833973666xt_a_b > a ).
thf(tp_one_se1488596747t_unit,type,
one_se1488596747t_unit: partia539144763t_unit > set_Product_prod_a_a ).
thf(tp_ord_le1824328871od_a_a,type,
ord_le1824328871od_a_a: set_Product_prod_a_a > set_Product_prod_a_a > $o ).
thf(tp_ord_le318720350_set_a,type,
ord_le318720350_set_a: set_set_a > set_set_a > $o ).
thf(tp_ord_le391835783od_a_a,type,
ord_le391835783od_a_a: set_se1596668135od_a_a > set_se1596668135od_a_a > $o ).
thf(tp_ord_less_eq_set_a,type,
ord_less_eq_set_a: set_a > set_a > $o ).
thf(tp_partia1066395285xt_a_b,type,
partia1066395285xt_a_b: partia1833973666xt_a_b > set_a ).
thf(tp_partia1955795460t_unit,type,
partia1955795460t_unit: partia96731725t_unit > set_a ).
thf(tp_partia206007992t_unit,type,
partia206007992t_unit: partia1993116613t_unit > set_Product_prod_a_a ).
thf(tp_partia616129906t_unit,type,
partia616129906t_unit: partia539144763t_unit > set_se1596668135od_a_a ).
thf(tp_pow_a,type,
pow_a: set_a > set_set_a ).
thf(tp_product_Pair_a_a,type,
product_Pair_a_a: a > a > product_prod_a_a ).
thf(tp_r,type,
r: partia1833973666xt_a_b ).
thf(tp_r2,type,
r2: a ).
thf(tp_r3,type,
r3: a ).
thf(tp_rel,type,
rel: partia1993116613t_unit ).
thf(tp_ring_a_b,type,
ring_a_b: partia1833973666xt_a_b > $o ).
thf(tp_s,type,
s: set_a ).
thf(tp_s2,type,
s2: a ).
thf(tp_s3,type,
s3: a ).
thf(tp_semiring_a_b,type,
semiring_a_b: partia1833973666xt_a_b > $o ).
thf(tp_set_add_a_b,type,
set_add_a_b: partia1833973666xt_a_b > set_a > set_a > set_a ).
thf(tp_units_1411277569xt_a_b,type,
units_1411277569xt_a_b: partia1833973666xt_a_b > partia96731725t_unit ).
thf(tp_units_1734235042t_unit,type,
units_1734235042t_unit: partia539144763t_unit > set_se1596668135od_a_a ).
thf(tp_units_390215097t_unit,type,
units_390215097t_unit: partia539144763t_unit > partia539144763t_unit ).
thf(tp_units_a_Product_unit,type,
units_a_Product_unit: partia96731725t_unit > set_a ).
thf(tp_units_a_ring_ext_a_b,type,
units_a_ring_ext_a_b: partia1833973666xt_a_b > set_a ).
thf(tp_zero_a_b,type,
zero_a_b: partia1833973666xt_a_b > a ).
thf(79,axiom,
! [G: partia539144763t_unit] :
( ( mult_s977248631t_unit @ ( units_390215097t_unit @ G ) )
= ( mult_s977248631t_unit @ G ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_276_units__of__mult) ).
thf(310,axiom,
monoid1022105667xt_a_b @ r,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_45_monoid__axioms) ).
thf(336,axiom,
ring_a_b @ r,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_local_Oring__axioms) ).
thf(338,axiom,
abelian_monoid_a_b @ r,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_17_abelian__monoid__axioms) ).
thf(342,axiom,
equiva2136214035t_unit @ rel,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_equiv__obj__rng__of__frac) ).
thf(344,axiom,
semiring_a_b @ r,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_local_Osemiring__axioms) ).
thf(345,axiom,
monoid1242292471t_unit @ ( locali1944243560ac_a_b @ r @ s ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_monoid__rng__of__frac) ).
thf(347,axiom,
locali425460998xt_a_b @ r @ s,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_submonoid__axioms) ).
thf(348,axiom,
locali1944243560ac_a_b = locali1944243560ac_a_b,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_eq__obj__rng__of__frac_Orec__monoid__rng__of__frac_Ocong) ).
thf(349,axiom,
locali880295127ng_a_b @ r @ s,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_mult__submonoid__of__rng__axioms) ).
thf(350,axiom,
locali807230110ng_a_b @ r @ s,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_mult__submonoid__of__crng__axioms) ).
thf(351,axiom,
( ( mult_s977248631t_unit @ ( locali1944243560ac_a_b @ r @ s ) @ ( locali1170246543t_unit @ rel @ r3 @ s3 ) @ ( locali1170246543t_unit @ rel @ r2 @ s2 ) )
= ( locali1170246543t_unit @ rel @ ( mult_a_ring_ext_a_b @ r @ r3 @ r2 ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ s2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_f2) ).
thf(352,axiom,
( ( mult_s977248631t_unit @ ( locali1944243560ac_a_b @ r @ s ) @ ( locali1170246543t_unit @ rel @ r2 @ s2 ) @ ( locali1170246543t_unit @ rel @ r3 @ s3 ) )
= ( locali1170246543t_unit @ rel @ ( mult_a_ring_ext_a_b @ r @ r2 @ r3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_f1) ).
thf(353,axiom,
locali1648887798ac_a_b @ r @ s,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_eq__obj__rng__of__frac__axioms) ).
thf(354,axiom,
( ( mult_a_ring_ext_a_b @ r @ s2 @ s3 )
= ( mult_a_ring_ext_a_b @ r @ s3 @ s2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_f4) ).
thf(355,axiom,
( ( mult_a_ring_ext_a_b @ r @ r2 @ r3 )
= ( mult_a_ring_ext_a_b @ r @ r3 @ r2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_f3) ).
thf(356,conjecture,
( ( mult_s977248631t_unit @ ( locali1944243560ac_a_b @ r @ s ) @ ( locali1170246543t_unit @ rel @ r2 @ s2 ) @ ( locali1170246543t_unit @ rel @ r3 @ s3 ) )
= ( mult_s977248631t_unit @ ( locali1944243560ac_a_b @ r @ s ) @ ( locali1170246543t_unit @ rel @ r3 @ s3 ) @ ( locali1170246543t_unit @ rel @ r2 @ s2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
thf(357,negated_conjecture,
( ( ( mult_s977248631t_unit @ ( locali1944243560ac_a_b @ r @ s ) @ ( locali1170246543t_unit @ rel @ r2 @ s2 ) @ ( locali1170246543t_unit @ rel @ r3 @ s3 ) )
= ( mult_s977248631t_unit @ ( locali1944243560ac_a_b @ r @ s ) @ ( locali1170246543t_unit @ rel @ r3 @ s3 ) @ ( locali1170246543t_unit @ rel @ r2 @ s2 ) ) )
= $false ),
inference(negate_conjecture,[status(cth)],[356]) ).
thf(358,plain,
( ( ( mult_s977248631t_unit @ ( locali1944243560ac_a_b @ r @ s ) @ ( locali1170246543t_unit @ rel @ r2 @ s2 ) @ ( locali1170246543t_unit @ rel @ r3 @ s3 ) )
= ( mult_s977248631t_unit @ ( locali1944243560ac_a_b @ r @ s ) @ ( locali1170246543t_unit @ rel @ r3 @ s3 ) @ ( locali1170246543t_unit @ rel @ r2 @ s2 ) ) )
= $false ),
inference(unfold_def,[status(thm)],[357]) ).
thf(359,plain,
( ( ! [G: partia539144763t_unit] :
( ( mult_s977248631t_unit @ ( units_390215097t_unit @ G ) )
= ( mult_s977248631t_unit @ G ) ) )
= $true ),
inference(unfold_def,[status(thm)],[79]) ).
thf(360,plain,
( ( monoid1022105667xt_a_b @ r )
= $true ),
inference(unfold_def,[status(thm)],[310]) ).
thf(361,plain,
( ( ring_a_b @ r )
= $true ),
inference(unfold_def,[status(thm)],[336]) ).
thf(362,plain,
( ( abelian_monoid_a_b @ r )
= $true ),
inference(unfold_def,[status(thm)],[338]) ).
thf(363,plain,
( ( equiva2136214035t_unit @ rel )
= $true ),
inference(unfold_def,[status(thm)],[342]) ).
thf(364,plain,
( ( semiring_a_b @ r )
= $true ),
inference(unfold_def,[status(thm)],[344]) ).
thf(365,plain,
( ( monoid1242292471t_unit @ ( locali1944243560ac_a_b @ r @ s ) )
= $true ),
inference(unfold_def,[status(thm)],[345]) ).
thf(366,plain,
( ( locali425460998xt_a_b @ r @ s )
= $true ),
inference(unfold_def,[status(thm)],[347]) ).
thf(367,plain,
( ( locali1944243560ac_a_b = locali1944243560ac_a_b )
= $true ),
inference(unfold_def,[status(thm)],[348]) ).
thf(368,plain,
( ( locali880295127ng_a_b @ r @ s )
= $true ),
inference(unfold_def,[status(thm)],[349]) ).
thf(369,plain,
( ( locali807230110ng_a_b @ r @ s )
= $true ),
inference(unfold_def,[status(thm)],[350]) ).
thf(370,plain,
( ( ( mult_s977248631t_unit @ ( locali1944243560ac_a_b @ r @ s ) @ ( locali1170246543t_unit @ rel @ r3 @ s3 ) @ ( locali1170246543t_unit @ rel @ r2 @ s2 ) )
= ( locali1170246543t_unit @ rel @ ( mult_a_ring_ext_a_b @ r @ r3 @ r2 ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ s2 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[351]) ).
thf(371,plain,
( ( ( mult_s977248631t_unit @ ( locali1944243560ac_a_b @ r @ s ) @ ( locali1170246543t_unit @ rel @ r2 @ s2 ) @ ( locali1170246543t_unit @ rel @ r3 @ s3 ) )
= ( locali1170246543t_unit @ rel @ ( mult_a_ring_ext_a_b @ r @ r2 @ r3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[352]) ).
thf(372,plain,
( ( locali1648887798ac_a_b @ r @ s )
= $true ),
inference(unfold_def,[status(thm)],[353]) ).
thf(373,plain,
( ( ( mult_a_ring_ext_a_b @ r @ s2 @ s3 )
= ( mult_a_ring_ext_a_b @ r @ s3 @ s2 ) )
= $true ),
inference(unfold_def,[status(thm)],[354]) ).
thf(374,plain,
( ( ( mult_a_ring_ext_a_b @ r @ r2 @ r3 )
= ( mult_a_ring_ext_a_b @ r @ r3 @ r2 ) )
= $true ),
inference(unfold_def,[status(thm)],[355]) ).
thf(375,plain,
( ( ( mult_s977248631t_unit @ ( locali1944243560ac_a_b @ r @ s ) @ ( locali1170246543t_unit @ rel @ r2 @ s2 ) @ ( locali1170246543t_unit @ rel @ r3 @ s3 ) )
!= ( mult_s977248631t_unit @ ( locali1944243560ac_a_b @ r @ s ) @ ( locali1170246543t_unit @ rel @ r3 @ s3 ) @ ( locali1170246543t_unit @ rel @ r2 @ s2 ) ) )
= $true ),
inference(polarity_switch,[status(thm)],[358]) ).
thf(376,plain,
( ( ( mult_a_ring_ext_a_b @ r @ r2 @ r3 )
= ( mult_a_ring_ext_a_b @ r @ r3 @ r2 ) )
= $true ),
inference(copy,[status(thm)],[374]) ).
thf(377,plain,
( ( ( mult_a_ring_ext_a_b @ r @ s2 @ s3 )
= ( mult_a_ring_ext_a_b @ r @ s3 @ s2 ) )
= $true ),
inference(copy,[status(thm)],[373]) ).
thf(378,plain,
( ( locali1648887798ac_a_b @ r @ s )
= $true ),
inference(copy,[status(thm)],[372]) ).
thf(379,plain,
( ( ( mult_s977248631t_unit @ ( locali1944243560ac_a_b @ r @ s ) @ ( locali1170246543t_unit @ rel @ r2 @ s2 ) @ ( locali1170246543t_unit @ rel @ r3 @ s3 ) )
= ( locali1170246543t_unit @ rel @ ( mult_a_ring_ext_a_b @ r @ r2 @ r3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) )
= $true ),
inference(copy,[status(thm)],[371]) ).
thf(380,plain,
( ( ( mult_s977248631t_unit @ ( locali1944243560ac_a_b @ r @ s ) @ ( locali1170246543t_unit @ rel @ r3 @ s3 ) @ ( locali1170246543t_unit @ rel @ r2 @ s2 ) )
= ( locali1170246543t_unit @ rel @ ( mult_a_ring_ext_a_b @ r @ r3 @ r2 ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ s2 ) ) )
= $true ),
inference(copy,[status(thm)],[370]) ).
thf(381,plain,
( ( locali807230110ng_a_b @ r @ s )
= $true ),
inference(copy,[status(thm)],[369]) ).
thf(382,plain,
( ( locali880295127ng_a_b @ r @ s )
= $true ),
inference(copy,[status(thm)],[368]) ).
thf(383,plain,
( ( locali1944243560ac_a_b = locali1944243560ac_a_b )
= $true ),
inference(copy,[status(thm)],[367]) ).
thf(384,plain,
( ( locali425460998xt_a_b @ r @ s )
= $true ),
inference(copy,[status(thm)],[366]) ).
thf(385,plain,
( ( monoid1242292471t_unit @ ( locali1944243560ac_a_b @ r @ s ) )
= $true ),
inference(copy,[status(thm)],[365]) ).
thf(386,plain,
( ( semiring_a_b @ r )
= $true ),
inference(copy,[status(thm)],[364]) ).
thf(387,plain,
( ( equiva2136214035t_unit @ rel )
= $true ),
inference(copy,[status(thm)],[363]) ).
thf(388,plain,
( ( abelian_monoid_a_b @ r )
= $true ),
inference(copy,[status(thm)],[362]) ).
thf(389,plain,
( ( ring_a_b @ r )
= $true ),
inference(copy,[status(thm)],[361]) ).
thf(390,plain,
( ( monoid1022105667xt_a_b @ r )
= $true ),
inference(copy,[status(thm)],[360]) ).
thf(391,plain,
( ( ! [G: partia539144763t_unit] :
( ( mult_s977248631t_unit @ ( units_390215097t_unit @ G ) )
= ( mult_s977248631t_unit @ G ) ) )
= $true ),
inference(copy,[status(thm)],[359]) ).
thf(392,plain,
( ( ( mult_s977248631t_unit @ ( locali1944243560ac_a_b @ r @ s ) @ ( locali1170246543t_unit @ rel @ r2 @ s2 ) @ ( locali1170246543t_unit @ rel @ r3 @ s3 ) )
!= ( mult_s977248631t_unit @ ( locali1944243560ac_a_b @ r @ s ) @ ( locali1170246543t_unit @ rel @ r3 @ s3 ) @ ( locali1170246543t_unit @ rel @ r2 @ s2 ) ) )
= $true ),
inference(copy,[status(thm)],[375]) ).
thf(393,plain,
( ( ! [SV1: partia1833973666xt_a_b] :
( ( locali1944243560ac_a_b @ SV1 )
= ( locali1944243560ac_a_b @ SV1 ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[383]) ).
thf(394,plain,
( ( locali1944243560ac_a_b = locali1944243560ac_a_b )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[383]) ).
thf(395,plain,
! [SV2: partia539144763t_unit] :
( ( ( mult_s977248631t_unit @ ( units_390215097t_unit @ SV2 ) )
= ( mult_s977248631t_unit @ SV2 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[391]) ).
thf(396,plain,
( ( ( mult_s977248631t_unit @ ( locali1944243560ac_a_b @ r @ s ) @ ( locali1170246543t_unit @ rel @ r2 @ s2 ) @ ( locali1170246543t_unit @ rel @ r3 @ s3 ) )
= ( mult_s977248631t_unit @ ( locali1944243560ac_a_b @ r @ s ) @ ( locali1170246543t_unit @ rel @ r3 @ s3 ) @ ( locali1170246543t_unit @ rel @ r2 @ s2 ) ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[392]) ).
thf(397,plain,
! [SV3: partia1833973666xt_a_b] :
( ( ( locali1944243560ac_a_b @ SV3 )
= ( locali1944243560ac_a_b @ SV3 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[393]) ).
thf(398,plain,
! [SV2: partia539144763t_unit] :
( ( ! [SV4: set_Product_prod_a_a] :
( ( mult_s977248631t_unit @ ( units_390215097t_unit @ SV2 ) @ SV4 )
= ( mult_s977248631t_unit @ SV2 @ SV4 ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[395]) ).
thf(399,plain,
! [SV2: partia539144763t_unit] :
( ( ( mult_s977248631t_unit @ ( units_390215097t_unit @ SV2 ) )
= ( mult_s977248631t_unit @ SV2 ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[395]) ).
thf(400,plain,
! [SV3: partia1833973666xt_a_b] :
( ( ! [SV5: set_a] :
( ( locali1944243560ac_a_b @ SV3 @ SV5 )
= ( locali1944243560ac_a_b @ SV3 @ SV5 ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[397]) ).
thf(401,plain,
! [SV3: partia1833973666xt_a_b] :
( ( ( locali1944243560ac_a_b @ SV3 )
= ( locali1944243560ac_a_b @ SV3 ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[397]) ).
thf(402,plain,
! [SV6: set_Product_prod_a_a,SV2: partia539144763t_unit] :
( ( ( mult_s977248631t_unit @ ( units_390215097t_unit @ SV2 ) @ SV6 )
= ( mult_s977248631t_unit @ SV2 @ SV6 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[398]) ).
thf(403,plain,
! [SV7: set_a,SV3: partia1833973666xt_a_b] :
( ( ( locali1944243560ac_a_b @ SV3 @ SV7 )
= ( locali1944243560ac_a_b @ SV3 @ SV7 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[400]) ).
thf(404,plain,
! [SV6: set_Product_prod_a_a,SV2: partia539144763t_unit] :
( ( ! [SV8: set_Product_prod_a_a] :
( ( mult_s977248631t_unit @ ( units_390215097t_unit @ SV2 ) @ SV6 @ SV8 )
= ( mult_s977248631t_unit @ SV2 @ SV6 @ SV8 ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[402]) ).
thf(405,plain,
! [SV6: set_Product_prod_a_a,SV2: partia539144763t_unit] :
( ( ( mult_s977248631t_unit @ ( units_390215097t_unit @ SV2 ) @ SV6 )
= ( mult_s977248631t_unit @ SV2 @ SV6 ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[402]) ).
thf(406,plain,
! [SV9: set_Product_prod_a_a,SV6: set_Product_prod_a_a,SV2: partia539144763t_unit] :
( ( ( mult_s977248631t_unit @ ( units_390215097t_unit @ SV2 ) @ SV6 @ SV9 )
= ( mult_s977248631t_unit @ SV2 @ SV6 @ SV9 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[404]) ).
thf(407,plain,
$false = $true,
inference(fo_atp_e,[status(thm)],[376,406,405,403,401,399,396,394,390,389,388,387,386,385,384,382,381,380,379,378,377]) ).
thf(408,plain,
$false,
inference(solved_all_splits,[solved_all_splits(join,[])],[407]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP107^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.17 % Computer : n009.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Tue Oct 6 11:17:32 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.78/0.53 ..
% 1.78/0.53
% 1.78/0.53 No.of.Axioms: 16
% 1.78/0.53
% 1.78/0.53 Length.of.Defs: 0
% 1.78/0.53
% 1.78/0.53 Contains.Choice.Funs: false
% 1.78/0.53 ....
% 1.78/0.53
% 1.78/0.53 ********************************
% 1.78/0.53 * All subproblems solved! *
% 1.78/0.53 ********************************
% 1.78/0.53 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:1,axioms:16,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:407,loop_count:0,foatp_calls:1,translation:fof_full)
% 1.78/0.53
% 1.78/0.53 %**** Beginning of derivation protocol ****
% 1.78/0.53 % SZS output start CNFRefutation
% See solution above
% 1.78/0.53
% 1.78/0.53 %**** End of derivation protocol ****
% 1.78/0.53 %**** no. of clauses in derivation: 69 ****
% 1.78/0.53 %**** clause counter: 407 ****
% 1.78/0.53
% 1.78/0.53 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:1,axioms:16,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:407,loop_count:0,foatp_calls:1,translation:fof_full)
%------------------------------------------------------------------------------