%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP620+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 : n004.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 06:26:40 PM UTC 2025
% Result : Theorem 15.70s 5.28s
% Output : CNFRefutation 16.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 13
% Syntax : Number of formulae : 107 ( 41 unt; 0 typ; 0 def)
% Number of atoms : 385 ( 2 equ)
% Maximal formula atoms : 19 ( 3 avg)
% Number of connectives : 459 ( 181 ~; 197 |; 53 &)
% ( 4 <=>; 24 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 5 avg)
% Maximal term depth : 2 ( 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-4 aty)
% Number of functors : 34 ( 34 usr; 16 con; 0-3 aty)
% Number of variables : 79 ( 79 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ m2_fraenkel > v4_group_6 > v3_group_6 > v2_group_6 > v1_partfun1 > v1_group_6 > v1_funct_2 > m2_relset_1 > m1_relset_1 > m1_fraenkel > r2_hidden > r1_tarski > m1_subset_1 > v4_group_1 > v3_struct_0 > v3_group_1 > v2_group_1 > v2_funct_1 > v1_xboole_0 > v1_relat_1 > v1_group_1 > v1_funct_1 > v1_fraenkel > l1_struct_0 > l1_group_1 > k2_zfmisc_1 > g1_group_1 > #nlpp > u1_struct_0 > u1_group_1 > k2_funct_1 > k1_zfmisc_1 > k1_autgroup > k1_xboole_0 > #skF_9 > #skF_11 > #skF_18 > #skF_17 > #skF_15 > #skF_25 > #skF_20 > #skF_19 > #skF_3 > #skF_16 > #skF_14 > #skF_5 > #skF_6 > #skF_13 > #skF_2 > #skF_1 > #skF_8 > #skF_26 > #skF_22 > #skF_24 > #skF_23 > #skF_7 > #skF_21 > #skF_12 > #skF_4 > #skF_10
%Foreground sorts:
%Background operators:
%Foreground operators:
tff('#skF_9',type,
'#skF_9': $i > $i ).
tff(v2_group_1,type,
v2_group_1: $i > $o ).
tff('#skF_11',type,
'#skF_11': ( $i * $i ) > $i ).
tff(m2_relset_1,type,
m2_relset_1: ( $i * $i * $i ) > $o ).
tff(v3_group_1,type,
v3_group_1: $i > $o ).
tff(u1_group_1,type,
u1_group_1: $i > $i ).
tff(v1_funct_1,type,
v1_funct_1: $i > $o ).
tff(k2_funct_1,type,
k2_funct_1: $i > $i ).
tff(v2_funct_1,type,
v2_funct_1: $i > $o ).
tff(k1_autgroup,type,
k1_autgroup: $i > $i ).
tff('#skF_18',type,
'#skF_18': $i ).
tff('#skF_17',type,
'#skF_17': $i ).
tff(r2_hidden,type,
r2_hidden: ( $i * $i ) > $o ).
tff('#skF_15',type,
'#skF_15': $i ).
tff(v1_partfun1,type,
v1_partfun1: ( $i * $i * $i ) > $o ).
tff('#skF_25',type,
'#skF_25': $i ).
tff(k1_xboole_0,type,
k1_xboole_0: $i ).
tff('#skF_20',type,
'#skF_20': ( $i * $i ) > $i ).
tff('#skF_19',type,
'#skF_19': $i ).
tff('#skF_3',type,
'#skF_3': ( $i * $i ) > $i ).
tff(r1_tarski,type,
r1_tarski: ( $i * $i ) > $o ).
tff(m1_relset_1,type,
m1_relset_1: ( $i * $i * $i ) > $o ).
tff(m1_fraenkel,type,
m1_fraenkel: ( $i * $i * $i ) > $o ).
tff('#skF_16',type,
'#skF_16': $i ).
tff(v1_group_6,type,
v1_group_6: ( $i * $i * $i ) > $o ).
tff('#skF_14',type,
'#skF_14': ( $i * $i ) > $i ).
tff(v3_group_6,type,
v3_group_6: ( $i * $i * $i ) > $o ).
tff('#skF_5',type,
'#skF_5': $i ).
tff(v1_funct_2,type,
v1_funct_2: ( $i * $i * $i ) > $o ).
tff(v4_group_6,type,
v4_group_6: ( $i * $i * $i ) > $o ).
tff('#skF_6',type,
'#skF_6': $i ).
tff('#skF_13',type,
'#skF_13': $i ).
tff(v1_group_1,type,
v1_group_1: $i > $o ).
tff('#skF_2',type,
'#skF_2': $i ).
tff('#skF_1',type,
'#skF_1': $i ).
tff('#skF_8',type,
'#skF_8': ( $i * $i ) > $i ).
tff(k1_zfmisc_1,type,
k1_zfmisc_1: $i > $i ).
tff(l1_struct_0,type,
l1_struct_0: $i > $o ).
tff('#skF_26',type,
'#skF_26': $i > $i ).
tff(v1_relat_1,type,
v1_relat_1: $i > $o ).
tff(k2_zfmisc_1,type,
k2_zfmisc_1: ( $i * $i ) > $i ).
tff('#skF_22',type,
'#skF_22': $i ).
tff(m2_fraenkel,type,
m2_fraenkel: ( $i * $i * $i * $i ) > $o ).
tff('#skF_24',type,
'#skF_24': $i ).
tff('#skF_23',type,
'#skF_23': $i ).
tff(v4_group_1,type,
v4_group_1: $i > $o ).
tff(v1_fraenkel,type,
v1_fraenkel: $i > $o ).
tff(g1_group_1,type,
g1_group_1: ( $i * $i ) > $i ).
tff('#skF_7',type,
'#skF_7': ( $i * $i ) > $i ).
tff(u1_struct_0,type,
u1_struct_0: $i > $i ).
tff('#skF_21',type,
'#skF_21': ( $i * $i ) > $i ).
tff(v1_xboole_0,type,
v1_xboole_0: $i > $o ).
tff(v2_group_6,type,
v2_group_6: ( $i * $i * $i ) > $o ).
tff(l1_group_1,type,
l1_group_1: $i > $o ).
tff('#skF_12',type,
'#skF_12': $i ).
tff('#skF_4',type,
'#skF_4': ( $i * $i ) > $i ).
tff('#skF_10',type,
'#skF_10': ( $i * $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_46,negated_conjecture,
~ ! [A] :
( ( ~ v3_struct_0(A)
& v1_group_1(A)
& v3_group_1(A)
& v4_group_1(A)
& l1_group_1(A) )
=> ! [B] :
( m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k1_autgroup(A))
=> m2_fraenkel(k2_funct_1(B),u1_struct_0(A),u1_struct_0(A),k1_autgroup(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_autgroup) ).
tff(f_290,axiom,
! [A] :
( l1_group_1(A)
=> l1_struct_0(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_group_1) ).
tff(f_277,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v1_group_1(A)
& v3_group_1(A)
& v4_group_1(A)
& l1_group_1(A) )
=> m1_fraenkel(k1_autgroup(A),u1_struct_0(A),u1_struct_0(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_autgroup) ).
tff(f_311,axiom,
! [A,B,C] :
( ( ~ v1_xboole_0(B)
& m1_fraenkel(C,A,B) )
=> ! [D] :
( m2_fraenkel(D,A,B,C)
=> ( v1_funct_1(D)
& v1_funct_2(D,A,B)
& m2_relset_1(D,A,B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_fraenkel) ).
tff(f_517,axiom,
! [A,B,C] :
( ( ~ v1_xboole_0(B)
& m1_fraenkel(C,A,B) )
=> ! [D] :
( m2_fraenkel(D,A,B,C)
<=> m1_subset_1(D,C) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_fraenkel) ).
tff(f_369,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& l1_struct_0(A) )
=> ~ v1_xboole_0(u1_struct_0(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).
tff(f_596,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v1_group_1(A)
& v3_group_1(A)
& v4_group_1(A)
& l1_group_1(A) )
=> ! [B] :
( m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k1_autgroup(A))
=> ( v1_funct_1(k2_funct_1(B))
& v1_funct_2(k2_funct_1(B),u1_struct_0(A),u1_struct_0(A))
& v1_group_6(k2_funct_1(B),A,A)
& m2_relset_1(k2_funct_1(B),u1_struct_0(A),u1_struct_0(A)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_autgroup) ).
tff(f_567,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v1_group_1(A)
& v3_group_1(A)
& v4_group_1(A)
& l1_group_1(A) )
=> ! [B] :
( ( v1_funct_1(B)
& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
& v1_group_6(B,A,A)
& m2_relset_1(B,u1_struct_0(A),u1_struct_0(A)) )
=> ( r2_hidden(B,k1_autgroup(A))
<=> v4_group_6(B,A,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_autgroup) ).
tff(f_254,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v1_group_1(A)
& v3_group_1(A)
& v4_group_1(A)
& l1_group_1(A) )
=> ! [B] :
( m1_fraenkel(B,u1_struct_0(A),u1_struct_0(A))
=> ( ( B = k1_autgroup(A) )
<=> ( ! [C] :
( m2_fraenkel(C,u1_struct_0(A),u1_struct_0(A),B)
=> ( v1_funct_1(C)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(A))
& v1_group_6(C,A,A)
& m2_relset_1(C,u1_struct_0(A),u1_struct_0(A)) ) )
& ! [C] :
( ( v1_funct_1(C)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(A))
& v1_group_6(C,A,A)
& m2_relset_1(C,u1_struct_0(A),u1_struct_0(A)) )
=> ( r2_hidden(C,B)
<=> ( v2_funct_1(C)
& v3_group_6(C,A,A) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_autgroup) ).
tff(f_297,axiom,
! [A,B,C] :
( m1_fraenkel(C,A,B)
=> ( ~ v1_xboole_0(C)
& v1_fraenkel(C) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_fraenkel) ).
tff(f_533,axiom,
! [A,B] :
( m1_subset_1(A,B)
=> ( v1_xboole_0(B)
| r2_hidden(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
tff(f_643,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v3_group_1(A)
& v4_group_1(A)
& l1_group_1(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& v3_group_1(B)
& v4_group_1(B)
& l1_group_1(B) )
=> ! [C] :
( ( v1_funct_1(C)
& v1_funct_2(C,u1_struct_0(B),u1_struct_0(A))
& v1_group_6(C,B,A)
& m2_relset_1(C,u1_struct_0(B),u1_struct_0(A)) )
=> ! [D] :
( ( v1_funct_1(D)
& v1_funct_2(D,u1_struct_0(A),u1_struct_0(B))
& v1_group_6(D,A,B)
& m2_relset_1(D,u1_struct_0(A),u1_struct_0(B)) )
=> ( ( v4_group_6(C,B,A)
& ( D = k2_funct_1(C) ) )
=> v4_group_6(D,A,B) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t73_group_6) ).
tff(f_527,axiom,
! [A,B] :
( r2_hidden(A,B)
=> m1_subset_1(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
tff(c_6,plain,
l1_group_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_46]) ).
tff(c_136,plain,
! [A_60] :
( l1_struct_0(A_60)
| ~ l1_group_1(A_60) ),
inference(cnfTransformation,[status(thm)],[f_290]) ).
tff(c_14,plain,
~ v3_struct_0('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_46]) ).
tff(c_12,plain,
v1_group_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_46]) ).
tff(c_10,plain,
v3_group_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_46]) ).
tff(c_8,plain,
v4_group_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_46]) ).
tff(c_1238,plain,
! [A_384] :
( m1_fraenkel(k1_autgroup(A_384),u1_struct_0(A_384),u1_struct_0(A_384))
| ~ l1_group_1(A_384)
| ~ v4_group_1(A_384)
| ~ v3_group_1(A_384)
| ~ v1_group_1(A_384)
| v3_struct_0(A_384) ),
inference(cnfTransformation,[status(thm)],[f_277]) ).
tff(c_4,plain,
m2_fraenkel('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'),k1_autgroup('#skF_1')),
inference(cnfTransformation,[status(thm)],[f_46]) ).
tff(c_722,plain,
! [D_303,A_304,B_305,C_306] :
( v1_funct_1(D_303)
| ~ m2_fraenkel(D_303,A_304,B_305,C_306)
| ~ m1_fraenkel(C_306,A_304,B_305)
| v1_xboole_0(B_305) ),
inference(cnfTransformation,[status(thm)],[f_311]) ).
tff(c_726,plain,
( v1_funct_1('#skF_2')
| ~ m1_fraenkel(k1_autgroup('#skF_1'),u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| v1_xboole_0(u1_struct_0('#skF_1')) ),
inference(resolution,[status(thm)],[c_4,c_722]) ).
tff(c_787,plain,
~ m1_fraenkel(k1_autgroup('#skF_1'),u1_struct_0('#skF_1'),u1_struct_0('#skF_1')),
inference(splitLeft,[status(thm)],[c_726]) ).
tff(c_1243,plain,
( ~ l1_group_1('#skF_1')
| ~ v4_group_1('#skF_1')
| ~ v3_group_1('#skF_1')
| ~ v1_group_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_1238,c_787]) ).
tff(c_1253,plain,
v3_struct_0('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_10,c_8,c_6,c_1243]) ).
tff(c_1255,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_1253]) ).
tff(c_1257,plain,
m1_fraenkel(k1_autgroup('#skF_1'),u1_struct_0('#skF_1'),u1_struct_0('#skF_1')),
inference(splitRight,[status(thm)],[c_726]) ).
tff(c_1449,plain,
! [D_399,C_400,A_401,B_402] :
( m1_subset_1(D_399,C_400)
| ~ m2_fraenkel(D_399,A_401,B_402,C_400)
| ~ m1_fraenkel(C_400,A_401,B_402)
| v1_xboole_0(B_402) ),
inference(cnfTransformation,[status(thm)],[f_517]) ).
tff(c_1455,plain,
( m1_subset_1('#skF_2',k1_autgroup('#skF_1'))
| ~ m1_fraenkel(k1_autgroup('#skF_1'),u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| v1_xboole_0(u1_struct_0('#skF_1')) ),
inference(resolution,[status(thm)],[c_4,c_1449]) ).
tff(c_1459,plain,
( m1_subset_1('#skF_2',k1_autgroup('#skF_1'))
| v1_xboole_0(u1_struct_0('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_1257,c_1455]) ).
tff(c_1461,plain,
v1_xboole_0(u1_struct_0('#skF_1')),
inference(splitLeft,[status(thm)],[c_1459]) ).
tff(c_182,plain,
! [A_90] :
( ~ v1_xboole_0(u1_struct_0(A_90))
| ~ l1_struct_0(A_90)
| v3_struct_0(A_90) ),
inference(cnfTransformation,[status(thm)],[f_369]) ).
tff(c_1466,plain,
( ~ l1_struct_0('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_1461,c_182]) ).
tff(c_1478,plain,
~ l1_struct_0('#skF_1'),
inference(negUnitSimplification,[status(thm)],[c_14,c_1466]) ).
tff(c_1484,plain,
~ l1_group_1('#skF_1'),
inference(resolution,[status(thm)],[c_136,c_1478]) ).
tff(c_1488,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_6,c_1484]) ).
tff(c_1490,plain,
~ v1_xboole_0(u1_struct_0('#skF_1')),
inference(splitRight,[status(thm)],[c_1459]) ).
tff(c_1509,plain,
! [D_405,A_406,B_407,C_408] :
( m2_fraenkel(D_405,A_406,B_407,C_408)
| ~ m1_subset_1(D_405,C_408)
| ~ m1_fraenkel(C_408,A_406,B_407)
| v1_xboole_0(B_407) ),
inference(cnfTransformation,[status(thm)],[f_517]) ).
tff(c_2,plain,
~ m2_fraenkel(k2_funct_1('#skF_2'),u1_struct_0('#skF_1'),u1_struct_0('#skF_1'),k1_autgroup('#skF_1')),
inference(cnfTransformation,[status(thm)],[f_46]) ).
tff(c_1518,plain,
( ~ m1_subset_1(k2_funct_1('#skF_2'),k1_autgroup('#skF_1'))
| ~ m1_fraenkel(k1_autgroup('#skF_1'),u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| v1_xboole_0(u1_struct_0('#skF_1')) ),
inference(resolution,[status(thm)],[c_1509,c_2]) ).
tff(c_1523,plain,
( ~ m1_subset_1(k2_funct_1('#skF_2'),k1_autgroup('#skF_1'))
| v1_xboole_0(u1_struct_0('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_1257,c_1518]) ).
tff(c_1524,plain,
~ m1_subset_1(k2_funct_1('#skF_2'),k1_autgroup('#skF_1')),
inference(negUnitSimplification,[status(thm)],[c_1490,c_1523]) ).
tff(c_2095,plain,
! [B_518,A_519] :
( v1_funct_1(k2_funct_1(B_518))
| ~ m2_fraenkel(B_518,u1_struct_0(A_519),u1_struct_0(A_519),k1_autgroup(A_519))
| ~ l1_group_1(A_519)
| ~ v4_group_1(A_519)
| ~ v3_group_1(A_519)
| ~ v1_group_1(A_519)
| v3_struct_0(A_519) ),
inference(cnfTransformation,[status(thm)],[f_596]) ).
tff(c_2106,plain,
( v1_funct_1(k2_funct_1('#skF_2'))
| ~ l1_group_1('#skF_1')
| ~ v4_group_1('#skF_1')
| ~ v3_group_1('#skF_1')
| ~ v1_group_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_4,c_2095]) ).
tff(c_2111,plain,
( v1_funct_1(k2_funct_1('#skF_2'))
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_10,c_8,c_6,c_2106]) ).
tff(c_2112,plain,
v1_funct_1(k2_funct_1('#skF_2')),
inference(negUnitSimplification,[status(thm)],[c_14,c_2111]) ).
tff(c_2336,plain,
! [B_554,A_555] :
( v1_group_6(k2_funct_1(B_554),A_555,A_555)
| ~ m2_fraenkel(B_554,u1_struct_0(A_555),u1_struct_0(A_555),k1_autgroup(A_555))
| ~ l1_group_1(A_555)
| ~ v4_group_1(A_555)
| ~ v3_group_1(A_555)
| ~ v1_group_1(A_555)
| v3_struct_0(A_555) ),
inference(cnfTransformation,[status(thm)],[f_596]) ).
tff(c_2347,plain,
( v1_group_6(k2_funct_1('#skF_2'),'#skF_1','#skF_1')
| ~ l1_group_1('#skF_1')
| ~ v4_group_1('#skF_1')
| ~ v3_group_1('#skF_1')
| ~ v1_group_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_4,c_2336]) ).
tff(c_2352,plain,
( v1_group_6(k2_funct_1('#skF_2'),'#skF_1','#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_10,c_8,c_6,c_2347]) ).
tff(c_2353,plain,
v1_group_6(k2_funct_1('#skF_2'),'#skF_1','#skF_1'),
inference(negUnitSimplification,[status(thm)],[c_14,c_2352]) ).
tff(c_2801,plain,
! [B_595,A_596] :
( m2_relset_1(k2_funct_1(B_595),u1_struct_0(A_596),u1_struct_0(A_596))
| ~ m2_fraenkel(B_595,u1_struct_0(A_596),u1_struct_0(A_596),k1_autgroup(A_596))
| ~ l1_group_1(A_596)
| ~ v4_group_1(A_596)
| ~ v3_group_1(A_596)
| ~ v1_group_1(A_596)
| v3_struct_0(A_596) ),
inference(cnfTransformation,[status(thm)],[f_596]) ).
tff(c_2812,plain,
( m2_relset_1(k2_funct_1('#skF_2'),u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ l1_group_1('#skF_1')
| ~ v4_group_1('#skF_1')
| ~ v3_group_1('#skF_1')
| ~ v1_group_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_4,c_2801]) ).
tff(c_2817,plain,
( m2_relset_1(k2_funct_1('#skF_2'),u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_10,c_8,c_6,c_2812]) ).
tff(c_2818,plain,
m2_relset_1(k2_funct_1('#skF_2'),u1_struct_0('#skF_1'),u1_struct_0('#skF_1')),
inference(negUnitSimplification,[status(thm)],[c_14,c_2817]) ).
tff(c_2938,plain,
! [B_601,A_602] :
( v1_funct_2(k2_funct_1(B_601),u1_struct_0(A_602),u1_struct_0(A_602))
| ~ m2_fraenkel(B_601,u1_struct_0(A_602),u1_struct_0(A_602),k1_autgroup(A_602))
| ~ l1_group_1(A_602)
| ~ v4_group_1(A_602)
| ~ v3_group_1(A_602)
| ~ v1_group_1(A_602)
| v3_struct_0(A_602) ),
inference(cnfTransformation,[status(thm)],[f_596]) ).
tff(c_2949,plain,
( v1_funct_2(k2_funct_1('#skF_2'),u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ l1_group_1('#skF_1')
| ~ v4_group_1('#skF_1')
| ~ v3_group_1('#skF_1')
| ~ v1_group_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_4,c_2938]) ).
tff(c_2954,plain,
( v1_funct_2(k2_funct_1('#skF_2'),u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_10,c_8,c_6,c_2949]) ).
tff(c_2955,plain,
v1_funct_2(k2_funct_1('#skF_2'),u1_struct_0('#skF_1'),u1_struct_0('#skF_1')),
inference(negUnitSimplification,[status(thm)],[c_14,c_2954]) ).
tff(c_4092,plain,
! [B_666,A_667] :
( r2_hidden(B_666,k1_autgroup(A_667))
| ~ v4_group_6(B_666,A_667,A_667)
| ~ m2_relset_1(B_666,u1_struct_0(A_667),u1_struct_0(A_667))
| ~ v1_group_6(B_666,A_667,A_667)
| ~ v1_funct_2(B_666,u1_struct_0(A_667),u1_struct_0(A_667))
| ~ v1_funct_1(B_666)
| ~ l1_group_1(A_667)
| ~ v4_group_1(A_667)
| ~ v3_group_1(A_667)
| ~ v1_group_1(A_667)
| v3_struct_0(A_667) ),
inference(cnfTransformation,[status(thm)],[f_567]) ).
tff(c_4103,plain,
( r2_hidden(k2_funct_1('#skF_2'),k1_autgroup('#skF_1'))
| ~ v4_group_6(k2_funct_1('#skF_2'),'#skF_1','#skF_1')
| ~ m2_relset_1(k2_funct_1('#skF_2'),u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ v1_group_6(k2_funct_1('#skF_2'),'#skF_1','#skF_1')
| ~ v1_funct_1(k2_funct_1('#skF_2'))
| ~ l1_group_1('#skF_1')
| ~ v4_group_1('#skF_1')
| ~ v3_group_1('#skF_1')
| ~ v1_group_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_2955,c_4092]) ).
tff(c_4131,plain,
( r2_hidden(k2_funct_1('#skF_2'),k1_autgroup('#skF_1'))
| ~ v4_group_6(k2_funct_1('#skF_2'),'#skF_1','#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_10,c_8,c_6,c_2112,c_2353,c_2818,c_4103]) ).
tff(c_4132,plain,
( r2_hidden(k2_funct_1('#skF_2'),k1_autgroup('#skF_1'))
| ~ v4_group_6(k2_funct_1('#skF_2'),'#skF_1','#skF_1') ),
inference(negUnitSimplification,[status(thm)],[c_14,c_4131]) ).
tff(c_4376,plain,
~ v4_group_6(k2_funct_1('#skF_2'),'#skF_1','#skF_1'),
inference(splitLeft,[status(thm)],[c_4132]) ).
tff(c_1256,plain,
( v1_xboole_0(u1_struct_0('#skF_1'))
| v1_funct_1('#skF_2') ),
inference(splitRight,[status(thm)],[c_726]) ).
tff(c_1258,plain,
v1_funct_1('#skF_2'),
inference(splitLeft,[status(thm)],[c_1256]) ).
tff(c_1592,plain,
! [D_418,A_419,B_420,C_421] :
( v1_funct_2(D_418,A_419,B_420)
| ~ m2_fraenkel(D_418,A_419,B_420,C_421)
| ~ m1_fraenkel(C_421,A_419,B_420)
| v1_xboole_0(B_420) ),
inference(cnfTransformation,[status(thm)],[f_311]) ).
tff(c_1601,plain,
( v1_funct_2('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ m1_fraenkel(k1_autgroup('#skF_1'),u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| v1_xboole_0(u1_struct_0('#skF_1')) ),
inference(resolution,[status(thm)],[c_4,c_1592]) ).
tff(c_1606,plain,
( v1_funct_2('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| v1_xboole_0(u1_struct_0('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_1257,c_1601]) ).
tff(c_1607,plain,
v1_funct_2('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1')),
inference(negUnitSimplification,[status(thm)],[c_1490,c_1606]) ).
tff(c_3276,plain,
! [C_613,A_614] :
( v1_group_6(C_613,A_614,A_614)
| ~ m2_fraenkel(C_613,u1_struct_0(A_614),u1_struct_0(A_614),k1_autgroup(A_614))
| ~ m1_fraenkel(k1_autgroup(A_614),u1_struct_0(A_614),u1_struct_0(A_614))
| ~ l1_group_1(A_614)
| ~ v4_group_1(A_614)
| ~ v3_group_1(A_614)
| ~ v1_group_1(A_614)
| v3_struct_0(A_614) ),
inference(cnfTransformation,[status(thm)],[f_254]) ).
tff(c_3287,plain,
( v1_group_6('#skF_2','#skF_1','#skF_1')
| ~ m1_fraenkel(k1_autgroup('#skF_1'),u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ l1_group_1('#skF_1')
| ~ v4_group_1('#skF_1')
| ~ v3_group_1('#skF_1')
| ~ v1_group_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_4,c_3276]) ).
tff(c_3292,plain,
( v1_group_6('#skF_2','#skF_1','#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_10,c_8,c_6,c_1257,c_3287]) ).
tff(c_3293,plain,
v1_group_6('#skF_2','#skF_1','#skF_1'),
inference(negUnitSimplification,[status(thm)],[c_14,c_3292]) ).
tff(c_1561,plain,
! [D_411,A_412,B_413,C_414] :
( m2_relset_1(D_411,A_412,B_413)
| ~ m2_fraenkel(D_411,A_412,B_413,C_414)
| ~ m1_fraenkel(C_414,A_412,B_413)
| v1_xboole_0(B_413) ),
inference(cnfTransformation,[status(thm)],[f_311]) ).
tff(c_1570,plain,
( m2_relset_1('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ m1_fraenkel(k1_autgroup('#skF_1'),u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| v1_xboole_0(u1_struct_0('#skF_1')) ),
inference(resolution,[status(thm)],[c_4,c_1561]) ).
tff(c_1575,plain,
( m2_relset_1('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| v1_xboole_0(u1_struct_0('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_1257,c_1570]) ).
tff(c_1576,plain,
m2_relset_1('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1')),
inference(negUnitSimplification,[status(thm)],[c_1490,c_1575]) ).
tff(c_142,plain,
! [C_63,A_61,B_62] :
( ~ v1_xboole_0(C_63)
| ~ m1_fraenkel(C_63,A_61,B_62) ),
inference(cnfTransformation,[status(thm)],[f_297]) ).
tff(c_1297,plain,
~ v1_xboole_0(k1_autgroup('#skF_1')),
inference(resolution,[status(thm)],[c_1257,c_142]) ).
tff(c_1489,plain,
m1_subset_1('#skF_2',k1_autgroup('#skF_1')),
inference(splitRight,[status(thm)],[c_1459]) ).
tff(c_292,plain,
! [A_120,B_121] :
( r2_hidden(A_120,B_121)
| v1_xboole_0(B_121)
| ~ m1_subset_1(A_120,B_121) ),
inference(cnfTransformation,[status(thm)],[f_533]) ).
tff(c_4118,plain,
( r2_hidden('#skF_2',k1_autgroup('#skF_1'))
| ~ v4_group_6('#skF_2','#skF_1','#skF_1')
| ~ m2_relset_1('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ v1_group_6('#skF_2','#skF_1','#skF_1')
| ~ v1_funct_1('#skF_2')
| ~ l1_group_1('#skF_1')
| ~ v4_group_1('#skF_1')
| ~ v3_group_1('#skF_1')
| ~ v1_group_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_1607,c_4092]) ).
tff(c_4138,plain,
( r2_hidden('#skF_2',k1_autgroup('#skF_1'))
| ~ v4_group_6('#skF_2','#skF_1','#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_10,c_8,c_6,c_1258,c_3293,c_1576,c_4118]) ).
tff(c_4139,plain,
( r2_hidden('#skF_2',k1_autgroup('#skF_1'))
| ~ v4_group_6('#skF_2','#skF_1','#skF_1') ),
inference(negUnitSimplification,[status(thm)],[c_14,c_4138]) ).
tff(c_4185,plain,
~ v4_group_6('#skF_2','#skF_1','#skF_1'),
inference(splitLeft,[status(thm)],[c_4139]) ).
tff(c_4278,plain,
! [B_676,A_677] :
( v4_group_6(B_676,A_677,A_677)
| ~ r2_hidden(B_676,k1_autgroup(A_677))
| ~ m2_relset_1(B_676,u1_struct_0(A_677),u1_struct_0(A_677))
| ~ v1_group_6(B_676,A_677,A_677)
| ~ v1_funct_2(B_676,u1_struct_0(A_677),u1_struct_0(A_677))
| ~ v1_funct_1(B_676)
| ~ l1_group_1(A_677)
| ~ v4_group_1(A_677)
| ~ v3_group_1(A_677)
| ~ v1_group_1(A_677)
| v3_struct_0(A_677) ),
inference(cnfTransformation,[status(thm)],[f_567]) ).
tff(c_4308,plain,
( v4_group_6('#skF_2','#skF_1','#skF_1')
| ~ r2_hidden('#skF_2',k1_autgroup('#skF_1'))
| ~ m2_relset_1('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ v1_group_6('#skF_2','#skF_1','#skF_1')
| ~ v1_funct_1('#skF_2')
| ~ l1_group_1('#skF_1')
| ~ v4_group_1('#skF_1')
| ~ v3_group_1('#skF_1')
| ~ v1_group_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_1607,c_4278]) ).
tff(c_4331,plain,
( v4_group_6('#skF_2','#skF_1','#skF_1')
| ~ r2_hidden('#skF_2',k1_autgroup('#skF_1'))
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_10,c_8,c_6,c_1258,c_3293,c_1576,c_4308]) ).
tff(c_4332,plain,
~ r2_hidden('#skF_2',k1_autgroup('#skF_1')),
inference(negUnitSimplification,[status(thm)],[c_14,c_4185,c_4331]) ).
tff(c_4338,plain,
( v1_xboole_0(k1_autgroup('#skF_1'))
| ~ m1_subset_1('#skF_2',k1_autgroup('#skF_1')) ),
inference(resolution,[status(thm)],[c_292,c_4332]) ).
tff(c_4341,plain,
v1_xboole_0(k1_autgroup('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_1489,c_4338]) ).
tff(c_4343,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1297,c_4341]) ).
tff(c_4345,plain,
v4_group_6('#skF_2','#skF_1','#skF_1'),
inference(splitRight,[status(thm)],[c_4139]) ).
tff(c_8750,plain,
! [C_990,A_991,B_992] :
( v4_group_6(k2_funct_1(C_990),A_991,B_992)
| ~ v4_group_6(C_990,B_992,A_991)
| ~ m2_relset_1(k2_funct_1(C_990),u1_struct_0(A_991),u1_struct_0(B_992))
| ~ v1_group_6(k2_funct_1(C_990),A_991,B_992)
| ~ v1_funct_2(k2_funct_1(C_990),u1_struct_0(A_991),u1_struct_0(B_992))
| ~ v1_funct_1(k2_funct_1(C_990))
| ~ m2_relset_1(C_990,u1_struct_0(B_992),u1_struct_0(A_991))
| ~ v1_group_6(C_990,B_992,A_991)
| ~ v1_funct_2(C_990,u1_struct_0(B_992),u1_struct_0(A_991))
| ~ v1_funct_1(C_990)
| ~ l1_group_1(B_992)
| ~ v4_group_1(B_992)
| ~ v3_group_1(B_992)
| v3_struct_0(B_992)
| ~ l1_group_1(A_991)
| ~ v4_group_1(A_991)
| ~ v3_group_1(A_991)
| v3_struct_0(A_991) ),
inference(cnfTransformation,[status(thm)],[f_643]) ).
tff(c_8760,plain,
( v4_group_6(k2_funct_1('#skF_2'),'#skF_1','#skF_1')
| ~ v4_group_6('#skF_2','#skF_1','#skF_1')
| ~ m2_relset_1(k2_funct_1('#skF_2'),u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ v1_group_6(k2_funct_1('#skF_2'),'#skF_1','#skF_1')
| ~ v1_funct_1(k2_funct_1('#skF_2'))
| ~ m2_relset_1('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ v1_group_6('#skF_2','#skF_1','#skF_1')
| ~ v1_funct_2('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ v1_funct_1('#skF_2')
| ~ l1_group_1('#skF_1')
| ~ v4_group_1('#skF_1')
| ~ v3_group_1('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_2955,c_8750]) ).
tff(c_8767,plain,
( v4_group_6(k2_funct_1('#skF_2'),'#skF_1','#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_8,c_6,c_1258,c_1607,c_3293,c_1576,c_2112,c_2353,c_2818,c_4345,c_8760]) ).
tff(c_8769,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_4376,c_8767]) ).
tff(c_8770,plain,
r2_hidden(k2_funct_1('#skF_2'),k1_autgroup('#skF_1')),
inference(splitRight,[status(thm)],[c_4132]) ).
tff(c_290,plain,
! [A_118,B_119] :
( m1_subset_1(A_118,B_119)
| ~ r2_hidden(A_118,B_119) ),
inference(cnfTransformation,[status(thm)],[f_527]) ).
tff(c_8791,plain,
m1_subset_1(k2_funct_1('#skF_2'),k1_autgroup('#skF_1')),
inference(resolution,[status(thm)],[c_8770,c_290]) ).
tff(c_8807,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1524,c_8791]) ).
tff(c_8808,plain,
v1_xboole_0(u1_struct_0('#skF_1')),
inference(splitRight,[status(thm)],[c_1256]) ).
tff(c_8820,plain,
( ~ l1_struct_0('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_8808,c_182]) ).
tff(c_8831,plain,
~ l1_struct_0('#skF_1'),
inference(negUnitSimplification,[status(thm)],[c_14,c_8820]) ).
tff(c_8837,plain,
~ l1_group_1('#skF_1'),
inference(resolution,[status(thm)],[c_136,c_8831]) ).
tff(c_8841,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_6,c_8837]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : GRP620+1 : TPTP v9.0.0. Released v3.4.0.
% 0.04/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 : n004.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 : Mon Apr 7 21:58:53 EDT 2025
% 0.13/0.35 % CPUTime :
% 15.70/5.28 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.70/5.30
% 15.70/5.30 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------