%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : TOP028+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 : Fri Jul 25 10:10:29 PM UTC 2025
% Result : Theorem 8.21s 1.35s
% Output : CNFRefutation 8.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 5
% Syntax : Number of formulae : 48 ( 30 unt; 0 def)
% Number of atoms : 122 ( 0 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 130 ( 56 ~; 49 |; 15 &)
% ( 0 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 10 ( 9 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 1 con; 0-2 aty)
% Number of variables : 24 ( 1 sgn 10 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(t10_tsp_2,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v2_pre_topc(A)
& l1_pre_topc(A) )
=> ? [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
& v1_tsp_2(B,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t10_tsp_2) ).
fof(t10_tsp_2_negated,plain,
~ ! [A] :
( ( ~ v3_struct_0(A)
& v2_pre_topc(A)
& l1_pre_topc(A) )
=> ? [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
& v1_tsp_2(B,A) ) ),
inference(negate_conjecture,[status(cth)],[t10_tsp_2]) ).
cnf(3,plain,
( ~ v1_tsp_2(X0,sK1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(cnf,[status(esa)],[t10_tsp_2_negated]) ).
cnf(l0,plain,
( ~ v1_tsp_2(sK17(sK1,sK8(u1_struct_0(sK1))),sK1)
| ~ m1_subset_1(sK17(sK1,sK8(u1_struct_0(sK1))),k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(instantiation,[status(thm)],[3]) ).
fof(t9_tsp_2,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v2_pre_topc(A)
& l1_pre_topc(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ~ ( v1_tsp_1(B,A)
& ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
=> ~ ( r1_tarski(B,C)
& v1_tsp_2(C,A) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t9_tsp_2) ).
cnf(153,plain,
( ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_tsp_1(X1,X0)
| v1_tsp_2(sK17(X0,X1),X0)
| v3_struct_0(X0) ),
inference(cnf,[status(esa)],[t9_tsp_2]) ).
cnf(l1,plain,
( ~ v2_pre_topc(sK1)
| ~ l1_pre_topc(sK1)
| ~ m1_subset_1(sK8(u1_struct_0(sK1)),k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v1_tsp_1(sK8(u1_struct_0(sK1)),sK1)
| v1_tsp_2(sK17(sK1,sK8(u1_struct_0(sK1))),sK1)
| v3_struct_0(sK1) ),
inference(instantiation,[status(thm)],[153]) ).
cnf(1,plain,
v2_pre_topc(sK1),
inference(cnf,[status(esa)],[t10_tsp_2_negated]) ).
cnf(l3,plain,
v2_pre_topc(sK1),
inference(instantiation,[status(thm)],[1]) ).
fof(t11_tsp_1,plain,
! [A] :
( ( ~ v3_struct_0(A)
& l1_pre_topc(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( v3_tex_2(B,A)
=> v1_tsp_1(B,A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t11_tsp_1) ).
cnf(140,plain,
( ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_tex_2(X1,X0)
| v3_struct_0(X0)
| v1_tsp_1(X1,X0) ),
inference(cnf,[status(esa)],[t11_tsp_1]) ).
cnf(l42,plain,
( ~ l1_pre_topc(sK1)
| ~ m1_subset_1(sK8(u1_struct_0(sK1)),k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v3_tex_2(sK8(u1_struct_0(sK1)),sK1)
| v3_struct_0(sK1)
| v1_tsp_1(sK8(u1_struct_0(sK1)),sK1) ),
inference(instantiation,[status(thm)],[140]) ).
cnf(2,plain,
l1_pre_topc(sK1),
inference(cnf,[status(esa)],[t10_tsp_2_negated]) ).
cnf(l50,plain,
l1_pre_topc(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(0,plain,
~ v3_struct_0(sK1),
inference(cnf,[status(esa)],[t10_tsp_2_negated]) ).
cnf(l44,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l7,plain,
l1_pre_topc(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l163,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
fof(rc2_subset_1,plain,
! [A] :
? [B] :
( m1_subset_1(B,k1_zfmisc_1(A))
& v1_xboole_0(B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_subset_1) ).
cnf(102,plain,
m1_subset_1(sK8(X0),k1_zfmisc_1(X0)),
inference(cnf,[status(esa)],[rc2_subset_1]) ).
cnf(l47,plain,
m1_subset_1(sK8(u1_struct_0(sK1)),k1_zfmisc_1(u1_struct_0(sK1))),
inference(instantiation,[status(thm)],[102]) ).
cnf(l2,plain,
m1_subset_1(sK8(u1_struct_0(sK1)),k1_zfmisc_1(u1_struct_0(sK1))),
inference(instantiation,[status(thm)],[102]) ).
fof(t35_tex_2,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v2_pre_topc(A)
& l1_pre_topc(A) )
=> ! [B] :
( ( v1_xboole_0(B)
& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
=> v3_tex_2(B,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t35_tex_2) ).
cnf(143,plain,
( ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_xboole_0(X1)
| v3_struct_0(X0)
| v3_tex_2(X1,X0) ),
inference(cnf,[status(esa)],[t35_tex_2]) ).
cnf(l49,plain,
( ~ v2_pre_topc(sK1)
| ~ l1_pre_topc(sK1)
| ~ m1_subset_1(sK8(u1_struct_0(sK1)),k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v1_xboole_0(sK8(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| v3_tex_2(sK8(u1_struct_0(sK1)),sK1) ),
inference(instantiation,[status(thm)],[143]) ).
cnf(l52,plain,
m1_subset_1(sK8(u1_struct_0(sK1)),k1_zfmisc_1(u1_struct_0(sK1))),
inference(instantiation,[status(thm)],[102]) ).
cnf(l143,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l51,plain,
l1_pre_topc(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(103,plain,
v1_xboole_0(sK8(X0)),
inference(cnf,[status(esa)],[rc2_subset_1]) ).
cnf(l134,plain,
v1_xboole_0(sK8(u1_struct_0(sK1))),
inference(instantiation,[status(thm)],[103]) ).
cnf(151,plain,
( ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_tsp_1(X1,X0)
| v3_struct_0(X0)
| m1_subset_1(sK17(X0,X1),k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf,[status(esa)],[t9_tsp_2]) ).
cnf(l227,plain,
( ~ v2_pre_topc(sK1)
| ~ l1_pre_topc(sK1)
| ~ m1_subset_1(sK8(u1_struct_0(sK1)),k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v1_tsp_1(sK8(u1_struct_0(sK1)),sK1)
| v3_struct_0(sK1)
| m1_subset_1(sK17(sK1,sK8(u1_struct_0(sK1))),k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(instantiation,[status(thm)],[151]) ).
cnf(l245,plain,
( ~ l1_pre_topc(sK1)
| ~ m1_subset_1(sK8(u1_struct_0(sK1)),k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v3_tex_2(sK8(u1_struct_0(sK1)),sK1)
| v3_struct_0(sK1)
| v1_tsp_1(sK8(u1_struct_0(sK1)),sK1) ),
inference(instantiation,[status(thm)],[140]) ).
cnf(l266,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l247,plain,
l1_pre_topc(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l248,plain,
m1_subset_1(sK8(u1_struct_0(sK1)),k1_zfmisc_1(u1_struct_0(sK1))),
inference(instantiation,[status(thm)],[102]) ).
cnf(l54,plain,
v2_pre_topc(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l228,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l229,plain,
v2_pre_topc(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l249,plain,
( ~ v2_pre_topc(sK1)
| ~ l1_pre_topc(sK1)
| ~ m1_subset_1(sK8(u1_struct_0(sK1)),k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v1_xboole_0(sK8(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| v3_tex_2(sK8(u1_struct_0(sK1)),sK1) ),
inference(instantiation,[status(thm)],[143]) ).
cnf(l267,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l252,plain,
m1_subset_1(sK8(u1_struct_0(sK1)),k1_zfmisc_1(u1_struct_0(sK1))),
inference(instantiation,[status(thm)],[102]) ).
cnf(l233,plain,
l1_pre_topc(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l250,plain,
v2_pre_topc(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l255,plain,
v1_xboole_0(sK8(u1_struct_0(sK1))),
inference(instantiation,[status(thm)],[103]) ).
cnf(l246,plain,
m1_subset_1(sK8(u1_struct_0(sK1)),k1_zfmisc_1(u1_struct_0(sK1))),
inference(instantiation,[status(thm)],[102]) ).
cnf(l263,plain,
l1_pre_topc(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l3,l42,l50,l44,l7,l163,l47,l2,l49,l52,l143,l51,l134,l227,l245,l266,l247,l248,l54,l228,l229,l249,l267,l252,l233,l250,l255,l246,l263]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : TOP028+1 : TPTP v9.0.0. Released v3.4.0.
% 0.00/0.10 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.30 % Computer : n017.cluster.edu
% 0.09/0.30 % Model : x86_64 x86_64
% 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.30 % Memory : 8042.1875MB
% 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.30 % CPULimit : 300
% 0.09/0.30 % WCLimit : 300
% 0.09/0.30 % DateTime : Tue Jul 22 21:36:04 EDT 2025
% 0.09/0.30 % CPUTime :
% 0.15/0.31 % launching worker at depth: 2
% 0.15/0.31 % launching worker at depth: 5
% 0.15/0.31 % launching worker at depth: 3
% 0.15/0.31 % launching worker at depth: 6
% 0.15/0.31 % launching worker at depth: 1
% 0.15/0.31 % launching worker at depth: 4
% 0.15/0.31 % launching worker at depth: 7
% 0.15/0.31 % launching worker at depth: 8
% 0.15/0.31 % launching worker at depth: 9
% 0.15/0.32 % launching worker at depth: 10
% 0.15/0.38 % launching worker at depth: 11
% 8.21/1.35 % SZS status Theorem for theBenchmark
% 8.21/1.35 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------