%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : TOP024+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 : n016.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 10:52:24 PM UTC 2025
% Result : Theorem 21.14s 8.84s
% Output : CNFRefutation 21.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 12
% Syntax : Number of formulae : 73 ( 25 unt; 0 typ; 0 def)
% Number of atoms : 185 ( 39 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 199 ( 87 ~; 79 |; 12 &)
% ( 3 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 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 : 27 ( 25 usr; 1 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 7 con; 0-2 aty)
% Number of variables : 56 ( 56 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ v4_pre_topc > v3_tops_1 > v3_pre_topc > v2_tops_1 > v1_tsp_2 > v1_tsp_1 > v1_tops_1 > r2_hidden > r1_tarski > m1_subset_1 > v5_membered > v4_ordinal2 > v4_membered > v3_struct_0 > v3_membered > v2_pre_topc > v2_membered > v1_xreal_0 > v1_xcmplx_0 > v1_xboole_0 > v1_rat_1 > v1_membered > v1_int_1 > l1_struct_0 > l1_pre_topc > k6_pre_topc > k3_tex_4 > #nlpp > u1_struct_0 > k2_pre_topc > k1_zfmisc_1 > k1_xboole_0 > #skF_9 > #skF_7 > #skF_5 > #skF_16 > #skF_11 > #skF_8 > #skF_15 > #skF_10 > #skF_6 > #skF_2 > #skF_3 > #skF_1 > #skF_13 > #skF_4 > #skF_17 > #skF_14 > #skF_12
%Foreground sorts:
%Background operators:
%Foreground operators:
tff('#skF_9',type,
'#skF_9': $i > $i ).
tff('#skF_7',type,
'#skF_7': $i > $i ).
tff('#skF_5',type,
'#skF_5': $i > $i ).
tff('#skF_16',type,
'#skF_16': $i > $i ).
tff(v3_pre_topc,type,
v3_pre_topc: ( $i * $i ) > $o ).
tff(r2_hidden,type,
r2_hidden: ( $i * $i ) > $o ).
tff('#skF_11',type,
'#skF_11': $i ).
tff(v1_int_1,type,
v1_int_1: $i > $o ).
tff(k1_xboole_0,type,
k1_xboole_0: $i ).
tff(v2_tops_1,type,
v2_tops_1: ( $i * $i ) > $o ).
tff(l1_pre_topc,type,
l1_pre_topc: $i > $o ).
tff('#skF_8',type,
'#skF_8': $i > $i ).
tff(v3_tops_1,type,
v3_tops_1: ( $i * $i ) > $o ).
tff(r1_tarski,type,
r1_tarski: ( $i * $i ) > $o ).
tff(v4_ordinal2,type,
v4_ordinal2: $i > $o ).
tff('#skF_15',type,
'#skF_15': $i > $i ).
tff(k3_tex_4,type,
k3_tex_4: ( $i * $i ) > $i ).
tff(v1_tops_1,type,
v1_tops_1: ( $i * $i ) > $o ).
tff('#skF_10',type,
'#skF_10': $i > $i ).
tff('#skF_6',type,
'#skF_6': $i ).
tff('#skF_2',type,
'#skF_2': $i ).
tff(v3_membered,type,
v3_membered: $i > $o ).
tff('#skF_3',type,
'#skF_3': $i ).
tff('#skF_1',type,
'#skF_1': $i ).
tff(v1_tsp_1,type,
v1_tsp_1: ( $i * $i ) > $o ).
tff(v1_tsp_2,type,
v1_tsp_2: ( $i * $i ) > $o ).
tff(v1_xreal_0,type,
v1_xreal_0: $i > $o ).
tff(v5_membered,type,
v5_membered: $i > $o ).
tff(k1_zfmisc_1,type,
k1_zfmisc_1: $i > $i ).
tff(l1_struct_0,type,
l1_struct_0: $i > $o ).
tff(v2_membered,type,
v2_membered: $i > $o ).
tff(v4_pre_topc,type,
v4_pre_topc: ( $i * $i ) > $o ).
tff(v1_membered,type,
v1_membered: $i > $o ).
tff(v1_xcmplx_0,type,
v1_xcmplx_0: $i > $o ).
tff('#skF_13',type,
'#skF_13': $i > $i ).
tff('#skF_4',type,
'#skF_4': $i ).
tff('#skF_17',type,
'#skF_17': $i > $i ).
tff('#skF_14',type,
'#skF_14': $i > $i ).
tff(v2_pre_topc,type,
v2_pre_topc: $i > $o ).
tff(v1_rat_1,type,
v1_rat_1: $i > $o ).
tff(k2_pre_topc,type,
k2_pre_topc: $i > $i ).
tff('#skF_12',type,
'#skF_12': $i > $i ).
tff(v4_membered,type,
v4_membered: $i > $o ).
tff(u1_struct_0,type,
u1_struct_0: $i > $i ).
tff(v1_xboole_0,type,
v1_xboole_0: $i > $o ).
tff(k6_pre_topc,type,
k6_pre_topc: ( $i * $i ) > $i ).
tff(v3_struct_0,type,
v3_struct_0: $i > $o ).
tff(m1_subset_1,type,
m1_subset_1: ( $i * $i ) > $o ).
tff(f_44,negated_conjecture,
~ ! [A] :
( ( ~ v3_struct_0(A)
& v2_pre_topc(A)
& l1_pre_topc(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( v1_tsp_2(B,A)
=> v1_tops_1(B,A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_tsp_2) ).
tff(f_385,axiom,
! [A] :
( ( v2_pre_topc(A)
& l1_pre_topc(A) )
=> ( v3_pre_topc(k2_pre_topc(A),A)
& v4_pre_topc(k2_pre_topc(A),A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc8_tops_1) ).
tff(f_326,axiom,
! [A] :
( l1_pre_topc(A)
=> l1_struct_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
tff(f_545,axiom,
! [A] :
( l1_struct_0(A)
=> ( k2_pre_topc(A) = u1_struct_0(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_pre_topc) ).
tff(f_302,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v2_pre_topc(A)
& l1_pre_topc(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( v1_tsp_2(B,A)
<=> ( v1_tsp_1(B,A)
& ( k3_tex_4(A,B) = u1_struct_0(A) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_tsp_2) ).
tff(f_599,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v2_pre_topc(A)
& l1_pre_topc(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( k6_pre_topc(A,k3_tex_4(A,B)) = k6_pre_topc(A,B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t64_tex_4) ).
tff(f_341,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& l1_struct_0(A) )
=> ~ v1_xboole_0(u1_struct_0(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_struct_0) ).
tff(f_307,axiom,
! [A] :
( l1_struct_0(A)
=> m1_subset_1(k2_pre_topc(A),k1_zfmisc_1(u1_struct_0(A))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_pre_topc) ).
tff(f_580,axiom,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( ( v4_pre_topc(B,A)
=> ( k6_pre_topc(A,B) = B ) )
& ( ( v2_pre_topc(A)
& ( k6_pre_topc(A,B) = B ) )
=> v4_pre_topc(B,A) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t52_pre_topc) ).
tff(f_541,axiom,
! [A,B] : r1_tarski(A,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
tff(f_559,axiom,
! [A,B] :
( m1_subset_1(A,k1_zfmisc_1(B))
<=> r1_tarski(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_subset) ).
tff(f_286,axiom,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( v1_tops_1(B,A)
<=> ( k6_pre_topc(A,B) = u1_struct_0(A) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_tops_3) ).
tff(c_2,plain,
~ v1_tops_1('#skF_2','#skF_1'),
inference(cnfTransformation,[status(thm)],[f_44]) ).
tff(c_10,plain,
v2_pre_topc('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_44]) ).
tff(c_8,plain,
l1_pre_topc('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_44]) ).
tff(c_184,plain,
! [A_77] :
( v4_pre_topc(k2_pre_topc(A_77),A_77)
| ~ l1_pre_topc(A_77)
| ~ v2_pre_topc(A_77) ),
inference(cnfTransformation,[status(thm)],[f_385]) ).
tff(c_4,plain,
v1_tsp_2('#skF_2','#skF_1'),
inference(cnfTransformation,[status(thm)],[f_44]) ).
tff(c_148,plain,
! [A_68] :
( l1_struct_0(A_68)
| ~ l1_pre_topc(A_68) ),
inference(cnfTransformation,[status(thm)],[f_326]) ).
tff(c_526,plain,
! [A_159] :
( ( u1_struct_0(A_159) = k2_pre_topc(A_159) )
| ~ l1_struct_0(A_159) ),
inference(cnfTransformation,[status(thm)],[f_545]) ).
tff(c_558,plain,
! [A_161] :
( ( u1_struct_0(A_161) = k2_pre_topc(A_161) )
| ~ l1_pre_topc(A_161) ),
inference(resolution,[status(thm)],[c_148,c_526]) ).
tff(c_566,plain,
u1_struct_0('#skF_1') = k2_pre_topc('#skF_1'),
inference(resolution,[status(thm)],[c_8,c_558]) ).
tff(c_6,plain,
m1_subset_1('#skF_2',k1_zfmisc_1(u1_struct_0('#skF_1'))),
inference(cnfTransformation,[status(thm)],[f_44]) ).
tff(c_584,plain,
m1_subset_1('#skF_2',k1_zfmisc_1(k2_pre_topc('#skF_1'))),
inference(demodulation,[status(thm),theory(equality)],[c_566,c_6]) ).
tff(c_12,plain,
~ v3_struct_0('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_44]) ).
tff(c_10624,plain,
! [A_527,B_528] :
( ( k3_tex_4(A_527,B_528) = u1_struct_0(A_527) )
| ~ v1_tsp_2(B_528,A_527)
| ~ m1_subset_1(B_528,k1_zfmisc_1(u1_struct_0(A_527)))
| ~ l1_pre_topc(A_527)
| ~ v2_pre_topc(A_527)
| v3_struct_0(A_527) ),
inference(cnfTransformation,[status(thm)],[f_302]) ).
tff(c_10668,plain,
! [B_528] :
( ( k3_tex_4('#skF_1',B_528) = u1_struct_0('#skF_1') )
| ~ v1_tsp_2(B_528,'#skF_1')
| ~ m1_subset_1(B_528,k1_zfmisc_1(k2_pre_topc('#skF_1')))
| ~ l1_pre_topc('#skF_1')
| ~ v2_pre_topc('#skF_1')
| v3_struct_0('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_566,c_10624]) ).
tff(c_10700,plain,
! [B_528] :
( ( k3_tex_4('#skF_1',B_528) = k2_pre_topc('#skF_1') )
| ~ v1_tsp_2(B_528,'#skF_1')
| ~ m1_subset_1(B_528,k1_zfmisc_1(k2_pre_topc('#skF_1')))
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_8,c_566,c_10668]) ).
tff(c_10752,plain,
! [B_532] :
( ( k3_tex_4('#skF_1',B_532) = k2_pre_topc('#skF_1') )
| ~ v1_tsp_2(B_532,'#skF_1')
| ~ m1_subset_1(B_532,k1_zfmisc_1(k2_pre_topc('#skF_1'))) ),
inference(negUnitSimplification,[status(thm)],[c_12,c_10700]) ).
tff(c_10787,plain,
( ( k3_tex_4('#skF_1','#skF_2') = k2_pre_topc('#skF_1') )
| ~ v1_tsp_2('#skF_2','#skF_1') ),
inference(resolution,[status(thm)],[c_584,c_10752]) ).
tff(c_10810,plain,
k3_tex_4('#skF_1','#skF_2') = k2_pre_topc('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_10787]) ).
tff(c_10909,plain,
! [A_537,B_538] :
( ( k6_pre_topc(A_537,k3_tex_4(A_537,B_538)) = k6_pre_topc(A_537,B_538) )
| ~ m1_subset_1(B_538,k1_zfmisc_1(u1_struct_0(A_537)))
| ~ l1_pre_topc(A_537)
| ~ v2_pre_topc(A_537)
| v3_struct_0(A_537) ),
inference(cnfTransformation,[status(thm)],[f_599]) ).
tff(c_10939,plain,
! [B_538] :
( ( k6_pre_topc('#skF_1',k3_tex_4('#skF_1',B_538)) = k6_pre_topc('#skF_1',B_538) )
| ~ m1_subset_1(B_538,k1_zfmisc_1(k2_pre_topc('#skF_1')))
| ~ l1_pre_topc('#skF_1')
| ~ v2_pre_topc('#skF_1')
| v3_struct_0('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_566,c_10909]) ).
tff(c_10966,plain,
! [B_538] :
( ( k6_pre_topc('#skF_1',k3_tex_4('#skF_1',B_538)) = k6_pre_topc('#skF_1',B_538) )
| ~ m1_subset_1(B_538,k1_zfmisc_1(k2_pre_topc('#skF_1')))
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_8,c_10939]) ).
tff(c_11037,plain,
! [B_542] :
( ( k6_pre_topc('#skF_1',k3_tex_4('#skF_1',B_542)) = k6_pre_topc('#skF_1',B_542) )
| ~ m1_subset_1(B_542,k1_zfmisc_1(k2_pre_topc('#skF_1'))) ),
inference(negUnitSimplification,[status(thm)],[c_12,c_10966]) ).
tff(c_11072,plain,
k6_pre_topc('#skF_1',k3_tex_4('#skF_1','#skF_2')) = k6_pre_topc('#skF_1','#skF_2'),
inference(resolution,[status(thm)],[c_584,c_11037]) ).
tff(c_11094,plain,
k6_pre_topc('#skF_1',k2_pre_topc('#skF_1')) = k6_pre_topc('#skF_1','#skF_2'),
inference(demodulation,[status(thm),theory(equality)],[c_10810,c_11072]) ).
tff(c_970,plain,
! [A_222] :
( ~ v1_xboole_0(u1_struct_0(A_222))
| ~ l1_struct_0(A_222)
| v3_struct_0(A_222) ),
inference(cnfTransformation,[status(thm)],[f_341]) ).
tff(c_973,plain,
( ~ v1_xboole_0(k2_pre_topc('#skF_1'))
| ~ l1_struct_0('#skF_1')
| v3_struct_0('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_566,c_970]) ).
tff(c_983,plain,
( ~ v1_xboole_0(k2_pre_topc('#skF_1'))
| ~ l1_struct_0('#skF_1') ),
inference(negUnitSimplification,[status(thm)],[c_12,c_973]) ).
tff(c_991,plain,
~ l1_struct_0('#skF_1'),
inference(splitLeft,[status(thm)],[c_983]) ).
tff(c_994,plain,
~ l1_pre_topc('#skF_1'),
inference(resolution,[status(thm)],[c_148,c_991]) ).
tff(c_998,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_994]) ).
tff(c_1000,plain,
l1_struct_0('#skF_1'),
inference(splitRight,[status(thm)],[c_983]) ).
tff(c_2298,plain,
! [A_336] :
( m1_subset_1(k2_pre_topc(A_336),k1_zfmisc_1(u1_struct_0(A_336)))
| ~ l1_struct_0(A_336) ),
inference(cnfTransformation,[status(thm)],[f_307]) ).
tff(c_2391,plain,
( m1_subset_1(k2_pre_topc('#skF_1'),k1_zfmisc_1(k2_pre_topc('#skF_1')))
| ~ l1_struct_0('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_566,c_2298]) ).
tff(c_2432,plain,
m1_subset_1(k2_pre_topc('#skF_1'),k1_zfmisc_1(k2_pre_topc('#skF_1'))),
inference(demodulation,[status(thm),theory(equality)],[c_1000,c_2391]) ).
tff(c_8316,plain,
! [B_451,A_452] :
( v4_pre_topc(B_451,A_452)
| ( k6_pre_topc(A_452,B_451) != B_451 )
| ~ v2_pre_topc(A_452)
| ~ m1_subset_1(B_451,k1_zfmisc_1(u1_struct_0(A_452)))
| ~ l1_pre_topc(A_452) ),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_8360,plain,
! [B_451] :
( v4_pre_topc(B_451,'#skF_1')
| ( k6_pre_topc('#skF_1',B_451) != B_451 )
| ~ v2_pre_topc('#skF_1')
| ~ m1_subset_1(B_451,k1_zfmisc_1(k2_pre_topc('#skF_1')))
| ~ l1_pre_topc('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_566,c_8316]) ).
tff(c_16924,plain,
! [B_725] :
( v4_pre_topc(B_725,'#skF_1')
| ( k6_pre_topc('#skF_1',B_725) != B_725 )
| ~ m1_subset_1(B_725,k1_zfmisc_1(k2_pre_topc('#skF_1'))) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_10,c_8360]) ).
tff(c_16955,plain,
( v4_pre_topc(k2_pre_topc('#skF_1'),'#skF_1')
| ( k6_pre_topc('#skF_1',k2_pre_topc('#skF_1')) != k2_pre_topc('#skF_1') ) ),
inference(resolution,[status(thm)],[c_2432,c_16924]) ).
tff(c_16986,plain,
( v4_pre_topc(k2_pre_topc('#skF_1'),'#skF_1')
| ( k6_pre_topc('#skF_1','#skF_2') != k2_pre_topc('#skF_1') ) ),
inference(demodulation,[status(thm),theory(equality)],[c_11094,c_16955]) ).
tff(c_16997,plain,
k6_pre_topc('#skF_1','#skF_2') != k2_pre_topc('#skF_1'),
inference(splitLeft,[status(thm)],[c_16986]) ).
tff(c_284,plain,
! [A_99] : r1_tarski(A_99,A_99),
inference(cnfTransformation,[status(thm)],[f_541]) ).
tff(c_294,plain,
! [A_106,B_107] :
( m1_subset_1(A_106,k1_zfmisc_1(B_107))
| ~ r1_tarski(A_106,B_107) ),
inference(cnfTransformation,[status(thm)],[f_559]) ).
tff(c_6145,plain,
! [A_399,B_400] :
( ( k6_pre_topc(A_399,B_400) = B_400 )
| ~ v4_pre_topc(B_400,A_399)
| ~ m1_subset_1(B_400,k1_zfmisc_1(u1_struct_0(A_399)))
| ~ l1_pre_topc(A_399) ),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_19265,plain,
! [A_799,A_800] :
( ( k6_pre_topc(A_799,A_800) = A_800 )
| ~ v4_pre_topc(A_800,A_799)
| ~ l1_pre_topc(A_799)
| ~ r1_tarski(A_800,u1_struct_0(A_799)) ),
inference(resolution,[status(thm)],[c_294,c_6145]) ).
tff(c_19311,plain,
! [A_800] :
( ( k6_pre_topc('#skF_1',A_800) = A_800 )
| ~ v4_pre_topc(A_800,'#skF_1')
| ~ l1_pre_topc('#skF_1')
| ~ r1_tarski(A_800,k2_pre_topc('#skF_1')) ),
inference(superposition,[status(thm),theory(equality)],[c_566,c_19265]) ).
tff(c_19343,plain,
! [A_801] :
( ( k6_pre_topc('#skF_1',A_801) = A_801 )
| ~ v4_pre_topc(A_801,'#skF_1')
| ~ r1_tarski(A_801,k2_pre_topc('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_19311]) ).
tff(c_19393,plain,
( ( k6_pre_topc('#skF_1',k2_pre_topc('#skF_1')) = k2_pre_topc('#skF_1') )
| ~ v4_pre_topc(k2_pre_topc('#skF_1'),'#skF_1') ),
inference(resolution,[status(thm)],[c_284,c_19343]) ).
tff(c_19429,plain,
( ( k6_pre_topc('#skF_1','#skF_2') = k2_pre_topc('#skF_1') )
| ~ v4_pre_topc(k2_pre_topc('#skF_1'),'#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_11094,c_19393]) ).
tff(c_19430,plain,
~ v4_pre_topc(k2_pre_topc('#skF_1'),'#skF_1'),
inference(negUnitSimplification,[status(thm)],[c_16997,c_19429]) ).
tff(c_19433,plain,
( ~ l1_pre_topc('#skF_1')
| ~ v2_pre_topc('#skF_1') ),
inference(resolution,[status(thm)],[c_184,c_19430]) ).
tff(c_19437,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10,c_8,c_19433]) ).
tff(c_19439,plain,
k6_pre_topc('#skF_1','#skF_2') = k2_pre_topc('#skF_1'),
inference(splitRight,[status(thm)],[c_16986]) ).
tff(c_669,plain,
! [A_180,B_181] :
( r1_tarski(A_180,B_181)
| ~ m1_subset_1(A_180,k1_zfmisc_1(B_181)) ),
inference(cnfTransformation,[status(thm)],[f_559]) ).
tff(c_680,plain,
r1_tarski('#skF_2',k2_pre_topc('#skF_1')),
inference(resolution,[status(thm)],[c_584,c_669]) ).
tff(c_7215,plain,
! [B_426,A_427] :
( v1_tops_1(B_426,A_427)
| ( k6_pre_topc(A_427,B_426) != u1_struct_0(A_427) )
| ~ m1_subset_1(B_426,k1_zfmisc_1(u1_struct_0(A_427)))
| ~ l1_pre_topc(A_427) ),
inference(cnfTransformation,[status(thm)],[f_286]) ).
tff(c_33437,plain,
! [A_1198,A_1199] :
( v1_tops_1(A_1198,A_1199)
| ( k6_pre_topc(A_1199,A_1198) != u1_struct_0(A_1199) )
| ~ l1_pre_topc(A_1199)
| ~ r1_tarski(A_1198,u1_struct_0(A_1199)) ),
inference(resolution,[status(thm)],[c_294,c_7215]) ).
tff(c_33490,plain,
! [A_1198] :
( v1_tops_1(A_1198,'#skF_1')
| ( k6_pre_topc('#skF_1',A_1198) != u1_struct_0('#skF_1') )
| ~ l1_pre_topc('#skF_1')
| ~ r1_tarski(A_1198,k2_pre_topc('#skF_1')) ),
inference(superposition,[status(thm),theory(equality)],[c_566,c_33437]) ).
tff(c_33526,plain,
! [A_1200] :
( v1_tops_1(A_1200,'#skF_1')
| ( k6_pre_topc('#skF_1',A_1200) != k2_pre_topc('#skF_1') )
| ~ r1_tarski(A_1200,k2_pre_topc('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_566,c_33490]) ).
tff(c_33569,plain,
( v1_tops_1('#skF_2','#skF_1')
| ( k6_pre_topc('#skF_1','#skF_2') != k2_pre_topc('#skF_1') ) ),
inference(resolution,[status(thm)],[c_680,c_33526]) ).
tff(c_33598,plain,
v1_tops_1('#skF_2','#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_19439,c_33569]) ).
tff(c_33600,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2,c_33598]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : TOP024+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.13/0.34 % Computer : n016.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Apr 9 10:32:08 EDT 2025
% 0.13/0.34 % CPUTime :
% 21.14/8.84 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.14/8.84
% 21.14/8.84 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------