%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : LAT301+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 : n015.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:46 PM UTC 2025
% Result : Theorem 12.75s 4.08s
% Output : CNFRefutation 13.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 13
% Syntax : Number of formulae : 67 ( 25 unt; 0 typ; 0 def)
% Number of atoms : 224 ( 14 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 251 ( 94 ~; 95 |; 40 &)
% ( 2 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 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 : 35 ( 33 usr; 1 prp; 0-3 aty)
% Number of functors : 39 ( 39 usr; 17 con; 0-3 aty)
% Number of variables : 46 ( 46 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ v1_partfun1 > v1_funct_2 > m2_relset_1 > m1_relset_1 > v2_binop_1 > v1_binop_1 > r2_hidden > 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 > v15_lattices > v14_lattices > v13_lattices > v10_lattices > l3_lattices > l2_lattices > l1_struct_0 > l1_lattices > g3_lattices > k7_filter_2 > k2_zfmisc_1 > k15_filter_2 > #nlpp > u2_lattices > u1_struct_0 > u1_lattices > k6_lattices > k5_lattices > k1_zfmisc_1 > k1_lattice2 > k1_xboole_0 > #skF_25 > #skF_7 > #skF_16 > #skF_18 > #skF_15 > #skF_8 > #skF_19 > #skF_13 > #skF_26 > #skF_14 > #skF_5 > #skF_10 > #skF_6 > #skF_2 > #skF_3 > #skF_1 > #skF_21 > #skF_4 > #skF_17 > #skF_11 > #skF_22 > #skF_24 > #skF_27 > #skF_23 > #skF_12 > #skF_9 > #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(k6_lattices,type,
k6_lattices: $i > $i ).
tff('#skF_25',type,
'#skF_25': $i > $i ).
tff('#skF_7',type,
'#skF_7': $i > $i ).
tff(m2_relset_1,type,
m2_relset_1: ( $i * $i * $i ) > $o ).
tff('#skF_16',type,
'#skF_16': $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(r2_hidden,type,
r2_hidden: ( $i * $i ) > $o ).
tff('#skF_15',type,
'#skF_15': $i ).
tff(v1_partfun1,type,
v1_partfun1: ( $i * $i * $i ) > $o ).
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_13',type,
'#skF_13': ( $i * $i ) > $i ).
tff(r1_tarski,type,
r1_tarski: ( $i * $i ) > $o ).
tff(m1_relset_1,type,
m1_relset_1: ( $i * $i * $i ) > $o ).
tff('#skF_26',type,
'#skF_26': $i ).
tff('#skF_14',type,
'#skF_14': $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('#skF_10',type,
'#skF_10': $i > $i ).
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_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('#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(l1_struct_0,type,
l1_struct_0: $i > $o ).
tff(k15_filter_2,type,
k15_filter_2: ( $i * $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('#skF_17',type,
'#skF_17': $i > $i ).
tff('#skF_11',type,
'#skF_11': $i > $i ).
tff('#skF_22',type,
'#skF_22': $i ).
tff(v8_lattices,type,
v8_lattices: $i > $o ).
tff('#skF_24',type,
'#skF_24': $i ).
tff('#skF_27',type,
'#skF_27': $i ).
tff('#skF_23',type,
'#skF_23': $i ).
tff(v3_lattices,type,
v3_lattices: $i > $o ).
tff(k5_lattices,type,
k5_lattices: $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('#skF_9',type,
'#skF_9': ( $i * $i ) > $i ).
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_44,negated_conjecture,
~ ! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( v13_lattices(A)
=> r2_hidden(k5_lattices(A),B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t25_filter_2) ).
tff(f_762,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A) )
=> ( v13_lattices(A)
<=> v14_lattices(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t63_lattice2) ).
tff(f_196,axiom,
! [A] :
( l3_lattices(A)
=> ( v3_lattices(k1_lattice2(A))
& l3_lattices(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_lattice2) ).
tff(f_530,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/sandbox/benchmark/theBenchmark.p',fc6_lattice2) ).
tff(f_685,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/sandbox/benchmark/theBenchmark.p',redefinition_k15_filter_2) ).
tff(f_281,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/sandbox/benchmark/theBenchmark.p',dt_m2_filter_2) ).
tff(f_293,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/sandbox/benchmark/theBenchmark.p',dt_m2_lattice4) ).
tff(f_163,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/sandbox/benchmark/theBenchmark.p',d6_filter_2) ).
tff(f_190,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/sandbox/benchmark/theBenchmark.p',dt_k15_filter_2) ).
tff(f_697,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/sandbox/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
tff(f_395,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& l3_lattices(A) )
=> ( ~ v3_struct_0(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_lattice2) ).
tff(f_777,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& v13_lattices(A)
& l3_lattices(A) )
=> ( k5_lattices(A) = k6_lattices(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t78_lattice2) ).
tff(f_724,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A) )
=> ! [B] :
( m1_filter_0(B,A)
=> ( ( ~ v3_struct_0(A)
& v10_lattices(A)
& v14_lattices(A)
& l3_lattices(A) )
=> r2_hidden(k6_lattices(A),B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_filter_0) ).
tff(c_12,plain,
~ v3_struct_0('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_44]) ).
tff(c_10,plain,
v10_lattices('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_44]) ).
tff(c_8,plain,
l3_lattices('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_44]) ).
tff(c_4,plain,
v13_lattices('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_44]) ).
tff(c_354,plain,
! [A_121] :
( v14_lattices(k1_lattice2(A_121))
| ~ v13_lattices(A_121)
| ~ l3_lattices(A_121)
| ~ v10_lattices(A_121)
| v3_struct_0(A_121) ),
inference(cnfTransformation,[status(thm)],[f_762]) ).
tff(c_66,plain,
! [A_23] :
( l3_lattices(k1_lattice2(A_23))
| ~ l3_lattices(A_23) ),
inference(cnfTransformation,[status(thm)],[f_196]) ).
tff(c_206,plain,
! [A_78] :
( v10_lattices(k1_lattice2(A_78))
| ~ l3_lattices(A_78)
| ~ v10_lattices(A_78)
| v3_struct_0(A_78) ),
inference(cnfTransformation,[status(thm)],[f_530]) ).
tff(c_6,plain,
m2_filter_2('#skF_2','#skF_1'),
inference(cnfTransformation,[status(thm)],[f_44]) ).
tff(c_1594,plain,
! [A_369,B_370] :
( ( k7_filter_2(A_369,B_370) = k15_filter_2(A_369,B_370) )
| ~ m2_filter_2(B_370,A_369)
| ~ l3_lattices(A_369)
| ~ v10_lattices(A_369)
| v3_struct_0(A_369) ),
inference(cnfTransformation,[status(thm)],[f_685]) ).
tff(c_1600,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_1594]) ).
tff(c_1604,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_10,c_8,c_1600]) ).
tff(c_1605,plain,
k7_filter_2('#skF_1','#skF_2') = k15_filter_2('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_12,c_1604]) ).
tff(c_104,plain,
! [B_39,A_37] :
( m2_lattice4(B_39,A_37)
| ~ m2_filter_2(B_39,A_37)
| ~ l3_lattices(A_37)
| ~ v10_lattices(A_37)
| v3_struct_0(A_37) ),
inference(cnfTransformation,[status(thm)],[f_281]) ).
tff(c_108,plain,
! [B_42,A_40] :
( m1_subset_1(B_42,k1_zfmisc_1(u1_struct_0(A_40)))
| ~ m2_lattice4(B_42,A_40)
| ~ l3_lattices(A_40)
| ~ v10_lattices(A_40)
| v3_struct_0(A_40) ),
inference(cnfTransformation,[status(thm)],[f_293]) ).
tff(c_1725,plain,
! [A_382,B_383] :
( ( k7_filter_2(A_382,B_383) = B_383 )
| ~ m1_subset_1(B_383,k1_zfmisc_1(u1_struct_0(A_382)))
| ~ l3_lattices(A_382)
| ~ v10_lattices(A_382)
| v3_struct_0(A_382) ),
inference(cnfTransformation,[status(thm)],[f_163]) ).
tff(c_1856,plain,
! [A_392,B_393] :
( ( k7_filter_2(A_392,B_393) = B_393 )
| ~ m2_lattice4(B_393,A_392)
| ~ l3_lattices(A_392)
| ~ v10_lattices(A_392)
| v3_struct_0(A_392) ),
inference(resolution,[status(thm)],[c_108,c_1725]) ).
tff(c_1892,plain,
! [A_397,B_398] :
( ( k7_filter_2(A_397,B_398) = B_398 )
| ~ m2_filter_2(B_398,A_397)
| ~ l3_lattices(A_397)
| ~ v10_lattices(A_397)
| v3_struct_0(A_397) ),
inference(resolution,[status(thm)],[c_104,c_1856]) ).
tff(c_1898,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_1892]) ).
tff(c_1902,plain,
( ( k15_filter_2('#skF_1','#skF_2') = '#skF_2' )
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_8,c_1605,c_1898]) ).
tff(c_1903,plain,
k15_filter_2('#skF_1','#skF_2') = '#skF_2',
inference(negUnitSimplification,[status(thm)],[c_12,c_1902]) ).
tff(c_64,plain,
! [A_21,B_22] :
( m1_filter_2(k15_filter_2(A_21,B_22),k1_lattice2(A_21))
| ~ m2_filter_2(B_22,A_21)
| ~ l3_lattices(A_21)
| ~ v10_lattices(A_21)
| v3_struct_0(A_21) ),
inference(cnfTransformation,[status(thm)],[f_190]) ).
tff(c_1908,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_1903,c_64]) ).
tff(c_1912,plain,
( m1_filter_2('#skF_2',k1_lattice2('#skF_1'))
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_8,c_6,c_1908]) ).
tff(c_1913,plain,
m1_filter_2('#skF_2',k1_lattice2('#skF_1')),
inference(negUnitSimplification,[status(thm)],[c_12,c_1912]) ).
tff(c_328,plain,
! [B_100,A_98] :
( m1_filter_0(B_100,A_98)
| ~ m1_filter_2(B_100,A_98)
| ~ l3_lattices(A_98)
| ~ v10_lattices(A_98)
| v3_struct_0(A_98) ),
inference(cnfTransformation,[status(thm)],[f_697]) ).
tff(c_1925,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_1913,c_328]) ).
tff(c_1967,plain,
~ v10_lattices(k1_lattice2('#skF_1')),
inference(splitLeft,[status(thm)],[c_1925]) ).
tff(c_1970,plain,
( ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_206,c_1967]) ).
tff(c_1973,plain,
v3_struct_0('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_8,c_1970]) ).
tff(c_1975,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12,c_1973]) ).
tff(c_1976,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_1925]) ).
tff(c_1984,plain,
~ l3_lattices(k1_lattice2('#skF_1')),
inference(splitLeft,[status(thm)],[c_1976]) ).
tff(c_2038,plain,
~ l3_lattices('#skF_1'),
inference(resolution,[status(thm)],[c_66,c_1984]) ).
tff(c_2042,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_2038]) ).
tff(c_2043,plain,
( m1_filter_0('#skF_2',k1_lattice2('#skF_1'))
| v3_struct_0(k1_lattice2('#skF_1')) ),
inference(splitRight,[status(thm)],[c_1976]) ).
tff(c_2064,plain,
v3_struct_0(k1_lattice2('#skF_1')),
inference(splitLeft,[status(thm)],[c_2043]) ).
tff(c_152,plain,
! [A_66] :
( ~ v3_struct_0(k1_lattice2(A_66))
| ~ l3_lattices(A_66)
| v3_struct_0(A_66) ),
inference(cnfTransformation,[status(thm)],[f_395]) ).
tff(c_2067,plain,
( ~ l3_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_2064,c_152]) ).
tff(c_2070,plain,
v3_struct_0('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_2067]) ).
tff(c_2072,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12,c_2070]) ).
tff(c_2074,plain,
~ v3_struct_0(k1_lattice2('#skF_1')),
inference(splitRight,[status(thm)],[c_2043]) ).
tff(c_1977,plain,
v10_lattices(k1_lattice2('#skF_1')),
inference(splitRight,[status(thm)],[c_1925]) ).
tff(c_2044,plain,
l3_lattices(k1_lattice2('#skF_1')),
inference(splitRight,[status(thm)],[c_1976]) ).
tff(c_2073,plain,
m1_filter_0('#skF_2',k1_lattice2('#skF_1')),
inference(splitRight,[status(thm)],[c_2043]) ).
tff(c_358,plain,
! [A_123] :
( ( k6_lattices(k1_lattice2(A_123)) = k5_lattices(A_123) )
| ~ l3_lattices(A_123)
| ~ v13_lattices(A_123)
| ~ v10_lattices(A_123)
| v3_struct_0(A_123) ),
inference(cnfTransformation,[status(thm)],[f_777]) ).
tff(c_1654,plain,
! [A_377,B_378] :
( r2_hidden(k6_lattices(A_377),B_378)
| ~ v14_lattices(A_377)
| ~ m1_filter_0(B_378,A_377)
| ~ l3_lattices(A_377)
| ~ v10_lattices(A_377)
| v3_struct_0(A_377) ),
inference(cnfTransformation,[status(thm)],[f_724]) ).
tff(c_6418,plain,
! [A_732,B_733] :
( r2_hidden(k5_lattices(A_732),B_733)
| ~ v14_lattices(k1_lattice2(A_732))
| ~ m1_filter_0(B_733,k1_lattice2(A_732))
| ~ l3_lattices(k1_lattice2(A_732))
| ~ v10_lattices(k1_lattice2(A_732))
| v3_struct_0(k1_lattice2(A_732))
| ~ l3_lattices(A_732)
| ~ v13_lattices(A_732)
| ~ v10_lattices(A_732)
| v3_struct_0(A_732) ),
inference(superposition,[status(thm),theory(equality)],[c_358,c_1654]) ).
tff(c_2,plain,
~ r2_hidden(k5_lattices('#skF_1'),'#skF_2'),
inference(cnfTransformation,[status(thm)],[f_44]) ).
tff(c_6500,plain,
( ~ v14_lattices(k1_lattice2('#skF_1'))
| ~ 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'))
| ~ l3_lattices('#skF_1')
| ~ v13_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_6418,c_2]) ).
tff(c_6527,plain,
( ~ v14_lattices(k1_lattice2('#skF_1'))
| v3_struct_0(k1_lattice2('#skF_1'))
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_4,c_8,c_1977,c_2044,c_2073,c_6500]) ).
tff(c_6528,plain,
~ v14_lattices(k1_lattice2('#skF_1')),
inference(negUnitSimplification,[status(thm)],[c_12,c_2074,c_6527]) ).
tff(c_6531,plain,
( ~ v13_lattices('#skF_1')
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_354,c_6528]) ).
tff(c_6534,plain,
v3_struct_0('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_8,c_4,c_6531]) ).
tff(c_6536,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12,c_6534]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : LAT301+1 : TPTP v9.0.0. Released v3.4.0.
% 0.11/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.12/0.34 % Computer : n015.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Tue Apr 8 04:10:35 EDT 2025
% 0.12/0.34 % CPUTime :
% 12.75/4.08 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.90/4.09
% 12.90/4.09 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------