%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP640+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 : n016.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:36 AM UTC 2026
% Result : Theorem 0.13s 0.49s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 7
% Syntax : Number of formulae : 86 ( 29 unt; 0 def)
% Number of atoms : 352 ( 41 equ)
% Maximal formula atoms : 16 ( 4 avg)
% Number of connectives : 448 ( 182 ~; 172 |; 69 &)
% ( 2 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 5 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-4 aty)
% Number of variables : 115 ( 0 sgn 31 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(redefinition_k2_funct_2,axiom,
! [A,B,C,D] :
( ( m1_relset_1(C,A,B)
& v1_funct_2(C,A,B)
& v1_funct_1(C) )
=> k2_funct_2(A,B,C,D) = k9_relat_1(C,D) ),
file('theBenchmark.p',redefinition_k2_funct_2) ).
fof(redefinition_m2_relset_1,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('theBenchmark.p',redefinition_m2_relset_1) ).
fof(redefinition_r1_group_2,axiom,
! [A,B,C] :
( ( m1_group_2(C,A)
& v1_group_1(C)
& m1_group_2(B,A)
& v1_group_1(B)
& l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ( r1_group_2(A,B,C)
<=> B = C ) ),
file('theBenchmark.p',redefinition_r1_group_2) ).
fof(dt_k5_group_4,axiom,
! [A,B] :
( ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
& l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ( m1_group_2(k5_group_4(A,B),A)
& v1_group_1(k5_group_4(A,B)) ) ),
file('theBenchmark.p',dt_k5_group_4) ).
fof(dt_k8_group_4,axiom,
! [A,B,C] :
( ( m1_group_2(C,A)
& m1_group_2(B,A)
& l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ( m1_group_2(k8_group_4(A,B,C),A)
& v1_group_1(k8_group_4(A,B,C)) ) ),
file('theBenchmark.p',dt_k8_group_4) ).
fof(t4_latsubgr,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_group_2(B,A)
=> ! [C] :
( m1_group_2(C,A)
=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))
=> ( D = k2_xboole_0(u1_struct_0(B),u1_struct_0(C))
=> r1_group_2(A,k8_group_4(A,B,C),k5_group_4(A,D)) ) ) ) ) ),
file('theBenchmark.p',t4_latsubgr) ).
fof(t13_latsubgr,conjecture,
! [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] :
( m1_group_2(C,A)
=> ! [D] :
( m1_group_2(D,A)
=> ! [E] :
( ( m2_relset_1(E,u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(E,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(E) )
=> ! [F] :
( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A)))
=> ( F = k2_xboole_0(u1_struct_0(C),u1_struct_0(D))
=> k2_funct_2(u1_struct_0(A),u1_struct_0(B),E,u1_struct_0(k8_group_4(A,C,D))) = k2_funct_2(u1_struct_0(A),u1_struct_0(B),E,u1_struct_0(k5_group_4(A,F))) ) ) ) ) ) ) ),
file('theBenchmark.p',t13_latsubgr) ).
fof(t13_latsubgr_neg,negated_conjecture,
~ ! [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] :
( m1_group_2(C,A)
=> ! [D] :
( m1_group_2(D,A)
=> ! [E] :
( ( m2_relset_1(E,u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(E,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(E) )
=> ! [F] :
( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A)))
=> ( F = k2_xboole_0(u1_struct_0(C),u1_struct_0(D))
=> k2_funct_2(u1_struct_0(A),u1_struct_0(B),E,u1_struct_0(k8_group_4(A,C,D))) = k2_funct_2(u1_struct_0(A),u1_struct_0(B),E,u1_struct_0(k5_group_4(A,F))) ) ) ) ) ) ) ),
inference(assume_negation,[status(cth)],[t13_latsubgr]) ).
fof(nnf_62,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( ? [E] :
( ? [F] :
( k2_funct_2(u1_struct_0(A),u1_struct_0(B),E,u1_struct_0(k5_group_4(A,F))) != k2_funct_2(u1_struct_0(A),u1_struct_0(B),E,u1_struct_0(k8_group_4(A,C,D)))
& k2_xboole_0(u1_struct_0(C),u1_struct_0(D)) = F
& m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A))) )
& m2_relset_1(E,u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(E,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(E) )
& m1_group_2(D,A) )
& m1_group_2(C,A) )
& 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(fof_nnf,[status(thm)],[t13_latsubgr_neg]) ).
fof(sk_t13_latsubgr_neg,plain,
( k2_funct_2(u1_struct_0(sK0),u1_struct_0(sK2),sK1,u1_struct_0(k5_group_4(sK0,sK5))) != k2_funct_2(u1_struct_0(sK0),u1_struct_0(sK2),sK1,u1_struct_0(k8_group_4(sK0,sK3,sK4)))
& k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4)) = sK5
& m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK0)))
& m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK2))
& v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK2))
& v1_funct_1(sK1)
& m1_group_2(sK4,sK0)
& m1_group_2(sK3,sK0)
& l1_group_1(sK2)
& v4_group_1(sK2)
& v3_group_1(sK2)
& ~ v3_struct_0(sK2)
& l1_group_1(sK0)
& v4_group_1(sK0)
& v3_group_1(sK0)
& ~ v3_struct_0(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK2,sK3,sK4,sK1,sK5]),skolemize(A,sK0),skolemize(B,sK2),skolemize(C,sK3),skolemize(D,sK4),skolemize(E,sK1),skolemize(F,sK5)],[nnf_62]) ).
cnf(c_63,negated_conjecture,
v4_group_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t13_latsubgr_neg]) ).
cnf(c_64,plain,
( r1_group_2(A,k8_group_4(A,B,C),k5_group_4(A,D))
| k2_xboole_0(u1_struct_0(B),u1_struct_0(C)) != D
| ~ m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_group_2(C,A)
| ~ m1_group_2(B,A)
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t4_latsubgr]) ).
cnf(c_65,plain,
( m1_group_2(k8_group_4(A,B,C),A)
| ~ m1_group_2(C,A)
| ~ m1_group_2(B,A)
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k8_group_4]) ).
cnf(c_66,plain,
( v1_group_1(k8_group_4(A,B,C))
| ~ m1_group_2(C,A)
| ~ m1_group_2(B,A)
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k8_group_4]) ).
cnf(c_67,plain,
( m1_group_2(k5_group_4(A,B),A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k5_group_4]) ).
cnf(c_68,plain,
( v1_group_1(k5_group_4(A,B))
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k5_group_4]) ).
cnf(c_70,plain,
( C = B
| ~ r1_group_2(A,B,C)
| ~ m1_group_2(C,A)
| ~ v1_group_1(C)
| ~ m1_group_2(B,A)
| ~ v1_group_1(B)
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[redefinition_r1_group_2]) ).
cnf(c_75,negated_conjecture,
v1_funct_1(sK1),
inference(split_conjunct,[status(thm)],[sk_t13_latsubgr_neg]) ).
cnf(c_76,plain,
( k9_relat_1(A,D) = k2_funct_2(B,C,A,D)
| ~ m1_relset_1(A,B,C)
| ~ v1_funct_2(A,B,C)
| ~ v1_funct_1(A) ),
inference(clausify,[status(thm)],[redefinition_k2_funct_2]) ).
cnf(c_88,plain,
( m1_relset_1(A,B,C)
| ~ m2_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_m2_relset_1]) ).
cnf(c_93,negated_conjecture,
m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK2)),
inference(split_conjunct,[status(thm)],[sk_t13_latsubgr_neg]) ).
cnf(c_157,negated_conjecture,
( k9_relat_1(sK1,C) = k2_funct_2(A,B,sK1,C)
| ~ m1_relset_1(sK1,A,B)
| ~ v1_funct_2(sK1,A,B) ),
inference(resolve,[status(thm)],[c_76,c_75]) ).
cnf(c_158,negated_conjecture,
( k2_funct_2(A,B,sK1,C) = k9_relat_1(sK1,C)
| ~ m1_relset_1(sK1,A,B)
| ~ v1_funct_2(sK1,A,B) ),
inference(copy,[status(thm)],[c_157]) ).
cnf(c_195,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t13_latsubgr_neg]) ).
cnf(c_196,negated_conjecture,
v3_group_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t13_latsubgr_neg]) ).
cnf(c_197,negated_conjecture,
l1_group_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t13_latsubgr_neg]) ).
cnf(c_201,negated_conjecture,
m1_group_2(sK3,sK0),
inference(split_conjunct,[status(thm)],[sk_t13_latsubgr_neg]) ).
cnf(c_202,negated_conjecture,
m1_group_2(sK4,sK0),
inference(split_conjunct,[status(thm)],[sk_t13_latsubgr_neg]) ).
cnf(c_203,negated_conjecture,
v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK2)),
inference(split_conjunct,[status(thm)],[sk_t13_latsubgr_neg]) ).
cnf(c_204,negated_conjecture,
m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK0))),
inference(split_conjunct,[status(thm)],[sk_t13_latsubgr_neg]) ).
cnf(c_205,negated_conjecture,
k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4)) = sK5,
inference(split_conjunct,[status(thm)],[sk_t13_latsubgr_neg]) ).
cnf(c_206,negated_conjecture,
sK5 = k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4)),
inference(copy,[status(thm)],[c_205]) ).
cnf(c_207,negated_conjecture,
k2_funct_2(u1_struct_0(sK0),u1_struct_0(sK2),sK1,u1_struct_0(k5_group_4(sK0,sK5))) != k2_funct_2(u1_struct_0(sK0),u1_struct_0(sK2),sK1,u1_struct_0(k8_group_4(sK0,sK3,sK4))),
inference(split_conjunct,[status(thm)],[sk_t13_latsubgr_neg]) ).
cnf(c_1513,negated_conjecture,
k2_funct_2(u1_struct_0(sK0),u1_struct_0(sK2),sK1,u1_struct_0(k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4))))) != k2_funct_2(u1_struct_0(sK0),u1_struct_0(sK2),sK1,u1_struct_0(k8_group_4(sK0,sK3,sK4))),
inference(paramod,[status(thm)],[c_206,c_207]) ).
cnf(c_208,negated_conjecture,
k2_funct_2(u1_struct_0(sK0),u1_struct_0(sK2),sK1,u1_struct_0(k8_group_4(sK0,sK3,sK4))) != k2_funct_2(u1_struct_0(sK0),u1_struct_0(sK2),sK1,u1_struct_0(k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4))))),
inference(copy,[status(thm)],[c_1513]) ).
cnf(c_209,negated_conjecture,
( r1_group_2(sK0,k8_group_4(sK0,A,B),k5_group_4(sK0,C))
| k2_xboole_0(u1_struct_0(A),u1_struct_0(B)) != C
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m1_group_2(B,sK0)
| ~ m1_group_2(A,sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_63,c_64]) ).
cnf(c_1514,negated_conjecture,
( r1_group_2(sK0,k8_group_4(sK0,A,B),k5_group_4(sK0,C))
| k2_xboole_0(u1_struct_0(A),u1_struct_0(B)) != C
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m1_group_2(B,sK0)
| ~ m1_group_2(A,sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(resolve,[status(thm)],[c_195,c_209]) ).
cnf(c_1515,negated_conjecture,
( r1_group_2(sK0,k8_group_4(sK0,A,B),k5_group_4(sK0,C))
| k2_xboole_0(u1_struct_0(A),u1_struct_0(B)) != C
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m1_group_2(B,sK0)
| ~ m1_group_2(A,sK0)
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_196,c_1514]) ).
cnf(c_210,negated_conjecture,
( r1_group_2(sK0,k8_group_4(sK0,A,B),k5_group_4(sK0,C))
| k2_xboole_0(u1_struct_0(A),u1_struct_0(B)) != C
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m1_group_2(B,sK0)
| ~ m1_group_2(A,sK0) ),
inference(resolve,[status(thm)],[c_197,c_1515]) ).
cnf(c_211,negated_conjecture,
( m1_group_2(k8_group_4(sK0,A,B),sK0)
| ~ m1_group_2(B,sK0)
| ~ m1_group_2(A,sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_63,c_65]) ).
cnf(c_1516,negated_conjecture,
( m1_group_2(k8_group_4(sK0,A,B),sK0)
| ~ m1_group_2(B,sK0)
| ~ m1_group_2(A,sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(resolve,[status(thm)],[c_195,c_211]) ).
cnf(c_1517,negated_conjecture,
( m1_group_2(k8_group_4(sK0,A,B),sK0)
| ~ m1_group_2(B,sK0)
| ~ m1_group_2(A,sK0)
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_196,c_1516]) ).
cnf(c_212,negated_conjecture,
( m1_group_2(k8_group_4(sK0,A,B),sK0)
| ~ m1_group_2(B,sK0)
| ~ m1_group_2(A,sK0) ),
inference(resolve,[status(thm)],[c_197,c_1517]) ).
cnf(c_213,negated_conjecture,
( v1_group_1(k8_group_4(sK0,A,B))
| ~ m1_group_2(B,sK0)
| ~ m1_group_2(A,sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_63,c_66]) ).
cnf(c_1518,negated_conjecture,
( v1_group_1(k8_group_4(sK0,A,B))
| ~ m1_group_2(B,sK0)
| ~ m1_group_2(A,sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(resolve,[status(thm)],[c_195,c_213]) ).
cnf(c_1519,negated_conjecture,
( v1_group_1(k8_group_4(sK0,A,B))
| ~ m1_group_2(B,sK0)
| ~ m1_group_2(A,sK0)
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_196,c_1518]) ).
cnf(c_214,negated_conjecture,
( v1_group_1(k8_group_4(sK0,A,B))
| ~ m1_group_2(B,sK0)
| ~ m1_group_2(A,sK0) ),
inference(resolve,[status(thm)],[c_197,c_1519]) ).
cnf(c_215,negated_conjecture,
( m1_group_2(k5_group_4(sK0,A),sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_63,c_67]) ).
cnf(c_1520,negated_conjecture,
( m1_group_2(k5_group_4(sK0,A),sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(resolve,[status(thm)],[c_195,c_215]) ).
cnf(c_1521,negated_conjecture,
( m1_group_2(k5_group_4(sK0,A),sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_196,c_1520]) ).
cnf(c_216,negated_conjecture,
( m1_group_2(k5_group_4(sK0,A),sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_197,c_1521]) ).
cnf(c_217,negated_conjecture,
( v1_group_1(k5_group_4(sK0,A))
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_63,c_68]) ).
cnf(c_1522,negated_conjecture,
( v1_group_1(k5_group_4(sK0,A))
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(resolve,[status(thm)],[c_195,c_217]) ).
cnf(c_1523,negated_conjecture,
( v1_group_1(k5_group_4(sK0,A))
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_196,c_1522]) ).
cnf(c_218,negated_conjecture,
( v1_group_1(k5_group_4(sK0,A))
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_197,c_1523]) ).
cnf(c_221,negated_conjecture,
( B = A
| ~ r1_group_2(sK0,A,B)
| ~ m1_group_2(B,sK0)
| ~ v1_group_1(B)
| ~ m1_group_2(A,sK0)
| ~ v1_group_1(A)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_63,c_70]) ).
cnf(c_1524,negated_conjecture,
( B = A
| ~ r1_group_2(sK0,A,B)
| ~ m1_group_2(B,sK0)
| ~ v1_group_1(B)
| ~ m1_group_2(A,sK0)
| ~ v1_group_1(A)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(resolve,[status(thm)],[c_195,c_221]) ).
cnf(c_1525,negated_conjecture,
( B = A
| ~ r1_group_2(sK0,A,B)
| ~ m1_group_2(B,sK0)
| ~ v1_group_1(B)
| ~ m1_group_2(A,sK0)
| ~ v1_group_1(A)
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_196,c_1524]) ).
cnf(c_222,negated_conjecture,
( B = A
| ~ r1_group_2(sK0,A,B)
| ~ m1_group_2(B,sK0)
| ~ v1_group_1(B)
| ~ m1_group_2(A,sK0)
| ~ v1_group_1(A) ),
inference(resolve,[status(thm)],[c_197,c_1525]) ).
cnf(c_251,negated_conjecture,
m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK2)),
inference(resolve,[status(thm)],[c_93,c_88]) ).
cnf(c_262,negated_conjecture,
m1_subset_1(k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4)),k1_zfmisc_1(u1_struct_0(sK0))),
inference(paramod,[status(thm)],[c_206,c_204]) ).
cnf(c_1526,negated_conjecture,
( k2_funct_2(u1_struct_0(sK0),u1_struct_0(sK2),sK1,A) = k9_relat_1(sK1,A)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK2)) ),
inference(resolve,[status(thm)],[c_203,c_158]) ).
cnf(c_375,negated_conjecture,
k2_funct_2(u1_struct_0(sK0),u1_struct_0(sK2),sK1,A) = k9_relat_1(sK1,A),
inference(resolve,[status(thm)],[c_251,c_1526]) ).
cnf(c_1527,negated_conjecture,
k9_relat_1(sK1,u1_struct_0(k8_group_4(sK0,sK3,sK4))) != k2_funct_2(u1_struct_0(sK0),u1_struct_0(sK2),sK1,u1_struct_0(k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4))))),
inference(paramod,[status(thm)],[c_375,c_208]) ).
cnf(c_379,negated_conjecture,
k9_relat_1(sK1,u1_struct_0(k8_group_4(sK0,sK3,sK4))) != k9_relat_1(sK1,u1_struct_0(k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4))))),
inference(paramod,[status(thm)],[c_375,c_1527]) ).
cnf(c_1528,negated_conjecture,
k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4)) = sK5,
inference(copy,[status(thm)],[c_206]) ).
cnf(c_1529,negated_conjecture,
( r1_group_2(sK0,k8_group_4(sK0,sK3,sK4),k5_group_4(sK0,sK5))
| ~ m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m1_group_2(sK4,sK0)
| ~ m1_group_2(sK3,sK0) ),
inference(resolve,[status(thm)],[c_210,c_1528]) ).
cnf(c_1530,negated_conjecture,
( r1_group_2(sK0,k8_group_4(sK0,sK3,sK4),k5_group_4(sK0,sK5))
| ~ m1_subset_1(k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4)),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m1_group_2(sK4,sK0)
| ~ m1_group_2(sK3,sK0) ),
inference(paramod,[status(thm)],[c_206,c_1529]) ).
cnf(c_1531,negated_conjecture,
( r1_group_2(sK0,k8_group_4(sK0,sK3,sK4),k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4))))
| ~ m1_subset_1(k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4)),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m1_group_2(sK4,sK0)
| ~ m1_group_2(sK3,sK0) ),
inference(paramod,[status(thm)],[c_206,c_1530]) ).
cnf(c_1532,negated_conjecture,
( r1_group_2(sK0,k8_group_4(sK0,sK3,sK4),k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4))))
| ~ m1_subset_1(k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4)),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m1_group_2(sK4,sK0) ),
inference(resolve,[status(thm)],[c_201,c_1531]) ).
cnf(c_1533,negated_conjecture,
( r1_group_2(sK0,k8_group_4(sK0,sK3,sK4),k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4))))
| ~ m1_subset_1(k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4)),k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_202,c_1532]) ).
cnf(c_388,negated_conjecture,
r1_group_2(sK0,k8_group_4(sK0,sK3,sK4),k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4)))),
inference(resolve,[status(thm)],[c_262,c_1533]) ).
cnf(c_394,plain,
( m1_group_2(k8_group_4(sK0,sK3,A),sK0)
| ~ m1_group_2(A,sK0) ),
inference(resolve,[status(thm)],[c_212,c_201]) ).
cnf(c_398,plain,
( v1_group_1(k8_group_4(sK0,sK3,A))
| ~ m1_group_2(A,sK0) ),
inference(resolve,[status(thm)],[c_214,c_201]) ).
cnf(c_460,plain,
v1_group_1(k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4)))),
inference(resolve,[status(thm)],[c_262,c_218]) ).
cnf(c_461,plain,
m1_group_2(k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4))),sK0),
inference(resolve,[status(thm)],[c_262,c_216]) ).
cnf(c_954,plain,
v1_group_1(k8_group_4(sK0,sK3,sK4)),
inference(resolve,[status(thm)],[c_398,c_202]) ).
cnf(c_1049,plain,
m1_group_2(k8_group_4(sK0,sK3,sK4),sK0),
inference(resolve,[status(thm)],[c_394,c_202]) ).
cnf(c_1534,negated_conjecture,
( k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4))) = k8_group_4(sK0,sK3,sK4)
| ~ m1_group_2(k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4))),sK0)
| ~ v1_group_1(k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4))))
| ~ m1_group_2(k8_group_4(sK0,sK3,sK4),sK0)
| ~ v1_group_1(k8_group_4(sK0,sK3,sK4)) ),
inference(resolve,[status(thm)],[c_388,c_222]) ).
cnf(c_1535,negated_conjecture,
( k8_group_4(sK0,sK3,sK4) = k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4)))
| ~ m1_group_2(k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4))),sK0)
| ~ v1_group_1(k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4))))
| ~ m1_group_2(k8_group_4(sK0,sK3,sK4),sK0)
| ~ v1_group_1(k8_group_4(sK0,sK3,sK4)) ),
inference(copy,[status(thm)],[c_1534]) ).
cnf(c_1536,negated_conjecture,
( k8_group_4(sK0,sK3,sK4) = k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4)))
| ~ m1_group_2(k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4))),sK0)
| ~ v1_group_1(k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4))))
| ~ m1_group_2(k8_group_4(sK0,sK3,sK4),sK0) ),
inference(resolve,[status(thm)],[c_954,c_1535]) ).
cnf(c_1537,negated_conjecture,
( k8_group_4(sK0,sK3,sK4) = k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4)))
| ~ m1_group_2(k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4))),sK0)
| ~ v1_group_1(k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4)))) ),
inference(resolve,[status(thm)],[c_1049,c_1536]) ).
cnf(c_1538,negated_conjecture,
( k8_group_4(sK0,sK3,sK4) = k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4)))
| ~ m1_group_2(k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4))),sK0) ),
inference(resolve,[status(thm)],[c_460,c_1537]) ).
cnf(c_1432,negated_conjecture,
k8_group_4(sK0,sK3,sK4) = k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4))),
inference(resolve,[status(thm)],[c_461,c_1538]) ).
cnf(c_1539,negated_conjecture,
k9_relat_1(sK1,u1_struct_0(k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4))))) != k9_relat_1(sK1,u1_struct_0(k5_group_4(sK0,k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4))))),
inference(paramod,[status(thm)],[c_1432,c_379]) ).
cnf(c_1512,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_1539]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP640+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n016.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Fri Sep 25 15:22:30 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.35 % Process 2739870 was started by sandbox2 on n016,
% 0.10/0.35 % Fri Sep 25 15:22:30 2026
% 0.10/0.35 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.13/0.37
% 0.13/0.37 % From the command line: assign(max_seconds, 300).
% 0.13/0.49
% 0.13/0.49 % SZS status Theorem for theBenchmark
% 0.13/0.49
% 0.13/0.49 % Proof 1 at 0.08 (+ 0.02) seconds.
% 0.13/0.49 % Length of proof is 56.
% 0.13/0.49 % Level of proof is 7.
% 0.13/0.49 % Maximum clause weight is 56.000.
% 0.13/0.49 % Given clauses 406.
% 0.13/0.49
% 0.13/0.49 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------