%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SEU408+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 : n013.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:54 PM UTC 2025
% Result : Theorem 76.79s 58.45s
% Output : CNFRefutation 76.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 5
% Syntax : Number of formulae : 24 ( 8 unt; 0 typ; 0 def)
% Number of atoms : 77 ( 5 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 90 ( 37 ~; 28 |; 14 &)
% ( 3 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 17 ( 15 usr; 1 prp; 0-3 aty)
% Number of functors : 24 ( 24 usr; 9 con; 0-6 aty)
% Number of variables : 31 ( 31 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ m2_relset_1 > m1_relset_1 > r2_hidden > r1_tarski > m1_subset_1 > v4_orders_2 > v3_struct_0 > v3_orders_2 > v2_orders_2 > v1_xboole_0 > v1_relat_1 > v1_orders_2 > v1_lattice3 > l1_struct_0 > l1_orders_2 > k7_relset_1 > k5_relat_1 > k2_zfmisc_1 > k2_xboole_0 > k1_latsum_1 > g1_orders_2 > #nlpp > u1_struct_0 > u1_orders_2 > k1_zfmisc_1 > k1_xboole_0 > #skF_9 > #skF_11 > #skF_4 > #skF_7 > #skF_6 > #skF_13 > #skF_5 > #skF_2 > #skF_10 > #skF_3 > #skF_1 > #skF_8 > #skF_14 > #skF_12
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(v1_orders_2,type,
v1_orders_2: $i > $o ).
tff('#skF_9',type,
'#skF_9': $i > $i ).
tff(m2_relset_1,type,
m2_relset_1: ( $i * $i * $i ) > $o ).
tff(v3_orders_2,type,
v3_orders_2: $i > $o ).
tff(r2_hidden,type,
r2_hidden: ( $i * $i ) > $o ).
tff('#skF_11',type,
'#skF_11': $i ).
tff(k7_relset_1,type,
k7_relset_1: ( $i * $i * $i * $i * $i * $i ) > $i ).
tff(k1_xboole_0,type,
k1_xboole_0: $i ).
tff(k5_relat_1,type,
k5_relat_1: ( $i * $i ) > $i ).
tff('#skF_4',type,
'#skF_4': ( $i * $i * $i ) > $i ).
tff('#skF_7',type,
'#skF_7': $i ).
tff(r1_tarski,type,
r1_tarski: ( $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(v1_lattice3,type,
v1_lattice3: $i > $o ).
tff('#skF_6',type,
'#skF_6': $i ).
tff('#skF_13',type,
'#skF_13': $i ).
tff('#skF_5',type,
'#skF_5': ( $i * $i * $i ) > $i ).
tff('#skF_2',type,
'#skF_2': $i ).
tff(k1_latsum_1,type,
k1_latsum_1: ( $i * $i ) > $i ).
tff('#skF_10',type,
'#skF_10': ( $i * $i ) > $i ).
tff('#skF_3',type,
'#skF_3': $i ).
tff('#skF_1',type,
'#skF_1': $i ).
tff(v4_orders_2,type,
v4_orders_2: $i > $o ).
tff('#skF_8',type,
'#skF_8': ( $i * $i ) > $i ).
tff(k1_zfmisc_1,type,
k1_zfmisc_1: $i > $i ).
tff(v2_orders_2,type,
v2_orders_2: $i > $o ).
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_14',type,
'#skF_14': $i > $i ).
tff(u1_orders_2,type,
u1_orders_2: $i > $i ).
tff(k2_xboole_0,type,
k2_xboole_0: ( $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_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(f_62,negated_conjecture,
~ ! [A] :
( ( ~ v3_struct_0(A)
& v2_orders_2(A)
& v3_orders_2(A)
& v4_orders_2(A)
& v1_lattice3(A)
& l1_orders_2(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& v2_orders_2(B)
& v3_orders_2(B)
& v4_orders_2(B)
& v1_lattice3(B)
& l1_orders_2(B) )
=> ! [C] :
( r2_hidden(C,u1_struct_0(B))
=> m1_subset_1(C,u1_struct_0(k1_latsum_1(A,B))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t11_latsum_1) ).
tff(f_118,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/sandbox/benchmark/theBenchmark.p',dt_k1_latsum_1) ).
tff(f_95,axiom,
! [A] :
( l1_orders_2(A)
=> ! [B] :
( l1_orders_2(B)
=> ! [C] :
( ( v1_orders_2(C)
& l1_orders_2(C) )
=> ( ( C = k1_latsum_1(A,B) )
<=> ( ( u1_struct_0(C) = k2_xboole_0(u1_struct_0(A),u1_struct_0(B)) )
& ( u1_orders_2(C) = k2_xboole_0(k2_xboole_0(u1_orders_2(A),u1_orders_2(B)),k7_relset_1(u1_struct_0(A),u1_struct_0(A),u1_struct_0(B),u1_struct_0(B),u1_orders_2(A),u1_orders_2(B))) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_latsum_1) ).
tff(f_104,axiom,
! [A,B,C] :
( ( C = k2_xboole_0(A,B) )
<=> ! [D] :
( r2_hidden(D,C)
<=> ( r2_hidden(D,A)
| r2_hidden(D,B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_xboole_0) ).
tff(f_251,axiom,
! [A,B] :
( r2_hidden(A,B)
=> m1_subset_1(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_subset) ).
tff(c_18,plain,
l1_orders_2('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_62]) ).
tff(c_6,plain,
l1_orders_2('#skF_2'),
inference(cnfTransformation,[status(thm)],[f_62]) ).
tff(c_66,plain,
! [A_28,B_29] :
( l1_orders_2(k1_latsum_1(A_28,B_29))
| ~ l1_orders_2(B_29)
| ~ l1_orders_2(A_28) ),
inference(cnfTransformation,[status(thm)],[f_118]) ).
tff(c_68,plain,
! [A_28,B_29] :
( v1_orders_2(k1_latsum_1(A_28,B_29))
| ~ l1_orders_2(B_29)
| ~ l1_orders_2(A_28) ),
inference(cnfTransformation,[status(thm)],[f_118]) ).
tff(c_4,plain,
r2_hidden('#skF_3',u1_struct_0('#skF_2')),
inference(cnfTransformation,[status(thm)],[f_62]) ).
tff(c_1497,plain,
! [A_351,B_352] :
( ( k2_xboole_0(u1_struct_0(A_351),u1_struct_0(B_352)) = u1_struct_0(k1_latsum_1(A_351,B_352)) )
| ~ l1_orders_2(k1_latsum_1(A_351,B_352))
| ~ v1_orders_2(k1_latsum_1(A_351,B_352))
| ~ l1_orders_2(B_352)
| ~ l1_orders_2(A_351) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_46,plain,
! [D_25,B_21,A_20] :
( ~ r2_hidden(D_25,B_21)
| r2_hidden(D_25,k2_xboole_0(A_20,B_21)) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_25844,plain,
! [D_1225,B_1226,A_1227] :
( ~ r2_hidden(D_1225,u1_struct_0(B_1226))
| r2_hidden(D_1225,u1_struct_0(k1_latsum_1(A_1227,B_1226)))
| ~ l1_orders_2(k1_latsum_1(A_1227,B_1226))
| ~ v1_orders_2(k1_latsum_1(A_1227,B_1226))
| ~ l1_orders_2(B_1226)
| ~ l1_orders_2(A_1227) ),
inference(superposition,[status(thm),theory(equality)],[c_1497,c_46]) ).
tff(c_150,plain,
! [A_82,B_83] :
( m1_subset_1(A_82,B_83)
| ~ r2_hidden(A_82,B_83) ),
inference(cnfTransformation,[status(thm)],[f_251]) ).
tff(c_227207,plain,
! [D_78813,A_78814,B_78815] :
( m1_subset_1(D_78813,u1_struct_0(k1_latsum_1(A_78814,B_78815)))
| ~ r2_hidden(D_78813,u1_struct_0(B_78815))
| ~ l1_orders_2(k1_latsum_1(A_78814,B_78815))
| ~ v1_orders_2(k1_latsum_1(A_78814,B_78815))
| ~ l1_orders_2(B_78815)
| ~ l1_orders_2(A_78814) ),
inference(resolution,[status(thm)],[c_25844,c_150]) ).
tff(c_2,plain,
~ m1_subset_1('#skF_3',u1_struct_0(k1_latsum_1('#skF_1','#skF_2'))),
inference(cnfTransformation,[status(thm)],[f_62]) ).
tff(c_227323,plain,
( ~ r2_hidden('#skF_3',u1_struct_0('#skF_2'))
| ~ l1_orders_2(k1_latsum_1('#skF_1','#skF_2'))
| ~ v1_orders_2(k1_latsum_1('#skF_1','#skF_2'))
| ~ l1_orders_2('#skF_2')
| ~ l1_orders_2('#skF_1') ),
inference(resolution,[status(thm)],[c_227207,c_2]) ).
tff(c_227373,plain,
( ~ l1_orders_2(k1_latsum_1('#skF_1','#skF_2'))
| ~ v1_orders_2(k1_latsum_1('#skF_1','#skF_2')) ),
inference(demodulation,[status(thm),theory(equality)],[c_18,c_6,c_4,c_227323]) ).
tff(c_227374,plain,
~ v1_orders_2(k1_latsum_1('#skF_1','#skF_2')),
inference(splitLeft,[status(thm)],[c_227373]) ).
tff(c_227377,plain,
( ~ l1_orders_2('#skF_2')
| ~ l1_orders_2('#skF_1') ),
inference(resolution,[status(thm)],[c_68,c_227374]) ).
tff(c_227381,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_18,c_6,c_227377]) ).
tff(c_227382,plain,
~ l1_orders_2(k1_latsum_1('#skF_1','#skF_2')),
inference(splitRight,[status(thm)],[c_227373]) ).
tff(c_227386,plain,
( ~ l1_orders_2('#skF_2')
| ~ l1_orders_2('#skF_1') ),
inference(resolution,[status(thm)],[c_66,c_227382]) ).
tff(c_227390,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_18,c_6,c_227386]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU408+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.13/0.34 % Computer : n013.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 : Tue Apr 8 23:09:47 EDT 2025
% 0.13/0.34 % CPUTime :
% 76.79/58.45 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 76.79/58.46
% 76.79/58.46 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------