%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : TOP042+2 : 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 : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 02:34:04 PM UTC 2026
% Result : Theorem 12.86s 2.66s
% Output : Refutation 13.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 23
% Syntax : Number of formulae : 219 ( 45 unt; 8 def)
% Number of atoms : 958 ( 134 equ)
% Maximal formula atoms : 20 ( 4 avg)
% Number of connectives : 1316 ( 577 ~; 621 |; 79 &)
% ( 8 <=>; 31 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 18 ( 16 usr; 4 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 8 con; 0-4 aty)
% Number of variables : 258 ( 0 sgn 246 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f117,axiom,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k3_xboole_0(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t48_xboole_1) ).
fof(f435,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) = k5_subset_1(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k5_subset_1) ).
fof(f437,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(f2190,axiom,
! [X0] :
( l1_struct_0(X0)
=> k2_pre_topc(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_pre_topc) ).
fof(f2245,axiom,
! [X0] :
( l1_pre_topc(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f2611,axiom,
! [X0] : u1_pre_topc(k2_pcomps_1(X0)) = k1_pcomps_1(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_pcomps_1) ).
fof(f2652,axiom,
! [X0] : k1_pcomps_1(X0) = k1_zfmisc_1(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k1_pcomps_1) ).
fof(f3438,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v4_pre_topc(X1,X0)
=> k3_tex_4(X0,X1) = X1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t62_tex_4) ).
fof(f3532,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m2_tsp_1(X1,X0)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ~ ( v4_pre_topc(X2,X0)
& ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
=> ~ ( v4_pre_topc(X3,X1)
& X3 = k3_xboole_0(X2,u1_struct_0(X1)) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_tsp_1) ).
fof(f3565,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(f3567,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(f3575,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(f3595,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m2_tsp_1(X1,X0)
=> m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l19_tsp_2) ).
fof(f3633,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(f3640,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v4_pre_topc(X2,X0)
=> v4_pre_topc(k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t35_tsp_2) ).
fof(f3641,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v4_pre_topc(X2,X0)
=> v4_pre_topc(k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),X1) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f3640]) ).
fof(f4116,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k5_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f435]) ).
fof(f4117,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k5_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f4116]) ).
fof(f4120,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,[],[f437]) ).
fof(f4121,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,[],[f4120]) ).
fof(f6150,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f2190]) ).
fof(f6203,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f2245]) ).
fof(f8211,plain,
! [X0] :
( ! [X1] :
( k3_tex_4(X0,X1) = X1
| ~ v4_pre_topc(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f3438]) ).
fof(f8212,plain,
! [X0] :
( ! [X1] :
( k3_tex_4(X0,X1) = X1
| ~ v4_pre_topc(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f8211]) ).
fof(f8384,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ~ v4_pre_topc(X2,X0)
| ? [X3] :
( v4_pre_topc(X3,X1)
& X3 = k3_xboole_0(X2,u1_struct_0(X1))
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m2_tsp_1(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f3532]) ).
fof(f8385,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ~ v4_pre_topc(X2,X0)
| ? [X3] :
( v4_pre_topc(X3,X1)
& X3 = k3_xboole_0(X2,u1_struct_0(X1))
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m2_tsp_1(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f8384]) ).
fof(f8447,plain,
! [X0] :
( ! [X1] :
( l1_pre_topc(X1)
| ~ m2_tsp_1(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f3565]) ).
fof(f8449,plain,
! [X0] :
( ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f3567]) ).
fof(f8464,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,[],[f3575]) ).
fof(f8465,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,[],[f8464]) ).
fof(f8504,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f3595]) ).
fof(f8505,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f8504]) ).
fof(f8580,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,[],[f3633]) ).
fof(f8581,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,[],[f8580]) ).
fof(f8594,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ v4_pre_topc(k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),X1)
& v4_pre_topc(X2,X0)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f3641]) ).
fof(f8595,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ v4_pre_topc(k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),X1)
& v4_pre_topc(X2,X0)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(flattening,[],[f8594]) ).
fof(f11046,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ~ v4_pre_topc(X2,X0)
| ( v4_pre_topc(sK1319(X1,X2),X1)
& k3_xboole_0(X2,u1_struct_0(X1)) = sK1319(X1,X2)
& m1_subset_1(sK1319(X1,X2),k1_zfmisc_1(u1_struct_0(X1))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m2_tsp_1(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1319]),skolemize(X3,sK1319(X1,X2))],[f8385]) ).
fof(f11118,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,[],[f8449]) ).
fof(f11176,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,[],[f8581]) ).
fof(f11177,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,[],[f11176]) ).
fof(f11178,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k4_tsp_2(X0,X1)
| ( k5_subset_1(u1_struct_0(X0),sK1385(X0,X1,X2),k3_tex_4(X0,sK1386(X0,X1,X2))) != k4_pre_topc(X0,X1,X2,sK1386(X0,X1,X2))
& m1_subset_1(sK1386(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)))
& u1_struct_0(X1) = sK1385(X0,X1,X2)
& m1_subset_1(sK1385(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,[sK1385,sK1386]),skolemize(X3,sK1385(X0,X1,X2)),skolemize(X4,sK1386(X0,X1,X2))],[f11177]) ).
fof(f11179,plain,
( ~ v4_pre_topc(k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),sK1389),sK1388)
& v4_pre_topc(sK1389,sK1387)
& m1_subset_1(sK1389,k1_zfmisc_1(u1_struct_0(sK1387)))
& ~ v3_struct_0(sK1388)
& v2_tsp_2(sK1388,sK1387)
& m2_tsp_1(sK1388,sK1387)
& ~ v3_struct_0(sK1387)
& v2_pre_topc(sK1387)
& l1_pre_topc(sK1387) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1387,sK1388,sK1389]),skolemize(X0,sK1387),skolemize(X1,sK1388),skolemize(X2,sK1389)],[f8595]) ).
fof(f11361,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k4_xboole_0(X0,k4_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f117]) ).
fof(f11796,plain,
! [X2,X0,X1] :
( k5_subset_1(X0,X1,X2) = k5_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f4117]) ).
fof(f11798,plain,
! [X2,X0,X1] :
( k3_xboole_0(X1,X2) = k5_subset_1(X0,X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f4121]) ).
fof(f15220,plain,
! [X0] :
( ~ l1_struct_0(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(cnf_transformation,[],[f6150]) ).
fof(f15310,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f6203]) ).
fof(f16056,plain,
! [X0] : k1_pcomps_1(X0) = u1_pre_topc(k2_pcomps_1(X0)),
inference(cnf_transformation,[],[f2611]) ).
fof(f16177,plain,
! [X0] : k1_zfmisc_1(X0) = k1_pcomps_1(X0),
inference(cnf_transformation,[],[f2652]) ).
fof(f18637,plain,
! [X0,X1] :
( k3_tex_4(X0,X1) = X1
| ~ v4_pre_topc(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f8212]) ).
fof(f18891,plain,
! [X2,X0,X1] :
( ~ v4_pre_topc(X2,X0)
| k3_xboole_0(X2,u1_struct_0(X1)) = sK1319(X1,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_tsp_1(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f11046]) ).
fof(f18892,plain,
! [X2,X0,X1] :
( ~ v4_pre_topc(X2,X0)
| v4_pre_topc(sK1319(X1,X2),X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_tsp_1(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f11046]) ).
fof(f19082,plain,
! [X0,X1] :
( ~ m2_tsp_1(X1,X0)
| l1_pre_topc(X1)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f8447]) ).
fof(f19084,plain,
! [X0,X1] :
( ~ m2_tsp_1(X1,X0)
| m1_pre_topc(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f11118]) ).
fof(f19104,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,[],[f8465]) ).
fof(f19105,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,[],[f8465]) ).
fof(f19106,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,[],[f8465]) ).
fof(f19107,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,[],[f8465]) ).
fof(f19160,plain,
! [X0,X1] :
( m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f8505]) ).
fof(f19266,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,[],[f11178]) ).
fof(f19279,plain,
l1_pre_topc(sK1387),
inference(cnf_transformation,[],[f11179]) ).
fof(f19280,plain,
v2_pre_topc(sK1387),
inference(cnf_transformation,[],[f11179]) ).
fof(f19281,plain,
~ v3_struct_0(sK1387),
inference(cnf_transformation,[],[f11179]) ).
fof(f19282,plain,
m2_tsp_1(sK1388,sK1387),
inference(cnf_transformation,[],[f11179]) ).
fof(f19283,plain,
v2_tsp_2(sK1388,sK1387),
inference(cnf_transformation,[],[f11179]) ).
fof(f19284,plain,
~ v3_struct_0(sK1388),
inference(cnf_transformation,[],[f11179]) ).
fof(f19285,plain,
m1_subset_1(sK1389,k1_zfmisc_1(u1_struct_0(sK1387))),
inference(cnf_transformation,[],[f11179]) ).
fof(f19286,plain,
v4_pre_topc(sK1389,sK1387),
inference(cnf_transformation,[],[f11179]) ).
fof(f19287,plain,
~ v4_pre_topc(k4_pre_topc(sK1387,sK1388,k4_tsp_2(sK1387,sK1388),sK1389),sK1388),
inference(cnf_transformation,[],[f11179]) ).
fof(f19289,plain,
! [X0] : k1_zfmisc_1(X0) = u1_pre_topc(k2_pcomps_1(X0)),
inference(definition_unfolding,[],[f16177,f16056]) ).
fof(f19618,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_pre_topc(k2_pcomps_1(X0)))
| ~ m1_subset_1(X1,u1_pre_topc(k2_pcomps_1(X0)))
| k5_subset_1(X0,X1,X2) = k5_subset_1(X0,X2,X1) ),
inference(definition_unfolding,[],[f11796,f19289,f19289]) ).
fof(f19620,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_pre_topc(k2_pcomps_1(X0)))
| ~ m1_subset_1(X1,u1_pre_topc(k2_pcomps_1(X0)))
| k5_subset_1(X0,X1,X2) = k4_xboole_0(X1,k4_xboole_0(X1,X2)) ),
inference(definition_unfolding,[],[f11798,f11361,f19289,f19289]) ).
fof(f21817,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_pre_topc(k2_pcomps_1(u1_struct_0(X0))))
| ~ v4_pre_topc(X1,X0)
| k3_tex_4(X0,X1) = X1
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(definition_unfolding,[],[f18637,f19289]) ).
fof(f21919,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_pre_topc(k2_pcomps_1(u1_struct_0(X0))))
| v4_pre_topc(sK1319(X1,X2),X1)
| ~ v4_pre_topc(X2,X0)
| ~ m2_tsp_1(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(definition_unfolding,[],[f18892,f19289]) ).
fof(f21920,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_pre_topc(k2_pcomps_1(u1_struct_0(X0))))
| sK1319(X1,X2) = k4_xboole_0(X2,k4_xboole_0(X2,u1_struct_0(X1)))
| ~ v4_pre_topc(X2,X0)
| ~ m2_tsp_1(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(definition_unfolding,[],[f18891,f11361,f19289]) ).
fof(f22043,plain,
! [X0,X1] :
( m1_subset_1(u1_struct_0(X1),u1_pre_topc(k2_pcomps_1(u1_struct_0(X0))))
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(definition_unfolding,[],[f19160,f19289]) ).
fof(f22082,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,u1_pre_topc(k2_pcomps_1(u1_struct_0(X0))))
| u1_struct_0(X1) != X5
| ~ m1_subset_1(X5,u1_pre_topc(k2_pcomps_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(definition_unfolding,[],[f19266,f19289,f19289]) ).
fof(f22091,plain,
m1_subset_1(sK1389,u1_pre_topc(k2_pcomps_1(u1_struct_0(sK1387)))),
inference(definition_unfolding,[],[f19285,f19289]) ).
fof(f22755,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,u1_pre_topc(k2_pcomps_1(u1_struct_0(X0))))
| ~ m1_subset_1(u1_struct_0(X1),u1_pre_topc(k2_pcomps_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,[],[f22082]) ).
fof(f22756,plain,
! [X0,X1,X6] :
( ~ v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_subset_1(X6,u1_pre_topc(k2_pcomps_1(u1_struct_0(X0))))
| ~ m1_subset_1(u1_struct_0(X1),u1_pre_topc(k2_pcomps_1(u1_struct_0(X0))))
| ~ v1_funct_1(k4_tsp_2(X0,X1))
| k5_subset_1(u1_struct_0(X0),u1_struct_0(X1),k3_tex_4(X0,X6)) = k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X6)
| ~ v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
| ~ m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(equality_resolution,[],[f22755]) ).
fof(f22757,definition,
sF1390 = k4_tsp_2(sK1387,sK1388),
introduced(definition,[new_symbols(definition,[sF1390])],[function_definition]) ).
fof(f22758,plain,
k4_tsp_2(sK1387,sK1388) = sF1390,
inference(reorient_equations,[],[f22757]) ).
fof(f22759,definition,
sF1391 = k4_pre_topc(sK1387,sK1388,sF1390,sK1389),
introduced(definition,[new_symbols(definition,[sF1391])],[function_definition]) ).
fof(f22760,plain,
k4_pre_topc(sK1387,sK1388,sF1390,sK1389) = sF1391,
inference(reorient_equations,[],[f22759]) ).
fof(f22761,plain,
~ v4_pre_topc(sF1391,sK1388),
inference(definition_folding,[],[f19287,f22760,f22758]) ).
fof(f22762,definition,
sF1392 = u1_struct_0(sK1387),
introduced(definition,[new_symbols(definition,[sF1392])],[function_definition]) ).
fof(f22763,plain,
u1_struct_0(sK1387) = sF1392,
inference(reorient_equations,[],[f22762]) ).
fof(f22764,definition,
sF1393 = k2_pcomps_1(sF1392),
introduced(definition,[new_symbols(definition,[sF1393])],[function_definition]) ).
fof(f22765,plain,
k2_pcomps_1(sF1392) = sF1393,
inference(reorient_equations,[],[f22764]) ).
fof(f22766,definition,
sF1394 = u1_pre_topc(sF1393),
introduced(definition,[new_symbols(definition,[sF1394])],[function_definition]) ).
fof(f22767,plain,
u1_pre_topc(sF1393) = sF1394,
inference(reorient_equations,[],[f22766]) ).
fof(f22768,plain,
m1_subset_1(sK1389,sF1394),
inference(definition_folding,[],[f22091,f22767,f22765,f22763]) ).
fof(f24961,definition,
( spl1395_391
<=> v1_funct_1(sF1390) ),
introduced(definition,[new_symbols(definition,[spl1395_391])],[avatar_definition]) ).
fof(f24962,plain,
( v1_funct_1(sF1390)
| ~ spl1395_391 ),
inference(avatar_component_clause,[],[f24961]) ).
fof(f24963,plain,
( ~ v1_funct_1(sF1390)
| spl1395_391 ),
inference(avatar_component_clause,[],[f24961]) ).
fof(f24965,definition,
( spl1395_392
<=> l1_struct_0(sK1388) ),
introduced(definition,[new_symbols(definition,[spl1395_392])],[avatar_definition]) ).
fof(f24966,plain,
( l1_struct_0(sK1388)
| ~ spl1395_392 ),
inference(avatar_component_clause,[],[f24965]) ).
fof(f24981,plain,
( v1_funct_2(sF1390,u1_struct_0(sK1387),u1_struct_0(sK1388))
| v3_struct_0(sK1387)
| ~ v2_pre_topc(sK1387)
| ~ l1_pre_topc(sK1387)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387) ),
inference(superposition,[],[f19106,f22758]) ).
fof(f24989,plain,
! [X0,X1] :
( ~ v1_funct_2(k4_tsp_2(sK1387,X0),sF1392,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_pre_topc(k2_pcomps_1(sF1392)))
| ~ m1_subset_1(u1_struct_0(X0),u1_pre_topc(k2_pcomps_1(sF1392)))
| ~ v1_funct_1(k4_tsp_2(sK1387,X0))
| k4_pre_topc(sK1387,X0,k4_tsp_2(sK1387,X0),X1) = k5_subset_1(sF1392,u1_struct_0(X0),k3_tex_4(sK1387,X1))
| ~ v5_pre_topc(k4_tsp_2(sK1387,X0),sK1387,X0)
| ~ m2_relset_1(k4_tsp_2(sK1387,X0),sF1392,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK1387)
| ~ m2_tsp_1(X0,sK1387)
| v3_struct_0(sK1387)
| ~ v2_pre_topc(sK1387)
| ~ l1_pre_topc(sK1387) ),
inference(superposition,[],[f22756,f22763]) ).
fof(f24992,plain,
( m2_relset_1(sF1390,u1_struct_0(sK1387),u1_struct_0(sK1388))
| v3_struct_0(sK1387)
| ~ v2_pre_topc(sK1387)
| ~ l1_pre_topc(sK1387)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387) ),
inference(superposition,[],[f19104,f22758]) ).
fof(f24995,plain,
( v5_pre_topc(sF1390,sK1387,sK1388)
| v3_struct_0(sK1387)
| ~ v2_pre_topc(sK1387)
| ~ l1_pre_topc(sK1387)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387) ),
inference(superposition,[],[f19105,f22758]) ).
fof(f24999,plain,
( m1_pre_topc(sK1388,sK1387)
| ~ l1_pre_topc(sK1387) ),
inference(resolution,[],[f19084,f19282]) ).
fof(f25000,plain,
m1_pre_topc(sK1388,sK1387),
inference(forward_subsumption_resolution,[],[f24999,f19279]) ).
fof(f25001,plain,
( v1_funct_1(sF1390)
| v3_struct_0(sK1387)
| ~ v2_pre_topc(sK1387)
| ~ l1_pre_topc(sK1387)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387) ),
inference(superposition,[],[f19107,f22758]) ).
fof(f25002,plain,
( l1_pre_topc(sK1388)
| ~ l1_pre_topc(sK1387) ),
inference(resolution,[],[f19082,f19282]) ).
fof(f25003,plain,
l1_pre_topc(sK1388),
inference(forward_subsumption_resolution,[],[f25002,f19279]) ).
fof(f25005,plain,
! [X0] :
( m1_subset_1(u1_struct_0(X0),u1_pre_topc(k2_pcomps_1(sF1392)))
| ~ m2_tsp_1(X0,sK1387)
| v3_struct_0(sK1387)
| ~ l1_pre_topc(sK1387) ),
inference(superposition,[],[f22043,f22763]) ).
fof(f25006,plain,
! [X0] :
( m1_subset_1(u1_struct_0(X0),u1_pre_topc(k2_pcomps_1(sF1392)))
| ~ m2_tsp_1(X0,sK1387)
| ~ l1_pre_topc(sK1387) ),
inference(forward_subsumption_resolution,[],[f25005,f19281]) ).
fof(f25008,plain,
! [X0] :
( m1_subset_1(u1_struct_0(X0),u1_pre_topc(k2_pcomps_1(sF1392)))
| ~ m2_tsp_1(X0,sK1387) ),
inference(forward_subsumption_resolution,[],[f25006,f19279]) ).
fof(f25009,plain,
! [X0] :
( m1_subset_1(u1_struct_0(X0),u1_pre_topc(sF1393))
| ~ m2_tsp_1(X0,sK1387) ),
inference(forward_demodulation,[],[f25008,f22765]) ).
fof(f25010,plain,
! [X0] :
( m1_subset_1(u1_struct_0(X0),sF1394)
| ~ m2_tsp_1(X0,sK1387) ),
inference(forward_demodulation,[],[f25009,f22767]) ).
fof(f25024,plain,
l1_struct_0(sK1388),
inference(resolution,[],[f15310,f25003]) ).
fof(f25025,plain,
spl1395_392,
inference(avatar_split_clause,[],[f25024,f24965]) ).
fof(f25043,plain,
( u1_struct_0(sK1388) = k2_pre_topc(sK1388)
| ~ spl1395_392 ),
inference(resolution,[],[f15220,f24966]) ).
fof(f25063,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_pre_topc(k2_pcomps_1(sF1392)))
| ~ v4_pre_topc(X0,sK1387)
| k3_tex_4(sK1387,X0) = X0
| v3_struct_0(sK1387)
| ~ v2_pre_topc(sK1387)
| ~ l1_pre_topc(sK1387) ),
inference(superposition,[],[f21817,f22763]) ).
fof(f25067,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_pre_topc(sF1393))
| ~ m1_subset_1(X1,u1_pre_topc(sF1393))
| k4_xboole_0(X1,k4_xboole_0(X1,X0)) = k5_subset_1(sF1392,X1,X0) ),
inference(superposition,[],[f19620,f22765]) ).
fof(f25068,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,sF1394)
| ~ m1_subset_1(X1,u1_pre_topc(sF1393))
| k4_xboole_0(X1,k4_xboole_0(X1,X0)) = k5_subset_1(sF1392,X1,X0) ),
inference(forward_demodulation,[],[f25067,f22767]) ).
fof(f25069,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,sF1394)
| ~ m1_subset_1(X0,sF1394)
| k4_xboole_0(X1,k4_xboole_0(X1,X0)) = k5_subset_1(sF1392,X1,X0) ),
inference(forward_demodulation,[],[f25068,f22767]) ).
fof(f25070,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1394)
| k4_xboole_0(sK1389,k4_xboole_0(sK1389,X0)) = k5_subset_1(sF1392,sK1389,X0) ),
inference(resolution,[],[f25069,f22768]) ).
fof(f25073,plain,
! [X0] :
( ~ m2_tsp_1(X0,sK1387)
| k4_xboole_0(sK1389,k4_xboole_0(sK1389,u1_struct_0(X0))) = k5_subset_1(sF1392,sK1389,u1_struct_0(X0)) ),
inference(resolution,[],[f25070,f25010]) ).
fof(f25075,plain,
k4_xboole_0(sK1389,k4_xboole_0(sK1389,u1_struct_0(sK1388))) = k5_subset_1(sF1392,sK1389,u1_struct_0(sK1388)),
inference(resolution,[],[f25073,f19282]) ).
fof(f25076,plain,
( k4_xboole_0(sK1389,k4_xboole_0(sK1389,k2_pre_topc(sK1388))) = k5_subset_1(sF1392,sK1389,k2_pre_topc(sK1388))
| ~ spl1395_392 ),
inference(forward_demodulation,[],[f25075,f25043]) ).
fof(f25103,plain,
( m1_subset_1(k2_pre_topc(sK1388),sF1394)
| ~ m2_tsp_1(sK1388,sK1387)
| ~ spl1395_392 ),
inference(superposition,[],[f25010,f25043]) ).
fof(f25108,plain,
( m1_subset_1(k2_pre_topc(sK1388),sF1394)
| ~ spl1395_392 ),
inference(forward_subsumption_resolution,[],[f25103,f19282]) ).
fof(f25167,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_pre_topc(k2_pcomps_1(sF1392)))
| k4_xboole_0(X0,k4_xboole_0(X0,u1_struct_0(X1))) = sK1319(X1,X0)
| ~ v4_pre_topc(X0,sK1387)
| ~ m2_tsp_1(X1,sK1387)
| ~ l1_pre_topc(sK1387) ),
inference(superposition,[],[f21920,f22763]) ).
fof(f25172,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_pre_topc(k2_pcomps_1(sF1392)))
| k4_xboole_0(X0,k4_xboole_0(X0,u1_struct_0(X1))) = sK1319(X1,X0)
| ~ v4_pre_topc(X0,sK1387)
| ~ m2_tsp_1(X1,sK1387) ),
inference(forward_subsumption_resolution,[],[f25167,f19279]) ).
fof(f25174,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_pre_topc(sF1393))
| k4_xboole_0(X0,k4_xboole_0(X0,u1_struct_0(X1))) = sK1319(X1,X0)
| ~ v4_pre_topc(X0,sK1387)
| ~ m2_tsp_1(X1,sK1387) ),
inference(forward_demodulation,[],[f25172,f22765]) ).
fof(f25175,plain,
! [X0,X1] :
( ~ m2_tsp_1(X1,sK1387)
| k4_xboole_0(X0,k4_xboole_0(X0,u1_struct_0(X1))) = sK1319(X1,X0)
| ~ v4_pre_topc(X0,sK1387)
| ~ m1_subset_1(X0,sF1394) ),
inference(forward_demodulation,[],[f25174,f22767]) ).
fof(f25176,plain,
! [X0] :
( k4_xboole_0(X0,k4_xboole_0(X0,u1_struct_0(sK1388))) = sK1319(sK1388,X0)
| ~ v4_pre_topc(X0,sK1387)
| ~ m1_subset_1(X0,sF1394) ),
inference(resolution,[],[f25175,f19282]) ).
fof(f25177,plain,
( ! [X0] :
( ~ v4_pre_topc(X0,sK1387)
| sK1319(sK1388,X0) = k4_xboole_0(X0,k4_xboole_0(X0,k2_pre_topc(sK1388)))
| ~ m1_subset_1(X0,sF1394) )
| ~ spl1395_392 ),
inference(forward_demodulation,[],[f25176,f25043]) ).
fof(f25178,plain,
( k4_xboole_0(sK1389,k4_xboole_0(sK1389,k2_pre_topc(sK1388))) = sK1319(sK1388,sK1389)
| ~ m1_subset_1(sK1389,sF1394)
| ~ spl1395_392 ),
inference(resolution,[],[f25177,f19286]) ).
fof(f25182,plain,
( k4_xboole_0(sK1389,k4_xboole_0(sK1389,k2_pre_topc(sK1388))) = sK1319(sK1388,sK1389)
| ~ spl1395_392 ),
inference(forward_subsumption_resolution,[],[f25178,f22768]) ).
fof(f25184,plain,
( k5_subset_1(sF1392,sK1389,k2_pre_topc(sK1388)) = sK1319(sK1388,sK1389)
| ~ spl1395_392 ),
inference(forward_demodulation,[],[f25182,f25076]) ).
fof(f25228,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_pre_topc(k2_pcomps_1(sF1392)))
| v4_pre_topc(sK1319(X1,X0),X1)
| ~ v4_pre_topc(X0,sK1387)
| ~ m2_tsp_1(X1,sK1387)
| ~ l1_pre_topc(sK1387) ),
inference(superposition,[],[f21919,f22763]) ).
fof(f25233,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_pre_topc(k2_pcomps_1(sF1392)))
| v4_pre_topc(sK1319(X1,X0),X1)
| ~ v4_pre_topc(X0,sK1387)
| ~ m2_tsp_1(X1,sK1387) ),
inference(forward_subsumption_resolution,[],[f25228,f19279]) ).
fof(f25235,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_pre_topc(sF1393))
| v4_pre_topc(sK1319(X1,X0),X1)
| ~ v4_pre_topc(X0,sK1387)
| ~ m2_tsp_1(X1,sK1387) ),
inference(forward_demodulation,[],[f25233,f22765]) ).
fof(f25236,plain,
! [X0,X1] :
( v4_pre_topc(sK1319(X1,X0),X1)
| ~ m1_subset_1(X0,sF1394)
| ~ v4_pre_topc(X0,sK1387)
| ~ m2_tsp_1(X1,sK1387) ),
inference(forward_demodulation,[],[f25235,f22767]) ).
fof(f25241,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_pre_topc(sF1393))
| ~ m1_subset_1(X1,u1_pre_topc(sF1393))
| k5_subset_1(sF1392,X1,X0) = k5_subset_1(sF1392,X0,X1) ),
inference(superposition,[],[f19618,f22765]) ).
fof(f25242,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,sF1394)
| ~ m1_subset_1(X1,u1_pre_topc(sF1393))
| k5_subset_1(sF1392,X1,X0) = k5_subset_1(sF1392,X0,X1) ),
inference(forward_demodulation,[],[f25241,f22767]) ).
fof(f25243,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,sF1394)
| ~ m1_subset_1(X0,sF1394)
| k5_subset_1(sF1392,X1,X0) = k5_subset_1(sF1392,X0,X1) ),
inference(forward_demodulation,[],[f25242,f22767]) ).
fof(f25246,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1394)
| k5_subset_1(sF1392,sK1389,X0) = k5_subset_1(sF1392,X0,sK1389) ),
inference(resolution,[],[f25243,f22768]) ).
fof(f25248,plain,
( k5_subset_1(sF1392,sK1389,k2_pre_topc(sK1388)) = k5_subset_1(sF1392,k2_pre_topc(sK1388),sK1389)
| ~ spl1395_392 ),
inference(resolution,[],[f25246,f25108]) ).
fof(f25250,plain,
( sK1319(sK1388,sK1389) = k5_subset_1(sF1392,k2_pre_topc(sK1388),sK1389)
| ~ spl1395_392 ),
inference(forward_demodulation,[],[f25248,f25184]) ).
fof(f25840,plain,
( v1_funct_2(sF1390,u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ v2_pre_topc(sK1387)
| ~ l1_pre_topc(sK1387)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387) ),
inference(forward_subsumption_resolution,[],[f24981,f19281]) ).
fof(f25842,plain,
! [X0,X1] :
( ~ v1_funct_2(k4_tsp_2(sK1387,X0),sF1392,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_pre_topc(k2_pcomps_1(sF1392)))
| ~ m1_subset_1(u1_struct_0(X0),u1_pre_topc(k2_pcomps_1(sF1392)))
| ~ v1_funct_1(k4_tsp_2(sK1387,X0))
| k4_pre_topc(sK1387,X0,k4_tsp_2(sK1387,X0),X1) = k5_subset_1(sF1392,u1_struct_0(X0),k3_tex_4(sK1387,X1))
| ~ v5_pre_topc(k4_tsp_2(sK1387,X0),sK1387,X0)
| ~ m2_relset_1(k4_tsp_2(sK1387,X0),sF1392,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK1387)
| ~ m2_tsp_1(X0,sK1387)
| ~ v2_pre_topc(sK1387)
| ~ l1_pre_topc(sK1387) ),
inference(forward_subsumption_resolution,[],[f24989,f19281]) ).
fof(f25845,plain,
( m2_relset_1(sF1390,u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ v2_pre_topc(sK1387)
| ~ l1_pre_topc(sK1387)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387) ),
inference(forward_subsumption_resolution,[],[f24992,f19281]) ).
fof(f25846,plain,
( v5_pre_topc(sF1390,sK1387,sK1388)
| ~ v2_pre_topc(sK1387)
| ~ l1_pre_topc(sK1387)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387) ),
inference(forward_subsumption_resolution,[],[f24995,f19281]) ).
fof(f25850,plain,
( v3_struct_0(sK1387)
| ~ v2_pre_topc(sK1387)
| ~ l1_pre_topc(sK1387)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387)
| spl1395_391 ),
inference(forward_subsumption_resolution,[],[f25001,f24963]) ).
fof(f25861,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_pre_topc(k2_pcomps_1(sF1392)))
| ~ v4_pre_topc(X0,sK1387)
| k3_tex_4(sK1387,X0) = X0
| ~ v2_pre_topc(sK1387)
| ~ l1_pre_topc(sK1387) ),
inference(forward_subsumption_resolution,[],[f25063,f19281]) ).
fof(f25925,plain,
( v1_funct_2(sF1390,u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ l1_pre_topc(sK1387)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387) ),
inference(forward_subsumption_resolution,[],[f25840,f19280]) ).
fof(f25927,plain,
! [X0,X1] :
( ~ v1_funct_2(k4_tsp_2(sK1387,X0),sF1392,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_pre_topc(k2_pcomps_1(sF1392)))
| ~ m1_subset_1(u1_struct_0(X0),u1_pre_topc(k2_pcomps_1(sF1392)))
| ~ v1_funct_1(k4_tsp_2(sK1387,X0))
| k4_pre_topc(sK1387,X0,k4_tsp_2(sK1387,X0),X1) = k5_subset_1(sF1392,u1_struct_0(X0),k3_tex_4(sK1387,X1))
| ~ v5_pre_topc(k4_tsp_2(sK1387,X0),sK1387,X0)
| ~ m2_relset_1(k4_tsp_2(sK1387,X0),sF1392,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK1387)
| ~ m2_tsp_1(X0,sK1387)
| ~ l1_pre_topc(sK1387) ),
inference(forward_subsumption_resolution,[],[f25842,f19280]) ).
fof(f25929,plain,
( m2_relset_1(sF1390,u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ l1_pre_topc(sK1387)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387) ),
inference(forward_subsumption_resolution,[],[f25845,f19280]) ).
fof(f25930,plain,
( v5_pre_topc(sF1390,sK1387,sK1388)
| ~ l1_pre_topc(sK1387)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387) ),
inference(forward_subsumption_resolution,[],[f25846,f19280]) ).
fof(f25933,plain,
( ~ v2_pre_topc(sK1387)
| ~ l1_pre_topc(sK1387)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387)
| spl1395_391 ),
inference(forward_subsumption_resolution,[],[f25850,f19281]) ).
fof(f25940,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_pre_topc(k2_pcomps_1(sF1392)))
| ~ v4_pre_topc(X0,sK1387)
| k3_tex_4(sK1387,X0) = X0
| ~ l1_pre_topc(sK1387) ),
inference(forward_subsumption_resolution,[],[f25861,f19280]) ).
fof(f25988,plain,
( v1_funct_2(sF1390,u1_struct_0(sK1387),u1_struct_0(sK1388))
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387) ),
inference(forward_subsumption_resolution,[],[f25925,f19279]) ).
fof(f25990,plain,
! [X0,X1] :
( ~ v1_funct_2(k4_tsp_2(sK1387,X0),sF1392,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_pre_topc(k2_pcomps_1(sF1392)))
| ~ m1_subset_1(u1_struct_0(X0),u1_pre_topc(k2_pcomps_1(sF1392)))
| ~ v1_funct_1(k4_tsp_2(sK1387,X0))
| k4_pre_topc(sK1387,X0,k4_tsp_2(sK1387,X0),X1) = k5_subset_1(sF1392,u1_struct_0(X0),k3_tex_4(sK1387,X1))
| ~ v5_pre_topc(k4_tsp_2(sK1387,X0),sK1387,X0)
| ~ m2_relset_1(k4_tsp_2(sK1387,X0),sF1392,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK1387)
| ~ m2_tsp_1(X0,sK1387) ),
inference(forward_subsumption_resolution,[],[f25927,f19279]) ).
fof(f25992,plain,
( m2_relset_1(sF1390,u1_struct_0(sK1387),u1_struct_0(sK1388))
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387) ),
inference(forward_subsumption_resolution,[],[f25929,f19279]) ).
fof(f25993,plain,
( v5_pre_topc(sF1390,sK1387,sK1388)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387) ),
inference(forward_subsumption_resolution,[],[f25930,f19279]) ).
fof(f25996,plain,
( ~ l1_pre_topc(sK1387)
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387)
| spl1395_391 ),
inference(forward_subsumption_resolution,[],[f25933,f19280]) ).
fof(f26003,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_pre_topc(k2_pcomps_1(sF1392)))
| ~ v4_pre_topc(X0,sK1387)
| k3_tex_4(sK1387,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f25940,f19279]) ).
fof(f26099,plain,
( v1_funct_2(sF1390,u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387) ),
inference(forward_subsumption_resolution,[],[f25988,f19284]) ).
fof(f26100,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_pre_topc(sF1393))
| ~ v1_funct_2(k4_tsp_2(sK1387,X0),sF1392,u1_struct_0(X0))
| ~ m1_subset_1(u1_struct_0(X0),u1_pre_topc(k2_pcomps_1(sF1392)))
| ~ v1_funct_1(k4_tsp_2(sK1387,X0))
| k4_pre_topc(sK1387,X0,k4_tsp_2(sK1387,X0),X1) = k5_subset_1(sF1392,u1_struct_0(X0),k3_tex_4(sK1387,X1))
| ~ v5_pre_topc(k4_tsp_2(sK1387,X0),sK1387,X0)
| ~ m2_relset_1(k4_tsp_2(sK1387,X0),sF1392,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK1387)
| ~ m2_tsp_1(X0,sK1387) ),
inference(forward_demodulation,[],[f25990,f22765]) ).
fof(f26101,plain,
( m2_relset_1(sF1390,u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387) ),
inference(forward_subsumption_resolution,[],[f25992,f19284]) ).
fof(f26102,plain,
( v5_pre_topc(sF1390,sK1387,sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387) ),
inference(forward_subsumption_resolution,[],[f25993,f19284]) ).
fof(f26103,plain,
( v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387)
| spl1395_391 ),
inference(forward_subsumption_resolution,[],[f25996,f19279]) ).
fof(f26109,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_pre_topc(sF1393))
| ~ v4_pre_topc(X0,sK1387)
| k3_tex_4(sK1387,X0) = X0 ),
inference(forward_demodulation,[],[f26003,f22765]) ).
fof(f26127,plain,
( v1_funct_2(sF1390,u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_pre_topc(sK1388,sK1387) ),
inference(forward_subsumption_resolution,[],[f26099,f19283]) ).
fof(f26128,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,sF1394)
| ~ v1_funct_2(k4_tsp_2(sK1387,X0),sF1392,u1_struct_0(X0))
| ~ m1_subset_1(u1_struct_0(X0),u1_pre_topc(k2_pcomps_1(sF1392)))
| ~ v1_funct_1(k4_tsp_2(sK1387,X0))
| k4_pre_topc(sK1387,X0,k4_tsp_2(sK1387,X0),X1) = k5_subset_1(sF1392,u1_struct_0(X0),k3_tex_4(sK1387,X1))
| ~ v5_pre_topc(k4_tsp_2(sK1387,X0),sK1387,X0)
| ~ m2_relset_1(k4_tsp_2(sK1387,X0),sF1392,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK1387)
| ~ m2_tsp_1(X0,sK1387) ),
inference(forward_demodulation,[],[f26100,f22767]) ).
fof(f26129,plain,
( m2_relset_1(sF1390,u1_struct_0(sK1387),u1_struct_0(sK1388))
| ~ m1_pre_topc(sK1388,sK1387) ),
inference(forward_subsumption_resolution,[],[f26101,f19283]) ).
fof(f26130,plain,
( v5_pre_topc(sF1390,sK1387,sK1388)
| ~ m1_pre_topc(sK1388,sK1387) ),
inference(forward_subsumption_resolution,[],[f26102,f19283]) ).
fof(f26131,plain,
( ~ v2_tsp_2(sK1388,sK1387)
| ~ m1_pre_topc(sK1388,sK1387)
| spl1395_391 ),
inference(forward_subsumption_resolution,[],[f26103,f19284]) ).
fof(f26137,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1394)
| ~ v4_pre_topc(X0,sK1387)
| k3_tex_4(sK1387,X0) = X0 ),
inference(forward_demodulation,[],[f26109,f22767]) ).
fof(f26147,plain,
v1_funct_2(sF1390,u1_struct_0(sK1387),u1_struct_0(sK1388)),
inference(forward_subsumption_resolution,[],[f26127,f25000]) ).
fof(f26148,plain,
! [X0,X1] :
( ~ m1_subset_1(u1_struct_0(X0),u1_pre_topc(sF1393))
| ~ m1_subset_1(X1,sF1394)
| ~ v1_funct_2(k4_tsp_2(sK1387,X0),sF1392,u1_struct_0(X0))
| ~ v1_funct_1(k4_tsp_2(sK1387,X0))
| k4_pre_topc(sK1387,X0,k4_tsp_2(sK1387,X0),X1) = k5_subset_1(sF1392,u1_struct_0(X0),k3_tex_4(sK1387,X1))
| ~ v5_pre_topc(k4_tsp_2(sK1387,X0),sK1387,X0)
| ~ m2_relset_1(k4_tsp_2(sK1387,X0),sF1392,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK1387)
| ~ m2_tsp_1(X0,sK1387) ),
inference(forward_demodulation,[],[f26128,f22765]) ).
fof(f26149,plain,
m2_relset_1(sF1390,u1_struct_0(sK1387),u1_struct_0(sK1388)),
inference(forward_subsumption_resolution,[],[f26129,f25000]) ).
fof(f26150,plain,
v5_pre_topc(sF1390,sK1387,sK1388),
inference(forward_subsumption_resolution,[],[f26130,f25000]) ).
fof(f26151,plain,
( ~ m1_pre_topc(sK1388,sK1387)
| spl1395_391 ),
inference(forward_subsumption_resolution,[],[f26131,f19283]) ).
fof(f26157,definition,
( spl1395_440
<=> ! [X0] :
( ~ m1_subset_1(X0,sF1394)
| k3_tex_4(sK1387,X0) = X0
| ~ v4_pre_topc(X0,sK1387) ) ),
introduced(definition,[new_symbols(definition,[spl1395_440])],[avatar_definition]) ).
fof(f26158,plain,
( ! [X0] :
( ~ v4_pre_topc(X0,sK1387)
| k3_tex_4(sK1387,X0) = X0
| ~ m1_subset_1(X0,sF1394) )
| ~ spl1395_440 ),
inference(avatar_component_clause,[],[f26157]) ).
fof(f26160,plain,
spl1395_440,
inference(avatar_split_clause,[],[f26137,f26157]) ).
fof(f26168,plain,
( v1_funct_2(sF1390,u1_struct_0(sK1387),k2_pre_topc(sK1388))
| ~ spl1395_392 ),
inference(forward_demodulation,[],[f26147,f25043]) ).
fof(f26169,plain,
! [X0,X1] :
( ~ m1_subset_1(u1_struct_0(X0),sF1394)
| ~ m1_subset_1(X1,sF1394)
| ~ v1_funct_2(k4_tsp_2(sK1387,X0),sF1392,u1_struct_0(X0))
| ~ v1_funct_1(k4_tsp_2(sK1387,X0))
| k4_pre_topc(sK1387,X0,k4_tsp_2(sK1387,X0),X1) = k5_subset_1(sF1392,u1_struct_0(X0),k3_tex_4(sK1387,X1))
| ~ v5_pre_topc(k4_tsp_2(sK1387,X0),sK1387,X0)
| ~ m2_relset_1(k4_tsp_2(sK1387,X0),sF1392,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK1387)
| ~ m2_tsp_1(X0,sK1387) ),
inference(forward_demodulation,[],[f26148,f22767]) ).
fof(f26170,plain,
( m2_relset_1(sF1390,u1_struct_0(sK1387),k2_pre_topc(sK1388))
| ~ spl1395_392 ),
inference(forward_demodulation,[],[f26149,f25043]) ).
fof(f26171,plain,
( $false
| spl1395_391 ),
inference(forward_subsumption_resolution,[],[f26151,f25000]) ).
fof(f26172,plain,
spl1395_391,
inference(avatar_contradiction_clause,[],[f26171]) ).
fof(f26175,plain,
( v1_funct_2(sF1390,sF1392,k2_pre_topc(sK1388))
| ~ spl1395_392 ),
inference(forward_demodulation,[],[f26168,f22763]) ).
fof(f26176,plain,
! [X0,X1] :
( ~ v1_funct_2(k4_tsp_2(sK1387,X0),sF1392,u1_struct_0(X0))
| ~ m1_subset_1(X1,sF1394)
| ~ v1_funct_1(k4_tsp_2(sK1387,X0))
| k4_pre_topc(sK1387,X0,k4_tsp_2(sK1387,X0),X1) = k5_subset_1(sF1392,u1_struct_0(X0),k3_tex_4(sK1387,X1))
| ~ v5_pre_topc(k4_tsp_2(sK1387,X0),sK1387,X0)
| ~ m2_relset_1(k4_tsp_2(sK1387,X0),sF1392,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK1387)
| ~ m2_tsp_1(X0,sK1387) ),
inference(forward_subsumption_resolution,[],[f26169,f25010]) ).
fof(f26177,plain,
( m2_relset_1(sF1390,sF1392,k2_pre_topc(sK1388))
| ~ spl1395_392 ),
inference(forward_demodulation,[],[f26170,f22763]) ).
fof(f26266,plain,
( sK1389 = k3_tex_4(sK1387,sK1389)
| ~ m1_subset_1(sK1389,sF1394)
| ~ spl1395_440 ),
inference(resolution,[],[f26158,f19286]) ).
fof(f26269,plain,
( sK1389 = k3_tex_4(sK1387,sK1389)
| ~ spl1395_440 ),
inference(forward_subsumption_resolution,[],[f26266,f22768]) ).
fof(f26542,plain,
! [X0] :
( ~ v1_funct_2(sF1390,sF1392,u1_struct_0(sK1388))
| ~ m1_subset_1(X0,sF1394)
| ~ v1_funct_1(sF1390)
| k4_pre_topc(sK1387,sK1388,sF1390,X0) = k5_subset_1(sF1392,u1_struct_0(sK1388),k3_tex_4(sK1387,X0))
| ~ v5_pre_topc(sF1390,sK1387,sK1388)
| ~ m2_relset_1(sF1390,sF1392,u1_struct_0(sK1388))
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m2_tsp_1(sK1388,sK1387) ),
inference(superposition,[],[f26176,f22758]) ).
fof(f26546,plain,
( ! [X0] :
( ~ v1_funct_2(sF1390,sF1392,u1_struct_0(sK1388))
| ~ m1_subset_1(X0,sF1394)
| k4_pre_topc(sK1387,sK1388,sF1390,X0) = k5_subset_1(sF1392,u1_struct_0(sK1388),k3_tex_4(sK1387,X0))
| ~ v5_pre_topc(sF1390,sK1387,sK1388)
| ~ m2_relset_1(sF1390,sF1392,u1_struct_0(sK1388))
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m2_tsp_1(sK1388,sK1387) )
| ~ spl1395_391 ),
inference(forward_subsumption_resolution,[],[f26542,f24962]) ).
fof(f26548,plain,
( ! [X0] :
( ~ v1_funct_2(sF1390,sF1392,u1_struct_0(sK1388))
| ~ m1_subset_1(X0,sF1394)
| k4_pre_topc(sK1387,sK1388,sF1390,X0) = k5_subset_1(sF1392,u1_struct_0(sK1388),k3_tex_4(sK1387,X0))
| ~ m2_relset_1(sF1390,sF1392,u1_struct_0(sK1388))
| v3_struct_0(sK1388)
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m2_tsp_1(sK1388,sK1387) )
| ~ spl1395_391 ),
inference(forward_subsumption_resolution,[],[f26546,f26150]) ).
fof(f26550,plain,
( ! [X0] :
( ~ v1_funct_2(sF1390,sF1392,u1_struct_0(sK1388))
| ~ m1_subset_1(X0,sF1394)
| k4_pre_topc(sK1387,sK1388,sF1390,X0) = k5_subset_1(sF1392,u1_struct_0(sK1388),k3_tex_4(sK1387,X0))
| ~ m2_relset_1(sF1390,sF1392,u1_struct_0(sK1388))
| ~ v2_tsp_2(sK1388,sK1387)
| ~ m2_tsp_1(sK1388,sK1387) )
| ~ spl1395_391 ),
inference(forward_subsumption_resolution,[],[f26548,f19284]) ).
fof(f26552,plain,
( ! [X0] :
( ~ v1_funct_2(sF1390,sF1392,u1_struct_0(sK1388))
| ~ m1_subset_1(X0,sF1394)
| k4_pre_topc(sK1387,sK1388,sF1390,X0) = k5_subset_1(sF1392,u1_struct_0(sK1388),k3_tex_4(sK1387,X0))
| ~ m2_relset_1(sF1390,sF1392,u1_struct_0(sK1388))
| ~ m2_tsp_1(sK1388,sK1387) )
| ~ spl1395_391 ),
inference(forward_subsumption_resolution,[],[f26550,f19283]) ).
fof(f26554,plain,
( ! [X0] :
( ~ v1_funct_2(sF1390,sF1392,u1_struct_0(sK1388))
| ~ m1_subset_1(X0,sF1394)
| k4_pre_topc(sK1387,sK1388,sF1390,X0) = k5_subset_1(sF1392,u1_struct_0(sK1388),k3_tex_4(sK1387,X0))
| ~ m2_relset_1(sF1390,sF1392,u1_struct_0(sK1388)) )
| ~ spl1395_391 ),
inference(forward_subsumption_resolution,[],[f26552,f19282]) ).
fof(f26556,plain,
( ! [X0] :
( ~ v1_funct_2(sF1390,sF1392,k2_pre_topc(sK1388))
| ~ m1_subset_1(X0,sF1394)
| k4_pre_topc(sK1387,sK1388,sF1390,X0) = k5_subset_1(sF1392,u1_struct_0(sK1388),k3_tex_4(sK1387,X0))
| ~ m2_relset_1(sF1390,sF1392,u1_struct_0(sK1388)) )
| ~ spl1395_391
| ~ spl1395_392 ),
inference(forward_demodulation,[],[f26554,f25043]) ).
fof(f26558,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF1394)
| k4_pre_topc(sK1387,sK1388,sF1390,X0) = k5_subset_1(sF1392,u1_struct_0(sK1388),k3_tex_4(sK1387,X0))
| ~ m2_relset_1(sF1390,sF1392,u1_struct_0(sK1388)) )
| ~ spl1395_391
| ~ spl1395_392 ),
inference(forward_subsumption_resolution,[],[f26556,f26175]) ).
fof(f26560,plain,
( ! [X0] :
( k4_pre_topc(sK1387,sK1388,sF1390,X0) = k5_subset_1(sF1392,k2_pre_topc(sK1388),k3_tex_4(sK1387,X0))
| ~ m1_subset_1(X0,sF1394)
| ~ m2_relset_1(sF1390,sF1392,u1_struct_0(sK1388)) )
| ~ spl1395_391
| ~ spl1395_392 ),
inference(forward_demodulation,[],[f26558,f25043]) ).
fof(f26562,plain,
( ! [X0] :
( ~ m2_relset_1(sF1390,sF1392,k2_pre_topc(sK1388))
| k4_pre_topc(sK1387,sK1388,sF1390,X0) = k5_subset_1(sF1392,k2_pre_topc(sK1388),k3_tex_4(sK1387,X0))
| ~ m1_subset_1(X0,sF1394) )
| ~ spl1395_391
| ~ spl1395_392 ),
inference(forward_demodulation,[],[f26560,f25043]) ).
fof(f26564,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF1394)
| k4_pre_topc(sK1387,sK1388,sF1390,X0) = k5_subset_1(sF1392,k2_pre_topc(sK1388),k3_tex_4(sK1387,X0)) )
| ~ spl1395_391
| ~ spl1395_392 ),
inference(forward_subsumption_resolution,[],[f26562,f26177]) ).
fof(f26570,plain,
( k4_pre_topc(sK1387,sK1388,sF1390,sK1389) = k5_subset_1(sF1392,k2_pre_topc(sK1388),k3_tex_4(sK1387,sK1389))
| ~ spl1395_391
| ~ spl1395_392 ),
inference(resolution,[],[f26564,f22768]) ).
fof(f26573,plain,
( k4_pre_topc(sK1387,sK1388,sF1390,sK1389) = k5_subset_1(sF1392,k2_pre_topc(sK1388),sK1389)
| ~ spl1395_391
| ~ spl1395_392
| ~ spl1395_440 ),
inference(forward_demodulation,[],[f26570,f26269]) ).
fof(f26575,plain,
( k4_pre_topc(sK1387,sK1388,sF1390,sK1389) = sK1319(sK1388,sK1389)
| ~ spl1395_391
| ~ spl1395_392
| ~ spl1395_440 ),
inference(forward_demodulation,[],[f26573,f25250]) ).
fof(f26577,plain,
( sF1391 = sK1319(sK1388,sK1389)
| ~ spl1395_391
| ~ spl1395_392
| ~ spl1395_440 ),
inference(forward_demodulation,[],[f26575,f22760]) ).
fof(f26578,plain,
( v4_pre_topc(sF1391,sK1388)
| ~ m1_subset_1(sK1389,sF1394)
| ~ v4_pre_topc(sK1389,sK1387)
| ~ m2_tsp_1(sK1388,sK1387)
| ~ spl1395_391
| ~ spl1395_392
| ~ spl1395_440 ),
inference(superposition,[],[f25236,f26577]) ).
fof(f26579,plain,
( ~ m1_subset_1(sK1389,sF1394)
| ~ v4_pre_topc(sK1389,sK1387)
| ~ m2_tsp_1(sK1388,sK1387)
| ~ spl1395_391
| ~ spl1395_392
| ~ spl1395_440 ),
inference(forward_subsumption_resolution,[],[f26578,f22761]) ).
fof(f26580,plain,
( ~ v4_pre_topc(sK1389,sK1387)
| ~ m2_tsp_1(sK1388,sK1387)
| ~ spl1395_391
| ~ spl1395_392
| ~ spl1395_440 ),
inference(forward_subsumption_resolution,[],[f26579,f22768]) ).
fof(f26581,plain,
( ~ m2_tsp_1(sK1388,sK1387)
| ~ spl1395_391
| ~ spl1395_392
| ~ spl1395_440 ),
inference(forward_subsumption_resolution,[],[f26580,f19286]) ).
fof(f26582,plain,
( $false
| ~ spl1395_391
| ~ spl1395_392
| ~ spl1395_440 ),
inference(forward_subsumption_resolution,[],[f26581,f19282]) ).
fof(f26583,plain,
( ~ spl1395_391
| ~ spl1395_392
| ~ spl1395_440 ),
inference(avatar_contradiction_clause,[],[f26582]) ).
cnf(s340,plain,
spl1395_392,
inference(sat_conversion,[],[f25025]) ).
cnf(s381,plain,
spl1395_440,
inference(sat_conversion,[],[f26160]) ).
cnf(s383,plain,
spl1395_391,
inference(sat_conversion,[],[f26172]) ).
cnf(s392,plain,
( ~ spl1395_391
| ~ spl1395_392
| ~ spl1395_440 ),
inference(sat_conversion,[],[f26583]) ).
cnf(s394,plain,
~ spl1395_392,
inference(rat,[],[s392,s383,s381]) ).
cnf(s400,plain,
$false,
inference(rat,[],[s340,s394]) ).
fof(f26584,plain,
$false,
inference(avatar_sat_refutation,[],[s400]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP042+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 % Computer : n017.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 18:58:07 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.24 Running first-order theorem proving
% 0.09/0.24 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
% 12.86/2.66 % (3891668)Detected formulas, will run a generic FOF schedule.
% 12.86/2.66 % (3891673)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=3568232854:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 12.86/2.66 % (3891678)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1089383036:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 12.86/2.66 % (3891674)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=1611178625:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 12.86/2.66 % (3891675)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=1242213507:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 12.86/2.66 % (3891679)dis-21_1_sil=8000:lcm=predicate:random_seed=1522101829:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 12.86/2.66 % (3891676)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=950945349:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 12.86/2.66 % (3891677)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1467229332:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 12.86/2.66 % (3891676)Refutation not found, incomplete strategy
% 12.86/2.66 % (3891676)------------------------------
% 12.86/2.66 % (3891676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.86/2.66 % (3891676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.86/2.66 % (3891676)CaDiCaL version: 2.1.3
% 12.86/2.66 % (3891676)Termination reason: Refutation not found, incomplete strategy
% 12.86/2.66 % (3891676)Time elapsed: 0.030 s
% 12.86/2.66 % (3891676)Peak memory usage: 93 MB
% 12.86/2.66 % (3891676)Instructions burned: 43 (million)
% 12.86/2.66 % (3891677)Instruction limit reached!
% 12.86/2.66 % (3891677)------------------------------
% 12.86/2.66 % (3891677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.86/2.66 % (3891677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.86/2.66 % (3891677)CaDiCaL version: 2.1.3
% 12.86/2.66 % (3891677)Termination reason: Instruction limit
% 12.86/2.66 % (3891677)Termination phase: Saturation
% 12.86/2.66 % (3891677)Time elapsed: 0.077 s
% 12.86/2.66 % (3891677)Peak memory usage: 94 MB
% 12.86/2.66 % (3891677)Instructions burned: 120 (million)
% 12.86/2.66 % (3891679)Instruction limit reached!
% 12.86/2.66 % (3891679)------------------------------
% 12.86/2.66 % (3891679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.86/2.66 % (3891679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.86/2.66 % (3891679)CaDiCaL version: 2.1.3
% 12.86/2.66 % (3891679)Termination reason: Instruction limit
% 12.86/2.66 % (3891679)Termination phase: Preprocessing 3
% 12.86/2.66 % (3891679)Time elapsed: 0.090 s
% 12.86/2.66 % (3891679)Peak memory usage: 95 MB
% 12.86/2.66 % (3891679)Instructions burned: 129 (million)
% 12.86/2.66 % (3891678)Instruction limit reached!
% 12.86/2.66 % (3891678)------------------------------
% 12.86/2.66 % (3891678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.86/2.66 % (3891678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.86/2.66 % (3891678)CaDiCaL version: 2.1.3
% 12.86/2.66 % (3891678)Termination reason: Instruction limit
% 12.86/2.66 % (3891678)Termination phase: Preprocessing 3
% 12.86/2.66 % (3891678)Time elapsed: 0.091 s
% 12.86/2.66 % (3891678)Peak memory usage: 94 MB
% 12.86/2.66 % (3891678)Instructions burned: 139 (million)
% 12.86/2.66 % (3891687)lrs+10_1_sil=8000:sp=occurrence:random_seed=728031449:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 12.86/2.66 % (3891689)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2334505749:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 12.86/2.66 % (3891688)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4004264505:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 12.86/2.66 % (3891676)------------------------------
% 12.86/2.66 % (3891676)------------------------------
% 12.86/2.66 % (3891688)Instruction limit reached!
% 12.86/2.66 % (3891688)------------------------------
% 12.86/2.66 % (3891688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.86/2.66 % (3891688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.86/2.66 % (3891688)CaDiCaL version: 2.1.3
% 12.86/2.66 % (3891688)Termination reason: Instruction limit
% 12.86/2.66 % (3891688)Termination phase: Saturation
% 12.86/2.66 % (3891688)Time elapsed: 0.089 s
% 12.86/2.66 % (3891688)Peak memory usage: 94 MB
% 12.86/2.66 % (3891688)Instructions burned: 158 (million)
% 12.86/2.66 % (3891689)Instruction limit reached!
% 12.86/2.66 % (3891689)------------------------------
% 12.86/2.66 % (3891689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.86/2.66 % (3891689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.86/2.66 % (3891689)CaDiCaL version: 2.1.3
% 12.86/2.66 % (3891689)Termination reason: Instruction limit
% 12.86/2.66 % (3891689)Termination phase: Saturation
% 12.86/2.66 % (3891689)Time elapsed: 0.135 s
% 12.86/2.66 % (3891689)Peak memory usage: 94 MB
% 12.86/2.66 % (3891689)Instructions burned: 325 (million)
% 12.86/2.66 % (3891687)Instruction limit reached!
% 12.86/2.66 % (3891687)------------------------------
% 12.86/2.66 % (3891687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.86/2.66 % (3891687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.86/2.66 % (3891687)CaDiCaL version: 2.1.3
% 12.86/2.66 % (3891687)Termination reason: Instruction limit
% 12.86/2.66 % (3891687)Termination phase: Saturation
% 12.86/2.66 % (3891687)Time elapsed: 0.193 s
% 12.86/2.66 % (3891687)Peak memory usage: 98 MB
% 12.86/2.66 % (3891687)Instructions burned: 285 (million)
% 12.86/2.66 % (3891693)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=3983453009:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 12.86/2.66 % (3891694)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3504536032:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 12.86/2.66 % (3891695)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3564996195:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 12.86/2.66 % (3891693)Instruction limit reached!
% 12.86/2.66 % (3891693)------------------------------
% 12.86/2.66 % (3891693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.86/2.66 % (3891693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.86/2.66 % (3891693)CaDiCaL version: 2.1.3
% 12.86/2.66 % (3891693)Termination reason: Instruction limit
% 12.86/2.66 % (3891693)Termination phase: Property scanning
% 12.86/2.66 % (3891693)Time elapsed: 0.144 s
% 12.86/2.66 % (3891693)Peak memory usage: 98 MB
% 12.86/2.66 % (3891693)Instructions burned: 251 (million)
% 12.86/2.66 % (3891696)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3843577547:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 12.86/2.66 % (3891694)Instruction limit reached!
% 12.86/2.66 % (3891694)------------------------------
% 12.86/2.66 % (3891694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.86/2.66 % (3891694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.86/2.66 % (3891694)CaDiCaL version: 2.1.3
% 12.86/2.66 % (3891694)Termination reason: Instruction limit
% 12.86/2.66 % (3891694)Termination phase: Saturation
% 12.86/2.66 % (3891694)Time elapsed: 0.169 s
% 12.86/2.66 % (3891694)Peak memory usage: 98 MB
% 12.86/2.66 % (3891694)Instructions burned: 296 (million)
% 12.86/2.66 % (3891696)Instruction limit reached!
% 12.86/2.66 % (3891696)------------------------------
% 12.86/2.66 % (3891696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.86/2.66 % (3891696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.86/2.66 % (3891696)CaDiCaL version: 2.1.3
% 12.86/2.66 % (3891696)Termination reason: Instruction limit
% 12.86/2.66 % (3891696)Termination phase: Function definition elimination
% 12.86/2.66 % (3891696)Time elapsed: 0.076 s
% 12.86/2.66 % (3891696)Peak memory usage: 94 MB
% 12.86/2.66 % (3891696)Instructions burned: 114 (million)
% 12.86/2.66 % (3891700)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1584431523:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 12.86/2.66 % (3891702)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2767777439:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2989 on theBenchmark for (2989ds/114Mi)
% 12.86/2.66 % (3891703)lrs+10_1_sil=8000:sp=occurrence:random_seed=2586531020:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 12.86/2.66 % (3891700)Instruction limit reached!
% 12.86/2.66 % (3891700)------------------------------
% 12.86/2.66 % (3891700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.86/2.66 % (3891700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.86/2.66 % (3891700)CaDiCaL version: 2.1.3
% 12.86/2.66 % (3891700)Termination reason: Instruction limit
% 12.86/2.66 % (3891700)Termination phase: Preprocessing 3
% 12.86/2.66 % (3891700)Time elapsed: 0.085 s
% 12.86/2.66 % (3891700)Peak memory usage: 96 MB
% 12.86/2.66 % (3891700)Instructions burned: 127 (million)
% 12.86/2.66 % (3891702)Instruction limit reached!
% 12.86/2.66 % (3891702)------------------------------
% 12.86/2.66 % (3891702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.86/2.66 % (3891702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.86/2.66 % (3891702)CaDiCaL version: 2.1.3
% 12.86/2.66 % (3891702)Termination reason: Instruction limit
% 12.86/2.66 % (3891702)Termination phase: Preprocessing 3
% 12.86/2.66 % (3891702)Time elapsed: 0.057 s
% 12.86/2.66 % (3891702)Peak memory usage: 91 MB
% 12.86/2.66 % (3891702)Instructions burned: 114 (million)
% 12.86/2.66 % (3891707)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2666812748:i=437:sd=1:aac=none:ss=included_2988 on theBenchmark for (2988ds/437Mi)
% 12.86/2.66 % (3891708)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2281383573:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi)
% 12.86/2.66 % (3891707)Instruction limit reached!
% 12.86/2.66 % (3891707)------------------------------
% 12.86/2.66 % (3891707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.86/2.66 % (3891707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.86/2.66 % (3891707)CaDiCaL version: 2.1.3
% 12.86/2.66 % (3891707)Termination reason: Instruction limit
% 12.86/2.66 % (3891707)Termination phase: Saturation
% 12.86/2.66 % (3891707)Time elapsed: 0.253 s
% 12.86/2.66 % (3891707)Peak memory usage: 98 MB
% 12.86/2.66 % (3891707)Instructions burned: 437 (million)
% 12.86/2.66 % (3891703)Instruction limit reached!
% 12.86/2.66 % (3891703)------------------------------
% 12.86/2.66 % (3891703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.86/2.66 % (3891703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.86/2.66 % (3891703)CaDiCaL version: 2.1.3
% 12.86/2.66 % (3891703)Termination reason: Instruction limit
% 12.86/2.66 % (3891703)Termination phase: Saturation
% 12.86/2.66 % (3891703)Time elapsed: 0.573 s
% 12.86/2.66 % (3891703)Peak memory usage: 106 MB
% 12.86/2.66 % (3891703)Instructions burned: 908 (million)
% 12.86/2.66 % (3891711)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2198796417:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2984 on theBenchmark for (2984ds/134Mi)
% 12.86/2.66 % (3891673)First to succeed.
% 12.86/2.66 % (3891673)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3891668"
% 12.86/2.66 % (3891711)Instruction limit reached!
% 12.86/2.66 % (3891711)------------------------------
% 12.86/2.66 % (3891711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.86/2.66 % (3891711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.86/2.66 % (3891711)CaDiCaL version: 2.1.3
% 12.86/2.66 % (3891711)Termination reason: Instruction limit
% 12.86/2.66 % (3891711)Termination phase: Saturation
% 12.86/2.66 % (3891711)Time elapsed: 0.083 s
% 12.86/2.66 % (3891711)Peak memory usage: 95 MB
% 12.86/2.66 % (3891711)Instructions burned: 134 (million)
% 12.86/2.66 % (3891712)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3635234458:st=8:i=592:sd=3:ep=RST:ss=axioms_2982 on theBenchmark for (2982ds/592Mi)
% 12.86/2.66 % (3891673)Refutation found. Thanks to Tanya!
% 12.86/2.66 % SZS status Theorem for theBenchmark
% 12.86/2.66 % SZS output start Proof for theBenchmark
% See solution above
% 13.67/2.85 % (3891673)------------------------------
% 13.67/2.85 % (3891673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.67/2.85 % (3891673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.67/2.85 % (3891673)CaDiCaL version: 2.1.3
% 13.67/2.85 % (3891673)Termination reason: Refutation
% 13.67/2.85 % (3891673)Time elapsed: 1.514 s
% 13.67/2.85 % (3891673)Peak memory usage: 240 MB
% 13.67/2.85 % (3891673)Instructions burned: 4487 (million)
% 13.67/2.85 % (3891673)------------------------------
% 13.67/2.85 % (3891673)------------------------------
% 13.67/2.85 % (3891668)Success in time 1.983 s
% 13.67/2.85 % Vampire exiting
%------------------------------------------------------------------------------