%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : TOP042+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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:03 AM UTC 2026
% Result : Theorem 205.56s 28.25s
% Output : CNFRefutation 205.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 15
% Syntax : Number of formulae : 142 ( 35 unt; 0 def)
% Number of atoms : 666 ( 96 equ)
% Maximal formula atoms : 18 ( 4 avg)
% Number of connectives : 914 ( 390 ~; 434 |; 54 &)
% ( 5 <=>; 31 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 3 con; 0-4 aty)
% Number of variables : 189 ( 12 sgn 44 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(commutativity_k3_xboole_0,axiom,
! [A,B] : k3_xboole_0(A,B) = k3_xboole_0(B,A),
file('theBenchmark.p',commutativity_k3_xboole_0) ).
fof(commutativity_k5_subset_1,axiom,
! [A,B,C] :
( ( m1_subset_1(C,k1_zfmisc_1(A))
& m1_subset_1(B,k1_zfmisc_1(A)) )
=> k5_subset_1(A,B,C) = k5_subset_1(A,C,B) ),
file('theBenchmark.p',commutativity_k5_subset_1) ).
fof(d12_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 = k4_tsp_2(A,B)
<=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))
=> ( D = u1_struct_0(B)
=> ! [E] :
( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A)))
=> k5_subset_1(u1_struct_0(A),D,k3_tex_4(A,E)) = k4_pre_topc(A,B,C,E) ) ) ) ) ) ) ),
file('theBenchmark.p',d12_tsp_2) ).
fof(d2_tsp_1,axiom,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( l1_pre_topc(B)
=> ( m2_tsp_1(B,A)
<=> ( ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
=> ( v4_pre_topc(C,B)
<=> ? [D] :
( C = k3_xboole_0(D,u1_struct_0(B))
& v4_pre_topc(D,A)
& m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) ) ) )
& r1_tarski(u1_struct_0(B),u1_struct_0(A)) ) ) ) ),
file('theBenchmark.p',d2_tsp_1) ).
fof(dt_k4_pre_topc,axiom,
! [A,B,C,D] :
( ( m1_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C)
& l1_struct_0(B)
& l1_struct_0(A) )
=> m1_subset_1(k4_pre_topc(A,B,C,D),k1_zfmisc_1(u1_struct_0(B))) ),
file('theBenchmark.p',dt_k4_pre_topc) ).
fof(dt_k4_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(k4_tsp_2(A,B),u1_struct_0(A),u1_struct_0(B))
& v5_pre_topc(k4_tsp_2(A,B),A,B)
& v1_funct_2(k4_tsp_2(A,B),u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(k4_tsp_2(A,B)) ) ),
file('theBenchmark.p',dt_k4_tsp_2) ).
fof(dt_l1_pre_topc,axiom,
! [A] :
( l1_pre_topc(A)
=> l1_struct_0(A) ),
file('theBenchmark.p',dt_l1_pre_topc) ).
fof(dt_m2_tsp_1,axiom,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( m2_tsp_1(B,A)
=> l1_pre_topc(B) ) ),
file('theBenchmark.p',dt_m2_tsp_1) ).
fof(redefinition_k4_pre_topc,axiom,
! [A,B,C,D] :
( ( m1_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C)
& l1_struct_0(B)
& l1_struct_0(A) )
=> k4_pre_topc(A,B,C,D) = k9_relat_1(C,D) ),
file('theBenchmark.p',redefinition_k4_pre_topc) ).
fof(redefinition_k5_subset_1,axiom,
! [A,B,C] :
( ( m1_subset_1(C,k1_zfmisc_1(A))
& m1_subset_1(B,k1_zfmisc_1(A)) )
=> k5_subset_1(A,B,C) = k3_xboole_0(B,C) ),
file('theBenchmark.p',redefinition_k5_subset_1) ).
fof(redefinition_m2_relset_1,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('theBenchmark.p',redefinition_m2_relset_1) ).
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(t1_tsep_1,axiom,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( m1_pre_topc(B,A)
=> m1_subset_1(u1_struct_0(B),k1_zfmisc_1(u1_struct_0(A))) ) ),
file('theBenchmark.p',t1_tsep_1) ).
fof(t62_tex_4,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( v4_pre_topc(B,A)
=> k3_tex_4(A,B) = B ) ) ),
file('theBenchmark.p',t62_tex_4) ).
fof(t35_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,k1_zfmisc_1(u1_struct_0(A)))
=> ( v4_pre_topc(C,A)
=> v4_pre_topc(k4_pre_topc(A,B,k4_tsp_2(A,B),C),B) ) ) ) ),
file('theBenchmark.p',t35_tsp_2) ).
fof(t35_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,k1_zfmisc_1(u1_struct_0(A)))
=> ( v4_pre_topc(C,A)
=> v4_pre_topc(k4_pre_topc(A,B,k4_tsp_2(A,B),C),B) ) ) ) ),
inference(assume_negation,[status(cth)],[t35_tsp_2]) ).
fof(nnf_122,plain,
? [A] :
( ? [B] :
( ? [C] :
( ~ v4_pre_topc(k4_pre_topc(A,B,k4_tsp_2(A,B),C),B)
& v4_pre_topc(C,A)
& m1_subset_1(C,k1_zfmisc_1(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)],[t35_tsp_2_neg]) ).
fof(sk_t35_tsp_2_neg,plain,
( ~ v4_pre_topc(k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),sK2),sK0)
& v4_pre_topc(sK2,sK1)
& m1_subset_1(sK2,k1_zfmisc_1(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]),skolemize(A,sK1),skolemize(B,sK0),skolemize(C,sK2)],[nnf_122]) ).
cnf(c_123,negated_conjecture,
v2_tsp_2(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_t35_tsp_2_neg]) ).
cnf(c_125,plain,
( m2_relset_1(k4_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_k4_tsp_2]) ).
cnf(c_126,plain,
( v5_pre_topc(k4_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_k4_tsp_2]) ).
cnf(c_127,plain,
( v1_funct_2(k4_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_k4_tsp_2]) ).
cnf(c_128,plain,
( v1_funct_1(k4_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_k4_tsp_2]) ).
cnf(c_137,plain,
( k5_subset_1(u1_struct_0(A),D,k3_tex_4(A,E)) = k4_pre_topc(A,B,C,E)
| ~ m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A)))
| u1_struct_0(B) != D
| ~ m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))
| k4_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)],[d12_tsp_2]) ).
cnf(c_189,negated_conjecture,
( v1_funct_1(k4_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_123,c_128]) ).
cnf(c_190,plain,
( k9_relat_1(C,D) = k4_pre_topc(A,B,C,D)
| ~ m1_relset_1(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(C)
| ~ l1_struct_0(B)
| ~ l1_struct_0(A) ),
inference(clausify,[status(thm)],[redefinition_k4_pre_topc]) ).
cnf(c_191,plain,
( m1_subset_1(k4_pre_topc(A,B,C,D),k1_zfmisc_1(u1_struct_0(B)))
| ~ m1_relset_1(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(C)
| ~ l1_struct_0(B)
| ~ l1_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k4_pre_topc]) ).
cnf(c_197,negated_conjecture,
( k5_subset_1(u1_struct_0(sK1),B,k3_tex_4(sK1,C)) = k4_pre_topc(sK1,sK0,A,C)
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != B
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| k4_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_123,c_137]) ).
cnf(c_198,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1)
| k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| k4_tsp_2(sK1,sK0) != k4_tsp_2(sK1,sK0)
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k4_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_197,c_189]) ).
cnf(c_22913,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1)
| k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k4_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_198]) ).
cnf(c_22914,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k4_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_22913]) ).
cnf(c_22915,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k4_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_22914]) ).
cnf(c_22916,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k4_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_22915]) ).
cnf(c_199,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k4_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_22916]) ).
cnf(c_214,negated_conjecture,
( m1_subset_1(k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C),k1_zfmisc_1(u1_struct_0(B)))
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A)
| ~ 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_189,c_191]) ).
cnf(c_215,negated_conjecture,
( k9_relat_1(k4_tsp_2(sK1,sK0),C) = k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A)
| ~ 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_189,c_190]) ).
cnf(c_216,negated_conjecture,
( k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C) = k9_relat_1(k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A)
| ~ 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_215]) ).
cnf(c_228,negated_conjecture,
( v1_funct_2(k4_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_123,c_127]) ).
cnf(c_229,negated_conjecture,
( v5_pre_topc(k4_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_123,c_126]) ).
cnf(c_230,negated_conjecture,
( m2_relset_1(k4_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_123,c_125]) ).
cnf(c_232,negated_conjecture,
~ v4_pre_topc(k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),sK2),sK0),
inference(split_conjunct,[status(thm)],[sk_t35_tsp_2_neg]) ).
cnf(c_233,negated_conjecture,
v4_pre_topc(sK2,sK1),
inference(split_conjunct,[status(thm)],[sk_t35_tsp_2_neg]) ).
cnf(c_234,negated_conjecture,
m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))),
inference(split_conjunct,[status(thm)],[sk_t35_tsp_2_neg]) ).
cnf(c_235,negated_conjecture,
m2_tsp_1(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_t35_tsp_2_neg]) ).
cnf(c_236,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t35_tsp_2_neg]) ).
cnf(c_237,negated_conjecture,
l1_pre_topc(sK1),
inference(split_conjunct,[status(thm)],[sk_t35_tsp_2_neg]) ).
cnf(c_238,negated_conjecture,
v2_pre_topc(sK1),
inference(split_conjunct,[status(thm)],[sk_t35_tsp_2_neg]) ).
cnf(c_239,negated_conjecture,
~ v3_struct_0(sK1),
inference(split_conjunct,[status(thm)],[sk_t35_tsp_2_neg]) ).
cnf(c_243,plain,
( k3_tex_4(A,B) = B
| ~ v4_pre_topc(B,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t62_tex_4]) ).
cnf(c_250,plain,
( m1_subset_1(u1_struct_0(B),k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_pre_topc(B,A)
| ~ l1_pre_topc(A) ),
inference(clausify,[status(thm)],[t1_tsep_1]) ).
cnf(c_254,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_256,plain,
( m1_relset_1(A,B,C)
| ~ m2_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_m2_relset_1]) ).
cnf(c_257,plain,
( k5_subset_1(B,A,C) = k3_xboole_0(A,C)
| ~ m1_subset_1(C,k1_zfmisc_1(B))
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[redefinition_k5_subset_1]) ).
cnf(c_347,plain,
( l1_pre_topc(B)
| ~ m2_tsp_1(B,A)
| ~ l1_pre_topc(A) ),
inference(clausify,[status(thm)],[dt_m2_tsp_1]) ).
cnf(c_350,plain,
( l1_struct_0(A)
| ~ l1_pre_topc(A) ),
inference(clausify,[status(thm)],[dt_l1_pre_topc]) ).
cnf(c_359,plain,
( k3_xboole_0(D,u1_struct_0(B)) != C
| ~ v4_pre_topc(D,A)
| ~ m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))
| v4_pre_topc(C,B)
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
| ~ m2_tsp_1(B,A)
| ~ l1_pre_topc(B)
| ~ l1_pre_topc(A) ),
inference(clausify,[status(thm)],[d2_tsp_1]) ).
cnf(c_364,plain,
( k5_subset_1(B,C,A) = k5_subset_1(B,A,C)
| ~ m1_subset_1(C,k1_zfmisc_1(B))
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[commutativity_k5_subset_1]) ).
cnf(c_365,plain,
k3_xboole_0(A,B) = k3_xboole_0(B,A),
inference(clausify,[status(thm)],[commutativity_k3_xboole_0]) ).
cnf(c_22917,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k4_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_239,c_199]) ).
cnf(c_22918,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k4_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_238,c_22917]) ).
cnf(c_22919,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k4_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_237,c_22918]) ).
cnf(c_22920,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1) ),
inference(resolve,[status(thm)],[c_236,c_22919]) ).
cnf(c_453,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_235,c_22920]) ).
cnf(c_22921,negated_conjecture,
( m2_relset_1(k4_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_239,c_230]) ).
cnf(c_22922,negated_conjecture,
( m2_relset_1(k4_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_238,c_22921]) ).
cnf(c_22923,negated_conjecture,
( m2_relset_1(k4_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_237,c_22922]) ).
cnf(c_455,negated_conjecture,
( m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m1_pre_topc(sK0,sK1) ),
inference(resolve,[status(thm)],[c_236,c_22923]) ).
cnf(c_22924,negated_conjecture,
( v5_pre_topc(k4_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_239,c_229]) ).
cnf(c_22925,negated_conjecture,
( v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_238,c_22924]) ).
cnf(c_22926,negated_conjecture,
( v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_237,c_22925]) ).
cnf(c_456,negated_conjecture,
( v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0)
| ~ m1_pre_topc(sK0,sK1) ),
inference(resolve,[status(thm)],[c_236,c_22926]) ).
cnf(c_22927,negated_conjecture,
( v1_funct_2(k4_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_239,c_228]) ).
cnf(c_22928,negated_conjecture,
( v1_funct_2(k4_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_238,c_22927]) ).
cnf(c_22929,negated_conjecture,
( v1_funct_2(k4_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_237,c_22928]) ).
cnf(c_457,negated_conjecture,
( v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m1_pre_topc(sK0,sK1) ),
inference(resolve,[status(thm)],[c_236,c_22929]) ).
cnf(c_22930,negated_conjecture,
( k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C) = k9_relat_1(k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_239,c_216]) ).
cnf(c_22931,negated_conjecture,
( k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C) = k9_relat_1(k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_238,c_22930]) ).
cnf(c_22932,negated_conjecture,
( k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C) = k9_relat_1(k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_237,c_22931]) ).
cnf(c_462,negated_conjecture,
( k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C) = k9_relat_1(k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A)
| ~ m1_pre_topc(sK0,sK1) ),
inference(resolve,[status(thm)],[c_236,c_22932]) ).
cnf(c_22933,negated_conjecture,
( m1_subset_1(k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C),k1_zfmisc_1(u1_struct_0(B)))
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_239,c_214]) ).
cnf(c_22934,negated_conjecture,
( m1_subset_1(k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C),k1_zfmisc_1(u1_struct_0(B)))
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_238,c_22933]) ).
cnf(c_22935,negated_conjecture,
( m1_subset_1(k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C),k1_zfmisc_1(u1_struct_0(B)))
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_237,c_22934]) ).
cnf(c_463,negated_conjecture,
( m1_subset_1(k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C),k1_zfmisc_1(u1_struct_0(B)))
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A)
| ~ m1_pre_topc(sK0,sK1) ),
inference(resolve,[status(thm)],[c_236,c_22935]) ).
cnf(c_22936,negated_conjecture,
( k3_tex_4(sK1,sK2) = sK2
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_243,c_233]) ).
cnf(c_22937,negated_conjecture,
( k3_tex_4(sK1,sK2) = sK2
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_239,c_22936]) ).
cnf(c_22938,negated_conjecture,
( k3_tex_4(sK1,sK2) = sK2
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_238,c_22937]) ).
cnf(c_22939,negated_conjecture,
( k3_tex_4(sK1,sK2) = sK2
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(resolve,[status(thm)],[c_237,c_22938]) ).
cnf(c_485,negated_conjecture,
k3_tex_4(sK1,sK2) = sK2,
inference(resolve,[status(thm)],[c_234,c_22939]) ).
cnf(c_22940,negated_conjecture,
( m1_pre_topc(sK0,sK1)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_254,c_235]) ).
cnf(c_489,negated_conjecture,
m1_pre_topc(sK0,sK1),
inference(resolve,[status(thm)],[c_237,c_22940]) ).
cnf(c_495,negated_conjecture,
( m1_subset_1(k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C),k1_zfmisc_1(u1_struct_0(B)))
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A) ),
inference(resolve,[status(thm)],[c_489,c_463]) ).
cnf(c_496,negated_conjecture,
( k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C) = k9_relat_1(k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A) ),
inference(resolve,[status(thm)],[c_489,c_462]) ).
cnf(c_501,negated_conjecture,
v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_489,c_457]) ).
cnf(c_502,negated_conjecture,
v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0),
inference(resolve,[status(thm)],[c_489,c_456]) ).
cnf(c_503,negated_conjecture,
m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_489,c_455]) ).
cnf(c_22941,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0) ),
inference(resolve,[status(thm)],[c_501,c_453]) ).
cnf(c_22942,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_502,c_22941]) ).
cnf(c_22943,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(resolve,[status(thm)],[c_503,c_22942]) ).
cnf(c_505,negated_conjecture,
( k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(resolve,[status(thm)],[c_489,c_22943]) ).
cnf(c_510,plain,
( k5_subset_1(u1_struct_0(sK1),A,sK2) = k3_xboole_0(A,sK2)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(resolve,[status(thm)],[c_257,c_234]) ).
cnf(c_22944,negated_conjecture,
( l1_pre_topc(sK0)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_347,c_235]) ).
cnf(c_580,negated_conjecture,
l1_pre_topc(sK0),
inference(resolve,[status(thm)],[c_237,c_22944]) ).
cnf(c_583,plain,
l1_struct_0(sK1),
inference(resolve,[status(thm)],[c_350,c_237]) ).
cnf(c_22945,negated_conjecture,
( k3_xboole_0(B,u1_struct_0(sK0)) != A
| ~ v4_pre_topc(B,sK1)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| v4_pre_topc(A,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_pre_topc(sK0)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_359,c_235]) ).
cnf(c_22946,negated_conjecture,
( k3_xboole_0(B,u1_struct_0(sK0)) != A
| ~ v4_pre_topc(B,sK1)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| v4_pre_topc(A,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_pre_topc(sK0) ),
inference(resolve,[status(thm)],[c_237,c_22945]) ).
cnf(c_592,negated_conjecture,
( k3_xboole_0(B,u1_struct_0(sK0)) != A
| ~ v4_pre_topc(B,sK1)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| v4_pre_topc(A,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_580,c_22946]) ).
cnf(c_22947,negated_conjecture,
( k5_subset_1(u1_struct_0(sK1),A,sK2) = k5_subset_1(u1_struct_0(sK1),sK2,A)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(resolve,[status(thm)],[c_364,c_234]) ).
cnf(c_598,negated_conjecture,
( k5_subset_1(u1_struct_0(sK1),sK2,A) = k5_subset_1(u1_struct_0(sK1),A,sK2)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(copy,[status(thm)],[c_22947]) ).
cnf(c_684,plain,
l1_struct_0(sK0),
inference(resolve,[status(thm)],[c_580,c_350]) ).
cnf(c_22948,plain,
( m1_subset_1(u1_struct_0(sK0),k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_489,c_250]) ).
cnf(c_724,negated_conjecture,
m1_subset_1(u1_struct_0(sK0),k1_zfmisc_1(u1_struct_0(sK1))),
inference(resolve,[status(thm)],[c_237,c_22948]) ).
cnf(c_751,plain,
m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_503,c_256]) ).
cnf(c_22949,negated_conjecture,
( k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,sK2)) = k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),sK2)
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(resolve,[status(thm)],[c_505,c_234]) ).
cnf(c_761,negated_conjecture,
( k5_subset_1(u1_struct_0(sK1),A,sK2) = k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),sK2)
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(paramod,[status(thm)],[c_485,c_22949]) ).
cnf(c_22950,negated_conjecture,
( k3_xboole_0(sK2,u1_struct_0(sK0)) != A
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v4_pre_topc(A,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_592,c_233]) ).
cnf(c_1442,negated_conjecture,
( k3_xboole_0(sK2,u1_struct_0(sK0)) != A
| v4_pre_topc(A,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_234,c_22950]) ).
cnf(c_22951,negated_conjecture,
( k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),A) = k9_relat_1(k4_tsp_2(sK1,sK0),A)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ l1_struct_0(sK0)
| ~ l1_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_751,c_496]) ).
cnf(c_22952,negated_conjecture,
( k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),A) = k9_relat_1(k4_tsp_2(sK1,sK0),A)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ l1_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_583,c_22951]) ).
cnf(c_22953,negated_conjecture,
( k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),A) = k9_relat_1(k4_tsp_2(sK1,sK0),A)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_684,c_22952]) ).
cnf(c_1551,negated_conjecture,
k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),A) = k9_relat_1(k4_tsp_2(sK1,sK0),A),
inference(resolve,[status(thm)],[c_501,c_22953]) ).
cnf(c_22954,negated_conjecture,
( m1_subset_1(k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),A),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ l1_struct_0(sK0)
| ~ l1_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_751,c_495]) ).
cnf(c_22955,negated_conjecture,
( m1_subset_1(k9_relat_1(k4_tsp_2(sK1,sK0),A),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ l1_struct_0(sK0)
| ~ l1_struct_0(sK1) ),
inference(paramod,[status(thm)],[c_1551,c_22954]) ).
cnf(c_22956,negated_conjecture,
( m1_subset_1(k9_relat_1(k4_tsp_2(sK1,sK0),A),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ l1_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_583,c_22955]) ).
cnf(c_22957,negated_conjecture,
( m1_subset_1(k9_relat_1(k4_tsp_2(sK1,sK0),A),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_684,c_22956]) ).
cnf(c_1552,negated_conjecture,
m1_subset_1(k9_relat_1(k4_tsp_2(sK1,sK0),A),k1_zfmisc_1(u1_struct_0(sK0))),
inference(resolve,[status(thm)],[c_501,c_22957]) ).
cnf(c_22958,negated_conjecture,
( k5_subset_1(u1_struct_0(sK1),A,sK2) = k9_relat_1(k4_tsp_2(sK1,sK0),sK2)
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(paramod,[status(thm)],[c_1551,c_761]) ).
cnf(c_1575,negated_conjecture,
( k9_relat_1(k4_tsp_2(sK1,sK0),sK2) = k5_subset_1(u1_struct_0(sK1),A,sK2)
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(copy,[status(thm)],[c_22958]) ).
cnf(c_1585,negated_conjecture,
~ v4_pre_topc(k9_relat_1(k4_tsp_2(sK1,sK0),sK2),sK0),
inference(paramod,[status(thm)],[c_1551,c_232]) ).
cnf(c_22959,plain,
k5_subset_1(u1_struct_0(sK1),sK2,u1_struct_0(sK0)) = k5_subset_1(u1_struct_0(sK1),u1_struct_0(sK0),sK2),
inference(resolve,[status(thm)],[c_724,c_598]) ).
cnf(c_2093,plain,
k5_subset_1(u1_struct_0(sK1),u1_struct_0(sK0),sK2) = k5_subset_1(u1_struct_0(sK1),sK2,u1_struct_0(sK0)),
inference(copy,[status(thm)],[c_22959]) ).
cnf(c_22960,plain,
k5_subset_1(u1_struct_0(sK1),u1_struct_0(sK0),sK2) = k3_xboole_0(u1_struct_0(sK0),sK2),
inference(resolve,[status(thm)],[c_724,c_510]) ).
cnf(c_22961,plain,
k5_subset_1(u1_struct_0(sK1),sK2,u1_struct_0(sK0)) = k3_xboole_0(u1_struct_0(sK0),sK2),
inference(paramod,[status(thm)],[c_2093,c_22960]) ).
cnf(c_2101,plain,
k5_subset_1(u1_struct_0(sK1),sK2,u1_struct_0(sK0)) = k3_xboole_0(sK2,u1_struct_0(sK0)),
inference(paramod,[status(thm)],[c_365,c_22961]) ).
cnf(c_2131,plain,
k5_subset_1(u1_struct_0(sK1),u1_struct_0(sK0),sK2) = k3_xboole_0(sK2,u1_struct_0(sK0)),
inference(paramod,[status(thm)],[c_2101,c_2093]) ).
cnf(c_22962,plain,
( k9_relat_1(k4_tsp_2(sK1,sK0),sK2) = k5_subset_1(u1_struct_0(sK1),u1_struct_0(sK0),sK2)
| u1_struct_0(sK0) != u1_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_1575,c_724]) ).
cnf(c_22963,plain,
( k9_relat_1(k4_tsp_2(sK1,sK0),sK2) = k3_xboole_0(sK2,u1_struct_0(sK0))
| u1_struct_0(sK0) != u1_struct_0(sK0) ),
inference(paramod,[status(thm)],[c_2131,c_22962]) ).
cnf(c_13144,plain,
k9_relat_1(k4_tsp_2(sK1,sK0),sK2) = k3_xboole_0(sK2,u1_struct_0(sK0)),
inference(copy,[status(thm)],[c_22963]) ).
cnf(c_13221,negated_conjecture,
~ v4_pre_topc(k3_xboole_0(sK2,u1_struct_0(sK0)),sK0),
inference(paramod,[status(thm)],[c_13144,c_1585]) ).
cnf(c_22894,plain,
m1_subset_1(k3_xboole_0(sK2,u1_struct_0(sK0)),k1_zfmisc_1(u1_struct_0(sK0))),
inference(paramod,[status(thm)],[c_13144,c_1552]) ).
cnf(c_22964,plain,
( k3_xboole_0(sK2,u1_struct_0(sK0)) != k3_xboole_0(sK2,u1_struct_0(sK0))
| v4_pre_topc(k3_xboole_0(sK2,u1_struct_0(sK0)),sK0) ),
inference(resolve,[status(thm)],[c_22894,c_1442]) ).
cnf(c_22965,plain,
v4_pre_topc(k3_xboole_0(sK2,u1_struct_0(sK0)),sK0),
inference(copy,[status(thm)],[c_22964]) ).
cnf(c_22912,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_13221,c_22965]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : TOP042+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n020.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 20:45:04 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 2493645 was started by sandbox2 on n020,
% 0.09/0.37 % Sat Sep 26 20:45:04 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.40
% 0.09/0.40 % From the command line: assign(max_seconds, 300).
% 205.56/28.25
% 205.56/28.25 % given #500 (T,wt=16): 1057 -v3_membered(u1_struct_0(c5)) | v3_membered(f12(c5)). [resolve(539,a,384,b)].
% 205.56/28.25
% 205.56/28.25 % given #1000 (T,wt=22): 1293 m1_subset_1(u1_struct_0(f10(c1)),k1_zfmisc_1(u1_struct_0(c1))). [resolve(1106,a,250,b),unit_del(a,346)].
% 205.56/28.25
% 205.56/28.25 % given #1500 (T,wt=23): 4208 r2_hidden(k3_xboole_0(c7,u1_struct_0(c5)),k1_zfmisc_1(u1_struct_0(c5))). [resolve(1413,a,248,a),unit_del(a,338)].
% 205.56/28.25
% 205.56/28.25 % given #2000 (T,wt=23): 10428 r1_tarski(k3_xboole_0(f12(c5),f20(c5)),u1_struct_0(c5)). [resolve(2441,a,247,a)].
% 205.56/28.25
% 205.56/28.25 % given #2500 (T,wt=24): 10922 -v5_membered(u1_struct_0(c5)) | v4_membered(k3_xboole_0(f15(c5),f19(c5))). [resolve(2570,a,373,b)].
% 205.56/28.25
% 205.56/28.25 % given #3000 (T,wt=24): 15601 -v5_membered(u1_struct_0(c6)) | v3_membered(k3_xboole_0(f14(c6),f20(c6))). [resolve(14883,a,374,b)].
% 205.56/28.25
% 205.56/28.25 % given #3500 (W,wt=16): 19201 -v4_membered(u1_struct_0(c5)) | v2_membered(f19(c6)). [resolve(18819,a,382,b)].
% 205.56/28.25
% 205.56/28.25 % given #4000 (T,wt=24): 20874 -v4_membered(u1_struct_0(c5)) | v4_membered(k3_xboole_0(f14(c6),f20(c5))). [resolve(18880,a,380,b)].
% 205.56/28.25
% 205.56/28.25 % given #4500 (T,wt=25): 11354 v3_tops_1(k1_xboole_0,f6(f6(c5))). [resolve(3561,a,786,a),unit_del(a,3562)].
% 205.56/28.25
% 205.56/28.25 % SZS status Theorem for theBenchmark
% 205.56/28.25
% 205.56/28.25 % Proof 1 at 2.71 (+ 0.88) seconds.
% 205.56/28.25 % Length of proof is 86.
% 205.56/28.25 % Level of proof is 11.
% 205.56/28.25 % Maximum clause weight is 80.000.
% 205.56/28.25 % Given clauses 4508.
% 205.56/28.25
% 205.56/28.25 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------