%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP108^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n007.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 Sep 30 08:04:23 AM UTC 2026
% Result : Theorem 0.73s 0.42s
% Output : CNFRefutation 0.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 13
% Syntax : Number of formulae : 39 ( 32 unt; 0 typ; 0 def)
% Number of atoms : 55 ( 25 equ; 0 cnn)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 2138 ( 17 ~; 11 |; 0 &;2105 @)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Number of types : 5 ( 4 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 21 ( 19 usr; 11 con; 0-3 aty)
% Number of variables : 10 ( 0 ^; 10 !; 0 ?; 10 :)
% Comments :
%------------------------------------------------------------------------------
thf(decl_sort1,type,
partia1833973666xt_a_b: $tType ).
thf(decl_sort2,type,
a: $tType ).
thf(decl_sort3,type,
set_a: $tType ).
thf(decl_sort4,type,
product_prod_a_a: $tType ).
thf(decl_26,type,
partia1066395285xt_a_b: partia1833973666xt_a_b > set_a ).
thf(decl_27,type,
mult_a_ring_ext_a_b: partia1833973666xt_a_b > a > a > a ).
thf(decl_39,type,
ord_less_eq_set_a: set_a > set_a > $o ).
thf(decl_40,type,
product_fst_a_a: product_prod_a_a > a ).
thf(decl_41,type,
product_snd_a_a: product_prod_a_a > a ).
thf(decl_43,type,
a_minus_a_b: partia1833973666xt_a_b > a > a > a ).
thf(decl_45,type,
add_a_b: partia1833973666xt_a_b > a > a > a ).
thf(decl_46,type,
zero_a_b: partia1833973666xt_a_b > a ).
thf(decl_49,type,
member_a: a > set_a > $o ).
thf(decl_50,type,
r: partia1833973666xt_a_b ).
thf(decl_51,type,
s: set_a ).
thf(decl_52,type,
r2: a ).
thf(decl_53,type,
r3: a ).
thf(decl_54,type,
s2: a ).
thf(decl_55,type,
s3: a ).
thf(decl_56,type,
t: a ).
thf(decl_57,type,
t2: a ).
thf(decl_58,type,
x: product_prod_a_a ).
thf(decl_59,type,
y: product_prod_a_a ).
thf(conj_0,conjecture,
( ( 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 @ t @ s3 ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ t2 @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ r2 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ ( product_fst_a_a @ x ) ) ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ s2 ) @ ( product_snd_a_a @ x ) ) @ ( mult_a_ring_ext_a_b @ r @ t @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ r3 ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ ( product_fst_a_a @ y ) ) ) ) ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( add_a_b @ r @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ r2 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ r3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.0orM7MA3G2/E---3.1_3843677.p',conj_0) ).
thf(fact_41_f25,axiom,
( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t @ s3 ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ t2 @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ r2 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ ( product_fst_a_a @ x ) ) ) ) )
= ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ r2 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.0orM7MA3G2/E---3.1_3843677.p',fact_41_f25) ).
thf(fact_57_f5,axiom,
( ( mult_a_ring_ext_a_b @ r @ t2 @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ r2 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ ( product_fst_a_a @ x ) ) ) )
= ( zero_a_b @ r ) ),
file('/export/starexec/sandbox2/tmp/tmp.0orM7MA3G2/E---3.1_3843677.p',fact_57_f5) ).
thf(fact_48_f30,axiom,
( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ s2 ) @ ( product_snd_a_a @ x ) ) @ ( mult_a_ring_ext_a_b @ r @ t @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ r3 ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ ( product_fst_a_a @ y ) ) ) ) )
= ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ r3 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.0orM7MA3G2/E---3.1_3843677.p',fact_48_f30) ).
thf(fact_58_f7,axiom,
( ( mult_a_ring_ext_a_b @ r @ t @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ r3 ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ ( product_fst_a_a @ y ) ) ) )
= ( zero_a_b @ r ) ),
file('/export/starexec/sandbox2/tmp/tmp.0orM7MA3G2/E---3.1_3843677.p',fact_58_f7) ).
thf(fact_21__092_060open_062_092_060lbrakk_062snd_Ax_H_A_092_060otimes_062_Asnd_Ay_H_A_092_060otimes_062_A_Is_H_A_092_060otimes_062_Ar_J_A_092_060ominus_062_As_A_092_060otimes_062_As_H_A_092_060otimes_062_A_Isnd_Ay_H_A_092_060otimes_062_Afst_Ax_H_J_A_092_060in_062_Acarrier_AR_059_Asnd_Ax_H_A_092_060otimes_062_Asnd_Ay_H_A_092_060otimes_062_A_Is_A_092_060otimes_062_Ar_H_J_A_092_060ominus_062_As_A_092_060otimes_062_As_H_A_092_060otimes_062_A_Isnd_Ax_H_A_092_060otimes_062_Afst_Ay_H_J_A_092_060in_062_Acarrier_AR_059_At_A_092_060otimes_062_At_H_A_092_060in_062_Acarrier_AR_092_060rbrakk_062_A_092_060Longrightarrow_062_At_A_092_060otimes_062_At_H_A_092_060otimes_062_A_Isnd_Ax_H_A_092_060otimes_062_Asnd_Ay_H_A_092_060otimes_062_A_Is_H_A_092_060otimes_062_Ar_J_A_092_060ominus_062_As_A_092_060otimes_062_As_H_A_092_060otimes_062_A_Isnd_Ay_H_A_092_060otimes_062_Afst_Ax_H_J_A_092_060oplus_062_A_Isnd_Ax_H_A_092_060otimes_062_Asnd_Ay_H_A_092_060otimes_062_A_Is_A_092_060otimes_062_Ar_H_J_A_092_060ominus_062_As_A_092_060otimes_062_As_H_A_092_060otimes_062_A_Isnd_Ax_H_A_092_060otimes_062_Afst_Ay_H_J_J_J_A_061_At_A_092_060otimes_062_At_H_A_092_060otimes_062_A_Isnd_Ax_H_A_092_060otimes_062_Asnd_Ay_H_A_092_060otimes_062_A_Is_H_A_092_060otimes_062_Ar_J_A_092_060ominus_062_As_A_092_060otimes_062_As_H_A_092_060otimes_062_A_Isnd_Ay_H_A_092_060otimes_062_Afst_Ax_H_J_J_A_092_060oplus_062_At_A_092_060otimes_062_At_H_A_092_060otimes_062_A_Isnd_Ax_H_A_092_060otimes_062_Asnd_Ay_H_A_092_060otimes_062_A_Is_A_092_060otimes_062_Ar_H_J_A_092_060ominus_062_As_A_092_060otimes_062_As_H_A_092_060otimes_062_A_Isnd_Ax_H_A_092_060otimes_062_Afst_Ay_H_J_J_092_060close_062,axiom,
( ( member_a @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ r2 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) @ ( partia1066395285xt_a_b @ r ) )
=> ( ( member_a @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ r3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) @ ( partia1066395285xt_a_b @ r ) )
=> ( ( member_a @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( partia1066395285xt_a_b @ r ) )
=> ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( add_a_b @ r @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ r2 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ r3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) )
= ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ r2 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ r3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.0orM7MA3G2/E---3.1_3843677.p',fact_21__092_060open_062_092_060lbrakk_062snd_Ax_H_A_092_060otimes_062_Asnd_Ay_H_A_092_060otimes_062_A_Is_H_A_092_060otimes_062_Ar_J_A_092_060ominus_062_As_A_092_060otimes_062_As_H_A_092_060otimes_062_A_Isnd_Ay_H_A_092_060otimes_062_Afst_Ax_H_J_A_092_060in_062_Acarrier_AR_059_Asnd_Ax_H_A_092_060otimes_062_Asnd_Ay_H_A_092_060otimes_062_A_Is_A_092_060otimes_062_Ar_H_J_A_092_060ominus_062_As_A_092_060otimes_062_As_H_A_092_060otimes_062_A_Isnd_Ax_H_A_092_060otimes_062_Afst_Ay_H_J_A_092_060in_062_Acarrier_AR_059_At_A_092_060otimes_062_At_H_A_092_060in_062_Acarrier_AR_092_060rbrakk_062_A_092_060Longrightarrow_062_At_A_092_060otimes_062_At_H_A_092_060otimes_062_A_Isnd_Ax_H_A_092_060otimes_062_Asnd_Ay_H_A_092_060otimes_062_A_Is_H_A_092_060otimes_062_Ar_J_A_092_060ominus_062_As_A_092_060otimes_062_As_H_A_092_060otimes_062_A_Isnd_Ay_H_A_092_060otimes_062_Afst_Ax_H_J_A_092_060oplus_062_A_Isnd_Ax_H_A_092_060otimes_062_Asnd_Ay_H_A_092_060otimes_062_A_Is_A_092_060otimes_062_Ar_H_J_A_092_060ominus_062_As_A_092_060otimes_062_As_H_A_092_060otimes_062_A_Isnd_Ax_H_A_092_060otimes_062_Afst_Ay_H_J_J_J_A_061_At_A_092_060otimes_062_At_H_A_092_060otimes_062_A_Isnd_Ax_H_A_092_060otimes_062_Asnd_Ay_H_A_092_060otimes_062_A_Is_H_A_092_060otimes_062_Ar_J_A_092_060ominus_062_As_A_092_060otimes_062_As_H_A_092_060otimes_062_A_Isnd_Ay_H_A_092_060otimes_062_Afst_Ax_H_J_J_A_092_060oplus_062_At_A_092_060otimes_062_At_H_A_092_060otimes_062_A_Isnd_Ax_H_A_092_060otimes_062_Asnd_Ay_H_A_092_060otimes_062_A_Is_A_092_060otimes_062_Ar_H_J_A_092_060ominus_062_As_A_092_060otimes_062_As_H_A_092_060otimes_062_A_Isnd_Ax_H_A_092_060otimes_062_Afst_Ay_H_J_J_092_060close_062) ).
thf(fact_42_f32,axiom,
( ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ r2 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ r2 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.0orM7MA3G2/E---3.1_3843677.p',fact_42_f32) ).
thf(fact_49_f33,axiom,
( ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ r3 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ r3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.0orM7MA3G2/E---3.1_3843677.p',fact_49_f33) ).
thf(fact_240_in__mono,axiom,
! [X9: set_a,X216: set_a,X4: a] :
( ( ord_less_eq_set_a @ X9 @ X216 )
=> ( ( member_a @ X4 @ X9 )
=> ( member_a @ X4 @ X216 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.0orM7MA3G2/E---3.1_3843677.p',fact_240_in__mono) ).
thf(fact_13_f42,axiom,
member_a @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ r3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) @ ( partia1066395285xt_a_b @ r ),
file('/export/starexec/sandbox2/tmp/tmp.0orM7MA3G2/E---3.1_3843677.p',fact_13_f42) ).
thf(fact_12_f41,axiom,
member_a @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ r2 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) @ ( partia1066395285xt_a_b @ r ),
file('/export/starexec/sandbox2/tmp/tmp.0orM7MA3G2/E---3.1_3843677.p',fact_12_f41) ).
thf(fact_142_subset,axiom,
ord_less_eq_set_a @ s @ ( partia1066395285xt_a_b @ r ),
file('/export/starexec/sandbox2/tmp/tmp.0orM7MA3G2/E---3.1_3843677.p',fact_142_subset) ).
thf(fact_65_f8,axiom,
member_a @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ s,
file('/export/starexec/sandbox2/tmp/tmp.0orM7MA3G2/E---3.1_3843677.p',fact_65_f8) ).
thf(c_0_13,negated_conjecture,
( ( 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 @ t @ s3 ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ t2 @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ r2 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ ( product_fst_a_a @ x ) ) ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ s2 ) @ ( product_snd_a_a @ x ) ) @ ( mult_a_ring_ext_a_b @ r @ t @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ r3 ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ ( product_fst_a_a @ y ) ) ) ) ) )
!= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( add_a_b @ r @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ r2 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ r3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) ) ),
inference(assume_negation,[status(cth)],[conj_0]) ).
thf(c_0_14,negated_conjecture,
( ( 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 @ t @ s3 ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ t2 @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ r2 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ ( product_fst_a_a @ x ) ) ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ s2 ) @ ( product_snd_a_a @ x ) ) @ ( mult_a_ring_ext_a_b @ r @ t @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ r3 ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ ( product_fst_a_a @ y ) ) ) ) ) )
!= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( add_a_b @ r @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ r2 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ r3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[c_0_13]) ).
thf(c_0_15,plain,
( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t @ s3 ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ t2 @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ r2 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ ( product_fst_a_a @ x ) ) ) ) )
= ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ r2 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) ) ),
inference(split_conjunct,[status(thm)],[fact_41_f25]) ).
thf(c_0_16,plain,
( ( mult_a_ring_ext_a_b @ r @ t2 @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ r2 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ ( product_fst_a_a @ x ) ) ) )
= ( zero_a_b @ r ) ),
inference(split_conjunct,[status(thm)],[fact_57_f5]) ).
thf(c_0_17,plain,
( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ s2 ) @ ( product_snd_a_a @ x ) ) @ ( mult_a_ring_ext_a_b @ r @ t @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ r3 ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ ( product_fst_a_a @ y ) ) ) ) )
= ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ r3 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) ),
inference(split_conjunct,[status(thm)],[fact_48_f30]) ).
thf(c_0_18,plain,
( ( mult_a_ring_ext_a_b @ r @ t @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ r3 ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ ( product_fst_a_a @ y ) ) ) )
= ( zero_a_b @ r ) ),
inference(split_conjunct,[status(thm)],[fact_58_f7]) ).
thf(c_0_19,negated_conjecture,
( ( 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 @ t @ s3 ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ t2 @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ r2 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ ( product_fst_a_a @ x ) ) ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ s2 ) @ ( product_snd_a_a @ x ) ) @ ( mult_a_ring_ext_a_b @ r @ t @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ r3 ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ ( product_fst_a_a @ y ) ) ) ) ) )
!= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( add_a_b @ r @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ r2 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ r3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) ) ),
inference(fof_nnf,[status(thm)],[c_0_14]) ).
thf(c_0_20,plain,
( ~ ( member_a @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ r2 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) @ ( partia1066395285xt_a_b @ r ) )
| ~ ( member_a @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ r3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) @ ( partia1066395285xt_a_b @ r ) )
| ~ ( member_a @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( partia1066395285xt_a_b @ r ) )
| ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( add_a_b @ r @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ r2 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ r3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) )
= ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ r2 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ r3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) ) ) ),
inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_21__092_060open_062_092_060lbrakk_062snd_Ax_H_A_092_060otimes_062_Asnd_Ay_H_A_092_060otimes_062_A_Is_H_A_092_060otimes_062_Ar_J_A_092_060ominus_062_As_A_092_060otimes_062_As_H_A_092_060otimes_062_A_Isnd_Ay_H_A_092_060otimes_062_Afst_Ax_H_J_A_092_060in_062_Acarrier_AR_059_Asnd_Ax_H_A_092_060otimes_062_Asnd_Ay_H_A_092_060otimes_062_A_Is_A_092_060otimes_062_Ar_H_J_A_092_060ominus_062_As_A_092_060otimes_062_As_H_A_092_060otimes_062_A_Isnd_Ax_H_A_092_060otimes_062_Afst_Ay_H_J_A_092_060in_062_Acarrier_AR_059_At_A_092_060otimes_062_At_H_A_092_060in_062_Acarrier_AR_092_060rbrakk_062_A_092_060Longrightarrow_062_At_A_092_060otimes_062_At_H_A_092_060otimes_062_A_Isnd_Ax_H_A_092_060otimes_062_Asnd_Ay_H_A_092_060otimes_062_A_Is_H_A_092_060otimes_062_Ar_J_A_092_060ominus_062_As_A_092_060otimes_062_As_H_A_092_060otimes_062_A_Isnd_Ay_H_A_092_060otimes_062_Afst_Ax_H_J_A_092_060oplus_062_A_Isnd_Ax_H_A_092_060otimes_062_Asnd_Ay_H_A_092_060otimes_062_A_Is_A_092_060otimes_062_Ar_H_J_A_092_060ominus_062_As_A_092_060otimes_062_As_H_A_092_060otimes_062_A_Isnd_Ax_H_A_092_060otimes_062_Afst_Ay_H_J_J_J_A_061_At_A_092_060otimes_062_At_H_A_092_060otimes_062_A_Isnd_Ax_H_A_092_060otimes_062_Asnd_Ay_H_A_092_060otimes_062_A_Is_H_A_092_060otimes_062_Ar_J_A_092_060ominus_062_As_A_092_060otimes_062_As_H_A_092_060otimes_062_A_Isnd_Ay_H_A_092_060otimes_062_Afst_Ax_H_J_J_A_092_060oplus_062_At_A_092_060otimes_062_At_H_A_092_060otimes_062_A_Isnd_Ax_H_A_092_060otimes_062_Asnd_Ay_H_A_092_060otimes_062_A_Is_A_092_060otimes_062_Ar_H_J_A_092_060ominus_062_As_A_092_060otimes_062_As_H_A_092_060otimes_062_A_Isnd_Ax_H_A_092_060otimes_062_Afst_Ay_H_J_J_092_060close_062])]) ).
thf(c_0_21,plain,
( ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ r2 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ r2 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) ) ),
inference(split_conjunct,[status(thm)],[fact_42_f32]) ).
thf(c_0_22,plain,
( ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ r2 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t @ s3 ) @ ( product_snd_a_a @ y ) ) @ ( zero_a_b @ r ) ) ),
inference(rw,[status(thm)],[c_0_15,c_0_16]) ).
thf(c_0_23,plain,
( ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ r3 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ r3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) ),
inference(split_conjunct,[status(thm)],[fact_49_f33]) ).
thf(c_0_24,plain,
( ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ r3 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ s2 ) @ ( product_snd_a_a @ x ) ) @ ( zero_a_b @ r ) ) ),
inference(rw,[status(thm)],[c_0_17,c_0_18]) ).
thf(c_0_25,negated_conjecture,
( ( 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 @ t @ s3 ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ t2 @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ r2 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ ( product_fst_a_a @ x ) ) ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ s2 ) @ ( product_snd_a_a @ x ) ) @ ( mult_a_ring_ext_a_b @ r @ t @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ r3 ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ ( product_fst_a_a @ y ) ) ) ) ) )
!= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( add_a_b @ r @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ r2 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ r3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
thf(c_0_26,plain,
! [X873: set_a,X874: set_a,X875: a] :
( ~ ( ord_less_eq_set_a @ X873 @ X874 )
| ~ ( member_a @ X875 @ X873 )
| ( member_a @ X875 @ X874 ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_240_in__mono])])]) ).
thf(c_0_27,plain,
( ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( add_a_b @ r @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ r2 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ r3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) )
= ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ r2 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ r3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) ) )
| ~ ( member_a @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ r2 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) @ ( partia1066395285xt_a_b @ r ) )
| ~ ( member_a @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ r3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) @ ( partia1066395285xt_a_b @ r ) )
| ~ ( member_a @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( partia1066395285xt_a_b @ r ) ) ),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
thf(c_0_28,plain,
( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ r2 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t @ s3 ) @ ( product_snd_a_a @ y ) ) @ ( zero_a_b @ r ) ) ),
inference(rw,[status(thm)],[c_0_21,c_0_22]) ).
thf(c_0_29,plain,
( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ r3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) )
= ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ s2 ) @ ( product_snd_a_a @ x ) ) @ ( zero_a_b @ r ) ) ),
inference(rw,[status(thm)],[c_0_23,c_0_24]) ).
thf(c_0_30,plain,
member_a @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ r3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) @ ( partia1066395285xt_a_b @ r ),
inference(split_conjunct,[status(thm)],[fact_13_f42]) ).
thf(c_0_31,plain,
member_a @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ r2 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) @ ( partia1066395285xt_a_b @ r ),
inference(split_conjunct,[status(thm)],[fact_12_f41]) ).
thf(c_0_32,negated_conjecture,
( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( add_a_b @ r @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s3 @ r2 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) @ ( a_minus_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_snd_a_a @ y ) ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ r3 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) )
!= ( 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 @ t @ s3 ) @ ( product_snd_a_a @ y ) ) @ ( zero_a_b @ r ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ s2 ) @ ( product_snd_a_a @ x ) ) @ ( zero_a_b @ r ) ) ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_25,c_0_16]),c_0_18]) ).
thf(c_0_33,plain,
! [X1: a,X32: set_a,X9: set_a] :
( ( member_a @ X1 @ X32 )
| ~ ( ord_less_eq_set_a @ X9 @ X32 )
| ~ ( member_a @ X1 @ X9 ) ),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
thf(c_0_34,plain,
ord_less_eq_set_a @ s @ ( partia1066395285xt_a_b @ r ),
inference(split_conjunct,[status(thm)],[fact_142_subset]) ).
thf(c_0_35,plain,
~ ( member_a @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( partia1066395285xt_a_b @ r ) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_27,c_0_28]),c_0_29]),c_0_30]),c_0_31])]),c_0_32]) ).
thf(c_0_36,plain,
! [X1: a] :
( ( member_a @ X1 @ ( partia1066395285xt_a_b @ r ) )
| ~ ( member_a @ X1 @ s ) ),
inference(spm,[status(thm)],[c_0_33,c_0_34]) ).
thf(c_0_37,plain,
member_a @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ s,
inference(split_conjunct,[status(thm)],[fact_65_f8]) ).
thf(c_0_38,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35,c_0_36]),c_0_37])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP108^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n007.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 Sep 29 19:52:26 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.23 Running higher-order theorem proving
% 0.21/0.28 Running: /export/starexec/sandbox2/solver/bin/eprover-ho --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/tmp/tmp.0orM7MA3G2/E---3.1_3843677.p
% 0.73/0.42 % Version: 3.5.1-ho
% 0.73/0.42 % Preprocessing class: HSLSSMSMSSSNSFA.
% 0.73/0.42 % Scheduled 6 strats onto 8 cores with 300 seconds (2400 total)
% 0.73/0.42 % Starting new_ho_10 with 900s (3) cores
% 0.73/0.42 % Starting sh2lt with 300s (1) cores
% 0.73/0.42 % Starting new_ho_5 with 300s (1) cores
% 0.73/0.42 % Starting full_lambda_5 with 300s (1) cores
% 0.73/0.42 % Starting sh9 with 300s (1) cores
% 0.73/0.42 % Starting ehoh_best8_lambda with 300s (1) cores
% 0.73/0.42 % sh2lt with pid 3843691 completed with status 0
% 0.73/0.42 % Result found by sh2lt
% 0.73/0.42 % Preprocessing class: HSLSSMSMSSSNSFA.
% 0.73/0.42 % Scheduled 6 strats onto 8 cores with 300 seconds (2400 total)
% 0.73/0.42 % Starting new_ho_10 with 900s (3) cores
% 0.73/0.42 % Starting sh2lt with 300s (1) cores
% 0.73/0.42 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,5,,4,20000,1.0,true))
% 0.73/0.42 % SinE strategy is GSinE(CountFormulas,hypos,5,,4,20000,1.0,true)
% 0.73/0.42 % Search class: HGHSM-FSLM31-DSFFFFBN
% 0.73/0.42 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.73/0.42 % Starting SubtermCWHack with 28s (1) cores
% 0.73/0.42 % SubtermCWHack with pid 3843697 completed with status 0
% 0.73/0.42 % Result found by SubtermCWHack
% 0.73/0.42 % Preprocessing class: HSLSSMSMSSSNSFA.
% 0.73/0.42 % Scheduled 6 strats onto 8 cores with 300 seconds (2400 total)
% 0.73/0.42 % Starting new_ho_10 with 900s (3) cores
% 0.73/0.42 % Starting sh2lt with 300s (1) cores
% 0.73/0.42 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,5,,4,20000,1.0,true))
% 0.73/0.42 % SinE strategy is GSinE(CountFormulas,hypos,5,,4,20000,1.0,true)
% 0.73/0.42 % Search class: HGHSM-FSLM31-DSFFFFBN
% 0.73/0.42 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.73/0.42 % Starting SubtermCWHack with 28s (1) cores
% 0.73/0.42 % Preprocessing time : 0.003 s
% 0.73/0.42
% 0.73/0.42 % Proof found!
% 0.73/0.42 % SZS status Theorem
% 0.73/0.42 % SZS output start CNFRefutation
% See solution above
% 0.73/0.43 % Parsed axioms : 287
% 0.73/0.43 % Removed by relevancy pruning/SinE : 50
% 0.73/0.43 % Initial clauses : 291
% 0.73/0.43 % Removed in clause preprocessing : 12
% 0.73/0.43 % Initial clauses in saturation : 279
% 0.73/0.43 % Processed clauses : 1804
% 0.73/0.43 % ...of these trivial : 68
% 0.73/0.43 % ...subsumed : 1298
% 0.73/0.43 % ...remaining for further processing : 438
% 0.73/0.43 % Other redundant clauses eliminated : 140
% 0.73/0.43 % Clauses deleted for lack of memory : 0
% 0.73/0.43 % Backward-subsumed : 0
% 0.73/0.43 % Backward-rewritten : 26
% 0.73/0.43 % Generated clauses : 6244
% 0.73/0.43 % ...of the previous two non-redundant : 5538
% 0.73/0.43 % ...aggressively subsumed : 0
% 0.73/0.43 % Contextual simplify-reflections : 0
% 0.73/0.43 % Paramodulations : 6092
% 0.73/0.43 % Factorizations : 2
% 0.73/0.43 % NegExts : 0
% 0.73/0.43 % Equation resolutions : 150
% 0.73/0.43 % Disequality decompositions : 0
% 0.73/0.43 % Total rewrite steps : 4217
% 0.73/0.43 % ...of those cached : 3570
% 0.73/0.43 % Propositional unsat checks : 0
% 0.73/0.43 % Propositional check models : 0
% 0.73/0.43 % Propositional check unsatisfiable : 0
% 0.73/0.43 % Propositional clauses : 0
% 0.73/0.43 % Propositional clauses after purity: 0
% 0.73/0.43 % Propositional unsat core size : 0
% 0.73/0.43 % Propositional preprocessing time : 0.000
% 0.73/0.43 % Propositional encoding time : 0.000
% 0.73/0.43 % Propositional solver time : 0.000
% 0.73/0.43 % Success case prop preproc time : 0.000
% 0.73/0.43 % Success case prop encoding time : 0.000
% 0.73/0.43 % Success case prop solver time : 0.000
% 0.73/0.43 % Current number of processed clauses : 375
% 0.73/0.43 % Positive orientable unit clauses : 80
% 0.73/0.43 % Positive unorientable unit clauses: 5
% 0.73/0.43 % Negative unit clauses : 5
% 0.73/0.43 % Non-unit-clauses : 285
% 0.73/0.43 % Current number of unprocessed clauses: 3755
% 0.73/0.43 % ...number of literals in the above : 8928
% 0.73/0.43 % Current number of archived formulas : 0
% 0.73/0.43 % Current number of archived clauses : 26
% 0.73/0.43 % Clause-clause subsumption calls (NU) : 113565
% 0.73/0.43 % Rec. Clause-clause subsumption calls : 84454
% 0.73/0.43 % Non-unit clause-clause subsumptions : 1205
% 0.73/0.43 % Unit Clause-clause subsumption calls : 3357
% 0.73/0.43 % Rewrite failures with RHS unbound : 22
% 0.73/0.43 % BW rewrite match attempts : 187
% 0.73/0.43 % BW rewrite match successes : 60
% 0.73/0.43 % Condensation attempts : 0
% 0.73/0.43 % Condensation successes : 0
% 0.73/0.43 % Termbank termtop insertions : 106720
% 0.73/0.43 % Search garbage collected termcells : 5204
% 0.73/0.43
% 0.73/0.43 % -------------------------------------------------
% 0.73/0.43 % User time : 0.093 s
% 0.73/0.43 % System time : 0.011 s
% 0.73/0.43 % Total time : 0.104 s
% 0.73/0.43 % Maximum resident set size: 5032 pages
% 0.73/0.43
% 0.73/0.43 % -------------------------------------------------
% 0.73/0.43 % User time : 0.104 s
% 0.73/0.43 % System time : 0.017 s
% 0.73/0.43 % Total time : 0.121 s
% 0.73/0.43 % Maximum resident set size: 5376 pages
% 0.73/0.43 % E exiting
%------------------------------------------------------------------------------