%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : TOP038+1 : 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 : n010.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:01 PM UTC 2026
% Result : Theorem 9.07s 3.04s
% Output : Refutation 17.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 52
% Number of leaves : 29
% Syntax : Number of formulae : 293 ( 35 unt; 13 def)
% Number of atoms : 1745 ( 106 equ)
% Maximal formula atoms : 21 ( 5 avg)
% Number of connectives : 2656 (1204 ~;1325 |; 78 &)
% ( 19 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 7 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 28 ( 26 usr; 14 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 4 con; 0-4 aty)
% Number of variables : 228 ( 0 sgn 216 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,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)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
=> k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),k4_subset_1(u1_struct_0(X0),X2,X3)) = k4_subset_1(u1_struct_0(X1),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X3)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t31_tsp_2) ).
fof(f2,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)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
=> k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),k4_subset_1(u1_struct_0(X0),X2,X3)) = k4_subset_1(u1_struct_0(X1),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X3)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f52,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k4_subset_1(X0,X1,X2) = k4_subset_1(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k4_subset_1) ).
fof(f54,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(f60,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& l1_pre_topc(X0)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> m1_subset_1(k3_tex_4(X0,X1),k1_zfmisc_1(u1_struct_0(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k3_tex_4) ).
fof(f62,axiom,
! [X0,X1,X2,X3] :
( ( l1_struct_0(X0)
& l1_struct_0(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_pre_topc) ).
fof(f63,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> m1_subset_1(k4_subset_1(X0,X1,X2),k1_zfmisc_1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_subset_1) ).
fof(f64,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(f67,axiom,
! [X0] :
( l1_pre_topc(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f73,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(f118,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k4_subset_1) ).
fof(f120,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(f121,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f122,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(f126,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m1_pre_topc(X1,X0)
=> m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_tsep_1) ).
fof(f127,axiom,
! [X0,X1,X2] : k3_xboole_0(X0,k2_xboole_0(X1,X2)) = k2_xboole_0(k3_xboole_0(X0,X1),k3_xboole_0(X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t23_xboole_1) ).
fof(f130,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> k3_tex_4(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k4_subset_1(u1_struct_0(X0),k3_tex_4(X0,X1),k3_tex_4(X0,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t38_tex_4) ).
fof(f167,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),k4_subset_1(u1_struct_0(X0),X2,X3)) != k4_subset_1(u1_struct_0(X1),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X3))
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(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,[],[f2]) ).
fof(f168,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),k4_subset_1(u1_struct_0(X0),X2,X3)) != k4_subset_1(u1_struct_0(X1),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X3))
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(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,[],[f167]) ).
fof(f172,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,[],[f64]) ).
fof(f173,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,[],[f172]) ).
fof(f174,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,[],[f54]) ).
fof(f175,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,[],[f174]) ).
fof(f176,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k3_tex_4(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k4_subset_1(u1_struct_0(X0),k3_tex_4(X0,X1),k3_tex_4(X0,X2))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f130]) ).
fof(f177,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k3_tex_4(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k4_subset_1(u1_struct_0(X0),k3_tex_4(X0,X1),k3_tex_4(X0,X2))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f176]) ).
fof(f178,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f118]) ).
fof(f179,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f178]) ).
fof(f182,plain,
! [X0,X1,X2] :
( m1_subset_1(k4_subset_1(X0,X1,X2),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f63]) ).
fof(f183,plain,
! [X0,X1,X2] :
( m1_subset_1(k4_subset_1(X0,X1,X2),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f182]) ).
fof(f184,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k4_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f52]) ).
fof(f185,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k4_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f184]) ).
fof(f200,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f62]) ).
fof(f201,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f200]) ).
fof(f202,plain,
! [X0] :
( ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f122]) ).
fof(f204,plain,
! [X0] :
( ! [X1] :
( l1_pre_topc(X1)
| ~ m2_tsp_1(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f73]) ).
fof(f206,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_pre_topc(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f126]) ).
fof(f212,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,[],[f120]) ).
fof(f213,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,[],[f212]) ).
fof(f220,plain,
! [X0,X1] :
( m1_subset_1(k3_tex_4(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(ennf_transformation,[],[f60]) ).
fof(f221,plain,
! [X0,X1] :
( m1_subset_1(k3_tex_4(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(flattening,[],[f220]) ).
fof(f262,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f67]) ).
fof(f315,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k4_subset_1(u1_struct_0(sK3),k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),sK4),k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),sK5))
& m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK2)))
& m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2)))
& ~ v3_struct_0(sK3)
& v2_tsp_2(sK3,sK2)
& m2_tsp_1(sK3,sK2)
& ~ v3_struct_0(sK2)
& v2_pre_topc(sK2)
& l1_pre_topc(sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4),skolemize(X3,sK5)],[f168]) ).
fof(f316,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,[],[f175]) ).
fof(f317,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,[],[f316]) ).
fof(f318,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k4_tsp_2(X0,X1)
| ( k5_subset_1(u1_struct_0(X0),sK6(X0,X1,X2),k3_tex_4(X0,sK7(X0,X1,X2))) != k4_pre_topc(X0,X1,X2,sK7(X0,X1,X2))
& m1_subset_1(sK7(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)))
& u1_struct_0(X1) = sK6(X0,X1,X2)
& m1_subset_1(sK6(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,[sK6,sK7]),skolemize(X3,sK6(X0,X1,X2)),skolemize(X4,sK7(X0,X1,X2))],[f317]) ).
fof(f320,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,[],[f202]) ).
fof(f326,plain,
! [X0,X1,X2] :
( ( m2_relset_1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) )
& ( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f121]) ).
fof(f343,plain,
l1_pre_topc(sK2),
inference(cnf_transformation,[],[f315]) ).
fof(f344,plain,
v2_pre_topc(sK2),
inference(cnf_transformation,[],[f315]) ).
fof(f345,plain,
~ v3_struct_0(sK2),
inference(cnf_transformation,[],[f315]) ).
fof(f346,plain,
m2_tsp_1(sK3,sK2),
inference(cnf_transformation,[],[f315]) ).
fof(f347,plain,
v2_tsp_2(sK3,sK2),
inference(cnf_transformation,[],[f315]) ).
fof(f348,plain,
~ v3_struct_0(sK3),
inference(cnf_transformation,[],[f315]) ).
fof(f349,plain,
m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2))),
inference(cnf_transformation,[],[f315]) ).
fof(f350,plain,
m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK2))),
inference(cnf_transformation,[],[f315]) ).
fof(f351,plain,
k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k4_subset_1(u1_struct_0(sK3),k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),sK4),k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),sK5)),
inference(cnf_transformation,[],[f315]) ).
fof(f354,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,[],[f173]) ).
fof(f355,plain,
! [X0,X1] :
( v5_pre_topc(k4_tsp_2(X0,X1),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(cnf_transformation,[],[f173]) ).
fof(f356,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,[],[f173]) ).
fof(f357,plain,
! [X0,X1] :
( v1_funct_1(k4_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(cnf_transformation,[],[f173]) ).
fof(f358,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,[],[f318]) ).
fof(f364,plain,
! [X2,X0,X1] :
( k3_tex_4(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k4_subset_1(u1_struct_0(X0),k3_tex_4(X0,X1),k3_tex_4(X0,X2))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f177]) ).
fof(f365,plain,
! [X2,X0,X1] :
( k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f179]) ).
fof(f367,plain,
! [X2,X0,X1] :
( m1_subset_1(k4_subset_1(X0,X1,X2),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f183]) ).
fof(f368,plain,
! [X2,X0,X1] :
( k4_subset_1(X0,X1,X2) = k4_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f185]) ).
fof(f381,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f201]) ).
fof(f382,plain,
! [X0,X1] :
( m1_pre_topc(X1,X0)
| ~ m2_tsp_1(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f320]) ).
fof(f385,plain,
! [X0,X1] :
( ~ m2_tsp_1(X1,X0)
| l1_pre_topc(X1)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f204]) ).
fof(f392,plain,
! [X0,X1] :
( m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_pre_topc(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f206]) ).
fof(f396,plain,
! [X2,X0,X1] :
( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f326]) ).
fof(f400,plain,
! [X2,X0,X1] :
( 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(cnf_transformation,[],[f213]) ).
fof(f404,plain,
! [X0,X1] :
( m1_subset_1(k3_tex_4(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f221]) ).
fof(f405,plain,
! [X2,X0,X1] : k3_xboole_0(X0,k2_xboole_0(X1,X2)) = k2_xboole_0(k3_xboole_0(X0,X1),k3_xboole_0(X0,X2)),
inference(cnf_transformation,[],[f127]) ).
fof(f479,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f262]) ).
fof(f604,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,[],[f358]) ).
fof(f605,plain,
! [X0,X1,X6] :
( 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)
| ~ 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))
| ~ 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(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,[],[f604]) ).
fof(f608,plain,
! [X2,X0,X1] :
( k3_tex_4(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k2_xboole_0(k3_tex_4(X0,X1),k3_tex_4(X0,X2))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(k3_tex_4(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(k3_tex_4(X0,X2),k1_zfmisc_1(u1_struct_0(X0))) ),
inference(superposition,[],[f364,f365]) ).
fof(f609,plain,
! [X2,X0,X1] :
( k3_tex_4(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k2_xboole_0(k3_tex_4(X0,X1),k3_tex_4(X0,X2))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(k3_tex_4(X0,X1),k1_zfmisc_1(u1_struct_0(X0))) ),
inference(forward_subsumption_resolution,[],[f608,f404]) ).
fof(f611,definition,
( spl27_1
<=> m1_subset_1(k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),sK5),k1_zfmisc_1(u1_struct_0(sK3))) ),
introduced(definition,[new_symbols(definition,[spl27_1])],[avatar_definition]) ).
fof(f612,plain,
( m1_subset_1(k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),sK5),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ spl27_1 ),
inference(avatar_component_clause,[],[f611]) ).
fof(f613,plain,
( ~ m1_subset_1(k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),sK5),k1_zfmisc_1(u1_struct_0(sK3)))
| spl27_1 ),
inference(avatar_component_clause,[],[f611]) ).
fof(f615,definition,
( spl27_2
<=> m1_subset_1(k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),sK4),k1_zfmisc_1(u1_struct_0(sK3))) ),
introduced(definition,[new_symbols(definition,[spl27_2])],[avatar_definition]) ).
fof(f616,plain,
( m1_subset_1(k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),sK4),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ spl27_2 ),
inference(avatar_component_clause,[],[f615]) ).
fof(f617,plain,
( ~ m1_subset_1(k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),sK4),k1_zfmisc_1(u1_struct_0(sK3)))
| spl27_2 ),
inference(avatar_component_clause,[],[f615]) ).
fof(f624,plain,
! [X2,X0,X1] :
( k3_tex_4(X0,k4_subset_1(u1_struct_0(X0),X1,X2)) = k2_xboole_0(k3_tex_4(X0,X1),k3_tex_4(X0,X2))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(forward_subsumption_resolution,[],[f609,f404]) ).
fof(f627,plain,
! [X2,X0,X1] :
( k3_xboole_0(u1_struct_0(X0),k3_tex_4(X1,X2)) = k4_pre_topc(X1,X0,k4_tsp_2(X1,X0),X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(X1)))
| ~ v1_funct_1(k4_tsp_2(X1,X0))
| ~ v1_funct_2(k4_tsp_2(X1,X0),u1_struct_0(X1),u1_struct_0(X0))
| ~ v5_pre_topc(k4_tsp_2(X1,X0),X1,X0)
| ~ m2_relset_1(k4_tsp_2(X1,X0),u1_struct_0(X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,X1)
| ~ m2_tsp_1(X0,X1)
| v3_struct_0(X1)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1)
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(X1)))
| ~ m1_subset_1(k3_tex_4(X1,X2),k1_zfmisc_1(u1_struct_0(X1))) ),
inference(superposition,[],[f605,f400]) ).
fof(f628,plain,
! [X2,X0,X1] :
( k3_xboole_0(u1_struct_0(X0),k3_tex_4(X1,X2)) = k4_pre_topc(X1,X0,k4_tsp_2(X1,X0),X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(X1)))
| ~ v1_funct_1(k4_tsp_2(X1,X0))
| ~ v1_funct_2(k4_tsp_2(X1,X0),u1_struct_0(X1),u1_struct_0(X0))
| ~ v5_pre_topc(k4_tsp_2(X1,X0),X1,X0)
| ~ m2_relset_1(k4_tsp_2(X1,X0),u1_struct_0(X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,X1)
| ~ m2_tsp_1(X0,X1)
| v3_struct_0(X1)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1)
| ~ m1_subset_1(k3_tex_4(X1,X2),k1_zfmisc_1(u1_struct_0(X1))) ),
inference(duplicate_literal_removal,[],[f627]) ).
fof(f630,plain,
! [X2,X0,X1] :
( k3_xboole_0(u1_struct_0(X0),k3_tex_4(X1,X2)) = k4_pre_topc(X1,X0,k4_tsp_2(X1,X0),X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(X1)))
| ~ v1_funct_1(k4_tsp_2(X1,X0))
| ~ v1_funct_2(k4_tsp_2(X1,X0),u1_struct_0(X1),u1_struct_0(X0))
| ~ v5_pre_topc(k4_tsp_2(X1,X0),X1,X0)
| ~ m2_relset_1(k4_tsp_2(X1,X0),u1_struct_0(X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,X1)
| ~ m2_tsp_1(X0,X1)
| v3_struct_0(X1)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1) ),
inference(forward_subsumption_resolution,[],[f628,f404]) ).
fof(f639,plain,
! [X2,X0,X1] :
( k4_subset_1(X0,X1,X2) = k2_xboole_0(X2,X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(superposition,[],[f365,f368]) ).
fof(f640,plain,
! [X2,X0,X1] :
( k4_subset_1(X0,X1,X2) = k2_xboole_0(X2,X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(duplicate_literal_removal,[],[f639]) ).
fof(f671,definition,
( spl27_4
<=> m1_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3)) ),
introduced(definition,[new_symbols(definition,[spl27_4])],[avatar_definition]) ).
fof(f672,plain,
( m1_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl27_4 ),
inference(avatar_component_clause,[],[f671]) ).
fof(f673,plain,
( ~ m1_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| spl27_4 ),
inference(avatar_component_clause,[],[f671]) ).
fof(f675,definition,
( spl27_5
<=> v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3)) ),
introduced(definition,[new_symbols(definition,[spl27_5])],[avatar_definition]) ).
fof(f676,plain,
( v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl27_5 ),
inference(avatar_component_clause,[],[f675]) ).
fof(f677,plain,
( ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| spl27_5 ),
inference(avatar_component_clause,[],[f675]) ).
fof(f679,definition,
( spl27_6
<=> v1_funct_1(k4_tsp_2(sK2,sK3)) ),
introduced(definition,[new_symbols(definition,[spl27_6])],[avatar_definition]) ).
fof(f680,plain,
( v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ spl27_6 ),
inference(avatar_component_clause,[],[f679]) ).
fof(f681,plain,
( ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| spl27_6 ),
inference(avatar_component_clause,[],[f679]) ).
fof(f683,definition,
( spl27_7
<=> l1_struct_0(sK3) ),
introduced(definition,[new_symbols(definition,[spl27_7])],[avatar_definition]) ).
fof(f684,plain,
( l1_struct_0(sK3)
| ~ spl27_7 ),
inference(avatar_component_clause,[],[f683]) ).
fof(f685,plain,
( ~ l1_struct_0(sK3)
| spl27_7 ),
inference(avatar_component_clause,[],[f683]) ).
fof(f687,definition,
( spl27_8
<=> l1_struct_0(sK2) ),
introduced(definition,[new_symbols(definition,[spl27_8])],[avatar_definition]) ).
fof(f688,plain,
( l1_struct_0(sK2)
| ~ spl27_8 ),
inference(avatar_component_clause,[],[f687]) ).
fof(f689,plain,
( ~ l1_struct_0(sK2)
| spl27_8 ),
inference(avatar_component_clause,[],[f687]) ).
fof(f759,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k4_subset_1(u1_struct_0(sK3),k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),sK4),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)))
| ~ m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m1_subset_1(u1_struct_0(sK3),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2) ),
inference(superposition,[],[f351,f630]) ).
fof(f766,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k4_subset_1(u1_struct_0(sK3),k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),sK4),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)))
| ~ m1_subset_1(u1_struct_0(sK3),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2) ),
inference(forward_subsumption_resolution,[],[f759,f350]) ).
fof(f769,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k4_subset_1(u1_struct_0(sK3),k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),sK4),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)))
| ~ m1_subset_1(u1_struct_0(sK3),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2) ),
inference(forward_subsumption_resolution,[],[f766,f348]) ).
fof(f772,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k4_subset_1(u1_struct_0(sK3),k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),sK4),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)))
| ~ m1_subset_1(u1_struct_0(sK3),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2) ),
inference(forward_subsumption_resolution,[],[f769,f347]) ).
fof(f775,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k4_subset_1(u1_struct_0(sK3),k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),sK4),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)))
| ~ m1_subset_1(u1_struct_0(sK3),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2) ),
inference(forward_subsumption_resolution,[],[f772,f346]) ).
fof(f778,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k4_subset_1(u1_struct_0(sK3),k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),sK4),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)))
| ~ m1_subset_1(u1_struct_0(sK3),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2) ),
inference(forward_subsumption_resolution,[],[f775,f345]) ).
fof(f781,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k4_subset_1(u1_struct_0(sK3),k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),sK4),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)))
| ~ m1_subset_1(u1_struct_0(sK3),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ l1_pre_topc(sK2) ),
inference(forward_subsumption_resolution,[],[f778,f344]) ).
fof(f784,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k4_subset_1(u1_struct_0(sK3),k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),sK4),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)))
| ~ m1_subset_1(u1_struct_0(sK3),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f781,f343]) ).
fof(f788,definition,
( spl27_12
<=> m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3)) ),
introduced(definition,[new_symbols(definition,[spl27_12])],[avatar_definition]) ).
fof(f789,plain,
( m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl27_12 ),
inference(avatar_component_clause,[],[f788]) ).
fof(f790,plain,
( ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| spl27_12 ),
inference(avatar_component_clause,[],[f788]) ).
fof(f792,definition,
( spl27_13
<=> v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3) ),
introduced(definition,[new_symbols(definition,[spl27_13])],[avatar_definition]) ).
fof(f793,plain,
( v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ spl27_13 ),
inference(avatar_component_clause,[],[f792]) ).
fof(f794,plain,
( ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| spl27_13 ),
inference(avatar_component_clause,[],[f792]) ).
fof(f796,definition,
( spl27_14
<=> m1_subset_1(u1_struct_0(sK3),k1_zfmisc_1(u1_struct_0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl27_14])],[avatar_definition]) ).
fof(f797,plain,
( m1_subset_1(u1_struct_0(sK3),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ spl27_14 ),
inference(avatar_component_clause,[],[f796]) ).
fof(f798,plain,
( ~ m1_subset_1(u1_struct_0(sK3),k1_zfmisc_1(u1_struct_0(sK2)))
| spl27_14 ),
inference(avatar_component_clause,[],[f796]) ).
fof(f800,definition,
( spl27_15
<=> k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) = k4_subset_1(u1_struct_0(sK3),k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),sK4),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5))) ),
introduced(definition,[new_symbols(definition,[spl27_15])],[avatar_definition]) ).
fof(f802,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k4_subset_1(u1_struct_0(sK3),k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),sK4),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)))
| spl27_15 ),
inference(avatar_component_clause,[],[f800]) ).
fof(f803,plain,
( ~ spl27_12
| ~ spl27_13
| ~ spl27_5
| ~ spl27_6
| ~ spl27_14
| ~ spl27_15 ),
inference(avatar_split_clause,[],[f784,f800,f796,f679,f675,f792,f788]) ).
fof(f805,definition,
( spl27_16
<=> m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)),k1_zfmisc_1(u1_struct_0(sK3))) ),
introduced(definition,[new_symbols(definition,[spl27_16])],[avatar_definition]) ).
fof(f806,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ spl27_16 ),
inference(avatar_component_clause,[],[f805]) ).
fof(f858,plain,
! [X2,X0,X1] :
( m1_subset_1(k2_xboole_0(X0,X1),k1_zfmisc_1(X2))
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(superposition,[],[f367,f365]) ).
fof(f861,plain,
! [X2,X0,X1] :
( m1_subset_1(k2_xboole_0(X0,X1),k1_zfmisc_1(X2))
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(duplicate_literal_removal,[],[f858]) ).
fof(f866,plain,
( ~ l1_struct_0(sK2)
| ~ l1_struct_0(sK3)
| ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| spl27_1 ),
inference(resolution,[],[f381,f613]) ).
fof(f1022,plain,
( l1_pre_topc(sK3)
| ~ l1_pre_topc(sK2) ),
inference(resolution,[],[f385,f346]) ).
fof(f1023,plain,
l1_pre_topc(sK3),
inference(forward_subsumption_resolution,[],[f1022,f343]) ).
fof(f1756,plain,
( v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2)
| spl27_5 ),
inference(resolution,[],[f356,f677]) ).
fof(f1757,plain,
( ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2)
| spl27_5 ),
inference(forward_subsumption_resolution,[],[f1756,f345]) ).
fof(f1758,plain,
( ~ l1_pre_topc(sK2)
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2)
| spl27_5 ),
inference(forward_subsumption_resolution,[],[f1757,f344]) ).
fof(f1759,plain,
( v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2)
| spl27_5 ),
inference(forward_subsumption_resolution,[],[f1758,f343]) ).
fof(f1760,plain,
( ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2)
| spl27_5 ),
inference(forward_subsumption_resolution,[],[f1759,f348]) ).
fof(f1761,plain,
( ~ m1_pre_topc(sK3,sK2)
| spl27_5 ),
inference(forward_subsumption_resolution,[],[f1760,f347]) ).
fof(f1762,plain,
( ~ m2_tsp_1(sK3,sK2)
| ~ l1_pre_topc(sK2)
| spl27_5 ),
inference(resolution,[],[f1761,f382]) ).
fof(f1763,plain,
( ~ l1_pre_topc(sK2)
| spl27_5 ),
inference(forward_subsumption_resolution,[],[f1762,f346]) ).
fof(f1764,plain,
( $false
| spl27_5 ),
inference(forward_subsumption_resolution,[],[f1763,f343]) ).
fof(f1765,plain,
spl27_5,
inference(avatar_contradiction_clause,[],[f1764]) ).
fof(f1766,plain,
( v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2)
| spl27_6 ),
inference(resolution,[],[f681,f357]) ).
fof(f1767,plain,
( ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2)
| spl27_6 ),
inference(forward_subsumption_resolution,[],[f1766,f345]) ).
fof(f1768,plain,
( ~ l1_pre_topc(sK2)
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2)
| spl27_6 ),
inference(forward_subsumption_resolution,[],[f1767,f344]) ).
fof(f1769,plain,
( v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2)
| spl27_6 ),
inference(forward_subsumption_resolution,[],[f1768,f343]) ).
fof(f1770,plain,
( ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2)
| spl27_6 ),
inference(forward_subsumption_resolution,[],[f1769,f348]) ).
fof(f1771,plain,
( ~ m1_pre_topc(sK3,sK2)
| spl27_6 ),
inference(forward_subsumption_resolution,[],[f1770,f347]) ).
fof(f1772,plain,
( ~ m2_tsp_1(sK3,sK2)
| ~ l1_pre_topc(sK2)
| spl27_6 ),
inference(resolution,[],[f1771,f382]) ).
fof(f1773,plain,
( ~ l1_pre_topc(sK2)
| spl27_6 ),
inference(forward_subsumption_resolution,[],[f1772,f346]) ).
fof(f1774,plain,
( $false
| spl27_6 ),
inference(forward_subsumption_resolution,[],[f1773,f343]) ).
fof(f1775,plain,
spl27_6,
inference(avatar_contradiction_clause,[],[f1774]) ).
fof(f1776,plain,
( v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2)
| spl27_12 ),
inference(resolution,[],[f790,f354]) ).
fof(f1777,plain,
( ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2)
| spl27_12 ),
inference(forward_subsumption_resolution,[],[f1776,f345]) ).
fof(f1778,plain,
( ~ l1_pre_topc(sK2)
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2)
| spl27_12 ),
inference(forward_subsumption_resolution,[],[f1777,f344]) ).
fof(f1779,plain,
( v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2)
| spl27_12 ),
inference(forward_subsumption_resolution,[],[f1778,f343]) ).
fof(f1780,plain,
( ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2)
| spl27_12 ),
inference(forward_subsumption_resolution,[],[f1779,f348]) ).
fof(f1781,plain,
( ~ m1_pre_topc(sK3,sK2)
| spl27_12 ),
inference(forward_subsumption_resolution,[],[f1780,f347]) ).
fof(f1782,plain,
( ~ m2_tsp_1(sK3,sK2)
| ~ l1_pre_topc(sK2)
| spl27_12 ),
inference(resolution,[],[f1781,f382]) ).
fof(f1783,plain,
( ~ l1_pre_topc(sK2)
| spl27_12 ),
inference(forward_subsumption_resolution,[],[f1782,f346]) ).
fof(f1784,plain,
( $false
| spl27_12 ),
inference(forward_subsumption_resolution,[],[f1783,f343]) ).
fof(f1785,plain,
spl27_12,
inference(avatar_contradiction_clause,[],[f1784]) ).
fof(f1786,plain,
( v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2)
| spl27_13 ),
inference(resolution,[],[f794,f355]) ).
fof(f1787,plain,
( ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2)
| spl27_13 ),
inference(forward_subsumption_resolution,[],[f1786,f345]) ).
fof(f1788,plain,
( ~ l1_pre_topc(sK2)
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2)
| spl27_13 ),
inference(forward_subsumption_resolution,[],[f1787,f344]) ).
fof(f1789,plain,
( v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2)
| spl27_13 ),
inference(forward_subsumption_resolution,[],[f1788,f343]) ).
fof(f1790,plain,
( ~ v2_tsp_2(sK3,sK2)
| ~ m1_pre_topc(sK3,sK2)
| spl27_13 ),
inference(forward_subsumption_resolution,[],[f1789,f348]) ).
fof(f1791,plain,
( ~ m1_pre_topc(sK3,sK2)
| spl27_13 ),
inference(forward_subsumption_resolution,[],[f1790,f347]) ).
fof(f1792,plain,
( ~ m2_tsp_1(sK3,sK2)
| ~ l1_pre_topc(sK2)
| spl27_13 ),
inference(resolution,[],[f1791,f382]) ).
fof(f1793,plain,
( ~ l1_pre_topc(sK2)
| spl27_13 ),
inference(forward_subsumption_resolution,[],[f1792,f346]) ).
fof(f1794,plain,
( $false
| spl27_13 ),
inference(forward_subsumption_resolution,[],[f1793,f343]) ).
fof(f1795,plain,
spl27_13,
inference(avatar_contradiction_clause,[],[f1794]) ).
fof(f1977,plain,
( ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| spl27_4 ),
inference(resolution,[],[f396,f673]) ).
fof(f1978,plain,
( $false
| spl27_4
| ~ spl27_12 ),
inference(forward_subsumption_resolution,[],[f1977,f789]) ).
fof(f1979,plain,
( spl27_4
| ~ spl27_12 ),
inference(avatar_contradiction_clause,[],[f1978]) ).
fof(f1980,plain,
( ~ l1_pre_topc(sK3)
| spl27_7 ),
inference(resolution,[],[f685,f479]) ).
fof(f1981,plain,
( $false
| spl27_7 ),
inference(forward_subsumption_resolution,[],[f1980,f1023]) ).
fof(f1982,plain,
spl27_7,
inference(avatar_contradiction_clause,[],[f1981]) ).
fof(f1983,plain,
( ~ l1_pre_topc(sK2)
| spl27_8 ),
inference(resolution,[],[f689,f479]) ).
fof(f1984,plain,
( $false
| spl27_8 ),
inference(forward_subsumption_resolution,[],[f1983,f343]) ).
fof(f1985,plain,
spl27_8,
inference(avatar_contradiction_clause,[],[f1984]) ).
fof(f1986,plain,
( ~ l1_struct_0(sK3)
| ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| spl27_1
| ~ spl27_8 ),
inference(forward_subsumption_resolution,[],[f866,f688]) ).
fof(f1987,plain,
( ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| spl27_1
| ~ spl27_7
| ~ spl27_8 ),
inference(forward_subsumption_resolution,[],[f1986,f684]) ).
fof(f1988,plain,
( ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| spl27_1
| ~ spl27_6
| ~ spl27_7
| ~ spl27_8 ),
inference(forward_subsumption_resolution,[],[f1987,f680]) ).
fof(f1989,plain,
( ~ m1_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| spl27_1
| ~ spl27_5
| ~ spl27_6
| ~ spl27_7
| ~ spl27_8 ),
inference(forward_subsumption_resolution,[],[f1988,f676]) ).
fof(f1990,plain,
( $false
| spl27_1
| ~ spl27_4
| ~ spl27_5
| ~ spl27_6
| ~ spl27_7
| ~ spl27_8 ),
inference(forward_subsumption_resolution,[],[f1989,f672]) ).
fof(f1991,plain,
( spl27_1
| ~ spl27_4
| ~ spl27_5
| ~ spl27_6
| ~ spl27_7
| ~ spl27_8 ),
inference(avatar_contradiction_clause,[],[f1990]) ).
fof(f2026,plain,
( ~ l1_struct_0(sK2)
| ~ l1_struct_0(sK3)
| ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| spl27_2 ),
inference(resolution,[],[f617,f381]) ).
fof(f2032,plain,
( ~ l1_struct_0(sK3)
| ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| spl27_2
| ~ spl27_8 ),
inference(forward_subsumption_resolution,[],[f2026,f688]) ).
fof(f2033,plain,
( ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| spl27_2
| ~ spl27_7
| ~ spl27_8 ),
inference(forward_subsumption_resolution,[],[f2032,f684]) ).
fof(f2034,plain,
( ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| spl27_2
| ~ spl27_6
| ~ spl27_7
| ~ spl27_8 ),
inference(forward_subsumption_resolution,[],[f2033,f680]) ).
fof(f2035,plain,
( ~ m1_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_7
| ~ spl27_8 ),
inference(forward_subsumption_resolution,[],[f2034,f676]) ).
fof(f2036,plain,
( $false
| spl27_2
| ~ spl27_4
| ~ spl27_5
| ~ spl27_6
| ~ spl27_7
| ~ spl27_8 ),
inference(forward_subsumption_resolution,[],[f2035,f672]) ).
fof(f2037,plain,
( spl27_2
| ~ spl27_4
| ~ spl27_5
| ~ spl27_6
| ~ spl27_7
| ~ spl27_8 ),
inference(avatar_contradiction_clause,[],[f2036]) ).
fof(f2098,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m1_subset_1(u1_struct_0(sK3),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_1 ),
inference(superposition,[],[f612,f630]) ).
fof(f2102,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m1_subset_1(u1_struct_0(sK3),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2 ),
inference(superposition,[],[f616,f630]) ).
fof(f2589,plain,
( ~ m1_pre_topc(sK3,sK2)
| ~ l1_pre_topc(sK2)
| spl27_14 ),
inference(resolution,[],[f392,f798]) ).
fof(f2590,plain,
( ~ m1_pre_topc(sK3,sK2)
| spl27_14 ),
inference(forward_subsumption_resolution,[],[f2589,f343]) ).
fof(f2591,plain,
( ~ m2_tsp_1(sK3,sK2)
| ~ l1_pre_topc(sK2)
| spl27_14 ),
inference(resolution,[],[f2590,f382]) ).
fof(f2592,plain,
( ~ l1_pre_topc(sK2)
| spl27_14 ),
inference(forward_subsumption_resolution,[],[f2591,f346]) ).
fof(f2593,plain,
( $false
| spl27_14 ),
inference(forward_subsumption_resolution,[],[f2592,f343]) ).
fof(f2594,plain,
spl27_14,
inference(avatar_contradiction_clause,[],[f2593]) ).
fof(f2613,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m1_subset_1(u1_struct_0(sK3),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_1 ),
inference(forward_subsumption_resolution,[],[f2098,f350]) ).
fof(f2615,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m1_subset_1(u1_struct_0(sK3),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2 ),
inference(forward_subsumption_resolution,[],[f2102,f349]) ).
fof(f2635,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_1
| ~ spl27_14 ),
inference(forward_subsumption_resolution,[],[f2613,f797]) ).
fof(f2637,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_14 ),
inference(forward_subsumption_resolution,[],[f2615,f797]) ).
fof(f2657,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_1
| ~ spl27_6
| ~ spl27_14 ),
inference(forward_subsumption_resolution,[],[f2635,f680]) ).
fof(f2659,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_6
| ~ spl27_14 ),
inference(forward_subsumption_resolution,[],[f2637,f680]) ).
fof(f2679,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_1
| ~ spl27_5
| ~ spl27_6
| ~ spl27_14 ),
inference(forward_subsumption_resolution,[],[f2657,f676]) ).
fof(f2681,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_14 ),
inference(forward_subsumption_resolution,[],[f2659,f676]) ).
fof(f2701,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_1
| ~ spl27_5
| ~ spl27_6
| ~ spl27_13
| ~ spl27_14 ),
inference(forward_subsumption_resolution,[],[f2679,f793]) ).
fof(f2703,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_13
| ~ spl27_14 ),
inference(forward_subsumption_resolution,[],[f2681,f793]) ).
fof(f2723,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)),k1_zfmisc_1(u1_struct_0(sK3)))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_1
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14 ),
inference(forward_subsumption_resolution,[],[f2701,f789]) ).
fof(f2725,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k1_zfmisc_1(u1_struct_0(sK3)))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14 ),
inference(forward_subsumption_resolution,[],[f2703,f789]) ).
fof(f2745,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_1
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14 ),
inference(forward_subsumption_resolution,[],[f2723,f348]) ).
fof(f2747,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14 ),
inference(forward_subsumption_resolution,[],[f2725,f348]) ).
fof(f2767,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_1
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14 ),
inference(forward_subsumption_resolution,[],[f2745,f347]) ).
fof(f2769,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14 ),
inference(forward_subsumption_resolution,[],[f2747,f347]) ).
fof(f2789,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)),k1_zfmisc_1(u1_struct_0(sK3)))
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_1
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14 ),
inference(forward_subsumption_resolution,[],[f2767,f346]) ).
fof(f2791,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k1_zfmisc_1(u1_struct_0(sK3)))
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14 ),
inference(forward_subsumption_resolution,[],[f2769,f346]) ).
fof(f2811,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_1
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14 ),
inference(forward_subsumption_resolution,[],[f2789,f345]) ).
fof(f2813,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14 ),
inference(forward_subsumption_resolution,[],[f2791,f345]) ).
fof(f2833,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l1_pre_topc(sK2)
| ~ spl27_1
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14 ),
inference(forward_subsumption_resolution,[],[f2811,f344]) ).
fof(f2835,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14 ),
inference(forward_subsumption_resolution,[],[f2813,f344]) ).
fof(f2854,definition,
( spl27_20
<=> m1_subset_1(k4_subset_1(u1_struct_0(sK2),sK4,sK5),k1_zfmisc_1(u1_struct_0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl27_20])],[avatar_definition]) ).
fof(f2855,plain,
( m1_subset_1(k4_subset_1(u1_struct_0(sK2),sK4,sK5),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ spl27_20 ),
inference(avatar_component_clause,[],[f2854]) ).
fof(f2856,plain,
( ~ m1_subset_1(k4_subset_1(u1_struct_0(sK2),sK4,sK5),k1_zfmisc_1(u1_struct_0(sK2)))
| spl27_20 ),
inference(avatar_component_clause,[],[f2854]) ).
fof(f2863,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ spl27_1
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14 ),
inference(forward_subsumption_resolution,[],[f2833,f343]) ).
fof(f2865,plain,
( m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14 ),
inference(forward_subsumption_resolution,[],[f2835,f343]) ).
fof(f2879,plain,
( spl27_16
| ~ spl27_1
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14 ),
inference(avatar_split_clause,[],[f2863,f796,f792,f788,f679,f675,f611,f805]) ).
fof(f2887,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k4_subset_1(u1_struct_0(sK3),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)))
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m1_subset_1(u1_struct_0(sK3),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| spl27_15 ),
inference(superposition,[],[f802,f630]) ).
fof(f2898,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k4_subset_1(u1_struct_0(sK3),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)))
| ~ m1_subset_1(u1_struct_0(sK3),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| spl27_15 ),
inference(forward_subsumption_resolution,[],[f2887,f349]) ).
fof(f2903,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k4_subset_1(u1_struct_0(sK3),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)))
| ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_14
| spl27_15 ),
inference(forward_subsumption_resolution,[],[f2898,f797]) ).
fof(f2906,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k4_subset_1(u1_struct_0(sK3),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_6
| ~ spl27_14
| spl27_15 ),
inference(forward_subsumption_resolution,[],[f2903,f680]) ).
fof(f2908,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k4_subset_1(u1_struct_0(sK3),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_5
| ~ spl27_6
| ~ spl27_14
| spl27_15 ),
inference(forward_subsumption_resolution,[],[f2906,f676]) ).
fof(f2910,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k4_subset_1(u1_struct_0(sK3),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)))
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_5
| ~ spl27_6
| ~ spl27_13
| ~ spl27_14
| spl27_15 ),
inference(forward_subsumption_resolution,[],[f2908,f793]) ).
fof(f2912,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k4_subset_1(u1_struct_0(sK3),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15 ),
inference(forward_subsumption_resolution,[],[f2910,f789]) ).
fof(f2914,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k4_subset_1(u1_struct_0(sK3),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)))
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15 ),
inference(forward_subsumption_resolution,[],[f2912,f348]) ).
fof(f2916,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k4_subset_1(u1_struct_0(sK3),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)))
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15 ),
inference(forward_subsumption_resolution,[],[f2914,f347]) ).
fof(f2918,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k4_subset_1(u1_struct_0(sK3),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)))
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15 ),
inference(forward_subsumption_resolution,[],[f2916,f346]) ).
fof(f2920,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k4_subset_1(u1_struct_0(sK3),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)))
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15 ),
inference(forward_subsumption_resolution,[],[f2918,f345]) ).
fof(f2922,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k4_subset_1(u1_struct_0(sK3),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)))
| ~ l1_pre_topc(sK2)
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15 ),
inference(forward_subsumption_resolution,[],[f2920,f344]) ).
fof(f2924,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k4_subset_1(u1_struct_0(sK3),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)))
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15 ),
inference(forward_subsumption_resolution,[],[f2922,f343]) ).
fof(f2966,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k2_xboole_0(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)))
| ~ m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15 ),
inference(superposition,[],[f2924,f365]) ).
fof(f2967,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k2_xboole_0(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)))
| ~ m1_subset_1(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)),k1_zfmisc_1(u1_struct_0(sK3)))
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15 ),
inference(forward_subsumption_resolution,[],[f2966,f2865]) ).
fof(f2969,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k2_xboole_0(k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK4)),k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,sK5)))
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15
| ~ spl27_16 ),
inference(forward_subsumption_resolution,[],[f2967,f806]) ).
fof(f2971,plain,
( k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_subset_1(u1_struct_0(sK2),sK4,sK5)) != k3_xboole_0(u1_struct_0(sK3),k2_xboole_0(k3_tex_4(sK2,sK4),k3_tex_4(sK2,sK5)))
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15
| ~ spl27_16 ),
inference(forward_demodulation,[],[f2969,f405]) ).
fof(f2975,plain,
( ~ m1_subset_1(k2_xboole_0(sK5,sK4),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2)))
| spl27_20 ),
inference(superposition,[],[f2856,f640]) ).
fof(f2978,plain,
( ~ m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2)))
| spl27_20 ),
inference(forward_subsumption_resolution,[],[f2975,f861]) ).
fof(f2981,plain,
( ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2)))
| spl27_20 ),
inference(forward_subsumption_resolution,[],[f2978,f350]) ).
fof(f2986,plain,
( $false
| spl27_20 ),
inference(forward_subsumption_resolution,[],[f2981,f349]) ).
fof(f2987,plain,
spl27_20,
inference(avatar_contradiction_clause,[],[f2986]) ).
fof(f2992,plain,
( k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,k4_subset_1(u1_struct_0(sK2),sK4,sK5))) != k3_xboole_0(u1_struct_0(sK3),k2_xboole_0(k3_tex_4(sK2,sK4),k3_tex_4(sK2,sK5)))
| ~ m1_subset_1(k4_subset_1(u1_struct_0(sK2),sK4,sK5),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m1_subset_1(u1_struct_0(sK3),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15
| ~ spl27_16 ),
inference(superposition,[],[f2971,f630]) ).
fof(f2995,plain,
( k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,k4_subset_1(u1_struct_0(sK2),sK4,sK5))) != k3_xboole_0(u1_struct_0(sK3),k2_xboole_0(k3_tex_4(sK2,sK4),k3_tex_4(sK2,sK5)))
| ~ m1_subset_1(u1_struct_0(sK3),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15
| ~ spl27_16
| ~ spl27_20 ),
inference(forward_subsumption_resolution,[],[f2992,f2855]) ).
fof(f3001,plain,
( k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,k4_subset_1(u1_struct_0(sK2),sK4,sK5))) != k3_xboole_0(u1_struct_0(sK3),k2_xboole_0(k3_tex_4(sK2,sK4),k3_tex_4(sK2,sK5)))
| ~ v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15
| ~ spl27_16
| ~ spl27_20 ),
inference(forward_subsumption_resolution,[],[f2995,f797]) ).
fof(f3007,plain,
( k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,k4_subset_1(u1_struct_0(sK2),sK4,sK5))) != k3_xboole_0(u1_struct_0(sK3),k2_xboole_0(k3_tex_4(sK2,sK4),k3_tex_4(sK2,sK5)))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15
| ~ spl27_16
| ~ spl27_20 ),
inference(forward_subsumption_resolution,[],[f3001,f680]) ).
fof(f3012,plain,
( k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,k4_subset_1(u1_struct_0(sK2),sK4,sK5))) != k3_xboole_0(u1_struct_0(sK3),k2_xboole_0(k3_tex_4(sK2,sK4),k3_tex_4(sK2,sK5)))
| ~ v5_pre_topc(k4_tsp_2(sK2,sK3),sK2,sK3)
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15
| ~ spl27_16
| ~ spl27_20 ),
inference(forward_subsumption_resolution,[],[f3007,f676]) ).
fof(f3016,plain,
( k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,k4_subset_1(u1_struct_0(sK2),sK4,sK5))) != k3_xboole_0(u1_struct_0(sK3),k2_xboole_0(k3_tex_4(sK2,sK4),k3_tex_4(sK2,sK5)))
| ~ m2_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15
| ~ spl27_16
| ~ spl27_20 ),
inference(forward_subsumption_resolution,[],[f3012,f793]) ).
fof(f3019,plain,
( k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,k4_subset_1(u1_struct_0(sK2),sK4,sK5))) != k3_xboole_0(u1_struct_0(sK3),k2_xboole_0(k3_tex_4(sK2,sK4),k3_tex_4(sK2,sK5)))
| v3_struct_0(sK3)
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15
| ~ spl27_16
| ~ spl27_20 ),
inference(forward_subsumption_resolution,[],[f3016,f789]) ).
fof(f3021,plain,
( k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,k4_subset_1(u1_struct_0(sK2),sK4,sK5))) != k3_xboole_0(u1_struct_0(sK3),k2_xboole_0(k3_tex_4(sK2,sK4),k3_tex_4(sK2,sK5)))
| ~ v2_tsp_2(sK3,sK2)
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15
| ~ spl27_16
| ~ spl27_20 ),
inference(forward_subsumption_resolution,[],[f3019,f348]) ).
fof(f3023,plain,
( k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,k4_subset_1(u1_struct_0(sK2),sK4,sK5))) != k3_xboole_0(u1_struct_0(sK3),k2_xboole_0(k3_tex_4(sK2,sK4),k3_tex_4(sK2,sK5)))
| ~ m2_tsp_1(sK3,sK2)
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15
| ~ spl27_16
| ~ spl27_20 ),
inference(forward_subsumption_resolution,[],[f3021,f347]) ).
fof(f3025,plain,
( k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,k4_subset_1(u1_struct_0(sK2),sK4,sK5))) != k3_xboole_0(u1_struct_0(sK3),k2_xboole_0(k3_tex_4(sK2,sK4),k3_tex_4(sK2,sK5)))
| v3_struct_0(sK2)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15
| ~ spl27_16
| ~ spl27_20 ),
inference(forward_subsumption_resolution,[],[f3023,f346]) ).
fof(f3027,plain,
( k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,k4_subset_1(u1_struct_0(sK2),sK4,sK5))) != k3_xboole_0(u1_struct_0(sK3),k2_xboole_0(k3_tex_4(sK2,sK4),k3_tex_4(sK2,sK5)))
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15
| ~ spl27_16
| ~ spl27_20 ),
inference(forward_subsumption_resolution,[],[f3025,f345]) ).
fof(f3029,plain,
( k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,k4_subset_1(u1_struct_0(sK2),sK4,sK5))) != k3_xboole_0(u1_struct_0(sK3),k2_xboole_0(k3_tex_4(sK2,sK4),k3_tex_4(sK2,sK5)))
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15
| ~ spl27_16
| ~ spl27_20 ),
inference(forward_subsumption_resolution,[],[f3027,f344]) ).
fof(f3031,plain,
( k3_xboole_0(u1_struct_0(sK3),k3_tex_4(sK2,k4_subset_1(u1_struct_0(sK2),sK4,sK5))) != k3_xboole_0(u1_struct_0(sK3),k2_xboole_0(k3_tex_4(sK2,sK4),k3_tex_4(sK2,sK5)))
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15
| ~ spl27_16
| ~ spl27_20 ),
inference(forward_subsumption_resolution,[],[f3029,f343]) ).
fof(f3037,plain,
( k3_xboole_0(u1_struct_0(sK3),k2_xboole_0(k3_tex_4(sK2,sK4),k3_tex_4(sK2,sK5))) != k3_xboole_0(u1_struct_0(sK3),k2_xboole_0(k3_tex_4(sK2,sK4),k3_tex_4(sK2,sK5)))
| ~ m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2)))
| v3_struct_0(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15
| ~ spl27_16
| ~ spl27_20 ),
inference(superposition,[],[f3031,f624]) ).
fof(f3040,plain,
( ~ m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2)))
| v3_struct_0(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15
| ~ spl27_16
| ~ spl27_20 ),
inference(trivial_inequality_removal,[],[f3037]) ).
fof(f3041,plain,
( ~ m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2)))
| v3_struct_0(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15
| ~ spl27_16
| ~ spl27_20 ),
inference(forward_subsumption_resolution,[],[f3040,f350]) ).
fof(f3045,plain,
( v3_struct_0(sK2)
| ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15
| ~ spl27_16
| ~ spl27_20 ),
inference(forward_subsumption_resolution,[],[f3041,f349]) ).
fof(f3049,plain,
( ~ l1_pre_topc(sK2)
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15
| ~ spl27_16
| ~ spl27_20 ),
inference(forward_subsumption_resolution,[],[f3045,f345]) ).
fof(f3052,plain,
( $false
| ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15
| ~ spl27_16
| ~ spl27_20 ),
inference(forward_subsumption_resolution,[],[f3049,f343]) ).
fof(f3053,plain,
( ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15
| ~ spl27_16
| ~ spl27_20 ),
inference(avatar_contradiction_clause,[],[f3052]) ).
cnf(s5,plain,
( ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| ~ spl27_15 ),
inference(sat_conversion,[],[f803]) ).
cnf(s8,plain,
spl27_5,
inference(sat_conversion,[],[f1765]) ).
cnf(s9,plain,
spl27_6,
inference(sat_conversion,[],[f1775]) ).
cnf(s10,plain,
spl27_12,
inference(sat_conversion,[],[f1785]) ).
cnf(s11,plain,
spl27_13,
inference(sat_conversion,[],[f1795]) ).
cnf(s12,plain,
( spl27_4
| ~ spl27_12 ),
inference(sat_conversion,[],[f1979]) ).
cnf(s13,plain,
spl27_7,
inference(sat_conversion,[],[f1982]) ).
cnf(s14,plain,
spl27_8,
inference(sat_conversion,[],[f1985]) ).
cnf(s15,plain,
( spl27_1
| ~ spl27_4
| ~ spl27_5
| ~ spl27_6
| ~ spl27_7
| ~ spl27_8 ),
inference(sat_conversion,[],[f1991]) ).
cnf(s18,plain,
( spl27_2
| ~ spl27_4
| ~ spl27_5
| ~ spl27_6
| ~ spl27_7
| ~ spl27_8 ),
inference(sat_conversion,[],[f2037]) ).
cnf(s20,plain,
spl27_14,
inference(sat_conversion,[],[f2594]) ).
cnf(s23,plain,
( ~ spl27_1
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_16 ),
inference(sat_conversion,[],[f2879]) ).
cnf(s27,plain,
spl27_20,
inference(sat_conversion,[],[f2987]) ).
cnf(s28,plain,
( ~ spl27_2
| ~ spl27_5
| ~ spl27_6
| ~ spl27_12
| ~ spl27_13
| ~ spl27_14
| spl27_15
| ~ spl27_16
| ~ spl27_20 ),
inference(sat_conversion,[],[f3053]) ).
cnf(s31,plain,
spl27_4,
inference(rat,[],[s12,s10]) ).
cnf(s32,plain,
spl27_2,
inference(rat,[],[s18,s14,s13,s9,s31,s8]) ).
cnf(s33,plain,
spl27_1,
inference(rat,[],[s15,s14,s13,s9,s31,s8]) ).
cnf(s34,plain,
spl27_16,
inference(rat,[],[s23,s8,s20,s11,s10,s9,s33]) ).
cnf(s35,plain,
spl27_15,
inference(rat,[],[s28,s27,s32,s8,s20,s11,s10,s9,s34]) ).
cnf(s37,plain,
$false,
inference(rat,[],[s5,s35,s20,s11,s10,s9,s8]) ).
fof(f3056,plain,
$false,
inference(avatar_sat_refutation,[],[s37]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : TOP038+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n010.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 19:00:33 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/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
% 13.35/2.70 % (2211849)Detected formulas, will run a generic FOF schedule.
% 13.35/2.70 % (2211856)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=2815635995:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 13.35/2.70 % (2211855)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=2326787376:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 13.35/2.70 % (2211859)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1178196255:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 13.35/2.70 % (2211854)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=2263669854:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 13.35/2.70 % (2211860)dis-21_1_sil=8000:lcm=predicate:random_seed=760416839:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 13.35/2.70 % (2211857)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=922869227:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 13.35/2.70 % (2211858)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=727876060:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 13.35/2.70 % (2211857)Refutation not found, incomplete strategy
% 13.35/2.70 % (2211857)------------------------------
% 13.35/2.70 % (2211857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.35/2.70 % (2211857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.35/2.70 % (2211857)CaDiCaL version: 2.1.3
% 13.35/2.70 % (2211857)Termination reason: Refutation not found, incomplete strategy
% 13.35/2.70 % (2211857)Time elapsed: 0.003 s
% 13.35/2.70 % (2211857)Peak memory usage: 88 MB
% 13.35/2.70 % (2211857)Instructions burned: 2 (million)
% 13.35/2.70 % (2211858)Instruction limit reached!
% 13.35/2.70 % (2211858)------------------------------
% 13.35/2.70 % (2211858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.35/2.70 % (2211858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.35/2.70 % (2211858)CaDiCaL version: 2.1.3
% 13.35/2.70 % (2211858)Termination reason: Instruction limit
% 13.35/2.70 % (2211858)Termination phase: Saturation
% 13.35/2.70 % (2211858)Time elapsed: 0.065 s
% 13.35/2.70 % (2211858)Peak memory usage: 88 MB
% 13.35/2.70 % (2211858)Instructions burned: 120 (million)
% 13.35/2.70 % (2211860)Instruction limit reached!
% 13.35/2.70 % (2211860)------------------------------
% 13.35/2.70 % (2211860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.35/2.70 % (2211860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.35/2.70 % (2211860)CaDiCaL version: 2.1.3
% 13.35/2.70 % (2211860)Termination reason: Instruction limit
% 13.35/2.70 % (2211860)Termination phase: Saturation
% 13.35/2.70 % (2211860)Time elapsed: 0.076 s
% 13.35/2.70 % (2211860)Peak memory usage: 90 MB
% 13.35/2.70 % (2211860)Instructions burned: 129 (million)
% 13.35/2.70 % (2211859)Instruction limit reached!
% 13.35/2.70 % (2211859)------------------------------
% 13.35/2.70 % (2211859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.35/2.70 % (2211859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.35/2.70 % (2211859)CaDiCaL version: 2.1.3
% 13.35/2.70 % (2211859)Termination reason: Instruction limit
% 13.35/2.70 % (2211859)Termination phase: Saturation
% 13.35/2.70 % (2211859)Time elapsed: 0.089 s
% 13.35/2.70 % (2211859)Peak memory usage: 89 MB
% 13.35/2.70 % (2211859)Instructions burned: 140 (million)
% 13.35/2.70 % (2211868)lrs+10_1_sil=8000:sp=occurrence:random_seed=3725092453:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 13.35/2.70 % (2211870)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1700109547:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 13.35/2.70 % (2211869)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1180736611:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 13.35/2.70 % (2211857)------------------------------
% 13.35/2.70 % (2211857)------------------------------
% 13.35/2.70 % (2211869)Instruction limit reached!
% 13.35/2.70 % (2211869)------------------------------
% 13.35/2.70 % (2211869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.07/3.04 % (2211869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.07/3.04 % (2211869)CaDiCaL version: 2.1.3
% 9.07/3.04 % (2211869)Termination reason: Instruction limit
% 9.07/3.04 % (2211869)Termination phase: Saturation
% 9.07/3.04 % (2211869)Time elapsed: 0.076 s
% 9.07/3.04 % (2211869)Peak memory usage: 90 MB
% 9.07/3.04 % (2211869)Instructions burned: 159 (million)
% 9.07/3.04 % (2211868)Instruction limit reached!
% 9.07/3.04 % (2211868)------------------------------
% 9.07/3.04 % (2211868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.07/3.04 % (2211868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.07/3.04 % (2211868)CaDiCaL version: 2.1.3
% 9.07/3.04 % (2211868)Termination reason: Instruction limit
% 9.07/3.04 % (2211868)Termination phase: Saturation
% 9.07/3.04 % (2211868)Time elapsed: 0.160 s
% 9.07/3.04 % (2211868)Peak memory usage: 92 MB
% 9.07/3.04 % (2211868)Instructions burned: 285 (million)
% 9.07/3.04 % (2211874)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=540887802:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 9.07/3.04 % (2211870)Instruction limit reached!
% 9.07/3.04 % (2211870)------------------------------
% 9.07/3.04 % (2211870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.07/3.04 % (2211870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.07/3.04 % (2211870)CaDiCaL version: 2.1.3
% 9.07/3.04 % (2211870)Termination reason: Instruction limit
% 9.07/3.04 % (2211870)Termination phase: Saturation
% 9.07/3.04 % (2211870)Time elapsed: 0.192 s
% 9.07/3.04 % (2211870)Peak memory usage: 91 MB
% 9.07/3.04 % (2211870)Instructions burned: 325 (million)
% 9.07/3.04 % (2211875)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2533799008:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 9.07/3.04 % (2211875)Refutation not found, incomplete strategy
% 9.07/3.04 % (2211875)------------------------------
% 9.07/3.04 % (2211875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.07/3.04 % (2211875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.07/3.04 % (2211875)CaDiCaL version: 2.1.3
% 9.07/3.04 % (2211875)Termination reason: Refutation not found, incomplete strategy
% 9.07/3.04 % (2211875)Time elapsed: 0.011 s
% 9.07/3.04 % (2211875)Peak memory usage: 89 MB
% 9.07/3.04 % (2211875)Instructions burned: 17 (million)
% 9.07/3.04 % (2211876)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1794491453:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 9.07/3.04 % (2211874)Instruction limit reached!
% 9.07/3.04 % (2211874)------------------------------
% 9.07/3.04 % (2211874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.07/3.04 % (2211874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.07/3.04 % (2211874)CaDiCaL version: 2.1.3
% 9.07/3.04 % (2211874)Termination reason: Instruction limit
% 9.07/3.04 % (2211874)Termination phase: Saturation
% 9.07/3.04 % (2211874)Time elapsed: 0.131 s
% 9.07/3.04 % (2211874)Peak memory usage: 93 MB
% 9.07/3.04 % (2211874)Instructions burned: 250 (million)
% 9.07/3.04 % (2211878)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=575671121:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 9.07/3.04 % (2211878)Instruction limit reached!
% 9.07/3.04 % (2211878)------------------------------
% 9.07/3.04 % (2211878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.07/3.04 % (2211878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.07/3.04 % (2211878)CaDiCaL version: 2.1.3
% 9.07/3.04 % (2211878)Termination reason: Instruction limit
% 9.07/3.04 % (2211878)Termination phase: Saturation
% 9.07/3.04 % (2211878)Time elapsed: 0.071 s
% 9.07/3.04 % (2211878)Peak memory usage: 91 MB
% 9.07/3.04 % (2211878)Instructions burned: 114 (million)
% 9.07/3.04 % (2211875)------------------------------
% 9.07/3.04 % (2211875)------------------------------
% 9.07/3.04 % (2211881)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2245625792:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 9.07/3.04 % (2211881)Instruction limit reached!
% 9.07/3.04 % (2211881)------------------------------
% 9.07/3.04 % (2211881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.07/3.04 % (2211881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.07/3.04 % (2211881)CaDiCaL version: 2.1.3
% 9.07/3.04 % (2211881)Termination reason: Instruction limit
% 9.07/3.04 % (2211881)Termination phase: Saturation
% 9.07/3.04 % (2211881)Time elapsed: 0.065 s
% 9.07/3.04 % (2211881)Peak memory usage: 89 MB
% 9.07/3.04 % (2211881)Instructions burned: 127 (million)
% 9.07/3.04 % (2211883)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=704425439:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 9.07/3.04 % (2211885)lrs+10_1_sil=8000:sp=occurrence:random_seed=994088038:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 9.07/3.04 % (2211883)Instruction limit reached!
% 9.07/3.04 % (2211883)------------------------------
% 9.07/3.04 % (2211883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.07/3.04 % (2211883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.07/3.04 % (2211883)CaDiCaL version: 2.1.3
% 9.07/3.04 % (2211883)Termination reason: Instruction limit
% 9.07/3.04 % (2211883)Termination phase: Saturation
% 9.07/3.04 % (2211883)Time elapsed: 0.063 s
% 9.07/3.04 % (2211883)Peak memory usage: 89 MB
% 9.07/3.04 % (2211883)Instructions burned: 114 (million)
% 9.07/3.04 % (2211886)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=84422556:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 9.07/3.04 % (2211886)Refutation not found, incomplete strategy
% 9.07/3.04 % (2211886)------------------------------
% 9.07/3.04 % (2211886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.07/3.04 % (2211886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.07/3.04 % (2211886)CaDiCaL version: 2.1.3
% 9.07/3.04 % (2211886)Termination reason: Refutation not found, incomplete strategy
% 9.07/3.04 % (2211886)Time elapsed: 0.013 s
% 9.07/3.04 % (2211886)Peak memory usage: 89 MB
% 9.07/3.04 % (2211886)Instructions burned: 20 (million)
% 9.07/3.04 % (2211889)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1959781488:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 9.07/3.04 % (2211886)------------------------------
% 9.07/3.04 % (2211886)------------------------------
% 9.07/3.04 % (2211885)Instruction limit reached!
% 9.07/3.04 % (2211885)------------------------------
% 9.07/3.04 % (2211885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.07/3.04 % (2211885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.07/3.04 % (2211885)CaDiCaL version: 2.1.3
% 9.07/3.04 % (2211885)Termination reason: Instruction limit
% 9.07/3.04 % (2211885)Termination phase: Saturation
% 9.07/3.04 % (2211885)Time elapsed: 0.469 s
% 9.07/3.04 % (2211885)Peak memory usage: 100 MB
% 9.07/3.04 % (2211885)Instructions burned: 908 (million)
% 9.07/3.04 % (2211892)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1916454282:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 9.07/3.04 % (2211892)Instruction limit reached!
% 9.07/3.04 % (2211892)------------------------------
% 9.07/3.04 % (2211892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.07/3.04 % (2211892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.07/3.04 % (2211892)CaDiCaL version: 2.1.3
% 9.07/3.04 % (2211892)Termination reason: Instruction limit
% 9.07/3.04 % (2211892)Termination phase: Saturation
% 9.07/3.04 % (2211892)Time elapsed: 0.070 s
% 9.07/3.04 % (2211892)Peak memory usage: 91 MB
% 9.07/3.04 % (2211892)Instructions burned: 136 (million)
% 9.07/3.04 % (2211893)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2635694977:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 9.07/3.04 % (2211895)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1844885066:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi)
% 9.07/3.04 % (2211893)Instruction limit reached!
% 9.07/3.04 % (2211893)------------------------------
% 9.07/3.04 % (2211893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.07/3.04 % (2211893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.07/3.04 % (2211893)CaDiCaL version: 2.1.3
% 9.07/3.04 % (2211893)Termination reason: Instruction limit
% 9.07/3.04 % (2211893)Termination phase: Saturation
% 9.07/3.04 % (2211893)Time elapsed: 0.342 s
% 9.07/3.04 % (2211893)Peak memory usage: 96 MB
% 9.07/3.04 % (2211893)Instructions burned: 593 (million)
% 9.07/3.04 % (2211889)First to succeed.
% 9.07/3.04 % (2211889)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2211849"
% 9.07/3.04 % (2211876)Instruction limit reached!
% 9.07/3.04 % (2211876)------------------------------
% 9.07/3.04 % (2211876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.07/3.04 % (2211876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.07/3.04 % (2211876)CaDiCaL version: 2.1.3
% 9.07/3.04 % (2211876)Termination reason: Instruction limit
% 9.07/3.04 % (2211876)Termination phase: Saturation
% 9.07/3.04 % (2211876)Time elapsed: 1.476 s
% 9.07/3.04 % (2211876)Peak memory usage: 143 MB
% 9.07/3.04 % (2211876)Instructions burned: 2350 (million)
% 9.07/3.04 % (2211898)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=3977231663:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/125Mi)
% 9.07/3.04 % (2211898)Instruction limit reached!
% 9.07/3.04 % (2211898)------------------------------
% 9.07/3.04 % (2211898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.07/3.04 % (2211898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.07/3.04 % (2211898)CaDiCaL version: 2.1.3
% 9.07/3.04 % (2211898)Termination reason: Instruction limit
% 9.07/3.04 % (2211898)Termination phase: Saturation
% 9.07/3.04 % (2211898)Time elapsed: 0.079 s
% 9.07/3.04 % (2211898)Peak memory usage: 92 MB
% 9.07/3.04 % (2211898)Instructions burned: 125 (million)
% 9.07/3.04 % (2211856)Also succeeded, but the first one will report.
% 9.07/3.04 % (2211889)Refutation found. Thanks to Tanya!
% 9.07/3.04 % SZS status Theorem for theBenchmark
% 9.07/3.04 % SZS output start Proof for theBenchmark
% See solution above
% 17.33/3.23 % (2211889)------------------------------
% 17.33/3.23 % (2211889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.33/3.23 % (2211889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.33/3.23 % (2211889)CaDiCaL version: 2.1.3
% 17.33/3.23 % (2211889)Termination reason: Refutation
% 17.33/3.23 % (2211889)Time elapsed: 0.855 s
% 17.33/3.23 % (2211889)Peak memory usage: 133 MB
% 17.33/3.23 % (2211889)Instructions burned: 1336 (million)
% 17.33/3.23 % (2211889)------------------------------
% 17.33/3.23 % (2211889)------------------------------
% 17.33/3.23 % (2211849)Success in time 2.365 s
% 17.33/3.23 % Vampire exiting
%------------------------------------------------------------------------------