%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : ALG220+1 : TPTP v9.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 05:24:48 PM UTC 2025
% Result : Theorem 26.00s 11.87s
% Output : CNFRefutation 26.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 6
% Syntax : Number of formulae : 140 ( 46 unt; 0 typ; 0 def)
% Number of atoms : 1520 ( 27 equ)
% Maximal formula atoms : 31 ( 10 avg)
% Number of connectives : 2486 (1106 ~;1257 |; 105 &)
% ( 1 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 33 ( 12 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 35 ( 33 usr; 1 prp; 0-3 aty)
% Number of functors : 37 ( 37 usr; 16 con; 0-5 aty)
% Number of variables : 106 ( 106 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ v1_funct_2 > m2_relset_1 > m1_rmod_2 > m1_relset_1 > v5_vectsp_2 > v3_vectsp_2 > r2_hidden > r1_tarski > m1_subset_1 > l1_vectsp_2 > v8_vectsp_1 > v7_vectsp_1 > v7_group_1 > v6_vectsp_1 > v6_rlvect_1 > v5_rlvect_1 > v4_rlvect_1 > v4_group_1 > v3_struct_0 > v3_rlvect_1 > v2_vectsp_2 > v2_group_1 > v1_xboole_0 > v1_relat_1 > v1_funct_1 > v10_vectsp_1 > l3_vectsp_1 > l2_vectsp_1 > l2_struct_0 > l1_vectsp_1 > l1_struct_0 > l1_rlvect_1 > l1_group_1 > g1_vectsp_2 > k1_rmod_5 > u1_vectsp_2 > k2_zfmisc_1 > #nlpp > u2_struct_0 > u1_struct_0 > u1_rlvect_1 > k1_zfmisc_1 > k1_xboole_0 > #skF_9 > #skF_18 > #skF_11 > #skF_25 > #skF_22 > #skF_7 > #skF_13 > #skF_10 > #skF_14 > #skF_15 > #skF_5 > #skF_19 > #skF_28 > #skF_6 > #skF_2 > #skF_3 > #skF_1 > #skF_21 > #skF_26 > #skF_8 > #skF_4 > #skF_17 > #skF_24 > #skF_23 > #skF_27 > #skF_16 > #skF_12 > #skF_20
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(v2_vectsp_2,type,
v2_vectsp_2: $i > $o ).
tff('#skF_9',type,
'#skF_9': $i > $i ).
tff(v2_group_1,type,
v2_group_1: $i > $o ).
tff(m2_relset_1,type,
m2_relset_1: ( $i * $i * $i ) > $o ).
tff(v1_funct_1,type,
v1_funct_1: $i > $o ).
tff('#skF_18',type,
'#skF_18': $i > $i ).
tff(l3_vectsp_1,type,
l3_vectsp_1: $i > $o ).
tff(r2_hidden,type,
r2_hidden: ( $i * $i ) > $o ).
tff('#skF_11',type,
'#skF_11': $i ).
tff(g1_vectsp_2,type,
g1_vectsp_2: ( $i * $i * $i * $i * $i ) > $i ).
tff(v4_rlvect_1,type,
v4_rlvect_1: $i > $o ).
tff(v8_vectsp_1,type,
v8_vectsp_1: $i > $o ).
tff(u2_struct_0,type,
u2_struct_0: $i > $i ).
tff('#skF_25',type,
'#skF_25': $i ).
tff(k1_xboole_0,type,
k1_xboole_0: $i ).
tff(v5_vectsp_2,type,
v5_vectsp_2: ( $i * $i ) > $o ).
tff('#skF_22',type,
'#skF_22': $i > $i ).
tff(v6_rlvect_1,type,
v6_rlvect_1: $i > $o ).
tff(l1_rlvect_1,type,
l1_rlvect_1: $i > $o ).
tff(v7_group_1,type,
v7_group_1: $i > $o ).
tff('#skF_7',type,
'#skF_7': $i ).
tff(u1_vectsp_2,type,
u1_vectsp_2: ( $i * $i ) > $i ).
tff('#skF_13',type,
'#skF_13': ( $i * $i ) > $i ).
tff(r1_tarski,type,
r1_tarski: ( $i * $i ) > $o ).
tff('#skF_10',type,
'#skF_10': $i ).
tff(v3_vectsp_2,type,
v3_vectsp_2: ( $i * $i ) > $o ).
tff(m1_relset_1,type,
m1_relset_1: ( $i * $i * $i ) > $o ).
tff('#skF_14',type,
'#skF_14': ( $i * $i ) > $i ).
tff('#skF_15',type,
'#skF_15': $i > $i ).
tff(k1_rmod_5,type,
k1_rmod_5: ( $i * $i * $i ) > $i ).
tff('#skF_5',type,
'#skF_5': $i ).
tff(v10_vectsp_1,type,
v10_vectsp_1: $i > $o ).
tff('#skF_19',type,
'#skF_19': ( $i * $i ) > $i ).
tff('#skF_28',type,
'#skF_28': $i > $i ).
tff(v1_funct_2,type,
v1_funct_2: ( $i * $i * $i ) > $o ).
tff('#skF_6',type,
'#skF_6': $i ).
tff('#skF_2',type,
'#skF_2': $i ).
tff('#skF_3',type,
'#skF_3': $i ).
tff('#skF_1',type,
'#skF_1': $i ).
tff(l1_vectsp_2,type,
l1_vectsp_2: ( $i * $i ) > $o ).
tff(m1_rmod_2,type,
m1_rmod_2: ( $i * $i * $i ) > $o ).
tff('#skF_21',type,
'#skF_21': $i ).
tff(l2_struct_0,type,
l2_struct_0: $i > $o ).
tff(l2_vectsp_1,type,
l2_vectsp_1: $i > $o ).
tff(k1_zfmisc_1,type,
k1_zfmisc_1: $i > $i ).
tff(l1_struct_0,type,
l1_struct_0: $i > $o ).
tff('#skF_26',type,
'#skF_26': $i > $i ).
tff('#skF_8',type,
'#skF_8': $i ).
tff(l1_vectsp_1,type,
l1_vectsp_1: $i > $o ).
tff(v1_relat_1,type,
v1_relat_1: $i > $o ).
tff(k2_zfmisc_1,type,
k2_zfmisc_1: ( $i * $i ) > $i ).
tff(v7_vectsp_1,type,
v7_vectsp_1: $i > $o ).
tff('#skF_4',type,
'#skF_4': $i ).
tff('#skF_17',type,
'#skF_17': $i > $i ).
tff('#skF_24',type,
'#skF_24': $i ).
tff('#skF_23',type,
'#skF_23': $i ).
tff(v4_group_1,type,
v4_group_1: $i > $o ).
tff('#skF_27',type,
'#skF_27': $i > $i ).
tff(v5_rlvect_1,type,
v5_rlvect_1: $i > $o ).
tff(u1_struct_0,type,
u1_struct_0: $i > $i ).
tff('#skF_16',type,
'#skF_16': ( $i * $i ) > $i ).
tff(v6_vectsp_1,type,
v6_vectsp_1: $i > $o ).
tff(v1_xboole_0,type,
v1_xboole_0: $i > $o ).
tff(l1_group_1,type,
l1_group_1: $i > $o ).
tff('#skF_12',type,
'#skF_12': $i ).
tff('#skF_20',type,
'#skF_20': $i > $i ).
tff(v3_rlvect_1,type,
v3_rlvect_1: $i > $o ).
tff(u1_rlvect_1,type,
u1_rlvect_1: $i > $i ).
tff(v3_struct_0,type,
v3_struct_0: $i > $o ).
tff(m1_subset_1,type,
m1_subset_1: ( $i * $i ) > $o ).
tff(f_87,negated_conjecture,
~ ! [A] :
( ( ~ v3_struct_0(A)
& v3_rlvect_1(A)
& v4_rlvect_1(A)
& v5_rlvect_1(A)
& v6_rlvect_1(A)
& v4_group_1(A)
& v7_group_1(A)
& v6_vectsp_1(A)
& v7_vectsp_1(A)
& v8_vectsp_1(A)
& ~ v10_vectsp_1(A)
& v2_vectsp_2(A)
& l3_vectsp_1(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& v3_rlvect_1(B)
& v4_rlvect_1(B)
& v5_rlvect_1(B)
& v6_rlvect_1(B)
& v3_vectsp_2(B,A)
& v5_vectsp_2(B,A)
& l1_vectsp_2(B,A) )
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))
=> ( ( ( k1_rmod_5(A,B,C) = B )
& r1_tarski(C,D) )
=> ( k1_rmod_5(A,B,D) = B ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t16_rmod_5) ).
tff(f_209,axiom,
! [A,B,C] :
( ( ~ v3_struct_0(A)
& v3_rlvect_1(A)
& v4_rlvect_1(A)
& v5_rlvect_1(A)
& v6_rlvect_1(A)
& v4_group_1(A)
& v7_group_1(A)
& v6_vectsp_1(A)
& v7_vectsp_1(A)
& v8_vectsp_1(A)
& ~ v10_vectsp_1(A)
& v2_vectsp_2(A)
& l3_vectsp_1(A)
& ~ v3_struct_0(B)
& v3_rlvect_1(B)
& v4_rlvect_1(B)
& v5_rlvect_1(B)
& v6_rlvect_1(B)
& v5_vectsp_2(B,A)
& l1_vectsp_2(B,A)
& m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) )
=> ( v3_vectsp_2(k1_rmod_5(A,B,C),A)
& m1_rmod_2(k1_rmod_5(A,B,C),A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_rmod_5) ).
tff(f_299,axiom,
! [A,B] :
( ( ~ v3_struct_0(A)
& v3_rlvect_1(A)
& v4_rlvect_1(A)
& v5_rlvect_1(A)
& v6_rlvect_1(A)
& v4_group_1(A)
& v6_vectsp_1(A)
& v7_vectsp_1(A)
& v8_vectsp_1(A)
& l3_vectsp_1(A)
& ~ v3_struct_0(B)
& v3_rlvect_1(B)
& v4_rlvect_1(B)
& v5_rlvect_1(B)
& v6_rlvect_1(B)
& v5_vectsp_2(B,A)
& l1_vectsp_2(B,A) )
=> ! [C] :
( m1_rmod_2(C,A,B)
=> ( ~ v3_struct_0(C)
& v3_rlvect_1(C)
& v4_rlvect_1(C)
& v5_rlvect_1(C)
& v6_rlvect_1(C)
& v5_vectsp_2(C,A)
& l1_vectsp_2(C,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_rmod_2) ).
tff(f_788,axiom,
! [A,B] :
( m1_subset_1(A,k1_zfmisc_1(B))
<=> r1_tarski(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_subset) ).
tff(f_711,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v3_rlvect_1(A)
& v4_rlvect_1(A)
& v5_rlvect_1(A)
& v6_rlvect_1(A)
& v4_group_1(A)
& v7_group_1(A)
& v6_vectsp_1(A)
& v7_vectsp_1(A)
& v8_vectsp_1(A)
& ~ v10_vectsp_1(A)
& v2_vectsp_2(A)
& l3_vectsp_1(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& v3_rlvect_1(B)
& v4_rlvect_1(B)
& v5_rlvect_1(B)
& v6_rlvect_1(B)
& v5_vectsp_2(B,A)
& l1_vectsp_2(B,A) )
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))
=> ( r1_tarski(C,D)
=> m1_rmod_2(k1_rmod_5(A,B,C),A,k1_rmod_5(A,B,D)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t15_rmod_5) ).
tff(f_784,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v3_rlvect_1(A)
& v4_rlvect_1(A)
& v5_rlvect_1(A)
& v6_rlvect_1(A)
& v4_group_1(A)
& v6_vectsp_1(A)
& v7_vectsp_1(A)
& v8_vectsp_1(A)
& l3_vectsp_1(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& v3_rlvect_1(B)
& v4_rlvect_1(B)
& v5_rlvect_1(B)
& v6_rlvect_1(B)
& v3_vectsp_2(B,A)
& v5_vectsp_2(B,A)
& l1_vectsp_2(B,A) )
=> ! [C] :
( ( ~ v3_struct_0(C)
& v3_rlvect_1(C)
& v4_rlvect_1(C)
& v5_rlvect_1(C)
& v6_rlvect_1(C)
& v3_vectsp_2(C,A)
& v5_vectsp_2(C,A)
& l1_vectsp_2(C,A) )
=> ( ( m1_rmod_2(C,A,B)
& m1_rmod_2(B,A,C) )
=> ( C = B ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t33_rmod_2) ).
tff(c_52,plain,
~ v3_struct_0('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_32,plain,
~ v10_vectsp_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_50,plain,
v3_rlvect_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_48,plain,
v4_rlvect_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_46,plain,
v5_rlvect_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_44,plain,
v6_rlvect_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_42,plain,
v4_group_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_40,plain,
v7_group_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_38,plain,
v6_vectsp_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_36,plain,
v7_vectsp_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_34,plain,
v8_vectsp_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_30,plain,
v2_vectsp_2('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_28,plain,
l3_vectsp_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_14,plain,
v5_vectsp_2('#skF_2','#skF_1'),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_12,plain,
l1_vectsp_2('#skF_2','#skF_1'),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_26,plain,
~ v3_struct_0('#skF_2'),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_24,plain,
v3_rlvect_1('#skF_2'),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_22,plain,
v4_rlvect_1('#skF_2'),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_20,plain,
v5_rlvect_1('#skF_2'),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_18,plain,
v6_rlvect_1('#skF_2'),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_8,plain,
m1_subset_1('#skF_4',k1_zfmisc_1(u1_struct_0('#skF_2'))),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_34180,plain,
! [A_1495,B_1496,C_1497] :
( m1_rmod_2(k1_rmod_5(A_1495,B_1496,C_1497),A_1495,B_1496)
| ~ m1_subset_1(C_1497,k1_zfmisc_1(u1_struct_0(B_1496)))
| ~ l1_vectsp_2(B_1496,A_1495)
| ~ v5_vectsp_2(B_1496,A_1495)
| ~ v6_rlvect_1(B_1496)
| ~ v5_rlvect_1(B_1496)
| ~ v4_rlvect_1(B_1496)
| ~ v3_rlvect_1(B_1496)
| v3_struct_0(B_1496)
| ~ l3_vectsp_1(A_1495)
| ~ v2_vectsp_2(A_1495)
| v10_vectsp_1(A_1495)
| ~ v8_vectsp_1(A_1495)
| ~ v7_vectsp_1(A_1495)
| ~ v6_vectsp_1(A_1495)
| ~ v7_group_1(A_1495)
| ~ v4_group_1(A_1495)
| ~ v6_rlvect_1(A_1495)
| ~ v5_rlvect_1(A_1495)
| ~ v4_rlvect_1(A_1495)
| ~ v3_rlvect_1(A_1495)
| v3_struct_0(A_1495) ),
inference(cnfTransformation,[status(thm)],[f_209]) ).
tff(c_34237,plain,
! [A_1495] :
( m1_rmod_2(k1_rmod_5(A_1495,'#skF_2','#skF_4'),A_1495,'#skF_2')
| ~ l1_vectsp_2('#skF_2',A_1495)
| ~ v5_vectsp_2('#skF_2',A_1495)
| ~ v6_rlvect_1('#skF_2')
| ~ v5_rlvect_1('#skF_2')
| ~ v4_rlvect_1('#skF_2')
| ~ v3_rlvect_1('#skF_2')
| v3_struct_0('#skF_2')
| ~ l3_vectsp_1(A_1495)
| ~ v2_vectsp_2(A_1495)
| v10_vectsp_1(A_1495)
| ~ v8_vectsp_1(A_1495)
| ~ v7_vectsp_1(A_1495)
| ~ v6_vectsp_1(A_1495)
| ~ v7_group_1(A_1495)
| ~ v4_group_1(A_1495)
| ~ v6_rlvect_1(A_1495)
| ~ v5_rlvect_1(A_1495)
| ~ v4_rlvect_1(A_1495)
| ~ v3_rlvect_1(A_1495)
| v3_struct_0(A_1495) ),
inference(resolution,[status(thm)],[c_8,c_34180]) ).
tff(c_34268,plain,
! [A_1495] :
( m1_rmod_2(k1_rmod_5(A_1495,'#skF_2','#skF_4'),A_1495,'#skF_2')
| ~ l1_vectsp_2('#skF_2',A_1495)
| ~ v5_vectsp_2('#skF_2',A_1495)
| v3_struct_0('#skF_2')
| ~ l3_vectsp_1(A_1495)
| ~ v2_vectsp_2(A_1495)
| v10_vectsp_1(A_1495)
| ~ v8_vectsp_1(A_1495)
| ~ v7_vectsp_1(A_1495)
| ~ v6_vectsp_1(A_1495)
| ~ v7_group_1(A_1495)
| ~ v4_group_1(A_1495)
| ~ v6_rlvect_1(A_1495)
| ~ v5_rlvect_1(A_1495)
| ~ v4_rlvect_1(A_1495)
| ~ v3_rlvect_1(A_1495)
| v3_struct_0(A_1495) ),
inference(demodulation,[status(thm),theory(equality)],[c_24,c_22,c_20,c_18,c_34237]) ).
tff(c_35809,plain,
! [A_1533] :
( m1_rmod_2(k1_rmod_5(A_1533,'#skF_2','#skF_4'),A_1533,'#skF_2')
| ~ l1_vectsp_2('#skF_2',A_1533)
| ~ v5_vectsp_2('#skF_2',A_1533)
| ~ l3_vectsp_1(A_1533)
| ~ v2_vectsp_2(A_1533)
| v10_vectsp_1(A_1533)
| ~ v8_vectsp_1(A_1533)
| ~ v7_vectsp_1(A_1533)
| ~ v6_vectsp_1(A_1533)
| ~ v7_group_1(A_1533)
| ~ v4_group_1(A_1533)
| ~ v6_rlvect_1(A_1533)
| ~ v5_rlvect_1(A_1533)
| ~ v4_rlvect_1(A_1533)
| ~ v3_rlvect_1(A_1533)
| v3_struct_0(A_1533) ),
inference(negUnitSimplification,[status(thm)],[c_26,c_34268]) ).
tff(c_112,plain,
! [C_41,A_38,B_39] :
( l1_vectsp_2(C_41,A_38)
| ~ m1_rmod_2(C_41,A_38,B_39)
| ~ l1_vectsp_2(B_39,A_38)
| ~ v5_vectsp_2(B_39,A_38)
| ~ v6_rlvect_1(B_39)
| ~ v5_rlvect_1(B_39)
| ~ v4_rlvect_1(B_39)
| ~ v3_rlvect_1(B_39)
| v3_struct_0(B_39)
| ~ l3_vectsp_1(A_38)
| ~ v8_vectsp_1(A_38)
| ~ v7_vectsp_1(A_38)
| ~ v6_vectsp_1(A_38)
| ~ v4_group_1(A_38)
| ~ v6_rlvect_1(A_38)
| ~ v5_rlvect_1(A_38)
| ~ v4_rlvect_1(A_38)
| ~ v3_rlvect_1(A_38)
| v3_struct_0(A_38) ),
inference(cnfTransformation,[status(thm)],[f_299]) ).
tff(c_35814,plain,
! [A_1533] :
( l1_vectsp_2(k1_rmod_5(A_1533,'#skF_2','#skF_4'),A_1533)
| ~ v6_rlvect_1('#skF_2')
| ~ v5_rlvect_1('#skF_2')
| ~ v4_rlvect_1('#skF_2')
| ~ v3_rlvect_1('#skF_2')
| v3_struct_0('#skF_2')
| ~ l1_vectsp_2('#skF_2',A_1533)
| ~ v5_vectsp_2('#skF_2',A_1533)
| ~ l3_vectsp_1(A_1533)
| ~ v2_vectsp_2(A_1533)
| v10_vectsp_1(A_1533)
| ~ v8_vectsp_1(A_1533)
| ~ v7_vectsp_1(A_1533)
| ~ v6_vectsp_1(A_1533)
| ~ v7_group_1(A_1533)
| ~ v4_group_1(A_1533)
| ~ v6_rlvect_1(A_1533)
| ~ v5_rlvect_1(A_1533)
| ~ v4_rlvect_1(A_1533)
| ~ v3_rlvect_1(A_1533)
| v3_struct_0(A_1533) ),
inference(resolution,[status(thm)],[c_35809,c_112]) ).
tff(c_35839,plain,
! [A_1533] :
( l1_vectsp_2(k1_rmod_5(A_1533,'#skF_2','#skF_4'),A_1533)
| v3_struct_0('#skF_2')
| ~ l1_vectsp_2('#skF_2',A_1533)
| ~ v5_vectsp_2('#skF_2',A_1533)
| ~ l3_vectsp_1(A_1533)
| ~ v2_vectsp_2(A_1533)
| v10_vectsp_1(A_1533)
| ~ v8_vectsp_1(A_1533)
| ~ v7_vectsp_1(A_1533)
| ~ v6_vectsp_1(A_1533)
| ~ v7_group_1(A_1533)
| ~ v4_group_1(A_1533)
| ~ v6_rlvect_1(A_1533)
| ~ v5_rlvect_1(A_1533)
| ~ v4_rlvect_1(A_1533)
| ~ v3_rlvect_1(A_1533)
| v3_struct_0(A_1533) ),
inference(demodulation,[status(thm),theory(equality)],[c_24,c_22,c_20,c_18,c_35814]) ).
tff(c_35840,plain,
! [A_1533] :
( l1_vectsp_2(k1_rmod_5(A_1533,'#skF_2','#skF_4'),A_1533)
| ~ l1_vectsp_2('#skF_2',A_1533)
| ~ v5_vectsp_2('#skF_2',A_1533)
| ~ l3_vectsp_1(A_1533)
| ~ v2_vectsp_2(A_1533)
| v10_vectsp_1(A_1533)
| ~ v8_vectsp_1(A_1533)
| ~ v7_vectsp_1(A_1533)
| ~ v6_vectsp_1(A_1533)
| ~ v7_group_1(A_1533)
| ~ v4_group_1(A_1533)
| ~ v6_rlvect_1(A_1533)
| ~ v5_rlvect_1(A_1533)
| ~ v4_rlvect_1(A_1533)
| ~ v3_rlvect_1(A_1533)
| v3_struct_0(A_1533) ),
inference(negUnitSimplification,[status(thm)],[c_26,c_35839]) ).
tff(c_475,plain,
! [A_193,B_194] :
( r1_tarski(A_193,B_194)
| ~ m1_subset_1(A_193,k1_zfmisc_1(B_194)) ),
inference(cnfTransformation,[status(thm)],[f_788]) ).
tff(c_496,plain,
r1_tarski('#skF_4',u1_struct_0('#skF_2')),
inference(resolution,[status(thm)],[c_8,c_475]) ).
tff(c_286,plain,
! [A_134,B_135] :
( m1_subset_1(A_134,k1_zfmisc_1(B_135))
| ~ r1_tarski(A_134,B_135) ),
inference(cnfTransformation,[status(thm)],[f_788]) ).
tff(c_33592,plain,
! [A_1486,B_1487,C_1488] :
( v3_vectsp_2(k1_rmod_5(A_1486,B_1487,C_1488),A_1486)
| ~ m1_subset_1(C_1488,k1_zfmisc_1(u1_struct_0(B_1487)))
| ~ l1_vectsp_2(B_1487,A_1486)
| ~ v5_vectsp_2(B_1487,A_1486)
| ~ v6_rlvect_1(B_1487)
| ~ v5_rlvect_1(B_1487)
| ~ v4_rlvect_1(B_1487)
| ~ v3_rlvect_1(B_1487)
| v3_struct_0(B_1487)
| ~ l3_vectsp_1(A_1486)
| ~ v2_vectsp_2(A_1486)
| v10_vectsp_1(A_1486)
| ~ v8_vectsp_1(A_1486)
| ~ v7_vectsp_1(A_1486)
| ~ v6_vectsp_1(A_1486)
| ~ v7_group_1(A_1486)
| ~ v4_group_1(A_1486)
| ~ v6_rlvect_1(A_1486)
| ~ v5_rlvect_1(A_1486)
| ~ v4_rlvect_1(A_1486)
| ~ v3_rlvect_1(A_1486)
| v3_struct_0(A_1486) ),
inference(cnfTransformation,[status(thm)],[f_209]) ).
tff(c_33671,plain,
! [A_1486,B_1487,A_134] :
( v3_vectsp_2(k1_rmod_5(A_1486,B_1487,A_134),A_1486)
| ~ l1_vectsp_2(B_1487,A_1486)
| ~ v5_vectsp_2(B_1487,A_1486)
| ~ v6_rlvect_1(B_1487)
| ~ v5_rlvect_1(B_1487)
| ~ v4_rlvect_1(B_1487)
| ~ v3_rlvect_1(B_1487)
| v3_struct_0(B_1487)
| ~ l3_vectsp_1(A_1486)
| ~ v2_vectsp_2(A_1486)
| v10_vectsp_1(A_1486)
| ~ v8_vectsp_1(A_1486)
| ~ v7_vectsp_1(A_1486)
| ~ v6_vectsp_1(A_1486)
| ~ v7_group_1(A_1486)
| ~ v4_group_1(A_1486)
| ~ v6_rlvect_1(A_1486)
| ~ v5_rlvect_1(A_1486)
| ~ v4_rlvect_1(A_1486)
| ~ v3_rlvect_1(A_1486)
| v3_struct_0(A_1486)
| ~ r1_tarski(A_134,u1_struct_0(B_1487)) ),
inference(resolution,[status(thm)],[c_286,c_33592]) ).
tff(c_2,plain,
k1_rmod_5('#skF_1','#skF_2','#skF_4') != '#skF_2',
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_4,plain,
r1_tarski('#skF_3','#skF_4'),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_122,plain,
! [C_41,A_38,B_39] :
( v3_rlvect_1(C_41)
| ~ m1_rmod_2(C_41,A_38,B_39)
| ~ l1_vectsp_2(B_39,A_38)
| ~ v5_vectsp_2(B_39,A_38)
| ~ v6_rlvect_1(B_39)
| ~ v5_rlvect_1(B_39)
| ~ v4_rlvect_1(B_39)
| ~ v3_rlvect_1(B_39)
| v3_struct_0(B_39)
| ~ l3_vectsp_1(A_38)
| ~ v8_vectsp_1(A_38)
| ~ v7_vectsp_1(A_38)
| ~ v6_vectsp_1(A_38)
| ~ v4_group_1(A_38)
| ~ v6_rlvect_1(A_38)
| ~ v5_rlvect_1(A_38)
| ~ v4_rlvect_1(A_38)
| ~ v3_rlvect_1(A_38)
| v3_struct_0(A_38) ),
inference(cnfTransformation,[status(thm)],[f_299]) ).
tff(c_35820,plain,
! [A_1533] :
( v3_rlvect_1(k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| ~ v6_rlvect_1('#skF_2')
| ~ v5_rlvect_1('#skF_2')
| ~ v4_rlvect_1('#skF_2')
| ~ v3_rlvect_1('#skF_2')
| v3_struct_0('#skF_2')
| ~ l1_vectsp_2('#skF_2',A_1533)
| ~ v5_vectsp_2('#skF_2',A_1533)
| ~ l3_vectsp_1(A_1533)
| ~ v2_vectsp_2(A_1533)
| v10_vectsp_1(A_1533)
| ~ v8_vectsp_1(A_1533)
| ~ v7_vectsp_1(A_1533)
| ~ v6_vectsp_1(A_1533)
| ~ v7_group_1(A_1533)
| ~ v4_group_1(A_1533)
| ~ v6_rlvect_1(A_1533)
| ~ v5_rlvect_1(A_1533)
| ~ v4_rlvect_1(A_1533)
| ~ v3_rlvect_1(A_1533)
| v3_struct_0(A_1533) ),
inference(resolution,[status(thm)],[c_35809,c_122]) ).
tff(c_35847,plain,
! [A_1533] :
( v3_rlvect_1(k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| v3_struct_0('#skF_2')
| ~ l1_vectsp_2('#skF_2',A_1533)
| ~ v5_vectsp_2('#skF_2',A_1533)
| ~ l3_vectsp_1(A_1533)
| ~ v2_vectsp_2(A_1533)
| v10_vectsp_1(A_1533)
| ~ v8_vectsp_1(A_1533)
| ~ v7_vectsp_1(A_1533)
| ~ v6_vectsp_1(A_1533)
| ~ v7_group_1(A_1533)
| ~ v4_group_1(A_1533)
| ~ v6_rlvect_1(A_1533)
| ~ v5_rlvect_1(A_1533)
| ~ v4_rlvect_1(A_1533)
| ~ v3_rlvect_1(A_1533)
| v3_struct_0(A_1533) ),
inference(demodulation,[status(thm),theory(equality)],[c_24,c_22,c_20,c_18,c_35820]) ).
tff(c_35848,plain,
! [A_1533] :
( v3_rlvect_1(k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| ~ l1_vectsp_2('#skF_2',A_1533)
| ~ v5_vectsp_2('#skF_2',A_1533)
| ~ l3_vectsp_1(A_1533)
| ~ v2_vectsp_2(A_1533)
| v10_vectsp_1(A_1533)
| ~ v8_vectsp_1(A_1533)
| ~ v7_vectsp_1(A_1533)
| ~ v6_vectsp_1(A_1533)
| ~ v7_group_1(A_1533)
| ~ v4_group_1(A_1533)
| ~ v6_rlvect_1(A_1533)
| ~ v5_rlvect_1(A_1533)
| ~ v4_rlvect_1(A_1533)
| ~ v3_rlvect_1(A_1533)
| v3_struct_0(A_1533) ),
inference(negUnitSimplification,[status(thm)],[c_26,c_35847]) ).
tff(c_16,plain,
v3_vectsp_2('#skF_2','#skF_1'),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_10,plain,
m1_subset_1('#skF_3',k1_zfmisc_1(u1_struct_0('#skF_2'))),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_6,plain,
k1_rmod_5('#skF_1','#skF_2','#skF_3') = '#skF_2',
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_34585,plain,
! [A_1512,B_1513,C_1514,D_1515] :
( m1_rmod_2(k1_rmod_5(A_1512,B_1513,C_1514),A_1512,k1_rmod_5(A_1512,B_1513,D_1515))
| ~ r1_tarski(C_1514,D_1515)
| ~ m1_subset_1(D_1515,k1_zfmisc_1(u1_struct_0(B_1513)))
| ~ m1_subset_1(C_1514,k1_zfmisc_1(u1_struct_0(B_1513)))
| ~ l1_vectsp_2(B_1513,A_1512)
| ~ v5_vectsp_2(B_1513,A_1512)
| ~ v6_rlvect_1(B_1513)
| ~ v5_rlvect_1(B_1513)
| ~ v4_rlvect_1(B_1513)
| ~ v3_rlvect_1(B_1513)
| v3_struct_0(B_1513)
| ~ l3_vectsp_1(A_1512)
| ~ v2_vectsp_2(A_1512)
| v10_vectsp_1(A_1512)
| ~ v8_vectsp_1(A_1512)
| ~ v7_vectsp_1(A_1512)
| ~ v6_vectsp_1(A_1512)
| ~ v7_group_1(A_1512)
| ~ v4_group_1(A_1512)
| ~ v6_rlvect_1(A_1512)
| ~ v5_rlvect_1(A_1512)
| ~ v4_rlvect_1(A_1512)
| ~ v3_rlvect_1(A_1512)
| v3_struct_0(A_1512) ),
inference(cnfTransformation,[status(thm)],[f_711]) ).
tff(c_34609,plain,
! [D_1515] :
( m1_rmod_2('#skF_2','#skF_1',k1_rmod_5('#skF_1','#skF_2',D_1515))
| ~ r1_tarski('#skF_3',D_1515)
| ~ m1_subset_1(D_1515,k1_zfmisc_1(u1_struct_0('#skF_2')))
| ~ m1_subset_1('#skF_3',k1_zfmisc_1(u1_struct_0('#skF_2')))
| ~ l1_vectsp_2('#skF_2','#skF_1')
| ~ v5_vectsp_2('#skF_2','#skF_1')
| ~ v6_rlvect_1('#skF_2')
| ~ v5_rlvect_1('#skF_2')
| ~ v4_rlvect_1('#skF_2')
| ~ v3_rlvect_1('#skF_2')
| v3_struct_0('#skF_2')
| ~ l3_vectsp_1('#skF_1')
| ~ v2_vectsp_2('#skF_1')
| v10_vectsp_1('#skF_1')
| ~ v8_vectsp_1('#skF_1')
| ~ v7_vectsp_1('#skF_1')
| ~ v6_vectsp_1('#skF_1')
| ~ v7_group_1('#skF_1')
| ~ v4_group_1('#skF_1')
| ~ v6_rlvect_1('#skF_1')
| ~ v5_rlvect_1('#skF_1')
| ~ v4_rlvect_1('#skF_1')
| ~ v3_rlvect_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_34585]) ).
tff(c_34621,plain,
! [D_1515] :
( m1_rmod_2('#skF_2','#skF_1',k1_rmod_5('#skF_1','#skF_2',D_1515))
| ~ r1_tarski('#skF_3',D_1515)
| ~ m1_subset_1(D_1515,k1_zfmisc_1(u1_struct_0('#skF_2')))
| v3_struct_0('#skF_2')
| v10_vectsp_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_48,c_46,c_44,c_42,c_40,c_38,c_36,c_34,c_30,c_28,c_24,c_22,c_20,c_18,c_14,c_12,c_10,c_34609]) ).
tff(c_34626,plain,
! [D_1516] :
( m1_rmod_2('#skF_2','#skF_1',k1_rmod_5('#skF_1','#skF_2',D_1516))
| ~ r1_tarski('#skF_3',D_1516)
| ~ m1_subset_1(D_1516,k1_zfmisc_1(u1_struct_0('#skF_2'))) ),
inference(negUnitSimplification,[status(thm)],[c_52,c_32,c_26,c_34621]) ).
tff(c_34704,plain,
( m1_rmod_2('#skF_2','#skF_1',k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ r1_tarski('#skF_3','#skF_4') ),
inference(resolution,[status(thm)],[c_8,c_34626]) ).
tff(c_34738,plain,
m1_rmod_2('#skF_2','#skF_1',k1_rmod_5('#skF_1','#skF_2','#skF_4')),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_34704]) ).
tff(c_34852,plain,
! [C_1517,B_1518,A_1519] :
( ( C_1517 = B_1518 )
| ~ m1_rmod_2(B_1518,A_1519,C_1517)
| ~ m1_rmod_2(C_1517,A_1519,B_1518)
| ~ l1_vectsp_2(C_1517,A_1519)
| ~ v5_vectsp_2(C_1517,A_1519)
| ~ v3_vectsp_2(C_1517,A_1519)
| ~ v6_rlvect_1(C_1517)
| ~ v5_rlvect_1(C_1517)
| ~ v4_rlvect_1(C_1517)
| ~ v3_rlvect_1(C_1517)
| v3_struct_0(C_1517)
| ~ l1_vectsp_2(B_1518,A_1519)
| ~ v5_vectsp_2(B_1518,A_1519)
| ~ v3_vectsp_2(B_1518,A_1519)
| ~ v6_rlvect_1(B_1518)
| ~ v5_rlvect_1(B_1518)
| ~ v4_rlvect_1(B_1518)
| ~ v3_rlvect_1(B_1518)
| v3_struct_0(B_1518)
| ~ l3_vectsp_1(A_1519)
| ~ v8_vectsp_1(A_1519)
| ~ v7_vectsp_1(A_1519)
| ~ v6_vectsp_1(A_1519)
| ~ v4_group_1(A_1519)
| ~ v6_rlvect_1(A_1519)
| ~ v5_rlvect_1(A_1519)
| ~ v4_rlvect_1(A_1519)
| ~ v3_rlvect_1(A_1519)
| v3_struct_0(A_1519) ),
inference(cnfTransformation,[status(thm)],[f_784]) ).
tff(c_34854,plain,
( ( k1_rmod_5('#skF_1','#skF_2','#skF_4') = '#skF_2' )
| ~ m1_rmod_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1','#skF_2')
| ~ l1_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v5_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v3_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v6_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v5_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v4_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v3_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| v3_struct_0(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ l1_vectsp_2('#skF_2','#skF_1')
| ~ v5_vectsp_2('#skF_2','#skF_1')
| ~ v3_vectsp_2('#skF_2','#skF_1')
| ~ v6_rlvect_1('#skF_2')
| ~ v5_rlvect_1('#skF_2')
| ~ v4_rlvect_1('#skF_2')
| ~ v3_rlvect_1('#skF_2')
| v3_struct_0('#skF_2')
| ~ l3_vectsp_1('#skF_1')
| ~ v8_vectsp_1('#skF_1')
| ~ v7_vectsp_1('#skF_1')
| ~ v6_vectsp_1('#skF_1')
| ~ v4_group_1('#skF_1')
| ~ v6_rlvect_1('#skF_1')
| ~ v5_rlvect_1('#skF_1')
| ~ v4_rlvect_1('#skF_1')
| ~ v3_rlvect_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_34738,c_34852]) ).
tff(c_34865,plain,
( ( k1_rmod_5('#skF_1','#skF_2','#skF_4') = '#skF_2' )
| ~ m1_rmod_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1','#skF_2')
| ~ l1_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v5_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v3_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v6_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v5_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v4_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v3_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| v3_struct_0(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| v3_struct_0('#skF_2')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_48,c_46,c_44,c_42,c_38,c_36,c_34,c_28,c_24,c_22,c_20,c_18,c_16,c_14,c_12,c_34854]) ).
tff(c_34866,plain,
( ~ m1_rmod_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1','#skF_2')
| ~ l1_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v5_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v3_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v6_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v5_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v4_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v3_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| v3_struct_0(k1_rmod_5('#skF_1','#skF_2','#skF_4')) ),
inference(negUnitSimplification,[status(thm)],[c_52,c_26,c_2,c_34865]) ).
tff(c_48786,plain,
~ v3_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4')),
inference(splitLeft,[status(thm)],[c_34866]) ).
tff(c_48789,plain,
( ~ l1_vectsp_2('#skF_2','#skF_1')
| ~ v5_vectsp_2('#skF_2','#skF_1')
| ~ l3_vectsp_1('#skF_1')
| ~ v2_vectsp_2('#skF_1')
| v10_vectsp_1('#skF_1')
| ~ v8_vectsp_1('#skF_1')
| ~ v7_vectsp_1('#skF_1')
| ~ v6_vectsp_1('#skF_1')
| ~ v7_group_1('#skF_1')
| ~ v4_group_1('#skF_1')
| ~ v6_rlvect_1('#skF_1')
| ~ v5_rlvect_1('#skF_1')
| ~ v4_rlvect_1('#skF_1')
| ~ v3_rlvect_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_35848,c_48786]) ).
tff(c_48792,plain,
( v10_vectsp_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_48,c_46,c_44,c_42,c_40,c_38,c_36,c_34,c_30,c_28,c_14,c_12,c_48789]) ).
tff(c_48794,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_52,c_32,c_48792]) ).
tff(c_48796,plain,
v3_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4')),
inference(splitRight,[status(thm)],[c_34866]) ).
tff(c_120,plain,
! [C_41,A_38,B_39] :
( v4_rlvect_1(C_41)
| ~ m1_rmod_2(C_41,A_38,B_39)
| ~ l1_vectsp_2(B_39,A_38)
| ~ v5_vectsp_2(B_39,A_38)
| ~ v6_rlvect_1(B_39)
| ~ v5_rlvect_1(B_39)
| ~ v4_rlvect_1(B_39)
| ~ v3_rlvect_1(B_39)
| v3_struct_0(B_39)
| ~ l3_vectsp_1(A_38)
| ~ v8_vectsp_1(A_38)
| ~ v7_vectsp_1(A_38)
| ~ v6_vectsp_1(A_38)
| ~ v4_group_1(A_38)
| ~ v6_rlvect_1(A_38)
| ~ v5_rlvect_1(A_38)
| ~ v4_rlvect_1(A_38)
| ~ v3_rlvect_1(A_38)
| v3_struct_0(A_38) ),
inference(cnfTransformation,[status(thm)],[f_299]) ).
tff(c_35832,plain,
! [A_1533] :
( v4_rlvect_1(k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| ~ v6_rlvect_1('#skF_2')
| ~ v5_rlvect_1('#skF_2')
| ~ v4_rlvect_1('#skF_2')
| ~ v3_rlvect_1('#skF_2')
| v3_struct_0('#skF_2')
| ~ l1_vectsp_2('#skF_2',A_1533)
| ~ v5_vectsp_2('#skF_2',A_1533)
| ~ l3_vectsp_1(A_1533)
| ~ v2_vectsp_2(A_1533)
| v10_vectsp_1(A_1533)
| ~ v8_vectsp_1(A_1533)
| ~ v7_vectsp_1(A_1533)
| ~ v6_vectsp_1(A_1533)
| ~ v7_group_1(A_1533)
| ~ v4_group_1(A_1533)
| ~ v6_rlvect_1(A_1533)
| ~ v5_rlvect_1(A_1533)
| ~ v4_rlvect_1(A_1533)
| ~ v3_rlvect_1(A_1533)
| v3_struct_0(A_1533) ),
inference(resolution,[status(thm)],[c_35809,c_120]) ).
tff(c_35863,plain,
! [A_1533] :
( v4_rlvect_1(k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| v3_struct_0('#skF_2')
| ~ l1_vectsp_2('#skF_2',A_1533)
| ~ v5_vectsp_2('#skF_2',A_1533)
| ~ l3_vectsp_1(A_1533)
| ~ v2_vectsp_2(A_1533)
| v10_vectsp_1(A_1533)
| ~ v8_vectsp_1(A_1533)
| ~ v7_vectsp_1(A_1533)
| ~ v6_vectsp_1(A_1533)
| ~ v7_group_1(A_1533)
| ~ v4_group_1(A_1533)
| ~ v6_rlvect_1(A_1533)
| ~ v5_rlvect_1(A_1533)
| ~ v4_rlvect_1(A_1533)
| ~ v3_rlvect_1(A_1533)
| v3_struct_0(A_1533) ),
inference(demodulation,[status(thm),theory(equality)],[c_24,c_22,c_20,c_18,c_35832]) ).
tff(c_35864,plain,
! [A_1533] :
( v4_rlvect_1(k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| ~ l1_vectsp_2('#skF_2',A_1533)
| ~ v5_vectsp_2('#skF_2',A_1533)
| ~ l3_vectsp_1(A_1533)
| ~ v2_vectsp_2(A_1533)
| v10_vectsp_1(A_1533)
| ~ v8_vectsp_1(A_1533)
| ~ v7_vectsp_1(A_1533)
| ~ v6_vectsp_1(A_1533)
| ~ v7_group_1(A_1533)
| ~ v4_group_1(A_1533)
| ~ v6_rlvect_1(A_1533)
| ~ v5_rlvect_1(A_1533)
| ~ v4_rlvect_1(A_1533)
| ~ v3_rlvect_1(A_1533)
| v3_struct_0(A_1533) ),
inference(negUnitSimplification,[status(thm)],[c_26,c_35863]) ).
tff(c_34269,plain,
! [A_1495] :
( m1_rmod_2(k1_rmod_5(A_1495,'#skF_2','#skF_4'),A_1495,'#skF_2')
| ~ l1_vectsp_2('#skF_2',A_1495)
| ~ v5_vectsp_2('#skF_2',A_1495)
| ~ l3_vectsp_1(A_1495)
| ~ v2_vectsp_2(A_1495)
| v10_vectsp_1(A_1495)
| ~ v8_vectsp_1(A_1495)
| ~ v7_vectsp_1(A_1495)
| ~ v6_vectsp_1(A_1495)
| ~ v7_group_1(A_1495)
| ~ v4_group_1(A_1495)
| ~ v6_rlvect_1(A_1495)
| ~ v5_rlvect_1(A_1495)
| ~ v4_rlvect_1(A_1495)
| ~ v3_rlvect_1(A_1495)
| v3_struct_0(A_1495) ),
inference(negUnitSimplification,[status(thm)],[c_26,c_34268]) ).
tff(c_34875,plain,
! [A_1520] :
( m1_rmod_2('#skF_2','#skF_1',k1_rmod_5('#skF_1','#skF_2',A_1520))
| ~ r1_tarski('#skF_3',A_1520)
| ~ r1_tarski(A_1520,u1_struct_0('#skF_2')) ),
inference(resolution,[status(thm)],[c_286,c_34626]) ).
tff(c_282,plain,
! [C_133,B_131,A_127] :
( ( C_133 = B_131 )
| ~ m1_rmod_2(B_131,A_127,C_133)
| ~ m1_rmod_2(C_133,A_127,B_131)
| ~ l1_vectsp_2(C_133,A_127)
| ~ v5_vectsp_2(C_133,A_127)
| ~ v3_vectsp_2(C_133,A_127)
| ~ v6_rlvect_1(C_133)
| ~ v5_rlvect_1(C_133)
| ~ v4_rlvect_1(C_133)
| ~ v3_rlvect_1(C_133)
| v3_struct_0(C_133)
| ~ l1_vectsp_2(B_131,A_127)
| ~ v5_vectsp_2(B_131,A_127)
| ~ v3_vectsp_2(B_131,A_127)
| ~ v6_rlvect_1(B_131)
| ~ v5_rlvect_1(B_131)
| ~ v4_rlvect_1(B_131)
| ~ v3_rlvect_1(B_131)
| v3_struct_0(B_131)
| ~ l3_vectsp_1(A_127)
| ~ v8_vectsp_1(A_127)
| ~ v7_vectsp_1(A_127)
| ~ v6_vectsp_1(A_127)
| ~ v4_group_1(A_127)
| ~ v6_rlvect_1(A_127)
| ~ v5_rlvect_1(A_127)
| ~ v4_rlvect_1(A_127)
| ~ v3_rlvect_1(A_127)
| v3_struct_0(A_127) ),
inference(cnfTransformation,[status(thm)],[f_784]) ).
tff(c_34877,plain,
! [A_1520] :
( ( k1_rmod_5('#skF_1','#skF_2',A_1520) = '#skF_2' )
| ~ m1_rmod_2(k1_rmod_5('#skF_1','#skF_2',A_1520),'#skF_1','#skF_2')
| ~ l1_vectsp_2(k1_rmod_5('#skF_1','#skF_2',A_1520),'#skF_1')
| ~ v5_vectsp_2(k1_rmod_5('#skF_1','#skF_2',A_1520),'#skF_1')
| ~ v3_vectsp_2(k1_rmod_5('#skF_1','#skF_2',A_1520),'#skF_1')
| ~ v6_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1520))
| ~ v5_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1520))
| ~ v4_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1520))
| ~ v3_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1520))
| v3_struct_0(k1_rmod_5('#skF_1','#skF_2',A_1520))
| ~ l1_vectsp_2('#skF_2','#skF_1')
| ~ v5_vectsp_2('#skF_2','#skF_1')
| ~ v3_vectsp_2('#skF_2','#skF_1')
| ~ v6_rlvect_1('#skF_2')
| ~ v5_rlvect_1('#skF_2')
| ~ v4_rlvect_1('#skF_2')
| ~ v3_rlvect_1('#skF_2')
| v3_struct_0('#skF_2')
| ~ l3_vectsp_1('#skF_1')
| ~ v8_vectsp_1('#skF_1')
| ~ v7_vectsp_1('#skF_1')
| ~ v6_vectsp_1('#skF_1')
| ~ v4_group_1('#skF_1')
| ~ v6_rlvect_1('#skF_1')
| ~ v5_rlvect_1('#skF_1')
| ~ v4_rlvect_1('#skF_1')
| ~ v3_rlvect_1('#skF_1')
| v3_struct_0('#skF_1')
| ~ r1_tarski('#skF_3',A_1520)
| ~ r1_tarski(A_1520,u1_struct_0('#skF_2')) ),
inference(resolution,[status(thm)],[c_34875,c_282]) ).
tff(c_34904,plain,
! [A_1520] :
( ( k1_rmod_5('#skF_1','#skF_2',A_1520) = '#skF_2' )
| ~ m1_rmod_2(k1_rmod_5('#skF_1','#skF_2',A_1520),'#skF_1','#skF_2')
| ~ l1_vectsp_2(k1_rmod_5('#skF_1','#skF_2',A_1520),'#skF_1')
| ~ v5_vectsp_2(k1_rmod_5('#skF_1','#skF_2',A_1520),'#skF_1')
| ~ v3_vectsp_2(k1_rmod_5('#skF_1','#skF_2',A_1520),'#skF_1')
| ~ v6_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1520))
| ~ v5_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1520))
| ~ v4_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1520))
| ~ v3_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1520))
| v3_struct_0(k1_rmod_5('#skF_1','#skF_2',A_1520))
| v3_struct_0('#skF_2')
| v3_struct_0('#skF_1')
| ~ r1_tarski('#skF_3',A_1520)
| ~ r1_tarski(A_1520,u1_struct_0('#skF_2')) ),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_48,c_46,c_44,c_42,c_38,c_36,c_34,c_28,c_24,c_22,c_20,c_18,c_16,c_14,c_12,c_34877]) ).
tff(c_50033,plain,
! [A_1728] :
( ( k1_rmod_5('#skF_1','#skF_2',A_1728) = '#skF_2' )
| ~ m1_rmod_2(k1_rmod_5('#skF_1','#skF_2',A_1728),'#skF_1','#skF_2')
| ~ l1_vectsp_2(k1_rmod_5('#skF_1','#skF_2',A_1728),'#skF_1')
| ~ v5_vectsp_2(k1_rmod_5('#skF_1','#skF_2',A_1728),'#skF_1')
| ~ v3_vectsp_2(k1_rmod_5('#skF_1','#skF_2',A_1728),'#skF_1')
| ~ v6_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1728))
| ~ v5_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1728))
| ~ v4_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1728))
| ~ v3_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1728))
| v3_struct_0(k1_rmod_5('#skF_1','#skF_2',A_1728))
| ~ r1_tarski('#skF_3',A_1728)
| ~ r1_tarski(A_1728,u1_struct_0('#skF_2')) ),
inference(negUnitSimplification,[status(thm)],[c_52,c_26,c_34904]) ).
tff(c_50049,plain,
( ( k1_rmod_5('#skF_1','#skF_2','#skF_4') = '#skF_2' )
| ~ l1_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v5_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v3_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v6_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v5_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v4_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v3_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| v3_struct_0(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ r1_tarski('#skF_3','#skF_4')
| ~ r1_tarski('#skF_4',u1_struct_0('#skF_2'))
| ~ l1_vectsp_2('#skF_2','#skF_1')
| ~ v5_vectsp_2('#skF_2','#skF_1')
| ~ l3_vectsp_1('#skF_1')
| ~ v2_vectsp_2('#skF_1')
| v10_vectsp_1('#skF_1')
| ~ v8_vectsp_1('#skF_1')
| ~ v7_vectsp_1('#skF_1')
| ~ v6_vectsp_1('#skF_1')
| ~ v7_group_1('#skF_1')
| ~ v4_group_1('#skF_1')
| ~ v6_rlvect_1('#skF_1')
| ~ v5_rlvect_1('#skF_1')
| ~ v4_rlvect_1('#skF_1')
| ~ v3_rlvect_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_34269,c_50033]) ).
tff(c_50073,plain,
( ( k1_rmod_5('#skF_1','#skF_2','#skF_4') = '#skF_2' )
| ~ l1_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v5_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v3_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v6_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v5_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v4_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| v3_struct_0(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| v10_vectsp_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_48,c_46,c_44,c_42,c_40,c_38,c_36,c_34,c_30,c_28,c_14,c_12,c_496,c_4,c_48796,c_50049]) ).
tff(c_50074,plain,
( ~ l1_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v5_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v3_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v6_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v5_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v4_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| v3_struct_0(k1_rmod_5('#skF_1','#skF_2','#skF_4')) ),
inference(negUnitSimplification,[status(thm)],[c_52,c_32,c_2,c_50073]) ).
tff(c_50803,plain,
~ v4_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4')),
inference(splitLeft,[status(thm)],[c_50074]) ).
tff(c_50806,plain,
( ~ l1_vectsp_2('#skF_2','#skF_1')
| ~ v5_vectsp_2('#skF_2','#skF_1')
| ~ l3_vectsp_1('#skF_1')
| ~ v2_vectsp_2('#skF_1')
| v10_vectsp_1('#skF_1')
| ~ v8_vectsp_1('#skF_1')
| ~ v7_vectsp_1('#skF_1')
| ~ v6_vectsp_1('#skF_1')
| ~ v7_group_1('#skF_1')
| ~ v4_group_1('#skF_1')
| ~ v6_rlvect_1('#skF_1')
| ~ v5_rlvect_1('#skF_1')
| ~ v4_rlvect_1('#skF_1')
| ~ v3_rlvect_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_35864,c_50803]) ).
tff(c_50809,plain,
( v10_vectsp_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_48,c_46,c_44,c_42,c_40,c_38,c_36,c_34,c_30,c_28,c_14,c_12,c_50806]) ).
tff(c_50811,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_52,c_32,c_50809]) ).
tff(c_50813,plain,
v4_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4')),
inference(splitRight,[status(thm)],[c_50074]) ).
tff(c_118,plain,
! [C_41,A_38,B_39] :
( v5_rlvect_1(C_41)
| ~ m1_rmod_2(C_41,A_38,B_39)
| ~ l1_vectsp_2(B_39,A_38)
| ~ v5_vectsp_2(B_39,A_38)
| ~ v6_rlvect_1(B_39)
| ~ v5_rlvect_1(B_39)
| ~ v4_rlvect_1(B_39)
| ~ v3_rlvect_1(B_39)
| v3_struct_0(B_39)
| ~ l3_vectsp_1(A_38)
| ~ v8_vectsp_1(A_38)
| ~ v7_vectsp_1(A_38)
| ~ v6_vectsp_1(A_38)
| ~ v4_group_1(A_38)
| ~ v6_rlvect_1(A_38)
| ~ v5_rlvect_1(A_38)
| ~ v4_rlvect_1(A_38)
| ~ v3_rlvect_1(A_38)
| v3_struct_0(A_38) ),
inference(cnfTransformation,[status(thm)],[f_299]) ).
tff(c_35823,plain,
! [A_1533] :
( v5_rlvect_1(k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| ~ v6_rlvect_1('#skF_2')
| ~ v5_rlvect_1('#skF_2')
| ~ v4_rlvect_1('#skF_2')
| ~ v3_rlvect_1('#skF_2')
| v3_struct_0('#skF_2')
| ~ l1_vectsp_2('#skF_2',A_1533)
| ~ v5_vectsp_2('#skF_2',A_1533)
| ~ l3_vectsp_1(A_1533)
| ~ v2_vectsp_2(A_1533)
| v10_vectsp_1(A_1533)
| ~ v8_vectsp_1(A_1533)
| ~ v7_vectsp_1(A_1533)
| ~ v6_vectsp_1(A_1533)
| ~ v7_group_1(A_1533)
| ~ v4_group_1(A_1533)
| ~ v6_rlvect_1(A_1533)
| ~ v5_rlvect_1(A_1533)
| ~ v4_rlvect_1(A_1533)
| ~ v3_rlvect_1(A_1533)
| v3_struct_0(A_1533) ),
inference(resolution,[status(thm)],[c_35809,c_118]) ).
tff(c_35851,plain,
! [A_1533] :
( v5_rlvect_1(k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| v3_struct_0('#skF_2')
| ~ l1_vectsp_2('#skF_2',A_1533)
| ~ v5_vectsp_2('#skF_2',A_1533)
| ~ l3_vectsp_1(A_1533)
| ~ v2_vectsp_2(A_1533)
| v10_vectsp_1(A_1533)
| ~ v8_vectsp_1(A_1533)
| ~ v7_vectsp_1(A_1533)
| ~ v6_vectsp_1(A_1533)
| ~ v7_group_1(A_1533)
| ~ v4_group_1(A_1533)
| ~ v6_rlvect_1(A_1533)
| ~ v5_rlvect_1(A_1533)
| ~ v4_rlvect_1(A_1533)
| ~ v3_rlvect_1(A_1533)
| v3_struct_0(A_1533) ),
inference(demodulation,[status(thm),theory(equality)],[c_24,c_22,c_20,c_18,c_35823]) ).
tff(c_35852,plain,
! [A_1533] :
( v5_rlvect_1(k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| ~ l1_vectsp_2('#skF_2',A_1533)
| ~ v5_vectsp_2('#skF_2',A_1533)
| ~ l3_vectsp_1(A_1533)
| ~ v2_vectsp_2(A_1533)
| v10_vectsp_1(A_1533)
| ~ v8_vectsp_1(A_1533)
| ~ v7_vectsp_1(A_1533)
| ~ v6_vectsp_1(A_1533)
| ~ v7_group_1(A_1533)
| ~ v4_group_1(A_1533)
| ~ v6_rlvect_1(A_1533)
| ~ v5_rlvect_1(A_1533)
| ~ v4_rlvect_1(A_1533)
| ~ v3_rlvect_1(A_1533)
| v3_struct_0(A_1533) ),
inference(negUnitSimplification,[status(thm)],[c_26,c_35851]) ).
tff(c_34730,plain,
! [A_134] :
( m1_rmod_2('#skF_2','#skF_1',k1_rmod_5('#skF_1','#skF_2',A_134))
| ~ r1_tarski('#skF_3',A_134)
| ~ r1_tarski(A_134,u1_struct_0('#skF_2')) ),
inference(resolution,[status(thm)],[c_286,c_34626]) ).
tff(c_35811,plain,
! [A_1533] :
( ( k1_rmod_5(A_1533,'#skF_2','#skF_4') = '#skF_2' )
| ~ m1_rmod_2('#skF_2',A_1533,k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| ~ v3_vectsp_2('#skF_2',A_1533)
| ~ v6_rlvect_1('#skF_2')
| ~ v5_rlvect_1('#skF_2')
| ~ v4_rlvect_1('#skF_2')
| ~ v3_rlvect_1('#skF_2')
| v3_struct_0('#skF_2')
| ~ l1_vectsp_2(k1_rmod_5(A_1533,'#skF_2','#skF_4'),A_1533)
| ~ v5_vectsp_2(k1_rmod_5(A_1533,'#skF_2','#skF_4'),A_1533)
| ~ v3_vectsp_2(k1_rmod_5(A_1533,'#skF_2','#skF_4'),A_1533)
| ~ v6_rlvect_1(k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| ~ v5_rlvect_1(k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| ~ v4_rlvect_1(k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| ~ v3_rlvect_1(k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| v3_struct_0(k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| ~ l1_vectsp_2('#skF_2',A_1533)
| ~ v5_vectsp_2('#skF_2',A_1533)
| ~ l3_vectsp_1(A_1533)
| ~ v2_vectsp_2(A_1533)
| v10_vectsp_1(A_1533)
| ~ v8_vectsp_1(A_1533)
| ~ v7_vectsp_1(A_1533)
| ~ v6_vectsp_1(A_1533)
| ~ v7_group_1(A_1533)
| ~ v4_group_1(A_1533)
| ~ v6_rlvect_1(A_1533)
| ~ v5_rlvect_1(A_1533)
| ~ v4_rlvect_1(A_1533)
| ~ v3_rlvect_1(A_1533)
| v3_struct_0(A_1533) ),
inference(resolution,[status(thm)],[c_35809,c_282]) ).
tff(c_35835,plain,
! [A_1533] :
( ( k1_rmod_5(A_1533,'#skF_2','#skF_4') = '#skF_2' )
| ~ m1_rmod_2('#skF_2',A_1533,k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| ~ v3_vectsp_2('#skF_2',A_1533)
| v3_struct_0('#skF_2')
| ~ l1_vectsp_2(k1_rmod_5(A_1533,'#skF_2','#skF_4'),A_1533)
| ~ v5_vectsp_2(k1_rmod_5(A_1533,'#skF_2','#skF_4'),A_1533)
| ~ v3_vectsp_2(k1_rmod_5(A_1533,'#skF_2','#skF_4'),A_1533)
| ~ v6_rlvect_1(k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| ~ v5_rlvect_1(k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| ~ v4_rlvect_1(k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| ~ v3_rlvect_1(k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| v3_struct_0(k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| ~ l1_vectsp_2('#skF_2',A_1533)
| ~ v5_vectsp_2('#skF_2',A_1533)
| ~ l3_vectsp_1(A_1533)
| ~ v2_vectsp_2(A_1533)
| v10_vectsp_1(A_1533)
| ~ v8_vectsp_1(A_1533)
| ~ v7_vectsp_1(A_1533)
| ~ v6_vectsp_1(A_1533)
| ~ v7_group_1(A_1533)
| ~ v4_group_1(A_1533)
| ~ v6_rlvect_1(A_1533)
| ~ v5_rlvect_1(A_1533)
| ~ v4_rlvect_1(A_1533)
| ~ v3_rlvect_1(A_1533)
| v3_struct_0(A_1533) ),
inference(demodulation,[status(thm),theory(equality)],[c_24,c_22,c_20,c_18,c_35811]) ).
tff(c_51844,plain,
! [A_1759] :
( ( k1_rmod_5(A_1759,'#skF_2','#skF_4') = '#skF_2' )
| ~ m1_rmod_2('#skF_2',A_1759,k1_rmod_5(A_1759,'#skF_2','#skF_4'))
| ~ v3_vectsp_2('#skF_2',A_1759)
| ~ l1_vectsp_2(k1_rmod_5(A_1759,'#skF_2','#skF_4'),A_1759)
| ~ v5_vectsp_2(k1_rmod_5(A_1759,'#skF_2','#skF_4'),A_1759)
| ~ v3_vectsp_2(k1_rmod_5(A_1759,'#skF_2','#skF_4'),A_1759)
| ~ v6_rlvect_1(k1_rmod_5(A_1759,'#skF_2','#skF_4'))
| ~ v5_rlvect_1(k1_rmod_5(A_1759,'#skF_2','#skF_4'))
| ~ v4_rlvect_1(k1_rmod_5(A_1759,'#skF_2','#skF_4'))
| ~ v3_rlvect_1(k1_rmod_5(A_1759,'#skF_2','#skF_4'))
| v3_struct_0(k1_rmod_5(A_1759,'#skF_2','#skF_4'))
| ~ l1_vectsp_2('#skF_2',A_1759)
| ~ v5_vectsp_2('#skF_2',A_1759)
| ~ l3_vectsp_1(A_1759)
| ~ v2_vectsp_2(A_1759)
| v10_vectsp_1(A_1759)
| ~ v8_vectsp_1(A_1759)
| ~ v7_vectsp_1(A_1759)
| ~ v6_vectsp_1(A_1759)
| ~ v7_group_1(A_1759)
| ~ v4_group_1(A_1759)
| ~ v6_rlvect_1(A_1759)
| ~ v5_rlvect_1(A_1759)
| ~ v4_rlvect_1(A_1759)
| ~ v3_rlvect_1(A_1759)
| v3_struct_0(A_1759) ),
inference(negUnitSimplification,[status(thm)],[c_26,c_35835]) ).
tff(c_51848,plain,
( ( k1_rmod_5('#skF_1','#skF_2','#skF_4') = '#skF_2' )
| ~ v3_vectsp_2('#skF_2','#skF_1')
| ~ l1_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v5_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v3_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v6_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v5_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v4_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v3_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| v3_struct_0(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ l1_vectsp_2('#skF_2','#skF_1')
| ~ v5_vectsp_2('#skF_2','#skF_1')
| ~ l3_vectsp_1('#skF_1')
| ~ v2_vectsp_2('#skF_1')
| v10_vectsp_1('#skF_1')
| ~ v8_vectsp_1('#skF_1')
| ~ v7_vectsp_1('#skF_1')
| ~ v6_vectsp_1('#skF_1')
| ~ v7_group_1('#skF_1')
| ~ v4_group_1('#skF_1')
| ~ v6_rlvect_1('#skF_1')
| ~ v5_rlvect_1('#skF_1')
| ~ v4_rlvect_1('#skF_1')
| ~ v3_rlvect_1('#skF_1')
| v3_struct_0('#skF_1')
| ~ r1_tarski('#skF_3','#skF_4')
| ~ r1_tarski('#skF_4',u1_struct_0('#skF_2')) ),
inference(resolution,[status(thm)],[c_34730,c_51844]) ).
tff(c_51854,plain,
( ( k1_rmod_5('#skF_1','#skF_2','#skF_4') = '#skF_2' )
| ~ l1_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v5_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v3_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v6_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v5_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| v3_struct_0(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| v10_vectsp_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_496,c_4,c_50,c_48,c_46,c_44,c_42,c_40,c_38,c_36,c_34,c_30,c_28,c_14,c_12,c_48796,c_50813,c_16,c_51848]) ).
tff(c_51855,plain,
( ~ l1_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v5_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v3_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v6_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v5_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| v3_struct_0(k1_rmod_5('#skF_1','#skF_2','#skF_4')) ),
inference(negUnitSimplification,[status(thm)],[c_52,c_32,c_2,c_51854]) ).
tff(c_53022,plain,
~ v5_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4')),
inference(splitLeft,[status(thm)],[c_51855]) ).
tff(c_53025,plain,
( ~ l1_vectsp_2('#skF_2','#skF_1')
| ~ v5_vectsp_2('#skF_2','#skF_1')
| ~ l3_vectsp_1('#skF_1')
| ~ v2_vectsp_2('#skF_1')
| v10_vectsp_1('#skF_1')
| ~ v8_vectsp_1('#skF_1')
| ~ v7_vectsp_1('#skF_1')
| ~ v6_vectsp_1('#skF_1')
| ~ v7_group_1('#skF_1')
| ~ v4_group_1('#skF_1')
| ~ v6_rlvect_1('#skF_1')
| ~ v5_rlvect_1('#skF_1')
| ~ v4_rlvect_1('#skF_1')
| ~ v3_rlvect_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_35852,c_53022]) ).
tff(c_53028,plain,
( v10_vectsp_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_48,c_46,c_44,c_42,c_40,c_38,c_36,c_34,c_30,c_28,c_14,c_12,c_53025]) ).
tff(c_53030,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_52,c_32,c_53028]) ).
tff(c_53032,plain,
v5_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4')),
inference(splitRight,[status(thm)],[c_51855]) ).
tff(c_116,plain,
! [C_41,A_38,B_39] :
( v6_rlvect_1(C_41)
| ~ m1_rmod_2(C_41,A_38,B_39)
| ~ l1_vectsp_2(B_39,A_38)
| ~ v5_vectsp_2(B_39,A_38)
| ~ v6_rlvect_1(B_39)
| ~ v5_rlvect_1(B_39)
| ~ v4_rlvect_1(B_39)
| ~ v3_rlvect_1(B_39)
| v3_struct_0(B_39)
| ~ l3_vectsp_1(A_38)
| ~ v8_vectsp_1(A_38)
| ~ v7_vectsp_1(A_38)
| ~ v6_vectsp_1(A_38)
| ~ v4_group_1(A_38)
| ~ v6_rlvect_1(A_38)
| ~ v5_rlvect_1(A_38)
| ~ v4_rlvect_1(A_38)
| ~ v3_rlvect_1(A_38)
| v3_struct_0(A_38) ),
inference(cnfTransformation,[status(thm)],[f_299]) ).
tff(c_35829,plain,
! [A_1533] :
( v6_rlvect_1(k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| ~ v6_rlvect_1('#skF_2')
| ~ v5_rlvect_1('#skF_2')
| ~ v4_rlvect_1('#skF_2')
| ~ v3_rlvect_1('#skF_2')
| v3_struct_0('#skF_2')
| ~ l1_vectsp_2('#skF_2',A_1533)
| ~ v5_vectsp_2('#skF_2',A_1533)
| ~ l3_vectsp_1(A_1533)
| ~ v2_vectsp_2(A_1533)
| v10_vectsp_1(A_1533)
| ~ v8_vectsp_1(A_1533)
| ~ v7_vectsp_1(A_1533)
| ~ v6_vectsp_1(A_1533)
| ~ v7_group_1(A_1533)
| ~ v4_group_1(A_1533)
| ~ v6_rlvect_1(A_1533)
| ~ v5_rlvect_1(A_1533)
| ~ v4_rlvect_1(A_1533)
| ~ v3_rlvect_1(A_1533)
| v3_struct_0(A_1533) ),
inference(resolution,[status(thm)],[c_35809,c_116]) ).
tff(c_35859,plain,
! [A_1533] :
( v6_rlvect_1(k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| v3_struct_0('#skF_2')
| ~ l1_vectsp_2('#skF_2',A_1533)
| ~ v5_vectsp_2('#skF_2',A_1533)
| ~ l3_vectsp_1(A_1533)
| ~ v2_vectsp_2(A_1533)
| v10_vectsp_1(A_1533)
| ~ v8_vectsp_1(A_1533)
| ~ v7_vectsp_1(A_1533)
| ~ v6_vectsp_1(A_1533)
| ~ v7_group_1(A_1533)
| ~ v4_group_1(A_1533)
| ~ v6_rlvect_1(A_1533)
| ~ v5_rlvect_1(A_1533)
| ~ v4_rlvect_1(A_1533)
| ~ v3_rlvect_1(A_1533)
| v3_struct_0(A_1533) ),
inference(demodulation,[status(thm),theory(equality)],[c_24,c_22,c_20,c_18,c_35829]) ).
tff(c_35860,plain,
! [A_1533] :
( v6_rlvect_1(k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| ~ l1_vectsp_2('#skF_2',A_1533)
| ~ v5_vectsp_2('#skF_2',A_1533)
| ~ l3_vectsp_1(A_1533)
| ~ v2_vectsp_2(A_1533)
| v10_vectsp_1(A_1533)
| ~ v8_vectsp_1(A_1533)
| ~ v7_vectsp_1(A_1533)
| ~ v6_vectsp_1(A_1533)
| ~ v7_group_1(A_1533)
| ~ v4_group_1(A_1533)
| ~ v6_rlvect_1(A_1533)
| ~ v5_rlvect_1(A_1533)
| ~ v4_rlvect_1(A_1533)
| ~ v3_rlvect_1(A_1533)
| v3_struct_0(A_1533) ),
inference(negUnitSimplification,[status(thm)],[c_26,c_35859]) ).
tff(c_51851,plain,
( ( k1_rmod_5('#skF_1','#skF_2','#skF_4') = '#skF_2' )
| ~ v3_vectsp_2('#skF_2','#skF_1')
| ~ l1_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v5_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v3_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v6_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v5_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v4_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v3_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| v3_struct_0(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ l1_vectsp_2('#skF_2','#skF_1')
| ~ v5_vectsp_2('#skF_2','#skF_1')
| ~ l3_vectsp_1('#skF_1')
| ~ v2_vectsp_2('#skF_1')
| v10_vectsp_1('#skF_1')
| ~ v8_vectsp_1('#skF_1')
| ~ v7_vectsp_1('#skF_1')
| ~ v6_vectsp_1('#skF_1')
| ~ v7_group_1('#skF_1')
| ~ v4_group_1('#skF_1')
| ~ v6_rlvect_1('#skF_1')
| ~ v5_rlvect_1('#skF_1')
| ~ v4_rlvect_1('#skF_1')
| ~ v3_rlvect_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_34738,c_51844]) ).
tff(c_51858,plain,
( ( k1_rmod_5('#skF_1','#skF_2','#skF_4') = '#skF_2' )
| ~ l1_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v5_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v3_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v6_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v5_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| v3_struct_0(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| v10_vectsp_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_48,c_46,c_44,c_42,c_40,c_38,c_36,c_34,c_30,c_28,c_14,c_12,c_48796,c_50813,c_16,c_51851]) ).
tff(c_51859,plain,
( ~ l1_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v5_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v3_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v6_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v5_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| v3_struct_0(k1_rmod_5('#skF_1','#skF_2','#skF_4')) ),
inference(negUnitSimplification,[status(thm)],[c_52,c_32,c_2,c_51858]) ).
tff(c_53795,plain,
( ~ l1_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v5_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v3_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v6_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| v3_struct_0(k1_rmod_5('#skF_1','#skF_2','#skF_4')) ),
inference(demodulation,[status(thm),theory(equality)],[c_53032,c_51859]) ).
tff(c_53796,plain,
~ v6_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4')),
inference(splitLeft,[status(thm)],[c_53795]) ).
tff(c_53799,plain,
( ~ l1_vectsp_2('#skF_2','#skF_1')
| ~ v5_vectsp_2('#skF_2','#skF_1')
| ~ l3_vectsp_1('#skF_1')
| ~ v2_vectsp_2('#skF_1')
| v10_vectsp_1('#skF_1')
| ~ v8_vectsp_1('#skF_1')
| ~ v7_vectsp_1('#skF_1')
| ~ v6_vectsp_1('#skF_1')
| ~ v7_group_1('#skF_1')
| ~ v4_group_1('#skF_1')
| ~ v6_rlvect_1('#skF_1')
| ~ v5_rlvect_1('#skF_1')
| ~ v4_rlvect_1('#skF_1')
| ~ v3_rlvect_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_35860,c_53796]) ).
tff(c_53802,plain,
( v10_vectsp_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_48,c_46,c_44,c_42,c_40,c_38,c_36,c_34,c_30,c_28,c_14,c_12,c_53799]) ).
tff(c_53804,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_52,c_32,c_53802]) ).
tff(c_53806,plain,
v6_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4')),
inference(splitRight,[status(thm)],[c_53795]) ).
tff(c_114,plain,
! [C_41,A_38,B_39] :
( v5_vectsp_2(C_41,A_38)
| ~ m1_rmod_2(C_41,A_38,B_39)
| ~ l1_vectsp_2(B_39,A_38)
| ~ v5_vectsp_2(B_39,A_38)
| ~ v6_rlvect_1(B_39)
| ~ v5_rlvect_1(B_39)
| ~ v4_rlvect_1(B_39)
| ~ v3_rlvect_1(B_39)
| v3_struct_0(B_39)
| ~ l3_vectsp_1(A_38)
| ~ v8_vectsp_1(A_38)
| ~ v7_vectsp_1(A_38)
| ~ v6_vectsp_1(A_38)
| ~ v4_group_1(A_38)
| ~ v6_rlvect_1(A_38)
| ~ v5_rlvect_1(A_38)
| ~ v4_rlvect_1(A_38)
| ~ v3_rlvect_1(A_38)
| v3_struct_0(A_38) ),
inference(cnfTransformation,[status(thm)],[f_299]) ).
tff(c_35817,plain,
! [A_1533] :
( v5_vectsp_2(k1_rmod_5(A_1533,'#skF_2','#skF_4'),A_1533)
| ~ v6_rlvect_1('#skF_2')
| ~ v5_rlvect_1('#skF_2')
| ~ v4_rlvect_1('#skF_2')
| ~ v3_rlvect_1('#skF_2')
| v3_struct_0('#skF_2')
| ~ l1_vectsp_2('#skF_2',A_1533)
| ~ v5_vectsp_2('#skF_2',A_1533)
| ~ l3_vectsp_1(A_1533)
| ~ v2_vectsp_2(A_1533)
| v10_vectsp_1(A_1533)
| ~ v8_vectsp_1(A_1533)
| ~ v7_vectsp_1(A_1533)
| ~ v6_vectsp_1(A_1533)
| ~ v7_group_1(A_1533)
| ~ v4_group_1(A_1533)
| ~ v6_rlvect_1(A_1533)
| ~ v5_rlvect_1(A_1533)
| ~ v4_rlvect_1(A_1533)
| ~ v3_rlvect_1(A_1533)
| v3_struct_0(A_1533) ),
inference(resolution,[status(thm)],[c_35809,c_114]) ).
tff(c_35843,plain,
! [A_1533] :
( v5_vectsp_2(k1_rmod_5(A_1533,'#skF_2','#skF_4'),A_1533)
| v3_struct_0('#skF_2')
| ~ l1_vectsp_2('#skF_2',A_1533)
| ~ v5_vectsp_2('#skF_2',A_1533)
| ~ l3_vectsp_1(A_1533)
| ~ v2_vectsp_2(A_1533)
| v10_vectsp_1(A_1533)
| ~ v8_vectsp_1(A_1533)
| ~ v7_vectsp_1(A_1533)
| ~ v6_vectsp_1(A_1533)
| ~ v7_group_1(A_1533)
| ~ v4_group_1(A_1533)
| ~ v6_rlvect_1(A_1533)
| ~ v5_rlvect_1(A_1533)
| ~ v4_rlvect_1(A_1533)
| ~ v3_rlvect_1(A_1533)
| v3_struct_0(A_1533) ),
inference(demodulation,[status(thm),theory(equality)],[c_24,c_22,c_20,c_18,c_35817]) ).
tff(c_35844,plain,
! [A_1533] :
( v5_vectsp_2(k1_rmod_5(A_1533,'#skF_2','#skF_4'),A_1533)
| ~ l1_vectsp_2('#skF_2',A_1533)
| ~ v5_vectsp_2('#skF_2',A_1533)
| ~ l3_vectsp_1(A_1533)
| ~ v2_vectsp_2(A_1533)
| v10_vectsp_1(A_1533)
| ~ v8_vectsp_1(A_1533)
| ~ v7_vectsp_1(A_1533)
| ~ v6_vectsp_1(A_1533)
| ~ v7_group_1(A_1533)
| ~ v4_group_1(A_1533)
| ~ v6_rlvect_1(A_1533)
| ~ v5_rlvect_1(A_1533)
| ~ v4_rlvect_1(A_1533)
| ~ v3_rlvect_1(A_1533)
| v3_struct_0(A_1533) ),
inference(negUnitSimplification,[status(thm)],[c_26,c_35843]) ).
tff(c_53519,plain,
! [A_1782,B_1783,A_1784] :
( m1_rmod_2(k1_rmod_5(A_1782,B_1783,A_1784),A_1782,B_1783)
| ~ l1_vectsp_2(B_1783,A_1782)
| ~ v5_vectsp_2(B_1783,A_1782)
| ~ v6_rlvect_1(B_1783)
| ~ v5_rlvect_1(B_1783)
| ~ v4_rlvect_1(B_1783)
| ~ v3_rlvect_1(B_1783)
| v3_struct_0(B_1783)
| ~ l3_vectsp_1(A_1782)
| ~ v2_vectsp_2(A_1782)
| v10_vectsp_1(A_1782)
| ~ v8_vectsp_1(A_1782)
| ~ v7_vectsp_1(A_1782)
| ~ v6_vectsp_1(A_1782)
| ~ v7_group_1(A_1782)
| ~ v4_group_1(A_1782)
| ~ v6_rlvect_1(A_1782)
| ~ v5_rlvect_1(A_1782)
| ~ v4_rlvect_1(A_1782)
| ~ v3_rlvect_1(A_1782)
| v3_struct_0(A_1782)
| ~ r1_tarski(A_1784,u1_struct_0(B_1783)) ),
inference(resolution,[status(thm)],[c_286,c_34180]) ).
tff(c_34905,plain,
! [A_1520] :
( ( k1_rmod_5('#skF_1','#skF_2',A_1520) = '#skF_2' )
| ~ m1_rmod_2(k1_rmod_5('#skF_1','#skF_2',A_1520),'#skF_1','#skF_2')
| ~ l1_vectsp_2(k1_rmod_5('#skF_1','#skF_2',A_1520),'#skF_1')
| ~ v5_vectsp_2(k1_rmod_5('#skF_1','#skF_2',A_1520),'#skF_1')
| ~ v3_vectsp_2(k1_rmod_5('#skF_1','#skF_2',A_1520),'#skF_1')
| ~ v6_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1520))
| ~ v5_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1520))
| ~ v4_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1520))
| ~ v3_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1520))
| v3_struct_0(k1_rmod_5('#skF_1','#skF_2',A_1520))
| ~ r1_tarski('#skF_3',A_1520)
| ~ r1_tarski(A_1520,u1_struct_0('#skF_2')) ),
inference(negUnitSimplification,[status(thm)],[c_52,c_26,c_34904]) ).
tff(c_53523,plain,
! [A_1784] :
( ( k1_rmod_5('#skF_1','#skF_2',A_1784) = '#skF_2' )
| ~ l1_vectsp_2(k1_rmod_5('#skF_1','#skF_2',A_1784),'#skF_1')
| ~ v5_vectsp_2(k1_rmod_5('#skF_1','#skF_2',A_1784),'#skF_1')
| ~ v3_vectsp_2(k1_rmod_5('#skF_1','#skF_2',A_1784),'#skF_1')
| ~ v6_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1784))
| ~ v5_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1784))
| ~ v4_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1784))
| ~ v3_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1784))
| v3_struct_0(k1_rmod_5('#skF_1','#skF_2',A_1784))
| ~ r1_tarski('#skF_3',A_1784)
| ~ l1_vectsp_2('#skF_2','#skF_1')
| ~ v5_vectsp_2('#skF_2','#skF_1')
| ~ v6_rlvect_1('#skF_2')
| ~ v5_rlvect_1('#skF_2')
| ~ v4_rlvect_1('#skF_2')
| ~ v3_rlvect_1('#skF_2')
| v3_struct_0('#skF_2')
| ~ l3_vectsp_1('#skF_1')
| ~ v2_vectsp_2('#skF_1')
| v10_vectsp_1('#skF_1')
| ~ v8_vectsp_1('#skF_1')
| ~ v7_vectsp_1('#skF_1')
| ~ v6_vectsp_1('#skF_1')
| ~ v7_group_1('#skF_1')
| ~ v4_group_1('#skF_1')
| ~ v6_rlvect_1('#skF_1')
| ~ v5_rlvect_1('#skF_1')
| ~ v4_rlvect_1('#skF_1')
| ~ v3_rlvect_1('#skF_1')
| v3_struct_0('#skF_1')
| ~ r1_tarski(A_1784,u1_struct_0('#skF_2')) ),
inference(resolution,[status(thm)],[c_53519,c_34905]) ).
tff(c_53552,plain,
! [A_1784] :
( ( k1_rmod_5('#skF_1','#skF_2',A_1784) = '#skF_2' )
| ~ l1_vectsp_2(k1_rmod_5('#skF_1','#skF_2',A_1784),'#skF_1')
| ~ v5_vectsp_2(k1_rmod_5('#skF_1','#skF_2',A_1784),'#skF_1')
| ~ v3_vectsp_2(k1_rmod_5('#skF_1','#skF_2',A_1784),'#skF_1')
| ~ v6_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1784))
| ~ v5_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1784))
| ~ v4_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1784))
| ~ v3_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1784))
| v3_struct_0(k1_rmod_5('#skF_1','#skF_2',A_1784))
| ~ r1_tarski('#skF_3',A_1784)
| v3_struct_0('#skF_2')
| v10_vectsp_1('#skF_1')
| v3_struct_0('#skF_1')
| ~ r1_tarski(A_1784,u1_struct_0('#skF_2')) ),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_48,c_46,c_44,c_42,c_40,c_38,c_36,c_34,c_30,c_28,c_24,c_22,c_20,c_18,c_14,c_12,c_53523]) ).
tff(c_54037,plain,
! [A_1801] :
( ( k1_rmod_5('#skF_1','#skF_2',A_1801) = '#skF_2' )
| ~ l1_vectsp_2(k1_rmod_5('#skF_1','#skF_2',A_1801),'#skF_1')
| ~ v5_vectsp_2(k1_rmod_5('#skF_1','#skF_2',A_1801),'#skF_1')
| ~ v3_vectsp_2(k1_rmod_5('#skF_1','#skF_2',A_1801),'#skF_1')
| ~ v6_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1801))
| ~ v5_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1801))
| ~ v4_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1801))
| ~ v3_rlvect_1(k1_rmod_5('#skF_1','#skF_2',A_1801))
| v3_struct_0(k1_rmod_5('#skF_1','#skF_2',A_1801))
| ~ r1_tarski('#skF_3',A_1801)
| ~ r1_tarski(A_1801,u1_struct_0('#skF_2')) ),
inference(negUnitSimplification,[status(thm)],[c_52,c_32,c_26,c_53552]) ).
tff(c_54041,plain,
( ( k1_rmod_5('#skF_1','#skF_2','#skF_4') = '#skF_2' )
| ~ l1_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v3_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v6_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v5_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v4_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ v3_rlvect_1(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| v3_struct_0(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| ~ r1_tarski('#skF_3','#skF_4')
| ~ r1_tarski('#skF_4',u1_struct_0('#skF_2'))
| ~ l1_vectsp_2('#skF_2','#skF_1')
| ~ v5_vectsp_2('#skF_2','#skF_1')
| ~ l3_vectsp_1('#skF_1')
| ~ v2_vectsp_2('#skF_1')
| v10_vectsp_1('#skF_1')
| ~ v8_vectsp_1('#skF_1')
| ~ v7_vectsp_1('#skF_1')
| ~ v6_vectsp_1('#skF_1')
| ~ v7_group_1('#skF_1')
| ~ v4_group_1('#skF_1')
| ~ v6_rlvect_1('#skF_1')
| ~ v5_rlvect_1('#skF_1')
| ~ v4_rlvect_1('#skF_1')
| ~ v3_rlvect_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_35844,c_54037]) ).
tff(c_54057,plain,
( ( k1_rmod_5('#skF_1','#skF_2','#skF_4') = '#skF_2' )
| ~ l1_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v3_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| v3_struct_0(k1_rmod_5('#skF_1','#skF_2','#skF_4'))
| v10_vectsp_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_48,c_46,c_44,c_42,c_40,c_38,c_36,c_34,c_30,c_28,c_14,c_12,c_496,c_4,c_48796,c_50813,c_53032,c_53806,c_54041]) ).
tff(c_54058,plain,
( ~ l1_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| ~ v3_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| v3_struct_0(k1_rmod_5('#skF_1','#skF_2','#skF_4')) ),
inference(negUnitSimplification,[status(thm)],[c_52,c_32,c_2,c_54057]) ).
tff(c_54071,plain,
~ v3_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1'),
inference(splitLeft,[status(thm)],[c_54058]) ).
tff(c_54074,plain,
( ~ l1_vectsp_2('#skF_2','#skF_1')
| ~ v5_vectsp_2('#skF_2','#skF_1')
| ~ v6_rlvect_1('#skF_2')
| ~ v5_rlvect_1('#skF_2')
| ~ v4_rlvect_1('#skF_2')
| ~ v3_rlvect_1('#skF_2')
| v3_struct_0('#skF_2')
| ~ l3_vectsp_1('#skF_1')
| ~ v2_vectsp_2('#skF_1')
| v10_vectsp_1('#skF_1')
| ~ v8_vectsp_1('#skF_1')
| ~ v7_vectsp_1('#skF_1')
| ~ v6_vectsp_1('#skF_1')
| ~ v7_group_1('#skF_1')
| ~ v4_group_1('#skF_1')
| ~ v6_rlvect_1('#skF_1')
| ~ v5_rlvect_1('#skF_1')
| ~ v4_rlvect_1('#skF_1')
| ~ v3_rlvect_1('#skF_1')
| v3_struct_0('#skF_1')
| ~ r1_tarski('#skF_4',u1_struct_0('#skF_2')) ),
inference(resolution,[status(thm)],[c_33671,c_54071]) ).
tff(c_54080,plain,
( v3_struct_0('#skF_2')
| v10_vectsp_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_496,c_50,c_48,c_46,c_44,c_42,c_40,c_38,c_36,c_34,c_30,c_28,c_24,c_22,c_20,c_18,c_14,c_12,c_54074]) ).
tff(c_54082,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_52,c_32,c_26,c_54080]) ).
tff(c_54083,plain,
( ~ l1_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1')
| v3_struct_0(k1_rmod_5('#skF_1','#skF_2','#skF_4')) ),
inference(splitRight,[status(thm)],[c_54058]) ).
tff(c_54085,plain,
~ l1_vectsp_2(k1_rmod_5('#skF_1','#skF_2','#skF_4'),'#skF_1'),
inference(splitLeft,[status(thm)],[c_54083]) ).
tff(c_54088,plain,
( ~ l1_vectsp_2('#skF_2','#skF_1')
| ~ v5_vectsp_2('#skF_2','#skF_1')
| ~ l3_vectsp_1('#skF_1')
| ~ v2_vectsp_2('#skF_1')
| v10_vectsp_1('#skF_1')
| ~ v8_vectsp_1('#skF_1')
| ~ v7_vectsp_1('#skF_1')
| ~ v6_vectsp_1('#skF_1')
| ~ v7_group_1('#skF_1')
| ~ v4_group_1('#skF_1')
| ~ v6_rlvect_1('#skF_1')
| ~ v5_rlvect_1('#skF_1')
| ~ v4_rlvect_1('#skF_1')
| ~ v3_rlvect_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_35840,c_54085]) ).
tff(c_54091,plain,
( v10_vectsp_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_48,c_46,c_44,c_42,c_40,c_38,c_36,c_34,c_30,c_28,c_14,c_12,c_54088]) ).
tff(c_54093,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_52,c_32,c_54091]) ).
tff(c_54094,plain,
v3_struct_0(k1_rmod_5('#skF_1','#skF_2','#skF_4')),
inference(splitRight,[status(thm)],[c_54083]) ).
tff(c_124,plain,
! [C_41,A_38,B_39] :
( ~ v3_struct_0(C_41)
| ~ m1_rmod_2(C_41,A_38,B_39)
| ~ l1_vectsp_2(B_39,A_38)
| ~ v5_vectsp_2(B_39,A_38)
| ~ v6_rlvect_1(B_39)
| ~ v5_rlvect_1(B_39)
| ~ v4_rlvect_1(B_39)
| ~ v3_rlvect_1(B_39)
| v3_struct_0(B_39)
| ~ l3_vectsp_1(A_38)
| ~ v8_vectsp_1(A_38)
| ~ v7_vectsp_1(A_38)
| ~ v6_vectsp_1(A_38)
| ~ v4_group_1(A_38)
| ~ v6_rlvect_1(A_38)
| ~ v5_rlvect_1(A_38)
| ~ v4_rlvect_1(A_38)
| ~ v3_rlvect_1(A_38)
| v3_struct_0(A_38) ),
inference(cnfTransformation,[status(thm)],[f_299]) ).
tff(c_35826,plain,
! [A_1533] :
( ~ v3_struct_0(k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| ~ v6_rlvect_1('#skF_2')
| ~ v5_rlvect_1('#skF_2')
| ~ v4_rlvect_1('#skF_2')
| ~ v3_rlvect_1('#skF_2')
| v3_struct_0('#skF_2')
| ~ l1_vectsp_2('#skF_2',A_1533)
| ~ v5_vectsp_2('#skF_2',A_1533)
| ~ l3_vectsp_1(A_1533)
| ~ v2_vectsp_2(A_1533)
| v10_vectsp_1(A_1533)
| ~ v8_vectsp_1(A_1533)
| ~ v7_vectsp_1(A_1533)
| ~ v6_vectsp_1(A_1533)
| ~ v7_group_1(A_1533)
| ~ v4_group_1(A_1533)
| ~ v6_rlvect_1(A_1533)
| ~ v5_rlvect_1(A_1533)
| ~ v4_rlvect_1(A_1533)
| ~ v3_rlvect_1(A_1533)
| v3_struct_0(A_1533) ),
inference(resolution,[status(thm)],[c_35809,c_124]) ).
tff(c_35855,plain,
! [A_1533] :
( ~ v3_struct_0(k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| v3_struct_0('#skF_2')
| ~ l1_vectsp_2('#skF_2',A_1533)
| ~ v5_vectsp_2('#skF_2',A_1533)
| ~ l3_vectsp_1(A_1533)
| ~ v2_vectsp_2(A_1533)
| v10_vectsp_1(A_1533)
| ~ v8_vectsp_1(A_1533)
| ~ v7_vectsp_1(A_1533)
| ~ v6_vectsp_1(A_1533)
| ~ v7_group_1(A_1533)
| ~ v4_group_1(A_1533)
| ~ v6_rlvect_1(A_1533)
| ~ v5_rlvect_1(A_1533)
| ~ v4_rlvect_1(A_1533)
| ~ v3_rlvect_1(A_1533)
| v3_struct_0(A_1533) ),
inference(demodulation,[status(thm),theory(equality)],[c_24,c_22,c_20,c_18,c_35826]) ).
tff(c_35856,plain,
! [A_1533] :
( ~ v3_struct_0(k1_rmod_5(A_1533,'#skF_2','#skF_4'))
| ~ l1_vectsp_2('#skF_2',A_1533)
| ~ v5_vectsp_2('#skF_2',A_1533)
| ~ l3_vectsp_1(A_1533)
| ~ v2_vectsp_2(A_1533)
| v10_vectsp_1(A_1533)
| ~ v8_vectsp_1(A_1533)
| ~ v7_vectsp_1(A_1533)
| ~ v6_vectsp_1(A_1533)
| ~ v7_group_1(A_1533)
| ~ v4_group_1(A_1533)
| ~ v6_rlvect_1(A_1533)
| ~ v5_rlvect_1(A_1533)
| ~ v4_rlvect_1(A_1533)
| ~ v3_rlvect_1(A_1533)
| v3_struct_0(A_1533) ),
inference(negUnitSimplification,[status(thm)],[c_26,c_35855]) ).
tff(c_54107,plain,
( ~ l1_vectsp_2('#skF_2','#skF_1')
| ~ v5_vectsp_2('#skF_2','#skF_1')
| ~ l3_vectsp_1('#skF_1')
| ~ v2_vectsp_2('#skF_1')
| v10_vectsp_1('#skF_1')
| ~ v8_vectsp_1('#skF_1')
| ~ v7_vectsp_1('#skF_1')
| ~ v6_vectsp_1('#skF_1')
| ~ v7_group_1('#skF_1')
| ~ v4_group_1('#skF_1')
| ~ v6_rlvect_1('#skF_1')
| ~ v5_rlvect_1('#skF_1')
| ~ v4_rlvect_1('#skF_1')
| ~ v3_rlvect_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_54094,c_35856]) ).
tff(c_54110,plain,
( v10_vectsp_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_48,c_46,c_44,c_42,c_40,c_38,c_36,c_34,c_30,c_28,c_14,c_12,c_54107]) ).
tff(c_54112,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_52,c_32,c_54110]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ALG220+1 : TPTP v9.0.0. Released v3.4.0.
% 0.07/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.14/0.34 % Computer : n006.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Sun Apr 6 07:14:08 EDT 2025
% 0.14/0.34 % CPUTime :
% 26.00/11.87 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.00/11.88
% 26.00/11.88 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------