%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : TOP035+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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 : Thu Sep 24 03:53:28 PM UTC 2026
% Result : Theorem 0.17s 0.48s
% Output : CNFRefutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 21
% Syntax : Number of formulae : 103 ( 21 unt; 16 def)
% Number of atoms : 493 ( 29 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 656 ( 266 ~; 294 |; 54 &)
% ( 20 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 30 ( 28 usr; 17 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-4 aty)
% Number of variables : 83 ( 79 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,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(negated_conjecture,[status(cth)],[f1]) ).
fof(f50,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f86,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f102,axiom,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( m2_tsp_1(B,A)
<=> m1_pre_topc(B,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f112,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))
& C = D
& 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(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f113,plain,
( k5_pre_topc(sK0_skl,sK1_skl,k1_tsp_2(sK0_skl,sK1_skl),k6_pre_topc(sK1_skl,k1_struct_0(sK1_skl,sK3_skl))) != k6_pre_topc(sK0_skl,k1_struct_0(sK0_skl,sK2_skl))
& sK2_skl = sK3_skl
& m1_subset_1(sK3_skl,u1_struct_0(sK1_skl))
& m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))
& m2_tsp_1(sK1_skl,sK0_skl)
& v2_tsp_2(sK1_skl,sK0_skl)
& ~ v3_struct_0(sK1_skl)
& l1_pre_topc(sK0_skl)
& v2_pre_topc(sK0_skl)
& ~ v3_struct_0(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl),skolemize(D,sK3_skl)],[f112]) ).
fof(f114,plain,
~ v3_struct_0(sK0_skl),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f115,plain,
v2_pre_topc(sK0_skl),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f116,plain,
l1_pre_topc(sK0_skl),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f117,plain,
~ v3_struct_0(sK1_skl),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f118,plain,
v2_tsp_2(sK1_skl,sK0_skl),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f119,plain,
m2_tsp_1(sK1_skl,sK0_skl),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f120,plain,
m1_subset_1(sK2_skl,u1_struct_0(sK0_skl)),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f121,plain,
m1_subset_1(sK3_skl,u1_struct_0(sK1_skl)),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f122,plain,
sK2_skl = sK3_skl,
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f123,plain,
k5_pre_topc(sK0_skl,sK1_skl,k1_tsp_2(sK0_skl,sK1_skl),k6_pre_topc(sK1_skl,k1_struct_0(sK1_skl,sK3_skl))) != k6_pre_topc(sK0_skl,k1_struct_0(sK0_skl,sK2_skl)),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f304,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( C = k1_tsp_2(A,B)
<=> 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(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f305,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ~ v3_borsuk_1(C,A,B)
| C = k1_tsp_2(A,B) )
& ( v3_borsuk_1(C,A,B)
| C != k1_tsp_2(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(NNF_transformation,[status(thm)],[f304]) ).
fof(f306,plain,
! [X0,X1,X2] :
( v3_borsuk_1(X2,X0,X1)
| X2 != k1_tsp_2(X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ m2_tsp_1(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f305]) ).
fof(f310,plain,
! [A,B] :
( ( 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)) )
| ~ 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(pre_NNF_transformation,[status(thm)],[f54]) ).
fof(f311,plain,
! [X0,X1] :
( v1_funct_1(k1_tsp_2(X0,X1))
| ~ m1_pre_topc(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f310]) ).
fof(f312,plain,
! [X0,X1] :
( v1_funct_2(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_pre_topc(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f310]) ).
fof(f313,plain,
! [X0,X1] :
( v5_pre_topc(k1_tsp_2(X0,X1),X0,X1)
| ~ m1_pre_topc(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f310]) ).
fof(f314,plain,
! [X0,X1] :
( m2_relset_1(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_pre_topc(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f310]) ).
fof(f378,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [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))
| D != E
| ~ 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(pre_NNF_transformation,[status(thm)],[f86]) ).
fof(f379,plain,
! [X0,X1,X2,X3,X4] :
( k5_pre_topc(X0,X1,X2,k6_pre_topc(X1,k1_struct_0(X1,X4))) = k6_pre_topc(X0,k1_struct_0(X0,X3))
| X3 != X4
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ v3_borsuk_1(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ m2_tsp_1(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f378]) ).
fof(f457,plain,
! [A] :
( ! [B] :
( m2_tsp_1(B,A)
<=> m1_pre_topc(B,A) )
| ~ l1_pre_topc(A) ),
inference(pre_NNF_transformation,[status(thm)],[f102]) ).
fof(f458,plain,
! [A] :
( ! [B] :
( ( ~ m1_pre_topc(B,A)
| m2_tsp_1(B,A) )
& ( m1_pre_topc(B,A)
| ~ m2_tsp_1(B,A) ) )
| ~ l1_pre_topc(A) ),
inference(NNF_transformation,[status(thm)],[f457]) ).
fof(f459,plain,
! [A] :
( ( ! [B] :
( ~ m1_pre_topc(B,A)
| m2_tsp_1(B,A) )
& ! [B] :
( m1_pre_topc(B,A)
| ~ m2_tsp_1(B,A) ) )
| ~ l1_pre_topc(A) ),
inference(miniscoping,[status(thm)],[f458]) ).
fof(f460,plain,
! [X0,X1] :
( m1_pre_topc(X1,X0)
| ~ m2_tsp_1(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[status(thm)],[f459]) ).
fof(f486,plain,
m1_subset_1(sK2_skl,u1_struct_0(sK1_skl)),
inference(backward_demodulation,[status(thm)],[f122,f121]) ).
fof(f487,plain,
k5_pre_topc(sK0_skl,sK1_skl,k1_tsp_2(sK0_skl,sK1_skl),k6_pre_topc(sK1_skl,k1_struct_0(sK1_skl,sK2_skl))) != k6_pre_topc(sK0_skl,k1_struct_0(sK0_skl,sK2_skl)),
inference(forward_demodulation,[status(thm)],[f122,f123]) ).
fof(f489,plain,
! [X0,X1] :
( v3_borsuk_1(k1_tsp_2(X0,X1),X0,X1)
| ~ m2_relset_1(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(k1_tsp_2(X0,X1),X0,X1)
| ~ v1_funct_2(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(k1_tsp_2(X0,X1))
| ~ m2_tsp_1(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f306]) ).
fof(f490,plain,
! [X0,X1,X2,X3] :
( k5_pre_topc(X0,X1,X2,k6_pre_topc(X1,k1_struct_0(X1,X3))) = k6_pre_topc(X0,k1_struct_0(X0,X3))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ v3_borsuk_1(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ m2_tsp_1(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f379]) ).
fof(f516,definition,
( sQ6_spl
<=> l1_pre_topc(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f518,plain,
( sQ6_spl
| ~ l1_pre_topc(sK0_skl) ),
inference(component_clause,[status(thm)],[f516]) ).
fof(f523,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f518,f116]) ).
fof(f524,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f523]) ).
fof(f537,definition,
( sQ11_spl
<=> v2_pre_topc(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f539,plain,
( sQ11_spl
| ~ v2_pre_topc(sK0_skl) ),
inference(component_clause,[status(thm)],[f537]) ).
fof(f561,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f539,f115]) ).
fof(f562,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f561]) ).
fof(f565,definition,
( sQ16_spl
<=> v2_tsp_2(sK1_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f567,plain,
( sQ16_spl
| ~ v2_tsp_2(sK1_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f565]) ).
fof(f568,definition,
( sQ17_spl
<=> m2_tsp_1(sK1_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f570,plain,
( sQ17_spl
| ~ m2_tsp_1(sK1_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f568]) ).
fof(f586,plain,
! [X0,X1,X2] :
( k5_pre_topc(sK0_skl,X0,X1,k6_pre_topc(X0,k1_struct_0(X0,X2))) = k6_pre_topc(sK0_skl,k1_struct_0(sK0_skl,X2))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(sK0_skl))
| ~ v3_borsuk_1(X1,sK0_skl,X0)
| ~ m2_relset_1(X1,u1_struct_0(sK0_skl),u1_struct_0(X0))
| ~ v5_pre_topc(X1,sK0_skl,X0)
| ~ v1_funct_2(X1,u1_struct_0(sK0_skl),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ m2_tsp_1(X0,sK0_skl)
| ~ v2_tsp_2(X0,sK0_skl)
| v3_struct_0(X0)
| ~ l1_pre_topc(sK0_skl)
| ~ v2_pre_topc(sK0_skl) ),
inference(resolution,[status(thm)],[f490,f114]) ).
fof(f591,definition,
! [X0,X1,X2] :
( sQ23_spl
<=> ( k5_pre_topc(sK0_skl,X0,X1,k6_pre_topc(X0,k1_struct_0(X0,X2))) = k6_pre_topc(sK0_skl,k1_struct_0(sK0_skl,X2))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(sK0_skl))
| ~ v3_borsuk_1(X1,sK0_skl,X0)
| ~ m2_relset_1(X1,u1_struct_0(sK0_skl),u1_struct_0(X0))
| ~ v5_pre_topc(X1,sK0_skl,X0)
| ~ v1_funct_2(X1,u1_struct_0(sK0_skl),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ m2_tsp_1(X0,sK0_skl)
| ~ v2_tsp_2(X0,sK0_skl)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f592,plain,
! [X0,X1,X2] :
( ~ sQ23_spl
| k5_pre_topc(sK0_skl,X0,X1,k6_pre_topc(X0,k1_struct_0(X0,X2))) = k6_pre_topc(sK0_skl,k1_struct_0(sK0_skl,X2))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(sK0_skl))
| ~ v3_borsuk_1(X1,sK0_skl,X0)
| ~ m2_relset_1(X1,u1_struct_0(sK0_skl),u1_struct_0(X0))
| ~ v5_pre_topc(X1,sK0_skl,X0)
| ~ v1_funct_2(X1,u1_struct_0(sK0_skl),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ m2_tsp_1(X0,sK0_skl)
| ~ v2_tsp_2(X0,sK0_skl)
| v3_struct_0(X0) ),
inference(component_clause,[status(thm)],[f591]) ).
fof(f594,plain,
( sQ23_spl
| ~ sQ6_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f586,f537,f516,f591]) ).
fof(f595,plain,
! [X0,X1] :
( ~ sQ23_spl
| k5_pre_topc(sK0_skl,sK1_skl,X0,k6_pre_topc(sK1_skl,k1_struct_0(sK1_skl,X1))) = k6_pre_topc(sK0_skl,k1_struct_0(sK0_skl,X1))
| ~ m1_subset_1(X1,u1_struct_0(sK1_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK0_skl))
| ~ v3_borsuk_1(X0,sK0_skl,sK1_skl)
| ~ m2_relset_1(X0,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v5_pre_topc(X0,sK0_skl,sK1_skl)
| ~ v1_funct_2(X0,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(X0)
| ~ m2_tsp_1(sK1_skl,sK0_skl)
| ~ v2_tsp_2(sK1_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f592,f117]) ).
fof(f597,definition,
! [X0,X1] :
( sQ24_spl
<=> ( k5_pre_topc(sK0_skl,sK1_skl,X0,k6_pre_topc(sK1_skl,k1_struct_0(sK1_skl,X1))) = k6_pre_topc(sK0_skl,k1_struct_0(sK0_skl,X1))
| ~ m1_subset_1(X1,u1_struct_0(sK1_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK0_skl))
| ~ v3_borsuk_1(X0,sK0_skl,sK1_skl)
| ~ m2_relset_1(X0,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v5_pre_topc(X0,sK0_skl,sK1_skl)
| ~ v1_funct_2(X0,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f598,plain,
! [X0,X1] :
( ~ sQ24_spl
| k5_pre_topc(sK0_skl,sK1_skl,X0,k6_pre_topc(sK1_skl,k1_struct_0(sK1_skl,X1))) = k6_pre_topc(sK0_skl,k1_struct_0(sK0_skl,X1))
| ~ m1_subset_1(X1,u1_struct_0(sK1_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK0_skl))
| ~ v3_borsuk_1(X0,sK0_skl,sK1_skl)
| ~ m2_relset_1(X0,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v5_pre_topc(X0,sK0_skl,sK1_skl)
| ~ v1_funct_2(X0,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(X0) ),
inference(component_clause,[status(thm)],[f597]) ).
fof(f600,plain,
( ~ sQ23_spl
| sQ24_spl
| ~ sQ17_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f595,f565,f568,f597,f591]) ).
fof(f605,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f570,f119]) ).
fof(f606,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f605]) ).
fof(f607,plain,
( sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f567,f118]) ).
fof(f608,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f607]) ).
fof(f615,definition,
( sQ27_spl
<=> v3_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f616,plain,
( ~ sQ27_spl
| v3_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f615]) ).
fof(f627,plain,
( ~ sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f616,f114]) ).
fof(f628,plain,
~ sQ27_spl,
inference(contradiction_clause,[status(thm)],[f627]) ).
fof(f629,plain,
( ~ sQ24_spl
| ~ m1_subset_1(sK2_skl,u1_struct_0(sK1_skl))
| ~ m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))
| ~ v3_borsuk_1(k1_tsp_2(sK0_skl,sK1_skl),sK0_skl,sK1_skl)
| ~ m2_relset_1(k1_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v5_pre_topc(k1_tsp_2(sK0_skl,sK1_skl),sK0_skl,sK1_skl)
| ~ v1_funct_2(k1_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(k1_tsp_2(sK0_skl,sK1_skl)) ),
inference(resolution,[status(thm)],[f598,f487]) ).
fof(f630,definition,
( sQ30_spl
<=> v1_funct_1(k1_tsp_2(sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f632,plain,
( sQ30_spl
| ~ v1_funct_1(k1_tsp_2(sK0_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f630]) ).
fof(f633,definition,
( sQ31_spl
<=> v1_funct_2(k1_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f635,plain,
( sQ31_spl
| ~ v1_funct_2(k1_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f633]) ).
fof(f636,definition,
( sQ32_spl
<=> v5_pre_topc(k1_tsp_2(sK0_skl,sK1_skl),sK0_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f638,plain,
( sQ32_spl
| ~ v5_pre_topc(k1_tsp_2(sK0_skl,sK1_skl),sK0_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f636]) ).
fof(f639,definition,
( sQ33_spl
<=> m2_relset_1(k1_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f641,plain,
( sQ33_spl
| ~ m2_relset_1(k1_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f639]) ).
fof(f642,definition,
( sQ34_spl
<=> v3_borsuk_1(k1_tsp_2(sK0_skl,sK1_skl),sK0_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f644,plain,
( sQ34_spl
| ~ v3_borsuk_1(k1_tsp_2(sK0_skl,sK1_skl),sK0_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f642]) ).
fof(f645,definition,
( sQ35_spl
<=> m1_subset_1(sK2_skl,u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f647,plain,
( sQ35_spl
| ~ m1_subset_1(sK2_skl,u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f645]) ).
fof(f648,definition,
( sQ36_spl
<=> m1_subset_1(sK2_skl,u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f650,plain,
( sQ36_spl
| ~ m1_subset_1(sK2_skl,u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f648]) ).
fof(f651,plain,
( ~ sQ24_spl
| ~ sQ36_spl
| ~ sQ35_spl
| ~ sQ34_spl
| ~ sQ33_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f629,f630,f633,f636,f639,f642,f645,f648,f597]) ).
fof(f652,plain,
( sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f650,f486]) ).
fof(f653,plain,
sQ36_spl,
inference(contradiction_clause,[status(thm)],[f652]) ).
fof(f654,plain,
( sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f647,f120]) ).
fof(f655,plain,
sQ35_spl,
inference(contradiction_clause,[status(thm)],[f654]) ).
fof(f690,plain,
( sQ34_spl
| ~ m2_relset_1(k1_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v5_pre_topc(k1_tsp_2(sK0_skl,sK1_skl),sK0_skl,sK1_skl)
| ~ v1_funct_2(k1_tsp_2(sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(k1_tsp_2(sK0_skl,sK1_skl))
| ~ m2_tsp_1(sK1_skl,sK0_skl)
| ~ v2_tsp_2(sK1_skl,sK0_skl)
| v3_struct_0(sK1_skl)
| ~ l1_pre_topc(sK0_skl)
| ~ v2_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f644,f489]) ).
fof(f691,definition,
( sQ41_spl
<=> v3_struct_0(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f692,plain,
( ~ sQ41_spl
| v3_struct_0(sK1_skl) ),
inference(component_clause,[status(thm)],[f691]) ).
fof(f694,plain,
( sQ34_spl
| ~ sQ33_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ17_spl
| ~ sQ16_spl
| sQ41_spl
| ~ sQ6_spl
| ~ sQ11_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f690,f615,f537,f516,f691,f565,f568,f630,f633,f636,f639,f642]) ).
fof(f695,plain,
( sQ33_spl
| ~ m1_pre_topc(sK1_skl,sK0_skl)
| ~ v2_tsp_2(sK1_skl,sK0_skl)
| v3_struct_0(sK1_skl)
| ~ l1_pre_topc(sK0_skl)
| ~ v2_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f641,f314]) ).
fof(f696,definition,
( sQ42_spl
<=> m1_pre_topc(sK1_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f698,plain,
( sQ42_spl
| ~ m1_pre_topc(sK1_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f696]) ).
fof(f699,plain,
( sQ33_spl
| ~ sQ42_spl
| ~ sQ16_spl
| sQ41_spl
| ~ sQ6_spl
| ~ sQ11_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f695,f615,f537,f516,f691,f565,f696,f639]) ).
fof(f700,plain,
( ~ sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f692,f117]) ).
fof(f701,plain,
~ sQ41_spl,
inference(contradiction_clause,[status(thm)],[f700]) ).
fof(f702,plain,
( sQ32_spl
| ~ m1_pre_topc(sK1_skl,sK0_skl)
| ~ v2_tsp_2(sK1_skl,sK0_skl)
| v3_struct_0(sK1_skl)
| ~ l1_pre_topc(sK0_skl)
| ~ v2_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f638,f313]) ).
fof(f703,plain,
( sQ32_spl
| ~ sQ42_spl
| ~ sQ16_spl
| sQ41_spl
| ~ sQ6_spl
| ~ sQ11_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f702,f615,f537,f516,f691,f565,f696,f636]) ).
fof(f704,plain,
( sQ31_spl
| ~ m1_pre_topc(sK1_skl,sK0_skl)
| ~ v2_tsp_2(sK1_skl,sK0_skl)
| v3_struct_0(sK1_skl)
| ~ l1_pre_topc(sK0_skl)
| ~ v2_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f635,f312]) ).
fof(f705,plain,
( sQ31_spl
| ~ sQ42_spl
| ~ sQ16_spl
| sQ41_spl
| ~ sQ6_spl
| ~ sQ11_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f704,f615,f537,f516,f691,f565,f696,f633]) ).
fof(f706,plain,
( sQ30_spl
| ~ m1_pre_topc(sK1_skl,sK0_skl)
| ~ v2_tsp_2(sK1_skl,sK0_skl)
| v3_struct_0(sK1_skl)
| ~ l1_pre_topc(sK0_skl)
| ~ v2_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f632,f311]) ).
fof(f707,plain,
( sQ30_spl
| ~ sQ42_spl
| ~ sQ16_spl
| sQ41_spl
| ~ sQ6_spl
| ~ sQ11_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f706,f615,f537,f516,f691,f565,f696,f630]) ).
fof(f790,plain,
( sQ42_spl
| ~ m2_tsp_1(sK1_skl,sK0_skl)
| ~ l1_pre_topc(sK0_skl) ),
inference(resolution,[status(thm)],[f460,f698]) ).
fof(f793,plain,
( sQ42_spl
| ~ sQ17_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f790,f516,f568,f696]) ).
fof(f796,plain,
$false,
inference(sat_refutation,[status(thm)],[f524,f562,f594,f600,f606,f608,f628,f651,f653,f655,f694,f699,f701,f703,f705,f707,f793]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : TOP035+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n006.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Mon Sep 21 12:42:27 UTC 2026
% 0.17/0.42 % CPUTime :
% 0.17/0.45 % Drodi V4.1.1
% 0.17/0.48 % Refutation found
% 0.17/0.48 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/0.48 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.23/0.52 % Elapsed time: 0.092711 seconds
% 0.23/0.52 % CPU time: 0.235756 seconds
% 0.23/0.52 % Total memory used: 44.033 MB
% 0.23/0.52 % Net memory used: 43.925 MB
%------------------------------------------------------------------------------