%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : TOP032+3 : 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 : n015.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:33:57 PM UTC 2026
% Result : Theorem 12.43s 4.66s
% Output : Refutation 24.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 27
% Syntax : Number of formulae : 290 ( 38 unt; 6 def)
% Number of atoms : 1344 ( 141 equ)
% Maximal formula atoms : 19 ( 4 avg)
% Number of connectives : 1784 ( 730 ~; 844 |; 140 &)
% ( 21 <=>; 49 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 6 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 25 ( 23 usr; 7 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 3 con; 0-4 aty)
% Number of variables : 382 ( 0 sgn 369 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f258,axiom,
! [X0] : k2_tarski(X0,X0) = k1_tarski(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f678,axiom,
! [X0,X1,X2] :
( ( r2_hidden(X0,X1)
& m1_subset_1(X1,k1_zfmisc_1(X2)) )
=> m1_subset_1(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
fof(f1394,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(f2016,axiom,
! [X0,X1,X2,X3] :
( ( ~ v1_xboole_0(X0)
& v1_funct_1(X2)
& v1_funct_2(X2,X0,X1)
& m1_relset_1(X2,X0,X1)
& m1_subset_1(X3,X0) )
=> m1_subset_1(k8_funct_2(X0,X1,X2,X3),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k8_funct_2) ).
fof(f2017,axiom,
! [X0,X1,X2,X3] :
( ( ~ v1_xboole_0(X0)
& v1_funct_1(X2)
& v1_funct_2(X2,X0,X1)
& m1_relset_1(X2,X0,X1)
& m1_subset_1(X3,X0) )
=> k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k8_funct_2) ).
fof(f6422,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f6435,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> k1_struct_0(X0,X1) = k1_tarski(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k1_struct_0) ).
fof(f6788,axiom,
! [X0] :
( l1_struct_0(X0)
=> k2_pre_topc(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_pre_topc) ).
fof(f6796,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> r2_hidden(X1,k2_pre_topc(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t13_pre_topc) ).
fof(f6850,axiom,
! [X0] :
( l1_pre_topc(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f11239,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& m1_pre_topc(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> m1_subset_1(X2,u1_struct_0(X0)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_topmetr) ).
fof(f13298,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_hidden(X2,k2_tex_4(X0,X1))
<=> k2_tex_4(X0,X2) = k2_tex_4(X0,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t23_tex_4) ).
fof(f13370,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> k4_tex_4(X0,X1) = k2_tex_4(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k4_tex_4) ).
fof(f13449,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ( X2 = u1_struct_0(X1)
=> ( v1_tsp_1(X2,X0)
<=> v2_t_0topsp(X1) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_tsp_1) ).
fof(f13459,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(f13461,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(f13472,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)))
=> ( v1_tsp_1(X1,X0)
<=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_hidden(X2,X1)
=> k5_subset_1(u1_struct_0(X0),X1,k4_tex_4(X0,X2)) = k1_struct_0(X0,X2) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_tsp_2) ).
fof(f13489,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(f13492,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& m2_tsp_1(X1,X0) )
=> ( v2_tsp_2(X1,X0)
<=> ( v2_t_0topsp(X1)
& ! [X2] :
( ( ~ v3_struct_0(X2)
& v2_t_0topsp(X2)
& m2_tsp_1(X2,X0) )
=> ( m2_tsp_1(X1,X2)
=> g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1)) = g1_pre_topc(u1_struct_0(X2),u1_pre_topc(X2)) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_tsp_2) ).
fof(f13508,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))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
=> ( ( X3 = u1_struct_0(X1)
& ! [X4] :
( m1_subset_1(X4,u1_struct_0(X0))
=> k5_subset_1(u1_struct_0(X0),X3,k4_tex_4(X0,X4)) = k1_struct_0(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X4)) ) )
=> ( 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)) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t18_tsp_2) ).
fof(f13509,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] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> r2_hidden(k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X3),k4_tex_4(X0,X3)) )
=> ( 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)) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t19_tsp_2) ).
fof(f13510,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] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> r2_hidden(k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X3),k4_tex_4(X0,X3)) )
=> ( 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)) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f13509]) ).
fof(f13570,plain,
! [X0] :
( ! [X1] :
( ( v1_tsp_1(X1,X0)
<=> ! [X2] :
( k5_subset_1(u1_struct_0(X0),X1,k4_tex_4(X0,X2)) = k1_struct_0(X0,X2)
| ~ r2_hidden(X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(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,[],[f13472]) ).
fof(f13571,plain,
! [X0] :
( ! [X1] :
( ( v1_tsp_1(X1,X0)
<=> ! [X2] :
( k5_subset_1(u1_struct_0(X0),X1,k4_tex_4(X0,X2)) = k1_struct_0(X0,X2)
| ~ r2_hidden(X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(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,[],[f13570]) ).
fof(f13604,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,[],[f13489]) ).
fof(f13605,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,[],[f13604]) ).
fof(f13610,plain,
! [X0] :
( ! [X1] :
( ( v2_tsp_2(X1,X0)
<=> ( v2_t_0topsp(X1)
& ! [X2] :
( g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1)) = g1_pre_topc(u1_struct_0(X2),u1_pre_topc(X2))
| ~ m2_tsp_1(X1,X2)
| v3_struct_0(X2)
| ~ v2_t_0topsp(X2)
| ~ m2_tsp_1(X2,X0) ) ) )
| v3_struct_0(X1)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13492]) ).
fof(f13611,plain,
! [X0] :
( ! [X1] :
( ( v2_tsp_2(X1,X0)
<=> ( v2_t_0topsp(X1)
& ! [X2] :
( g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1)) = g1_pre_topc(u1_struct_0(X2),u1_pre_topc(X2))
| ~ m2_tsp_1(X1,X2)
| v3_struct_0(X2)
| ~ v2_t_0topsp(X2)
| ~ m2_tsp_1(X2,X0) ) ) )
| v3_struct_0(X1)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f13610]) ).
fof(f13642,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( 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)) )
| u1_struct_0(X1) != X3
| ? [X4] :
( k5_subset_1(u1_struct_0(X0),X3,k4_tex_4(X0,X4)) != k1_struct_0(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X4))
& m1_subset_1(X4,u1_struct_0(X0)) )
| ~ 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))
| ~ 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,[],[f13508]) ).
fof(f13643,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( 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)) )
| u1_struct_0(X1) != X3
| ? [X4] :
( k5_subset_1(u1_struct_0(X0),X3,k4_tex_4(X0,X4)) != k1_struct_0(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X4))
& m1_subset_1(X4,u1_struct_0(X0)) )
| ~ 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))
| ~ 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,[],[f13642]) ).
fof(f13644,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
& ! [X3] :
( r2_hidden(k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X3),k4_tex_4(X0,X3))
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(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,[],[f13510]) ).
fof(f13645,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
& ! [X3] :
( r2_hidden(k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X3),k4_tex_4(X0,X3))
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(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,[],[f13644]) ).
fof(f13654,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ m1_pre_topc(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f11239]) ).
fof(f13655,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ m1_pre_topc(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f13654]) ).
fof(f13703,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(ennf_transformation,[],[f678]) ).
fof(f13704,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(flattening,[],[f13703]) ).
fof(f13715,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v1_tsp_1(X2,X0)
<=> v2_t_0topsp(X1) )
| u1_struct_0(X1) != X2
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X1)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13449]) ).
fof(f13716,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v1_tsp_1(X2,X0)
<=> v2_t_0topsp(X1) )
| u1_struct_0(X1) != X2
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X1)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f13715]) ).
fof(f13747,plain,
! [X0,X1] :
( k4_tex_4(X0,X1) = k2_tex_4(X0,X1)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f13370]) ).
fof(f13748,plain,
! [X0,X1] :
( k4_tex_4(X0,X1) = k2_tex_4(X0,X1)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f13747]) ).
fof(f13782,plain,
! [X0,X1] :
( k1_struct_0(X0,X1) = k1_tarski(X1)
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f6435]) ).
fof(f13783,plain,
! [X0,X1] :
( k1_struct_0(X0,X1) = k1_tarski(X1)
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f13782]) ).
fof(f14155,plain,
! [X0] :
( ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13461]) ).
fof(f14157,plain,
! [X0] :
( ! [X1] :
( l1_pre_topc(X1)
| ~ m2_tsp_1(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13459]) ).
fof(f14403,plain,
! [X0,X1,X2,X3] :
( k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(ennf_transformation,[],[f2017]) ).
fof(f14404,plain,
! [X0,X1,X2,X3] :
( k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(flattening,[],[f14403]) ).
fof(f14405,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k8_funct_2(X0,X1,X2,X3),X1)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(ennf_transformation,[],[f2016]) ).
fof(f14406,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k8_funct_2(X0,X1,X2,X3),X1)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(flattening,[],[f14405]) ).
fof(f14525,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X2,k2_tex_4(X0,X1))
<=> k2_tex_4(X0,X2) = k2_tex_4(X0,X1) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13298]) ).
fof(f14526,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X2,k2_tex_4(X0,X1))
<=> k2_tex_4(X0,X2) = k2_tex_4(X0,X1) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f14525]) ).
fof(f14765,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f6850]) ).
fof(f14769,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f6422]) ).
fof(f14770,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f14769]) ).
fof(f15069,plain,
! [X0] :
( ! [X1] :
( r2_hidden(X1,k2_pre_topc(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f6796]) ).
fof(f15070,plain,
! [X0] :
( ! [X1] :
( r2_hidden(X1,k2_pre_topc(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f15069]) ).
fof(f15072,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f6788]) ).
fof(f17059,plain,
! [X0] :
( ! [X1] :
( ( ( v1_tsp_1(X1,X0)
| ? [X2] :
( k1_struct_0(X0,X2) != k5_subset_1(u1_struct_0(X0),X1,k4_tex_4(X0,X2))
& r2_hidden(X2,X1)
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X2] :
( k5_subset_1(u1_struct_0(X0),X1,k4_tex_4(X0,X2)) = k1_struct_0(X0,X2)
| ~ r2_hidden(X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ v1_tsp_1(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(nnf_transformation,[],[f13571]) ).
fof(f17060,plain,
! [X0] :
( ! [X1] :
( ( ( v1_tsp_1(X1,X0)
| ? [X2] :
( k1_struct_0(X0,X2) != k5_subset_1(u1_struct_0(X0),X1,k4_tex_4(X0,X2))
& r2_hidden(X2,X1)
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X3] :
( k1_struct_0(X0,X3) = k5_subset_1(u1_struct_0(X0),X1,k4_tex_4(X0,X3))
| ~ r2_hidden(X3,X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ v1_tsp_1(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(rectify,[],[f17059]) ).
fof(f17061,plain,
! [X0] :
( ! [X1] :
( ( ( v1_tsp_1(X1,X0)
| ( k1_struct_0(X0,sK34(X0,X1)) != k5_subset_1(u1_struct_0(X0),X1,k4_tex_4(X0,sK34(X0,X1)))
& r2_hidden(sK34(X0,X1),X1)
& m1_subset_1(sK34(X0,X1),u1_struct_0(X0)) ) )
& ( ! [X3] :
( k1_struct_0(X0,X3) = k5_subset_1(u1_struct_0(X0),X1,k4_tex_4(X0,X3))
| ~ r2_hidden(X3,X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ v1_tsp_1(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(skolemize,[status(esa),new_symbols(skolem,[sK34]),skolemize(X2,sK34(X0,X1))],[f17060]) ).
fof(f17080,plain,
! [X0] :
( ! [X1] :
( ( ( v2_tsp_2(X1,X0)
| ~ v2_t_0topsp(X1)
| ? [X2] :
( g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1)) != g1_pre_topc(u1_struct_0(X2),u1_pre_topc(X2))
& m2_tsp_1(X1,X2)
& ~ v3_struct_0(X2)
& v2_t_0topsp(X2)
& m2_tsp_1(X2,X0) ) )
& ( ( v2_t_0topsp(X1)
& ! [X2] :
( g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1)) = g1_pre_topc(u1_struct_0(X2),u1_pre_topc(X2))
| ~ m2_tsp_1(X1,X2)
| v3_struct_0(X2)
| ~ v2_t_0topsp(X2)
| ~ m2_tsp_1(X2,X0) ) )
| ~ v2_tsp_2(X1,X0) ) )
| v3_struct_0(X1)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f13611]) ).
fof(f17081,plain,
! [X0] :
( ! [X1] :
( ( ( v2_tsp_2(X1,X0)
| ~ v2_t_0topsp(X1)
| ? [X2] :
( g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1)) != g1_pre_topc(u1_struct_0(X2),u1_pre_topc(X2))
& m2_tsp_1(X1,X2)
& ~ v3_struct_0(X2)
& v2_t_0topsp(X2)
& m2_tsp_1(X2,X0) ) )
& ( ( v2_t_0topsp(X1)
& ! [X2] :
( g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1)) = g1_pre_topc(u1_struct_0(X2),u1_pre_topc(X2))
| ~ m2_tsp_1(X1,X2)
| v3_struct_0(X2)
| ~ v2_t_0topsp(X2)
| ~ m2_tsp_1(X2,X0) ) )
| ~ v2_tsp_2(X1,X0) ) )
| v3_struct_0(X1)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f17080]) ).
fof(f17082,plain,
! [X0] :
( ! [X1] :
( ( ( v2_tsp_2(X1,X0)
| ~ v2_t_0topsp(X1)
| ? [X2] :
( g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1)) != g1_pre_topc(u1_struct_0(X2),u1_pre_topc(X2))
& m2_tsp_1(X1,X2)
& ~ v3_struct_0(X2)
& v2_t_0topsp(X2)
& m2_tsp_1(X2,X0) ) )
& ( ( v2_t_0topsp(X1)
& ! [X3] :
( g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1)) = g1_pre_topc(u1_struct_0(X3),u1_pre_topc(X3))
| ~ m2_tsp_1(X1,X3)
| v3_struct_0(X3)
| ~ v2_t_0topsp(X3)
| ~ m2_tsp_1(X3,X0) ) )
| ~ v2_tsp_2(X1,X0) ) )
| v3_struct_0(X1)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(rectify,[],[f17081]) ).
fof(f17083,plain,
! [X0] :
( ! [X1] :
( ( ( v2_tsp_2(X1,X0)
| ~ v2_t_0topsp(X1)
| ( g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1)) != g1_pre_topc(u1_struct_0(sK43(X0,X1)),u1_pre_topc(sK43(X0,X1)))
& m2_tsp_1(X1,sK43(X0,X1))
& ~ v3_struct_0(sK43(X0,X1))
& v2_t_0topsp(sK43(X0,X1))
& m2_tsp_1(sK43(X0,X1),X0) ) )
& ( ( v2_t_0topsp(X1)
& ! [X3] :
( g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1)) = g1_pre_topc(u1_struct_0(X3),u1_pre_topc(X3))
| ~ m2_tsp_1(X1,X3)
| v3_struct_0(X3)
| ~ v2_t_0topsp(X3)
| ~ m2_tsp_1(X3,X0) ) )
| ~ v2_tsp_2(X1,X0) ) )
| v3_struct_0(X1)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK43]),skolemize(X2,sK43(X0,X1))],[f17082]) ).
fof(f17099,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( 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)) )
| u1_struct_0(X1) != X3
| ( k5_subset_1(u1_struct_0(X0),X3,k4_tex_4(X0,sK49(X0,X1,X2,X3))) != k1_struct_0(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,sK49(X0,X1,X2,X3)))
& m1_subset_1(sK49(X0,X1,X2,X3),u1_struct_0(X0)) )
| ~ 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))
| ~ 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,[sK49]),skolemize(X4,sK49(X0,X1,X2,X3))],[f13643]) ).
fof(f17100,plain,
( ( ~ v1_funct_1(sK52)
| ~ v1_funct_2(sK52,u1_struct_0(sK50),u1_struct_0(sK51))
| ~ v5_pre_topc(sK52,sK50,sK51)
| ~ m2_relset_1(sK52,u1_struct_0(sK50),u1_struct_0(sK51)) )
& ! [X3] :
( r2_hidden(k8_funct_2(u1_struct_0(sK50),u1_struct_0(sK51),sK52,X3),k4_tex_4(sK50,X3))
| ~ m1_subset_1(X3,u1_struct_0(sK50)) )
& v1_funct_1(sK52)
& v1_funct_2(sK52,u1_struct_0(sK50),u1_struct_0(sK51))
& m2_relset_1(sK52,u1_struct_0(sK50),u1_struct_0(sK51))
& ~ v3_struct_0(sK51)
& v2_tsp_2(sK51,sK50)
& m2_tsp_1(sK51,sK50)
& ~ v3_struct_0(sK50)
& v2_pre_topc(sK50)
& l1_pre_topc(sK50) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK50,sK51,sK52]),skolemize(X0,sK50),skolemize(X1,sK51),skolemize(X2,sK52)],[f13645]) ).
fof(f17135,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v1_tsp_1(X2,X0)
| ~ v2_t_0topsp(X1) )
& ( v2_t_0topsp(X1)
| ~ v1_tsp_1(X2,X0) ) )
| u1_struct_0(X1) != X2
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X1)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f13716]) ).
fof(f17275,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,[],[f14155]) ).
fof(f17391,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,[],[f1394]) ).
fof(f17409,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( r2_hidden(X2,k2_tex_4(X0,X1))
| k2_tex_4(X0,X1) != k2_tex_4(X0,X2) )
& ( k2_tex_4(X0,X2) = k2_tex_4(X0,X1)
| ~ r2_hidden(X2,k2_tex_4(X0,X1)) ) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f14526]) ).
fof(f18301,plain,
! [X3,X0,X1] :
( k1_struct_0(X0,X3) = k5_subset_1(u1_struct_0(X0),X1,k4_tex_4(X0,X3))
| ~ r2_hidden(X3,X1)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ v1_tsp_1(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,[],[f17061]) ).
fof(f18345,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,[],[f13605]) ).
fof(f18351,plain,
! [X0,X1] :
( ~ v2_pre_topc(X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| v2_t_0topsp(X1)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f17083]) ).
fof(f18407,plain,
! [X2,X3,X0,X1] :
( v5_pre_topc(X2,X0,X1)
| u1_struct_0(X1) != X3
| m1_subset_1(sK49(X0,X1,X2,X3),u1_struct_0(X0))
| ~ 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))
| ~ 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,[],[f17099]) ).
fof(f18408,plain,
! [X2,X3,X0,X1] :
( v5_pre_topc(X2,X0,X1)
| u1_struct_0(X1) != X3
| k5_subset_1(u1_struct_0(X0),X3,k4_tex_4(X0,sK49(X0,X1,X2,X3))) != k1_struct_0(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,sK49(X0,X1,X2,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))
| ~ 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,[],[f17099]) ).
fof(f18413,plain,
l1_pre_topc(sK50),
inference(cnf_transformation,[],[f17100]) ).
fof(f18414,plain,
v2_pre_topc(sK50),
inference(cnf_transformation,[],[f17100]) ).
fof(f18415,plain,
~ v3_struct_0(sK50),
inference(cnf_transformation,[],[f17100]) ).
fof(f18416,plain,
m2_tsp_1(sK51,sK50),
inference(cnf_transformation,[],[f17100]) ).
fof(f18417,plain,
v2_tsp_2(sK51,sK50),
inference(cnf_transformation,[],[f17100]) ).
fof(f18418,plain,
~ v3_struct_0(sK51),
inference(cnf_transformation,[],[f17100]) ).
fof(f18419,plain,
m2_relset_1(sK52,u1_struct_0(sK50),u1_struct_0(sK51)),
inference(cnf_transformation,[],[f17100]) ).
fof(f18420,plain,
v1_funct_2(sK52,u1_struct_0(sK50),u1_struct_0(sK51)),
inference(cnf_transformation,[],[f17100]) ).
fof(f18421,plain,
v1_funct_1(sK52),
inference(cnf_transformation,[],[f17100]) ).
fof(f18422,plain,
! [X3] :
( r2_hidden(k8_funct_2(u1_struct_0(sK50),u1_struct_0(sK51),sK52,X3),k4_tex_4(sK50,X3))
| ~ m1_subset_1(X3,u1_struct_0(sK50)) ),
inference(cnf_transformation,[],[f17100]) ).
fof(f18423,plain,
( ~ v1_funct_1(sK52)
| ~ v1_funct_2(sK52,u1_struct_0(sK50),u1_struct_0(sK51))
| ~ v5_pre_topc(sK52,sK50,sK51)
| ~ m2_relset_1(sK52,u1_struct_0(sK50),u1_struct_0(sK51)) ),
inference(cnf_transformation,[],[f17100]) ).
fof(f18432,plain,
! [X2,X0,X1] :
( ~ v2_pre_topc(X0)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| v3_struct_0(X1)
| ~ m1_pre_topc(X1,X0)
| v3_struct_0(X0)
| m1_subset_1(X2,u1_struct_0(X0))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f13655]) ).
fof(f18526,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(cnf_transformation,[],[f13704]) ).
fof(f18545,plain,
! [X2,X0,X1] :
( v1_tsp_1(X2,X0)
| ~ v2_t_0topsp(X1)
| u1_struct_0(X1) != X2
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X1)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f17135]) ).
fof(f18635,plain,
! [X0,X1] :
( ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| k2_tex_4(X0,X1) = k4_tex_4(X0,X1)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f13748]) ).
fof(f18661,plain,
! [X0,X1] :
( k1_tarski(X1) = k1_struct_0(X0,X1)
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f13783]) ).
fof(f19118,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ m2_tsp_1(X1,X0)
| m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f17275]) ).
fof(f19121,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ m2_tsp_1(X1,X0)
| l1_pre_topc(X1) ),
inference(cnf_transformation,[],[f14157]) ).
fof(f19661,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_1(X2)
| v1_xboole_0(X0)
| k1_funct_1(X2,X3) = k8_funct_2(X0,X1,X2,X3)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(cnf_transformation,[],[f14404]) ).
fof(f19662,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k8_funct_2(X0,X1,X2,X3),X1)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(cnf_transformation,[],[f14406]) ).
fof(f19670,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f17391]) ).
fof(f19832,plain,
! [X2,X0,X1] :
( ~ l1_pre_topc(X0)
| ~ r2_hidden(X2,k2_tex_4(X0,X1))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| k2_tex_4(X0,X1) = k2_tex_4(X0,X2) ),
inference(cnf_transformation,[],[f17409]) ).
fof(f20201,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f14765]) ).
fof(f20207,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f14770]) ).
fof(f20763,plain,
! [X0,X1] :
( ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| r2_hidden(X1,k2_pre_topc(X0)) ),
inference(cnf_transformation,[],[f15070]) ).
fof(f20765,plain,
! [X0] :
( ~ l1_struct_0(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(cnf_transformation,[],[f15072]) ).
fof(f21362,plain,
! [X0] : k1_tarski(X0) = k2_tarski(X0,X0),
inference(cnf_transformation,[],[f258]) ).
fof(f23579,plain,
! [X0,X1] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| k1_struct_0(X0,X1) = k2_tarski(X1,X1)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(definition_unfolding,[],[f18661,f21362]) ).
fof(f24481,plain,
! [X2,X0,X1] :
( ~ v2_pre_topc(X0)
| k5_subset_1(u1_struct_0(X0),u1_struct_0(X1),k4_tex_4(X0,sK49(X0,X1,X2,u1_struct_0(X1)))) != k1_struct_0(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,sK49(X0,X1,X2,u1_struct_0(X1))))
| ~ m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(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)
| v5_pre_topc(X2,X0,X1)
| ~ l1_pre_topc(X0) ),
inference(equality_resolution,[],[f18408]) ).
fof(f24482,plain,
! [X2,X0,X1] :
( ~ v2_pre_topc(X0)
| m1_subset_1(sK49(X0,X1,X2,u1_struct_0(X1)),u1_struct_0(X0))
| ~ m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(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)
| v5_pre_topc(X2,X0,X1)
| ~ l1_pre_topc(X0) ),
inference(equality_resolution,[],[f18407]) ).
fof(f24487,plain,
! [X0,X1] :
( ~ v2_t_0topsp(X1)
| v1_tsp_1(u1_struct_0(X1),X0)
| ~ m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X1)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(equality_resolution,[],[f18545]) ).
fof(f25351,plain,
( ~ v1_funct_2(sK52,u1_struct_0(sK50),u1_struct_0(sK51))
| ~ v5_pre_topc(sK52,sK50,sK51)
| ~ m2_relset_1(sK52,u1_struct_0(sK50),u1_struct_0(sK51)) ),
inference(forward_subsumption_resolution,[],[f18423,f18421]) ).
fof(f25367,plain,
! [X3,X0,X1] :
( ~ v2_pre_topc(X0)
| ~ r2_hidden(X3,X1)
| ~ v1_tsp_1(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| k1_struct_0(X0,X3) = k5_subset_1(u1_struct_0(X0),X1,k4_tex_4(X0,X3))
| ~ l1_pre_topc(X0) ),
inference(forward_subsumption_resolution,[],[f18301,f18526]) ).
fof(f25484,plain,
( ~ v5_pre_topc(sK52,sK50,sK51)
| ~ m2_relset_1(sK52,u1_struct_0(sK50),u1_struct_0(sK51)) ),
inference(forward_subsumption_resolution,[],[f25351,f18420]) ).
fof(f25535,plain,
~ v5_pre_topc(sK52,sK50,sK51),
inference(forward_subsumption_resolution,[],[f25484,f18419]) ).
fof(f25563,plain,
m1_relset_1(sK52,u1_struct_0(sK50),u1_struct_0(sK51)),
inference(resolution,[],[f19670,f18419]) ).
fof(f25565,plain,
! [X0] :
( ~ m2_tsp_1(X0,sK50)
| l1_pre_topc(X0) ),
inference(resolution,[],[f19121,f18413]) ).
fof(f25566,plain,
! [X0] :
( ~ m2_tsp_1(X0,sK50)
| m1_pre_topc(X0,sK50) ),
inference(resolution,[],[f19118,f18413]) ).
fof(f25567,plain,
m1_pre_topc(sK51,sK50),
inference(resolution,[],[f25566,f18416]) ).
fof(f25568,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(sK52,X0,X2)
| k1_funct_1(sK52,X1) = k8_funct_2(X0,X2,sK52,X1)
| v1_xboole_0(X0)
| ~ m1_relset_1(sK52,X0,X2)
| ~ m1_subset_1(X1,X0) ),
inference(resolution,[],[f19661,f18421]) ).
fof(f25569,plain,
l1_pre_topc(sK51),
inference(resolution,[],[f25565,f18416]) ).
fof(f25574,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(resolution,[],[f20765,f20201]) ).
fof(f25575,plain,
u1_struct_0(sK50) = k2_pre_topc(sK50),
inference(resolution,[],[f25574,f18413]) ).
fof(f25576,plain,
u1_struct_0(sK51) = k2_pre_topc(sK51),
inference(resolution,[],[f25574,f25569]) ).
fof(f25577,plain,
m1_relset_1(sK52,k2_pre_topc(sK50),u1_struct_0(sK51)),
inference(superposition,[],[f25563,f25575]) ).
fof(f25578,plain,
! [X0] :
( r2_hidden(k8_funct_2(k2_pre_topc(sK50),u1_struct_0(sK51),sK52,X0),k4_tex_4(sK50,X0))
| ~ m1_subset_1(X0,k2_pre_topc(sK50)) ),
inference(superposition,[],[f18422,f25575]) ).
fof(f25579,plain,
m2_relset_1(sK52,k2_pre_topc(sK50),u1_struct_0(sK51)),
inference(superposition,[],[f18419,f25575]) ).
fof(f25580,plain,
v1_funct_2(sK52,k2_pre_topc(sK50),u1_struct_0(sK51)),
inference(superposition,[],[f18420,f25575]) ).
fof(f25581,plain,
! [X0] :
( m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK50)))
| ~ m2_tsp_1(X0,sK50)
| v3_struct_0(sK50)
| ~ l1_pre_topc(sK50) ),
inference(superposition,[],[f18345,f25575]) ).
fof(f25597,plain,
! [X0] :
( m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK50)))
| ~ m2_tsp_1(X0,sK50)
| ~ l1_pre_topc(sK50) ),
inference(forward_subsumption_resolution,[],[f25581,f18415]) ).
fof(f25598,plain,
v1_funct_2(sK52,k2_pre_topc(sK50),k2_pre_topc(sK51)),
inference(forward_demodulation,[],[f25580,f25576]) ).
fof(f25599,plain,
m2_relset_1(sK52,k2_pre_topc(sK50),k2_pre_topc(sK51)),
inference(forward_demodulation,[],[f25579,f25576]) ).
fof(f25600,plain,
! [X0] :
( r2_hidden(k8_funct_2(k2_pre_topc(sK50),k2_pre_topc(sK51),sK52,X0),k4_tex_4(sK50,X0))
| ~ m1_subset_1(X0,k2_pre_topc(sK50)) ),
inference(forward_demodulation,[],[f25578,f25576]) ).
fof(f25601,plain,
m1_relset_1(sK52,k2_pre_topc(sK50),k2_pre_topc(sK51)),
inference(forward_demodulation,[],[f25577,f25576]) ).
fof(f25603,plain,
! [X0] :
( ~ m2_tsp_1(X0,sK50)
| m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK50))) ),
inference(forward_subsumption_resolution,[],[f25597,f18413]) ).
fof(f25634,plain,
! [X0] :
( v3_struct_0(sK50)
| k4_tex_4(sK50,X0) = k2_tex_4(sK50,X0)
| ~ l1_pre_topc(sK50)
| ~ m1_subset_1(X0,u1_struct_0(sK50)) ),
inference(resolution,[],[f18635,f18414]) ).
fof(f25635,plain,
! [X0] :
( k4_tex_4(sK50,X0) = k2_tex_4(sK50,X0)
| ~ l1_pre_topc(sK50)
| ~ m1_subset_1(X0,u1_struct_0(sK50)) ),
inference(forward_subsumption_resolution,[],[f25634,f18415]) ).
fof(f25636,plain,
! [X0] :
( k4_tex_4(sK50,X0) = k2_tex_4(sK50,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK50)) ),
inference(forward_subsumption_resolution,[],[f25635,f18413]) ).
fof(f25637,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(sK50))
| k4_tex_4(sK50,X0) = k2_tex_4(sK50,X0) ),
inference(forward_demodulation,[],[f25636,f25575]) ).
fof(f25644,plain,
! [X0,X1] :
( k5_subset_1(u1_struct_0(sK50),u1_struct_0(X0),k4_tex_4(sK50,sK49(sK50,X0,X1,u1_struct_0(X0)))) != k1_struct_0(X0,k8_funct_2(u1_struct_0(sK50),u1_struct_0(X0),X1,sK49(sK50,X0,X1,u1_struct_0(X0))))
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(sK50)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK50),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK50),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK50)
| ~ m2_tsp_1(X0,sK50)
| v3_struct_0(sK50)
| v5_pre_topc(X1,sK50,X0)
| ~ l1_pre_topc(sK50) ),
inference(resolution,[],[f24481,f18414]) ).
fof(f25645,plain,
! [X0,X1] :
( k5_subset_1(u1_struct_0(sK50),u1_struct_0(X0),k4_tex_4(sK50,sK49(sK50,X0,X1,u1_struct_0(X0)))) != k1_struct_0(X0,k8_funct_2(u1_struct_0(sK50),u1_struct_0(X0),X1,sK49(sK50,X0,X1,u1_struct_0(X0))))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK50),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK50),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK50)
| ~ m2_tsp_1(X0,sK50)
| v3_struct_0(sK50)
| v5_pre_topc(X1,sK50,X0)
| ~ l1_pre_topc(sK50) ),
inference(forward_subsumption_resolution,[],[f25644,f18345]) ).
fof(f25646,plain,
! [X0,X1] :
( k5_subset_1(u1_struct_0(sK50),u1_struct_0(X0),k4_tex_4(sK50,sK49(sK50,X0,X1,u1_struct_0(X0)))) != k1_struct_0(X0,k8_funct_2(u1_struct_0(sK50),u1_struct_0(X0),X1,sK49(sK50,X0,X1,u1_struct_0(X0))))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK50),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK50),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK50)
| ~ m2_tsp_1(X0,sK50)
| v5_pre_topc(X1,sK50,X0)
| ~ l1_pre_topc(sK50) ),
inference(forward_subsumption_resolution,[],[f25645,f18415]) ).
fof(f25647,plain,
! [X0,X1] :
( k5_subset_1(u1_struct_0(sK50),u1_struct_0(X0),k4_tex_4(sK50,sK49(sK50,X0,X1,u1_struct_0(X0)))) != k1_struct_0(X0,k8_funct_2(u1_struct_0(sK50),u1_struct_0(X0),X1,sK49(sK50,X0,X1,u1_struct_0(X0))))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK50),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK50),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK50)
| ~ m2_tsp_1(X0,sK50)
| v5_pre_topc(X1,sK50,X0) ),
inference(forward_subsumption_resolution,[],[f25646,f18413]) ).
fof(f25648,plain,
! [X0,X1] :
( k5_subset_1(k2_pre_topc(sK50),u1_struct_0(X0),k4_tex_4(sK50,sK49(sK50,X0,X1,u1_struct_0(X0)))) != k1_struct_0(X0,k8_funct_2(k2_pre_topc(sK50),u1_struct_0(X0),X1,sK49(sK50,X0,X1,u1_struct_0(X0))))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK50),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK50),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK50)
| ~ m2_tsp_1(X0,sK50)
| v5_pre_topc(X1,sK50,X0) ),
inference(forward_demodulation,[],[f25647,f25575]) ).
fof(f25649,plain,
! [X0,X1] :
( ~ v1_funct_2(X1,k2_pre_topc(sK50),u1_struct_0(X0))
| k5_subset_1(k2_pre_topc(sK50),u1_struct_0(X0),k4_tex_4(sK50,sK49(sK50,X0,X1,u1_struct_0(X0)))) != k1_struct_0(X0,k8_funct_2(k2_pre_topc(sK50),u1_struct_0(X0),X1,sK49(sK50,X0,X1,u1_struct_0(X0))))
| ~ v1_funct_1(X1)
| ~ m2_relset_1(X1,u1_struct_0(sK50),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK50)
| ~ m2_tsp_1(X0,sK50)
| v5_pre_topc(X1,sK50,X0) ),
inference(forward_demodulation,[],[f25648,f25575]) ).
fof(f25650,plain,
! [X0,X1] :
( ~ v2_tsp_2(X0,sK50)
| ~ v1_funct_2(X1,k2_pre_topc(sK50),u1_struct_0(X0))
| k5_subset_1(k2_pre_topc(sK50),u1_struct_0(X0),k4_tex_4(sK50,sK49(sK50,X0,X1,u1_struct_0(X0)))) != k1_struct_0(X0,k8_funct_2(k2_pre_topc(sK50),u1_struct_0(X0),X1,sK49(sK50,X0,X1,u1_struct_0(X0))))
| ~ v1_funct_1(X1)
| v3_struct_0(X0)
| ~ m2_relset_1(X1,k2_pre_topc(sK50),u1_struct_0(X0))
| ~ m2_tsp_1(X0,sK50)
| v5_pre_topc(X1,sK50,X0) ),
inference(forward_demodulation,[],[f25649,f25575]) ).
fof(f25651,plain,
! [X0] :
( ~ v1_funct_2(X0,k2_pre_topc(sK50),u1_struct_0(sK51))
| k5_subset_1(k2_pre_topc(sK50),u1_struct_0(sK51),k4_tex_4(sK50,sK49(sK50,sK51,X0,u1_struct_0(sK51)))) != k1_struct_0(sK51,k8_funct_2(k2_pre_topc(sK50),u1_struct_0(sK51),X0,sK49(sK50,sK51,X0,u1_struct_0(sK51))))
| ~ v1_funct_1(X0)
| v3_struct_0(sK51)
| ~ m2_relset_1(X0,k2_pre_topc(sK50),u1_struct_0(sK51))
| ~ m2_tsp_1(sK51,sK50)
| v5_pre_topc(X0,sK50,sK51) ),
inference(resolution,[],[f25650,f18417]) ).
fof(f25652,plain,
! [X0] :
( ~ v1_funct_2(X0,k2_pre_topc(sK50),u1_struct_0(sK51))
| k5_subset_1(k2_pre_topc(sK50),u1_struct_0(sK51),k4_tex_4(sK50,sK49(sK50,sK51,X0,u1_struct_0(sK51)))) != k1_struct_0(sK51,k8_funct_2(k2_pre_topc(sK50),u1_struct_0(sK51),X0,sK49(sK50,sK51,X0,u1_struct_0(sK51))))
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,k2_pre_topc(sK50),u1_struct_0(sK51))
| ~ m2_tsp_1(sK51,sK50)
| v5_pre_topc(X0,sK50,sK51) ),
inference(forward_subsumption_resolution,[],[f25651,f18418]) ).
fof(f25653,plain,
! [X0] :
( ~ v1_funct_2(X0,k2_pre_topc(sK50),u1_struct_0(sK51))
| k5_subset_1(k2_pre_topc(sK50),u1_struct_0(sK51),k4_tex_4(sK50,sK49(sK50,sK51,X0,u1_struct_0(sK51)))) != k1_struct_0(sK51,k8_funct_2(k2_pre_topc(sK50),u1_struct_0(sK51),X0,sK49(sK50,sK51,X0,u1_struct_0(sK51))))
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,k2_pre_topc(sK50),u1_struct_0(sK51))
| v5_pre_topc(X0,sK50,sK51) ),
inference(forward_subsumption_resolution,[],[f25652,f18416]) ).
fof(f25654,plain,
! [X0] :
( ~ v1_funct_2(X0,k2_pre_topc(sK50),k2_pre_topc(sK51))
| k5_subset_1(k2_pre_topc(sK50),u1_struct_0(sK51),k4_tex_4(sK50,sK49(sK50,sK51,X0,u1_struct_0(sK51)))) != k1_struct_0(sK51,k8_funct_2(k2_pre_topc(sK50),u1_struct_0(sK51),X0,sK49(sK50,sK51,X0,u1_struct_0(sK51))))
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,k2_pre_topc(sK50),u1_struct_0(sK51))
| v5_pre_topc(X0,sK50,sK51) ),
inference(forward_demodulation,[],[f25653,f25576]) ).
fof(f25655,plain,
! [X0] :
( k5_subset_1(k2_pre_topc(sK50),k2_pre_topc(sK51),k4_tex_4(sK50,sK49(sK50,sK51,X0,k2_pre_topc(sK51)))) != k1_struct_0(sK51,k8_funct_2(k2_pre_topc(sK50),k2_pre_topc(sK51),X0,sK49(sK50,sK51,X0,k2_pre_topc(sK51))))
| ~ v1_funct_2(X0,k2_pre_topc(sK50),k2_pre_topc(sK51))
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,k2_pre_topc(sK50),u1_struct_0(sK51))
| v5_pre_topc(X0,sK50,sK51) ),
inference(forward_demodulation,[],[f25654,f25576]) ).
fof(f25656,plain,
! [X0] :
( k5_subset_1(k2_pre_topc(sK50),k2_pre_topc(sK51),k4_tex_4(sK50,sK49(sK50,sK51,X0,k2_pre_topc(sK51)))) != k1_struct_0(sK51,k8_funct_2(k2_pre_topc(sK50),k2_pre_topc(sK51),X0,sK49(sK50,sK51,X0,k2_pre_topc(sK51))))
| ~ m2_relset_1(X0,k2_pre_topc(sK50),k2_pre_topc(sK51))
| ~ v1_funct_2(X0,k2_pre_topc(sK50),k2_pre_topc(sK51))
| ~ v1_funct_1(X0)
| v5_pre_topc(X0,sK50,sK51) ),
inference(forward_demodulation,[],[f25655,f25576]) ).
fof(f25665,plain,
! [X0,X1] :
( m1_subset_1(sK49(sK50,X0,X1,u1_struct_0(X0)),u1_struct_0(sK50))
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(sK50)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK50),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK50),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK50)
| ~ m2_tsp_1(X0,sK50)
| v3_struct_0(sK50)
| v5_pre_topc(X1,sK50,X0)
| ~ l1_pre_topc(sK50) ),
inference(resolution,[],[f24482,f18414]) ).
fof(f25666,plain,
! [X0,X1] :
( m1_subset_1(sK49(sK50,X0,X1,u1_struct_0(X0)),u1_struct_0(sK50))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK50),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK50),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK50)
| ~ m2_tsp_1(X0,sK50)
| v3_struct_0(sK50)
| v5_pre_topc(X1,sK50,X0)
| ~ l1_pre_topc(sK50) ),
inference(forward_subsumption_resolution,[],[f25665,f18345]) ).
fof(f25667,plain,
! [X0,X1] :
( m1_subset_1(sK49(sK50,X0,X1,u1_struct_0(X0)),u1_struct_0(sK50))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK50),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK50),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK50)
| ~ m2_tsp_1(X0,sK50)
| v5_pre_topc(X1,sK50,X0)
| ~ l1_pre_topc(sK50) ),
inference(forward_subsumption_resolution,[],[f25666,f18415]) ).
fof(f25668,plain,
! [X0,X1] :
( m1_subset_1(sK49(sK50,X0,X1,u1_struct_0(X0)),u1_struct_0(sK50))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK50),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK50),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK50)
| ~ m2_tsp_1(X0,sK50)
| v5_pre_topc(X1,sK50,X0) ),
inference(forward_subsumption_resolution,[],[f25667,f18413]) ).
fof(f25669,plain,
! [X0,X1] :
( m1_subset_1(sK49(sK50,X0,X1,u1_struct_0(X0)),k2_pre_topc(sK50))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK50),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK50),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK50)
| ~ m2_tsp_1(X0,sK50)
| v5_pre_topc(X1,sK50,X0) ),
inference(forward_demodulation,[],[f25668,f25575]) ).
fof(f25670,plain,
! [X0,X1] :
( ~ v1_funct_2(X1,k2_pre_topc(sK50),u1_struct_0(X0))
| m1_subset_1(sK49(sK50,X0,X1,u1_struct_0(X0)),k2_pre_topc(sK50))
| ~ v1_funct_1(X1)
| ~ m2_relset_1(X1,u1_struct_0(sK50),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK50)
| ~ m2_tsp_1(X0,sK50)
| v5_pre_topc(X1,sK50,X0) ),
inference(forward_demodulation,[],[f25669,f25575]) ).
fof(f25671,plain,
! [X0,X1] :
( ~ v2_tsp_2(X0,sK50)
| ~ v1_funct_2(X1,k2_pre_topc(sK50),u1_struct_0(X0))
| m1_subset_1(sK49(sK50,X0,X1,u1_struct_0(X0)),k2_pre_topc(sK50))
| ~ v1_funct_1(X1)
| v3_struct_0(X0)
| ~ m2_relset_1(X1,k2_pre_topc(sK50),u1_struct_0(X0))
| ~ m2_tsp_1(X0,sK50)
| v5_pre_topc(X1,sK50,X0) ),
inference(forward_demodulation,[],[f25670,f25575]) ).
fof(f25672,plain,
! [X0] :
( ~ v1_funct_2(X0,k2_pre_topc(sK50),u1_struct_0(sK51))
| m1_subset_1(sK49(sK50,sK51,X0,u1_struct_0(sK51)),k2_pre_topc(sK50))
| ~ v1_funct_1(X0)
| v3_struct_0(sK51)
| ~ m2_relset_1(X0,k2_pre_topc(sK50),u1_struct_0(sK51))
| ~ m2_tsp_1(sK51,sK50)
| v5_pre_topc(X0,sK50,sK51) ),
inference(resolution,[],[f25671,f18417]) ).
fof(f25673,plain,
! [X0] :
( ~ v1_funct_2(X0,k2_pre_topc(sK50),u1_struct_0(sK51))
| m1_subset_1(sK49(sK50,sK51,X0,u1_struct_0(sK51)),k2_pre_topc(sK50))
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,k2_pre_topc(sK50),u1_struct_0(sK51))
| ~ m2_tsp_1(sK51,sK50)
| v5_pre_topc(X0,sK50,sK51) ),
inference(forward_subsumption_resolution,[],[f25672,f18418]) ).
fof(f25674,plain,
! [X0] :
( ~ v1_funct_2(X0,k2_pre_topc(sK50),u1_struct_0(sK51))
| m1_subset_1(sK49(sK50,sK51,X0,u1_struct_0(sK51)),k2_pre_topc(sK50))
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,k2_pre_topc(sK50),u1_struct_0(sK51))
| v5_pre_topc(X0,sK50,sK51) ),
inference(forward_subsumption_resolution,[],[f25673,f18416]) ).
fof(f25675,plain,
! [X0] :
( ~ v1_funct_2(X0,k2_pre_topc(sK50),k2_pre_topc(sK51))
| m1_subset_1(sK49(sK50,sK51,X0,u1_struct_0(sK51)),k2_pre_topc(sK50))
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,k2_pre_topc(sK50),u1_struct_0(sK51))
| v5_pre_topc(X0,sK50,sK51) ),
inference(forward_demodulation,[],[f25674,f25576]) ).
fof(f25676,plain,
! [X0] :
( m1_subset_1(sK49(sK50,sK51,X0,k2_pre_topc(sK51)),k2_pre_topc(sK50))
| ~ v1_funct_2(X0,k2_pre_topc(sK50),k2_pre_topc(sK51))
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,k2_pre_topc(sK50),u1_struct_0(sK51))
| v5_pre_topc(X0,sK50,sK51) ),
inference(forward_demodulation,[],[f25675,f25576]) ).
fof(f25677,plain,
! [X0] :
( m1_subset_1(sK49(sK50,sK51,X0,k2_pre_topc(sK51)),k2_pre_topc(sK50))
| ~ m2_relset_1(X0,k2_pre_topc(sK50),k2_pre_topc(sK51))
| ~ v1_funct_2(X0,k2_pre_topc(sK50),k2_pre_topc(sK51))
| ~ v1_funct_1(X0)
| v5_pre_topc(X0,sK50,sK51) ),
inference(forward_demodulation,[],[f25676,f25576]) ).
fof(f25678,plain,
! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_pre_topc(sK50),k2_pre_topc(sK51))
| ~ m2_relset_1(X0,k2_pre_topc(sK50),k2_pre_topc(sK51))
| v5_pre_topc(X0,sK50,sK51)
| k4_tex_4(sK50,sK49(sK50,sK51,X0,k2_pre_topc(sK51))) = k2_tex_4(sK50,sK49(sK50,sK51,X0,k2_pre_topc(sK51))) ),
inference(resolution,[],[f25677,f25637]) ).
fof(f25679,plain,
! [X0] :
( ~ v2_tsp_2(X0,sK50)
| v3_struct_0(X0)
| ~ m2_tsp_1(X0,sK50)
| v3_struct_0(sK50)
| v2_t_0topsp(X0)
| ~ l1_pre_topc(sK50) ),
inference(resolution,[],[f18351,f18414]) ).
fof(f25680,plain,
! [X0] :
( ~ v2_tsp_2(X0,sK50)
| v3_struct_0(X0)
| ~ m2_tsp_1(X0,sK50)
| v2_t_0topsp(X0)
| ~ l1_pre_topc(sK50) ),
inference(forward_subsumption_resolution,[],[f25679,f18415]) ).
fof(f25681,plain,
! [X0] :
( ~ v2_tsp_2(X0,sK50)
| v3_struct_0(X0)
| ~ m2_tsp_1(X0,sK50)
| v2_t_0topsp(X0) ),
inference(forward_subsumption_resolution,[],[f25680,f18413]) ).
fof(f25682,plain,
( v3_struct_0(sK51)
| ~ m2_tsp_1(sK51,sK50)
| v2_t_0topsp(sK51) ),
inference(resolution,[],[f25681,f18417]) ).
fof(f25683,plain,
( ~ m2_tsp_1(sK51,sK50)
| v2_t_0topsp(sK51) ),
inference(forward_subsumption_resolution,[],[f25682,f18418]) ).
fof(f25684,plain,
v2_t_0topsp(sK51),
inference(forward_subsumption_resolution,[],[f25683,f18416]) ).
fof(f25709,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(resolution,[],[f20207,f20201]) ).
fof(f25725,plain,
! [X0] :
( k8_funct_2(u1_struct_0(sK50),u1_struct_0(sK51),sK52,X0) = k1_funct_1(sK52,X0)
| v1_xboole_0(u1_struct_0(sK50))
| ~ m1_relset_1(sK52,u1_struct_0(sK50),u1_struct_0(sK51))
| ~ m1_subset_1(X0,u1_struct_0(sK50)) ),
inference(resolution,[],[f25568,f18420]) ).
fof(f25728,plain,
! [X0] :
( k8_funct_2(u1_struct_0(sK50),u1_struct_0(sK51),sK52,X0) = k1_funct_1(sK52,X0)
| v1_xboole_0(u1_struct_0(sK50))
| ~ m1_subset_1(X0,u1_struct_0(sK50)) ),
inference(forward_subsumption_resolution,[],[f25725,f25563]) ).
fof(f25730,definition,
( spl771_26
<=> v1_xboole_0(k2_pre_topc(sK50)) ),
introduced(definition,[new_symbols(definition,[spl771_26])],[avatar_definition]) ).
fof(f25731,plain,
( v1_xboole_0(k2_pre_topc(sK50))
| ~ spl771_26 ),
inference(avatar_component_clause,[],[f25730]) ).
fof(f25733,definition,
( spl771_27
<=> ! [X0] :
( k8_funct_2(k2_pre_topc(sK50),k2_pre_topc(sK51),sK52,X0) = k1_funct_1(sK52,X0)
| ~ m1_subset_1(X0,k2_pre_topc(sK50)) ) ),
introduced(definition,[new_symbols(definition,[spl771_27])],[avatar_definition]) ).
fof(f25734,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(sK50))
| k8_funct_2(k2_pre_topc(sK50),k2_pre_topc(sK51),sK52,X0) = k1_funct_1(sK52,X0) )
| ~ spl771_27 ),
inference(avatar_component_clause,[],[f25733]) ).
fof(f25736,plain,
! [X0] :
( k1_funct_1(sK52,X0) = k8_funct_2(u1_struct_0(sK50),k2_pre_topc(sK51),sK52,X0)
| v1_xboole_0(u1_struct_0(sK50))
| ~ m1_subset_1(X0,u1_struct_0(sK50)) ),
inference(forward_demodulation,[],[f25728,f25576]) ).
fof(f25737,plain,
! [X0] :
( k8_funct_2(k2_pre_topc(sK50),k2_pre_topc(sK51),sK52,X0) = k1_funct_1(sK52,X0)
| v1_xboole_0(u1_struct_0(sK50))
| ~ m1_subset_1(X0,u1_struct_0(sK50)) ),
inference(forward_demodulation,[],[f25736,f25575]) ).
fof(f25738,plain,
! [X0] :
( v1_xboole_0(k2_pre_topc(sK50))
| k8_funct_2(k2_pre_topc(sK50),k2_pre_topc(sK51),sK52,X0) = k1_funct_1(sK52,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK50)) ),
inference(forward_demodulation,[],[f25737,f25575]) ).
fof(f25739,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(sK50))
| v1_xboole_0(k2_pre_topc(sK50))
| k8_funct_2(k2_pre_topc(sK50),k2_pre_topc(sK51),sK52,X0) = k1_funct_1(sK52,X0) ),
inference(forward_demodulation,[],[f25738,f25575]) ).
fof(f25740,plain,
( spl771_26
| spl771_27 ),
inference(avatar_split_clause,[],[f25739,f25733,f25730]) ).
fof(f25741,plain,
( ~ v1_xboole_0(k2_pre_topc(sK50))
| v3_struct_0(sK50)
| ~ l1_pre_topc(sK50) ),
inference(superposition,[],[f25709,f25575]) ).
fof(f25744,plain,
( v3_struct_0(sK50)
| ~ l1_pre_topc(sK50)
| ~ spl771_26 ),
inference(forward_subsumption_resolution,[],[f25741,f25731]) ).
fof(f25746,plain,
( ~ l1_pre_topc(sK50)
| ~ spl771_26 ),
inference(forward_subsumption_resolution,[],[f25744,f18415]) ).
fof(f25747,plain,
( $false
| ~ spl771_26 ),
inference(forward_subsumption_resolution,[],[f25746,f18413]) ).
fof(f25748,plain,
~ spl771_26,
inference(avatar_contradiction_clause,[],[f25747]) ).
fof(f25749,plain,
( ~ v1_xboole_0(k2_pre_topc(sK50))
| ~ l1_pre_topc(sK50) ),
inference(forward_subsumption_resolution,[],[f25741,f18415]) ).
fof(f25750,plain,
~ v1_xboole_0(k2_pre_topc(sK50)),
inference(forward_subsumption_resolution,[],[f25749,f18413]) ).
fof(f25752,plain,
( ! [X0] :
( ~ m2_relset_1(X0,k2_pre_topc(sK50),k2_pre_topc(sK51))
| k8_funct_2(k2_pre_topc(sK50),k2_pre_topc(sK51),sK52,sK49(sK50,sK51,X0,k2_pre_topc(sK51))) = k1_funct_1(sK52,sK49(sK50,sK51,X0,k2_pre_topc(sK51)))
| ~ v1_funct_2(X0,k2_pre_topc(sK50),k2_pre_topc(sK51))
| ~ v1_funct_1(X0)
| v5_pre_topc(X0,sK50,sK51) )
| ~ spl771_27 ),
inference(resolution,[],[f25734,f25677]) ).
fof(f25866,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| v3_struct_0(X1)
| ~ m1_pre_topc(X1,sK50)
| v3_struct_0(sK50)
| m1_subset_1(X0,u1_struct_0(sK50))
| ~ l1_pre_topc(sK50) ),
inference(resolution,[],[f18432,f18414]) ).
fof(f25867,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| v3_struct_0(X1)
| ~ m1_pre_topc(X1,sK50)
| m1_subset_1(X0,u1_struct_0(sK50))
| ~ l1_pre_topc(sK50) ),
inference(forward_subsumption_resolution,[],[f25866,f18415]) ).
fof(f25868,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| v3_struct_0(X1)
| ~ m1_pre_topc(X1,sK50)
| m1_subset_1(X0,u1_struct_0(sK50)) ),
inference(forward_subsumption_resolution,[],[f25867,f18413]) ).
fof(f25869,plain,
! [X0,X1] :
( ~ m1_pre_topc(X1,sK50)
| ~ m1_subset_1(X0,u1_struct_0(X1))
| v3_struct_0(X1)
| m1_subset_1(X0,k2_pre_topc(sK50)) ),
inference(forward_demodulation,[],[f25868,f25575]) ).
fof(f25870,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK51))
| v3_struct_0(sK51)
| m1_subset_1(X0,k2_pre_topc(sK50)) ),
inference(resolution,[],[f25869,f25567]) ).
fof(f25871,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK51))
| m1_subset_1(X0,k2_pre_topc(sK50)) ),
inference(forward_subsumption_resolution,[],[f25870,f18418]) ).
fof(f25872,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(sK51))
| m1_subset_1(X0,k2_pre_topc(sK50)) ),
inference(forward_demodulation,[],[f25871,f25576]) ).
fof(f26022,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| k1_struct_0(X0,X1) = k2_tarski(X1,X1)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0) ),
inference(resolution,[],[f23579,f20201]) ).
fof(f26023,plain,
! [X0] :
( k2_tarski(X0,X0) = k1_struct_0(sK50,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK50))
| v3_struct_0(sK50) ),
inference(resolution,[],[f26022,f18413]) ).
fof(f26024,plain,
! [X0] :
( k2_tarski(X0,X0) = k1_struct_0(sK51,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK51))
| v3_struct_0(sK51) ),
inference(resolution,[],[f26022,f25569]) ).
fof(f26025,plain,
! [X0] :
( k2_tarski(X0,X0) = k1_struct_0(sK51,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK51)) ),
inference(forward_subsumption_resolution,[],[f26024,f18418]) ).
fof(f26026,plain,
! [X0] :
( k2_tarski(X0,X0) = k1_struct_0(sK50,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK50)) ),
inference(forward_subsumption_resolution,[],[f26023,f18415]) ).
fof(f26027,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(sK51))
| k2_tarski(X0,X0) = k1_struct_0(sK51,X0) ),
inference(forward_demodulation,[],[f26025,f25576]) ).
fof(f26028,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(sK50))
| k2_tarski(X0,X0) = k1_struct_0(sK50,X0) ),
inference(forward_demodulation,[],[f26026,f25575]) ).
fof(f26038,plain,
( ~ v1_funct_2(sK52,k2_pre_topc(sK50),k2_pre_topc(sK51))
| ~ m2_relset_1(sK52,k2_pre_topc(sK50),k2_pre_topc(sK51))
| v5_pre_topc(sK52,sK50,sK51)
| k4_tex_4(sK50,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))) = k2_tex_4(sK50,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))) ),
inference(resolution,[],[f25678,f18421]) ).
fof(f26039,plain,
( ~ m2_relset_1(sK52,k2_pre_topc(sK50),k2_pre_topc(sK51))
| v5_pre_topc(sK52,sK50,sK51)
| k4_tex_4(sK50,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))) = k2_tex_4(sK50,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))) ),
inference(forward_subsumption_resolution,[],[f26038,f25598]) ).
fof(f26040,plain,
( v5_pre_topc(sK52,sK50,sK51)
| k4_tex_4(sK50,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))) = k2_tex_4(sK50,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))) ),
inference(forward_subsumption_resolution,[],[f26039,f25599]) ).
fof(f26041,plain,
k4_tex_4(sK50,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))) = k2_tex_4(sK50,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))),
inference(forward_subsumption_resolution,[],[f26040,f25535]) ).
fof(f26080,plain,
m1_subset_1(u1_struct_0(sK51),k1_zfmisc_1(k2_pre_topc(sK50))),
inference(resolution,[],[f25603,f18416]) ).
fof(f26081,plain,
m1_subset_1(k2_pre_topc(sK51),k1_zfmisc_1(k2_pre_topc(sK50))),
inference(forward_demodulation,[],[f26080,f25576]) ).
fof(f26489,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k2_tex_4(sK50,X1))
| ~ m1_subset_1(X0,u1_struct_0(sK50))
| ~ m1_subset_1(X1,u1_struct_0(sK50))
| v3_struct_0(sK50)
| k2_tex_4(sK50,X0) = k2_tex_4(sK50,X1) ),
inference(resolution,[],[f19832,f18413]) ).
fof(f26492,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k2_tex_4(sK50,X1))
| ~ m1_subset_1(X0,u1_struct_0(sK50))
| ~ m1_subset_1(X1,u1_struct_0(sK50))
| k2_tex_4(sK50,X0) = k2_tex_4(sK50,X1) ),
inference(forward_subsumption_resolution,[],[f26489,f18415]) ).
fof(f26494,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k2_pre_topc(sK50))
| ~ r2_hidden(X0,k2_tex_4(sK50,X1))
| ~ m1_subset_1(X1,u1_struct_0(sK50))
| k2_tex_4(sK50,X0) = k2_tex_4(sK50,X1) ),
inference(forward_demodulation,[],[f26492,f25575]) ).
fof(f26496,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k2_pre_topc(sK50))
| ~ m1_subset_1(X1,k2_pre_topc(sK50))
| ~ r2_hidden(X0,k2_tex_4(sK50,X1))
| k2_tex_4(sK50,X0) = k2_tex_4(sK50,X1) ),
inference(forward_demodulation,[],[f26494,f25575]) ).
fof(f26527,plain,
( k8_funct_2(k2_pre_topc(sK50),k2_pre_topc(sK51),sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))) = k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51)))
| ~ v1_funct_2(sK52,k2_pre_topc(sK50),k2_pre_topc(sK51))
| ~ v1_funct_1(sK52)
| v5_pre_topc(sK52,sK50,sK51)
| ~ spl771_27 ),
inference(resolution,[],[f25752,f25599]) ).
fof(f26528,plain,
( k8_funct_2(k2_pre_topc(sK50),k2_pre_topc(sK51),sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))) = k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51)))
| ~ v1_funct_1(sK52)
| v5_pre_topc(sK52,sK50,sK51)
| ~ spl771_27 ),
inference(forward_subsumption_resolution,[],[f26527,f25598]) ).
fof(f26529,plain,
( k8_funct_2(k2_pre_topc(sK50),k2_pre_topc(sK51),sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))) = k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51)))
| v5_pre_topc(sK52,sK50,sK51)
| ~ spl771_27 ),
inference(forward_subsumption_resolution,[],[f26528,f18421]) ).
fof(f26530,plain,
( k8_funct_2(k2_pre_topc(sK50),k2_pre_topc(sK51),sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))) = k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51)))
| ~ spl771_27 ),
inference(forward_subsumption_resolution,[],[f26529,f25535]) ).
fof(f26532,plain,
( r2_hidden(k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))),k4_tex_4(sK50,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))))
| ~ m1_subset_1(sK49(sK50,sK51,sK52,k2_pre_topc(sK51)),k2_pre_topc(sK50))
| ~ spl771_27 ),
inference(superposition,[],[f25600,f26530]) ).
fof(f26533,plain,
( k5_subset_1(k2_pre_topc(sK50),k2_pre_topc(sK51),k4_tex_4(sK50,sK49(sK50,sK51,sK52,k2_pre_topc(sK51)))) != k1_struct_0(sK51,k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))))
| ~ m2_relset_1(sK52,k2_pre_topc(sK50),k2_pre_topc(sK51))
| ~ v1_funct_2(sK52,k2_pre_topc(sK50),k2_pre_topc(sK51))
| ~ v1_funct_1(sK52)
| v5_pre_topc(sK52,sK50,sK51)
| ~ spl771_27 ),
inference(superposition,[],[f25656,f26530]) ).
fof(f26535,plain,
( m1_subset_1(k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))),k2_pre_topc(sK51))
| v1_xboole_0(k2_pre_topc(sK50))
| ~ v1_funct_1(sK52)
| ~ v1_funct_2(sK52,k2_pre_topc(sK50),k2_pre_topc(sK51))
| ~ m1_relset_1(sK52,k2_pre_topc(sK50),k2_pre_topc(sK51))
| ~ m1_subset_1(sK49(sK50,sK51,sK52,k2_pre_topc(sK51)),k2_pre_topc(sK50))
| ~ spl771_27 ),
inference(superposition,[],[f19662,f26530]) ).
fof(f26536,plain,
( m1_subset_1(k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))),k2_pre_topc(sK51))
| ~ v1_funct_1(sK52)
| ~ v1_funct_2(sK52,k2_pre_topc(sK50),k2_pre_topc(sK51))
| ~ m1_relset_1(sK52,k2_pre_topc(sK50),k2_pre_topc(sK51))
| ~ m1_subset_1(sK49(sK50,sK51,sK52,k2_pre_topc(sK51)),k2_pre_topc(sK50))
| ~ spl771_27 ),
inference(forward_subsumption_resolution,[],[f26535,f25750]) ).
fof(f26538,plain,
( k5_subset_1(k2_pre_topc(sK50),k2_pre_topc(sK51),k4_tex_4(sK50,sK49(sK50,sK51,sK52,k2_pre_topc(sK51)))) != k1_struct_0(sK51,k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))))
| ~ v1_funct_2(sK52,k2_pre_topc(sK50),k2_pre_topc(sK51))
| ~ v1_funct_1(sK52)
| v5_pre_topc(sK52,sK50,sK51)
| ~ spl771_27 ),
inference(forward_subsumption_resolution,[],[f26533,f25599]) ).
fof(f26540,definition,
( spl771_49
<=> m1_subset_1(sK49(sK50,sK51,sK52,k2_pre_topc(sK51)),k2_pre_topc(sK50)) ),
introduced(definition,[new_symbols(definition,[spl771_49])],[avatar_definition]) ).
fof(f26541,plain,
( ~ m1_subset_1(sK49(sK50,sK51,sK52,k2_pre_topc(sK51)),k2_pre_topc(sK50))
| spl771_49 ),
inference(avatar_component_clause,[],[f26540]) ).
fof(f26543,definition,
( spl771_50
<=> r2_hidden(k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))),k4_tex_4(sK50,sK49(sK50,sK51,sK52,k2_pre_topc(sK51)))) ),
introduced(definition,[new_symbols(definition,[spl771_50])],[avatar_definition]) ).
fof(f26544,plain,
( r2_hidden(k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))),k4_tex_4(sK50,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))))
| ~ spl771_50 ),
inference(avatar_component_clause,[],[f26543]) ).
fof(f26545,plain,
( ~ spl771_49
| spl771_50
| ~ spl771_27 ),
inference(avatar_split_clause,[],[f26532,f25733,f26543,f26540]) ).
fof(f26550,plain,
( m1_subset_1(k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))),k2_pre_topc(sK51))
| ~ v1_funct_2(sK52,k2_pre_topc(sK50),k2_pre_topc(sK51))
| ~ m1_relset_1(sK52,k2_pre_topc(sK50),k2_pre_topc(sK51))
| ~ m1_subset_1(sK49(sK50,sK51,sK52,k2_pre_topc(sK51)),k2_pre_topc(sK50))
| ~ spl771_27 ),
inference(forward_subsumption_resolution,[],[f26536,f18421]) ).
fof(f26552,plain,
( k5_subset_1(k2_pre_topc(sK50),k2_pre_topc(sK51),k4_tex_4(sK50,sK49(sK50,sK51,sK52,k2_pre_topc(sK51)))) != k1_struct_0(sK51,k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))))
| ~ v1_funct_1(sK52)
| v5_pre_topc(sK52,sK50,sK51)
| ~ spl771_27 ),
inference(forward_subsumption_resolution,[],[f26538,f25598]) ).
fof(f26553,plain,
( m1_subset_1(k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))),k2_pre_topc(sK51))
| ~ m1_relset_1(sK52,k2_pre_topc(sK50),k2_pre_topc(sK51))
| ~ m1_subset_1(sK49(sK50,sK51,sK52,k2_pre_topc(sK51)),k2_pre_topc(sK50))
| ~ spl771_27 ),
inference(forward_subsumption_resolution,[],[f26550,f25598]) ).
fof(f26555,plain,
( k5_subset_1(k2_pre_topc(sK50),k2_pre_topc(sK51),k4_tex_4(sK50,sK49(sK50,sK51,sK52,k2_pre_topc(sK51)))) != k1_struct_0(sK51,k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))))
| v5_pre_topc(sK52,sK50,sK51)
| ~ spl771_27 ),
inference(forward_subsumption_resolution,[],[f26552,f18421]) ).
fof(f26556,plain,
( m1_subset_1(k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))),k2_pre_topc(sK51))
| ~ m1_subset_1(sK49(sK50,sK51,sK52,k2_pre_topc(sK51)),k2_pre_topc(sK50))
| ~ spl771_27 ),
inference(forward_subsumption_resolution,[],[f26553,f25601]) ).
fof(f26558,plain,
( k5_subset_1(k2_pre_topc(sK50),k2_pre_topc(sK51),k4_tex_4(sK50,sK49(sK50,sK51,sK52,k2_pre_topc(sK51)))) != k1_struct_0(sK51,k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))))
| ~ spl771_27 ),
inference(forward_subsumption_resolution,[],[f26555,f25535]) ).
fof(f26560,definition,
( spl771_52
<=> m1_subset_1(k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))),k2_pre_topc(sK51)) ),
introduced(definition,[new_symbols(definition,[spl771_52])],[avatar_definition]) ).
fof(f26561,plain,
( m1_subset_1(k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))),k2_pre_topc(sK51))
| ~ spl771_52 ),
inference(avatar_component_clause,[],[f26560]) ).
fof(f26562,plain,
( ~ spl771_49
| spl771_52
| ~ spl771_27 ),
inference(avatar_split_clause,[],[f26556,f25733,f26560,f26540]) ).
fof(f26569,plain,
( ~ m2_relset_1(sK52,k2_pre_topc(sK50),k2_pre_topc(sK51))
| ~ v1_funct_2(sK52,k2_pre_topc(sK50),k2_pre_topc(sK51))
| ~ v1_funct_1(sK52)
| v5_pre_topc(sK52,sK50,sK51)
| spl771_49 ),
inference(resolution,[],[f26541,f25677]) ).
fof(f26571,plain,
( ~ v1_funct_2(sK52,k2_pre_topc(sK50),k2_pre_topc(sK51))
| ~ v1_funct_1(sK52)
| v5_pre_topc(sK52,sK50,sK51)
| spl771_49 ),
inference(forward_subsumption_resolution,[],[f26569,f25599]) ).
fof(f26572,plain,
( ~ v1_funct_1(sK52)
| v5_pre_topc(sK52,sK50,sK51)
| spl771_49 ),
inference(forward_subsumption_resolution,[],[f26571,f25598]) ).
fof(f26573,plain,
( v5_pre_topc(sK52,sK50,sK51)
| spl771_49 ),
inference(forward_subsumption_resolution,[],[f26572,f18421]) ).
fof(f26574,plain,
( $false
| spl771_49 ),
inference(forward_subsumption_resolution,[],[f26573,f25535]) ).
fof(f26575,plain,
spl771_49,
inference(avatar_contradiction_clause,[],[f26574]) ).
fof(f26578,plain,
( k1_struct_0(sK51,k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51)))) = k2_tarski(k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))),k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))))
| ~ spl771_52 ),
inference(resolution,[],[f26561,f26027]) ).
fof(f26579,plain,
( m1_subset_1(k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))),k2_pre_topc(sK50))
| ~ spl771_52 ),
inference(resolution,[],[f26561,f25872]) ).
fof(f26583,plain,
( k2_tarski(k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))),k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51)))) = k1_struct_0(sK50,k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))))
| ~ spl771_52 ),
inference(resolution,[],[f26579,f26028]) ).
fof(f26585,plain,
( k4_tex_4(sK50,k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51)))) = k2_tex_4(sK50,k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))))
| ~ spl771_52 ),
inference(resolution,[],[f26579,f25637]) ).
fof(f26611,plain,
( k1_struct_0(sK51,k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51)))) = k1_struct_0(sK50,k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))))
| ~ spl771_52 ),
inference(superposition,[],[f26578,f26583]) ).
fof(f26944,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(sK50))
| ~ r2_hidden(k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))),k2_tex_4(sK50,X0))
| k2_tex_4(sK50,X0) = k2_tex_4(sK50,k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51)))) )
| ~ spl771_52 ),
inference(resolution,[],[f26496,f26579]) ).
fof(f26947,plain,
( ! [X0] :
( ~ r2_hidden(k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))),k2_tex_4(sK50,X0))
| ~ m1_subset_1(X0,k2_pre_topc(sK50))
| k2_tex_4(sK50,X0) = k4_tex_4(sK50,k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51)))) )
| ~ spl771_52 ),
inference(forward_demodulation,[],[f26944,f26585]) ).
fof(f27115,plain,
! [X0,X1] :
( ~ l1_pre_topc(X1)
| v3_struct_0(X1)
| r2_hidden(X0,k2_pre_topc(X1))
| ~ m1_subset_1(X0,u1_struct_0(X1)) ),
inference(resolution,[],[f20763,f20201]) ).
fof(f27117,plain,
! [X0] :
( v3_struct_0(sK51)
| r2_hidden(X0,k2_pre_topc(sK51))
| ~ m1_subset_1(X0,u1_struct_0(sK51)) ),
inference(resolution,[],[f27115,f25569]) ).
fof(f27118,plain,
! [X0] :
( r2_hidden(X0,k2_pre_topc(sK51))
| ~ m1_subset_1(X0,u1_struct_0(sK51)) ),
inference(forward_subsumption_resolution,[],[f27117,f18418]) ).
fof(f27120,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(sK51))
| r2_hidden(X0,k2_pre_topc(sK51)) ),
inference(forward_demodulation,[],[f27118,f25576]) ).
fof(f27125,plain,
( r2_hidden(k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))),k2_pre_topc(sK51))
| ~ spl771_52 ),
inference(resolution,[],[f27120,f26561]) ).
fof(f27430,plain,
! [X0] :
( v1_tsp_1(u1_struct_0(sK51),X0)
| ~ m1_subset_1(u1_struct_0(sK51),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(sK51)
| ~ m2_tsp_1(sK51,X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(resolution,[],[f24487,f25684]) ).
fof(f27431,plain,
! [X0] :
( v1_tsp_1(u1_struct_0(sK51),X0)
| v3_struct_0(sK51)
| ~ m2_tsp_1(sK51,X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(forward_subsumption_resolution,[],[f27430,f18345]) ).
fof(f27432,plain,
! [X0] :
( v1_tsp_1(u1_struct_0(sK51),X0)
| ~ m2_tsp_1(sK51,X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(forward_subsumption_resolution,[],[f27431,f18418]) ).
fof(f27433,plain,
! [X0] :
( v1_tsp_1(k2_pre_topc(sK51),X0)
| ~ m2_tsp_1(sK51,X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(forward_demodulation,[],[f27432,f25576]) ).
fof(f27518,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_tsp_1(X1,sK50)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK50)))
| v3_struct_0(sK50)
| k1_struct_0(sK50,X0) = k5_subset_1(u1_struct_0(sK50),X1,k4_tex_4(sK50,X0))
| ~ l1_pre_topc(sK50) ),
inference(resolution,[],[f25367,f18414]) ).
fof(f27519,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_tsp_1(X1,sK50)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK50)))
| k1_struct_0(sK50,X0) = k5_subset_1(u1_struct_0(sK50),X1,k4_tex_4(sK50,X0))
| ~ l1_pre_topc(sK50) ),
inference(forward_subsumption_resolution,[],[f27518,f18415]) ).
fof(f27520,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_tsp_1(X1,sK50)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK50)))
| k1_struct_0(sK50,X0) = k5_subset_1(u1_struct_0(sK50),X1,k4_tex_4(sK50,X0)) ),
inference(forward_subsumption_resolution,[],[f27519,f18413]) ).
fof(f27521,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(k2_pre_topc(sK50)))
| ~ r2_hidden(X0,X1)
| ~ v1_tsp_1(X1,sK50)
| k1_struct_0(sK50,X0) = k5_subset_1(u1_struct_0(sK50),X1,k4_tex_4(sK50,X0)) ),
inference(forward_demodulation,[],[f27520,f25575]) ).
fof(f27522,plain,
! [X0,X1] :
( ~ v1_tsp_1(X1,sK50)
| ~ m1_subset_1(X1,k1_zfmisc_1(k2_pre_topc(sK50)))
| ~ r2_hidden(X0,X1)
| k1_struct_0(sK50,X0) = k5_subset_1(k2_pre_topc(sK50),X1,k4_tex_4(sK50,X0)) ),
inference(forward_demodulation,[],[f27521,f25575]) ).
fof(f27524,plain,
! [X0] :
( ~ m1_subset_1(k2_pre_topc(sK51),k1_zfmisc_1(k2_pre_topc(sK50)))
| ~ r2_hidden(X0,k2_pre_topc(sK51))
| k1_struct_0(sK50,X0) = k5_subset_1(k2_pre_topc(sK50),k2_pre_topc(sK51),k4_tex_4(sK50,X0))
| ~ m2_tsp_1(sK51,sK50)
| v3_struct_0(sK50)
| ~ l1_pre_topc(sK50) ),
inference(resolution,[],[f27522,f27433]) ).
fof(f27525,plain,
! [X0] :
( ~ r2_hidden(X0,k2_pre_topc(sK51))
| k1_struct_0(sK50,X0) = k5_subset_1(k2_pre_topc(sK50),k2_pre_topc(sK51),k4_tex_4(sK50,X0))
| ~ m2_tsp_1(sK51,sK50)
| v3_struct_0(sK50)
| ~ l1_pre_topc(sK50) ),
inference(forward_subsumption_resolution,[],[f27524,f26081]) ).
fof(f27527,plain,
! [X0] :
( ~ r2_hidden(X0,k2_pre_topc(sK51))
| k1_struct_0(sK50,X0) = k5_subset_1(k2_pre_topc(sK50),k2_pre_topc(sK51),k4_tex_4(sK50,X0))
| v3_struct_0(sK50)
| ~ l1_pre_topc(sK50) ),
inference(forward_subsumption_resolution,[],[f27525,f18416]) ).
fof(f27529,plain,
! [X0] :
( ~ r2_hidden(X0,k2_pre_topc(sK51))
| k1_struct_0(sK50,X0) = k5_subset_1(k2_pre_topc(sK50),k2_pre_topc(sK51),k4_tex_4(sK50,X0))
| ~ l1_pre_topc(sK50) ),
inference(forward_subsumption_resolution,[],[f27527,f18415]) ).
fof(f27531,plain,
! [X0] :
( ~ r2_hidden(X0,k2_pre_topc(sK51))
| k1_struct_0(sK50,X0) = k5_subset_1(k2_pre_topc(sK50),k2_pre_topc(sK51),k4_tex_4(sK50,X0)) ),
inference(forward_subsumption_resolution,[],[f27529,f18413]) ).
fof(f27535,plain,
( k1_struct_0(sK50,k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51)))) = k5_subset_1(k2_pre_topc(sK50),k2_pre_topc(sK51),k4_tex_4(sK50,k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51)))))
| ~ spl771_52 ),
inference(resolution,[],[f27531,f27125]) ).
fof(f29619,plain,
( ~ r2_hidden(k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))),k4_tex_4(sK50,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))))
| ~ m1_subset_1(sK49(sK50,sK51,sK52,k2_pre_topc(sK51)),k2_pre_topc(sK50))
| k4_tex_4(sK50,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))) = k4_tex_4(sK50,k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))))
| ~ spl771_52 ),
inference(superposition,[],[f26947,f26041]) ).
fof(f29621,plain,
( ~ m1_subset_1(sK49(sK50,sK51,sK52,k2_pre_topc(sK51)),k2_pre_topc(sK50))
| k4_tex_4(sK50,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))) = k4_tex_4(sK50,k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))))
| ~ spl771_50
| ~ spl771_52 ),
inference(forward_subsumption_resolution,[],[f29619,f26544]) ).
fof(f29623,definition,
( spl771_164
<=> k4_tex_4(sK50,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))) = k4_tex_4(sK50,k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51)))) ),
introduced(definition,[new_symbols(definition,[spl771_164])],[avatar_definition]) ).
fof(f29624,plain,
( k4_tex_4(sK50,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))) = k4_tex_4(sK50,k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))))
| ~ spl771_164 ),
inference(avatar_component_clause,[],[f29623]) ).
fof(f29625,plain,
( spl771_164
| ~ spl771_49
| ~ spl771_50
| ~ spl771_52 ),
inference(avatar_split_clause,[],[f29621,f26560,f26543,f26540,f29623]) ).
fof(f29630,plain,
( k5_subset_1(k2_pre_topc(sK50),k2_pre_topc(sK51),k4_tex_4(sK50,sK49(sK50,sK51,sK52,k2_pre_topc(sK51)))) = k1_struct_0(sK50,k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))))
| ~ spl771_52
| ~ spl771_164 ),
inference(superposition,[],[f27535,f29624]) ).
fof(f29657,plain,
( k1_struct_0(sK51,k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51)))) != k1_struct_0(sK50,k1_funct_1(sK52,sK49(sK50,sK51,sK52,k2_pre_topc(sK51))))
| ~ spl771_27
| ~ spl771_52
| ~ spl771_164 ),
inference(superposition,[],[f26558,f29630]) ).
fof(f29658,plain,
( $false
| ~ spl771_27
| ~ spl771_52
| ~ spl771_164 ),
inference(forward_subsumption_resolution,[],[f29657,f26611]) ).
fof(f29659,plain,
( ~ spl771_27
| ~ spl771_52
| ~ spl771_164 ),
inference(avatar_contradiction_clause,[],[f29658]) ).
cnf(s24,plain,
( spl771_26
| spl771_27 ),
inference(sat_conversion,[],[f25740]) ).
cnf(s25,plain,
~ spl771_26,
inference(sat_conversion,[],[f25748]) ).
cnf(s51,plain,
( ~ spl771_27
| ~ spl771_49
| spl771_50 ),
inference(sat_conversion,[],[f26545]) ).
cnf(s53,plain,
( ~ spl771_27
| ~ spl771_49
| spl771_52 ),
inference(sat_conversion,[],[f26562]) ).
cnf(s56,plain,
spl771_49,
inference(sat_conversion,[],[f26575]) ).
cnf(s146,plain,
( ~ spl771_49
| ~ spl771_50
| ~ spl771_52
| spl771_164 ),
inference(sat_conversion,[],[f29625]) ).
cnf(s147,plain,
( ~ spl771_27
| ~ spl771_52
| ~ spl771_164 ),
inference(sat_conversion,[],[f29659]) ).
cnf(s155,plain,
( ~ spl771_27
| spl771_52 ),
inference(rat,[],[s53,s56]) ).
cnf(s157,plain,
( ~ spl771_27
| spl771_50 ),
inference(rat,[],[s51,s56]) ).
cnf(s181,plain,
spl771_27,
inference(rat,[],[s24,s25]) ).
cnf(s183,plain,
spl771_52,
inference(rat,[],[s155,s181]) ).
cnf(s185,plain,
spl771_50,
inference(rat,[],[s157,s181]) ).
cnf(s188,plain,
~ spl771_164,
inference(rat,[],[s147,s181,s183]) ).
cnf(s191,plain,
$false,
inference(rat,[],[s146,s188,s56,s183,s185]) ).
fof(f29660,plain,
$false,
inference(avatar_sat_refutation,[],[s191]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP032+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n015.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 18:58:08 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 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
% 14.90/3.36 % (2903015)Detected formulas, will run a generic FOF schedule.
% 14.90/3.36 % (2903023)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2831316844:i=109:sd=1:ins=1:gsp=on:ss=axioms_2993 on theBenchmark for (2993ds/109Mi)
% 14.90/3.36 % (2903025)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3176191521:s2a=on:i=139:gtg=position_2993 on theBenchmark for (2993ds/139Mi)
% 14.90/3.36 % (2903026)dis-21_1_sil=8000:lcm=predicate:random_seed=2756534075:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2993 on theBenchmark for (2993ds/129Mi)
% 14.90/3.36 % (2903024)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2346231555:i=119:av=off:ss=axioms_2993 on theBenchmark for (2993ds/119Mi)
% 14.90/3.36 % (2903020)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=344369181:i=141193_2993 on theBenchmark for (2993ds/141193Mi)
% 14.90/3.36 % (2903022)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=2258286734:i=141695:sd=1:nm=32:gsp=on:ss=included_2993 on theBenchmark for (2993ds/141695Mi)
% 14.90/3.36 % (2903021)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=4249269675:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2993 on theBenchmark for (2993ds/134677Mi)
% 14.90/3.36 % (2903023)Instruction limit reached!
% 14.90/3.36 % (2903023)------------------------------
% 14.90/3.36 % (2903023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.90/3.36 % (2903023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/3.36 % (2903023)CaDiCaL version: 2.1.3
% 14.90/3.36 % (2903023)Termination reason: Instruction limit
% 14.90/3.36 % (2903023)Termination phase: Saturation
% 14.90/3.36 % (2903023)Time elapsed: 0.051 s
% 14.90/3.36 % (2903023)Peak memory usage: 107 MB
% 14.90/3.36 % (2903023)Instructions burned: 110 (million)
% 14.90/3.36 % (2903025)Instruction limit reached!
% 14.90/3.36 % (2903025)------------------------------
% 14.90/3.36 % (2903025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.90/3.36 % (2903025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/3.36 % (2903025)CaDiCaL version: 2.1.3
% 14.90/3.36 % (2903025)Termination reason: Instruction limit
% 14.90/3.36 % (2903025)Termination phase: Property scanning
% 14.90/3.36 % (2903025)Time elapsed: 0.058 s
% 14.90/3.36 % (2903025)Peak memory usage: 102 MB
% 14.90/3.36 % (2903025)Instructions burned: 139 (million)
% 14.90/3.36 % (2903026)Instruction limit reached!
% 14.90/3.36 % (2903026)------------------------------
% 14.90/3.36 % (2903026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.90/3.36 % (2903026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/3.36 % (2903026)CaDiCaL version: 2.1.3
% 14.90/3.36 % (2903026)Termination reason: Instruction limit
% 14.90/3.36 % (2903026)Termination phase: Preprocessing 1
% 14.90/3.36 % (2903026)Time elapsed: 0.095 s
% 14.90/3.36 % (2903026)Peak memory usage: 103 MB
% 14.90/3.36 % (2903026)Instructions burned: 130 (million)
% 14.90/3.36 % (2903024)Instruction limit reached!
% 14.90/3.36 % (2903024)------------------------------
% 14.90/3.36 % (2903024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.90/3.36 % (2903024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/3.36 % (2903024)CaDiCaL version: 2.1.3
% 14.90/3.36 % (2903024)Termination reason: Instruction limit
% 14.90/3.36 % (2903024)Termination phase: Preprocessing 3
% 14.90/3.36 % (2903024)Time elapsed: 0.103 s
% 14.90/3.36 % (2903024)Peak memory usage: 105 MB
% 14.90/3.36 % (2903024)Instructions burned: 119 (million)
% 14.90/3.36 % (2903034)lrs+10_1_sil=8000:sp=occurrence:random_seed=3198231854:i=285:sd=3:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/285Mi)
% 14.90/3.36 % (2903035)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3030150844:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/157Mi)
% 14.90/3.36 % (2903036)lrs+1011_1_sil=32000:sp=occurrence:random_seed=192166708:i=325:sd=1:ss=axioms:sgt=32_2990 on theBenchmark for (2990ds/325Mi)
% 14.90/3.36 % (2903034)Instruction limit reached!
% 14.90/3.36 % (2903034)------------------------------
% 14.90/3.36 % (2903034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.90/3.36 % (2903034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.51/4.40 % (2903034)CaDiCaL version: 2.1.3
% 22.51/4.40 % (2903034)Termination reason: Instruction limit
% 22.51/4.40 % (2903034)Termination phase: Saturation
% 22.51/4.40 % (2903034)Time elapsed: 0.107 s
% 22.51/4.40 % (2903034)Peak memory usage: 110 MB
% 22.51/4.40 % (2903034)Instructions burned: 289 (million)
% 22.51/4.40 % (2903037)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=869494660:s2a=on:i=248:s2at=1.23:gtg=position_2990 on theBenchmark for (2990ds/248Mi)
% 22.51/4.40 % (2903035)Instruction limit reached!
% 22.51/4.40 % (2903035)------------------------------
% 22.51/4.40 % (2903035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.51/4.40 % (2903035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.51/4.40 % (2903035)CaDiCaL version: 2.1.3
% 22.51/4.40 % (2903035)Termination reason: Instruction limit
% 22.51/4.40 % (2903035)Termination phase: Property scanning
% 22.51/4.40 % (2903035)Time elapsed: 0.069 s
% 22.51/4.40 % (2903035)Peak memory usage: 102 MB
% 22.51/4.40 % (2903035)Instructions burned: 159 (million)
% 22.51/4.40 % (2903041)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3676707150:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2989 on theBenchmark for (2989ds/294Mi)
% 22.51/4.40 % (2903037)Instruction limit reached!
% 22.51/4.40 % (2903037)------------------------------
% 22.51/4.40 % (2903037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.51/4.40 % (2903037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.51/4.40 % (2903037)CaDiCaL version: 2.1.3
% 22.51/4.40 % (2903037)Termination reason: Instruction limit
% 22.51/4.40 % (2903037)Termination phase: SInE selection
% 22.51/4.40 % (2903037)Time elapsed: 0.132 s
% 22.51/4.40 % (2903037)Peak memory usage: 103 MB
% 22.51/4.40 % (2903037)Instructions burned: 248 (million)
% 22.51/4.40 % (2903043)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3949568950:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 22.51/4.40 % (2903036)Instruction limit reached!
% 22.51/4.40 % (2903036)------------------------------
% 22.51/4.40 % (2903036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.51/4.40 % (2903036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.51/4.40 % (2903036)CaDiCaL version: 2.1.3
% 22.51/4.40 % (2903036)Termination reason: Instruction limit
% 22.51/4.40 % (2903036)Termination phase: Saturation
% 22.51/4.40 % (2903036)Time elapsed: 0.219 s
% 22.51/4.40 % (2903036)Peak memory usage: 109 MB
% 22.51/4.40 % (2903036)Instructions burned: 326 (million)
% 22.51/4.40 % (2903041)Instruction limit reached!
% 22.51/4.40 % (2903041)------------------------------
% 22.51/4.40 % (2903041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.51/4.40 % (2903041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.51/4.40 % (2903041)CaDiCaL version: 2.1.3
% 22.51/4.40 % (2903041)Termination reason: Instruction limit
% 22.51/4.40 % (2903041)Termination phase: Saturation
% 22.51/4.40 % (2903041)Time elapsed: 0.110 s
% 22.51/4.40 % (2903041)Peak memory usage: 110 MB
% 22.51/4.40 % (2903041)Instructions burned: 297 (million)
% 22.51/4.40 % (2903045)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1164668145:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 22.51/4.40 % (2903047)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2538547219:i=127:av=off:fsr=off:sup=off_2986 on theBenchmark for (2986ds/127Mi)
% 22.51/4.40 % (2903048)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2895890606:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2986 on theBenchmark for (2986ds/114Mi)
% 22.51/4.40 % (2903048)Instruction limit reached!
% 22.51/4.40 % (2903048)------------------------------
% 22.51/4.40 % (2903048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.51/4.40 % (2903048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.51/4.40 % (2903048)CaDiCaL version: 2.1.3
% 22.51/4.40 % (2903048)Termination reason: Instruction limit
% 22.51/4.40 % (2903048)Termination phase: Property scanning
% 22.51/4.40 % (2903048)Time elapsed: 0.027 s
% 22.51/4.40 % (2903048)Peak memory usage: 102 MB
% 22.51/4.40 % (2903048)Instructions burned: 115 (million)
% 22.51/4.40 % (2903045)Instruction limit reached!
% 22.51/4.40 % (2903045)------------------------------
% 22.51/4.40 % (2903045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.43/4.66 % (2903045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.43/4.66 % (2903045)CaDiCaL version: 2.1.3
% 12.43/4.66 % (2903045)Termination reason: Instruction limit
% 12.43/4.66 % (2903045)Termination phase: Naming
% 12.43/4.66 % (2903045)Time elapsed: 0.101 s
% 12.43/4.66 % (2903045)Peak memory usage: 105 MB
% 12.43/4.66 % (2903045)Instructions burned: 114 (million)
% 12.43/4.66 % (2903047)Instruction limit reached!
% 12.43/4.66 % (2903047)------------------------------
% 12.43/4.66 % (2903047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.43/4.66 % (2903047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.43/4.66 % (2903047)CaDiCaL version: 2.1.3
% 12.43/4.66 % (2903047)Termination reason: Instruction limit
% 12.43/4.66 % (2903047)Termination phase: Preprocessing 2
% 12.43/4.66 % (2903047)Time elapsed: 0.103 s
% 12.43/4.66 % (2903047)Peak memory usage: 106 MB
% 12.43/4.66 % (2903047)Instructions burned: 127 (million)
% 12.43/4.66 % (2903052)lrs+10_1_sil=8000:sp=occurrence:random_seed=2467614793:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 12.43/4.66 % (2903053)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2891611024:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 12.43/4.66 % (2903054)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=514098233:i=5202:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/5202Mi)
% 12.43/4.66 % (2903052)Instruction limit reached!
% 12.43/4.66 % (2903052)------------------------------
% 12.43/4.66 % (2903052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.43/4.66 % (2903052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.43/4.66 % (2903052)CaDiCaL version: 2.1.3
% 12.43/4.66 % (2903052)Termination reason: Instruction limit
% 12.43/4.66 % (2903052)Termination phase: Saturation
% 12.43/4.66 % (2903052)Time elapsed: 0.295 s
% 12.43/4.66 % (2903052)Peak memory usage: 121 MB
% 12.43/4.66 % (2903052)Instructions burned: 908 (million)
% 12.43/4.66 % (2903053)Instruction limit reached!
% 12.43/4.66 % (2903053)------------------------------
% 12.43/4.66 % (2903053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.43/4.66 % (2903053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.43/4.66 % (2903053)CaDiCaL version: 2.1.3
% 12.43/4.66 % (2903053)Termination reason: Instruction limit
% 12.43/4.66 % (2903053)Termination phase: Saturation
% 12.43/4.66 % (2903053)Time elapsed: 0.270 s
% 12.43/4.66 % (2903053)Peak memory usage: 111 MB
% 12.43/4.66 % (2903053)Instructions burned: 438 (million)
% 12.43/4.66 % (2903058)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3955377511:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2980 on theBenchmark for (2980ds/134Mi)
% 12.43/4.66 % (2903058)Instruction limit reached!
% 12.43/4.66 % (2903058)------------------------------
% 12.43/4.66 % (2903058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.43/4.66 % (2903058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.43/4.66 % (2903058)CaDiCaL version: 2.1.3
% 12.43/4.66 % (2903058)Termination reason: Instruction limit
% 12.43/4.66 % (2903058)Termination phase: Property scanning
% 12.43/4.66 % (2903058)Time elapsed: 0.063 s
% 12.43/4.66 % (2903058)Peak memory usage: 106 MB
% 12.43/4.66 % (2903058)Instructions burned: 138 (million)
% 12.43/4.66 % (2903059)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2044416809:st=8:i=592:sd=3:ep=RST:ss=axioms_2980 on theBenchmark for (2980ds/592Mi)
% 12.43/4.66 % (2903061)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1736418083:st=3:i=13193:sd=3:ss=axioms_2979 on theBenchmark for (2979ds/13193Mi)
% 12.43/4.66 % (2903059)Instruction limit reached!
% 12.43/4.66 % (2903059)------------------------------
% 12.43/4.66 % (2903059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.43/4.66 % (2903059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.43/4.66 % (2903059)CaDiCaL version: 2.1.3
% 12.43/4.66 % (2903059)Termination reason: Instruction limit
% 12.43/4.66 % (2903059)Termination phase: Property scanning
% 12.43/4.66 % (2903059)Time elapsed: 0.400 s
% 12.43/4.66 % (2903059)Peak memory usage: 124 MB
% 12.43/4.66 % (2903059)Instructions burned: 594 (million)
% 12.43/4.66 % (2903064)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=3598957240:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/125Mi)
% 12.43/4.66 % (2903064)Instruction limit reached!
% 12.43/4.66 % (2903064)------------------------------
% 12.43/4.66 % (2903064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.43/4.66 % (2903064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.43/4.66 % (2903064)CaDiCaL version: 2.1.3
% 12.43/4.66 % (2903064)Termination reason: Instruction limit
% 12.43/4.66 % (2903064)Termination phase: Property scanning
% 12.43/4.66 % (2903064)Time elapsed: 0.055 s
% 12.43/4.66 % (2903064)Peak memory usage: 102 MB
% 12.43/4.66 % (2903064)Instructions burned: 125 (million)
% 12.43/4.66 % (2903043)Instruction limit reached!
% 12.43/4.66 % (2903043)------------------------------
% 12.43/4.66 % (2903043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.43/4.66 % (2903043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.43/4.66 % (2903043)CaDiCaL version: 2.1.3
% 12.43/4.66 % (2903043)Termination reason: Instruction limit
% 12.43/4.66 % (2903043)Termination phase: Saturation
% 12.43/4.66 % (2903043)Time elapsed: 1.463 s
% 12.43/4.66 % (2903043)Peak memory usage: 239 MB
% 12.43/4.66 % (2903043)Instructions burned: 2351 (million)
% 12.43/4.66 % (2903066)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2821959127:i=134:gtgl=5:slsql=off:gtg=exists_sym_2972 on theBenchmark for (2972ds/134Mi)
% 12.43/4.66 % (2903067)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3856096873:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/141Mi)
% 12.43/4.66 % (2903066)Instruction limit reached!
% 12.43/4.66 % (2903066)------------------------------
% 12.43/4.66 % (2903066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.43/4.66 % (2903066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.43/4.66 % (2903066)CaDiCaL version: 2.1.3
% 12.43/4.66 % (2903066)Termination reason: Instruction limit
% 12.43/4.66 % (2903066)Termination phase: Property scanning
% 12.43/4.66 % (2903066)Time elapsed: 0.059 s
% 12.43/4.66 % (2903066)Peak memory usage: 102 MB
% 12.43/4.66 % (2903066)Instructions burned: 134 (million)
% 12.43/4.66 % (2903067)Instruction limit reached!
% 12.43/4.66 % (2903067)------------------------------
% 12.43/4.66 % (2903067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.43/4.66 % (2903067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.43/4.66 % (2903067)CaDiCaL version: 2.1.3
% 12.43/4.66 % (2903067)Termination reason: Instruction limit
% 12.43/4.66 % (2903067)Termination phase: Saturation
% 12.43/4.66 % (2903067)Time elapsed: 0.107 s
% 12.43/4.66 % (2903067)Peak memory usage: 108 MB
% 12.43/4.66 % (2903067)Instructions burned: 142 (million)
% 12.43/4.66 % (2903070)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3864451009:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2970 on theBenchmark for (2970ds/431Mi)
% 12.43/4.66 % (2903071)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=1482667952:i=6060:aac=none:ins=25_2969 on theBenchmark for (2969ds/6060Mi)
% 12.43/4.66 % (2903070)Instruction limit reached!
% 12.43/4.66 % (2903070)------------------------------
% 12.43/4.66 % (2903070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.43/4.66 % (2903070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.43/4.66 % (2903070)CaDiCaL version: 2.1.3
% 12.43/4.66 % (2903070)Termination reason: Instruction limit
% 12.43/4.66 % (2903070)Termination phase: Saturation
% 12.43/4.66 % (2903070)Time elapsed: 0.280 s
% 12.43/4.66 % (2903070)Peak memory usage: 111 MB
% 12.43/4.66 % (2903070)Instructions burned: 432 (million)
% 12.43/4.66 % (2903074)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1896944820:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2965 on theBenchmark for (2965ds/150Mi)
% 12.43/4.66 % (2903021)First to succeed.
% 12.43/4.66 % (2903021)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2903015"
% 12.43/4.66 % (2903074)Instruction limit reached!
% 12.43/4.66 % (2903074)------------------------------
% 12.43/4.66 % (2903074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.43/4.66 % (2903074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.43/4.66 % (2903074)CaDiCaL version: 2.1.3
% 12.43/4.66 % (2903074)Termination reason: Instruction limit
% 12.43/4.66 % (2903074)Termination phase: Preprocessing 1
% 12.43/4.66 % (2903074)Time elapsed: 0.114 s
% 12.43/4.66 % (2903074)Peak memory usage: 103 MB
% 12.43/4.66 % (2903074)Instructions burned: 150 (million)
% 12.43/4.66 % (2903076)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1328061911:i=14155:bd=all_2962 on theBenchmark for (2962ds/14155Mi)
% 12.43/4.66 % (2903021)Refutation found. Thanks to Tanya!
% 12.43/4.66 % SZS status Theorem for theBenchmark
% 12.43/4.66 % SZS output start Proof for theBenchmark
% See solution above
% 24.54/4.86 % (2903021)------------------------------
% 24.54/4.86 % (2903021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.54/4.86 % (2903021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.54/4.86 % (2903021)CaDiCaL version: 2.1.3
% 24.54/4.86 % (2903021)Termination reason: Refutation
% 24.54/4.86 % (2903021)Time elapsed: 2.823 s
% 24.54/4.86 % (2903021)Peak memory usage: 224 MB
% 24.54/4.86 % (2903021)Instructions burned: 4403 (million)
% 24.54/4.86 % (2903021)------------------------------
% 24.54/4.86 % (2903021)------------------------------
% 24.54/4.86 % (2903015)Success in time 3.983 s
% 24.54/4.86 % Vampire exiting
%------------------------------------------------------------------------------