%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP619+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:30:30 AM UTC 2026
% Result : Theorem 231.37s 30.85s
% Output : CNFRefutation 231.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 12
% Syntax : Number of formulae : 71 ( 18 unt; 0 def)
% Number of atoms : 218 ( 4 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 239 ( 92 ~; 93 |; 37 &)
% ( 2 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 1 prp; 0-4 aty)
% Number of functors : 6 ( 6 usr; 1 con; 0-2 aty)
% Number of variables : 115 ( 6 sgn 40 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cc1_fraenkel,axiom,
! [A] :
( v1_fraenkel(A)
=> ! [B] :
( m1_subset_1(B,A)
=> ( v1_funct_1(B)
& v1_relat_1(B) ) ) ),
file('theBenchmark.p',cc1_fraenkel) ).
fof(d3_tarski,axiom,
! [A,B] :
( r1_tarski(A,B)
<=> ! [C] :
( r2_hidden(C,A)
=> r2_hidden(C,B) ) ),
file('theBenchmark.p',d3_tarski) ).
fof(dt_k1_autgroup,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& v1_group_1(A)
& ~ v3_struct_0(A) )
=> m1_fraenkel(k1_autgroup(A),u1_struct_0(A),u1_struct_0(A)) ),
file('theBenchmark.p',dt_k1_autgroup) ).
fof(dt_l1_group_1,axiom,
! [A] :
( l1_group_1(A)
=> l1_struct_0(A) ),
file('theBenchmark.p',dt_l1_group_1) ).
fof(dt_m1_fraenkel,axiom,
! [A,B,C] :
( m1_fraenkel(C,A,B)
=> ( v1_fraenkel(C)
& ~ v1_xboole_0(C) ) ),
file('theBenchmark.p',dt_m1_fraenkel) ).
fof(dt_m2_fraenkel,axiom,
! [A,B,C] :
( ( m1_fraenkel(C,A,B)
& ~ v1_xboole_0(B) )
=> ! [D] :
( m2_fraenkel(D,A,B,C)
=> ( m2_relset_1(D,A,B)
& v1_funct_2(D,A,B)
& v1_funct_1(D) ) ) ),
file('theBenchmark.p',dt_m2_fraenkel) ).
fof(fc1_struct_0,axiom,
! [A] :
( ( l1_struct_0(A)
& ~ v3_struct_0(A) )
=> ~ v1_xboole_0(u1_struct_0(A)) ),
file('theBenchmark.p',fc1_struct_0) ).
fof(redefinition_k1_fraenkel,axiom,
! [A,B] :
( ~ v1_xboole_0(B)
=> k1_fraenkel(A,B) = k1_funct_2(A,B) ),
file('theBenchmark.p',redefinition_k1_fraenkel) ).
fof(redefinition_m2_fraenkel,axiom,
! [A,B,C] :
( ( m1_fraenkel(C,A,B)
& ~ v1_xboole_0(B) )
=> ! [D] :
( m2_fraenkel(D,A,B,C)
<=> m1_subset_1(D,C) ) ),
file('theBenchmark.p',redefinition_m2_fraenkel) ).
fof(t12_funct_2,axiom,
! [A,B] :
( ( m2_relset_1(B,A,A)
& v1_funct_2(B,A,A)
& v1_funct_1(B) )
=> r2_hidden(B,k1_funct_2(A,A)) ),
file('theBenchmark.p',t12_funct_2) ).
fof(t1_subset,axiom,
! [A,B] :
( r2_hidden(A,B)
=> m1_subset_1(A,B) ),
file('theBenchmark.p',t1_subset) ).
fof(t3_autgroup,conjecture,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& v1_group_1(A)
& ~ v3_struct_0(A) )
=> r1_tarski(k1_autgroup(A),k1_fraenkel(u1_struct_0(A),u1_struct_0(A))) ),
file('theBenchmark.p',t3_autgroup) ).
fof(t3_autgroup_neg,negated_conjecture,
~ ! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& v1_group_1(A)
& ~ v3_struct_0(A) )
=> r1_tarski(k1_autgroup(A),k1_fraenkel(u1_struct_0(A),u1_struct_0(A))) ),
inference(assume_negation,[status(cth)],[t3_autgroup]) ).
cnf(c_71,plain,
( m1_fraenkel(k1_autgroup(A),u1_struct_0(A),u1_struct_0(A))
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| ~ v1_group_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k1_autgroup]) ).
fof(nnf_68,plain,
? [A] :
( ~ r1_tarski(k1_autgroup(A),k1_fraenkel(u1_struct_0(A),u1_struct_0(A)))
& l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& v1_group_1(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t3_autgroup_neg]) ).
fof(sk_t3_autgroup_neg,plain,
( ~ r1_tarski(k1_autgroup(sK0),k1_fraenkel(u1_struct_0(sK0),u1_struct_0(sK0)))
& l1_group_1(sK0)
& v4_group_1(sK0)
& v3_group_1(sK0)
& v1_group_1(sK0)
& ~ v3_struct_0(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(A,sK0)],[nnf_68]) ).
cnf(c_76,negated_conjecture,
v1_group_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t3_autgroup_neg]) ).
cnf(c_77,plain,
( v1_funct_1(B)
| ~ m1_subset_1(B,A)
| ~ v1_fraenkel(A) ),
inference(clausify,[status(thm)],[cc1_fraenkel]) ).
cnf(c_78,plain,
( v1_fraenkel(A)
| ~ m1_fraenkel(A,B,C) ),
inference(clausify,[status(thm)],[dt_m1_fraenkel]) ).
cnf(c_98,plain,
( ~ m1_fraenkel(B,C,D)
| v1_funct_1(A)
| ~ m1_subset_1(A,B) ),
inference(resolve,[status(thm)],[c_77,c_78]) ).
cnf(c_113,plain,
( r2_hidden(A,k1_funct_2(B,B))
| ~ m2_relset_1(A,B,B)
| ~ v1_funct_2(A,B,B)
| ~ v1_funct_1(A) ),
inference(clausify,[status(thm)],[t12_funct_2]) ).
cnf(c_119,plain,
( ~ v1_xboole_0(u1_struct_0(A))
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_struct_0]) ).
cnf(c_121,plain,
( l1_struct_0(A)
| ~ l1_group_1(A) ),
inference(clausify,[status(thm)],[dt_l1_group_1]) ).
cnf(c_123,plain,
( m2_relset_1(D,C,A)
| ~ m2_fraenkel(D,C,A,B)
| ~ m1_fraenkel(B,C,A)
| v1_xboole_0(A) ),
inference(clausify,[status(thm)],[dt_m2_fraenkel]) ).
cnf(c_124,plain,
( v1_funct_2(D,C,A)
| ~ m2_fraenkel(D,C,A,B)
| ~ m1_fraenkel(B,C,A)
| v1_xboole_0(A) ),
inference(clausify,[status(thm)],[dt_m2_fraenkel]) ).
cnf(c_126,plain,
( ~ m1_subset_1(D,B)
| m2_fraenkel(D,C,A,B)
| ~ m1_fraenkel(B,C,A)
| v1_xboole_0(A) ),
inference(clausify,[status(thm)],[redefinition_m2_fraenkel]) ).
cnf(c_150,plain,
( v1_funct_2(D,C,A)
| ~ m1_fraenkel(B,C,A)
| v1_xboole_0(A)
| ~ m1_subset_1(D,B)
| ~ m1_fraenkel(B,C,A)
| v1_xboole_0(A) ),
inference(resolve,[status(thm)],[c_126,c_124]) ).
cnf(c_22712,plain,
( v1_funct_2(D,C,A)
| ~ m1_fraenkel(B,C,A)
| ~ m1_subset_1(D,B)
| ~ m1_fraenkel(B,C,A)
| v1_xboole_0(A) ),
inference(copy,[status(thm)],[c_150]) ).
cnf(c_151,plain,
( v1_funct_2(D,C,A)
| ~ m1_subset_1(D,B)
| ~ m1_fraenkel(B,C,A)
| v1_xboole_0(A) ),
inference(copy,[status(thm)],[c_22712]) ).
cnf(c_152,plain,
( m2_relset_1(D,C,A)
| ~ m1_fraenkel(B,C,A)
| v1_xboole_0(A)
| ~ m1_subset_1(D,B)
| ~ m1_fraenkel(B,C,A)
| v1_xboole_0(A) ),
inference(resolve,[status(thm)],[c_126,c_123]) ).
cnf(c_22713,plain,
( m2_relset_1(D,C,A)
| ~ m1_fraenkel(B,C,A)
| ~ m1_subset_1(D,B)
| ~ m1_fraenkel(B,C,A)
| v1_xboole_0(A) ),
inference(copy,[status(thm)],[c_152]) ).
cnf(c_153,plain,
( m2_relset_1(D,C,A)
| ~ m1_subset_1(D,B)
| ~ m1_fraenkel(B,C,A)
| v1_xboole_0(A) ),
inference(copy,[status(thm)],[c_22713]) ).
cnf(c_184,plain,
( ~ m1_fraenkel(C,D,E)
| ~ m1_subset_1(A,C)
| r2_hidden(A,k1_funct_2(B,B))
| ~ m2_relset_1(A,B,B)
| ~ v1_funct_2(A,B,B) ),
inference(resolve,[status(thm)],[c_113,c_98]) ).
cnf(c_254,negated_conjecture,
( m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_76,c_71]) ).
cnf(c_261,negated_conjecture,
~ r1_tarski(k1_autgroup(sK0),k1_fraenkel(u1_struct_0(sK0),u1_struct_0(sK0))),
inference(split_conjunct,[status(thm)],[sk_t3_autgroup_neg]) ).
cnf(c_262,negated_conjecture,
l1_group_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t3_autgroup_neg]) ).
cnf(c_263,negated_conjecture,
v4_group_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t3_autgroup_neg]) ).
cnf(c_264,negated_conjecture,
v3_group_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t3_autgroup_neg]) ).
cnf(c_265,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t3_autgroup_neg]) ).
cnf(c_274,plain,
( m1_subset_1(A,B)
| ~ r2_hidden(A,B) ),
inference(clausify,[status(thm)],[t1_subset]) ).
cnf(c_278,plain,
( k1_funct_2(B,A) = k1_fraenkel(B,A)
| v1_xboole_0(A) ),
inference(clausify,[status(thm)],[redefinition_k1_fraenkel]) ).
cnf(c_279,plain,
( k1_fraenkel(B,A) = k1_funct_2(B,A)
| v1_xboole_0(A) ),
inference(copy,[status(thm)],[c_278]) ).
fof(nnf_11,plain,
! [A,B] :
( ( ? [C] :
( ~ r2_hidden(C,B)
& r2_hidden(C,A) )
| r1_tarski(A,B) )
& ( ! [X0] :
( r2_hidden(X0,B)
| ~ r2_hidden(X0,A) )
| ~ r1_tarski(A,B) ) ),
inference(fof_nnf,[status(thm)],[d3_tarski]) ).
fof(sk_d3_tarski_sk,plain,
! [A,B] :
( ( ( ~ r2_hidden(sK1(A,B),B)
& r2_hidden(sK1(A,B),A) )
| r1_tarski(A,B) )
& ( ! [X0] :
( r2_hidden(X0,B)
| ~ r2_hidden(X0,A) )
| ~ r1_tarski(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(C,sK1(A,B))],[nnf_11]) ).
fof(sk_d3_tarski,plain,
( ! [VAR_0,VAR_1] :
( ~ r2_hidden(sK1(VAR_0,VAR_1),VAR_1)
| r1_tarski(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( r2_hidden(sK1(VAR_0,VAR_1),VAR_0)
| r1_tarski(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( r2_hidden(VAR_2,VAR_1)
| ~ r2_hidden(VAR_2,VAR_0)
| ~ r1_tarski(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_d3_tarski_sk]) ).
cnf(c_309,plain,
( ~ r2_hidden(sK1(A,B),B)
| r1_tarski(A,B) ),
inference(split_conjunct,[status(thm)],[sk_d3_tarski]) ).
cnf(c_310,plain,
( r2_hidden(sK1(A,B),A)
| r1_tarski(A,B) ),
inference(split_conjunct,[status(thm)],[sk_d3_tarski]) ).
cnf(c_322,plain,
( ~ v1_xboole_0(u1_struct_0(A))
| v3_struct_0(A)
| ~ l1_group_1(A) ),
inference(resolve,[status(thm)],[c_121,c_119]) ).
cnf(c_22714,negated_conjecture,
( m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(resolve,[status(thm)],[c_265,c_254]) ).
cnf(c_22715,negated_conjecture,
( m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0) ),
inference(resolve,[status(thm)],[c_264,c_22714]) ).
cnf(c_22716,negated_conjecture,
( m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_263,c_22715]) ).
cnf(c_327,negated_conjecture,
m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_262,c_22716]) ).
cnf(c_576,plain,
r2_hidden(sK1(k1_autgroup(sK0),k1_fraenkel(u1_struct_0(sK0),u1_struct_0(sK0))),k1_autgroup(sK0)),
inference(resolve,[status(thm)],[c_310,c_261]) ).
cnf(c_22717,negated_conjecture,
( ~ v1_xboole_0(u1_struct_0(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_322,c_262]) ).
cnf(c_610,negated_conjecture,
~ v1_xboole_0(u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_265,c_22717]) ).
cnf(c_629,plain,
( ~ m1_subset_1(A,k1_autgroup(sK0))
| r2_hidden(A,k1_funct_2(B,B))
| ~ m2_relset_1(A,B,B)
| ~ v1_funct_2(A,B,B) ),
inference(resolve,[status(thm)],[c_327,c_184]) ).
cnf(c_22718,negated_conjecture,
( m2_relset_1(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m1_subset_1(A,k1_autgroup(sK0))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_327,c_153]) ).
cnf(c_635,negated_conjecture,
( m2_relset_1(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m1_subset_1(A,k1_autgroup(sK0)) ),
inference(resolve,[status(thm)],[c_610,c_22718]) ).
cnf(c_22719,negated_conjecture,
( v1_funct_2(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m1_subset_1(A,k1_autgroup(sK0))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_327,c_151]) ).
cnf(c_636,negated_conjecture,
( v1_funct_2(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m1_subset_1(A,k1_autgroup(sK0)) ),
inference(resolve,[status(thm)],[c_610,c_22719]) ).
cnf(c_667,plain,
k1_fraenkel(A,u1_struct_0(sK0)) = k1_funct_2(A,u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_610,c_279]) ).
cnf(c_668,plain,
r2_hidden(sK1(k1_autgroup(sK0),k1_funct_2(u1_struct_0(sK0),u1_struct_0(sK0))),k1_autgroup(sK0)),
inference(paramod,[status(thm)],[c_667,c_576]) ).
cnf(c_669,negated_conjecture,
~ r1_tarski(k1_autgroup(sK0),k1_funct_2(u1_struct_0(sK0),u1_struct_0(sK0))),
inference(paramod,[status(thm)],[c_667,c_261]) ).
cnf(c_2014,plain,
m1_subset_1(sK1(k1_autgroup(sK0),k1_funct_2(u1_struct_0(sK0),u1_struct_0(sK0))),k1_autgroup(sK0)),
inference(resolve,[status(thm)],[c_668,c_274]) ).
cnf(c_2518,plain,
v1_funct_2(sK1(k1_autgroup(sK0),k1_funct_2(u1_struct_0(sK0),u1_struct_0(sK0))),u1_struct_0(sK0),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_2014,c_636]) ).
cnf(c_2519,plain,
m2_relset_1(sK1(k1_autgroup(sK0),k1_funct_2(u1_struct_0(sK0),u1_struct_0(sK0))),u1_struct_0(sK0),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_2014,c_635]) ).
cnf(c_22720,plain,
( ~ m1_subset_1(sK1(k1_autgroup(sK0),k1_funct_2(u1_struct_0(sK0),u1_struct_0(sK0))),k1_autgroup(sK0))
| r2_hidden(sK1(k1_autgroup(sK0),k1_funct_2(u1_struct_0(sK0),u1_struct_0(sK0))),k1_funct_2(u1_struct_0(sK0),u1_struct_0(sK0)))
| ~ m2_relset_1(sK1(k1_autgroup(sK0),k1_funct_2(u1_struct_0(sK0),u1_struct_0(sK0))),u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_2518,c_629]) ).
cnf(c_22721,plain,
( ~ m1_subset_1(sK1(k1_autgroup(sK0),k1_funct_2(u1_struct_0(sK0),u1_struct_0(sK0))),k1_autgroup(sK0))
| r2_hidden(sK1(k1_autgroup(sK0),k1_funct_2(u1_struct_0(sK0),u1_struct_0(sK0))),k1_funct_2(u1_struct_0(sK0),u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_2519,c_22720]) ).
cnf(c_9460,plain,
r2_hidden(sK1(k1_autgroup(sK0),k1_funct_2(u1_struct_0(sK0),u1_struct_0(sK0))),k1_funct_2(u1_struct_0(sK0),u1_struct_0(sK0))),
inference(resolve,[status(thm)],[c_2014,c_22721]) ).
cnf(c_22722,plain,
r1_tarski(k1_autgroup(sK0),k1_funct_2(u1_struct_0(sK0),u1_struct_0(sK0))),
inference(resolve,[status(thm)],[c_9460,c_309]) ).
cnf(c_22711,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_669,c_22722]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP619+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.42 % Computer : n014.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Fri Sep 25 15:02:17 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.43 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.16/0.43 % Process 525381 was started by sandbox2 on n014,
% 0.16/0.43 % Fri Sep 25 15:02:17 2026
% 0.16/0.43 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.16/0.46
% 0.16/0.46 % From the command line: assign(max_seconds, 300).
% 231.37/30.85
% 231.37/30.85 % given #500 (T,wt=10): 1496 r2_hidden(f4(f4(k1_autgroup(c14))),k2_zfmisc_1(u1_struct_0(c14),u1_struct_0(c14))). [resolve(1477,a,728,b),unit_del(a,1137)].
% 231.37/30.85
% 231.37/30.85 % given #1000 (W,wt=12): 3360 m1_subset_1(f4(f9(c9)),A) | r2_hidden(f1(f9(c9),A),u1_struct_0(c9)). [resolve(3119,c,755,a),unit_del(a,619)].
% 231.37/30.85
% 231.37/30.85 % given #1500 (F,wt=12): 11037 -r2_hidden(u1_struct_0(c9),f1(f9(c9),f1(f9(c9),f4(f9(c9))))). [resolve(10931,a,312,b)].
% 231.37/30.85
% 231.37/30.85 % given #2000 (A,wt=92): 1214 v1_xboole_0(f4(k1_zfmisc_1(k1_funct_2(A,B)))) | v3_struct_0(g1_group_1(C,f4(f4(k1_zfmisc_1(k1_funct_2(A,B)))))) | -v3_group_1(g1_group_1(C,f4(f4(k1_zfmisc_1(k1_funct_2(A,B)))))) | -v4_group_1(g1_group_1(C,f4(f4(k1_zfmisc_1(k1_funct_2(A,B)))))) | -l1_group_1(g1_group_1(C,f4(f4(k1_zfmisc_1(k1_funct_2(A,B)))))) | m1_fraenkel(k1_autgroup(g1_group_1(C,f4(f4(k1_zfmisc_1(k1_funct_2(A,B)))))),u1_struct_0(g1_group_1(C,f4(f4(k1_zfmisc_1(k1_funct_2(A,B)))))),u1_struct_0(g1_group_1(C,f4(f4(k1_zfmisc_1(k1_funct_2(A,B))))))) | -v1_funct_2(f4(f4(k1_zfmisc_1(k1_funct_2(A,B)))),k2_zfmisc_1(C,C),C) | -m1_relset_1(f4(f4(k1_zfmisc_1(k1_funct_2(A,B)))),k2_zfmisc_1(C,C),C). [resolve(817,a,161,h)].
% 231.37/30.85
% 231.37/30.85 % given #2500 (A,wt=23): 1421 k1_fraenkel(A,k1_funct_2(B,C)) = k1_funct_2(A,k1_funct_2(B,C)) | v1_xboole_0(D) | v1_xboole_0(E) | -m1_relset_1(C,D,E) | -v1_funct_2(C,D,E). [resolve(452,a,252,e)].
% 231.37/30.85
% 231.37/30.85 % given #3000 (T,wt=14): 9460 r2_hidden(f1(k1_autgroup(c14),k1_funct_2(u1_struct_0(c14),u1_struct_0(c14))),k1_funct_2(u1_struct_0(c14),u1_struct_0(c14))). [resolve(2518,a,629,a),unit_del(a,2519),unit_del(c,2014)].
% 231.37/30.85
% 231.37/30.85 % SZS status Theorem for theBenchmark
% 231.37/30.85
% 231.37/30.85 % Proof 1 at 4.89 (+ 1.21) seconds.
% 231.37/30.85 % Length of proof is 54.
% 231.37/30.85 % Level of proof is 9.
% 231.37/30.85 % Maximum clause weight is 20.000.
% 231.37/30.85 % Given clauses 3000.
% 231.37/30.85
% 231.37/30.85 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------