%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : ALG218+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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n031.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 52.55s 35.44s
% Output : CNFRefutation 52.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 18
% Syntax : Number of formulae : 153 ( 64 unt; 0 typ; 0 def)
% Number of atoms : 535 ( 79 equ)
% Maximal formula atoms : 24 ( 3 avg)
% Number of connectives : 646 ( 264 ~; 296 |; 61 &)
% ( 3 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 5 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 : 37 ( 35 usr; 1 prp; 0-3 aty)
% Number of functors : 44 ( 44 usr; 15 con; 0-5 aty)
% Number of variables : 112 ( 110 !; 2 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ v1_funct_2 > m2_relset_1 > m1_rmod_2 > m1_relset_1 > v5_vectsp_2 > v3_vectsp_2 > r2_hidden > r1_tarski > r1_rlvect_1 > 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 > v1_finset_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 > k7_rlvect_2 > k2_zfmisc_1 > k1_rmod_2 > #nlpp > u2_struct_0 > u1_struct_0 > u1_rlvect_1 > k1_zfmisc_1 > k1_tarski > k1_rlvect_1 > k1_xboole_0 > #skF_25 > #skF_6 > #skF_24 > #skF_19 > #skF_31 > #skF_22 > #skF_7 > #skF_10 > #skF_29 > #skF_26 > #skF_14 > #skF_18 > #skF_13 > #skF_2 > #skF_3 > #skF_1 > #skF_9 > #skF_8 > #skF_17 > #skF_11 > #skF_28 > #skF_27 > #skF_23 > #skF_16 > #skF_21 > #skF_5 > #skF_30 > #skF_15 > #skF_12 > #skF_4 > #skF_20
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(v2_vectsp_2,type,
v2_vectsp_2: $i > $o ).
tff('#skF_25',type,
'#skF_25': $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('#skF_6',type,
'#skF_6': ( $i * $i ) > $i ).
tff(v1_funct_1,type,
v1_funct_1: $i > $o ).
tff('#skF_24',type,
'#skF_24': $i > $i ).
tff(l3_vectsp_1,type,
l3_vectsp_1: $i > $o ).
tff(r2_hidden,type,
r2_hidden: ( $i * $i ) > $o ).
tff(g1_vectsp_2,type,
g1_vectsp_2: ( $i * $i * $i * $i * $i ) > $i ).
tff(k1_tarski,type,
k1_tarski: $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_19',type,
'#skF_19': $i > $i ).
tff(k1_rlvect_1,type,
k1_rlvect_1: $i > $i ).
tff('#skF_31',type,
'#skF_31': $i > $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(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_29',type,
'#skF_29': $i > $i ).
tff('#skF_26',type,
'#skF_26': $i ).
tff(k1_rmod_5,type,
k1_rmod_5: ( $i * $i * $i ) > $i ).
tff('#skF_14',type,
'#skF_14': $i ).
tff('#skF_18',type,
'#skF_18': ( $i * $i ) > $i ).
tff(v10_vectsp_1,type,
v10_vectsp_1: $i > $o ).
tff(v1_funct_2,type,
v1_funct_2: ( $i * $i * $i ) > $o ).
tff('#skF_13',type,
'#skF_13': $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(l2_struct_0,type,
l2_struct_0: $i > $o ).
tff(l2_vectsp_1,type,
l2_vectsp_1: $i > $o ).
tff('#skF_9',type,
'#skF_9': $i ).
tff(r1_rlvect_1,type,
r1_rlvect_1: ( $i * $i ) > $o ).
tff(k1_zfmisc_1,type,
k1_zfmisc_1: $i > $i ).
tff(l1_struct_0,type,
l1_struct_0: $i > $o ).
tff(k1_rmod_2,type,
k1_rmod_2: ( $i * $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_17',type,
'#skF_17': $i > $i ).
tff('#skF_11',type,
'#skF_11': $i > $i ).
tff(k7_rlvect_2,type,
k7_rlvect_2: ( $i * $i ) > $i ).
tff('#skF_28',type,
'#skF_28': $i ).
tff('#skF_27',type,
'#skF_27': $i ).
tff('#skF_23',type,
'#skF_23': $i ).
tff(v4_group_1,type,
v4_group_1: $i > $o ).
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('#skF_21',type,
'#skF_21': ( $i * $i ) > $i ).
tff(v1_xboole_0,type,
v1_xboole_0: $i > $o ).
tff(l1_group_1,type,
l1_group_1: $i > $o ).
tff(v1_finset_1,type,
v1_finset_1: $i > $o ).
tff('#skF_5',type,
'#skF_5': ( $i * $i ) > $i ).
tff('#skF_30',type,
'#skF_30': $i > $i ).
tff('#skF_15',type,
'#skF_15': ( $i * $i ) > $i ).
tff('#skF_12',type,
'#skF_12': $i ).
tff('#skF_4',type,
'#skF_4': ( $i * $i ) > $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_462,axiom,
! [A] :
? [B] : m1_subset_1(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_m1_subset_1) ).
tff(f_683,axiom,
? [A] : v1_xboole_0(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_xboole_0) ).
tff(f_878,axiom,
! [A] :
( v1_xboole_0(A)
=> ( A = k1_xboole_0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_boole) ).
tff(f_85,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)
& v5_vectsp_2(B,A)
& l1_vectsp_2(B,A) )
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
=> ~ ( ( k1_rmod_5(A,B,C) = k1_rmod_2(A,B) )
& ( C != k1_xboole_0 )
& ( C != k7_rlvect_2(B,k1_rlvect_1(B)) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_rmod_5) ).
tff(f_816,axiom,
! [A,B] :
( m1_subset_1(A,B)
=> ( v1_xboole_0(B)
| r2_hidden(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_subset) ).
tff(f_318,axiom,
! [A] :
( l3_vectsp_1(A)
=> ( l1_rlvect_1(A)
& l2_vectsp_1(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l3_vectsp_1) ).
tff(f_312,axiom,
! [A] :
( l2_vectsp_1(A)
=> ( l1_vectsp_1(A)
& l2_struct_0(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l2_vectsp_1) ).
tff(f_306,axiom,
! [A] :
( l2_struct_0(A)
=> l1_struct_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l2_struct_0) ).
tff(f_302,axiom,
! [A] :
( l1_struct_0(A)
=> ! [B] :
( l1_vectsp_2(B,A)
=> l1_rlvect_1(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_vectsp_2) ).
tff(f_291,axiom,
! [A] :
( l1_rlvect_1(A)
=> l2_struct_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_rlvect_1) ).
tff(f_867,axiom,
! [A,B,C] :
( ( r2_hidden(A,B)
& m1_subset_1(B,k1_zfmisc_1(C)) )
=> m1_subset_1(A,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
tff(f_283,axiom,
! [A,B] :
( ( ~ v3_struct_0(A)
& l1_struct_0(A)
& m1_subset_1(B,u1_struct_0(A)) )
=> ( v1_finset_1(k7_rlvect_2(A,B))
& m1_subset_1(k7_rlvect_2(A,B),k1_zfmisc_1(u1_struct_0(A))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k7_rlvect_2) ).
tff(f_749,axiom,
! [A,B] :
( ( ~ v3_struct_0(A)
& l1_struct_0(A)
& m1_subset_1(B,u1_struct_0(A)) )
=> ( k7_rlvect_2(A,B) = k1_tarski(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k7_rlvect_2) ).
tff(f_806,axiom,
! [A,B] :
( ( ~ v3_struct_0(B)
& v3_rlvect_1(B)
& v4_rlvect_1(B)
& v5_rlvect_1(B)
& v6_rlvect_1(B)
& v4_group_1(B)
& v7_group_1(B)
& v6_vectsp_1(B)
& v7_vectsp_1(B)
& v8_vectsp_1(B)
& ~ v10_vectsp_1(B)
& v2_vectsp_2(B)
& l3_vectsp_1(B) )
=> ! [C] :
( ( ~ v3_struct_0(C)
& v3_rlvect_1(C)
& v4_rlvect_1(C)
& v5_rlvect_1(C)
& v6_rlvect_1(C)
& v5_vectsp_2(C,B)
& l1_vectsp_2(C,B) )
=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(C)))
=> ( r2_hidden(A,D)
=> r1_rlvect_1(k1_rmod_5(B,C,D),A) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t10_rmod_5) ).
tff(f_861,axiom,
! [A,B] :
( ( ~ v3_struct_0(B)
& v3_rlvect_1(B)
& v4_rlvect_1(B)
& v5_rlvect_1(B)
& v6_rlvect_1(B)
& v4_group_1(B)
& v6_vectsp_1(B)
& v7_vectsp_1(B)
& v8_vectsp_1(B)
& l3_vectsp_1(B) )
=> ! [C] :
( ( ~ v3_struct_0(C)
& v3_rlvect_1(C)
& v4_rlvect_1(C)
& v5_rlvect_1(C)
& v6_rlvect_1(C)
& v5_vectsp_2(C,B)
& l1_vectsp_2(C,B) )
=> ( r1_rlvect_1(k1_rmod_2(B,C),A)
<=> ( A = k1_rlvect_1(C) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t46_rmod_2) ).
tff(f_398,axiom,
! [A] :
( l2_struct_0(A)
=> m1_subset_1(u2_struct_0(A),u1_struct_0(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_u2_struct_0) ).
tff(f_182,axiom,
! [A] :
( l2_struct_0(A)
=> m1_subset_1(k1_rlvect_1(A),u1_struct_0(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_rlvect_1) ).
tff(f_151,axiom,
! [A,B] :
( ( B = k1_tarski(A) )
<=> ! [C] :
( r2_hidden(C,B)
<=> ( C = A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_tarski) ).
tff(c_198,plain,
! [A_67] : m1_subset_1('#skF_17'(A_67),A_67),
inference(cnfTransformation,[status(thm)],[f_462]) ).
tff(c_276,plain,
v1_xboole_0('#skF_23'),
inference(cnfTransformation,[status(thm)],[f_683]) ).
tff(c_349,plain,
! [A_158] :
( ( k1_xboole_0 = A_158 )
| ~ v1_xboole_0(A_158) ),
inference(cnfTransformation,[status(thm)],[f_878]) ).
tff(c_362,plain,
k1_xboole_0 = '#skF_23',
inference(resolution,[status(thm)],[c_276,c_349]) ).
tff(c_4,plain,
k1_xboole_0 != '#skF_3',
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_364,plain,
'#skF_3' != '#skF_23',
inference(demodulation,[status(thm),theory(equality)],[c_362,c_4]) ).
tff(c_322,plain,
! [A_133,B_134] :
( r2_hidden(A_133,B_134)
| v1_xboole_0(B_134)
| ~ m1_subset_1(A_133,B_134) ),
inference(cnfTransformation,[status(thm)],[f_816]) ).
tff(c_22,plain,
~ v3_struct_0('#skF_2'),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_24,plain,
l3_vectsp_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_387,plain,
! [A_162] :
( l2_vectsp_1(A_162)
| ~ l3_vectsp_1(A_162) ),
inference(cnfTransformation,[status(thm)],[f_318]) ).
tff(c_394,plain,
l2_vectsp_1('#skF_1'),
inference(resolution,[status(thm)],[c_24,c_387]) ).
tff(c_434,plain,
! [A_165] :
( l2_struct_0(A_165)
| ~ l2_vectsp_1(A_165) ),
inference(cnfTransformation,[status(thm)],[f_312]) ).
tff(c_445,plain,
l2_struct_0('#skF_1'),
inference(resolution,[status(thm)],[c_394,c_434]) ).
tff(c_132,plain,
! [A_45] :
( l1_struct_0(A_45)
| ~ l2_struct_0(A_45) ),
inference(cnfTransformation,[status(thm)],[f_306]) ).
tff(c_467,plain,
l1_struct_0('#skF_1'),
inference(resolution,[status(thm)],[c_445,c_132]) ).
tff(c_10,plain,
l1_vectsp_2('#skF_2','#skF_1'),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_542,plain,
! [B_204,A_205] :
( l1_rlvect_1(B_204)
| ~ l1_vectsp_2(B_204,A_205)
| ~ l1_struct_0(A_205) ),
inference(cnfTransformation,[status(thm)],[f_302]) ).
tff(c_554,plain,
( l1_rlvect_1('#skF_2')
| ~ l1_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_10,c_542]) ).
tff(c_560,plain,
l1_rlvect_1('#skF_2'),
inference(demodulation,[status(thm),theory(equality)],[c_467,c_554]) ).
tff(c_124,plain,
! [A_40] :
( l2_struct_0(A_40)
| ~ l1_rlvect_1(A_40) ),
inference(cnfTransformation,[status(thm)],[f_291]) ).
tff(c_447,plain,
! [A_166] :
( l1_struct_0(A_166)
| ~ l2_struct_0(A_166) ),
inference(cnfTransformation,[status(thm)],[f_306]) ).
tff(c_457,plain,
! [A_40] :
( l1_struct_0(A_40)
| ~ l1_rlvect_1(A_40) ),
inference(resolution,[status(thm)],[c_124,c_447]) ).
tff(c_8,plain,
m1_subset_1('#skF_3',k1_zfmisc_1(u1_struct_0('#skF_2'))),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_1451,plain,
! [A_309,C_310,B_311] :
( m1_subset_1(A_309,C_310)
| ~ m1_subset_1(B_311,k1_zfmisc_1(C_310))
| ~ r2_hidden(A_309,B_311) ),
inference(cnfTransformation,[status(thm)],[f_867]) ).
tff(c_1480,plain,
! [A_309] :
( m1_subset_1(A_309,u1_struct_0('#skF_2'))
| ~ r2_hidden(A_309,'#skF_3') ),
inference(resolution,[status(thm)],[c_8,c_1451]) ).
tff(c_1735,plain,
! [A_351,B_352] :
( v1_finset_1(k7_rlvect_2(A_351,B_352))
| ~ m1_subset_1(B_352,u1_struct_0(A_351))
| ~ l1_struct_0(A_351)
| v3_struct_0(A_351) ),
inference(cnfTransformation,[status(thm)],[f_283]) ).
tff(c_1738,plain,
! [A_309] :
( v1_finset_1(k7_rlvect_2('#skF_2',A_309))
| ~ l1_struct_0('#skF_2')
| v3_struct_0('#skF_2')
| ~ r2_hidden(A_309,'#skF_3') ),
inference(resolution,[status(thm)],[c_1480,c_1735]) ).
tff(c_1755,plain,
! [A_309] :
( v1_finset_1(k7_rlvect_2('#skF_2',A_309))
| ~ l1_struct_0('#skF_2')
| ~ r2_hidden(A_309,'#skF_3') ),
inference(negUnitSimplification,[status(thm)],[c_22,c_1738]) ).
tff(c_1771,plain,
~ l1_struct_0('#skF_2'),
inference(splitLeft,[status(thm)],[c_1755]) ).
tff(c_1774,plain,
~ l1_rlvect_1('#skF_2'),
inference(resolution,[status(thm)],[c_457,c_1771]) ).
tff(c_1781,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_560,c_1774]) ).
tff(c_1783,plain,
l1_struct_0('#skF_2'),
inference(splitRight,[status(thm)],[c_1755]) ).
tff(c_2473,plain,
! [A_399,B_400] :
( ( k7_rlvect_2(A_399,B_400) = k1_tarski(B_400) )
| ~ m1_subset_1(B_400,u1_struct_0(A_399))
| ~ l1_struct_0(A_399)
| v3_struct_0(A_399) ),
inference(cnfTransformation,[status(thm)],[f_749]) ).
tff(c_2476,plain,
! [A_309] :
( ( k7_rlvect_2('#skF_2',A_309) = k1_tarski(A_309) )
| ~ l1_struct_0('#skF_2')
| v3_struct_0('#skF_2')
| ~ r2_hidden(A_309,'#skF_3') ),
inference(resolution,[status(thm)],[c_1480,c_2473]) ).
tff(c_2493,plain,
! [A_309] :
( ( k7_rlvect_2('#skF_2',A_309) = k1_tarski(A_309) )
| v3_struct_0('#skF_2')
| ~ r2_hidden(A_309,'#skF_3') ),
inference(demodulation,[status(thm),theory(equality)],[c_1783,c_2476]) ).
tff(c_2554,plain,
! [A_402] :
( ( k7_rlvect_2('#skF_2',A_402) = k1_tarski(A_402) )
| ~ r2_hidden(A_402,'#skF_3') ),
inference(negUnitSimplification,[status(thm)],[c_22,c_2493]) ).
tff(c_2573,plain,
! [A_133] :
( ( k7_rlvect_2('#skF_2',A_133) = k1_tarski(A_133) )
| v1_xboole_0('#skF_3')
| ~ m1_subset_1(A_133,'#skF_3') ),
inference(resolution,[status(thm)],[c_322,c_2554]) ).
tff(c_2873,plain,
v1_xboole_0('#skF_3'),
inference(splitLeft,[status(thm)],[c_2573]) ).
tff(c_336,plain,
! [A_147] :
( ( k1_xboole_0 = A_147 )
| ~ v1_xboole_0(A_147) ),
inference(cnfTransformation,[status(thm)],[f_878]) ).
tff(c_363,plain,
! [A_147] :
( ( A_147 = '#skF_23' )
| ~ v1_xboole_0(A_147) ),
inference(demodulation,[status(thm),theory(equality)],[c_362,c_336]) ).
tff(c_2885,plain,
'#skF_3' = '#skF_23',
inference(resolution,[status(thm)],[c_2873,c_363]) ).
tff(c_2893,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_364,c_2885]) ).
tff(c_2895,plain,
~ v1_xboole_0('#skF_3'),
inference(splitRight,[status(thm)],[c_2573]) ).
tff(c_48,plain,
~ v3_struct_0('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_46,plain,
v3_rlvect_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_44,plain,
v4_rlvect_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_42,plain,
v5_rlvect_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_40,plain,
v6_rlvect_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_38,plain,
v4_group_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_34,plain,
v6_vectsp_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_32,plain,
v7_vectsp_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_30,plain,
v8_vectsp_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_20,plain,
v3_rlvect_1('#skF_2'),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_18,plain,
v4_rlvect_1('#skF_2'),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_16,plain,
v5_rlvect_1('#skF_2'),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_14,plain,
v6_rlvect_1('#skF_2'),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_12,plain,
v5_vectsp_2('#skF_2','#skF_1'),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_28,plain,
~ v10_vectsp_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_36,plain,
v7_group_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_26,plain,
v2_vectsp_2('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_6,plain,
k1_rmod_5('#skF_1','#skF_2','#skF_3') = k1_rmod_2('#skF_1','#skF_2'),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_20424,plain,
! [B_1041,C_1042,D_1043,A_1044] :
( r1_rlvect_1(k1_rmod_5(B_1041,C_1042,D_1043),A_1044)
| ~ r2_hidden(A_1044,D_1043)
| ~ m1_subset_1(D_1043,k1_zfmisc_1(u1_struct_0(C_1042)))
| ~ l1_vectsp_2(C_1042,B_1041)
| ~ v5_vectsp_2(C_1042,B_1041)
| ~ v6_rlvect_1(C_1042)
| ~ v5_rlvect_1(C_1042)
| ~ v4_rlvect_1(C_1042)
| ~ v3_rlvect_1(C_1042)
| v3_struct_0(C_1042)
| ~ l3_vectsp_1(B_1041)
| ~ v2_vectsp_2(B_1041)
| v10_vectsp_1(B_1041)
| ~ v8_vectsp_1(B_1041)
| ~ v7_vectsp_1(B_1041)
| ~ v6_vectsp_1(B_1041)
| ~ v7_group_1(B_1041)
| ~ v4_group_1(B_1041)
| ~ v6_rlvect_1(B_1041)
| ~ v5_rlvect_1(B_1041)
| ~ v4_rlvect_1(B_1041)
| ~ v3_rlvect_1(B_1041)
| v3_struct_0(B_1041) ),
inference(cnfTransformation,[status(thm)],[f_806]) ).
tff(c_20487,plain,
! [B_1041,A_1044] :
( r1_rlvect_1(k1_rmod_5(B_1041,'#skF_2','#skF_3'),A_1044)
| ~ r2_hidden(A_1044,'#skF_3')
| ~ l1_vectsp_2('#skF_2',B_1041)
| ~ v5_vectsp_2('#skF_2',B_1041)
| ~ 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(B_1041)
| ~ v2_vectsp_2(B_1041)
| v10_vectsp_1(B_1041)
| ~ v8_vectsp_1(B_1041)
| ~ v7_vectsp_1(B_1041)
| ~ v6_vectsp_1(B_1041)
| ~ v7_group_1(B_1041)
| ~ v4_group_1(B_1041)
| ~ v6_rlvect_1(B_1041)
| ~ v5_rlvect_1(B_1041)
| ~ v4_rlvect_1(B_1041)
| ~ v3_rlvect_1(B_1041)
| v3_struct_0(B_1041) ),
inference(resolution,[status(thm)],[c_8,c_20424]) ).
tff(c_20530,plain,
! [B_1041,A_1044] :
( r1_rlvect_1(k1_rmod_5(B_1041,'#skF_2','#skF_3'),A_1044)
| ~ r2_hidden(A_1044,'#skF_3')
| ~ l1_vectsp_2('#skF_2',B_1041)
| ~ v5_vectsp_2('#skF_2',B_1041)
| v3_struct_0('#skF_2')
| ~ l3_vectsp_1(B_1041)
| ~ v2_vectsp_2(B_1041)
| v10_vectsp_1(B_1041)
| ~ v8_vectsp_1(B_1041)
| ~ v7_vectsp_1(B_1041)
| ~ v6_vectsp_1(B_1041)
| ~ v7_group_1(B_1041)
| ~ v4_group_1(B_1041)
| ~ v6_rlvect_1(B_1041)
| ~ v5_rlvect_1(B_1041)
| ~ v4_rlvect_1(B_1041)
| ~ v3_rlvect_1(B_1041)
| v3_struct_0(B_1041) ),
inference(demodulation,[status(thm),theory(equality)],[c_20,c_18,c_16,c_14,c_20487]) ).
tff(c_31960,plain,
! [B_1276,A_1277] :
( r1_rlvect_1(k1_rmod_5(B_1276,'#skF_2','#skF_3'),A_1277)
| ~ r2_hidden(A_1277,'#skF_3')
| ~ l1_vectsp_2('#skF_2',B_1276)
| ~ v5_vectsp_2('#skF_2',B_1276)
| ~ l3_vectsp_1(B_1276)
| ~ v2_vectsp_2(B_1276)
| v10_vectsp_1(B_1276)
| ~ v8_vectsp_1(B_1276)
| ~ v7_vectsp_1(B_1276)
| ~ v6_vectsp_1(B_1276)
| ~ v7_group_1(B_1276)
| ~ v4_group_1(B_1276)
| ~ v6_rlvect_1(B_1276)
| ~ v5_rlvect_1(B_1276)
| ~ v4_rlvect_1(B_1276)
| ~ v3_rlvect_1(B_1276)
| v3_struct_0(B_1276) ),
inference(negUnitSimplification,[status(thm)],[c_22,c_20530]) ).
tff(c_31963,plain,
! [A_1277] :
( r1_rlvect_1(k1_rmod_2('#skF_1','#skF_2'),A_1277)
| ~ r2_hidden(A_1277,'#skF_3')
| ~ 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(superposition,[status(thm),theory(equality)],[c_6,c_31960]) ).
tff(c_31965,plain,
! [A_1277] :
( r1_rlvect_1(k1_rmod_2('#skF_1','#skF_2'),A_1277)
| ~ r2_hidden(A_1277,'#skF_3')
| v10_vectsp_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_46,c_44,c_42,c_40,c_38,c_36,c_34,c_32,c_30,c_26,c_24,c_12,c_10,c_31963]) ).
tff(c_31967,plain,
! [A_1278] :
( r1_rlvect_1(k1_rmod_2('#skF_1','#skF_2'),A_1278)
| ~ r2_hidden(A_1278,'#skF_3') ),
inference(negUnitSimplification,[status(thm)],[c_48,c_28,c_31965]) ).
tff(c_330,plain,
! [C_140,A_137,B_138] :
( ( k1_rlvect_1(C_140) = A_137 )
| ~ r1_rlvect_1(k1_rmod_2(B_138,C_140),A_137)
| ~ l1_vectsp_2(C_140,B_138)
| ~ v5_vectsp_2(C_140,B_138)
| ~ v6_rlvect_1(C_140)
| ~ v5_rlvect_1(C_140)
| ~ v4_rlvect_1(C_140)
| ~ v3_rlvect_1(C_140)
| v3_struct_0(C_140)
| ~ l3_vectsp_1(B_138)
| ~ v8_vectsp_1(B_138)
| ~ v7_vectsp_1(B_138)
| ~ v6_vectsp_1(B_138)
| ~ v4_group_1(B_138)
| ~ v6_rlvect_1(B_138)
| ~ v5_rlvect_1(B_138)
| ~ v4_rlvect_1(B_138)
| ~ v3_rlvect_1(B_138)
| v3_struct_0(B_138) ),
inference(cnfTransformation,[status(thm)],[f_861]) ).
tff(c_31970,plain,
! [A_1278] :
( ( k1_rlvect_1('#skF_2') = A_1278 )
| ~ 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')
| ~ 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')
| ~ r2_hidden(A_1278,'#skF_3') ),
inference(resolution,[status(thm)],[c_31967,c_330]) ).
tff(c_31973,plain,
! [A_1278] :
( ( k1_rlvect_1('#skF_2') = A_1278 )
| v3_struct_0('#skF_2')
| v3_struct_0('#skF_1')
| ~ r2_hidden(A_1278,'#skF_3') ),
inference(demodulation,[status(thm),theory(equality)],[c_46,c_44,c_42,c_40,c_38,c_34,c_32,c_30,c_24,c_20,c_18,c_16,c_14,c_12,c_10,c_31970]) ).
tff(c_31975,plain,
! [A_1279] :
( ( k1_rlvect_1('#skF_2') = A_1279 )
| ~ r2_hidden(A_1279,'#skF_3') ),
inference(negUnitSimplification,[status(thm)],[c_48,c_22,c_31973]) ).
tff(c_32022,plain,
! [A_133] :
( ( k1_rlvect_1('#skF_2') = A_133 )
| v1_xboole_0('#skF_3')
| ~ m1_subset_1(A_133,'#skF_3') ),
inference(resolution,[status(thm)],[c_322,c_31975]) ).
tff(c_32050,plain,
! [A_1280] :
( ( k1_rlvect_1('#skF_2') = A_1280 )
| ~ m1_subset_1(A_1280,'#skF_3') ),
inference(negUnitSimplification,[status(thm)],[c_2895,c_32022]) ).
tff(c_32106,plain,
k1_rlvect_1('#skF_2') = '#skF_17'('#skF_3'),
inference(resolution,[status(thm)],[c_198,c_32050]) ).
tff(c_176,plain,
! [A_58] :
( m1_subset_1(u2_struct_0(A_58),u1_struct_0(A_58))
| ~ l2_struct_0(A_58) ),
inference(cnfTransformation,[status(thm)],[f_398]) ).
tff(c_20823,plain,
! [A_1051] :
( ( k7_rlvect_2(A_1051,u2_struct_0(A_1051)) = k1_tarski(u2_struct_0(A_1051)) )
| ~ l1_struct_0(A_1051)
| v3_struct_0(A_1051)
| ~ l2_struct_0(A_1051) ),
inference(resolution,[status(thm)],[c_176,c_2473]) ).
tff(c_1782,plain,
! [A_309] :
( v1_finset_1(k7_rlvect_2('#skF_2',A_309))
| ~ r2_hidden(A_309,'#skF_3') ),
inference(splitRight,[status(thm)],[c_1755]) ).
tff(c_20844,plain,
( v1_finset_1(k1_tarski(u2_struct_0('#skF_2')))
| ~ r2_hidden(u2_struct_0('#skF_2'),'#skF_3')
| ~ l1_struct_0('#skF_2')
| v3_struct_0('#skF_2')
| ~ l2_struct_0('#skF_2') ),
inference(superposition,[status(thm),theory(equality)],[c_20823,c_1782]) ).
tff(c_20856,plain,
( v1_finset_1(k1_tarski(u2_struct_0('#skF_2')))
| ~ r2_hidden(u2_struct_0('#skF_2'),'#skF_3')
| v3_struct_0('#skF_2')
| ~ l2_struct_0('#skF_2') ),
inference(demodulation,[status(thm),theory(equality)],[c_1783,c_20844]) ).
tff(c_20857,plain,
( v1_finset_1(k1_tarski(u2_struct_0('#skF_2')))
| ~ r2_hidden(u2_struct_0('#skF_2'),'#skF_3')
| ~ l2_struct_0('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_22,c_20856]) ).
tff(c_20879,plain,
~ l2_struct_0('#skF_2'),
inference(splitLeft,[status(thm)],[c_20857]) ).
tff(c_20883,plain,
~ l1_rlvect_1('#skF_2'),
inference(resolution,[status(thm)],[c_124,c_20879]) ).
tff(c_20887,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_560,c_20883]) ).
tff(c_20889,plain,
l2_struct_0('#skF_2'),
inference(splitRight,[status(thm)],[c_20857]) ).
tff(c_100,plain,
! [A_31] :
( m1_subset_1(k1_rlvect_1(A_31),u1_struct_0(A_31))
| ~ l2_struct_0(A_31) ),
inference(cnfTransformation,[status(thm)],[f_182]) ).
tff(c_21034,plain,
! [A_1054] :
( ( k7_rlvect_2(A_1054,k1_rlvect_1(A_1054)) = k1_tarski(k1_rlvect_1(A_1054)) )
| ~ l1_struct_0(A_1054)
| v3_struct_0(A_1054)
| ~ l2_struct_0(A_1054) ),
inference(resolution,[status(thm)],[c_100,c_2473]) ).
tff(c_2,plain,
k7_rlvect_2('#skF_2',k1_rlvect_1('#skF_2')) != '#skF_3',
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_21058,plain,
( ( k1_tarski(k1_rlvect_1('#skF_2')) != '#skF_3' )
| ~ l1_struct_0('#skF_2')
| v3_struct_0('#skF_2')
| ~ l2_struct_0('#skF_2') ),
inference(superposition,[status(thm),theory(equality)],[c_21034,c_2]) ).
tff(c_21073,plain,
( ( k1_tarski(k1_rlvect_1('#skF_2')) != '#skF_3' )
| v3_struct_0('#skF_2') ),
inference(demodulation,[status(thm),theory(equality)],[c_20889,c_1783,c_21058]) ).
tff(c_21074,plain,
k1_tarski(k1_rlvect_1('#skF_2')) != '#skF_3',
inference(negUnitSimplification,[status(thm)],[c_22,c_21073]) ).
tff(c_32155,plain,
k1_tarski('#skF_17'('#skF_3')) != '#skF_3',
inference(demodulation,[status(thm),theory(equality)],[c_32106,c_21074]) ).
tff(c_26808,plain,
! [B_1164,A_1165] :
( r1_rlvect_1(k1_rmod_5(B_1164,'#skF_2','#skF_3'),A_1165)
| ~ r2_hidden(A_1165,'#skF_3')
| ~ l1_vectsp_2('#skF_2',B_1164)
| ~ v5_vectsp_2('#skF_2',B_1164)
| ~ l3_vectsp_1(B_1164)
| ~ v2_vectsp_2(B_1164)
| v10_vectsp_1(B_1164)
| ~ v8_vectsp_1(B_1164)
| ~ v7_vectsp_1(B_1164)
| ~ v6_vectsp_1(B_1164)
| ~ v7_group_1(B_1164)
| ~ v4_group_1(B_1164)
| ~ v6_rlvect_1(B_1164)
| ~ v5_rlvect_1(B_1164)
| ~ v4_rlvect_1(B_1164)
| ~ v3_rlvect_1(B_1164)
| v3_struct_0(B_1164) ),
inference(negUnitSimplification,[status(thm)],[c_22,c_20530]) ).
tff(c_26811,plain,
! [A_1165] :
( r1_rlvect_1(k1_rmod_2('#skF_1','#skF_2'),A_1165)
| ~ r2_hidden(A_1165,'#skF_3')
| ~ 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(superposition,[status(thm),theory(equality)],[c_6,c_26808]) ).
tff(c_26813,plain,
! [A_1165] :
( r1_rlvect_1(k1_rmod_2('#skF_1','#skF_2'),A_1165)
| ~ r2_hidden(A_1165,'#skF_3')
| v10_vectsp_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_46,c_44,c_42,c_40,c_38,c_36,c_34,c_32,c_30,c_26,c_24,c_12,c_10,c_26811]) ).
tff(c_26815,plain,
! [A_1166] :
( r1_rlvect_1(k1_rmod_2('#skF_1','#skF_2'),A_1166)
| ~ r2_hidden(A_1166,'#skF_3') ),
inference(negUnitSimplification,[status(thm)],[c_48,c_28,c_26813]) ).
tff(c_26818,plain,
! [A_1166] :
( ( k1_rlvect_1('#skF_2') = A_1166 )
| ~ 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')
| ~ 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')
| ~ r2_hidden(A_1166,'#skF_3') ),
inference(resolution,[status(thm)],[c_26815,c_330]) ).
tff(c_26821,plain,
! [A_1166] :
( ( k1_rlvect_1('#skF_2') = A_1166 )
| v3_struct_0('#skF_2')
| v3_struct_0('#skF_1')
| ~ r2_hidden(A_1166,'#skF_3') ),
inference(demodulation,[status(thm),theory(equality)],[c_46,c_44,c_42,c_40,c_38,c_34,c_32,c_30,c_24,c_20,c_18,c_16,c_14,c_12,c_10,c_26818]) ).
tff(c_26823,plain,
! [A_1167] :
( ( k1_rlvect_1('#skF_2') = A_1167 )
| ~ r2_hidden(A_1167,'#skF_3') ),
inference(negUnitSimplification,[status(thm)],[c_48,c_22,c_26821]) ).
tff(c_26859,plain,
! [A_133] :
( ( k1_rlvect_1('#skF_2') = A_133 )
| v1_xboole_0('#skF_3')
| ~ m1_subset_1(A_133,'#skF_3') ),
inference(resolution,[status(thm)],[c_322,c_26823]) ).
tff(c_26877,plain,
! [A_1168] :
( ( k1_rlvect_1('#skF_2') = A_1168 )
| ~ m1_subset_1(A_1168,'#skF_3') ),
inference(negUnitSimplification,[status(thm)],[c_2895,c_26859]) ).
tff(c_26925,plain,
k1_rlvect_1('#skF_2') = '#skF_17'('#skF_3'),
inference(resolution,[status(thm)],[c_198,c_26877]) ).
tff(c_21055,plain,
( v1_finset_1(k1_tarski(k1_rlvect_1('#skF_2')))
| ~ r2_hidden(k1_rlvect_1('#skF_2'),'#skF_3')
| ~ l1_struct_0('#skF_2')
| v3_struct_0('#skF_2')
| ~ l2_struct_0('#skF_2') ),
inference(superposition,[status(thm),theory(equality)],[c_21034,c_1782]) ).
tff(c_21070,plain,
( v1_finset_1(k1_tarski(k1_rlvect_1('#skF_2')))
| ~ r2_hidden(k1_rlvect_1('#skF_2'),'#skF_3')
| v3_struct_0('#skF_2') ),
inference(demodulation,[status(thm),theory(equality)],[c_20889,c_1783,c_21055]) ).
tff(c_21071,plain,
( v1_finset_1(k1_tarski(k1_rlvect_1('#skF_2')))
| ~ r2_hidden(k1_rlvect_1('#skF_2'),'#skF_3') ),
inference(negUnitSimplification,[status(thm)],[c_22,c_21070]) ).
tff(c_21076,plain,
~ r2_hidden(k1_rlvect_1('#skF_2'),'#skF_3'),
inference(splitLeft,[status(thm)],[c_21071]) ).
tff(c_21082,plain,
( v1_xboole_0('#skF_3')
| ~ m1_subset_1(k1_rlvect_1('#skF_2'),'#skF_3') ),
inference(resolution,[status(thm)],[c_322,c_21076]) ).
tff(c_21087,plain,
~ m1_subset_1(k1_rlvect_1('#skF_2'),'#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2895,c_21082]) ).
tff(c_26929,plain,
~ m1_subset_1('#skF_17'('#skF_3'),'#skF_3'),
inference(demodulation,[status(thm),theory(equality)],[c_26925,c_21087]) ).
tff(c_26935,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_198,c_26929]) ).
tff(c_26937,plain,
r2_hidden(k1_rlvect_1('#skF_2'),'#skF_3'),
inference(splitRight,[status(thm)],[c_21071]) ).
tff(c_32153,plain,
r2_hidden('#skF_17'('#skF_3'),'#skF_3'),
inference(demodulation,[status(thm),theory(equality)],[c_32106,c_26937]) ).
tff(c_88,plain,
! [A_16,B_17] :
( ( '#skF_4'(A_16,B_17) = A_16 )
| r2_hidden('#skF_5'(A_16,B_17),B_17)
| ( k1_tarski(A_16) = B_17 ) ),
inference(cnfTransformation,[status(thm)],[f_151]) ).
tff(c_32045,plain,
! [A_16] :
( ( k1_rlvect_1('#skF_2') = '#skF_5'(A_16,'#skF_3') )
| ( '#skF_4'(A_16,'#skF_3') = A_16 )
| ( k1_tarski(A_16) = '#skF_3' ) ),
inference(resolution,[status(thm)],[c_88,c_31975]) ).
tff(c_69674,plain,
! [A_1948] :
( ( '#skF_5'(A_1948,'#skF_3') = '#skF_17'('#skF_3') )
| ( '#skF_4'(A_1948,'#skF_3') = A_1948 )
| ( k1_tarski(A_1948) = '#skF_3' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_32106,c_32045]) ).
tff(c_70371,plain,
( ( '#skF_5'('#skF_17'('#skF_3'),'#skF_3') = '#skF_17'('#skF_3') )
| ( '#skF_4'('#skF_17'('#skF_3'),'#skF_3') = '#skF_17'('#skF_3') ) ),
inference(superposition,[status(thm),theory(equality)],[c_69674,c_32155]) ).
tff(c_130449,plain,
'#skF_4'('#skF_17'('#skF_3'),'#skF_3') = '#skF_17'('#skF_3'),
inference(splitLeft,[status(thm)],[c_70371]) ).
tff(c_86,plain,
! [A_16,B_17] :
( ~ r2_hidden('#skF_4'(A_16,B_17),B_17)
| r2_hidden('#skF_5'(A_16,B_17),B_17)
| ( k1_tarski(A_16) = B_17 ) ),
inference(cnfTransformation,[status(thm)],[f_151]) ).
tff(c_32044,plain,
! [A_16] :
( ( k1_rlvect_1('#skF_2') = '#skF_5'(A_16,'#skF_3') )
| ~ r2_hidden('#skF_4'(A_16,'#skF_3'),'#skF_3')
| ( k1_tarski(A_16) = '#skF_3' ) ),
inference(resolution,[status(thm)],[c_86,c_31975]) ).
tff(c_93179,plain,
! [A_16] :
( ( '#skF_5'(A_16,'#skF_3') = '#skF_17'('#skF_3') )
| ~ r2_hidden('#skF_4'(A_16,'#skF_3'),'#skF_3')
| ( k1_tarski(A_16) = '#skF_3' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_32106,c_32044]) ).
tff(c_130658,plain,
( ( '#skF_5'('#skF_17'('#skF_3'),'#skF_3') = '#skF_17'('#skF_3') )
| ~ r2_hidden('#skF_17'('#skF_3'),'#skF_3')
| ( k1_tarski('#skF_17'('#skF_3')) = '#skF_3' ) ),
inference(superposition,[status(thm),theory(equality)],[c_130449,c_93179]) ).
tff(c_130691,plain,
( ( '#skF_5'('#skF_17'('#skF_3'),'#skF_3') = '#skF_17'('#skF_3') )
| ( k1_tarski('#skF_17'('#skF_3')) = '#skF_3' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_32153,c_130658]) ).
tff(c_130692,plain,
'#skF_5'('#skF_17'('#skF_3'),'#skF_3') = '#skF_17'('#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_32155,c_130691]) ).
tff(c_1950,plain,
! [A_367,B_368] :
( ~ r2_hidden('#skF_4'(A_367,B_368),B_368)
| ( '#skF_5'(A_367,B_368) != A_367 )
| ( k1_tarski(A_367) = B_368 ) ),
inference(cnfTransformation,[status(thm)],[f_151]) ).
tff(c_1958,plain,
! [A_367,B_134] :
( ( '#skF_5'(A_367,B_134) != A_367 )
| ( k1_tarski(A_367) = B_134 )
| v1_xboole_0(B_134)
| ~ m1_subset_1('#skF_4'(A_367,B_134),B_134) ),
inference(resolution,[status(thm)],[c_322,c_1950]) ).
tff(c_130665,plain,
( ( '#skF_5'('#skF_17'('#skF_3'),'#skF_3') != '#skF_17'('#skF_3') )
| ( k1_tarski('#skF_17'('#skF_3')) = '#skF_3' )
| v1_xboole_0('#skF_3')
| ~ m1_subset_1('#skF_17'('#skF_3'),'#skF_3') ),
inference(superposition,[status(thm),theory(equality)],[c_130449,c_1958]) ).
tff(c_130700,plain,
( ( '#skF_5'('#skF_17'('#skF_3'),'#skF_3') != '#skF_17'('#skF_3') )
| ( k1_tarski('#skF_17'('#skF_3')) = '#skF_3' )
| v1_xboole_0('#skF_3') ),
inference(demodulation,[status(thm),theory(equality)],[c_198,c_130665]) ).
tff(c_130701,plain,
'#skF_5'('#skF_17'('#skF_3'),'#skF_3') != '#skF_17'('#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2895,c_32155,c_130700]) ).
tff(c_130928,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_130692,c_130701]) ).
tff(c_130930,plain,
'#skF_4'('#skF_17'('#skF_3'),'#skF_3') != '#skF_17'('#skF_3'),
inference(splitRight,[status(thm)],[c_70371]) ).
tff(c_130929,plain,
'#skF_5'('#skF_17'('#skF_3'),'#skF_3') = '#skF_17'('#skF_3'),
inference(splitRight,[status(thm)],[c_70371]) ).
tff(c_84,plain,
! [A_16,B_17] :
( ( '#skF_4'(A_16,B_17) = A_16 )
| ( '#skF_5'(A_16,B_17) != A_16 )
| ( k1_tarski(A_16) = B_17 ) ),
inference(cnfTransformation,[status(thm)],[f_151]) ).
tff(c_131040,plain,
( ( '#skF_4'('#skF_17'('#skF_3'),'#skF_3') = '#skF_17'('#skF_3') )
| ( k1_tarski('#skF_17'('#skF_3')) = '#skF_3' ) ),
inference(superposition,[status(thm),theory(equality)],[c_130929,c_84]) ).
tff(c_131124,plain,
'#skF_4'('#skF_17'('#skF_3'),'#skF_3') = '#skF_17'('#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_32155,c_131040]) ).
tff(c_131254,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_130930,c_131124]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ALG218+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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.39 % Computer : n031.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8042.1875MB
% 0.13/0.39 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sun Apr 6 07:11:52 EDT 2025
% 0.13/0.39 % CPUTime :
% 52.55/35.44 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 52.55/35.46
% 52.55/35.46 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------