%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP645+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 : n010.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:38 AM UTC 2026
% Result : Theorem 0.55s 0.47s
% Output : CNFRefutation 0.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 8
% Syntax : Number of formulae : 127 ( 37 unt; 0 def)
% Number of atoms : 493 ( 85 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 650 ( 284 ~; 297 |; 53 &)
% ( 1 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-3 aty)
% Number of variables : 116 ( 1 sgn 23 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(commutativity_k3_xboole_0,axiom,
! [A,B] : k3_xboole_0(A,B) = k3_xboole_0(B,A),
file('theBenchmark.p',commutativity_k3_xboole_0) ).
fof(commutativity_k9_group_2,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) )
=> k9_group_2(A,B,C) = k9_group_2(A,C,B) ),
file('theBenchmark.p',commutativity_k9_group_2) ).
fof(d1_latsubgr,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m2_relset_1(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
& v1_funct_2(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
& v1_funct_1(B) )
=> ( B = k1_latsubgr(A)
<=> ! [C] :
( ( m1_group_2(C,A)
& v1_group_1(C) )
=> k1_funct_1(B,C) = u1_struct_0(C) ) ) ) ),
file('theBenchmark.p',d1_latsubgr) ).
fof(dt_k1_latsubgr,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ( m2_relset_1(k1_latsubgr(A),k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
& v1_funct_2(k1_latsubgr(A),k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
& v1_funct_1(k1_latsubgr(A)) ) ),
file('theBenchmark.p',dt_k1_latsubgr) ).
fof(dt_k9_group_2,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(k9_group_2(A,B,C),A)
& v1_group_1(k9_group_2(A,B,C)) ) ),
file('theBenchmark.p',dt_k9_group_2) ).
fof(idempotence_k3_xboole_0,axiom,
! [A,B] : k3_xboole_0(A,A) = A,
file('theBenchmark.p',idempotence_k3_xboole_0) ).
fof(t23_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)
& v1_group_1(B) )
=> ! [C] :
( ( m1_group_2(C,A)
& v1_group_1(C) )
=> u1_struct_0(k9_group_2(A,B,C)) = k3_xboole_0(k1_funct_1(k1_latsubgr(A),B),k1_funct_1(k1_latsubgr(A),C)) ) ) ),
file('theBenchmark.p',t23_latsubgr) ).
fof(t24_latsubgr,conjecture,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m1_group_2(B,A)
& v1_group_1(B) )
=> ! [C] :
( ( m1_group_2(C,A)
& v1_group_1(C) )
=> k1_funct_1(k1_latsubgr(A),k9_group_2(A,B,C)) = k3_xboole_0(k1_funct_1(k1_latsubgr(A),B),k1_funct_1(k1_latsubgr(A),C)) ) ) ),
file('theBenchmark.p',t24_latsubgr) ).
fof(t24_latsubgr_neg,negated_conjecture,
~ ! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m1_group_2(B,A)
& v1_group_1(B) )
=> ! [C] :
( ( m1_group_2(C,A)
& v1_group_1(C) )
=> k1_funct_1(k1_latsubgr(A),k9_group_2(A,B,C)) = k3_xboole_0(k1_funct_1(k1_latsubgr(A),B),k1_funct_1(k1_latsubgr(A),C)) ) ) ),
inference(assume_negation,[status(cth)],[t24_latsubgr]) ).
fof(nnf_61,plain,
? [A] :
( ? [B] :
( ? [C] :
( k3_xboole_0(k1_funct_1(k1_latsubgr(A),B),k1_funct_1(k1_latsubgr(A),C)) != k1_funct_1(k1_latsubgr(A),k9_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(fof_nnf,[status(thm)],[t24_latsubgr_neg]) ).
fof(sk_t24_latsubgr_neg,plain,
( k3_xboole_0(k1_funct_1(k1_latsubgr(sK0),sK1),k1_funct_1(k1_latsubgr(sK0),sK2)) != k1_funct_1(k1_latsubgr(sK0),k9_group_2(sK0,sK1,sK2))
& m1_group_2(sK2,sK0)
& v1_group_1(sK2)
& m1_group_2(sK1,sK0)
& v1_group_1(sK1)
& l1_group_1(sK0)
& v4_group_1(sK0)
& v3_group_1(sK0)
& ~ v3_struct_0(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(A,sK0),skolemize(B,sK1),skolemize(C,sK2)],[nnf_61]) ).
cnf(c_62,negated_conjecture,
v4_group_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t24_latsubgr_neg]) ).
cnf(c_63,plain,
( u1_struct_0(k9_group_2(A,B,C)) = k3_xboole_0(k1_funct_1(k1_latsubgr(A),B),k1_funct_1(k1_latsubgr(A),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)],[t23_latsubgr]) ).
cnf(c_66,plain,
( m1_group_2(k9_group_2(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_k9_group_2]) ).
cnf(c_67,plain,
( v1_group_1(k9_group_2(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_k9_group_2]) ).
cnf(c_70,plain,
( m2_relset_1(k1_latsubgr(A),k1_group_3(A),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_k1_latsubgr]) ).
cnf(c_71,plain,
( v1_funct_2(k1_latsubgr(A),k1_group_3(A),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_k1_latsubgr]) ).
cnf(c_72,plain,
( v1_funct_1(k1_latsubgr(A))
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k1_latsubgr]) ).
cnf(c_76,plain,
( u1_struct_0(C) = k1_funct_1(B,C)
| ~ m1_group_2(C,A)
| ~ v1_group_1(C)
| k1_latsubgr(A) != B
| ~ m2_relset_1(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))
| ~ v1_funct_2(B,k1_group_3(A),k1_zfmisc_1(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(clausify,[status(thm)],[d1_latsubgr]) ).
cnf(c_77,plain,
( k9_group_2(A,C,B) = k9_group_2(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)],[commutativity_k9_group_2]) ).
cnf(c_78,negated_conjecture,
( v1_funct_1(k1_latsubgr(sK0))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_62,c_72]) ).
cnf(c_82,negated_conjecture,
( u1_struct_0(B) = k1_funct_1(A,B)
| ~ m1_group_2(B,sK0)
| ~ v1_group_1(B)
| k1_latsubgr(sK0) != A
| ~ m2_relset_1(A,k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_funct_2(A,k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_funct_1(A)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_62,c_76]) ).
cnf(c_104,negated_conjecture,
( k9_group_2(sK0,B,A) = k9_group_2(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_62,c_77]) ).
cnf(c_105,negated_conjecture,
( v1_funct_2(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_62,c_71]) ).
cnf(c_106,negated_conjecture,
( m2_relset_1(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_62,c_70]) ).
cnf(c_109,negated_conjecture,
( v1_group_1(k9_group_2(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_62,c_67]) ).
cnf(c_110,negated_conjecture,
( m1_group_2(k9_group_2(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_62,c_66]) ).
cnf(c_113,negated_conjecture,
( u1_struct_0(k9_group_2(sK0,A,B)) = k3_xboole_0(k1_funct_1(k1_latsubgr(sK0),A),k1_funct_1(k1_latsubgr(sK0),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_62,c_63]) ).
cnf(c_114,negated_conjecture,
( k3_xboole_0(k1_funct_1(k1_latsubgr(sK0),A),k1_funct_1(k1_latsubgr(sK0),B)) = u1_struct_0(k9_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(copy,[status(thm)],[c_113]) ).
cnf(c_115,negated_conjecture,
k3_xboole_0(k1_funct_1(k1_latsubgr(sK0),sK1),k1_funct_1(k1_latsubgr(sK0),sK2)) != k1_funct_1(k1_latsubgr(sK0),k9_group_2(sK0,sK1,sK2)),
inference(split_conjunct,[status(thm)],[sk_t24_latsubgr_neg]) ).
cnf(c_116,negated_conjecture,
m1_group_2(sK2,sK0),
inference(split_conjunct,[status(thm)],[sk_t24_latsubgr_neg]) ).
cnf(c_117,negated_conjecture,
v1_group_1(sK2),
inference(split_conjunct,[status(thm)],[sk_t24_latsubgr_neg]) ).
cnf(c_118,negated_conjecture,
m1_group_2(sK1,sK0),
inference(split_conjunct,[status(thm)],[sk_t24_latsubgr_neg]) ).
cnf(c_119,negated_conjecture,
v1_group_1(sK1),
inference(split_conjunct,[status(thm)],[sk_t24_latsubgr_neg]) ).
cnf(c_120,negated_conjecture,
l1_group_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t24_latsubgr_neg]) ).
cnf(c_121,negated_conjecture,
v3_group_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t24_latsubgr_neg]) ).
cnf(c_122,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t24_latsubgr_neg]) ).
cnf(c_143,plain,
k3_xboole_0(A,A) = A,
inference(clausify,[status(thm)],[idempotence_k3_xboole_0]) ).
cnf(c_158,plain,
k3_xboole_0(A,B) = k3_xboole_0(B,A),
inference(clausify,[status(thm)],[commutativity_k3_xboole_0]) ).
cnf(c_162,negated_conjecture,
( u1_struct_0(A) = k1_funct_1(k1_latsubgr(sK0),A)
| ~ m1_group_2(A,sK0)
| ~ v1_group_1(A)
| k1_latsubgr(sK0) != k1_latsubgr(sK0)
| ~ m2_relset_1(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_funct_2(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_78,c_82]) ).
cnf(c_1018,negated_conjecture,
( k1_funct_1(k1_latsubgr(sK0),A) = u1_struct_0(A)
| ~ m1_group_2(A,sK0)
| ~ v1_group_1(A)
| k1_latsubgr(sK0) != k1_latsubgr(sK0)
| ~ m2_relset_1(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_funct_2(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_162]) ).
cnf(c_1019,negated_conjecture,
( k1_funct_1(k1_latsubgr(sK0),A) = u1_struct_0(A)
| ~ m1_group_2(A,sK0)
| ~ v1_group_1(A)
| ~ m2_relset_1(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_funct_2(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_1018]) ).
cnf(c_1020,negated_conjecture,
( k1_funct_1(k1_latsubgr(sK0),A) = u1_struct_0(A)
| ~ m1_group_2(A,sK0)
| ~ v1_group_1(A)
| ~ m2_relset_1(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_funct_2(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_1019]) ).
cnf(c_1021,negated_conjecture,
( k1_funct_1(k1_latsubgr(sK0),A) = u1_struct_0(A)
| ~ m1_group_2(A,sK0)
| ~ v1_group_1(A)
| ~ m2_relset_1(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_funct_2(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_group_1(sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_1020]) ).
cnf(c_1022,negated_conjecture,
( k1_funct_1(k1_latsubgr(sK0),A) = u1_struct_0(A)
| ~ m1_group_2(A,sK0)
| ~ v1_group_1(A)
| ~ m2_relset_1(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_funct_2(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_1021]) ).
cnf(c_1023,negated_conjecture,
( k1_funct_1(k1_latsubgr(sK0),A) = u1_struct_0(A)
| ~ m1_group_2(A,sK0)
| ~ v1_group_1(A)
| ~ m2_relset_1(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_funct_2(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(resolve,[status(thm)],[c_122,c_1022]) ).
cnf(c_1024,negated_conjecture,
( k1_funct_1(k1_latsubgr(sK0),A) = u1_struct_0(A)
| ~ m1_group_2(A,sK0)
| ~ v1_group_1(A)
| ~ m2_relset_1(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_funct_2(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_121,c_1023]) ).
cnf(c_163,negated_conjecture,
( k1_funct_1(k1_latsubgr(sK0),A) = u1_struct_0(A)
| ~ m1_group_2(A,sK0)
| ~ v1_group_1(A)
| ~ m2_relset_1(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_funct_2(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_120,c_1024]) ).
cnf(c_1025,plain,
( v1_group_1(k9_group_2(sK0,A,A))
| ~ m1_group_2(A,sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(factor,[status(thm)],[c_109]) ).
cnf(c_1026,negated_conjecture,
( v1_group_1(k9_group_2(sK0,A,A))
| ~ m1_group_2(A,sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(resolve,[status(thm)],[c_122,c_1025]) ).
cnf(c_1027,negated_conjecture,
( v1_group_1(k9_group_2(sK0,A,A))
| ~ m1_group_2(A,sK0)
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_121,c_1026]) ).
cnf(c_248,negated_conjecture,
( v1_group_1(k9_group_2(sK0,A,A))
| ~ m1_group_2(A,sK0) ),
inference(resolve,[status(thm)],[c_120,c_1027]) ).
cnf(c_1028,plain,
( m1_group_2(k9_group_2(sK0,A,A),sK0)
| ~ m1_group_2(A,sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(factor,[status(thm)],[c_110]) ).
cnf(c_1029,negated_conjecture,
( m1_group_2(k9_group_2(sK0,A,A),sK0)
| ~ m1_group_2(A,sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(resolve,[status(thm)],[c_122,c_1028]) ).
cnf(c_1030,negated_conjecture,
( m1_group_2(k9_group_2(sK0,A,A),sK0)
| ~ m1_group_2(A,sK0)
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_121,c_1029]) ).
cnf(c_249,negated_conjecture,
( m1_group_2(k9_group_2(sK0,A,A),sK0)
| ~ m1_group_2(A,sK0) ),
inference(resolve,[status(thm)],[c_120,c_1030]) ).
cnf(c_1031,plain,
( k3_xboole_0(k1_funct_1(k1_latsubgr(sK0),A),k1_funct_1(k1_latsubgr(sK0),A)) = u1_struct_0(k9_group_2(sK0,A,A))
| ~ m1_group_2(A,sK0)
| ~ m1_group_2(A,sK0)
| ~ v1_group_1(A)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(factor,[status(thm)],[c_114]) ).
cnf(c_1032,plain,
( k1_funct_1(k1_latsubgr(sK0),A) = u1_struct_0(k9_group_2(sK0,A,A))
| ~ m1_group_2(A,sK0)
| ~ m1_group_2(A,sK0)
| ~ v1_group_1(A)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(paramod,[status(thm)],[c_143,c_1031]) ).
cnf(c_1033,plain,
( u1_struct_0(k9_group_2(sK0,A,A)) = k1_funct_1(k1_latsubgr(sK0),A)
| ~ m1_group_2(A,sK0)
| ~ m1_group_2(A,sK0)
| ~ v1_group_1(A)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_1032]) ).
cnf(c_1034,plain,
( u1_struct_0(k9_group_2(sK0,A,A)) = k1_funct_1(k1_latsubgr(sK0),A)
| ~ m1_group_2(A,sK0)
| ~ v1_group_1(A)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_1033]) ).
cnf(c_1035,negated_conjecture,
( u1_struct_0(k9_group_2(sK0,A,A)) = k1_funct_1(k1_latsubgr(sK0),A)
| ~ m1_group_2(A,sK0)
| ~ v1_group_1(A)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(resolve,[status(thm)],[c_122,c_1034]) ).
cnf(c_1036,negated_conjecture,
( u1_struct_0(k9_group_2(sK0,A,A)) = k1_funct_1(k1_latsubgr(sK0),A)
| ~ m1_group_2(A,sK0)
| ~ v1_group_1(A)
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_121,c_1035]) ).
cnf(c_251,negated_conjecture,
( u1_struct_0(k9_group_2(sK0,A,A)) = k1_funct_1(k1_latsubgr(sK0),A)
| ~ m1_group_2(A,sK0)
| ~ v1_group_1(A) ),
inference(resolve,[status(thm)],[c_120,c_1036]) ).
cnf(c_1037,negated_conjecture,
( k3_xboole_0(k1_funct_1(k1_latsubgr(sK0),A),k1_funct_1(k1_latsubgr(sK0),B)) = u1_struct_0(k9_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_122,c_114]) ).
cnf(c_1038,negated_conjecture,
( k3_xboole_0(k1_funct_1(k1_latsubgr(sK0),A),k1_funct_1(k1_latsubgr(sK0),B)) = u1_struct_0(k9_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_121,c_1037]) ).
cnf(c_252,negated_conjecture,
( k3_xboole_0(k1_funct_1(k1_latsubgr(sK0),A),k1_funct_1(k1_latsubgr(sK0),B)) = u1_struct_0(k9_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_120,c_1038]) ).
cnf(c_1039,negated_conjecture,
( m1_group_2(k9_group_2(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_122,c_110]) ).
cnf(c_1040,negated_conjecture,
( m1_group_2(k9_group_2(sK0,A,B),sK0)
| ~ m1_group_2(B,sK0)
| ~ m1_group_2(A,sK0)
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_121,c_1039]) ).
cnf(c_255,negated_conjecture,
( m1_group_2(k9_group_2(sK0,A,B),sK0)
| ~ m1_group_2(B,sK0)
| ~ m1_group_2(A,sK0) ),
inference(resolve,[status(thm)],[c_120,c_1040]) ).
cnf(c_1041,negated_conjecture,
( v1_group_1(k9_group_2(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_122,c_109]) ).
cnf(c_1042,negated_conjecture,
( v1_group_1(k9_group_2(sK0,A,B))
| ~ m1_group_2(B,sK0)
| ~ m1_group_2(A,sK0)
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_121,c_1041]) ).
cnf(c_256,negated_conjecture,
( v1_group_1(k9_group_2(sK0,A,B))
| ~ m1_group_2(B,sK0)
| ~ m1_group_2(A,sK0) ),
inference(resolve,[status(thm)],[c_120,c_1042]) ).
cnf(c_1043,negated_conjecture,
( m2_relset_1(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(resolve,[status(thm)],[c_122,c_106]) ).
cnf(c_1044,negated_conjecture,
( m2_relset_1(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_121,c_1043]) ).
cnf(c_259,negated_conjecture,
m2_relset_1(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0))),
inference(resolve,[status(thm)],[c_120,c_1044]) ).
cnf(c_1045,negated_conjecture,
( v1_funct_2(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(resolve,[status(thm)],[c_122,c_105]) ).
cnf(c_1046,negated_conjecture,
( v1_funct_2(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_121,c_1045]) ).
cnf(c_260,negated_conjecture,
v1_funct_2(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0))),
inference(resolve,[status(thm)],[c_120,c_1046]) ).
cnf(c_1047,negated_conjecture,
( k9_group_2(sK0,B,A) = k9_group_2(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_122,c_104]) ).
cnf(c_1048,negated_conjecture,
( k9_group_2(sK0,B,A) = k9_group_2(sK0,A,B)
| ~ m1_group_2(B,sK0)
| ~ m1_group_2(A,sK0)
| ~ l1_group_1(sK0) ),
inference(resolve,[status(thm)],[c_121,c_1047]) ).
cnf(c_261,negated_conjecture,
( k9_group_2(sK0,B,A) = k9_group_2(sK0,A,B)
| ~ m1_group_2(B,sK0)
| ~ m1_group_2(A,sK0) ),
inference(resolve,[status(thm)],[c_120,c_1048]) ).
cnf(c_1049,negated_conjecture,
( k1_funct_1(k1_latsubgr(sK0),A) = u1_struct_0(A)
| ~ m1_group_2(A,sK0)
| ~ v1_group_1(A)
| ~ m2_relset_1(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_260,c_163]) ).
cnf(c_268,negated_conjecture,
( k1_funct_1(k1_latsubgr(sK0),A) = u1_struct_0(A)
| ~ m1_group_2(A,sK0)
| ~ v1_group_1(A) ),
inference(resolve,[status(thm)],[c_259,c_1049]) ).
cnf(c_317,plain,
v1_group_1(k9_group_2(sK0,sK2,sK2)),
inference(resolve,[status(thm)],[c_248,c_116]) ).
cnf(c_319,plain,
m1_group_2(k9_group_2(sK0,sK2,sK2),sK0),
inference(resolve,[status(thm)],[c_249,c_116]) ).
cnf(c_1050,negated_conjecture,
( u1_struct_0(k9_group_2(sK0,sK2,sK2)) = k1_funct_1(k1_latsubgr(sK0),sK2)
| ~ v1_group_1(sK2) ),
inference(resolve,[status(thm)],[c_251,c_116]) ).
cnf(c_323,negated_conjecture,
u1_struct_0(k9_group_2(sK0,sK2,sK2)) = k1_funct_1(k1_latsubgr(sK0),sK2),
inference(resolve,[status(thm)],[c_117,c_1050]) ).
cnf(c_1051,negated_conjecture,
( k3_xboole_0(k1_funct_1(k1_latsubgr(sK0),A),k1_funct_1(k1_latsubgr(sK0),sK1)) = u1_struct_0(k9_group_2(sK0,A,sK1))
| ~ v1_group_1(sK1)
| ~ m1_group_2(A,sK0)
| ~ v1_group_1(A) ),
inference(resolve,[status(thm)],[c_252,c_118]) ).
cnf(c_326,negated_conjecture,
( k3_xboole_0(k1_funct_1(k1_latsubgr(sK0),A),k1_funct_1(k1_latsubgr(sK0),sK1)) = u1_struct_0(k9_group_2(sK0,A,sK1))
| ~ m1_group_2(A,sK0)
| ~ v1_group_1(A) ),
inference(resolve,[status(thm)],[c_119,c_1051]) ).
cnf(c_332,plain,
( m1_group_2(k9_group_2(sK0,sK1,A),sK0)
| ~ m1_group_2(A,sK0) ),
inference(resolve,[status(thm)],[c_255,c_118]) ).
cnf(c_336,plain,
( v1_group_1(k9_group_2(sK0,sK1,A))
| ~ m1_group_2(A,sK0) ),
inference(resolve,[status(thm)],[c_256,c_118]) ).
cnf(c_1052,negated_conjecture,
( k9_group_2(sK0,A,sK1) = k9_group_2(sK0,sK1,A)
| ~ m1_group_2(A,sK0) ),
inference(resolve,[status(thm)],[c_261,c_118]) ).
cnf(c_350,negated_conjecture,
( k9_group_2(sK0,sK1,A) = k9_group_2(sK0,A,sK1)
| ~ m1_group_2(A,sK0) ),
inference(copy,[status(thm)],[c_1052]) ).
cnf(c_1053,negated_conjecture,
( k1_funct_1(k1_latsubgr(sK0),sK1) = u1_struct_0(sK1)
| ~ v1_group_1(sK1) ),
inference(resolve,[status(thm)],[c_268,c_118]) ).
cnf(c_352,negated_conjecture,
k1_funct_1(k1_latsubgr(sK0),sK1) = u1_struct_0(sK1),
inference(resolve,[status(thm)],[c_119,c_1053]) ).
cnf(c_1054,negated_conjecture,
( k1_funct_1(k1_latsubgr(sK0),sK2) = u1_struct_0(sK2)
| ~ v1_group_1(sK2) ),
inference(resolve,[status(thm)],[c_268,c_116]) ).
cnf(c_353,negated_conjecture,
k1_funct_1(k1_latsubgr(sK0),sK2) = u1_struct_0(sK2),
inference(resolve,[status(thm)],[c_117,c_1054]) ).
cnf(c_354,negated_conjecture,
( k3_xboole_0(k1_funct_1(k1_latsubgr(sK0),A),u1_struct_0(sK1)) = u1_struct_0(k9_group_2(sK0,A,sK1))
| ~ m1_group_2(A,sK0)
| ~ v1_group_1(A) ),
inference(paramod,[status(thm)],[c_352,c_326]) ).
cnf(c_1055,negated_conjecture,
k3_xboole_0(u1_struct_0(sK1),k1_funct_1(k1_latsubgr(sK0),sK2)) != k1_funct_1(k1_latsubgr(sK0),k9_group_2(sK0,sK1,sK2)),
inference(paramod,[status(thm)],[c_352,c_115]) ).
cnf(c_357,negated_conjecture,
k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)) != k1_funct_1(k1_latsubgr(sK0),k9_group_2(sK0,sK1,sK2)),
inference(paramod,[status(thm)],[c_353,c_1055]) ).
cnf(c_360,negated_conjecture,
u1_struct_0(k9_group_2(sK0,sK2,sK2)) = u1_struct_0(sK2),
inference(paramod,[status(thm)],[c_353,c_323]) ).
cnf(c_1056,negated_conjecture,
( k1_funct_1(k1_latsubgr(sK0),k9_group_2(sK0,sK2,sK2)) = u1_struct_0(k9_group_2(sK0,sK2,sK2))
| ~ v1_group_1(k9_group_2(sK0,sK2,sK2)) ),
inference(resolve,[status(thm)],[c_319,c_268]) ).
cnf(c_1057,negated_conjecture,
( k1_funct_1(k1_latsubgr(sK0),k9_group_2(sK0,sK2,sK2)) = u1_struct_0(sK2)
| ~ v1_group_1(k9_group_2(sK0,sK2,sK2)) ),
inference(paramod,[status(thm)],[c_360,c_1056]) ).
cnf(c_463,negated_conjecture,
k1_funct_1(k1_latsubgr(sK0),k9_group_2(sK0,sK2,sK2)) = u1_struct_0(sK2),
inference(resolve,[status(thm)],[c_317,c_1057]) ).
cnf(c_536,plain,
v1_group_1(k9_group_2(sK0,sK1,sK2)),
inference(resolve,[status(thm)],[c_336,c_116]) ).
cnf(c_678,plain,
m1_group_2(k9_group_2(sK0,sK1,sK2),sK0),
inference(resolve,[status(thm)],[c_332,c_116]) ).
cnf(c_1058,negated_conjecture,
( k1_funct_1(k1_latsubgr(sK0),k9_group_2(sK0,sK1,sK2)) = u1_struct_0(k9_group_2(sK0,sK1,sK2))
| ~ v1_group_1(k9_group_2(sK0,sK1,sK2)) ),
inference(resolve,[status(thm)],[c_678,c_268]) ).
cnf(c_692,negated_conjecture,
k1_funct_1(k1_latsubgr(sK0),k9_group_2(sK0,sK1,sK2)) = u1_struct_0(k9_group_2(sK0,sK1,sK2)),
inference(resolve,[status(thm)],[c_536,c_1058]) ).
cnf(c_713,negated_conjecture,
k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)) != u1_struct_0(k9_group_2(sK0,sK1,sK2)),
inference(paramod,[status(thm)],[c_692,c_357]) ).
cnf(c_1059,plain,
k9_group_2(sK0,sK1,k9_group_2(sK0,sK2,sK2)) = k9_group_2(sK0,k9_group_2(sK0,sK2,sK2),sK1),
inference(resolve,[status(thm)],[c_350,c_319]) ).
cnf(c_971,plain,
k9_group_2(sK0,k9_group_2(sK0,sK2,sK2),sK1) = k9_group_2(sK0,sK1,k9_group_2(sK0,sK2,sK2)),
inference(copy,[status(thm)],[c_1059]) ).
cnf(c_1060,negated_conjecture,
k9_group_2(sK0,sK1,sK2) = k9_group_2(sK0,sK2,sK1),
inference(resolve,[status(thm)],[c_350,c_116]) ).
cnf(c_974,negated_conjecture,
k9_group_2(sK0,sK2,sK1) = k9_group_2(sK0,sK1,sK2),
inference(copy,[status(thm)],[c_1060]) ).
cnf(c_1061,plain,
( k3_xboole_0(k1_funct_1(k1_latsubgr(sK0),k9_group_2(sK0,sK2,sK2)),u1_struct_0(sK1)) = u1_struct_0(k9_group_2(sK0,k9_group_2(sK0,sK2,sK2),sK1))
| ~ v1_group_1(k9_group_2(sK0,sK2,sK2)) ),
inference(resolve,[status(thm)],[c_354,c_319]) ).
cnf(c_1062,plain,
( k3_xboole_0(u1_struct_0(sK2),u1_struct_0(sK1)) = u1_struct_0(k9_group_2(sK0,k9_group_2(sK0,sK2,sK2),sK1))
| ~ v1_group_1(k9_group_2(sK0,sK2,sK2)) ),
inference(paramod,[status(thm)],[c_463,c_1061]) ).
cnf(c_1063,plain,
( k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)) = u1_struct_0(k9_group_2(sK0,k9_group_2(sK0,sK2,sK2),sK1))
| ~ v1_group_1(k9_group_2(sK0,sK2,sK2)) ),
inference(paramod,[status(thm)],[c_158,c_1062]) ).
cnf(c_1064,plain,
( k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)) = u1_struct_0(k9_group_2(sK0,sK1,k9_group_2(sK0,sK2,sK2)))
| ~ v1_group_1(k9_group_2(sK0,sK2,sK2)) ),
inference(paramod,[status(thm)],[c_971,c_1063]) ).
cnf(c_1013,plain,
k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)) = u1_struct_0(k9_group_2(sK0,sK1,k9_group_2(sK0,sK2,sK2))),
inference(resolve,[status(thm)],[c_317,c_1064]) ).
cnf(c_1065,negated_conjecture,
( k3_xboole_0(k1_funct_1(k1_latsubgr(sK0),sK2),u1_struct_0(sK1)) = u1_struct_0(k9_group_2(sK0,sK2,sK1))
| ~ v1_group_1(sK2) ),
inference(resolve,[status(thm)],[c_354,c_116]) ).
cnf(c_1066,negated_conjecture,
( k3_xboole_0(u1_struct_0(sK2),u1_struct_0(sK1)) = u1_struct_0(k9_group_2(sK0,sK2,sK1))
| ~ v1_group_1(sK2) ),
inference(paramod,[status(thm)],[c_353,c_1065]) ).
cnf(c_1067,negated_conjecture,
( k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)) = u1_struct_0(k9_group_2(sK0,sK2,sK1))
| ~ v1_group_1(sK2) ),
inference(paramod,[status(thm)],[c_158,c_1066]) ).
cnf(c_1068,negated_conjecture,
( u1_struct_0(k9_group_2(sK0,sK1,k9_group_2(sK0,sK2,sK2))) = u1_struct_0(k9_group_2(sK0,sK2,sK1))
| ~ v1_group_1(sK2) ),
inference(paramod,[status(thm)],[c_1013,c_1067]) ).
cnf(c_1069,negated_conjecture,
( u1_struct_0(k9_group_2(sK0,sK1,k9_group_2(sK0,sK2,sK2))) = u1_struct_0(k9_group_2(sK0,sK1,sK2))
| ~ v1_group_1(sK2) ),
inference(paramod,[status(thm)],[c_974,c_1068]) ).
cnf(c_1016,negated_conjecture,
u1_struct_0(k9_group_2(sK0,sK1,k9_group_2(sK0,sK2,sK2))) = u1_struct_0(k9_group_2(sK0,sK1,sK2)),
inference(resolve,[status(thm)],[c_117,c_1069]) ).
cnf(c_1070,negated_conjecture,
u1_struct_0(k9_group_2(sK0,sK1,k9_group_2(sK0,sK2,sK2))) != u1_struct_0(k9_group_2(sK0,sK1,sK2)),
inference(paramod,[status(thm)],[c_1013,c_713]) ).
cnf(c_1071,negated_conjecture,
u1_struct_0(k9_group_2(sK0,sK1,sK2)) != u1_struct_0(k9_group_2(sK0,sK1,sK2)),
inference(paramod,[status(thm)],[c_1016,c_1070]) ).
cnf(c_1017,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_1071]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP645+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n010.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 15:21:50 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 1084385 was started by sandbox on n010,
% 0.09/0.36 % Fri Sep 25 15:21:50 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.38
% 0.09/0.38 % From the command line: assign(max_seconds, 300).
% 0.55/0.47
% 0.55/0.47 % SZS status Theorem for theBenchmark
% 0.55/0.47
% 0.55/0.47 % Proof 1 at 0.06 (+ 0.02) seconds.
% 0.55/0.47 % Length of proof is 70.
% 0.55/0.47 % Level of proof is 11.
% 0.55/0.47 % Maximum clause weight is 31.000.
% 0.55/0.47 % Given clauses 349.
% 0.55/0.47
% 0.55/0.47 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------