%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP108^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n013.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:10:43 AM UTC 2026
% Result : Theorem 23.39s 3.71s
% Output : Refutation 23.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 18
% Syntax : Number of formulae : 102 ( 75 unt; 0 typ; 4 def)
% Number of atoms : 258 ( 100 equ; 0 cnn)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 4916 ( 40 ~; 35 |; 0 &;4816 @)
% ( 4 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 6 ( 5 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 95 ( 91 usr; 20 con; 0-4 aty)
% ( 4 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 95 ( 0 sgn 5 !; 0 ?; 95 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
partia1833973666xt_a_b: $tType ).
thf(type_def_6,type,
product_prod_a_a: $tType ).
thf(type_def_7,type,
set_a: $tType ).
thf(type_def_8,type,
int: $tType ).
thf(type_def_9,type,
a: $tType ).
thf(type_def_10,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
a_l_coset_a_b: partia1833973666xt_a_b > a > set_a > set_a ).
thf(func_def_1,type,
additi2104487374up_a_b: set_a > partia1833973666xt_a_b > $o ).
thf(func_def_2,type,
set_add_a_b: partia1833973666xt_a_b > set_a > set_a > set_a ).
thf(func_def_3,type,
partia1066395285xt_a_b: partia1833973666xt_a_b > set_a ).
thf(func_def_4,type,
mult_a_ring_ext_a_b: partia1833973666xt_a_b > a > a > a ).
thf(func_def_5,type,
minus_minus_int: int > int > int ).
thf(func_def_6,type,
minus_minus_set_a: set_a > set_a > set_a ).
thf(func_def_7,type,
plus_plus_int: int > int > int ).
thf(func_def_8,type,
uminus_uminus_int: int > int ).
thf(func_def_9,type,
uminus_uminus_set_a: set_a > set_a ).
thf(func_def_10,type,
locali1648887798ac_a_b: partia1833973666xt_a_b > set_a > $o ).
thf(func_def_11,type,
locali807230110ng_a_b: partia1833973666xt_a_b > set_a > $o ).
thf(func_def_12,type,
locali880295127ng_a_b: partia1833973666xt_a_b > set_a > $o ).
thf(func_def_13,type,
locali425460998xt_a_b: partia1833973666xt_a_b > set_a > $o ).
thf(func_def_14,type,
bot_bot_set_a: set_a ).
thf(func_def_15,type,
ord_less_eq_int: int > int > $o ).
thf(func_def_16,type,
ord_less_eq_set_a: set_a > set_a > $o ).
thf(func_def_17,type,
product_fst_a_a: product_prod_a_a > a ).
thf(func_def_18,type,
product_snd_a_a: product_prod_a_a > a ).
thf(func_def_19,type,
a_inv_a_b: partia1833973666xt_a_b > a > a ).
thf(func_def_20,type,
a_minus_a_b: partia1833973666xt_a_b > a > a > a ).
thf(func_def_21,type,
add_pow_a_b_int: partia1833973666xt_a_b > int > a > a ).
thf(func_def_22,type,
add_a_b: partia1833973666xt_a_b > a > a > a ).
thf(func_def_23,type,
zero_a_b: partia1833973666xt_a_b > a ).
thf(func_def_24,type,
semiring_a_b: partia1833973666xt_a_b > $o ).
thf(func_def_25,type,
collect_a: ( a > $o ) > set_a ).
thf(func_def_26,type,
member_a: a > set_a > $o ).
thf(func_def_27,type,
r: partia1833973666xt_a_b ).
thf(func_def_28,type,
s: set_a ).
thf(func_def_29,type,
r2: a ).
thf(func_def_30,type,
r3: a ).
thf(func_def_31,type,
s2: a ).
thf(func_def_32,type,
s3: a ).
thf(func_def_33,type,
t: a ).
thf(func_def_34,type,
t2: a ).
thf(func_def_35,type,
x: product_prod_a_a ).
thf(func_def_36,type,
y: product_prod_a_a ).
thf(func_def_40,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_41,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_42,type,
vEQ:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
thf(func_def_43,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_44,type,
vAND: $o > $o > $o ).
thf(func_def_45,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_46,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_47,type,
vNOT: $o > $o ).
thf(func_def_48,type,
vSIGMA:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_49,type,
vIMP: $o > $o > $o ).
thf(func_def_50,type,
sK0: ( a > $o ) > ( a > $o ) > a ).
thf(func_def_51,type,
sK1: ( a > a > $o ) > a ).
thf(func_def_52,type,
sK2: ( a > a > $o ) > a ).
thf(func_def_53,type,
sK3: a > a ).
thf(func_def_54,type,
sK4: a > a ).
thf(func_def_55,type,
sK5: a > a ).
thf(func_def_56,type,
sK6: a ).
thf(func_def_57,type,
sK7: a ).
thf(func_def_58,type,
sK8: set_a > a ).
thf(func_def_59,type,
sK9: set_a > a ).
thf(func_def_60,type,
sK10: set_a > a ).
thf(func_def_61,type,
sK11: set_a > set_a > a ).
thf(func_def_62,type,
sK12: set_a > a ).
thf(func_def_63,type,
sK13: set_a > set_a > a ).
thf(func_def_64,type,
sK14: set_a > set_a > a ).
thf(func_def_65,type,
sK15: set_a > a ).
thf(func_def_66,type,
sK16: set_a > a ).
thf(func_def_67,type,
sK17: set_a > set_a > a ).
thf(func_def_68,type,
sK18: set_a > set_a > a ).
thf(func_def_69,type,
sK19: set_a > set_a > a ).
thf(func_def_70,type,
sK20: set_a > set_a > a ).
thf(func_def_71,type,
sK21: set_a > set_a > a ).
thf(func_def_72,type,
sK22: ( a > $o ) > a ).
thf(func_def_73,type,
sK23: ( a > $o ) > a ).
thf(func_def_74,type,
sK24: set_a > a ).
thf(func_def_75,type,
sK25: set_a > set_a > a ).
thf(func_def_76,type,
sK26: set_a > a ).
thf(func_def_77,type,
sK27: set_a > a ).
thf(func_def_78,type,
sK28: set_a > a ).
thf(func_def_79,type,
sK29: set_a > a ).
thf(func_def_80,type,
sK30: set_a > a ).
thf(func_def_81,type,
sK31: set_a > a ).
thf(func_def_82,type,
sK32: set_a > a ).
thf(func_def_83,type,
sK33: set_a > a ).
thf(func_def_84,type,
sK34: set_a > a ).
thf(func_def_85,type,
sK35: set_a > a ).
thf(func_def_86,type,
sK36: set_a > a ).
thf(func_def_87,type,
sK37: set_a > a ).
thf(func_def_88,type,
sK38: set_a > a ).
thf(f13,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/benchmark/theBenchmark.p',fact_12_f41) ).
thf(f14,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/benchmark/theBenchmark.p',fact_13_f42) ).
thf(f22,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/benchmark/theBenchmark.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(f42,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/benchmark/theBenchmark.p',fact_41_f25) ).
thf(f43,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/benchmark/theBenchmark.p',fact_42_f32) ).
thf(f49,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/benchmark/theBenchmark.p',fact_48_f30) ).
thf(f50,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/benchmark/theBenchmark.p',fact_49_f33) ).
thf(f58,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/benchmark/theBenchmark.p',fact_57_f5) ).
thf(f59,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/benchmark/theBenchmark.p',fact_58_f7) ).
thf(f66,axiom,
member_a @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ s,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_65_f8) ).
thf(f131,axiom,
( a_minus_a_b
= ( ^ [X0: partia1833973666xt_a_b,X1: a,X2: a] : ( add_a_b @ X0 @ X1 @ ( a_inv_a_b @ X0 @ X2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_130_a__minus__def) ).
thf(f143,axiom,
ord_less_eq_set_a @ s @ ( partia1066395285xt_a_b @ r ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_142_subset) ).
thf(f244,axiom,
( ord_less_eq_set_a
= ( ^ [X0: set_a,X1: set_a] :
! [X2: a] :
( ( member_a @ X2 @ X0 )
=> ( member_a @ X2 @ X1 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_243_subset__eq) ).
thf(f245,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/benchmark/theBenchmark.p',conj_0) ).
thf(f246,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(negated_conjecture,[status(cth)],[f245]) ).
thf(f267,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(rectify,[],[f13]) ).
thf(f268,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 ) )
= $true ),
inference(fool_elimination,[],[f267]) ).
thf(f269,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(rectify,[],[f14]) ).
thf(f270,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 ) )
= $true ),
inference(fool_elimination,[],[f269]) ).
thf(f283,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(rectify,[],[f22]) ).
thf(f284,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 ) )
= $true )
=> ( ( ( 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 ) )
= $true )
=> ( ( ( member_a @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( partia1066395285xt_a_b @ r ) )
= $true )
=> ( ( 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 ) ) ) ) ) )
= ( 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(fool_elimination,[],[f283]) ).
thf(f327,plain,
member_a @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ s,
inference(rectify,[],[f66]) ).
thf(f328,plain,
( ( member_a @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ s )
= $true ),
inference(fool_elimination,[],[f327]) ).
thf(f446,plain,
( a_minus_a_b
= ( ^ [Y0: partia1833973666xt_a_b,Y1: a,Y2: a] : ( add_a_b @ Y0 @ Y1 @ ( a_inv_a_b @ Y0 @ Y2 ) ) ) ),
inference(fool_elimination,[],[f131]) ).
thf(f469,plain,
ord_less_eq_set_a @ s @ ( partia1066395285xt_a_b @ r ),
inference(rectify,[],[f143]) ).
thf(f470,plain,
( ( ord_less_eq_set_a @ s @ ( partia1066395285xt_a_b @ r ) )
= $true ),
inference(fool_elimination,[],[f469]) ).
thf(f564,plain,
( ord_less_eq_set_a
= ( ^ [X0: set_a,X1: set_a] :
! [X2: a] :
( ( member_a @ X2 @ X0 )
=> ( member_a @ X2 @ X1 ) ) ) ),
inference(rectify,[],[f244]) ).
thf(f565,plain,
( ord_less_eq_set_a
= ( ^ [Y0: set_a,Y1: set_a] :
( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y0 )
=> ( member_a @ Y2 @ Y1 ) ) ) ) ),
inference(fool_elimination,[],[f564]) ).
thf(f572,plain,
( ( 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(flattening,[],[f246]) ).
thf(f595,plain,
( ( ( 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 ) ) ) ) ) )
= ( 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 ) ) ) ) ) ) )
| ( ( member_a @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( partia1066395285xt_a_b @ r ) )
!= $true )
| ( ( 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 ) )
!= $true )
| ( ( 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 ) )
!= $true ) ),
inference(ennf_transformation,[],[f284]) ).
thf(f596,plain,
( ( ( 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 ) ) ) ) ) )
= ( 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 ) ) ) ) ) ) )
| ( ( member_a @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( partia1066395285xt_a_b @ r ) )
!= $true )
| ( ( 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 ) )
!= $true )
| ( ( 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 ) )
!= $true ) ),
inference(flattening,[],[f595]) ).
thf(f794,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 ) )
= $true ),
inference(cnf_transformation,[],[f268]) ).
thf(f795,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 ) )
= $true ),
inference(cnf_transformation,[],[f270]) ).
thf(f803,plain,
( ( ( 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 ) ) ) ) ) )
= ( 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 ) ) ) ) ) ) )
| ( ( member_a @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( partia1066395285xt_a_b @ r ) )
!= $true )
| ( ( 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 ) )
!= $true )
| ( ( 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 ) )
!= $true ) ),
inference(cnf_transformation,[],[f596]) ).
thf(f823,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(cnf_transformation,[],[f42]) ).
thf(f824,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 ) ) ) ) )
= ( 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(cnf_transformation,[],[f43]) ).
thf(f830,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(cnf_transformation,[],[f49]) ).
thf(f831,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 ) ) ) ) )
= ( 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(cnf_transformation,[],[f50]) ).
thf(f839,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(cnf_transformation,[],[f58]) ).
thf(f840,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(cnf_transformation,[],[f59]) ).
thf(f847,plain,
( ( member_a @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ s )
= $true ),
inference(cnf_transformation,[],[f328]) ).
thf(f917,plain,
( a_minus_a_b
= ( ^ [Y0: partia1833973666xt_a_b,Y1: a,Y2: a] : ( add_a_b @ Y0 @ Y1 @ ( a_inv_a_b @ Y0 @ Y2 ) ) ) ),
inference(cnf_transformation,[],[f446]) ).
thf(f929,plain,
( ( ord_less_eq_set_a @ s @ ( partia1066395285xt_a_b @ r ) )
= $true ),
inference(cnf_transformation,[],[f470]) ).
thf(f1037,plain,
( ord_less_eq_set_a
= ( ^ [Y0: set_a,Y1: set_a] :
( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y0 )
=> ( member_a @ Y2 @ Y1 ) ) ) ) ),
inference(cnf_transformation,[],[f565]) ).
thf(f1038,plain,
( ( 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(cnf_transformation,[],[f572]) ).
thf(f1042,plain,
( $true
= ( member_a
@ ( ^ [Y0: partia1833973666xt_a_b,Y1: a,Y2: a] : ( add_a_b @ Y0 @ Y1 @ ( a_inv_a_b @ Y0 @ Y2 ) )
@ 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(definition_unfolding,[],[f794,f917]) ).
thf(f1043,plain,
( $true
= ( member_a
@ ( ^ [Y0: partia1833973666xt_a_b,Y1: a,Y2: a] : ( add_a_b @ Y0 @ Y1 @ ( a_inv_a_b @ Y0 @ Y2 ) )
@ 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(definition_unfolding,[],[f795,f917]) ).
thf(f1047,plain,
( ( ( add_a_b @ r
@ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t )
@ ( ^ [Y0: partia1833973666xt_a_b,Y1: a,Y2: a] : ( add_a_b @ Y0 @ Y1 @ ( a_inv_a_b @ Y0 @ Y2 ) )
@ 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 )
@ ( ^ [Y0: partia1833973666xt_a_b,Y1: a,Y2: a] : ( add_a_b @ Y0 @ Y1 @ ( a_inv_a_b @ Y0 @ Y2 ) )
@ 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 @ t2 @ t )
@ ( add_a_b @ r
@ ( ^ [Y0: partia1833973666xt_a_b,Y1: a,Y2: a] : ( add_a_b @ Y0 @ Y1 @ ( a_inv_a_b @ Y0 @ Y2 ) )
@ 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 ) ) ) )
@ ( ^ [Y0: partia1833973666xt_a_b,Y1: a,Y2: a] : ( add_a_b @ Y0 @ Y1 @ ( a_inv_a_b @ Y0 @ Y2 ) )
@ 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 @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( partia1066395285xt_a_b @ r ) )
!= $true )
| ( $true
!= ( member_a
@ ( ^ [Y0: partia1833973666xt_a_b,Y1: a,Y2: a] : ( add_a_b @ Y0 @ Y1 @ ( a_inv_a_b @ Y0 @ Y2 ) )
@ 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 ) ) )
| ( $true
!= ( member_a
@ ( ^ [Y0: partia1833973666xt_a_b,Y1: a,Y2: a] : ( add_a_b @ Y0 @ Y1 @ ( a_inv_a_b @ Y0 @ Y2 ) )
@ 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(definition_unfolding,[],[f803,f917,f917,f917,f917,f917,f917]) ).
thf(f1052,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
@ ( ^ [Y0: partia1833973666xt_a_b,Y1: a,Y2: a] : ( add_a_b @ Y0 @ Y1 @ ( a_inv_a_b @ Y0 @ Y2 ) )
@ 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 ) ) ) ) )
= ( ^ [Y0: partia1833973666xt_a_b,Y1: a,Y2: a] : ( add_a_b @ Y0 @ Y1 @ ( a_inv_a_b @ Y0 @ Y2 ) )
@ 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(definition_unfolding,[],[f823,f917,f917]) ).
thf(f1053,plain,
( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t )
@ ( ^ [Y0: partia1833973666xt_a_b,Y1: a,Y2: a] : ( add_a_b @ Y0 @ Y1 @ ( a_inv_a_b @ Y0 @ Y2 ) )
@ 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 ) ) ) ) )
= ( ^ [Y0: partia1833973666xt_a_b,Y1: a,Y2: a] : ( add_a_b @ Y0 @ Y1 @ ( a_inv_a_b @ Y0 @ Y2 ) )
@ 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(definition_unfolding,[],[f824,f917,f917]) ).
thf(f1056,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
@ ( ^ [Y0: partia1833973666xt_a_b,Y1: a,Y2: a] : ( add_a_b @ Y0 @ Y1 @ ( a_inv_a_b @ Y0 @ Y2 ) )
@ 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 ) ) ) ) )
= ( ^ [Y0: partia1833973666xt_a_b,Y1: a,Y2: a] : ( add_a_b @ Y0 @ Y1 @ ( a_inv_a_b @ Y0 @ Y2 ) )
@ 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(definition_unfolding,[],[f830,f917,f917]) ).
thf(f1057,plain,
( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t )
@ ( ^ [Y0: partia1833973666xt_a_b,Y1: a,Y2: a] : ( add_a_b @ Y0 @ Y1 @ ( a_inv_a_b @ Y0 @ Y2 ) )
@ 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 ) ) ) ) )
= ( ^ [Y0: partia1833973666xt_a_b,Y1: a,Y2: a] : ( add_a_b @ Y0 @ Y1 @ ( a_inv_a_b @ Y0 @ Y2 ) )
@ 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(definition_unfolding,[],[f831,f917,f917]) ).
thf(f1063,plain,
( ( zero_a_b @ r )
= ( mult_a_ring_ext_a_b @ r @ t2
@ ( ^ [Y0: partia1833973666xt_a_b,Y1: a,Y2: a] : ( add_a_b @ Y0 @ Y1 @ ( a_inv_a_b @ Y0 @ Y2 ) )
@ 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 ) ) ) ) ),
inference(definition_unfolding,[],[f839,f917]) ).
thf(f1064,plain,
( ( zero_a_b @ r )
= ( mult_a_ring_ext_a_b @ r @ t
@ ( ^ [Y0: partia1833973666xt_a_b,Y1: a,Y2: a] : ( add_a_b @ Y0 @ Y1 @ ( a_inv_a_b @ Y0 @ Y2 ) )
@ 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 ) ) ) ) ),
inference(definition_unfolding,[],[f840,f917]) ).
thf(f1071,plain,
( $true
= ( ^ [Y0: set_a,Y1: set_a] :
( !! @ a
@ ^ [Y2: a] :
( ( member_a @ Y2 @ Y0 )
=> ( member_a @ Y2 @ Y1 ) ) )
@ s
@ ( partia1066395285xt_a_b @ r ) ) ),
inference(definition_unfolding,[],[f929,f1037]) ).
thf(f1129,plain,
( ( 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
@ ( ^ [Y0: partia1833973666xt_a_b,Y1: a,Y2: a] : ( add_a_b @ Y0 @ Y1 @ ( a_inv_a_b @ Y0 @ Y2 ) )
@ 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
@ ( ^ [Y0: partia1833973666xt_a_b,Y1: a,Y2: a] : ( add_a_b @ Y0 @ Y1 @ ( a_inv_a_b @ Y0 @ Y2 ) )
@ 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
@ ( ^ [Y0: partia1833973666xt_a_b,Y1: a,Y2: a] : ( add_a_b @ Y0 @ Y1 @ ( a_inv_a_b @ Y0 @ Y2 ) )
@ 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 ) ) ) )
@ ( ^ [Y0: partia1833973666xt_a_b,Y1: a,Y2: a] : ( add_a_b @ Y0 @ Y1 @ ( a_inv_a_b @ Y0 @ Y2 ) )
@ 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(definition_unfolding,[],[f1038,f917,f917,f917,f917]) ).
thf(f1146,plain,
( ( 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 @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ r2 ) @ ( a_inv_a_b @ r @ ( 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 @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ r3 ) @ ( a_inv_a_b @ r @ ( 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 @ ( add_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 ) ) @ ( a_inv_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 @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) ) @ ( add_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 ) ) @ ( a_inv_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 @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f1129]) ).
thf(f1467,plain,
( $true
= ( !! @ a
@ ^ [Y0: a] :
( ( member_a @ Y0 @ s )
=> ( member_a @ Y0 @ ( partia1066395285xt_a_b @ r ) ) ) ) ),
inference(beta-eta_normalization,[],[f1071]) ).
thf(f1468,plain,
! [X1: a] :
( $true
= ( ^ [Y0: a] :
( ( member_a @ Y0 @ s )
=> ( member_a @ Y0 @ ( partia1066395285xt_a_b @ r ) ) )
@ X1 ) ),
inference(pi_proxy_clausification,[],[f1467]) ).
thf(f1469,plain,
! [X1: a] :
( $true
= ( ( member_a @ X1 @ s )
=> ( member_a @ X1 @ ( partia1066395285xt_a_b @ r ) ) ) ),
inference(beta-eta_normalization,[],[f1468]) ).
thf(f1470,plain,
! [X1: a] :
( ( ( member_a @ X1 @ ( partia1066395285xt_a_b @ r ) )
= $true )
| ( ( member_a @ X1 @ s )
= $false ) ),
inference(imp_proxy_clausification,[],[f1469]) ).
thf(f1538,plain,
( ( zero_a_b @ r )
= ( mult_a_ring_ext_a_b @ r @ t @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ r3 ) @ ( a_inv_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s3 @ ( product_fst_a_a @ y ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f1064]) ).
thf(f1539,plain,
( ( zero_a_b @ r )
= ( mult_a_ring_ext_a_b @ r @ t2 @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ r2 ) @ ( a_inv_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ ( product_fst_a_a @ x ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f1063]) ).
thf(f1545,plain,
( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( add_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 ) ) @ ( a_inv_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 @ ( 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 ) @ ( 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 ) ) ) @ ( a_inv_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 @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f1057]) ).
thf(f1546,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 @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ r3 ) @ ( a_inv_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s3 @ ( 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 ) @ ( 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 ) ) ) @ ( a_inv_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 @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f1056]) ).
thf(f1553,plain,
( ( add_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 ) ) ) @ ( a_inv_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 @ 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 ) @ ( add_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 ) ) @ ( a_inv_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 @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f1053]) ).
thf(f1554,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 @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ r2 ) @ ( a_inv_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ ( product_fst_a_a @ x ) ) ) ) ) )
= ( add_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 ) ) ) @ ( a_inv_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 @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f1052]) ).
thf(f1559,plain,
( ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( add_a_b @ r @ ( add_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 ) ) @ ( a_inv_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 @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) ) @ ( add_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 ) ) @ ( a_inv_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 @ ( 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 ) @ ( add_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 ) ) @ ( a_inv_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 @ ( 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 ) @ ( add_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 ) ) @ ( a_inv_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 @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) ) ) )
| ( ( member_a @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( partia1066395285xt_a_b @ r ) )
!= $true )
| ( $true
!= ( member_a @ ( add_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 ) ) @ ( a_inv_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 @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) @ ( partia1066395285xt_a_b @ r ) ) )
| ( $true
!= ( member_a @ ( add_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 ) ) @ ( a_inv_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 @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) ) @ ( partia1066395285xt_a_b @ r ) ) ) ),
inference(beta-eta_normalization,[],[f1047]) ).
thf(f1563,plain,
( $true
= ( member_a @ ( add_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 ) ) @ ( a_inv_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 @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) @ ( partia1066395285xt_a_b @ r ) ) ),
inference(beta-eta_normalization,[],[f1043]) ).
thf(f1564,plain,
( $true
= ( member_a @ ( add_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 ) ) @ ( a_inv_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 @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) ) @ ( partia1066395285xt_a_b @ r ) ) ),
inference(beta-eta_normalization,[],[f1042]) ).
thf(f1566,definition,
( spl39_1
<=> ( $true
= ( member_a @ ( add_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 ) ) @ ( a_inv_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 @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) ) @ ( partia1066395285xt_a_b @ r ) ) ) ),
introduced(definition,[new_symbols(definition,[spl39_1])],[avatar_definition]) ).
thf(f1570,definition,
( spl39_2
<=> ( $true
= ( member_a @ ( add_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 ) ) @ ( a_inv_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 @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) @ ( partia1066395285xt_a_b @ r ) ) ) ),
introduced(definition,[new_symbols(definition,[spl39_2])],[avatar_definition]) ).
thf(f1574,definition,
( spl39_3
<=> ( ( member_a @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( partia1066395285xt_a_b @ r ) )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl39_3])],[avatar_definition]) ).
thf(f1576,plain,
( ( ( member_a @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( partia1066395285xt_a_b @ r ) )
!= $true )
| spl39_3 ),
inference(avatar_component_clause,[],[f1574]) ).
thf(f1578,definition,
( spl39_4
<=> ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( add_a_b @ r @ ( add_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 ) ) @ ( a_inv_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 @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) ) @ ( add_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 ) ) @ ( a_inv_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 @ ( 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 ) @ ( add_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 ) ) @ ( a_inv_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 @ ( 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 ) @ ( add_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 ) ) @ ( a_inv_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 @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl39_4])],[avatar_definition]) ).
thf(f1580,plain,
( ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( add_a_b @ r @ ( add_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 ) ) @ ( a_inv_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 @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) ) @ ( add_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 ) ) @ ( a_inv_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 @ ( 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 ) @ ( add_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 ) ) @ ( a_inv_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 @ ( 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 ) @ ( add_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 ) ) @ ( a_inv_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 @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) ) ) )
| ~ spl39_4 ),
inference(avatar_component_clause,[],[f1578]) ).
thf(f1581,plain,
( ~ spl39_1
| ~ spl39_2
| ~ spl39_3
| spl39_4 ),
inference(avatar_split_clause,[],[f1559,f1578,f1574,f1570,f1566]) ).
thf(f1582,plain,
spl39_2,
inference(avatar_split_clause,[],[f1563,f1570]) ).
thf(f1583,plain,
spl39_1,
inference(avatar_split_clause,[],[f1564,f1566]) ).
thf(f1764,plain,
( ( $true != $true )
| ( ( member_a @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ s )
= $false )
| spl39_3 ),
inference(constrained_superposition,[],[f1576,f1470]) ).
thf(f1765,plain,
( ( ( member_a @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ s )
= $false )
| spl39_3 ),
inference(trivial_inequality_removal,[],[f1764]) ).
thf(f7447,plain,
( ( add_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 ) ) ) @ ( a_inv_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 @ 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(forward_demodulation,[],[f1546,f1538]) ).
thf(f7477,plain,
( ( add_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 ) ) ) @ ( a_inv_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 @ 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(forward_demodulation,[],[f1554,f1539]) ).
thf(f7511,plain,
( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( add_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 ) ) @ ( a_inv_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 @ ( 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(forward_demodulation,[],[f1545,f7447]) ).
thf(f7513,plain,
( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( add_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 ) ) @ ( a_inv_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 @ ( 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(forward_demodulation,[],[f1553,f7477]) ).
thf(f14778,plain,
( ( $true = $false )
| spl39_3 ),
inference(constrained_superposition,[],[f1765,f847]) ).
thf(f14800,plain,
( $false
| spl39_3 ),
inference(trivial_inequality_removal,[],[f14778]) ).
thf(f14801,plain,
spl39_3,
inference(avatar_contradiction_clause,[],[f14800]) ).
thf(f14804,plain,
( ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( add_a_b @ r @ ( add_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 ) ) @ ( a_inv_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 @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) ) @ ( add_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 ) ) @ ( a_inv_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 @ ( 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 @ t2 @ t ) @ ( add_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 ) ) @ ( a_inv_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 @ ( product_snd_a_a @ x ) @ ( product_fst_a_a @ y ) ) ) ) ) ) ) )
| ~ spl39_4 ),
inference(forward_demodulation,[],[f1580,f7513]) ).
thf(f22698,plain,
( ( ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ t2 @ t ) @ ( add_a_b @ r @ ( add_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 ) ) @ ( a_inv_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 @ ( product_snd_a_a @ y ) @ ( product_fst_a_a @ x ) ) ) ) ) @ ( add_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 ) ) @ ( a_inv_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 @ ( 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 ) ) ) )
| ~ spl39_4 ),
inference(forward_demodulation,[],[f14804,f7511]) ).
thf(f22978,plain,
( ( ( 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 @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ x ) @ r2 ) @ ( a_inv_a_b @ r @ ( 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 @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ r3 ) @ ( a_inv_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s3 @ ( 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 ) ) ) )
| ~ spl39_4 ),
inference(constrained_superposition,[],[f1146,f22698]) ).
thf(f22979,plain,
( ( ( 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 ) ) )
!= ( 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 ) ) @ ( mult_a_ring_ext_a_b @ r @ t @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( product_snd_a_a @ y ) @ r3 ) @ ( a_inv_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s3 @ ( product_fst_a_a @ y ) ) ) ) ) ) ) )
| ~ spl39_4 ),
inference(forward_demodulation,[],[f22978,f1539]) ).
thf(f22980,plain,
( ( ( 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 ) ) )
!= ( 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 ) ) ) )
| ~ spl39_4 ),
inference(forward_demodulation,[],[f22979,f1538]) ).
thf(f22981,plain,
( $false
| ~ spl39_4 ),
inference(trivial_inequality_removal,[],[f22980]) ).
thf(f22982,plain,
~ spl39_4,
inference(avatar_contradiction_clause,[],[f22981]) ).
cnf(s1,plain,
( ~ spl39_1
| ~ spl39_2
| ~ spl39_3
| spl39_4 ),
inference(sat_conversion,[],[f1581]) ).
cnf(s2,plain,
spl39_2,
inference(sat_conversion,[],[f1582]) ).
cnf(s3,plain,
spl39_1,
inference(sat_conversion,[],[f1583]) ).
cnf(s251,plain,
spl39_3,
inference(sat_conversion,[],[f14801]) ).
cnf(s641,plain,
~ spl39_4,
inference(sat_conversion,[],[f22982]) ).
cnf(s762,plain,
$false,
inference(rat,[],[s1,s641,s251,s2,s3]) ).
thf(f22983,plain,
$false,
inference(avatar_sat_refutation,[],[s762]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP108^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.18 % Computer : n013.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Tue Sep 29 19:53:51 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.00/0.97 % (2580762)Will run a generic schedule for satisfiability detection.
% 4.00/0.97 % (2580767)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=670816028_2999 on theBenchmark for (2999ds/0Mi)
% 4.00/0.97 % (2580768)% WARNING: option uhcvi not known.
% 4.00/0.97 % (2580769)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3138224465:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.00/0.97 % (2580768)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3354006192:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.00/0.97 % (2580770)dis+10_1_sil=32000:sp=arity:random_seed=496190119:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.00/0.97 % (2580771)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3412901091:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.00/0.97 % (2580772)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3053917507:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.00/0.97 % (2580773)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=255273369:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.00/0.97 % Exception at run slice level
% 4.00/0.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.00/0.97 % (2580768)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.00/0.97 % (2580771)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.00/0.97 % (2580781)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3026469:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.00/0.97 % (2580768)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.00/0.97 % (2580770)Instruction limit reached!
% 4.00/0.97 % (2580770)------------------------------
% 4.00/0.97 % (2580770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.00/0.97 % (2580770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/0.97 % (2580770)CaDiCaL version: 2.1.3
% 4.00/0.97 % (2580770)Termination reason: Instruction limit
% 4.00/0.97 % (2580770)Termination phase: Saturation
% 4.00/0.97 % (2580770)Time elapsed: 0.041 s
% 4.00/0.97 % (2580770)Peak memory usage: 12 MB
% 4.00/0.97 % (2580770)Instructions burned: 104 (million)
% 4.00/0.97 % Exception at run slice level
% 4.00/0.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.00/0.97 % (2580771)Instruction limit reached!
% 4.00/0.97 % (2580771)------------------------------
% 4.00/0.97 % (2580771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.00/0.97 % (2580771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/0.97 % (2580771)CaDiCaL version: 2.1.3
% 4.00/0.97 % (2580771)Termination reason: Instruction limit
% 4.00/0.97 % (2580771)Termination phase: Saturation
% 4.00/0.97 % (2580771)Time elapsed: 0.046 s
% 4.00/0.97 % (2580771)Peak memory usage: 12 MB
% 4.00/0.97 % (2580771)Instructions burned: 116 (million)
% 4.00/0.97 % (2580784)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=31436254:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.00/0.97 % (2580772)Instruction limit reached!
% 4.00/0.97 % (2580772)------------------------------
% 4.00/0.97 % (2580772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.00/0.97 % (2580772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/0.97 % (2580772)CaDiCaL version: 2.1.3
% 4.00/0.97 % (2580772)Termination reason: Instruction limit
% 4.00/0.97 % (2580772)Termination phase: Saturation
% 4.00/0.97 % (2580772)Time elapsed: 0.057 s
% 4.00/0.97 % (2580772)Peak memory usage: 12 MB
% 4.00/0.97 % (2580772)Instructions burned: 140 (million)
% 4.00/0.97 % (2580783)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3024746312:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.00/0.97 % (2580784)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.00/0.97 % (2580785)ott-21_1_sil=16000:fs=off:random_seed=1784588437:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 4.00/0.97 % (2580773)Instruction limit reached!
% 4.00/0.97 % (2580773)------------------------------
% 4.00/0.97 % (2580773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.71/2.55 % (2580773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.71/2.55 % (2580773)CaDiCaL version: 2.1.3
% 15.71/2.55 % (2580773)Termination reason: Instruction limit
% 15.71/2.55 % (2580773)Termination phase: Saturation
% 15.71/2.55 % (2580773)Time elapsed: 0.068 s
% 15.71/2.55 % (2580773)Peak memory usage: 13 MB
% 15.71/2.55 % (2580773)Instructions burned: 159 (million)
% 15.71/2.55 % (2580784)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 15.71/2.55 % (2580787)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3970582697:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 15.71/2.55 % (2580790)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1136293747:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 15.71/2.55 % (2580783)Instruction limit reached!
% 15.71/2.55 % (2580783)------------------------------
% 15.71/2.55 % (2580783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.71/2.55 % (2580783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.71/2.55 % (2580783)CaDiCaL version: 2.1.3
% 15.71/2.55 % (2580783)Termination reason: Instruction limit
% 15.71/2.55 % (2580783)Termination phase: Saturation
% 15.71/2.55 % (2580783)Time elapsed: 0.055 s
% 15.71/2.55 % (2580783)Peak memory usage: 12 MB
% 15.71/2.55 % (2580783)Instructions burned: 132 (million)
% 15.71/2.55 % Exception at run slice level
% 15.71/2.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 15.71/2.55 % (2580793)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=363871261:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 15.71/2.55 % (2580785)Instruction limit reached!
% 15.71/2.55 % (2580785)------------------------------
% 15.71/2.55 % (2580785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.71/2.55 % (2580785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.71/2.55 % (2580785)CaDiCaL version: 2.1.3
% 15.71/2.55 % (2580785)Termination reason: Instruction limit
% 15.71/2.55 % (2580785)Termination phase: Saturation
% 15.71/2.55 % (2580785)Time elapsed: 0.076 s
% 15.71/2.55 % (2580785)Peak memory usage: 12 MB
% 15.71/2.55 % (2580785)Instructions burned: 181 (million)
% 15.71/2.55 % (2580794)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2793076738:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 15.71/2.55 % (2580796)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2376073155:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 15.71/2.55 % (2580796)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 15.71/2.55 % Exception at run slice level
% 15.71/2.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 15.71/2.55 % (2580799)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2229459762:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 15.71/2.55 % (2580784)Instruction limit reached!
% 15.71/2.55 % (2580784)------------------------------
% 15.71/2.55 % (2580784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.71/2.55 % (2580784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.71/2.55 % (2580784)CaDiCaL version: 2.1.3
% 15.71/2.55 % (2580784)Termination reason: Instruction limit
% 15.71/2.55 % (2580784)Termination phase: Saturation
% 15.71/2.55 % (2580784)Time elapsed: 0.166 s
% 15.71/2.55 % (2580784)Peak memory usage: 15 MB
% 15.71/2.55 % (2580784)Instructions burned: 688 (million)
% 15.71/2.55 % (2580799)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 15.71/2.55 % (2580801)fmb+10_1_sil=64000:random_seed=1230879567:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 15.71/2.55 % (2580801)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 15.71/2.55 % Exception at run slice level
% 15.71/2.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 15.71/2.55 % (2580803)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1015286357:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi)
% 15.71/2.55 % Exception at run slice level
% 15.71/2.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 23.39/3.71 % (2580805)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=48952680:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi)
% 23.39/3.71 % (2580787)Instruction limit reached!
% 23.39/3.71 % (2580787)------------------------------
% 23.39/3.71 % (2580787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.39/3.71 % (2580787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.39/3.71 % (2580787)CaDiCaL version: 2.1.3
% 23.39/3.71 % (2580787)Termination reason: Instruction limit
% 23.39/3.71 % (2580787)Termination phase: Saturation
% 23.39/3.71 % (2580787)Time elapsed: 0.231 s
% 23.39/3.71 % (2580787)Peak memory usage: 14 MB
% 23.39/3.71 % (2580787)Instructions burned: 477 (million)
% 23.39/3.71 % Exception at run slice level
% 23.39/3.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 23.39/3.71 % (2580808)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1170310516:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi)
% 23.39/3.71 % (2580807)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1736239169:i=5131_2996 on theBenchmark for (2996ds/5131Mi)
% 23.39/3.71 % (2580808)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 23.39/3.71 % (2580808)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 23.39/3.71 % (2580807)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 23.39/3.71 % (2580796)Instruction limit reached!
% 23.39/3.71 % (2580796)------------------------------
% 23.39/3.71 % (2580796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.39/3.71 % (2580796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.39/3.71 % (2580796)CaDiCaL version: 2.1.3
% 23.39/3.71 % (2580796)Termination reason: Instruction limit
% 23.39/3.71 % (2580796)Termination phase: Saturation
% 23.39/3.71 % (2580796)Time elapsed: 0.269 s
% 23.39/3.71 % (2580796)Peak memory usage: 15 MB
% 23.39/3.71 % (2580796)Instructions burned: 693 (million)
% 23.39/3.71 % (2580811)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1149245100:i=6324_2995 on theBenchmark for (2995ds/6324Mi)
% 23.39/3.71 % Exception at run slice level
% 23.39/3.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 23.39/3.71 % (2580813)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3793221280:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 23.39/3.71 % Exception at run slice level
% 23.39/3.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 23.39/3.71 % (2580815)ott-2_1_sil=16000:newcnf=on:random_seed=3320617219:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 23.39/3.71 % (2580815)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 23.39/3.71 % (2580799)Instruction limit reached!
% 23.39/3.71 % (2580799)------------------------------
% 23.39/3.71 % (2580799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.39/3.71 % (2580799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.39/3.71 % (2580799)CaDiCaL version: 2.1.3
% 23.39/3.71 % (2580799)Termination reason: Instruction limit
% 23.39/3.71 % (2580799)Termination phase: Saturation
% 23.39/3.71 % (2580799)Time elapsed: 0.403 s
% 23.39/3.71 % (2580799)Peak memory usage: 16 MB
% 23.39/3.71 % (2580799)Instructions burned: 881 (million)
% 23.39/3.71 % (2580817)ott+10_1_sil=32000:tgt=ground:random_seed=2112185249:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi)
% 23.39/3.71 % (2580793)Instruction limit reached!
% 23.39/3.71 % (2580793)------------------------------
% 23.39/3.71 % (2580793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.39/3.71 % (2580793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.39/3.71 % (2580793)CaDiCaL version: 2.1.3
% 23.39/3.71 % (2580793)Termination reason: Instruction limit
% 23.39/3.71 % (2580793)Termination phase: Saturation
% 23.39/3.71 % (2580793)Time elapsed: 0.504 s
% 23.39/3.71 % (2580793)Peak memory usage: 16 MB
% 23.39/3.71 % (2580793)Instructions burned: 1180 (million)
% 23.39/3.71 % (2580819)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2692234769:i=54282_2993 on theBenchmark for (2993ds/54282Mi)
% 23.39/3.71 % Exception at run slice level
% 23.39/3.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 23.39/3.71 % (2580808)Instruction limit reached!
% 23.39/3.71 % (2580808)------------------------------
% 23.39/3.71 % (2580808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.39/3.71 % (2580808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.39/3.71 % (2580808)CaDiCaL version: 2.1.3
% 23.39/3.71 % (2580808)Termination reason: Instruction limit
% 23.39/3.71 % (2580808)Termination phase: Saturation
% 23.39/3.71 % (2580808)Time elapsed: 0.380 s
% 23.39/3.71 % (2580808)Peak memory usage: 17 MB
% 23.39/3.71 % (2580808)Instructions burned: 1474 (million)
% 23.39/3.71 % (2580822)dis+21_1_sil=32000:sas=cadical:random_seed=2713611080:i=3773:amm=off_2992 on theBenchmark for (2992ds/3773Mi)
% 23.39/3.71 % (2580821)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2444279686:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi)
% 23.39/3.71 % (2580821)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 23.39/3.71 % (2580815)Instruction limit reached!
% 23.39/3.71 % (2580815)------------------------------
% 23.39/3.71 % (2580815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.39/3.71 % (2580815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.39/3.71 % (2580815)CaDiCaL version: 2.1.3
% 23.39/3.71 % (2580815)Termination reason: Instruction limit
% 23.39/3.71 % (2580815)Termination phase: Saturation
% 23.39/3.71 % (2580815)Time elapsed: 0.391 s
% 23.39/3.71 % (2580815)Peak memory usage: 16 MB
% 23.39/3.71 % (2580815)Instructions burned: 871 (million)
% 23.39/3.71 % (2580825)ott+11_1_sil=16000:gs=on:random_seed=91176314:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2989 on theBenchmark for (2989ds/2251Mi)
% 23.39/3.71 % (2580825)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 23.39/3.71 % (2580822)Instruction limit reached!
% 23.39/3.71 % (2580822)------------------------------
% 23.39/3.71 % (2580822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.39/3.71 % (2580822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.39/3.71 % (2580822)CaDiCaL version: 2.1.3
% 23.39/3.71 % (2580822)Termination reason: Instruction limit
% 23.39/3.71 % (2580822)Termination phase: Saturation
% 23.39/3.71 % (2580822)Time elapsed: 0.886 s
% 23.39/3.71 % (2580822)Peak memory usage: 19 MB
% 23.39/3.71 % (2580822)Instructions burned: 3777 (million)
% 23.39/3.71 % (2580827)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2266322667:fmbsr=1.6:i=67534_2983 on theBenchmark for (2983ds/67534Mi)
% 23.39/3.71 % Exception at run slice level
% 23.39/3.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 23.39/3.71 % (2580829)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3690227402:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2983 on theBenchmark for (2983ds/4591Mi)
% 23.39/3.71 % (2580825)Instruction limit reached!
% 23.39/3.71 % (2580825)------------------------------
% 23.39/3.71 % (2580825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.39/3.71 % (2580825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.39/3.71 % (2580825)CaDiCaL version: 2.1.3
% 23.39/3.71 % (2580825)Termination reason: Instruction limit
% 23.39/3.71 % (2580825)Termination phase: Saturation
% 23.39/3.71 % (2580825)Time elapsed: 0.906 s
% 23.39/3.71 % (2580825)Peak memory usage: 16 MB
% 23.39/3.71 % (2580825)Instructions burned: 2252 (million)
% 23.39/3.71 % (2580832)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=925711032:i=29340_2980 on theBenchmark for (2980ds/29340Mi)
% 23.39/3.71 % (2580821)Instruction limit reached!
% 23.39/3.71 % (2580821)------------------------------
% 23.39/3.71 % (2580821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.39/3.71 % (2580821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.39/3.71 % (2580821)CaDiCaL version: 2.1.3
% 23.39/3.71 % (2580821)Termination reason: Instruction limit
% 23.39/3.71 % (2580821)Termination phase: Saturation
% 23.39/3.71 % (2580821)Time elapsed: 1.539 s
% 23.39/3.71 % (2580821)Peak memory usage: 20 MB
% 23.39/3.71 % (2580821)Instructions burned: 3513 (million)
% 23.39/3.71 % (2580834)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1195924253:i=5211_2976 on theBenchmark for (2976ds/5211Mi)
% 23.39/3.71 % (2580807)Instruction limit reached!
% 23.39/3.71 % (2580807)------------------------------
% 23.39/3.71 % (2580807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.39/3.71 % (2580807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.39/3.71 % (2580807)CaDiCaL version: 2.1.3
% 23.39/3.71 % (2580807)Termination reason: Instruction limit
% 23.39/3.71 % (2580807)Termination phase: Saturation
% 23.39/3.71 % (2580807)Time elapsed: 2.086 s
% 23.39/3.71 % (2580807)Peak memory usage: 20 MB
% 23.39/3.71 % (2580807)Instructions burned: 5133 (million)
% 23.39/3.71 % (2580836)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=556156808:i=5497:nm=2_2975 on theBenchmark for (2975ds/5497Mi)
% 23.39/3.71 % Exception at run slice level
% 23.39/3.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 23.39/3.71 % (2580838)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1951318794:fmbsr=2:i=46332_2974 on theBenchmark for (2974ds/46332Mi)
% 23.39/3.71 % Exception at run slice level
% 23.39/3.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 23.39/3.71 % (2580840)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3440825235:i=14071_2974 on theBenchmark for (2974ds/14071Mi)
% 23.39/3.71 % Exception at run slice level
% 23.39/3.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 23.39/3.71 % (2580842)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3499148085:i=22565:add=on:rawr=on_2973 on theBenchmark for (2973ds/22565Mi)
% 23.39/3.71 % (2580817)Instruction limit reached!
% 23.39/3.71 % (2580817)------------------------------
% 23.39/3.71 % (2580817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.39/3.71 % (2580817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.39/3.71 % (2580817)CaDiCaL version: 2.1.3
% 23.39/3.71 % (2580817)Termination reason: Instruction limit
% 23.39/3.71 % (2580817)Termination phase: Saturation
% 23.39/3.71 % (2580817)Time elapsed: 2.200 s
% 23.39/3.71 % (2580817)Peak memory usage: 27 MB
% 23.39/3.71 % (2580817)Instructions burned: 5116 (million)
% 23.39/3.71 % (2580829)Instruction limit reached!
% 23.39/3.71 % (2580829)------------------------------
% 23.39/3.71 % (2580829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.39/3.71 % (2580829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.39/3.71 % (2580829)CaDiCaL version: 2.1.3
% 23.39/3.71 % (2580829)Termination reason: Instruction limit
% 23.39/3.71 % (2580829)Termination phase: Saturation
% 23.39/3.71 % (2580829)Time elapsed: 1.193 s
% 23.39/3.71 % (2580829)Peak memory usage: 26 MB
% 23.39/3.71 % (2580829)Instructions burned: 4594 (million)
% 23.39/3.71 % (2580845)dis+10_16:1_sil=16000:random_seed=2425755684:i=9155:fsr=off_2971 on theBenchmark for (2971ds/9155Mi)
% 23.39/3.71 % (2580844)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1457057563:i=8173:av=off_2971 on theBenchmark for (2971ds/8173Mi)
% 23.39/3.71 % (2580845) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2580762-2580845"...
% 23.39/3.71 % (2580845)...printing done.
% 23.39/3.71 % (2580845)Refutation found. Thanks to Tanya!
% 23.39/3.71 % SZS status Theorem for theBenchmark
% 23.39/3.71 % SZS output start Proof for theBenchmark
% See solution above
% 23.39/3.71 % (2580845)------------------------------
% 23.39/3.71 % (2580845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.39/3.71 % (2580845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.39/3.71 % (2580845)CaDiCaL version: 2.1.3
% 23.39/3.71 % (2580845)Termination reason: Refutation
% 23.39/3.71 % (2580845)Time elapsed: 0.575 s
% 23.39/3.71 % (2580845)Peak memory usage: 20 MB
% 23.39/3.71 % (2580845)Instructions burned: 2434 (million)
% 23.39/3.71 % (2580762)Success in time 3.482 s
% 23.39/3.71 % Vampire exiting
%------------------------------------------------------------------------------