%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : TOP041+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 : 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:30 PM UTC 2025
% Result : Theorem 23.63s 8.06s
% Output : CNFRefutation 23.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 16
% Syntax : Number of formulae : 102 ( 38 unt; 0 typ; 0 def)
% Number of atoms : 336 ( 32 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 381 ( 147 ~; 164 |; 36 &)
% ( 6 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 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 : 45 ( 43 usr; 1 prp; 0-3 aty)
% Number of functors : 39 ( 39 usr; 8 con; 0-4 aty)
% Number of variables : 89 ( 87 !; 2 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ v5_pre_topc > v1_funct_2 > m2_relset_1 > m1_relset_1 > v4_pre_topc > v3_tops_1 > v3_pre_topc > v2_tsp_2 > v2_tops_1 > v2_tex_2 > v1_tsep_1 > v1_tex_3 > v1_borsuk_1 > r2_hidden > r1_tarski > m2_tsp_1 > m1_tsp_1 > m1_subset_1 > m1_pre_topc > v5_tdlat_3 > v5_membered > v4_tdlat_3 > v4_ordinal2 > v4_membered > v3_tdlat_3 > v3_struct_0 > v3_realset2 > v3_membered > v2_tdlat_3 > v2_t_0topsp > v2_pre_topc > v2_membered > v1_xreal_0 > v1_xcmplx_0 > v1_xboole_0 > v1_tdlat_3 > v1_relat_1 > v1_rat_1 > v1_membered > v1_int_1 > v1_funct_1 > l1_struct_0 > l1_pre_topc > k4_pre_topc > k5_subset_1 > k9_relat_1 > k4_tsp_2 > k3_xboole_0 > k3_tex_4 > k2_zfmisc_1 > k1_tsp_2 > #nlpp > u1_struct_0 > k1_zfmisc_1 > k1_xboole_0 > #skF_25 > #skF_21 > #skF_16 > #skF_18 > #skF_17 > #skF_24 > #skF_6 > #skF_19 > #skF_4 > #skF_10 > #skF_12 > #skF_28 > #skF_5 > #skF_2 > #skF_3 > #skF_1 > #skF_8 > #skF_9 > #skF_23 > #skF_26 > #skF_13 > #skF_11 > #skF_22 > #skF_14 > #skF_27 > #skF_7 > #skF_15 > #skF_20
%Foreground sorts:
%Background operators:
%Foreground operators:
tff('#skF_25',type,
'#skF_25': $i > $i ).
tff(m2_relset_1,type,
m2_relset_1: ( $i * $i * $i ) > $o ).
tff(m2_tsp_1,type,
m2_tsp_1: ( $i * $i ) > $o ).
tff('#skF_21',type,
'#skF_21': $i > $i ).
tff('#skF_16',type,
'#skF_16': $i > $i ).
tff(v1_funct_1,type,
v1_funct_1: $i > $o ).
tff(v3_pre_topc,type,
v3_pre_topc: ( $i * $i ) > $o ).
tff('#skF_18',type,
'#skF_18': $i > $i ).
tff('#skF_17',type,
'#skF_17': $i ).
tff('#skF_24',type,
'#skF_24': $i > $i ).
tff(r2_hidden,type,
r2_hidden: ( $i * $i ) > $o ).
tff('#skF_6',type,
'#skF_6': ( $i * $i * $i ) > $i ).
tff('#skF_19',type,
'#skF_19': $i > $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(v1_tex_3,type,
v1_tex_3: ( $i * $i ) > $o ).
tff(l1_pre_topc,type,
l1_pre_topc: $i > $o ).
tff(k1_tsp_2,type,
k1_tsp_2: ( $i * $i ) > $i ).
tff(v3_tops_1,type,
v3_tops_1: ( $i * $i ) > $o ).
tff(v1_tdlat_3,type,
v1_tdlat_3: $i > $o ).
tff('#skF_4',type,
'#skF_4': ( $i * $i * $i ) > $i ).
tff(r1_tarski,type,
r1_tarski: ( $i * $i ) > $o ).
tff(v2_tsp_2,type,
v2_tsp_2: ( $i * $i ) > $o ).
tff('#skF_10',type,
'#skF_10': $i ).
tff(m1_relset_1,type,
m1_relset_1: ( $i * $i * $i ) > $o ).
tff(v5_tdlat_3,type,
v5_tdlat_3: $i > $o ).
tff(v4_ordinal2,type,
v4_ordinal2: $i > $o ).
tff(k5_subset_1,type,
k5_subset_1: ( $i * $i * $i ) > $i ).
tff('#skF_12',type,
'#skF_12': ( $i * $i ) > $i ).
tff(k3_tex_4,type,
k3_tex_4: ( $i * $i ) > $i ).
tff('#skF_28',type,
'#skF_28': $i > $i ).
tff(v1_funct_2,type,
v1_funct_2: ( $i * $i * $i ) > $o ).
tff(v2_tex_2,type,
v2_tex_2: ( $i * $i ) > $o ).
tff('#skF_5',type,
'#skF_5': ( $i * $i * $i ) > $i ).
tff('#skF_2',type,
'#skF_2': $i ).
tff(k9_relat_1,type,
k9_relat_1: ( $i * $i ) > $i ).
tff(v3_realset2,type,
v3_realset2: $i > $o ).
tff(v3_membered,type,
v3_membered: $i > $o ).
tff('#skF_3',type,
'#skF_3': $i ).
tff('#skF_1',type,
'#skF_1': $i ).
tff(v4_tdlat_3,type,
v4_tdlat_3: $i > $o ).
tff(v2_t_0topsp,type,
v2_t_0topsp: $i > $o ).
tff('#skF_8',type,
'#skF_8': ( $i * $i ) > $i ).
tff(v1_xreal_0,type,
v1_xreal_0: $i > $o ).
tff('#skF_9',type,
'#skF_9': $i ).
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('#skF_23',type,
'#skF_23': $i > $i ).
tff(v2_membered,type,
v2_membered: $i > $o ).
tff(v3_tdlat_3,type,
v3_tdlat_3: $i > $o ).
tff(v4_pre_topc,type,
v4_pre_topc: ( $i * $i ) > $o ).
tff(v1_membered,type,
v1_membered: $i > $o ).
tff('#skF_26',type,
'#skF_26': $i > $i ).
tff(v1_xcmplx_0,type,
v1_xcmplx_0: $i > $o ).
tff('#skF_13',type,
'#skF_13': $i > $i ).
tff(v1_relat_1,type,
v1_relat_1: $i > $o ).
tff(k2_zfmisc_1,type,
k2_zfmisc_1: ( $i * $i ) > $i ).
tff(v1_tsep_1,type,
v1_tsep_1: ( $i * $i ) > $o ).
tff('#skF_11',type,
'#skF_11': $i > $i ).
tff('#skF_22',type,
'#skF_22': $i ).
tff('#skF_14',type,
'#skF_14': $i > $i ).
tff(v5_pre_topc,type,
v5_pre_topc: ( $i * $i * $i ) > $o ).
tff(m1_pre_topc,type,
m1_pre_topc: ( $i * $i ) > $o ).
tff(k4_tsp_2,type,
k4_tsp_2: ( $i * $i ) > $i ).
tff(v2_pre_topc,type,
v2_pre_topc: $i > $o ).
tff(m1_tsp_1,type,
m1_tsp_1: ( $i * $i ) > $o ).
tff(v1_rat_1,type,
v1_rat_1: $i > $o ).
tff('#skF_27',type,
'#skF_27': $i > $i ).
tff(k3_xboole_0,type,
k3_xboole_0: ( $i * $i ) > $i ).
tff('#skF_7',type,
'#skF_7': ( $i * $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('#skF_15',type,
'#skF_15': ( $i * $i ) > $i ).
tff(k4_pre_topc,type,
k4_pre_topc: ( $i * $i * $i * $i ) > $i ).
tff('#skF_20',type,
'#skF_20': $i > $i ).
tff(v2_tdlat_3,type,
v2_tdlat_3: $i > $o ).
tff(v3_struct_0,type,
v3_struct_0: $i > $o ).
tff(m1_subset_1,type,
m1_subset_1: ( $i * $i ) > $o ).
tff(v1_borsuk_1,type,
v1_borsuk_1: ( $i * $i ) > $o ).
tff(f_52,negated_conjecture,
~ ! [A] :
( ( ~ v3_struct_0(A)
& v2_pre_topc(A)
& l1_pre_topc(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& v2_tsp_2(B,A)
& m2_tsp_1(B,A) )
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
=> ( v3_pre_topc(C,A)
=> v3_pre_topc(k4_pre_topc(A,B,k4_tsp_2(A,B),C),B) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t34_tsp_2) ).
tff(f_1290,axiom,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( m2_tsp_1(B,A)
<=> m1_pre_topc(B,A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_tsp_1) ).
tff(f_1279,axiom,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( m1_tsp_1(B,A)
<=> m1_pre_topc(B,A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m1_tsp_1) ).
tff(f_777,axiom,
! [A,B] : ( k3_xboole_0(A,B) = k3_xboole_0(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k3_xboole_0) ).
tff(f_1303,axiom,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( m1_pre_topc(B,A)
=> m1_subset_1(u1_struct_0(B),k1_zfmisc_1(u1_struct_0(A))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_tsep_1) ).
tff(f_1266,axiom,
! [A,B] :
( ( ~ v3_struct_0(A)
& v2_pre_topc(A)
& l1_pre_topc(A)
& ~ v3_struct_0(B)
& v2_tsp_2(B,A)
& m1_pre_topc(B,A) )
=> ( k4_tsp_2(A,B) = k1_tsp_2(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k4_tsp_2) ).
tff(f_906,axiom,
! [A,B] :
( ( ~ v3_struct_0(A)
& v2_pre_topc(A)
& l1_pre_topc(A)
& ~ v3_struct_0(B)
& v2_tsp_2(B,A)
& m1_pre_topc(B,A) )
=> ( v1_funct_1(k4_tsp_2(A,B))
& v1_funct_2(k4_tsp_2(A,B),u1_struct_0(A),u1_struct_0(B))
& v5_pre_topc(k4_tsp_2(A,B),A,B)
& m2_relset_1(k4_tsp_2(A,B),u1_struct_0(A),u1_struct_0(B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_tsp_2) ).
tff(f_819,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v2_pre_topc(A)
& l1_pre_topc(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& v2_tsp_2(B,A)
& m2_tsp_1(B,A) )
=> ! [C] :
( ( v1_funct_1(C)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v5_pre_topc(C,A,B)
& m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
=> ( ( C = k4_tsp_2(A,B) )
<=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))
=> ( ( D = u1_struct_0(B) )
=> ! [E] :
( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A)))
=> ( k5_subset_1(u1_struct_0(A),D,k3_tex_4(A,E)) = k4_pre_topc(A,B,C,E) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d12_tsp_2) ).
tff(f_1272,axiom,
! [A,B,C] :
( ( m1_subset_1(B,k1_zfmisc_1(A))
& m1_subset_1(C,k1_zfmisc_1(A)) )
=> ( k5_subset_1(A,B,C) = k3_xboole_0(B,C) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k5_subset_1) ).
tff(f_1335,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)))
=> ( v3_pre_topc(B,A)
=> ( k3_tex_4(A,B) = B ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t58_tex_4) ).
tff(f_941,axiom,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( m2_tsp_1(B,A)
=> l1_pre_topc(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_tsp_1) ).
tff(f_916,axiom,
! [A] :
( l1_pre_topc(A)
=> l1_struct_0(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
tff(f_1187,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& l1_struct_0(A) )
=> ? [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
& ~ v1_xboole_0(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc5_struct_0) ).
tff(f_1283,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_884,axiom,
! [A,B,C,D] :
( ( l1_struct_0(A)
& l1_struct_0(B)
& v1_funct_1(C)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
=> m1_subset_1(k4_pre_topc(A,B,C,D),k1_zfmisc_1(u1_struct_0(B))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_pre_topc) ).
tff(f_840,axiom,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( l1_pre_topc(B)
=> ( m1_tsp_1(B,A)
<=> ( r1_tarski(u1_struct_0(B),u1_struct_0(A))
& ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
=> ( v3_pre_topc(C,B)
<=> ? [D] :
( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))
& v3_pre_topc(D,A)
& ( C = k3_xboole_0(D,u1_struct_0(B)) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_tsp_1) ).
tff(c_14,plain,
l1_pre_topc('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_8,plain,
m2_tsp_1('#skF_2','#skF_1'),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_3211,plain,
! [B_635,A_636] :
( m1_pre_topc(B_635,A_636)
| ~ m2_tsp_1(B_635,A_636)
| ~ l1_pre_topc(A_636) ),
inference(cnfTransformation,[status(thm)],[f_1290]) ).
tff(c_3220,plain,
( m1_pre_topc('#skF_2','#skF_1')
| ~ l1_pre_topc('#skF_1') ),
inference(resolution,[status(thm)],[c_8,c_3211]) ).
tff(c_3225,plain,
m1_pre_topc('#skF_2','#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_3220]) ).
tff(c_576,plain,
! [B_313,A_311] :
( m1_tsp_1(B_313,A_311)
| ~ m1_pre_topc(B_313,A_311)
| ~ l1_pre_topc(A_311) ),
inference(cnfTransformation,[status(thm)],[f_1279]) ).
tff(c_6,plain,
m1_subset_1('#skF_3',k1_zfmisc_1(u1_struct_0('#skF_1'))),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_284,plain,
! [B_116,A_115] : ( k3_xboole_0(B_116,A_115) = k3_xboole_0(A_115,B_116) ),
inference(cnfTransformation,[status(thm)],[f_777]) ).
tff(c_590,plain,
! [B_326,A_324] :
( m1_subset_1(u1_struct_0(B_326),k1_zfmisc_1(u1_struct_0(A_324)))
| ~ m1_pre_topc(B_326,A_324)
| ~ l1_pre_topc(A_324) ),
inference(cnfTransformation,[status(thm)],[f_1303]) ).
tff(c_18,plain,
~ v3_struct_0('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_12,plain,
~ v3_struct_0('#skF_2'),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_16,plain,
v2_pre_topc('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_10,plain,
v2_tsp_2('#skF_2','#skF_1'),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_9823,plain,
! [A_1024,B_1025] :
( ( k4_tsp_2(A_1024,B_1025) = k1_tsp_2(A_1024,B_1025) )
| ~ m1_pre_topc(B_1025,A_1024)
| ~ v2_tsp_2(B_1025,A_1024)
| v3_struct_0(B_1025)
| ~ l1_pre_topc(A_1024)
| ~ v2_pre_topc(A_1024)
| v3_struct_0(A_1024) ),
inference(cnfTransformation,[status(thm)],[f_1266]) ).
tff(c_9826,plain,
( ( k4_tsp_2('#skF_1','#skF_2') = k1_tsp_2('#skF_1','#skF_2') )
| ~ m1_pre_topc('#skF_2','#skF_1')
| v3_struct_0('#skF_2')
| ~ l1_pre_topc('#skF_1')
| ~ v2_pre_topc('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_10,c_9823]) ).
tff(c_9829,plain,
( ( k4_tsp_2('#skF_1','#skF_2') = k1_tsp_2('#skF_1','#skF_2') )
| v3_struct_0('#skF_2')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_14,c_3225,c_9826]) ).
tff(c_9830,plain,
k4_tsp_2('#skF_1','#skF_2') = k1_tsp_2('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_18,c_12,c_9829]) ).
tff(c_352,plain,
! [A_221,B_222] :
( v1_funct_1(k4_tsp_2(A_221,B_222))
| ~ m1_pre_topc(B_222,A_221)
| ~ v2_tsp_2(B_222,A_221)
| v3_struct_0(B_222)
| ~ l1_pre_topc(A_221)
| ~ v2_pre_topc(A_221)
| v3_struct_0(A_221) ),
inference(cnfTransformation,[status(thm)],[f_906]) ).
tff(c_9838,plain,
( v1_funct_1(k1_tsp_2('#skF_1','#skF_2'))
| ~ m1_pre_topc('#skF_2','#skF_1')
| ~ v2_tsp_2('#skF_2','#skF_1')
| v3_struct_0('#skF_2')
| ~ l1_pre_topc('#skF_1')
| ~ v2_pre_topc('#skF_1')
| v3_struct_0('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_9830,c_352]) ).
tff(c_9845,plain,
( v1_funct_1(k1_tsp_2('#skF_1','#skF_2'))
| v3_struct_0('#skF_2')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_14,c_10,c_3225,c_9838]) ).
tff(c_9846,plain,
v1_funct_1(k1_tsp_2('#skF_1','#skF_2')),
inference(negUnitSimplification,[status(thm)],[c_18,c_12,c_9845]) ).
tff(c_11074,plain,
! [A_1087,B_1088] :
( v1_funct_2(k4_tsp_2(A_1087,B_1088),u1_struct_0(A_1087),u1_struct_0(B_1088))
| ~ m1_pre_topc(B_1088,A_1087)
| ~ v2_tsp_2(B_1088,A_1087)
| v3_struct_0(B_1088)
| ~ l1_pre_topc(A_1087)
| ~ v2_pre_topc(A_1087)
| v3_struct_0(A_1087) ),
inference(cnfTransformation,[status(thm)],[f_906]) ).
tff(c_11077,plain,
( v1_funct_2(k1_tsp_2('#skF_1','#skF_2'),u1_struct_0('#skF_1'),u1_struct_0('#skF_2'))
| ~ m1_pre_topc('#skF_2','#skF_1')
| ~ v2_tsp_2('#skF_2','#skF_1')
| v3_struct_0('#skF_2')
| ~ l1_pre_topc('#skF_1')
| ~ v2_pre_topc('#skF_1')
| v3_struct_0('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_9830,c_11074]) ).
tff(c_11079,plain,
( v1_funct_2(k1_tsp_2('#skF_1','#skF_2'),u1_struct_0('#skF_1'),u1_struct_0('#skF_2'))
| v3_struct_0('#skF_2')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_14,c_10,c_3225,c_11077]) ).
tff(c_11080,plain,
v1_funct_2(k1_tsp_2('#skF_1','#skF_2'),u1_struct_0('#skF_1'),u1_struct_0('#skF_2')),
inference(negUnitSimplification,[status(thm)],[c_18,c_12,c_11079]) ).
tff(c_348,plain,
! [A_221,B_222] :
( v5_pre_topc(k4_tsp_2(A_221,B_222),A_221,B_222)
| ~ m1_pre_topc(B_222,A_221)
| ~ v2_tsp_2(B_222,A_221)
| v3_struct_0(B_222)
| ~ l1_pre_topc(A_221)
| ~ v2_pre_topc(A_221)
| v3_struct_0(A_221) ),
inference(cnfTransformation,[status(thm)],[f_906]) ).
tff(c_9835,plain,
( v5_pre_topc(k1_tsp_2('#skF_1','#skF_2'),'#skF_1','#skF_2')
| ~ m1_pre_topc('#skF_2','#skF_1')
| ~ v2_tsp_2('#skF_2','#skF_1')
| v3_struct_0('#skF_2')
| ~ l1_pre_topc('#skF_1')
| ~ v2_pre_topc('#skF_1')
| v3_struct_0('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_9830,c_348]) ).
tff(c_9842,plain,
( v5_pre_topc(k1_tsp_2('#skF_1','#skF_2'),'#skF_1','#skF_2')
| v3_struct_0('#skF_2')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_14,c_10,c_3225,c_9835]) ).
tff(c_9843,plain,
v5_pre_topc(k1_tsp_2('#skF_1','#skF_2'),'#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_18,c_12,c_9842]) ).
tff(c_10789,plain,
! [A_1071,B_1072] :
( m2_relset_1(k4_tsp_2(A_1071,B_1072),u1_struct_0(A_1071),u1_struct_0(B_1072))
| ~ m1_pre_topc(B_1072,A_1071)
| ~ v2_tsp_2(B_1072,A_1071)
| v3_struct_0(B_1072)
| ~ l1_pre_topc(A_1071)
| ~ v2_pre_topc(A_1071)
| v3_struct_0(A_1071) ),
inference(cnfTransformation,[status(thm)],[f_906]) ).
tff(c_10808,plain,
( m2_relset_1(k1_tsp_2('#skF_1','#skF_2'),u1_struct_0('#skF_1'),u1_struct_0('#skF_2'))
| ~ m1_pre_topc('#skF_2','#skF_1')
| ~ v2_tsp_2('#skF_2','#skF_1')
| v3_struct_0('#skF_2')
| ~ l1_pre_topc('#skF_1')
| ~ v2_pre_topc('#skF_1')
| v3_struct_0('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_9830,c_10789]) ).
tff(c_10817,plain,
( m2_relset_1(k1_tsp_2('#skF_1','#skF_2'),u1_struct_0('#skF_1'),u1_struct_0('#skF_2'))
| v3_struct_0('#skF_2')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_14,c_10,c_3225,c_10808]) ).
tff(c_10818,plain,
m2_relset_1(k1_tsp_2('#skF_1','#skF_2'),u1_struct_0('#skF_1'),u1_struct_0('#skF_2')),
inference(negUnitSimplification,[status(thm)],[c_18,c_12,c_10817]) ).
tff(c_19452,plain,
! [A_1298,B_1299,E_1300] :
( ( k5_subset_1(u1_struct_0(A_1298),u1_struct_0(B_1299),k3_tex_4(A_1298,E_1300)) = k4_pre_topc(A_1298,B_1299,k4_tsp_2(A_1298,B_1299),E_1300) )
| ~ m1_subset_1(E_1300,k1_zfmisc_1(u1_struct_0(A_1298)))
| ~ m1_subset_1(u1_struct_0(B_1299),k1_zfmisc_1(u1_struct_0(A_1298)))
| ~ m2_relset_1(k4_tsp_2(A_1298,B_1299),u1_struct_0(A_1298),u1_struct_0(B_1299))
| ~ v5_pre_topc(k4_tsp_2(A_1298,B_1299),A_1298,B_1299)
| ~ v1_funct_2(k4_tsp_2(A_1298,B_1299),u1_struct_0(A_1298),u1_struct_0(B_1299))
| ~ v1_funct_1(k4_tsp_2(A_1298,B_1299))
| ~ m2_tsp_1(B_1299,A_1298)
| ~ v2_tsp_2(B_1299,A_1298)
| v3_struct_0(B_1299)
| ~ l1_pre_topc(A_1298)
| ~ v2_pre_topc(A_1298)
| v3_struct_0(A_1298) ),
inference(cnfTransformation,[status(thm)],[f_819]) ).
tff(c_19456,plain,
! [E_1300] :
( ( k5_subset_1(u1_struct_0('#skF_1'),u1_struct_0('#skF_2'),k3_tex_4('#skF_1',E_1300)) = k4_pre_topc('#skF_1','#skF_2',k4_tsp_2('#skF_1','#skF_2'),E_1300) )
| ~ m1_subset_1(E_1300,k1_zfmisc_1(u1_struct_0('#skF_1')))
| ~ m1_subset_1(u1_struct_0('#skF_2'),k1_zfmisc_1(u1_struct_0('#skF_1')))
| ~ m2_relset_1(k4_tsp_2('#skF_1','#skF_2'),u1_struct_0('#skF_1'),u1_struct_0('#skF_2'))
| ~ v5_pre_topc(k4_tsp_2('#skF_1','#skF_2'),'#skF_1','#skF_2')
| ~ v1_funct_2(k1_tsp_2('#skF_1','#skF_2'),u1_struct_0('#skF_1'),u1_struct_0('#skF_2'))
| ~ v1_funct_1(k4_tsp_2('#skF_1','#skF_2'))
| ~ m2_tsp_1('#skF_2','#skF_1')
| ~ v2_tsp_2('#skF_2','#skF_1')
| v3_struct_0('#skF_2')
| ~ l1_pre_topc('#skF_1')
| ~ v2_pre_topc('#skF_1')
| v3_struct_0('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_9830,c_19452]) ).
tff(c_19459,plain,
! [E_1300] :
( ( k5_subset_1(u1_struct_0('#skF_1'),u1_struct_0('#skF_2'),k3_tex_4('#skF_1',E_1300)) = k4_pre_topc('#skF_1','#skF_2',k1_tsp_2('#skF_1','#skF_2'),E_1300) )
| ~ m1_subset_1(E_1300,k1_zfmisc_1(u1_struct_0('#skF_1')))
| ~ m1_subset_1(u1_struct_0('#skF_2'),k1_zfmisc_1(u1_struct_0('#skF_1')))
| v3_struct_0('#skF_2')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_14,c_10,c_8,c_9846,c_9830,c_11080,c_9843,c_9830,c_10818,c_9830,c_9830,c_19456]) ).
tff(c_19460,plain,
! [E_1300] :
( ( k5_subset_1(u1_struct_0('#skF_1'),u1_struct_0('#skF_2'),k3_tex_4('#skF_1',E_1300)) = k4_pre_topc('#skF_1','#skF_2',k1_tsp_2('#skF_1','#skF_2'),E_1300) )
| ~ m1_subset_1(E_1300,k1_zfmisc_1(u1_struct_0('#skF_1')))
| ~ m1_subset_1(u1_struct_0('#skF_2'),k1_zfmisc_1(u1_struct_0('#skF_1'))) ),
inference(negUnitSimplification,[status(thm)],[c_18,c_12,c_19459]) ).
tff(c_19530,plain,
~ m1_subset_1(u1_struct_0('#skF_2'),k1_zfmisc_1(u1_struct_0('#skF_1'))),
inference(splitLeft,[status(thm)],[c_19460]) ).
tff(c_19533,plain,
( ~ m1_pre_topc('#skF_2','#skF_1')
| ~ l1_pre_topc('#skF_1') ),
inference(resolution,[status(thm)],[c_590,c_19530]) ).
tff(c_19540,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_3225,c_19533]) ).
tff(c_19542,plain,
m1_subset_1(u1_struct_0('#skF_2'),k1_zfmisc_1(u1_struct_0('#skF_1'))),
inference(splitRight,[status(thm)],[c_19460]) ).
tff(c_6744,plain,
! [A_880,B_881,C_882] :
( ( k5_subset_1(A_880,B_881,C_882) = k3_xboole_0(B_881,C_882) )
| ~ m1_subset_1(C_882,k1_zfmisc_1(A_880))
| ~ m1_subset_1(B_881,k1_zfmisc_1(A_880)) ),
inference(cnfTransformation,[status(thm)],[f_1272]) ).
tff(c_6790,plain,
! [B_881] :
( ( k5_subset_1(u1_struct_0('#skF_1'),B_881,'#skF_3') = k3_xboole_0(B_881,'#skF_3') )
| ~ m1_subset_1(B_881,k1_zfmisc_1(u1_struct_0('#skF_1'))) ),
inference(resolution,[status(thm)],[c_6,c_6744]) ).
tff(c_19594,plain,
k5_subset_1(u1_struct_0('#skF_1'),u1_struct_0('#skF_2'),'#skF_3') = k3_xboole_0(u1_struct_0('#skF_2'),'#skF_3'),
inference(resolution,[status(thm)],[c_19542,c_6790]) ).
tff(c_19759,plain,
k5_subset_1(u1_struct_0('#skF_1'),u1_struct_0('#skF_2'),'#skF_3') = k3_xboole_0('#skF_3',u1_struct_0('#skF_2')),
inference(demodulation,[status(thm),theory(equality)],[c_284,c_19594]) ).
tff(c_4,plain,
v3_pre_topc('#skF_3','#skF_1'),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_8964,plain,
! [A_992,B_993] :
( ( k3_tex_4(A_992,B_993) = B_993 )
| ~ v3_pre_topc(B_993,A_992)
| ~ m1_subset_1(B_993,k1_zfmisc_1(u1_struct_0(A_992)))
| ~ l1_pre_topc(A_992)
| ~ v2_pre_topc(A_992)
| v3_struct_0(A_992) ),
inference(cnfTransformation,[status(thm)],[f_1335]) ).
tff(c_9013,plain,
( ( k3_tex_4('#skF_1','#skF_3') = '#skF_3' )
| ~ v3_pre_topc('#skF_3','#skF_1')
| ~ l1_pre_topc('#skF_1')
| ~ v2_pre_topc('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_6,c_8964]) ).
tff(c_9034,plain,
( ( k3_tex_4('#skF_1','#skF_3') = '#skF_3' )
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_14,c_4,c_9013]) ).
tff(c_9035,plain,
k3_tex_4('#skF_1','#skF_3') = '#skF_3',
inference(negUnitSimplification,[status(thm)],[c_18,c_9034]) ).
tff(c_22216,plain,
! [E_1375] :
( ( k5_subset_1(u1_struct_0('#skF_1'),u1_struct_0('#skF_2'),k3_tex_4('#skF_1',E_1375)) = k4_pre_topc('#skF_1','#skF_2',k1_tsp_2('#skF_1','#skF_2'),E_1375) )
| ~ m1_subset_1(E_1375,k1_zfmisc_1(u1_struct_0('#skF_1'))) ),
inference(splitRight,[status(thm)],[c_19460]) ).
tff(c_22237,plain,
( ( k5_subset_1(u1_struct_0('#skF_1'),u1_struct_0('#skF_2'),'#skF_3') = k4_pre_topc('#skF_1','#skF_2',k1_tsp_2('#skF_1','#skF_2'),'#skF_3') )
| ~ m1_subset_1('#skF_3',k1_zfmisc_1(u1_struct_0('#skF_1'))) ),
inference(superposition,[status(thm),theory(equality)],[c_9035,c_22216]) ).
tff(c_22249,plain,
k4_pre_topc('#skF_1','#skF_2',k1_tsp_2('#skF_1','#skF_2'),'#skF_3') = k3_xboole_0('#skF_3',u1_struct_0('#skF_2')),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_19759,c_22237]) ).
tff(c_2,plain,
~ v3_pre_topc(k4_pre_topc('#skF_1','#skF_2',k4_tsp_2('#skF_1','#skF_2'),'#skF_3'),'#skF_2'),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_9831,plain,
~ v3_pre_topc(k4_pre_topc('#skF_1','#skF_2',k1_tsp_2('#skF_1','#skF_2'),'#skF_3'),'#skF_2'),
inference(demodulation,[status(thm),theory(equality)],[c_9830,c_2]) ).
tff(c_22541,plain,
~ v3_pre_topc(k3_xboole_0('#skF_3',u1_struct_0('#skF_2')),'#skF_2'),
inference(demodulation,[status(thm),theory(equality)],[c_22249,c_9831]) ).
tff(c_2083,plain,
! [B_500,A_501] :
( l1_pre_topc(B_500)
| ~ m2_tsp_1(B_500,A_501)
| ~ l1_pre_topc(A_501) ),
inference(cnfTransformation,[status(thm)],[f_941]) ).
tff(c_2089,plain,
( l1_pre_topc('#skF_2')
| ~ l1_pre_topc('#skF_1') ),
inference(resolution,[status(thm)],[c_8,c_2083]) ).
tff(c_2093,plain,
l1_pre_topc('#skF_2'),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_2089]) ).
tff(c_358,plain,
! [A_226] :
( l1_struct_0(A_226)
| ~ l1_pre_topc(A_226) ),
inference(cnfTransformation,[status(thm)],[f_916]) ).
tff(c_534,plain,
! [A_294] :
( m1_subset_1('#skF_25'(A_294),k1_zfmisc_1(u1_struct_0(A_294)))
| ~ l1_struct_0(A_294)
| v3_struct_0(A_294) ),
inference(cnfTransformation,[status(thm)],[f_1187]) ).
tff(c_6968,plain,
! [B_892] :
( ( k5_subset_1(u1_struct_0('#skF_1'),B_892,'#skF_3') = k3_xboole_0(B_892,'#skF_3') )
| ~ m1_subset_1(B_892,k1_zfmisc_1(u1_struct_0('#skF_1'))) ),
inference(resolution,[status(thm)],[c_6,c_6744]) ).
tff(c_6988,plain,
( ( k5_subset_1(u1_struct_0('#skF_1'),'#skF_25'('#skF_1'),'#skF_3') = k3_xboole_0('#skF_25'('#skF_1'),'#skF_3') )
| ~ l1_struct_0('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_534,c_6968]) ).
tff(c_7039,plain,
( ( k5_subset_1(u1_struct_0('#skF_1'),'#skF_25'('#skF_1'),'#skF_3') = k3_xboole_0('#skF_3','#skF_25'('#skF_1')) )
| ~ l1_struct_0('#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_284,c_6988]) ).
tff(c_7040,plain,
( ( k5_subset_1(u1_struct_0('#skF_1'),'#skF_25'('#skF_1'),'#skF_3') = k3_xboole_0('#skF_3','#skF_25'('#skF_1')) )
| ~ l1_struct_0('#skF_1') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_7039]) ).
tff(c_7492,plain,
~ l1_struct_0('#skF_1'),
inference(splitLeft,[status(thm)],[c_7040]) ).
tff(c_7495,plain,
~ l1_pre_topc('#skF_1'),
inference(resolution,[status(thm)],[c_358,c_7492]) ).
tff(c_7499,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_7495]) ).
tff(c_7501,plain,
l1_struct_0('#skF_1'),
inference(splitRight,[status(thm)],[c_7040]) ).
tff(c_578,plain,
! [C_316,A_314,B_315] :
( m1_relset_1(C_316,A_314,B_315)
| ~ m2_relset_1(C_316,A_314,B_315) ),
inference(cnfTransformation,[status(thm)],[f_1283]) ).
tff(c_10841,plain,
m1_relset_1(k1_tsp_2('#skF_1','#skF_2'),u1_struct_0('#skF_1'),u1_struct_0('#skF_2')),
inference(resolution,[status(thm)],[c_10818,c_578]) ).
tff(c_344,plain,
! [A_217,B_218,C_219,D_220] :
( m1_subset_1(k4_pre_topc(A_217,B_218,C_219,D_220),k1_zfmisc_1(u1_struct_0(B_218)))
| ~ m1_relset_1(C_219,u1_struct_0(A_217),u1_struct_0(B_218))
| ~ v1_funct_2(C_219,u1_struct_0(A_217),u1_struct_0(B_218))
| ~ v1_funct_1(C_219)
| ~ l1_struct_0(B_218)
| ~ l1_struct_0(A_217) ),
inference(cnfTransformation,[status(thm)],[f_884]) ).
tff(c_22545,plain,
( m1_subset_1(k3_xboole_0('#skF_3',u1_struct_0('#skF_2')),k1_zfmisc_1(u1_struct_0('#skF_2')))
| ~ m1_relset_1(k1_tsp_2('#skF_1','#skF_2'),u1_struct_0('#skF_1'),u1_struct_0('#skF_2'))
| ~ v1_funct_2(k1_tsp_2('#skF_1','#skF_2'),u1_struct_0('#skF_1'),u1_struct_0('#skF_2'))
| ~ v1_funct_1(k1_tsp_2('#skF_1','#skF_2'))
| ~ l1_struct_0('#skF_2')
| ~ l1_struct_0('#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_22249,c_344]) ).
tff(c_22549,plain,
( m1_subset_1(k3_xboole_0('#skF_3',u1_struct_0('#skF_2')),k1_zfmisc_1(u1_struct_0('#skF_2')))
| ~ l1_struct_0('#skF_2') ),
inference(demodulation,[status(thm),theory(equality)],[c_7501,c_9846,c_11080,c_10841,c_22545]) ).
tff(c_22551,plain,
~ l1_struct_0('#skF_2'),
inference(splitLeft,[status(thm)],[c_22549]) ).
tff(c_22554,plain,
~ l1_pre_topc('#skF_2'),
inference(resolution,[status(thm)],[c_358,c_22551]) ).
tff(c_22558,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2093,c_22554]) ).
tff(c_22559,plain,
m1_subset_1(k3_xboole_0('#skF_3',u1_struct_0('#skF_2')),k1_zfmisc_1(u1_struct_0('#skF_2'))),
inference(splitRight,[status(thm)],[c_22549]) ).
tff(c_13300,plain,
! [D_1181,B_1182,A_1183] :
( v3_pre_topc(k3_xboole_0(D_1181,u1_struct_0(B_1182)),B_1182)
| ~ v3_pre_topc(D_1181,A_1183)
| ~ m1_subset_1(D_1181,k1_zfmisc_1(u1_struct_0(A_1183)))
| ~ m1_subset_1(k3_xboole_0(D_1181,u1_struct_0(B_1182)),k1_zfmisc_1(u1_struct_0(B_1182)))
| ~ m1_tsp_1(B_1182,A_1183)
| ~ l1_pre_topc(B_1182)
| ~ l1_pre_topc(A_1183) ),
inference(cnfTransformation,[status(thm)],[f_840]) ).
tff(c_13342,plain,
! [B_1182] :
( v3_pre_topc(k3_xboole_0('#skF_3',u1_struct_0(B_1182)),B_1182)
| ~ v3_pre_topc('#skF_3','#skF_1')
| ~ m1_subset_1(k3_xboole_0('#skF_3',u1_struct_0(B_1182)),k1_zfmisc_1(u1_struct_0(B_1182)))
| ~ m1_tsp_1(B_1182,'#skF_1')
| ~ l1_pre_topc(B_1182)
| ~ l1_pre_topc('#skF_1') ),
inference(resolution,[status(thm)],[c_6,c_13300]) ).
tff(c_13368,plain,
! [B_1182] :
( v3_pre_topc(k3_xboole_0('#skF_3',u1_struct_0(B_1182)),B_1182)
| ~ m1_subset_1(k3_xboole_0('#skF_3',u1_struct_0(B_1182)),k1_zfmisc_1(u1_struct_0(B_1182)))
| ~ m1_tsp_1(B_1182,'#skF_1')
| ~ l1_pre_topc(B_1182) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_4,c_13342]) ).
tff(c_22580,plain,
( v3_pre_topc(k3_xboole_0('#skF_3',u1_struct_0('#skF_2')),'#skF_2')
| ~ m1_tsp_1('#skF_2','#skF_1')
| ~ l1_pre_topc('#skF_2') ),
inference(resolution,[status(thm)],[c_22559,c_13368]) ).
tff(c_22739,plain,
( v3_pre_topc(k3_xboole_0('#skF_3',u1_struct_0('#skF_2')),'#skF_2')
| ~ m1_tsp_1('#skF_2','#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_2093,c_22580]) ).
tff(c_22740,plain,
~ m1_tsp_1('#skF_2','#skF_1'),
inference(negUnitSimplification,[status(thm)],[c_22541,c_22739]) ).
tff(c_22836,plain,
( ~ m1_pre_topc('#skF_2','#skF_1')
| ~ l1_pre_topc('#skF_1') ),
inference(resolution,[status(thm)],[c_576,c_22740]) ).
tff(c_22840,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_3225,c_22836]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : TOP041+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/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.13/0.35 % Computer : n016.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed Apr 9 10:42:23 EDT 2025
% 0.13/0.35 % CPUTime :
% 23.63/8.06 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.63/8.07
% 23.63/8.07 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------