%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : TOP033+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n026.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:58 PM UTC 2026
% Result : Theorem 58.55s 17.19s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 89
% Syntax : Number of formulae : 539 ( 95 unt; 60 def)
% Number of atoms : 2441 ( 222 equ)
% Maximal formula atoms : 19 ( 4 avg)
% Number of connectives : 3335 (1433 ~;1614 |; 147 &)
% ( 79 <=>; 62 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 79 ( 77 usr; 57 prp; 0-3 aty)
% Number of functors : 25 ( 25 usr; 5 con; 0-4 aty)
% Number of variables : 478 ( 0 sgn 465 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f117,axiom,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k3_xboole_0(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t48_xboole_1) ).
fof(f258,axiom,
! [X0] : k2_tarski(X0,X0) = k1_tarski(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f574,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k5_subset_1) ).
fof(f678,axiom,
! [X0,X1,X2] :
( ( r2_hidden(X0,X1)
& m1_subset_1(X1,k1_zfmisc_1(X2)) )
=> m1_subset_1(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
fof(f1483,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f2105,axiom,
! [X0,X1,X2,X3] :
( ( ~ v1_xboole_0(X0)
& v1_funct_1(X2)
& v1_funct_2(X2,X0,X1)
& m1_relset_1(X2,X0,X1)
& m1_subset_1(X3,X0) )
=> m1_subset_1(k8_funct_2(X0,X1,X2,X3),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k8_funct_2) ).
fof(f17598,axiom,
! [X0] :
( l1_struct_0(X0)
=> ( v3_struct_0(X0)
<=> v1_xboole_0(u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_struct_0) ).
fof(f17609,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> k1_struct_0(X0,X1) = k1_tarski(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k1_struct_0) ).
fof(f18263,axiom,
! [X0] :
( l1_struct_0(X0)
=> k2_pre_topc(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_pre_topc) ).
fof(f18264,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> r2_hidden(X1,k2_pre_topc(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t13_pre_topc) ).
fof(f18318,axiom,
! [X0] :
( l1_pre_topc(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f18322,axiom,
! [X0] :
( l1_struct_0(X0)
=> m1_subset_1(k2_pre_topc(X0),k1_zfmisc_1(u1_struct_0(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_pre_topc) ).
fof(f18409,axiom,
! [X0] :
( ( v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> v3_pre_topc(k2_pre_topc(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t53_tops_1) ).
fof(f27913,axiom,
! [X0] :
( l1_pre_topc(X0)
=> m1_pre_topc(X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_tsep_1) ).
fof(f34203,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_hidden(X2,k2_tex_4(X0,X1))
<=> k2_tex_4(X0,X2) = k2_tex_4(X0,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t23_tex_4) ).
fof(f34234,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v3_pre_topc(X1,X0)
=> k3_tex_4(X0,X1) = X1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t58_tex_4) ).
fof(f34274,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/sandbox/benchmark/theBenchmark.p',dt_k4_tex_4) ).
fof(f34275,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> k4_tex_4(X0,X1) = k2_tex_4(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k4_tex_4) ).
fof(f34354,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ( X2 = u1_struct_0(X1)
=> ( v1_tsp_1(X2,X0)
<=> v2_t_0topsp(X1) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_tsp_1) ).
fof(f34364,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m2_tsp_1(X1,X0)
=> l1_pre_topc(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_tsp_1) ).
fof(f34366,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_tsp_1) ).
fof(f34377,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v1_tsp_1(X1,X0)
<=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_hidden(X2,X1)
=> k5_subset_1(u1_struct_0(X0),X1,k4_tex_4(X0,X2)) = k1_struct_0(X0,X2) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_tsp_2) ).
fof(f34381,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_2(X1,X0)
<=> ( v1_tsp_1(X1,X0)
& k3_tex_4(X0,X1) = u1_struct_0(X0) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_tsp_2) ).
fof(f34393,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_pre_topc(X0) )
=> ! [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_2(X2,X0)
<=> v2_tsp_2(X1,X0) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t11_tsp_2) ).
fof(f34394,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m2_tsp_1(X1,X0)
=> m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l19_tsp_2) ).
fof(f34397,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& m2_tsp_1(X1,X0) )
=> ( v2_tsp_2(X1,X0)
<=> ( v2_t_0topsp(X1)
& ! [X2] :
( ( ~ v3_struct_0(X2)
& v2_t_0topsp(X2)
& m2_tsp_1(X2,X0) )
=> ( m2_tsp_1(X1,X2)
=> g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1)) = g1_pre_topc(u1_struct_0(X2),u1_pre_topc(X2)) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_tsp_2) ).
fof(f34399,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m1_pre_topc(X1,X0)
=> ( v2_tsp_2(X1,X0)
=> ( v2_pre_topc(X1)
& v1_tex_3(X1,X0) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc3_tsp_2) ).
fof(f34415,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/sandbox/benchmark/theBenchmark.p',t20_tsp_2) ).
fof(f34416,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/sandbox/benchmark/theBenchmark.p',t21_tsp_2) ).
fof(f34417,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)],[f34416]) ).
fof(f34515,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,[],[f34417]) ).
fof(f34516,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,[],[f34515]) ).
fof(f34523,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(f34524,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(flattening,[],[f34523]) ).
fof(f34552,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,[],[f2105]) ).
fof(f34553,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,[],[f34552]) ).
fof(f34574,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,[],[f34415]) ).
fof(f34575,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,[],[f34574]) ).
fof(f34598,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,[],[f34397]) ).
fof(f34599,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,[],[f34598]) ).
fof(f34600,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34394]) ).
fof(f34601,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,[],[f34600]) ).
fof(f34602,plain,
! [X0] :
( ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34366]) ).
fof(f34604,plain,
! [X0] :
( ! [X1] :
( l1_pre_topc(X1)
| ~ m2_tsp_1(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34364]) ).
fof(f34617,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,[],[f34354]) ).
fof(f34618,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,[],[f34617]) ).
fof(f34642,plain,
! [X0] :
( ! [X1] :
( ( v2_pre_topc(X1)
& v1_tex_3(X1,X0) )
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34399]) ).
fof(f34643,plain,
! [X0] :
( ! [X1] :
( ( v2_pre_topc(X1)
& v1_tex_3(X1,X0) )
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f34642]) ).
fof(f34654,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,[],[f34377]) ).
fof(f34655,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,[],[f34654]) ).
fof(f34658,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,[],[f34275]) ).
fof(f34659,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,[],[f34658]) ).
fof(f34660,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,[],[f34274]) ).
fof(f34661,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,[],[f34660]) ).
fof(f35050,plain,
! [X0] :
( m1_pre_topc(X0,X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f27913]) ).
fof(f35100,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f574]) ).
fof(f35101,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f35100]) ).
fof(f35123,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,[],[f17609]) ).
fof(f35124,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,[],[f35123]) ).
fof(f35402,plain,
! [X0] :
( ! [X1] :
( k3_tex_4(X0,X1) = X1
| ~ v3_pre_topc(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34234]) ).
fof(f35403,plain,
! [X0] :
( ! [X1] :
( k3_tex_4(X0,X1) = X1
| ~ v3_pre_topc(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f35402]) ).
fof(f35527,plain,
! [X0] :
( ! [X1] :
( ( v1_tsp_2(X1,X0)
<=> ( v1_tsp_1(X1,X0)
& k3_tex_4(X0,X1) = 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,[],[f34381]) ).
fof(f35528,plain,
! [X0] :
( ! [X1] :
( ( v1_tsp_2(X1,X0)
<=> ( v1_tsp_1(X1,X0)
& k3_tex_4(X0,X1) = 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,[],[f35527]) ).
fof(f35798,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v1_tsp_2(X2,X0)
<=> v2_tsp_2(X1,X0) )
| u1_struct_0(X1) != X2
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34393]) ).
fof(f35799,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v1_tsp_2(X2,X0)
<=> v2_tsp_2(X1,X0) )
| u1_struct_0(X1) != X2
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f35798]) ).
fof(f35848,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,[],[f34203]) ).
fof(f35849,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,[],[f35848]) ).
fof(f36548,plain,
! [X0] :
( v3_pre_topc(k2_pre_topc(X0),X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f18409]) ).
fof(f36549,plain,
! [X0] :
( v3_pre_topc(k2_pre_topc(X0),X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f36548]) ).
fof(f36554,plain,
! [X0] :
( m1_subset_1(k2_pre_topc(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f18322]) ).
fof(f36574,plain,
! [X0] :
( ! [X1] :
( r2_hidden(X1,k2_pre_topc(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f18264]) ).
fof(f36575,plain,
! [X0] :
( ! [X1] :
( r2_hidden(X1,k2_pre_topc(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f36574]) ).
fof(f36576,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f18263]) ).
fof(f36851,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f18318]) ).
fof(f36852,plain,
! [X0] :
( ( v3_struct_0(X0)
<=> v1_xboole_0(u1_struct_0(X0)) )
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f17598]) ).
fof(f38225,plain,
( ~ v3_borsuk_1(sK108,sK106,sK107)
& ! [X3] :
( r2_hidden(k8_funct_2(u1_struct_0(sK106),u1_struct_0(sK107),sK108,X3),k4_tex_4(sK106,X3))
| ~ m1_subset_1(X3,u1_struct_0(sK106)) )
& v1_funct_1(sK108)
& v1_funct_2(sK108,u1_struct_0(sK106),u1_struct_0(sK107))
& v5_pre_topc(sK108,sK106,sK107)
& m2_relset_1(sK108,u1_struct_0(sK106),u1_struct_0(sK107))
& ~ v3_struct_0(sK107)
& v2_tsp_2(sK107,sK106)
& m2_tsp_1(sK107,sK106)
& ~ v3_struct_0(sK106)
& v2_pre_topc(sK106)
& l1_pre_topc(sK106) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK106,sK107,sK108]),skolemize(X0,sK106),skolemize(X1,sK107),skolemize(X2,sK108)],[f34516]) ).
fof(f38252,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,sK129(X0,X1,X2,X3))) != k1_struct_0(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,sK129(X0,X1,X2,X3)))
& m1_subset_1(sK129(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,[sK129]),skolemize(X4,sK129(X0,X1,X2,X3))],[f34575]) ).
fof(f38272,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,[],[f34599]) ).
fof(f38273,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,[],[f38272]) ).
fof(f38274,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,[],[f38273]) ).
fof(f38275,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(sK137(X0,X1)),u1_pre_topc(sK137(X0,X1)))
& m2_tsp_1(X1,sK137(X0,X1))
& ~ v3_struct_0(sK137(X0,X1))
& v2_t_0topsp(sK137(X0,X1))
& m2_tsp_1(sK137(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,[sK137]),skolemize(X2,sK137(X0,X1))],[f38274]) ).
fof(f38276,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,[],[f34602]) ).
fof(f38280,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,[],[f34618]) ).
fof(f38310,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,[],[f34655]) ).
fof(f38311,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,[],[f38310]) ).
fof(f38312,plain,
! [X0] :
( ! [X1] :
( ( ( v1_tsp_1(X1,X0)
| ( k1_struct_0(X0,sK158(X0,X1)) != k5_subset_1(u1_struct_0(X0),X1,k4_tex_4(X0,sK158(X0,X1)))
& r2_hidden(sK158(X0,X1),X1)
& m1_subset_1(sK158(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,[sK158]),skolemize(X2,sK158(X0,X1))],[f38311]) ).
fof(f38409,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,[],[f1483]) ).
fof(f38661,plain,
! [X0] :
( ! [X1] :
( ( ( v1_tsp_2(X1,X0)
| ~ v1_tsp_1(X1,X0)
| u1_struct_0(X0) != k3_tex_4(X0,X1) )
& ( ( v1_tsp_1(X1,X0)
& k3_tex_4(X0,X1) = u1_struct_0(X0) )
| ~ v1_tsp_2(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,[],[f35528]) ).
fof(f38662,plain,
! [X0] :
( ! [X1] :
( ( ( v1_tsp_2(X1,X0)
| ~ v1_tsp_1(X1,X0)
| u1_struct_0(X0) != k3_tex_4(X0,X1) )
& ( ( v1_tsp_1(X1,X0)
& k3_tex_4(X0,X1) = u1_struct_0(X0) )
| ~ v1_tsp_2(X1,X0) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f38661]) ).
fof(f38762,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v1_tsp_2(X2,X0)
| ~ v2_tsp_2(X1,X0) )
& ( v2_tsp_2(X1,X0)
| ~ v1_tsp_2(X2,X0) ) )
| u1_struct_0(X1) != X2
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f35799]) ).
fof(f38770,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,[],[f35849]) ).
fof(f39139,plain,
! [X0] :
( ( ( v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) )
& ( v1_xboole_0(u1_struct_0(X0))
| ~ v3_struct_0(X0) ) )
| ~ l1_struct_0(X0) ),
inference(nnf_transformation,[],[f36852]) ).
fof(f39742,plain,
l1_pre_topc(sK106),
inference(cnf_transformation,[],[f38225]) ).
fof(f39743,plain,
v2_pre_topc(sK106),
inference(cnf_transformation,[],[f38225]) ).
fof(f39744,plain,
~ v3_struct_0(sK106),
inference(cnf_transformation,[],[f38225]) ).
fof(f39745,plain,
m2_tsp_1(sK107,sK106),
inference(cnf_transformation,[],[f38225]) ).
fof(f39746,plain,
v2_tsp_2(sK107,sK106),
inference(cnf_transformation,[],[f38225]) ).
fof(f39747,plain,
~ v3_struct_0(sK107),
inference(cnf_transformation,[],[f38225]) ).
fof(f39748,plain,
m2_relset_1(sK108,u1_struct_0(sK106),u1_struct_0(sK107)),
inference(cnf_transformation,[],[f38225]) ).
fof(f39749,plain,
v5_pre_topc(sK108,sK106,sK107),
inference(cnf_transformation,[],[f38225]) ).
fof(f39750,plain,
v1_funct_2(sK108,u1_struct_0(sK106),u1_struct_0(sK107)),
inference(cnf_transformation,[],[f38225]) ).
fof(f39751,plain,
v1_funct_1(sK108),
inference(cnf_transformation,[],[f38225]) ).
fof(f39752,plain,
! [X3] :
( r2_hidden(k8_funct_2(u1_struct_0(sK106),u1_struct_0(sK107),sK108,X3),k4_tex_4(sK106,X3))
| ~ m1_subset_1(X3,u1_struct_0(sK106)) ),
inference(cnf_transformation,[],[f38225]) ).
fof(f39753,plain,
~ v3_borsuk_1(sK108,sK106,sK107),
inference(cnf_transformation,[],[f38225]) ).
fof(f39764,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(cnf_transformation,[],[f34524]) ).
fof(f39813,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,[],[f34553]) ).
fof(f39849,plain,
! [X2,X3,X0,X1] :
( u1_struct_0(X1) != X3
| v3_borsuk_1(X2,X0,X1)
| m1_subset_1(sK129(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,[],[f38252]) ).
fof(f39850,plain,
! [X2,X3,X0,X1] :
( k5_subset_1(u1_struct_0(X0),X3,k4_tex_4(X0,sK129(X0,X1,X2,X3))) != k1_struct_0(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,sK129(X0,X1,X2,X3)))
| u1_struct_0(X1) != X3
| v3_borsuk_1(X2,X0,X1)
| ~ 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,[],[f38252]) ).
fof(f39893,plain,
! [X0,X1] :
( ~ v2_tsp_2(X1,X0)
| v2_t_0topsp(X1)
| v3_struct_0(X1)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f38275]) ).
fof(f39899,plain,
! [X0,X1] :
( m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f34601]) ).
fof(f39900,plain,
! [X0,X1] :
( m1_pre_topc(X1,X0)
| ~ m2_tsp_1(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f38276]) ).
fof(f39901,plain,
! [X0,X1] :
( ~ m1_pre_topc(X1,X0)
| m2_tsp_1(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f38276]) ).
fof(f39903,plain,
! [X0,X1] :
( ~ m2_tsp_1(X1,X0)
| l1_pre_topc(X1)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f34604]) ).
fof(f39920,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,[],[f38280]) ).
fof(f39999,plain,
! [X0,X1] :
( ~ v2_tsp_2(X1,X0)
| v2_pre_topc(X1)
| ~ m1_pre_topc(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f34643]) ).
fof(f40025,plain,
! [X3,X0,X1] :
( ~ v2_pre_topc(X0)
| ~ 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)
| k1_struct_0(X0,X3) = k5_subset_1(u1_struct_0(X0),X1,k4_tex_4(X0,X3))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f38312]) ).
fof(f40036,plain,
! [X0,X1] :
( k2_tex_4(X0,X1) = k4_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(cnf_transformation,[],[f34659]) ).
fof(f40037,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,[],[f34661]) ).
fof(f40347,plain,
! [X2,X0,X1] :
( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f38409]) ).
fof(f40657,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| m1_pre_topc(X0,X0) ),
inference(cnf_transformation,[],[f35050]) ).
fof(f40719,plain,
! [X2,X0,X1] :
( k3_xboole_0(X1,X2) = k5_subset_1(X0,X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f35101]) ).
fof(f40742,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,[],[f35124]) ).
fof(f41104,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k4_xboole_0(X0,k4_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f117]) ).
fof(f41182,plain,
! [X0,X1] :
( ~ v3_pre_topc(X1,X0)
| k3_tex_4(X0,X1) = X1
| ~ 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,[],[f35403]) ).
fof(f41473,plain,
! [X0,X1] :
( ~ v2_pre_topc(X0)
| ~ v1_tsp_2(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| u1_struct_0(X0) = k3_tex_4(X0,X1)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f38662]) ).
fof(f41474,plain,
! [X0,X1] :
( ~ v2_pre_topc(X0)
| ~ v1_tsp_2(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| v1_tsp_1(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f38662]) ).
fof(f41475,plain,
! [X0,X1] :
( u1_struct_0(X0) != k3_tex_4(X0,X1)
| ~ v1_tsp_1(X1,X0)
| v1_tsp_2(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,[],[f38662]) ).
fof(f42006,plain,
! [X2,X0,X1] :
( u1_struct_0(X1) != X2
| ~ v2_tsp_2(X1,X0)
| v1_tsp_2(X2,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f38762]) ).
fof(f42043,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X2,k2_tex_4(X0,X1))
| k2_tex_4(X0,X1) = k2_tex_4(X0,X2)
| ~ 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(cnf_transformation,[],[f38770]) ).
fof(f43123,plain,
! [X0] : k1_tarski(X0) = k2_tarski(X0,X0),
inference(cnf_transformation,[],[f258]) ).
fof(f43142,plain,
! [X0] :
( ~ v2_pre_topc(X0)
| v3_pre_topc(k2_pre_topc(X0),X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f36549]) ).
fof(f43147,plain,
! [X0] :
( ~ l1_struct_0(X0)
| m1_subset_1(k2_pre_topc(X0),k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f36554]) ).
fof(f43168,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| r2_hidden(X1,k2_pre_topc(X0))
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f36575]) ).
fof(f43169,plain,
! [X0] :
( u1_struct_0(X0) = k2_pre_topc(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f36576]) ).
fof(f43506,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f36851]) ).
fof(f43509,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f39139]) ).
fof(f45861,plain,
! [X2,X0,X1] :
( k5_subset_1(X0,X1,X2) = k4_xboole_0(X1,k4_xboole_0(X1,X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(definition_unfolding,[],[f40719,f41104]) ).
fof(f45862,plain,
! [X0,X1] :
( v3_struct_0(X0)
| k1_struct_0(X0,X1) = k2_tarski(X1,X1)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(definition_unfolding,[],[f40742,f43123]) ).
fof(f46545,definition,
sF924 = u1_struct_0(sK106),
introduced(definition,[new_symbols(definition,[sF924])],[function_definition]) ).
fof(f46546,plain,
u1_struct_0(sK106) = sF924,
inference(reorient_equations,[],[f46545]) ).
fof(f46547,definition,
sF925 = u1_struct_0(sK107),
introduced(definition,[new_symbols(definition,[sF925])],[function_definition]) ).
fof(f46548,plain,
u1_struct_0(sK107) = sF925,
inference(reorient_equations,[],[f46547]) ).
fof(f46549,definition,
! [X3] : sF926(X3) = k8_funct_2(sF924,sF925,sK108,X3),
introduced(definition,[new_symbols(definition,[sF926])],[function_definition]) ).
fof(f46550,plain,
! [X3] : k8_funct_2(sF924,sF925,sK108,X3) = sF926(X3),
inference(reorient_equations,[],[f46549]) ).
fof(f46551,definition,
! [X3] : sF927(X3) = k4_tex_4(sK106,X3),
introduced(definition,[new_symbols(definition,[sF927])],[function_definition]) ).
fof(f46552,plain,
! [X3] : k4_tex_4(sK106,X3) = sF927(X3),
inference(reorient_equations,[],[f46551]) ).
fof(f46553,plain,
! [X3] :
( r2_hidden(sF926(X3),sF927(X3))
| ~ m1_subset_1(X3,sF924) ),
inference(definition_folding,[],[f39752,f46546,f46552,f46550,f46548,f46546]) ).
fof(f46554,plain,
v1_funct_2(sK108,sF924,sF925),
inference(definition_folding,[],[f39750,f46548,f46546]) ).
fof(f46555,plain,
m2_relset_1(sK108,sF924,sF925),
inference(definition_folding,[],[f39748,f46548,f46546]) ).
fof(f46659,plain,
( l1_pre_topc(sK107)
| ~ l1_pre_topc(sK106) ),
inference(resolution,[],[f39903,f39745]) ).
fof(f46661,definition,
( spl928_18
<=> l1_pre_topc(sK106) ),
introduced(definition,[new_symbols(definition,[spl928_18])],[avatar_definition]) ).
fof(f46665,definition,
( spl928_19
<=> l1_pre_topc(sK107) ),
introduced(definition,[new_symbols(definition,[spl928_19])],[avatar_definition]) ).
fof(f46667,plain,
( l1_pre_topc(sK107)
| ~ spl928_19 ),
inference(avatar_component_clause,[],[f46665]) ).
fof(f46668,plain,
( ~ spl928_18
| spl928_19 ),
inference(avatar_split_clause,[],[f46659,f46665,f46661]) ).
fof(f46669,plain,
! [X0] :
( m1_subset_1(sF927(X0),k1_zfmisc_1(u1_struct_0(sK106)))
| v3_struct_0(sK106)
| ~ v2_pre_topc(sK106)
| ~ l1_pre_topc(sK106)
| ~ m1_subset_1(X0,u1_struct_0(sK106)) ),
inference(superposition,[],[f40037,f46552]) ).
fof(f46674,definition,
( spl928_20
<=> v2_pre_topc(sK107) ),
introduced(definition,[new_symbols(definition,[spl928_20])],[avatar_definition]) ).
fof(f46675,plain,
( v2_pre_topc(sK107)
| ~ spl928_20 ),
inference(avatar_component_clause,[],[f46674]) ).
fof(f46678,definition,
( spl928_21
<=> v3_struct_0(sK107) ),
introduced(definition,[new_symbols(definition,[spl928_21])],[avatar_definition]) ).
fof(f46679,plain,
( ~ v3_struct_0(sK107)
| spl928_21 ),
inference(avatar_component_clause,[],[f46678]) ).
fof(f46685,plain,
! [X0] :
( m1_subset_1(sF927(X0),k1_zfmisc_1(sF924))
| v3_struct_0(sK106)
| ~ v2_pre_topc(sK106)
| ~ l1_pre_topc(sK106)
| ~ m1_subset_1(X0,u1_struct_0(sK106)) ),
inference(forward_demodulation,[],[f46669,f46546]) ).
fof(f46687,definition,
( spl928_23
<=> v2_pre_topc(sK106) ),
introduced(definition,[new_symbols(definition,[spl928_23])],[avatar_definition]) ).
fof(f46688,plain,
( v2_pre_topc(sK106)
| ~ spl928_23 ),
inference(avatar_component_clause,[],[f46687]) ).
fof(f46691,definition,
( spl928_24
<=> v3_struct_0(sK106) ),
introduced(definition,[new_symbols(definition,[spl928_24])],[avatar_definition]) ).
fof(f46692,plain,
( ~ v3_struct_0(sK106)
| spl928_24 ),
inference(avatar_component_clause,[],[f46691]) ).
fof(f46695,definition,
( spl928_25
<=> ! [X0] :
( m1_subset_1(sF927(X0),k1_zfmisc_1(sF924))
| ~ m1_subset_1(X0,sF924) ) ),
introduced(definition,[new_symbols(definition,[spl928_25])],[avatar_definition]) ).
fof(f46696,plain,
( ! [X0] :
( m1_subset_1(sF927(X0),k1_zfmisc_1(sF924))
| ~ m1_subset_1(X0,sF924) )
| ~ spl928_25 ),
inference(avatar_component_clause,[],[f46695]) ).
fof(f46698,plain,
! [X0] :
( ~ m1_subset_1(X0,sF924)
| m1_subset_1(sF927(X0),k1_zfmisc_1(sF924))
| v3_struct_0(sK106)
| ~ v2_pre_topc(sK106)
| ~ l1_pre_topc(sK106) ),
inference(forward_demodulation,[],[f46685,f46546]) ).
fof(f46699,plain,
( ~ spl928_18
| ~ spl928_23
| spl928_24
| spl928_25 ),
inference(avatar_split_clause,[],[f46698,f46695,f46691,f46687,f46661]) ).
fof(f46703,definition,
( spl928_26
<=> m1_relset_1(sK108,sF924,sF925) ),
introduced(definition,[new_symbols(definition,[spl928_26])],[avatar_definition]) ).
fof(f46705,plain,
( ~ m1_relset_1(sK108,sF924,sF925)
| spl928_26 ),
inference(avatar_component_clause,[],[f46703]) ).
fof(f46707,definition,
( spl928_27
<=> v1_funct_2(sK108,sF924,sF925) ),
introduced(definition,[new_symbols(definition,[spl928_27])],[avatar_definition]) ).
fof(f46708,plain,
( v1_funct_2(sK108,sF924,sF925)
| ~ spl928_27 ),
inference(avatar_component_clause,[],[f46707]) ).
fof(f46711,definition,
( spl928_28
<=> v1_funct_1(sK108) ),
introduced(definition,[new_symbols(definition,[spl928_28])],[avatar_definition]) ).
fof(f46715,definition,
( spl928_29
<=> v1_xboole_0(sF924) ),
introduced(definition,[new_symbols(definition,[spl928_29])],[avatar_definition]) ).
fof(f46723,plain,
! [X0] :
( m1_subset_1(sF926(X0),sF925)
| v1_xboole_0(sF924)
| ~ v1_funct_1(sK108)
| ~ v1_funct_2(sK108,sF924,sF925)
| ~ m1_relset_1(sK108,sF924,sF925)
| ~ m1_subset_1(X0,sF924) ),
inference(superposition,[],[f39813,f46550]) ).
fof(f46727,definition,
( spl928_31
<=> ! [X0] :
( m1_subset_1(sF926(X0),sF925)
| ~ m1_subset_1(X0,sF924) ) ),
introduced(definition,[new_symbols(definition,[spl928_31])],[avatar_definition]) ).
fof(f46728,plain,
( ! [X0] :
( m1_subset_1(sF926(X0),sF925)
| ~ m1_subset_1(X0,sF924) )
| ~ spl928_31 ),
inference(avatar_component_clause,[],[f46727]) ).
fof(f46729,plain,
( ~ spl928_26
| ~ spl928_27
| ~ spl928_28
| spl928_29
| spl928_31 ),
inference(avatar_split_clause,[],[f46723,f46727,f46715,f46711,f46707,f46703]) ).
fof(f46730,plain,
! [X0] :
( m1_subset_1(sF925,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_tsp_1(sK107,X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(superposition,[],[f39899,f46548]) ).
fof(f46764,plain,
! [X2,X0,X1] :
( m1_subset_1(sK129(X1,X2,X0,u1_struct_0(X2)),u1_struct_0(X1))
| v3_borsuk_1(X0,X1,X2)
| ~ m1_subset_1(u1_struct_0(X2),k1_zfmisc_1(u1_struct_0(X1)))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v5_pre_topc(X0,X1,X2)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ v2_tsp_2(X2,X1)
| ~ m2_tsp_1(X2,X1)
| v3_struct_0(X1)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1) ),
inference(equality_resolution,[],[f39849]) ).
fof(f46775,plain,
~ spl928_24,
inference(avatar_split_clause,[],[f39744,f46691]) ).
fof(f46778,plain,
~ spl928_21,
inference(avatar_split_clause,[],[f39747,f46678]) ).
fof(f46779,plain,
! [X0,X1] :
( m1_subset_1(sK129(X0,sK107,X1,sF925),u1_struct_0(X0))
| v3_borsuk_1(X1,X0,sK107)
| ~ m1_subset_1(sF925,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),sF925)
| ~ v5_pre_topc(X1,X0,sK107)
| ~ m2_relset_1(X1,u1_struct_0(X0),sF925)
| v3_struct_0(sK107)
| ~ v2_tsp_2(sK107,X0)
| ~ m2_tsp_1(sK107,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(superposition,[],[f46764,f46548]) ).
fof(f46796,definition,
( spl928_43
<=> ! [X0,X1] :
( m1_subset_1(sK129(X0,sK107,X1,sF925),u1_struct_0(X0))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ m2_tsp_1(sK107,X0)
| ~ v2_tsp_2(sK107,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),sF925)
| ~ v5_pre_topc(X1,X0,sK107)
| ~ v1_funct_2(X1,u1_struct_0(X0),sF925)
| ~ v1_funct_1(X1)
| ~ m1_subset_1(sF925,k1_zfmisc_1(u1_struct_0(X0)))
| v3_borsuk_1(X1,X0,sK107) ) ),
introduced(definition,[new_symbols(definition,[spl928_43])],[avatar_definition]) ).
fof(f46797,plain,
( ! [X0,X1] :
( m1_subset_1(sK129(X0,sK107,X1,sF925),u1_struct_0(X0))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ m2_tsp_1(sK107,X0)
| ~ v2_tsp_2(sK107,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),sF925)
| ~ v5_pre_topc(X1,X0,sK107)
| ~ v1_funct_2(X1,u1_struct_0(X0),sF925)
| ~ v1_funct_1(X1)
| ~ m1_subset_1(sF925,k1_zfmisc_1(u1_struct_0(X0)))
| v3_borsuk_1(X1,X0,sK107) )
| ~ spl928_43 ),
inference(avatar_component_clause,[],[f46796]) ).
fof(f46798,plain,
( spl928_21
| spl928_43 ),
inference(avatar_split_clause,[],[f46779,f46796,f46678]) ).
fof(f46818,plain,
( ! [X0] :
( m1_subset_1(sK129(sK106,sK107,X0,sF925),sF924)
| ~ l1_pre_topc(sK106)
| ~ v2_pre_topc(sK106)
| v3_struct_0(sK106)
| ~ m2_tsp_1(sK107,sK106)
| ~ v2_tsp_2(sK107,sK106)
| ~ m2_relset_1(X0,sF924,sF925)
| ~ v5_pre_topc(X0,sK106,sK107)
| ~ v1_funct_2(X0,sF924,sF925)
| ~ v1_funct_1(X0)
| ~ m1_subset_1(sF925,k1_zfmisc_1(sF924))
| v3_borsuk_1(X0,sK106,sK107) )
| ~ spl928_43 ),
inference(superposition,[],[f46797,f46546]) ).
fof(f46820,definition,
( spl928_48
<=> m1_subset_1(sF925,k1_zfmisc_1(sF924)) ),
introduced(definition,[new_symbols(definition,[spl928_48])],[avatar_definition]) ).
fof(f46824,definition,
( spl928_49
<=> v2_tsp_2(sK107,sK106) ),
introduced(definition,[new_symbols(definition,[spl928_49])],[avatar_definition]) ).
fof(f46825,plain,
( v2_tsp_2(sK107,sK106)
| ~ spl928_49 ),
inference(avatar_component_clause,[],[f46824]) ).
fof(f46828,definition,
( spl928_50
<=> m2_tsp_1(sK107,sK106) ),
introduced(definition,[new_symbols(definition,[spl928_50])],[avatar_definition]) ).
fof(f46832,definition,
( spl928_51
<=> ! [X0] :
( m1_subset_1(sK129(sK106,sK107,X0,sF925),sF924)
| v3_borsuk_1(X0,sK106,sK107)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF924,sF925)
| ~ v5_pre_topc(X0,sK106,sK107)
| ~ m2_relset_1(X0,sF924,sF925) ) ),
introduced(definition,[new_symbols(definition,[spl928_51])],[avatar_definition]) ).
fof(f46833,plain,
( ! [X0] :
( m1_subset_1(sK129(sK106,sK107,X0,sF925),sF924)
| v3_borsuk_1(X0,sK106,sK107)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF924,sF925)
| ~ v5_pre_topc(X0,sK106,sK107)
| ~ m2_relset_1(X0,sF924,sF925) )
| ~ spl928_51 ),
inference(avatar_component_clause,[],[f46832]) ).
fof(f46834,plain,
( ~ spl928_48
| ~ spl928_49
| ~ spl928_50
| spl928_24
| ~ spl928_23
| ~ spl928_18
| spl928_51
| ~ spl928_43 ),
inference(avatar_split_clause,[],[f46818,f46796,f46832,f46661,f46687,f46691,f46828,f46824,f46820]) ).
fof(f46836,definition,
( spl928_52
<=> m1_subset_1(sF925,k1_zfmisc_1(sF925)) ),
introduced(definition,[new_symbols(definition,[spl928_52])],[avatar_definition]) ).
fof(f46844,definition,
( spl928_54
<=> m2_tsp_1(sK107,sK107) ),
introduced(definition,[new_symbols(definition,[spl928_54])],[avatar_definition]) ).
fof(f46845,plain,
( m2_tsp_1(sK107,sK107)
| ~ spl928_54 ),
inference(avatar_component_clause,[],[f46844]) ).
fof(f46855,definition,
( spl928_56
<=> v2_t_0topsp(sK107) ),
introduced(definition,[new_symbols(definition,[spl928_56])],[avatar_definition]) ).
fof(f46859,plain,
( ~ m2_relset_1(sK108,sF924,sF925)
| spl928_26 ),
inference(resolution,[],[f46705,f40347]) ).
fof(f46860,plain,
( $false
| spl928_26 ),
inference(backward_subsumption_resolution,[],[f46555,f46859]) ).
fof(f46862,plain,
spl928_26,
inference(avatar_contradiction_clause,[],[f46860]) ).
fof(f46865,plain,
spl928_18,
inference(avatar_split_clause,[],[f39742,f46661]) ).
fof(f46868,plain,
spl928_23,
inference(avatar_split_clause,[],[f39743,f46687]) ).
fof(f46871,plain,
spl928_50,
inference(avatar_split_clause,[],[f39745,f46828]) ).
fof(f46877,plain,
( m1_subset_1(sF925,k1_zfmisc_1(sF925))
| ~ m2_tsp_1(sK107,sK107)
| v3_struct_0(sK107)
| ~ l1_pre_topc(sK107) ),
inference(superposition,[],[f46730,f46548]) ).
fof(f46878,plain,
( m1_subset_1(sF925,k1_zfmisc_1(sF924))
| ~ m2_tsp_1(sK107,sK106)
| v3_struct_0(sK106)
| ~ l1_pre_topc(sK106) ),
inference(superposition,[],[f46730,f46546]) ).
fof(f46879,plain,
( ~ spl928_18
| spl928_24
| ~ spl928_50
| spl928_48 ),
inference(avatar_split_clause,[],[f46878,f46820,f46828,f46691,f46661]) ).
fof(f46880,plain,
( ~ spl928_19
| spl928_21
| ~ spl928_54
| spl928_52 ),
inference(avatar_split_clause,[],[f46877,f46836,f46844,f46678,f46665]) ).
fof(f46883,plain,
spl928_49,
inference(avatar_split_clause,[],[f39746,f46824]) ).
fof(f46884,plain,
( v2_t_0topsp(sK107)
| v3_struct_0(sK107)
| ~ m2_tsp_1(sK107,sK106)
| v3_struct_0(sK106)
| ~ v2_pre_topc(sK106)
| ~ l1_pre_topc(sK106)
| ~ spl928_49 ),
inference(resolution,[],[f46825,f39893]) ).
fof(f46885,plain,
( ~ spl928_18
| ~ spl928_23
| spl928_24
| ~ spl928_50
| spl928_21
| spl928_56
| ~ spl928_49 ),
inference(avatar_split_clause,[],[f46884,f46824,f46855,f46678,f46828,f46691,f46687,f46661]) ).
fof(f46944,plain,
spl928_27,
inference(avatar_split_clause,[],[f46554,f46707]) ).
fof(f46947,plain,
spl928_28,
inference(avatar_split_clause,[],[f39751,f46711]) ).
fof(f46950,plain,
! [X0,X1] :
( ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(X1)))
| v1_tsp_2(u1_struct_0(X0),X1)
| ~ v2_tsp_2(X0,X1)
| ~ m2_tsp_1(X0,X1)
| v3_struct_0(X1)
| ~ l1_pre_topc(X1) ),
inference(equality_resolution,[],[f42006]) ).
fof(f46952,plain,
! [X0] :
( ~ m1_subset_1(sF925,k1_zfmisc_1(u1_struct_0(X0)))
| v1_tsp_2(sF925,X0)
| ~ v2_tsp_2(sK107,X0)
| ~ m2_tsp_1(sK107,X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(superposition,[],[f46950,f46548]) ).
fof(f46981,plain,
! [X0] :
( v1_tsp_2(sF925,X0)
| ~ v2_tsp_2(sK107,X0)
| ~ m2_tsp_1(sK107,X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0)
| ~ m2_tsp_1(sK107,X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(resolution,[],[f46952,f46730]) ).
fof(f46984,plain,
! [X0] :
( v1_tsp_2(sF925,X0)
| ~ v2_tsp_2(sK107,X0)
| ~ m2_tsp_1(sK107,X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(duplicate_literal_removal,[],[f46981]) ).
fof(f46995,definition,
( spl928_72
<=> l1_struct_0(sK106) ),
introduced(definition,[new_symbols(definition,[spl928_72])],[avatar_definition]) ).
fof(f46997,plain,
( ~ l1_struct_0(sK106)
| spl928_72 ),
inference(avatar_component_clause,[],[f46995]) ).
fof(f47003,definition,
( spl928_74
<=> l1_struct_0(sK107) ),
introduced(definition,[new_symbols(definition,[spl928_74])],[avatar_definition]) ).
fof(f47004,plain,
( l1_struct_0(sK107)
| ~ spl928_74 ),
inference(avatar_component_clause,[],[f47003]) ).
fof(f47005,plain,
( ~ l1_struct_0(sK107)
| spl928_74 ),
inference(avatar_component_clause,[],[f47003]) ).
fof(f47010,plain,
( ~ l1_pre_topc(sK106)
| spl928_72 ),
inference(resolution,[],[f46997,f43506]) ).
fof(f47011,plain,
( ~ spl928_18
| spl928_72 ),
inference(avatar_split_clause,[],[f47010,f46995,f46661]) ).
fof(f47012,plain,
( ~ l1_pre_topc(sK107)
| spl928_74 ),
inference(resolution,[],[f47005,f43506]) ).
fof(f47013,plain,
( ~ spl928_19
| spl928_74 ),
inference(avatar_split_clause,[],[f47012,f47003,f46665]) ).
fof(f47096,definition,
( spl928_84
<=> m2_relset_1(sK108,sF924,sF925) ),
introduced(definition,[new_symbols(definition,[spl928_84])],[avatar_definition]) ).
fof(f47100,definition,
( spl928_85
<=> v5_pre_topc(sK108,sK106,sK107) ),
introduced(definition,[new_symbols(definition,[spl928_85])],[avatar_definition]) ).
fof(f47104,definition,
( spl928_86
<=> v3_borsuk_1(sK108,sK106,sK107) ),
introduced(definition,[new_symbols(definition,[spl928_86])],[avatar_definition]) ).
fof(f47400,plain,
spl928_84,
inference(avatar_split_clause,[],[f46555,f47096]) ).
fof(f47409,plain,
spl928_85,
inference(avatar_split_clause,[],[f39749,f47100]) ).
fof(f47412,plain,
~ spl928_86,
inference(avatar_split_clause,[],[f39753,f47104]) ).
fof(f47423,plain,
( v2_pre_topc(sK107)
| ~ m1_pre_topc(sK107,sK106)
| v3_struct_0(sK106)
| ~ v2_pre_topc(sK106)
| ~ l1_pre_topc(sK106)
| ~ spl928_49 ),
inference(resolution,[],[f39999,f46825]) ).
fof(f47425,definition,
( spl928_128
<=> m1_pre_topc(sK107,sK106) ),
introduced(definition,[new_symbols(definition,[spl928_128])],[avatar_definition]) ).
fof(f47427,plain,
( ~ m1_pre_topc(sK107,sK106)
| spl928_128 ),
inference(avatar_component_clause,[],[f47425]) ).
fof(f47428,plain,
( ~ spl928_18
| ~ spl928_23
| spl928_24
| ~ spl928_128
| spl928_20
| ~ spl928_49 ),
inference(avatar_split_clause,[],[f47423,f46824,f46674,f47425,f46691,f46687,f46661]) ).
fof(f47430,plain,
( ~ v1_xboole_0(sF924)
| v3_struct_0(sK106)
| ~ l1_struct_0(sK106) ),
inference(superposition,[],[f43509,f46546]) ).
fof(f47431,plain,
( ~ spl928_72
| spl928_24
| ~ spl928_29 ),
inference(avatar_split_clause,[],[f47430,f46715,f46691,f46995]) ).
fof(f47626,plain,
! [X0,X1] :
( m1_subset_1(sF926(X0),X1)
| ~ m1_subset_1(sF927(X0),k1_zfmisc_1(X1))
| ~ m1_subset_1(X0,sF924) ),
inference(resolution,[],[f39764,f46553]) ).
fof(f47750,plain,
( ! [X0] :
( k2_tarski(X0,X0) = k1_struct_0(sK106,X0)
| ~ l1_struct_0(sK106)
| ~ m1_subset_1(X0,u1_struct_0(sK106)) )
| spl928_24 ),
inference(resolution,[],[f45862,f46692]) ).
fof(f47751,plain,
( ! [X0] :
( k2_tarski(X0,X0) = k1_struct_0(sK107,X0)
| ~ l1_struct_0(sK107)
| ~ m1_subset_1(X0,u1_struct_0(sK107)) )
| spl928_21 ),
inference(resolution,[],[f45862,f46679]) ).
fof(f47752,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF925)
| k2_tarski(X0,X0) = k1_struct_0(sK107,X0)
| ~ l1_struct_0(sK107) )
| spl928_21 ),
inference(forward_demodulation,[],[f47751,f46548]) ).
fof(f47753,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF924)
| k2_tarski(X0,X0) = k1_struct_0(sK106,X0)
| ~ l1_struct_0(sK106) )
| spl928_24 ),
inference(forward_demodulation,[],[f47750,f46546]) ).
fof(f47755,definition,
( spl928_159
<=> ! [X0] :
( ~ m1_subset_1(X0,sF925)
| k2_tarski(X0,X0) = k1_struct_0(sK107,X0) ) ),
introduced(definition,[new_symbols(definition,[spl928_159])],[avatar_definition]) ).
fof(f47756,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF925)
| k2_tarski(X0,X0) = k1_struct_0(sK107,X0) )
| ~ spl928_159 ),
inference(avatar_component_clause,[],[f47755]) ).
fof(f47757,plain,
( ~ spl928_74
| spl928_159
| spl928_21 ),
inference(avatar_split_clause,[],[f47752,f46678,f47755,f47003]) ).
fof(f47759,definition,
( spl928_160
<=> ! [X0] :
( ~ m1_subset_1(X0,sF924)
| k2_tarski(X0,X0) = k1_struct_0(sK106,X0) ) ),
introduced(definition,[new_symbols(definition,[spl928_160])],[avatar_definition]) ).
fof(f47760,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF924)
| k2_tarski(X0,X0) = k1_struct_0(sK106,X0) )
| ~ spl928_160 ),
inference(avatar_component_clause,[],[f47759]) ).
fof(f47761,plain,
( ~ spl928_72
| spl928_160
| spl928_24 ),
inference(avatar_split_clause,[],[f47753,f46691,f47759,f46995]) ).
fof(f47818,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X2,k4_tex_4(X0,X1))
| k2_tex_4(X0,X2) = k4_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)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(superposition,[],[f42043,f40036]) ).
fof(f47819,plain,
! [X2,X0,X1] :
( ~ v2_pre_topc(X0)
| k2_tex_4(X0,X2) = k4_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)
| ~ r2_hidden(X2,k4_tex_4(X0,X1)) ),
inference(duplicate_literal_removal,[],[f47818]) ).
fof(f47820,plain,
( ! [X0,X1] :
( k2_tex_4(sK106,X0) = k4_tex_4(sK106,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK106))
| ~ m1_subset_1(X1,u1_struct_0(sK106))
| v3_struct_0(sK106)
| ~ l1_pre_topc(sK106)
| ~ r2_hidden(X0,k4_tex_4(sK106,X1)) )
| ~ spl928_23 ),
inference(resolution,[],[f47819,f46688]) ).
fof(f47821,plain,
( ! [X0,X1] :
( k2_tex_4(sK106,X0) = sF927(X1)
| ~ m1_subset_1(X0,u1_struct_0(sK106))
| ~ m1_subset_1(X1,u1_struct_0(sK106))
| v3_struct_0(sK106)
| ~ l1_pre_topc(sK106)
| ~ r2_hidden(X0,k4_tex_4(sK106,X1)) )
| ~ spl928_23 ),
inference(forward_demodulation,[],[f47820,f46552]) ).
fof(f47822,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF924)
| k2_tex_4(sK106,X0) = sF927(X1)
| ~ m1_subset_1(X1,u1_struct_0(sK106))
| v3_struct_0(sK106)
| ~ l1_pre_topc(sK106)
| ~ r2_hidden(X0,k4_tex_4(sK106,X1)) )
| ~ spl928_23 ),
inference(forward_demodulation,[],[f47821,f46546]) ).
fof(f47823,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF924)
| ~ m1_subset_1(X0,sF924)
| k2_tex_4(sK106,X0) = sF927(X1)
| v3_struct_0(sK106)
| ~ l1_pre_topc(sK106)
| ~ r2_hidden(X0,k4_tex_4(sK106,X1)) )
| ~ spl928_23 ),
inference(forward_demodulation,[],[f47822,f46546]) ).
fof(f47824,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF927(X1))
| ~ m1_subset_1(X1,sF924)
| ~ m1_subset_1(X0,sF924)
| k2_tex_4(sK106,X0) = sF927(X1)
| v3_struct_0(sK106)
| ~ l1_pre_topc(sK106) )
| ~ spl928_23 ),
inference(forward_demodulation,[],[f47823,f46552]) ).
fof(f47826,definition,
( spl928_167
<=> ! [X0,X1] :
( ~ r2_hidden(X0,sF927(X1))
| k2_tex_4(sK106,X0) = sF927(X1)
| ~ m1_subset_1(X0,sF924)
| ~ m1_subset_1(X1,sF924) ) ),
introduced(definition,[new_symbols(definition,[spl928_167])],[avatar_definition]) ).
fof(f47827,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF927(X1))
| k2_tex_4(sK106,X0) = sF927(X1)
| ~ m1_subset_1(X0,sF924)
| ~ m1_subset_1(X1,sF924) )
| ~ spl928_167 ),
inference(avatar_component_clause,[],[f47826]) ).
fof(f47828,plain,
( ~ spl928_18
| spl928_24
| spl928_167
| ~ spl928_23 ),
inference(avatar_split_clause,[],[f47824,f46687,f47826,f46691,f46661]) ).
fof(f47829,plain,
( ! [X0] :
( sF927(X0) = k2_tex_4(sK106,sF926(X0))
| ~ m1_subset_1(sF926(X0),sF924)
| ~ m1_subset_1(X0,sF924)
| ~ m1_subset_1(X0,sF924) )
| ~ spl928_167 ),
inference(resolution,[],[f47827,f46553]) ).
fof(f47830,plain,
( ! [X0] :
( ~ m1_subset_1(sF926(X0),sF924)
| sF927(X0) = k2_tex_4(sK106,sF926(X0))
| ~ m1_subset_1(X0,sF924) )
| ~ spl928_167 ),
inference(duplicate_literal_removal,[],[f47829]) ).
fof(f47831,plain,
( ! [X0] :
( sF927(X0) = k2_tex_4(sK106,sF926(X0))
| ~ m1_subset_1(X0,sF924)
| ~ m1_subset_1(sF927(X0),k1_zfmisc_1(sF924))
| ~ m1_subset_1(X0,sF924) )
| ~ spl928_167 ),
inference(resolution,[],[f47830,f47626]) ).
fof(f47833,plain,
( ! [X0] :
( ~ m1_subset_1(sF927(X0),k1_zfmisc_1(sF924))
| ~ m1_subset_1(X0,sF924)
| sF927(X0) = k2_tex_4(sK106,sF926(X0)) )
| ~ spl928_167 ),
inference(duplicate_literal_removal,[],[f47831]) ).
fof(f47834,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF924)
| sF927(X0) = k2_tex_4(sK106,sF926(X0))
| ~ m1_subset_1(X0,sF924) )
| ~ spl928_25
| ~ spl928_167 ),
inference(resolution,[],[f47833,f46696]) ).
fof(f47836,plain,
( ! [X0] :
( sF927(X0) = k2_tex_4(sK106,sF926(X0))
| ~ m1_subset_1(X0,sF924) )
| ~ spl928_25
| ~ spl928_167 ),
inference(duplicate_literal_removal,[],[f47834]) ).
fof(f47837,plain,
( ! [X0] :
( sF927(X0) = k4_tex_4(sK106,sF926(X0))
| ~ m1_subset_1(X0,sF924)
| v3_struct_0(sK106)
| ~ v2_pre_topc(sK106)
| ~ l1_pre_topc(sK106)
| ~ m1_subset_1(sF926(X0),u1_struct_0(sK106)) )
| ~ spl928_25
| ~ spl928_167 ),
inference(superposition,[],[f47836,f40036]) ).
fof(f47843,plain,
( ! [X0] :
( sF927(X0) = sF927(sF926(X0))
| ~ m1_subset_1(X0,sF924)
| v3_struct_0(sK106)
| ~ v2_pre_topc(sK106)
| ~ l1_pre_topc(sK106)
| ~ m1_subset_1(sF926(X0),u1_struct_0(sK106)) )
| ~ spl928_25
| ~ spl928_167 ),
inference(forward_demodulation,[],[f47837,f46552]) ).
fof(f47845,plain,
( ! [X0] :
( ~ m1_subset_1(sF926(X0),sF924)
| sF927(X0) = sF927(sF926(X0))
| ~ m1_subset_1(X0,sF924)
| v3_struct_0(sK106)
| ~ v2_pre_topc(sK106)
| ~ l1_pre_topc(sK106) )
| ~ spl928_25
| ~ spl928_167 ),
inference(forward_demodulation,[],[f47843,f46546]) ).
fof(f47847,definition,
( spl928_168
<=> ! [X0] :
( ~ m1_subset_1(sF926(X0),sF924)
| ~ m1_subset_1(X0,sF924)
| sF927(X0) = sF927(sF926(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl928_168])],[avatar_definition]) ).
fof(f47848,plain,
( ! [X0] :
( ~ m1_subset_1(sF926(X0),sF924)
| ~ m1_subset_1(X0,sF924)
| sF927(X0) = sF927(sF926(X0)) )
| ~ spl928_168 ),
inference(avatar_component_clause,[],[f47847]) ).
fof(f47850,plain,
( ~ spl928_18
| ~ spl928_23
| spl928_24
| spl928_168
| ~ spl928_25
| ~ spl928_167 ),
inference(avatar_split_clause,[],[f47845,f47826,f46695,f47847,f46691,f46687,f46661]) ).
fof(f47851,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF924)
| sF927(X0) = sF927(sF926(X0))
| ~ m1_subset_1(sF927(X0),k1_zfmisc_1(sF924))
| ~ m1_subset_1(X0,sF924) )
| ~ spl928_168 ),
inference(resolution,[],[f47848,f47626]) ).
fof(f47853,plain,
( ! [X0] :
( ~ m1_subset_1(sF927(X0),k1_zfmisc_1(sF924))
| sF927(X0) = sF927(sF926(X0))
| ~ m1_subset_1(X0,sF924) )
| ~ spl928_168 ),
inference(duplicate_literal_removal,[],[f47851]) ).
fof(f47882,plain,
( ! [X0] :
( sF927(X0) = sF927(sF926(X0))
| ~ m1_subset_1(X0,sF924)
| ~ m1_subset_1(X0,sF924) )
| ~ spl928_25
| ~ spl928_168 ),
inference(resolution,[],[f47853,f46696]) ).
fof(f47884,plain,
( ! [X0] :
( sF927(X0) = sF927(sF926(X0))
| ~ m1_subset_1(X0,sF924) )
| ~ spl928_25
| ~ spl928_168 ),
inference(duplicate_literal_removal,[],[f47882]) ).
fof(f48012,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK106))
| ~ v1_tsp_1(X1,sK106)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK106)))
| v3_struct_0(sK106)
| k1_struct_0(sK106,X0) = k5_subset_1(u1_struct_0(sK106),X1,k4_tex_4(sK106,X0))
| ~ l1_pre_topc(sK106) )
| ~ spl928_23 ),
inference(resolution,[],[f40025,f46688]) ).
fof(f48013,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF924)
| ~ r2_hidden(X0,X1)
| ~ v1_tsp_1(X1,sK106)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK106)))
| v3_struct_0(sK106)
| k1_struct_0(sK106,X0) = k5_subset_1(u1_struct_0(sK106),X1,k4_tex_4(sK106,X0))
| ~ l1_pre_topc(sK106) )
| ~ spl928_23 ),
inference(forward_demodulation,[],[f48012,f46546]) ).
fof(f48014,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(sF924))
| ~ m1_subset_1(X0,sF924)
| ~ r2_hidden(X0,X1)
| ~ v1_tsp_1(X1,sK106)
| v3_struct_0(sK106)
| k1_struct_0(sK106,X0) = k5_subset_1(u1_struct_0(sK106),X1,k4_tex_4(sK106,X0))
| ~ l1_pre_topc(sK106) )
| ~ spl928_23 ),
inference(forward_demodulation,[],[f48013,f46546]) ).
fof(f48015,plain,
( ! [X0,X1] :
( k1_struct_0(sK106,X0) = k5_subset_1(u1_struct_0(sK106),X1,sF927(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(sF924))
| ~ m1_subset_1(X0,sF924)
| ~ r2_hidden(X0,X1)
| ~ v1_tsp_1(X1,sK106)
| v3_struct_0(sK106)
| ~ l1_pre_topc(sK106) )
| ~ spl928_23 ),
inference(forward_demodulation,[],[f48014,f46552]) ).
fof(f48016,plain,
( ! [X0,X1] :
( k1_struct_0(sK106,X0) = k5_subset_1(sF924,X1,sF927(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(sF924))
| ~ m1_subset_1(X0,sF924)
| ~ r2_hidden(X0,X1)
| ~ v1_tsp_1(X1,sK106)
| v3_struct_0(sK106)
| ~ l1_pre_topc(sK106) )
| ~ spl928_23 ),
inference(forward_demodulation,[],[f48015,f46546]) ).
fof(f48018,definition,
( spl928_179
<=> ! [X0,X1] :
( k1_struct_0(sK106,X0) = k5_subset_1(sF924,X1,sF927(X0))
| ~ v1_tsp_1(X1,sK106)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X0,sF924)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF924)) ) ),
introduced(definition,[new_symbols(definition,[spl928_179])],[avatar_definition]) ).
fof(f48019,plain,
( ! [X0,X1] :
( ~ v1_tsp_1(X1,sK106)
| k1_struct_0(sK106,X0) = k5_subset_1(sF924,X1,sF927(X0))
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X0,sF924)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF924)) )
| ~ spl928_179 ),
inference(avatar_component_clause,[],[f48018]) ).
fof(f48020,plain,
( ~ spl928_18
| spl928_24
| spl928_179
| ~ spl928_23 ),
inference(avatar_split_clause,[],[f48016,f46687,f48018,f46691,f46661]) ).
fof(f48067,plain,
! [X2,X3,X0,X1] :
( k4_xboole_0(X0,k4_xboole_0(X0,k4_tex_4(X1,sK129(X1,X2,X3,X0)))) != k1_struct_0(X2,k8_funct_2(u1_struct_0(X1),u1_struct_0(X2),X3,sK129(X1,X2,X3,X0)))
| u1_struct_0(X2) != X0
| v3_borsuk_1(X3,X1,X2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))
| ~ v5_pre_topc(X3,X1,X2)
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ v2_tsp_2(X2,X1)
| ~ m2_tsp_1(X2,X1)
| v3_struct_0(X1)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| ~ m1_subset_1(k4_tex_4(X1,sK129(X1,X2,X3,X0)),k1_zfmisc_1(u1_struct_0(X1))) ),
inference(superposition,[],[f39850,f45861]) ).
fof(f48074,plain,
! [X2,X3,X0,X1] :
( ~ v2_pre_topc(X1)
| u1_struct_0(X2) != X0
| v3_borsuk_1(X3,X1,X2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))
| ~ v5_pre_topc(X3,X1,X2)
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ v2_tsp_2(X2,X1)
| ~ m2_tsp_1(X2,X1)
| v3_struct_0(X1)
| k4_xboole_0(X0,k4_xboole_0(X0,k4_tex_4(X1,sK129(X1,X2,X3,X0)))) != k1_struct_0(X2,k8_funct_2(u1_struct_0(X1),u1_struct_0(X2),X3,sK129(X1,X2,X3,X0)))
| ~ l1_pre_topc(X1)
| ~ m1_subset_1(k4_tex_4(X1,sK129(X1,X2,X3,X0)),k1_zfmisc_1(u1_struct_0(X1))) ),
inference(duplicate_literal_removal,[],[f48067]) ).
fof(f48075,plain,
( ! [X2,X0,X1] :
( u1_struct_0(X0) != X1
| v3_borsuk_1(X2,sK106,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK106)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK106),u1_struct_0(X0))
| ~ v5_pre_topc(X2,sK106,X0)
| ~ m2_relset_1(X2,u1_struct_0(sK106),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK106)
| ~ m2_tsp_1(X0,sK106)
| v3_struct_0(sK106)
| k4_xboole_0(X1,k4_xboole_0(X1,k4_tex_4(sK106,sK129(sK106,X0,X2,X1)))) != k1_struct_0(X0,k8_funct_2(u1_struct_0(sK106),u1_struct_0(X0),X2,sK129(sK106,X0,X2,X1)))
| ~ l1_pre_topc(sK106)
| ~ m1_subset_1(k4_tex_4(sK106,sK129(sK106,X0,X2,X1)),k1_zfmisc_1(u1_struct_0(sK106))) )
| ~ spl928_23 ),
inference(resolution,[],[f48074,f46688]) ).
fof(f48076,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(sF924))
| u1_struct_0(X0) != X1
| v3_borsuk_1(X2,sK106,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK106),u1_struct_0(X0))
| ~ v5_pre_topc(X2,sK106,X0)
| ~ m2_relset_1(X2,u1_struct_0(sK106),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK106)
| ~ m2_tsp_1(X0,sK106)
| v3_struct_0(sK106)
| k4_xboole_0(X1,k4_xboole_0(X1,k4_tex_4(sK106,sK129(sK106,X0,X2,X1)))) != k1_struct_0(X0,k8_funct_2(u1_struct_0(sK106),u1_struct_0(X0),X2,sK129(sK106,X0,X2,X1)))
| ~ l1_pre_topc(sK106)
| ~ m1_subset_1(k4_tex_4(sK106,sK129(sK106,X0,X2,X1)),k1_zfmisc_1(u1_struct_0(sK106))) )
| ~ spl928_23 ),
inference(forward_demodulation,[],[f48075,f46546]) ).
fof(f48077,plain,
( ! [X2,X0,X1] :
( ~ v1_funct_2(X2,sF924,u1_struct_0(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(sF924))
| u1_struct_0(X0) != X1
| v3_borsuk_1(X2,sK106,X0)
| ~ v1_funct_1(X2)
| ~ v5_pre_topc(X2,sK106,X0)
| ~ m2_relset_1(X2,u1_struct_0(sK106),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK106)
| ~ m2_tsp_1(X0,sK106)
| v3_struct_0(sK106)
| k4_xboole_0(X1,k4_xboole_0(X1,k4_tex_4(sK106,sK129(sK106,X0,X2,X1)))) != k1_struct_0(X0,k8_funct_2(u1_struct_0(sK106),u1_struct_0(X0),X2,sK129(sK106,X0,X2,X1)))
| ~ l1_pre_topc(sK106)
| ~ m1_subset_1(k4_tex_4(sK106,sK129(sK106,X0,X2,X1)),k1_zfmisc_1(u1_struct_0(sK106))) )
| ~ spl928_23 ),
inference(forward_demodulation,[],[f48076,f46546]) ).
fof(f48078,plain,
( ! [X2,X0,X1] :
( ~ m2_relset_1(X2,sF924,u1_struct_0(X0))
| ~ v1_funct_2(X2,sF924,u1_struct_0(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(sF924))
| u1_struct_0(X0) != X1
| v3_borsuk_1(X2,sK106,X0)
| ~ v1_funct_1(X2)
| ~ v5_pre_topc(X2,sK106,X0)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK106)
| ~ m2_tsp_1(X0,sK106)
| v3_struct_0(sK106)
| k4_xboole_0(X1,k4_xboole_0(X1,k4_tex_4(sK106,sK129(sK106,X0,X2,X1)))) != k1_struct_0(X0,k8_funct_2(u1_struct_0(sK106),u1_struct_0(X0),X2,sK129(sK106,X0,X2,X1)))
| ~ l1_pre_topc(sK106)
| ~ m1_subset_1(k4_tex_4(sK106,sK129(sK106,X0,X2,X1)),k1_zfmisc_1(u1_struct_0(sK106))) )
| ~ spl928_23 ),
inference(forward_demodulation,[],[f48077,f46546]) ).
fof(f48079,plain,
( ! [X2,X0,X1] :
( k4_xboole_0(X1,k4_xboole_0(X1,k4_tex_4(sK106,sK129(sK106,X0,X2,X1)))) != k1_struct_0(X0,k8_funct_2(sF924,u1_struct_0(X0),X2,sK129(sK106,X0,X2,X1)))
| ~ m2_relset_1(X2,sF924,u1_struct_0(X0))
| ~ v1_funct_2(X2,sF924,u1_struct_0(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(sF924))
| u1_struct_0(X0) != X1
| v3_borsuk_1(X2,sK106,X0)
| ~ v1_funct_1(X2)
| ~ v5_pre_topc(X2,sK106,X0)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK106)
| ~ m2_tsp_1(X0,sK106)
| v3_struct_0(sK106)
| ~ l1_pre_topc(sK106)
| ~ m1_subset_1(k4_tex_4(sK106,sK129(sK106,X0,X2,X1)),k1_zfmisc_1(u1_struct_0(sK106))) )
| ~ spl928_23 ),
inference(forward_demodulation,[],[f48078,f46546]) ).
fof(f48080,plain,
( ! [X2,X0,X1] :
( k1_struct_0(X0,k8_funct_2(sF924,u1_struct_0(X0),X2,sK129(sK106,X0,X2,X1))) != k4_xboole_0(X1,k4_xboole_0(X1,sF927(sK129(sK106,X0,X2,X1))))
| ~ m2_relset_1(X2,sF924,u1_struct_0(X0))
| ~ v1_funct_2(X2,sF924,u1_struct_0(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(sF924))
| u1_struct_0(X0) != X1
| v3_borsuk_1(X2,sK106,X0)
| ~ v1_funct_1(X2)
| ~ v5_pre_topc(X2,sK106,X0)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK106)
| ~ m2_tsp_1(X0,sK106)
| v3_struct_0(sK106)
| ~ l1_pre_topc(sK106)
| ~ m1_subset_1(k4_tex_4(sK106,sK129(sK106,X0,X2,X1)),k1_zfmisc_1(u1_struct_0(sK106))) )
| ~ spl928_23 ),
inference(forward_demodulation,[],[f48079,f46552]) ).
fof(f48081,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(k4_tex_4(sK106,sK129(sK106,X0,X2,X1)),k1_zfmisc_1(sF924))
| k1_struct_0(X0,k8_funct_2(sF924,u1_struct_0(X0),X2,sK129(sK106,X0,X2,X1))) != k4_xboole_0(X1,k4_xboole_0(X1,sF927(sK129(sK106,X0,X2,X1))))
| ~ m2_relset_1(X2,sF924,u1_struct_0(X0))
| ~ v1_funct_2(X2,sF924,u1_struct_0(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(sF924))
| u1_struct_0(X0) != X1
| v3_borsuk_1(X2,sK106,X0)
| ~ v1_funct_1(X2)
| ~ v5_pre_topc(X2,sK106,X0)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK106)
| ~ m2_tsp_1(X0,sK106)
| v3_struct_0(sK106)
| ~ l1_pre_topc(sK106) )
| ~ spl928_23 ),
inference(forward_demodulation,[],[f48080,f46546]) ).
fof(f48082,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(sF927(sK129(sK106,X0,X2,X1)),k1_zfmisc_1(sF924))
| k1_struct_0(X0,k8_funct_2(sF924,u1_struct_0(X0),X2,sK129(sK106,X0,X2,X1))) != k4_xboole_0(X1,k4_xboole_0(X1,sF927(sK129(sK106,X0,X2,X1))))
| ~ m2_relset_1(X2,sF924,u1_struct_0(X0))
| ~ v1_funct_2(X2,sF924,u1_struct_0(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(sF924))
| u1_struct_0(X0) != X1
| v3_borsuk_1(X2,sK106,X0)
| ~ v1_funct_1(X2)
| ~ v5_pre_topc(X2,sK106,X0)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK106)
| ~ m2_tsp_1(X0,sK106)
| v3_struct_0(sK106)
| ~ l1_pre_topc(sK106) )
| ~ spl928_23 ),
inference(forward_demodulation,[],[f48081,f46552]) ).
fof(f48084,definition,
( spl928_185
<=> ! [X2,X0,X1] :
( ~ m1_subset_1(sF927(sK129(sK106,X0,X2,X1)),k1_zfmisc_1(sF924))
| ~ m2_tsp_1(X0,sK106)
| ~ v2_tsp_2(X0,sK106)
| v3_struct_0(X0)
| ~ v5_pre_topc(X2,sK106,X0)
| ~ v1_funct_1(X2)
| v3_borsuk_1(X2,sK106,X0)
| u1_struct_0(X0) != X1
| ~ m1_subset_1(X1,k1_zfmisc_1(sF924))
| ~ v1_funct_2(X2,sF924,u1_struct_0(X0))
| ~ m2_relset_1(X2,sF924,u1_struct_0(X0))
| k1_struct_0(X0,k8_funct_2(sF924,u1_struct_0(X0),X2,sK129(sK106,X0,X2,X1))) != k4_xboole_0(X1,k4_xboole_0(X1,sF927(sK129(sK106,X0,X2,X1)))) ) ),
introduced(definition,[new_symbols(definition,[spl928_185])],[avatar_definition]) ).
fof(f48085,plain,
( ! [X2,X0,X1] :
( ~ v2_tsp_2(X0,sK106)
| ~ m2_tsp_1(X0,sK106)
| ~ m1_subset_1(sF927(sK129(sK106,X0,X2,X1)),k1_zfmisc_1(sF924))
| v3_struct_0(X0)
| ~ v5_pre_topc(X2,sK106,X0)
| ~ v1_funct_1(X2)
| v3_borsuk_1(X2,sK106,X0)
| u1_struct_0(X0) != X1
| ~ m1_subset_1(X1,k1_zfmisc_1(sF924))
| ~ v1_funct_2(X2,sF924,u1_struct_0(X0))
| ~ m2_relset_1(X2,sF924,u1_struct_0(X0))
| k1_struct_0(X0,k8_funct_2(sF924,u1_struct_0(X0),X2,sK129(sK106,X0,X2,X1))) != k4_xboole_0(X1,k4_xboole_0(X1,sF927(sK129(sK106,X0,X2,X1)))) )
| ~ spl928_185 ),
inference(avatar_component_clause,[],[f48084]) ).
fof(f48086,plain,
( ~ spl928_18
| spl928_24
| spl928_185
| ~ spl928_23 ),
inference(avatar_split_clause,[],[f48082,f46687,f48084,f46691,f46661]) ).
fof(f48087,plain,
( ! [X0,X1] :
( ~ m2_tsp_1(sK107,sK106)
| ~ m1_subset_1(sF927(sK129(sK106,sK107,X0,X1)),k1_zfmisc_1(sF924))
| v3_struct_0(sK107)
| ~ v5_pre_topc(X0,sK106,sK107)
| ~ v1_funct_1(X0)
| v3_borsuk_1(X0,sK106,sK107)
| u1_struct_0(sK107) != X1
| ~ m1_subset_1(X1,k1_zfmisc_1(sF924))
| ~ v1_funct_2(X0,sF924,u1_struct_0(sK107))
| ~ m2_relset_1(X0,sF924,u1_struct_0(sK107))
| k1_struct_0(sK107,k8_funct_2(sF924,u1_struct_0(sK107),X0,sK129(sK106,sK107,X0,X1))) != k4_xboole_0(X1,k4_xboole_0(X1,sF927(sK129(sK106,sK107,X0,X1)))) )
| ~ spl928_49
| ~ spl928_185 ),
inference(resolution,[],[f48085,f46825]) ).
fof(f48088,plain,
( ! [X0,X1] :
( sF925 != X1
| ~ m2_tsp_1(sK107,sK106)
| ~ m1_subset_1(sF927(sK129(sK106,sK107,X0,X1)),k1_zfmisc_1(sF924))
| v3_struct_0(sK107)
| ~ v5_pre_topc(X0,sK106,sK107)
| ~ v1_funct_1(X0)
| v3_borsuk_1(X0,sK106,sK107)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF924))
| ~ v1_funct_2(X0,sF924,u1_struct_0(sK107))
| ~ m2_relset_1(X0,sF924,u1_struct_0(sK107))
| k1_struct_0(sK107,k8_funct_2(sF924,u1_struct_0(sK107),X0,sK129(sK106,sK107,X0,X1))) != k4_xboole_0(X1,k4_xboole_0(X1,sF927(sK129(sK106,sK107,X0,X1)))) )
| ~ spl928_49
| ~ spl928_185 ),
inference(forward_demodulation,[],[f48087,f46548]) ).
fof(f48089,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X0,sF924,sF925)
| sF925 != X1
| ~ m2_tsp_1(sK107,sK106)
| ~ m1_subset_1(sF927(sK129(sK106,sK107,X0,X1)),k1_zfmisc_1(sF924))
| v3_struct_0(sK107)
| ~ v5_pre_topc(X0,sK106,sK107)
| ~ v1_funct_1(X0)
| v3_borsuk_1(X0,sK106,sK107)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF924))
| ~ m2_relset_1(X0,sF924,u1_struct_0(sK107))
| k1_struct_0(sK107,k8_funct_2(sF924,u1_struct_0(sK107),X0,sK129(sK106,sK107,X0,X1))) != k4_xboole_0(X1,k4_xboole_0(X1,sF927(sK129(sK106,sK107,X0,X1)))) )
| ~ spl928_49
| ~ spl928_185 ),
inference(forward_demodulation,[],[f48088,f46548]) ).
fof(f48090,plain,
( ! [X0,X1] :
( ~ m2_relset_1(X0,sF924,sF925)
| ~ v1_funct_2(X0,sF924,sF925)
| sF925 != X1
| ~ m2_tsp_1(sK107,sK106)
| ~ m1_subset_1(sF927(sK129(sK106,sK107,X0,X1)),k1_zfmisc_1(sF924))
| v3_struct_0(sK107)
| ~ v5_pre_topc(X0,sK106,sK107)
| ~ v1_funct_1(X0)
| v3_borsuk_1(X0,sK106,sK107)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF924))
| k1_struct_0(sK107,k8_funct_2(sF924,u1_struct_0(sK107),X0,sK129(sK106,sK107,X0,X1))) != k4_xboole_0(X1,k4_xboole_0(X1,sF927(sK129(sK106,sK107,X0,X1)))) )
| ~ spl928_49
| ~ spl928_185 ),
inference(forward_demodulation,[],[f48089,f46548]) ).
fof(f48091,plain,
( ! [X0,X1] :
( k1_struct_0(sK107,k8_funct_2(sF924,sF925,X0,sK129(sK106,sK107,X0,X1))) != k4_xboole_0(X1,k4_xboole_0(X1,sF927(sK129(sK106,sK107,X0,X1))))
| ~ m2_relset_1(X0,sF924,sF925)
| ~ v1_funct_2(X0,sF924,sF925)
| sF925 != X1
| ~ m2_tsp_1(sK107,sK106)
| ~ m1_subset_1(sF927(sK129(sK106,sK107,X0,X1)),k1_zfmisc_1(sF924))
| v3_struct_0(sK107)
| ~ v5_pre_topc(X0,sK106,sK107)
| ~ v1_funct_1(X0)
| v3_borsuk_1(X0,sK106,sK107)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF924)) )
| ~ spl928_49
| ~ spl928_185 ),
inference(forward_demodulation,[],[f48090,f46548]) ).
fof(f48093,definition,
( spl928_186
<=> ! [X0,X1] :
( k1_struct_0(sK107,k8_funct_2(sF924,sF925,X0,sK129(sK106,sK107,X0,X1))) != k4_xboole_0(X1,k4_xboole_0(X1,sF927(sK129(sK106,sK107,X0,X1))))
| ~ m1_subset_1(X1,k1_zfmisc_1(sF924))
| v3_borsuk_1(X0,sK106,sK107)
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK106,sK107)
| ~ m1_subset_1(sF927(sK129(sK106,sK107,X0,X1)),k1_zfmisc_1(sF924))
| sF925 != X1
| ~ v1_funct_2(X0,sF924,sF925)
| ~ m2_relset_1(X0,sF924,sF925) ) ),
introduced(definition,[new_symbols(definition,[spl928_186])],[avatar_definition]) ).
fof(f48094,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X0,sF924,sF925)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF924))
| v3_borsuk_1(X0,sK106,sK107)
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK106,sK107)
| ~ m1_subset_1(sF927(sK129(sK106,sK107,X0,X1)),k1_zfmisc_1(sF924))
| sF925 != X1
| k1_struct_0(sK107,k8_funct_2(sF924,sF925,X0,sK129(sK106,sK107,X0,X1))) != k4_xboole_0(X1,k4_xboole_0(X1,sF927(sK129(sK106,sK107,X0,X1))))
| ~ m2_relset_1(X0,sF924,sF925) )
| ~ spl928_186 ),
inference(avatar_component_clause,[],[f48093]) ).
fof(f48095,plain,
( spl928_21
| ~ spl928_50
| spl928_186
| ~ spl928_49
| ~ spl928_185 ),
inference(avatar_split_clause,[],[f48091,f48084,f46824,f48093,f46828,f46678]) ).
fof(f48096,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF924))
| v3_borsuk_1(sK108,sK106,sK107)
| ~ v1_funct_1(sK108)
| ~ v5_pre_topc(sK108,sK106,sK107)
| ~ m1_subset_1(sF927(sK129(sK106,sK107,sK108,X0)),k1_zfmisc_1(sF924))
| sF925 != X0
| k1_struct_0(sK107,k8_funct_2(sF924,sF925,sK108,sK129(sK106,sK107,sK108,X0))) != k4_xboole_0(X0,k4_xboole_0(X0,sF927(sK129(sK106,sK107,sK108,X0))))
| ~ m2_relset_1(sK108,sF924,sF925) )
| ~ spl928_27
| ~ spl928_186 ),
inference(resolution,[],[f48094,f46708]) ).
fof(f48097,plain,
( ! [X0] :
( k1_struct_0(sK107,sF926(sK129(sK106,sK107,sK108,X0))) != k4_xboole_0(X0,k4_xboole_0(X0,sF927(sK129(sK106,sK107,sK108,X0))))
| ~ m1_subset_1(X0,k1_zfmisc_1(sF924))
| v3_borsuk_1(sK108,sK106,sK107)
| ~ v1_funct_1(sK108)
| ~ v5_pre_topc(sK108,sK106,sK107)
| ~ m1_subset_1(sF927(sK129(sK106,sK107,sK108,X0)),k1_zfmisc_1(sF924))
| sF925 != X0
| ~ m2_relset_1(sK108,sF924,sF925) )
| ~ spl928_27
| ~ spl928_186 ),
inference(forward_demodulation,[],[f48096,f46550]) ).
fof(f48099,definition,
( spl928_187
<=> ! [X0] :
( k1_struct_0(sK107,sF926(sK129(sK106,sK107,sK108,X0))) != k4_xboole_0(X0,k4_xboole_0(X0,sF927(sK129(sK106,sK107,sK108,X0))))
| sF925 != X0
| ~ m1_subset_1(sF927(sK129(sK106,sK107,sK108,X0)),k1_zfmisc_1(sF924))
| ~ m1_subset_1(X0,k1_zfmisc_1(sF924)) ) ),
introduced(definition,[new_symbols(definition,[spl928_187])],[avatar_definition]) ).
fof(f48100,plain,
( ! [X0] :
( sF925 != X0
| k1_struct_0(sK107,sF926(sK129(sK106,sK107,sK108,X0))) != k4_xboole_0(X0,k4_xboole_0(X0,sF927(sK129(sK106,sK107,sK108,X0))))
| ~ m1_subset_1(sF927(sK129(sK106,sK107,sK108,X0)),k1_zfmisc_1(sF924))
| ~ m1_subset_1(X0,k1_zfmisc_1(sF924)) )
| ~ spl928_187 ),
inference(avatar_component_clause,[],[f48099]) ).
fof(f48101,plain,
( ~ spl928_84
| ~ spl928_85
| ~ spl928_28
| spl928_86
| spl928_187
| ~ spl928_27
| ~ spl928_186 ),
inference(avatar_split_clause,[],[f48097,f48093,f46707,f48099,f47104,f46711,f47100,f47096]) ).
fof(f48102,plain,
( k1_struct_0(sK107,sF926(sK129(sK106,sK107,sK108,sF925))) != k4_xboole_0(sF925,k4_xboole_0(sF925,sF927(sK129(sK106,sK107,sK108,sF925))))
| ~ m1_subset_1(sF927(sK129(sK106,sK107,sK108,sF925)),k1_zfmisc_1(sF924))
| ~ m1_subset_1(sF925,k1_zfmisc_1(sF924))
| ~ spl928_187 ),
inference(equality_resolution,[],[f48100]) ).
fof(f48104,definition,
( spl928_188
<=> m1_subset_1(sF927(sK129(sK106,sK107,sK108,sF925)),k1_zfmisc_1(sF924)) ),
introduced(definition,[new_symbols(definition,[spl928_188])],[avatar_definition]) ).
fof(f48106,plain,
( ~ m1_subset_1(sF927(sK129(sK106,sK107,sK108,sF925)),k1_zfmisc_1(sF924))
| spl928_188 ),
inference(avatar_component_clause,[],[f48104]) ).
fof(f48108,definition,
( spl928_189
<=> k1_struct_0(sK107,sF926(sK129(sK106,sK107,sK108,sF925))) = k4_xboole_0(sF925,k4_xboole_0(sF925,sF927(sK129(sK106,sK107,sK108,sF925)))) ),
introduced(definition,[new_symbols(definition,[spl928_189])],[avatar_definition]) ).
fof(f48110,plain,
( k1_struct_0(sK107,sF926(sK129(sK106,sK107,sK108,sF925))) != k4_xboole_0(sF925,k4_xboole_0(sF925,sF927(sK129(sK106,sK107,sK108,sF925))))
| spl928_189 ),
inference(avatar_component_clause,[],[f48108]) ).
fof(f48111,plain,
( ~ spl928_48
| ~ spl928_188
| ~ spl928_189
| ~ spl928_187 ),
inference(avatar_split_clause,[],[f48102,f48099,f48108,f48104,f46820]) ).
fof(f48112,plain,
( ~ m1_subset_1(sK129(sK106,sK107,sK108,sF925),sF924)
| ~ spl928_25
| spl928_188 ),
inference(resolution,[],[f48106,f46696]) ).
fof(f48115,plain,
( v3_borsuk_1(sK108,sK106,sK107)
| ~ v1_funct_1(sK108)
| ~ v1_funct_2(sK108,sF924,sF925)
| ~ v5_pre_topc(sK108,sK106,sK107)
| ~ m2_relset_1(sK108,sF924,sF925)
| ~ spl928_25
| ~ spl928_51
| spl928_188 ),
inference(resolution,[],[f48112,f46833]) ).
fof(f48118,plain,
( ~ spl928_84
| ~ spl928_85
| ~ spl928_27
| ~ spl928_28
| spl928_86
| ~ spl928_25
| ~ spl928_51
| spl928_188 ),
inference(avatar_split_clause,[],[f48115,f48104,f46832,f46695,f47104,f46711,f46707,f47100,f47096]) ).
fof(f48122,plain,
( ! [X0] :
( k1_struct_0(sK107,sF926(sK129(sK106,sK107,sK108,sF925))) != k5_subset_1(X0,sF925,sF927(sK129(sK106,sK107,sK108,sF925)))
| ~ m1_subset_1(sF925,k1_zfmisc_1(X0))
| ~ m1_subset_1(sF927(sK129(sK106,sK107,sK108,sF925)),k1_zfmisc_1(X0)) )
| spl928_189 ),
inference(superposition,[],[f48110,f45861]) ).
fof(f48220,plain,
( ~ m2_tsp_1(sK107,sK106)
| ~ l1_pre_topc(sK106)
| spl928_128 ),
inference(resolution,[],[f47427,f39900]) ).
fof(f48221,plain,
( ~ spl928_18
| ~ spl928_50
| spl928_128 ),
inference(avatar_split_clause,[],[f48220,f47425,f46828,f46661]) ).
fof(f49056,definition,
( spl928_276
<=> m1_subset_1(sK129(sK106,sK107,sK108,sF925),sF924) ),
introduced(definition,[new_symbols(definition,[spl928_276])],[avatar_definition]) ).
fof(f49058,plain,
( ~ m1_subset_1(sK129(sK106,sK107,sK108,sF925),sF924)
| spl928_276 ),
inference(avatar_component_clause,[],[f49056]) ).
fof(f49063,plain,
( v3_borsuk_1(sK108,sK106,sK107)
| ~ v1_funct_1(sK108)
| ~ v1_funct_2(sK108,sF924,sF925)
| ~ v5_pre_topc(sK108,sK106,sK107)
| ~ m2_relset_1(sK108,sF924,sF925)
| ~ spl928_51
| spl928_276 ),
inference(resolution,[],[f49058,f46833]) ).
fof(f49066,plain,
( ~ spl928_84
| ~ spl928_85
| ~ spl928_27
| ~ spl928_28
| spl928_86
| ~ spl928_51
| spl928_276 ),
inference(avatar_split_clause,[],[f49063,f49056,f46832,f47104,f46711,f46707,f47100,f47096]) ).
fof(f49186,plain,
( ! [X0] :
( ~ v1_tsp_2(X0,sK106)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK106)))
| v3_struct_0(sK106)
| v1_tsp_1(X0,sK106)
| ~ l1_pre_topc(sK106) )
| ~ spl928_23 ),
inference(resolution,[],[f41474,f46688]) ).
fof(f49189,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF924))
| ~ v1_tsp_2(X0,sK106)
| v3_struct_0(sK106)
| v1_tsp_1(X0,sK106)
| ~ l1_pre_topc(sK106) )
| ~ spl928_23 ),
inference(forward_demodulation,[],[f49186,f46546]) ).
fof(f49195,definition,
( spl928_290
<=> ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF924))
| v1_tsp_1(X0,sK106)
| ~ v1_tsp_2(X0,sK106) ) ),
introduced(definition,[new_symbols(definition,[spl928_290])],[avatar_definition]) ).
fof(f49196,plain,
( ! [X0] :
( v1_tsp_1(X0,sK106)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF924))
| ~ v1_tsp_2(X0,sK106) )
| ~ spl928_290 ),
inference(avatar_component_clause,[],[f49195]) ).
fof(f49197,plain,
( ~ spl928_18
| spl928_24
| spl928_290
| ~ spl928_23 ),
inference(avatar_split_clause,[],[f49189,f46687,f49195,f46691,f46661]) ).
fof(f49200,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF924))
| ~ v1_tsp_2(X0,sK106)
| k1_struct_0(sK106,X1) = k5_subset_1(sF924,X0,sF927(X1))
| ~ r2_hidden(X1,X0)
| ~ m1_subset_1(X1,sF924)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF924)) )
| ~ spl928_179
| ~ spl928_290 ),
inference(resolution,[],[f49196,f48019]) ).
fof(f49201,plain,
( ! [X0,X1] :
( ~ v1_tsp_2(X0,sK106)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF924))
| k1_struct_0(sK106,X1) = k5_subset_1(sF924,X0,sF927(X1))
| ~ r2_hidden(X1,X0)
| ~ m1_subset_1(X1,sF924) )
| ~ spl928_179
| ~ spl928_290 ),
inference(duplicate_literal_removal,[],[f49200]) ).
fof(f49318,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK107))
| r2_hidden(X0,k2_pre_topc(sK107))
| ~ l1_struct_0(sK107) )
| spl928_21 ),
inference(resolution,[],[f43168,f46679]) ).
fof(f49319,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF925)
| r2_hidden(X0,k2_pre_topc(sK107))
| ~ l1_struct_0(sK107) )
| spl928_21 ),
inference(forward_demodulation,[],[f49318,f46548]) ).
fof(f49322,definition,
( spl928_308
<=> ! [X0] :
( ~ m1_subset_1(X0,sF925)
| r2_hidden(X0,k2_pre_topc(sK107)) ) ),
introduced(definition,[new_symbols(definition,[spl928_308])],[avatar_definition]) ).
fof(f49323,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF925)
| r2_hidden(X0,k2_pre_topc(sK107)) )
| ~ spl928_308 ),
inference(avatar_component_clause,[],[f49322]) ).
fof(f49324,plain,
( ~ spl928_74
| spl928_308
| spl928_21 ),
inference(avatar_split_clause,[],[f49319,f46678,f49322,f47003]) ).
fof(f49425,plain,
( ! [X0] :
( ~ v1_tsp_2(X0,sK107)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK107)))
| v3_struct_0(sK107)
| u1_struct_0(sK107) = k3_tex_4(sK107,X0)
| ~ l1_pre_topc(sK107) )
| ~ spl928_20 ),
inference(resolution,[],[f41473,f46675]) ).
fof(f49426,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF925))
| ~ v1_tsp_2(X0,sK107)
| v3_struct_0(sK107)
| u1_struct_0(sK107) = k3_tex_4(sK107,X0)
| ~ l1_pre_topc(sK107) )
| ~ spl928_20 ),
inference(forward_demodulation,[],[f49425,f46548]) ).
fof(f49428,plain,
( ! [X0] :
( sF925 = k3_tex_4(sK107,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF925))
| ~ v1_tsp_2(X0,sK107)
| v3_struct_0(sK107)
| ~ l1_pre_topc(sK107) )
| ~ spl928_20 ),
inference(forward_demodulation,[],[f49426,f46548]) ).
fof(f49431,definition,
( spl928_316
<=> ! [X0] :
( sF925 = k3_tex_4(sK107,X0)
| ~ v1_tsp_2(X0,sK107)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF925)) ) ),
introduced(definition,[new_symbols(definition,[spl928_316])],[avatar_definition]) ).
fof(f49432,plain,
( ! [X0] :
( ~ v1_tsp_2(X0,sK107)
| sF925 = k3_tex_4(sK107,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF925)) )
| ~ spl928_316 ),
inference(avatar_component_clause,[],[f49431]) ).
fof(f49433,plain,
( ~ spl928_19
| spl928_21
| spl928_316
| ~ spl928_20 ),
inference(avatar_split_clause,[],[f49428,f46674,f49431,f46678,f46665]) ).
fof(f49667,plain,
( m1_subset_1(k2_pre_topc(sK107),k1_zfmisc_1(u1_struct_0(sK107)))
| ~ spl928_74 ),
inference(resolution,[],[f43147,f47004]) ).
fof(f49668,plain,
( m1_subset_1(k2_pre_topc(sK107),k1_zfmisc_1(sF925))
| ~ spl928_74 ),
inference(forward_demodulation,[],[f49667,f46548]) ).
fof(f49894,plain,
( ! [X0] :
( ~ m1_subset_1(sF925,k1_zfmisc_1(sF924))
| k1_struct_0(sK106,X0) = k5_subset_1(sF924,sF925,sF927(X0))
| ~ r2_hidden(X0,sF925)
| ~ m1_subset_1(X0,sF924)
| ~ v2_tsp_2(sK107,sK106)
| ~ m2_tsp_1(sK107,sK106)
| v3_struct_0(sK106)
| ~ l1_pre_topc(sK106) )
| ~ spl928_179
| ~ spl928_290 ),
inference(resolution,[],[f49201,f46984]) ).
fof(f49902,definition,
( spl928_349
<=> ! [X0] :
( k1_struct_0(sK106,X0) = k5_subset_1(sF924,sF925,sF927(X0))
| ~ m1_subset_1(X0,sF924)
| ~ r2_hidden(X0,sF925) ) ),
introduced(definition,[new_symbols(definition,[spl928_349])],[avatar_definition]) ).
fof(f49903,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF925)
| ~ m1_subset_1(X0,sF924)
| k1_struct_0(sK106,X0) = k5_subset_1(sF924,sF925,sF927(X0)) )
| ~ spl928_349 ),
inference(avatar_component_clause,[],[f49902]) ).
fof(f49904,plain,
( ~ spl928_18
| spl928_24
| ~ spl928_50
| ~ spl928_49
| spl928_349
| ~ spl928_48
| ~ spl928_179
| ~ spl928_290 ),
inference(avatar_split_clause,[],[f49894,f49195,f48018,f46820,f49902,f46824,f46828,f46691,f46661]) ).
fof(f50584,plain,
( m1_pre_topc(sK107,sK107)
| ~ spl928_19 ),
inference(resolution,[],[f40657,f46667]) ).
fof(f51707,plain,
( v3_pre_topc(k2_pre_topc(sK107),sK107)
| ~ l1_pre_topc(sK107)
| ~ spl928_20 ),
inference(resolution,[],[f43142,f46675]) ).
fof(f51709,definition,
( spl928_554
<=> v3_pre_topc(k2_pre_topc(sK107),sK107) ),
introduced(definition,[new_symbols(definition,[spl928_554])],[avatar_definition]) ).
fof(f51711,plain,
( v3_pre_topc(k2_pre_topc(sK107),sK107)
| ~ spl928_554 ),
inference(avatar_component_clause,[],[f51709]) ).
fof(f51712,plain,
( ~ spl928_19
| spl928_554
| ~ spl928_20 ),
inference(avatar_split_clause,[],[f51707,f46674,f51709,f46665]) ).
fof(f51722,plain,
( k2_pre_topc(sK107) = k3_tex_4(sK107,k2_pre_topc(sK107))
| ~ m1_subset_1(k2_pre_topc(sK107),k1_zfmisc_1(u1_struct_0(sK107)))
| v3_struct_0(sK107)
| ~ v2_pre_topc(sK107)
| ~ l1_pre_topc(sK107)
| ~ spl928_554 ),
inference(resolution,[],[f51711,f41182]) ).
fof(f51729,plain,
( v3_pre_topc(u1_struct_0(sK107),sK107)
| ~ l1_struct_0(sK107)
| ~ spl928_554 ),
inference(superposition,[],[f51711,f43169]) ).
fof(f51730,plain,
( v3_pre_topc(sF925,sK107)
| ~ l1_struct_0(sK107)
| ~ spl928_554 ),
inference(forward_demodulation,[],[f51729,f46548]) ).
fof(f51733,plain,
( ~ m1_subset_1(k2_pre_topc(sK107),k1_zfmisc_1(sF925))
| k2_pre_topc(sK107) = k3_tex_4(sK107,k2_pre_topc(sK107))
| v3_struct_0(sK107)
| ~ v2_pre_topc(sK107)
| ~ l1_pre_topc(sK107)
| ~ spl928_554 ),
inference(forward_demodulation,[],[f51722,f46548]) ).
fof(f51737,definition,
( spl928_556
<=> v3_pre_topc(sF925,sK107) ),
introduced(definition,[new_symbols(definition,[spl928_556])],[avatar_definition]) ).
fof(f51739,plain,
( v3_pre_topc(sF925,sK107)
| ~ spl928_556 ),
inference(avatar_component_clause,[],[f51737]) ).
fof(f51740,plain,
( ~ spl928_74
| spl928_556
| ~ spl928_554 ),
inference(avatar_split_clause,[],[f51730,f51709,f51737,f47003]) ).
fof(f51745,definition,
( spl928_558
<=> k2_pre_topc(sK107) = k3_tex_4(sK107,k2_pre_topc(sK107)) ),
introduced(definition,[new_symbols(definition,[spl928_558])],[avatar_definition]) ).
fof(f51747,plain,
( k2_pre_topc(sK107) = k3_tex_4(sK107,k2_pre_topc(sK107))
| ~ spl928_558 ),
inference(avatar_component_clause,[],[f51745]) ).
fof(f51749,definition,
( spl928_559
<=> m1_subset_1(k2_pre_topc(sK107),k1_zfmisc_1(sF925)) ),
introduced(definition,[new_symbols(definition,[spl928_559])],[avatar_definition]) ).
fof(f51757,plain,
( ~ spl928_19
| ~ spl928_20
| spl928_21
| spl928_558
| ~ spl928_559
| ~ spl928_554 ),
inference(avatar_split_clause,[],[f51733,f51709,f51749,f51745,f46678,f46674,f46665]) ).
fof(f51770,plain,
( sF925 = k3_tex_4(sK107,sF925)
| ~ m1_subset_1(sF925,k1_zfmisc_1(u1_struct_0(sK107)))
| v3_struct_0(sK107)
| ~ v2_pre_topc(sK107)
| ~ l1_pre_topc(sK107)
| ~ spl928_556 ),
inference(resolution,[],[f51739,f41182]) ).
fof(f51775,plain,
( ~ m1_subset_1(sF925,k1_zfmisc_1(sF925))
| sF925 = k3_tex_4(sK107,sF925)
| v3_struct_0(sK107)
| ~ v2_pre_topc(sK107)
| ~ l1_pre_topc(sK107)
| ~ spl928_556 ),
inference(forward_demodulation,[],[f51770,f46548]) ).
fof(f51779,definition,
( spl928_563
<=> sF925 = k3_tex_4(sK107,sF925) ),
introduced(definition,[new_symbols(definition,[spl928_563])],[avatar_definition]) ).
fof(f51781,plain,
( sF925 = k3_tex_4(sK107,sF925)
| ~ spl928_563 ),
inference(avatar_component_clause,[],[f51779]) ).
fof(f51787,plain,
( ~ spl928_19
| ~ spl928_20
| spl928_21
| spl928_563
| ~ spl928_52
| ~ spl928_556 ),
inference(avatar_split_clause,[],[f51775,f51737,f46836,f51779,f46678,f46674,f46665]) ).
fof(f51799,plain,
( u1_struct_0(sK107) != sF925
| ~ v1_tsp_1(sF925,sK107)
| v1_tsp_2(sF925,sK107)
| ~ m1_subset_1(sF925,k1_zfmisc_1(u1_struct_0(sK107)))
| v3_struct_0(sK107)
| ~ v2_pre_topc(sK107)
| ~ l1_pre_topc(sK107)
| ~ spl928_563 ),
inference(superposition,[],[f41475,f51781]) ).
fof(f51801,plain,
( sF925 != sF925
| ~ v1_tsp_1(sF925,sK107)
| v1_tsp_2(sF925,sK107)
| ~ m1_subset_1(sF925,k1_zfmisc_1(u1_struct_0(sK107)))
| v3_struct_0(sK107)
| ~ v2_pre_topc(sK107)
| ~ l1_pre_topc(sK107)
| ~ spl928_563 ),
inference(forward_demodulation,[],[f51799,f46548]) ).
fof(f51802,plain,
( ~ v1_tsp_1(sF925,sK107)
| v1_tsp_2(sF925,sK107)
| ~ m1_subset_1(sF925,k1_zfmisc_1(u1_struct_0(sK107)))
| v3_struct_0(sK107)
| ~ v2_pre_topc(sK107)
| ~ l1_pre_topc(sK107)
| ~ spl928_563 ),
inference(trivial_inequality_removal,[],[f51801]) ).
fof(f51803,plain,
( ~ m1_subset_1(sF925,k1_zfmisc_1(sF925))
| ~ v1_tsp_1(sF925,sK107)
| v1_tsp_2(sF925,sK107)
| v3_struct_0(sK107)
| ~ v2_pre_topc(sK107)
| ~ l1_pre_topc(sK107)
| ~ spl928_563 ),
inference(forward_demodulation,[],[f51802,f46548]) ).
fof(f51805,definition,
( spl928_567
<=> v1_tsp_2(sF925,sK107) ),
introduced(definition,[new_symbols(definition,[spl928_567])],[avatar_definition]) ).
fof(f51809,definition,
( spl928_568
<=> v1_tsp_1(sF925,sK107) ),
introduced(definition,[new_symbols(definition,[spl928_568])],[avatar_definition]) ).
fof(f51811,plain,
( ~ v1_tsp_1(sF925,sK107)
| spl928_568 ),
inference(avatar_component_clause,[],[f51809]) ).
fof(f51812,plain,
( ~ spl928_19
| ~ spl928_20
| spl928_21
| spl928_567
| ~ spl928_568
| ~ spl928_52
| ~ spl928_563 ),
inference(avatar_split_clause,[],[f51803,f51779,f46836,f51809,f51805,f46678,f46674,f46665]) ).
fof(f51818,definition,
( spl928_569
<=> ! [X0] :
( ~ v2_t_0topsp(X0)
| ~ m2_tsp_1(X0,sK107)
| v3_struct_0(X0)
| u1_struct_0(X0) != sF925 ) ),
introduced(definition,[new_symbols(definition,[spl928_569])],[avatar_definition]) ).
fof(f51819,plain,
( ! [X0] :
( ~ m2_tsp_1(X0,sK107)
| ~ v2_t_0topsp(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) != sF925 )
| ~ spl928_569 ),
inference(avatar_component_clause,[],[f51818]) ).
fof(f51828,plain,
( ! [X0] :
( ~ v2_t_0topsp(X0)
| u1_struct_0(X0) != sF925
| ~ m1_subset_1(sF925,k1_zfmisc_1(u1_struct_0(sK107)))
| v3_struct_0(X0)
| ~ m2_tsp_1(X0,sK107)
| v3_struct_0(sK107)
| ~ l1_pre_topc(sK107) )
| spl928_568 ),
inference(resolution,[],[f51811,f39920]) ).
fof(f51829,plain,
( ! [X0] :
( ~ m1_subset_1(sF925,k1_zfmisc_1(sF925))
| ~ v2_t_0topsp(X0)
| u1_struct_0(X0) != sF925
| v3_struct_0(X0)
| ~ m2_tsp_1(X0,sK107)
| v3_struct_0(sK107)
| ~ l1_pre_topc(sK107) )
| spl928_568 ),
inference(forward_demodulation,[],[f51828,f46548]) ).
fof(f51831,plain,
( ~ spl928_19
| spl928_21
| spl928_569
| ~ spl928_52
| spl928_568 ),
inference(avatar_split_clause,[],[f51829,f51809,f46836,f51818,f46678,f46665]) ).
fof(f51906,plain,
( spl928_559
| ~ spl928_74 ),
inference(avatar_split_clause,[],[f49668,f47003,f51749]) ).
fof(f51925,definition,
( spl928_578
<=> v1_tsp_2(k2_pre_topc(sK107),sK107) ),
introduced(definition,[new_symbols(definition,[spl928_578])],[avatar_definition]) ).
fof(f51926,plain,
( ~ v1_tsp_2(k2_pre_topc(sK107),sK107)
| spl928_578 ),
inference(avatar_component_clause,[],[f51925]) ).
fof(f51927,plain,
( v1_tsp_2(k2_pre_topc(sK107),sK107)
| ~ spl928_578 ),
inference(avatar_component_clause,[],[f51925]) ).
fof(f51933,definition,
( spl928_580
<=> sF925 = k2_pre_topc(sK107) ),
introduced(definition,[new_symbols(definition,[spl928_580])],[avatar_definition]) ).
fof(f51934,plain,
( sF925 = k2_pre_topc(sK107)
| ~ spl928_580 ),
inference(avatar_component_clause,[],[f51933]) ).
fof(f51955,plain,
( ~ v1_tsp_2(u1_struct_0(sK107),sK107)
| ~ l1_struct_0(sK107)
| spl928_578 ),
inference(superposition,[],[f51926,f43169]) ).
fof(f51956,plain,
( ~ v1_tsp_2(sF925,sK107)
| ~ l1_struct_0(sK107)
| spl928_578 ),
inference(forward_demodulation,[],[f51955,f46548]) ).
fof(f52051,definition,
( spl928_592
<=> m1_subset_1(sF926(sK129(sK106,sK107,sK108,sF925)),sF924) ),
introduced(definition,[new_symbols(definition,[spl928_592])],[avatar_definition]) ).
fof(f52052,plain,
( m1_subset_1(sF926(sK129(sK106,sK107,sK108,sF925)),sF924)
| ~ spl928_592 ),
inference(avatar_component_clause,[],[f52051]) ).
fof(f52053,plain,
( ~ m1_subset_1(sF926(sK129(sK106,sK107,sK108,sF925)),sF924)
| spl928_592 ),
inference(avatar_component_clause,[],[f52051]) ).
fof(f52100,plain,
( ~ m1_subset_1(sF927(sK129(sK106,sK107,sK108,sF925)),k1_zfmisc_1(sF924))
| ~ m1_subset_1(sK129(sK106,sK107,sK108,sF925),sF924)
| spl928_592 ),
inference(resolution,[],[f52053,f47626]) ).
fof(f52103,plain,
( ~ spl928_276
| ~ spl928_188
| spl928_592 ),
inference(avatar_split_clause,[],[f52100,f52051,f48104,f49056]) ).
fof(f52112,plain,
( k1_struct_0(sK106,sF926(sK129(sK106,sK107,sK108,sF925))) = k2_tarski(sF926(sK129(sK106,sK107,sK108,sF925)),sF926(sK129(sK106,sK107,sK108,sF925)))
| ~ spl928_160
| ~ spl928_592 ),
inference(resolution,[],[f52052,f47760]) ).
fof(f52263,plain,
( m2_tsp_1(sK107,sK107)
| ~ l1_pre_topc(sK107)
| ~ spl928_19 ),
inference(resolution,[],[f50584,f39901]) ).
fof(f52264,plain,
( ~ spl928_19
| spl928_54
| ~ spl928_19 ),
inference(avatar_split_clause,[],[f52263,f46665,f46844,f46665]) ).
fof(f52313,plain,
( ~ v2_t_0topsp(sK107)
| v3_struct_0(sK107)
| u1_struct_0(sK107) != sF925
| ~ spl928_54
| ~ spl928_569 ),
inference(resolution,[],[f46845,f51819]) ).
fof(f52317,plain,
( sF925 != sF925
| ~ v2_t_0topsp(sK107)
| v3_struct_0(sK107)
| ~ spl928_54
| ~ spl928_569 ),
inference(forward_demodulation,[],[f52313,f46548]) ).
fof(f52318,plain,
( ~ v2_t_0topsp(sK107)
| v3_struct_0(sK107)
| ~ spl928_54
| ~ spl928_569 ),
inference(trivial_inequality_removal,[],[f52317]) ).
fof(f52328,plain,
( spl928_21
| ~ spl928_56
| ~ spl928_54
| ~ spl928_569 ),
inference(avatar_split_clause,[],[f52318,f51818,f46844,f46855,f46678]) ).
fof(f52345,plain,
( ~ spl928_74
| ~ spl928_567
| spl928_578 ),
inference(avatar_split_clause,[],[f51956,f51925,f51805,f47003]) ).
fof(f52360,plain,
( sF925 = k3_tex_4(sK107,k2_pre_topc(sK107))
| ~ m1_subset_1(k2_pre_topc(sK107),k1_zfmisc_1(sF925))
| ~ spl928_316
| ~ spl928_578 ),
inference(resolution,[],[f51927,f49432]) ).
fof(f52367,plain,
( sF925 = k2_pre_topc(sK107)
| ~ m1_subset_1(k2_pre_topc(sK107),k1_zfmisc_1(sF925))
| ~ spl928_316
| ~ spl928_558
| ~ spl928_578 ),
inference(forward_demodulation,[],[f52360,f51747]) ).
fof(f52368,plain,
( ~ spl928_559
| spl928_580
| ~ spl928_316
| ~ spl928_558
| ~ spl928_578 ),
inference(avatar_split_clause,[],[f52367,f51925,f51745,f49431,f51933,f51749]) ).
fof(f53165,definition,
( spl928_699
<=> m1_subset_1(sF926(sK129(sK106,sK107,sK108,sF925)),sF925) ),
introduced(definition,[new_symbols(definition,[spl928_699])],[avatar_definition]) ).
fof(f53166,plain,
( ~ m1_subset_1(sF926(sK129(sK106,sK107,sK108,sF925)),sF925)
| spl928_699 ),
inference(avatar_component_clause,[],[f53165]) ).
fof(f53167,plain,
( m1_subset_1(sF926(sK129(sK106,sK107,sK108,sF925)),sF925)
| ~ spl928_699 ),
inference(avatar_component_clause,[],[f53165]) ).
fof(f62589,definition,
( spl928_1507
<=> sF927(sK129(sK106,sK107,sK108,sF925)) = sF927(sF926(sK129(sK106,sK107,sK108,sF925))) ),
introduced(definition,[new_symbols(definition,[spl928_1507])],[avatar_definition]) ).
fof(f62590,plain,
( sF927(sK129(sK106,sK107,sK108,sF925)) != sF927(sF926(sK129(sK106,sK107,sK108,sF925)))
| spl928_1507 ),
inference(avatar_component_clause,[],[f62589]) ).
fof(f62591,plain,
( sF927(sK129(sK106,sK107,sK108,sF925)) = sF927(sF926(sK129(sK106,sK107,sK108,sF925)))
| ~ spl928_1507 ),
inference(avatar_component_clause,[],[f62589]) ).
fof(f62845,plain,
( sF927(sK129(sK106,sK107,sK108,sF925)) != sF927(sK129(sK106,sK107,sK108,sF925))
| ~ m1_subset_1(sK129(sK106,sK107,sK108,sF925),sF924)
| ~ spl928_25
| ~ spl928_168
| spl928_1507 ),
inference(superposition,[],[f62590,f47884]) ).
fof(f62846,plain,
( ~ m1_subset_1(sK129(sK106,sK107,sK108,sF925),sF924)
| ~ spl928_25
| ~ spl928_168
| spl928_1507 ),
inference(trivial_inequality_removal,[],[f62845]) ).
fof(f62847,plain,
( ~ spl928_276
| ~ spl928_25
| ~ spl928_168
| spl928_1507 ),
inference(avatar_split_clause,[],[f62846,f62589,f47847,f46695,f49056]) ).
fof(f63834,plain,
( ~ m1_subset_1(sK129(sK106,sK107,sK108,sF925),sF924)
| ~ spl928_31
| spl928_699 ),
inference(resolution,[],[f53166,f46728]) ).
fof(f63842,plain,
( ~ spl928_276
| ~ spl928_31
| spl928_699 ),
inference(avatar_split_clause,[],[f63834,f53165,f46727,f49056]) ).
fof(f63843,plain,
( k1_struct_0(sK107,sF926(sK129(sK106,sK107,sK108,sF925))) = k2_tarski(sF926(sK129(sK106,sK107,sK108,sF925)),sF926(sK129(sK106,sK107,sK108,sF925)))
| ~ spl928_159
| ~ spl928_699 ),
inference(resolution,[],[f53167,f47756]) ).
fof(f63849,plain,
( r2_hidden(sF926(sK129(sK106,sK107,sK108,sF925)),k2_pre_topc(sK107))
| ~ spl928_308
| ~ spl928_699 ),
inference(resolution,[],[f53167,f49323]) ).
fof(f63858,plain,
( r2_hidden(sF926(sK129(sK106,sK107,sK108,sF925)),sF925)
| ~ spl928_308
| ~ spl928_580
| ~ spl928_699 ),
inference(forward_demodulation,[],[f63849,f51934]) ).
fof(f63860,plain,
( k1_struct_0(sK107,sF926(sK129(sK106,sK107,sK108,sF925))) = k1_struct_0(sK106,sF926(sK129(sK106,sK107,sK108,sF925)))
| ~ spl928_159
| ~ spl928_160
| ~ spl928_592
| ~ spl928_699 ),
inference(forward_demodulation,[],[f63843,f52112]) ).
fof(f63893,definition,
( spl928_1627
<=> r2_hidden(sF926(sK129(sK106,sK107,sK108,sF925)),sF925) ),
introduced(definition,[new_symbols(definition,[spl928_1627])],[avatar_definition]) ).
fof(f63894,plain,
( r2_hidden(sF926(sK129(sK106,sK107,sK108,sF925)),sF925)
| ~ spl928_1627 ),
inference(avatar_component_clause,[],[f63893]) ).
fof(f64200,plain,
( spl928_1627
| ~ spl928_308
| ~ spl928_580
| ~ spl928_699 ),
inference(avatar_split_clause,[],[f63858,f53165,f51933,f49322,f63893]) ).
fof(f64203,plain,
( ~ m1_subset_1(sF926(sK129(sK106,sK107,sK108,sF925)),sF924)
| k1_struct_0(sK106,sF926(sK129(sK106,sK107,sK108,sF925))) = k5_subset_1(sF924,sF925,sF927(sF926(sK129(sK106,sK107,sK108,sF925))))
| ~ spl928_349
| ~ spl928_1627 ),
inference(resolution,[],[f63894,f49903]) ).
fof(f64209,plain,
( k1_struct_0(sK106,sF926(sK129(sK106,sK107,sK108,sF925))) = k5_subset_1(sF924,sF925,sF927(sK129(sK106,sK107,sK108,sF925)))
| ~ m1_subset_1(sF926(sK129(sK106,sK107,sK108,sF925)),sF924)
| ~ spl928_349
| ~ spl928_1507
| ~ spl928_1627 ),
inference(forward_demodulation,[],[f64203,f62591]) ).
fof(f64211,definition,
( spl928_1668
<=> k1_struct_0(sK106,sF926(sK129(sK106,sK107,sK108,sF925))) = k5_subset_1(sF924,sF925,sF927(sK129(sK106,sK107,sK108,sF925))) ),
introduced(definition,[new_symbols(definition,[spl928_1668])],[avatar_definition]) ).
fof(f64213,plain,
( k1_struct_0(sK106,sF926(sK129(sK106,sK107,sK108,sF925))) = k5_subset_1(sF924,sF925,sF927(sK129(sK106,sK107,sK108,sF925)))
| ~ spl928_1668 ),
inference(avatar_component_clause,[],[f64211]) ).
fof(f64214,plain,
( ~ spl928_592
| spl928_1668
| ~ spl928_349
| ~ spl928_1507
| ~ spl928_1627 ),
inference(avatar_split_clause,[],[f64209,f63893,f62589,f49902,f64211,f52051]) ).
fof(f64338,plain,
( k1_struct_0(sK107,sF926(sK129(sK106,sK107,sK108,sF925))) != k1_struct_0(sK106,sF926(sK129(sK106,sK107,sK108,sF925)))
| ~ m1_subset_1(sF925,k1_zfmisc_1(sF924))
| ~ m1_subset_1(sF927(sK129(sK106,sK107,sK108,sF925)),k1_zfmisc_1(sF924))
| spl928_189
| ~ spl928_1668 ),
inference(superposition,[],[f48122,f64213]) ).
fof(f64347,plain,
( k1_struct_0(sK106,sF926(sK129(sK106,sK107,sK108,sF925))) != k1_struct_0(sK106,sF926(sK129(sK106,sK107,sK108,sF925)))
| ~ m1_subset_1(sF925,k1_zfmisc_1(sF924))
| ~ m1_subset_1(sF927(sK129(sK106,sK107,sK108,sF925)),k1_zfmisc_1(sF924))
| ~ spl928_159
| ~ spl928_160
| spl928_189
| ~ spl928_592
| ~ spl928_699
| ~ spl928_1668 ),
inference(forward_demodulation,[],[f64338,f63860]) ).
fof(f64348,plain,
( ~ m1_subset_1(sF925,k1_zfmisc_1(sF924))
| ~ m1_subset_1(sF927(sK129(sK106,sK107,sK108,sF925)),k1_zfmisc_1(sF924))
| ~ spl928_159
| ~ spl928_160
| spl928_189
| ~ spl928_592
| ~ spl928_699
| ~ spl928_1668 ),
inference(trivial_inequality_removal,[],[f64347]) ).
fof(f64354,plain,
( ~ spl928_188
| ~ spl928_48
| ~ spl928_159
| ~ spl928_160
| spl928_189
| ~ spl928_592
| ~ spl928_699
| ~ spl928_1668 ),
inference(avatar_split_clause,[],[f64348,f64211,f53165,f52051,f48108,f47759,f47755,f46820,f48104]) ).
cnf(s13,plain,
( ~ spl928_18
| spl928_19 ),
inference(sat_conversion,[],[f46668]) ).
cnf(s16,plain,
( ~ spl928_18
| ~ spl928_23
| spl928_24
| spl928_25 ),
inference(sat_conversion,[],[f46699]) ).
cnf(s19,plain,
( ~ spl928_26
| ~ spl928_27
| ~ spl928_28
| spl928_29
| spl928_31 ),
inference(sat_conversion,[],[f46729]) ).
cnf(s27,plain,
~ spl928_24,
inference(sat_conversion,[],[f46775]) ).
cnf(s29,plain,
~ spl928_21,
inference(sat_conversion,[],[f46778]) ).
cnf(s33,plain,
( spl928_21
| spl928_43 ),
inference(sat_conversion,[],[f46798]) ).
cnf(s36,plain,
( ~ spl928_18
| ~ spl928_23
| spl928_24
| ~ spl928_43
| ~ spl928_48
| ~ spl928_49
| ~ spl928_50
| spl928_51 ),
inference(sat_conversion,[],[f46834]) ).
cnf(s39,plain,
spl928_26,
inference(sat_conversion,[],[f46862]) ).
cnf(s41,plain,
spl928_18,
inference(sat_conversion,[],[f46865]) ).
cnf(s43,plain,
spl928_23,
inference(sat_conversion,[],[f46868]) ).
cnf(s45,plain,
spl928_50,
inference(sat_conversion,[],[f46871]) ).
cnf(s48,plain,
( ~ spl928_18
| spl928_24
| spl928_48
| ~ spl928_50 ),
inference(sat_conversion,[],[f46879]) ).
cnf(s49,plain,
( ~ spl928_19
| spl928_21
| spl928_52
| ~ spl928_54 ),
inference(sat_conversion,[],[f46880]) ).
cnf(s51,plain,
spl928_49,
inference(sat_conversion,[],[f46883]) ).
cnf(s52,plain,
( ~ spl928_18
| spl928_21
| ~ spl928_23
| spl928_24
| ~ spl928_49
| ~ spl928_50
| spl928_56 ),
inference(sat_conversion,[],[f46885]) ).
cnf(s64,plain,
spl928_27,
inference(sat_conversion,[],[f46944]) ).
cnf(s66,plain,
spl928_28,
inference(sat_conversion,[],[f46947]) ).
cnf(s74,plain,
( ~ spl928_18
| spl928_72 ),
inference(sat_conversion,[],[f47011]) ).
cnf(s75,plain,
( ~ spl928_19
| spl928_74 ),
inference(sat_conversion,[],[f47013]) ).
cnf(s141,plain,
spl928_84,
inference(sat_conversion,[],[f47400]) ).
cnf(s144,plain,
spl928_85,
inference(sat_conversion,[],[f47409]) ).
cnf(s146,plain,
~ spl928_86,
inference(sat_conversion,[],[f47412]) ).
cnf(s149,plain,
( ~ spl928_18
| spl928_20
| ~ spl928_23
| spl928_24
| ~ spl928_49
| ~ spl928_128 ),
inference(sat_conversion,[],[f47428]) ).
cnf(s150,plain,
( spl928_24
| ~ spl928_29
| ~ spl928_72 ),
inference(sat_conversion,[],[f47431]) ).
cnf(s189,plain,
( spl928_21
| ~ spl928_74
| spl928_159 ),
inference(sat_conversion,[],[f47757]) ).
cnf(s190,plain,
( spl928_24
| ~ spl928_72
| spl928_160 ),
inference(sat_conversion,[],[f47761]) ).
cnf(s197,plain,
( ~ spl928_18
| ~ spl928_23
| spl928_24
| spl928_167 ),
inference(sat_conversion,[],[f47828]) ).
cnf(s199,plain,
( ~ spl928_18
| ~ spl928_23
| spl928_24
| ~ spl928_25
| ~ spl928_167
| spl928_168 ),
inference(sat_conversion,[],[f47850]) ).
cnf(s210,plain,
( ~ spl928_18
| ~ spl928_23
| spl928_24
| spl928_179 ),
inference(sat_conversion,[],[f48020]) ).
cnf(s215,plain,
( ~ spl928_18
| ~ spl928_23
| spl928_24
| spl928_185 ),
inference(sat_conversion,[],[f48086]) ).
cnf(s216,plain,
( spl928_21
| ~ spl928_49
| ~ spl928_50
| ~ spl928_185
| spl928_186 ),
inference(sat_conversion,[],[f48095]) ).
cnf(s217,plain,
( ~ spl928_27
| ~ spl928_28
| ~ spl928_84
| ~ spl928_85
| spl928_86
| ~ spl928_186
| spl928_187 ),
inference(sat_conversion,[],[f48101]) ).
cnf(s218,plain,
( ~ spl928_48
| ~ spl928_187
| ~ spl928_188
| ~ spl928_189 ),
inference(sat_conversion,[],[f48111]) ).
cnf(s219,plain,
( ~ spl928_25
| ~ spl928_27
| ~ spl928_28
| ~ spl928_51
| ~ spl928_84
| ~ spl928_85
| spl928_86
| spl928_188 ),
inference(sat_conversion,[],[f48118]) ).
cnf(s228,plain,
( ~ spl928_18
| ~ spl928_50
| spl928_128 ),
inference(sat_conversion,[],[f48221]) ).
cnf(s313,plain,
( ~ spl928_27
| ~ spl928_28
| ~ spl928_51
| ~ spl928_84
| ~ spl928_85
| spl928_86
| spl928_276 ),
inference(sat_conversion,[],[f49066]) ).
cnf(s326,plain,
( ~ spl928_18
| ~ spl928_23
| spl928_24
| spl928_290 ),
inference(sat_conversion,[],[f49197]) ).
cnf(s342,plain,
( spl928_21
| ~ spl928_74
| spl928_308 ),
inference(sat_conversion,[],[f49324]) ).
cnf(s349,plain,
( ~ spl928_19
| ~ spl928_20
| spl928_21
| spl928_316 ),
inference(sat_conversion,[],[f49433]) ).
cnf(s390,plain,
( ~ spl928_18
| spl928_24
| ~ spl928_48
| ~ spl928_49
| ~ spl928_50
| ~ spl928_179
| ~ spl928_290
| spl928_349 ),
inference(sat_conversion,[],[f49904]) ).
cnf(s587,plain,
( ~ spl928_19
| ~ spl928_20
| spl928_554 ),
inference(sat_conversion,[],[f51712]) ).
cnf(s589,plain,
( ~ spl928_74
| ~ spl928_554
| spl928_556 ),
inference(sat_conversion,[],[f51740]) ).
cnf(s592,plain,
( ~ spl928_19
| ~ spl928_20
| spl928_21
| ~ spl928_554
| spl928_558
| ~ spl928_559 ),
inference(sat_conversion,[],[f51757]) ).
cnf(s597,plain,
( ~ spl928_19
| ~ spl928_20
| spl928_21
| ~ spl928_52
| ~ spl928_556
| spl928_563 ),
inference(sat_conversion,[],[f51787]) ).
cnf(s600,plain,
( ~ spl928_19
| ~ spl928_20
| spl928_21
| ~ spl928_52
| ~ spl928_563
| spl928_567
| ~ spl928_568 ),
inference(sat_conversion,[],[f51812]) ).
cnf(s606,plain,
( ~ spl928_19
| spl928_21
| ~ spl928_52
| spl928_568
| spl928_569 ),
inference(sat_conversion,[],[f51831]) ).
cnf(s629,plain,
( ~ spl928_74
| spl928_559 ),
inference(sat_conversion,[],[f51906]) ).
cnf(s650,plain,
( ~ spl928_188
| ~ spl928_276
| spl928_592 ),
inference(sat_conversion,[],[f52103]) ).
cnf(s660,plain,
( ~ spl928_19
| ~ spl928_19
| spl928_54 ),
inference(sat_conversion,[],[f52264]) ).
cnf(s661,plain,
( ~ spl928_19
| spl928_54 ),
inference(rat,[],[s660]) ).
cnf(s670,plain,
( spl928_21
| ~ spl928_54
| ~ spl928_56
| ~ spl928_569 ),
inference(sat_conversion,[],[f52328]) ).
cnf(s678,plain,
( ~ spl928_74
| ~ spl928_567
| spl928_578 ),
inference(sat_conversion,[],[f52345]) ).
cnf(s681,plain,
( ~ spl928_316
| ~ spl928_558
| ~ spl928_559
| ~ spl928_578
| spl928_580 ),
inference(sat_conversion,[],[f52368]) ).
cnf(s1970,plain,
( ~ spl928_25
| ~ spl928_168
| ~ spl928_276
| spl928_1507 ),
inference(sat_conversion,[],[f62847]) ).
cnf(s2154,plain,
( ~ spl928_31
| ~ spl928_276
| spl928_699 ),
inference(sat_conversion,[],[f63842]) ).
cnf(s2215,plain,
( ~ spl928_308
| ~ spl928_580
| ~ spl928_699
| spl928_1627 ),
inference(sat_conversion,[],[f64200]) ).
cnf(s2216,plain,
( ~ spl928_349
| ~ spl928_592
| ~ spl928_1507
| ~ spl928_1627
| spl928_1668 ),
inference(sat_conversion,[],[f64214]) ).
cnf(s2256,plain,
( ~ spl928_48
| ~ spl928_159
| ~ spl928_160
| ~ spl928_188
| spl928_189
| ~ spl928_592
| ~ spl928_699
| ~ spl928_1668 ),
inference(sat_conversion,[],[f64354]) ).
cnf(s2293,plain,
spl928_128,
inference(rat,[],[s228,s45,s41]) ).
cnf(s2304,plain,
spl928_72,
inference(rat,[],[s74,s41]) ).
cnf(s2318,plain,
( spl928_24
| ~ spl928_43
| ~ spl928_48
| spl928_51 ),
inference(rat,[],[s36,s45,s51,s43,s41]) ).
cnf(s2323,plain,
spl928_43,
inference(rat,[],[s33,s29]) ).
cnf(s2331,plain,
spl928_160,
inference(rat,[],[s190,s2304,s27]) ).
cnf(s2334,plain,
~ spl928_29,
inference(rat,[],[s150,s2304,s27]) ).
cnf(s2341,plain,
spl928_48,
inference(rat,[],[s48,s45,s41,s27]) ).
cnf(s2377,plain,
spl928_290,
inference(rat,[],[s326,s41,s43,s27]) ).
cnf(s2379,plain,
spl928_185,
inference(rat,[],[s215,s41,s43,s27]) ).
cnf(s2381,plain,
spl928_179,
inference(rat,[],[s210,s41,s43,s27]) ).
cnf(s2383,plain,
spl928_167,
inference(rat,[],[s197,s41,s43,s27]) ).
cnf(s2393,plain,
spl928_20,
inference(rat,[],[s149,s2293,s51,s41,s43,s27]) ).
cnf(s2394,plain,
spl928_56,
inference(rat,[],[s52,s29,s45,s51,s41,s43,s27]) ).
cnf(s2409,plain,
spl928_51,
inference(rat,[],[s2318,s27,s2323,s2341]) ).
cnf(s2416,plain,
spl928_186,
inference(rat,[],[s216,s29,s45,s51,s2379]) ).
cnf(s2419,plain,
spl928_349,
inference(rat,[],[s390,s2341,s2377,s27,s45,s51,s41,s2381]) ).
cnf(s2432,plain,
spl928_276,
inference(rat,[],[s313,s64,s146,s144,s141,s66,s2409]) ).
cnf(s2436,plain,
spl928_187,
inference(rat,[],[s217,s64,s66,s146,s144,s141,s2416]) ).
cnf(s2465,plain,
spl928_31,
inference(rat,[],[s19,s2334,s66,s64,s39]) ).
cnf(s2466,plain,
spl928_699,
inference(rat,[],[s2154,s2432,s2465]) ).
cnf(s2474,plain,
spl928_25,
inference(rat,[],[s16,s27,s43,s41]) ).
cnf(s2477,plain,
spl928_188,
inference(rat,[],[s219,s2409,s146,s144,s141,s64,s66,s2474]) ).
cnf(s2479,plain,
spl928_168,
inference(rat,[],[s199,s2383,s27,s41,s43,s2474]) ).
cnf(s2482,plain,
spl928_592,
inference(rat,[],[s650,s2432,s2477]) ).
cnf(s2483,plain,
~ spl928_189,
inference(rat,[],[s218,s2436,s2341,s2477]) ).
cnf(s2485,plain,
spl928_1507,
inference(rat,[],[s1970,s2474,s2432,s2479]) ).
cnf(s2517,plain,
spl928_19,
inference(rat,[],[s13,s41]) ).
cnf(s2549,plain,
spl928_54,
inference(rat,[],[s661,s2517]) ).
cnf(s2553,plain,
spl928_554,
inference(rat,[],[s587,s2393,s2517]) ).
cnf(s2563,plain,
spl928_316,
inference(rat,[],[s349,s2393,s29,s2517]) ).
cnf(s2598,plain,
spl928_74,
inference(rat,[],[s75,s2517]) ).
cnf(s2602,plain,
spl928_52,
inference(rat,[],[s49,s2549,s29,s2517]) ).
cnf(s2622,plain,
~ spl928_569,
inference(rat,[],[s670,s2394,s29,s2549]) ).
cnf(s2654,plain,
spl928_559,
inference(rat,[],[s629,s2598]) ).
cnf(s2655,plain,
spl928_556,
inference(rat,[],[s589,s2553,s2598]) ).
cnf(s2659,plain,
spl928_308,
inference(rat,[],[s342,s29,s2598]) ).
cnf(s2661,plain,
spl928_159,
inference(rat,[],[s189,s29,s2598]) ).
cnf(s2678,plain,
spl928_568,
inference(rat,[],[s606,s2622,s2517,s29,s2602]) ).
cnf(s2705,plain,
spl928_558,
inference(rat,[],[s592,s2553,s2517,s2393,s29,s2654]) ).
cnf(s2709,plain,
spl928_563,
inference(rat,[],[s597,s2602,s2517,s2393,s29,s2655]) ).
cnf(s2714,plain,
~ spl928_1668,
inference(rat,[],[s2256,s2483,s2466,s2482,s2477,s2341,s2331,s2661]) ).
cnf(s2748,plain,
spl928_567,
inference(rat,[],[s600,s2678,s2602,s2517,s2393,s29,s2709]) ).
cnf(s2752,plain,
~ spl928_1627,
inference(rat,[],[s2216,s2485,s2482,s2419,s2714]) ).
cnf(s2781,plain,
spl928_578,
inference(rat,[],[s678,s2598,s2748]) ).
cnf(s2825,plain,
~ spl928_580,
inference(rat,[],[s2215,s2659,s2466,s2752]) ).
cnf(s2856,plain,
$false,
inference(rat,[],[s681,s2705,s2654,s2563,s2825,s2781]) ).
fof(f64356,plain,
$false,
inference(avatar_sat_refutation,[],[s2856]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP033+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 % Computer : n026.cluster.edu
% 0.09/0.22 % Model : x86_64 x86_64
% 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.22 % Memory : 8046.5625MB
% 0.09/0.22 % OS : Linux 6.8.0-71-generic
% 0.09/0.22 % CPULimit : 300
% 0.09/0.22 % WCLimit : 300
% 0.09/0.22 % DateTime : Mon Sep 28 18:58:07 UTC 2026
% 0.09/0.22 % CPUTime :
% 0.09/0.22 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.26 Running first-order theorem proving
% 0.09/0.26 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.95/4.52 % (4153824)Detected formulas, will run a generic FOF schedule.
% 13.95/4.52 % (4153834)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2194212673:s2a=on:i=139:gtg=position_2978 on theBenchmark for (2978ds/139Mi)
% 13.95/4.52 % (4153833)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3985632756:i=119:av=off:ss=axioms_2978 on theBenchmark for (2978ds/119Mi)
% 13.95/4.52 % (4153829)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=3678467160:i=141193_2978 on theBenchmark for (2978ds/141193Mi)
% 13.95/4.52 % (4153832)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3571794324:i=109:sd=1:ins=1:gsp=on:ss=axioms_2978 on theBenchmark for (2978ds/109Mi)
% 13.95/4.52 % (4153830)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=2870947091:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2978 on theBenchmark for (2978ds/134677Mi)
% 13.95/4.52 % (4153831)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=3399981555:i=141695:sd=1:nm=32:gsp=on:ss=included_2978 on theBenchmark for (2978ds/141695Mi)
% 13.95/4.52 % (4153835)dis-21_1_sil=8000:lcm=predicate:random_seed=4204926505:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2978 on theBenchmark for (2978ds/129Mi)
% 13.95/4.52 % (4153834)Instruction limit reached!
% 13.95/4.52 % (4153834)------------------------------
% 13.95/4.52 % (4153834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.95/4.52 % (4153834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.95/4.52 % (4153834)CaDiCaL version: 2.1.3
% 13.95/4.52 % (4153834)Termination reason: Instruction limit
% 13.95/4.52 % (4153834)Termination phase: Property scanning
% 13.95/4.52 % (4153834)Time elapsed: 0.036 s
% 13.95/4.52 % (4153834)Peak memory usage: 136 MB
% 13.95/4.52 % (4153834)Instructions burned: 143 (million)
% 13.95/4.52 % (4153832)Instruction limit reached!
% 13.95/4.52 % (4153832)------------------------------
% 13.95/4.52 % (4153832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.95/4.52 % (4153832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.95/4.52 % (4153832)CaDiCaL version: 2.1.3
% 13.95/4.52 % (4153832)Termination reason: Instruction limit
% 13.95/4.52 % (4153832)Termination phase: SInE selection
% 13.95/4.52 % (4153832)Time elapsed: 0.080 s
% 13.95/4.52 % (4153832)Peak memory usage: 135 MB
% 13.95/4.52 % (4153832)Instructions burned: 109 (million)
% 13.95/4.52 % (4153833)Instruction limit reached!
% 13.95/4.52 % (4153833)------------------------------
% 13.95/4.52 % (4153833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.95/4.52 % (4153833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.95/4.52 % (4153833)CaDiCaL version: 2.1.3
% 13.95/4.52 % (4153833)Termination reason: Instruction limit
% 13.95/4.52 % (4153833)Termination phase: SInE selection
% 13.95/4.52 % (4153833)Time elapsed: 0.094 s
% 13.95/4.52 % (4153833)Peak memory usage: 136 MB
% 13.95/4.52 % (4153833)Instructions burned: 126 (million)
% 13.95/4.52 % (4153835)Instruction limit reached!
% 13.95/4.52 % (4153835)------------------------------
% 13.95/4.52 % (4153835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.95/4.52 % (4153835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.95/4.52 % (4153835)CaDiCaL version: 2.1.3
% 13.95/4.52 % (4153835)Termination reason: Instruction limit
% 13.95/4.52 % (4153835)Termination phase: SInE selection
% 13.95/4.52 % (4153835)Time elapsed: 0.086 s
% 13.95/4.52 % (4153835)Peak memory usage: 136 MB
% 13.95/4.52 % (4153835)Instructions burned: 131 (million)
% 13.95/4.52 % (4153843)lrs+10_1_sil=8000:sp=occurrence:random_seed=3867749793:i=285:sd=3:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/285Mi)
% 13.95/4.52 % (4153845)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2974193552:i=325:sd=1:ss=axioms:sgt=32_2975 on theBenchmark for (2975ds/325Mi)
% 13.95/4.52 % (4153844)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1542689314:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/157Mi)
% 13.95/4.52 % (4153843)Instruction limit reached!
% 13.95/4.52 % (4153843)------------------------------
% 13.95/4.52 % (4153843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.95/4.52 % (4153843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.42/5.34 % (4153843)CaDiCaL version: 2.1.3
% 19.42/5.34 % (4153843)Termination reason: Instruction limit
% 19.42/5.34 % (4153843)Termination phase: Preprocessing 3
% 19.42/5.34 % (4153843)Time elapsed: 0.136 s
% 19.42/5.34 % (4153843)Peak memory usage: 140 MB
% 19.42/5.34 % (4153843)Instructions burned: 286 (million)
% 19.42/5.34 % (4153847)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=2491820894:s2a=on:i=248:s2at=1.23:gtg=position_2975 on theBenchmark for (2975ds/248Mi)
% 19.42/5.34 % (4153844)Instruction limit reached!
% 19.42/5.34 % (4153844)------------------------------
% 19.42/5.34 % (4153844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.42/5.34 % (4153844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.42/5.34 % (4153844)CaDiCaL version: 2.1.3
% 19.42/5.34 % (4153844)Termination reason: Instruction limit
% 19.42/5.34 % (4153844)Termination phase: Property scanning
% 19.42/5.34 % (4153844)Time elapsed: 0.071 s
% 19.42/5.34 % (4153844)Peak memory usage: 136 MB
% 19.42/5.34 % (4153844)Instructions burned: 159 (million)
% 19.42/5.34 % (4153851)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=676861660:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2974 on theBenchmark for (2974ds/294Mi)
% 19.42/5.34 % (4153847)Instruction limit reached!
% 19.42/5.34 % (4153847)------------------------------
% 19.42/5.34 % (4153847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.42/5.34 % (4153847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.42/5.34 % (4153847)CaDiCaL version: 2.1.3
% 19.42/5.34 % (4153847)Termination reason: Instruction limit
% 19.42/5.34 % (4153847)Termination phase: Property scanning
% 19.42/5.34 % (4153847)Time elapsed: 0.110 s
% 19.42/5.34 % (4153847)Peak memory usage: 136 MB
% 19.42/5.34 % (4153847)Instructions burned: 250 (million)
% 19.42/5.34 % (4153852)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1243226154:i=2350_2973 on theBenchmark for (2973ds/2350Mi)
% 19.42/5.34 % (4153851)Instruction limit reached!
% 19.42/5.34 % (4153851)------------------------------
% 19.42/5.34 % (4153851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.42/5.34 % (4153851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.42/5.34 % (4153851)CaDiCaL version: 2.1.3
% 19.42/5.34 % (4153851)Termination reason: Instruction limit
% 19.42/5.34 % (4153851)Termination phase: SInE selection
% 19.42/5.34 % (4153851)Time elapsed: 0.104 s
% 19.42/5.34 % (4153851)Peak memory usage: 136 MB
% 19.42/5.34 % (4153851)Instructions burned: 295 (million)
% 19.42/5.34 % (4153845)Instruction limit reached!
% 19.42/5.34 % (4153845)------------------------------
% 19.42/5.34 % (4153845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.42/5.34 % (4153845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.42/5.34 % (4153845)CaDiCaL version: 2.1.3
% 19.42/5.34 % (4153845)Termination reason: Instruction limit
% 19.42/5.34 % (4153845)Termination phase: Saturation
% 19.42/5.34 % (4153845)Time elapsed: 0.252 s
% 19.42/5.34 % (4153845)Peak memory usage: 142 MB
% 19.42/5.34 % (4153845)Instructions burned: 325 (million)
% 19.42/5.34 % (4153854)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4284783605:cts=off:i=113:fsr=off:ss=included:sgt=4_2973 on theBenchmark for (2973ds/113Mi)
% 19.42/5.34 % (4153856)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2803687396:i=127:av=off:fsr=off:sup=off_2972 on theBenchmark for (2972ds/127Mi)
% 19.42/5.34 % (4153854)Instruction limit reached!
% 19.42/5.34 % (4153854)------------------------------
% 19.42/5.34 % (4153854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.42/5.34 % (4153854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.42/5.34 % (4153854)CaDiCaL version: 2.1.3
% 19.42/5.34 % (4153854)Termination reason: Instruction limit
% 19.42/5.34 % (4153854)Termination phase: SInE selection
% 19.42/5.34 % (4153854)Time elapsed: 0.087 s
% 19.42/5.34 % (4153854)Peak memory usage: 136 MB
% 19.42/5.34 % (4153854)Instructions burned: 113 (million)
% 19.42/5.34 % (4153856)Instruction limit reached!
% 19.42/5.34 % (4153856)------------------------------
% 19.42/5.34 % (4153856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.42/5.34 % (4153856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.42/5.34 % (4153856)CaDiCaL version: 2.1.3
% 63.10/11.48 % (4153856)Termination reason: Instruction limit
% 63.10/11.48 % (4153856)Termination phase: Preprocessing 1
% 63.10/11.48 % (4153856)Time elapsed: 0.057 s
% 63.10/11.48 % (4153856)Peak memory usage: 137 MB
% 63.10/11.48 % (4153856)Instructions burned: 129 (million)
% 63.10/11.48 % (4153858)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4210917431:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2971 on theBenchmark for (2971ds/114Mi)
% 63.10/11.48 % (4153858)Instruction limit reached!
% 63.10/11.48 % (4153858)------------------------------
% 63.10/11.48 % (4153858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.10/11.48 % (4153858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.10/11.48 % (4153858)CaDiCaL version: 2.1.3
% 63.10/11.48 % (4153858)Termination reason: Instruction limit
% 63.10/11.48 % (4153858)Termination phase: Property scanning
% 63.10/11.48 % (4153858)Time elapsed: 0.052 s
% 63.10/11.48 % (4153858)Peak memory usage: 136 MB
% 63.10/11.48 % (4153858)Instructions burned: 114 (million)
% 63.10/11.48 % (4153861)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2228398373:i=437:sd=1:aac=none:ss=included_2970 on theBenchmark for (2970ds/437Mi)
% 63.10/11.48 % (4153860)lrs+10_1_sil=8000:sp=occurrence:random_seed=1261277809:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2971 on theBenchmark for (2971ds/907Mi)
% 63.10/11.48 % (4153863)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3020457413:i=5202:ss=axioms:sgt=16_2970 on theBenchmark for (2970ds/5202Mi)
% 63.10/11.48 % (4153861)Instruction limit reached!
% 63.10/11.48 % (4153861)------------------------------
% 63.10/11.48 % (4153861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.10/11.48 % (4153861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.10/11.48 % (4153861)CaDiCaL version: 2.1.3
% 63.10/11.48 % (4153861)Termination reason: Instruction limit
% 63.10/11.48 % (4153861)Termination phase: Saturation
% 63.10/11.48 % (4153861)Time elapsed: 0.175 s
% 63.10/11.48 % (4153861)Peak memory usage: 143 MB
% 63.10/11.48 % (4153861)Instructions burned: 438 (million)
% 63.10/11.48 % (4153867)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4269068326:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2968 on theBenchmark for (2968ds/134Mi)
% 63.10/11.48 % (4153867)Instruction limit reached!
% 63.10/11.48 % (4153867)------------------------------
% 63.10/11.48 % (4153867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.10/11.48 % (4153867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.10/11.48 % (4153867)CaDiCaL version: 2.1.3
% 63.10/11.48 % (4153867)Termination reason: Instruction limit
% 63.10/11.48 % (4153867)Termination phase: SInE selection
% 63.10/11.48 % (4153867)Time elapsed: 0.061 s
% 63.10/11.48 % (4153867)Peak memory usage: 136 MB
% 63.10/11.48 % (4153867)Instructions burned: 136 (million)
% 63.10/11.48 % (4153869)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3805270200:st=8:i=592:sd=3:ep=RST:ss=axioms_2966 on theBenchmark for (2966ds/592Mi)
% 63.10/11.48 % (4153860)Instruction limit reached!
% 63.10/11.48 % (4153860)------------------------------
% 63.10/11.48 % (4153860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.10/11.48 % (4153860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.10/11.48 % (4153860)CaDiCaL version: 2.1.3
% 63.10/11.48 % (4153860)Termination reason: Instruction limit
% 63.10/11.48 % (4153860)Termination phase: Property scanning
% 63.10/11.48 % (4153860)Time elapsed: 0.613 s
% 63.10/11.48 % (4153860)Peak memory usage: 158 MB
% 63.10/11.48 % (4153860)Instructions burned: 909 (million)
% 63.10/11.48 % (4153869)Instruction limit reached!
% 63.10/11.48 % (4153869)------------------------------
% 63.10/11.48 % (4153869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.10/11.48 % (4153869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.10/11.48 % (4153869)CaDiCaL version: 2.1.3
% 63.10/11.48 % (4153869)Termination reason: Instruction limit
% 63.10/11.48 % (4153869)Termination phase: Preprocessing 2
% 63.10/11.48 % (4153869)Time elapsed: 0.270 s
% 63.10/11.48 % (4153869)Peak memory usage: 147 MB
% 63.10/11.48 % (4153869)Instructions burned: 593 (million)
% 63.10/11.48 % (4153871)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=510100784:st=3:i=13193:sd=3:ss=axioms_2963 on theBenchmark for (2963ds/13193Mi)
% 63.10/11.48 % (4153872)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=2910188893:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2962 on theBenchmark for (2962ds/125Mi)
% 74.74/13.10 % (4153872)Instruction limit reached!
% 74.74/13.10 % (4153872)------------------------------
% 74.74/13.10 % (4153872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.74/13.10 % (4153872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.74/13.10 % (4153872)CaDiCaL version: 2.1.3
% 74.74/13.10 % (4153872)Termination reason: Instruction limit
% 74.74/13.10 % (4153872)Termination phase: Property scanning
% 74.74/13.10 % (4153872)Time elapsed: 0.033 s
% 74.74/13.10 % (4153872)Peak memory usage: 136 MB
% 74.74/13.10 % (4153872)Instructions burned: 129 (million)
% 74.74/13.10 % (4153875)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3883348079:i=134:gtgl=5:slsql=off:gtg=exists_sym_2961 on theBenchmark for (2961ds/134Mi)
% 74.74/13.10 % (4153875)Instruction limit reached!
% 74.74/13.10 % (4153875)------------------------------
% 74.74/13.10 % (4153875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.74/13.10 % (4153875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.74/13.10 % (4153875)CaDiCaL version: 2.1.3
% 74.74/13.10 % (4153875)Termination reason: Instruction limit
% 74.74/13.10 % (4153875)Termination phase: Property scanning
% 74.74/13.10 % (4153875)Time elapsed: 0.034 s
% 74.74/13.10 % (4153875)Peak memory usage: 136 MB
% 74.74/13.10 % (4153875)Instructions burned: 137 (million)
% 74.74/13.10 % (4153877)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3292588473:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2960 on theBenchmark for (2960ds/141Mi)
% 74.74/13.10 % (4153877)Instruction limit reached!
% 74.74/13.10 % (4153877)------------------------------
% 74.74/13.10 % (4153877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.74/13.10 % (4153877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.74/13.10 % (4153877)CaDiCaL version: 2.1.3
% 74.74/13.10 % (4153877)Termination reason: Instruction limit
% 74.74/13.10 % (4153877)Termination phase: SInE selection
% 74.74/13.10 % (4153877)Time elapsed: 0.064 s
% 74.74/13.10 % (4153877)Peak memory usage: 136 MB
% 74.74/13.10 % (4153877)Instructions burned: 142 (million)
% 74.74/13.10 % (4153879)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1275220923:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2958 on theBenchmark for (2958ds/431Mi)
% 74.74/13.10 % (4153852)Instruction limit reached!
% 74.74/13.10 % (4153852)------------------------------
% 74.74/13.10 % (4153852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.74/13.10 % (4153852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.74/13.10 % (4153852)CaDiCaL version: 2.1.3
% 74.74/13.10 % (4153852)Termination reason: Instruction limit
% 74.74/13.10 % (4153852)Termination phase: Property scanning
% 74.74/13.10 % (4153852)Time elapsed: 1.557 s
% 74.74/13.10 % (4153852)Peak memory usage: 232 MB
% 74.74/13.10 % (4153852)Instructions burned: 2353 (million)
% 74.74/13.10 % (4153879)Instruction limit reached!
% 74.74/13.10 % (4153879)------------------------------
% 74.74/13.10 % (4153879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.74/13.10 % (4153879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.74/13.10 % (4153879)CaDiCaL version: 2.1.3
% 74.74/13.10 % (4153879)Termination reason: Instruction limit
% 74.74/13.10 % (4153879)Termination phase: Saturation
% 74.74/13.10 % (4153879)Time elapsed: 0.186 s
% 74.74/13.10 % (4153879)Peak memory usage: 143 MB
% 74.74/13.10 % (4153879)Instructions burned: 433 (million)
% 74.74/13.10 % (4153881)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=4272375717:i=6060:aac=none:ins=25_2956 on theBenchmark for (2956ds/6060Mi)
% 74.74/13.10 % (4153883)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=3812814132:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2955 on theBenchmark for (2955ds/150Mi)
% 74.74/13.10 % (4153883)Instruction limit reached!
% 74.74/13.10 % (4153883)------------------------------
% 74.74/13.10 % (4153883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.74/13.10 % (4153883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.74/13.10 % (4153883)CaDiCaL version: 2.1.3
% 74.74/13.10 % (4153883)Termination reason: Instruction limit
% 58.55/17.18 % (4153883)Termination phase: SInE selection
% 58.55/17.18 % (4153883)Time elapsed: 0.072 s
% 58.55/17.18 % (4153883)Peak memory usage: 136 MB
% 58.55/17.18 % (4153883)Instructions burned: 152 (million)
% 58.55/17.18 % (4153885)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2307708327:i=14155:bd=all_2953 on theBenchmark for (2953ds/14155Mi)
% 58.55/17.18 % (4153863)Instruction limit reached!
% 58.55/17.18 % (4153863)------------------------------
% 58.55/17.18 % (4153863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.55/17.18 % (4153863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.55/17.18 % (4153863)CaDiCaL version: 2.1.3
% 58.55/17.18 % (4153863)Termination reason: Instruction limit
% 58.55/17.18 % (4153863)Termination phase: Saturation
% 58.55/17.18 % (4153863)Time elapsed: 3.832 s
% 58.55/17.18 % (4153863)Peak memory usage: 594 MB
% 58.55/17.18 % (4153863)Instructions burned: 5202 (million)
% 58.55/17.18 % (4153888)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3334036845:i=667:av=off:fsr=off_2929 on theBenchmark for (2929ds/667Mi)
% 58.55/17.19 % (4153888)Instruction limit reached!
% 58.55/17.19 % (4153888)------------------------------
% 58.55/17.19 % (4153888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.55/17.19 % (4153888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.55/17.19 % (4153888)CaDiCaL version: 2.1.3
% 58.55/17.19 % (4153888)Termination reason: Instruction limit
% 58.55/17.19 % (4153888)Termination phase: NewCNF
% 58.55/17.19 % (4153888)Time elapsed: 0.539 s
% 58.55/17.19 % (4153888)Peak memory usage: 185 MB
% 58.55/17.19 % (4153888)Instructions burned: 668 (million)
% 58.55/17.19 % (4153890)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1436685779:s2a=on:i=185:s2at=1.8:fdi=4_2923 on theBenchmark for (2923ds/185Mi)
% 58.55/17.19 % (4153890)Instruction limit reached!
% 58.55/17.19 % (4153890)------------------------------
% 58.55/17.19 % (4153890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.55/17.19 % (4153890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.55/17.19 % (4153890)CaDiCaL version: 2.1.3
% 58.55/17.19 % (4153890)Termination reason: Instruction limit
% 58.55/17.19 % (4153890)Termination phase: SInE selection
% 58.55/17.19 % (4153890)Time elapsed: 0.128 s
% 58.55/17.19 % (4153890)Peak memory usage: 136 MB
% 58.55/17.19 % (4153890)Instructions burned: 185 (million)
% 58.55/17.19 % (4153892)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1777290759:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2920 on theBenchmark for (2920ds/193Mi)
% 58.55/17.19 % (4153892)Instruction limit reached!
% 58.55/17.19 % (4153892)------------------------------
% 58.55/17.19 % (4153892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.55/17.19 % (4153892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.55/17.19 % (4153892)CaDiCaL version: 2.1.3
% 58.55/17.19 % (4153892)Termination reason: Instruction limit
% 58.55/17.19 % (4153892)Termination phase: SInE selection
% 58.55/17.19 % (4153892)Time elapsed: 0.148 s
% 58.55/17.19 % (4153892)Peak memory usage: 136 MB
% 58.55/17.19 % (4153892)Instructions burned: 194 (million)
% 58.55/17.19 % (4153881)Instruction limit reached!
% 58.55/17.19 % (4153881)------------------------------
% 58.55/17.19 % (4153881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.55/17.19 % (4153881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.55/17.19 % (4153881)CaDiCaL version: 2.1.3
% 58.55/17.19 % (4153881)Termination reason: Instruction limit
% 58.55/17.19 % (4153881)Termination phase: Function definition elimination
% 58.55/17.19 % (4153881)Time elapsed: 3.850 s
% 58.55/17.19 % (4153881)Peak memory usage: 244 MB
% 58.55/17.19 % (4153881)Instructions burned: 6060 (million)
% 58.55/17.19 % (4153894)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2775833851:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2917 on theBenchmark for (2917ds/4850Mi)
% 58.55/17.19 % (4153895)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1720600673:i=12111:sd=1:ss=included_2916 on theBenchmark for (2916ds/12111Mi)
% 58.55/17.19 % (4153885)Instruction limit reached!
% 58.55/17.19 % (4153885)------------------------------
% 58.55/17.19 % (4153885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.55/17.19 % (4153885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.55/17.19 % (4153885)CaDiCaL version: 2.1.3
% 58.55/17.19 % (4153885)Termination reason: Instruction limit
% 58.55/17.19 % (4153885)Termination phase: Saturation
% 58.55/17.19 % (4153885)Time elapsed: 6.023 s
% 58.55/17.19 % (4153885)Peak memory usage: 1333 MB
% 58.55/17.19 % (4153885)Instructions burned: 14157 (million)
% 58.55/17.19 % (4153894)Instruction limit reached!
% 58.55/17.19 % (4153894)------------------------------
% 58.55/17.19 % (4153894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.55/17.19 % (4153894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.55/17.19 % (4153894)CaDiCaL version: 2.1.3
% 58.55/17.19 % (4153894)Termination reason: Instruction limit
% 58.55/17.19 % (4153894)Termination phase: Property scanning
% 58.55/17.19 % (4153894)Time elapsed: 2.502 s
% 58.55/17.19 % (4153894)Peak memory usage: 217 MB
% 58.55/17.19 % (4153894)Instructions burned: 4851 (million)
% 58.55/17.19 % (4153898)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3837039396:i=319:kws=precedence:fsr=off_2891 on theBenchmark for (2891ds/319Mi)
% 58.55/17.19 % (4153899)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=204691357:i=2064:ep=RST_2890 on theBenchmark for (2890ds/2064Mi)
% 58.55/17.19 % (4153898)Instruction limit reached!
% 58.55/17.19 % (4153898)------------------------------
% 58.55/17.19 % (4153898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.55/17.19 % (4153898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.55/17.19 % (4153898)CaDiCaL version: 2.1.3
% 58.55/17.19 % (4153898)Termination reason: Instruction limit
% 58.55/17.19 % (4153898)Termination phase: Unused predicate definition removal
% 58.55/17.19 % (4153898)Time elapsed: 0.155 s
% 58.55/17.19 % (4153898)Peak memory usage: 142 MB
% 58.55/17.19 % (4153898)Instructions burned: 319 (million)
% 58.55/17.19 % (4153902)dis-1011_128_sil=32000:random_seed=735252971:i=3706:ep=RST:av=off_2888 on theBenchmark for (2888ds/3706Mi)
% 58.55/17.19 % (4153871)Instruction limit reached!
% 58.55/17.19 % (4153871)------------------------------
% 58.55/17.19 % (4153871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.55/17.19 % (4153871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.55/17.19 % (4153871)CaDiCaL version: 2.1.3
% 58.55/17.19 % (4153871)Termination reason: Instruction limit
% 58.55/17.19 % (4153871)Termination phase: Saturation
% 58.55/17.19 % (4153871)Time elapsed: 7.851 s
% 58.55/17.19 % (4153871)Peak memory usage: 307 MB
% 58.55/17.19 % (4153871)Instructions burned: 13193 (million)
% 58.55/17.19 % (4153904)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3086976681:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2883 on theBenchmark for (2883ds/757Mi)
% 58.55/17.19 % (4153904)Instruction limit reached!
% 58.55/17.19 % (4153904)------------------------------
% 58.55/17.19 % (4153904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.55/17.19 % (4153904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.55/17.19 % (4153904)CaDiCaL version: 2.1.3
% 58.55/17.19 % (4153904)Termination reason: Instruction limit
% 58.55/17.19 % (4153904)Termination phase: Saturation
% 58.55/17.19 % (4153904)Time elapsed: 0.560 s
% 58.55/17.19 % (4153904)Peak memory usage: 151 MB
% 58.55/17.19 % (4153904)Instructions burned: 757 (million)
% 58.55/17.19 % (4153899)Instruction limit reached!
% 58.55/17.19 % (4153899)------------------------------
% 58.55/17.19 % (4153899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.55/17.19 % (4153899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.55/17.19 % (4153899)CaDiCaL version: 2.1.3
% 58.55/17.19 % (4153899)Termination reason: Instruction limit
% 58.55/17.19 % (4153899)Termination phase: Property scanning
% 58.55/17.19 % (4153899)Time elapsed: 1.325 s
% 58.55/17.19 % (4153899)Peak memory usage: 231 MB
% 58.55/17.19 % (4153899)Instructions burned: 2066 (million)
% 58.55/17.19 % (4153902)Instruction limit reached!
% 58.55/17.19 % (4153902)------------------------------
% 58.55/17.19 % (4153902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.55/17.19 % (4153902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.55/17.19 % (4153902)CaDiCaL version: 2.1.3
% 58.55/17.19 % (4153902)Termination reason: Instruction limit
% 58.55/17.19 % (4153902)Termination phase: Function definition elimination
% 58.55/17.19 % (4153902)Time elapsed: 1.158 s
% 58.55/17.19 % (4153902)Peak memory usage: 241 MB
% 58.55/17.19 % (4153902)Instructions burned: 3709 (million)
% 58.55/17.19 % (4153906)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=33136734:i=13913:ss=axioms:sgt=8_2876 on theBenchmark for (2876ds/13913Mi)
% 58.55/17.19 % (4153908)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2364338534:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2875 on theBenchmark for (2875ds/2479Mi)
% 58.55/17.19 % (4153907)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2383688420:i=9925:aac=none_2876 on theBenchmark for (2876ds/9925Mi)
% 58.55/17.19 % (4153908)Instruction limit reached!
% 58.55/17.19 % (4153908)------------------------------
% 58.55/17.19 % (4153908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.55/17.19 % (4153908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.55/17.19 % (4153908)CaDiCaL version: 2.1.3
% 58.55/17.19 % (4153908)Termination reason: Instruction limit
% 58.55/17.19 % (4153908)Termination phase: Saturation
% 58.55/17.19 % (4153908)Time elapsed: 0.824 s
% 58.55/17.19 % (4153908)Peak memory usage: 156 MB
% 58.55/17.19 % (4153908)Instructions burned: 2480 (million)
% 58.55/17.19 % (4153912)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2780343340:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2866 on theBenchmark for (2866ds/440Mi)
% 58.55/17.19 % (4153912)Instruction limit reached!
% 58.55/17.19 % (4153912)------------------------------
% 58.55/17.19 % (4153912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.55/17.19 % (4153912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.55/17.19 % (4153912)CaDiCaL version: 2.1.3
% 58.55/17.19 % (4153912)Termination reason: Instruction limit
% 58.55/17.19 % (4153912)Termination phase: Property scanning
% 58.55/17.19 % (4153912)Time elapsed: 0.102 s
% 58.55/17.19 % (4153912)Peak memory usage: 136 MB
% 58.55/17.19 % (4153912)Instructions burned: 444 (million)
% 58.55/17.19 % (4153914)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1542778426:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2864 on theBenchmark for (2864ds/11145Mi)
% 58.55/17.19 % (4153914)First to succeed.
% 58.55/17.19 % (4153914)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-4153824"
% 58.55/17.19 % (4153914)Refutation found. Thanks to Tanya!
% 58.55/17.19 % SZS status Theorem for theBenchmark
% 58.55/17.19 % SZS output start Proof for theBenchmark
% See solution above
% 0.20/17.30 % (4153914)------------------------------
% 0.20/17.30 % (4153914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.20/17.30 % (4153914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/17.30 % (4153914)CaDiCaL version: 2.1.3
% 0.20/17.30 % (4153914)Termination reason: Refutation
% 0.20/17.30 % (4153914)Time elapsed: 2.460 s
% 0.20/17.30 % (4153914)Peak memory usage: 240 MB
% 0.20/17.30 % (4153914)Instructions burned: 6569 (million)
% 0.20/17.30 % (4153914)------------------------------
% 0.20/17.30 % (4153914)------------------------------
% 0.20/17.30 % (4153824)Success in time 16.482 s
% 0.20/17.30 % Vampire exiting
%------------------------------------------------------------------------------