%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : GRP640+1 : TPTP v9.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Jul 24 06:27:43 PM UTC 2025
% Result : Theorem 36.85s 4.95s
% Output : CNFRefutation 36.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 5
% Syntax : Number of formulae : 58 ( 40 unt; 0 def)
% Number of atoms : 196 ( 14 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 217 ( 79 ~; 78 |; 37 &)
% ( 1 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 6 con; 0-4 aty)
% Number of variables : 41 ( 0 sgn 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(t13_latsubgr,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v3_group_1(A)
& v4_group_1(A)
& l1_group_1(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& v3_group_1(B)
& v4_group_1(B)
& l1_group_1(B) )
=> ! [C] :
( m1_group_2(C,A)
=> ! [D] :
( m1_group_2(D,A)
=> ! [E] :
( ( v1_funct_1(E)
& v1_funct_2(E,u1_struct_0(A),u1_struct_0(B))
& m2_relset_1(E,u1_struct_0(A),u1_struct_0(B)) )
=> ! [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('/export/starexec/sandbox/benchmark/theBenchmark.p',t13_latsubgr) ).
fof(t13_latsubgr_negated,plain,
~ ! [A] :
( ( ~ v3_struct_0(A)
& v3_group_1(A)
& v4_group_1(A)
& l1_group_1(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& v3_group_1(B)
& v4_group_1(B)
& l1_group_1(B) )
=> ! [C] :
( m1_group_2(C,A)
=> ! [D] :
( m1_group_2(D,A)
=> ! [E] :
( ( v1_funct_1(E)
& v1_funct_2(E,u1_struct_0(A),u1_struct_0(B))
& m2_relset_1(E,u1_struct_0(A),u1_struct_0(B)) )
=> ! [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(negate_conjecture,[status(cth)],[t13_latsubgr]) ).
cnf(0,plain,
~ v3_struct_0(sK1),
inference(cnf,[status(esa)],[t13_latsubgr_negated]) ).
cnf(l0,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
fof(redefinition_r1_group_2,plain,
! [A,B,C] :
( ( ~ v3_struct_0(A)
& v3_group_1(A)
& v4_group_1(A)
& l1_group_1(A)
& v1_group_1(B)
& m1_group_2(B,A)
& v1_group_1(C)
& m1_group_2(C,A) )
=> ( r1_group_2(A,B,C)
<=> B = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_r1_group_2) ).
cnf(74,plain,
( ~ m1_group_2(X0,X1)
| ~ m1_group_2(X2,X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ v1_group_1(X0)
| ~ v1_group_1(X2)
| ~ r1_group_2(X1,X0,X2)
| v3_struct_0(X1)
| X0 = X2 ),
inference(cnf,[status(esa)],[redefinition_r1_group_2]) ).
cnf(l1,plain,
( ~ m1_group_2(k8_group_4(sK1,sK3,sK4),sK1)
| ~ m1_group_2(k5_group_4(sK1,sK6),sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| ~ v1_group_1(k8_group_4(sK1,sK3,sK4))
| ~ v1_group_1(k5_group_4(sK1,sK6))
| ~ r1_group_2(sK1,k8_group_4(sK1,sK3,sK4),k5_group_4(sK1,sK6))
| v3_struct_0(sK1)
| k8_group_4(sK1,sK3,sK4) = k5_group_4(sK1,sK6) ),
inference(instantiation,[status(thm)],[74]) ).
cnf(1,plain,
v3_group_1(sK1),
inference(cnf,[status(esa)],[t13_latsubgr_negated]) ).
cnf(l85,plain,
v3_group_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(3,plain,
l1_group_1(sK1),
inference(cnf,[status(esa)],[t13_latsubgr_negated]) ).
cnf(l47,plain,
l1_group_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
fof(dt_k5_group_4,plain,
! [A,B] :
( ( ~ v3_struct_0(A)
& v3_group_1(A)
& v4_group_1(A)
& l1_group_1(A)
& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
=> ( v1_group_1(k5_group_4(A,B))
& m1_group_2(k5_group_4(A,B),A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k5_group_4) ).
cnf(77,plain,
( ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| v1_group_1(k5_group_4(X0,X1)) ),
inference(cnf,[status(esa)],[dt_k5_group_4]) ).
cnf(l104,plain,
( ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| ~ m1_subset_1(sK6,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| v1_group_1(k5_group_4(sK1,sK6)) ),
inference(instantiation,[status(thm)],[77]) ).
cnf(2,plain,
v4_group_1(sK1),
inference(cnf,[status(esa)],[t13_latsubgr_negated]) ).
cnf(l127,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(78,plain,
( ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| m1_group_2(k5_group_4(X0,X1),X0)
| v3_struct_0(X0) ),
inference(cnf,[status(esa)],[dt_k5_group_4]) ).
cnf(l2,plain,
( ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| ~ m1_subset_1(sK6,k1_zfmisc_1(u1_struct_0(sK1)))
| m1_group_2(k5_group_4(sK1,sK6),sK1)
| v3_struct_0(sK1) ),
inference(instantiation,[status(thm)],[78]) ).
cnf(l119,plain,
v3_group_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l106,plain,
l1_group_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l4,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l82,plain,
l1_group_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
fof(dt_k8_group_4,plain,
! [A,B,C] :
( ( ~ v3_struct_0(A)
& v3_group_1(A)
& v4_group_1(A)
& l1_group_1(A)
& m1_group_2(B,A)
& m1_group_2(C,A) )
=> ( v1_group_1(k8_group_4(A,B,C))
& m1_group_2(k8_group_4(A,B,C),A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k8_group_4) ).
cnf(79,plain,
( ~ m1_group_2(X0,X1)
| ~ m1_group_2(X2,X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X1)
| v1_group_1(k8_group_4(X1,X0,X2)) ),
inference(cnf,[status(esa)],[dt_k8_group_4]) ).
cnf(l101,plain,
( ~ m1_group_2(sK3,sK1)
| ~ m1_group_2(sK4,sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| v3_struct_0(sK1)
| v1_group_1(k8_group_4(sK1,sK3,sK4)) ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l6,plain,
v3_group_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l396,plain,
l1_group_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
fof(t4_latsubgr,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v3_group_1(A)
& v4_group_1(A)
& l1_group_1(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('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_latsubgr) ).
cnf(89,plain,
( ~ m1_group_2(X0,X1)
| ~ m1_group_2(X2,X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
| X3 != k2_xboole_0(u1_struct_0(X0),u1_struct_0(X2))
| v3_struct_0(X1)
| r1_group_2(X1,k8_group_4(X1,X0,X2),k5_group_4(X1,X3)) ),
inference(cnf,[status(esa)],[t4_latsubgr]) ).
cnf(l283,plain,
( ~ m1_group_2(sK3,sK1)
| ~ m1_group_2(sK4,sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| ~ m1_subset_1(sK6,k1_zfmisc_1(u1_struct_0(sK1)))
| sK6 != k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4))
| v3_struct_0(sK1)
| r1_group_2(sK1,k8_group_4(sK1,sK3,sK4),k5_group_4(sK1,sK6)) ),
inference(instantiation,[status(thm)],[89]) ).
cnf(8,plain,
m1_group_2(sK3,sK1),
inference(cnf,[status(esa)],[t13_latsubgr_negated]) ).
cnf(l229,plain,
m1_group_2(sK3,sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(l307,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l318,plain,
v3_group_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(13,plain,
m1_subset_1(sK6,k1_zfmisc_1(u1_struct_0(sK1))),
inference(cnf,[status(esa)],[t13_latsubgr_negated]) ).
cnf(l72,plain,
m1_subset_1(sK6,k1_zfmisc_1(u1_struct_0(sK1))),
inference(instantiation,[status(thm)],[13]) ).
cnf(l296,plain,
l1_group_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(9,plain,
m1_group_2(sK4,sK1),
inference(cnf,[status(esa)],[t13_latsubgr_negated]) ).
cnf(l286,plain,
m1_group_2(sK4,sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(l312,plain,
v3_group_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l112,plain,
m1_subset_1(sK6,k1_zfmisc_1(u1_struct_0(sK1))),
inference(instantiation,[status(thm)],[13]) ).
cnf(15,plain,
k2_funct_2(u1_struct_0(sK1),u1_struct_0(sK2),sK5,u1_struct_0(k8_group_4(sK1,sK3,sK4))) != k2_funct_2(u1_struct_0(sK1),u1_struct_0(sK2),sK5,u1_struct_0(k5_group_4(sK1,sK6))),
inference(cnf,[status(esa)],[t13_latsubgr_negated]) ).
cnf(l364,plain,
k2_funct_2(u1_struct_0(sK1),u1_struct_0(sK2),sK5,u1_struct_0(k8_group_4(sK1,sK3,sK4))) != k2_funct_2(u1_struct_0(sK1),u1_struct_0(sK2),sK5,u1_struct_0(k5_group_4(sK1,sK6))),
inference(instantiation,[status(thm)],[15]) ).
cnf(l123,plain,
m1_group_2(sK4,sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(l393,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(80,plain,
( ~ m1_group_2(X0,X1)
| ~ m1_group_2(X2,X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| m1_group_2(k8_group_4(X1,X0,X2),X1)
| v3_struct_0(X1) ),
inference(cnf,[status(esa)],[dt_k8_group_4]) ).
cnf(l3,plain,
( ~ m1_group_2(sK3,sK1)
| ~ m1_group_2(sK4,sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| m1_group_2(k8_group_4(sK1,sK3,sK4),sK1)
| v3_struct_0(sK1) ),
inference(instantiation,[status(thm)],[80]) ).
cnf(l102,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l308,plain,
m1_subset_1(sK6,k1_zfmisc_1(u1_struct_0(sK1))),
inference(instantiation,[status(thm)],[13]) ).
cnf(l5,plain,
m1_group_2(sK3,sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(14,plain,
sK6 = k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4)),
inference(cnf,[status(esa)],[t13_latsubgr_negated]) ).
cnf(l297,plain,
sK6 = k2_xboole_0(u1_struct_0(sK3),u1_struct_0(sK4)),
inference(instantiation,[status(thm)],[14]) ).
cnf(l302,plain,
m1_group_2(sK3,sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(l23,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l10,plain,
m1_group_2(sK4,sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(l22,plain,
v3_group_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l37,plain,
l1_group_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l85,l47,l104,l127,l2,l119,l106,l4,l82,l101,l6,l396,l283,l229,l307,l318,l72,l296,l286,l312,l112,l364,l123,l393,l3,l102,l308,l5,l297,l302,l23,l10,l22,l37]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP640+1 : TPTP v9.0.0. Released v3.4.0.
% 0.03/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n017.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Sun Jul 20 16:18:49 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.34 % launching worker at depth: 9
% 0.19/0.38 % launching worker at depth: 10
% 3.34/0.75 % launching worker at depth: 11
% 36.85/4.95 % SZS status Theorem for theBenchmark
% 36.85/4.95 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------