%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : LAT327+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 : n003.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:54 PM UTC 2025
% Result : Theorem 6.39s 2.43s
% Output : CNFRefutation 6.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 5
% Syntax : Number of formulae : 74 ( 35 unt; 0 typ; 0 def)
% Number of atoms : 253 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 319 ( 140 ~; 139 |; 25 &)
% ( 2 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 21 ( 20 usr; 1 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 11 con; 0-3 aty)
% Number of variables : 48 ( 48 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ r3_lattices > r1_lattices > r2_hidden > r1_tarski > m2_lattice4 > m1_subset_1 > v9_lattices > v8_lattices > v7_lattices > v6_lattices > v5_lattices > v4_lattices > v3_struct_0 > v1_xboole_0 > v1_funct_1 > v10_lattices > l3_lattices > l2_lattices > l1_struct_0 > l1_lattices > k22_filter_2 > #nlpp > u1_struct_0 > k1_zfmisc_1 > k1_xboole_0 > #skF_5 > #skF_16 > #skF_4 > #skF_15 > #skF_7 > #skF_14 > #skF_10 > #skF_13 > #skF_2 > #skF_3 > #skF_1 > #skF_9 > #skF_8 > #skF_11 > #skF_6 > #skF_12
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(l3_lattices,type,
l3_lattices: $i > $o ).
tff('#skF_5',type,
'#skF_5': $i > $i ).
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('#skF_4',type,
'#skF_4': $i > $i ).
tff(r3_lattices,type,
r3_lattices: ( $i * $i * $i ) > $o ).
tff(r2_hidden,type,
r2_hidden: ( $i * $i ) > $o ).
tff('#skF_15',type,
'#skF_15': $i ).
tff(k1_xboole_0,type,
k1_xboole_0: $i ).
tff(m2_lattice4,type,
m2_lattice4: ( $i * $i ) > $o ).
tff(l1_lattices,type,
l1_lattices: $i > $o ).
tff('#skF_7',type,
'#skF_7': $i ).
tff(r1_lattices,type,
r1_lattices: ( $i * $i * $i ) > $o ).
tff(r1_tarski,type,
r1_tarski: ( $i * $i ) > $o ).
tff('#skF_14',type,
'#skF_14': $i ).
tff(v4_lattices,type,
v4_lattices: $i > $o ).
tff('#skF_10',type,
'#skF_10': $i > $i ).
tff(k22_filter_2,type,
k22_filter_2: ( $i * $i * $i ) > $i ).
tff('#skF_13',type,
'#skF_13': $i ).
tff(v6_lattices,type,
v6_lattices: $i > $o ).
tff('#skF_2',type,
'#skF_2': $i ).
tff(v9_lattices,type,
v9_lattices: $i > $o ).
tff('#skF_3',type,
'#skF_3': $i ).
tff('#skF_1',type,
'#skF_1': $i ).
tff(v5_lattices,type,
v5_lattices: $i > $o ).
tff(v10_lattices,type,
v10_lattices: $i > $o ).
tff('#skF_9',type,
'#skF_9': $i ).
tff(k1_zfmisc_1,type,
k1_zfmisc_1: $i > $i ).
tff(l1_struct_0,type,
l1_struct_0: $i > $o ).
tff('#skF_8',type,
'#skF_8': $i ).
tff('#skF_11',type,
'#skF_11': $i > $i ).
tff(v8_lattices,type,
v8_lattices: $i > $o ).
tff(u1_struct_0,type,
u1_struct_0: $i > $i ).
tff(v1_xboole_0,type,
v1_xboole_0: $i > $o ).
tff('#skF_6',type,
'#skF_6': $i > $i ).
tff('#skF_12',type,
'#skF_12': $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_49,negated_conjecture,
~ ! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( r3_lattices(A,B,C)
=> ( r2_hidden(B,k22_filter_2(A,B,C))
& r2_hidden(C,k22_filter_2(A,B,C)) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t64_filter_2) ).
tff(f_299,axiom,
! [A] :
( l3_lattices(A)
=> ( ( ~ v3_struct_0(A)
& v10_lattices(A) )
=> ( ~ v3_struct_0(A)
& v4_lattices(A)
& v5_lattices(A)
& v6_lattices(A)
& v7_lattices(A)
& v8_lattices(A)
& v9_lattices(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_lattices) ).
tff(f_231,axiom,
! [A,B,C] :
( ( ~ v3_struct_0(A)
& v6_lattices(A)
& v8_lattices(A)
& v9_lattices(A)
& l3_lattices(A)
& m1_subset_1(B,u1_struct_0(A))
& m1_subset_1(C,u1_struct_0(A)) )
=> r3_lattices(A,B,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_r3_lattices) ).
tff(f_255,axiom,
! [A,B,C] :
( ( ~ v3_struct_0(A)
& v6_lattices(A)
& v8_lattices(A)
& v9_lattices(A)
& l3_lattices(A)
& m1_subset_1(B,u1_struct_0(A))
& m1_subset_1(C,u1_struct_0(A)) )
=> ( r3_lattices(A,B,C)
<=> r1_lattices(A,B,C) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_r3_lattices) ).
tff(f_332,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ! [D] :
( m1_subset_1(D,u1_struct_0(A))
=> ( r3_lattices(A,B,C)
=> ( r2_hidden(D,k22_filter_2(A,B,C))
<=> ( r3_lattices(A,B,D)
& r3_lattices(A,D,C) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t63_filter_2) ).
tff(c_14,plain,
~ v3_struct_0('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_12,plain,
v10_lattices('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_10,plain,
l3_lattices('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_8,plain,
m1_subset_1('#skF_2',u1_struct_0('#skF_1')),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_6,plain,
m1_subset_1('#skF_3',u1_struct_0('#skF_1')),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_4,plain,
r3_lattices('#skF_1','#skF_2','#skF_3'),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_118,plain,
! [A_53] :
( v6_lattices(A_53)
| ~ v10_lattices(A_53)
| v3_struct_0(A_53)
| ~ l3_lattices(A_53) ),
inference(cnfTransformation,[status(thm)],[f_299]) ).
tff(c_1638,plain,
! [A_324,B_325,C_326] :
( r3_lattices(A_324,B_325,B_325)
| ~ m1_subset_1(C_326,u1_struct_0(A_324))
| ~ m1_subset_1(B_325,u1_struct_0(A_324))
| ~ l3_lattices(A_324)
| ~ v9_lattices(A_324)
| ~ v8_lattices(A_324)
| ~ v6_lattices(A_324)
| v3_struct_0(A_324) ),
inference(cnfTransformation,[status(thm)],[f_231]) ).
tff(c_1644,plain,
! [B_325] :
( r3_lattices('#skF_1',B_325,B_325)
| ~ m1_subset_1(B_325,u1_struct_0('#skF_1'))
| ~ l3_lattices('#skF_1')
| ~ v9_lattices('#skF_1')
| ~ v8_lattices('#skF_1')
| ~ v6_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_6,c_1638]) ).
tff(c_1652,plain,
! [B_325] :
( r3_lattices('#skF_1',B_325,B_325)
| ~ m1_subset_1(B_325,u1_struct_0('#skF_1'))
| ~ v9_lattices('#skF_1')
| ~ v8_lattices('#skF_1')
| ~ v6_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_1644]) ).
tff(c_1653,plain,
! [B_325] :
( r3_lattices('#skF_1',B_325,B_325)
| ~ m1_subset_1(B_325,u1_struct_0('#skF_1'))
| ~ v9_lattices('#skF_1')
| ~ v8_lattices('#skF_1')
| ~ v6_lattices('#skF_1') ),
inference(negUnitSimplification,[status(thm)],[c_14,c_1652]) ).
tff(c_1790,plain,
~ v6_lattices('#skF_1'),
inference(splitLeft,[status(thm)],[c_1653]) ).
tff(c_1793,plain,
( ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1')
| ~ l3_lattices('#skF_1') ),
inference(resolution,[status(thm)],[c_118,c_1790]) ).
tff(c_1796,plain,
v3_struct_0('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_12,c_1793]) ).
tff(c_1798,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_1796]) ).
tff(c_1800,plain,
v6_lattices('#skF_1'),
inference(splitRight,[status(thm)],[c_1653]) ).
tff(c_114,plain,
! [A_53] :
( v8_lattices(A_53)
| ~ v10_lattices(A_53)
| v3_struct_0(A_53)
| ~ l3_lattices(A_53) ),
inference(cnfTransformation,[status(thm)],[f_299]) ).
tff(c_112,plain,
! [A_53] :
( v9_lattices(A_53)
| ~ v10_lattices(A_53)
| v3_struct_0(A_53)
| ~ l3_lattices(A_53) ),
inference(cnfTransformation,[status(thm)],[f_299]) ).
tff(c_1799,plain,
! [B_325] :
( ~ v8_lattices('#skF_1')
| ~ v9_lattices('#skF_1')
| r3_lattices('#skF_1',B_325,B_325)
| ~ m1_subset_1(B_325,u1_struct_0('#skF_1')) ),
inference(splitRight,[status(thm)],[c_1653]) ).
tff(c_1801,plain,
~ v9_lattices('#skF_1'),
inference(splitLeft,[status(thm)],[c_1799]) ).
tff(c_1804,plain,
( ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1')
| ~ l3_lattices('#skF_1') ),
inference(resolution,[status(thm)],[c_112,c_1801]) ).
tff(c_1807,plain,
v3_struct_0('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_12,c_1804]) ).
tff(c_1809,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_1807]) ).
tff(c_1811,plain,
v9_lattices('#skF_1'),
inference(splitRight,[status(thm)],[c_1799]) ).
tff(c_1819,plain,
! [A_339,B_340,C_341] :
( r1_lattices(A_339,B_340,C_341)
| ~ r3_lattices(A_339,B_340,C_341)
| ~ m1_subset_1(C_341,u1_struct_0(A_339))
| ~ m1_subset_1(B_340,u1_struct_0(A_339))
| ~ l3_lattices(A_339)
| ~ v9_lattices(A_339)
| ~ v8_lattices(A_339)
| ~ v6_lattices(A_339)
| v3_struct_0(A_339) ),
inference(cnfTransformation,[status(thm)],[f_255]) ).
tff(c_1821,plain,
( r1_lattices('#skF_1','#skF_2','#skF_3')
| ~ m1_subset_1('#skF_3',u1_struct_0('#skF_1'))
| ~ m1_subset_1('#skF_2',u1_struct_0('#skF_1'))
| ~ l3_lattices('#skF_1')
| ~ v9_lattices('#skF_1')
| ~ v8_lattices('#skF_1')
| ~ v6_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_4,c_1819]) ).
tff(c_1824,plain,
( r1_lattices('#skF_1','#skF_2','#skF_3')
| ~ v8_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_1800,c_1811,c_10,c_8,c_6,c_1821]) ).
tff(c_1825,plain,
( r1_lattices('#skF_1','#skF_2','#skF_3')
| ~ v8_lattices('#skF_1') ),
inference(negUnitSimplification,[status(thm)],[c_14,c_1824]) ).
tff(c_1826,plain,
~ v8_lattices('#skF_1'),
inference(splitLeft,[status(thm)],[c_1825]) ).
tff(c_1829,plain,
( ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1')
| ~ l3_lattices('#skF_1') ),
inference(resolution,[status(thm)],[c_114,c_1826]) ).
tff(c_1832,plain,
v3_struct_0('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_12,c_1829]) ).
tff(c_1834,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_1832]) ).
tff(c_1836,plain,
v8_lattices('#skF_1'),
inference(splitRight,[status(thm)],[c_1825]) ).
tff(c_1642,plain,
! [B_325] :
( r3_lattices('#skF_1',B_325,B_325)
| ~ m1_subset_1(B_325,u1_struct_0('#skF_1'))
| ~ l3_lattices('#skF_1')
| ~ v9_lattices('#skF_1')
| ~ v8_lattices('#skF_1')
| ~ v6_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_8,c_1638]) ).
tff(c_1648,plain,
! [B_325] :
( r3_lattices('#skF_1',B_325,B_325)
| ~ m1_subset_1(B_325,u1_struct_0('#skF_1'))
| ~ v9_lattices('#skF_1')
| ~ v8_lattices('#skF_1')
| ~ v6_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_1642]) ).
tff(c_1649,plain,
! [B_325] :
( r3_lattices('#skF_1',B_325,B_325)
| ~ m1_subset_1(B_325,u1_struct_0('#skF_1'))
| ~ v9_lattices('#skF_1')
| ~ v8_lattices('#skF_1')
| ~ v6_lattices('#skF_1') ),
inference(negUnitSimplification,[status(thm)],[c_14,c_1648]) ).
tff(c_1839,plain,
! [B_342] :
( r3_lattices('#skF_1',B_342,B_342)
| ~ m1_subset_1(B_342,u1_struct_0('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_1800,c_1836,c_1811,c_1649]) ).
tff(c_1857,plain,
r3_lattices('#skF_1','#skF_3','#skF_3'),
inference(resolution,[status(thm)],[c_6,c_1839]) ).
tff(c_2031,plain,
! [D_363,A_364,B_365,C_366] :
( r2_hidden(D_363,k22_filter_2(A_364,B_365,C_366))
| ~ r3_lattices(A_364,D_363,C_366)
| ~ r3_lattices(A_364,B_365,D_363)
| ~ r3_lattices(A_364,B_365,C_366)
| ~ m1_subset_1(D_363,u1_struct_0(A_364))
| ~ m1_subset_1(C_366,u1_struct_0(A_364))
| ~ m1_subset_1(B_365,u1_struct_0(A_364))
| ~ l3_lattices(A_364)
| ~ v10_lattices(A_364)
| v3_struct_0(A_364) ),
inference(cnfTransformation,[status(thm)],[f_332]) ).
tff(c_662,plain,
! [A_177,B_178,C_179] :
( r3_lattices(A_177,B_178,B_178)
| ~ m1_subset_1(C_179,u1_struct_0(A_177))
| ~ m1_subset_1(B_178,u1_struct_0(A_177))
| ~ l3_lattices(A_177)
| ~ v9_lattices(A_177)
| ~ v8_lattices(A_177)
| ~ v6_lattices(A_177)
| v3_struct_0(A_177) ),
inference(cnfTransformation,[status(thm)],[f_231]) ).
tff(c_666,plain,
! [B_178] :
( r3_lattices('#skF_1',B_178,B_178)
| ~ m1_subset_1(B_178,u1_struct_0('#skF_1'))
| ~ l3_lattices('#skF_1')
| ~ v9_lattices('#skF_1')
| ~ v8_lattices('#skF_1')
| ~ v6_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_8,c_662]) ).
tff(c_672,plain,
! [B_178] :
( r3_lattices('#skF_1',B_178,B_178)
| ~ m1_subset_1(B_178,u1_struct_0('#skF_1'))
| ~ v9_lattices('#skF_1')
| ~ v8_lattices('#skF_1')
| ~ v6_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_666]) ).
tff(c_673,plain,
! [B_178] :
( r3_lattices('#skF_1',B_178,B_178)
| ~ m1_subset_1(B_178,u1_struct_0('#skF_1'))
| ~ v9_lattices('#skF_1')
| ~ v8_lattices('#skF_1')
| ~ v6_lattices('#skF_1') ),
inference(negUnitSimplification,[status(thm)],[c_14,c_672]) ).
tff(c_722,plain,
~ v6_lattices('#skF_1'),
inference(splitLeft,[status(thm)],[c_673]) ).
tff(c_725,plain,
( ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1')
| ~ l3_lattices('#skF_1') ),
inference(resolution,[status(thm)],[c_118,c_722]) ).
tff(c_728,plain,
v3_struct_0('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_12,c_725]) ).
tff(c_730,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_728]) ).
tff(c_731,plain,
! [B_178] :
( ~ v8_lattices('#skF_1')
| ~ v9_lattices('#skF_1')
| r3_lattices('#skF_1',B_178,B_178)
| ~ m1_subset_1(B_178,u1_struct_0('#skF_1')) ),
inference(splitRight,[status(thm)],[c_673]) ).
tff(c_740,plain,
~ v9_lattices('#skF_1'),
inference(splitLeft,[status(thm)],[c_731]) ).
tff(c_743,plain,
( ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1')
| ~ l3_lattices('#skF_1') ),
inference(resolution,[status(thm)],[c_112,c_740]) ).
tff(c_746,plain,
v3_struct_0('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_12,c_743]) ).
tff(c_748,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_746]) ).
tff(c_749,plain,
! [B_178] :
( ~ v8_lattices('#skF_1')
| r3_lattices('#skF_1',B_178,B_178)
| ~ m1_subset_1(B_178,u1_struct_0('#skF_1')) ),
inference(splitRight,[status(thm)],[c_731]) ).
tff(c_779,plain,
~ v8_lattices('#skF_1'),
inference(splitLeft,[status(thm)],[c_749]) ).
tff(c_782,plain,
( ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1')
| ~ l3_lattices('#skF_1') ),
inference(resolution,[status(thm)],[c_114,c_779]) ).
tff(c_785,plain,
v3_struct_0('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_12,c_782]) ).
tff(c_787,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_785]) ).
tff(c_798,plain,
! [B_189] :
( r3_lattices('#skF_1',B_189,B_189)
| ~ m1_subset_1(B_189,u1_struct_0('#skF_1')) ),
inference(splitRight,[status(thm)],[c_749]) ).
tff(c_811,plain,
r3_lattices('#skF_1','#skF_2','#skF_2'),
inference(resolution,[status(thm)],[c_8,c_798]) ).
tff(c_1026,plain,
! [D_216,A_217,B_218,C_219] :
( r2_hidden(D_216,k22_filter_2(A_217,B_218,C_219))
| ~ r3_lattices(A_217,D_216,C_219)
| ~ r3_lattices(A_217,B_218,D_216)
| ~ r3_lattices(A_217,B_218,C_219)
| ~ m1_subset_1(D_216,u1_struct_0(A_217))
| ~ m1_subset_1(C_219,u1_struct_0(A_217))
| ~ m1_subset_1(B_218,u1_struct_0(A_217))
| ~ l3_lattices(A_217)
| ~ v10_lattices(A_217)
| v3_struct_0(A_217) ),
inference(cnfTransformation,[status(thm)],[f_332]) ).
tff(c_2,plain,
( ~ r2_hidden('#skF_3',k22_filter_2('#skF_1','#skF_2','#skF_3'))
| ~ r2_hidden('#skF_2',k22_filter_2('#skF_1','#skF_2','#skF_3')) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_139,plain,
~ r2_hidden('#skF_2',k22_filter_2('#skF_1','#skF_2','#skF_3')),
inference(splitLeft,[status(thm)],[c_2]) ).
tff(c_1050,plain,
( ~ r3_lattices('#skF_1','#skF_2','#skF_2')
| ~ r3_lattices('#skF_1','#skF_2','#skF_3')
| ~ m1_subset_1('#skF_3',u1_struct_0('#skF_1'))
| ~ m1_subset_1('#skF_2',u1_struct_0('#skF_1'))
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_1026,c_139]) ).
tff(c_1061,plain,
v3_struct_0('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_10,c_8,c_6,c_4,c_811,c_1050]) ).
tff(c_1063,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_1061]) ).
tff(c_1064,plain,
~ r2_hidden('#skF_3',k22_filter_2('#skF_1','#skF_2','#skF_3')),
inference(splitRight,[status(thm)],[c_2]) ).
tff(c_2055,plain,
( ~ r3_lattices('#skF_1','#skF_3','#skF_3')
| ~ r3_lattices('#skF_1','#skF_2','#skF_3')
| ~ m1_subset_1('#skF_3',u1_struct_0('#skF_1'))
| ~ m1_subset_1('#skF_2',u1_struct_0('#skF_1'))
| ~ l3_lattices('#skF_1')
| ~ v10_lattices('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_2031,c_1064]) ).
tff(c_2066,plain,
v3_struct_0('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_10,c_8,c_6,c_4,c_1857,c_2055]) ).
tff(c_2068,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_2066]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : LAT327+1 : TPTP v9.0.0. Released v3.4.0.
% 0.03/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 : n003.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:25:03 EDT 2025
% 0.12/0.34 % CPUTime :
% 6.39/2.43 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.56/2.44
% 6.56/2.44 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------