%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : TOP035+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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 : Sun Sep 27 09:53:01 AM UTC 2026
% Result : Theorem 10.39s 6.73s
% Output : CNFRefutation 10.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 5
% Syntax : Number of formulae : 85 ( 19 unt; 0 def)
% Number of atoms : 542 ( 58 equ)
% Maximal formula atoms : 18 ( 6 avg)
% Number of connectives : 790 ( 333 ~; 385 |; 48 &)
% ( 2 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 7 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 : 78 ( 0 sgn 20 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d9_tsp_2,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m2_tsp_1(B,A)
& v2_tsp_2(B,A)
& ~ v3_struct_0(B) )
=> ! [C] :
( ( m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v5_pre_topc(C,A,B)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C) )
=> ( C = k1_tsp_2(A,B)
<=> v3_borsuk_1(C,A,B) ) ) ) ),
file('theBenchmark.p',d9_tsp_2) ).
fof(dt_k1_tsp_2,axiom,
! [A,B] :
( ( m1_pre_topc(B,A)
& v2_tsp_2(B,A)
& ~ v3_struct_0(B)
& l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ( m2_relset_1(k1_tsp_2(A,B),u1_struct_0(A),u1_struct_0(B))
& v5_pre_topc(k1_tsp_2(A,B),A,B)
& v1_funct_2(k1_tsp_2(A,B),u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(k1_tsp_2(A,B)) ) ),
file('theBenchmark.p',dt_k1_tsp_2) ).
fof(l33_tsp_2,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m2_tsp_1(B,A)
& v2_tsp_2(B,A)
& ~ v3_struct_0(B) )
=> ! [C] :
( ( m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v5_pre_topc(C,A,B)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C) )
=> ( 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('theBenchmark.p',l33_tsp_2) ).
fof(redefinition_m2_tsp_1,axiom,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( m2_tsp_1(B,A)
<=> m1_pre_topc(B,A) ) ),
file('theBenchmark.p',redefinition_m2_tsp_1) ).
fof(t24_tsp_2,conjecture,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m2_tsp_1(B,A)
& v2_tsp_2(B,A)
& ~ v3_struct_0(B) )
=> ! [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('theBenchmark.p',t24_tsp_2) ).
fof(t24_tsp_2_neg,negated_conjecture,
~ ! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m2_tsp_1(B,A)
& v2_tsp_2(B,A)
& ~ v3_struct_0(B) )
=> ! [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(assume_negation,[status(cth)],[t24_tsp_2]) ).
fof(nnf_110,plain,
? [A] :
( ? [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))
& D = C
& m1_subset_1(D,u1_struct_0(B)) )
& m1_subset_1(C,u1_struct_0(A)) )
& m2_tsp_1(B,A)
& v2_tsp_2(B,A)
& ~ v3_struct_0(B) )
& l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t24_tsp_2_neg]) ).
fof(sk_t24_tsp_2_neg,plain,
( k5_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),k6_pre_topc(sK0,k1_struct_0(sK0,sK3))) != k6_pre_topc(sK1,k1_struct_0(sK1,sK2))
& sK3 = sK2
& m1_subset_1(sK3,u1_struct_0(sK0))
& m1_subset_1(sK2,u1_struct_0(sK1))
& m2_tsp_1(sK0,sK1)
& v2_tsp_2(sK0,sK1)
& ~ v3_struct_0(sK0)
& l1_pre_topc(sK1)
& v2_pre_topc(sK1)
& ~ v3_struct_0(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK0,sK2,sK3]),skolemize(A,sK1),skolemize(B,sK0),skolemize(C,sK2),skolemize(D,sK3)],[nnf_110]) ).
cnf(c_111,negated_conjecture,
v2_tsp_2(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_t24_tsp_2_neg]) ).
cnf(c_112,plain,
( k5_pre_topc(A,B,C,k6_pre_topc(B,k1_struct_0(B,E))) = k6_pre_topc(A,k1_struct_0(A,D))
| E != D
| ~ m1_subset_1(E,u1_struct_0(B))
| ~ m1_subset_1(D,u1_struct_0(A))
| ~ v3_borsuk_1(C,A,B)
| ~ m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
| ~ v5_pre_topc(C,A,B)
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(C)
| ~ m2_tsp_1(B,A)
| ~ v2_tsp_2(B,A)
| v3_struct_0(B)
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[l33_tsp_2]) ).
cnf(c_113,plain,
( m2_relset_1(k1_tsp_2(A,B),u1_struct_0(A),u1_struct_0(B))
| ~ m1_pre_topc(B,A)
| ~ v2_tsp_2(B,A)
| v3_struct_0(B)
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k1_tsp_2]) ).
cnf(c_114,plain,
( v5_pre_topc(k1_tsp_2(A,B),A,B)
| ~ m1_pre_topc(B,A)
| ~ v2_tsp_2(B,A)
| v3_struct_0(B)
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k1_tsp_2]) ).
cnf(c_115,plain,
( v1_funct_2(k1_tsp_2(A,B),u1_struct_0(A),u1_struct_0(B))
| ~ m1_pre_topc(B,A)
| ~ v2_tsp_2(B,A)
| v3_struct_0(B)
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k1_tsp_2]) ).
cnf(c_116,plain,
( v1_funct_1(k1_tsp_2(A,B))
| ~ m1_pre_topc(B,A)
| ~ v2_tsp_2(B,A)
| v3_struct_0(B)
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k1_tsp_2]) ).
cnf(c_118,plain,
( v3_borsuk_1(C,A,B)
| k1_tsp_2(A,B) != C
| ~ m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
| ~ v5_pre_topc(C,A,B)
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(C)
| ~ m2_tsp_1(B,A)
| ~ v2_tsp_2(B,A)
| v3_struct_0(B)
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d9_tsp_2]) ).
cnf(c_207,negated_conjecture,
( v1_funct_1(k1_tsp_2(sK1,sK0))
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_111,c_116]) ).
cnf(c_208,negated_conjecture,
( k5_pre_topc(sK1,sK0,A,k6_pre_topc(sK0,k1_struct_0(sK0,C))) = k6_pre_topc(sK1,k1_struct_0(sK1,B))
| C != B
| ~ m1_subset_1(C,u1_struct_0(sK0))
| ~ m1_subset_1(B,u1_struct_0(sK1))
| ~ v3_borsuk_1(A,sK1,sK0)
| ~ m2_relset_1(A,u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(A,sK1,sK0)
| ~ v1_funct_2(A,u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_111,c_112]) ).
cnf(c_212,negated_conjecture,
( v3_borsuk_1(A,sK1,sK0)
| k1_tsp_2(sK1,sK0) != A
| ~ m2_relset_1(A,u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(A,sK1,sK0)
| ~ v1_funct_2(A,u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_111,c_118]) ).
cnf(c_376,plain,
( m1_pre_topc(B,A)
| ~ m2_tsp_1(B,A)
| ~ l1_pre_topc(A) ),
inference(clausify,[status(thm)],[redefinition_m2_tsp_1]) ).
cnf(c_385,negated_conjecture,
~ v3_struct_0(sK1),
inference(split_conjunct,[status(thm)],[sk_t24_tsp_2_neg]) ).
cnf(c_386,negated_conjecture,
v2_pre_topc(sK1),
inference(split_conjunct,[status(thm)],[sk_t24_tsp_2_neg]) ).
cnf(c_387,negated_conjecture,
l1_pre_topc(sK1),
inference(split_conjunct,[status(thm)],[sk_t24_tsp_2_neg]) ).
cnf(c_388,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t24_tsp_2_neg]) ).
cnf(c_389,negated_conjecture,
m2_tsp_1(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_t24_tsp_2_neg]) ).
cnf(c_390,negated_conjecture,
m1_subset_1(sK2,u1_struct_0(sK1)),
inference(split_conjunct,[status(thm)],[sk_t24_tsp_2_neg]) ).
cnf(c_391,negated_conjecture,
m1_subset_1(sK3,u1_struct_0(sK0)),
inference(split_conjunct,[status(thm)],[sk_t24_tsp_2_neg]) ).
cnf(c_392,negated_conjecture,
sK3 = sK2,
inference(split_conjunct,[status(thm)],[sk_t24_tsp_2_neg]) ).
cnf(c_393,negated_conjecture,
k5_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),k6_pre_topc(sK0,k1_struct_0(sK0,sK3))) != k6_pre_topc(sK1,k1_struct_0(sK1,sK2)),
inference(split_conjunct,[status(thm)],[sk_t24_tsp_2_neg]) ).
cnf(c_394,negated_conjecture,
( m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_111,c_113]) ).
cnf(c_7143,negated_conjecture,
( m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_385,c_394]) ).
cnf(c_7144,negated_conjecture,
( m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_386,c_7143]) ).
cnf(c_7145,negated_conjecture,
( m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_387,c_7144]) ).
cnf(c_395,negated_conjecture,
( m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m1_pre_topc(sK0,sK1) ),
inference(resolve,[status(thm)],[c_388,c_7145]) ).
cnf(c_396,negated_conjecture,
( v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_111,c_114]) ).
cnf(c_7146,negated_conjecture,
( v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_385,c_396]) ).
cnf(c_7147,negated_conjecture,
( v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_386,c_7146]) ).
cnf(c_7148,negated_conjecture,
( v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_387,c_7147]) ).
cnf(c_397,negated_conjecture,
( v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m1_pre_topc(sK0,sK1) ),
inference(resolve,[status(thm)],[c_388,c_7148]) ).
cnf(c_398,negated_conjecture,
( v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_111,c_115]) ).
cnf(c_7149,negated_conjecture,
( v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_385,c_398]) ).
cnf(c_7150,negated_conjecture,
( v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_386,c_7149]) ).
cnf(c_7151,negated_conjecture,
( v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_387,c_7150]) ).
cnf(c_399,negated_conjecture,
( v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m1_pre_topc(sK0,sK1) ),
inference(resolve,[status(thm)],[c_388,c_7151]) ).
cnf(c_427,negated_conjecture,
( k5_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),k6_pre_topc(sK0,k1_struct_0(sK0,B))) = k6_pre_topc(sK1,k1_struct_0(sK1,A))
| B != A
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_207,c_208]) ).
cnf(c_7152,negated_conjecture,
( k5_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),k6_pre_topc(sK0,k1_struct_0(sK0,B))) = k6_pre_topc(sK1,k1_struct_0(sK1,A))
| B != A
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_427]) ).
cnf(c_7153,negated_conjecture,
( k5_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),k6_pre_topc(sK0,k1_struct_0(sK0,B))) = k6_pre_topc(sK1,k1_struct_0(sK1,A))
| B != A
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_7152]) ).
cnf(c_7154,negated_conjecture,
( k5_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),k6_pre_topc(sK0,k1_struct_0(sK0,B))) = k6_pre_topc(sK1,k1_struct_0(sK1,A))
| B != A
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_7153]) ).
cnf(c_7155,negated_conjecture,
( k5_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),k6_pre_topc(sK0,k1_struct_0(sK0,B))) = k6_pre_topc(sK1,k1_struct_0(sK1,A))
| B != A
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_7154]) ).
cnf(c_7156,negated_conjecture,
( k5_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),k6_pre_topc(sK0,k1_struct_0(sK0,B))) = k6_pre_topc(sK1,k1_struct_0(sK1,A))
| B != A
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_385,c_7155]) ).
cnf(c_7157,negated_conjecture,
( k5_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),k6_pre_topc(sK0,k1_struct_0(sK0,B))) = k6_pre_topc(sK1,k1_struct_0(sK1,A))
| B != A
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_386,c_7156]) ).
cnf(c_7158,negated_conjecture,
( k5_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),k6_pre_topc(sK0,k1_struct_0(sK0,B))) = k6_pre_topc(sK1,k1_struct_0(sK1,A))
| B != A
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_387,c_7157]) ).
cnf(c_7159,negated_conjecture,
( k5_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),k6_pre_topc(sK0,k1_struct_0(sK0,B))) = k6_pre_topc(sK1,k1_struct_0(sK1,A))
| B != A
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| ~ m1_pre_topc(sK0,sK1) ),
inference(resolve,[status(thm)],[c_388,c_7158]) ).
cnf(c_428,negated_conjecture,
( k5_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),k6_pre_topc(sK0,k1_struct_0(sK0,B))) = k6_pre_topc(sK1,k1_struct_0(sK1,A))
| B != A
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m1_pre_topc(sK0,sK1) ),
inference(resolve,[status(thm)],[c_389,c_7159]) ).
cnf(c_433,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1)
| v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| k1_tsp_2(sK1,sK0) != k1_tsp_2(sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_212,c_207]) ).
cnf(c_7160,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1)
| v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_433]) ).
cnf(c_7161,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_7160]) ).
cnf(c_7162,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_7161]) ).
cnf(c_7163,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_7162]) ).
cnf(c_7164,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_7163]) ).
cnf(c_7165,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_385,c_7164]) ).
cnf(c_7166,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_386,c_7165]) ).
cnf(c_7167,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_387,c_7166]) ).
cnf(c_7168,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1) ),
inference(resolve,[status(thm)],[c_388,c_7167]) ).
cnf(c_434,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_389,c_7168]) ).
cnf(c_7169,negated_conjecture,
( m1_pre_topc(sK0,sK1)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_389,c_376]) ).
cnf(c_610,negated_conjecture,
m1_pre_topc(sK0,sK1),
inference(resolve,[status(thm)],[c_387,c_7169]) ).
cnf(c_614,negated_conjecture,
( v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_610,c_434]) ).
cnf(c_617,negated_conjecture,
( k5_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),k6_pre_topc(sK0,k1_struct_0(sK0,B))) = k6_pre_topc(sK1,k1_struct_0(sK1,A))
| B != A
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_610,c_428]) ).
cnf(c_622,negated_conjecture,
v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_610,c_399]) ).
cnf(c_623,negated_conjecture,
v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0),
inference(resolve,[status(thm)],[c_610,c_397]) ).
cnf(c_624,negated_conjecture,
m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_610,c_395]) ).
cnf(c_7170,negated_conjecture,
( k5_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),k6_pre_topc(sK0,k1_struct_0(sK0,B))) = k6_pre_topc(sK1,k1_struct_0(sK1,A))
| B != A
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0) ),
inference(resolve,[status(thm)],[c_622,c_617]) ).
cnf(c_7171,negated_conjecture,
( k5_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),k6_pre_topc(sK0,k1_struct_0(sK0,B))) = k6_pre_topc(sK1,k1_struct_0(sK1,A))
| B != A
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_623,c_7170]) ).
cnf(c_625,negated_conjecture,
( k5_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),k6_pre_topc(sK0,k1_struct_0(sK0,B))) = k6_pre_topc(sK1,k1_struct_0(sK1,A))
| B != A
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0) ),
inference(resolve,[status(thm)],[c_624,c_7171]) ).
cnf(c_7172,negated_conjecture,
( v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0) ),
inference(resolve,[status(thm)],[c_622,c_614]) ).
cnf(c_7173,negated_conjecture,
( v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_623,c_7172]) ).
cnf(c_626,negated_conjecture,
v3_borsuk_1(k1_tsp_2(sK1,sK0),sK1,sK0),
inference(resolve,[status(thm)],[c_624,c_7173]) ).
cnf(c_627,negated_conjecture,
( k5_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),k6_pre_topc(sK0,k1_struct_0(sK0,B))) = k6_pre_topc(sK1,k1_struct_0(sK1,A))
| B != A
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK1)) ),
inference(resolve,[status(thm)],[c_626,c_625]) ).
cnf(c_660,plain,
m1_subset_1(sK2,u1_struct_0(sK0)),
inference(paramod,[status(thm)],[c_392,c_391]) ).
cnf(c_661,plain,
k5_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),k6_pre_topc(sK0,k1_struct_0(sK0,sK2))) != k6_pre_topc(sK1,k1_struct_0(sK1,sK2)),
inference(paramod,[status(thm)],[c_392,c_393]) ).
cnf(c_7174,negated_conjecture,
( k5_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),k6_pre_topc(sK0,k1_struct_0(sK0,A))) = k6_pre_topc(sK1,k1_struct_0(sK1,sK2))
| A != sK2
| ~ m1_subset_1(A,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_627,c_390]) ).
cnf(c_1567,negated_conjecture,
( k5_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),k6_pre_topc(sK0,k1_struct_0(sK0,A))) = k6_pre_topc(sK1,k1_struct_0(sK1,sK2))
| sK2 != A
| ~ m1_subset_1(A,u1_struct_0(sK0)) ),
inference(copy,[status(thm)],[c_7174]) ).
cnf(c_7175,plain,
( k5_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),k6_pre_topc(sK0,k1_struct_0(sK0,sK2))) = k6_pre_topc(sK1,k1_struct_0(sK1,sK2))
| sK2 != sK2 ),
inference(resolve,[status(thm)],[c_1567,c_660]) ).
cnf(c_7176,plain,
k5_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),k6_pre_topc(sK0,k1_struct_0(sK0,sK2))) = k6_pre_topc(sK1,k1_struct_0(sK1,sK2)),
inference(copy,[status(thm)],[c_7175]) ).
cnf(c_7142,plain,
$false,
inference(resolve,[status(thm)],[c_661,c_7176]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP035+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/5.37 % Computer : n001.cluster.edu
% 0.11/5.37 % Model : x86_64 x86_64
% 0.11/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.37 % Memory : 8046.5625MB
% 0.11/5.37 % OS : Linux 6.8.0-71-generic
% 0.11/5.37 % CPULimit : 300
% 0.11/5.37 % WCLimit : 300
% 0.11/5.37 % DateTime : Sat Sep 26 20:45:05 UTC 2026
% 0.11/5.37 % CPUTime :
% 0.11/5.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/5.37 % Process 2624152 was started by sandbox on n001,
% 0.11/5.37 % Sat Sep 26 20:45:05 2026
% 0.11/5.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.14/5.40
% 0.14/5.40 % From the command line: assign(max_seconds, 300).
% 10.39/6.73
% 10.39/6.73 % given #500 (A,wt=21): 672 v4_membered(k1_tarski(f3(A))) | -v4_membered(A). [resolve(415,c,321,a)].
% 10.39/6.73
% 10.39/6.73 % given #1000 (T,wt=17): 3374 -v5_membered(u1_struct_0(c6)) | v4_membered(k1_struct_0(c6,c7)). [resolve(878,a,303,b)].
% 10.39/6.73
% 10.39/6.73 % given #1500 (T,wt=21): 4125 f13(f5(c5)) = f11(c1). [resolve(1072,a,713,a),flip(a)].
% 10.39/6.73
% 10.39/6.73 % given #2000 (T,wt=22): 5697 v3_tops_1(k1_xboole_0,f1(f1(c6))). [resolve(3709,a,997,a),unit_del(a,3708)].
% 10.39/6.73
% 10.39/6.73 % SZS status Theorem for theBenchmark
% 10.39/6.73
% 10.39/6.73 % Proof 1 at 1.06 (+ 0.24) seconds.
% 10.39/6.73 % Length of proof is 48.
% 10.39/6.73 % Level of proof is 9.
% 10.39/6.73 % Maximum clause weight is 79.000.
% 10.39/6.73 % Given clauses 2114.
% 10.39/6.73
% 10.39/6.73 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------