%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP620+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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:31 AM UTC 2026
% Result : Theorem 2.54s 0.74s
% Output : CNFRefutation 2.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 12
% Syntax : Number of formulae : 154 ( 20 unt; 0 def)
% Number of atoms : 821 ( 45 equ)
% Maximal formula atoms : 19 ( 5 avg)
% Number of connectives : 1198 ( 531 ~; 573 |; 66 &)
% ( 4 <=>; 24 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 1 prp; 0-4 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-1 aty)
% Number of variables : 171 ( 2 sgn 30 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d1_autgroup,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& v1_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_fraenkel(B,u1_struct_0(A),u1_struct_0(A))
=> ( B = k1_autgroup(A)
<=> ( ! [C] :
( ( m2_relset_1(C,u1_struct_0(A),u1_struct_0(A))
& v1_group_6(C,A,A)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(A))
& v1_funct_1(C) )
=> ( r2_hidden(C,B)
<=> ( v3_group_6(C,A,A)
& v2_funct_1(C) ) ) )
& ! [C] :
( m2_fraenkel(C,u1_struct_0(A),u1_struct_0(A),B)
=> ( m2_relset_1(C,u1_struct_0(A),u1_struct_0(A))
& v1_group_6(C,A,A)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(A))
& v1_funct_1(C) ) ) ) ) ) ),
file('theBenchmark.p',d1_autgroup) ).
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(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_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(t1_subset,axiom,
! [A,B] :
( r2_hidden(A,B)
=> m1_subset_1(A,B) ),
file('theBenchmark.p',t1_subset) ).
fof(t2_subset,axiom,
! [A,B] :
( m1_subset_1(A,B)
=> ( r2_hidden(A,B)
| v1_xboole_0(B) ) ),
file('theBenchmark.p',t2_subset) ).
fof(t5_autgroup,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& v1_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m2_relset_1(B,u1_struct_0(A),u1_struct_0(A))
& v1_group_6(B,A,A)
& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
& v1_funct_1(B) )
=> ( r2_hidden(B,k1_autgroup(A))
<=> v4_group_6(B,A,A) ) ) ),
file('theBenchmark.p',t5_autgroup) ).
fof(t6_autgroup,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& v1_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k1_autgroup(A))
=> ( m2_relset_1(k2_funct_1(B),u1_struct_0(A),u1_struct_0(A))
& v1_group_6(k2_funct_1(B),A,A)
& v1_funct_2(k2_funct_1(B),u1_struct_0(A),u1_struct_0(A))
& v1_funct_1(k2_funct_1(B)) ) ) ),
file('theBenchmark.p',t6_autgroup) ).
fof(t73_group_6,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_group_1(B)
& v4_group_1(B)
& v3_group_1(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( ( m2_relset_1(C,u1_struct_0(B),u1_struct_0(A))
& v1_group_6(C,B,A)
& v1_funct_2(C,u1_struct_0(B),u1_struct_0(A))
& v1_funct_1(C) )
=> ! [D] :
( ( m2_relset_1(D,u1_struct_0(A),u1_struct_0(B))
& v1_group_6(D,A,B)
& v1_funct_2(D,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(D) )
=> ( ( D = k2_funct_1(C)
& v4_group_6(C,B,A) )
=> v4_group_6(D,A,B) ) ) ) ) ),
file('theBenchmark.p',t73_group_6) ).
fof(t7_autgroup,conjecture,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& v1_group_1(A)
& ~ v3_struct_0(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('theBenchmark.p',t7_autgroup) ).
fof(t7_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) )
=> ! [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)) ) ),
inference(assume_negation,[status(cth)],[t7_autgroup]) ).
cnf(c_87,plain,
( m2_relset_1(C,u1_struct_0(A),u1_struct_0(A))
| ~ m2_fraenkel(C,u1_struct_0(A),u1_struct_0(A),B)
| k1_autgroup(A) != B
| ~ m1_fraenkel(B,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)],[d1_autgroup]) ).
cnf(c_88,plain,
( v1_group_6(C,A,A)
| ~ m2_fraenkel(C,u1_struct_0(A),u1_struct_0(A),B)
| k1_autgroup(A) != B
| ~ m1_fraenkel(B,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)],[d1_autgroup]) ).
cnf(c_89,plain,
( v1_funct_2(C,u1_struct_0(A),u1_struct_0(A))
| ~ m2_fraenkel(C,u1_struct_0(A),u1_struct_0(A),B)
| k1_autgroup(A) != B
| ~ m1_fraenkel(B,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)],[d1_autgroup]) ).
cnf(c_90,plain,
( v1_funct_1(C)
| ~ m2_fraenkel(C,u1_struct_0(A),u1_struct_0(A),B)
| k1_autgroup(A) != B
| ~ m1_fraenkel(B,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)],[d1_autgroup]) ).
cnf(c_92,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]) ).
cnf(c_97,plain,
( v4_group_6(B,A,A)
| ~ r2_hidden(B,k1_autgroup(A))
| ~ m2_relset_1(B,u1_struct_0(A),u1_struct_0(A))
| ~ v1_group_6(B,A,A)
| ~ v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
| ~ v1_funct_1(B)
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| ~ v1_group_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t5_autgroup]) ).
cnf(c_98,plain,
( ~ v4_group_6(B,A,A)
| r2_hidden(B,k1_autgroup(A))
| ~ m2_relset_1(B,u1_struct_0(A),u1_struct_0(A))
| ~ v1_group_6(B,A,A)
| ~ v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
| ~ v1_funct_1(B)
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| ~ v1_group_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t5_autgroup]) ).
cnf(c_99,plain,
( v1_funct_1(k2_funct_1(B))
| ~ m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k1_autgroup(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)],[t6_autgroup]) ).
cnf(c_100,plain,
( v1_funct_2(k2_funct_1(B),u1_struct_0(A),u1_struct_0(A))
| ~ m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k1_autgroup(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)],[t6_autgroup]) ).
cnf(c_101,plain,
( v1_group_6(k2_funct_1(B),A,A)
| ~ m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k1_autgroup(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)],[t6_autgroup]) ).
cnf(c_102,plain,
( m2_relset_1(k2_funct_1(B),u1_struct_0(A),u1_struct_0(A))
| ~ m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k1_autgroup(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)],[t6_autgroup]) ).
fof(nnf_68,plain,
? [A] :
( ? [B] :
( ~ m2_fraenkel(k2_funct_1(B),u1_struct_0(A),u1_struct_0(A),k1_autgroup(A))
& m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k1_autgroup(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)],[t7_autgroup_neg]) ).
fof(sk_t7_autgroup_neg,plain,
( ~ m2_fraenkel(k2_funct_1(sK1),u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0))
& m2_fraenkel(sK1,u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(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,sK1]),skolemize(A,sK0),skolemize(B,sK1)],[nnf_68]) ).
cnf(c_103,negated_conjecture,
v1_group_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t7_autgroup_neg]) ).
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_132,negated_conjecture,
( v1_funct_1(B)
| ~ m2_fraenkel(B,u1_struct_0(sK0),u1_struct_0(sK0),A)
| k1_autgroup(sK0) != A
| ~ m1_fraenkel(A,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_103,c_90]) ).
cnf(c_133,negated_conjecture,
( v1_funct_2(B,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m2_fraenkel(B,u1_struct_0(sK0),u1_struct_0(sK0),A)
| k1_autgroup(sK0) != A
| ~ m1_fraenkel(A,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_103,c_89]) ).
cnf(c_134,negated_conjecture,
( v1_group_6(B,sK0,sK0)
| ~ m2_fraenkel(B,u1_struct_0(sK0),u1_struct_0(sK0),A)
| k1_autgroup(sK0) != A
| ~ m1_fraenkel(A,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_103,c_88]) ).
cnf(c_135,negated_conjecture,
( m2_relset_1(B,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m2_fraenkel(B,u1_struct_0(sK0),u1_struct_0(sK0),A)
| k1_autgroup(sK0) != A
| ~ m1_fraenkel(A,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_103,c_87]) ).
cnf(c_153,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_103,c_92]) ).
cnf(c_154,negated_conjecture,
( v4_group_6(A,sK0,sK0)
| ~ r2_hidden(A,k1_autgroup(sK0))
| ~ m2_relset_1(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(A,sK0,sK0)
| ~ v1_funct_2(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_103,c_97]) ).
cnf(c_155,negated_conjecture,
( ~ v4_group_6(A,sK0,sK0)
| r2_hidden(A,k1_autgroup(sK0))
| ~ m2_relset_1(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(A,sK0,sK0)
| ~ v1_funct_2(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_103,c_98]) ).
cnf(c_156,negated_conjecture,
( v1_funct_1(k2_funct_1(A))
| ~ m2_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_103,c_99]) ).
cnf(c_157,negated_conjecture,
( v1_funct_2(k2_funct_1(A),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m2_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_103,c_100]) ).
cnf(c_158,negated_conjecture,
( v1_group_6(k2_funct_1(A),sK0,sK0)
| ~ m2_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_103,c_101]) ).
cnf(c_159,negated_conjecture,
( m2_relset_1(k2_funct_1(A),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m2_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_103,c_102]) ).
cnf(c_276,negated_conjecture,
~ m2_fraenkel(k2_funct_1(sK1),u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0)),
inference(split_conjunct,[status(thm)],[sk_t7_autgroup_neg]) ).
cnf(c_277,negated_conjecture,
m2_fraenkel(sK1,u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0)),
inference(split_conjunct,[status(thm)],[sk_t7_autgroup_neg]) ).
cnf(c_278,negated_conjecture,
l1_group_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t7_autgroup_neg]) ).
cnf(c_279,negated_conjecture,
v4_group_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t7_autgroup_neg]) ).
cnf(c_280,negated_conjecture,
v3_group_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t7_autgroup_neg]) ).
cnf(c_281,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t7_autgroup_neg]) ).
cnf(c_284,plain,
( v4_group_6(D,A,B)
| k2_funct_1(C) != D
| ~ v4_group_6(C,B,A)
| ~ m2_relset_1(D,u1_struct_0(A),u1_struct_0(B))
| ~ v1_group_6(D,A,B)
| ~ v1_funct_2(D,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(D)
| ~ m2_relset_1(C,u1_struct_0(B),u1_struct_0(A))
| ~ v1_group_6(C,B,A)
| ~ v1_funct_2(C,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_1(C)
| ~ l1_group_1(B)
| ~ v4_group_1(B)
| ~ v3_group_1(B)
| v3_struct_0(B)
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t73_group_6]) ).
cnf(c_288,plain,
( r2_hidden(A,B)
| v1_xboole_0(B)
| ~ m1_subset_1(A,B) ),
inference(clausify,[status(thm)],[t2_subset]) ).
cnf(c_289,plain,
( m1_subset_1(A,B)
| ~ r2_hidden(A,B) ),
inference(clausify,[status(thm)],[t1_subset]) ).
cnf(c_292,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_293,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_347,plain,
( ~ v1_xboole_0(A)
| ~ m1_fraenkel(A,B,C) ),
inference(clausify,[status(thm)],[dt_m1_fraenkel]) ).
cnf(c_370,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_1659,negated_conjecture,
( m2_relset_1(k2_funct_1(A),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m2_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(resolve,[status(thm)],[c_281,c_159]) ).
cnf(c_1660,negated_conjecture,
( m2_relset_1(k2_funct_1(A),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m2_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0) ),
inference(resolve,[status(thm)],[c_280,c_1659]) ).
cnf(c_1661,negated_conjecture,
( m2_relset_1(k2_funct_1(A),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m2_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0))
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_279,c_1660]) ).
cnf(c_381,negated_conjecture,
( m2_relset_1(k2_funct_1(A),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m2_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0)) ),
inference(resolve,[status(thm)],[c_278,c_1661]) ).
cnf(c_1662,negated_conjecture,
( v1_group_6(k2_funct_1(A),sK0,sK0)
| ~ m2_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(resolve,[status(thm)],[c_281,c_158]) ).
cnf(c_1663,negated_conjecture,
( v1_group_6(k2_funct_1(A),sK0,sK0)
| ~ m2_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0) ),
inference(resolve,[status(thm)],[c_280,c_1662]) ).
cnf(c_1664,negated_conjecture,
( v1_group_6(k2_funct_1(A),sK0,sK0)
| ~ m2_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0))
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_279,c_1663]) ).
cnf(c_382,negated_conjecture,
( v1_group_6(k2_funct_1(A),sK0,sK0)
| ~ m2_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0)) ),
inference(resolve,[status(thm)],[c_278,c_1664]) ).
cnf(c_1665,negated_conjecture,
( v1_funct_2(k2_funct_1(A),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m2_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(resolve,[status(thm)],[c_281,c_157]) ).
cnf(c_1666,negated_conjecture,
( v1_funct_2(k2_funct_1(A),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m2_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0) ),
inference(resolve,[status(thm)],[c_280,c_1665]) ).
cnf(c_1667,negated_conjecture,
( v1_funct_2(k2_funct_1(A),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m2_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0))
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_279,c_1666]) ).
cnf(c_383,negated_conjecture,
( v1_funct_2(k2_funct_1(A),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m2_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0)) ),
inference(resolve,[status(thm)],[c_278,c_1667]) ).
cnf(c_1668,negated_conjecture,
( v1_funct_1(k2_funct_1(A))
| ~ m2_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(resolve,[status(thm)],[c_281,c_156]) ).
cnf(c_1669,negated_conjecture,
( v1_funct_1(k2_funct_1(A))
| ~ m2_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0) ),
inference(resolve,[status(thm)],[c_280,c_1668]) ).
cnf(c_1670,negated_conjecture,
( v1_funct_1(k2_funct_1(A))
| ~ m2_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0))
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_279,c_1669]) ).
cnf(c_384,negated_conjecture,
( v1_funct_1(k2_funct_1(A))
| ~ m2_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0)) ),
inference(resolve,[status(thm)],[c_278,c_1670]) ).
cnf(c_1671,negated_conjecture,
( ~ v4_group_6(A,sK0,sK0)
| r2_hidden(A,k1_autgroup(sK0))
| ~ m2_relset_1(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(A,sK0,sK0)
| ~ v1_funct_2(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(resolve,[status(thm)],[c_281,c_155]) ).
cnf(c_1672,negated_conjecture,
( ~ v4_group_6(A,sK0,sK0)
| r2_hidden(A,k1_autgroup(sK0))
| ~ m2_relset_1(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(A,sK0,sK0)
| ~ v1_funct_2(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0) ),
inference(resolve,[status(thm)],[c_280,c_1671]) ).
cnf(c_1673,negated_conjecture,
( ~ v4_group_6(A,sK0,sK0)
| r2_hidden(A,k1_autgroup(sK0))
| ~ m2_relset_1(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(A,sK0,sK0)
| ~ v1_funct_2(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_279,c_1672]) ).
cnf(c_385,negated_conjecture,
( ~ v4_group_6(A,sK0,sK0)
| r2_hidden(A,k1_autgroup(sK0))
| ~ m2_relset_1(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(A,sK0,sK0)
| ~ v1_funct_2(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(A) ),
inference(resolve,[status(thm)],[c_278,c_1673]) ).
cnf(c_1674,negated_conjecture,
( v4_group_6(A,sK0,sK0)
| ~ r2_hidden(A,k1_autgroup(sK0))
| ~ m2_relset_1(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(A,sK0,sK0)
| ~ v1_funct_2(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(resolve,[status(thm)],[c_281,c_154]) ).
cnf(c_1675,negated_conjecture,
( v4_group_6(A,sK0,sK0)
| ~ r2_hidden(A,k1_autgroup(sK0))
| ~ m2_relset_1(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(A,sK0,sK0)
| ~ v1_funct_2(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0) ),
inference(resolve,[status(thm)],[c_280,c_1674]) ).
cnf(c_1676,negated_conjecture,
( v4_group_6(A,sK0,sK0)
| ~ r2_hidden(A,k1_autgroup(sK0))
| ~ m2_relset_1(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(A,sK0,sK0)
| ~ v1_funct_2(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_279,c_1675]) ).
cnf(c_386,negated_conjecture,
( v4_group_6(A,sK0,sK0)
| ~ r2_hidden(A,k1_autgroup(sK0))
| ~ m2_relset_1(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(A,sK0,sK0)
| ~ v1_funct_2(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(A) ),
inference(resolve,[status(thm)],[c_278,c_1676]) ).
cnf(c_1677,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_281,c_153]) ).
cnf(c_1678,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_280,c_1677]) ).
cnf(c_1679,negated_conjecture,
( m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_279,c_1678]) ).
cnf(c_387,negated_conjecture,
m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_278,c_1679]) ).
cnf(c_1680,negated_conjecture,
( m2_relset_1(B,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m2_fraenkel(B,u1_struct_0(sK0),u1_struct_0(sK0),A)
| k1_autgroup(sK0) != A
| ~ m1_fraenkel(A,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_281,c_135]) ).
cnf(c_1681,negated_conjecture,
( m2_relset_1(B,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m2_fraenkel(B,u1_struct_0(sK0),u1_struct_0(sK0),A)
| k1_autgroup(sK0) != A
| ~ m1_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0) ),
inference(resolve,[status(thm)],[c_280,c_1680]) ).
cnf(c_1682,negated_conjecture,
( m2_relset_1(B,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m2_fraenkel(B,u1_struct_0(sK0),u1_struct_0(sK0),A)
| k1_autgroup(sK0) != A
| ~ m1_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_279,c_1681]) ).
cnf(c_405,negated_conjecture,
( m2_relset_1(B,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m2_fraenkel(B,u1_struct_0(sK0),u1_struct_0(sK0),A)
| k1_autgroup(sK0) != A
| ~ m1_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_278,c_1682]) ).
cnf(c_1683,negated_conjecture,
( v1_group_6(B,sK0,sK0)
| ~ m2_fraenkel(B,u1_struct_0(sK0),u1_struct_0(sK0),A)
| k1_autgroup(sK0) != A
| ~ m1_fraenkel(A,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_281,c_134]) ).
cnf(c_1684,negated_conjecture,
( v1_group_6(B,sK0,sK0)
| ~ m2_fraenkel(B,u1_struct_0(sK0),u1_struct_0(sK0),A)
| k1_autgroup(sK0) != A
| ~ m1_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0) ),
inference(resolve,[status(thm)],[c_280,c_1683]) ).
cnf(c_1685,negated_conjecture,
( v1_group_6(B,sK0,sK0)
| ~ m2_fraenkel(B,u1_struct_0(sK0),u1_struct_0(sK0),A)
| k1_autgroup(sK0) != A
| ~ m1_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_279,c_1684]) ).
cnf(c_406,negated_conjecture,
( v1_group_6(B,sK0,sK0)
| ~ m2_fraenkel(B,u1_struct_0(sK0),u1_struct_0(sK0),A)
| k1_autgroup(sK0) != A
| ~ m1_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_278,c_1685]) ).
cnf(c_1686,negated_conjecture,
( v1_funct_2(B,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m2_fraenkel(B,u1_struct_0(sK0),u1_struct_0(sK0),A)
| k1_autgroup(sK0) != A
| ~ m1_fraenkel(A,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_281,c_133]) ).
cnf(c_1687,negated_conjecture,
( v1_funct_2(B,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m2_fraenkel(B,u1_struct_0(sK0),u1_struct_0(sK0),A)
| k1_autgroup(sK0) != A
| ~ m1_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0) ),
inference(resolve,[status(thm)],[c_280,c_1686]) ).
cnf(c_1688,negated_conjecture,
( v1_funct_2(B,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m2_fraenkel(B,u1_struct_0(sK0),u1_struct_0(sK0),A)
| k1_autgroup(sK0) != A
| ~ m1_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_279,c_1687]) ).
cnf(c_407,negated_conjecture,
( v1_funct_2(B,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m2_fraenkel(B,u1_struct_0(sK0),u1_struct_0(sK0),A)
| k1_autgroup(sK0) != A
| ~ m1_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_278,c_1688]) ).
cnf(c_1689,negated_conjecture,
( v1_funct_1(B)
| ~ m2_fraenkel(B,u1_struct_0(sK0),u1_struct_0(sK0),A)
| k1_autgroup(sK0) != A
| ~ m1_fraenkel(A,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_281,c_132]) ).
cnf(c_1690,negated_conjecture,
( v1_funct_1(B)
| ~ m2_fraenkel(B,u1_struct_0(sK0),u1_struct_0(sK0),A)
| k1_autgroup(sK0) != A
| ~ m1_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0) ),
inference(resolve,[status(thm)],[c_280,c_1689]) ).
cnf(c_1691,negated_conjecture,
( v1_funct_1(B)
| ~ m2_fraenkel(B,u1_struct_0(sK0),u1_struct_0(sK0),A)
| k1_autgroup(sK0) != A
| ~ m1_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_279,c_1690]) ).
cnf(c_408,negated_conjecture,
( v1_funct_1(B)
| ~ m2_fraenkel(B,u1_struct_0(sK0),u1_struct_0(sK0),A)
| k1_autgroup(sK0) != A
| ~ m1_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_278,c_1691]) ).
cnf(c_1692,plain,
( v4_group_6(C,A,A)
| k2_funct_1(B) != C
| ~ v4_group_6(B,A,A)
| ~ m2_relset_1(C,u1_struct_0(A),u1_struct_0(A))
| ~ v1_group_6(C,A,A)
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(A))
| ~ v1_funct_1(C)
| ~ m2_relset_1(B,u1_struct_0(A),u1_struct_0(A))
| ~ v1_group_6(B,A,A)
| ~ v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
| ~ v1_funct_1(B)
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(factor,[status(thm)],[c_284]) ).
cnf(c_1693,plain,
( v4_group_6(C,A,A)
| k2_funct_1(B) != C
| ~ v4_group_6(B,A,A)
| ~ m2_relset_1(C,u1_struct_0(A),u1_struct_0(A))
| ~ v1_group_6(C,A,A)
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(A))
| ~ v1_funct_1(C)
| ~ m2_relset_1(B,u1_struct_0(A),u1_struct_0(A))
| ~ v1_group_6(B,A,A)
| ~ v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
| ~ v1_funct_1(B)
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_1692]) ).
cnf(c_1694,plain,
( v4_group_6(C,A,A)
| k2_funct_1(B) != C
| ~ v4_group_6(B,A,A)
| ~ m2_relset_1(C,u1_struct_0(A),u1_struct_0(A))
| ~ v1_group_6(C,A,A)
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(A))
| ~ v1_funct_1(C)
| ~ m2_relset_1(B,u1_struct_0(A),u1_struct_0(A))
| ~ v1_group_6(B,A,A)
| ~ v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
| ~ v1_funct_1(B)
| ~ l1_group_1(A)
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_1693]) ).
cnf(c_410,plain,
( v4_group_6(C,A,A)
| k2_funct_1(B) != C
| ~ v4_group_6(B,A,A)
| ~ m2_relset_1(C,u1_struct_0(A),u1_struct_0(A))
| ~ v1_group_6(C,A,A)
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(A))
| ~ v1_funct_1(C)
| ~ m2_relset_1(B,u1_struct_0(A),u1_struct_0(A))
| ~ v1_group_6(B,A,A)
| ~ v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
| ~ v1_funct_1(B)
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_1694]) ).
cnf(c_1695,negated_conjecture,
( m1_subset_1(sK1,k1_autgroup(sK0))
| ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_293,c_277]) ).
cnf(c_509,negated_conjecture,
( m1_subset_1(sK1,k1_autgroup(sK0))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_387,c_1695]) ).
cnf(c_624,plain,
m2_relset_1(k2_funct_1(sK1),u1_struct_0(sK0),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_381,c_277]) ).
cnf(c_625,plain,
v1_group_6(k2_funct_1(sK1),sK0,sK0),
inference(resolve,[status(thm)],[c_382,c_277]) ).
cnf(c_626,plain,
v1_funct_2(k2_funct_1(sK1),u1_struct_0(sK0),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_383,c_277]) ).
cnf(c_627,plain,
v1_funct_1(k2_funct_1(sK1)),
inference(resolve,[status(thm)],[c_384,c_277]) ).
cnf(c_630,plain,
~ v1_xboole_0(k1_autgroup(sK0)),
inference(resolve,[status(thm)],[c_387,c_347]) ).
cnf(c_632,plain,
( ~ m1_subset_1(A,k1_autgroup(sK0))
| m2_fraenkel(A,u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_387,c_292]) ).
cnf(c_1696,negated_conjecture,
( m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| k1_autgroup(sK0) != k1_autgroup(sK0)
| ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_405,c_277]) ).
cnf(c_1697,negated_conjecture,
( m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(copy,[status(thm)],[c_1696]) ).
cnf(c_639,negated_conjecture,
m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_387,c_1697]) ).
cnf(c_1698,negated_conjecture,
( v1_group_6(sK1,sK0,sK0)
| k1_autgroup(sK0) != k1_autgroup(sK0)
| ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_406,c_277]) ).
cnf(c_1699,negated_conjecture,
( v1_group_6(sK1,sK0,sK0)
| ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(copy,[status(thm)],[c_1698]) ).
cnf(c_640,negated_conjecture,
v1_group_6(sK1,sK0,sK0),
inference(resolve,[status(thm)],[c_387,c_1699]) ).
cnf(c_1700,negated_conjecture,
( v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| k1_autgroup(sK0) != k1_autgroup(sK0)
| ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_407,c_277]) ).
cnf(c_1701,negated_conjecture,
( v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(copy,[status(thm)],[c_1700]) ).
cnf(c_641,negated_conjecture,
v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_387,c_1701]) ).
cnf(c_1702,negated_conjecture,
( v1_funct_1(sK1)
| k1_autgroup(sK0) != k1_autgroup(sK0)
| ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_408,c_277]) ).
cnf(c_1703,negated_conjecture,
( v1_funct_1(sK1)
| ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(copy,[status(thm)],[c_1702]) ).
cnf(c_642,negated_conjecture,
v1_funct_1(sK1),
inference(resolve,[status(thm)],[c_387,c_1703]) ).
cnf(c_1704,plain,
( r2_hidden(sK1,k1_autgroup(sK0))
| v1_xboole_0(k1_autgroup(sK0))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_509,c_288]) ).
cnf(c_741,plain,
( r2_hidden(sK1,k1_autgroup(sK0))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_630,c_1704]) ).
cnf(c_1705,negated_conjecture,
( v4_group_6(sK1,sK0,sK0)
| ~ r2_hidden(sK1,k1_autgroup(sK0))
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1) ),
inference(resolve,[status(thm)],[c_640,c_386]) ).
cnf(c_1706,negated_conjecture,
( v4_group_6(sK1,sK0,sK0)
| ~ r2_hidden(sK1,k1_autgroup(sK0))
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_642,c_1705]) ).
cnf(c_1707,negated_conjecture,
( v4_group_6(sK1,sK0,sK0)
| ~ r2_hidden(sK1,k1_autgroup(sK0))
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_641,c_1706]) ).
cnf(c_750,negated_conjecture,
( v4_group_6(sK1,sK0,sK0)
| ~ r2_hidden(sK1,k1_autgroup(sK0)) ),
inference(resolve,[status(thm)],[c_639,c_1707]) ).
cnf(c_973,plain,
( v1_xboole_0(u1_struct_0(sK0))
| v4_group_6(sK1,sK0,sK0) ),
inference(resolve,[status(thm)],[c_750,c_741]) ).
cnf(c_1708,plain,
( v4_group_6(A,sK0,sK0)
| k2_funct_1(sK1) != A
| ~ m2_relset_1(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(A,sK0,sK0)
| ~ v1_funct_2(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_973,c_410]) ).
cnf(c_1709,negated_conjecture,
( v4_group_6(A,sK0,sK0)
| k2_funct_1(sK1) != A
| ~ m2_relset_1(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(A,sK0,sK0)
| ~ v1_funct_2(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_281,c_1708]) ).
cnf(c_1710,negated_conjecture,
( v4_group_6(A,sK0,sK0)
| k2_funct_1(sK1) != A
| ~ m2_relset_1(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(A,sK0,sK0)
| ~ v1_funct_2(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_280,c_1709]) ).
cnf(c_1711,negated_conjecture,
( v4_group_6(A,sK0,sK0)
| k2_funct_1(sK1) != A
| ~ m2_relset_1(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(A,sK0,sK0)
| ~ v1_funct_2(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_group_1(sK0)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_279,c_1710]) ).
cnf(c_1712,negated_conjecture,
( v4_group_6(A,sK0,sK0)
| k2_funct_1(sK1) != A
| ~ m2_relset_1(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(A,sK0,sK0)
| ~ v1_funct_2(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_278,c_1711]) ).
cnf(c_1713,negated_conjecture,
( v4_group_6(A,sK0,sK0)
| k2_funct_1(sK1) != A
| ~ m2_relset_1(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(A,sK0,sK0)
| ~ v1_funct_2(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_642,c_1712]) ).
cnf(c_1714,negated_conjecture,
( v4_group_6(A,sK0,sK0)
| k2_funct_1(sK1) != A
| ~ m2_relset_1(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(A,sK0,sK0)
| ~ v1_funct_2(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK1,sK0,sK0)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_641,c_1713]) ).
cnf(c_1715,negated_conjecture,
( v4_group_6(A,sK0,sK0)
| k2_funct_1(sK1) != A
| ~ m2_relset_1(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(A,sK0,sK0)
| ~ v1_funct_2(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_640,c_1714]) ).
cnf(c_978,negated_conjecture,
( v4_group_6(A,sK0,sK0)
| k2_funct_1(sK1) != A
| ~ m2_relset_1(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(A,sK0,sK0)
| ~ v1_funct_2(A,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_639,c_1715]) ).
cnf(c_1716,plain,
( v4_group_6(k2_funct_1(sK1),sK0,sK0)
| k2_funct_1(sK1) != k2_funct_1(sK1)
| ~ m2_relset_1(k2_funct_1(sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k2_funct_1(sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k2_funct_1(sK1))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_978,c_625]) ).
cnf(c_1717,plain,
( v4_group_6(k2_funct_1(sK1),sK0,sK0)
| ~ m2_relset_1(k2_funct_1(sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k2_funct_1(sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k2_funct_1(sK1))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(copy,[status(thm)],[c_1716]) ).
cnf(c_1718,plain,
( v4_group_6(k2_funct_1(sK1),sK0,sK0)
| ~ m2_relset_1(k2_funct_1(sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k2_funct_1(sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_627,c_1717]) ).
cnf(c_1719,plain,
( v4_group_6(k2_funct_1(sK1),sK0,sK0)
| ~ m2_relset_1(k2_funct_1(sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_626,c_1718]) ).
cnf(c_1624,plain,
( v4_group_6(k2_funct_1(sK1),sK0,sK0)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_624,c_1719]) ).
cnf(c_1720,negated_conjecture,
( r2_hidden(k2_funct_1(sK1),k1_autgroup(sK0))
| ~ m2_relset_1(k2_funct_1(sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(k2_funct_1(sK1),sK0,sK0)
| ~ v1_funct_2(k2_funct_1(sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k2_funct_1(sK1))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_1624,c_385]) ).
cnf(c_1721,negated_conjecture,
( r2_hidden(k2_funct_1(sK1),k1_autgroup(sK0))
| ~ m2_relset_1(k2_funct_1(sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(k2_funct_1(sK1),sK0,sK0)
| ~ v1_funct_2(k2_funct_1(sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_627,c_1720]) ).
cnf(c_1722,negated_conjecture,
( r2_hidden(k2_funct_1(sK1),k1_autgroup(sK0))
| ~ m2_relset_1(k2_funct_1(sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(k2_funct_1(sK1),sK0,sK0)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_626,c_1721]) ).
cnf(c_1723,negated_conjecture,
( r2_hidden(k2_funct_1(sK1),k1_autgroup(sK0))
| ~ m2_relset_1(k2_funct_1(sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_625,c_1722]) ).
cnf(c_1628,negated_conjecture,
( r2_hidden(k2_funct_1(sK1),k1_autgroup(sK0))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_624,c_1723]) ).
cnf(c_1646,plain,
( m1_subset_1(k2_funct_1(sK1),k1_autgroup(sK0))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_1628,c_289]) ).
cnf(c_1724,plain,
( m2_fraenkel(k2_funct_1(sK1),u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0))
| v1_xboole_0(u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_1646,c_632]) ).
cnf(c_1725,plain,
( m2_fraenkel(k2_funct_1(sK1),u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(copy,[status(thm)],[c_1724]) ).
cnf(c_1647,negated_conjecture,
v1_xboole_0(u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_276,c_1725]) ).
cnf(c_1726,plain,
( v3_struct_0(sK0)
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_1647,c_370]) ).
cnf(c_1727,negated_conjecture,
v3_struct_0(sK0),
inference(resolve,[status(thm)],[c_278,c_1726]) ).
cnf(c_1658,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_281,c_1727]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP620+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n003.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Fri Sep 25 15:03:52 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.13/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.35 % Process 478012 was started by sandbox on n003,
% 0.13/0.35 % Fri Sep 25 15:03:52 2026
% 0.13/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.13/0.38
% 0.13/0.38 % From the command line: assign(max_seconds, 300).
% 2.54/0.74
% 2.54/0.74 % given #500 (T,wt=21): 765 v1_funct_1(k2_funct_1(k2_funct_1(c4))). [resolve(586,a,348,a),unit_del(a,580)].
% 2.54/0.74
% 2.54/0.74 % SZS status Theorem for theBenchmark
% 2.54/0.74
% 2.54/0.74 % Proof 1 at 0.28 (+ 0.03) seconds.
% 2.54/0.74 % Length of proof is 82.
% 2.54/0.74 % Level of proof is 12.
% 2.54/0.74 % Maximum clause weight is 74.000.
% 2.54/0.74 % Given clauses 776.
% 2.54/0.74
% 2.54/0.74 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------