%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SEU413+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 : n012.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:56 PM UTC 2025
% Result : Theorem 12.05s 3.89s
% Output : CNFRefutation 12.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 5
% Syntax : Number of formulae : 32 ( 14 unt; 0 typ; 0 def)
% Number of atoms : 104 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 131 ( 59 ~; 50 |; 9 &)
% ( 1 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 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 : 13 ( 12 usr; 1 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 9 con; 0-2 aty)
% Number of variables : 40 ( 40 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ r1_orders_2 > m2_relset_1 > m1_relset_1 > v12_waybel_0 > r2_hidden > r1_tarski > m1_subset_1 > v1_xboole_0 > v1_relat_1 > v1_orders_2 > l1_struct_0 > l1_orders_2 > k4_tarski > k3_xboole_0 > k2_zfmisc_1 > k1_latsum_1 > g1_orders_2 > #nlpp > u1_struct_0 > u1_orders_2 > k1_zfmisc_1 > k1_xboole_0 > #skF_11 > #skF_8 > #skF_10 > #skF_5 > #skF_6 > #skF_2 > #skF_3 > #skF_1 > #skF_4 > #skF_7 > #skF_9
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(v1_orders_2,type,
v1_orders_2: $i > $o ).
tff(m2_relset_1,type,
m2_relset_1: ( $i * $i * $i ) > $o ).
tff(r2_hidden,type,
r2_hidden: ( $i * $i ) > $o ).
tff('#skF_11',type,
'#skF_11': $i ).
tff(k4_tarski,type,
k4_tarski: ( $i * $i ) > $i ).
tff(r1_orders_2,type,
r1_orders_2: ( $i * $i * $i ) > $o ).
tff(k1_xboole_0,type,
k1_xboole_0: $i ).
tff('#skF_8',type,
'#skF_8': $i > $i ).
tff(r1_tarski,type,
r1_tarski: ( $i * $i ) > $o ).
tff('#skF_10',type,
'#skF_10': $i ).
tff(v12_waybel_0,type,
v12_waybel_0: ( $i * $i ) > $o ).
tff(m1_relset_1,type,
m1_relset_1: ( $i * $i * $i ) > $o ).
tff(g1_orders_2,type,
g1_orders_2: ( $i * $i ) > $i ).
tff('#skF_5',type,
'#skF_5': $i ).
tff('#skF_6',type,
'#skF_6': $i ).
tff('#skF_2',type,
'#skF_2': $i ).
tff(k1_latsum_1,type,
k1_latsum_1: ( $i * $i ) > $i ).
tff('#skF_3',type,
'#skF_3': $i ).
tff('#skF_1',type,
'#skF_1': $i ).
tff(k1_zfmisc_1,type,
k1_zfmisc_1: $i > $i ).
tff(l1_struct_0,type,
l1_struct_0: $i > $o ).
tff(l1_orders_2,type,
l1_orders_2: $i > $o ).
tff(v1_relat_1,type,
v1_relat_1: $i > $o ).
tff(k2_zfmisc_1,type,
k2_zfmisc_1: ( $i * $i ) > $i ).
tff('#skF_4',type,
'#skF_4': $i ).
tff(k3_xboole_0,type,
k3_xboole_0: ( $i * $i ) > $i ).
tff(u1_orders_2,type,
u1_orders_2: $i > $i ).
tff('#skF_7',type,
'#skF_7': ( $i * $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(m1_subset_1,type,
m1_subset_1: ( $i * $i ) > $o ).
tff(f_51,negated_conjecture,
~ ! [A] :
( l1_orders_2(A)
=> ! [B] :
( l1_orders_2(B)
=> ! [C] :
( m1_subset_1(C,u1_struct_0(k1_latsum_1(A,B)))
=> ! [D] :
( m1_subset_1(D,u1_struct_0(k1_latsum_1(A,B)))
=> ( ( v12_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)
& m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(B)))
& r1_orders_2(k1_latsum_1(A,B),C,D)
& r2_hidden(D,u1_struct_0(A)) )
=> r2_hidden(C,u1_struct_0(A)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t23_latsum_1) ).
tff(f_94,axiom,
! [A,B] :
( ( l1_orders_2(A)
& l1_orders_2(B) )
=> ( v1_orders_2(k1_latsum_1(A,B))
& l1_orders_2(k1_latsum_1(A,B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_latsum_1) ).
tff(f_80,axiom,
! [A] :
( l1_orders_2(A)
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( r1_orders_2(A,B,C)
<=> r2_hidden(k4_tarski(B,C),u1_orders_2(A)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d9_orders_2) ).
tff(f_197,axiom,
! [A,B] :
~ ( r2_hidden(A,B)
& v1_xboole_0(B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
tff(f_163,axiom,
! [A] :
( l1_orders_2(A)
=> ! [B] :
( l1_orders_2(B)
=> ! [C,D] :
( ( v12_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)
& m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(B)))
& r2_hidden(k4_tarski(C,D),u1_orders_2(k1_latsum_1(A,B)))
& r2_hidden(D,u1_struct_0(A)) )
=> r2_hidden(C,u1_struct_0(A)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t21_latsum_1) ).
tff(c_2,plain,
~ r2_hidden('#skF_3',u1_struct_0('#skF_1')),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_14,plain,
m1_subset_1('#skF_3',u1_struct_0(k1_latsum_1('#skF_1','#skF_2'))),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_12,plain,
m1_subset_1('#skF_4',u1_struct_0(k1_latsum_1('#skF_1','#skF_2'))),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_4,plain,
r2_hidden('#skF_4',u1_struct_0('#skF_1')),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_6,plain,
r1_orders_2(k1_latsum_1('#skF_1','#skF_2'),'#skF_3','#skF_4'),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_18,plain,
l1_orders_2('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_16,plain,
l1_orders_2('#skF_2'),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_36,plain,
! [A_29,B_30] :
( l1_orders_2(k1_latsum_1(A_29,B_30))
| ~ l1_orders_2(B_30)
| ~ l1_orders_2(A_29) ),
inference(cnfTransformation,[status(thm)],[f_94]) ).
tff(c_3357,plain,
! [B_480,C_481,A_482] :
( r2_hidden(k4_tarski(B_480,C_481),u1_orders_2(A_482))
| ~ r1_orders_2(A_482,B_480,C_481)
| ~ m1_subset_1(C_481,u1_struct_0(A_482))
| ~ m1_subset_1(B_480,u1_struct_0(A_482))
| ~ l1_orders_2(A_482) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_110,plain,
! [B_83,A_82] :
( ~ v1_xboole_0(B_83)
| ~ r2_hidden(A_82,B_83) ),
inference(cnfTransformation,[status(thm)],[f_197]) ).
tff(c_10153,plain,
! [A_918,B_919,C_920] :
( ~ v1_xboole_0(u1_orders_2(A_918))
| ~ r1_orders_2(A_918,B_919,C_920)
| ~ m1_subset_1(C_920,u1_struct_0(A_918))
| ~ m1_subset_1(B_919,u1_struct_0(A_918))
| ~ l1_orders_2(A_918) ),
inference(resolution,[status(thm)],[c_3357,c_110]) ).
tff(c_10155,plain,
( ~ v1_xboole_0(u1_orders_2(k1_latsum_1('#skF_1','#skF_2')))
| ~ m1_subset_1('#skF_4',u1_struct_0(k1_latsum_1('#skF_1','#skF_2')))
| ~ m1_subset_1('#skF_3',u1_struct_0(k1_latsum_1('#skF_1','#skF_2')))
| ~ l1_orders_2(k1_latsum_1('#skF_1','#skF_2')) ),
inference(resolution,[status(thm)],[c_6,c_10153]) ).
tff(c_10158,plain,
( ~ v1_xboole_0(u1_orders_2(k1_latsum_1('#skF_1','#skF_2')))
| ~ l1_orders_2(k1_latsum_1('#skF_1','#skF_2')) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_12,c_10155]) ).
tff(c_10159,plain,
~ l1_orders_2(k1_latsum_1('#skF_1','#skF_2')),
inference(splitLeft,[status(thm)],[c_10158]) ).
tff(c_10162,plain,
( ~ l1_orders_2('#skF_2')
| ~ l1_orders_2('#skF_1') ),
inference(resolution,[status(thm)],[c_36,c_10159]) ).
tff(c_10166,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_18,c_16,c_10162]) ).
tff(c_10168,plain,
l1_orders_2(k1_latsum_1('#skF_1','#skF_2')),
inference(splitRight,[status(thm)],[c_10158]) ).
tff(c_10,plain,
v12_waybel_0(k3_xboole_0(u1_struct_0('#skF_1'),u1_struct_0('#skF_2')),'#skF_2'),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_8,plain,
m1_subset_1(k3_xboole_0(u1_struct_0('#skF_1'),u1_struct_0('#skF_2')),k1_zfmisc_1(u1_struct_0('#skF_2'))),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_30,plain,
! [B_24,C_26,A_20] :
( r2_hidden(k4_tarski(B_24,C_26),u1_orders_2(A_20))
| ~ r1_orders_2(A_20,B_24,C_26)
| ~ m1_subset_1(C_26,u1_struct_0(A_20))
| ~ m1_subset_1(B_24,u1_struct_0(A_20))
| ~ l1_orders_2(A_20) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_3621,plain,
! [C_503,A_504,D_505,B_506] :
( r2_hidden(C_503,u1_struct_0(A_504))
| ~ r2_hidden(D_505,u1_struct_0(A_504))
| ~ r2_hidden(k4_tarski(C_503,D_505),u1_orders_2(k1_latsum_1(A_504,B_506)))
| ~ m1_subset_1(k3_xboole_0(u1_struct_0(A_504),u1_struct_0(B_506)),k1_zfmisc_1(u1_struct_0(B_506)))
| ~ v12_waybel_0(k3_xboole_0(u1_struct_0(A_504),u1_struct_0(B_506)),B_506)
| ~ l1_orders_2(B_506)
| ~ l1_orders_2(A_504) ),
inference(cnfTransformation,[status(thm)],[f_163]) ).
tff(c_11171,plain,
! [B_993,A_994,C_995,B_996] :
( r2_hidden(B_993,u1_struct_0(A_994))
| ~ r2_hidden(C_995,u1_struct_0(A_994))
| ~ m1_subset_1(k3_xboole_0(u1_struct_0(A_994),u1_struct_0(B_996)),k1_zfmisc_1(u1_struct_0(B_996)))
| ~ v12_waybel_0(k3_xboole_0(u1_struct_0(A_994),u1_struct_0(B_996)),B_996)
| ~ l1_orders_2(B_996)
| ~ l1_orders_2(A_994)
| ~ r1_orders_2(k1_latsum_1(A_994,B_996),B_993,C_995)
| ~ m1_subset_1(C_995,u1_struct_0(k1_latsum_1(A_994,B_996)))
| ~ m1_subset_1(B_993,u1_struct_0(k1_latsum_1(A_994,B_996)))
| ~ l1_orders_2(k1_latsum_1(A_994,B_996)) ),
inference(resolution,[status(thm)],[c_30,c_3621]) ).
tff(c_11185,plain,
! [B_993,C_995] :
( r2_hidden(B_993,u1_struct_0('#skF_1'))
| ~ r2_hidden(C_995,u1_struct_0('#skF_1'))
| ~ v12_waybel_0(k3_xboole_0(u1_struct_0('#skF_1'),u1_struct_0('#skF_2')),'#skF_2')
| ~ l1_orders_2('#skF_2')
| ~ l1_orders_2('#skF_1')
| ~ r1_orders_2(k1_latsum_1('#skF_1','#skF_2'),B_993,C_995)
| ~ m1_subset_1(C_995,u1_struct_0(k1_latsum_1('#skF_1','#skF_2')))
| ~ m1_subset_1(B_993,u1_struct_0(k1_latsum_1('#skF_1','#skF_2')))
| ~ l1_orders_2(k1_latsum_1('#skF_1','#skF_2')) ),
inference(resolution,[status(thm)],[c_8,c_11171]) ).
tff(c_11227,plain,
! [B_997,C_998] :
( r2_hidden(B_997,u1_struct_0('#skF_1'))
| ~ r2_hidden(C_998,u1_struct_0('#skF_1'))
| ~ r1_orders_2(k1_latsum_1('#skF_1','#skF_2'),B_997,C_998)
| ~ m1_subset_1(C_998,u1_struct_0(k1_latsum_1('#skF_1','#skF_2')))
| ~ m1_subset_1(B_997,u1_struct_0(k1_latsum_1('#skF_1','#skF_2'))) ),
inference(demodulation,[status(thm),theory(equality)],[c_10168,c_18,c_16,c_10,c_11185]) ).
tff(c_11229,plain,
( r2_hidden('#skF_3',u1_struct_0('#skF_1'))
| ~ r2_hidden('#skF_4',u1_struct_0('#skF_1'))
| ~ m1_subset_1('#skF_4',u1_struct_0(k1_latsum_1('#skF_1','#skF_2')))
| ~ m1_subset_1('#skF_3',u1_struct_0(k1_latsum_1('#skF_1','#skF_2'))) ),
inference(resolution,[status(thm)],[c_6,c_11227]) ).
tff(c_11232,plain,
r2_hidden('#skF_3',u1_struct_0('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_12,c_4,c_11229]) ).
tff(c_11234,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2,c_11232]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : SEU413+1 : TPTP v9.0.0. Released v3.4.0.
% 0.06/0.12 % 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.12/0.33 % Computer : n012.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Tue Apr 8 23:12:59 EDT 2025
% 0.12/0.33 % CPUTime :
% 12.05/3.89 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.08/3.89
% 12.08/3.89 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------