%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP643+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n015.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 : Fri Sep 25 01:27:47 PM UTC 2026
% Result : Theorem 75.80s 10.20s
% Output : Proof 75.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 12
% Syntax : Number of formulae : 174 ( 142 unt; 0 def)
% Number of atoms : 329 ( 121 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 268 ( 113 ~; 85 |; 49 &)
% ( 1 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 2 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 13 ( 11 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 8 con; 0-4 aty)
% Number of variables : 194 ( 5 sgn 62 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f45,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_subset_1(C,u1_struct_0(A))
=> ( r2_hidden(C,k1_funct_1(k1_latsubgr(A),B))
<=> r1_rlvect_1(B,C) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t18_latsubgr) ).
fof(f45_nnf,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ~ r1_rlvect_1(B,C)
| r2_hidden(C,k1_funct_1(k1_latsubgr(A),B)) )
& ( r1_rlvect_1(B,C)
| ~ r2_hidden(C,k1_funct_1(k1_latsubgr(A),B)) ) )
| ~ m1_subset_1(C,u1_struct_0(A)) )
| ~ 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(nnf_transformation,[status(thm)],[f45]) ).
fof(f45_sk,plain,
! [A,B,C] :
( ( ( ~ r1_rlvect_1(B,C)
| r2_hidden(C,k1_funct_1(k1_latsubgr(A),B)) )
& ( r1_rlvect_1(B,C)
| ~ r2_hidden(C,k1_funct_1(k1_latsubgr(A),B)) ) )
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ 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(skolemisation,[status(esa)],[f45_nnf]) ).
cnf(c80,plain,
( ~ r1_rlvect_1(X1,X2)
| r2_hidden(X2,k1_funct_1(k1_latsubgr(X0),X1))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(t250,plain,
ifeq(v3_group_1(X1),true,ifeq(v4_group_1(X1),true,ifeq(l1_group_1(X1),true,ifeq(v1_group_1(X2),true,ifeq(m1_group_2(X2,X1),true,ifeq(m1_subset_1(X3,u1_struct_0(X1)),true,ifeq(r1_rlvect_1(X2,X3),true,or(v3_struct_0(X1),r2_hidden(X3,k1_funct_1(k1_latsubgr(X1),X2))),true),true),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c80]) ).
cnf(t320,plain,
ifeq(v3_group_1(X1),true,ifeq(v4_group_1(X1),true,ifeq(l1_group_1(X1),true,ifeq(v1_group_1(X2),true,ifeq(m1_group_2(X2,X1),true,ifeq(m1_subset_1(X3,u1_struct_0(X1)),true,ifeq(r1_rlvect_1(X2,X3),true,or(v3_struct_0(X1),r2_hidden(X3,k1_funct_1(k1_latsubgr(X1),X2))),true),true),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t250]) ).
fof(f0,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_subset_1(C,u1_struct_0(A))
=> ! [D] :
( m1_subset_1(D,u1_struct_0(A))
=> ( ( r2_hidden(D,k1_funct_1(k1_latsubgr(A),B))
& r2_hidden(C,k1_funct_1(k1_latsubgr(A),B)) )
=> r2_hidden(k1_group_1(A,C,D),k1_funct_1(k1_latsubgr(A),B)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t21_latsubgr) ).
fof(f0_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_subset_1(C,u1_struct_0(A))
=> ! [D] :
( m1_subset_1(D,u1_struct_0(A))
=> ( ( r2_hidden(D,k1_funct_1(k1_latsubgr(A),B))
& r2_hidden(C,k1_funct_1(k1_latsubgr(A),B)) )
=> r2_hidden(k1_group_1(A,C,D),k1_funct_1(k1_latsubgr(A),B)) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f0]) ).
fof(f0_nnf,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( ~ r2_hidden(k1_group_1(A,C,D),k1_funct_1(k1_latsubgr(A),B))
& r2_hidden(D,k1_funct_1(k1_latsubgr(A),B))
& r2_hidden(C,k1_funct_1(k1_latsubgr(A),B))
& m1_subset_1(D,u1_struct_0(A)) )
& m1_subset_1(C,u1_struct_0(A)) )
& 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(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
( ~ r2_hidden(k1_group_1(sk0,sk2,sk3),k1_funct_1(k1_latsubgr(sk0),sk1))
& r2_hidden(sk3,k1_funct_1(k1_latsubgr(sk0),sk1))
& r2_hidden(sk2,k1_funct_1(k1_latsubgr(sk0),sk1))
& m1_subset_1(sk3,u1_struct_0(sk0))
& m1_subset_1(sk2,u1_struct_0(sk0))
& 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(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2,sk3])],[f0_nnf]) ).
cnf(c3,plain,
l1_group_1(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t1,plain,
l1_group_1(sk0) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t420,plain,
l1_group_1(sk0) = true,
inference(orient,[status(thm)],[t1]) ).
cnf(t437,plain,
true = ifeq(v3_group_1(sk0),true,ifeq(v4_group_1(sk0),true,ifeq(true,true,ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(m1_subset_1(X2,u1_struct_0(sk0)),true,ifeq(r1_rlvect_1(X1,X2),true,or(v3_struct_0(sk0),r2_hidden(X2,k1_funct_1(k1_latsubgr(sk0),X1))),true),true),true),true),true),true),true),
inference(cp,[status(thm)],[t320,t420]) ).
cnf(c1,plain,
v3_group_1(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t13,plain,
v3_group_1(sk0) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t569,plain,
v3_group_1(sk0) = true,
inference(orient,[status(thm)],[t13]) ).
cnf(t25875,plain,
true = ifeq(true,true,ifeq(v4_group_1(sk0),true,ifeq(true,true,ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(m1_subset_1(X2,u1_struct_0(sk0)),true,ifeq(r1_rlvect_1(X1,X2),true,or(v3_struct_0(sk0),r2_hidden(X2,k1_funct_1(k1_latsubgr(sk0),X1))),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t437,t569]) ).
cnf(t40,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t258,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t40]) ).
cnf(t25876,plain,
true = ifeq(v4_group_1(sk0),true,ifeq(true,true,ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(m1_subset_1(X2,u1_struct_0(sk0)),true,ifeq(r1_rlvect_1(X1,X2),true,or(v3_struct_0(sk0),r2_hidden(X2,k1_funct_1(k1_latsubgr(sk0),X1))),true),true),true),true),true),true),
inference(step,[status(thm)],[t25875,t258]) ).
cnf(c2,plain,
v4_group_1(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t16,plain,
v4_group_1(sk0) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t582,plain,
v4_group_1(sk0) = true,
inference(orient,[status(thm)],[t16]) ).
cnf(t25877,plain,
true = ifeq(true,true,ifeq(true,true,ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(m1_subset_1(X2,u1_struct_0(sk0)),true,ifeq(r1_rlvect_1(X1,X2),true,or(v3_struct_0(sk0),r2_hidden(X2,k1_funct_1(k1_latsubgr(sk0),X1))),true),true),true),true),true),true),
inference(step,[status(thm)],[t25876,t582]) ).
cnf(t25878,plain,
true = ifeq(true,true,ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(m1_subset_1(X2,u1_struct_0(sk0)),true,ifeq(r1_rlvect_1(X1,X2),true,or(v3_struct_0(sk0),r2_hidden(X2,k1_funct_1(k1_latsubgr(sk0),X1))),true),true),true),true),true),
inference(step,[status(thm)],[t25877,t258]) ).
cnf(t25879,plain,
true = ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(m1_subset_1(X2,u1_struct_0(sk0)),true,ifeq(r1_rlvect_1(X1,X2),true,or(v3_struct_0(sk0),r2_hidden(X2,k1_funct_1(k1_latsubgr(sk0),X1))),true),true),true),true),
inference(step,[status(thm)],[t25878,t258]) ).
cnf(c0,plain,
~ v3_struct_0(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t14,plain,
v3_struct_0(sk0) = false,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t641,plain,
v3_struct_0(sk0) = false,
inference(orient,[status(thm)],[t14]) ).
cnf(t25880,plain,
true = ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(m1_subset_1(X2,u1_struct_0(sk0)),true,ifeq(r1_rlvect_1(X1,X2),true,or(false,r2_hidden(X2,k1_funct_1(k1_latsubgr(sk0),X1))),true),true),true),true),
inference(step,[status(thm)],[t25879,t641]) ).
cnf(t20,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t257,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t20]) ).
cnf(t25881,plain,
true = ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(m1_subset_1(X2,u1_struct_0(sk0)),true,ifeq(r1_rlvect_1(X1,X2),true,r2_hidden(X2,k1_funct_1(k1_latsubgr(sk0),X1)),true),true),true),true),
inference(step,[status(thm)],[t25880,t257]) ).
cnf(t20912,plain,
ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(m1_subset_1(X2,u1_struct_0(sk0)),true,ifeq(r1_rlvect_1(X1,X2),true,r2_hidden(X2,k1_funct_1(k1_latsubgr(sk0),X1)),true),true),true),true) = true,
inference(orient,[status(thm)],[t25881]) ).
fof(f50,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ! [D] :
( m1_group_2(D,A)
=> ( ( r1_rlvect_1(D,C)
& r1_rlvect_1(D,B) )
=> r1_rlvect_1(D,k1_group_1(A,B,C)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t59_group_2) ).
fof(f50_nnf,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( r1_rlvect_1(D,k1_group_1(A,B,C))
| ~ r1_rlvect_1(D,C)
| ~ r1_rlvect_1(D,B)
| ~ m1_group_2(D,A) )
| ~ m1_subset_1(C,u1_struct_0(A)) )
| ~ m1_subset_1(B,u1_struct_0(A)) )
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f50]) ).
fof(f50_sk,plain,
! [A,B,C,D] :
( r1_rlvect_1(D,k1_group_1(A,B,C))
| ~ r1_rlvect_1(D,C)
| ~ r1_rlvect_1(D,B)
| ~ m1_group_2(D,A)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(skolemisation,[status(esa)],[f50_nnf]) ).
cnf(c86,plain,
( r1_rlvect_1(X3,k1_group_1(X0,X1,X2))
| ~ r1_rlvect_1(X3,X2)
| ~ r1_rlvect_1(X3,X1)
| ~ m1_group_2(X3,X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f50_sk]) ).
cnf(t253,plain,
ifeq(v3_group_1(X1),true,ifeq(v4_group_1(X1),true,ifeq(l1_group_1(X1),true,ifeq(m1_subset_1(X2,u1_struct_0(X1)),true,ifeq(m1_subset_1(X3,u1_struct_0(X1)),true,ifeq(m1_group_2(X4,X1),true,ifeq(r1_rlvect_1(X4,X2),true,ifeq(r1_rlvect_1(X4,X3),true,or(v3_struct_0(X1),r1_rlvect_1(X4,k1_group_1(X1,X2,X3))),true),true),true),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c86]) ).
cnf(t318,plain,
ifeq(v3_group_1(X1),true,ifeq(v4_group_1(X1),true,ifeq(l1_group_1(X1),true,ifeq(m1_subset_1(X2,u1_struct_0(X1)),true,ifeq(m1_subset_1(X3,u1_struct_0(X1)),true,ifeq(m1_group_2(X4,X1),true,ifeq(r1_rlvect_1(X4,X2),true,ifeq(r1_rlvect_1(X4,X3),true,or(v3_struct_0(X1),r1_rlvect_1(X4,k1_group_1(X1,X2,X3))),true),true),true),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t253]) ).
cnf(c6,plain,
m1_subset_1(sk2,u1_struct_0(sk0)),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t33,plain,
m1_subset_1(sk2,u1_struct_0(sk0)) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t383,plain,
m1_subset_1(sk2,u1_struct_0(sk0)) = true,
inference(orient,[status(thm)],[t33]) ).
cnf(t390,plain,
true = ifeq(v3_group_1(sk0),true,ifeq(v4_group_1(sk0),true,ifeq(l1_group_1(sk0),true,ifeq(true,true,ifeq(m1_subset_1(X1,u1_struct_0(sk0)),true,ifeq(m1_group_2(X2,sk0),true,ifeq(r1_rlvect_1(X2,sk2),true,ifeq(r1_rlvect_1(X2,X1),true,or(v3_struct_0(sk0),r1_rlvect_1(X2,k1_group_1(sk0,sk2,X1))),true),true),true),true),true),true),true),true),
inference(cp,[status(thm)],[t318,t383]) ).
cnf(t22664,plain,
true = ifeq(true,true,ifeq(v4_group_1(sk0),true,ifeq(l1_group_1(sk0),true,ifeq(true,true,ifeq(m1_subset_1(X1,u1_struct_0(sk0)),true,ifeq(m1_group_2(X2,sk0),true,ifeq(r1_rlvect_1(X2,sk2),true,ifeq(r1_rlvect_1(X2,X1),true,or(v3_struct_0(sk0),r1_rlvect_1(X2,k1_group_1(sk0,sk2,X1))),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t390,t569]) ).
cnf(t22665,plain,
true = ifeq(v4_group_1(sk0),true,ifeq(l1_group_1(sk0),true,ifeq(true,true,ifeq(m1_subset_1(X1,u1_struct_0(sk0)),true,ifeq(m1_group_2(X2,sk0),true,ifeq(r1_rlvect_1(X2,sk2),true,ifeq(r1_rlvect_1(X2,X1),true,or(v3_struct_0(sk0),r1_rlvect_1(X2,k1_group_1(sk0,sk2,X1))),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t22664,t258]) ).
cnf(t22666,plain,
true = ifeq(true,true,ifeq(l1_group_1(sk0),true,ifeq(true,true,ifeq(m1_subset_1(X1,u1_struct_0(sk0)),true,ifeq(m1_group_2(X2,sk0),true,ifeq(r1_rlvect_1(X2,sk2),true,ifeq(r1_rlvect_1(X2,X1),true,or(v3_struct_0(sk0),r1_rlvect_1(X2,k1_group_1(sk0,sk2,X1))),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t22665,t582]) ).
cnf(t22667,plain,
true = ifeq(l1_group_1(sk0),true,ifeq(true,true,ifeq(m1_subset_1(X1,u1_struct_0(sk0)),true,ifeq(m1_group_2(X2,sk0),true,ifeq(r1_rlvect_1(X2,sk2),true,ifeq(r1_rlvect_1(X2,X1),true,or(v3_struct_0(sk0),r1_rlvect_1(X2,k1_group_1(sk0,sk2,X1))),true),true),true),true),true),true),
inference(step,[status(thm)],[t22666,t258]) ).
cnf(t22668,plain,
true = ifeq(true,true,ifeq(true,true,ifeq(m1_subset_1(X1,u1_struct_0(sk0)),true,ifeq(m1_group_2(X2,sk0),true,ifeq(r1_rlvect_1(X2,sk2),true,ifeq(r1_rlvect_1(X2,X1),true,or(v3_struct_0(sk0),r1_rlvect_1(X2,k1_group_1(sk0,sk2,X1))),true),true),true),true),true),true),
inference(step,[status(thm)],[t22667,t420]) ).
cnf(t22669,plain,
true = ifeq(true,true,ifeq(m1_subset_1(X1,u1_struct_0(sk0)),true,ifeq(m1_group_2(X2,sk0),true,ifeq(r1_rlvect_1(X2,sk2),true,ifeq(r1_rlvect_1(X2,X1),true,or(v3_struct_0(sk0),r1_rlvect_1(X2,k1_group_1(sk0,sk2,X1))),true),true),true),true),true),
inference(step,[status(thm)],[t22668,t258]) ).
cnf(t22670,plain,
true = ifeq(m1_subset_1(X1,u1_struct_0(sk0)),true,ifeq(m1_group_2(X2,sk0),true,ifeq(r1_rlvect_1(X2,sk2),true,ifeq(r1_rlvect_1(X2,X1),true,or(v3_struct_0(sk0),r1_rlvect_1(X2,k1_group_1(sk0,sk2,X1))),true),true),true),true),
inference(step,[status(thm)],[t22669,t258]) ).
cnf(t22671,plain,
true = ifeq(m1_subset_1(X1,u1_struct_0(sk0)),true,ifeq(m1_group_2(X2,sk0),true,ifeq(r1_rlvect_1(X2,sk2),true,ifeq(r1_rlvect_1(X2,X1),true,or(false,r1_rlvect_1(X2,k1_group_1(sk0,sk2,X1))),true),true),true),true),
inference(step,[status(thm)],[t22670,t641]) ).
cnf(t22672,plain,
true = ifeq(m1_subset_1(X1,u1_struct_0(sk0)),true,ifeq(m1_group_2(X2,sk0),true,ifeq(r1_rlvect_1(X2,sk2),true,ifeq(r1_rlvect_1(X2,X1),true,r1_rlvect_1(X2,k1_group_1(sk0,sk2,X1)),true),true),true),true),
inference(step,[status(thm)],[t22671,t257]) ).
cnf(t3371,plain,
ifeq(m1_subset_1(X1,u1_struct_0(sk0)),true,ifeq(m1_group_2(X2,sk0),true,ifeq(r1_rlvect_1(X2,sk2),true,ifeq(r1_rlvect_1(X2,X1),true,r1_rlvect_1(X2,k1_group_1(sk0,sk2,X1)),true),true),true),true) = true,
inference(orient,[status(thm)],[t22672]) ).
cnf(c79,plain,
( r1_rlvect_1(X1,X2)
| ~ r2_hidden(X2,k1_funct_1(k1_latsubgr(X0),X1))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(t251,plain,
ifeq(v3_group_1(X1),true,ifeq(v4_group_1(X1),true,ifeq(l1_group_1(X1),true,ifeq(v1_group_1(X2),true,ifeq(m1_group_2(X2,X1),true,ifeq(m1_subset_1(X3,u1_struct_0(X1)),true,ifeq(r2_hidden(X3,k1_funct_1(k1_latsubgr(X1),X2)),true,or(v3_struct_0(X1),r1_rlvect_1(X2,X3)),true),true),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c79]) ).
cnf(t319,plain,
ifeq(v3_group_1(X1),true,ifeq(v4_group_1(X1),true,ifeq(l1_group_1(X1),true,ifeq(v1_group_1(X2),true,ifeq(m1_group_2(X2,X1),true,ifeq(m1_subset_1(X3,u1_struct_0(X1)),true,ifeq(r2_hidden(X3,k1_funct_1(k1_latsubgr(X1),X2)),true,or(v3_struct_0(X1),r1_rlvect_1(X2,X3)),true),true),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t251]) ).
cnf(c7,plain,
m1_subset_1(sk3,u1_struct_0(sk0)),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t34,plain,
m1_subset_1(sk3,u1_struct_0(sk0)) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t393,plain,
m1_subset_1(sk3,u1_struct_0(sk0)) = true,
inference(orient,[status(thm)],[t34]) ).
cnf(t399,plain,
true = ifeq(v3_group_1(sk0),true,ifeq(v4_group_1(sk0),true,ifeq(l1_group_1(sk0),true,ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(true,true,ifeq(r2_hidden(sk3,k1_funct_1(k1_latsubgr(sk0),X1)),true,or(v3_struct_0(sk0),r1_rlvect_1(X1,sk3)),true),true),true),true),true),true),true),
inference(cp,[status(thm)],[t319,t393]) ).
cnf(t23024,plain,
true = ifeq(true,true,ifeq(v4_group_1(sk0),true,ifeq(l1_group_1(sk0),true,ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(true,true,ifeq(r2_hidden(sk3,k1_funct_1(k1_latsubgr(sk0),X1)),true,or(v3_struct_0(sk0),r1_rlvect_1(X1,sk3)),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t399,t569]) ).
cnf(t23025,plain,
true = ifeq(v4_group_1(sk0),true,ifeq(l1_group_1(sk0),true,ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(true,true,ifeq(r2_hidden(sk3,k1_funct_1(k1_latsubgr(sk0),X1)),true,or(v3_struct_0(sk0),r1_rlvect_1(X1,sk3)),true),true),true),true),true),true),
inference(step,[status(thm)],[t23024,t258]) ).
cnf(t23026,plain,
true = ifeq(true,true,ifeq(l1_group_1(sk0),true,ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(true,true,ifeq(r2_hidden(sk3,k1_funct_1(k1_latsubgr(sk0),X1)),true,or(v3_struct_0(sk0),r1_rlvect_1(X1,sk3)),true),true),true),true),true),true),
inference(step,[status(thm)],[t23025,t582]) ).
cnf(t23027,plain,
true = ifeq(l1_group_1(sk0),true,ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(true,true,ifeq(r2_hidden(sk3,k1_funct_1(k1_latsubgr(sk0),X1)),true,or(v3_struct_0(sk0),r1_rlvect_1(X1,sk3)),true),true),true),true),true),
inference(step,[status(thm)],[t23026,t258]) ).
cnf(t23028,plain,
true = ifeq(true,true,ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(true,true,ifeq(r2_hidden(sk3,k1_funct_1(k1_latsubgr(sk0),X1)),true,or(v3_struct_0(sk0),r1_rlvect_1(X1,sk3)),true),true),true),true),true),
inference(step,[status(thm)],[t23027,t420]) ).
cnf(t23029,plain,
true = ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(true,true,ifeq(r2_hidden(sk3,k1_funct_1(k1_latsubgr(sk0),X1)),true,or(v3_struct_0(sk0),r1_rlvect_1(X1,sk3)),true),true),true),true),
inference(step,[status(thm)],[t23028,t258]) ).
cnf(t23030,plain,
true = ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(r2_hidden(sk3,k1_funct_1(k1_latsubgr(sk0),X1)),true,or(v3_struct_0(sk0),r1_rlvect_1(X1,sk3)),true),true),true),
inference(step,[status(thm)],[t23029,t258]) ).
cnf(t23031,plain,
true = ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(r2_hidden(sk3,k1_funct_1(k1_latsubgr(sk0),X1)),true,or(false,r1_rlvect_1(X1,sk3)),true),true),true),
inference(step,[status(thm)],[t23030,t641]) ).
cnf(t23032,plain,
true = ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(r2_hidden(sk3,k1_funct_1(k1_latsubgr(sk0),X1)),true,r1_rlvect_1(X1,sk3),true),true),true),
inference(step,[status(thm)],[t23031,t257]) ).
cnf(t5721,plain,
ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(r2_hidden(sk3,k1_funct_1(k1_latsubgr(sk0),X1)),true,r1_rlvect_1(X1,sk3),true),true),true) = true,
inference(orient,[status(thm)],[t23032]) ).
cnf(c4,plain,
v1_group_1(sk1),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t9,plain,
v1_group_1(sk1) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t562,plain,
v1_group_1(sk1) = true,
inference(orient,[status(thm)],[t9]) ).
cnf(t5723,plain,
true = ifeq(true,true,ifeq(m1_group_2(sk1,sk0),true,ifeq(r2_hidden(sk3,k1_funct_1(k1_latsubgr(sk0),sk1)),true,r1_rlvect_1(sk1,sk3),true),true),true),
inference(cp,[status(thm)],[t5721,t562]) ).
cnf(t23033,plain,
true = ifeq(m1_group_2(sk1,sk0),true,ifeq(r2_hidden(sk3,k1_funct_1(k1_latsubgr(sk0),sk1)),true,r1_rlvect_1(sk1,sk3),true),true),
inference(step,[status(thm)],[t5723,t258]) ).
cnf(c5,plain,
m1_group_2(sk1,sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t17,plain,
m1_group_2(sk1,sk0) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t590,plain,
m1_group_2(sk1,sk0) = true,
inference(orient,[status(thm)],[t17]) ).
cnf(t23034,plain,
true = ifeq(true,true,ifeq(r2_hidden(sk3,k1_funct_1(k1_latsubgr(sk0),sk1)),true,r1_rlvect_1(sk1,sk3),true),true),
inference(step,[status(thm)],[t23033,t590]) ).
cnf(t23035,plain,
true = ifeq(r2_hidden(sk3,k1_funct_1(k1_latsubgr(sk0),sk1)),true,r1_rlvect_1(sk1,sk3),true),
inference(step,[status(thm)],[t23034,t258]) ).
cnf(c9,plain,
r2_hidden(sk3,k1_funct_1(k1_latsubgr(sk0),sk1)),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t94,plain,
r2_hidden(sk3,k1_funct_1(k1_latsubgr(sk0),sk1)) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t470,plain,
r2_hidden(sk3,k1_funct_1(k1_latsubgr(sk0),sk1)) = true,
inference(orient,[status(thm)],[t94]) ).
cnf(t23036,plain,
true = ifeq(true,true,r1_rlvect_1(sk1,sk3),true),
inference(step,[status(thm)],[t23035,t470]) ).
cnf(t23037,plain,
true = r1_rlvect_1(sk1,sk3),
inference(step,[status(thm)],[t23036,t258]) ).
cnf(t5730,plain,
r1_rlvect_1(sk1,sk3) = true,
inference(orient,[status(thm)],[t23037]) ).
cnf(t5732,plain,
true = ifeq(m1_subset_1(sk3,u1_struct_0(sk0)),true,ifeq(m1_group_2(sk1,sk0),true,ifeq(r1_rlvect_1(sk1,sk2),true,ifeq(true,true,r1_rlvect_1(sk1,k1_group_1(sk0,sk2,sk3)),true),true),true),true),
inference(cp,[status(thm)],[t3371,t5730]) ).
cnf(t23045,plain,
true = ifeq(true,true,ifeq(m1_group_2(sk1,sk0),true,ifeq(r1_rlvect_1(sk1,sk2),true,ifeq(true,true,r1_rlvect_1(sk1,k1_group_1(sk0,sk2,sk3)),true),true),true),true),
inference(step,[status(thm)],[t5732,t393]) ).
cnf(t23046,plain,
true = ifeq(m1_group_2(sk1,sk0),true,ifeq(r1_rlvect_1(sk1,sk2),true,ifeq(true,true,r1_rlvect_1(sk1,k1_group_1(sk0,sk2,sk3)),true),true),true),
inference(step,[status(thm)],[t23045,t258]) ).
cnf(t23047,plain,
true = ifeq(true,true,ifeq(r1_rlvect_1(sk1,sk2),true,ifeq(true,true,r1_rlvect_1(sk1,k1_group_1(sk0,sk2,sk3)),true),true),true),
inference(step,[status(thm)],[t23046,t590]) ).
cnf(t23048,plain,
true = ifeq(r1_rlvect_1(sk1,sk2),true,ifeq(true,true,r1_rlvect_1(sk1,k1_group_1(sk0,sk2,sk3)),true),true),
inference(step,[status(thm)],[t23047,t258]) ).
cnf(t389,plain,
true = ifeq(v3_group_1(sk0),true,ifeq(v4_group_1(sk0),true,ifeq(l1_group_1(sk0),true,ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(true,true,ifeq(r2_hidden(sk2,k1_funct_1(k1_latsubgr(sk0),X1)),true,or(v3_struct_0(sk0),r1_rlvect_1(X1,sk2)),true),true),true),true),true),true),true),
inference(cp,[status(thm)],[t319,t383]) ).
cnf(t22646,plain,
true = ifeq(true,true,ifeq(v4_group_1(sk0),true,ifeq(l1_group_1(sk0),true,ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(true,true,ifeq(r2_hidden(sk2,k1_funct_1(k1_latsubgr(sk0),X1)),true,or(v3_struct_0(sk0),r1_rlvect_1(X1,sk2)),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t389,t569]) ).
cnf(t22647,plain,
true = ifeq(v4_group_1(sk0),true,ifeq(l1_group_1(sk0),true,ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(true,true,ifeq(r2_hidden(sk2,k1_funct_1(k1_latsubgr(sk0),X1)),true,or(v3_struct_0(sk0),r1_rlvect_1(X1,sk2)),true),true),true),true),true),true),
inference(step,[status(thm)],[t22646,t258]) ).
cnf(t22648,plain,
true = ifeq(true,true,ifeq(l1_group_1(sk0),true,ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(true,true,ifeq(r2_hidden(sk2,k1_funct_1(k1_latsubgr(sk0),X1)),true,or(v3_struct_0(sk0),r1_rlvect_1(X1,sk2)),true),true),true),true),true),true),
inference(step,[status(thm)],[t22647,t582]) ).
cnf(t22649,plain,
true = ifeq(l1_group_1(sk0),true,ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(true,true,ifeq(r2_hidden(sk2,k1_funct_1(k1_latsubgr(sk0),X1)),true,or(v3_struct_0(sk0),r1_rlvect_1(X1,sk2)),true),true),true),true),true),
inference(step,[status(thm)],[t22648,t258]) ).
cnf(t22650,plain,
true = ifeq(true,true,ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(true,true,ifeq(r2_hidden(sk2,k1_funct_1(k1_latsubgr(sk0),X1)),true,or(v3_struct_0(sk0),r1_rlvect_1(X1,sk2)),true),true),true),true),true),
inference(step,[status(thm)],[t22649,t420]) ).
cnf(t22651,plain,
true = ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(true,true,ifeq(r2_hidden(sk2,k1_funct_1(k1_latsubgr(sk0),X1)),true,or(v3_struct_0(sk0),r1_rlvect_1(X1,sk2)),true),true),true),true),
inference(step,[status(thm)],[t22650,t258]) ).
cnf(t22652,plain,
true = ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(r2_hidden(sk2,k1_funct_1(k1_latsubgr(sk0),X1)),true,or(v3_struct_0(sk0),r1_rlvect_1(X1,sk2)),true),true),true),
inference(step,[status(thm)],[t22651,t258]) ).
cnf(t22653,plain,
true = ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(r2_hidden(sk2,k1_funct_1(k1_latsubgr(sk0),X1)),true,or(false,r1_rlvect_1(X1,sk2)),true),true),true),
inference(step,[status(thm)],[t22652,t641]) ).
cnf(t22654,plain,
true = ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(r2_hidden(sk2,k1_funct_1(k1_latsubgr(sk0),X1)),true,r1_rlvect_1(X1,sk2),true),true),true),
inference(step,[status(thm)],[t22653,t257]) ).
cnf(t3241,plain,
ifeq(v1_group_1(X1),true,ifeq(m1_group_2(X1,sk0),true,ifeq(r2_hidden(sk2,k1_funct_1(k1_latsubgr(sk0),X1)),true,r1_rlvect_1(X1,sk2),true),true),true) = true,
inference(orient,[status(thm)],[t22654]) ).
cnf(t3243,plain,
true = ifeq(true,true,ifeq(m1_group_2(sk1,sk0),true,ifeq(r2_hidden(sk2,k1_funct_1(k1_latsubgr(sk0),sk1)),true,r1_rlvect_1(sk1,sk2),true),true),true),
inference(cp,[status(thm)],[t3241,t562]) ).
cnf(t22655,plain,
true = ifeq(m1_group_2(sk1,sk0),true,ifeq(r2_hidden(sk2,k1_funct_1(k1_latsubgr(sk0),sk1)),true,r1_rlvect_1(sk1,sk2),true),true),
inference(step,[status(thm)],[t3243,t258]) ).
cnf(t22656,plain,
true = ifeq(true,true,ifeq(r2_hidden(sk2,k1_funct_1(k1_latsubgr(sk0),sk1)),true,r1_rlvect_1(sk1,sk2),true),true),
inference(step,[status(thm)],[t22655,t590]) ).
cnf(t22657,plain,
true = ifeq(r2_hidden(sk2,k1_funct_1(k1_latsubgr(sk0),sk1)),true,r1_rlvect_1(sk1,sk2),true),
inference(step,[status(thm)],[t22656,t258]) ).
cnf(c8,plain,
r2_hidden(sk2,k1_funct_1(k1_latsubgr(sk0),sk1)),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t93,plain,
r2_hidden(sk2,k1_funct_1(k1_latsubgr(sk0),sk1)) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t456,plain,
r2_hidden(sk2,k1_funct_1(k1_latsubgr(sk0),sk1)) = true,
inference(orient,[status(thm)],[t93]) ).
cnf(t22658,plain,
true = ifeq(true,true,r1_rlvect_1(sk1,sk2),true),
inference(step,[status(thm)],[t22657,t456]) ).
cnf(t22659,plain,
true = r1_rlvect_1(sk1,sk2),
inference(step,[status(thm)],[t22658,t258]) ).
cnf(t3250,plain,
r1_rlvect_1(sk1,sk2) = true,
inference(orient,[status(thm)],[t22659]) ).
cnf(t23049,plain,
true = ifeq(true,true,ifeq(true,true,r1_rlvect_1(sk1,k1_group_1(sk0,sk2,sk3)),true),true),
inference(step,[status(thm)],[t23048,t3250]) ).
cnf(t23050,plain,
true = ifeq(true,true,r1_rlvect_1(sk1,k1_group_1(sk0,sk2,sk3)),true),
inference(step,[status(thm)],[t23049,t258]) ).
cnf(t23051,plain,
true = r1_rlvect_1(sk1,k1_group_1(sk0,sk2,sk3)),
inference(step,[status(thm)],[t23050,t258]) ).
cnf(t5745,plain,
r1_rlvect_1(sk1,k1_group_1(sk0,sk2,sk3)) = true,
inference(orient,[status(thm)],[t23051]) ).
cnf(t21656,plain,
true = ifeq(v1_group_1(sk1),true,ifeq(m1_group_2(sk1,sk0),true,ifeq(m1_subset_1(k1_group_1(sk0,sk2,sk3),u1_struct_0(sk0)),true,ifeq(true,true,r2_hidden(k1_group_1(sk0,sk2,sk3),k1_funct_1(k1_latsubgr(sk0),sk1)),true),true),true),true),
inference(cp,[status(thm)],[t20912,t5745]) ).
cnf(t25882,plain,
true = ifeq(true,true,ifeq(m1_group_2(sk1,sk0),true,ifeq(m1_subset_1(k1_group_1(sk0,sk2,sk3),u1_struct_0(sk0)),true,ifeq(true,true,r2_hidden(k1_group_1(sk0,sk2,sk3),k1_funct_1(k1_latsubgr(sk0),sk1)),true),true),true),true),
inference(step,[status(thm)],[t21656,t562]) ).
cnf(t25883,plain,
true = ifeq(m1_group_2(sk1,sk0),true,ifeq(m1_subset_1(k1_group_1(sk0,sk2,sk3),u1_struct_0(sk0)),true,ifeq(true,true,r2_hidden(k1_group_1(sk0,sk2,sk3),k1_funct_1(k1_latsubgr(sk0),sk1)),true),true),true),
inference(step,[status(thm)],[t25882,t258]) ).
cnf(t25884,plain,
true = ifeq(true,true,ifeq(m1_subset_1(k1_group_1(sk0,sk2,sk3),u1_struct_0(sk0)),true,ifeq(true,true,r2_hidden(k1_group_1(sk0,sk2,sk3),k1_funct_1(k1_latsubgr(sk0),sk1)),true),true),true),
inference(step,[status(thm)],[t25883,t590]) ).
cnf(t25885,plain,
true = ifeq(m1_subset_1(k1_group_1(sk0,sk2,sk3),u1_struct_0(sk0)),true,ifeq(true,true,r2_hidden(k1_group_1(sk0,sk2,sk3),k1_funct_1(k1_latsubgr(sk0),sk1)),true),true),
inference(step,[status(thm)],[t25884,t258]) ).
fof(f9,axiom,
! [A,B,C] :
( ( m1_subset_1(C,u1_struct_0(A))
& m1_subset_1(B,u1_struct_0(A))
& l1_group_1(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k1_group_1(A,B,C),u1_struct_0(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_group_1) ).
fof(f9_nnf,plain,
! [A,B,C] :
( m1_subset_1(k1_group_1(A,B,C),u1_struct_0(A))
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l1_group_1(A)
| v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [A,B,C] :
( m1_subset_1(k1_group_1(A,B,C),u1_struct_0(A))
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l1_group_1(A)
| v3_struct_0(A) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c26,plain,
( m1_subset_1(k1_group_1(X0,X1,X2),u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t243,plain,
ifeq(l1_group_1(X1),true,ifeq(m1_subset_1(X2,u1_struct_0(X1)),true,ifeq(m1_subset_1(X3,u1_struct_0(X1)),true,or(v3_struct_0(X1),m1_subset_1(k1_group_1(X1,X2,X3),u1_struct_0(X1))),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c26]) ).
cnf(t278,plain,
ifeq(l1_group_1(X1),true,ifeq(m1_subset_1(X2,u1_struct_0(X1)),true,ifeq(m1_subset_1(X3,u1_struct_0(X1)),true,or(v3_struct_0(X1),m1_subset_1(k1_group_1(X1,X2,X3),u1_struct_0(X1))),true),true),true) = true,
inference(orient,[status(thm)],[t243]) ).
cnf(t387,plain,
true = ifeq(l1_group_1(sk0),true,ifeq(true,true,ifeq(m1_subset_1(X1,u1_struct_0(sk0)),true,or(v3_struct_0(sk0),m1_subset_1(k1_group_1(sk0,sk2,X1),u1_struct_0(sk0))),true),true),true),
inference(cp,[status(thm)],[t278,t383]) ).
cnf(t22551,plain,
true = ifeq(true,true,ifeq(true,true,ifeq(m1_subset_1(X1,u1_struct_0(sk0)),true,or(v3_struct_0(sk0),m1_subset_1(k1_group_1(sk0,sk2,X1),u1_struct_0(sk0))),true),true),true),
inference(step,[status(thm)],[t387,t420]) ).
cnf(t22552,plain,
true = ifeq(true,true,ifeq(m1_subset_1(X1,u1_struct_0(sk0)),true,or(v3_struct_0(sk0),m1_subset_1(k1_group_1(sk0,sk2,X1),u1_struct_0(sk0))),true),true),
inference(step,[status(thm)],[t22551,t258]) ).
cnf(t22553,plain,
true = ifeq(m1_subset_1(X1,u1_struct_0(sk0)),true,or(v3_struct_0(sk0),m1_subset_1(k1_group_1(sk0,sk2,X1),u1_struct_0(sk0))),true),
inference(step,[status(thm)],[t22552,t258]) ).
cnf(t22554,plain,
true = ifeq(m1_subset_1(X1,u1_struct_0(sk0)),true,or(false,m1_subset_1(k1_group_1(sk0,sk2,X1),u1_struct_0(sk0))),true),
inference(step,[status(thm)],[t22553,t641]) ).
cnf(t22555,plain,
true = ifeq(m1_subset_1(X1,u1_struct_0(sk0)),true,m1_subset_1(k1_group_1(sk0,sk2,X1),u1_struct_0(sk0)),true),
inference(step,[status(thm)],[t22554,t257]) ).
cnf(t2784,plain,
ifeq(m1_subset_1(X1,u1_struct_0(sk0)),true,m1_subset_1(k1_group_1(sk0,sk2,X1),u1_struct_0(sk0)),true) = true,
inference(orient,[status(thm)],[t22555]) ).
cnf(t2786,plain,
true = ifeq(true,true,m1_subset_1(k1_group_1(sk0,sk2,sk3),u1_struct_0(sk0)),true),
inference(cp,[status(thm)],[t2784,t393]) ).
cnf(t22556,plain,
true = m1_subset_1(k1_group_1(sk0,sk2,sk3),u1_struct_0(sk0)),
inference(step,[status(thm)],[t2786,t258]) ).
cnf(t2788,plain,
m1_subset_1(k1_group_1(sk0,sk2,sk3),u1_struct_0(sk0)) = true,
inference(orient,[status(thm)],[t22556]) ).
cnf(t25886,plain,
true = ifeq(true,true,ifeq(true,true,r2_hidden(k1_group_1(sk0,sk2,sk3),k1_funct_1(k1_latsubgr(sk0),sk1)),true),true),
inference(step,[status(thm)],[t25885,t2788]) ).
cnf(t25887,plain,
true = ifeq(true,true,r2_hidden(k1_group_1(sk0,sk2,sk3),k1_funct_1(k1_latsubgr(sk0),sk1)),true),
inference(step,[status(thm)],[t25886,t258]) ).
cnf(t25888,plain,
true = r2_hidden(k1_group_1(sk0,sk2,sk3),k1_funct_1(k1_latsubgr(sk0),sk1)),
inference(step,[status(thm)],[t25887,t258]) ).
cnf(c10,plain,
~ r2_hidden(k1_group_1(sk0,sk2,sk3),k1_funct_1(k1_latsubgr(sk0),sk1)),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t145,plain,
r2_hidden(k1_group_1(sk0,sk2,sk3),k1_funct_1(k1_latsubgr(sk0),sk1)) = false,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t630,plain,
r2_hidden(k1_group_1(sk0,sk2,sk3),k1_funct_1(k1_latsubgr(sk0),sk1)) = false,
inference(orient,[status(thm)],[t145]) ).
cnf(t25889,plain,
true = false,
inference(step,[status(thm)],[t25888,t630]) ).
cnf(t21733,plain,
false = true,
inference(orient,[status(thm)],[t25889]) ).
fof(f2,axiom,
! [A,B] :
( r2_hidden(A,B)
=> ~ r2_hidden(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(f2_nnf,plain,
! [A,B] :
( ~ r2_hidden(B,A)
| ~ r2_hidden(A,B) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A,B] :
( ~ r2_hidden(B,A)
| ~ r2_hidden(A,B) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c12,plain,
( ~ r2_hidden(X1,X0)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
fof(f31,axiom,
! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f31_nnf,plain,
! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c54,plain,
~ v1_xboole_0(k1_zfmisc_1(X0)),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
fof(f40,axiom,
? [A] : ~ v1_xboole_0(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(f40_nnf,plain,
? [A] : ~ v1_xboole_0(A),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
~ v1_xboole_0(sk15),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk15])],[f40_nnf]) ).
cnf(c71,plain,
~ v1_xboole_0(sk15),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
fof(f41,axiom,
? [A] :
( ~ v3_struct_0(A)
& l1_struct_0(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc3_struct_0) ).
fof(f41_nnf,plain,
? [A] :
( ~ v3_struct_0(A)
& l1_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
( ~ v3_struct_0(sk16)
& l1_struct_0(sk16) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk16])],[f41_nnf]) ).
cnf(c73,plain,
~ v3_struct_0(sk16),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
fof(f51,axiom,
! [A,B,C] :
~ ( v1_xboole_0(C)
& m1_subset_1(B,k1_zfmisc_1(C))
& r2_hidden(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_subset) ).
fof(f51_nnf,plain,
! [A,B,C] :
( ~ v1_xboole_0(C)
| ~ m1_subset_1(B,k1_zfmisc_1(C))
| ~ r2_hidden(A,B) ),
inference(nnf_transformation,[status(thm)],[f51]) ).
fof(f51_sk,plain,
! [A,B,C] :
( ~ v1_xboole_0(C)
| ~ m1_subset_1(B,k1_zfmisc_1(C))
| ~ r2_hidden(A,B) ),
inference(skolemisation,[status(esa)],[f51_nnf]) ).
cnf(c87,plain,
( ~ v1_xboole_0(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
fof(f53,axiom,
! [A,B] :
~ ( v1_xboole_0(B)
& r2_hidden(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f53_nnf,plain,
! [A,B] :
( ~ v1_xboole_0(B)
| ~ r2_hidden(A,B) ),
inference(nnf_transformation,[status(thm)],[f53]) ).
fof(f53_sk,plain,
! [A,B] :
( ~ v1_xboole_0(B)
| ~ r2_hidden(A,B) ),
inference(skolemisation,[status(esa)],[f53_nnf]) ).
cnf(c89,plain,
( ~ v1_xboole_0(X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f53_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c10,c12,c54,c71,c73,c87,c89]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t21733]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP643+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n015.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 15:28:09 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 75.80/10.20 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 75.80/10.20 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------