%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : TOP042+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n014.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 : Tue Sep 29 02:34:04 PM UTC 2026
% Result : Theorem 14.55s 5.78s
% Output : Refutation 32.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 21
% Syntax : Number of formulae : 253 ( 52 unt; 5 def)
% Number of atoms : 1283 ( 154 equ)
% Maximal formula atoms : 20 ( 5 avg)
% Number of connectives : 1767 ( 737 ~; 848 |; 131 &)
% ( 16 <=>; 35 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 6 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 3 con; 0-4 aty)
% Number of variables : 307 ( 0 sgn 288 !; 19 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f57,axiom,
! [X0,X1] : k3_xboole_0(X0,X1) = k3_xboole_0(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k3_xboole_0) ).
fof(f117,axiom,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k3_xboole_0(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t48_xboole_1) ).
fof(f574,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k5_subset_1) ).
fof(f18256,axiom,
! [X0] :
( l1_struct_0(X0)
=> k2_pre_topc(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_pre_topc) ).
fof(f18318,axiom,
! [X0] :
( l1_pre_topc(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f34237,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v4_pre_topc(X1,X0)
=> k3_tex_4(X0,X1) = X1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t62_tex_4) ).
fof(f34364,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m2_tsp_1(X1,X0)
=> l1_pre_topc(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_tsp_1) ).
fof(f34366,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_tsp_1) ).
fof(f34374,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0)
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m1_pre_topc(X1,X0) )
=> ( v1_funct_1(k4_tsp_2(X0,X1))
& v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
& m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_tsp_2) ).
fof(f34375,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0)
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m1_pre_topc(X1,X0) )
=> k4_tsp_2(X0,X1) = k1_tsp_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k4_tsp_2) ).
fof(f34394,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m2_tsp_1(X1,X0)
=> m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l19_tsp_2) ).
fof(f34412,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v4_pre_topc(X2,X0)
<=> ( X2 = k3_tex_4(X0,X2)
& ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
& v4_pre_topc(X3,X1)
& X3 = k3_xboole_0(X2,u1_struct_0(X1)) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t17_tsp_2) ).
fof(f34417,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ? [X2] :
( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v3_borsuk_1(X2,X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t22_tsp_2) ).
fof(f34424,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( X2 = k1_tsp_2(X0,X1)
<=> v3_borsuk_1(X2,X0,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d9_tsp_2) ).
fof(f34432,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( X2 = k4_tsp_2(X0,X1)
<=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
=> ( X3 = u1_struct_0(X1)
=> ! [X4] :
( m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)))
=> k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4)) = k4_pre_topc(X0,X1,X2,X4) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d12_tsp_2) ).
fof(f34439,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v4_pre_topc(X2,X0)
=> v4_pre_topc(k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t35_tsp_2) ).
fof(f34440,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v4_pre_topc(X2,X0)
=> v4_pre_topc(k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),X1) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f34439]) ).
fof(f34535,plain,
! [X0,X1] :
( ( v1_funct_1(k4_tsp_2(X0,X1))
& v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
& m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(ennf_transformation,[],[f34374]) ).
fof(f34536,plain,
! [X0,X1] :
( ( v1_funct_1(k4_tsp_2(X0,X1))
& v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
& m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(flattening,[],[f34535]) ).
fof(f34537,plain,
! [X0,X1] :
( k4_tsp_2(X0,X1) = k1_tsp_2(X0,X1)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(ennf_transformation,[],[f34375]) ).
fof(f34538,plain,
! [X0,X1] :
( k4_tsp_2(X0,X1) = k1_tsp_2(X0,X1)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(flattening,[],[f34537]) ).
fof(f34575,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34394]) ).
fof(f34576,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f34575]) ).
fof(f34611,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v4_pre_topc(X2,X0)
<=> ( X2 = k3_tex_4(X0,X2)
& ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
& v4_pre_topc(X3,X1)
& X3 = k3_xboole_0(X2,u1_struct_0(X1)) ) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34412]) ).
fof(f34612,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v4_pre_topc(X2,X0)
<=> ( X2 = k3_tex_4(X0,X2)
& ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
& v4_pre_topc(X3,X1)
& X3 = k3_xboole_0(X2,u1_struct_0(X1)) ) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f34611]) ).
fof(f34621,plain,
! [X0] :
( ! [X1] :
( ? [X2] :
( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v3_borsuk_1(X2,X0,X1) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34417]) ).
fof(f34622,plain,
! [X0] :
( ! [X1] :
( ? [X2] :
( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v3_borsuk_1(X2,X0,X1) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f34621]) ).
fof(f34635,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k1_tsp_2(X0,X1)
<=> v3_borsuk_1(X2,X0,X1) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34424]) ).
fof(f34636,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k1_tsp_2(X0,X1)
<=> v3_borsuk_1(X2,X0,X1) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f34635]) ).
fof(f34651,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k4_tsp_2(X0,X1)
<=> ! [X3] :
( ! [X4] :
( k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4)) = k4_pre_topc(X0,X1,X2,X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0))) )
| u1_struct_0(X1) != X3
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34432]) ).
fof(f34652,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k4_tsp_2(X0,X1)
<=> ! [X3] :
( ! [X4] :
( k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4)) = k4_pre_topc(X0,X1,X2,X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0))) )
| u1_struct_0(X1) != X3
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f34651]) ).
fof(f34665,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ v4_pre_topc(k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),X1)
& v4_pre_topc(X2,X0)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34440]) ).
fof(f34666,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ v4_pre_topc(k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),X1)
& v4_pre_topc(X2,X0)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(flattening,[],[f34665]) ).
fof(f34771,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f574]) ).
fof(f34772,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f34771]) ).
fof(f34922,plain,
! [X0] :
( ! [X1] :
( k3_tex_4(X0,X1) = X1
| ~ v4_pre_topc(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34237]) ).
fof(f34923,plain,
! [X0] :
( ! [X1] :
( k3_tex_4(X0,X1) = X1
| ~ v4_pre_topc(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f34922]) ).
fof(f35222,plain,
! [X0] :
( ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34366]) ).
fof(f35224,plain,
! [X0] :
( ! [X1] :
( l1_pre_topc(X1)
| ~ m2_tsp_1(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34364]) ).
fof(f35933,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f18318]) ).
fof(f36339,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f18256]) ).
fof(f41458,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v4_pre_topc(X2,X0)
| k3_tex_4(X0,X2) != X2
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v4_pre_topc(X3,X1)
| k3_xboole_0(X2,u1_struct_0(X1)) != X3 ) )
& ( ( X2 = k3_tex_4(X0,X2)
& ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
& v4_pre_topc(X3,X1)
& X3 = k3_xboole_0(X2,u1_struct_0(X1)) ) )
| ~ v4_pre_topc(X2,X0) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f34612]) ).
fof(f41459,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v4_pre_topc(X2,X0)
| k3_tex_4(X0,X2) != X2
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v4_pre_topc(X3,X1)
| k3_xboole_0(X2,u1_struct_0(X1)) != X3 ) )
& ( ( X2 = k3_tex_4(X0,X2)
& ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
& v4_pre_topc(X3,X1)
& X3 = k3_xboole_0(X2,u1_struct_0(X1)) ) )
| ~ v4_pre_topc(X2,X0) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f41458]) ).
fof(f41460,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v4_pre_topc(X2,X0)
| k3_tex_4(X0,X2) != X2
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v4_pre_topc(X3,X1)
| k3_xboole_0(X2,u1_struct_0(X1)) != X3 ) )
& ( ( X2 = k3_tex_4(X0,X2)
& ? [X4] :
( m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X1)))
& v4_pre_topc(X4,X1)
& k3_xboole_0(X2,u1_struct_0(X1)) = X4 ) )
| ~ v4_pre_topc(X2,X0) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(rectify,[],[f41459]) ).
fof(f41461,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v4_pre_topc(X2,X0)
| k3_tex_4(X0,X2) != X2
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v4_pre_topc(X3,X1)
| k3_xboole_0(X2,u1_struct_0(X1)) != X3 ) )
& ( ( X2 = k3_tex_4(X0,X2)
& m1_subset_1(sK48(X1,X2),k1_zfmisc_1(u1_struct_0(X1)))
& v4_pre_topc(sK48(X1,X2),X1)
& k3_xboole_0(X2,u1_struct_0(X1)) = sK48(X1,X2) )
| ~ v4_pre_topc(X2,X0) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK48]),skolemize(X4,sK48(X1,X2))],[f41460]) ).
fof(f41466,plain,
! [X0] :
( ! [X1] :
( ( v1_funct_1(sK53(X0,X1))
& v1_funct_2(sK53(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(sK53(X0,X1),X0,X1)
& m2_relset_1(sK53(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v3_borsuk_1(sK53(X0,X1),X0,X1) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK53]),skolemize(X2,sK53(X0,X1))],[f34622]) ).
fof(f41467,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k1_tsp_2(X0,X1)
| ~ v3_borsuk_1(X2,X0,X1) )
& ( v3_borsuk_1(X2,X0,X1)
| k1_tsp_2(X0,X1) != X2 ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f34636]) ).
fof(f41474,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k4_tsp_2(X0,X1)
| ? [X3] :
( ? [X4] :
( k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4)) != k4_pre_topc(X0,X1,X2,X4)
& m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0))) )
& u1_struct_0(X1) = X3
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ! [X3] :
( ! [X4] :
( k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4)) = k4_pre_topc(X0,X1,X2,X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0))) )
| u1_struct_0(X1) != X3
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
| k4_tsp_2(X0,X1) != X2 ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f34652]) ).
fof(f41475,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k4_tsp_2(X0,X1)
| ? [X3] :
( ? [X4] :
( k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4)) != k4_pre_topc(X0,X1,X2,X4)
& m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0))) )
& u1_struct_0(X1) = X3
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ! [X5] :
( ! [X6] :
( k5_subset_1(u1_struct_0(X0),X5,k3_tex_4(X0,X6)) = k4_pre_topc(X0,X1,X2,X6)
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0))) )
| u1_struct_0(X1) != X5
| ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X0))) )
| k4_tsp_2(X0,X1) != X2 ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(rectify,[],[f41474]) ).
fof(f41476,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k4_tsp_2(X0,X1)
| ( k5_subset_1(u1_struct_0(X0),sK57(X0,X1,X2),k3_tex_4(X0,sK58(X0,X1,X2))) != k4_pre_topc(X0,X1,X2,sK58(X0,X1,X2))
& m1_subset_1(sK58(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)))
& u1_struct_0(X1) = sK57(X0,X1,X2)
& m1_subset_1(sK57(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ! [X5] :
( ! [X6] :
( k5_subset_1(u1_struct_0(X0),X5,k3_tex_4(X0,X6)) = k4_pre_topc(X0,X1,X2,X6)
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0))) )
| u1_struct_0(X1) != X5
| ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X0))) )
| k4_tsp_2(X0,X1) != X2 ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK57,sK58]),skolemize(X3,sK57(X0,X1,X2)),skolemize(X4,sK58(X0,X1,X2))],[f41475]) ).
fof(f41477,plain,
( ~ v4_pre_topc(k4_pre_topc(sK59,sK60,k4_tsp_2(sK59,sK60),sK61),sK60)
& v4_pre_topc(sK61,sK59)
& m1_subset_1(sK61,k1_zfmisc_1(u1_struct_0(sK59)))
& ~ v3_struct_0(sK60)
& v2_tsp_2(sK60,sK59)
& m2_tsp_1(sK60,sK59)
& ~ v3_struct_0(sK59)
& v2_pre_topc(sK59)
& l1_pre_topc(sK59) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK59,sK60,sK61]),skolemize(X0,sK59),skolemize(X1,sK60),skolemize(X2,sK61)],[f34666]) ).
fof(f41667,plain,
! [X0] :
( ! [X1] :
( ( m2_tsp_1(X1,X0)
| ~ m1_pre_topc(X1,X0) )
& ( m1_pre_topc(X1,X0)
| ~ m2_tsp_1(X1,X0) ) )
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f35222]) ).
fof(f43645,plain,
! [X0,X1] :
( m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f34536]) ).
fof(f43646,plain,
! [X0,X1] :
( ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f34536]) ).
fof(f43647,plain,
! [X0,X1] :
( v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f34536]) ).
fof(f43649,plain,
! [X0,X1] :
( ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| k1_tsp_2(X0,X1) = k4_tsp_2(X0,X1)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f34538]) ).
fof(f43701,plain,
! [X0,X1] :
( m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f34576]) ).
fof(f43756,plain,
! [X2,X0,X1] :
( k3_xboole_0(X2,u1_struct_0(X1)) = sK48(X1,X2)
| ~ v4_pre_topc(X2,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f41461]) ).
fof(f43757,plain,
! [X2,X0,X1] :
( ~ v2_pre_topc(X0)
| ~ v4_pre_topc(X2,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| v4_pre_topc(sK48(X1,X2),X1)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f41461]) ).
fof(f43781,plain,
! [X0,X1] :
( v3_borsuk_1(sK53(X0,X1),X0,X1)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f41466]) ).
fof(f43782,plain,
! [X0,X1] :
( m2_relset_1(sK53(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f41466]) ).
fof(f43783,plain,
! [X0,X1] :
( v5_pre_topc(sK53(X0,X1),X0,X1)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f41466]) ).
fof(f43784,plain,
! [X0,X1] :
( v1_funct_2(sK53(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f41466]) ).
fof(f43785,plain,
! [X0,X1] :
( v1_funct_1(sK53(X0,X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f41466]) ).
fof(f43793,plain,
! [X2,X0,X1] :
( ~ v2_pre_topc(X0)
| ~ v3_borsuk_1(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| k1_tsp_2(X0,X1) = X2
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f41467]) ).
fof(f43807,plain,
! [X2,X0,X1,X6,X5] :
( k5_subset_1(u1_struct_0(X0),X5,k3_tex_4(X0,X6)) = k4_pre_topc(X0,X1,X2,X6)
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0)))
| u1_struct_0(X1) != X5
| ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X0)))
| k4_tsp_2(X0,X1) != X2
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f41476]) ).
fof(f43820,plain,
l1_pre_topc(sK59),
inference(cnf_transformation,[],[f41477]) ).
fof(f43821,plain,
v2_pre_topc(sK59),
inference(cnf_transformation,[],[f41477]) ).
fof(f43822,plain,
~ v3_struct_0(sK59),
inference(cnf_transformation,[],[f41477]) ).
fof(f43823,plain,
m2_tsp_1(sK60,sK59),
inference(cnf_transformation,[],[f41477]) ).
fof(f43824,plain,
v2_tsp_2(sK60,sK59),
inference(cnf_transformation,[],[f41477]) ).
fof(f43825,plain,
~ v3_struct_0(sK60),
inference(cnf_transformation,[],[f41477]) ).
fof(f43826,plain,
m1_subset_1(sK61,k1_zfmisc_1(u1_struct_0(sK59))),
inference(cnf_transformation,[],[f41477]) ).
fof(f43827,plain,
v4_pre_topc(sK61,sK59),
inference(cnf_transformation,[],[f41477]) ).
fof(f43828,plain,
~ v4_pre_topc(k4_pre_topc(sK59,sK60,k4_tsp_2(sK59,sK60),sK61),sK60),
inference(cnf_transformation,[],[f41477]) ).
fof(f44050,plain,
! [X2,X0,X1] :
( k3_xboole_0(X1,X2) = k5_subset_1(X0,X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f34772]) ).
fof(f44212,plain,
! [X0,X1] :
( ~ v2_pre_topc(X0)
| ~ v4_pre_topc(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| k3_tex_4(X0,X1) = X1
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f34923]) ).
fof(f44572,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ m2_tsp_1(X1,X0)
| m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f41667]) ).
fof(f44575,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ m2_tsp_1(X1,X0)
| l1_pre_topc(X1) ),
inference(cnf_transformation,[],[f35224]) ).
fof(f45061,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k3_xboole_0(X1,X0),
inference(cnf_transformation,[],[f57]) ).
fof(f45856,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f35933]) ).
fof(f46096,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k4_xboole_0(X0,k4_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f117]) ).
fof(f46449,plain,
! [X0] :
( ~ l1_struct_0(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(cnf_transformation,[],[f36339]) ).
fof(f53762,plain,
! [X2,X0,X1] :
( ~ v2_pre_topc(X0)
| ~ v4_pre_topc(X2,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| sK48(X1,X2) = k4_xboole_0(X2,k4_xboole_0(X2,u1_struct_0(X1)))
| ~ l1_pre_topc(X0) ),
inference(definition_unfolding,[],[f43756,f46096]) ).
fof(f53771,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| k5_subset_1(X0,X1,X2) = k4_xboole_0(X1,k4_xboole_0(X1,X2)) ),
inference(definition_unfolding,[],[f44050,f46096]) ).
fof(f53850,plain,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k4_xboole_0(X1,k4_xboole_0(X1,X0)),
inference(definition_unfolding,[],[f45061,f46096,f46096]) ).
fof(f56526,plain,
! [X2,X0,X1,X6] :
( k4_pre_topc(X0,X1,X2,X6) = k5_subset_1(u1_struct_0(X0),u1_struct_0(X1),k3_tex_4(X0,X6))
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| k4_tsp_2(X0,X1) != X2
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(equality_resolution,[],[f43807]) ).
fof(f56527,plain,
! [X0,X1,X6] :
( ~ v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_1(k4_tsp_2(X0,X1))
| k5_subset_1(u1_struct_0(X0),u1_struct_0(X1),k3_tex_4(X0,X6)) = k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X6)
| ~ v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
| ~ m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(equality_resolution,[],[f56526]) ).
fof(f58358,plain,
! [X0] :
( ~ m2_tsp_1(X0,sK59)
| l1_pre_topc(X0) ),
inference(resolution,[],[f44575,f43820]) ).
fof(f58359,plain,
! [X0] :
( ~ m2_tsp_1(X0,sK59)
| m1_pre_topc(X0,sK59) ),
inference(resolution,[],[f44572,f43820]) ).
fof(f58360,plain,
m1_pre_topc(sK60,sK59),
inference(resolution,[],[f58359,f43823]) ).
fof(f58368,plain,
l1_pre_topc(sK60),
inference(resolution,[],[f58358,f43823]) ).
fof(f58373,plain,
! [X0] :
( v3_struct_0(sK59)
| k1_tsp_2(sK59,X0) = k4_tsp_2(sK59,X0)
| ~ l1_pre_topc(sK59)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK59)
| ~ m1_pre_topc(X0,sK59) ),
inference(resolution,[],[f43649,f43821]) ).
fof(f58374,plain,
! [X0] :
( k1_tsp_2(sK59,X0) = k4_tsp_2(sK59,X0)
| ~ l1_pre_topc(sK59)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK59)
| ~ m1_pre_topc(X0,sK59) ),
inference(forward_subsumption_resolution,[],[f58373,f43822]) ).
fof(f58375,plain,
! [X0] :
( ~ v2_tsp_2(X0,sK59)
| v3_struct_0(X0)
| k1_tsp_2(sK59,X0) = k4_tsp_2(sK59,X0)
| ~ m1_pre_topc(X0,sK59) ),
inference(forward_subsumption_resolution,[],[f58374,f43820]) ).
fof(f58376,plain,
( v3_struct_0(sK60)
| k4_tsp_2(sK59,sK60) = k1_tsp_2(sK59,sK60)
| ~ m1_pre_topc(sK60,sK59) ),
inference(resolution,[],[f58375,f43824]) ).
fof(f58377,plain,
( k4_tsp_2(sK59,sK60) = k1_tsp_2(sK59,sK60)
| ~ m1_pre_topc(sK60,sK59) ),
inference(forward_subsumption_resolution,[],[f58376,f43825]) ).
fof(f58378,plain,
k4_tsp_2(sK59,sK60) = k1_tsp_2(sK59,sK60),
inference(forward_subsumption_resolution,[],[f58377,f58360]) ).
fof(f58379,plain,
~ v4_pre_topc(k4_pre_topc(sK59,sK60,k1_tsp_2(sK59,sK60),sK61),sK60),
inference(superposition,[],[f43828,f58378]) ).
fof(f58384,plain,
! [X0,X1] :
( ~ v4_pre_topc(X0,sK59)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK59)))
| ~ v2_tsp_2(X1,sK59)
| ~ m2_tsp_1(X1,sK59)
| v3_struct_0(sK59)
| v4_pre_topc(sK48(X1,X0),X1)
| ~ l1_pre_topc(sK59) ),
inference(resolution,[],[f43757,f43821]) ).
fof(f58385,plain,
! [X0] :
( ~ v4_pre_topc(X0,sK59)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK59)))
| v3_struct_0(sK59)
| k3_tex_4(sK59,X0) = X0
| ~ l1_pre_topc(sK59) ),
inference(resolution,[],[f44212,f43821]) ).
fof(f58387,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(resolution,[],[f46449,f45856]) ).
fof(f58388,plain,
u1_struct_0(sK59) = k2_pre_topc(sK59),
inference(resolution,[],[f58387,f43820]) ).
fof(f58389,plain,
u1_struct_0(sK60) = k2_pre_topc(sK60),
inference(resolution,[],[f58387,f58368]) ).
fof(f58390,plain,
m1_subset_1(sK61,k1_zfmisc_1(k2_pre_topc(sK59))),
inference(superposition,[],[f43826,f58388]) ).
fof(f58391,plain,
! [X0] :
( m2_relset_1(k4_tsp_2(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| v3_struct_0(sK59)
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK59)
| ~ m1_pre_topc(X0,sK59) ),
inference(superposition,[],[f43645,f58388]) ).
fof(f58393,plain,
! [X0] :
( v1_funct_2(k4_tsp_2(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| v3_struct_0(sK59)
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK59)
| ~ m1_pre_topc(X0,sK59) ),
inference(superposition,[],[f43647,f58388]) ).
fof(f58395,plain,
! [X0] :
( m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ m2_tsp_1(X0,sK59)
| v3_struct_0(sK59)
| ~ l1_pre_topc(sK59) ),
inference(superposition,[],[f43701,f58388]) ).
fof(f58397,plain,
! [X0] :
( m2_relset_1(sK53(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK59)
| ~ m2_tsp_1(X0,sK59)
| v3_struct_0(sK59)
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59) ),
inference(superposition,[],[f43782,f58388]) ).
fof(f58399,plain,
! [X0] :
( v1_funct_2(sK53(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK59)
| ~ m2_tsp_1(X0,sK59)
| v3_struct_0(sK59)
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59) ),
inference(superposition,[],[f43784,f58388]) ).
fof(f58404,plain,
! [X0,X1] :
( ~ v1_funct_2(k4_tsp_2(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ v1_funct_1(k4_tsp_2(sK59,X0))
| k4_pre_topc(sK59,X0,k4_tsp_2(sK59,X0),X1) = k5_subset_1(k2_pre_topc(sK59),u1_struct_0(X0),k3_tex_4(sK59,X1))
| ~ v5_pre_topc(k4_tsp_2(sK59,X0),sK59,X0)
| ~ m2_relset_1(k4_tsp_2(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK59)
| ~ m2_tsp_1(X0,sK59)
| v3_struct_0(sK59)
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59) ),
inference(superposition,[],[f56527,f58388]) ).
fof(f58427,plain,
! [X0,X1] :
( ~ v1_funct_2(k4_tsp_2(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ v1_funct_1(k4_tsp_2(sK59,X0))
| k4_pre_topc(sK59,X0,k4_tsp_2(sK59,X0),X1) = k5_subset_1(k2_pre_topc(sK59),u1_struct_0(X0),k3_tex_4(sK59,X1))
| ~ v5_pre_topc(k4_tsp_2(sK59,X0),sK59,X0)
| ~ m2_relset_1(k4_tsp_2(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK59)
| ~ m2_tsp_1(X0,sK59)
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59) ),
inference(forward_subsumption_resolution,[],[f58404,f43822]) ).
fof(f58435,plain,
! [X0] :
( v1_funct_2(sK53(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK59)
| ~ m2_tsp_1(X0,sK59)
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59) ),
inference(forward_subsumption_resolution,[],[f58399,f43822]) ).
fof(f58437,plain,
! [X0] :
( m2_relset_1(sK53(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK59)
| ~ m2_tsp_1(X0,sK59)
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59) ),
inference(forward_subsumption_resolution,[],[f58397,f43822]) ).
fof(f58439,plain,
! [X0] :
( m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ m2_tsp_1(X0,sK59)
| ~ l1_pre_topc(sK59) ),
inference(forward_subsumption_resolution,[],[f58395,f43822]) ).
fof(f58441,plain,
! [X0] :
( v1_funct_2(k4_tsp_2(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK59)
| ~ m1_pre_topc(X0,sK59) ),
inference(forward_subsumption_resolution,[],[f58393,f43822]) ).
fof(f58443,plain,
! [X0] :
( m2_relset_1(k4_tsp_2(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK59)
| ~ m1_pre_topc(X0,sK59) ),
inference(forward_subsumption_resolution,[],[f58391,f43822]) ).
fof(f58444,plain,
! [X0,X1] :
( ~ v1_funct_2(k4_tsp_2(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ v1_funct_1(k4_tsp_2(sK59,X0))
| k4_pre_topc(sK59,X0,k4_tsp_2(sK59,X0),X1) = k5_subset_1(k2_pre_topc(sK59),u1_struct_0(X0),k3_tex_4(sK59,X1))
| ~ v5_pre_topc(k4_tsp_2(sK59,X0),sK59,X0)
| ~ m2_relset_1(k4_tsp_2(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK59)
| ~ m2_tsp_1(X0,sK59)
| ~ l1_pre_topc(sK59) ),
inference(forward_subsumption_resolution,[],[f58427,f43821]) ).
fof(f58446,plain,
! [X0] :
( v1_funct_2(sK53(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK59)
| ~ m2_tsp_1(X0,sK59)
| ~ l1_pre_topc(sK59) ),
inference(forward_subsumption_resolution,[],[f58435,f43821]) ).
fof(f58447,plain,
! [X0] :
( m2_relset_1(sK53(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK59)
| ~ m2_tsp_1(X0,sK59)
| ~ l1_pre_topc(sK59) ),
inference(forward_subsumption_resolution,[],[f58437,f43821]) ).
fof(f58448,plain,
! [X0] :
( ~ m2_tsp_1(X0,sK59)
| m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK59))) ),
inference(forward_subsumption_resolution,[],[f58439,f43820]) ).
fof(f58449,plain,
! [X0] :
( v1_funct_2(k4_tsp_2(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| ~ l1_pre_topc(sK59)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK59)
| ~ m1_pre_topc(X0,sK59) ),
inference(forward_subsumption_resolution,[],[f58441,f43821]) ).
fof(f58450,plain,
! [X0] :
( m2_relset_1(k4_tsp_2(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| ~ l1_pre_topc(sK59)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK59)
| ~ m1_pre_topc(X0,sK59) ),
inference(forward_subsumption_resolution,[],[f58443,f43821]) ).
fof(f58451,plain,
! [X0,X1] :
( ~ v1_funct_2(k4_tsp_2(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ v1_funct_1(k4_tsp_2(sK59,X0))
| k4_pre_topc(sK59,X0,k4_tsp_2(sK59,X0),X1) = k5_subset_1(k2_pre_topc(sK59),u1_struct_0(X0),k3_tex_4(sK59,X1))
| ~ v5_pre_topc(k4_tsp_2(sK59,X0),sK59,X0)
| ~ m2_relset_1(k4_tsp_2(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK59)
| ~ m2_tsp_1(X0,sK59) ),
inference(forward_subsumption_resolution,[],[f58444,f43820]) ).
fof(f58452,plain,
! [X0] :
( ~ v2_tsp_2(X0,sK59)
| v3_struct_0(X0)
| v1_funct_2(sK53(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| ~ m2_tsp_1(X0,sK59) ),
inference(forward_subsumption_resolution,[],[f58446,f43820]) ).
fof(f58453,plain,
! [X0] :
( ~ v2_tsp_2(X0,sK59)
| v3_struct_0(X0)
| m2_relset_1(sK53(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| ~ m2_tsp_1(X0,sK59) ),
inference(forward_subsumption_resolution,[],[f58447,f43820]) ).
fof(f58454,plain,
! [X0] :
( ~ v2_tsp_2(X0,sK59)
| v3_struct_0(X0)
| v1_funct_2(k4_tsp_2(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| ~ m1_pre_topc(X0,sK59) ),
inference(forward_subsumption_resolution,[],[f58449,f43820]) ).
fof(f58455,plain,
! [X0] :
( ~ v2_tsp_2(X0,sK59)
| v3_struct_0(X0)
| m2_relset_1(k4_tsp_2(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| ~ m1_pre_topc(X0,sK59) ),
inference(forward_subsumption_resolution,[],[f58450,f43820]) ).
fof(f58456,plain,
! [X0,X1] :
( ~ v2_tsp_2(X0,sK59)
| ~ m1_subset_1(X1,k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ v1_funct_1(k4_tsp_2(sK59,X0))
| k4_pre_topc(sK59,X0,k4_tsp_2(sK59,X0),X1) = k5_subset_1(k2_pre_topc(sK59),u1_struct_0(X0),k3_tex_4(sK59,X1))
| ~ v5_pre_topc(k4_tsp_2(sK59,X0),sK59,X0)
| ~ m2_relset_1(k4_tsp_2(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_funct_2(k4_tsp_2(sK59,X0),k2_pre_topc(sK59),u1_struct_0(X0))
| ~ m2_tsp_1(X0,sK59) ),
inference(forward_subsumption_resolution,[],[f58451,f58448]) ).
fof(f58542,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ v1_funct_1(k4_tsp_2(sK59,sK60))
| k4_pre_topc(sK59,sK60,k4_tsp_2(sK59,sK60),X0) = k5_subset_1(k2_pre_topc(sK59),u1_struct_0(sK60),k3_tex_4(sK59,X0))
| ~ v5_pre_topc(k4_tsp_2(sK59,sK60),sK59,sK60)
| ~ m2_relset_1(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60))
| v3_struct_0(sK60)
| ~ v1_funct_2(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60))
| ~ m2_tsp_1(sK60,sK59) ),
inference(resolution,[],[f58456,f43824]) ).
fof(f58543,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ v1_funct_1(k4_tsp_2(sK59,sK60))
| k4_pre_topc(sK59,sK60,k4_tsp_2(sK59,sK60),X0) = k5_subset_1(k2_pre_topc(sK59),u1_struct_0(sK60),k3_tex_4(sK59,X0))
| ~ v5_pre_topc(k4_tsp_2(sK59,sK60),sK59,sK60)
| ~ m2_relset_1(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60))
| ~ v1_funct_2(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60))
| ~ m2_tsp_1(sK60,sK59) ),
inference(forward_subsumption_resolution,[],[f58542,f43825]) ).
fof(f58544,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ v1_funct_1(k4_tsp_2(sK59,sK60))
| k4_pre_topc(sK59,sK60,k4_tsp_2(sK59,sK60),X0) = k5_subset_1(k2_pre_topc(sK59),u1_struct_0(sK60),k3_tex_4(sK59,X0))
| ~ v5_pre_topc(k4_tsp_2(sK59,sK60),sK59,sK60)
| ~ m2_relset_1(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60))
| ~ v1_funct_2(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60)) ),
inference(forward_subsumption_resolution,[],[f58543,f43823]) ).
fof(f58545,plain,
! [X0] :
( ~ v1_funct_1(k1_tsp_2(sK59,sK60))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59)))
| k4_pre_topc(sK59,sK60,k4_tsp_2(sK59,sK60),X0) = k5_subset_1(k2_pre_topc(sK59),u1_struct_0(sK60),k3_tex_4(sK59,X0))
| ~ v5_pre_topc(k4_tsp_2(sK59,sK60),sK59,sK60)
| ~ m2_relset_1(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60))
| ~ v1_funct_2(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60)) ),
inference(forward_demodulation,[],[f58544,f58378]) ).
fof(f58546,plain,
! [X0] :
( k4_pre_topc(sK59,sK60,k4_tsp_2(sK59,sK60),X0) = k5_subset_1(k2_pre_topc(sK59),k2_pre_topc(sK60),k3_tex_4(sK59,X0))
| ~ v1_funct_1(k1_tsp_2(sK59,sK60))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ v5_pre_topc(k4_tsp_2(sK59,sK60),sK59,sK60)
| ~ m2_relset_1(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60))
| ~ v1_funct_2(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60)) ),
inference(forward_demodulation,[],[f58545,f58389]) ).
fof(f58547,plain,
! [X0] :
( k4_pre_topc(sK59,sK60,k1_tsp_2(sK59,sK60),X0) = k5_subset_1(k2_pre_topc(sK59),k2_pre_topc(sK60),k3_tex_4(sK59,X0))
| ~ v1_funct_1(k1_tsp_2(sK59,sK60))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ v5_pre_topc(k4_tsp_2(sK59,sK60),sK59,sK60)
| ~ m2_relset_1(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60))
| ~ v1_funct_2(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60)) ),
inference(forward_demodulation,[],[f58546,f58378]) ).
fof(f58548,plain,
! [X0] :
( ~ v5_pre_topc(k1_tsp_2(sK59,sK60),sK59,sK60)
| k4_pre_topc(sK59,sK60,k1_tsp_2(sK59,sK60),X0) = k5_subset_1(k2_pre_topc(sK59),k2_pre_topc(sK60),k3_tex_4(sK59,X0))
| ~ v1_funct_1(k1_tsp_2(sK59,sK60))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ m2_relset_1(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60))
| ~ v1_funct_2(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60)) ),
inference(forward_demodulation,[],[f58547,f58378]) ).
fof(f58549,plain,
! [X0] :
( ~ m2_relset_1(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60))
| ~ v5_pre_topc(k1_tsp_2(sK59,sK60),sK59,sK60)
| k4_pre_topc(sK59,sK60,k1_tsp_2(sK59,sK60),X0) = k5_subset_1(k2_pre_topc(sK59),k2_pre_topc(sK60),k3_tex_4(sK59,X0))
| ~ v1_funct_1(k1_tsp_2(sK59,sK60))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ v1_funct_2(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60)) ),
inference(forward_demodulation,[],[f58548,f58389]) ).
fof(f58550,plain,
! [X0] :
( ~ m2_relset_1(k1_tsp_2(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60))
| ~ v5_pre_topc(k1_tsp_2(sK59,sK60),sK59,sK60)
| k4_pre_topc(sK59,sK60,k1_tsp_2(sK59,sK60),X0) = k5_subset_1(k2_pre_topc(sK59),k2_pre_topc(sK60),k3_tex_4(sK59,X0))
| ~ v1_funct_1(k1_tsp_2(sK59,sK60))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ v1_funct_2(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60)) ),
inference(forward_demodulation,[],[f58549,f58378]) ).
fof(f58551,plain,
! [X0] :
( ~ v1_funct_2(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60))
| ~ m2_relset_1(k1_tsp_2(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60))
| ~ v5_pre_topc(k1_tsp_2(sK59,sK60),sK59,sK60)
| k4_pre_topc(sK59,sK60,k1_tsp_2(sK59,sK60),X0) = k5_subset_1(k2_pre_topc(sK59),k2_pre_topc(sK60),k3_tex_4(sK59,X0))
| ~ v1_funct_1(k1_tsp_2(sK59,sK60))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59))) ),
inference(forward_demodulation,[],[f58550,f58389]) ).
fof(f58552,plain,
! [X0] :
( ~ v1_funct_2(k1_tsp_2(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60))
| ~ m2_relset_1(k1_tsp_2(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60))
| ~ v5_pre_topc(k1_tsp_2(sK59,sK60),sK59,sK60)
| k4_pre_topc(sK59,sK60,k1_tsp_2(sK59,sK60),X0) = k5_subset_1(k2_pre_topc(sK59),k2_pre_topc(sK60),k3_tex_4(sK59,X0))
| ~ v1_funct_1(k1_tsp_2(sK59,sK60))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59))) ),
inference(forward_demodulation,[],[f58551,f58378]) ).
fof(f58554,definition,
( spl1395_66
<=> v1_funct_1(k1_tsp_2(sK59,sK60)) ),
introduced(definition,[new_symbols(definition,[spl1395_66])],[avatar_definition]) ).
fof(f58555,plain,
( ~ v1_funct_1(k1_tsp_2(sK59,sK60))
| spl1395_66 ),
inference(avatar_component_clause,[],[f58554]) ).
fof(f58557,definition,
( spl1395_67
<=> ! [X0] :
( k4_pre_topc(sK59,sK60,k1_tsp_2(sK59,sK60),X0) = k5_subset_1(k2_pre_topc(sK59),k2_pre_topc(sK60),k3_tex_4(sK59,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59))) ) ),
introduced(definition,[new_symbols(definition,[spl1395_67])],[avatar_definition]) ).
fof(f58558,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59)))
| k4_pre_topc(sK59,sK60,k1_tsp_2(sK59,sK60),X0) = k5_subset_1(k2_pre_topc(sK59),k2_pre_topc(sK60),k3_tex_4(sK59,X0)) )
| ~ spl1395_67 ),
inference(avatar_component_clause,[],[f58557]) ).
fof(f58560,definition,
( spl1395_68
<=> v5_pre_topc(k1_tsp_2(sK59,sK60),sK59,sK60) ),
introduced(definition,[new_symbols(definition,[spl1395_68])],[avatar_definition]) ).
fof(f58561,plain,
( ~ v5_pre_topc(k1_tsp_2(sK59,sK60),sK59,sK60)
| spl1395_68 ),
inference(avatar_component_clause,[],[f58560]) ).
fof(f58563,definition,
( spl1395_69
<=> m2_relset_1(k1_tsp_2(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60)) ),
introduced(definition,[new_symbols(definition,[spl1395_69])],[avatar_definition]) ).
fof(f58564,plain,
( ~ m2_relset_1(k1_tsp_2(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60))
| spl1395_69 ),
inference(avatar_component_clause,[],[f58563]) ).
fof(f58566,definition,
( spl1395_70
<=> v1_funct_2(k1_tsp_2(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60)) ),
introduced(definition,[new_symbols(definition,[spl1395_70])],[avatar_definition]) ).
fof(f58567,plain,
( ~ v1_funct_2(k1_tsp_2(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60))
| spl1395_70 ),
inference(avatar_component_clause,[],[f58566]) ).
fof(f58568,plain,
( ~ spl1395_66
| spl1395_67
| ~ spl1395_68
| ~ spl1395_69
| ~ spl1395_70 ),
inference(avatar_split_clause,[],[f58552,f58566,f58563,f58560,f58557,f58554]) ).
fof(f58575,plain,
! [X0] :
( v3_struct_0(sK59)
| v5_pre_topc(k4_tsp_2(sK59,X0),sK59,X0)
| ~ l1_pre_topc(sK59)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK59)
| ~ m1_pre_topc(X0,sK59) ),
inference(resolution,[],[f43646,f43821]) ).
fof(f58576,plain,
! [X0] :
( v5_pre_topc(k4_tsp_2(sK59,X0),sK59,X0)
| ~ l1_pre_topc(sK59)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK59)
| ~ m1_pre_topc(X0,sK59) ),
inference(forward_subsumption_resolution,[],[f58575,f43822]) ).
fof(f58577,plain,
! [X0] :
( ~ v2_tsp_2(X0,sK59)
| v3_struct_0(X0)
| v5_pre_topc(k4_tsp_2(sK59,X0),sK59,X0)
| ~ m1_pre_topc(X0,sK59) ),
inference(forward_subsumption_resolution,[],[f58576,f43820]) ).
fof(f58578,plain,
( v3_struct_0(sK60)
| v5_pre_topc(k4_tsp_2(sK59,sK60),sK59,sK60)
| ~ m1_pre_topc(sK60,sK59) ),
inference(resolution,[],[f58577,f43824]) ).
fof(f58579,plain,
( v5_pre_topc(k4_tsp_2(sK59,sK60),sK59,sK60)
| ~ m1_pre_topc(sK60,sK59) ),
inference(forward_subsumption_resolution,[],[f58578,f43825]) ).
fof(f58580,plain,
v5_pre_topc(k4_tsp_2(sK59,sK60),sK59,sK60),
inference(forward_subsumption_resolution,[],[f58579,f58360]) ).
fof(f58581,plain,
v5_pre_topc(k1_tsp_2(sK59,sK60),sK59,sK60),
inference(forward_demodulation,[],[f58580,f58378]) ).
fof(f58583,plain,
! [X0,X1] :
( ~ v4_pre_topc(X0,sK59)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK59)))
| ~ v2_tsp_2(X1,sK59)
| ~ m2_tsp_1(X1,sK59)
| v3_struct_0(sK59)
| sK48(X1,X0) = k4_xboole_0(X0,k4_xboole_0(X0,u1_struct_0(X1)))
| ~ l1_pre_topc(sK59) ),
inference(resolution,[],[f53762,f43821]) ).
fof(f58584,plain,
( v3_struct_0(sK60)
| v1_funct_2(sK53(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60))
| ~ m2_tsp_1(sK60,sK59) ),
inference(resolution,[],[f58452,f43824]) ).
fof(f58585,plain,
( v1_funct_2(sK53(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60))
| ~ m2_tsp_1(sK60,sK59) ),
inference(forward_subsumption_resolution,[],[f58584,f43825]) ).
fof(f58586,plain,
v1_funct_2(sK53(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60)),
inference(forward_subsumption_resolution,[],[f58585,f43823]) ).
fof(f58587,plain,
v1_funct_2(sK53(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60)),
inference(forward_demodulation,[],[f58586,f58389]) ).
fof(f58591,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59)))
| k4_xboole_0(X0,k4_xboole_0(X0,sK61)) = k5_subset_1(k2_pre_topc(sK59),X0,sK61) ),
inference(resolution,[],[f53771,f58390]) ).
fof(f58596,plain,
( v3_struct_0(sK60)
| m2_relset_1(sK53(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60))
| ~ m2_tsp_1(sK60,sK59) ),
inference(resolution,[],[f58453,f43824]) ).
fof(f58597,plain,
( m2_relset_1(sK53(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60))
| ~ m2_tsp_1(sK60,sK59) ),
inference(forward_subsumption_resolution,[],[f58596,f43825]) ).
fof(f58598,plain,
m2_relset_1(sK53(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60)),
inference(forward_subsumption_resolution,[],[f58597,f43823]) ).
fof(f58599,plain,
m2_relset_1(sK53(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60)),
inference(forward_demodulation,[],[f58598,f58389]) ).
fof(f58618,plain,
! [X0,X1] :
( ~ v3_borsuk_1(X0,sK59,X1)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK59),u1_struct_0(X1))
| ~ v5_pre_topc(X0,sK59,X1)
| ~ m2_relset_1(X0,u1_struct_0(sK59),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,sK59)
| ~ m2_tsp_1(X1,sK59)
| v3_struct_0(sK59)
| k1_tsp_2(sK59,X1) = X0
| ~ l1_pre_topc(sK59) ),
inference(resolution,[],[f43793,f43821]) ).
fof(f58619,plain,
( v3_struct_0(sK60)
| v1_funct_2(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60))
| ~ m1_pre_topc(sK60,sK59) ),
inference(resolution,[],[f58454,f43824]) ).
fof(f58620,plain,
( v1_funct_2(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60))
| ~ m1_pre_topc(sK60,sK59) ),
inference(forward_subsumption_resolution,[],[f58619,f43825]) ).
fof(f58621,plain,
v1_funct_2(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60)),
inference(forward_subsumption_resolution,[],[f58620,f58360]) ).
fof(f58622,plain,
v1_funct_2(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60)),
inference(forward_demodulation,[],[f58621,f58389]) ).
fof(f58623,plain,
v1_funct_2(k1_tsp_2(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60)),
inference(forward_demodulation,[],[f58622,f58378]) ).
fof(f58624,plain,
( v3_struct_0(sK60)
| m2_relset_1(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60))
| ~ m1_pre_topc(sK60,sK59) ),
inference(resolution,[],[f58455,f43824]) ).
fof(f58625,plain,
( m2_relset_1(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60))
| ~ m1_pre_topc(sK60,sK59) ),
inference(forward_subsumption_resolution,[],[f58624,f43825]) ).
fof(f58626,plain,
m2_relset_1(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60)),
inference(forward_subsumption_resolution,[],[f58625,f58360]) ).
fof(f58627,plain,
m2_relset_1(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60)),
inference(forward_demodulation,[],[f58626,f58389]) ).
fof(f58628,plain,
m2_relset_1(k1_tsp_2(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60)),
inference(forward_demodulation,[],[f58627,f58378]) ).
fof(f58631,plain,
m1_subset_1(u1_struct_0(sK60),k1_zfmisc_1(k2_pre_topc(sK59))),
inference(resolution,[],[f58448,f43823]) ).
fof(f58632,plain,
m1_subset_1(k2_pre_topc(sK60),k1_zfmisc_1(k2_pre_topc(sK59))),
inference(forward_demodulation,[],[f58631,f58389]) ).
fof(f58633,plain,
k4_xboole_0(k2_pre_topc(sK60),k4_xboole_0(k2_pre_topc(sK60),sK61)) = k5_subset_1(k2_pre_topc(sK59),k2_pre_topc(sK60),sK61),
inference(resolution,[],[f58632,f58591]) ).
fof(f58635,plain,
k5_subset_1(k2_pre_topc(sK59),k2_pre_topc(sK60),sK61) = k4_xboole_0(sK61,k4_xboole_0(sK61,k2_pre_topc(sK60))),
inference(forward_demodulation,[],[f58633,f53850]) ).
fof(f58667,plain,
! [X0,X1] :
( ~ v4_pre_topc(X0,sK59)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK59)))
| ~ v2_tsp_2(X1,sK59)
| ~ m2_tsp_1(X1,sK59)
| v4_pre_topc(sK48(X1,X0),X1)
| ~ l1_pre_topc(sK59) ),
inference(forward_subsumption_resolution,[],[f58384,f43822]) ).
fof(f58668,plain,
! [X0] :
( ~ v4_pre_topc(X0,sK59)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK59)))
| k3_tex_4(sK59,X0) = X0
| ~ l1_pre_topc(sK59) ),
inference(forward_subsumption_resolution,[],[f58385,f43822]) ).
fof(f58670,plain,
! [X0,X1] :
( ~ v4_pre_topc(X0,sK59)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK59)))
| ~ v2_tsp_2(X1,sK59)
| ~ m2_tsp_1(X1,sK59)
| sK48(X1,X0) = k4_xboole_0(X0,k4_xboole_0(X0,u1_struct_0(X1)))
| ~ l1_pre_topc(sK59) ),
inference(forward_subsumption_resolution,[],[f58583,f43822]) ).
fof(f58671,plain,
! [X0,X1] :
( ~ v3_borsuk_1(X0,sK59,X1)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK59),u1_struct_0(X1))
| ~ v5_pre_topc(X0,sK59,X1)
| ~ m2_relset_1(X0,u1_struct_0(sK59),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,sK59)
| ~ m2_tsp_1(X1,sK59)
| k1_tsp_2(sK59,X1) = X0
| ~ l1_pre_topc(sK59) ),
inference(forward_subsumption_resolution,[],[f58618,f43822]) ).
fof(f58674,plain,
! [X0,X1] :
( ~ v4_pre_topc(X0,sK59)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK59)))
| ~ v2_tsp_2(X1,sK59)
| ~ m2_tsp_1(X1,sK59)
| v4_pre_topc(sK48(X1,X0),X1) ),
inference(forward_subsumption_resolution,[],[f58667,f43820]) ).
fof(f58675,plain,
! [X0] :
( ~ v4_pre_topc(X0,sK59)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK59)))
| k3_tex_4(sK59,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f58668,f43820]) ).
fof(f58677,plain,
! [X0,X1] :
( ~ v4_pre_topc(X0,sK59)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK59)))
| ~ v2_tsp_2(X1,sK59)
| ~ m2_tsp_1(X1,sK59)
| sK48(X1,X0) = k4_xboole_0(X0,k4_xboole_0(X0,u1_struct_0(X1))) ),
inference(forward_subsumption_resolution,[],[f58670,f43820]) ).
fof(f58678,plain,
! [X0,X1] :
( ~ v3_borsuk_1(X0,sK59,X1)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK59),u1_struct_0(X1))
| ~ v5_pre_topc(X0,sK59,X1)
| ~ m2_relset_1(X0,u1_struct_0(sK59),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,sK59)
| ~ m2_tsp_1(X1,sK59)
| k1_tsp_2(sK59,X1) = X0 ),
inference(forward_subsumption_resolution,[],[f58671,f43820]) ).
fof(f58680,plain,
! [X0,X1] :
( ~ v2_tsp_2(X1,sK59)
| ~ v4_pre_topc(X0,sK59)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ m2_tsp_1(X1,sK59)
| v4_pre_topc(sK48(X1,X0),X1) ),
inference(forward_demodulation,[],[f58674,f58388]) ).
fof(f58681,plain,
! [X0] :
( ~ v4_pre_topc(X0,sK59)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59)))
| k3_tex_4(sK59,X0) = X0 ),
inference(forward_demodulation,[],[f58675,f58388]) ).
fof(f58683,plain,
! [X0,X1] :
( ~ v2_tsp_2(X1,sK59)
| ~ v4_pre_topc(X0,sK59)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ m2_tsp_1(X1,sK59)
| sK48(X1,X0) = k4_xboole_0(X0,k4_xboole_0(X0,u1_struct_0(X1))) ),
inference(forward_demodulation,[],[f58677,f58388]) ).
fof(f58684,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK59),u1_struct_0(X1))
| ~ v3_borsuk_1(X0,sK59,X1)
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK59,X1)
| ~ m2_relset_1(X0,u1_struct_0(sK59),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,sK59)
| ~ m2_tsp_1(X1,sK59)
| k1_tsp_2(sK59,X1) = X0 ),
inference(forward_demodulation,[],[f58678,f58388]) ).
fof(f58686,plain,
! [X0,X1] :
( ~ v2_tsp_2(X1,sK59)
| ~ v1_funct_2(X0,k2_pre_topc(sK59),u1_struct_0(X1))
| ~ v3_borsuk_1(X0,sK59,X1)
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK59,X1)
| v3_struct_0(X1)
| ~ m2_relset_1(X0,k2_pre_topc(sK59),u1_struct_0(X1))
| ~ m2_tsp_1(X1,sK59)
| k1_tsp_2(sK59,X1) = X0 ),
inference(forward_demodulation,[],[f58684,f58388]) ).
fof(f58687,plain,
( ~ m1_subset_1(sK61,k1_zfmisc_1(k2_pre_topc(sK59)))
| sK61 = k3_tex_4(sK59,sK61) ),
inference(resolution,[],[f58681,f43827]) ).
fof(f58689,plain,
sK61 = k3_tex_4(sK59,sK61),
inference(forward_subsumption_resolution,[],[f58687,f58390]) ).
fof(f58690,plain,
! [X0] :
( ~ v4_pre_topc(X0,sK59)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ m2_tsp_1(sK60,sK59)
| v4_pre_topc(sK48(sK60,X0),sK60) ),
inference(resolution,[],[f58680,f43824]) ).
fof(f58691,plain,
! [X0] :
( v4_pre_topc(sK48(sK60,X0),sK60)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ v4_pre_topc(X0,sK59) ),
inference(forward_subsumption_resolution,[],[f58690,f43823]) ).
fof(f58699,plain,
! [X0] :
( ~ v1_funct_2(X0,k2_pre_topc(sK59),u1_struct_0(sK60))
| ~ v3_borsuk_1(X0,sK59,sK60)
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK59,sK60)
| v3_struct_0(sK60)
| ~ m2_relset_1(X0,k2_pre_topc(sK59),u1_struct_0(sK60))
| ~ m2_tsp_1(sK60,sK59)
| k1_tsp_2(sK59,sK60) = X0 ),
inference(resolution,[],[f58686,f43824]) ).
fof(f58700,plain,
! [X0] :
( ~ v1_funct_2(X0,k2_pre_topc(sK59),u1_struct_0(sK60))
| ~ v3_borsuk_1(X0,sK59,sK60)
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK59,sK60)
| ~ m2_relset_1(X0,k2_pre_topc(sK59),u1_struct_0(sK60))
| ~ m2_tsp_1(sK60,sK59)
| k1_tsp_2(sK59,sK60) = X0 ),
inference(forward_subsumption_resolution,[],[f58699,f43825]) ).
fof(f58701,plain,
! [X0] :
( ~ v1_funct_2(X0,k2_pre_topc(sK59),u1_struct_0(sK60))
| ~ v3_borsuk_1(X0,sK59,sK60)
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK59,sK60)
| ~ m2_relset_1(X0,k2_pre_topc(sK59),u1_struct_0(sK60))
| k1_tsp_2(sK59,sK60) = X0 ),
inference(forward_subsumption_resolution,[],[f58700,f43823]) ).
fof(f58702,plain,
! [X0] :
( ~ v1_funct_2(X0,k2_pre_topc(sK59),k2_pre_topc(sK60))
| ~ v3_borsuk_1(X0,sK59,sK60)
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK59,sK60)
| ~ m2_relset_1(X0,k2_pre_topc(sK59),u1_struct_0(sK60))
| k1_tsp_2(sK59,sK60) = X0 ),
inference(forward_demodulation,[],[f58701,f58389]) ).
fof(f58703,plain,
! [X0] :
( ~ v3_borsuk_1(X0,sK59,sK60)
| ~ v1_funct_2(X0,k2_pre_topc(sK59),k2_pre_topc(sK60))
| ~ m2_relset_1(X0,k2_pre_topc(sK59),k2_pre_topc(sK60))
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK59,sK60)
| k1_tsp_2(sK59,sK60) = X0 ),
inference(forward_demodulation,[],[f58702,f58389]) ).
fof(f58704,plain,
! [X0] :
( ~ v4_pre_topc(X0,sK59)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ m2_tsp_1(sK60,sK59)
| sK48(sK60,X0) = k4_xboole_0(X0,k4_xboole_0(X0,u1_struct_0(sK60))) ),
inference(resolution,[],[f58683,f43824]) ).
fof(f58705,plain,
! [X0] :
( ~ v4_pre_topc(X0,sK59)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59)))
| sK48(sK60,X0) = k4_xboole_0(X0,k4_xboole_0(X0,u1_struct_0(sK60))) ),
inference(forward_subsumption_resolution,[],[f58704,f43823]) ).
fof(f58706,plain,
! [X0] :
( ~ v4_pre_topc(X0,sK59)
| k4_xboole_0(X0,k4_xboole_0(X0,k2_pre_topc(sK60))) = sK48(sK60,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59))) ),
inference(forward_demodulation,[],[f58705,f58389]) ).
fof(f58707,plain,
( k4_xboole_0(sK61,k4_xboole_0(sK61,k2_pre_topc(sK60))) = sK48(sK60,sK61)
| ~ m1_subset_1(sK61,k1_zfmisc_1(k2_pre_topc(sK59))) ),
inference(resolution,[],[f58706,f43827]) ).
fof(f58709,plain,
k4_xboole_0(sK61,k4_xboole_0(sK61,k2_pre_topc(sK60))) = sK48(sK60,sK61),
inference(forward_subsumption_resolution,[],[f58707,f58390]) ).
fof(f58718,plain,
( ~ v1_funct_2(sK53(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60))
| ~ m2_relset_1(sK53(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60))
| ~ v1_funct_1(sK53(sK59,sK60))
| ~ v5_pre_topc(sK53(sK59,sK60),sK59,sK60)
| k1_tsp_2(sK59,sK60) = sK53(sK59,sK60)
| v3_struct_0(sK60)
| ~ v2_tsp_2(sK60,sK59)
| ~ m2_tsp_1(sK60,sK59)
| v3_struct_0(sK59)
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59) ),
inference(resolution,[],[f58703,f43781]) ).
fof(f58719,plain,
( ~ v1_funct_2(sK53(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60))
| ~ m2_relset_1(sK53(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60))
| ~ v5_pre_topc(sK53(sK59,sK60),sK59,sK60)
| k1_tsp_2(sK59,sK60) = sK53(sK59,sK60)
| v3_struct_0(sK60)
| ~ v2_tsp_2(sK60,sK59)
| ~ m2_tsp_1(sK60,sK59)
| v3_struct_0(sK59)
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59) ),
inference(forward_subsumption_resolution,[],[f58718,f43785]) ).
fof(f58720,plain,
( ~ v1_funct_2(sK53(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60))
| ~ m2_relset_1(sK53(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60))
| k1_tsp_2(sK59,sK60) = sK53(sK59,sK60)
| v3_struct_0(sK60)
| ~ v2_tsp_2(sK60,sK59)
| ~ m2_tsp_1(sK60,sK59)
| v3_struct_0(sK59)
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59) ),
inference(forward_subsumption_resolution,[],[f58719,f43783]) ).
fof(f58721,plain,
( ~ m2_relset_1(sK53(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60))
| k1_tsp_2(sK59,sK60) = sK53(sK59,sK60)
| v3_struct_0(sK60)
| ~ v2_tsp_2(sK60,sK59)
| ~ m2_tsp_1(sK60,sK59)
| v3_struct_0(sK59)
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59) ),
inference(forward_subsumption_resolution,[],[f58720,f58587]) ).
fof(f58722,plain,
( k1_tsp_2(sK59,sK60) = sK53(sK59,sK60)
| v3_struct_0(sK60)
| ~ v2_tsp_2(sK60,sK59)
| ~ m2_tsp_1(sK60,sK59)
| v3_struct_0(sK59)
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59) ),
inference(forward_subsumption_resolution,[],[f58721,f58599]) ).
fof(f58723,plain,
( k1_tsp_2(sK59,sK60) = sK53(sK59,sK60)
| ~ v2_tsp_2(sK60,sK59)
| ~ m2_tsp_1(sK60,sK59)
| v3_struct_0(sK59)
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59) ),
inference(forward_subsumption_resolution,[],[f58722,f43825]) ).
fof(f58724,plain,
( k1_tsp_2(sK59,sK60) = sK53(sK59,sK60)
| ~ m2_tsp_1(sK60,sK59)
| v3_struct_0(sK59)
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59) ),
inference(forward_subsumption_resolution,[],[f58723,f43824]) ).
fof(f58725,plain,
( k1_tsp_2(sK59,sK60) = sK53(sK59,sK60)
| v3_struct_0(sK59)
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59) ),
inference(forward_subsumption_resolution,[],[f58724,f43823]) ).
fof(f58726,plain,
( k1_tsp_2(sK59,sK60) = sK53(sK59,sK60)
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59) ),
inference(forward_subsumption_resolution,[],[f58725,f43822]) ).
fof(f58727,plain,
( k1_tsp_2(sK59,sK60) = sK53(sK59,sK60)
| ~ l1_pre_topc(sK59) ),
inference(forward_subsumption_resolution,[],[f58726,f43821]) ).
fof(f58728,plain,
k1_tsp_2(sK59,sK60) = sK53(sK59,sK60),
inference(forward_subsumption_resolution,[],[f58727,f43820]) ).
fof(f58734,plain,
( v1_funct_1(k1_tsp_2(sK59,sK60))
| v3_struct_0(sK60)
| ~ v2_tsp_2(sK60,sK59)
| ~ m2_tsp_1(sK60,sK59)
| v3_struct_0(sK59)
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59) ),
inference(superposition,[],[f43785,f58728]) ).
fof(f58737,plain,
( v3_struct_0(sK60)
| ~ v2_tsp_2(sK60,sK59)
| ~ m2_tsp_1(sK60,sK59)
| v3_struct_0(sK59)
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59)
| spl1395_66 ),
inference(forward_subsumption_resolution,[],[f58734,f58555]) ).
fof(f58741,plain,
( ~ v2_tsp_2(sK60,sK59)
| ~ m2_tsp_1(sK60,sK59)
| v3_struct_0(sK59)
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59)
| spl1395_66 ),
inference(forward_subsumption_resolution,[],[f58737,f43825]) ).
fof(f58745,plain,
( ~ m2_tsp_1(sK60,sK59)
| v3_struct_0(sK59)
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59)
| spl1395_66 ),
inference(forward_subsumption_resolution,[],[f58741,f43824]) ).
fof(f58749,plain,
( v3_struct_0(sK59)
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59)
| spl1395_66 ),
inference(forward_subsumption_resolution,[],[f58745,f43823]) ).
fof(f58753,plain,
( ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59)
| spl1395_66 ),
inference(forward_subsumption_resolution,[],[f58749,f43822]) ).
fof(f58757,plain,
( ~ l1_pre_topc(sK59)
| spl1395_66 ),
inference(forward_subsumption_resolution,[],[f58753,f43821]) ).
fof(f58761,plain,
( $false
| spl1395_66 ),
inference(forward_subsumption_resolution,[],[f58757,f43820]) ).
fof(f58762,plain,
spl1395_66,
inference(avatar_contradiction_clause,[],[f58761]) ).
fof(f58766,plain,
( $false
| spl1395_68 ),
inference(forward_subsumption_resolution,[],[f58561,f58581]) ).
fof(f58767,plain,
spl1395_68,
inference(avatar_contradiction_clause,[],[f58766]) ).
fof(f58774,plain,
( $false
| spl1395_69 ),
inference(forward_subsumption_resolution,[],[f58564,f58628]) ).
fof(f58775,plain,
spl1395_69,
inference(avatar_contradiction_clause,[],[f58774]) ).
fof(f58776,plain,
( $false
| spl1395_70 ),
inference(forward_subsumption_resolution,[],[f58567,f58623]) ).
fof(f58777,plain,
spl1395_70,
inference(avatar_contradiction_clause,[],[f58776]) ).
fof(f58779,plain,
( k4_pre_topc(sK59,sK60,k1_tsp_2(sK59,sK60),sK61) = k5_subset_1(k2_pre_topc(sK59),k2_pre_topc(sK60),k3_tex_4(sK59,sK61))
| ~ spl1395_67 ),
inference(resolution,[],[f58558,f58390]) ).
fof(f58781,plain,
( k4_pre_topc(sK59,sK60,k1_tsp_2(sK59,sK60),sK61) = k5_subset_1(k2_pre_topc(sK59),k2_pre_topc(sK60),sK61)
| ~ spl1395_67 ),
inference(forward_demodulation,[],[f58779,f58689]) ).
fof(f58782,plain,
( k4_pre_topc(sK59,sK60,k1_tsp_2(sK59,sK60),sK61) = k4_xboole_0(sK61,k4_xboole_0(sK61,k2_pre_topc(sK60)))
| ~ spl1395_67 ),
inference(forward_demodulation,[],[f58781,f58635]) ).
fof(f58783,plain,
( k4_pre_topc(sK59,sK60,k1_tsp_2(sK59,sK60),sK61) = sK48(sK60,sK61)
| ~ spl1395_67 ),
inference(forward_demodulation,[],[f58782,f58709]) ).
fof(f58784,plain,
( ~ v4_pre_topc(sK48(sK60,sK61),sK60)
| ~ spl1395_67 ),
inference(superposition,[],[f58379,f58783]) ).
fof(f58803,plain,
( ~ m1_subset_1(sK61,k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ v4_pre_topc(sK61,sK59)
| ~ spl1395_67 ),
inference(resolution,[],[f58784,f58691]) ).
fof(f58807,plain,
( ~ v4_pre_topc(sK61,sK59)
| ~ spl1395_67 ),
inference(forward_subsumption_resolution,[],[f58803,f58390]) ).
fof(f58808,plain,
( $false
| ~ spl1395_67 ),
inference(forward_subsumption_resolution,[],[f58807,f43827]) ).
fof(f58809,plain,
~ spl1395_67,
inference(avatar_contradiction_clause,[],[f58808]) ).
cnf(s54,plain,
( ~ spl1395_66
| spl1395_67
| ~ spl1395_68
| ~ spl1395_69
| ~ spl1395_70 ),
inference(sat_conversion,[],[f58568]) ).
cnf(s60,plain,
spl1395_66,
inference(sat_conversion,[],[f58762]) ).
cnf(s61,plain,
spl1395_68,
inference(sat_conversion,[],[f58767]) ).
cnf(s62,plain,
spl1395_69,
inference(sat_conversion,[],[f58775]) ).
cnf(s63,plain,
spl1395_70,
inference(sat_conversion,[],[f58777]) ).
cnf(s68,plain,
~ spl1395_67,
inference(sat_conversion,[],[f58809]) ).
cnf(s69,plain,
$false,
inference(rat,[],[s54,s63,s62,s61,s68,s60]) ).
fof(f58810,plain,
$false,
inference(avatar_sat_refutation,[],[s69]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP042+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n014.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 19:03:07 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running first-order theorem proving
% 0.09/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.74/3.54 % (2075286)Detected formulas, will run a generic FOF schedule.
% 16.74/3.54 % (2075297)dis-21_1_sil=8000:lcm=predicate:random_seed=3792489611:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2991 on theBenchmark for (2991ds/129Mi)
% 16.74/3.54 % (2075294)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1156582161:i=109:sd=1:ins=1:gsp=on:ss=axioms_2991 on theBenchmark for (2991ds/109Mi)
% 16.74/3.54 % (2075291)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3354920377:i=141193_2991 on theBenchmark for (2991ds/141193Mi)
% 16.74/3.54 % (2075292)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1455188130:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2991 on theBenchmark for (2991ds/134677Mi)
% 16.74/3.54 % (2075296)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=418036671:s2a=on:i=139:gtg=position_2991 on theBenchmark for (2991ds/139Mi)
% 16.74/3.54 % (2075295)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3833337883:i=119:av=off:ss=axioms_2991 on theBenchmark for (2991ds/119Mi)
% 16.74/3.54 % (2075293)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2464030414:i=141695:sd=1:nm=32:gsp=on:ss=included_2991 on theBenchmark for (2991ds/141695Mi)
% 16.74/3.54 % (2075296)Instruction limit reached!
% 16.74/3.54 % (2075296)------------------------------
% 16.74/3.54 % (2075296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.74/3.54 % (2075296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.74/3.54 % (2075296)CaDiCaL version: 2.1.3
% 16.74/3.54 % (2075296)Termination reason: Instruction limit
% 16.74/3.54 % (2075296)Termination phase: Property scanning
% 16.74/3.54 % (2075296)Time elapsed: 0.060 s
% 16.74/3.54 % (2075296)Peak memory usage: 136 MB
% 16.74/3.54 % (2075296)Instructions burned: 140 (million)
% 16.74/3.54 % (2075294)Instruction limit reached!
% 16.74/3.54 % (2075294)------------------------------
% 16.74/3.54 % (2075294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.74/3.54 % (2075294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.74/3.54 % (2075294)CaDiCaL version: 2.1.3
% 16.74/3.54 % (2075294)Termination reason: Instruction limit
% 16.74/3.54 % (2075294)Termination phase: SInE selection
% 16.74/3.54 % (2075294)Time elapsed: 0.080 s
% 16.74/3.54 % (2075294)Peak memory usage: 135 MB
% 16.74/3.54 % (2075294)Instructions burned: 111 (million)
% 16.74/3.54 % (2075295)Instruction limit reached!
% 16.74/3.54 % (2075295)------------------------------
% 16.74/3.54 % (2075295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.74/3.54 % (2075295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.74/3.54 % (2075295)CaDiCaL version: 2.1.3
% 16.74/3.54 % (2075295)Termination reason: Instruction limit
% 16.74/3.54 % (2075295)Termination phase: SInE selection
% 16.74/3.54 % (2075295)Time elapsed: 0.085 s
% 16.74/3.54 % (2075295)Peak memory usage: 135 MB
% 16.74/3.54 % (2075295)Instructions burned: 119 (million)
% 16.74/3.54 % (2075297)Instruction limit reached!
% 16.74/3.54 % (2075297)------------------------------
% 16.74/3.54 % (2075297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.74/3.54 % (2075297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.74/3.54 % (2075297)CaDiCaL version: 2.1.3
% 16.74/3.54 % (2075297)Termination reason: Instruction limit
% 16.74/3.54 % (2075297)Termination phase: SInE selection
% 16.74/3.54 % (2075297)Time elapsed: 0.094 s
% 16.74/3.54 % (2075297)Peak memory usage: 135 MB
% 16.74/3.54 % (2075297)Instructions burned: 129 (million)
% 16.74/3.54 % (2075305)lrs+10_1_sil=8000:sp=occurrence:random_seed=2030984655:i=285:sd=3:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/285Mi)
% 16.74/3.54 % (2075307)lrs+1011_1_sil=32000:sp=occurrence:random_seed=813489778:i=325:sd=1:ss=axioms:sgt=32_2988 on theBenchmark for (2988ds/325Mi)
% 16.74/3.54 % (2075306)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4001013293:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/157Mi)
% 16.74/3.54 % (2075308)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1415513744:s2a=on:i=248:s2at=1.23:gtg=position_2988 on theBenchmark for (2988ds/248Mi)
% 16.74/3.54 % (2075306)Instruction limit reached!
% 23.14/4.57 % (2075306)------------------------------
% 23.14/4.57 % (2075306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.14/4.57 % (2075306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.14/4.57 % (2075306)CaDiCaL version: 2.1.3
% 23.14/4.57 % (2075306)Termination reason: Instruction limit
% 23.14/4.57 % (2075306)Termination phase: Property scanning
% 23.14/4.57 % (2075306)Time elapsed: 0.071 s
% 23.14/4.57 % (2075306)Peak memory usage: 136 MB
% 23.14/4.57 % (2075306)Instructions burned: 159 (million)
% 23.14/4.57 % (2075308)Instruction limit reached!
% 23.14/4.57 % (2075308)------------------------------
% 23.14/4.57 % (2075308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.14/4.57 % (2075308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.14/4.57 % (2075308)CaDiCaL version: 2.1.3
% 23.14/4.57 % (2075308)Termination reason: Instruction limit
% 23.14/4.57 % (2075308)Termination phase: Property scanning
% 23.14/4.57 % (2075308)Time elapsed: 0.108 s
% 23.14/4.57 % (2075308)Peak memory usage: 136 MB
% 23.14/4.57 % (2075308)Instructions burned: 249 (million)
% 23.14/4.57 % (2075305)Instruction limit reached!
% 23.14/4.57 % (2075305)------------------------------
% 23.14/4.57 % (2075305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.14/4.57 % (2075305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.14/4.57 % (2075305)CaDiCaL version: 2.1.3
% 23.14/4.57 % (2075305)Termination reason: Instruction limit
% 23.14/4.57 % (2075305)Termination phase: Preprocessing 3
% 23.14/4.57 % (2075305)Time elapsed: 0.236 s
% 23.14/4.57 % (2075305)Peak memory usage: 139 MB
% 23.14/4.57 % (2075305)Instructions burned: 286 (million)
% 23.14/4.57 % (2075313)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=988109971:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2986 on theBenchmark for (2986ds/294Mi)
% 23.14/4.57 % (2075307)Instruction limit reached!
% 23.14/4.57 % (2075307)------------------------------
% 23.14/4.57 % (2075307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.14/4.57 % (2075307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.14/4.57 % (2075307)CaDiCaL version: 2.1.3
% 23.14/4.57 % (2075307)Termination reason: Instruction limit
% 23.14/4.58 % (2075307)Termination phase: Saturation
% 23.14/4.58 % (2075307)Time elapsed: 0.253 s
% 23.14/4.58 % (2075307)Peak memory usage: 141 MB
% 23.14/4.58 % (2075307)Instructions burned: 325 (million)
% 23.14/4.58 % (2075314)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3374722003:i=2350_2985 on theBenchmark for (2985ds/2350Mi)
% 23.14/4.58 % (2075315)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1612469774:cts=off:i=113:fsr=off:ss=included:sgt=4_2984 on theBenchmark for (2984ds/113Mi)
% 23.14/4.58 % (2075317)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3728088859:i=127:av=off:fsr=off:sup=off_2984 on theBenchmark for (2984ds/127Mi)
% 23.14/4.58 % (2075313)Instruction limit reached!
% 23.14/4.58 % (2075313)------------------------------
% 23.14/4.58 % (2075313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.14/4.58 % (2075313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.14/4.58 % (2075313)CaDiCaL version: 2.1.3
% 23.14/4.58 % (2075313)Termination reason: Instruction limit
% 23.14/4.58 % (2075313)Termination phase: SInE selection
% 23.14/4.58 % (2075313)Time elapsed: 0.188 s
% 23.14/4.58 % (2075313)Peak memory usage: 136 MB
% 23.14/4.58 % (2075313)Instructions burned: 294 (million)
% 23.14/4.58 % (2075315)Instruction limit reached!
% 23.14/4.58 % (2075315)------------------------------
% 23.14/4.58 % (2075315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.14/4.58 % (2075315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.14/4.58 % (2075315)CaDiCaL version: 2.1.3
% 23.14/4.58 % (2075315)Termination reason: Instruction limit
% 23.14/4.58 % (2075315)Termination phase: SInE selection
% 23.14/4.58 % (2075315)Time elapsed: 0.087 s
% 23.14/4.58 % (2075315)Peak memory usage: 135 MB
% 23.14/4.58 % (2075315)Instructions burned: 114 (million)
% 23.14/4.58 % (2075317)Instruction limit reached!
% 23.14/4.58 % (2075317)------------------------------
% 23.14/4.58 % (2075317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.14/4.58 % (2075317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.14/4.58 % (2075317)CaDiCaL version: 2.1.3
% 14.55/5.78 % (2075317)Termination reason: Instruction limit
% 14.55/5.78 % (2075317)Termination phase: Preprocessing 1
% 14.55/5.78 % (2075317)Time elapsed: 0.098 s
% 14.55/5.78 % (2075317)Peak memory usage: 137 MB
% 14.55/5.78 % (2075317)Instructions burned: 128 (million)
% 14.55/5.78 % (2075321)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2645789022:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2982 on theBenchmark for (2982ds/114Mi)
% 14.55/5.78 % (2075322)lrs+10_1_sil=8000:sp=occurrence:random_seed=2834882050:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2982 on theBenchmark for (2982ds/907Mi)
% 14.55/5.78 % (2075321)Instruction limit reached!
% 14.55/5.78 % (2075321)------------------------------
% 14.55/5.78 % (2075321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.55/5.78 % (2075321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.55/5.78 % (2075321)CaDiCaL version: 2.1.3
% 14.55/5.78 % (2075321)Termination reason: Instruction limit
% 14.55/5.78 % (2075321)Termination phase: Property scanning
% 14.55/5.78 % (2075321)Time elapsed: 0.053 s
% 14.55/5.78 % (2075321)Peak memory usage: 136 MB
% 14.55/5.78 % (2075321)Instructions burned: 116 (million)
% 14.55/5.78 % (2075323)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3858810389:i=437:sd=1:aac=none:ss=included_2981 on theBenchmark for (2981ds/437Mi)
% 14.55/5.78 % (2075326)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2111198841:i=5202:ss=axioms:sgt=16_2980 on theBenchmark for (2980ds/5202Mi)
% 14.55/5.78 % (2075323)Instruction limit reached!
% 14.55/5.78 % (2075323)------------------------------
% 14.55/5.78 % (2075323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.55/5.78 % (2075323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.55/5.78 % (2075323)CaDiCaL version: 2.1.3
% 14.55/5.78 % (2075323)Termination reason: Instruction limit
% 14.55/5.78 % (2075323)Termination phase: Saturation
% 14.55/5.78 % (2075323)Time elapsed: 0.301 s
% 14.55/5.78 % (2075323)Peak memory usage: 144 MB
% 14.55/5.78 % (2075323)Instructions burned: 438 (million)
% 14.55/5.78 % (2075329)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2020457941:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2977 on theBenchmark for (2977ds/134Mi)
% 14.55/5.78 % (2075322)Instruction limit reached!
% 14.55/5.78 % (2075322)------------------------------
% 14.55/5.78 % (2075322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.55/5.78 % (2075322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.55/5.78 % (2075322)CaDiCaL version: 2.1.3
% 14.55/5.78 % (2075322)Termination reason: Instruction limit
% 14.55/5.78 % (2075322)Termination phase: Saturation
% 14.55/5.78 % (2075322)Time elapsed: 0.550 s
% 14.55/5.78 % (2075322)Peak memory usage: 151 MB
% 14.55/5.78 % (2075322)Instructions burned: 907 (million)
% 14.55/5.78 % (2075329)Instruction limit reached!
% 14.55/5.78 % (2075329)------------------------------
% 14.55/5.78 % (2075329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.55/5.78 % (2075329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.55/5.78 % (2075329)CaDiCaL version: 2.1.3
% 14.55/5.78 % (2075329)Termination reason: Instruction limit
% 14.55/5.78 % (2075329)Termination phase: SInE selection
% 14.55/5.78 % (2075329)Time elapsed: 0.102 s
% 14.55/5.78 % (2075329)Peak memory usage: 136 MB
% 14.55/5.78 % (2075329)Instructions burned: 135 (million)
% 14.55/5.78 % (2075331)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=943070517:st=8:i=592:sd=3:ep=RST:ss=axioms_2975 on theBenchmark for (2975ds/592Mi)
% 14.55/5.78 % (2075332)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2942446577:st=3:i=13193:sd=3:ss=axioms_2974 on theBenchmark for (2974ds/13193Mi)
% 14.55/5.78 % (2075314)Instruction limit reached!
% 14.55/5.78 % (2075314)------------------------------
% 14.55/5.78 % (2075314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.55/5.78 % (2075314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.55/5.78 % (2075314)CaDiCaL version: 2.1.3
% 14.55/5.78 % (2075314)Termination reason: Instruction limit
% 14.55/5.78 % (2075314)Termination phase: Property scanning
% 14.55/5.78 % (2075314)Time elapsed: 1.460 s
% 14.55/5.78 % (2075314)Peak memory usage: 232 MB
% 14.55/5.78 % (2075314)Instructions burned: 2352 (million)
% 14.55/5.78 % (2075331)Instruction limit reached!
% 14.55/5.78 % (2075331)------------------------------
% 14.55/5.78 % (2075331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.55/5.78 % (2075331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.55/5.78 % (2075331)CaDiCaL version: 2.1.3
% 14.55/5.78 % (2075331)Termination reason: Instruction limit
% 14.55/5.78 % (2075331)Termination phase: Preprocessing 2
% 14.55/5.78 % (2075331)Time elapsed: 0.472 s
% 14.55/5.78 % (2075331)Peak memory usage: 151 MB
% 14.55/5.78 % (2075331)Instructions burned: 592 (million)
% 14.55/5.78 % (2075335)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=1602641341:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/125Mi)
% 14.55/5.78 % (2075336)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2811310788:i=134:gtgl=5:slsql=off:gtg=exists_sym_2968 on theBenchmark for (2968ds/134Mi)
% 14.55/5.78 % (2075335)Instruction limit reached!
% 14.55/5.78 % (2075335)------------------------------
% 14.55/5.78 % (2075335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.55/5.78 % (2075335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.55/5.78 % (2075335)CaDiCaL version: 2.1.3
% 14.55/5.78 % (2075335)Termination reason: Instruction limit
% 14.55/5.78 % (2075335)Termination phase: Property scanning
% 14.55/5.78 % (2075335)Time elapsed: 0.058 s
% 14.55/5.78 % (2075335)Peak memory usage: 136 MB
% 14.55/5.78 % (2075335)Instructions burned: 126 (million)
% 14.55/5.78 % (2075336)Instruction limit reached!
% 14.55/5.78 % (2075336)------------------------------
% 14.55/5.78 % (2075336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.55/5.78 % (2075336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.55/5.78 % (2075336)CaDiCaL version: 2.1.3
% 14.55/5.78 % (2075336)Termination reason: Instruction limit
% 14.55/5.78 % (2075336)Termination phase: Property scanning
% 14.55/5.78 % (2075336)Time elapsed: 0.062 s
% 14.55/5.78 % (2075336)Peak memory usage: 136 MB
% 14.55/5.78 % (2075336)Instructions burned: 136 (million)
% 14.55/5.78 % (2075339)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2135162184:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2966 on theBenchmark for (2966ds/141Mi)
% 14.55/5.78 % (2075340)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2856812838:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2966 on theBenchmark for (2966ds/431Mi)
% 14.55/5.78 % (2075339)Instruction limit reached!
% 14.55/5.78 % (2075339)------------------------------
% 14.55/5.78 % (2075339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.55/5.78 % (2075339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.55/5.78 % (2075339)CaDiCaL version: 2.1.3
% 14.55/5.78 % (2075339)Termination reason: Instruction limit
% 14.55/5.78 % (2075339)Termination phase: SInE selection
% 14.55/5.78 % (2075339)Time elapsed: 0.108 s
% 14.55/5.78 % (2075339)Peak memory usage: 136 MB
% 14.55/5.78 % (2075339)Instructions burned: 142 (million)
% 14.55/5.78 % (2075343)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=184597260:i=6060:aac=none:ins=25_2963 on theBenchmark for (2963ds/6060Mi)
% 14.55/5.78 % (2075340)Instruction limit reached!
% 14.55/5.78 % (2075340)------------------------------
% 14.55/5.78 % (2075340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.55/5.78 % (2075340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.55/5.78 % (2075340)CaDiCaL version: 2.1.3
% 14.55/5.78 % (2075340)Termination reason: Instruction limit
% 14.55/5.78 % (2075340)Termination phase: Saturation
% 14.55/5.78 % (2075340)Time elapsed: 0.325 s
% 14.55/5.78 % (2075340)Peak memory usage: 144 MB
% 14.55/5.78 % (2075340)Instructions burned: 431 (million)
% 14.55/5.78 % (2075345)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=2511379058:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2961 on theBenchmark for (2961ds/150Mi)
% 14.55/5.78 % (2075345)Instruction limit reached!
% 14.55/5.78 % (2075345)------------------------------
% 14.55/5.78 % (2075345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.55/5.78 % (2075345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.55/5.78 % (2075345)CaDiCaL version: 2.1.3
% 14.55/5.78 % (2075345)Termination reason: Instruction limit
% 14.55/5.78 % (2075345)Termination phase: SInE selection
% 14.55/5.78 % (2075345)Time elapsed: 0.114 s
% 14.55/5.78 % (2075345)Peak memory usage: 136 MB
% 14.55/5.78 % (2075345)Instructions burned: 150 (million)
% 14.55/5.78 % (2075347)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3444788466:i=14155:bd=all_2958 on theBenchmark for (2958ds/14155Mi)
% 14.55/5.78 % (2075292)First to succeed.
% 14.55/5.78 % (2075292)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2075286"
% 14.55/5.78 % (2075292)Refutation found. Thanks to Tanya!
% 14.55/5.78 % SZS status Theorem for theBenchmark
% 14.55/5.78 % SZS output start Proof for theBenchmark
% See solution above
% 32.66/5.92 % (2075292)------------------------------
% 32.66/5.92 % (2075292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.66/5.92 % (2075292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.66/5.92 % (2075292)CaDiCaL version: 2.1.3
% 32.66/5.92 % (2075292)Termination reason: Refutation
% 32.66/5.92 % (2075292)Time elapsed: 3.902 s
% 32.66/5.92 % (2075292)Peak memory usage: 296 MB
% 32.66/5.92 % (2075292)Instructions burned: 6534 (million)
% 32.66/5.92 % (2075292)------------------------------
% 32.66/5.92 % (2075292)------------------------------
% 32.66/5.92 % (2075286)Success in time 5.364 s
% 32.66/5.92 % Vampire exiting
%------------------------------------------------------------------------------