%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : LAT332+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:56 PM UTC 2025
% Result : Theorem 25.75s 12.44s
% Output : CNFRefutation 26.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 26
% Syntax : Number of formulae : 182 ( 61 unt; 0 typ; 0 def)
% Number of atoms : 552 ( 99 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 612 ( 242 ~; 297 |; 38 &)
% ( 5 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 34 ( 32 usr; 1 prp; 0-3 aty)
% Number of functors : 45 ( 45 usr; 15 con; 0-4 aty)
% Number of variables : 158 ( 155 !; 3 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ v1_partfun1 > v1_funct_2 > r1_filter_2 > m2_relset_1 > m1_relset_1 > v2_binop_1 > v1_binop_1 > r2_hidden > r1_tarski > m2_nat_lat > 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 > v10_lattices > l3_lattices > l2_lattices > l1_struct_0 > l1_lattices > k8_relset_1 > k4_relset_1 > g3_lattices > k7_relat_1 > k2_zfmisc_1 > k23_filter_2 > k1_realset1 > #nlpp > u2_lattices > u1_struct_0 > u1_lattices > k1_zfmisc_1 > k1_relat_1 > k1_filter_2 > k1_filter_0 > k17_filter_2 > k1_xboole_0 > #skF_9 > #skF_20 > #skF_18 > #skF_19 > #skF_25 > #skF_22 > #skF_8 > #skF_7 > #skF_16 > #skF_26 > #skF_5 > #skF_6 > #skF_10 > #skF_1 > #skF_2 > #skF_21 > #skF_13 > #skF_4 > #skF_17 > #skF_11 > #skF_3 > #skF_14 > #skF_29 > #skF_28 > #skF_24 > #skF_23 > #skF_27 > #skF_12 > #skF_15
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(l3_lattices,type,
l3_lattices: $i > $o ).
tff('#skF_9',type,
'#skF_9': $i > $i ).
tff(m2_relset_1,type,
m2_relset_1: ( $i * $i * $i ) > $o ).
tff(l2_lattices,type,
l2_lattices: $i > $o ).
tff('#skF_20',type,
'#skF_20': $i ).
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 > $i ).
tff(m2_nat_lat,type,
m2_nat_lat: ( $i * $i ) > $o ).
tff(r2_hidden,type,
r2_hidden: ( $i * $i ) > $o ).
tff(k7_relat_1,type,
k7_relat_1: ( $i * $i ) > $i ).
tff(v1_partfun1,type,
v1_partfun1: ( $i * $i * $i ) > $o ).
tff('#skF_19',type,
'#skF_19': $i > $i ).
tff(k8_relset_1,type,
k8_relset_1: ( $i * $i * $i * $i ) > $i ).
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('#skF_22',type,
'#skF_22': $i > $i ).
tff(l1_lattices,type,
l1_lattices: $i > $o ).
tff(k23_filter_2,type,
k23_filter_2: ( $i * $i ) > $i ).
tff('#skF_8',type,
'#skF_8': $i > $i ).
tff('#skF_7',type,
'#skF_7': $i ).
tff(r1_tarski,type,
r1_tarski: ( $i * $i ) > $o ).
tff(k4_relset_1,type,
k4_relset_1: ( $i * $i * $i ) > $i ).
tff(m1_relset_1,type,
m1_relset_1: ( $i * $i * $i ) > $o ).
tff('#skF_16',type,
'#skF_16': $i ).
tff(k17_filter_2,type,
k17_filter_2: $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(k1_filter_0,type,
k1_filter_0: $i > $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_1',type,
'#skF_1': $i ).
tff('#skF_2',type,
'#skF_2': ( $i * $i * $i ) > $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('#skF_21',type,
'#skF_21': $i ).
tff(v10_lattices,type,
v10_lattices: $i > $o ).
tff(k1_zfmisc_1,type,
k1_zfmisc_1: $i > $i ).
tff(k1_realset1,type,
k1_realset1: ( $i * $i ) > $i ).
tff(l1_struct_0,type,
l1_struct_0: $i > $o ).
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(v1_relat_1,type,
v1_relat_1: $i > $o ).
tff(k2_zfmisc_1,type,
k2_zfmisc_1: ( $i * $i ) > $i ).
tff('#skF_4',type,
'#skF_4': $i ).
tff('#skF_17',type,
'#skF_17': $i > $i ).
tff('#skF_11',type,
'#skF_11': $i > $i ).
tff(r1_filter_2,type,
r1_filter_2: ( $i * $i * $i ) > $o ).
tff('#skF_3',type,
'#skF_3': ( $i * $i * $i ) > $i ).
tff('#skF_14',type,
'#skF_14': $i > $i ).
tff(v8_lattices,type,
v8_lattices: $i > $o ).
tff('#skF_29',type,
'#skF_29': $i ).
tff('#skF_28',type,
'#skF_28': $i ).
tff('#skF_24',type,
'#skF_24': $i ).
tff('#skF_23',type,
'#skF_23': $i ).
tff(v3_lattices,type,
v3_lattices: $i > $o ).
tff('#skF_27',type,
'#skF_27': $i > $i ).
tff('#skF_12',type,
'#skF_12': $i > $i ).
tff(u1_struct_0,type,
u1_struct_0: $i > $i ).
tff(v1_xboole_0,type,
v1_xboole_0: $i > $o ).
tff(k1_relat_1,type,
k1_relat_1: $i > $i ).
tff('#skF_15',type,
'#skF_15': ( $i * $i ) > $i ).
tff(k1_filter_2,type,
k1_filter_2: $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_41,negated_conjecture,
~ ! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A) )
=> ( ( k23_filter_2(A,k17_filter_2(A)) = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) )
& ( k23_filter_2(A,k1_filter_2(A)) = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t72_filter_2) ).
tff(f_195,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A) )
=> ( k17_filter_2(A) = u1_struct_0(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_filter_2) ).
tff(f_181,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A) )
=> ( k1_filter_0(A) = u1_struct_0(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_filter_0) ).
tff(f_755,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A) )
=> ( k1_filter_2(A) = k1_filter_0(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k1_filter_2) ).
tff(f_279,axiom,
! [A] :
( l3_lattices(A)
=> ( l1_lattices(A)
& l2_lattices(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l3_lattices) ).
tff(f_273,axiom,
! [A] :
( l2_lattices(A)
=> l1_struct_0(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l2_lattices) ).
tff(f_452,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& l1_struct_0(A) )
=> ~ v1_xboole_0(u1_struct_0(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).
tff(f_238,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A) )
=> m1_filter_2(k1_filter_2(A),A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_filter_2) ).
tff(f_309,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_365,axiom,
! [A] :
( l1_lattices(A)
=> ( v1_funct_1(u1_lattices(A))
& v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& m2_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u1_lattices) ).
tff(f_357,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
=> m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_relset_1) ).
tff(f_82,axiom,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))
=> v1_relat_1(C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_relset_1) ).
tff(f_779,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
tff(f_759,axiom,
! [A,B,C] :
( m1_relset_1(C,A,B)
=> ( k4_relset_1(A,B,C) = k1_relat_1(C) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k4_relset_1) ).
tff(f_257,axiom,
! [A,B,C] :
( m1_relset_1(C,A,B)
=> m1_subset_1(k4_relset_1(A,B,C),k1_zfmisc_1(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_relset_1) ).
tff(f_826,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_862,axiom,
! [A,B] :
( v1_relat_1(B)
=> ( r1_tarski(k1_relat_1(B),A)
=> ( k7_relat_1(B,A) = B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t97_relat_1) ).
tff(f_186,axiom,
! [A] :
( v1_relat_1(A)
=> ! [B] : ( k1_realset1(A,B) = k7_relat_1(A,k2_zfmisc_1(B,B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_realset1) ).
tff(f_373,axiom,
! [A] :
( l2_lattices(A)
=> ( v1_funct_1(u2_lattices(A))
& v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& m2_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u2_lattices) ).
tff(f_684,axiom,
? [A] :
( v1_relat_1(A)
& v1_xboole_0(A)
& v1_funct_1(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_funct_1) ).
tff(f_843,axiom,
! [A] :
( v1_xboole_0(A)
=> ( A = k1_xboole_0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_boole) ).
tff(f_172,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
=> ( ( ( ( B = k1_xboole_0 )
=> ( A = k1_xboole_0 ) )
=> ( v1_funct_2(C,A,B)
<=> ( A = k4_relset_1(A,B,C) ) ) )
& ( ( B = k1_xboole_0 )
=> ( ( A = k1_xboole_0 )
| ( v1_funct_2(C,A,B)
<=> ( C = k1_xboole_0 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_funct_2) ).
tff(f_154,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A) )
=> ! [B] :
( ( ~ v1_xboole_0(B)
& m2_lattice4(B,A) )
=> ! [C] :
( m2_nat_lat(C,A)
=> ( ( C = k23_filter_2(A,B) )
<=> ? [D] :
( v1_funct_1(D)
& v1_funct_2(D,k2_zfmisc_1(B,B),B)
& m2_relset_1(D,k2_zfmisc_1(B,B),B)
& ? [E] :
( v1_funct_1(E)
& v1_funct_2(E,k2_zfmisc_1(B,B),B)
& m2_relset_1(E,k2_zfmisc_1(B,B),B)
& ( D = k1_realset1(u2_lattices(A),B) )
& ( E = k1_realset1(u1_lattices(A),B) )
& ( C = g3_lattices(B,D,E) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d16_filter_2) ).
tff(f_253,axiom,
! [A,B] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A)
& ~ v1_xboole_0(B)
& m2_lattice4(B,A) )
=> m2_nat_lat(k23_filter_2(A,B),A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k23_filter_2) ).
tff(f_763,axiom,
! [A,B,C,D] :
( m1_relset_1(C,A,B)
=> ( k8_relset_1(A,B,C,D) = k7_relat_1(C,D) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k8_relset_1) ).
tff(f_265,axiom,
! [A,B,C,D] :
( m1_relset_1(C,A,B)
=> m2_relset_1(k8_relset_1(A,B,C,D),A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k8_relset_1) ).
tff(c_6,plain,
v10_lattices('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_41]) ).
tff(c_4,plain,
l3_lattices('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_41]) ).
tff(c_33477,plain,
! [A_1897] :
( ( u1_struct_0(A_1897) = k17_filter_2(A_1897) )
| ~ l3_lattices(A_1897)
| ~ v10_lattices(A_1897)
| v3_struct_0(A_1897) ),
inference(cnfTransformation,[status(thm)],[f_195]) ).
tff(c_8,plain,
~ v3_struct_0('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_41]) ).
tff(c_33483,plain,
( ( u1_struct_0('#skF_1') = k17_filter_2('#skF_1') )
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1') ),
inference(resolution,[status(thm)],[c_33477,c_8]) ).
tff(c_33496,plain,
u1_struct_0('#skF_1') = k17_filter_2('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_4,c_33483]) ).
tff(c_33614,plain,
! [A_1909] :
( ( u1_struct_0(A_1909) = k1_filter_0(A_1909) )
| ~ l3_lattices(A_1909)
| ~ v10_lattices(A_1909)
| v3_struct_0(A_1909) ),
inference(cnfTransformation,[status(thm)],[f_181]) ).
tff(c_33620,plain,
( ( u1_struct_0('#skF_1') = k1_filter_0('#skF_1') )
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1') ),
inference(resolution,[status(thm)],[c_33614,c_8]) ).
tff(c_33633,plain,
k1_filter_0('#skF_1') = k17_filter_2('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_4,c_33496,c_33620]) ).
tff(c_33645,plain,
! [A_1910] :
( ( k1_filter_2(A_1910) = k1_filter_0(A_1910) )
| ~ l3_lattices(A_1910)
| ~ v10_lattices(A_1910)
| v3_struct_0(A_1910) ),
inference(cnfTransformation,[status(thm)],[f_755]) ).
tff(c_33651,plain,
( ( k1_filter_2('#skF_1') = k1_filter_0('#skF_1') )
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1') ),
inference(resolution,[status(thm)],[c_33645,c_8]) ).
tff(c_33664,plain,
k1_filter_2('#skF_1') = k17_filter_2('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_4,c_33633,c_33651]) ).
tff(c_498,plain,
! [A_221] :
( l2_lattices(A_221)
| ~ l3_lattices(A_221) ),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_516,plain,
l2_lattices('#skF_1'),
inference(resolution,[status(thm)],[c_4,c_498]) ).
tff(c_520,plain,
! [A_223] :
( l1_struct_0(A_223)
| ~ l2_lattices(A_223) ),
inference(cnfTransformation,[status(thm)],[f_273]) ).
tff(c_541,plain,
l1_struct_0('#skF_1'),
inference(resolution,[status(thm)],[c_516,c_520]) ).
tff(c_825,plain,
! [A_350] :
( ( u1_struct_0(A_350) = k17_filter_2(A_350) )
| ~ l3_lattices(A_350)
| ~ v10_lattices(A_350)
| v3_struct_0(A_350) ),
inference(cnfTransformation,[status(thm)],[f_195]) ).
tff(c_831,plain,
( ( u1_struct_0('#skF_1') = k17_filter_2('#skF_1') )
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1') ),
inference(resolution,[status(thm)],[c_825,c_8]) ).
tff(c_844,plain,
u1_struct_0('#skF_1') = k17_filter_2('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_4,c_831]) ).
tff(c_184,plain,
! [A_132] :
( ~ v1_xboole_0(u1_struct_0(A_132))
| ~ l1_struct_0(A_132)
| v3_struct_0(A_132) ),
inference(cnfTransformation,[status(thm)],[f_452]) ).
tff(c_856,plain,
( ~ v1_xboole_0(k17_filter_2('#skF_1'))
| ~ l1_struct_0('#skF_1')
| v3_struct_0('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_844,c_184]) ).
tff(c_860,plain,
( ~ v1_xboole_0(k17_filter_2('#skF_1'))
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_541,c_856]) ).
tff(c_861,plain,
~ v1_xboole_0(k17_filter_2('#skF_1')),
inference(negUnitSimplification,[status(thm)],[c_8,c_860]) ).
tff(c_2,plain,
( ( g3_lattices(u1_struct_0('#skF_1'),u2_lattices('#skF_1'),u1_lattices('#skF_1')) != k23_filter_2('#skF_1',k1_filter_2('#skF_1')) )
| ( g3_lattices(u1_struct_0('#skF_1'),u2_lattices('#skF_1'),u1_lattices('#skF_1')) != k23_filter_2('#skF_1',k17_filter_2('#skF_1')) ) ),
inference(cnfTransformation,[status(thm)],[f_41]) ).
tff(c_401,plain,
g3_lattices(u1_struct_0('#skF_1'),u2_lattices('#skF_1'),u1_lattices('#skF_1')) != k23_filter_2('#skF_1',k17_filter_2('#skF_1')),
inference(splitLeft,[status(thm)],[c_2]) ).
tff(c_852,plain,
g3_lattices(k17_filter_2('#skF_1'),u2_lattices('#skF_1'),u1_lattices('#skF_1')) != k23_filter_2('#skF_1',k17_filter_2('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_844,c_401]) ).
tff(c_879,plain,
! [A_354] :
( ( u1_struct_0(A_354) = k1_filter_0(A_354) )
| ~ l3_lattices(A_354)
| ~ v10_lattices(A_354)
| v3_struct_0(A_354) ),
inference(cnfTransformation,[status(thm)],[f_181]) ).
tff(c_885,plain,
( ( u1_struct_0('#skF_1') = k1_filter_0('#skF_1') )
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1') ),
inference(resolution,[status(thm)],[c_879,c_8]) ).
tff(c_898,plain,
k1_filter_0('#skF_1') = k17_filter_2('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_4,c_844,c_885]) ).
tff(c_942,plain,
! [A_358] :
( ( k1_filter_2(A_358) = k1_filter_0(A_358) )
| ~ l3_lattices(A_358)
| ~ v10_lattices(A_358)
| v3_struct_0(A_358) ),
inference(cnfTransformation,[status(thm)],[f_755]) ).
tff(c_948,plain,
( ( k1_filter_2('#skF_1') = k1_filter_0('#skF_1') )
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1') ),
inference(resolution,[status(thm)],[c_942,c_8]) ).
tff(c_961,plain,
k1_filter_2('#skF_1') = k17_filter_2('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_4,c_898,c_948]) ).
tff(c_88,plain,
! [A_77] :
( m1_filter_2(k1_filter_2(A_77),A_77)
| ~ l3_lattices(A_77)
| ~ v10_lattices(A_77)
| v3_struct_0(A_77) ),
inference(cnfTransformation,[status(thm)],[f_238]) ).
tff(c_972,plain,
( m1_filter_2(k17_filter_2('#skF_1'),'#skF_1')
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_961,c_88]) ).
tff(c_976,plain,
( m1_filter_2(k17_filter_2('#skF_1'),'#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_4,c_972]) ).
tff(c_977,plain,
m1_filter_2(k17_filter_2('#skF_1'),'#skF_1'),
inference(negUnitSimplification,[status(thm)],[c_8,c_976]) ).
tff(c_122,plain,
! [B_97,A_95] :
( m2_lattice4(B_97,A_95)
| ~ m1_filter_2(B_97,A_95)
| ~ l3_lattices(A_95)
| ~ v10_lattices(A_95)
| v3_struct_0(A_95) ),
inference(cnfTransformation,[status(thm)],[f_309]) ).
tff(c_405,plain,
! [A_215] :
( l1_lattices(A_215)
| ~ l3_lattices(A_215) ),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_423,plain,
l1_lattices('#skF_1'),
inference(resolution,[status(thm)],[c_4,c_405]) ).
tff(c_2076,plain,
! [A_502] :
( m2_relset_1(u1_lattices(A_502),k2_zfmisc_1(u1_struct_0(A_502),u1_struct_0(A_502)),u1_struct_0(A_502))
| ~ l1_lattices(A_502) ),
inference(cnfTransformation,[status(thm)],[f_365]) ).
tff(c_2100,plain,
( m2_relset_1(u1_lattices('#skF_1'),k2_zfmisc_1(u1_struct_0('#skF_1'),u1_struct_0('#skF_1')),k17_filter_2('#skF_1'))
| ~ l1_lattices('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_844,c_2076]) ).
tff(c_2114,plain,
m2_relset_1(u1_lattices('#skF_1'),k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1')),k17_filter_2('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_423,c_844,c_844,c_2100]) ).
tff(c_769,plain,
! [C_330,A_331,B_332] :
( m1_subset_1(C_330,k1_zfmisc_1(k2_zfmisc_1(A_331,B_332)))
| ~ m2_relset_1(C_330,A_331,B_332) ),
inference(cnfTransformation,[status(thm)],[f_357]) ).
tff(c_30,plain,
! [C_8,A_6,B_7] :
( v1_relat_1(C_8)
| ~ m1_subset_1(C_8,k1_zfmisc_1(k2_zfmisc_1(A_6,B_7))) ),
inference(cnfTransformation,[status(thm)],[f_82]) ).
tff(c_782,plain,
! [C_330,A_331,B_332] :
( v1_relat_1(C_330)
| ~ m2_relset_1(C_330,A_331,B_332) ),
inference(resolution,[status(thm)],[c_769,c_30]) ).
tff(c_2122,plain,
v1_relat_1(u1_lattices('#skF_1')),
inference(resolution,[status(thm)],[c_2114,c_782]) ).
tff(c_368,plain,
! [C_181,A_179,B_180] :
( m1_relset_1(C_181,A_179,B_180)
| ~ m2_relset_1(C_181,A_179,B_180) ),
inference(cnfTransformation,[status(thm)],[f_779]) ).
tff(c_2123,plain,
m1_relset_1(u1_lattices('#skF_1'),k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1')),k17_filter_2('#skF_1')),
inference(resolution,[status(thm)],[c_2114,c_368]) ).
tff(c_360,plain,
! [A_169,B_170,C_171] :
( ( k4_relset_1(A_169,B_170,C_171) = k1_relat_1(C_171) )
| ~ m1_relset_1(C_171,A_169,B_170) ),
inference(cnfTransformation,[status(thm)],[f_759]) ).
tff(c_2157,plain,
k4_relset_1(k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1')),k17_filter_2('#skF_1'),u1_lattices('#skF_1')) = k1_relat_1(u1_lattices('#skF_1')),
inference(resolution,[status(thm)],[c_2123,c_360]) ).
tff(c_1407,plain,
! [A_407,B_408,C_409] :
( m1_subset_1(k4_relset_1(A_407,B_408,C_409),k1_zfmisc_1(A_407))
| ~ m1_relset_1(C_409,A_407,B_408) ),
inference(cnfTransformation,[status(thm)],[f_257]) ).
tff(c_386,plain,
! [A_197,B_198] :
( r1_tarski(A_197,B_198)
| ~ m1_subset_1(A_197,k1_zfmisc_1(B_198)) ),
inference(cnfTransformation,[status(thm)],[f_826]) ).
tff(c_1436,plain,
! [A_407,B_408,C_409] :
( r1_tarski(k4_relset_1(A_407,B_408,C_409),A_407)
| ~ m1_relset_1(C_409,A_407,B_408) ),
inference(resolution,[status(thm)],[c_1407,c_386]) ).
tff(c_2173,plain,
( r1_tarski(k1_relat_1(u1_lattices('#skF_1')),k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1')))
| ~ m1_relset_1(u1_lattices('#skF_1'),k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1')),k17_filter_2('#skF_1')) ),
inference(superposition,[status(thm),theory(equality)],[c_2157,c_1436]) ).
tff(c_2180,plain,
r1_tarski(k1_relat_1(u1_lattices('#skF_1')),k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1'))),
inference(demodulation,[status(thm),theory(equality)],[c_2123,c_2173]) ).
tff(c_400,plain,
! [B_211,A_210] :
( ( k7_relat_1(B_211,A_210) = B_211 )
| ~ r1_tarski(k1_relat_1(B_211),A_210)
| ~ v1_relat_1(B_211) ),
inference(cnfTransformation,[status(thm)],[f_862]) ).
tff(c_2190,plain,
( ( k7_relat_1(u1_lattices('#skF_1'),k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1'))) = u1_lattices('#skF_1') )
| ~ v1_relat_1(u1_lattices('#skF_1')) ),
inference(resolution,[status(thm)],[c_2180,c_400]) ).
tff(c_2198,plain,
k7_relat_1(u1_lattices('#skF_1'),k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1'))) = u1_lattices('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_2122,c_2190]) ).
tff(c_76,plain,
! [A_68,B_70] :
( ( k7_relat_1(A_68,k2_zfmisc_1(B_70,B_70)) = k1_realset1(A_68,B_70) )
| ~ v1_relat_1(A_68) ),
inference(cnfTransformation,[status(thm)],[f_186]) ).
tff(c_2229,plain,
( ( k1_realset1(u1_lattices('#skF_1'),k17_filter_2('#skF_1')) = u1_lattices('#skF_1') )
| ~ v1_relat_1(u1_lattices('#skF_1')) ),
inference(superposition,[status(thm),theory(equality)],[c_2198,c_76]) ).
tff(c_2242,plain,
k1_realset1(u1_lattices('#skF_1'),k17_filter_2('#skF_1')) = u1_lattices('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_2122,c_2229]) ).
tff(c_2454,plain,
! [A_526] :
( m2_relset_1(u2_lattices(A_526),k2_zfmisc_1(u1_struct_0(A_526),u1_struct_0(A_526)),u1_struct_0(A_526))
| ~ l2_lattices(A_526) ),
inference(cnfTransformation,[status(thm)],[f_373]) ).
tff(c_2472,plain,
( m2_relset_1(u2_lattices('#skF_1'),k2_zfmisc_1(k17_filter_2('#skF_1'),u1_struct_0('#skF_1')),u1_struct_0('#skF_1'))
| ~ l2_lattices('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_844,c_2454]) ).
tff(c_2488,plain,
m2_relset_1(u2_lattices('#skF_1'),k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1')),k17_filter_2('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_516,c_844,c_844,c_2472]) ).
tff(c_2508,plain,
v1_relat_1(u2_lattices('#skF_1')),
inference(resolution,[status(thm)],[c_2488,c_782]) ).
tff(c_2509,plain,
m1_relset_1(u2_lattices('#skF_1'),k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1')),k17_filter_2('#skF_1')),
inference(resolution,[status(thm)],[c_2488,c_368]) ).
tff(c_2545,plain,
k4_relset_1(k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1')),k17_filter_2('#skF_1'),u2_lattices('#skF_1')) = k1_relat_1(u2_lattices('#skF_1')),
inference(resolution,[status(thm)],[c_2509,c_360]) ).
tff(c_2555,plain,
( r1_tarski(k1_relat_1(u2_lattices('#skF_1')),k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1')))
| ~ m1_relset_1(u2_lattices('#skF_1'),k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1')),k17_filter_2('#skF_1')) ),
inference(superposition,[status(thm),theory(equality)],[c_2545,c_1436]) ).
tff(c_2562,plain,
r1_tarski(k1_relat_1(u2_lattices('#skF_1')),k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1'))),
inference(demodulation,[status(thm),theory(equality)],[c_2509,c_2555]) ).
tff(c_2572,plain,
( ( k7_relat_1(u2_lattices('#skF_1'),k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1'))) = u2_lattices('#skF_1') )
| ~ v1_relat_1(u2_lattices('#skF_1')) ),
inference(resolution,[status(thm)],[c_2562,c_400]) ).
tff(c_2580,plain,
k7_relat_1(u2_lattices('#skF_1'),k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1'))) = u2_lattices('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_2508,c_2572]) ).
tff(c_2611,plain,
( ( k1_realset1(u2_lattices('#skF_1'),k17_filter_2('#skF_1')) = u2_lattices('#skF_1') )
| ~ v1_relat_1(u2_lattices('#skF_1')) ),
inference(superposition,[status(thm),theory(equality)],[c_2580,c_76]) ).
tff(c_2624,plain,
k1_realset1(u2_lattices('#skF_1'),k17_filter_2('#skF_1')) = u2_lattices('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_2508,c_2611]) ).
tff(c_2419,plain,
! [A_525] :
( v1_funct_2(u1_lattices(A_525),k2_zfmisc_1(u1_struct_0(A_525),u1_struct_0(A_525)),u1_struct_0(A_525))
| ~ l1_lattices(A_525) ),
inference(cnfTransformation,[status(thm)],[f_365]) ).
tff(c_2431,plain,
( v1_funct_2(u1_lattices('#skF_1'),k2_zfmisc_1(k17_filter_2('#skF_1'),u1_struct_0('#skF_1')),u1_struct_0('#skF_1'))
| ~ l1_lattices('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_844,c_2419]) ).
tff(c_2445,plain,
v1_funct_2(u1_lattices('#skF_1'),k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1')),k17_filter_2('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_423,c_844,c_844,c_2431]) ).
tff(c_304,plain,
v1_xboole_0('#skF_21'),
inference(cnfTransformation,[status(thm)],[f_684]) ).
tff(c_444,plain,
! [A_217] :
( ( k1_xboole_0 = A_217 )
| ~ v1_xboole_0(A_217) ),
inference(cnfTransformation,[status(thm)],[f_843]) ).
tff(c_459,plain,
k1_xboole_0 = '#skF_21',
inference(resolution,[status(thm)],[c_304,c_444]) ).
tff(c_72,plain,
! [B_65,A_64,C_66] :
( ( k1_xboole_0 = B_65 )
| ( k4_relset_1(A_64,B_65,C_66) = A_64 )
| ~ v1_funct_2(C_66,A_64,B_65)
| ~ m2_relset_1(C_66,A_64,B_65) ),
inference(cnfTransformation,[status(thm)],[f_172]) ).
tff(c_3736,plain,
! [B_593,A_594,C_595] :
( ( B_593 = '#skF_21' )
| ( k4_relset_1(A_594,B_593,C_595) = A_594 )
| ~ v1_funct_2(C_595,A_594,B_593)
| ~ m2_relset_1(C_595,A_594,B_593) ),
inference(demodulation,[status(thm),theory(equality)],[c_459,c_72]) ).
tff(c_3745,plain,
( ( k17_filter_2('#skF_1') = '#skF_21' )
| ( k4_relset_1(k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1')),k17_filter_2('#skF_1'),u1_lattices('#skF_1')) = k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1')) )
| ~ m2_relset_1(u1_lattices('#skF_1'),k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1')),k17_filter_2('#skF_1')) ),
inference(resolution,[status(thm)],[c_2445,c_3736]) ).
tff(c_3767,plain,
( ( k17_filter_2('#skF_1') = '#skF_21' )
| ( k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1')) = k1_relat_1(u1_lattices('#skF_1')) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2114,c_2157,c_3745]) ).
tff(c_3780,plain,
k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1')) = k1_relat_1(u1_lattices('#skF_1')),
inference(splitLeft,[status(thm)],[c_3767]) ).
tff(c_1763,plain,
! [A_475] :
( v1_funct_2(u2_lattices(A_475),k2_zfmisc_1(u1_struct_0(A_475),u1_struct_0(A_475)),u1_struct_0(A_475))
| ~ l2_lattices(A_475) ),
inference(cnfTransformation,[status(thm)],[f_373]) ).
tff(c_1775,plain,
( v1_funct_2(u2_lattices('#skF_1'),k2_zfmisc_1(k17_filter_2('#skF_1'),u1_struct_0('#skF_1')),u1_struct_0('#skF_1'))
| ~ l2_lattices('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_844,c_1763]) ).
tff(c_1789,plain,
v1_funct_2(u2_lattices('#skF_1'),k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1')),k17_filter_2('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_516,c_844,c_844,c_1775]) ).
tff(c_3795,plain,
v1_funct_2(u2_lattices('#skF_1'),k1_relat_1(u1_lattices('#skF_1')),k17_filter_2('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_3780,c_1789]) ).
tff(c_3787,plain,
m2_relset_1(u2_lattices('#skF_1'),k1_relat_1(u1_lattices('#skF_1')),k17_filter_2('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_3780,c_2488]) ).
tff(c_3788,plain,
v1_funct_2(u1_lattices('#skF_1'),k1_relat_1(u1_lattices('#skF_1')),k17_filter_2('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_3780,c_2445]) ).
tff(c_3794,plain,
m2_relset_1(u1_lattices('#skF_1'),k1_relat_1(u1_lattices('#skF_1')),k17_filter_2('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_3780,c_2114]) ).
tff(c_7166,plain,
! [B_805,A_806] :
( ( g3_lattices(B_805,k1_realset1(u2_lattices(A_806),B_805),k1_realset1(u1_lattices(A_806),B_805)) = k23_filter_2(A_806,B_805) )
| ~ m2_relset_1(k1_realset1(u1_lattices(A_806),B_805),k2_zfmisc_1(B_805,B_805),B_805)
| ~ v1_funct_2(k1_realset1(u1_lattices(A_806),B_805),k2_zfmisc_1(B_805,B_805),B_805)
| ~ v1_funct_1(k1_realset1(u1_lattices(A_806),B_805))
| ~ m2_relset_1(k1_realset1(u2_lattices(A_806),B_805),k2_zfmisc_1(B_805,B_805),B_805)
| ~ v1_funct_2(k1_realset1(u2_lattices(A_806),B_805),k2_zfmisc_1(B_805,B_805),B_805)
| ~ v1_funct_1(k1_realset1(u2_lattices(A_806),B_805))
| ~ m2_nat_lat(g3_lattices(B_805,k1_realset1(u2_lattices(A_806),B_805),k1_realset1(u1_lattices(A_806),B_805)),A_806)
| ~ m2_lattice4(B_805,A_806)
| v1_xboole_0(B_805)
| ~ l3_lattices(A_806)
| ~ v10_lattices(A_806)
| v3_struct_0(A_806) ),
inference(cnfTransformation,[status(thm)],[f_154]) ).
tff(c_7173,plain,
( ( g3_lattices(k17_filter_2('#skF_1'),k1_realset1(u2_lattices('#skF_1'),k17_filter_2('#skF_1')),k1_realset1(u1_lattices('#skF_1'),k17_filter_2('#skF_1'))) = k23_filter_2('#skF_1',k17_filter_2('#skF_1')) )
| ~ m2_relset_1(k1_realset1(u1_lattices('#skF_1'),k17_filter_2('#skF_1')),k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1')),k17_filter_2('#skF_1'))
| ~ v1_funct_2(k1_realset1(u1_lattices('#skF_1'),k17_filter_2('#skF_1')),k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1')),k17_filter_2('#skF_1'))
| ~ v1_funct_1(k1_realset1(u1_lattices('#skF_1'),k17_filter_2('#skF_1')))
| ~ m2_relset_1(k1_realset1(u2_lattices('#skF_1'),k17_filter_2('#skF_1')),k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1')),k17_filter_2('#skF_1'))
| ~ v1_funct_2(u2_lattices('#skF_1'),k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1')),k17_filter_2('#skF_1'))
| ~ v1_funct_1(k1_realset1(u2_lattices('#skF_1'),k17_filter_2('#skF_1')))
| ~ m2_nat_lat(g3_lattices(k17_filter_2('#skF_1'),k1_realset1(u2_lattices('#skF_1'),k17_filter_2('#skF_1')),k1_realset1(u1_lattices('#skF_1'),k17_filter_2('#skF_1'))),'#skF_1')
| ~ m2_lattice4(k17_filter_2('#skF_1'),'#skF_1')
| v1_xboole_0(k17_filter_2('#skF_1'))
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_2624,c_7166]) ).
tff(c_7178,plain,
( ( g3_lattices(k17_filter_2('#skF_1'),u2_lattices('#skF_1'),u1_lattices('#skF_1')) = k23_filter_2('#skF_1',k17_filter_2('#skF_1')) )
| ~ v1_funct_1(u1_lattices('#skF_1'))
| ~ v1_funct_1(u2_lattices('#skF_1'))
| ~ m2_nat_lat(g3_lattices(k17_filter_2('#skF_1'),u2_lattices('#skF_1'),u1_lattices('#skF_1')),'#skF_1')
| ~ m2_lattice4(k17_filter_2('#skF_1'),'#skF_1')
| v1_xboole_0(k17_filter_2('#skF_1'))
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_4,c_2242,c_2624,c_2624,c_3795,c_3780,c_3787,c_2624,c_3780,c_2242,c_3788,c_2242,c_3780,c_3794,c_2242,c_3780,c_2242,c_2624,c_7173]) ).
tff(c_7179,plain,
( ~ v1_funct_1(u1_lattices('#skF_1'))
| ~ v1_funct_1(u2_lattices('#skF_1'))
| ~ m2_nat_lat(g3_lattices(k17_filter_2('#skF_1'),u2_lattices('#skF_1'),u1_lattices('#skF_1')),'#skF_1')
| ~ m2_lattice4(k17_filter_2('#skF_1'),'#skF_1') ),
inference(negUnitSimplification,[status(thm)],[c_8,c_861,c_852,c_7178]) ).
tff(c_7181,plain,
~ m2_lattice4(k17_filter_2('#skF_1'),'#skF_1'),
inference(splitLeft,[status(thm)],[c_7179]) ).
tff(c_7184,plain,
( ~ m1_filter_2(k17_filter_2('#skF_1'),'#skF_1')
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_122,c_7181]) ).
tff(c_7190,plain,
v3_struct_0('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_4,c_977,c_7184]) ).
tff(c_7192,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8,c_7190]) ).
tff(c_7194,plain,
m2_lattice4(k17_filter_2('#skF_1'),'#skF_1'),
inference(splitRight,[status(thm)],[c_7179]) ).
tff(c_98,plain,
! [A_78,B_79] :
( m2_nat_lat(k23_filter_2(A_78,B_79),A_78)
| ~ m2_lattice4(B_79,A_78)
| v1_xboole_0(B_79)
| ~ l3_lattices(A_78)
| ~ v10_lattices(A_78)
| v3_struct_0(A_78) ),
inference(cnfTransformation,[status(thm)],[f_253]) ).
tff(c_5696,plain,
! [A_710,B_711] :
( ( k1_realset1(u2_lattices(A_710),B_711) = '#skF_2'(A_710,B_711,k23_filter_2(A_710,B_711)) )
| ~ m2_nat_lat(k23_filter_2(A_710,B_711),A_710)
| ~ m2_lattice4(B_711,A_710)
| v1_xboole_0(B_711)
| ~ l3_lattices(A_710)
| ~ v10_lattices(A_710)
| v3_struct_0(A_710) ),
inference(cnfTransformation,[status(thm)],[f_154]) ).
tff(c_5699,plain,
! [A_78,B_79] :
( ( k1_realset1(u2_lattices(A_78),B_79) = '#skF_2'(A_78,B_79,k23_filter_2(A_78,B_79)) )
| ~ m2_lattice4(B_79,A_78)
| v1_xboole_0(B_79)
| ~ l3_lattices(A_78)
| ~ v10_lattices(A_78)
| v3_struct_0(A_78) ),
inference(resolution,[status(thm)],[c_98,c_5696]) ).
tff(c_5794,plain,
! [A_721,B_722] :
( ( k1_realset1(u1_lattices(A_721),B_722) = '#skF_3'(A_721,B_722,k23_filter_2(A_721,B_722)) )
| ~ m2_nat_lat(k23_filter_2(A_721,B_722),A_721)
| ~ m2_lattice4(B_722,A_721)
| v1_xboole_0(B_722)
| ~ l3_lattices(A_721)
| ~ v10_lattices(A_721)
| v3_struct_0(A_721) ),
inference(cnfTransformation,[status(thm)],[f_154]) ).
tff(c_11022,plain,
! [A_971,B_972] :
( ( k1_realset1(u1_lattices(A_971),B_972) = '#skF_3'(A_971,B_972,k23_filter_2(A_971,B_972)) )
| ~ m2_lattice4(B_972,A_971)
| v1_xboole_0(B_972)
| ~ l3_lattices(A_971)
| ~ v10_lattices(A_971)
| v3_struct_0(A_971) ),
inference(resolution,[status(thm)],[c_98,c_5794]) ).
tff(c_362,plain,
! [A_172,B_173,C_174,D_175] :
( ( k8_relset_1(A_172,B_173,C_174,D_175) = k7_relat_1(C_174,D_175) )
| ~ m1_relset_1(C_174,A_172,B_173) ),
inference(cnfTransformation,[status(thm)],[f_763]) ).
tff(c_2697,plain,
! [D_542] : ( k8_relset_1(k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1')),k17_filter_2('#skF_1'),u1_lattices('#skF_1'),D_542) = k7_relat_1(u1_lattices('#skF_1'),D_542) ),
inference(resolution,[status(thm)],[c_2123,c_362]) ).
tff(c_106,plain,
! [A_85,B_86,C_87,D_88] :
( m2_relset_1(k8_relset_1(A_85,B_86,C_87,D_88),A_85,B_86)
| ~ m1_relset_1(C_87,A_85,B_86) ),
inference(cnfTransformation,[status(thm)],[f_265]) ).
tff(c_2709,plain,
! [D_542] :
( m2_relset_1(k7_relat_1(u1_lattices('#skF_1'),D_542),k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1')),k17_filter_2('#skF_1'))
| ~ m1_relset_1(u1_lattices('#skF_1'),k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1')),k17_filter_2('#skF_1')) ),
inference(superposition,[status(thm),theory(equality)],[c_2697,c_106]) ).
tff(c_2719,plain,
! [D_542] : m2_relset_1(k7_relat_1(u1_lattices('#skF_1'),D_542),k2_zfmisc_1(k17_filter_2('#skF_1'),k17_filter_2('#skF_1')),k17_filter_2('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_2123,c_2709]) ).
tff(c_6572,plain,
! [D_763] : m2_relset_1(k7_relat_1(u1_lattices('#skF_1'),D_763),k1_relat_1(u1_lattices('#skF_1')),k17_filter_2('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_3780,c_2719]) ).
tff(c_6603,plain,
! [D_764] : m1_relset_1(k7_relat_1(u1_lattices('#skF_1'),D_764),k1_relat_1(u1_lattices('#skF_1')),k17_filter_2('#skF_1')),
inference(resolution,[status(thm)],[c_6572,c_368]) ).
tff(c_6621,plain,
! [B_70] :
( m1_relset_1(k1_realset1(u1_lattices('#skF_1'),B_70),k1_relat_1(u1_lattices('#skF_1')),k17_filter_2('#skF_1'))
| ~ v1_relat_1(u1_lattices('#skF_1')) ),
inference(superposition,[status(thm),theory(equality)],[c_76,c_6603]) ).
tff(c_6634,plain,
! [B_70] : m1_relset_1(k1_realset1(u1_lattices('#skF_1'),B_70),k1_relat_1(u1_lattices('#skF_1')),k17_filter_2('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_2122,c_6621]) ).
tff(c_11051,plain,
! [B_972] :
( m1_relset_1('#skF_3'('#skF_1',B_972,k23_filter_2('#skF_1',B_972)),k1_relat_1(u1_lattices('#skF_1')),k17_filter_2('#skF_1'))
| ~ m2_lattice4(B_972,'#skF_1')
| v1_xboole_0(B_972)
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_11022,c_6634]) ).
tff(c_11092,plain,
! [B_972] :
( m1_relset_1('#skF_3'('#skF_1',B_972,k23_filter_2('#skF_1',B_972)),k1_relat_1(u1_lattices('#skF_1')),k17_filter_2('#skF_1'))
| ~ m2_lattice4(B_972,'#skF_1')
| v1_xboole_0(B_972)
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_4,c_11051]) ).
tff(c_11727,plain,
! [B_1021] :
( m1_relset_1('#skF_3'('#skF_1',B_1021,k23_filter_2('#skF_1',B_1021)),k1_relat_1(u1_lattices('#skF_1')),k17_filter_2('#skF_1'))
| ~ m2_lattice4(B_1021,'#skF_1')
| v1_xboole_0(B_1021) ),
inference(negUnitSimplification,[status(thm)],[c_8,c_11092]) ).
tff(c_16079,plain,
! [B_1305] :
( ( k4_relset_1(k1_relat_1(u1_lattices('#skF_1')),k17_filter_2('#skF_1'),'#skF_3'('#skF_1',B_1305,k23_filter_2('#skF_1',B_1305))) = k1_relat_1('#skF_3'('#skF_1',B_1305,k23_filter_2('#skF_1',B_1305))) )
| ~ m2_lattice4(B_1305,'#skF_1')
| v1_xboole_0(B_1305) ),
inference(resolution,[status(thm)],[c_11727,c_360]) ).
tff(c_5985,plain,
! [A_730,B_731] :
( m2_relset_1('#skF_3'(A_730,B_731,k23_filter_2(A_730,B_731)),k2_zfmisc_1(B_731,B_731),B_731)
| ~ m2_nat_lat(k23_filter_2(A_730,B_731),A_730)
| ~ m2_lattice4(B_731,A_730)
| v1_xboole_0(B_731)
| ~ l3_lattices(A_730)
| ~ v10_lattices(A_730)
| v3_struct_0(A_730) ),
inference(cnfTransformation,[status(thm)],[f_154]) ).
tff(c_5994,plain,
! [A_730] :
( m2_relset_1('#skF_3'(A_730,k17_filter_2('#skF_1'),k23_filter_2(A_730,k17_filter_2('#skF_1'))),k1_relat_1(u1_lattices('#skF_1')),k17_filter_2('#skF_1'))
| ~ m2_nat_lat(k23_filter_2(A_730,k17_filter_2('#skF_1')),A_730)
| ~ m2_lattice4(k17_filter_2('#skF_1'),A_730)
| v1_xboole_0(k17_filter_2('#skF_1'))
| ~ l3_lattices(A_730)
| ~ v10_lattices(A_730)
| v3_struct_0(A_730) ),
inference(superposition,[status(thm),theory(equality)],[c_3780,c_5985]) ).
tff(c_5997,plain,
! [A_730] :
( m2_relset_1('#skF_3'(A_730,k17_filter_2('#skF_1'),k23_filter_2(A_730,k17_filter_2('#skF_1'))),k1_relat_1(u1_lattices('#skF_1')),k17_filter_2('#skF_1'))
| ~ m2_nat_lat(k23_filter_2(A_730,k17_filter_2('#skF_1')),A_730)
| ~ m2_lattice4(k17_filter_2('#skF_1'),A_730)
| ~ l3_lattices(A_730)
| ~ v10_lattices(A_730)
| v3_struct_0(A_730) ),
inference(negUnitSimplification,[status(thm)],[c_861,c_5994]) ).
tff(c_6039,plain,
! [A_736,B_737] :
( v1_funct_2('#skF_2'(A_736,B_737,k23_filter_2(A_736,B_737)),k2_zfmisc_1(B_737,B_737),B_737)
| ~ m2_nat_lat(k23_filter_2(A_736,B_737),A_736)
| ~ m2_lattice4(B_737,A_736)
| v1_xboole_0(B_737)
| ~ l3_lattices(A_736)
| ~ v10_lattices(A_736)
| v3_struct_0(A_736) ),
inference(cnfTransformation,[status(thm)],[f_154]) ).
tff(c_6049,plain,
! [A_736] :
( v1_funct_2('#skF_2'(A_736,k17_filter_2('#skF_1'),k23_filter_2(A_736,k17_filter_2('#skF_1'))),k1_relat_1(u1_lattices('#skF_1')),k17_filter_2('#skF_1'))
| ~ m2_nat_lat(k23_filter_2(A_736,k17_filter_2('#skF_1')),A_736)
| ~ m2_lattice4(k17_filter_2('#skF_1'),A_736)
| v1_xboole_0(k17_filter_2('#skF_1'))
| ~ l3_lattices(A_736)
| ~ v10_lattices(A_736)
| v3_struct_0(A_736) ),
inference(superposition,[status(thm),theory(equality)],[c_3780,c_6039]) ).
tff(c_7160,plain,
! [A_804] :
( v1_funct_2('#skF_2'(A_804,k17_filter_2('#skF_1'),k23_filter_2(A_804,k17_filter_2('#skF_1'))),k1_relat_1(u1_lattices('#skF_1')),k17_filter_2('#skF_1'))
| ~ m2_nat_lat(k23_filter_2(A_804,k17_filter_2('#skF_1')),A_804)
| ~ m2_lattice4(k17_filter_2('#skF_1'),A_804)
| ~ l3_lattices(A_804)
| ~ v10_lattices(A_804)
| v3_struct_0(A_804) ),
inference(negUnitSimplification,[status(thm)],[c_861,c_6049]) ).
tff(c_3735,plain,
! [B_65,A_64,C_66] :
( ( B_65 = '#skF_21' )
| ( k4_relset_1(A_64,B_65,C_66) = A_64 )
| ~ v1_funct_2(C_66,A_64,B_65)
| ~ m2_relset_1(C_66,A_64,B_65) ),
inference(demodulation,[status(thm),theory(equality)],[c_459,c_72]) ).
tff(c_7164,plain,
! [A_804] :
( ( k17_filter_2('#skF_1') = '#skF_21' )
| ( k4_relset_1(k1_relat_1(u1_lattices('#skF_1')),k17_filter_2('#skF_1'),'#skF_2'(A_804,k17_filter_2('#skF_1'),k23_filter_2(A_804,k17_filter_2('#skF_1')))) = k1_relat_1(u1_lattices('#skF_1')) )
| ~ m2_relset_1('#skF_2'(A_804,k17_filter_2('#skF_1'),k23_filter_2(A_804,k17_filter_2('#skF_1'))),k1_relat_1(u1_lattices('#skF_1')),k17_filter_2('#skF_1'))
| ~ m2_nat_lat(k23_filter_2(A_804,k17_filter_2('#skF_1')),A_804)
| ~ m2_lattice4(k17_filter_2('#skF_1'),A_804)
| ~ l3_lattices(A_804)
| ~ v10_lattices(A_804)
| v3_struct_0(A_804) ),
inference(resolution,[status(thm)],[c_7160,c_3735]) ).
tff(c_10361,plain,
k17_filter_2('#skF_1') = '#skF_21',
inference(splitLeft,[status(thm)],[c_7164]) ).
tff(c_10451,plain,
~ v1_xboole_0('#skF_21'),
inference(demodulation,[status(thm),theory(equality)],[c_10361,c_861]) ).
tff(c_10457,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_304,c_10451]) ).
tff(c_10459,plain,
k17_filter_2('#skF_1') != '#skF_21',
inference(splitRight,[status(thm)],[c_7164]) ).
tff(c_6296,plain,
! [A_749,B_750] :
( v1_funct_2('#skF_3'(A_749,B_750,k23_filter_2(A_749,B_750)),k2_zfmisc_1(B_750,B_750),B_750)
| ~ m2_nat_lat(k23_filter_2(A_749,B_750),A_749)
| ~ m2_lattice4(B_750,A_749)
| v1_xboole_0(B_750)
| ~ l3_lattices(A_749)
| ~ v10_lattices(A_749)
| v3_struct_0(A_749) ),
inference(cnfTransformation,[status(thm)],[f_154]) ).
tff(c_6306,plain,
! [A_749] :
( v1_funct_2('#skF_3'(A_749,k17_filter_2('#skF_1'),k23_filter_2(A_749,k17_filter_2('#skF_1'))),k1_relat_1(u1_lattices('#skF_1')),k17_filter_2('#skF_1'))
| ~ m2_nat_lat(k23_filter_2(A_749,k17_filter_2('#skF_1')),A_749)
| ~ m2_lattice4(k17_filter_2('#skF_1'),A_749)
| v1_xboole_0(k17_filter_2('#skF_1'))
| ~ l3_lattices(A_749)
| ~ v10_lattices(A_749)
| v3_struct_0(A_749) ),
inference(superposition,[status(thm),theory(equality)],[c_3780,c_6296]) ).
tff(c_6677,plain,
! [A_769] :
( v1_funct_2('#skF_3'(A_769,k17_filter_2('#skF_1'),k23_filter_2(A_769,k17_filter_2('#skF_1'))),k1_relat_1(u1_lattices('#skF_1')),k17_filter_2('#skF_1'))
| ~ m2_nat_lat(k23_filter_2(A_769,k17_filter_2('#skF_1')),A_769)
| ~ m2_lattice4(k17_filter_2('#skF_1'),A_769)
| ~ l3_lattices(A_769)
| ~ v10_lattices(A_769)
| v3_struct_0(A_769) ),
inference(negUnitSimplification,[status(thm)],[c_861,c_6306]) ).
tff(c_6681,plain,
! [A_769] :
( ( k17_filter_2('#skF_1') = '#skF_21' )
| ( k4_relset_1(k1_relat_1(u1_lattices('#skF_1')),k17_filter_2('#skF_1'),'#skF_3'(A_769,k17_filter_2('#skF_1'),k23_filter_2(A_769,k17_filter_2('#skF_1')))) = k1_relat_1(u1_lattices('#skF_1')) )
| ~ m2_relset_1('#skF_3'(A_769,k17_filter_2('#skF_1'),k23_filter_2(A_769,k17_filter_2('#skF_1'))),k1_relat_1(u1_lattices('#skF_1')),k17_filter_2('#skF_1'))
| ~ m2_nat_lat(k23_filter_2(A_769,k17_filter_2('#skF_1')),A_769)
| ~ m2_lattice4(k17_filter_2('#skF_1'),A_769)
| ~ l3_lattices(A_769)
| ~ v10_lattices(A_769)
| v3_struct_0(A_769) ),
inference(resolution,[status(thm)],[c_6677,c_3735]) ).
tff(c_10587,plain,
! [A_948] :
( ( k4_relset_1(k1_relat_1(u1_lattices('#skF_1')),k17_filter_2('#skF_1'),'#skF_3'(A_948,k17_filter_2('#skF_1'),k23_filter_2(A_948,k17_filter_2('#skF_1')))) = k1_relat_1(u1_lattices('#skF_1')) )
| ~ m2_relset_1('#skF_3'(A_948,k17_filter_2('#skF_1'),k23_filter_2(A_948,k17_filter_2('#skF_1'))),k1_relat_1(u1_lattices('#skF_1')),k17_filter_2('#skF_1'))
| ~ m2_nat_lat(k23_filter_2(A_948,k17_filter_2('#skF_1')),A_948)
| ~ m2_lattice4(k17_filter_2('#skF_1'),A_948)
| ~ l3_lattices(A_948)
| ~ v10_lattices(A_948)
| v3_struct_0(A_948) ),
inference(negUnitSimplification,[status(thm)],[c_10459,c_6681]) ).
tff(c_10594,plain,
! [A_730] :
( ( k4_relset_1(k1_relat_1(u1_lattices('#skF_1')),k17_filter_2('#skF_1'),'#skF_3'(A_730,k17_filter_2('#skF_1'),k23_filter_2(A_730,k17_filter_2('#skF_1')))) = k1_relat_1(u1_lattices('#skF_1')) )
| ~ m2_nat_lat(k23_filter_2(A_730,k17_filter_2('#skF_1')),A_730)
| ~ m2_lattice4(k17_filter_2('#skF_1'),A_730)
| ~ l3_lattices(A_730)
| ~ v10_lattices(A_730)
| v3_struct_0(A_730) ),
inference(resolution,[status(thm)],[c_5997,c_10587]) ).
tff(c_16086,plain,
( ( k1_relat_1('#skF_3'('#skF_1',k17_filter_2('#skF_1'),k23_filter_2('#skF_1',k17_filter_2('#skF_1')))) = k1_relat_1(u1_lattices('#skF_1')) )
| ~ m2_nat_lat(k23_filter_2('#skF_1',k17_filter_2('#skF_1')),'#skF_1')
| ~ m2_lattice4(k17_filter_2('#skF_1'),'#skF_1')
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1')
| ~ m2_lattice4(k17_filter_2('#skF_1'),'#skF_1')
| v1_xboole_0(k17_filter_2('#skF_1')) ),
inference(superposition,[status(thm),theory(equality)],[c_16079,c_10594]) ).
tff(c_16121,plain,
( ( k1_relat_1('#skF_3'('#skF_1',k17_filter_2('#skF_1'),k23_filter_2('#skF_1',k17_filter_2('#skF_1')))) = k1_relat_1(u1_lattices('#skF_1')) )
| ~ m2_nat_lat(k23_filter_2('#skF_1',k17_filter_2('#skF_1')),'#skF_1')
| v3_struct_0('#skF_1')
| v1_xboole_0(k17_filter_2('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_7194,c_6,c_4,c_7194,c_16086]) ).
tff(c_16122,plain,
( ( k1_relat_1('#skF_3'('#skF_1',k17_filter_2('#skF_1'),k23_filter_2('#skF_1',k17_filter_2('#skF_1')))) = k1_relat_1(u1_lattices('#skF_1')) )
| ~ m2_nat_lat(k23_filter_2('#skF_1',k17_filter_2('#skF_1')),'#skF_1') ),
inference(negUnitSimplification,[status(thm)],[c_861,c_8,c_16121]) ).
tff(c_16262,plain,
~ m2_nat_lat(k23_filter_2('#skF_1',k17_filter_2('#skF_1')),'#skF_1'),
inference(splitLeft,[status(thm)],[c_16122]) ).
tff(c_16265,plain,
( ~ m2_lattice4(k17_filter_2('#skF_1'),'#skF_1')
| v1_xboole_0(k17_filter_2('#skF_1'))
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_98,c_16262]) ).
tff(c_16268,plain,
( v1_xboole_0(k17_filter_2('#skF_1'))
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_4,c_7194,c_16265]) ).
tff(c_16270,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8,c_861,c_16268]) ).
tff(c_16272,plain,
m2_nat_lat(k23_filter_2('#skF_1',k17_filter_2('#skF_1')),'#skF_1'),
inference(splitRight,[status(thm)],[c_16122]) ).
tff(c_44,plain,
! [B_39,A_11] :
( ( g3_lattices(B_39,'#skF_2'(A_11,B_39,k23_filter_2(A_11,B_39)),'#skF_3'(A_11,B_39,k23_filter_2(A_11,B_39))) = k23_filter_2(A_11,B_39) )
| ~ m2_nat_lat(k23_filter_2(A_11,B_39),A_11)
| ~ m2_lattice4(B_39,A_11)
| v1_xboole_0(B_39)
| ~ l3_lattices(A_11)
| ~ v10_lattices(A_11)
| v3_struct_0(A_11) ),
inference(cnfTransformation,[status(thm)],[f_154]) ).
tff(c_32696,plain,
! [B_1769,A_1770] :
( ( g3_lattices(B_1769,'#skF_2'(A_1770,B_1769,k23_filter_2(A_1770,B_1769)),k1_realset1(u1_lattices(A_1770),B_1769)) = k23_filter_2(A_1770,B_1769) )
| ~ m2_nat_lat(k23_filter_2(A_1770,B_1769),A_1770)
| ~ m2_lattice4(B_1769,A_1770)
| v1_xboole_0(B_1769)
| ~ l3_lattices(A_1770)
| ~ v10_lattices(A_1770)
| v3_struct_0(A_1770)
| ~ m2_lattice4(B_1769,A_1770)
| v1_xboole_0(B_1769)
| ~ l3_lattices(A_1770)
| ~ v10_lattices(A_1770)
| v3_struct_0(A_1770) ),
inference(superposition,[status(thm),theory(equality)],[c_11022,c_44]) ).
tff(c_32761,plain,
( ( g3_lattices(k17_filter_2('#skF_1'),'#skF_2'('#skF_1',k17_filter_2('#skF_1'),k23_filter_2('#skF_1',k17_filter_2('#skF_1'))),u1_lattices('#skF_1')) = k23_filter_2('#skF_1',k17_filter_2('#skF_1')) )
| ~ m2_nat_lat(k23_filter_2('#skF_1',k17_filter_2('#skF_1')),'#skF_1')
| ~ m2_lattice4(k17_filter_2('#skF_1'),'#skF_1')
| v1_xboole_0(k17_filter_2('#skF_1'))
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1')
| ~ m2_lattice4(k17_filter_2('#skF_1'),'#skF_1')
| v1_xboole_0(k17_filter_2('#skF_1'))
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_2242,c_32696]) ).
tff(c_32768,plain,
( ( g3_lattices(k17_filter_2('#skF_1'),'#skF_2'('#skF_1',k17_filter_2('#skF_1'),k23_filter_2('#skF_1',k17_filter_2('#skF_1'))),u1_lattices('#skF_1')) = k23_filter_2('#skF_1',k17_filter_2('#skF_1')) )
| v1_xboole_0(k17_filter_2('#skF_1'))
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_4,c_7194,c_6,c_4,c_7194,c_16272,c_32761]) ).
tff(c_32769,plain,
g3_lattices(k17_filter_2('#skF_1'),'#skF_2'('#skF_1',k17_filter_2('#skF_1'),k23_filter_2('#skF_1',k17_filter_2('#skF_1'))),u1_lattices('#skF_1')) = k23_filter_2('#skF_1',k17_filter_2('#skF_1')),
inference(negUnitSimplification,[status(thm)],[c_8,c_861,c_32768]) ).
tff(c_33052,plain,
( ( g3_lattices(k17_filter_2('#skF_1'),k1_realset1(u2_lattices('#skF_1'),k17_filter_2('#skF_1')),u1_lattices('#skF_1')) = k23_filter_2('#skF_1',k17_filter_2('#skF_1')) )
| ~ m2_lattice4(k17_filter_2('#skF_1'),'#skF_1')
| v1_xboole_0(k17_filter_2('#skF_1'))
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_5699,c_32769]) ).
tff(c_33077,plain,
( ( g3_lattices(k17_filter_2('#skF_1'),u2_lattices('#skF_1'),u1_lattices('#skF_1')) = k23_filter_2('#skF_1',k17_filter_2('#skF_1')) )
| v1_xboole_0(k17_filter_2('#skF_1'))
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_4,c_7194,c_2624,c_33052]) ).
tff(c_33079,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8,c_861,c_852,c_33077]) ).
tff(c_33081,plain,
g3_lattices(u1_struct_0('#skF_1'),u2_lattices('#skF_1'),u1_lattices('#skF_1')) = k23_filter_2('#skF_1',k17_filter_2('#skF_1')),
inference(splitRight,[status(thm)],[c_2]) ).
tff(c_33080,plain,
g3_lattices(u1_struct_0('#skF_1'),u2_lattices('#skF_1'),u1_lattices('#skF_1')) != k23_filter_2('#skF_1',k1_filter_2('#skF_1')),
inference(splitRight,[status(thm)],[c_2]) ).
tff(c_33129,plain,
k23_filter_2('#skF_1',k1_filter_2('#skF_1')) != k23_filter_2('#skF_1',k17_filter_2('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_33081,c_33080]) ).
tff(c_33678,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_33664,c_33129]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.08 % Problem : LAT332+1 : TPTP v9.0.0. Released v3.4.0.
% 0.02/0.08 % 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.08/0.26 % Computer : n032.cluster.edu
% 0.08/0.26 % Model : x86_64 x86_64
% 0.08/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.26 % Memory : 8042.1875MB
% 0.08/0.26 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.27 % CPULimit : 300
% 0.08/0.27 % WCLimit : 300
% 0.08/0.27 % DateTime : Tue Apr 8 04:28:00 EDT 2025
% 0.08/0.27 % CPUTime :
% 25.75/12.44 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 25.75/12.46
% 25.75/12.46 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------