%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : ALG215+1 : TPTP v9.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n022.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 09:45:59 AM UTC 2025
% Result : Theorem 21.89s 3.08s
% Output : CNFRefutation 21.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 9
% Syntax : Number of formulae : 139 ( 115 unt; 0 def)
% Number of atoms : 419 ( 13 equ)
% Maximal formula atoms : 22 ( 3 avg)
% Number of connectives : 465 ( 185 ~; 181 |; 80 &)
% ( 2 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 1 prp; 0-4 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-3 aty)
% Number of variables : 41 ( 1 sgn 21 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(t4_rmod_5,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v3_rlvect_1(A)
& v4_rlvect_1(A)
& v5_rlvect_1(A)
& v6_rlvect_1(A)
& v4_group_1(A)
& v6_vectsp_1(A)
& v7_vectsp_1(A)
& v8_vectsp_1(A)
& l3_vectsp_1(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& v3_rlvect_1(B)
& v4_rlvect_1(B)
& v5_rlvect_1(B)
& v6_rlvect_1(B)
& v5_vectsp_2(B,A)
& l1_vectsp_2(B,A) )
=> v1_rmod_5(k1_subset_1(u1_struct_0(B)),A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_rmod_5) ).
fof(t4_rmod_5_negated,plain,
~ ! [A] :
( ( ~ v3_struct_0(A)
& v3_rlvect_1(A)
& v4_rlvect_1(A)
& v5_rlvect_1(A)
& v6_rlvect_1(A)
& v4_group_1(A)
& v6_vectsp_1(A)
& v7_vectsp_1(A)
& v8_vectsp_1(A)
& l3_vectsp_1(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& v3_rlvect_1(B)
& v4_rlvect_1(B)
& v5_rlvect_1(B)
& v6_rlvect_1(B)
& v5_vectsp_2(B,A)
& l1_vectsp_2(B,A) )
=> v1_rmod_5(k1_subset_1(u1_struct_0(B)),A,B) ) ),
inference(negate_conjecture,[status(cth)],[t4_rmod_5]) ).
cnf(0,plain,
~ v3_struct_0(sK1),
inference(cnf,[status(esa)],[t4_rmod_5_negated]) ).
cnf(l0,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
fof(d7_rmod_4,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v3_rlvect_1(A)
& v4_rlvect_1(A)
& v5_rlvect_1(A)
& v6_rlvect_1(A)
& v4_group_1(A)
& v6_vectsp_1(A)
& v7_vectsp_1(A)
& v8_vectsp_1(A)
& l3_vectsp_1(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& v3_rlvect_1(B)
& v4_rlvect_1(B)
& v5_rlvect_1(B)
& v6_rlvect_1(B)
& v5_vectsp_2(B,A)
& l1_vectsp_2(B,A) )
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
=> ! [D] :
( m1_rmod_4(D,A,B)
=> ( m2_rmod_4(D,A,B,C)
<=> r1_tarski(k2_rmod_4(A,B,D),C) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d7_rmod_4) ).
cnf(25,plain,
( ~ l3_vectsp_1(X0)
| ~ v3_rlvect_1(X0)
| ~ v3_rlvect_1(X1)
| ~ v5_rlvect_1(X0)
| ~ v5_rlvect_1(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0)
| ~ v4_rlvect_1(X0)
| ~ v4_rlvect_1(X1)
| ~ v6_rlvect_1(X0)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ m2_rmod_4(X3,X0,X1,X2)
| ~ v8_vectsp_1(X0)
| ~ m1_rmod_4(X3,X0,X1)
| v3_struct_0(X0)
| v3_struct_0(X1)
| r1_tarski(k2_rmod_4(X0,X1,X3),X2) ),
inference(cnf,[status(esa)],[d7_rmod_4]) ).
cnf(l1,plain,
( ~ l3_vectsp_1(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v3_rlvect_1(sK2)
| ~ v5_rlvect_1(sK1)
| ~ v5_rlvect_1(sK2)
| ~ m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| ~ v4_rlvect_1(sK1)
| ~ v4_rlvect_1(sK2)
| ~ v6_rlvect_1(sK1)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ m2_rmod_4(sK3(sK1,sK2,k1_subset_1(u1_struct_0(sK2))),sK1,sK2,k1_xboole_0)
| ~ v8_vectsp_1(sK1)
| ~ m1_rmod_4(sK3(sK1,sK2,k1_subset_1(u1_struct_0(sK2))),sK1,sK2)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| r1_tarski(k2_rmod_4(sK1,sK2,sK3(sK1,sK2,k1_subset_1(u1_struct_0(sK2)))),k1_xboole_0) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(13,plain,
v5_rlvect_1(sK2),
inference(cnf,[status(esa)],[t4_rmod_5_negated]) ).
cnf(l8,plain,
v5_rlvect_1(sK2),
inference(instantiation,[status(thm)],[13]) ).
cnf(16,plain,
l1_vectsp_2(sK2,sK1),
inference(cnf,[status(esa)],[t4_rmod_5_negated]) ).
cnf(l6,plain,
l1_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[16]) ).
fof(t3_xboole_1,plain,
! [A] :
( r1_tarski(A,k1_xboole_0)
=> A = k1_xboole_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_xboole_1) ).
cnf(105,plain,
( ~ r1_tarski(X0,k1_xboole_0)
| X0 = k1_xboole_0 ),
inference(cnf,[status(esa)],[t3_xboole_1]) ).
cnf(l1815,plain,
( ~ r1_tarski(k2_rmod_4(sK1,sK2,sK3(sK1,sK2,k1_subset_1(u1_struct_0(sK2)))),k1_xboole_0)
| k2_rmod_4(sK1,sK2,sK3(sK1,sK2,k1_subset_1(u1_struct_0(sK2)))) = k1_xboole_0 ),
inference(instantiation,[status(thm)],[105]) ).
cnf(8,plain,
v8_vectsp_1(sK1),
inference(cnf,[status(esa)],[t4_rmod_5_negated]) ).
cnf(l81,plain,
v8_vectsp_1(sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(9,plain,
l3_vectsp_1(sK1),
inference(cnf,[status(esa)],[t4_rmod_5_negated]) ).
cnf(l5,plain,
l3_vectsp_1(sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(11,plain,
v3_rlvect_1(sK2),
inference(cnf,[status(esa)],[t4_rmod_5_negated]) ).
cnf(l29,plain,
v3_rlvect_1(sK2),
inference(instantiation,[status(thm)],[11]) ).
cnf(14,plain,
v6_rlvect_1(sK2),
inference(cnf,[status(esa)],[t4_rmod_5_negated]) ).
cnf(l12,plain,
v6_rlvect_1(sK2),
inference(instantiation,[status(thm)],[14]) ).
fof(t8_boole,plain,
! [A,B] :
~ ( v1_xboole_0(A)
& A != B
& v1_xboole_0(B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_boole) ).
cnf(110,plain,
( ~ v1_xboole_0(X0)
| ~ v1_xboole_0(X1)
| X0 = X1 ),
inference(cnf,[status(esa)],[t8_boole]) ).
cnf(l17,plain,
( ~ v1_xboole_0(k1_subset_1(u1_struct_0(sK2)))
| ~ v1_xboole_0(k1_xboole_0)
| k1_subset_1(u1_struct_0(sK2)) = k1_xboole_0 ),
inference(instantiation,[status(thm)],[110]) ).
cnf(1,plain,
v3_rlvect_1(sK1),
inference(cnf,[status(esa)],[t4_rmod_5_negated]) ).
cnf(l2,plain,
v3_rlvect_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(5,plain,
v4_group_1(sK1),
inference(cnf,[status(esa)],[t4_rmod_5_negated]) ).
cnf(l27,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[5]) ).
fof(fc1_xboole_0,plain,
v1_xboole_0(k1_xboole_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_xboole_0) ).
cnf(69,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf,[status(esa)],[fc1_xboole_0]) ).
cnf(l47,plain,
v1_xboole_0(k1_xboole_0),
inference(instantiation,[status(thm)],[69]) ).
fof(d1_rmod_5,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v3_rlvect_1(A)
& v4_rlvect_1(A)
& v5_rlvect_1(A)
& v6_rlvect_1(A)
& v4_group_1(A)
& v6_vectsp_1(A)
& v7_vectsp_1(A)
& v8_vectsp_1(A)
& l3_vectsp_1(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& v3_rlvect_1(B)
& v4_rlvect_1(B)
& v5_rlvect_1(B)
& v6_rlvect_1(B)
& v5_vectsp_2(B,A)
& l1_vectsp_2(B,A) )
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
=> ( v1_rmod_5(C,A,B)
<=> ! [D] :
( m2_rmod_4(D,A,B,C)
=> ( k5_rmod_4(A,B,D) = k1_rlvect_1(B)
=> k2_rmod_4(A,B,D) = k1_xboole_0 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_rmod_5) ).
cnf(21,plain,
( ~ l3_vectsp_1(X0)
| ~ v3_rlvect_1(X0)
| ~ v3_rlvect_1(X1)
| ~ v5_rlvect_1(X0)
| ~ v5_rlvect_1(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0)
| ~ v4_rlvect_1(X0)
| ~ v4_rlvect_1(X1)
| ~ v6_rlvect_1(X0)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| v1_rmod_5(X2,X0,X1)
| v3_struct_0(X0)
| v3_struct_0(X1)
| m2_rmod_4(sK3(X0,X1,X2),X0,X1,X2) ),
inference(cnf,[status(esa)],[d1_rmod_5]) ).
cnf(l579,plain,
( ~ l3_vectsp_1(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v3_rlvect_1(sK2)
| ~ v5_rlvect_1(sK1)
| ~ v5_rlvect_1(sK2)
| ~ m1_subset_1(k1_subset_1(u1_struct_0(sK2)),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| ~ v4_rlvect_1(sK1)
| ~ v4_rlvect_1(sK2)
| ~ v6_rlvect_1(sK1)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| v1_rmod_5(k1_subset_1(u1_struct_0(sK2)),sK1,sK2)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| m2_rmod_4(sK3(sK1,sK2,k1_subset_1(u1_struct_0(sK2))),sK1,sK2,k1_subset_1(u1_struct_0(sK2))) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(3,plain,
v5_rlvect_1(sK1),
inference(cnf,[status(esa)],[t4_rmod_5_negated]) ).
cnf(l2004,plain,
v5_rlvect_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(10,plain,
~ v3_struct_0(sK2),
inference(cnf,[status(esa)],[t4_rmod_5_negated]) ).
cnf(l484,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[10]) ).
cnf(2,plain,
v4_rlvect_1(sK1),
inference(cnf,[status(esa)],[t4_rmod_5_negated]) ).
cnf(l2010,plain,
v4_rlvect_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1997,plain,
v6_rlvect_1(sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(17,plain,
~ v1_rmod_5(k1_subset_1(u1_struct_0(sK2)),sK1,sK2),
inference(cnf,[status(esa)],[t4_rmod_5_negated]) ).
cnf(l1996,plain,
~ v1_rmod_5(k1_subset_1(u1_struct_0(sK2)),sK1,sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(l2013,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[10]) ).
cnf(l2008,plain,
v3_rlvect_1(sK2),
inference(instantiation,[status(thm)],[11]) ).
cnf(4,plain,
v6_rlvect_1(sK1),
inference(cnf,[status(esa)],[t4_rmod_5_negated]) ).
cnf(l2002,plain,
v6_rlvect_1(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l630,plain,
l3_vectsp_1(sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2007,plain,
l1_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[16]) ).
cnf(l2009,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(7,plain,
v7_vectsp_1(sK1),
inference(cnf,[status(esa)],[t4_rmod_5_negated]) ).
cnf(l2011,plain,
v7_vectsp_1(sK1),
inference(instantiation,[status(thm)],[7]) ).
cnf(12,plain,
v4_rlvect_1(sK2),
inference(cnf,[status(esa)],[t4_rmod_5_negated]) ).
cnf(l2005,plain,
v4_rlvect_1(sK2),
inference(instantiation,[status(thm)],[12]) ).
cnf(l22,plain,
v7_vectsp_1(sK1),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1998,plain,
v5_rlvect_1(sK2),
inference(instantiation,[status(thm)],[13]) ).
cnf(l24,plain,
v5_rlvect_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l28,plain,
v4_rlvect_1(sK2),
inference(instantiation,[status(thm)],[12]) ).
cnf(6,plain,
v6_vectsp_1(sK1),
inference(cnf,[status(esa)],[t4_rmod_5_negated]) ).
cnf(l2003,plain,
v6_vectsp_1(sK1),
inference(instantiation,[status(thm)],[6]) ).
cnf(23,plain,
( ~ l3_vectsp_1(X0)
| ~ v3_rlvect_1(X0)
| ~ v3_rlvect_1(X1)
| ~ v5_rlvect_1(X0)
| ~ v5_rlvect_1(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0)
| ~ v4_rlvect_1(X0)
| ~ v4_rlvect_1(X1)
| ~ v6_rlvect_1(X0)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| k2_rmod_4(X0,X1,sK3(X0,X1,X2)) != k1_xboole_0
| v1_rmod_5(X2,X0,X1)
| v3_struct_0(X0)
| v3_struct_0(X1) ),
inference(cnf,[status(esa)],[d1_rmod_5]) ).
cnf(l1941,plain,
( ~ l3_vectsp_1(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v3_rlvect_1(sK2)
| ~ v5_rlvect_1(sK1)
| ~ v5_rlvect_1(sK2)
| ~ m1_subset_1(k1_subset_1(u1_struct_0(sK2)),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| ~ v4_rlvect_1(sK1)
| ~ v4_rlvect_1(sK2)
| ~ v6_rlvect_1(sK1)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| k2_rmod_4(sK1,sK2,sK3(sK1,sK2,k1_subset_1(u1_struct_0(sK2)))) != k1_xboole_0
| v1_rmod_5(k1_subset_1(u1_struct_0(sK2)),sK1,sK2)
| v3_struct_0(sK1)
| v3_struct_0(sK2) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l2056,plain,
v6_vectsp_1(sK1),
inference(instantiation,[status(thm)],[6]) ).
cnf(l36,plain,
v4_rlvect_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2063,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[10]) ).
cnf(l44,plain,
v6_rlvect_1(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2067,plain,
v4_rlvect_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
fof(dt_m2_rmod_4,plain,
! [A,B,C] :
( ( ~ v3_struct_0(A)
& v3_rlvect_1(A)
& v4_rlvect_1(A)
& v5_rlvect_1(A)
& v6_rlvect_1(A)
& v4_group_1(A)
& v6_vectsp_1(A)
& v7_vectsp_1(A)
& v8_vectsp_1(A)
& l3_vectsp_1(A)
& ~ v3_struct_0(B)
& v3_rlvect_1(B)
& v4_rlvect_1(B)
& v5_rlvect_1(B)
& v6_rlvect_1(B)
& v5_vectsp_2(B,A)
& l1_vectsp_2(B,A)
& m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) )
=> ! [D] :
( m2_rmod_4(D,A,B,C)
=> m1_rmod_4(D,A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_rmod_4) ).
cnf(51,plain,
( ~ l3_vectsp_1(X0)
| ~ v3_rlvect_1(X0)
| ~ v3_rlvect_1(X1)
| ~ v5_rlvect_1(X0)
| ~ v5_rlvect_1(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0)
| ~ v4_rlvect_1(X0)
| ~ v4_rlvect_1(X1)
| ~ v6_rlvect_1(X0)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ m2_rmod_4(X3,X0,X1,X2)
| ~ v8_vectsp_1(X0)
| v3_struct_0(X0)
| v3_struct_0(X1)
| m1_rmod_4(X3,X0,X1) ),
inference(cnf,[status(esa)],[dt_m2_rmod_4]) ).
cnf(l51,plain,
( ~ l3_vectsp_1(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v3_rlvect_1(sK2)
| ~ v5_rlvect_1(sK1)
| ~ v5_rlvect_1(sK2)
| ~ m1_subset_1(k1_subset_1(u1_struct_0(sK2)),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| ~ v4_rlvect_1(sK1)
| ~ v4_rlvect_1(sK2)
| ~ v6_rlvect_1(sK1)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ m2_rmod_4(sK3(sK1,sK2,k1_subset_1(u1_struct_0(sK2))),sK1,sK2,k1_subset_1(u1_struct_0(sK2)))
| ~ v8_vectsp_1(sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| m1_rmod_4(sK3(sK1,sK2,k1_subset_1(u1_struct_0(sK2))),sK1,sK2) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(15,plain,
v5_vectsp_2(sK2,sK1),
inference(cnf,[status(esa)],[t4_rmod_5_negated]) ).
cnf(l2000,plain,
v5_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[15]) ).
cnf(l2066,plain,
l1_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[16]) ).
cnf(l2054,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l2057,plain,
v6_rlvect_1(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l66,plain,
v6_rlvect_1(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l59,plain,
v5_rlvect_1(sK2),
inference(instantiation,[status(thm)],[13]) ).
fof(dt_k1_subset_1,plain,
! [A] :
( v1_xboole_0(k1_subset_1(A))
& m1_subset_1(k1_subset_1(A),k1_zfmisc_1(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_subset_1) ).
cnf(30,plain,
m1_subset_1(k1_subset_1(X0),k1_zfmisc_1(X0)),
inference(cnf,[status(esa)],[dt_k1_subset_1]) ).
cnf(l1999,plain,
m1_subset_1(k1_subset_1(u1_struct_0(sK2)),k1_zfmisc_1(u1_struct_0(sK2))),
inference(instantiation,[status(thm)],[30]) ).
cnf(l48,plain,
v6_vectsp_1(sK1),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1943,plain,
v3_rlvect_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l61,plain,
v5_rlvect_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l137,plain,
v6_vectsp_1(sK1),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2052,plain,
v5_rlvect_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1942,plain,
v3_rlvect_1(sK2),
inference(instantiation,[status(thm)],[11]) ).
cnf(l2055,plain,
v8_vectsp_1(sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(l54,plain,
v3_rlvect_1(sK2),
inference(instantiation,[status(thm)],[11]) ).
cnf(l3,plain,
v5_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[15]) ).
cnf(29,plain,
v1_xboole_0(k1_subset_1(X0)),
inference(cnf,[status(esa)],[dt_k1_subset_1]) ).
cnf(l74,plain,
v1_xboole_0(k1_subset_1(u1_struct_0(sK2))),
inference(instantiation,[status(thm)],[29]) ).
cnf(l637,plain,
v3_rlvect_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l133,plain,
v7_vectsp_1(sK1),
inference(instantiation,[status(thm)],[7]) ).
cnf(l126,plain,
v6_rlvect_1(sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2051,plain,
v5_rlvect_1(sK2),
inference(instantiation,[status(thm)],[13]) ).
cnf(l2059,plain,
v6_rlvect_1(sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2006,plain,
l3_vectsp_1(sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(l2065,plain,
v7_vectsp_1(sK1),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2058,plain,
v5_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[15]) ).
cnf(l65,plain,
l1_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[16]) ).
cnf(l2064,plain,
~ v1_rmod_5(k1_subset_1(u1_struct_0(sK2)),sK1,sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(l116,plain,
( ~ l3_vectsp_1(sK1)
| ~ v3_rlvect_1(sK1)
| ~ v3_rlvect_1(sK2)
| ~ v5_rlvect_1(sK1)
| ~ v5_rlvect_1(sK2)
| ~ m1_subset_1(k1_subset_1(u1_struct_0(sK2)),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v5_vectsp_2(sK2,sK1)
| ~ l1_vectsp_2(sK2,sK1)
| ~ v4_rlvect_1(sK1)
| ~ v4_rlvect_1(sK2)
| ~ v6_rlvect_1(sK1)
| ~ v6_rlvect_1(sK2)
| ~ v4_group_1(sK1)
| ~ v6_vectsp_1(sK1)
| ~ v7_vectsp_1(sK1)
| ~ v8_vectsp_1(sK1)
| v1_rmod_5(k1_subset_1(u1_struct_0(sK2)),sK1,sK2)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| m2_rmod_4(sK3(sK1,sK2,k1_subset_1(u1_struct_0(sK2))),sK1,sK2,k1_subset_1(u1_struct_0(sK2))) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1499,plain,
m1_subset_1(k1_subset_1(u1_struct_0(sK2)),k1_zfmisc_1(u1_struct_0(sK2))),
inference(instantiation,[status(thm)],[30]) ).
cnf(l204,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[10]) ).
cnf(l63,plain,
v8_vectsp_1(sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(l57,plain,
l3_vectsp_1(sK1),
inference(instantiation,[status(thm)],[9]) ).
fof(t6_boole,plain,
! [A] :
( v1_xboole_0(A)
=> A = k1_xboole_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_boole) ).
cnf(108,plain,
( ~ v1_xboole_0(X0)
| X0 = k1_xboole_0 ),
inference(cnf,[status(esa)],[t6_boole]) ).
cnf(l582,plain,
( ~ v1_xboole_0(k1_subset_1(u1_struct_0(sK2)))
| k1_subset_1(u1_struct_0(sK2)) = k1_xboole_0 ),
inference(instantiation,[status(thm)],[108]) ).
cnf(l2060,plain,
v4_rlvect_1(sK2),
inference(instantiation,[status(thm)],[12]) ).
cnf(l124,plain,
v5_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1508,plain,
v5_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1501,plain,
v5_rlvect_1(sK1),
inference(instantiation,[status(thm)],[3]) ).
cnf(l645,plain,
v1_xboole_0(k1_subset_1(u1_struct_0(sK2))),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1504,plain,
v6_rlvect_1(sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l10,plain,
m1_subset_1(k1_subset_1(u1_struct_0(sK2)),k1_zfmisc_1(u1_struct_0(sK2))),
inference(instantiation,[status(thm)],[30]) ).
cnf(l1503,plain,
v4_rlvect_1(sK2),
inference(instantiation,[status(thm)],[12]) ).
cnf(l82,plain,
v4_rlvect_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l271,plain,
v8_vectsp_1(sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1534,plain,
v6_vectsp_1(sK1),
inference(instantiation,[status(thm)],[6]) ).
cnf(l55,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l134,plain,
v4_rlvect_1(sK2),
inference(instantiation,[status(thm)],[12]) ).
cnf(l197,plain,
v3_rlvect_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1509,plain,
v7_vectsp_1(sK1),
inference(instantiation,[status(thm)],[7]) ).
cnf(l125,plain,
m1_subset_1(k1_subset_1(u1_struct_0(sK2)),k1_zfmisc_1(u1_struct_0(sK2))),
inference(instantiation,[status(thm)],[30]) ).
cnf(l1505,plain,
v5_rlvect_1(sK2),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1535,plain,
~ v1_rmod_5(k1_subset_1(u1_struct_0(sK2)),sK1,sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1502,plain,
v4_group_1(sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l2001,plain,
v8_vectsp_1(sK1),
inference(instantiation,[status(thm)],[8]) ).
cnf(l159,plain,
l3_vectsp_1(sK1),
inference(instantiation,[status(thm)],[9]) ).
cnf(l168,plain,
v3_rlvect_1(sK2),
inference(instantiation,[status(thm)],[11]) ).
cnf(l2053,plain,
m1_subset_1(k1_subset_1(u1_struct_0(sK2)),k1_zfmisc_1(u1_struct_0(sK2))),
inference(instantiation,[status(thm)],[30]) ).
cnf(l62,plain,
v3_rlvect_1(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1510,plain,
l1_vectsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[16]) ).
cnf(l1500,plain,
v4_rlvect_1(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l272,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1506,plain,
v6_rlvect_1(sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l8,l6,l1815,l81,l5,l29,l12,l17,l2,l27,l47,l579,l2004,l484,l2010,l1997,l1996,l2013,l2008,l2002,l630,l2007,l2009,l2011,l2005,l22,l1998,l24,l28,l2003,l1941,l2056,l36,l2063,l44,l2067,l51,l2000,l2066,l2054,l2057,l66,l59,l1999,l48,l1943,l61,l137,l2052,l1942,l2055,l54,l3,l74,l637,l133,l126,l2051,l2059,l2006,l2065,l2058,l65,l2064,l116,l1499,l204,l63,l57,l582,l2060,l124,l1508,l1501,l645,l1504,l10,l1503,l82,l271,l1534,l55,l134,l197,l1509,l125,l1505,l1535,l1502,l2001,l159,l168,l2053,l62,l1510,l1500,l272,l1506]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : ALG215+1 : TPTP v9.0.0. Released v3.4.0.
% 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.34 % Computer : n022.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Sun Jul 20 02:46:49 EDT 2025
% 0.12/0.34 % CPUTime :
% 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: 4
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.35 % launching worker at depth: 9
% 0.12/0.39 % launching worker at depth: 10
% 2.35/0.65 % launching worker at depth: 11
% 21.89/3.08 % SZS status Theorem for theBenchmark
% 21.89/3.08 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------