%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : TOP033+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n008.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 17.72s 6.45s
% Output : Refutation 37.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 27
% Syntax : Number of formulae : 287 ( 40 unt; 5 def)
% Number of atoms : 1363 ( 141 equ)
% Maximal formula atoms : 19 ( 4 avg)
% Number of connectives : 1843 ( 767 ~; 864 |; 138 &)
% ( 24 <=>; 50 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 6 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 25 ( 23 usr; 6 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 3 con; 0-4 aty)
% Number of variables : 383 ( 0 sgn 370 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f258,axiom,
! [X0] : k2_tarski(X0,X0) = k1_tarski(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f480,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
=> ( m1_subset_1(X1,X0)
<=> r2_hidden(X1,X0) ) )
& ( v1_xboole_0(X0)
=> ( m1_subset_1(X1,X0)
<=> v1_xboole_0(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_subset_1) ).
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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',d3_pre_topc) ).
fof(f6850,axiom,
! [X0] :
( l1_pre_topc(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',t23_tex_4) ).
fof(f13369,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> ( ~ v1_xboole_0(k4_tex_4(X0,X1))
& m1_subset_1(k4_tex_4(X0,X1),k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',d8_tsp_2) ).
fof(f13510,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ! [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)) ) )
=> v3_borsuk_1(X2,X0,X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t20_tsp_2) ).
fof(f13511,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))
& v5_pre_topc(X2,X0,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)) )
=> v3_borsuk_1(X2,X0,X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t21_tsp_2) ).
fof(f13512,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))
& v5_pre_topc(X2,X0,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)) )
=> v3_borsuk_1(X2,X0,X1) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f13511]) ).
fof(f13600,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(f13601,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,[],[f13600]) ).
fof(f13634,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(f13635,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,[],[f13634]) ).
fof(f13640,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(f13641,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,[],[f13640]) ).
fof(f13676,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( v3_borsuk_1(X2,X0,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))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13510]) ).
fof(f13677,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( v3_borsuk_1(X2,X0,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))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f13676]) ).
fof(f13678,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ v3_borsuk_1(X2,X0,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))
& v5_pre_topc(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13512]) ).
fof(f13679,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ v3_borsuk_1(X2,X0,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))
& v5_pre_topc(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(flattening,[],[f13678]) ).
fof(f13688,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(f13689,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,[],[f13688]) ).
fof(f13737,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(f13738,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(flattening,[],[f13737]) ).
fof(f13749,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(f13750,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,[],[f13749]) ).
fof(f13781,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(f13782,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,[],[f13781]) ).
fof(f13783,plain,
! [X0,X1] :
( ( ~ v1_xboole_0(k4_tex_4(X0,X1))
& m1_subset_1(k4_tex_4(X0,X1),k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f13369]) ).
fof(f13784,plain,
! [X0,X1] :
( ( ~ v1_xboole_0(k4_tex_4(X0,X1))
& m1_subset_1(k4_tex_4(X0,X1),k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f13783]) ).
fof(f13816,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(f13817,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,[],[f13816]) ).
fof(f14107,plain,
! [X0,X1] :
( ( ( m1_subset_1(X1,X0)
<=> r2_hidden(X1,X0) )
| v1_xboole_0(X0) )
& ( ( m1_subset_1(X1,X0)
<=> v1_xboole_0(X1) )
| ~ v1_xboole_0(X0) ) ),
inference(ennf_transformation,[],[f480]) ).
fof(f14189,plain,
! [X0] :
( ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13461]) ).
fof(f14191,plain,
! [X0] :
( ! [X1] :
( l1_pre_topc(X1)
| ~ m2_tsp_1(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13459]) ).
fof(f14449,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(f14450,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,[],[f14449]) ).
fof(f14451,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(f14452,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,[],[f14451]) ).
fof(f14571,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(f14572,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,[],[f14571]) ).
fof(f14811,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f6850]) ).
fof(f14815,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f6422]) ).
fof(f14816,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f14815]) ).
fof(f15118,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f6788]) ).
fof(f20641,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,[],[f13601]) ).
fof(f20642,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,[],[f20641]) ).
fof(f20643,plain,
! [X0] :
( ! [X1] :
( ( ( v1_tsp_1(X1,X0)
| ( k1_struct_0(X0,sK51(X0,X1)) != k5_subset_1(u1_struct_0(X0),X1,k4_tex_4(X0,sK51(X0,X1)))
& r2_hidden(sK51(X0,X1),X1)
& m1_subset_1(sK51(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,[sK51]),skolemize(X2,sK51(X0,X1))],[f20642]) ).
fof(f20662,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,[],[f13641]) ).
fof(f20663,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,[],[f20662]) ).
fof(f20664,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,[],[f20663]) ).
fof(f20665,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(sK60(X0,X1)),u1_pre_topc(sK60(X0,X1)))
& m2_tsp_1(X1,sK60(X0,X1))
& ~ v3_struct_0(sK60(X0,X1))
& v2_t_0topsp(sK60(X0,X1))
& m2_tsp_1(sK60(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,[sK60]),skolemize(X2,sK60(X0,X1))],[f20664]) ).
fof(f20683,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( v3_borsuk_1(X2,X0,X1)
| u1_struct_0(X1) != X3
| ( k5_subset_1(u1_struct_0(X0),X3,k4_tex_4(X0,sK68(X0,X1,X2,X3))) != k1_struct_0(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,sK68(X0,X1,X2,X3)))
& m1_subset_1(sK68(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))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK68]),skolemize(X4,sK68(X0,X1,X2,X3))],[f13677]) ).
fof(f20684,plain,
( ~ v3_borsuk_1(sK71,sK69,sK70)
& ! [X3] :
( r2_hidden(k8_funct_2(u1_struct_0(sK69),u1_struct_0(sK70),sK71,X3),k4_tex_4(sK69,X3))
| ~ m1_subset_1(X3,u1_struct_0(sK69)) )
& v1_funct_1(sK71)
& v1_funct_2(sK71,u1_struct_0(sK69),u1_struct_0(sK70))
& v5_pre_topc(sK71,sK69,sK70)
& m2_relset_1(sK71,u1_struct_0(sK69),u1_struct_0(sK70))
& ~ v3_struct_0(sK70)
& v2_tsp_2(sK70,sK69)
& m2_tsp_1(sK70,sK69)
& ~ v3_struct_0(sK69)
& v2_pre_topc(sK69)
& l1_pre_topc(sK69) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK69,sK70,sK71]),skolemize(X0,sK69),skolemize(X1,sK70),skolemize(X2,sK71)],[f13679]) ).
fof(f20719,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,[],[f13750]) ).
fof(f20832,plain,
! [X0,X1] :
( ( ( ( m1_subset_1(X1,X0)
| ~ r2_hidden(X1,X0) )
& ( r2_hidden(X1,X0)
| ~ m1_subset_1(X1,X0) ) )
| v1_xboole_0(X0) )
& ( ( ( m1_subset_1(X1,X0)
| ~ v1_xboole_0(X1) )
& ( v1_xboole_0(X1)
| ~ m1_subset_1(X1,X0) ) )
| ~ v1_xboole_0(X0) ) ),
inference(nnf_transformation,[],[f14107]) ).
fof(f20859,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,[],[f14189]) ).
fof(f20984,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(f21002,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,[],[f14572]) ).
fof(f22958,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,[],[f20643]) ).
fof(f23002,plain,
! [X0,X1] :
( ~ m2_tsp_1(X1,X0)
| m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f13635]) ).
fof(f23008,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,[],[f20665]) ).
fof(f23078,plain,
! [X2,X3,X0,X1] :
( v3_borsuk_1(X2,X0,X1)
| u1_struct_0(X1) != X3
| m1_subset_1(sK68(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))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f20683]) ).
fof(f23079,plain,
! [X2,X3,X0,X1] :
( v3_borsuk_1(X2,X0,X1)
| u1_struct_0(X1) != X3
| k5_subset_1(u1_struct_0(X0),X3,k4_tex_4(X0,sK68(X0,X1,X2,X3))) != k1_struct_0(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,sK68(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))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f20683]) ).
fof(f23080,plain,
l1_pre_topc(sK69),
inference(cnf_transformation,[],[f20684]) ).
fof(f23081,plain,
v2_pre_topc(sK69),
inference(cnf_transformation,[],[f20684]) ).
fof(f23082,plain,
~ v3_struct_0(sK69),
inference(cnf_transformation,[],[f20684]) ).
fof(f23083,plain,
m2_tsp_1(sK70,sK69),
inference(cnf_transformation,[],[f20684]) ).
fof(f23084,plain,
v2_tsp_2(sK70,sK69),
inference(cnf_transformation,[],[f20684]) ).
fof(f23085,plain,
~ v3_struct_0(sK70),
inference(cnf_transformation,[],[f20684]) ).
fof(f23086,plain,
m2_relset_1(sK71,u1_struct_0(sK69),u1_struct_0(sK70)),
inference(cnf_transformation,[],[f20684]) ).
fof(f23087,plain,
v5_pre_topc(sK71,sK69,sK70),
inference(cnf_transformation,[],[f20684]) ).
fof(f23088,plain,
v1_funct_2(sK71,u1_struct_0(sK69),u1_struct_0(sK70)),
inference(cnf_transformation,[],[f20684]) ).
fof(f23089,plain,
v1_funct_1(sK71),
inference(cnf_transformation,[],[f20684]) ).
fof(f23090,plain,
! [X3] :
( r2_hidden(k8_funct_2(u1_struct_0(sK69),u1_struct_0(sK70),sK71,X3),k4_tex_4(sK69,X3))
| ~ m1_subset_1(X3,u1_struct_0(sK69)) ),
inference(cnf_transformation,[],[f20684]) ).
fof(f23091,plain,
~ v3_borsuk_1(sK71,sK69,sK70),
inference(cnf_transformation,[],[f20684]) ).
fof(f23100,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,[],[f13689]) ).
fof(f23194,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(cnf_transformation,[],[f13738]) ).
fof(f23213,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,[],[f20719]) ).
fof(f23303,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,[],[f13782]) ).
fof(f23304,plain,
! [X0,X1] :
( m1_subset_1(k4_tex_4(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f13784]) ).
fof(f23329,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,[],[f13817]) ).
fof(f23696,plain,
! [X0,X1] :
( r2_hidden(X1,X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f20832]) ).
fof(f23786,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ m2_tsp_1(X1,X0)
| m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f20859]) ).
fof(f23789,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ m2_tsp_1(X1,X0)
| l1_pre_topc(X1) ),
inference(cnf_transformation,[],[f14191]) ).
fof(f24355,plain,
! [X2,X3,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| k1_funct_1(X2,X3) = k8_funct_2(X0,X1,X2,X3)
| ~ m1_subset_1(X3,X0) ),
inference(cnf_transformation,[],[f14450]) ).
fof(f24356,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,[],[f14452]) ).
fof(f24364,plain,
! [X2,X0,X1] :
( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f20984]) ).
fof(f24526,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,[],[f21002]) ).
fof(f24895,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f14811]) ).
fof(f24901,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f14816]) ).
fof(f25459,plain,
! [X0] :
( ~ l1_struct_0(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(cnf_transformation,[],[f15118]) ).
fof(f26156,plain,
! [X0] : k1_tarski(X0) = k2_tarski(X0,X0),
inference(cnf_transformation,[],[f258]) ).
fof(f32996,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,[],[f23329,f26156]) ).
fof(f35089,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| k5_subset_1(u1_struct_0(X0),u1_struct_0(X1),k4_tex_4(X0,sK68(X0,X1,X2,u1_struct_0(X1)))) != k1_struct_0(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,sK68(X0,X1,X2,u1_struct_0(X1))))
| v3_borsuk_1(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(equality_resolution,[],[f23079]) ).
fof(f35090,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| m1_subset_1(sK68(X0,X1,X2,u1_struct_0(X1)),u1_struct_0(X0))
| v3_borsuk_1(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(equality_resolution,[],[f23078]) ).
fof(f35093,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,[],[f23213]) ).
fof(f36708,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,[],[f22958,f23194]) ).
fof(f37043,plain,
! [X0] :
( ~ m2_tsp_1(X0,sK69)
| l1_pre_topc(X0) ),
inference(resolution,[],[f23789,f23080]) ).
fof(f37045,plain,
! [X0] :
( ~ m2_tsp_1(X0,sK69)
| m1_pre_topc(X0,sK69) ),
inference(resolution,[],[f23786,f23080]) ).
fof(f37046,plain,
m1_pre_topc(sK70,sK69),
inference(resolution,[],[f37045,f23083]) ).
fof(f37047,plain,
l1_pre_topc(sK70),
inference(resolution,[],[f37043,f23083]) ).
fof(f37052,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(resolution,[],[f25459,f24895]) ).
fof(f37053,plain,
u1_struct_0(sK69) = k2_pre_topc(sK69),
inference(resolution,[],[f37052,f23080]) ).
fof(f37054,plain,
u1_struct_0(sK70) = k2_pre_topc(sK70),
inference(resolution,[],[f37052,f37047]) ).
fof(f37055,plain,
! [X0] :
( r2_hidden(k8_funct_2(k2_pre_topc(sK69),u1_struct_0(sK70),sK71,X0),k4_tex_4(sK69,X0))
| ~ m1_subset_1(X0,k2_pre_topc(sK69)) ),
inference(superposition,[],[f23090,f37053]) ).
fof(f37056,plain,
v1_funct_2(sK71,k2_pre_topc(sK69),u1_struct_0(sK70)),
inference(superposition,[],[f23088,f37053]) ).
fof(f37057,plain,
m2_relset_1(sK71,k2_pre_topc(sK69),u1_struct_0(sK70)),
inference(superposition,[],[f23086,f37053]) ).
fof(f37058,plain,
! [X0] :
( m1_subset_1(k4_tex_4(sK69,X0),k1_zfmisc_1(k2_pre_topc(sK69)))
| v3_struct_0(sK69)
| ~ v2_pre_topc(sK69)
| ~ l1_pre_topc(sK69)
| ~ m1_subset_1(X0,k2_pre_topc(sK69)) ),
inference(superposition,[],[f23304,f37053]) ).
fof(f37061,plain,
! [X0,X1] :
( ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK69)))
| k5_subset_1(k2_pre_topc(sK69),u1_struct_0(X0),k4_tex_4(sK69,sK68(sK69,X0,X1,u1_struct_0(X0)))) != k1_struct_0(X0,k8_funct_2(k2_pre_topc(sK69),u1_struct_0(X0),X1,sK68(sK69,X0,X1,u1_struct_0(X0))))
| v3_borsuk_1(X1,sK69,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_pre_topc(sK69),u1_struct_0(X0))
| ~ v5_pre_topc(X1,sK69,X0)
| ~ m2_relset_1(X1,k2_pre_topc(sK69),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK69)
| ~ m2_tsp_1(X0,sK69)
| v3_struct_0(sK69)
| ~ v2_pre_topc(sK69)
| ~ l1_pre_topc(sK69) ),
inference(superposition,[],[f35089,f37053]) ).
fof(f37063,plain,
! [X0,X1] :
( ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK69)))
| m1_subset_1(sK68(sK69,X0,X1,u1_struct_0(X0)),k2_pre_topc(sK69))
| v3_borsuk_1(X1,sK69,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_pre_topc(sK69),u1_struct_0(X0))
| ~ v5_pre_topc(X1,sK69,X0)
| ~ m2_relset_1(X1,k2_pre_topc(sK69),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK69)
| ~ m2_tsp_1(X0,sK69)
| v3_struct_0(sK69)
| ~ v2_pre_topc(sK69)
| ~ l1_pre_topc(sK69) ),
inference(superposition,[],[f35090,f37053]) ).
fof(f37076,plain,
! [X0,X1] :
( ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK69)))
| m1_subset_1(sK68(sK69,X0,X1,u1_struct_0(X0)),k2_pre_topc(sK69))
| v3_borsuk_1(X1,sK69,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_pre_topc(sK69),u1_struct_0(X0))
| ~ v5_pre_topc(X1,sK69,X0)
| ~ m2_relset_1(X1,k2_pre_topc(sK69),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK69)
| ~ m2_tsp_1(X0,sK69)
| ~ v2_pre_topc(sK69)
| ~ l1_pre_topc(sK69) ),
inference(forward_subsumption_resolution,[],[f37063,f23082]) ).
fof(f37077,plain,
! [X0,X1] :
( ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK69)))
| k5_subset_1(k2_pre_topc(sK69),u1_struct_0(X0),k4_tex_4(sK69,sK68(sK69,X0,X1,u1_struct_0(X0)))) != k1_struct_0(X0,k8_funct_2(k2_pre_topc(sK69),u1_struct_0(X0),X1,sK68(sK69,X0,X1,u1_struct_0(X0))))
| v3_borsuk_1(X1,sK69,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_pre_topc(sK69),u1_struct_0(X0))
| ~ v5_pre_topc(X1,sK69,X0)
| ~ m2_relset_1(X1,k2_pre_topc(sK69),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK69)
| ~ m2_tsp_1(X0,sK69)
| ~ v2_pre_topc(sK69)
| ~ l1_pre_topc(sK69) ),
inference(forward_subsumption_resolution,[],[f37061,f23082]) ).
fof(f37080,plain,
! [X0] :
( m1_subset_1(k4_tex_4(sK69,X0),k1_zfmisc_1(k2_pre_topc(sK69)))
| ~ v2_pre_topc(sK69)
| ~ l1_pre_topc(sK69)
| ~ m1_subset_1(X0,k2_pre_topc(sK69)) ),
inference(forward_subsumption_resolution,[],[f37058,f23082]) ).
fof(f37081,plain,
m2_relset_1(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70)),
inference(forward_demodulation,[],[f37057,f37054]) ).
fof(f37082,plain,
v1_funct_2(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70)),
inference(forward_demodulation,[],[f37056,f37054]) ).
fof(f37083,plain,
! [X0] :
( r2_hidden(k8_funct_2(k2_pre_topc(sK69),k2_pre_topc(sK70),sK71,X0),k4_tex_4(sK69,X0))
| ~ m1_subset_1(X0,k2_pre_topc(sK69)) ),
inference(forward_demodulation,[],[f37055,f37054]) ).
fof(f37084,plain,
! [X0,X1] :
( ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK69)))
| m1_subset_1(sK68(sK69,X0,X1,u1_struct_0(X0)),k2_pre_topc(sK69))
| v3_borsuk_1(X1,sK69,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_pre_topc(sK69),u1_struct_0(X0))
| ~ v5_pre_topc(X1,sK69,X0)
| ~ m2_relset_1(X1,k2_pre_topc(sK69),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK69)
| ~ m2_tsp_1(X0,sK69)
| ~ l1_pre_topc(sK69) ),
inference(forward_subsumption_resolution,[],[f37076,f23081]) ).
fof(f37085,plain,
! [X0,X1] :
( ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK69)))
| k5_subset_1(k2_pre_topc(sK69),u1_struct_0(X0),k4_tex_4(sK69,sK68(sK69,X0,X1,u1_struct_0(X0)))) != k1_struct_0(X0,k8_funct_2(k2_pre_topc(sK69),u1_struct_0(X0),X1,sK68(sK69,X0,X1,u1_struct_0(X0))))
| v3_borsuk_1(X1,sK69,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_pre_topc(sK69),u1_struct_0(X0))
| ~ v5_pre_topc(X1,sK69,X0)
| ~ m2_relset_1(X1,k2_pre_topc(sK69),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK69)
| ~ m2_tsp_1(X0,sK69)
| ~ l1_pre_topc(sK69) ),
inference(forward_subsumption_resolution,[],[f37077,f23081]) ).
fof(f37088,plain,
! [X0] :
( m1_subset_1(k4_tex_4(sK69,X0),k1_zfmisc_1(k2_pre_topc(sK69)))
| ~ l1_pre_topc(sK69)
| ~ m1_subset_1(X0,k2_pre_topc(sK69)) ),
inference(forward_subsumption_resolution,[],[f37080,f23081]) ).
fof(f37089,plain,
! [X0,X1] :
( ~ v2_tsp_2(X0,sK69)
| m1_subset_1(sK68(sK69,X0,X1,u1_struct_0(X0)),k2_pre_topc(sK69))
| v3_borsuk_1(X1,sK69,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_pre_topc(sK69),u1_struct_0(X0))
| ~ v5_pre_topc(X1,sK69,X0)
| ~ m2_relset_1(X1,k2_pre_topc(sK69),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK69)))
| ~ m2_tsp_1(X0,sK69) ),
inference(forward_subsumption_resolution,[],[f37084,f23080]) ).
fof(f37090,plain,
! [X0,X1] :
( ~ v2_tsp_2(X0,sK69)
| k5_subset_1(k2_pre_topc(sK69),u1_struct_0(X0),k4_tex_4(sK69,sK68(sK69,X0,X1,u1_struct_0(X0)))) != k1_struct_0(X0,k8_funct_2(k2_pre_topc(sK69),u1_struct_0(X0),X1,sK68(sK69,X0,X1,u1_struct_0(X0))))
| v3_borsuk_1(X1,sK69,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_pre_topc(sK69),u1_struct_0(X0))
| ~ v5_pre_topc(X1,sK69,X0)
| ~ m2_relset_1(X1,k2_pre_topc(sK69),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK69)))
| ~ m2_tsp_1(X0,sK69) ),
inference(forward_subsumption_resolution,[],[f37085,f23080]) ).
fof(f37093,plain,
! [X0] :
( m1_subset_1(k4_tex_4(sK69,X0),k1_zfmisc_1(k2_pre_topc(sK69)))
| ~ m1_subset_1(X0,k2_pre_topc(sK69)) ),
inference(forward_subsumption_resolution,[],[f37088,f23080]) ).
fof(f37150,plain,
! [X0] :
( ~ v2_tsp_2(X0,sK69)
| v3_struct_0(X0)
| ~ m2_tsp_1(X0,sK69)
| v3_struct_0(sK69)
| v2_t_0topsp(X0)
| ~ l1_pre_topc(sK69) ),
inference(resolution,[],[f23008,f23081]) ).
fof(f37151,plain,
! [X0] :
( ~ v2_tsp_2(X0,sK69)
| v3_struct_0(X0)
| ~ m2_tsp_1(X0,sK69)
| v2_t_0topsp(X0)
| ~ l1_pre_topc(sK69) ),
inference(forward_subsumption_resolution,[],[f37150,f23082]) ).
fof(f37152,plain,
! [X0] :
( ~ v2_tsp_2(X0,sK69)
| v3_struct_0(X0)
| ~ m2_tsp_1(X0,sK69)
| v2_t_0topsp(X0) ),
inference(forward_subsumption_resolution,[],[f37151,f23080]) ).
fof(f37153,plain,
( v3_struct_0(sK70)
| ~ m2_tsp_1(sK70,sK69)
| v2_t_0topsp(sK70) ),
inference(resolution,[],[f37152,f23084]) ).
fof(f37154,plain,
( ~ m2_tsp_1(sK70,sK69)
| v2_t_0topsp(sK70) ),
inference(forward_subsumption_resolution,[],[f37153,f23085]) ).
fof(f37155,plain,
v2_t_0topsp(sK70),
inference(forward_subsumption_resolution,[],[f37154,f23083]) ).
fof(f37156,plain,
( m1_subset_1(u1_struct_0(sK70),k1_zfmisc_1(u1_struct_0(sK69)))
| v3_struct_0(sK69)
| ~ l1_pre_topc(sK69) ),
inference(resolution,[],[f23002,f23083]) ).
fof(f37161,plain,
( m1_subset_1(u1_struct_0(sK70),k1_zfmisc_1(u1_struct_0(sK69)))
| ~ l1_pre_topc(sK69) ),
inference(forward_subsumption_resolution,[],[f37156,f23082]) ).
fof(f37162,plain,
m1_subset_1(u1_struct_0(sK70),k1_zfmisc_1(u1_struct_0(sK69))),
inference(forward_subsumption_resolution,[],[f37161,f23080]) ).
fof(f37163,plain,
m1_subset_1(u1_struct_0(sK70),k1_zfmisc_1(k2_pre_topc(sK69))),
inference(forward_demodulation,[],[f37162,f37053]) ).
fof(f37164,plain,
m1_subset_1(k2_pre_topc(sK70),k1_zfmisc_1(k2_pre_topc(sK69))),
inference(forward_demodulation,[],[f37163,f37054]) ).
fof(f37170,plain,
! [X0] :
( v3_struct_0(sK69)
| k4_tex_4(sK69,X0) = k2_tex_4(sK69,X0)
| ~ l1_pre_topc(sK69)
| ~ m1_subset_1(X0,u1_struct_0(sK69)) ),
inference(resolution,[],[f23303,f23081]) ).
fof(f37171,plain,
! [X0] :
( k4_tex_4(sK69,X0) = k2_tex_4(sK69,X0)
| ~ l1_pre_topc(sK69)
| ~ m1_subset_1(X0,u1_struct_0(sK69)) ),
inference(forward_subsumption_resolution,[],[f37170,f23082]) ).
fof(f37172,plain,
! [X0] :
( k4_tex_4(sK69,X0) = k2_tex_4(sK69,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK69)) ),
inference(forward_subsumption_resolution,[],[f37171,f23080]) ).
fof(f37173,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(sK69))
| k4_tex_4(sK69,X0) = k2_tex_4(sK69,X0) ),
inference(forward_demodulation,[],[f37172,f37053]) ).
fof(f37191,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_1(X1)
| v1_xboole_0(X0)
| ~ v1_funct_2(X1,X0,X2)
| k1_funct_1(X1,X3) = k8_funct_2(X0,X2,X1,X3)
| ~ m1_subset_1(X3,X0)
| ~ m2_relset_1(X1,X0,X2) ),
inference(resolution,[],[f24355,f24364]) ).
fof(f37197,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(resolution,[],[f24901,f24895]) ).
fof(f37253,plain,
( ~ v1_xboole_0(k2_pre_topc(sK69))
| v3_struct_0(sK69)
| ~ l1_pre_topc(sK69) ),
inference(superposition,[],[f37197,f37053]) ).
fof(f37254,plain,
( ~ v1_xboole_0(k2_pre_topc(sK70))
| v3_struct_0(sK70)
| ~ l1_pre_topc(sK70) ),
inference(superposition,[],[f37197,f37054]) ).
fof(f37255,plain,
( ~ v1_xboole_0(k2_pre_topc(sK70))
| ~ l1_pre_topc(sK70) ),
inference(forward_subsumption_resolution,[],[f37254,f23085]) ).
fof(f37256,plain,
( ~ v1_xboole_0(k2_pre_topc(sK69))
| ~ l1_pre_topc(sK69) ),
inference(forward_subsumption_resolution,[],[f37253,f23082]) ).
fof(f37257,plain,
~ v1_xboole_0(k2_pre_topc(sK70)),
inference(forward_subsumption_resolution,[],[f37255,f37047]) ).
fof(f37258,plain,
~ v1_xboole_0(k2_pre_topc(sK69)),
inference(forward_subsumption_resolution,[],[f37256,f23080]) ).
fof(f37259,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(sK71,X0,X1)
| v1_xboole_0(X0)
| k1_funct_1(sK71,X2) = k8_funct_2(X0,X1,sK71,X2)
| ~ m1_subset_1(X2,X0)
| ~ m2_relset_1(sK71,X0,X1) ),
inference(resolution,[],[f37191,f23089]) ).
fof(f37262,plain,
! [X0] :
( v1_xboole_0(k2_pre_topc(sK69))
| k8_funct_2(k2_pre_topc(sK69),k2_pre_topc(sK70),sK71,X0) = k1_funct_1(sK71,X0)
| ~ m1_subset_1(X0,k2_pre_topc(sK69))
| ~ m2_relset_1(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70)) ),
inference(resolution,[],[f37259,f37082]) ).
fof(f37263,plain,
! [X0] :
( k8_funct_2(k2_pre_topc(sK69),k2_pre_topc(sK70),sK71,X0) = k1_funct_1(sK71,X0)
| ~ m1_subset_1(X0,k2_pre_topc(sK69))
| ~ m2_relset_1(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70)) ),
inference(forward_subsumption_resolution,[],[f37262,f37258]) ).
fof(f37265,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(sK69))
| k8_funct_2(k2_pre_topc(sK69),k2_pre_topc(sK70),sK71,X0) = k1_funct_1(sK71,X0) ),
inference(forward_subsumption_resolution,[],[f37263,f37081]) ).
fof(f37322,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| v3_struct_0(X1)
| ~ m1_pre_topc(X1,sK69)
| v3_struct_0(sK69)
| m1_subset_1(X0,u1_struct_0(sK69))
| ~ l1_pre_topc(sK69) ),
inference(resolution,[],[f23100,f23081]) ).
fof(f37323,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| v3_struct_0(X1)
| ~ m1_pre_topc(X1,sK69)
| m1_subset_1(X0,u1_struct_0(sK69))
| ~ l1_pre_topc(sK69) ),
inference(forward_subsumption_resolution,[],[f37322,f23082]) ).
fof(f37324,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| v3_struct_0(X1)
| ~ m1_pre_topc(X1,sK69)
| m1_subset_1(X0,u1_struct_0(sK69)) ),
inference(forward_subsumption_resolution,[],[f37323,f23080]) ).
fof(f37325,plain,
! [X0,X1] :
( ~ m1_pre_topc(X1,sK69)
| ~ m1_subset_1(X0,u1_struct_0(X1))
| v3_struct_0(X1)
| m1_subset_1(X0,k2_pre_topc(sK69)) ),
inference(forward_demodulation,[],[f37324,f37053]) ).
fof(f37326,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK70))
| v3_struct_0(sK70)
| m1_subset_1(X0,k2_pre_topc(sK69)) ),
inference(resolution,[],[f37325,f37046]) ).
fof(f37327,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK70))
| m1_subset_1(X0,k2_pre_topc(sK69)) ),
inference(forward_subsumption_resolution,[],[f37326,f23085]) ).
fof(f37328,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(sK70))
| m1_subset_1(X0,k2_pre_topc(sK69)) ),
inference(forward_demodulation,[],[f37327,f37054]) ).
fof(f37553,plain,
! [X0] :
( k5_subset_1(k2_pre_topc(sK69),u1_struct_0(sK70),k4_tex_4(sK69,sK68(sK69,sK70,X0,u1_struct_0(sK70)))) != k1_struct_0(sK70,k8_funct_2(k2_pre_topc(sK69),u1_struct_0(sK70),X0,sK68(sK69,sK70,X0,u1_struct_0(sK70))))
| v3_borsuk_1(X0,sK69,sK70)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_pre_topc(sK69),u1_struct_0(sK70))
| ~ v5_pre_topc(X0,sK69,sK70)
| ~ m2_relset_1(X0,k2_pre_topc(sK69),u1_struct_0(sK70))
| v3_struct_0(sK70)
| ~ m1_subset_1(u1_struct_0(sK70),k1_zfmisc_1(k2_pre_topc(sK69)))
| ~ m2_tsp_1(sK70,sK69) ),
inference(resolution,[],[f37090,f23084]) ).
fof(f37554,plain,
! [X0] :
( k5_subset_1(k2_pre_topc(sK69),u1_struct_0(sK70),k4_tex_4(sK69,sK68(sK69,sK70,X0,u1_struct_0(sK70)))) != k1_struct_0(sK70,k8_funct_2(k2_pre_topc(sK69),u1_struct_0(sK70),X0,sK68(sK69,sK70,X0,u1_struct_0(sK70))))
| v3_borsuk_1(X0,sK69,sK70)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_pre_topc(sK69),u1_struct_0(sK70))
| ~ v5_pre_topc(X0,sK69,sK70)
| ~ m2_relset_1(X0,k2_pre_topc(sK69),u1_struct_0(sK70))
| ~ m1_subset_1(u1_struct_0(sK70),k1_zfmisc_1(k2_pre_topc(sK69)))
| ~ m2_tsp_1(sK70,sK69) ),
inference(forward_subsumption_resolution,[],[f37553,f23085]) ).
fof(f37555,plain,
! [X0] :
( k5_subset_1(k2_pre_topc(sK69),u1_struct_0(sK70),k4_tex_4(sK69,sK68(sK69,sK70,X0,u1_struct_0(sK70)))) != k1_struct_0(sK70,k8_funct_2(k2_pre_topc(sK69),u1_struct_0(sK70),X0,sK68(sK69,sK70,X0,u1_struct_0(sK70))))
| v3_borsuk_1(X0,sK69,sK70)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_pre_topc(sK69),u1_struct_0(sK70))
| ~ v5_pre_topc(X0,sK69,sK70)
| ~ m2_relset_1(X0,k2_pre_topc(sK69),u1_struct_0(sK70))
| ~ m1_subset_1(u1_struct_0(sK70),k1_zfmisc_1(k2_pre_topc(sK69))) ),
inference(forward_subsumption_resolution,[],[f37554,f23083]) ).
fof(f37556,plain,
! [X0] :
( k5_subset_1(k2_pre_topc(sK69),k2_pre_topc(sK70),k4_tex_4(sK69,sK68(sK69,sK70,X0,k2_pre_topc(sK70)))) != k1_struct_0(sK70,k8_funct_2(k2_pre_topc(sK69),k2_pre_topc(sK70),X0,sK68(sK69,sK70,X0,k2_pre_topc(sK70))))
| v3_borsuk_1(X0,sK69,sK70)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_pre_topc(sK69),u1_struct_0(sK70))
| ~ v5_pre_topc(X0,sK69,sK70)
| ~ m2_relset_1(X0,k2_pre_topc(sK69),u1_struct_0(sK70))
| ~ m1_subset_1(u1_struct_0(sK70),k1_zfmisc_1(k2_pre_topc(sK69))) ),
inference(forward_demodulation,[],[f37555,f37054]) ).
fof(f37557,plain,
! [X0] :
( ~ v1_funct_2(X0,k2_pre_topc(sK69),k2_pre_topc(sK70))
| k5_subset_1(k2_pre_topc(sK69),k2_pre_topc(sK70),k4_tex_4(sK69,sK68(sK69,sK70,X0,k2_pre_topc(sK70)))) != k1_struct_0(sK70,k8_funct_2(k2_pre_topc(sK69),k2_pre_topc(sK70),X0,sK68(sK69,sK70,X0,k2_pre_topc(sK70))))
| v3_borsuk_1(X0,sK69,sK70)
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK69,sK70)
| ~ m2_relset_1(X0,k2_pre_topc(sK69),u1_struct_0(sK70))
| ~ m1_subset_1(u1_struct_0(sK70),k1_zfmisc_1(k2_pre_topc(sK69))) ),
inference(forward_demodulation,[],[f37556,f37054]) ).
fof(f37558,plain,
! [X0] :
( ~ m2_relset_1(X0,k2_pre_topc(sK69),k2_pre_topc(sK70))
| ~ v1_funct_2(X0,k2_pre_topc(sK69),k2_pre_topc(sK70))
| k5_subset_1(k2_pre_topc(sK69),k2_pre_topc(sK70),k4_tex_4(sK69,sK68(sK69,sK70,X0,k2_pre_topc(sK70)))) != k1_struct_0(sK70,k8_funct_2(k2_pre_topc(sK69),k2_pre_topc(sK70),X0,sK68(sK69,sK70,X0,k2_pre_topc(sK70))))
| v3_borsuk_1(X0,sK69,sK70)
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK69,sK70)
| ~ m1_subset_1(u1_struct_0(sK70),k1_zfmisc_1(k2_pre_topc(sK69))) ),
inference(forward_demodulation,[],[f37557,f37054]) ).
fof(f37559,plain,
! [X0] :
( ~ m1_subset_1(k2_pre_topc(sK70),k1_zfmisc_1(k2_pre_topc(sK69)))
| ~ m2_relset_1(X0,k2_pre_topc(sK69),k2_pre_topc(sK70))
| ~ v1_funct_2(X0,k2_pre_topc(sK69),k2_pre_topc(sK70))
| k5_subset_1(k2_pre_topc(sK69),k2_pre_topc(sK70),k4_tex_4(sK69,sK68(sK69,sK70,X0,k2_pre_topc(sK70)))) != k1_struct_0(sK70,k8_funct_2(k2_pre_topc(sK69),k2_pre_topc(sK70),X0,sK68(sK69,sK70,X0,k2_pre_topc(sK70))))
| v3_borsuk_1(X0,sK69,sK70)
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK69,sK70) ),
inference(forward_demodulation,[],[f37558,f37054]) ).
fof(f37560,plain,
! [X0] :
( k5_subset_1(k2_pre_topc(sK69),k2_pre_topc(sK70),k4_tex_4(sK69,sK68(sK69,sK70,X0,k2_pre_topc(sK70)))) != k1_struct_0(sK70,k8_funct_2(k2_pre_topc(sK69),k2_pre_topc(sK70),X0,sK68(sK69,sK70,X0,k2_pre_topc(sK70))))
| ~ v1_funct_2(X0,k2_pre_topc(sK69),k2_pre_topc(sK70))
| ~ m2_relset_1(X0,k2_pre_topc(sK69),k2_pre_topc(sK70))
| v3_borsuk_1(X0,sK69,sK70)
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK69,sK70) ),
inference(forward_subsumption_resolution,[],[f37559,f37164]) ).
fof(f37703,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k4_tex_4(sK69,X1))
| m1_subset_1(X0,k2_pre_topc(sK69))
| ~ m1_subset_1(X1,k2_pre_topc(sK69)) ),
inference(resolution,[],[f23194,f37093]) ).
fof(f38179,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,[],[f32996,f24895]) ).
fof(f38180,plain,
! [X0] :
( k2_tarski(X0,X0) = k1_struct_0(sK69,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK69))
| v3_struct_0(sK69) ),
inference(resolution,[],[f38179,f23080]) ).
fof(f38181,plain,
! [X0] :
( k2_tarski(X0,X0) = k1_struct_0(sK70,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK70))
| v3_struct_0(sK70) ),
inference(resolution,[],[f38179,f37047]) ).
fof(f38182,plain,
! [X0] :
( k2_tarski(X0,X0) = k1_struct_0(sK70,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK70)) ),
inference(forward_subsumption_resolution,[],[f38181,f23085]) ).
fof(f38183,plain,
! [X0] :
( k2_tarski(X0,X0) = k1_struct_0(sK69,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK69)) ),
inference(forward_subsumption_resolution,[],[f38180,f23082]) ).
fof(f38184,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(sK70))
| k2_tarski(X0,X0) = k1_struct_0(sK70,X0) ),
inference(forward_demodulation,[],[f38182,f37054]) ).
fof(f38185,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(sK69))
| k2_tarski(X0,X0) = k1_struct_0(sK69,X0) ),
inference(forward_demodulation,[],[f38183,f37053]) ).
fof(f38198,plain,
! [X0] :
( v1_tsp_1(u1_struct_0(sK70),X0)
| ~ m1_subset_1(u1_struct_0(sK70),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(sK70)
| ~ m2_tsp_1(sK70,X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(resolution,[],[f35093,f37155]) ).
fof(f38199,plain,
! [X0] :
( v1_tsp_1(u1_struct_0(sK70),X0)
| v3_struct_0(sK70)
| ~ m2_tsp_1(sK70,X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(forward_subsumption_resolution,[],[f38198,f23002]) ).
fof(f38200,plain,
! [X0] :
( v1_tsp_1(u1_struct_0(sK70),X0)
| ~ m2_tsp_1(sK70,X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(forward_subsumption_resolution,[],[f38199,f23085]) ).
fof(f38201,plain,
! [X0] :
( v1_tsp_1(k2_pre_topc(sK70),X0)
| ~ m2_tsp_1(sK70,X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(forward_demodulation,[],[f38200,f37054]) ).
fof(f38304,definition,
( spl1367_110
<=> m1_relset_1(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70)) ),
introduced(definition,[new_symbols(definition,[spl1367_110])],[avatar_definition]) ).
fof(f38305,plain,
( ~ m1_relset_1(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70))
| spl1367_110 ),
inference(avatar_component_clause,[],[f38304]) ).
fof(f38395,plain,
! [X0] :
( m1_subset_1(sK68(sK69,sK70,X0,u1_struct_0(sK70)),k2_pre_topc(sK69))
| v3_borsuk_1(X0,sK69,sK70)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_pre_topc(sK69),u1_struct_0(sK70))
| ~ v5_pre_topc(X0,sK69,sK70)
| ~ m2_relset_1(X0,k2_pre_topc(sK69),u1_struct_0(sK70))
| v3_struct_0(sK70)
| ~ m1_subset_1(u1_struct_0(sK70),k1_zfmisc_1(k2_pre_topc(sK69)))
| ~ m2_tsp_1(sK70,sK69) ),
inference(resolution,[],[f37089,f23084]) ).
fof(f38396,plain,
! [X0] :
( m1_subset_1(sK68(sK69,sK70,X0,u1_struct_0(sK70)),k2_pre_topc(sK69))
| v3_borsuk_1(X0,sK69,sK70)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_pre_topc(sK69),u1_struct_0(sK70))
| ~ v5_pre_topc(X0,sK69,sK70)
| ~ m2_relset_1(X0,k2_pre_topc(sK69),u1_struct_0(sK70))
| ~ m1_subset_1(u1_struct_0(sK70),k1_zfmisc_1(k2_pre_topc(sK69)))
| ~ m2_tsp_1(sK70,sK69) ),
inference(forward_subsumption_resolution,[],[f38395,f23085]) ).
fof(f38397,plain,
! [X0] :
( m1_subset_1(sK68(sK69,sK70,X0,u1_struct_0(sK70)),k2_pre_topc(sK69))
| v3_borsuk_1(X0,sK69,sK70)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_pre_topc(sK69),u1_struct_0(sK70))
| ~ v5_pre_topc(X0,sK69,sK70)
| ~ m2_relset_1(X0,k2_pre_topc(sK69),u1_struct_0(sK70))
| ~ m1_subset_1(u1_struct_0(sK70),k1_zfmisc_1(k2_pre_topc(sK69))) ),
inference(forward_subsumption_resolution,[],[f38396,f23083]) ).
fof(f38398,plain,
! [X0] :
( m1_subset_1(sK68(sK69,sK70,X0,k2_pre_topc(sK70)),k2_pre_topc(sK69))
| v3_borsuk_1(X0,sK69,sK70)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_pre_topc(sK69),u1_struct_0(sK70))
| ~ v5_pre_topc(X0,sK69,sK70)
| ~ m2_relset_1(X0,k2_pre_topc(sK69),u1_struct_0(sK70))
| ~ m1_subset_1(u1_struct_0(sK70),k1_zfmisc_1(k2_pre_topc(sK69))) ),
inference(forward_demodulation,[],[f38397,f37054]) ).
fof(f38399,plain,
! [X0] :
( ~ v1_funct_2(X0,k2_pre_topc(sK69),k2_pre_topc(sK70))
| m1_subset_1(sK68(sK69,sK70,X0,k2_pre_topc(sK70)),k2_pre_topc(sK69))
| v3_borsuk_1(X0,sK69,sK70)
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK69,sK70)
| ~ m2_relset_1(X0,k2_pre_topc(sK69),u1_struct_0(sK70))
| ~ m1_subset_1(u1_struct_0(sK70),k1_zfmisc_1(k2_pre_topc(sK69))) ),
inference(forward_demodulation,[],[f38398,f37054]) ).
fof(f38400,plain,
! [X0] :
( ~ m2_relset_1(X0,k2_pre_topc(sK69),k2_pre_topc(sK70))
| ~ v1_funct_2(X0,k2_pre_topc(sK69),k2_pre_topc(sK70))
| m1_subset_1(sK68(sK69,sK70,X0,k2_pre_topc(sK70)),k2_pre_topc(sK69))
| v3_borsuk_1(X0,sK69,sK70)
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK69,sK70)
| ~ m1_subset_1(u1_struct_0(sK70),k1_zfmisc_1(k2_pre_topc(sK69))) ),
inference(forward_demodulation,[],[f38399,f37054]) ).
fof(f38401,plain,
! [X0] :
( ~ m1_subset_1(k2_pre_topc(sK70),k1_zfmisc_1(k2_pre_topc(sK69)))
| ~ m2_relset_1(X0,k2_pre_topc(sK69),k2_pre_topc(sK70))
| ~ v1_funct_2(X0,k2_pre_topc(sK69),k2_pre_topc(sK70))
| m1_subset_1(sK68(sK69,sK70,X0,k2_pre_topc(sK70)),k2_pre_topc(sK69))
| v3_borsuk_1(X0,sK69,sK70)
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK69,sK70) ),
inference(forward_demodulation,[],[f38400,f37054]) ).
fof(f38402,plain,
! [X0] :
( m1_subset_1(sK68(sK69,sK70,X0,k2_pre_topc(sK70)),k2_pre_topc(sK69))
| ~ v1_funct_2(X0,k2_pre_topc(sK69),k2_pre_topc(sK70))
| ~ m2_relset_1(X0,k2_pre_topc(sK69),k2_pre_topc(sK70))
| v3_borsuk_1(X0,sK69,sK70)
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK69,sK70) ),
inference(forward_subsumption_resolution,[],[f38401,f37164]) ).
fof(f38406,plain,
! [X0] :
( ~ v5_pre_topc(X0,sK69,sK70)
| ~ m2_relset_1(X0,k2_pre_topc(sK69),k2_pre_topc(sK70))
| v3_borsuk_1(X0,sK69,sK70)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_pre_topc(sK69),k2_pre_topc(sK70))
| k8_funct_2(k2_pre_topc(sK69),k2_pre_topc(sK70),sK71,sK68(sK69,sK70,X0,k2_pre_topc(sK70))) = k1_funct_1(sK71,sK68(sK69,sK70,X0,k2_pre_topc(sK70))) ),
inference(resolution,[],[f38402,f37265]) ).
fof(f38407,plain,
! [X0] :
( ~ v5_pre_topc(X0,sK69,sK70)
| ~ m2_relset_1(X0,k2_pre_topc(sK69),k2_pre_topc(sK70))
| v3_borsuk_1(X0,sK69,sK70)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_pre_topc(sK69),k2_pre_topc(sK70))
| k4_tex_4(sK69,sK68(sK69,sK70,X0,k2_pre_topc(sK70))) = k2_tex_4(sK69,sK68(sK69,sK70,X0,k2_pre_topc(sK70))) ),
inference(resolution,[],[f38402,f37173]) ).
fof(f38427,plain,
( ~ m2_relset_1(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70))
| spl1367_110 ),
inference(resolution,[],[f38305,f24364]) ).
fof(f38429,plain,
( $false
| spl1367_110 ),
inference(forward_subsumption_resolution,[],[f38427,f37081]) ).
fof(f38430,plain,
spl1367_110,
inference(avatar_contradiction_clause,[],[f38429]) ).
fof(f38440,plain,
( ~ m2_relset_1(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70))
| v3_borsuk_1(sK71,sK69,sK70)
| ~ v1_funct_1(sK71)
| ~ v1_funct_2(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70))
| k4_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))) = k2_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))) ),
inference(resolution,[],[f38407,f23087]) ).
fof(f38441,plain,
( v3_borsuk_1(sK71,sK69,sK70)
| ~ v1_funct_1(sK71)
| ~ v1_funct_2(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70))
| k4_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))) = k2_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))) ),
inference(forward_subsumption_resolution,[],[f38440,f37081]) ).
fof(f38442,plain,
( ~ v1_funct_1(sK71)
| ~ v1_funct_2(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70))
| k4_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))) = k2_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))) ),
inference(forward_subsumption_resolution,[],[f38441,f23091]) ).
fof(f38443,plain,
( ~ v1_funct_2(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70))
| k4_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))) = k2_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))) ),
inference(forward_subsumption_resolution,[],[f38442,f23089]) ).
fof(f38444,plain,
k4_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))) = k2_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))),
inference(forward_subsumption_resolution,[],[f38443,f37082]) ).
fof(f38448,plain,
( ~ m2_relset_1(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70))
| v3_borsuk_1(sK71,sK69,sK70)
| ~ v1_funct_1(sK71)
| ~ v1_funct_2(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70))
| k8_funct_2(k2_pre_topc(sK69),k2_pre_topc(sK70),sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))) = k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))) ),
inference(resolution,[],[f38406,f23087]) ).
fof(f38449,plain,
( v3_borsuk_1(sK71,sK69,sK70)
| ~ v1_funct_1(sK71)
| ~ v1_funct_2(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70))
| k8_funct_2(k2_pre_topc(sK69),k2_pre_topc(sK70),sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))) = k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))) ),
inference(forward_subsumption_resolution,[],[f38448,f37081]) ).
fof(f38450,plain,
( ~ v1_funct_1(sK71)
| ~ v1_funct_2(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70))
| k8_funct_2(k2_pre_topc(sK69),k2_pre_topc(sK70),sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))) = k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))) ),
inference(forward_subsumption_resolution,[],[f38449,f23091]) ).
fof(f38451,plain,
( ~ v1_funct_2(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70))
| k8_funct_2(k2_pre_topc(sK69),k2_pre_topc(sK70),sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))) = k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))) ),
inference(forward_subsumption_resolution,[],[f38450,f23089]) ).
fof(f38452,plain,
k8_funct_2(k2_pre_topc(sK69),k2_pre_topc(sK70),sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))) = k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))),
inference(forward_subsumption_resolution,[],[f38451,f37082]) ).
fof(f38453,plain,
( r2_hidden(k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))),k4_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))))
| ~ m1_subset_1(sK68(sK69,sK70,sK71,k2_pre_topc(sK70)),k2_pre_topc(sK69)) ),
inference(superposition,[],[f37083,f38452]) ).
fof(f38454,plain,
( k5_subset_1(k2_pre_topc(sK69),k2_pre_topc(sK70),k4_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70)))) != k1_struct_0(sK70,k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))))
| ~ v1_funct_2(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70))
| ~ m2_relset_1(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70))
| v3_borsuk_1(sK71,sK69,sK70)
| ~ v1_funct_1(sK71)
| ~ v5_pre_topc(sK71,sK69,sK70) ),
inference(superposition,[],[f37560,f38452]) ).
fof(f38456,plain,
( m1_subset_1(k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))),k2_pre_topc(sK70))
| v1_xboole_0(k2_pre_topc(sK69))
| ~ v1_funct_1(sK71)
| ~ v1_funct_2(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70))
| ~ m1_relset_1(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70))
| ~ m1_subset_1(sK68(sK69,sK70,sK71,k2_pre_topc(sK70)),k2_pre_topc(sK69)) ),
inference(superposition,[],[f24356,f38452]) ).
fof(f38457,plain,
( m1_subset_1(k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))),k2_pre_topc(sK70))
| ~ v1_funct_1(sK71)
| ~ v1_funct_2(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70))
| ~ m1_relset_1(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70))
| ~ m1_subset_1(sK68(sK69,sK70,sK71,k2_pre_topc(sK70)),k2_pre_topc(sK69)) ),
inference(forward_subsumption_resolution,[],[f38456,f37258]) ).
fof(f38459,plain,
( k5_subset_1(k2_pre_topc(sK69),k2_pre_topc(sK70),k4_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70)))) != k1_struct_0(sK70,k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))))
| ~ m2_relset_1(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70))
| v3_borsuk_1(sK71,sK69,sK70)
| ~ v1_funct_1(sK71)
| ~ v5_pre_topc(sK71,sK69,sK70) ),
inference(forward_subsumption_resolution,[],[f38454,f37082]) ).
fof(f38461,definition,
( spl1367_118
<=> m1_subset_1(sK68(sK69,sK70,sK71,k2_pre_topc(sK70)),k2_pre_topc(sK69)) ),
introduced(definition,[new_symbols(definition,[spl1367_118])],[avatar_definition]) ).
fof(f38462,plain,
( ~ m1_subset_1(sK68(sK69,sK70,sK71,k2_pre_topc(sK70)),k2_pre_topc(sK69))
| spl1367_118 ),
inference(avatar_component_clause,[],[f38461]) ).
fof(f38464,definition,
( spl1367_119
<=> r2_hidden(k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))),k4_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70)))) ),
introduced(definition,[new_symbols(definition,[spl1367_119])],[avatar_definition]) ).
fof(f38465,plain,
( r2_hidden(k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))),k4_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))))
| ~ spl1367_119 ),
inference(avatar_component_clause,[],[f38464]) ).
fof(f38466,plain,
( ~ spl1367_118
| spl1367_119 ),
inference(avatar_split_clause,[],[f38453,f38464,f38461]) ).
fof(f38467,plain,
( m1_subset_1(k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))),k2_pre_topc(sK70))
| ~ v1_funct_2(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70))
| ~ m1_relset_1(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70))
| ~ m1_subset_1(sK68(sK69,sK70,sK71,k2_pre_topc(sK70)),k2_pre_topc(sK69)) ),
inference(forward_subsumption_resolution,[],[f38457,f23089]) ).
fof(f38469,plain,
( k5_subset_1(k2_pre_topc(sK69),k2_pre_topc(sK70),k4_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70)))) != k1_struct_0(sK70,k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))))
| v3_borsuk_1(sK71,sK69,sK70)
| ~ v1_funct_1(sK71)
| ~ v5_pre_topc(sK71,sK69,sK70) ),
inference(forward_subsumption_resolution,[],[f38459,f37081]) ).
fof(f38470,plain,
( m1_subset_1(k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))),k2_pre_topc(sK70))
| ~ m1_relset_1(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70))
| ~ m1_subset_1(sK68(sK69,sK70,sK71,k2_pre_topc(sK70)),k2_pre_topc(sK69)) ),
inference(forward_subsumption_resolution,[],[f38467,f37082]) ).
fof(f38472,plain,
( k5_subset_1(k2_pre_topc(sK69),k2_pre_topc(sK70),k4_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70)))) != k1_struct_0(sK70,k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))))
| ~ v1_funct_1(sK71)
| ~ v5_pre_topc(sK71,sK69,sK70) ),
inference(forward_subsumption_resolution,[],[f38469,f23091]) ).
fof(f38474,definition,
( spl1367_120
<=> m1_subset_1(k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))),k2_pre_topc(sK70)) ),
introduced(definition,[new_symbols(definition,[spl1367_120])],[avatar_definition]) ).
fof(f38475,plain,
( m1_subset_1(k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))),k2_pre_topc(sK70))
| ~ spl1367_120 ),
inference(avatar_component_clause,[],[f38474]) ).
fof(f38476,plain,
( ~ spl1367_118
| ~ spl1367_110
| spl1367_120 ),
inference(avatar_split_clause,[],[f38470,f38474,f38304,f38461]) ).
fof(f38478,plain,
( k5_subset_1(k2_pre_topc(sK69),k2_pre_topc(sK70),k4_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70)))) != k1_struct_0(sK70,k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))))
| ~ v5_pre_topc(sK71,sK69,sK70) ),
inference(forward_subsumption_resolution,[],[f38472,f23089]) ).
fof(f38480,plain,
k5_subset_1(k2_pre_topc(sK69),k2_pre_topc(sK70),k4_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70)))) != k1_struct_0(sK70,k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70)))),
inference(forward_subsumption_resolution,[],[f38478,f23087]) ).
fof(f38486,plain,
( ~ v1_funct_2(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70))
| ~ m2_relset_1(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70))
| v3_borsuk_1(sK71,sK69,sK70)
| ~ v1_funct_1(sK71)
| ~ v5_pre_topc(sK71,sK69,sK70)
| spl1367_118 ),
inference(resolution,[],[f38462,f38402]) ).
fof(f38488,plain,
( ~ m2_relset_1(sK71,k2_pre_topc(sK69),k2_pre_topc(sK70))
| v3_borsuk_1(sK71,sK69,sK70)
| ~ v1_funct_1(sK71)
| ~ v5_pre_topc(sK71,sK69,sK70)
| spl1367_118 ),
inference(forward_subsumption_resolution,[],[f38486,f37082]) ).
fof(f38489,plain,
( v3_borsuk_1(sK71,sK69,sK70)
| ~ v1_funct_1(sK71)
| ~ v5_pre_topc(sK71,sK69,sK70)
| spl1367_118 ),
inference(forward_subsumption_resolution,[],[f38488,f37081]) ).
fof(f38490,plain,
( ~ v1_funct_1(sK71)
| ~ v5_pre_topc(sK71,sK69,sK70)
| spl1367_118 ),
inference(forward_subsumption_resolution,[],[f38489,f23091]) ).
fof(f38491,plain,
( ~ v5_pre_topc(sK71,sK69,sK70)
| spl1367_118 ),
inference(forward_subsumption_resolution,[],[f38490,f23089]) ).
fof(f38492,plain,
( $false
| spl1367_118 ),
inference(forward_subsumption_resolution,[],[f38491,f23087]) ).
fof(f38493,plain,
spl1367_118,
inference(avatar_contradiction_clause,[],[f38492]) ).
fof(f38495,plain,
( k1_struct_0(sK70,k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70)))) = k2_tarski(k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))),k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))))
| ~ spl1367_120 ),
inference(resolution,[],[f38475,f38184]) ).
fof(f38498,plain,
( m1_subset_1(k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))),k2_pre_topc(sK69))
| ~ spl1367_120 ),
inference(resolution,[],[f38475,f37328]) ).
fof(f38501,plain,
( k2_tarski(k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))),k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70)))) = k1_struct_0(sK69,k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))))
| ~ spl1367_120 ),
inference(resolution,[],[f38498,f38185]) ).
fof(f38504,plain,
( k4_tex_4(sK69,k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70)))) = k2_tex_4(sK69,k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))))
| ~ spl1367_120 ),
inference(resolution,[],[f38498,f37173]) ).
fof(f40135,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_tsp_1(X1,sK69)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK69)))
| v3_struct_0(sK69)
| k1_struct_0(sK69,X0) = k5_subset_1(u1_struct_0(sK69),X1,k4_tex_4(sK69,X0))
| ~ l1_pre_topc(sK69) ),
inference(resolution,[],[f36708,f23081]) ).
fof(f40138,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_tsp_1(X1,sK69)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK69)))
| k1_struct_0(sK69,X0) = k5_subset_1(u1_struct_0(sK69),X1,k4_tex_4(sK69,X0))
| ~ l1_pre_topc(sK69) ),
inference(forward_subsumption_resolution,[],[f40135,f23082]) ).
fof(f40140,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_tsp_1(X1,sK69)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK69)))
| k1_struct_0(sK69,X0) = k5_subset_1(u1_struct_0(sK69),X1,k4_tex_4(sK69,X0)) ),
inference(forward_subsumption_resolution,[],[f40138,f23080]) ).
fof(f40142,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(k2_pre_topc(sK69)))
| ~ r2_hidden(X0,X1)
| ~ v1_tsp_1(X1,sK69)
| k1_struct_0(sK69,X0) = k5_subset_1(u1_struct_0(sK69),X1,k4_tex_4(sK69,X0)) ),
inference(forward_demodulation,[],[f40140,f37053]) ).
fof(f40144,plain,
! [X0,X1] :
( ~ v1_tsp_1(X1,sK69)
| ~ m1_subset_1(X1,k1_zfmisc_1(k2_pre_topc(sK69)))
| ~ r2_hidden(X0,X1)
| k1_struct_0(sK69,X0) = k5_subset_1(k2_pre_topc(sK69),X1,k4_tex_4(sK69,X0)) ),
inference(forward_demodulation,[],[f40142,f37053]) ).
fof(f40146,plain,
! [X0] :
( ~ m1_subset_1(k2_pre_topc(sK70),k1_zfmisc_1(k2_pre_topc(sK69)))
| ~ r2_hidden(X0,k2_pre_topc(sK70))
| k1_struct_0(sK69,X0) = k5_subset_1(k2_pre_topc(sK69),k2_pre_topc(sK70),k4_tex_4(sK69,X0))
| ~ m2_tsp_1(sK70,sK69)
| v3_struct_0(sK69)
| ~ l1_pre_topc(sK69) ),
inference(resolution,[],[f40144,f38201]) ).
fof(f40147,plain,
! [X0] :
( ~ r2_hidden(X0,k2_pre_topc(sK70))
| k1_struct_0(sK69,X0) = k5_subset_1(k2_pre_topc(sK69),k2_pre_topc(sK70),k4_tex_4(sK69,X0))
| ~ m2_tsp_1(sK70,sK69)
| v3_struct_0(sK69)
| ~ l1_pre_topc(sK69) ),
inference(forward_subsumption_resolution,[],[f40146,f37164]) ).
fof(f40149,plain,
! [X0] :
( ~ r2_hidden(X0,k2_pre_topc(sK70))
| k1_struct_0(sK69,X0) = k5_subset_1(k2_pre_topc(sK69),k2_pre_topc(sK70),k4_tex_4(sK69,X0))
| v3_struct_0(sK69)
| ~ l1_pre_topc(sK69) ),
inference(forward_subsumption_resolution,[],[f40147,f23083]) ).
fof(f40151,plain,
! [X0] :
( ~ r2_hidden(X0,k2_pre_topc(sK70))
| k1_struct_0(sK69,X0) = k5_subset_1(k2_pre_topc(sK69),k2_pre_topc(sK70),k4_tex_4(sK69,X0))
| ~ l1_pre_topc(sK69) ),
inference(forward_subsumption_resolution,[],[f40149,f23082]) ).
fof(f40153,plain,
! [X0] :
( ~ r2_hidden(X0,k2_pre_topc(sK70))
| k1_struct_0(sK69,X0) = k5_subset_1(k2_pre_topc(sK69),k2_pre_topc(sK70),k4_tex_4(sK69,X0)) ),
inference(forward_subsumption_resolution,[],[f40151,f23080]) ).
fof(f40156,plain,
! [X0] :
( k1_struct_0(sK69,X0) = k5_subset_1(k2_pre_topc(sK69),k2_pre_topc(sK70),k4_tex_4(sK69,X0))
| ~ m1_subset_1(X0,k2_pre_topc(sK70))
| v1_xboole_0(k2_pre_topc(sK70)) ),
inference(resolution,[],[f40153,f23696]) ).
fof(f40159,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(sK70))
| k1_struct_0(sK69,X0) = k5_subset_1(k2_pre_topc(sK69),k2_pre_topc(sK70),k4_tex_4(sK69,X0)) ),
inference(forward_subsumption_resolution,[],[f40156,f37257]) ).
fof(f40164,plain,
( k1_struct_0(sK69,k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70)))) = k5_subset_1(k2_pre_topc(sK69),k2_pre_topc(sK70),k4_tex_4(sK69,k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70)))))
| ~ spl1367_120 ),
inference(resolution,[],[f40159,f38475]) ).
fof(f40984,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k2_tex_4(sK69,X1))
| ~ m1_subset_1(X0,u1_struct_0(sK69))
| ~ m1_subset_1(X1,u1_struct_0(sK69))
| v3_struct_0(sK69)
| k2_tex_4(sK69,X0) = k2_tex_4(sK69,X1) ),
inference(resolution,[],[f24526,f23080]) ).
fof(f40991,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k2_tex_4(sK69,X1))
| ~ m1_subset_1(X0,u1_struct_0(sK69))
| ~ m1_subset_1(X1,u1_struct_0(sK69))
| k2_tex_4(sK69,X0) = k2_tex_4(sK69,X1) ),
inference(forward_subsumption_resolution,[],[f40984,f23082]) ).
fof(f40995,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k2_pre_topc(sK69))
| ~ r2_hidden(X0,k2_tex_4(sK69,X1))
| ~ m1_subset_1(X1,u1_struct_0(sK69))
| k2_tex_4(sK69,X0) = k2_tex_4(sK69,X1) ),
inference(forward_demodulation,[],[f40991,f37053]) ).
fof(f41002,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k2_tex_4(sK69,X1))
| ~ m1_subset_1(X0,k2_pre_topc(sK69))
| ~ m1_subset_1(X1,k2_pre_topc(sK69))
| k2_tex_4(sK69,X0) = k2_tex_4(sK69,X1) ),
inference(forward_demodulation,[],[f40995,f37053]) ).
fof(f41019,plain,
! [X0] :
( ~ r2_hidden(X0,k4_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))))
| ~ m1_subset_1(X0,k2_pre_topc(sK69))
| ~ m1_subset_1(sK68(sK69,sK70,sK71,k2_pre_topc(sK70)),k2_pre_topc(sK69))
| k2_tex_4(sK69,X0) = k4_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))) ),
inference(superposition,[],[f41002,f38444]) ).
fof(f41022,plain,
! [X0] :
( ~ r2_hidden(X0,k4_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))))
| ~ m1_subset_1(sK68(sK69,sK70,sK71,k2_pre_topc(sK70)),k2_pre_topc(sK69))
| k2_tex_4(sK69,X0) = k4_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))) ),
inference(forward_subsumption_resolution,[],[f41019,f37703]) ).
fof(f41033,definition,
( spl1367_255
<=> ! [X0] :
( ~ r2_hidden(X0,k4_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))))
| k2_tex_4(sK69,X0) = k4_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))) ) ),
introduced(definition,[new_symbols(definition,[spl1367_255])],[avatar_definition]) ).
fof(f41034,plain,
( ! [X0] :
( ~ r2_hidden(X0,k4_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))))
| k2_tex_4(sK69,X0) = k4_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))) )
| ~ spl1367_255 ),
inference(avatar_component_clause,[],[f41033]) ).
fof(f41035,plain,
( ~ spl1367_118
| spl1367_255 ),
inference(avatar_split_clause,[],[f41022,f41033,f38461]) ).
fof(f41046,plain,
( k4_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))) = k2_tex_4(sK69,k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))))
| ~ spl1367_119
| ~ spl1367_255 ),
inference(resolution,[],[f41034,f38465]) ).
fof(f41062,plain,
( k4_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))) = k4_tex_4(sK69,k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))))
| ~ spl1367_119
| ~ spl1367_120
| ~ spl1367_255 ),
inference(superposition,[],[f38504,f41046]) ).
fof(f41066,plain,
( k5_subset_1(k2_pre_topc(sK69),k2_pre_topc(sK70),k4_tex_4(sK69,sK68(sK69,sK70,sK71,k2_pre_topc(sK70)))) = k1_struct_0(sK69,k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))))
| ~ spl1367_119
| ~ spl1367_120
| ~ spl1367_255 ),
inference(superposition,[],[f40164,f41062]) ).
fof(f42225,plain,
( k1_struct_0(sK70,k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70)))) = k1_struct_0(sK69,k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))))
| ~ spl1367_120 ),
inference(superposition,[],[f38495,f38501]) ).
fof(f44189,plain,
( k1_struct_0(sK70,k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70)))) != k1_struct_0(sK69,k1_funct_1(sK71,sK68(sK69,sK70,sK71,k2_pre_topc(sK70))))
| ~ spl1367_119
| ~ spl1367_120
| ~ spl1367_255 ),
inference(superposition,[],[f38480,f41066]) ).
fof(f44190,plain,
( $false
| ~ spl1367_119
| ~ spl1367_120
| ~ spl1367_255 ),
inference(forward_subsumption_resolution,[],[f44189,f42225]) ).
fof(f44191,plain,
( ~ spl1367_119
| ~ spl1367_120
| ~ spl1367_255 ),
inference(avatar_contradiction_clause,[],[f44190]) ).
cnf(s114,plain,
spl1367_110,
inference(sat_conversion,[],[f38430]) ).
cnf(s115,plain,
( ~ spl1367_118
| spl1367_119 ),
inference(sat_conversion,[],[f38466]) ).
cnf(s116,plain,
( ~ spl1367_110
| ~ spl1367_118
| spl1367_120 ),
inference(sat_conversion,[],[f38476]) ).
cnf(s119,plain,
spl1367_118,
inference(sat_conversion,[],[f38493]) ).
cnf(s254,plain,
( ~ spl1367_118
| spl1367_255 ),
inference(sat_conversion,[],[f41035]) ).
cnf(s487,plain,
( ~ spl1367_119
| ~ spl1367_120
| ~ spl1367_255 ),
inference(sat_conversion,[],[f44191]) ).
cnf(s685,plain,
spl1367_255,
inference(rat,[],[s254,s119]) ).
cnf(s688,plain,
( ~ spl1367_110
| spl1367_120 ),
inference(rat,[],[s116,s119]) ).
cnf(s689,plain,
spl1367_119,
inference(rat,[],[s115,s119]) ).
cnf(s690,plain,
~ spl1367_120,
inference(rat,[],[s487,s685,s689]) ).
cnf(s691,plain,
~ spl1367_110,
inference(rat,[],[s688,s690]) ).
cnf(s692,plain,
$false,
inference(rat,[],[s114,s691]) ).
fof(f44192,plain,
$false,
inference(avatar_sat_refutation,[],[s692]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP033+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n008.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 18:55:56 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.21 Running first-order theorem proving
% 0.07/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.92/3.31 % (2527811)Detected formulas, will run a generic FOF schedule.
% 14.92/3.31 % (2527822)dis-21_1_sil=8000:lcm=predicate:random_seed=1154386668: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.92/3.31 % (2527817)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=46656300:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2993 on theBenchmark for (2993ds/134677Mi)
% 14.92/3.31 % (2527820)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2978617501:i=119:av=off:ss=axioms_2993 on theBenchmark for (2993ds/119Mi)
% 14.92/3.31 % (2527819)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2083206759:i=109:sd=1:ins=1:gsp=on:ss=axioms_2993 on theBenchmark for (2993ds/109Mi)
% 14.92/3.31 % (2527821)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2330594905:s2a=on:i=139:gtg=position_2993 on theBenchmark for (2993ds/139Mi)
% 14.92/3.31 % (2527818)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=187739562:i=141695:sd=1:nm=32:gsp=on:ss=included_2993 on theBenchmark for (2993ds/141695Mi)
% 14.92/3.31 % (2527816)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=2548834170:i=141193_2993 on theBenchmark for (2993ds/141193Mi)
% 14.92/3.31 % (2527822)Instruction limit reached!
% 14.92/3.31 % (2527822)------------------------------
% 14.92/3.31 % (2527822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.92/3.31 % (2527822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.92/3.31 % (2527822)CaDiCaL version: 2.1.3
% 14.92/3.31 % (2527822)Termination reason: Instruction limit
% 14.92/3.31 % (2527822)Termination phase: Preprocessing 1
% 14.92/3.31 % (2527822)Time elapsed: 0.055 s
% 14.92/3.31 % (2527822)Peak memory usage: 103 MB
% 14.92/3.31 % (2527822)Instructions burned: 130 (million)
% 14.92/3.31 % (2527821)Instruction limit reached!
% 14.92/3.31 % (2527821)------------------------------
% 14.92/3.31 % (2527821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.92/3.31 % (2527821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.92/3.31 % (2527821)CaDiCaL version: 2.1.3
% 14.92/3.31 % (2527821)Termination reason: Instruction limit
% 14.92/3.31 % (2527821)Termination phase: Property scanning
% 14.92/3.31 % (2527821)Time elapsed: 0.059 s
% 14.92/3.31 % (2527821)Peak memory usage: 102 MB
% 14.92/3.31 % (2527821)Instructions burned: 141 (million)
% 14.92/3.31 % (2527819)Instruction limit reached!
% 14.92/3.31 % (2527819)------------------------------
% 14.92/3.31 % (2527819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.92/3.31 % (2527819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.92/3.31 % (2527819)CaDiCaL version: 2.1.3
% 14.92/3.31 % (2527819)Termination reason: Instruction limit
% 14.92/3.31 % (2527819)Termination phase: Saturation
% 14.92/3.31 % (2527819)Time elapsed: 0.083 s
% 14.92/3.31 % (2527819)Peak memory usage: 106 MB
% 14.92/3.31 % (2527819)Instructions burned: 110 (million)
% 14.92/3.31 % (2527820)Instruction limit reached!
% 14.92/3.31 % (2527820)------------------------------
% 14.92/3.31 % (2527820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.92/3.31 % (2527820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.92/3.31 % (2527820)CaDiCaL version: 2.1.3
% 14.92/3.31 % (2527820)Termination reason: Instruction limit
% 14.92/3.31 % (2527820)Termination phase: Preprocessing 3
% 14.92/3.31 % (2527820)Time elapsed: 0.102 s
% 14.92/3.31 % (2527820)Peak memory usage: 105 MB
% 14.92/3.31 % (2527820)Instructions burned: 120 (million)
% 14.92/3.31 % (2527830)lrs+10_1_sil=8000:sp=occurrence:random_seed=2402861752:i=285:sd=3:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/285Mi)
% 14.92/3.31 % (2527831)lrs+10_1_sil=32000:urr=on:br=off:random_seed=623547839:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/157Mi)
% 14.92/3.31 % (2527832)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1264448405:i=325:sd=1:ss=axioms:sgt=32_2990 on theBenchmark for (2990ds/325Mi)
% 14.92/3.31 % (2527830)Instruction limit reached!
% 14.92/3.31 % (2527830)------------------------------
% 14.92/3.31 % (2527830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.92/3.31 % (2527830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.04/4.03 % (2527830)CaDiCaL version: 2.1.3
% 19.04/4.03 % (2527830)Termination reason: Instruction limit
% 19.04/4.03 % (2527830)Termination phase: Saturation
% 19.04/4.03 % (2527830)Time elapsed: 0.103 s
% 19.04/4.03 % (2527830)Peak memory usage: 110 MB
% 19.04/4.03 % (2527830)Instructions burned: 287 (million)
% 19.04/4.03 % (2527833)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=2631465442:s2a=on:i=248:s2at=1.23:gtg=position_2990 on theBenchmark for (2990ds/248Mi)
% 19.04/4.03 % (2527831)Instruction limit reached!
% 19.04/4.03 % (2527831)------------------------------
% 19.04/4.03 % (2527831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.04/4.03 % (2527831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.04/4.03 % (2527831)CaDiCaL version: 2.1.3
% 19.04/4.03 % (2527831)Termination reason: Instruction limit
% 19.04/4.03 % (2527831)Termination phase: Property scanning
% 19.04/4.03 % (2527831)Time elapsed: 0.069 s
% 19.04/4.03 % (2527831)Peak memory usage: 102 MB
% 19.04/4.03 % (2527831)Instructions burned: 159 (million)
% 19.04/4.03 % (2527837)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3424670074:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2989 on theBenchmark for (2989ds/294Mi)
% 19.04/4.03 % (2527833)Instruction limit reached!
% 19.04/4.03 % (2527833)------------------------------
% 19.04/4.03 % (2527833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.04/4.03 % (2527833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.04/4.03 % (2527833)CaDiCaL version: 2.1.3
% 19.04/4.03 % (2527833)Termination reason: Instruction limit
% 19.04/4.03 % (2527833)Termination phase: SInE selection
% 19.04/4.03 % (2527833)Time elapsed: 0.131 s
% 19.04/4.03 % (2527833)Peak memory usage: 103 MB
% 19.04/4.03 % (2527833)Instructions burned: 249 (million)
% 19.04/4.03 % (2527839)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2298261856:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 19.04/4.03 % (2527832)Instruction limit reached!
% 19.04/4.03 % (2527832)------------------------------
% 19.04/4.03 % (2527832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.04/4.03 % (2527832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.04/4.03 % (2527832)CaDiCaL version: 2.1.3
% 19.04/4.03 % (2527832)Termination reason: Instruction limit
% 19.04/4.03 % (2527832)Termination phase: Saturation
% 19.04/4.03 % (2527832)Time elapsed: 0.223 s
% 19.04/4.03 % (2527832)Peak memory usage: 109 MB
% 19.04/4.03 % (2527832)Instructions burned: 326 (million)
% 19.04/4.03 % (2527837)Instruction limit reached!
% 19.04/4.03 % (2527837)------------------------------
% 19.04/4.03 % (2527837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.04/4.03 % (2527837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.04/4.03 % (2527837)CaDiCaL version: 2.1.3
% 19.04/4.03 % (2527837)Termination reason: Instruction limit
% 19.04/4.03 % (2527837)Termination phase: Saturation
% 19.04/4.03 % (2527837)Time elapsed: 0.106 s
% 19.04/4.03 % (2527837)Peak memory usage: 110 MB
% 19.04/4.03 % (2527837)Instructions burned: 296 (million)
% 19.04/4.03 % (2527841)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2935872220:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 19.04/4.03 % (2527844)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=591732932:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2986 on theBenchmark for (2986ds/114Mi)
% 19.04/4.03 % (2527844)Instruction limit reached!
% 19.04/4.03 % (2527844)------------------------------
% 19.04/4.03 % (2527844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.04/4.03 % (2527844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.04/4.03 % (2527844)CaDiCaL version: 2.1.3
% 19.04/4.03 % (2527844)Termination reason: Instruction limit
% 19.04/4.03 % (2527844)Termination phase: Property scanning
% 19.04/4.03 % (2527844)Time elapsed: 0.027 s
% 19.04/4.03 % (2527844)Peak memory usage: 102 MB
% 19.04/4.03 % (2527844)Instructions burned: 119 (million)
% 19.04/4.03 % (2527843)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3635462684:i=127:av=off:fsr=off:sup=off_2986 on theBenchmark for (2986ds/127Mi)
% 19.04/4.03 % (2527841)Instruction limit reached!
% 19.04/4.03 % (2527841)------------------------------
% 19.04/4.03 % (2527841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.72/6.45 % (2527841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.72/6.45 % (2527841)CaDiCaL version: 2.1.3
% 17.72/6.45 % (2527841)Termination reason: Instruction limit
% 17.72/6.45 % (2527841)Termination phase: Naming
% 17.72/6.45 % (2527841)Time elapsed: 0.096 s
% 17.72/6.45 % (2527841)Peak memory usage: 105 MB
% 17.72/6.45 % (2527841)Instructions burned: 113 (million)
% 17.72/6.45 % (2527843)Instruction limit reached!
% 17.72/6.45 % (2527843)------------------------------
% 17.72/6.45 % (2527843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.72/6.45 % (2527843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.72/6.45 % (2527843)CaDiCaL version: 2.1.3
% 17.72/6.45 % (2527843)Termination reason: Instruction limit
% 17.72/6.45 % (2527843)Termination phase: Preprocessing 2
% 17.72/6.45 % (2527843)Time elapsed: 0.101 s
% 17.72/6.45 % (2527843)Peak memory usage: 106 MB
% 17.72/6.45 % (2527843)Instructions burned: 128 (million)
% 17.72/6.45 % (2527847)lrs+10_1_sil=8000:sp=occurrence:random_seed=1611912228:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 17.72/6.45 % (2527849)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3845951542:i=437:sd=1:aac=none:ss=included_2985 on theBenchmark for (2985ds/437Mi)
% 17.72/6.45 % (2527850)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2987448497:i=5202:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/5202Mi)
% 17.72/6.45 % (2527847)Instruction limit reached!
% 17.72/6.45 % (2527847)------------------------------
% 17.72/6.45 % (2527847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.72/6.45 % (2527847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.72/6.45 % (2527847)CaDiCaL version: 2.1.3
% 17.72/6.45 % (2527847)Termination reason: Instruction limit
% 17.72/6.45 % (2527847)Termination phase: Saturation
% 17.72/6.45 % (2527847)Time elapsed: 0.289 s
% 17.72/6.45 % (2527847)Peak memory usage: 123 MB
% 17.72/6.45 % (2527847)Instructions burned: 910 (million)
% 17.72/6.45 % (2527849)Instruction limit reached!
% 17.72/6.45 % (2527849)------------------------------
% 17.72/6.45 % (2527849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.72/6.45 % (2527849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.72/6.45 % (2527849)CaDiCaL version: 2.1.3
% 17.72/6.45 % (2527849)Termination reason: Instruction limit
% 17.72/6.45 % (2527849)Termination phase: Saturation
% 17.72/6.45 % (2527849)Time elapsed: 0.270 s
% 17.72/6.45 % (2527849)Peak memory usage: 111 MB
% 17.72/6.45 % (2527849)Instructions burned: 437 (million)
% 17.72/6.45 % (2527854)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3460395093:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2981 on theBenchmark for (2981ds/134Mi)
% 17.72/6.45 % (2527854)Instruction limit reached!
% 17.72/6.45 % (2527854)------------------------------
% 17.72/6.45 % (2527854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.72/6.45 % (2527854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.72/6.45 % (2527854)CaDiCaL version: 2.1.3
% 17.72/6.45 % (2527854)Termination reason: Instruction limit
% 17.72/6.45 % (2527854)Termination phase: Property scanning
% 17.72/6.45 % (2527854)Time elapsed: 0.060 s
% 17.72/6.45 % (2527854)Peak memory usage: 106 MB
% 17.72/6.45 % (2527854)Instructions burned: 135 (million)
% 17.72/6.45 % (2527855)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4082776538:st=8:i=592:sd=3:ep=RST:ss=axioms_2980 on theBenchmark for (2980ds/592Mi)
% 17.72/6.45 % (2527857)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3285709999:st=3:i=13193:sd=3:ss=axioms_2979 on theBenchmark for (2979ds/13193Mi)
% 17.72/6.45 % (2527855)Instruction limit reached!
% 17.72/6.45 % (2527855)------------------------------
% 17.72/6.45 % (2527855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.72/6.45 % (2527855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.72/6.45 % (2527855)CaDiCaL version: 2.1.3
% 17.72/6.45 % (2527855)Termination reason: Instruction limit
% 17.72/6.45 % (2527855)Termination phase: Property scanning
% 17.72/6.45 % (2527855)Time elapsed: 0.398 s
% 17.72/6.45 % (2527855)Peak memory usage: 124 MB
% 17.72/6.45 % (2527855)Instructions burned: 593 (million)
% 17.72/6.45 % (2527860)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=280237209:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/125Mi)
% 17.72/6.45 % (2527860)Instruction limit reached!
% 17.72/6.45 % (2527860)------------------------------
% 17.72/6.45 % (2527860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.72/6.45 % (2527860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.72/6.45 % (2527860)CaDiCaL version: 2.1.3
% 17.72/6.45 % (2527860)Termination reason: Instruction limit
% 17.72/6.45 % (2527860)Termination phase: Property scanning
% 17.72/6.45 % (2527860)Time elapsed: 0.055 s
% 17.72/6.45 % (2527860)Peak memory usage: 102 MB
% 17.72/6.45 % (2527860)Instructions burned: 126 (million)
% 17.72/6.45 % (2527839)Instruction limit reached!
% 17.72/6.45 % (2527839)------------------------------
% 17.72/6.45 % (2527839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.72/6.45 % (2527839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.72/6.45 % (2527839)CaDiCaL version: 2.1.3
% 17.72/6.45 % (2527839)Termination reason: Instruction limit
% 17.72/6.45 % (2527839)Termination phase: Saturation
% 17.72/6.45 % (2527839)Time elapsed: 1.436 s
% 17.72/6.45 % (2527839)Peak memory usage: 238 MB
% 17.72/6.45 % (2527839)Instructions burned: 2350 (million)
% 17.72/6.45 % (2527862)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1936798021:i=134:gtgl=5:slsql=off:gtg=exists_sym_2972 on theBenchmark for (2972ds/134Mi)
% 17.72/6.45 % (2527862)Instruction limit reached!
% 17.72/6.45 % (2527862)------------------------------
% 17.72/6.45 % (2527862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.72/6.45 % (2527862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.72/6.45 % (2527862)CaDiCaL version: 2.1.3
% 17.72/6.45 % (2527862)Termination reason: Instruction limit
% 17.72/6.45 % (2527862)Termination phase: Property scanning
% 17.72/6.45 % (2527862)Time elapsed: 0.032 s
% 17.72/6.45 % (2527862)Peak memory usage: 102 MB
% 17.72/6.45 % (2527862)Instructions burned: 135 (million)
% 17.72/6.45 % (2527863)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1111496590:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/141Mi)
% 17.72/6.45 % (2527863)Instruction limit reached!
% 17.72/6.45 % (2527863)------------------------------
% 17.72/6.45 % (2527863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.72/6.45 % (2527863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.72/6.45 % (2527863)CaDiCaL version: 2.1.3
% 17.72/6.45 % (2527863)Termination reason: Instruction limit
% 17.72/6.45 % (2527863)Termination phase: Saturation
% 17.72/6.45 % (2527863)Time elapsed: 0.101 s
% 17.72/6.45 % (2527863)Peak memory usage: 108 MB
% 17.72/6.45 % (2527863)Instructions burned: 142 (million)
% 17.72/6.45 % (2527865)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4284884408:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2971 on theBenchmark for (2971ds/431Mi)
% 17.72/6.45 % (2527867)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=2894845185:i=6060:aac=none:ins=25_2969 on theBenchmark for (2969ds/6060Mi)
% 17.72/6.45 % (2527865)Instruction limit reached!
% 17.72/6.45 % (2527865)------------------------------
% 17.72/6.45 % (2527865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.72/6.45 % (2527865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.72/6.45 % (2527865)CaDiCaL version: 2.1.3
% 17.72/6.45 % (2527865)Termination reason: Instruction limit
% 17.72/6.45 % (2527865)Termination phase: Saturation
% 17.72/6.45 % (2527865)Time elapsed: 0.147 s
% 17.72/6.45 % (2527865)Peak memory usage: 110 MB
% 17.72/6.45 % (2527865)Instructions burned: 434 (million)
% 17.72/6.45 % (2527870)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=2073224525:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2968 on theBenchmark for (2968ds/150Mi)
% 17.72/6.45 % (2527870)Instruction limit reached!
% 17.72/6.45 % (2527870)------------------------------
% 17.72/6.45 % (2527870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.72/6.45 % (2527870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.72/6.45 % (2527870)CaDiCaL version: 2.1.3
% 17.72/6.45 % (2527870)Termination reason: Instruction limit
% 17.72/6.45 % (2527870)Termination phase: Preprocessing 1
% 17.72/6.45 % (2527870)Time elapsed: 0.067 s
% 17.72/6.45 % (2527870)Peak memory usage: 103 MB
% 17.72/6.45 % (2527870)Instructions burned: 152 (million)
% 17.72/6.45 % (2527872)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3628687274:i=14155:bd=all_2966 on theBenchmark for (2966ds/14155Mi)
% 17.72/6.45 % (2527850)Instruction limit reached!
% 17.72/6.45 % (2527850)------------------------------
% 17.72/6.45 % (2527850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.72/6.45 % (2527850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.72/6.45 % (2527850)CaDiCaL version: 2.1.3
% 17.72/6.45 % (2527850)Termination reason: Instruction limit
% 17.72/6.45 % (2527850)Termination phase: Saturation
% 17.72/6.45 % (2527850)Time elapsed: 3.712 s
% 17.72/6.45 % (2527850)Peak memory usage: 310 MB
% 17.72/6.45 % (2527850)Instructions burned: 5204 (million)
% 17.72/6.45 % (2527817)First to succeed.
% 17.72/6.45 % (2527817)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2527811"
% 17.72/6.45 % (2527874)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1889878151:i=667:av=off:fsr=off_2945 on theBenchmark for (2945ds/667Mi)
% 17.72/6.45 % (2527817)Refutation found. Thanks to Tanya!
% 17.72/6.45 % SZS status Theorem for theBenchmark
% 17.72/6.45 % SZS output start Proof for theBenchmark
% See solution above
% 37.43/6.65 % (2527817)------------------------------
% 37.43/6.65 % (2527817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.43/6.65 % (2527817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.43/6.65 % (2527817)CaDiCaL version: 2.1.3
% 37.43/6.65 % (2527817)Termination reason: Refutation
% 37.43/6.65 % (2527817)Time elapsed: 4.621 s
% 37.43/6.65 % (2527817)Peak memory usage: 258 MB
% 37.43/6.65 % (2527817)Instructions burned: 7431 (million)
% 37.43/6.65 % (2527817)------------------------------
% 37.43/6.65 % (2527817)------------------------------
% 37.43/6.65 % (2527811)Success in time 5.792 s
% 37.43/6.65 % Vampire exiting
%------------------------------------------------------------------------------