%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : TOP035+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 : n024.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:31 PM UTC 2025
% Result : Theorem 140.24s 17.95s
% Output : CNFRefutation 140.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 5
% Syntax : Number of formulae : 105 ( 74 unt; 0 def)
% Number of atoms : 299 ( 17 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 328 ( 134 ~; 140 |; 30 &)
% ( 2 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-4 aty)
% Number of variables : 38 ( 0 sgn 20 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(t24_tsp_2,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v2_pre_topc(A)
& l1_pre_topc(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& v2_tsp_2(B,A)
& m2_tsp_1(B,A) )
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ! [D] :
( m1_subset_1(D,u1_struct_0(B))
=> ( C = D
=> k5_pre_topc(A,B,k1_tsp_2(A,B),k6_pre_topc(B,k1_struct_0(B,D))) = k6_pre_topc(A,k1_struct_0(A,C)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t24_tsp_2) ).
fof(t24_tsp_2_negated,plain,
~ ! [A] :
( ( ~ v3_struct_0(A)
& v2_pre_topc(A)
& l1_pre_topc(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& v2_tsp_2(B,A)
& m2_tsp_1(B,A) )
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ! [D] :
( m1_subset_1(D,u1_struct_0(B))
=> ( C = D
=> k5_pre_topc(A,B,k1_tsp_2(A,B),k6_pre_topc(B,k1_struct_0(B,D))) = k6_pre_topc(A,k1_struct_0(A,C)) ) ) ) ) ),
inference(negate_conjecture,[status(cth)],[t24_tsp_2]) ).
cnf(0,plain,
~ v3_struct_0(sK1),
inference(cnf,[status(esa)],[t24_tsp_2_negated]) ).
cnf(l0,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
fof(d9_tsp_2,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v2_pre_topc(A)
& l1_pre_topc(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& v2_tsp_2(B,A)
& m2_tsp_1(B,A) )
=> ! [C] :
( ( v1_funct_1(C)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v5_pre_topc(C,A,B)
& m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
=> ( C = k1_tsp_2(A,B)
<=> v3_borsuk_1(C,A,B) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d9_tsp_2) ).
cnf(108,plain,
( ~ m2_tsp_1(X0,X1)
| ~ l1_pre_topc(X1)
| X2 != k1_tsp_2(X1,X0)
| ~ v2_tsp_2(X0,X1)
| ~ v2_pre_topc(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v5_pre_topc(X2,X1,X0)
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| v3_struct_0(X1)
| v3_struct_0(X0)
| v3_borsuk_1(X2,X1,X0) ),
inference(cnf,[status(esa)],[d9_tsp_2]) ).
cnf(l1,plain,
( ~ m2_tsp_1(sK2,sK1)
| ~ l1_pre_topc(sK1)
| k1_tsp_2(sK1,sK2) != k1_tsp_2(sK1,sK2)
| ~ v2_tsp_2(sK2,sK1)
| ~ v2_pre_topc(sK1)
| ~ v1_funct_1(k1_tsp_2(sK1,sK2))
| ~ v1_funct_2(k1_tsp_2(sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK2),sK1,sK2)
| ~ m2_relset_1(k1_tsp_2(sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK2))
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| v3_borsuk_1(k1_tsp_2(sK1,sK2),sK1,sK2) ),
inference(instantiation,[status(thm)],[108]) ).
cnf(3,plain,
~ v3_struct_0(sK2),
inference(cnf,[status(esa)],[t24_tsp_2_negated]) ).
cnf(l3352,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[3]) ).
cnf(2,plain,
l1_pre_topc(sK1),
inference(cnf,[status(esa)],[t24_tsp_2_negated]) ).
cnf(l3,plain,
l1_pre_topc(sK1),
inference(instantiation,[status(thm)],[2]) ).
fof(dt_k1_tsp_2,plain,
! [A,B] :
( ( ~ v3_struct_0(A)
& v2_pre_topc(A)
& l1_pre_topc(A)
& ~ v3_struct_0(B)
& v2_tsp_2(B,A)
& m1_pre_topc(B,A) )
=> ( v1_funct_1(k1_tsp_2(A,B))
& v1_funct_2(k1_tsp_2(A,B),u1_struct_0(A),u1_struct_0(B))
& v5_pre_topc(k1_tsp_2(A,B),A,B)
& m2_relset_1(k1_tsp_2(A,B),u1_struct_0(A),u1_struct_0(B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_tsp_2) ).
cnf(113,plain,
( ~ l1_pre_topc(X0)
| ~ v2_tsp_2(X1,X0)
| ~ v2_pre_topc(X0)
| ~ m1_pre_topc(X1,X0)
| v3_struct_0(X0)
| v3_struct_0(X1)
| v5_pre_topc(k1_tsp_2(X0,X1),X0,X1) ),
inference(cnf,[status(esa)],[dt_k1_tsp_2]) ).
cnf(l315,plain,
( ~ l1_pre_topc(sK1)
| ~ v2_tsp_2(sK2,sK1)
| ~ v2_pre_topc(sK1)
| ~ m1_pre_topc(sK2,sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| v5_pre_topc(k1_tsp_2(sK1,sK2),sK1,sK2) ),
inference(instantiation,[status(thm)],[113]) ).
fof(l33_tsp_2,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v2_pre_topc(A)
& l1_pre_topc(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& v2_tsp_2(B,A)
& m2_tsp_1(B,A) )
=> ! [C] :
( ( v1_funct_1(C)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v5_pre_topc(C,A,B)
& m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
=> ( v3_borsuk_1(C,A,B)
=> ! [D] :
( m1_subset_1(D,u1_struct_0(A))
=> ! [E] :
( m1_subset_1(E,u1_struct_0(B))
=> ( D = E
=> k5_pre_topc(A,B,C,k6_pre_topc(B,k1_struct_0(B,E))) = k6_pre_topc(A,k1_struct_0(A,D)) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l33_tsp_2) ).
cnf(154,plain,
( ~ m2_tsp_1(X0,X1)
| ~ l1_pre_topc(X1)
| X2 != X3
| ~ v2_tsp_2(X0,X1)
| ~ v2_pre_topc(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X0))
| ~ v5_pre_topc(X4,X1,X0)
| ~ m2_relset_1(X4,u1_struct_0(X1),u1_struct_0(X0))
| ~ v3_borsuk_1(X4,X1,X0)
| k5_pre_topc(X1,X0,X4,k6_pre_topc(X0,k1_struct_0(X0,X3))) = k6_pre_topc(X1,k1_struct_0(X1,X2))
| v3_struct_0(X1)
| v3_struct_0(X0) ),
inference(cnf,[status(esa)],[l33_tsp_2]) ).
cnf(l2729,plain,
( ~ m2_tsp_1(sK2,sK1)
| ~ l1_pre_topc(sK1)
| sK3 != sK4
| ~ v2_tsp_2(sK2,sK1)
| ~ v2_pre_topc(sK1)
| ~ m1_subset_1(sK3,u1_struct_0(sK1))
| ~ m1_subset_1(sK4,u1_struct_0(sK2))
| ~ v1_funct_1(k1_tsp_2(sK1,sK2))
| ~ v1_funct_2(k1_tsp_2(sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK2),sK1,sK2)
| ~ m2_relset_1(k1_tsp_2(sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v3_borsuk_1(k1_tsp_2(sK1,sK2),sK1,sK2)
| k5_pre_topc(sK1,sK2,k1_tsp_2(sK1,sK2),k6_pre_topc(sK2,k1_struct_0(sK2,sK4))) = k6_pre_topc(sK1,k1_struct_0(sK1,sK3))
| v3_struct_0(sK1)
| v3_struct_0(sK2) ),
inference(instantiation,[status(thm)],[154]) ).
cnf(1,plain,
v2_pre_topc(sK1),
inference(cnf,[status(esa)],[t24_tsp_2_negated]) ).
cnf(l103,plain,
v2_pre_topc(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2763,plain,
l1_pre_topc(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(111,plain,
( ~ l1_pre_topc(X0)
| ~ v2_tsp_2(X1,X0)
| ~ v2_pre_topc(X0)
| ~ m1_pre_topc(X1,X0)
| v3_struct_0(X0)
| v3_struct_0(X1)
| v1_funct_1(k1_tsp_2(X0,X1)) ),
inference(cnf,[status(esa)],[dt_k1_tsp_2]) ).
cnf(l12,plain,
( ~ l1_pre_topc(sK1)
| ~ v2_tsp_2(sK2,sK1)
| ~ v2_pre_topc(sK1)
| ~ m1_pre_topc(sK2,sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| v1_funct_1(k1_tsp_2(sK1,sK2)) ),
inference(instantiation,[status(thm)],[111]) ).
cnf(l136,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[3]) ).
cnf(l50,plain,
v2_pre_topc(sK1),
inference(instantiation,[status(thm)],[1]) ).
fof(redefinition_m2_tsp_1,plain,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( m2_tsp_1(B,A)
<=> m1_pre_topc(B,A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_tsp_1) ).
cnf(206,plain,
( ~ m2_tsp_1(X0,X1)
| ~ l1_pre_topc(X1)
| m1_pre_topc(X0,X1) ),
inference(cnf,[status(esa)],[redefinition_m2_tsp_1]) ).
cnf(l2724,plain,
( ~ m2_tsp_1(sK2,sK1)
| ~ l1_pre_topc(sK1)
| m1_pre_topc(sK2,sK1) ),
inference(instantiation,[status(thm)],[206]) ).
cnf(114,plain,
( ~ l1_pre_topc(X0)
| ~ v2_tsp_2(X1,X0)
| ~ v2_pre_topc(X0)
| ~ m1_pre_topc(X1,X0)
| v3_struct_0(X0)
| v3_struct_0(X1)
| m2_relset_1(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf,[status(esa)],[dt_k1_tsp_2]) ).
cnf(l2773,plain,
( ~ l1_pre_topc(sK1)
| ~ v2_tsp_2(sK2,sK1)
| ~ v2_pre_topc(sK1)
| ~ m1_pre_topc(sK2,sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| m2_relset_1(k1_tsp_2(sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK2)) ),
inference(instantiation,[status(thm)],[114]) ).
cnf(l2844,plain,
( ~ l1_pre_topc(sK1)
| ~ v2_tsp_2(sK2,sK1)
| ~ v2_pre_topc(sK1)
| ~ m1_pre_topc(sK2,sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| v5_pre_topc(k1_tsp_2(sK1,sK2),sK1,sK2) ),
inference(instantiation,[status(thm)],[113]) ).
cnf(l3271,plain,
l1_pre_topc(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(5,plain,
m2_tsp_1(sK2,sK1),
inference(cnf,[status(esa)],[t24_tsp_2_negated]) ).
cnf(l2742,plain,
m2_tsp_1(sK2,sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3275,plain,
v2_pre_topc(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l28,plain,
l1_pre_topc(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l317,plain,
v2_pre_topc(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l4700,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[3]) ).
cnf(112,plain,
( ~ l1_pre_topc(X0)
| ~ v2_tsp_2(X1,X0)
| ~ v2_pre_topc(X0)
| ~ m1_pre_topc(X1,X0)
| v3_struct_0(X0)
| v3_struct_0(X1)
| v1_funct_2(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf,[status(esa)],[dt_k1_tsp_2]) ).
cnf(l2743,plain,
( ~ l1_pre_topc(sK1)
| ~ v2_tsp_2(sK2,sK1)
| ~ v2_pre_topc(sK1)
| ~ m1_pre_topc(sK2,sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| v1_funct_2(k1_tsp_2(sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK2)) ),
inference(instantiation,[status(thm)],[112]) ).
cnf(l2739,plain,
( ~ l1_pre_topc(sK1)
| ~ v2_tsp_2(sK2,sK1)
| ~ v2_pre_topc(sK1)
| ~ m1_pre_topc(sK2,sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| m2_relset_1(k1_tsp_2(sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK2)) ),
inference(instantiation,[status(thm)],[114]) ).
cnf(l306,plain,
( ~ l1_pre_topc(sK1)
| ~ v2_tsp_2(sK2,sK1)
| ~ v2_pre_topc(sK1)
| ~ m1_pre_topc(sK2,sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| v1_funct_2(k1_tsp_2(sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK2)) ),
inference(instantiation,[status(thm)],[112]) ).
cnf(l2731,plain,
v2_pre_topc(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3722,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1920,plain,
( ~ m2_tsp_1(sK2,sK1)
| ~ l1_pre_topc(sK1)
| m1_pre_topc(sK2,sK1) ),
inference(instantiation,[status(thm)],[206]) ).
cnf(4,plain,
v2_tsp_2(sK2,sK1),
inference(cnf,[status(esa)],[t24_tsp_2_negated]) ).
cnf(l334,plain,
v2_tsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2971,plain,
v2_tsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l4702,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3074,plain,
l1_pre_topc(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3073,plain,
l1_pre_topc(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l4701,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3281,plain,
v2_tsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l111,plain,
v2_tsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l3712,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[3]) ).
cnf(l331,plain,
l1_pre_topc(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2843,plain,
v2_tsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l316,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3076,plain,
v2_pre_topc(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2750,plain,
l1_pre_topc(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2916,plain,
( ~ m2_tsp_1(sK2,sK1)
| ~ l1_pre_topc(sK1)
| m1_pre_topc(sK2,sK1) ),
inference(instantiation,[status(thm)],[206]) ).
cnf(l2879,plain,
v2_pre_topc(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3723,plain,
l1_pre_topc(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2762,plain,
v2_tsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2732,plain,
m2_tsp_1(sK2,sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1166,plain,
v2_tsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l24,plain,
v2_tsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l866,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[3]) ).
cnf(l868,plain,
( ~ m2_tsp_1(sK2,sK1)
| ~ l1_pre_topc(sK1)
| m1_pre_topc(sK2,sK1) ),
inference(instantiation,[status(thm)],[206]) ).
cnf(l1924,plain,
l1_pre_topc(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1634,plain,
m2_tsp_1(sK2,sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l4703,plain,
( ~ m2_tsp_1(sK2,sK1)
| ~ l1_pre_topc(sK1)
| m1_pre_topc(sK2,sK1) ),
inference(instantiation,[status(thm)],[206]) ).
cnf(9,plain,
k5_pre_topc(sK1,sK2,k1_tsp_2(sK1,sK2),k6_pre_topc(sK2,k1_struct_0(sK2,sK4))) != k6_pre_topc(sK1,k1_struct_0(sK1,sK3)),
inference(cnf,[status(esa)],[t24_tsp_2_negated]) ).
cnf(l2771,plain,
k5_pre_topc(sK1,sK2,k1_tsp_2(sK1,sK2),k6_pre_topc(sK2,k1_struct_0(sK2,sK4))) != k6_pre_topc(sK1,k1_struct_0(sK1,sK3)),
inference(instantiation,[status(thm)],[9]) ).
cnf(l4716,plain,
l1_pre_topc(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l876,plain,
l1_pre_topc(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1596,plain,
l1_pre_topc(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2850,plain,
( ~ m2_tsp_1(sK2,sK1)
| ~ l1_pre_topc(sK1)
| m1_pre_topc(sK2,sK1) ),
inference(instantiation,[status(thm)],[206]) ).
cnf(l4714,plain,
m2_tsp_1(sK2,sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l2872,plain,
l1_pre_topc(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2849,plain,
( ~ l1_pre_topc(sK1)
| ~ v2_tsp_2(sK2,sK1)
| ~ v2_pre_topc(sK1)
| ~ m1_pre_topc(sK2,sK1)
| v3_struct_0(sK1)
| v3_struct_0(sK2)
| v1_funct_1(k1_tsp_2(sK1,sK2)) ),
inference(instantiation,[status(thm)],[111]) ).
cnf(l2,plain,
m2_tsp_1(sK2,sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l2754,plain,
v2_pre_topc(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2734,plain,
l1_pre_topc(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(6,plain,
m1_subset_1(sK3,u1_struct_0(sK1)),
inference(cnf,[status(esa)],[t24_tsp_2_negated]) ).
cnf(l2779,plain,
m1_subset_1(sK3,u1_struct_0(sK1)),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2887,plain,
l1_pre_topc(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1923,plain,
m2_tsp_1(sK2,sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3718,plain,
m2_tsp_1(sK2,sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3091,plain,
v2_pre_topc(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(7,plain,
m1_subset_1(sK4,u1_struct_0(sK2)),
inference(cnf,[status(esa)],[t24_tsp_2_negated]) ).
cnf(l2840,plain,
m1_subset_1(sK4,u1_struct_0(sK2)),
inference(instantiation,[status(thm)],[7]) ).
cnf(l3088,plain,
( ~ m2_tsp_1(sK2,sK1)
| ~ l1_pre_topc(sK1)
| m1_pre_topc(sK2,sK1) ),
inference(instantiation,[status(thm)],[206]) ).
cnf(l2875,plain,
v2_tsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l3700,plain,
~ v3_struct_0(sK2),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3089,plain,
m2_tsp_1(sK2,sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l865,plain,
v2_pre_topc(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(8,plain,
sK3 = sK4,
inference(cnf,[status(esa)],[t24_tsp_2_negated]) ).
cnf(l2730,plain,
sK3 = sK4,
inference(instantiation,[status(thm)],[8]) ).
cnf(l2855,plain,
v2_tsp_2(sK2,sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2758,plain,
( ~ m2_tsp_1(sK2,sK1)
| ~ l1_pre_topc(sK1)
| m1_pre_topc(sK2,sK1) ),
inference(instantiation,[status(thm)],[206]) ).
cnf(l2774,plain,
l1_pre_topc(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2871,plain,
m2_tsp_1(sK2,sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3092,plain,
l1_pre_topc(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2776,plain,
m2_tsp_1(sK2,sK1),
inference(instantiation,[status(thm)],[5]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l3352,l3,l315,l2729,l103,l2763,l12,l136,l50,l2724,l2773,l2844,l3271,l2742,l3275,l28,l317,l4700,l2743,l2739,l306,l2731,l3722,l1920,l334,l2971,l4702,l3074,l3073,l4701,l3281,l111,l3712,l331,l2843,l316,l3076,l2750,l2916,l2879,l3723,l2762,l2732,l1166,l24,l866,l868,l1924,l1634,l4703,l2771,l4716,l876,l1596,l2850,l4714,l2872,l2849,l2,l2754,l2734,l2779,l2887,l1923,l3718,l3091,l2840,l3088,l2875,l3700,l3089,l865,l2730,l2855,l2758,l2774,l2871,l3092,l2776]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : TOP035+1 : TPTP v9.0.0. Released v3.4.0.
% 0.00/0.10 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.30 % Computer : n024.cluster.edu
% 0.10/0.30 % Model : x86_64 x86_64
% 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.30 % Memory : 8042.1875MB
% 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.30 % CPULimit : 300
% 0.10/0.30 % WCLimit : 300
% 0.10/0.30 % DateTime : Tue Jul 22 21:43:34 EDT 2025
% 0.10/0.30 % CPUTime :
% 0.10/0.31 % launching worker at depth: 2
% 0.10/0.31 % launching worker at depth: 3
% 0.10/0.31 % launching worker at depth: 7
% 0.10/0.31 % launching worker at depth: 5
% 0.10/0.31 % launching worker at depth: 6
% 0.10/0.31 % launching worker at depth: 1
% 0.10/0.31 % launching worker at depth: 8
% 0.10/0.31 % launching worker at depth: 4
% 0.10/0.32 % launching worker at depth: 9
% 0.10/0.35 % launching worker at depth: 10
% 0.15/0.71 % launching worker at depth: 11
% 58.12/7.66 % launching worker at depth: 12
% 140.24/17.95 % SZS status Theorem for theBenchmark
% 140.24/17.95 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------