%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : TOP041+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 : n019.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:03 PM UTC 2026
% Result : Theorem 23.48s 7.85s
% Output : Refutation 35.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 22
% Syntax : Number of formulae : 258 ( 53 unt; 6 def)
% Number of atoms : 1292 ( 154 equ)
% Maximal formula atoms : 20 ( 5 avg)
% Number of connectives : 1772 ( 738 ~; 851 |; 131 &)
% ( 17 <=>; 35 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 7 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(f34234,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)))
=> ( v3_pre_topc(X1,X0)
=> k3_tex_4(X0,X1) = X1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t58_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(f34410,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)))
=> ( v3_pre_topc(X2,X0)
<=> ( X2 = k3_tex_4(X0,X2)
& ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
& v3_pre_topc(X3,X1)
& X3 = k3_xboole_0(X2,u1_struct_0(X1)) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_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(f34438,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)))
=> ( v3_pre_topc(X2,X0)
=> v3_pre_topc(k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t34_tsp_2) ).
fof(f34439,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)))
=> ( v3_pre_topc(X2,X0)
=> v3_pre_topc(k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),X1) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f34438]) ).
fof(f34534,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(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(flattening,[],[f34534]) ).
fof(f34536,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(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(flattening,[],[f34536]) ).
fof(f34574,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(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(flattening,[],[f34574]) ).
fof(f34606,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v3_pre_topc(X2,X0)
<=> ( X2 = k3_tex_4(X0,X2)
& ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
& v3_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,[],[f34410]) ).
fof(f34607,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v3_pre_topc(X2,X0)
<=> ( X2 = k3_tex_4(X0,X2)
& ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
& v3_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,[],[f34606]) ).
fof(f34620,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(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(flattening,[],[f34620]) ).
fof(f34634,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(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(flattening,[],[f34634]) ).
fof(f34650,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(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(flattening,[],[f34650]) ).
fof(f34662,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ v3_pre_topc(k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),X1)
& v3_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,[],[f34439]) ).
fof(f34663,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ v3_pre_topc(k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),X1)
& v3_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,[],[f34662]) ).
fof(f34768,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(f34769,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,[],[f34768]) ).
fof(f34925,plain,
! [X0] :
( ! [X1] :
( k3_tex_4(X0,X1) = X1
| ~ v3_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,[],[f34234]) ).
fof(f34926,plain,
! [X0] :
( ! [X1] :
( k3_tex_4(X0,X1) = X1
| ~ v3_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,[],[f34925]) ).
fof(f35219,plain,
! [X0] :
( ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34366]) ).
fof(f35221,plain,
! [X0] :
( ! [X1] :
( l1_pre_topc(X1)
| ~ m2_tsp_1(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34364]) ).
fof(f35930,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f18318]) ).
fof(f36336,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f18256]) ).
fof(f41449,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v3_pre_topc(X2,X0)
| k3_tex_4(X0,X2) != X2
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v3_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)))
& v3_pre_topc(X3,X1)
& X3 = k3_xboole_0(X2,u1_struct_0(X1)) ) )
| ~ v3_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,[],[f34607]) ).
fof(f41450,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v3_pre_topc(X2,X0)
| k3_tex_4(X0,X2) != X2
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v3_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)))
& v3_pre_topc(X3,X1)
& X3 = k3_xboole_0(X2,u1_struct_0(X1)) ) )
| ~ v3_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,[],[f41449]) ).
fof(f41451,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v3_pre_topc(X2,X0)
| k3_tex_4(X0,X2) != X2
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v3_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)))
& v3_pre_topc(X4,X1)
& k3_xboole_0(X2,u1_struct_0(X1)) = X4 ) )
| ~ v3_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,[],[f41450]) ).
fof(f41452,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v3_pre_topc(X2,X0)
| k3_tex_4(X0,X2) != X2
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v3_pre_topc(X3,X1)
| k3_xboole_0(X2,u1_struct_0(X1)) != X3 ) )
& ( ( X2 = k3_tex_4(X0,X2)
& m1_subset_1(sK47(X1,X2),k1_zfmisc_1(u1_struct_0(X1)))
& v3_pre_topc(sK47(X1,X2),X1)
& k3_xboole_0(X2,u1_struct_0(X1)) = sK47(X1,X2) )
| ~ v3_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,[sK47]),skolemize(X4,sK47(X1,X2))],[f41451]) ).
fof(f41463,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))],[f34621]) ).
fof(f41464,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,[],[f34635]) ).
fof(f41471,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,[],[f34651]) ).
fof(f41472,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,[],[f41471]) ).
fof(f41473,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))],[f41472]) ).
fof(f41474,plain,
( ~ v3_pre_topc(k4_pre_topc(sK59,sK60,k4_tsp_2(sK59,sK60),sK61),sK60)
& v3_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)],[f34663]) ).
fof(f41664,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,[],[f35219]) ).
fof(f43642,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,[],[f34535]) ).
fof(f43643,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,[],[f34535]) ).
fof(f43644,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,[],[f34535]) ).
fof(f43646,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,[],[f34537]) ).
fof(f43698,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,[],[f34575]) ).
fof(f43745,plain,
! [X2,X0,X1] :
( k3_xboole_0(X2,u1_struct_0(X1)) = sK47(X1,X2)
| ~ v3_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,[],[f41452]) ).
fof(f43746,plain,
! [X2,X0,X1] :
( ~ v2_pre_topc(X0)
| ~ v3_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)
| v3_pre_topc(sK47(X1,X2),X1)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f41452]) ).
fof(f43778,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,[],[f41463]) ).
fof(f43779,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,[],[f41463]) ).
fof(f43780,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,[],[f41463]) ).
fof(f43781,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,[],[f41463]) ).
fof(f43782,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,[],[f41463]) ).
fof(f43790,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,[],[f41464]) ).
fof(f43804,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,[],[f41473]) ).
fof(f43816,plain,
l1_pre_topc(sK59),
inference(cnf_transformation,[],[f41474]) ).
fof(f43817,plain,
v2_pre_topc(sK59),
inference(cnf_transformation,[],[f41474]) ).
fof(f43818,plain,
~ v3_struct_0(sK59),
inference(cnf_transformation,[],[f41474]) ).
fof(f43819,plain,
m2_tsp_1(sK60,sK59),
inference(cnf_transformation,[],[f41474]) ).
fof(f43820,plain,
v2_tsp_2(sK60,sK59),
inference(cnf_transformation,[],[f41474]) ).
fof(f43821,plain,
~ v3_struct_0(sK60),
inference(cnf_transformation,[],[f41474]) ).
fof(f43822,plain,
m1_subset_1(sK61,k1_zfmisc_1(u1_struct_0(sK59))),
inference(cnf_transformation,[],[f41474]) ).
fof(f43823,plain,
v3_pre_topc(sK61,sK59),
inference(cnf_transformation,[],[f41474]) ).
fof(f43824,plain,
~ v3_pre_topc(k4_pre_topc(sK59,sK60,k4_tsp_2(sK59,sK60),sK61),sK60),
inference(cnf_transformation,[],[f41474]) ).
fof(f44046,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,[],[f34769]) ).
fof(f44211,plain,
! [X0,X1] :
( ~ v2_pre_topc(X0)
| ~ v3_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,[],[f34926]) ).
fof(f44568,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ m2_tsp_1(X1,X0)
| m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f41664]) ).
fof(f44571,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ m2_tsp_1(X1,X0)
| l1_pre_topc(X1) ),
inference(cnf_transformation,[],[f35221]) ).
fof(f45057,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k3_xboole_0(X1,X0),
inference(cnf_transformation,[],[f57]) ).
fof(f45852,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f35930]) ).
fof(f46092,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k4_xboole_0(X0,k4_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f117]) ).
fof(f46445,plain,
! [X0] :
( ~ l1_struct_0(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(cnf_transformation,[],[f36336]) ).
fof(f53754,plain,
! [X2,X0,X1] :
( ~ v2_pre_topc(X0)
| ~ v3_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)
| sK47(X1,X2) = k4_xboole_0(X2,k4_xboole_0(X2,u1_struct_0(X1)))
| ~ l1_pre_topc(X0) ),
inference(definition_unfolding,[],[f43745,f46092]) ).
fof(f53767,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,[],[f44046,f46092]) ).
fof(f53846,plain,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k4_xboole_0(X1,k4_xboole_0(X1,X0)),
inference(definition_unfolding,[],[f45057,f46092,f46092]) ).
fof(f56522,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,[],[f43804]) ).
fof(f56523,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,[],[f56522]) ).
fof(f58354,plain,
! [X0] :
( ~ m2_tsp_1(X0,sK59)
| l1_pre_topc(X0) ),
inference(resolution,[],[f44571,f43816]) ).
fof(f58355,plain,
! [X0] :
( ~ m2_tsp_1(X0,sK59)
| m1_pre_topc(X0,sK59) ),
inference(resolution,[],[f44568,f43816]) ).
fof(f58356,plain,
m1_pre_topc(sK60,sK59),
inference(resolution,[],[f58355,f43819]) ).
fof(f58364,plain,
l1_pre_topc(sK60),
inference(resolution,[],[f58354,f43819]) ).
fof(f58369,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,[],[f43646,f43817]) ).
fof(f58370,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,[],[f58369,f43818]) ).
fof(f58371,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,[],[f58370,f43816]) ).
fof(f58372,plain,
( v3_struct_0(sK60)
| k4_tsp_2(sK59,sK60) = k1_tsp_2(sK59,sK60)
| ~ m1_pre_topc(sK60,sK59) ),
inference(resolution,[],[f58371,f43820]) ).
fof(f58373,plain,
( k4_tsp_2(sK59,sK60) = k1_tsp_2(sK59,sK60)
| ~ m1_pre_topc(sK60,sK59) ),
inference(forward_subsumption_resolution,[],[f58372,f43821]) ).
fof(f58374,plain,
k4_tsp_2(sK59,sK60) = k1_tsp_2(sK59,sK60),
inference(forward_subsumption_resolution,[],[f58373,f58356]) ).
fof(f58375,plain,
~ v3_pre_topc(k4_pre_topc(sK59,sK60,k1_tsp_2(sK59,sK60),sK61),sK60),
inference(superposition,[],[f43824,f58374]) ).
fof(f58379,plain,
! [X0,X1] :
( ~ v3_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)
| v3_pre_topc(sK47(X1,X0),X1)
| ~ l1_pre_topc(sK59) ),
inference(resolution,[],[f43746,f43817]) ).
fof(f58381,plain,
! [X0] :
( ~ v3_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,[],[f44211,f43817]) ).
fof(f58383,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(resolution,[],[f46445,f45852]) ).
fof(f58384,plain,
u1_struct_0(sK59) = k2_pre_topc(sK59),
inference(resolution,[],[f58383,f43816]) ).
fof(f58385,plain,
u1_struct_0(sK60) = k2_pre_topc(sK60),
inference(resolution,[],[f58383,f58364]) ).
fof(f58386,plain,
m1_subset_1(sK61,k1_zfmisc_1(k2_pre_topc(sK59))),
inference(superposition,[],[f43822,f58384]) ).
fof(f58387,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,[],[f43642,f58384]) ).
fof(f58389,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,[],[f43644,f58384]) ).
fof(f58391,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,[],[f43698,f58384]) ).
fof(f58393,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,[],[f43779,f58384]) ).
fof(f58395,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,[],[f43781,f58384]) ).
fof(f58400,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,[],[f56523,f58384]) ).
fof(f58423,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,[],[f58400,f43818]) ).
fof(f58431,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,[],[f58395,f43818]) ).
fof(f58433,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,[],[f58393,f43818]) ).
fof(f58435,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,[],[f58391,f43818]) ).
fof(f58437,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,[],[f58389,f43818]) ).
fof(f58439,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,[],[f58387,f43818]) ).
fof(f58440,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,[],[f58423,f43817]) ).
fof(f58442,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,[],[f58431,f43817]) ).
fof(f58443,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,[],[f58433,f43817]) ).
fof(f58444,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,[],[f58435,f43816]) ).
fof(f58445,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,[],[f58437,f43817]) ).
fof(f58446,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,[],[f58439,f43817]) ).
fof(f58447,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,[],[f58440,f43816]) ).
fof(f58448,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,[],[f58442,f43816]) ).
fof(f58449,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,[],[f58443,f43816]) ).
fof(f58450,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,[],[f58445,f43816]) ).
fof(f58451,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,[],[f58446,f43816]) ).
fof(f58452,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,[],[f58447,f58444]) ).
fof(f58538,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,[],[f58452,f43820]) ).
fof(f58539,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,[],[f58538,f43821]) ).
fof(f58540,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,[],[f58539,f43819]) ).
fof(f58541,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,[],[f58540,f58374]) ).
fof(f58542,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,[],[f58541,f58385]) ).
fof(f58543,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,[],[f58542,f58374]) ).
fof(f58544,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,[],[f58543,f58374]) ).
fof(f58545,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,[],[f58544,f58385]) ).
fof(f58546,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,[],[f58545,f58374]) ).
fof(f58547,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,[],[f58546,f58385]) ).
fof(f58548,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,[],[f58547,f58374]) ).
fof(f58550,definition,
( spl1395_66
<=> v1_funct_1(k1_tsp_2(sK59,sK60)) ),
introduced(definition,[new_symbols(definition,[spl1395_66])],[avatar_definition]) ).
fof(f58551,plain,
( ~ v1_funct_1(k1_tsp_2(sK59,sK60))
| spl1395_66 ),
inference(avatar_component_clause,[],[f58550]) ).
fof(f58553,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(f58554,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,[],[f58553]) ).
fof(f58556,definition,
( spl1395_68
<=> v5_pre_topc(k1_tsp_2(sK59,sK60),sK59,sK60) ),
introduced(definition,[new_symbols(definition,[spl1395_68])],[avatar_definition]) ).
fof(f58557,plain,
( ~ v5_pre_topc(k1_tsp_2(sK59,sK60),sK59,sK60)
| spl1395_68 ),
inference(avatar_component_clause,[],[f58556]) ).
fof(f58559,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(f58560,plain,
( ~ m2_relset_1(k1_tsp_2(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60))
| spl1395_69 ),
inference(avatar_component_clause,[],[f58559]) ).
fof(f58562,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(f58563,plain,
( ~ v1_funct_2(k1_tsp_2(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60))
| spl1395_70 ),
inference(avatar_component_clause,[],[f58562]) ).
fof(f58564,plain,
( ~ spl1395_66
| spl1395_67
| ~ spl1395_68
| ~ spl1395_69
| ~ spl1395_70 ),
inference(avatar_split_clause,[],[f58548,f58562,f58559,f58556,f58553,f58550]) ).
fof(f58571,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,[],[f43643,f43817]) ).
fof(f58572,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,[],[f58571,f43818]) ).
fof(f58573,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,[],[f58572,f43816]) ).
fof(f58574,plain,
( v3_struct_0(sK60)
| v5_pre_topc(k4_tsp_2(sK59,sK60),sK59,sK60)
| ~ m1_pre_topc(sK60,sK59) ),
inference(resolution,[],[f58573,f43820]) ).
fof(f58575,plain,
( v5_pre_topc(k4_tsp_2(sK59,sK60),sK59,sK60)
| ~ m1_pre_topc(sK60,sK59) ),
inference(forward_subsumption_resolution,[],[f58574,f43821]) ).
fof(f58576,plain,
v5_pre_topc(k4_tsp_2(sK59,sK60),sK59,sK60),
inference(forward_subsumption_resolution,[],[f58575,f58356]) ).
fof(f58577,plain,
v5_pre_topc(k1_tsp_2(sK59,sK60),sK59,sK60),
inference(forward_demodulation,[],[f58576,f58374]) ).
fof(f58578,plain,
! [X0,X1] :
( ~ v3_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)
| sK47(X1,X0) = k4_xboole_0(X0,k4_xboole_0(X0,u1_struct_0(X1)))
| ~ l1_pre_topc(sK59) ),
inference(resolution,[],[f53754,f43817]) ).
fof(f58580,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,[],[f58448,f43820]) ).
fof(f58581,plain,
( v1_funct_2(sK53(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60))
| ~ m2_tsp_1(sK60,sK59) ),
inference(forward_subsumption_resolution,[],[f58580,f43821]) ).
fof(f58582,plain,
v1_funct_2(sK53(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60)),
inference(forward_subsumption_resolution,[],[f58581,f43819]) ).
fof(f58583,plain,
v1_funct_2(sK53(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60)),
inference(forward_demodulation,[],[f58582,f58385]) ).
fof(f58587,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,[],[f53767,f58386]) ).
fof(f58592,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,[],[f58449,f43820]) ).
fof(f58593,plain,
( m2_relset_1(sK53(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60))
| ~ m2_tsp_1(sK60,sK59) ),
inference(forward_subsumption_resolution,[],[f58592,f43821]) ).
fof(f58594,plain,
m2_relset_1(sK53(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60)),
inference(forward_subsumption_resolution,[],[f58593,f43819]) ).
fof(f58595,plain,
m2_relset_1(sK53(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60)),
inference(forward_demodulation,[],[f58594,f58385]) ).
fof(f58614,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,[],[f43790,f43817]) ).
fof(f58615,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,[],[f58450,f43820]) ).
fof(f58616,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,[],[f58615,f43821]) ).
fof(f58617,plain,
v1_funct_2(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60)),
inference(forward_subsumption_resolution,[],[f58616,f58356]) ).
fof(f58618,plain,
v1_funct_2(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60)),
inference(forward_demodulation,[],[f58617,f58385]) ).
fof(f58619,plain,
v1_funct_2(k1_tsp_2(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60)),
inference(forward_demodulation,[],[f58618,f58374]) ).
fof(f58622,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,[],[f58451,f43820]) ).
fof(f58623,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,[],[f58622,f43821]) ).
fof(f58624,plain,
m2_relset_1(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),u1_struct_0(sK60)),
inference(forward_subsumption_resolution,[],[f58623,f58356]) ).
fof(f58625,plain,
m2_relset_1(k4_tsp_2(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60)),
inference(forward_demodulation,[],[f58624,f58385]) ).
fof(f58626,plain,
m2_relset_1(k1_tsp_2(sK59,sK60),k2_pre_topc(sK59),k2_pre_topc(sK60)),
inference(forward_demodulation,[],[f58625,f58374]) ).
fof(f58628,plain,
m1_subset_1(u1_struct_0(sK60),k1_zfmisc_1(k2_pre_topc(sK59))),
inference(resolution,[],[f58444,f43819]) ).
fof(f58629,plain,
m1_subset_1(k2_pre_topc(sK60),k1_zfmisc_1(k2_pre_topc(sK59))),
inference(forward_demodulation,[],[f58628,f58385]) ).
fof(f58630,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,[],[f58629,f58587]) ).
fof(f58632,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,[],[f58630,f53846]) ).
fof(f58664,plain,
! [X0,X1] :
( ~ v3_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_pre_topc(sK47(X1,X0),X1)
| ~ l1_pre_topc(sK59) ),
inference(forward_subsumption_resolution,[],[f58379,f43818]) ).
fof(f58665,plain,
! [X0] :
( ~ v3_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,[],[f58381,f43818]) ).
fof(f58666,plain,
! [X0,X1] :
( ~ v3_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)
| sK47(X1,X0) = k4_xboole_0(X0,k4_xboole_0(X0,u1_struct_0(X1)))
| ~ l1_pre_topc(sK59) ),
inference(forward_subsumption_resolution,[],[f58578,f43818]) ).
fof(f58668,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,[],[f58614,f43818]) ).
fof(f58672,plain,
! [X0,X1] :
( ~ v3_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_pre_topc(sK47(X1,X0),X1) ),
inference(forward_subsumption_resolution,[],[f58664,f43816]) ).
fof(f58673,plain,
! [X0] :
( ~ v3_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,[],[f58665,f43816]) ).
fof(f58674,plain,
! [X0,X1] :
( ~ v3_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)
| sK47(X1,X0) = k4_xboole_0(X0,k4_xboole_0(X0,u1_struct_0(X1))) ),
inference(forward_subsumption_resolution,[],[f58666,f43816]) ).
fof(f58676,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,[],[f58668,f43816]) ).
fof(f58679,plain,
! [X0,X1] :
( ~ v2_tsp_2(X1,sK59)
| ~ v3_pre_topc(X0,sK59)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ m2_tsp_1(X1,sK59)
| v3_pre_topc(sK47(X1,X0),X1) ),
inference(forward_demodulation,[],[f58672,f58384]) ).
fof(f58680,plain,
! [X0] :
( ~ v3_pre_topc(X0,sK59)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59)))
| k3_tex_4(sK59,X0) = X0 ),
inference(forward_demodulation,[],[f58673,f58384]) ).
fof(f58681,plain,
! [X0,X1] :
( ~ v2_tsp_2(X1,sK59)
| ~ v3_pre_topc(X0,sK59)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ m2_tsp_1(X1,sK59)
| sK47(X1,X0) = k4_xboole_0(X0,k4_xboole_0(X0,u1_struct_0(X1))) ),
inference(forward_demodulation,[],[f58674,f58384]) ).
fof(f58683,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,[],[f58676,f58384]) ).
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,[],[f58683,f58384]) ).
fof(f58687,plain,
( ~ m1_subset_1(sK61,k1_zfmisc_1(k2_pre_topc(sK59)))
| sK61 = k3_tex_4(sK59,sK61) ),
inference(resolution,[],[f58680,f43823]) ).
fof(f58689,plain,
sK61 = k3_tex_4(sK59,sK61),
inference(forward_subsumption_resolution,[],[f58687,f58386]) ).
fof(f58690,plain,
! [X0] :
( ~ v3_pre_topc(X0,sK59)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ m2_tsp_1(sK60,sK59)
| v3_pre_topc(sK47(sK60,X0),sK60) ),
inference(resolution,[],[f58679,f43820]) ).
fof(f58691,plain,
! [X0] :
( v3_pre_topc(sK47(sK60,X0),sK60)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ v3_pre_topc(X0,sK59) ),
inference(forward_subsumption_resolution,[],[f58690,f43819]) ).
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,f43820]) ).
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,f43821]) ).
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,f43819]) ).
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,f58385]) ).
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,f58385]) ).
fof(f58722,definition,
( spl1395_73
<=> v3_pre_topc(sK47(sK60,sK61),sK60) ),
introduced(definition,[new_symbols(definition,[spl1395_73])],[avatar_definition]) ).
fof(f58723,plain,
( ~ v3_pre_topc(sK47(sK60,sK61),sK60)
| spl1395_73 ),
inference(avatar_component_clause,[],[f58722]) ).
fof(f58725,plain,
! [X0] :
( ~ v3_pre_topc(X0,sK59)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ m2_tsp_1(sK60,sK59)
| sK47(sK60,X0) = k4_xboole_0(X0,k4_xboole_0(X0,u1_struct_0(sK60))) ),
inference(resolution,[],[f58681,f43820]) ).
fof(f58726,plain,
! [X0] :
( ~ v3_pre_topc(X0,sK59)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59)))
| sK47(sK60,X0) = k4_xboole_0(X0,k4_xboole_0(X0,u1_struct_0(sK60))) ),
inference(forward_subsumption_resolution,[],[f58725,f43819]) ).
fof(f58727,plain,
! [X0] :
( ~ v3_pre_topc(X0,sK59)
| k4_xboole_0(X0,k4_xboole_0(X0,k2_pre_topc(sK60))) = sK47(sK60,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK59))) ),
inference(forward_demodulation,[],[f58726,f58385]) ).
fof(f58728,plain,
( k4_xboole_0(sK61,k4_xboole_0(sK61,k2_pre_topc(sK60))) = sK47(sK60,sK61)
| ~ m1_subset_1(sK61,k1_zfmisc_1(k2_pre_topc(sK59))) ),
inference(resolution,[],[f58727,f43823]) ).
fof(f58730,plain,
k4_xboole_0(sK61,k4_xboole_0(sK61,k2_pre_topc(sK60))) = sK47(sK60,sK61),
inference(forward_subsumption_resolution,[],[f58728,f58386]) ).
fof(f58739,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,f43778]) ).
fof(f58740,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,[],[f58739,f43782]) ).
fof(f58741,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,[],[f58740,f43780]) ).
fof(f58742,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,[],[f58741,f58583]) ).
fof(f58743,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,[],[f58742,f58595]) ).
fof(f58744,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,[],[f58743,f43821]) ).
fof(f58745,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,[],[f58744,f43820]) ).
fof(f58746,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,[],[f58745,f43819]) ).
fof(f58747,plain,
( k1_tsp_2(sK59,sK60) = sK53(sK59,sK60)
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59) ),
inference(forward_subsumption_resolution,[],[f58746,f43818]) ).
fof(f58748,plain,
( k1_tsp_2(sK59,sK60) = sK53(sK59,sK60)
| ~ l1_pre_topc(sK59) ),
inference(forward_subsumption_resolution,[],[f58747,f43817]) ).
fof(f58749,plain,
k1_tsp_2(sK59,sK60) = sK53(sK59,sK60),
inference(forward_subsumption_resolution,[],[f58748,f43816]) ).
fof(f58755,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,[],[f43782,f58749]) ).
fof(f58758,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,[],[f58755,f58551]) ).
fof(f58762,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,[],[f58758,f43821]) ).
fof(f58766,plain,
( ~ m2_tsp_1(sK60,sK59)
| v3_struct_0(sK59)
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59)
| spl1395_66 ),
inference(forward_subsumption_resolution,[],[f58762,f43820]) ).
fof(f58770,plain,
( v3_struct_0(sK59)
| ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59)
| spl1395_66 ),
inference(forward_subsumption_resolution,[],[f58766,f43819]) ).
fof(f58774,plain,
( ~ v2_pre_topc(sK59)
| ~ l1_pre_topc(sK59)
| spl1395_66 ),
inference(forward_subsumption_resolution,[],[f58770,f43818]) ).
fof(f58778,plain,
( ~ l1_pre_topc(sK59)
| spl1395_66 ),
inference(forward_subsumption_resolution,[],[f58774,f43817]) ).
fof(f58782,plain,
( $false
| spl1395_66 ),
inference(forward_subsumption_resolution,[],[f58778,f43816]) ).
fof(f58783,plain,
spl1395_66,
inference(avatar_contradiction_clause,[],[f58782]) ).
fof(f58787,plain,
( $false
| spl1395_68 ),
inference(forward_subsumption_resolution,[],[f58557,f58577]) ).
fof(f58788,plain,
spl1395_68,
inference(avatar_contradiction_clause,[],[f58787]) ).
fof(f58795,plain,
( $false
| spl1395_69 ),
inference(forward_subsumption_resolution,[],[f58560,f58626]) ).
fof(f58796,plain,
spl1395_69,
inference(avatar_contradiction_clause,[],[f58795]) ).
fof(f58797,plain,
( $false
| spl1395_70 ),
inference(forward_subsumption_resolution,[],[f58563,f58619]) ).
fof(f58798,plain,
spl1395_70,
inference(avatar_contradiction_clause,[],[f58797]) ).
fof(f58800,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,[],[f58554,f58386]) ).
fof(f58802,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,[],[f58800,f58689]) ).
fof(f58803,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,[],[f58802,f58632]) ).
fof(f58804,plain,
( k4_pre_topc(sK59,sK60,k1_tsp_2(sK59,sK60),sK61) = sK47(sK60,sK61)
| ~ spl1395_67 ),
inference(forward_demodulation,[],[f58803,f58730]) ).
fof(f58805,plain,
( ~ v3_pre_topc(sK47(sK60,sK61),sK60)
| ~ spl1395_67 ),
inference(superposition,[],[f58375,f58804]) ).
fof(f58808,plain,
( ~ spl1395_73
| ~ spl1395_67 ),
inference(avatar_split_clause,[],[f58805,f58553,f58722]) ).
fof(f58813,plain,
( ~ m1_subset_1(sK61,k1_zfmisc_1(k2_pre_topc(sK59)))
| ~ v3_pre_topc(sK61,sK59)
| spl1395_73 ),
inference(resolution,[],[f58723,f58691]) ).
fof(f58817,plain,
( ~ v3_pre_topc(sK61,sK59)
| spl1395_73 ),
inference(forward_subsumption_resolution,[],[f58813,f58386]) ).
fof(f58818,plain,
( $false
| spl1395_73 ),
inference(forward_subsumption_resolution,[],[f58817,f43823]) ).
fof(f58819,plain,
spl1395_73,
inference(avatar_contradiction_clause,[],[f58818]) ).
cnf(s54,plain,
( ~ spl1395_66
| spl1395_67
| ~ spl1395_68
| ~ spl1395_69
| ~ spl1395_70 ),
inference(sat_conversion,[],[f58564]) ).
cnf(s61,plain,
spl1395_66,
inference(sat_conversion,[],[f58783]) ).
cnf(s62,plain,
spl1395_68,
inference(sat_conversion,[],[f58788]) ).
cnf(s63,plain,
spl1395_69,
inference(sat_conversion,[],[f58796]) ).
cnf(s64,plain,
spl1395_70,
inference(sat_conversion,[],[f58798]) ).
cnf(s65,plain,
( ~ spl1395_67
| ~ spl1395_73 ),
inference(sat_conversion,[],[f58808]) ).
cnf(s69,plain,
spl1395_73,
inference(sat_conversion,[],[f58819]) ).
cnf(s70,plain,
~ spl1395_67,
inference(rat,[],[s65,s69]) ).
cnf(s72,plain,
$false,
inference(rat,[],[s54,s64,s63,s62,s70,s61]) ).
fof(f58820,plain,
$false,
inference(avatar_sat_refutation,[],[s72]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP041+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.19 % Computer : n019.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 19:02:39 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 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
% 18.83/5.14 % (120666)Detected formulas, will run a generic FOF schedule.
% 18.83/5.14 % (120671)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=888352557:i=141193_2978 on theBenchmark for (2978ds/141193Mi)
% 18.83/5.14 % (120674)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2630049261:i=109:sd=1:ins=1:gsp=on:ss=axioms_2978 on theBenchmark for (2978ds/109Mi)
% 18.83/5.14 % (120672)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=3582241610:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2978 on theBenchmark for (2978ds/134677Mi)
% 18.83/5.14 % (120673)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=1781642956:i=141695:sd=1:nm=32:gsp=on:ss=included_2978 on theBenchmark for (2978ds/141695Mi)
% 18.83/5.14 % (120675)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3845337176:i=119:av=off:ss=axioms_2978 on theBenchmark for (2978ds/119Mi)
% 18.83/5.14 % (120676)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2470029351:s2a=on:i=139:gtg=position_2978 on theBenchmark for (2978ds/139Mi)
% 18.83/5.14 % (120677)dis-21_1_sil=8000:lcm=predicate:random_seed=3110797841:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2978 on theBenchmark for (2978ds/129Mi)
% 18.83/5.14 % (120674)Instruction limit reached!
% 18.83/5.14 % (120674)------------------------------
% 18.83/5.14 % (120674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.83/5.14 % (120674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.83/5.14 % (120674)CaDiCaL version: 2.1.3
% 18.83/5.14 % (120674)Termination reason: Instruction limit
% 18.83/5.14 % (120674)Termination phase: SInE selection
% 18.83/5.14 % (120674)Time elapsed: 0.084 s
% 18.83/5.14 % (120674)Peak memory usage: 136 MB
% 18.83/5.14 % (120674)Instructions burned: 110 (million)
% 18.83/5.14 % (120676)Instruction limit reached!
% 18.83/5.14 % (120676)------------------------------
% 18.83/5.14 % (120676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.83/5.14 % (120676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.83/5.14 % (120676)CaDiCaL version: 2.1.3
% 18.83/5.14 % (120676)Termination reason: Instruction limit
% 18.83/5.14 % (120676)Termination phase: Property scanning
% 18.83/5.14 % (120676)Time elapsed: 0.063 s
% 18.83/5.14 % (120676)Peak memory usage: 136 MB
% 18.83/5.14 % (120676)Instructions burned: 140 (million)
% 18.83/5.14 % (120675)Instruction limit reached!
% 18.83/5.14 % (120675)------------------------------
% 18.83/5.14 % (120675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.83/5.14 % (120675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.83/5.14 % (120675)CaDiCaL version: 2.1.3
% 18.83/5.14 % (120675)Termination reason: Instruction limit
% 18.83/5.14 % (120675)Termination phase: SInE selection
% 18.83/5.14 % (120675)Time elapsed: 0.092 s
% 18.83/5.14 % (120675)Peak memory usage: 136 MB
% 18.83/5.14 % (120675)Instructions burned: 120 (million)
% 18.83/5.14 % (120677)Instruction limit reached!
% 18.83/5.14 % (120677)------------------------------
% 18.83/5.14 % (120677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.83/5.14 % (120677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.83/5.14 % (120677)CaDiCaL version: 2.1.3
% 18.83/5.14 % (120677)Termination reason: Instruction limit
% 18.83/5.14 % (120677)Termination phase: SInE selection
% 18.83/5.14 % (120677)Time elapsed: 0.097 s
% 18.83/5.14 % (120677)Peak memory usage: 136 MB
% 18.83/5.14 % (120677)Instructions burned: 130 (million)
% 18.83/5.14 % (120685)lrs+10_1_sil=8000:sp=occurrence:random_seed=2550440126:i=285:sd=3:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/285Mi)
% 18.83/5.14 % (120686)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4058271718:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/157Mi)
% 18.83/5.14 % (120687)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3252867131:i=325:sd=1:ss=axioms:sgt=32_2975 on theBenchmark for (2975ds/325Mi)
% 18.83/5.14 % (120688)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=3797798919:s2a=on:i=248:s2at=1.23:gtg=position_2975 on theBenchmark for (2975ds/248Mi)
% 18.83/5.14 % (120686)Instruction limit reached!
% 18.83/5.14 % (120686)------------------------------
% 25.83/6.37 % (120686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.83/6.37 % (120686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.83/6.37 % (120686)CaDiCaL version: 2.1.3
% 25.83/6.37 % (120686)Termination reason: Instruction limit
% 25.83/6.37 % (120686)Termination phase: Property scanning
% 25.83/6.37 % (120686)Time elapsed: 0.070 s
% 25.83/6.37 % (120686)Peak memory usage: 136 MB
% 25.83/6.37 % (120686)Instructions burned: 157 (million)
% 25.83/6.37 % (120688)Instruction limit reached!
% 25.83/6.37 % (120688)------------------------------
% 25.83/6.37 % (120688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.83/6.37 % (120688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.83/6.37 % (120688)CaDiCaL version: 2.1.3
% 25.83/6.37 % (120688)Termination reason: Instruction limit
% 25.83/6.37 % (120688)Termination phase: Property scanning
% 25.83/6.37 % (120688)Time elapsed: 0.108 s
% 25.83/6.37 % (120688)Peak memory usage: 136 MB
% 25.83/6.37 % (120688)Instructions burned: 250 (million)
% 25.83/6.37 % (120685)Instruction limit reached!
% 25.83/6.37 % (120685)------------------------------
% 25.83/6.37 % (120685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.83/6.37 % (120685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.83/6.37 % (120685)CaDiCaL version: 2.1.3
% 25.83/6.37 % (120685)Termination reason: Instruction limit
% 25.83/6.37 % (120685)Termination phase: Preprocessing 3
% 25.83/6.37 % (120685)Time elapsed: 0.225 s
% 25.83/6.37 % (120685)Peak memory usage: 140 MB
% 25.83/6.37 % (120685)Instructions burned: 285 (million)
% 25.83/6.37 % (120693)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2570594934:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2973 on theBenchmark for (2973ds/294Mi)
% 25.83/6.37 % (120687)Instruction limit reached!
% 25.83/6.37 % (120687)------------------------------
% 25.83/6.37 % (120687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.83/6.37 % (120687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.83/6.37 % (120687)CaDiCaL version: 2.1.3
% 25.83/6.37 % (120687)Termination reason: Instruction limit
% 25.83/6.37 % (120687)Termination phase: Saturation
% 25.83/6.37 % (120687)Time elapsed: 0.260 s
% 25.83/6.37 % (120687)Peak memory usage: 142 MB
% 25.83/6.37 % (120687)Instructions burned: 325 (million)
% 25.83/6.37 % (120694)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3021015476:i=2350_2972 on theBenchmark for (2972ds/2350Mi)
% 25.83/6.37 % (120695)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4227957462:cts=off:i=113:fsr=off:ss=included:sgt=4_2972 on theBenchmark for (2972ds/113Mi)
% 25.83/6.37 % (120693)Instruction limit reached!
% 25.83/6.37 % (120693)------------------------------
% 25.83/6.37 % (120693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.83/6.37 % (120693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.83/6.37 % (120693)CaDiCaL version: 2.1.3
% 25.83/6.37 % (120693)Termination reason: Instruction limit
% 25.83/6.37 % (120693)Termination phase: SInE selection
% 25.83/6.37 % (120693)Time elapsed: 0.182 s
% 25.83/6.37 % (120693)Peak memory usage: 136 MB
% 25.83/6.37 % (120693)Instructions burned: 295 (million)
% 25.83/6.37 % (120697)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1363207520:i=127:av=off:fsr=off:sup=off_2971 on theBenchmark for (2971ds/127Mi)
% 25.83/6.37 % (120695)Instruction limit reached!
% 25.83/6.37 % (120695)------------------------------
% 25.83/6.37 % (120695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.83/6.37 % (120695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.83/6.37 % (120695)CaDiCaL version: 2.1.3
% 25.83/6.37 % (120695)Termination reason: Instruction limit
% 25.83/6.37 % (120695)Termination phase: SInE selection
% 25.83/6.37 % (120695)Time elapsed: 0.086 s
% 25.83/6.37 % (120695)Peak memory usage: 136 MB
% 25.83/6.37 % (120695)Instructions burned: 113 (million)
% 25.83/6.37 % (120697)Instruction limit reached!
% 25.83/6.37 % (120697)------------------------------
% 25.83/6.37 % (120697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.83/6.37 % (120697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.83/6.37 % (120697)CaDiCaL version: 2.1.3
% 25.83/6.37 % (120697)Termination reason: Instruction limit
% 25.83/6.37 % (120697)Termination phase: Preprocessing 1
% 25.83/6.37 % (120697)Time elapsed: 0.098 s
% 23.48/7.85 % (120697)Peak memory usage: 137 MB
% 23.48/7.85 % (120697)Instructions burned: 128 (million)
% 23.48/7.85 % (120700)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1945406446:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2970 on theBenchmark for (2970ds/114Mi)
% 23.48/7.85 % (120702)lrs+10_1_sil=8000:sp=occurrence:random_seed=743769949:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2969 on theBenchmark for (2969ds/907Mi)
% 23.48/7.85 % (120700)Instruction limit reached!
% 23.48/7.85 % (120700)------------------------------
% 23.48/7.85 % (120700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.48/7.85 % (120700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.48/7.85 % (120700)CaDiCaL version: 2.1.3
% 23.48/7.85 % (120700)Termination reason: Instruction limit
% 23.48/7.85 % (120700)Termination phase: Property scanning
% 23.48/7.85 % (120700)Time elapsed: 0.053 s
% 23.48/7.85 % (120700)Peak memory usage: 136 MB
% 23.48/7.85 % (120700)Instructions burned: 116 (million)
% 23.48/7.85 % (120703)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=977313945:i=437:sd=1:aac=none:ss=included_2968 on theBenchmark for (2968ds/437Mi)
% 23.48/7.85 % (120706)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=613139913:i=5202:ss=axioms:sgt=16_2967 on theBenchmark for (2967ds/5202Mi)
% 23.48/7.85 % (120703)Instruction limit reached!
% 23.48/7.85 % (120703)------------------------------
% 23.48/7.85 % (120703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.48/7.85 % (120703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.48/7.85 % (120703)CaDiCaL version: 2.1.3
% 23.48/7.85 % (120703)Termination reason: Instruction limit
% 23.48/7.85 % (120703)Termination phase: Saturation
% 23.48/7.85 % (120703)Time elapsed: 0.305 s
% 23.48/7.85 % (120703)Peak memory usage: 144 MB
% 23.48/7.85 % (120703)Instructions burned: 438 (million)
% 23.48/7.85 % (120702)Instruction limit reached!
% 23.48/7.85 % (120702)------------------------------
% 23.48/7.85 % (120702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.48/7.85 % (120702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.48/7.85 % (120702)CaDiCaL version: 2.1.3
% 23.48/7.85 % (120702)Termination reason: Instruction limit
% 23.48/7.85 % (120702)Termination phase: Saturation
% 23.48/7.85 % (120702)Time elapsed: 0.546 s
% 23.48/7.85 % (120702)Peak memory usage: 151 MB
% 23.48/7.85 % (120702)Instructions burned: 907 (million)
% 23.48/7.85 % (120709)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1540597498:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2963 on theBenchmark for (2963ds/134Mi)
% 23.48/7.85 % (120709)Instruction limit reached!
% 23.48/7.85 % (120709)------------------------------
% 23.48/7.85 % (120709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.48/7.85 % (120709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.48/7.85 % (120709)CaDiCaL version: 2.1.3
% 23.48/7.85 % (120709)Termination reason: Instruction limit
% 23.48/7.85 % (120709)Termination phase: SInE selection
% 23.48/7.85 % (120709)Time elapsed: 0.099 s
% 23.48/7.85 % (120709)Peak memory usage: 136 MB
% 23.48/7.85 % (120709)Instructions burned: 135 (million)
% 23.48/7.85 % (120710)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2797340429:st=8:i=592:sd=3:ep=RST:ss=axioms_2962 on theBenchmark for (2962ds/592Mi)
% 23.48/7.85 % (120712)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2200538053:st=3:i=13193:sd=3:ss=axioms_2961 on theBenchmark for (2961ds/13193Mi)
% 23.48/7.85 % (120710)Instruction limit reached!
% 23.48/7.85 % (120710)------------------------------
% 23.48/7.85 % (120710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.48/7.85 % (120710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.48/7.85 % (120710)CaDiCaL version: 2.1.3
% 23.48/7.85 % (120710)Termination reason: Instruction limit
% 23.48/7.85 % (120710)Termination phase: Preprocessing 2
% 23.48/7.85 % (120710)Time elapsed: 0.450 s
% 23.48/7.85 % (120710)Peak memory usage: 152 MB
% 23.48/7.85 % (120710)Instructions burned: 592 (million)
% 23.48/7.85 % (120694)Instruction limit reached!
% 23.48/7.85 % (120694)------------------------------
% 23.48/7.85 % (120694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.48/7.85 % (120694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.48/7.85 % (120694)CaDiCaL version: 2.1.3
% 23.48/7.85 % (120694)Termination reason: Instruction limit
% 23.48/7.85 % (120694)Termination phase: Property scanning
% 23.48/7.85 % (120694)Time elapsed: 1.571 s
% 23.48/7.85 % (120694)Peak memory usage: 232 MB
% 23.48/7.85 % (120694)Instructions burned: 2352 (million)
% 23.48/7.85 % (120715)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=4038537889:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2956 on theBenchmark for (2956ds/125Mi)
% 23.48/7.85 % (120715)Instruction limit reached!
% 23.48/7.85 % (120715)------------------------------
% 23.48/7.85 % (120715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.48/7.85 % (120715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.48/7.85 % (120715)CaDiCaL version: 2.1.3
% 23.48/7.85 % (120715)Termination reason: Instruction limit
% 23.48/7.85 % (120715)Termination phase: Property scanning
% 23.48/7.85 % (120715)Time elapsed: 0.057 s
% 23.48/7.85 % (120715)Peak memory usage: 136 MB
% 23.48/7.85 % (120715)Instructions burned: 128 (million)
% 23.48/7.85 % (120716)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=978326663:i=134:gtgl=5:slsql=off:gtg=exists_sym_2955 on theBenchmark for (2955ds/134Mi)
% 23.48/7.85 % (120716)Instruction limit reached!
% 23.48/7.85 % (120716)------------------------------
% 23.48/7.85 % (120716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.48/7.85 % (120716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.48/7.85 % (120716)CaDiCaL version: 2.1.3
% 23.48/7.85 % (120716)Termination reason: Instruction limit
% 23.48/7.85 % (120716)Termination phase: Property scanning
% 23.48/7.85 % (120716)Time elapsed: 0.061 s
% 23.48/7.85 % (120716)Peak memory usage: 136 MB
% 23.48/7.85 % (120716)Instructions burned: 135 (million)
% 23.48/7.85 % (120718)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3090187884:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2953 on theBenchmark for (2953ds/141Mi)
% 23.48/7.85 % (120718)Instruction limit reached!
% 23.48/7.85 % (120718)------------------------------
% 23.48/7.85 % (120718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.48/7.85 % (120718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.48/7.85 % (120718)CaDiCaL version: 2.1.3
% 23.48/7.85 % (120718)Termination reason: Instruction limit
% 23.48/7.85 % (120718)Termination phase: SInE selection
% 23.48/7.85 % (120718)Time elapsed: 0.105 s
% 23.48/7.85 % (120718)Peak memory usage: 136 MB
% 23.48/7.85 % (120718)Instructions burned: 141 (million)
% 23.48/7.85 % (120721)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=200388257:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2952 on theBenchmark for (2952ds/431Mi)
% 23.48/7.85 % (120723)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=635459481:i=6060:aac=none:ins=25_2951 on theBenchmark for (2951ds/6060Mi)
% 23.48/7.85 % (120721)Instruction limit reached!
% 23.48/7.85 % (120721)------------------------------
% 23.48/7.85 % (120721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.48/7.85 % (120721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.48/7.85 % (120721)CaDiCaL version: 2.1.3
% 23.48/7.85 % (120721)Termination reason: Instruction limit
% 23.48/7.85 % (120721)Termination phase: Saturation
% 23.48/7.85 % (120721)Time elapsed: 0.329 s
% 23.48/7.85 % (120721)Peak memory usage: 144 MB
% 23.48/7.85 % (120721)Instructions burned: 432 (million)
% 23.48/7.85 % (120726)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=2585274953:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2947 on theBenchmark for (2947ds/150Mi)
% 23.48/7.85 % (120726)Instruction limit reached!
% 23.48/7.85 % (120726)------------------------------
% 23.48/7.85 % (120726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.48/7.85 % (120726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.48/7.85 % (120726)CaDiCaL version: 2.1.3
% 23.48/7.85 % (120726)Termination reason: Instruction limit
% 23.48/7.85 % (120726)Termination phase: SInE selection
% 23.48/7.85 % (120726)Time elapsed: 0.113 s
% 23.48/7.85 % (120726)Peak memory usage: 136 MB
% 23.48/7.85 % (120726)Instructions burned: 150 (million)
% 23.48/7.85 % (120728)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=606714833:i=14155:bd=all_2944 on theBenchmark for (2944ds/14155Mi)
% 23.48/7.85 % (120672)First to succeed.
% 23.48/7.85 % (120672)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-120666"
% 23.48/7.85 % (120672)Refutation found. Thanks to Tanya!
% 23.48/7.85 % SZS status Theorem for theBenchmark
% 23.48/7.85 % SZS output start Proof for theBenchmark
% See solution above
% 35.90/8.09 % (120672)------------------------------
% 35.90/8.09 % (120672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.90/8.09 % (120672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.90/8.09 % (120672)CaDiCaL version: 2.1.3
% 35.90/8.09 % (120672)Termination reason: Refutation
% 35.90/8.09 % (120672)Time elapsed: 4.446 s
% 35.90/8.09 % (120672)Peak memory usage: 284 MB
% 35.90/8.09 % (120672)Instructions burned: 6536 (million)
% 35.90/8.09 % (120672)------------------------------
% 35.90/8.09 % (120672)------------------------------
% 35.90/8.09 % (120666)Success in time 7.186 s
% 35.90/8.09 % Vampire exiting
%------------------------------------------------------------------------------