%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SEU417+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 : n007.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 08:53:57 PM UTC 2025
% Result : Theorem 75.41s 58.34s
% Output : CNFRefutation 75.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 11
% Syntax : Number of formulae : 46 ( 23 unt; 0 typ; 0 def)
% Number of atoms : 93 ( 25 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 80 ( 33 ~; 28 |; 5 &)
% ( 0 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 7 con; 0-3 aty)
% Number of variables : 73 ( 73 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ r2_hidden > r1_tarski > m1_subset_1 > v3_relat_1 > v1_xboole_0 > v1_relat_1 > k5_subset_1 > k4_subset_1 > k1_relset_2 > k8_setfam_1 > k3_xboole_0 > k2_xboole_0 > #nlpp > k1_zfmisc_1 > k1_xboole_0 > #skF_4 > #skF_8 > #skF_7 > #skF_5 > #skF_2 > #skF_3 > #skF_1 > #skF_9 > #skF_6
%Foreground sorts:
%Background operators:
%Foreground operators:
tff('#skF_4',type,
'#skF_4': $i > $i ).
tff(r2_hidden,type,
r2_hidden: ( $i * $i ) > $o ).
tff(k1_xboole_0,type,
k1_xboole_0: $i ).
tff(k8_setfam_1,type,
k8_setfam_1: ( $i * $i ) > $i ).
tff(v3_relat_1,type,
v3_relat_1: $i > $o ).
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(k5_subset_1,type,
k5_subset_1: ( $i * $i * $i ) > $i ).
tff(k4_subset_1,type,
k4_subset_1: ( $i * $i * $i ) > $i ).
tff('#skF_5',type,
'#skF_5': $i ).
tff(k1_relset_2,type,
k1_relset_2: ( $i * $i * $i ) > $i ).
tff('#skF_2',type,
'#skF_2': $i ).
tff('#skF_3',type,
'#skF_3': $i ).
tff('#skF_1',type,
'#skF_1': $i ).
tff('#skF_9',type,
'#skF_9': $i ).
tff(k1_zfmisc_1,type,
k1_zfmisc_1: $i > $i ).
tff(v1_relat_1,type,
v1_relat_1: $i > $o ).
tff(k3_xboole_0,type,
k3_xboole_0: ( $i * $i ) > $i ).
tff(k2_xboole_0,type,
k2_xboole_0: ( $i * $i ) > $i ).
tff(v1_xboole_0,type,
v1_xboole_0: $i > $o ).
tff('#skF_6',type,
'#skF_6': $i > $i ).
tff(m1_subset_1,type,
m1_subset_1: ( $i * $i ) > $o ).
tff(f_37,negated_conjecture,
~ ! [A,B] :
( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(A)))
=> r1_tarski(k5_subset_1(A,k8_setfam_1(A,B),k8_setfam_1(A,C)),k8_setfam_1(A,k1_relset_2(A,B,C))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_relset_2) ).
tff(f_184,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_87,axiom,
! [A,B,C] :
( ( m1_subset_1(B,k1_zfmisc_1(A))
& m1_subset_1(C,k1_zfmisc_1(A)) )
=> m1_subset_1(k5_subset_1(A,B,C),k1_zfmisc_1(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_subset_1) ).
tff(f_54,axiom,
! [A,B] : ( k2_xboole_0(A,B) = k2_xboole_0(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k2_xboole_0) ).
tff(f_178,axiom,
! [A,B,C] :
( ( m1_subset_1(B,k1_zfmisc_1(A))
& m1_subset_1(C,k1_zfmisc_1(A)) )
=> ( k4_subset_1(A,B,C) = k2_xboole_0(B,C) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k4_subset_1) ).
tff(f_81,axiom,
! [A,B,C] :
( ( m1_subset_1(B,k1_zfmisc_1(A))
& m1_subset_1(C,k1_zfmisc_1(A)) )
=> m1_subset_1(k4_subset_1(A,B,C),k1_zfmisc_1(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_subset_1) ).
tff(f_56,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_194,axiom,
! [A,B,C] : r1_tarski(k3_xboole_0(A,B),k2_xboole_0(A,C)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t29_xboole_1) ).
tff(f_221,axiom,
! [A,B] :
( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(A)))
=> ( r1_tarski(B,C)
=> r1_tarski(k8_setfam_1(A,C),k8_setfam_1(A,B)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t59_setfam_1) ).
tff(f_257,axiom,
! [A,B] :
( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(A)))
=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(k1_zfmisc_1(A)))
=> ( ( B = k4_subset_1(k1_zfmisc_1(A),C,D) )
=> ( k8_setfam_1(A,B) = k5_subset_1(A,k8_setfam_1(A,C),k8_setfam_1(A,D)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_mssubfam) ).
tff(f_172,axiom,
! [A,B,C] :
( ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
& m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(A))) )
=> ( k1_relset_2(A,B,C) = k3_xboole_0(B,C) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k1_relset_2) ).
tff(c_4,plain,
m1_subset_1('#skF_3',k1_zfmisc_1(k1_zfmisc_1('#skF_1'))),
inference(cnfTransformation,[status(thm)],[f_37]) ).
tff(c_6,plain,
m1_subset_1('#skF_2',k1_zfmisc_1(k1_zfmisc_1('#skF_1'))),
inference(cnfTransformation,[status(thm)],[f_37]) ).
tff(c_58194,plain,
! [A_1908,B_1909,C_1910] :
( ( k5_subset_1(A_1908,B_1909,C_1910) = k3_xboole_0(B_1909,C_1910) )
| ~ m1_subset_1(C_1910,k1_zfmisc_1(A_1908))
| ~ m1_subset_1(B_1909,k1_zfmisc_1(A_1908)) ),
inference(cnfTransformation,[status(thm)],[f_184]) ).
tff(c_59265,plain,
! [B_1956] :
( ( k5_subset_1(k1_zfmisc_1('#skF_1'),B_1956,'#skF_2') = k3_xboole_0(B_1956,'#skF_2') )
| ~ m1_subset_1(B_1956,k1_zfmisc_1(k1_zfmisc_1('#skF_1'))) ),
inference(resolution,[status(thm)],[c_6,c_58194]) ).
tff(c_59317,plain,
k5_subset_1(k1_zfmisc_1('#skF_1'),'#skF_3','#skF_2') = k3_xboole_0('#skF_3','#skF_2'),
inference(resolution,[status(thm)],[c_4,c_59265]) ).
tff(c_34,plain,
! [A_24,B_25,C_26] :
( m1_subset_1(k5_subset_1(A_24,B_25,C_26),k1_zfmisc_1(A_24))
| ~ m1_subset_1(C_26,k1_zfmisc_1(A_24))
| ~ m1_subset_1(B_25,k1_zfmisc_1(A_24)) ),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_59334,plain,
( m1_subset_1(k3_xboole_0('#skF_3','#skF_2'),k1_zfmisc_1(k1_zfmisc_1('#skF_1')))
| ~ m1_subset_1('#skF_2',k1_zfmisc_1(k1_zfmisc_1('#skF_1')))
| ~ m1_subset_1('#skF_3',k1_zfmisc_1(k1_zfmisc_1('#skF_1'))) ),
inference(superposition,[status(thm),theory(equality)],[c_59317,c_34]) ).
tff(c_59338,plain,
m1_subset_1(k3_xboole_0('#skF_3','#skF_2'),k1_zfmisc_1(k1_zfmisc_1('#skF_1'))),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_6,c_59334]) ).
tff(c_14,plain,
! [B_9,A_8] : ( k2_xboole_0(B_9,A_8) = k2_xboole_0(A_8,B_9) ),
inference(cnfTransformation,[status(thm)],[f_54]) ).
tff(c_58281,plain,
! [A_1916,B_1917,C_1918] :
( ( k4_subset_1(A_1916,B_1917,C_1918) = k2_xboole_0(B_1917,C_1918) )
| ~ m1_subset_1(C_1918,k1_zfmisc_1(A_1916))
| ~ m1_subset_1(B_1917,k1_zfmisc_1(A_1916)) ),
inference(cnfTransformation,[status(thm)],[f_178]) ).
tff(c_59074,plain,
! [B_1951] :
( ( k4_subset_1(k1_zfmisc_1('#skF_1'),B_1951,'#skF_3') = k2_xboole_0(B_1951,'#skF_3') )
| ~ m1_subset_1(B_1951,k1_zfmisc_1(k1_zfmisc_1('#skF_1'))) ),
inference(resolution,[status(thm)],[c_4,c_58281]) ).
tff(c_59108,plain,
k4_subset_1(k1_zfmisc_1('#skF_1'),'#skF_2','#skF_3') = k2_xboole_0('#skF_2','#skF_3'),
inference(resolution,[status(thm)],[c_6,c_59074]) ).
tff(c_59126,plain,
k4_subset_1(k1_zfmisc_1('#skF_1'),'#skF_2','#skF_3') = k2_xboole_0('#skF_3','#skF_2'),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_59108]) ).
tff(c_32,plain,
! [A_21,B_22,C_23] :
( m1_subset_1(k4_subset_1(A_21,B_22,C_23),k1_zfmisc_1(A_21))
| ~ m1_subset_1(C_23,k1_zfmisc_1(A_21))
| ~ m1_subset_1(B_22,k1_zfmisc_1(A_21)) ),
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_59140,plain,
( m1_subset_1(k2_xboole_0('#skF_3','#skF_2'),k1_zfmisc_1(k1_zfmisc_1('#skF_1')))
| ~ m1_subset_1('#skF_3',k1_zfmisc_1(k1_zfmisc_1('#skF_1')))
| ~ m1_subset_1('#skF_2',k1_zfmisc_1(k1_zfmisc_1('#skF_1'))) ),
inference(superposition,[status(thm),theory(equality)],[c_59126,c_32]) ).
tff(c_59144,plain,
m1_subset_1(k2_xboole_0('#skF_3','#skF_2'),k1_zfmisc_1(k1_zfmisc_1('#skF_1'))),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_4,c_59140]) ).
tff(c_16,plain,
! [B_11,A_10] : ( k3_xboole_0(B_11,A_10) = k3_xboole_0(A_10,B_11) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_498,plain,
! [A_136,B_137,C_138] : r1_tarski(k3_xboole_0(A_136,B_137),k2_xboole_0(A_136,C_138)),
inference(cnfTransformation,[status(thm)],[f_194]) ).
tff(c_694,plain,
! [A_154,B_155,B_156] : r1_tarski(k3_xboole_0(A_154,B_155),k2_xboole_0(B_156,A_154)),
inference(superposition,[status(thm),theory(equality)],[c_14,c_498]) ).
tff(c_703,plain,
! [A_10,B_11,B_156] : r1_tarski(k3_xboole_0(A_10,B_11),k2_xboole_0(B_156,B_11)),
inference(superposition,[status(thm),theory(equality)],[c_16,c_694]) ).
tff(c_112,plain,
! [A_78,C_81,B_79] :
( r1_tarski(k8_setfam_1(A_78,C_81),k8_setfam_1(A_78,B_79))
| ~ r1_tarski(B_79,C_81)
| ~ m1_subset_1(C_81,k1_zfmisc_1(k1_zfmisc_1(A_78)))
| ~ m1_subset_1(B_79,k1_zfmisc_1(k1_zfmisc_1(A_78))) ),
inference(cnfTransformation,[status(thm)],[f_221]) ).
tff(c_60378,plain,
! [A_1992,C_1993,D_1994] :
( ( k5_subset_1(A_1992,k8_setfam_1(A_1992,C_1993),k8_setfam_1(A_1992,D_1994)) = k8_setfam_1(A_1992,k4_subset_1(k1_zfmisc_1(A_1992),C_1993,D_1994)) )
| ~ m1_subset_1(D_1994,k1_zfmisc_1(k1_zfmisc_1(A_1992)))
| ~ m1_subset_1(C_1993,k1_zfmisc_1(k1_zfmisc_1(A_1992)))
| ~ m1_subset_1(k4_subset_1(k1_zfmisc_1(A_1992),C_1993,D_1994),k1_zfmisc_1(k1_zfmisc_1(A_1992))) ),
inference(cnfTransformation,[status(thm)],[f_257]) ).
tff(c_77898,plain,
! [A_2420,B_2421,C_2422] :
( ( k5_subset_1(A_2420,k8_setfam_1(A_2420,B_2421),k8_setfam_1(A_2420,C_2422)) = k8_setfam_1(A_2420,k4_subset_1(k1_zfmisc_1(A_2420),B_2421,C_2422)) )
| ~ m1_subset_1(C_2422,k1_zfmisc_1(k1_zfmisc_1(A_2420)))
| ~ m1_subset_1(B_2421,k1_zfmisc_1(k1_zfmisc_1(A_2420))) ),
inference(resolution,[status(thm)],[c_32,c_60378]) ).
tff(c_78629,plain,
! [B_2436] :
( ( k5_subset_1('#skF_1',k8_setfam_1('#skF_1',B_2436),k8_setfam_1('#skF_1','#skF_3')) = k8_setfam_1('#skF_1',k4_subset_1(k1_zfmisc_1('#skF_1'),B_2436,'#skF_3')) )
| ~ m1_subset_1(B_2436,k1_zfmisc_1(k1_zfmisc_1('#skF_1'))) ),
inference(resolution,[status(thm)],[c_4,c_77898]) ).
tff(c_78689,plain,
k5_subset_1('#skF_1',k8_setfam_1('#skF_1','#skF_2'),k8_setfam_1('#skF_1','#skF_3')) = k8_setfam_1('#skF_1',k4_subset_1(k1_zfmisc_1('#skF_1'),'#skF_2','#skF_3')),
inference(resolution,[status(thm)],[c_6,c_78629]) ).
tff(c_78711,plain,
k5_subset_1('#skF_1',k8_setfam_1('#skF_1','#skF_2'),k8_setfam_1('#skF_1','#skF_3')) = k8_setfam_1('#skF_1',k2_xboole_0('#skF_3','#skF_2')),
inference(demodulation,[status(thm),theory(equality)],[c_59126,c_78689]) ).
tff(c_59414,plain,
! [A_1957,B_1958,C_1959] :
( ( k1_relset_2(A_1957,B_1958,C_1959) = k3_xboole_0(B_1958,C_1959) )
| ~ m1_subset_1(C_1959,k1_zfmisc_1(k1_zfmisc_1(A_1957)))
| ~ m1_subset_1(B_1958,k1_zfmisc_1(k1_zfmisc_1(A_1957))) ),
inference(cnfTransformation,[status(thm)],[f_172]) ).
tff(c_59473,plain,
! [B_1961] :
( ( k1_relset_2('#skF_1',B_1961,'#skF_3') = k3_xboole_0(B_1961,'#skF_3') )
| ~ m1_subset_1(B_1961,k1_zfmisc_1(k1_zfmisc_1('#skF_1'))) ),
inference(resolution,[status(thm)],[c_4,c_59414]) ).
tff(c_59513,plain,
k1_relset_2('#skF_1','#skF_2','#skF_3') = k3_xboole_0('#skF_2','#skF_3'),
inference(resolution,[status(thm)],[c_6,c_59473]) ).
tff(c_59535,plain,
k1_relset_2('#skF_1','#skF_2','#skF_3') = k3_xboole_0('#skF_3','#skF_2'),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_59513]) ).
tff(c_2,plain,
~ r1_tarski(k5_subset_1('#skF_1',k8_setfam_1('#skF_1','#skF_2'),k8_setfam_1('#skF_1','#skF_3')),k8_setfam_1('#skF_1',k1_relset_2('#skF_1','#skF_2','#skF_3'))),
inference(cnfTransformation,[status(thm)],[f_37]) ).
tff(c_59540,plain,
~ r1_tarski(k5_subset_1('#skF_1',k8_setfam_1('#skF_1','#skF_2'),k8_setfam_1('#skF_1','#skF_3')),k8_setfam_1('#skF_1',k3_xboole_0('#skF_3','#skF_2'))),
inference(demodulation,[status(thm),theory(equality)],[c_59535,c_2]) ).
tff(c_198132,plain,
~ r1_tarski(k8_setfam_1('#skF_1',k2_xboole_0('#skF_3','#skF_2')),k8_setfam_1('#skF_1',k3_xboole_0('#skF_3','#skF_2'))),
inference(demodulation,[status(thm),theory(equality)],[c_78711,c_59540]) ).
tff(c_198270,plain,
( ~ r1_tarski(k3_xboole_0('#skF_3','#skF_2'),k2_xboole_0('#skF_3','#skF_2'))
| ~ m1_subset_1(k2_xboole_0('#skF_3','#skF_2'),k1_zfmisc_1(k1_zfmisc_1('#skF_1')))
| ~ m1_subset_1(k3_xboole_0('#skF_3','#skF_2'),k1_zfmisc_1(k1_zfmisc_1('#skF_1'))) ),
inference(resolution,[status(thm)],[c_112,c_198132]) ).
tff(c_198275,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_59338,c_59144,c_703,c_198270]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.10 % Problem : SEU417+1 : TPTP v9.0.0. Released v3.4.0.
% 0.09/0.10 % 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.10/0.31 % Computer : n007.cluster.edu
% 0.10/0.31 % Model : x86_64 x86_64
% 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.31 % Memory : 8042.1875MB
% 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.31 % CPULimit : 300
% 0.10/0.31 % WCLimit : 300
% 0.10/0.31 % DateTime : Tue Apr 8 23:16:39 EDT 2025
% 0.10/0.31 % CPUTime :
% 75.41/58.34 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 75.41/58.35
% 75.41/58.35 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------