%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : ITP106^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 : n018.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 2.67s 0.65s
% Output : CNFRefutation 2.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 30
% Syntax : Number of formulae : 245 ( 146 unt; 0 typ; 0 def)
% Number of atoms : 1188 ( 755 equ; 0 cnn)
% Maximal formula atoms : 3 ( 4 avg)
% Number of connectives : 3205 ( 377 ~; 257 |; 6 &;2541 @)
% ( 0 <=>; 24 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Number of types : 11 ( 10 usr)
% Number of type conns : 41 ( 41 >; 0 *; 0 +; 0 <<)
% Number of symbols : 57 ( 54 usr; 10 con; 0-3 aty)
% Number of variables : 638 ( 4 ^; 628 !; 6 ?; 638 :)
% Comments :
%------------------------------------------------------------------------------
thf(tp_a,type,
a: $tType ).
thf(tp_b,type,
b: $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_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_a_inv_a_b,type,
a_inv_a_b: partia1833973666xt_a_b > a > a ).
thf(tp_a_minus_a_b,type,
a_minus_a_b: partia1833973666xt_a_b > a > a > a ).
thf(tp_abelian_group_a_b,type,
abelian_group_a_b: partia1833973666xt_a_b > $o ).
thf(tp_add_a_b,type,
add_a_b: partia1833973666xt_a_b > a > a > a ).
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_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_comm_g1684316527t_unit,type,
comm_g1684316527t_unit: partia96731725t_unit > $o ).
thf(tp_comm_g791708116xt_a_b,type,
comm_g791708116xt_a_b: partia1833973666xt_a_b > $o ).
thf(tp_field_a_b,type,
field_a_b: partia1833973666xt_a_b > $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_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_minus_minus_int,type,
minus_minus_int: int > int > int ).
thf(tp_minus_minus_nat,type,
minus_minus_nat: nat > nat > nat ).
thf(tp_more_a_b,type,
more_a_b: partia1833973666xt_a_b > b ).
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_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_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_plus_plus_int,type,
plus_plus_int: int > int > int ).
thf(tp_plus_plus_nat,type,
plus_plus_nat: nat > nat > nat ).
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_r4,type,
r4: a ).
thf(tp_rel,type,
rel: partia1993116613t_unit ).
thf(tp_s,type,
s: a ).
thf(tp_s2,type,
s2: a ).
thf(tp_s3,type,
s3: a ).
thf(tp_sK1_SY52,type,
sK1_SY52: product_prod_a_a > a ).
thf(tp_sK2_SY54,type,
sK2_SY54: product_prod_a_a > a ).
thf(tp_sK3_SY85,type,
sK3_SY85: product_prod_a_a > a ).
thf(tp_sK4_SY57,type,
sK4_SY57: product_prod_a_a > ( product_prod_a_a > $o ) > a ).
thf(tp_sK5_SY60,type,
sK5_SY60: product_prod_a_a > ( product_prod_a_a > $o ) > a ).
thf(tp_sK6_SY84,type,
sK6_SY84: product_prod_a_a > a ).
thf(tp_sK7_SY88,type,
sK7_SY88: product_prod_a_a > ( product_prod_a_a > $o ) > a ).
thf(tp_sK8_SY89,type,
sK8_SY89: product_prod_a_a > ( product_prod_a_a > $o ) > a ).
thf(tp_semiri1382578993at_nat,type,
semiri1382578993at_nat: nat > nat ).
thf(tp_semiri2019852685at_int,type,
semiri2019852685at_int: nat > int ).
thf(tp_semiring_a_b,type,
semiring_a_b: partia1833973666xt_a_b > $o ).
thf(tp_suc,type,
suc: nat > nat ).
thf(tp_uminus_uminus_int,type,
uminus_uminus_int: int > int ).
thf(tp_units_1411277569xt_a_b,type,
units_1411277569xt_a_b: partia1833973666xt_a_b > partia96731725t_unit ).
thf(tp_units_873712258t_unit,type,
units_873712258t_unit: partia96731725t_unit > partia96731725t_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(175,axiom,
abelian_group_a_b @ r,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_107_is__abelian__group) ).
thf(222,axiom,
! [P2: product_prod_a_a] :
? [X3: a,Y4: a] :
( P2
= ( product_Pair_a_a @ X3 @ Y4 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_60_surj__pair) ).
thf(223,axiom,
! [P: product_prod_a_a > $o,P2: product_prod_a_a] :
( ! [A4: a,B3: a] : ( P @ ( product_Pair_a_a @ A4 @ B3 ) )
=> ( P @ P2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_59_prod__cases) ).
thf(224,axiom,
! [A: a,B: a,A2: a,B2: a] :
( ( ( product_Pair_a_a @ A @ B )
= ( product_Pair_a_a @ A2 @ B2 ) )
=> ~ ( ( A = A2 )
=> ( B != B2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_58_Pair__inject) ).
thf(225,axiom,
! [Y: product_prod_a_a] :
~ ! [A4: a,B3: a] :
( Y
!= ( product_Pair_a_a @ A4 @ B3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_57_old_Oprod_Oexhaust) ).
thf(226,axiom,
! [P: product_prod_a_a > $o,Prod: product_prod_a_a] :
( ! [A4: a,B3: a] : ( P @ ( product_Pair_a_a @ A4 @ B3 ) )
=> ( P @ Prod ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_56_old_Oprod_Oinducts) ).
thf(235,axiom,
! [A3: set_Product_prod_a_a] :
( ( collec645855634od_a_a
@ ^ [X4: product_prod_a_a] : ( member449909584od_a_a @ X4 @ A3 ) )
= A3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_47_Collect__mem__eq) ).
thf(237,axiom,
! [A: product_prod_a_a,P: product_prod_a_a > $o] :
( ( member449909584od_a_a @ A @ ( collec645855634od_a_a @ P ) )
= ( P @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_45_mem__Collect__eq) ).
thf(253,axiom,
! [A: a,B: a,C: a] :
( ( A = B )
=> ( ( a_minus_a_b @ r @ C @ A )
= ( a_minus_a_b @ r @ C @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_local_Oright__minus__eq) ).
thf(260,axiom,
semiring_a_b @ r,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_local_Osemiring__axioms) ).
thf(261,axiom,
! [A: a,B: a,A2: a,B2: a] :
( ( ( product_Pair_a_a @ A @ B )
= ( product_Pair_a_a @ A2 @ B2 ) )
= ( ( A = A2 )
& ( B = B2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21_old_Oprod_Oinject) ).
thf(262,axiom,
! [X1: a,X2: a,Y1: a,Y2: a] :
( ( ( product_Pair_a_a @ X1 @ X2 )
= ( product_Pair_a_a @ Y1 @ Y2 ) )
= ( ( X1 = Y1 )
& ( X2 = Y2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_20_prod_Oinject) ).
thf(266,axiom,
member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ r2 ) @ ( mult_a_ring_ext_a_b @ r @ s @ r3 ) ) @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s2 ) @ s3 ) ) @ ( partia206007992t_unit @ rel ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_f12) ).
thf(267,axiom,
( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s2 ) @ s3 ) @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) )
= ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s2 ) @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s2 ) @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15_f8) ).
thf(268,axiom,
( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ r2 ) @ ( mult_a_ring_ext_a_b @ r @ s @ r3 ) ) @ r4 ) )
= ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ r2 ) @ r4 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ r3 ) @ r4 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_f7) ).
thf(269,axiom,
( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ r2 ) @ ( mult_a_ring_ext_a_b @ r @ s @ r3 ) ) @ r4 ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s2 ) @ s3 ) @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13__092_060open_062s_A_092_060otimes_062_As_H_H_A_092_060otimes_062_A_Is_H_A_092_060otimes_062_As_H_H_J_A_092_060otimes_062_A_I_Is_H_A_092_060otimes_062_Ar_A_092_060oplus_062_As_A_092_060otimes_062_Ar_H_J_A_092_060otimes_062_Ar_H_H_J_A_061_As_A_092_060otimes_062_As_H_A_092_060otimes_062_As_H_H_A_092_060otimes_062_A_Is_H_A_092_060otimes_062_As_H_H_A_092_060otimes_062_A_Ir_A_092_060otimes_062_Ar_H_H_J_A_092_060oplus_062_As_A_092_060otimes_062_As_H_H_A_092_060otimes_062_A_Ir_H_A_092_060otimes_062_Ar_H_H_J_J_092_060close_062) ).
thf(270,axiom,
( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ r2 ) @ ( mult_a_ring_ext_a_b @ r @ s @ r3 ) ) @ r4 ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ r2 ) @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ r3 ) @ r4 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12__092_060open_062s_A_092_060otimes_062_As_H_H_A_092_060otimes_062_A_Is_H_A_092_060otimes_062_As_H_H_J_A_092_060otimes_062_A_I_Is_H_A_092_060otimes_062_Ar_A_092_060oplus_062_As_A_092_060otimes_062_Ar_H_J_A_092_060otimes_062_Ar_H_H_J_A_061_As_A_092_060otimes_062_As_H_H_A_092_060otimes_062_A_Is_H_A_092_060otimes_062_As_H_H_J_A_092_060otimes_062_A_Is_H_A_092_060otimes_062_Ar_A_092_060otimes_062_Ar_H_H_A_092_060oplus_062_As_A_092_060otimes_062_Ar_H_A_092_060otimes_062_Ar_H_H_J_092_060close_062) ).
thf(271,axiom,
member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) ) @ ( partia206007992t_unit @ rel ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_f4) ).
thf(272,axiom,
member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( partia206007992t_unit @ rel ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_f5) ).
thf(273,axiom,
( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ r2 ) @ r4 ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s2 ) @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_f10) ).
thf(274,axiom,
( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ r3 ) @ r4 ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s2 ) @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8__092_060open_062s_A_092_060otimes_062_As_H_H_A_092_060otimes_062_A_Is_H_A_092_060otimes_062_As_H_H_J_A_092_060otimes_062_A_Is_A_092_060otimes_062_Ar_H_A_092_060otimes_062_Ar_H_H_J_A_061_As_A_092_060otimes_062_As_H_A_092_060otimes_062_As_H_H_A_092_060otimes_062_A_Is_A_092_060otimes_062_As_H_H_A_092_060otimes_062_A_Ir_H_A_092_060otimes_062_Ar_H_H_J_J_092_060close_062) ).
thf(275,axiom,
( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s3 @ s ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7__092_060open_062s_A_092_060otimes_062_As_H_H_A_092_060otimes_062_A_Ir_H_A_092_060otimes_062_Ar_H_H_J_A_061_As_H_H_A_092_060otimes_062_As_A_092_060otimes_062_A_Ir_H_A_092_060otimes_062_Ar_H_H_J_092_060close_062) ).
thf(276,axiom,
( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s2 ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ s3 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_f9) ).
thf(277,axiom,
( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ ( mult_a_ring_ext_a_b @ r @ s3 @ s2 ) ) @ s3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5__092_060open_062s_A_092_060otimes_062_As_H_H_A_092_060otimes_062_A_Is_H_A_092_060otimes_062_As_H_H_J_A_061_As_A_092_060otimes_062_A_Is_H_H_A_092_060otimes_062_As_H_J_A_092_060otimes_062_As_H_H_092_060close_062) ).
thf(278,axiom,
! [R: a,S: a,R2: a,S2: a] :
( ( member449909584od_a_a @ ( product_Pair_a_a @ R @ S ) @ ( partia206007992t_unit @ rel ) )
=> ( ( member449909584od_a_a @ ( product_Pair_a_a @ R2 @ S2 ) @ ( partia206007992t_unit @ rel ) )
=> ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ S2 @ R ) @ ( mult_a_ring_ext_a_b @ r @ S @ R2 ) ) @ ( mult_a_ring_ext_a_b @ r @ S @ S2 ) ) @ ( partia206007992t_unit @ rel ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_closed__rel__add) ).
thf(279,axiom,
member449909584od_a_a @ ( product_Pair_a_a @ r2 @ s ) @ ( partia206007992t_unit @ rel ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_assms_I1_J) ).
thf(280,axiom,
member449909584od_a_a @ ( product_Pair_a_a @ r3 @ s2 ) @ ( partia206007992t_unit @ rel ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_assms_I2_J) ).
thf(281,axiom,
member449909584od_a_a @ ( product_Pair_a_a @ r4 @ s3 ) @ ( partia206007992t_unit @ rel ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_assms_I3_J) ).
thf(282,axiom,
! [A: a,B: a,C: a] :
( ( A = B )
=> ( ( add_a_b @ r @ C @ A )
= ( add_a_b @ r @ C @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_right__add__eq) ).
thf(283,conjecture,
member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) ) @ ( partia206007992t_unit @ rel ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
thf(284,negated_conjecture,
( ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) ) @ ( partia206007992t_unit @ rel ) )
= $false ),
inference(negate_conjecture,[status(cth)],[283]) ).
thf(285,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) ) @ ( partia206007992t_unit @ rel ) )
= $false ),
inference(unfold_def,[status(thm)],[284]) ).
thf(286,plain,
( ( abelian_group_a_b @ r )
= $true ),
inference(unfold_def,[status(thm)],[175]) ).
thf(287,plain,
( ( ! [P2: product_prod_a_a] :
? [X3: a,Y4: a] :
( P2
= ( product_Pair_a_a @ X3 @ Y4 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[222]) ).
thf(288,plain,
( ( ! [P: product_prod_a_a > $o,P2: product_prod_a_a] :
( ! [A4: a,B3: a] : ( P @ ( product_Pair_a_a @ A4 @ B3 ) )
=> ( P @ P2 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[223]) ).
thf(289,plain,
( ( ! [A: a,B: a,A2: a,B2: a] :
( ( ( product_Pair_a_a @ A @ B )
= ( product_Pair_a_a @ A2 @ B2 ) )
=> ~ ( ( A = A2 )
=> ( B != B2 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[224]) ).
thf(290,plain,
( ( ! [Y: product_prod_a_a] :
~ ! [A4: a,B3: a] :
( Y
!= ( product_Pair_a_a @ A4 @ B3 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[225]) ).
thf(291,plain,
( ( ! [P: product_prod_a_a > $o,Prod: product_prod_a_a] :
( ! [A4: a,B3: a] : ( P @ ( product_Pair_a_a @ A4 @ B3 ) )
=> ( P @ Prod ) ) )
= $true ),
inference(unfold_def,[status(thm)],[226]) ).
thf(292,plain,
( ( ! [A3: set_Product_prod_a_a] :
( ( collec645855634od_a_a
@ ^ [X4: product_prod_a_a] : ( member449909584od_a_a @ X4 @ A3 ) )
= A3 ) )
= $true ),
inference(unfold_def,[status(thm)],[235]) ).
thf(293,plain,
( ( ! [A: product_prod_a_a,P: product_prod_a_a > $o] :
( ( member449909584od_a_a @ A @ ( collec645855634od_a_a @ P ) )
= ( P @ A ) ) )
= $true ),
inference(unfold_def,[status(thm)],[237]) ).
thf(294,plain,
( ( ! [A: a,B: a,C: a] :
( ( A = B )
=> ( ( a_minus_a_b @ r @ C @ A )
= ( a_minus_a_b @ r @ C @ B ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[253]) ).
thf(295,plain,
( ( semiring_a_b @ r )
= $true ),
inference(unfold_def,[status(thm)],[260]) ).
thf(296,plain,
( ( ! [A: a,B: a,A2: a,B2: a] :
( ( ( product_Pair_a_a @ A @ B )
= ( product_Pair_a_a @ A2 @ B2 ) )
= ( ( A = A2 )
& ( B = B2 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[261]) ).
thf(297,plain,
( ( ! [X1: a,X2: a,Y1: a,Y2: a] :
( ( ( product_Pair_a_a @ X1 @ X2 )
= ( product_Pair_a_a @ Y1 @ Y2 ) )
= ( ( X1 = Y1 )
& ( X2 = Y2 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[262]) ).
thf(298,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ r2 ) @ ( mult_a_ring_ext_a_b @ r @ s @ r3 ) ) @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s2 ) @ s3 ) ) @ ( partia206007992t_unit @ rel ) )
= $true ),
inference(unfold_def,[status(thm)],[266]) ).
thf(299,plain,
( ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s2 ) @ s3 ) @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) )
= ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s2 ) @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s2 ) @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[267]) ).
thf(300,plain,
( ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ r2 ) @ ( mult_a_ring_ext_a_b @ r @ s @ r3 ) ) @ r4 ) )
= ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ r2 ) @ r4 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ r3 ) @ r4 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[268]) ).
thf(301,plain,
( ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ r2 ) @ ( mult_a_ring_ext_a_b @ r @ s @ r3 ) ) @ r4 ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s2 ) @ s3 ) @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[269]) ).
thf(302,plain,
( ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ r2 ) @ ( mult_a_ring_ext_a_b @ r @ s @ r3 ) ) @ r4 ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ r2 ) @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ r3 ) @ r4 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[270]) ).
thf(303,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) ) @ ( partia206007992t_unit @ rel ) )
= $true ),
inference(unfold_def,[status(thm)],[271]) ).
thf(304,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( partia206007992t_unit @ rel ) )
= $true ),
inference(unfold_def,[status(thm)],[272]) ).
thf(305,plain,
( ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ r2 ) @ r4 ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s2 ) @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[273]) ).
thf(306,plain,
( ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ r3 ) @ r4 ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s2 ) @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[274]) ).
thf(307,plain,
( ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s3 @ s ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[275]) ).
thf(308,plain,
( ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s2 ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ s3 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[276]) ).
thf(309,plain,
( ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ ( mult_a_ring_ext_a_b @ r @ s3 @ s2 ) ) @ s3 ) )
= $true ),
inference(unfold_def,[status(thm)],[277]) ).
thf(310,plain,
( ( ! [R: a,S: a,R2: a,S2: a] :
( ( member449909584od_a_a @ ( product_Pair_a_a @ R @ S ) @ ( partia206007992t_unit @ rel ) )
=> ( ( member449909584od_a_a @ ( product_Pair_a_a @ R2 @ S2 ) @ ( partia206007992t_unit @ rel ) )
=> ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ S2 @ R ) @ ( mult_a_ring_ext_a_b @ r @ S @ R2 ) ) @ ( mult_a_ring_ext_a_b @ r @ S @ S2 ) ) @ ( partia206007992t_unit @ rel ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[278]) ).
thf(311,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ r2 @ s ) @ ( partia206007992t_unit @ rel ) )
= $true ),
inference(unfold_def,[status(thm)],[279]) ).
thf(312,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ r3 @ s2 ) @ ( partia206007992t_unit @ rel ) )
= $true ),
inference(unfold_def,[status(thm)],[280]) ).
thf(313,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ r4 @ s3 ) @ ( partia206007992t_unit @ rel ) )
= $true ),
inference(unfold_def,[status(thm)],[281]) ).
thf(314,plain,
( ( ! [A: a,B: a,C: a] :
( ( A = B )
=> ( ( add_a_b @ r @ C @ A )
= ( add_a_b @ r @ C @ B ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[282]) ).
thf(315,plain,
( ( ~ ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) ) @ ( partia206007992t_unit @ rel ) ) )
= $true ),
inference(polarity_switch,[status(thm)],[285]) ).
thf(316,plain,
( ( ! [A: a,B: a,C: a] :
( ( A = B )
=> ( ( add_a_b @ r @ C @ A )
= ( add_a_b @ r @ C @ B ) ) ) )
= $true ),
inference(copy,[status(thm)],[314]) ).
thf(317,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ r4 @ s3 ) @ ( partia206007992t_unit @ rel ) )
= $true ),
inference(copy,[status(thm)],[313]) ).
thf(318,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ r3 @ s2 ) @ ( partia206007992t_unit @ rel ) )
= $true ),
inference(copy,[status(thm)],[312]) ).
thf(319,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ r2 @ s ) @ ( partia206007992t_unit @ rel ) )
= $true ),
inference(copy,[status(thm)],[311]) ).
thf(320,plain,
( ( ! [R: a,S: a,R2: a,S2: a] :
( ( member449909584od_a_a @ ( product_Pair_a_a @ R @ S ) @ ( partia206007992t_unit @ rel ) )
=> ( ( member449909584od_a_a @ ( product_Pair_a_a @ R2 @ S2 ) @ ( partia206007992t_unit @ rel ) )
=> ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ S2 @ R ) @ ( mult_a_ring_ext_a_b @ r @ S @ R2 ) ) @ ( mult_a_ring_ext_a_b @ r @ S @ S2 ) ) @ ( partia206007992t_unit @ rel ) ) ) ) )
= $true ),
inference(copy,[status(thm)],[310]) ).
thf(321,plain,
( ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ ( mult_a_ring_ext_a_b @ r @ s3 @ s2 ) ) @ s3 ) )
= $true ),
inference(copy,[status(thm)],[309]) ).
thf(322,plain,
( ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s2 ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ s3 ) ) )
= $true ),
inference(copy,[status(thm)],[308]) ).
thf(323,plain,
( ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s3 @ s ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) )
= $true ),
inference(copy,[status(thm)],[307]) ).
thf(324,plain,
( ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ r3 ) @ r4 ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s2 ) @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) )
= $true ),
inference(copy,[status(thm)],[306]) ).
thf(325,plain,
( ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ r2 ) @ r4 ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s2 ) @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) ) )
= $true ),
inference(copy,[status(thm)],[305]) ).
thf(326,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( partia206007992t_unit @ rel ) )
= $true ),
inference(copy,[status(thm)],[304]) ).
thf(327,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) ) @ ( partia206007992t_unit @ rel ) )
= $true ),
inference(copy,[status(thm)],[303]) ).
thf(328,plain,
( ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ r2 ) @ ( mult_a_ring_ext_a_b @ r @ s @ r3 ) ) @ r4 ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ r2 ) @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ r3 ) @ r4 ) ) ) )
= $true ),
inference(copy,[status(thm)],[302]) ).
thf(329,plain,
( ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ r2 ) @ ( mult_a_ring_ext_a_b @ r @ s @ r3 ) ) @ r4 ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s2 ) @ s3 ) @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) ) )
= $true ),
inference(copy,[status(thm)],[301]) ).
thf(330,plain,
( ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ r2 ) @ ( mult_a_ring_ext_a_b @ r @ s @ r3 ) ) @ r4 ) )
= ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ r2 ) @ r4 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ r3 ) @ r4 ) ) ) )
= $true ),
inference(copy,[status(thm)],[300]) ).
thf(331,plain,
( ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s2 ) @ s3 ) @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) )
= ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s2 ) @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s2 ) @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) ) )
= $true ),
inference(copy,[status(thm)],[299]) ).
thf(332,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ r2 ) @ ( mult_a_ring_ext_a_b @ r @ s @ r3 ) ) @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s2 ) @ s3 ) ) @ ( partia206007992t_unit @ rel ) )
= $true ),
inference(copy,[status(thm)],[298]) ).
thf(333,plain,
( ( ! [X1: a,X2: a,Y1: a,Y2: a] :
( ( ( product_Pair_a_a @ X1 @ X2 )
= ( product_Pair_a_a @ Y1 @ Y2 ) )
= ( ( X1 = Y1 )
& ( X2 = Y2 ) ) ) )
= $true ),
inference(copy,[status(thm)],[297]) ).
thf(334,plain,
( ( ! [A: a,B: a,A2: a,B2: a] :
( ( ( product_Pair_a_a @ A @ B )
= ( product_Pair_a_a @ A2 @ B2 ) )
= ( ( A = A2 )
& ( B = B2 ) ) ) )
= $true ),
inference(copy,[status(thm)],[296]) ).
thf(335,plain,
( ( semiring_a_b @ r )
= $true ),
inference(copy,[status(thm)],[295]) ).
thf(336,plain,
( ( ! [A: a,B: a,C: a] :
( ( A = B )
=> ( ( a_minus_a_b @ r @ C @ A )
= ( a_minus_a_b @ r @ C @ B ) ) ) )
= $true ),
inference(copy,[status(thm)],[294]) ).
thf(337,plain,
( ( ! [A: product_prod_a_a,P: product_prod_a_a > $o] :
( ( member449909584od_a_a @ A @ ( collec645855634od_a_a @ P ) )
= ( P @ A ) ) )
= $true ),
inference(copy,[status(thm)],[293]) ).
thf(338,plain,
( ( ! [A3: set_Product_prod_a_a] :
( ( collec645855634od_a_a
@ ^ [X4: product_prod_a_a] : ( member449909584od_a_a @ X4 @ A3 ) )
= A3 ) )
= $true ),
inference(copy,[status(thm)],[292]) ).
thf(339,plain,
( ( ! [P: product_prod_a_a > $o,Prod: product_prod_a_a] :
( ! [A4: a,B3: a] : ( P @ ( product_Pair_a_a @ A4 @ B3 ) )
=> ( P @ Prod ) ) )
= $true ),
inference(copy,[status(thm)],[291]) ).
thf(340,plain,
( ( ! [Y: product_prod_a_a] :
~ ! [A4: a,B3: a] :
( Y
!= ( product_Pair_a_a @ A4 @ B3 ) ) )
= $true ),
inference(copy,[status(thm)],[290]) ).
thf(341,plain,
( ( ! [A: a,B: a,A2: a,B2: a] :
( ( ( product_Pair_a_a @ A @ B )
= ( product_Pair_a_a @ A2 @ B2 ) )
=> ~ ( ( A = A2 )
=> ( B != B2 ) ) ) )
= $true ),
inference(copy,[status(thm)],[289]) ).
thf(342,plain,
( ( ! [P: product_prod_a_a > $o,P2: product_prod_a_a] :
( ! [A4: a,B3: a] : ( P @ ( product_Pair_a_a @ A4 @ B3 ) )
=> ( P @ P2 ) ) )
= $true ),
inference(copy,[status(thm)],[288]) ).
thf(343,plain,
( ( ! [P2: product_prod_a_a] :
? [X3: a,Y4: a] :
( P2
= ( product_Pair_a_a @ X3 @ Y4 ) ) )
= $true ),
inference(copy,[status(thm)],[287]) ).
thf(344,plain,
( ( abelian_group_a_b @ r )
= $true ),
inference(copy,[status(thm)],[286]) ).
thf(345,plain,
( ( ~ ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) ) @ ( partia206007992t_unit @ rel ) ) )
= $true ),
inference(copy,[status(thm)],[315]) ).
thf(346,plain,
( ( ! [SX0: a,SX1: a,SX2: a] :
( ( SX0 != SX1 )
| ( ( a_minus_a_b @ r @ SX2 @ SX0 )
= ( a_minus_a_b @ r @ SX2 @ SX1 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[336]) ).
thf(347,plain,
( ( ! [SX0: a,SX1: a,SX2: a] :
( ( SX0 != SX1 )
| ( ( add_a_b @ r @ SX2 @ SX0 )
= ( add_a_b @ r @ SX2 @ SX1 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[316]) ).
thf(348,plain,
( ( ! [SX0: a,SX1: a,SX2: a,SX3: a] :
( ( ( product_Pair_a_a @ SX0 @ SX1 )
!= ( product_Pair_a_a @ SX2 @ SX3 ) )
| ~ ( ( SX0 != SX2 )
| ( SX1 != SX3 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[341]) ).
thf(349,plain,
( ( ! [SX0: a,SX1: a,SX2: a,SX3: a] :
( ~ ( member449909584od_a_a @ ( product_Pair_a_a @ SX0 @ SX1 ) @ ( partia206007992t_unit @ rel ) )
| ~ ( member449909584od_a_a @ ( product_Pair_a_a @ SX2 @ SX3 ) @ ( partia206007992t_unit @ rel ) )
| ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ SX3 @ SX0 ) @ ( mult_a_ring_ext_a_b @ r @ SX1 @ SX2 ) ) @ ( mult_a_ring_ext_a_b @ r @ SX1 @ SX3 ) ) @ ( partia206007992t_unit @ rel ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[320]) ).
thf(350,plain,
( ( ! [SX0: product_prod_a_a] :
~ ! [SX1: a] :
~ ~ ! [SX2: a] :
( SX0
!= ( product_Pair_a_a @ SX1 @ SX2 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[343]) ).
thf(351,plain,
( ( ! [SX0: product_prod_a_a] :
~ ! [SX1: a,SX2: a] :
( SX0
!= ( product_Pair_a_a @ SX1 @ SX2 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[340]) ).
thf(352,plain,
( ( ! [SX0: product_prod_a_a > $o,SX1: product_prod_a_a] :
( ~ ! [SX2: a,SX3: a] : ( SX0 @ ( product_Pair_a_a @ SX2 @ SX3 ) )
| ( SX0 @ SX1 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[342]) ).
thf(353,plain,
( ( ! [SX0: product_prod_a_a > $o,SX1: product_prod_a_a] :
( ~ ! [SX2: a,SX3: a] : ( SX0 @ ( product_Pair_a_a @ SX2 @ SX3 ) )
| ( SX0 @ SX1 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[339]) ).
thf(354,plain,
( ( ! [SX0: a,SX1: a,SX2: a,SX3: a] :
( ( ( product_Pair_a_a @ SX0 @ SX1 )
= ( product_Pair_a_a @ SX2 @ SX3 ) )
= ( ~ ( ( SX0 != SX2 )
| ( SX1 != SX3 ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[333]) ).
thf(355,plain,
( ( ! [SX0: a,SX1: a,SX2: a,SX3: a] :
( ( ( product_Pair_a_a @ SX0 @ SX1 )
= ( product_Pair_a_a @ SX2 @ SX3 ) )
= ( ~ ( ( SX0 != SX2 )
| ( SX1 != SX3 ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[334]) ).
thf(356,plain,
! [SV1: product_prod_a_a] :
( ( ! [SY40: product_prod_a_a > $o] :
( ( member449909584od_a_a @ SV1 @ ( collec645855634od_a_a @ SY40 ) )
= ( SY40 @ SV1 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[337]) ).
thf(357,plain,
! [SV2: set_Product_prod_a_a] :
( ( ( collec645855634od_a_a
@ ^ [SY41: product_prod_a_a] : ( member449909584od_a_a @ SY41 @ SV2 ) )
= SV2 )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[338]) ).
thf(358,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) ) @ ( partia206007992t_unit @ rel ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[345]) ).
thf(359,plain,
! [SV3: a] :
( ( ! [SY42: a,SY43: a] :
( ( SV3 != SY42 )
| ( ( a_minus_a_b @ r @ SY43 @ SV3 )
= ( a_minus_a_b @ r @ SY43 @ SY42 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[346]) ).
thf(360,plain,
! [SV4: a] :
( ( ! [SY44: a,SY45: a] :
( ( SV4 != SY44 )
| ( ( add_a_b @ r @ SY45 @ SV4 )
= ( add_a_b @ r @ SY45 @ SY44 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[347]) ).
thf(361,plain,
! [SV5: a] :
( ( ! [SY46: a,SY47: a,SY48: a] :
( ( ( product_Pair_a_a @ SV5 @ SY46 )
!= ( product_Pair_a_a @ SY47 @ SY48 ) )
| ~ ( ( SV5 != SY47 )
| ( SY46 != SY48 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[348]) ).
thf(362,plain,
! [SV6: a] :
( ( ! [SY49: a,SY50: a,SY51: a] :
( ~ ( member449909584od_a_a @ ( product_Pair_a_a @ SV6 @ SY49 ) @ ( partia206007992t_unit @ rel ) )
| ~ ( member449909584od_a_a @ ( product_Pair_a_a @ SY50 @ SY51 ) @ ( partia206007992t_unit @ rel ) )
| ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ SY51 @ SV6 ) @ ( mult_a_ring_ext_a_b @ r @ SY49 @ SY50 ) ) @ ( mult_a_ring_ext_a_b @ r @ SY49 @ SY51 ) ) @ ( partia206007992t_unit @ rel ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[349]) ).
thf(363,plain,
! [SV7: product_prod_a_a] :
( ( ~ ! [SY52: a] :
~ ~ ! [SY53: a] :
( SV7
!= ( product_Pair_a_a @ SY52 @ SY53 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[350]) ).
thf(364,plain,
! [SV8: product_prod_a_a] :
( ( ~ ! [SY54: a,SY55: a] :
( SV8
!= ( product_Pair_a_a @ SY54 @ SY55 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[351]) ).
thf(365,plain,
! [SV9: product_prod_a_a > $o] :
( ( ! [SY56: product_prod_a_a] :
( ~ ! [SY57: a,SY58: a] : ( SV9 @ ( product_Pair_a_a @ SY57 @ SY58 ) )
| ( SV9 @ SY56 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[352]) ).
thf(366,plain,
! [SV10: product_prod_a_a > $o] :
( ( ! [SY59: product_prod_a_a] :
( ~ ! [SY60: a,SY61: a] : ( SV10 @ ( product_Pair_a_a @ SY60 @ SY61 ) )
| ( SV10 @ SY59 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[353]) ).
thf(367,plain,
! [SV11: a] :
( ( ! [SY62: a,SY63: a,SY64: a] :
( ( ( product_Pair_a_a @ SV11 @ SY62 )
= ( product_Pair_a_a @ SY63 @ SY64 ) )
= ( ~ ( ( SV11 != SY63 )
| ( SY62 != SY64 ) ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[354]) ).
thf(368,plain,
! [SV12: a] :
( ( ! [SY65: a,SY66: a,SY67: a] :
( ( ( product_Pair_a_a @ SV12 @ SY65 )
= ( product_Pair_a_a @ SY66 @ SY67 ) )
= ( ~ ( ( SV12 != SY66 )
| ( SY65 != SY67 ) ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[355]) ).
thf(369,plain,
! [SV13: product_prod_a_a > $o,SV1: product_prod_a_a] :
( ( ( member449909584od_a_a @ SV1 @ ( collec645855634od_a_a @ SV13 ) )
= ( SV13 @ SV1 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[356]) ).
thf(370,plain,
! [SV14: a,SV3: a] :
( ( ! [SY68: a] :
( ( SV3 != SV14 )
| ( ( a_minus_a_b @ r @ SY68 @ SV3 )
= ( a_minus_a_b @ r @ SY68 @ SV14 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[359]) ).
thf(371,plain,
! [SV15: a,SV4: a] :
( ( ! [SY69: a] :
( ( SV4 != SV15 )
| ( ( add_a_b @ r @ SY69 @ SV4 )
= ( add_a_b @ r @ SY69 @ SV15 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[360]) ).
thf(372,plain,
! [SV16: a,SV5: a] :
( ( ! [SY70: a,SY71: a] :
( ( ( product_Pair_a_a @ SV5 @ SV16 )
!= ( product_Pair_a_a @ SY70 @ SY71 ) )
| ~ ( ( SV5 != SY70 )
| ( SV16 != SY71 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[361]) ).
thf(373,plain,
! [SV17: a,SV6: a] :
( ( ! [SY72: a,SY73: a] :
( ~ ( member449909584od_a_a @ ( product_Pair_a_a @ SV6 @ SV17 ) @ ( partia206007992t_unit @ rel ) )
| ~ ( member449909584od_a_a @ ( product_Pair_a_a @ SY72 @ SY73 ) @ ( partia206007992t_unit @ rel ) )
| ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ SY73 @ SV6 ) @ ( mult_a_ring_ext_a_b @ r @ SV17 @ SY72 ) ) @ ( mult_a_ring_ext_a_b @ r @ SV17 @ SY73 ) ) @ ( partia206007992t_unit @ rel ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[362]) ).
thf(374,plain,
! [SV7: product_prod_a_a] :
( ( ! [SY52: a] :
~ ~ ! [SY53: a] :
( SV7
!= ( product_Pair_a_a @ SY52 @ SY53 ) ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[363]) ).
thf(375,plain,
! [SV8: product_prod_a_a] :
( ( ! [SY54: a,SY55: a] :
( SV8
!= ( product_Pair_a_a @ SY54 @ SY55 ) ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[364]) ).
thf(376,plain,
! [SV18: product_prod_a_a,SV9: product_prod_a_a > $o] :
( ( ~ ! [SY57: a,SY58: a] : ( SV9 @ ( product_Pair_a_a @ SY57 @ SY58 ) )
| ( SV9 @ SV18 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[365]) ).
thf(377,plain,
! [SV19: product_prod_a_a,SV10: product_prod_a_a > $o] :
( ( ~ ! [SY60: a,SY61: a] : ( SV10 @ ( product_Pair_a_a @ SY60 @ SY61 ) )
| ( SV10 @ SV19 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[366]) ).
thf(378,plain,
! [SV20: a,SV11: a] :
( ( ! [SY78: a,SY79: a] :
( ( ( product_Pair_a_a @ SV11 @ SV20 )
= ( product_Pair_a_a @ SY78 @ SY79 ) )
= ( ~ ( ( SV11 != SY78 )
| ( SV20 != SY79 ) ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[367]) ).
thf(379,plain,
! [SV21: a,SV12: a] :
( ( ! [SY80: a,SY81: a] :
( ( ( product_Pair_a_a @ SV12 @ SV21 )
= ( product_Pair_a_a @ SY80 @ SY81 ) )
= ( ~ ( ( SV12 != SY80 )
| ( SV21 != SY81 ) ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[368]) ).
thf(380,plain,
! [SV13: product_prod_a_a > $o,SV1: product_prod_a_a] :
( ( ~ ( ( member449909584od_a_a @ SV1 @ ( collec645855634od_a_a @ SV13 ) )
| ( SV13 @ SV1 ) )
| ~ ( ~ ( member449909584od_a_a @ SV1 @ ( collec645855634od_a_a @ SV13 ) )
| ~ ( SV13 @ SV1 ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[369]) ).
thf(381,plain,
! [SV13: product_prod_a_a > $o,SV1: product_prod_a_a] :
( ( ( member449909584od_a_a @ SV1 @ ( collec645855634od_a_a @ SV13 ) )
= ( SV13 @ SV1 ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[369]) ).
thf(382,plain,
! [SV22: a,SV14: a,SV3: a] :
( ( ( SV3 != SV14 )
| ( ( a_minus_a_b @ r @ SV22 @ SV3 )
= ( a_minus_a_b @ r @ SV22 @ SV14 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[370]) ).
thf(383,plain,
! [SV23: a,SV15: a,SV4: a] :
( ( ( SV4 != SV15 )
| ( ( add_a_b @ r @ SV23 @ SV4 )
= ( add_a_b @ r @ SV23 @ SV15 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[371]) ).
thf(384,plain,
! [SV24: a,SV16: a,SV5: a] :
( ( ! [SY82: a] :
( ( ( product_Pair_a_a @ SV5 @ SV16 )
!= ( product_Pair_a_a @ SV24 @ SY82 ) )
| ~ ( ( SV5 != SV24 )
| ( SV16 != SY82 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[372]) ).
thf(385,plain,
! [SV25: a,SV17: a,SV6: a] :
( ( ! [SY83: a] :
( ~ ( member449909584od_a_a @ ( product_Pair_a_a @ SV6 @ SV17 ) @ ( partia206007992t_unit @ rel ) )
| ~ ( member449909584od_a_a @ ( product_Pair_a_a @ SV25 @ SY83 ) @ ( partia206007992t_unit @ rel ) )
| ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ SY83 @ SV6 ) @ ( mult_a_ring_ext_a_b @ r @ SV17 @ SV25 ) ) @ ( mult_a_ring_ext_a_b @ r @ SV17 @ SY83 ) ) @ ( partia206007992t_unit @ rel ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[373]) ).
thf(386,plain,
! [SV7: product_prod_a_a] :
( ( ~ ~ ! [SY84: a] :
( SV7
!= ( product_Pair_a_a @ ( sK1_SY52 @ SV7 ) @ SY84 ) ) )
= $false ),
inference(extcnf_forall_neg,[status(esa)],[374]) ).
thf(387,plain,
! [SV8: product_prod_a_a] :
( ( ! [SY85: a] :
( SV8
!= ( product_Pair_a_a @ ( sK2_SY54 @ SV8 ) @ SY85 ) ) )
= $false ),
inference(extcnf_forall_neg,[status(esa)],[375]) ).
thf(388,plain,
! [SV18: product_prod_a_a,SV9: product_prod_a_a > $o] :
( ( ( ~ ! [SY57: a,SY58: a] : ( SV9 @ ( product_Pair_a_a @ SY57 @ SY58 ) ) )
= $true )
| ( ( SV9 @ SV18 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[376]) ).
thf(389,plain,
! [SV19: product_prod_a_a,SV10: product_prod_a_a > $o] :
( ( ( ~ ! [SY60: a,SY61: a] : ( SV10 @ ( product_Pair_a_a @ SY60 @ SY61 ) ) )
= $true )
| ( ( SV10 @ SV19 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[377]) ).
thf(390,plain,
! [SV26: a,SV20: a,SV11: a] :
( ( ! [SY86: a] :
( ( ( product_Pair_a_a @ SV11 @ SV20 )
= ( product_Pair_a_a @ SV26 @ SY86 ) )
= ( ~ ( ( SV11 != SV26 )
| ( SV20 != SY86 ) ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[378]) ).
thf(391,plain,
! [SV27: a,SV21: a,SV12: a] :
( ( ! [SY87: a] :
( ( ( product_Pair_a_a @ SV12 @ SV21 )
= ( product_Pair_a_a @ SV27 @ SY87 ) )
= ( ~ ( ( SV12 != SV27 )
| ( SV21 != SY87 ) ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[379]) ).
thf(392,plain,
! [SV13: product_prod_a_a > $o,SV1: product_prod_a_a] :
( ( ( ~ ( ( member449909584od_a_a @ SV1 @ ( collec645855634od_a_a @ SV13 ) )
| ( SV13 @ SV1 ) ) )
= $true )
| ( ( ~ ( ~ ( member449909584od_a_a @ SV1 @ ( collec645855634od_a_a @ SV13 ) )
| ~ ( SV13 @ SV1 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[380]) ).
thf(393,plain,
! [SV22: a,SV14: a,SV3: a] :
( ( ( SV3 != SV14 )
= $true )
| ( ( ( a_minus_a_b @ r @ SV22 @ SV3 )
= ( a_minus_a_b @ r @ SV22 @ SV14 ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[382]) ).
thf(394,plain,
! [SV23: a,SV15: a,SV4: a] :
( ( ( SV4 != SV15 )
= $true )
| ( ( ( add_a_b @ r @ SV23 @ SV4 )
= ( add_a_b @ r @ SV23 @ SV15 ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[383]) ).
thf(395,plain,
! [SV28: a,SV24: a,SV16: a,SV5: a] :
( ( ( ( product_Pair_a_a @ SV5 @ SV16 )
!= ( product_Pair_a_a @ SV24 @ SV28 ) )
| ~ ( ( SV5 != SV24 )
| ( SV16 != SV28 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[384]) ).
thf(396,plain,
! [SV29: a,SV25: a,SV17: a,SV6: a] :
( ( ~ ( member449909584od_a_a @ ( product_Pair_a_a @ SV6 @ SV17 ) @ ( partia206007992t_unit @ rel ) )
| ~ ( member449909584od_a_a @ ( product_Pair_a_a @ SV25 @ SV29 ) @ ( partia206007992t_unit @ rel ) )
| ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ SV29 @ SV6 ) @ ( mult_a_ring_ext_a_b @ r @ SV17 @ SV25 ) ) @ ( mult_a_ring_ext_a_b @ r @ SV17 @ SV29 ) ) @ ( partia206007992t_unit @ rel ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[385]) ).
thf(397,plain,
! [SV7: product_prod_a_a] :
( ( ~ ! [SY84: a] :
( SV7
!= ( product_Pair_a_a @ ( sK1_SY52 @ SV7 ) @ SY84 ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[386]) ).
thf(398,plain,
! [SV8: product_prod_a_a] :
( ( SV8
!= ( product_Pair_a_a @ ( sK2_SY54 @ SV8 ) @ ( sK3_SY85 @ SV8 ) ) )
= $false ),
inference(extcnf_forall_neg,[status(esa)],[387]) ).
thf(399,plain,
! [SV18: product_prod_a_a,SV9: product_prod_a_a > $o] :
( ( ( ! [SY57: a,SY58: a] : ( SV9 @ ( product_Pair_a_a @ SY57 @ SY58 ) ) )
= $false )
| ( ( SV9 @ SV18 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[388]) ).
thf(400,plain,
! [SV19: product_prod_a_a,SV10: product_prod_a_a > $o] :
( ( ( ! [SY60: a,SY61: a] : ( SV10 @ ( product_Pair_a_a @ SY60 @ SY61 ) ) )
= $false )
| ( ( SV10 @ SV19 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[389]) ).
thf(401,plain,
! [SV30: a,SV26: a,SV20: a,SV11: a] :
( ( ( ( product_Pair_a_a @ SV11 @ SV20 )
= ( product_Pair_a_a @ SV26 @ SV30 ) )
= ( ~ ( ( SV11 != SV26 )
| ( SV20 != SV30 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[390]) ).
thf(402,plain,
! [SV31: a,SV27: a,SV21: a,SV12: a] :
( ( ( ( product_Pair_a_a @ SV12 @ SV21 )
= ( product_Pair_a_a @ SV27 @ SV31 ) )
= ( ~ ( ( SV12 != SV27 )
| ( SV21 != SV31 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[391]) ).
thf(403,plain,
! [SV13: product_prod_a_a > $o,SV1: product_prod_a_a] :
( ( ( ( member449909584od_a_a @ SV1 @ ( collec645855634od_a_a @ SV13 ) )
| ( SV13 @ SV1 ) )
= $false )
| ( ( ~ ( ~ ( member449909584od_a_a @ SV1 @ ( collec645855634od_a_a @ SV13 ) )
| ~ ( SV13 @ SV1 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[392]) ).
thf(404,plain,
! [SV22: a,SV14: a,SV3: a] :
( ( ( SV3 = SV14 )
= $false )
| ( ( ( a_minus_a_b @ r @ SV22 @ SV3 )
= ( a_minus_a_b @ r @ SV22 @ SV14 ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[393]) ).
thf(405,plain,
! [SV23: a,SV15: a,SV4: a] :
( ( ( SV4 = SV15 )
= $false )
| ( ( ( add_a_b @ r @ SV23 @ SV4 )
= ( add_a_b @ r @ SV23 @ SV15 ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[394]) ).
thf(406,plain,
! [SV28: a,SV24: a,SV16: a,SV5: a] :
( ( ( ( product_Pair_a_a @ SV5 @ SV16 )
!= ( product_Pair_a_a @ SV24 @ SV28 ) )
= $true )
| ( ( ~ ( ( SV5 != SV24 )
| ( SV16 != SV28 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[395]) ).
thf(407,plain,
! [SV29: a,SV25: a,SV17: a,SV6: a] :
( ( ( ~ ( member449909584od_a_a @ ( product_Pair_a_a @ SV6 @ SV17 ) @ ( partia206007992t_unit @ rel ) ) )
= $true )
| ( ( ~ ( member449909584od_a_a @ ( product_Pair_a_a @ SV25 @ SV29 ) @ ( partia206007992t_unit @ rel ) )
| ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ SV29 @ SV6 ) @ ( mult_a_ring_ext_a_b @ r @ SV17 @ SV25 ) ) @ ( mult_a_ring_ext_a_b @ r @ SV17 @ SV29 ) ) @ ( partia206007992t_unit @ rel ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[396]) ).
thf(408,plain,
! [SV7: product_prod_a_a] :
( ( ! [SY84: a] :
( SV7
!= ( product_Pair_a_a @ ( sK1_SY52 @ SV7 ) @ SY84 ) ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[397]) ).
thf(409,plain,
! [SV8: product_prod_a_a] :
( ( SV8
= ( product_Pair_a_a @ ( sK2_SY54 @ SV8 ) @ ( sK3_SY85 @ SV8 ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[398]) ).
thf(410,plain,
! [SV18: product_prod_a_a,SV9: product_prod_a_a > $o] :
( ( ( ! [SY88: a] : ( SV9 @ ( product_Pair_a_a @ ( sK4_SY57 @ SV18 @ SV9 ) @ SY88 ) ) )
= $false )
| ( ( SV9 @ SV18 )
= $true ) ),
inference(extcnf_forall_neg,[status(esa)],[399]) ).
thf(411,plain,
! [SV19: product_prod_a_a,SV10: product_prod_a_a > $o] :
( ( ( ! [SY89: a] : ( SV10 @ ( product_Pair_a_a @ ( sK5_SY60 @ SV19 @ SV10 ) @ SY89 ) ) )
= $false )
| ( ( SV10 @ SV19 )
= $true ) ),
inference(extcnf_forall_neg,[status(esa)],[400]) ).
thf(412,plain,
! [SV30: a,SV26: a,SV20: a,SV11: a] :
( ( ~ ( ( ( product_Pair_a_a @ SV11 @ SV20 )
= ( product_Pair_a_a @ SV26 @ SV30 ) )
| ~ ( ( SV11 != SV26 )
| ( SV20 != SV30 ) ) )
| ~ ( ( ( product_Pair_a_a @ SV11 @ SV20 )
!= ( product_Pair_a_a @ SV26 @ SV30 ) )
| ~ ~ ( ( SV11 != SV26 )
| ( SV20 != SV30 ) ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[401]) ).
thf(413,plain,
! [SV30: a,SV26: a,SV20: a,SV11: a] :
( ( ( ( product_Pair_a_a @ SV11 @ SV20 )
= ( product_Pair_a_a @ SV26 @ SV30 ) )
= ( ~ ( ( SV11 != SV26 )
| ( SV20 != SV30 ) ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[401]) ).
thf(414,plain,
! [SV31: a,SV27: a,SV21: a,SV12: a] :
( ( ~ ( ( ( product_Pair_a_a @ SV12 @ SV21 )
= ( product_Pair_a_a @ SV27 @ SV31 ) )
| ~ ( ( SV12 != SV27 )
| ( SV21 != SV31 ) ) )
| ~ ( ( ( product_Pair_a_a @ SV12 @ SV21 )
!= ( product_Pair_a_a @ SV27 @ SV31 ) )
| ~ ~ ( ( SV12 != SV27 )
| ( SV21 != SV31 ) ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[402]) ).
thf(415,plain,
! [SV31: a,SV27: a,SV21: a,SV12: a] :
( ( ( ( product_Pair_a_a @ SV12 @ SV21 )
= ( product_Pair_a_a @ SV27 @ SV31 ) )
= ( ~ ( ( SV12 != SV27 )
| ( SV21 != SV31 ) ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[402]) ).
thf(416,plain,
! [SV13: product_prod_a_a > $o,SV1: product_prod_a_a] :
( ( ( member449909584od_a_a @ SV1 @ ( collec645855634od_a_a @ SV13 ) )
= $false )
| ( ( ~ ( ~ ( member449909584od_a_a @ SV1 @ ( collec645855634od_a_a @ SV13 ) )
| ~ ( SV13 @ SV1 ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[403]) ).
thf(417,plain,
! [SV1: product_prod_a_a,SV13: product_prod_a_a > $o] :
( ( ( SV13 @ SV1 )
= $false )
| ( ( ~ ( ~ ( member449909584od_a_a @ SV1 @ ( collec645855634od_a_a @ SV13 ) )
| ~ ( SV13 @ SV1 ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[403]) ).
thf(418,plain,
! [SV28: a,SV24: a,SV16: a,SV5: a] :
( ( ( ( product_Pair_a_a @ SV5 @ SV16 )
= ( product_Pair_a_a @ SV24 @ SV28 ) )
= $false )
| ( ( ~ ( ( SV5 != SV24 )
| ( SV16 != SV28 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[406]) ).
thf(419,plain,
! [SV29: a,SV25: a,SV17: a,SV6: a] :
( ( ( member449909584od_a_a @ ( product_Pair_a_a @ SV6 @ SV17 ) @ ( partia206007992t_unit @ rel ) )
= $false )
| ( ( ~ ( member449909584od_a_a @ ( product_Pair_a_a @ SV25 @ SV29 ) @ ( partia206007992t_unit @ rel ) )
| ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ SV29 @ SV6 ) @ ( mult_a_ring_ext_a_b @ r @ SV17 @ SV25 ) ) @ ( mult_a_ring_ext_a_b @ r @ SV17 @ SV29 ) ) @ ( partia206007992t_unit @ rel ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[407]) ).
thf(420,plain,
! [SV7: product_prod_a_a] :
( ( SV7
!= ( product_Pair_a_a @ ( sK1_SY52 @ SV7 ) @ ( sK6_SY84 @ SV7 ) ) )
= $false ),
inference(extcnf_forall_neg,[status(esa)],[408]) ).
thf(421,plain,
! [SV18: product_prod_a_a,SV9: product_prod_a_a > $o] :
( ( ( SV9 @ ( product_Pair_a_a @ ( sK4_SY57 @ SV18 @ SV9 ) @ ( sK7_SY88 @ SV18 @ SV9 ) ) )
= $false )
| ( ( SV9 @ SV18 )
= $true ) ),
inference(extcnf_forall_neg,[status(esa)],[410]) ).
thf(422,plain,
! [SV19: product_prod_a_a,SV10: product_prod_a_a > $o] :
( ( ( SV10 @ ( product_Pair_a_a @ ( sK5_SY60 @ SV19 @ SV10 ) @ ( sK8_SY89 @ SV19 @ SV10 ) ) )
= $false )
| ( ( SV10 @ SV19 )
= $true ) ),
inference(extcnf_forall_neg,[status(esa)],[411]) ).
thf(423,plain,
! [SV30: a,SV26: a,SV20: a,SV11: a] :
( ( ( ~ ( ( ( product_Pair_a_a @ SV11 @ SV20 )
= ( product_Pair_a_a @ SV26 @ SV30 ) )
| ~ ( ( SV11 != SV26 )
| ( SV20 != SV30 ) ) ) )
= $true )
| ( ( ~ ( ( ( product_Pair_a_a @ SV11 @ SV20 )
!= ( product_Pair_a_a @ SV26 @ SV30 ) )
| ~ ~ ( ( SV11 != SV26 )
| ( SV20 != SV30 ) ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[412]) ).
thf(424,plain,
! [SV31: a,SV27: a,SV21: a,SV12: a] :
( ( ( ~ ( ( ( product_Pair_a_a @ SV12 @ SV21 )
= ( product_Pair_a_a @ SV27 @ SV31 ) )
| ~ ( ( SV12 != SV27 )
| ( SV21 != SV31 ) ) ) )
= $true )
| ( ( ~ ( ( ( product_Pair_a_a @ SV12 @ SV21 )
!= ( product_Pair_a_a @ SV27 @ SV31 ) )
| ~ ~ ( ( SV12 != SV27 )
| ( SV21 != SV31 ) ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[414]) ).
thf(425,plain,
! [SV13: product_prod_a_a > $o,SV1: product_prod_a_a] :
( ( ( ~ ( member449909584od_a_a @ SV1 @ ( collec645855634od_a_a @ SV13 ) )
| ~ ( SV13 @ SV1 ) )
= $false )
| ( ( member449909584od_a_a @ SV1 @ ( collec645855634od_a_a @ SV13 ) )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[416]) ).
thf(426,plain,
! [SV13: product_prod_a_a > $o,SV1: product_prod_a_a] :
( ( ( ~ ( member449909584od_a_a @ SV1 @ ( collec645855634od_a_a @ SV13 ) )
| ~ ( SV13 @ SV1 ) )
= $false )
| ( ( SV13 @ SV1 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[417]) ).
thf(427,plain,
! [SV28: a,SV16: a,SV24: a,SV5: a] :
( ( ( ( SV5 != SV24 )
| ( SV16 != SV28 ) )
= $false )
| ( ( ( product_Pair_a_a @ SV5 @ SV16 )
= ( product_Pair_a_a @ SV24 @ SV28 ) )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[418]) ).
thf(428,plain,
! [SV17: a,SV6: a,SV29: a,SV25: a] :
( ( ( ~ ( member449909584od_a_a @ ( product_Pair_a_a @ SV25 @ SV29 ) @ ( partia206007992t_unit @ rel ) ) )
= $true )
| ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ SV29 @ SV6 ) @ ( mult_a_ring_ext_a_b @ r @ SV17 @ SV25 ) ) @ ( mult_a_ring_ext_a_b @ r @ SV17 @ SV29 ) ) @ ( partia206007992t_unit @ rel ) )
= $true )
| ( ( member449909584od_a_a @ ( product_Pair_a_a @ SV6 @ SV17 ) @ ( partia206007992t_unit @ rel ) )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[419]) ).
thf(429,plain,
! [SV7: product_prod_a_a] :
( ( SV7
= ( product_Pair_a_a @ ( sK1_SY52 @ SV7 ) @ ( sK6_SY84 @ SV7 ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[420]) ).
thf(430,plain,
! [SV30: a,SV26: a,SV20: a,SV11: a] :
( ( ( ( ( product_Pair_a_a @ SV11 @ SV20 )
= ( product_Pair_a_a @ SV26 @ SV30 ) )
| ~ ( ( SV11 != SV26 )
| ( SV20 != SV30 ) ) )
= $false )
| ( ( ~ ( ( ( product_Pair_a_a @ SV11 @ SV20 )
!= ( product_Pair_a_a @ SV26 @ SV30 ) )
| ~ ~ ( ( SV11 != SV26 )
| ( SV20 != SV30 ) ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[423]) ).
thf(431,plain,
! [SV31: a,SV27: a,SV21: a,SV12: a] :
( ( ( ( ( product_Pair_a_a @ SV12 @ SV21 )
= ( product_Pair_a_a @ SV27 @ SV31 ) )
| ~ ( ( SV12 != SV27 )
| ( SV21 != SV31 ) ) )
= $false )
| ( ( ~ ( ( ( product_Pair_a_a @ SV12 @ SV21 )
!= ( product_Pair_a_a @ SV27 @ SV31 ) )
| ~ ~ ( ( SV12 != SV27 )
| ( SV21 != SV31 ) ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[424]) ).
thf(432,plain,
! [SV13: product_prod_a_a > $o,SV1: product_prod_a_a] :
( ( ( ~ ( member449909584od_a_a @ SV1 @ ( collec645855634od_a_a @ SV13 ) ) )
= $false )
| ( ( member449909584od_a_a @ SV1 @ ( collec645855634od_a_a @ SV13 ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[425]) ).
thf(433,plain,
! [SV1: product_prod_a_a,SV13: product_prod_a_a > $o] :
( ( ( ~ ( SV13 @ SV1 ) )
= $false )
| ( ( member449909584od_a_a @ SV1 @ ( collec645855634od_a_a @ SV13 ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[425]) ).
thf(434,plain,
! [SV13: product_prod_a_a > $o,SV1: product_prod_a_a] :
( ( ( ~ ( member449909584od_a_a @ SV1 @ ( collec645855634od_a_a @ SV13 ) ) )
= $false )
| ( ( SV13 @ SV1 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[426]) ).
thf(435,plain,
! [SV1: product_prod_a_a,SV13: product_prod_a_a > $o] :
( ( ( ~ ( SV13 @ SV1 ) )
= $false )
| ( ( SV13 @ SV1 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[426]) ).
thf(436,plain,
! [SV28: a,SV16: a,SV24: a,SV5: a] :
( ( ( SV5 != SV24 )
= $false )
| ( ( ( product_Pair_a_a @ SV5 @ SV16 )
= ( product_Pair_a_a @ SV24 @ SV28 ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[427]) ).
thf(437,plain,
! [SV24: a,SV5: a,SV28: a,SV16: a] :
( ( ( SV16 != SV28 )
= $false )
| ( ( ( product_Pair_a_a @ SV5 @ SV16 )
= ( product_Pair_a_a @ SV24 @ SV28 ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[427]) ).
thf(438,plain,
! [SV17: a,SV6: a,SV29: a,SV25: a] :
( ( ( member449909584od_a_a @ ( product_Pair_a_a @ SV25 @ SV29 ) @ ( partia206007992t_unit @ rel ) )
= $false )
| ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ SV29 @ SV6 ) @ ( mult_a_ring_ext_a_b @ r @ SV17 @ SV25 ) ) @ ( mult_a_ring_ext_a_b @ r @ SV17 @ SV29 ) ) @ ( partia206007992t_unit @ rel ) )
= $true )
| ( ( member449909584od_a_a @ ( product_Pair_a_a @ SV6 @ SV17 ) @ ( partia206007992t_unit @ rel ) )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[428]) ).
thf(439,plain,
! [SV30: a,SV26: a,SV20: a,SV11: a] :
( ( ( ( product_Pair_a_a @ SV11 @ SV20 )
= ( product_Pair_a_a @ SV26 @ SV30 ) )
= $false )
| ( ( ~ ( ( ( product_Pair_a_a @ SV11 @ SV20 )
!= ( product_Pair_a_a @ SV26 @ SV30 ) )
| ~ ~ ( ( SV11 != SV26 )
| ( SV20 != SV30 ) ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[430]) ).
thf(440,plain,
! [SV30: a,SV20: a,SV26: a,SV11: a] :
( ( ( ~ ( ( SV11 != SV26 )
| ( SV20 != SV30 ) ) )
= $false )
| ( ( ~ ( ( ( product_Pair_a_a @ SV11 @ SV20 )
!= ( product_Pair_a_a @ SV26 @ SV30 ) )
| ~ ~ ( ( SV11 != SV26 )
| ( SV20 != SV30 ) ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[430]) ).
thf(441,plain,
! [SV31: a,SV27: a,SV21: a,SV12: a] :
( ( ( ( product_Pair_a_a @ SV12 @ SV21 )
= ( product_Pair_a_a @ SV27 @ SV31 ) )
= $false )
| ( ( ~ ( ( ( product_Pair_a_a @ SV12 @ SV21 )
!= ( product_Pair_a_a @ SV27 @ SV31 ) )
| ~ ~ ( ( SV12 != SV27 )
| ( SV21 != SV31 ) ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[431]) ).
thf(442,plain,
! [SV31: a,SV21: a,SV27: a,SV12: a] :
( ( ( ~ ( ( SV12 != SV27 )
| ( SV21 != SV31 ) ) )
= $false )
| ( ( ~ ( ( ( product_Pair_a_a @ SV12 @ SV21 )
!= ( product_Pair_a_a @ SV27 @ SV31 ) )
| ~ ~ ( ( SV12 != SV27 )
| ( SV21 != SV31 ) ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[431]) ).
thf(443,plain,
! [SV13: product_prod_a_a > $o,SV1: product_prod_a_a] :
( ( ( member449909584od_a_a @ SV1 @ ( collec645855634od_a_a @ SV13 ) )
= $true )
| ( ( member449909584od_a_a @ SV1 @ ( collec645855634od_a_a @ SV13 ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[432]) ).
thf(444,plain,
! [SV1: product_prod_a_a,SV13: product_prod_a_a > $o] :
( ( ( SV13 @ SV1 )
= $true )
| ( ( member449909584od_a_a @ SV1 @ ( collec645855634od_a_a @ SV13 ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[433]) ).
thf(445,plain,
! [SV13: product_prod_a_a > $o,SV1: product_prod_a_a] :
( ( ( member449909584od_a_a @ SV1 @ ( collec645855634od_a_a @ SV13 ) )
= $true )
| ( ( SV13 @ SV1 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[434]) ).
thf(446,plain,
! [SV1: product_prod_a_a,SV13: product_prod_a_a > $o] :
( ( ( SV13 @ SV1 )
= $true )
| ( ( SV13 @ SV1 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[435]) ).
thf(447,plain,
! [SV28: a,SV16: a,SV24: a,SV5: a] :
( ( ( SV5 = SV24 )
= $true )
| ( ( ( product_Pair_a_a @ SV5 @ SV16 )
= ( product_Pair_a_a @ SV24 @ SV28 ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[436]) ).
thf(448,plain,
! [SV24: a,SV5: a,SV28: a,SV16: a] :
( ( ( SV16 = SV28 )
= $true )
| ( ( ( product_Pair_a_a @ SV5 @ SV16 )
= ( product_Pair_a_a @ SV24 @ SV28 ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[437]) ).
thf(449,plain,
! [SV30: a,SV26: a,SV20: a,SV11: a] :
( ( ( ( ( product_Pair_a_a @ SV11 @ SV20 )
!= ( product_Pair_a_a @ SV26 @ SV30 ) )
| ~ ~ ( ( SV11 != SV26 )
| ( SV20 != SV30 ) ) )
= $false )
| ( ( ( product_Pair_a_a @ SV11 @ SV20 )
= ( product_Pair_a_a @ SV26 @ SV30 ) )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[439]) ).
thf(450,plain,
! [SV30: a,SV20: a,SV26: a,SV11: a] :
( ( ( ( SV11 != SV26 )
| ( SV20 != SV30 ) )
= $true )
| ( ( ~ ( ( ( product_Pair_a_a @ SV11 @ SV20 )
!= ( product_Pair_a_a @ SV26 @ SV30 ) )
| ~ ~ ( ( SV11 != SV26 )
| ( SV20 != SV30 ) ) ) )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[440]) ).
thf(451,plain,
! [SV31: a,SV27: a,SV21: a,SV12: a] :
( ( ( ( ( product_Pair_a_a @ SV12 @ SV21 )
!= ( product_Pair_a_a @ SV27 @ SV31 ) )
| ~ ~ ( ( SV12 != SV27 )
| ( SV21 != SV31 ) ) )
= $false )
| ( ( ( product_Pair_a_a @ SV12 @ SV21 )
= ( product_Pair_a_a @ SV27 @ SV31 ) )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[441]) ).
thf(452,plain,
! [SV31: a,SV21: a,SV27: a,SV12: a] :
( ( ( ( SV12 != SV27 )
| ( SV21 != SV31 ) )
= $true )
| ( ( ~ ( ( ( product_Pair_a_a @ SV12 @ SV21 )
!= ( product_Pair_a_a @ SV27 @ SV31 ) )
| ~ ~ ( ( SV12 != SV27 )
| ( SV21 != SV31 ) ) ) )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[442]) ).
thf(453,plain,
! [SV30: a,SV26: a,SV20: a,SV11: a] :
( ( ( ( product_Pair_a_a @ SV11 @ SV20 )
!= ( product_Pair_a_a @ SV26 @ SV30 ) )
= $false )
| ( ( ( product_Pair_a_a @ SV11 @ SV20 )
= ( product_Pair_a_a @ SV26 @ SV30 ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[449]) ).
thf(454,plain,
! [SV30: a,SV20: a,SV26: a,SV11: a] :
( ( ( ~ ~ ( ( SV11 != SV26 )
| ( SV20 != SV30 ) ) )
= $false )
| ( ( ( product_Pair_a_a @ SV11 @ SV20 )
= ( product_Pair_a_a @ SV26 @ SV30 ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[449]) ).
thf(455,plain,
! [SV30: a,SV20: a,SV26: a,SV11: a] :
( ( ( SV11 != SV26 )
= $true )
| ( ( SV20 != SV30 )
= $true )
| ( ( ~ ( ( ( product_Pair_a_a @ SV11 @ SV20 )
!= ( product_Pair_a_a @ SV26 @ SV30 ) )
| ~ ~ ( ( SV11 != SV26 )
| ( SV20 != SV30 ) ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[450]) ).
thf(456,plain,
! [SV31: a,SV27: a,SV21: a,SV12: a] :
( ( ( ( product_Pair_a_a @ SV12 @ SV21 )
!= ( product_Pair_a_a @ SV27 @ SV31 ) )
= $false )
| ( ( ( product_Pair_a_a @ SV12 @ SV21 )
= ( product_Pair_a_a @ SV27 @ SV31 ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[451]) ).
thf(457,plain,
! [SV31: a,SV21: a,SV27: a,SV12: a] :
( ( ( ~ ~ ( ( SV12 != SV27 )
| ( SV21 != SV31 ) ) )
= $false )
| ( ( ( product_Pair_a_a @ SV12 @ SV21 )
= ( product_Pair_a_a @ SV27 @ SV31 ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[451]) ).
thf(458,plain,
! [SV31: a,SV21: a,SV27: a,SV12: a] :
( ( ( SV12 != SV27 )
= $true )
| ( ( SV21 != SV31 )
= $true )
| ( ( ~ ( ( ( product_Pair_a_a @ SV12 @ SV21 )
!= ( product_Pair_a_a @ SV27 @ SV31 ) )
| ~ ~ ( ( SV12 != SV27 )
| ( SV21 != SV31 ) ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[452]) ).
thf(459,plain,
! [SV30: a,SV26: a,SV20: a,SV11: a] :
( ( ( ( product_Pair_a_a @ SV11 @ SV20 )
= ( product_Pair_a_a @ SV26 @ SV30 ) )
= $true )
| ( ( ( product_Pair_a_a @ SV11 @ SV20 )
= ( product_Pair_a_a @ SV26 @ SV30 ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[453]) ).
thf(460,plain,
! [SV30: a,SV20: a,SV26: a,SV11: a] :
( ( ( ~ ( ( SV11 != SV26 )
| ( SV20 != SV30 ) ) )
= $true )
| ( ( ( product_Pair_a_a @ SV11 @ SV20 )
= ( product_Pair_a_a @ SV26 @ SV30 ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[454]) ).
thf(461,plain,
! [SV30: a,SV20: a,SV26: a,SV11: a] :
( ( ( SV11 = SV26 )
= $false )
| ( ( SV20 != SV30 )
= $true )
| ( ( ~ ( ( ( product_Pair_a_a @ SV11 @ SV20 )
!= ( product_Pair_a_a @ SV26 @ SV30 ) )
| ~ ~ ( ( SV11 != SV26 )
| ( SV20 != SV30 ) ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[455]) ).
thf(462,plain,
! [SV31: a,SV27: a,SV21: a,SV12: a] :
( ( ( ( product_Pair_a_a @ SV12 @ SV21 )
= ( product_Pair_a_a @ SV27 @ SV31 ) )
= $true )
| ( ( ( product_Pair_a_a @ SV12 @ SV21 )
= ( product_Pair_a_a @ SV27 @ SV31 ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[456]) ).
thf(463,plain,
! [SV31: a,SV21: a,SV27: a,SV12: a] :
( ( ( ~ ( ( SV12 != SV27 )
| ( SV21 != SV31 ) ) )
= $true )
| ( ( ( product_Pair_a_a @ SV12 @ SV21 )
= ( product_Pair_a_a @ SV27 @ SV31 ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[457]) ).
thf(464,plain,
! [SV31: a,SV21: a,SV27: a,SV12: a] :
( ( ( SV12 = SV27 )
= $false )
| ( ( SV21 != SV31 )
= $true )
| ( ( ~ ( ( ( product_Pair_a_a @ SV12 @ SV21 )
!= ( product_Pair_a_a @ SV27 @ SV31 ) )
| ~ ~ ( ( SV12 != SV27 )
| ( SV21 != SV31 ) ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[458]) ).
thf(465,plain,
! [SV30: a,SV20: a,SV26: a,SV11: a] :
( ( ( ( SV11 != SV26 )
| ( SV20 != SV30 ) )
= $false )
| ( ( ( product_Pair_a_a @ SV11 @ SV20 )
= ( product_Pair_a_a @ SV26 @ SV30 ) )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[460]) ).
thf(466,plain,
! [SV26: a,SV11: a,SV30: a,SV20: a] :
( ( ( SV20 = SV30 )
= $false )
| ( ( SV11 = SV26 )
= $false )
| ( ( ~ ( ( ( product_Pair_a_a @ SV11 @ SV20 )
!= ( product_Pair_a_a @ SV26 @ SV30 ) )
| ~ ~ ( ( SV11 != SV26 )
| ( SV20 != SV30 ) ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[461]) ).
thf(467,plain,
! [SV31: a,SV21: a,SV27: a,SV12: a] :
( ( ( ( SV12 != SV27 )
| ( SV21 != SV31 ) )
= $false )
| ( ( ( product_Pair_a_a @ SV12 @ SV21 )
= ( product_Pair_a_a @ SV27 @ SV31 ) )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[463]) ).
thf(468,plain,
! [SV27: a,SV12: a,SV31: a,SV21: a] :
( ( ( SV21 = SV31 )
= $false )
| ( ( SV12 = SV27 )
= $false )
| ( ( ~ ( ( ( product_Pair_a_a @ SV12 @ SV21 )
!= ( product_Pair_a_a @ SV27 @ SV31 ) )
| ~ ~ ( ( SV12 != SV27 )
| ( SV21 != SV31 ) ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[464]) ).
thf(469,plain,
! [SV30: a,SV20: a,SV26: a,SV11: a] :
( ( ( SV11 != SV26 )
= $false )
| ( ( ( product_Pair_a_a @ SV11 @ SV20 )
= ( product_Pair_a_a @ SV26 @ SV30 ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[465]) ).
thf(470,plain,
! [SV26: a,SV11: a,SV30: a,SV20: a] :
( ( ( SV20 != SV30 )
= $false )
| ( ( ( product_Pair_a_a @ SV11 @ SV20 )
= ( product_Pair_a_a @ SV26 @ SV30 ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[465]) ).
thf(471,plain,
! [SV30: a,SV26: a,SV20: a,SV11: a] :
( ( ( ( ( product_Pair_a_a @ SV11 @ SV20 )
!= ( product_Pair_a_a @ SV26 @ SV30 ) )
| ~ ~ ( ( SV11 != SV26 )
| ( SV20 != SV30 ) ) )
= $false )
| ( ( SV11 = SV26 )
= $false )
| ( ( SV20 = SV30 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[466]) ).
thf(472,plain,
! [SV31: a,SV21: a,SV27: a,SV12: a] :
( ( ( SV12 != SV27 )
= $false )
| ( ( ( product_Pair_a_a @ SV12 @ SV21 )
= ( product_Pair_a_a @ SV27 @ SV31 ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[467]) ).
thf(473,plain,
! [SV27: a,SV12: a,SV31: a,SV21: a] :
( ( ( SV21 != SV31 )
= $false )
| ( ( ( product_Pair_a_a @ SV12 @ SV21 )
= ( product_Pair_a_a @ SV27 @ SV31 ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[467]) ).
thf(474,plain,
! [SV31: a,SV27: a,SV21: a,SV12: a] :
( ( ( ( ( product_Pair_a_a @ SV12 @ SV21 )
!= ( product_Pair_a_a @ SV27 @ SV31 ) )
| ~ ~ ( ( SV12 != SV27 )
| ( SV21 != SV31 ) ) )
= $false )
| ( ( SV12 = SV27 )
= $false )
| ( ( SV21 = SV31 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[468]) ).
thf(475,plain,
! [SV30: a,SV20: a,SV26: a,SV11: a] :
( ( ( SV11 = SV26 )
= $true )
| ( ( ( product_Pair_a_a @ SV11 @ SV20 )
= ( product_Pair_a_a @ SV26 @ SV30 ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[469]) ).
thf(476,plain,
! [SV26: a,SV11: a,SV30: a,SV20: a] :
( ( ( SV20 = SV30 )
= $true )
| ( ( ( product_Pair_a_a @ SV11 @ SV20 )
= ( product_Pair_a_a @ SV26 @ SV30 ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[470]) ).
thf(477,plain,
! [SV30: a,SV26: a,SV20: a,SV11: a] :
( ( ( ( product_Pair_a_a @ SV11 @ SV20 )
!= ( product_Pair_a_a @ SV26 @ SV30 ) )
= $false )
| ( ( SV11 = SV26 )
= $false )
| ( ( SV20 = SV30 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[471]) ).
thf(478,plain,
! [SV30: a,SV20: a,SV26: a,SV11: a] :
( ( ( ~ ~ ( ( SV11 != SV26 )
| ( SV20 != SV30 ) ) )
= $false )
| ( ( SV11 = SV26 )
= $false )
| ( ( SV20 = SV30 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[471]) ).
thf(479,plain,
! [SV31: a,SV21: a,SV27: a,SV12: a] :
( ( ( SV12 = SV27 )
= $true )
| ( ( ( product_Pair_a_a @ SV12 @ SV21 )
= ( product_Pair_a_a @ SV27 @ SV31 ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[472]) ).
thf(480,plain,
! [SV27: a,SV12: a,SV31: a,SV21: a] :
( ( ( SV21 = SV31 )
= $true )
| ( ( ( product_Pair_a_a @ SV12 @ SV21 )
= ( product_Pair_a_a @ SV27 @ SV31 ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[473]) ).
thf(481,plain,
! [SV31: a,SV27: a,SV21: a,SV12: a] :
( ( ( ( product_Pair_a_a @ SV12 @ SV21 )
!= ( product_Pair_a_a @ SV27 @ SV31 ) )
= $false )
| ( ( SV12 = SV27 )
= $false )
| ( ( SV21 = SV31 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[474]) ).
thf(482,plain,
! [SV31: a,SV21: a,SV27: a,SV12: a] :
( ( ( ~ ~ ( ( SV12 != SV27 )
| ( SV21 != SV31 ) ) )
= $false )
| ( ( SV12 = SV27 )
= $false )
| ( ( SV21 = SV31 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[474]) ).
thf(483,plain,
! [SV30: a,SV26: a,SV20: a,SV11: a] :
( ( ( ( product_Pair_a_a @ SV11 @ SV20 )
= ( product_Pair_a_a @ SV26 @ SV30 ) )
= $true )
| ( ( SV11 = SV26 )
= $false )
| ( ( SV20 = SV30 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[477]) ).
thf(484,plain,
! [SV30: a,SV20: a,SV26: a,SV11: a] :
( ( ( ~ ( ( SV11 != SV26 )
| ( SV20 != SV30 ) ) )
= $true )
| ( ( SV11 = SV26 )
= $false )
| ( ( SV20 = SV30 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[478]) ).
thf(485,plain,
! [SV31: a,SV27: a,SV21: a,SV12: a] :
( ( ( ( product_Pair_a_a @ SV12 @ SV21 )
= ( product_Pair_a_a @ SV27 @ SV31 ) )
= $true )
| ( ( SV12 = SV27 )
= $false )
| ( ( SV21 = SV31 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[481]) ).
thf(486,plain,
! [SV31: a,SV21: a,SV27: a,SV12: a] :
( ( ( ~ ( ( SV12 != SV27 )
| ( SV21 != SV31 ) ) )
= $true )
| ( ( SV12 = SV27 )
= $false )
| ( ( SV21 = SV31 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[482]) ).
thf(487,plain,
! [SV30: a,SV20: a,SV26: a,SV11: a] :
( ( ( ( SV11 != SV26 )
| ( SV20 != SV30 ) )
= $false )
| ( ( SV11 = SV26 )
= $false )
| ( ( SV20 = SV30 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[484]) ).
thf(488,plain,
! [SV31: a,SV21: a,SV27: a,SV12: a] :
( ( ( ( SV12 != SV27 )
| ( SV21 != SV31 ) )
= $false )
| ( ( SV12 = SV27 )
= $false )
| ( ( SV21 = SV31 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[486]) ).
thf(489,plain,
! [SV30: a,SV20: a,SV26: a,SV11: a] :
( ( ( SV11 != SV26 )
= $false )
| ( ( SV11 = SV26 )
= $false )
| ( ( SV20 = SV30 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[487]) ).
thf(490,plain,
! [SV26: a,SV11: a,SV30: a,SV20: a] :
( ( ( SV20 != SV30 )
= $false )
| ( ( SV11 = SV26 )
= $false )
| ( ( SV20 = SV30 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[487]) ).
thf(491,plain,
! [SV31: a,SV21: a,SV27: a,SV12: a] :
( ( ( SV12 != SV27 )
= $false )
| ( ( SV12 = SV27 )
= $false )
| ( ( SV21 = SV31 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[488]) ).
thf(492,plain,
! [SV27: a,SV12: a,SV31: a,SV21: a] :
( ( ( SV21 != SV31 )
= $false )
| ( ( SV12 = SV27 )
= $false )
| ( ( SV21 = SV31 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[488]) ).
thf(493,plain,
! [SV30: a,SV20: a,SV26: a,SV11: a] :
( ( ( SV11 = SV26 )
= $true )
| ( ( SV11 = SV26 )
= $false )
| ( ( SV20 = SV30 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[489]) ).
thf(494,plain,
! [SV26: a,SV11: a,SV30: a,SV20: a] :
( ( ( SV20 = SV30 )
= $true )
| ( ( SV11 = SV26 )
= $false )
| ( ( SV20 = SV30 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[490]) ).
thf(495,plain,
! [SV31: a,SV21: a,SV27: a,SV12: a] :
( ( ( SV12 = SV27 )
= $true )
| ( ( SV12 = SV27 )
= $false )
| ( ( SV21 = SV31 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[491]) ).
thf(496,plain,
! [SV27: a,SV12: a,SV31: a,SV21: a] :
( ( ( SV21 = SV31 )
= $true )
| ( ( SV12 = SV27 )
= $false )
| ( ( SV21 = SV31 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[492]) ).
thf(497,plain,
$false = $true,
inference(fo_atp_e,[status(thm)],[317,496,495,494,493,485,483,480,479,476,475,462,459,448,447,446,445,444,443,438,429,422,421,415,413,409,405,404,381,358,357,344,335,332,331,330,329,328,327,326,325,324,323,322,321,319,318]) ).
thf(498,plain,
$false,
inference(solved_all_splits,[solved_all_splits(join,[])],[497]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP106^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.07/0.19 % Computer : n018.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Tue Oct 6 11:19:52 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.67/0.65 ..
% 2.67/0.65
% 2.67/0.65 No.of.Axioms: 29
% 2.67/0.65
% 2.67/0.65 Length.of.Defs: 0
% 2.67/0.65
% 2.67/0.65 Contains.Choice.Funs: false
% 2.67/0.65 ........
% 2.67/0.65
% 2.67/0.65 ********************************
% 2.67/0.65 * All subproblems solved! *
% 2.67/0.65 ********************************
% 2.67/0.65 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:1,axioms:29,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:497,loop_count:0,foatp_calls:1,translation:fof_full)
% 2.67/0.65
% 2.67/0.65 %**** Beginning of derivation protocol ****
% 2.67/0.65 % SZS output start CNFRefutation
% See solution above
% 2.67/0.65
% 2.67/0.65 %**** End of derivation protocol ****
% 2.67/0.65 %**** no. of clauses in derivation: 245 ****
% 2.67/0.65 %**** clause counter: 497 ****
% 2.67/0.65
% 2.67/0.65 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:1,axioms:29,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:497,loop_count:0,foatp_calls:1,translation:fof_full)
%------------------------------------------------------------------------------