%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : LAT323+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 : n032.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 07:11:53 PM UTC 2025
% Result : Theorem 32.08s 16.68s
% Output : CNFRefutation 32.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 18
% Syntax : Number of formulae : 170 ( 63 unt; 0 typ; 0 def)
% Number of atoms : 545 ( 46 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 611 ( 236 ~; 268 |; 71 &)
% ( 4 <=>; 32 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 4 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 : 41 ( 39 usr; 1 prp; 0-3 aty)
% Number of functors : 43 ( 43 usr; 21 con; 0-3 aty)
% Number of variables : 96 ( 96 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ v1_partfun1 > v1_funct_2 > m2_relset_1 > m1_relset_1 > v2_binop_1 > v1_filter_0 > v1_binop_1 > r2_hidden > r2_filter_2 > r1_tarski > m2_lattice4 > m2_filter_2 > m1_subset_1 > m1_filter_2 > m1_filter_0 > v9_lattices > v8_lattices > v7_lattices > v6_lattices > v5_lattices > v4_lattices > v3_struct_0 > v3_lattices > v2_funct_1 > v1_xboole_0 > v1_relat_1 > v1_funct_1 > v17_lattices > v16_lattices > v15_lattices > v14_lattices > v13_lattices > v12_lattices > v11_lattices > v10_lattices > l3_lattices > l2_lattices > l1_struct_0 > l1_lattices > g3_lattices > k7_lattices > k7_filter_2 > k5_filter_2 > k2_zfmisc_1 > k15_filter_2 > #nlpp > u2_lattices > u1_struct_0 > u1_lattices > k1_zfmisc_1 > k1_lattice2 > k1_xboole_0 > #skF_9 > #skF_21 > #skF_18 > #skF_17 > #skF_24 > #skF_31 > #skF_15 > #skF_25 > #skF_8 > #skF_19 > #skF_7 > #skF_16 > #skF_14 > #skF_29 > #skF_26 > #skF_5 > #skF_6 > #skF_2 > #skF_10 > #skF_3 > #skF_1 > #skF_30 > #skF_13 > #skF_4 > #skF_11 > #skF_22 > #skF_28 > #skF_27 > #skF_23 > #skF_12 > #skF_20
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(l3_lattices,type,
l3_lattices: $i > $o ).
tff(k1_lattice2,type,
k1_lattice2: $i > $i ).
tff('#skF_9',type,
'#skF_9': $i > $i ).
tff(v12_lattices,type,
v12_lattices: $i > $o ).
tff(m2_relset_1,type,
m2_relset_1: ( $i * $i * $i ) > $o ).
tff('#skF_21',type,
'#skF_21': $i > $i ).
tff(k5_filter_2,type,
k5_filter_2: ( $i * $i ) > $i ).
tff(l2_lattices,type,
l2_lattices: $i > $o ).
tff(v1_funct_1,type,
v1_funct_1: $i > $o ).
tff(v2_funct_1,type,
v2_funct_1: $i > $o ).
tff('#skF_18',type,
'#skF_18': $i ).
tff('#skF_17',type,
'#skF_17': $i ).
tff('#skF_24',type,
'#skF_24': $i > $i ).
tff(r2_hidden,type,
r2_hidden: ( $i * $i ) > $o ).
tff(v1_filter_0,type,
v1_filter_0: ( $i * $i ) > $o ).
tff('#skF_31',type,
'#skF_31': $i ).
tff('#skF_15',type,
'#skF_15': $i ).
tff(v1_partfun1,type,
v1_partfun1: ( $i * $i * $i ) > $o ).
tff('#skF_25',type,
'#skF_25': $i ).
tff(k1_xboole_0,type,
k1_xboole_0: $i ).
tff(m2_lattice4,type,
m2_lattice4: ( $i * $i ) > $o ).
tff(m2_filter_2,type,
m2_filter_2: ( $i * $i ) > $o ).
tff(l1_lattices,type,
l1_lattices: $i > $o ).
tff('#skF_8',type,
'#skF_8': $i > $i ).
tff('#skF_19',type,
'#skF_19': $i ).
tff('#skF_7',type,
'#skF_7': $i ).
tff(r1_tarski,type,
r1_tarski: ( $i * $i ) > $o ).
tff(m1_relset_1,type,
m1_relset_1: ( $i * $i * $i ) > $o ).
tff(v17_lattices,type,
v17_lattices: $i > $o ).
tff('#skF_16',type,
'#skF_16': $i ).
tff('#skF_14',type,
'#skF_14': ( $i * $i ) > $i ).
tff('#skF_29',type,
'#skF_29': $i > $i ).
tff('#skF_26',type,
'#skF_26': $i ).
tff('#skF_5',type,
'#skF_5': $i ).
tff(v1_funct_2,type,
v1_funct_2: ( $i * $i * $i ) > $o ).
tff(v4_lattices,type,
v4_lattices: $i > $o ).
tff(m1_filter_0,type,
m1_filter_0: ( $i * $i ) > $o ).
tff('#skF_6',type,
'#skF_6': $i ).
tff(v6_lattices,type,
v6_lattices: $i > $o ).
tff('#skF_2',type,
'#skF_2': $i ).
tff(u2_lattices,type,
u2_lattices: $i > $i ).
tff(v9_lattices,type,
v9_lattices: $i > $o ).
tff('#skF_10',type,
'#skF_10': ( $i * $i ) > $i ).
tff('#skF_3',type,
'#skF_3': $i ).
tff('#skF_1',type,
'#skF_1': $i ).
tff(m1_filter_2,type,
m1_filter_2: ( $i * $i ) > $o ).
tff(u1_lattices,type,
u1_lattices: $i > $i ).
tff(g3_lattices,type,
g3_lattices: ( $i * $i * $i ) > $i ).
tff(v5_lattices,type,
v5_lattices: $i > $o ).
tff(v10_lattices,type,
v10_lattices: $i > $o ).
tff(k1_zfmisc_1,type,
k1_zfmisc_1: $i > $i ).
tff(l1_struct_0,type,
l1_struct_0: $i > $o ).
tff(k15_filter_2,type,
k15_filter_2: ( $i * $i ) > $i ).
tff('#skF_30',type,
'#skF_30': $i ).
tff('#skF_13',type,
'#skF_13': $i > $i ).
tff(v1_binop_1,type,
v1_binop_1: ( $i * $i ) > $o ).
tff(v2_binop_1,type,
v2_binop_1: ( $i * $i ) > $o ).
tff(v14_lattices,type,
v14_lattices: $i > $o ).
tff(v1_relat_1,type,
v1_relat_1: $i > $o ).
tff(k2_zfmisc_1,type,
k2_zfmisc_1: ( $i * $i ) > $i ).
tff(v13_lattices,type,
v13_lattices: $i > $o ).
tff(k7_filter_2,type,
k7_filter_2: ( $i * $i ) > $i ).
tff('#skF_4',type,
'#skF_4': $i ).
tff(v11_lattices,type,
v11_lattices: $i > $o ).
tff('#skF_11',type,
'#skF_11': $i > $i ).
tff('#skF_22',type,
'#skF_22': $i ).
tff(r2_filter_2,type,
r2_filter_2: ( $i * $i ) > $o ).
tff(v8_lattices,type,
v8_lattices: $i > $o ).
tff('#skF_28',type,
'#skF_28': $i ).
tff('#skF_27',type,
'#skF_27': $i ).
tff('#skF_23',type,
'#skF_23': $i ).
tff(v3_lattices,type,
v3_lattices: $i > $o ).
tff('#skF_12',type,
'#skF_12': $i > $i ).
tff(k7_lattices,type,
k7_lattices: ( $i * $i ) > $i ).
tff(u1_struct_0,type,
u1_struct_0: $i > $i ).
tff(v16_lattices,type,
v16_lattices: $i > $o ).
tff(v1_xboole_0,type,
v1_xboole_0: $i > $o ).
tff(v15_lattices,type,
v15_lattices: $i > $o ).
tff('#skF_20',type,
'#skF_20': $i > $i ).
tff(v3_struct_0,type,
v3_struct_0: $i > $o ).
tff(m1_subset_1,type,
m1_subset_1: ( $i * $i ) > $o ).
tff(v7_lattices,type,
v7_lattices: $i > $o ).
tff(f_52,negated_conjecture,
~ ! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& v17_lattices(A)
& l3_lattices(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( r2_filter_2(A,B)
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( r2_hidden(C,B)
<=> ~ r2_hidden(k7_lattices(A,C),B) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t59_filter_2) ).
tff(f_662,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A) )
=> ( ~ v3_struct_0(k1_lattice2(A))
& v3_lattices(k1_lattice2(A))
& v4_lattices(k1_lattice2(A))
& v5_lattices(k1_lattice2(A))
& v6_lattices(k1_lattice2(A))
& v7_lattices(k1_lattice2(A))
& v8_lattices(k1_lattice2(A))
& v9_lattices(k1_lattice2(A))
& v10_lattices(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc6_lattice2) ).
tff(f_922,axiom,
! [A,B] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A)
& m2_filter_2(B,A) )
=> ( k15_filter_2(A,B) = k7_filter_2(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k15_filter_2) ).
tff(f_371,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( ~ v1_xboole_0(B)
& m2_lattice4(B,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_filter_2) ).
tff(f_383,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A) )
=> ! [B] :
( m2_lattice4(B,A)
=> m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_lattice4) ).
tff(f_247,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( k7_filter_2(A,B) = B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d6_filter_2) ).
tff(f_274,axiom,
! [A,B] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A)
& m2_filter_2(B,A) )
=> m1_filter_2(k15_filter_2(A,B),k1_lattice2(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k15_filter_2) ).
tff(f_934,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A) )
=> ! [B] :
( m1_filter_2(B,A)
<=> m1_filter_0(B,A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
tff(f_280,axiom,
! [A] :
( l3_lattices(A)
=> ( v3_lattices(k1_lattice2(A))
& l3_lattices(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_lattice2) ).
tff(f_356,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A) )
=> ! [B] :
( m1_filter_2(B,A)
=> ( ~ v1_xboole_0(B)
& m2_lattice4(B,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_filter_2) ).
tff(f_485,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& l3_lattices(A) )
=> ( ~ v3_struct_0(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_lattice2) ).
tff(f_964,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( r2_filter_2(A,B)
<=> v1_filter_0(k15_filter_2(A,B),k1_lattice2(A)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t33_filter_2) ).
tff(f_593,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& v17_lattices(A)
& l3_lattices(A) )
=> ( ~ v3_struct_0(k1_lattice2(A))
& v3_lattices(k1_lattice2(A))
& v4_lattices(k1_lattice2(A))
& v5_lattices(k1_lattice2(A))
& v6_lattices(k1_lattice2(A))
& v7_lattices(k1_lattice2(A))
& v8_lattices(k1_lattice2(A))
& v9_lattices(k1_lattice2(A))
& v10_lattices(k1_lattice2(A))
& v11_lattices(k1_lattice2(A))
& v12_lattices(k1_lattice2(A))
& v13_lattices(k1_lattice2(A))
& v14_lattices(k1_lattice2(A))
& v15_lattices(k1_lattice2(A))
& v16_lattices(k1_lattice2(A))
& v17_lattices(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_filter_2) ).
tff(f_175,axiom,
! [A] :
( l3_lattices(A)
=> ( ( ~ v3_struct_0(A)
& v17_lattices(A) )
=> ( ~ v3_struct_0(A)
& v11_lattices(A)
& v13_lattices(A)
& v14_lattices(A)
& v15_lattices(A)
& v16_lattices(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc5_lattices) ).
tff(f_235,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ( k5_filter_2(A,B) = B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_filter_2) ).
tff(f_292,axiom,
! [A,B] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A)
& m1_subset_1(B,u1_struct_0(A)) )
=> m1_subset_1(k5_filter_2(A,B),u1_struct_0(k1_lattice2(A))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_filter_2) ).
tff(f_697,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& v17_lattices(A)
& l3_lattices(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ( k7_lattices(k1_lattice2(A),k5_filter_2(A,B)) = k7_lattices(A,B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l70_filter_2) ).
tff(f_996,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& v17_lattices(A)
& l3_lattices(A) )
=> ! [B] :
( m1_filter_0(B,A)
=> ( v1_filter_0(B,A)
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( r2_hidden(C,B)
<=> ~ r2_hidden(k7_lattices(A,C),B) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t59_filter_0) ).
tff(c_14,plain,
~ v3_struct_0('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_8,plain,
l3_lattices('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_12,plain,
v10_lattices('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_284,plain,
! [A_90] :
( v10_lattices(k1_lattice2(A_90))
| ~ l3_lattices(A_90)
| ~ v10_lattices(A_90)
| v3_struct_0(A_90) ),
inference(cnfTransformation,[status(thm)],[f_662]) ).
tff(c_6,plain,
m2_filter_2('#skF_2','#skF_1'),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_35652,plain,
! [A_2322,B_2323] :
( ( k7_filter_2(A_2322,B_2323) = k15_filter_2(A_2322,B_2323) )
| ~ m2_filter_2(B_2323,A_2322)
| ~ l3_lattices(A_2322)
| ~ v10_lattices(A_2322)
| v3_struct_0(A_2322) ),
inference(cnfTransformation,[status(thm)],[f_922]) ).
tff(c_35658,plain,
( ( k7_filter_2('#skF_1','#skF_2') = k15_filter_2('#skF_1','#skF_2') )
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_6,c_35652]) ).
tff(c_35662,plain,
( ( k7_filter_2('#skF_1','#skF_2') = k15_filter_2('#skF_1','#skF_2') )
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_8,c_35658]) ).
tff(c_35663,plain,
k7_filter_2('#skF_1','#skF_2') = k15_filter_2('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_14,c_35662]) ).
tff(c_150,plain,
! [B_50,A_48] :
( m2_lattice4(B_50,A_48)
| ~ m2_filter_2(B_50,A_48)
| ~ l3_lattices(A_48)
| ~ v10_lattices(A_48)
| v3_struct_0(A_48) ),
inference(cnfTransformation,[status(thm)],[f_371]) ).
tff(c_154,plain,
! [B_53,A_51] :
( m1_subset_1(B_53,k1_zfmisc_1(u1_struct_0(A_51)))
| ~ m2_lattice4(B_53,A_51)
| ~ l3_lattices(A_51)
| ~ v10_lattices(A_51)
| v3_struct_0(A_51) ),
inference(cnfTransformation,[status(thm)],[f_383]) ).
tff(c_35729,plain,
! [A_2335,B_2336] :
( ( k7_filter_2(A_2335,B_2336) = B_2336 )
| ~ m1_subset_1(B_2336,k1_zfmisc_1(u1_struct_0(A_2335)))
| ~ l3_lattices(A_2335)
| ~ v10_lattices(A_2335)
| v3_struct_0(A_2335) ),
inference(cnfTransformation,[status(thm)],[f_247]) ).
tff(c_35924,plain,
! [A_2351,B_2352] :
( ( k7_filter_2(A_2351,B_2352) = B_2352 )
| ~ m2_lattice4(B_2352,A_2351)
| ~ l3_lattices(A_2351)
| ~ v10_lattices(A_2351)
| v3_struct_0(A_2351) ),
inference(resolution,[status(thm)],[c_154,c_35729]) ).
tff(c_35972,plain,
! [A_2357,B_2358] :
( ( k7_filter_2(A_2357,B_2358) = B_2358 )
| ~ m2_filter_2(B_2358,A_2357)
| ~ l3_lattices(A_2357)
| ~ v10_lattices(A_2357)
| v3_struct_0(A_2357) ),
inference(resolution,[status(thm)],[c_150,c_35924]) ).
tff(c_35978,plain,
( ( k7_filter_2('#skF_1','#skF_2') = '#skF_2' )
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_6,c_35972]) ).
tff(c_35982,plain,
( ( k15_filter_2('#skF_1','#skF_2') = '#skF_2' )
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_8,c_35663,c_35978]) ).
tff(c_35983,plain,
k15_filter_2('#skF_1','#skF_2') = '#skF_2',
inference(negUnitSimplification,[status(thm)],[c_14,c_35982]) ).
tff(c_110,plain,
! [A_30,B_31] :
( m1_filter_2(k15_filter_2(A_30,B_31),k1_lattice2(A_30))
| ~ m2_filter_2(B_31,A_30)
| ~ l3_lattices(A_30)
| ~ v10_lattices(A_30)
| v3_struct_0(A_30) ),
inference(cnfTransformation,[status(thm)],[f_274]) ).
tff(c_35989,plain,
( m1_filter_2('#skF_2',k1_lattice2('#skF_1'))
| ~ m2_filter_2('#skF_2','#skF_1')
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_35983,c_110]) ).
tff(c_35993,plain,
( m1_filter_2('#skF_2',k1_lattice2('#skF_1'))
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_8,c_6,c_35989]) ).
tff(c_35994,plain,
m1_filter_2('#skF_2',k1_lattice2('#skF_1')),
inference(negUnitSimplification,[status(thm)],[c_14,c_35993]) ).
tff(c_496,plain,
! [B_115,A_113] :
( m1_filter_0(B_115,A_113)
| ~ m1_filter_2(B_115,A_113)
| ~ l3_lattices(A_113)
| ~ v10_lattices(A_113)
| v3_struct_0(A_113) ),
inference(cnfTransformation,[status(thm)],[f_934]) ).
tff(c_36014,plain,
( m1_filter_0('#skF_2',k1_lattice2('#skF_1'))
| ~ l3_lattices(k1_lattice2('#skF_1'))
| ~ v10_lattices(k1_lattice2('#skF_1'))
| v3_struct_0(k1_lattice2('#skF_1')) ),
inference(resolution,[status(thm)],[c_35994,c_496]) ).
tff(c_36016,plain,
~ v10_lattices(k1_lattice2('#skF_1')),
inference(splitLeft,[status(thm)],[c_36014]) ).
tff(c_36019,plain,
( ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_284,c_36016]) ).
tff(c_36022,plain,
v3_struct_0('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_8,c_36019]) ).
tff(c_36024,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_36022]) ).
tff(c_36026,plain,
v10_lattices(k1_lattice2('#skF_1')),
inference(splitRight,[status(thm)],[c_36014]) ).
tff(c_112,plain,
! [A_32] :
( l3_lattices(k1_lattice2(A_32))
| ~ l3_lattices(A_32) ),
inference(cnfTransformation,[status(thm)],[f_280]) ).
tff(c_36025,plain,
( ~ l3_lattices(k1_lattice2('#skF_1'))
| v3_struct_0(k1_lattice2('#skF_1'))
| m1_filter_0('#skF_2',k1_lattice2('#skF_1')) ),
inference(splitRight,[status(thm)],[c_36014]) ).
tff(c_36027,plain,
~ l3_lattices(k1_lattice2('#skF_1')),
inference(splitLeft,[status(thm)],[c_36025]) ).
tff(c_36030,plain,
~ l3_lattices('#skF_1'),
inference(resolution,[status(thm)],[c_112,c_36027]) ).
tff(c_36034,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_36030]) ).
tff(c_36036,plain,
l3_lattices(k1_lattice2('#skF_1')),
inference(splitRight,[status(thm)],[c_36025]) ).
tff(c_142,plain,
! [B_47,A_45] :
( m2_lattice4(B_47,A_45)
| ~ m1_filter_2(B_47,A_45)
| ~ l3_lattices(A_45)
| ~ v10_lattices(A_45)
| v3_struct_0(A_45) ),
inference(cnfTransformation,[status(thm)],[f_356]) ).
tff(c_35938,plain,
! [A_45,B_47] :
( ( k7_filter_2(A_45,B_47) = B_47 )
| ~ m1_filter_2(B_47,A_45)
| ~ l3_lattices(A_45)
| ~ v10_lattices(A_45)
| v3_struct_0(A_45) ),
inference(resolution,[status(thm)],[c_142,c_35924]) ).
tff(c_36012,plain,
( ( k7_filter_2(k1_lattice2('#skF_1'),'#skF_2') = '#skF_2' )
| ~ l3_lattices(k1_lattice2('#skF_1'))
| ~ v10_lattices(k1_lattice2('#skF_1'))
| v3_struct_0(k1_lattice2('#skF_1')) ),
inference(resolution,[status(thm)],[c_35994,c_35938]) ).
tff(c_36051,plain,
( ( k7_filter_2(k1_lattice2('#skF_1'),'#skF_2') = '#skF_2' )
| v3_struct_0(k1_lattice2('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_36026,c_36036,c_36012]) ).
tff(c_36052,plain,
v3_struct_0(k1_lattice2('#skF_1')),
inference(splitLeft,[status(thm)],[c_36051]) ).
tff(c_198,plain,
! [A_77] :
( ~ v3_struct_0(k1_lattice2(A_77))
| ~ l3_lattices(A_77)
| v3_struct_0(A_77) ),
inference(cnfTransformation,[status(thm)],[f_485]) ).
tff(c_36055,plain,
( ~ l3_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_36052,c_198]) ).
tff(c_36058,plain,
v3_struct_0('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_36055]) ).
tff(c_36060,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_36058]) ).
tff(c_36062,plain,
~ v3_struct_0(k1_lattice2('#skF_1')),
inference(splitRight,[status(thm)],[c_36051]) ).
tff(c_36035,plain,
( m1_filter_0('#skF_2',k1_lattice2('#skF_1'))
| v3_struct_0(k1_lattice2('#skF_1')) ),
inference(splitRight,[status(thm)],[c_36025]) ).
tff(c_36281,plain,
m1_filter_0('#skF_2',k1_lattice2('#skF_1')),
inference(negUnitSimplification,[status(thm)],[c_36062,c_36035]) ).
tff(c_16,plain,
( r2_hidden(k7_lattices('#skF_1','#skF_3'),'#skF_2')
| ~ r2_hidden('#skF_3','#skF_2') ),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_531,plain,
~ r2_hidden('#skF_3','#skF_2'),
inference(splitLeft,[status(thm)],[c_16]) ).
tff(c_22,plain,
( r2_hidden('#skF_3','#skF_2')
| ~ r2_hidden(k7_lattices('#skF_1','#skF_3'),'#skF_2') ),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_532,plain,
~ r2_hidden(k7_lattices('#skF_1','#skF_3'),'#skF_2'),
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_2408,plain,
! [A_410,B_411] :
( ( k7_filter_2(A_410,B_411) = k15_filter_2(A_410,B_411) )
| ~ m2_filter_2(B_411,A_410)
| ~ l3_lattices(A_410)
| ~ v10_lattices(A_410)
| v3_struct_0(A_410) ),
inference(cnfTransformation,[status(thm)],[f_922]) ).
tff(c_2414,plain,
( ( k7_filter_2('#skF_1','#skF_2') = k15_filter_2('#skF_1','#skF_2') )
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_6,c_2408]) ).
tff(c_2418,plain,
( ( k7_filter_2('#skF_1','#skF_2') = k15_filter_2('#skF_1','#skF_2') )
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_8,c_2414]) ).
tff(c_2419,plain,
k7_filter_2('#skF_1','#skF_2') = k15_filter_2('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_14,c_2418]) ).
tff(c_2234,plain,
! [A_399,B_400] :
( ( k7_filter_2(A_399,B_400) = B_400 )
| ~ m1_subset_1(B_400,k1_zfmisc_1(u1_struct_0(A_399)))
| ~ l3_lattices(A_399)
| ~ v10_lattices(A_399)
| v3_struct_0(A_399) ),
inference(cnfTransformation,[status(thm)],[f_247]) ).
tff(c_2429,plain,
! [A_413,B_414] :
( ( k7_filter_2(A_413,B_414) = B_414 )
| ~ m2_lattice4(B_414,A_413)
| ~ l3_lattices(A_413)
| ~ v10_lattices(A_413)
| v3_struct_0(A_413) ),
inference(resolution,[status(thm)],[c_154,c_2234]) ).
tff(c_2540,plain,
! [A_431,B_432] :
( ( k7_filter_2(A_431,B_432) = B_432 )
| ~ m2_filter_2(B_432,A_431)
| ~ l3_lattices(A_431)
| ~ v10_lattices(A_431)
| v3_struct_0(A_431) ),
inference(resolution,[status(thm)],[c_150,c_2429]) ).
tff(c_2546,plain,
( ( k7_filter_2('#skF_1','#skF_2') = '#skF_2' )
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_6,c_2540]) ).
tff(c_2550,plain,
( ( k15_filter_2('#skF_1','#skF_2') = '#skF_2' )
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_8,c_2419,c_2546]) ).
tff(c_2551,plain,
k15_filter_2('#skF_1','#skF_2') = '#skF_2',
inference(negUnitSimplification,[status(thm)],[c_14,c_2550]) ).
tff(c_2556,plain,
( m1_filter_2('#skF_2',k1_lattice2('#skF_1'))
| ~ m2_filter_2('#skF_2','#skF_1')
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_2551,c_110]) ).
tff(c_2560,plain,
( m1_filter_2('#skF_2',k1_lattice2('#skF_1'))
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_8,c_6,c_2556]) ).
tff(c_2561,plain,
m1_filter_2('#skF_2',k1_lattice2('#skF_1')),
inference(negUnitSimplification,[status(thm)],[c_14,c_2560]) ).
tff(c_2569,plain,
( m1_filter_0('#skF_2',k1_lattice2('#skF_1'))
| ~ l3_lattices(k1_lattice2('#skF_1'))
| ~ v10_lattices(k1_lattice2('#skF_1'))
| v3_struct_0(k1_lattice2('#skF_1')) ),
inference(resolution,[status(thm)],[c_2561,c_496]) ).
tff(c_2610,plain,
~ v10_lattices(k1_lattice2('#skF_1')),
inference(splitLeft,[status(thm)],[c_2569]) ).
tff(c_2614,plain,
( ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_284,c_2610]) ).
tff(c_2617,plain,
v3_struct_0('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_8,c_2614]) ).
tff(c_2619,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_2617]) ).
tff(c_2621,plain,
v10_lattices(k1_lattice2('#skF_1')),
inference(splitRight,[status(thm)],[c_2569]) ).
tff(c_2620,plain,
( ~ l3_lattices(k1_lattice2('#skF_1'))
| v3_struct_0(k1_lattice2('#skF_1'))
| m1_filter_0('#skF_2',k1_lattice2('#skF_1')) ),
inference(splitRight,[status(thm)],[c_2569]) ).
tff(c_2622,plain,
~ l3_lattices(k1_lattice2('#skF_1')),
inference(splitLeft,[status(thm)],[c_2620]) ).
tff(c_2625,plain,
~ l3_lattices('#skF_1'),
inference(resolution,[status(thm)],[c_112,c_2622]) ).
tff(c_2629,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_2625]) ).
tff(c_2631,plain,
l3_lattices(k1_lattice2('#skF_1')),
inference(splitRight,[status(thm)],[c_2620]) ).
tff(c_2584,plain,
! [A_434,B_435] :
( ( k7_filter_2(A_434,B_435) = B_435 )
| ~ m1_filter_2(B_435,A_434)
| ~ l3_lattices(A_434)
| ~ v10_lattices(A_434)
| v3_struct_0(A_434) ),
inference(resolution,[status(thm)],[c_142,c_2429]) ).
tff(c_2597,plain,
( ( k7_filter_2(k1_lattice2('#skF_1'),'#skF_2') = '#skF_2' )
| ~ l3_lattices(k1_lattice2('#skF_1'))
| ~ v10_lattices(k1_lattice2('#skF_1'))
| v3_struct_0(k1_lattice2('#skF_1')) ),
inference(resolution,[status(thm)],[c_2561,c_2584]) ).
tff(c_2696,plain,
( ( k7_filter_2(k1_lattice2('#skF_1'),'#skF_2') = '#skF_2' )
| v3_struct_0(k1_lattice2('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_2621,c_2631,c_2597]) ).
tff(c_2697,plain,
v3_struct_0(k1_lattice2('#skF_1')),
inference(splitLeft,[status(thm)],[c_2696]) ).
tff(c_2700,plain,
( ~ l3_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_2697,c_198]) ).
tff(c_2703,plain,
v3_struct_0('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_2700]) ).
tff(c_2705,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_2703]) ).
tff(c_2707,plain,
~ v3_struct_0(k1_lattice2('#skF_1')),
inference(splitRight,[status(thm)],[c_2696]) ).
tff(c_2630,plain,
( m1_filter_0('#skF_2',k1_lattice2('#skF_1'))
| v3_struct_0(k1_lattice2('#skF_1')) ),
inference(splitRight,[status(thm)],[c_2620]) ).
tff(c_2920,plain,
m1_filter_0('#skF_2',k1_lattice2('#skF_1')),
inference(negUnitSimplification,[status(thm)],[c_2707,c_2630]) ).
tff(c_4,plain,
r2_filter_2('#skF_1','#skF_2'),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_3111,plain,
! [A_462,B_463] :
( v1_filter_0(k15_filter_2(A_462,B_463),k1_lattice2(A_462))
| ~ r2_filter_2(A_462,B_463)
| ~ m2_filter_2(B_463,A_462)
| ~ l3_lattices(A_462)
| ~ v10_lattices(A_462)
| v3_struct_0(A_462) ),
inference(cnfTransformation,[status(thm)],[f_964]) ).
tff(c_3117,plain,
( v1_filter_0('#skF_2',k1_lattice2('#skF_1'))
| ~ r2_filter_2('#skF_1','#skF_2')
| ~ m2_filter_2('#skF_2','#skF_1')
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_2551,c_3111]) ).
tff(c_3120,plain,
( v1_filter_0('#skF_2',k1_lattice2('#skF_1'))
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_8,c_6,c_4,c_3117]) ).
tff(c_3121,plain,
v1_filter_0('#skF_2',k1_lattice2('#skF_1')),
inference(negUnitSimplification,[status(thm)],[c_14,c_3120]) ).
tff(c_10,plain,
v17_lattices('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_230,plain,
! [A_85] :
( v17_lattices(k1_lattice2(A_85))
| ~ l3_lattices(A_85)
| ~ v17_lattices(A_85)
| ~ v10_lattices(A_85)
| v3_struct_0(A_85) ),
inference(cnfTransformation,[status(thm)],[f_593]) ).
tff(c_66,plain,
! [A_17] :
( v16_lattices(A_17)
| ~ v17_lattices(A_17)
| v3_struct_0(A_17)
| ~ l3_lattices(A_17) ),
inference(cnfTransformation,[status(thm)],[f_175]) ).
tff(c_2737,plain,
( v16_lattices(k1_lattice2('#skF_1'))
| ~ v17_lattices(k1_lattice2('#skF_1'))
| ~ l3_lattices(k1_lattice2('#skF_1')) ),
inference(resolution,[status(thm)],[c_66,c_2707]) ).
tff(c_2770,plain,
( v16_lattices(k1_lattice2('#skF_1'))
| ~ v17_lattices(k1_lattice2('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_2631,c_2737]) ).
tff(c_2782,plain,
~ v17_lattices(k1_lattice2('#skF_1')),
inference(splitLeft,[status(thm)],[c_2770]) ).
tff(c_2799,plain,
( ~ l3_lattices('#skF_1')
| ~ v17_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_230,c_2782]) ).
tff(c_2802,plain,
v3_struct_0('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_10,c_8,c_2799]) ).
tff(c_2804,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_2802]) ).
tff(c_2806,plain,
v17_lattices(k1_lattice2('#skF_1')),
inference(splitRight,[status(thm)],[c_2770]) ).
tff(c_2,plain,
m1_subset_1('#skF_3',u1_struct_0('#skF_1')),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_2171,plain,
! [A_393,B_394] :
( ( k5_filter_2(A_393,B_394) = B_394 )
| ~ m1_subset_1(B_394,u1_struct_0(A_393))
| ~ l3_lattices(A_393)
| ~ v10_lattices(A_393)
| v3_struct_0(A_393) ),
inference(cnfTransformation,[status(thm)],[f_235]) ).
tff(c_2189,plain,
( ( k5_filter_2('#skF_1','#skF_3') = '#skF_3' )
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_2,c_2171]) ).
tff(c_2196,plain,
( ( k5_filter_2('#skF_1','#skF_3') = '#skF_3' )
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_8,c_2189]) ).
tff(c_2197,plain,
k5_filter_2('#skF_1','#skF_3') = '#skF_3',
inference(negUnitSimplification,[status(thm)],[c_14,c_2196]) ).
tff(c_2859,plain,
! [A_446,B_447] :
( m1_subset_1(k5_filter_2(A_446,B_447),u1_struct_0(k1_lattice2(A_446)))
| ~ m1_subset_1(B_447,u1_struct_0(A_446))
| ~ l3_lattices(A_446)
| ~ v10_lattices(A_446)
| v3_struct_0(A_446) ),
inference(cnfTransformation,[status(thm)],[f_292]) ).
tff(c_2867,plain,
( m1_subset_1('#skF_3',u1_struct_0(k1_lattice2('#skF_1')))
| ~ m1_subset_1('#skF_3',u1_struct_0('#skF_1'))
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_2197,c_2859]) ).
tff(c_2871,plain,
( m1_subset_1('#skF_3',u1_struct_0(k1_lattice2('#skF_1')))
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_8,c_2,c_2867]) ).
tff(c_2872,plain,
m1_subset_1('#skF_3',u1_struct_0(k1_lattice2('#skF_1'))),
inference(negUnitSimplification,[status(thm)],[c_14,c_2871]) ).
tff(c_3425,plain,
! [A_469,B_470] :
( ( k7_lattices(k1_lattice2(A_469),k5_filter_2(A_469,B_470)) = k7_lattices(A_469,B_470) )
| ~ m1_subset_1(B_470,u1_struct_0(A_469))
| ~ l3_lattices(A_469)
| ~ v17_lattices(A_469)
| ~ v10_lattices(A_469)
| v3_struct_0(A_469) ),
inference(cnfTransformation,[status(thm)],[f_697]) ).
tff(c_3443,plain,
( ( k7_lattices(k1_lattice2('#skF_1'),'#skF_3') = k7_lattices('#skF_1','#skF_3') )
| ~ m1_subset_1('#skF_3',u1_struct_0('#skF_1'))
| ~ l3_lattices('#skF_1')
| ~ v17_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_2197,c_3425]) ).
tff(c_3452,plain,
( ( k7_lattices(k1_lattice2('#skF_1'),'#skF_3') = k7_lattices('#skF_1','#skF_3') )
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_10,c_8,c_2,c_3443]) ).
tff(c_3453,plain,
k7_lattices(k1_lattice2('#skF_1'),'#skF_3') = k7_lattices('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_14,c_3452]) ).
tff(c_3626,plain,
! [C_477,B_478,A_479] :
( r2_hidden(C_477,B_478)
| r2_hidden(k7_lattices(A_479,C_477),B_478)
| ~ m1_subset_1(C_477,u1_struct_0(A_479))
| ~ v1_filter_0(B_478,A_479)
| ~ m1_filter_0(B_478,A_479)
| ~ l3_lattices(A_479)
| ~ v17_lattices(A_479)
| ~ v10_lattices(A_479)
| v3_struct_0(A_479) ),
inference(cnfTransformation,[status(thm)],[f_996]) ).
tff(c_3684,plain,
! [B_478] :
( r2_hidden('#skF_3',B_478)
| r2_hidden(k7_lattices('#skF_1','#skF_3'),B_478)
| ~ m1_subset_1('#skF_3',u1_struct_0(k1_lattice2('#skF_1')))
| ~ v1_filter_0(B_478,k1_lattice2('#skF_1'))
| ~ m1_filter_0(B_478,k1_lattice2('#skF_1'))
| ~ l3_lattices(k1_lattice2('#skF_1'))
| ~ v17_lattices(k1_lattice2('#skF_1'))
| ~ v10_lattices(k1_lattice2('#skF_1'))
| v3_struct_0(k1_lattice2('#skF_1')) ),
inference(superposition,[status(thm),theory(equality)],[c_3453,c_3626]) ).
tff(c_3711,plain,
! [B_478] :
( r2_hidden('#skF_3',B_478)
| r2_hidden(k7_lattices('#skF_1','#skF_3'),B_478)
| ~ v1_filter_0(B_478,k1_lattice2('#skF_1'))
| ~ m1_filter_0(B_478,k1_lattice2('#skF_1'))
| v3_struct_0(k1_lattice2('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_2621,c_2806,c_2631,c_2872,c_3684]) ).
tff(c_13901,plain,
! [B_887] :
( r2_hidden('#skF_3',B_887)
| r2_hidden(k7_lattices('#skF_1','#skF_3'),B_887)
| ~ v1_filter_0(B_887,k1_lattice2('#skF_1'))
| ~ m1_filter_0(B_887,k1_lattice2('#skF_1')) ),
inference(negUnitSimplification,[status(thm)],[c_2707,c_3711]) ).
tff(c_13904,plain,
( r2_hidden('#skF_3','#skF_2')
| r2_hidden(k7_lattices('#skF_1','#skF_3'),'#skF_2')
| ~ m1_filter_0('#skF_2',k1_lattice2('#skF_1')) ),
inference(resolution,[status(thm)],[c_3121,c_13901]) ).
tff(c_13911,plain,
( r2_hidden('#skF_3','#skF_2')
| r2_hidden(k7_lattices('#skF_1','#skF_3'),'#skF_2') ),
inference(demodulation,[status(thm),theory(equality)],[c_2920,c_13904]) ).
tff(c_13913,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_532,c_531,c_13911]) ).
tff(c_13914,plain,
r2_hidden('#skF_3','#skF_2'),
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_13916,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_531,c_13914]) ).
tff(c_13918,plain,
r2_hidden('#skF_3','#skF_2'),
inference(splitRight,[status(thm)],[c_16]) ).
tff(c_13917,plain,
r2_hidden(k7_lattices('#skF_1','#skF_3'),'#skF_2'),
inference(splitRight,[status(thm)],[c_16]) ).
tff(c_36601,plain,
! [A_2399,B_2400] :
( v1_filter_0(k15_filter_2(A_2399,B_2400),k1_lattice2(A_2399))
| ~ r2_filter_2(A_2399,B_2400)
| ~ m2_filter_2(B_2400,A_2399)
| ~ l3_lattices(A_2399)
| ~ v10_lattices(A_2399)
| v3_struct_0(A_2399) ),
inference(cnfTransformation,[status(thm)],[f_964]) ).
tff(c_36607,plain,
( v1_filter_0('#skF_2',k1_lattice2('#skF_1'))
| ~ r2_filter_2('#skF_1','#skF_2')
| ~ m2_filter_2('#skF_2','#skF_1')
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_35983,c_36601]) ).
tff(c_36610,plain,
( v1_filter_0('#skF_2',k1_lattice2('#skF_1'))
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_8,c_6,c_4,c_36607]) ).
tff(c_36611,plain,
v1_filter_0('#skF_2',k1_lattice2('#skF_1')),
inference(negUnitSimplification,[status(thm)],[c_14,c_36610]) ).
tff(c_36083,plain,
( v16_lattices(k1_lattice2('#skF_1'))
| ~ v17_lattices(k1_lattice2('#skF_1'))
| ~ l3_lattices(k1_lattice2('#skF_1')) ),
inference(resolution,[status(thm)],[c_66,c_36062]) ).
tff(c_36116,plain,
( v16_lattices(k1_lattice2('#skF_1'))
| ~ v17_lattices(k1_lattice2('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_36036,c_36083]) ).
tff(c_36183,plain,
~ v17_lattices(k1_lattice2('#skF_1')),
inference(splitLeft,[status(thm)],[c_36116]) ).
tff(c_36186,plain,
( ~ l3_lattices('#skF_1')
| ~ v17_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_230,c_36183]) ).
tff(c_36189,plain,
v3_struct_0('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_10,c_8,c_36186]) ).
tff(c_36191,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_36189]) ).
tff(c_36193,plain,
v17_lattices(k1_lattice2('#skF_1')),
inference(splitRight,[status(thm)],[c_36116]) ).
tff(c_35431,plain,
! [A_2296,B_2297] :
( ( k5_filter_2(A_2296,B_2297) = B_2297 )
| ~ m1_subset_1(B_2297,u1_struct_0(A_2296))
| ~ l3_lattices(A_2296)
| ~ v10_lattices(A_2296)
| v3_struct_0(A_2296) ),
inference(cnfTransformation,[status(thm)],[f_235]) ).
tff(c_35456,plain,
( ( k5_filter_2('#skF_1','#skF_3') = '#skF_3' )
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_2,c_35431]) ).
tff(c_35465,plain,
( ( k5_filter_2('#skF_1','#skF_3') = '#skF_3' )
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_8,c_35456]) ).
tff(c_35466,plain,
k5_filter_2('#skF_1','#skF_3') = '#skF_3',
inference(negUnitSimplification,[status(thm)],[c_14,c_35465]) ).
tff(c_36236,plain,
! [A_2364,B_2365] :
( m1_subset_1(k5_filter_2(A_2364,B_2365),u1_struct_0(k1_lattice2(A_2364)))
| ~ m1_subset_1(B_2365,u1_struct_0(A_2364))
| ~ l3_lattices(A_2364)
| ~ v10_lattices(A_2364)
| v3_struct_0(A_2364) ),
inference(cnfTransformation,[status(thm)],[f_292]) ).
tff(c_36252,plain,
( m1_subset_1('#skF_3',u1_struct_0(k1_lattice2('#skF_1')))
| ~ m1_subset_1('#skF_3',u1_struct_0('#skF_1'))
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_35466,c_36236]) ).
tff(c_36262,plain,
( m1_subset_1('#skF_3',u1_struct_0(k1_lattice2('#skF_1')))
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_8,c_2,c_36252]) ).
tff(c_36263,plain,
m1_subset_1('#skF_3',u1_struct_0(k1_lattice2('#skF_1'))),
inference(negUnitSimplification,[status(thm)],[c_14,c_36262]) ).
tff(c_37229,plain,
! [A_2434,B_2435] :
( ( k7_lattices(k1_lattice2(A_2434),k5_filter_2(A_2434,B_2435)) = k7_lattices(A_2434,B_2435) )
| ~ m1_subset_1(B_2435,u1_struct_0(A_2434))
| ~ l3_lattices(A_2434)
| ~ v17_lattices(A_2434)
| ~ v10_lattices(A_2434)
| v3_struct_0(A_2434) ),
inference(cnfTransformation,[status(thm)],[f_697]) ).
tff(c_37250,plain,
( ( k7_lattices(k1_lattice2('#skF_1'),'#skF_3') = k7_lattices('#skF_1','#skF_3') )
| ~ m1_subset_1('#skF_3',u1_struct_0('#skF_1'))
| ~ l3_lattices('#skF_1')
| ~ v17_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_35466,c_37229]) ).
tff(c_37259,plain,
( ( k7_lattices(k1_lattice2('#skF_1'),'#skF_3') = k7_lattices('#skF_1','#skF_3') )
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_10,c_8,c_2,c_37250]) ).
tff(c_37260,plain,
k7_lattices(k1_lattice2('#skF_1'),'#skF_3') = k7_lattices('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_14,c_37259]) ).
tff(c_37692,plain,
! [A_2448,C_2449,B_2450] :
( ~ r2_hidden(k7_lattices(A_2448,C_2449),B_2450)
| ~ r2_hidden(C_2449,B_2450)
| ~ m1_subset_1(C_2449,u1_struct_0(A_2448))
| ~ v1_filter_0(B_2450,A_2448)
| ~ m1_filter_0(B_2450,A_2448)
| ~ l3_lattices(A_2448)
| ~ v17_lattices(A_2448)
| ~ v10_lattices(A_2448)
| v3_struct_0(A_2448) ),
inference(cnfTransformation,[status(thm)],[f_996]) ).
tff(c_37698,plain,
! [B_2450] :
( ~ r2_hidden(k7_lattices('#skF_1','#skF_3'),B_2450)
| ~ r2_hidden('#skF_3',B_2450)
| ~ m1_subset_1('#skF_3',u1_struct_0(k1_lattice2('#skF_1')))
| ~ v1_filter_0(B_2450,k1_lattice2('#skF_1'))
| ~ m1_filter_0(B_2450,k1_lattice2('#skF_1'))
| ~ l3_lattices(k1_lattice2('#skF_1'))
| ~ v17_lattices(k1_lattice2('#skF_1'))
| ~ v10_lattices(k1_lattice2('#skF_1'))
| v3_struct_0(k1_lattice2('#skF_1')) ),
inference(superposition,[status(thm),theory(equality)],[c_37260,c_37692]) ).
tff(c_37711,plain,
! [B_2450] :
( ~ r2_hidden(k7_lattices('#skF_1','#skF_3'),B_2450)
| ~ r2_hidden('#skF_3',B_2450)
| ~ v1_filter_0(B_2450,k1_lattice2('#skF_1'))
| ~ m1_filter_0(B_2450,k1_lattice2('#skF_1'))
| v3_struct_0(k1_lattice2('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_36026,c_36193,c_36036,c_36263,c_37698]) ).
tff(c_45379,plain,
! [B_2744] :
( ~ r2_hidden(k7_lattices('#skF_1','#skF_3'),B_2744)
| ~ r2_hidden('#skF_3',B_2744)
| ~ v1_filter_0(B_2744,k1_lattice2('#skF_1'))
| ~ m1_filter_0(B_2744,k1_lattice2('#skF_1')) ),
inference(negUnitSimplification,[status(thm)],[c_36062,c_37711]) ).
tff(c_45382,plain,
( ~ r2_hidden(k7_lattices('#skF_1','#skF_3'),'#skF_2')
| ~ r2_hidden('#skF_3','#skF_2')
| ~ m1_filter_0('#skF_2',k1_lattice2('#skF_1')) ),
inference(resolution,[status(thm)],[c_36611,c_45379]) ).
tff(c_45390,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_36281,c_13918,c_13917,c_45382]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : LAT323+1 : TPTP v9.0.0. Released v3.4.0.
% 0.00/0.09 % 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.09/0.28 % Computer : n032.cluster.edu
% 0.09/0.28 % Model : x86_64 x86_64
% 0.09/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.28 % Memory : 8042.1875MB
% 0.09/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.28 % CPULimit : 300
% 0.09/0.28 % WCLimit : 300
% 0.09/0.28 % DateTime : Tue Apr 8 04:22:45 EDT 2025
% 0.09/0.28 % CPUTime :
% 32.08/16.68 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 32.08/16.69
% 32.08/16.69 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------