%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : TOP032+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 02:33:57 PM UTC 2026
% Result : Theorem 120.03s 33.09s
% Output : Refutation 213.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 92
% Syntax : Number of formulae : 592 ( 97 unt; 69 def)
% Number of atoms : 2826 ( 279 equ)
% Maximal formula atoms : 19 ( 4 avg)
% Number of connectives : 3986 (1752 ~;1955 |; 148 &)
% ( 80 <=>; 51 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 84 ( 82 usr; 66 prp; 0-3 aty)
% Number of functors : 26 ( 26 usr; 5 con; 0-4 aty)
% Number of variables : 600 ( 0 sgn 587 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f258,axiom,
! [X0] : k2_tarski(X0,X0) = k1_tarski(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f676,axiom,
! [X0,X1] :
( m1_subset_1(X0,X1)
=> ( v1_xboole_0(X1)
| r2_hidden(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
fof(f678,axiom,
! [X0,X1,X2] :
( ( r2_hidden(X0,X1)
& m1_subset_1(X1,k1_zfmisc_1(X2)) )
=> m1_subset_1(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_subset) ).
fof(f1483,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f1495,axiom,
! [X0,X1,X2] :
( m1_relset_1(X2,X0,X1)
=> k4_relset_1(X0,X1,X2) = k1_relat_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k4_relset_1) ).
fof(f1543,axiom,
! [X0,X1,X2,X3] :
( ( v1_funct_1(X3)
& m2_relset_1(X3,X0,X1) )
=> ( r2_hidden(X2,k4_relset_1(X0,X1,X3))
=> r2_hidden(k1_funct_1(X3,X2),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t27_partfun1) ).
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/sandbox2/benchmark/theBenchmark.p',dt_k8_funct_2) ).
fof(f2106,axiom,
! [X0,X1,X2,X3] :
( ( ~ v1_xboole_0(X0)
& v1_funct_1(X2)
& v1_funct_2(X2,X0,X1)
& m1_relset_1(X2,X0,X1)
& m1_subset_1(X3,X0) )
=> k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k8_funct_2) ).
fof(f17598,axiom,
! [X0] :
( l1_struct_0(X0)
=> ( v3_struct_0(X0)
<=> v1_xboole_0(u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',t12_pre_topc) ).
fof(f18318,axiom,
! [X0] :
( l1_pre_topc(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f18585,axiom,
! [X0] :
( l1_struct_0(X0)
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& l1_struct_0(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( k1_relat_1(X2) = k2_pre_topc(X0)
& r1_tarski(k2_relat_1(X2),k2_pre_topc(X1)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t51_tops_2) ).
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/sandbox2/benchmark/theBenchmark.p',t23_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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',dt_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/sandbox2/benchmark/theBenchmark.p',d2_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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',d8_tsp_2) ).
fof(f34413,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
=> ( ( X3 = u1_struct_0(X1)
& ! [X4] :
( m1_subset_1(X4,u1_struct_0(X0))
=> k5_subset_1(u1_struct_0(X0),X3,k4_tex_4(X0,X4)) = k1_struct_0(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X4)) ) )
=> ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t18_tsp_2) ).
fof(f34414,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> r2_hidden(k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X3),k4_tex_4(X0,X3)) )
=> ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t19_tsp_2) ).
fof(f34415,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> r2_hidden(k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X3),k4_tex_4(X0,X3)) )
=> ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f34414]) ).
fof(f34504,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
& ! [X3] :
( r2_hidden(k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X3),k4_tex_4(X0,X3))
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34415]) ).
fof(f34505,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
& ! [X3] :
( r2_hidden(k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X3),k4_tex_4(X0,X3))
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(flattening,[],[f34504]) ).
fof(f34512,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(f34513,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(flattening,[],[f34512]) ).
fof(f34514,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(ennf_transformation,[],[f676]) ).
fof(f34515,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(flattening,[],[f34514]) ).
fof(f34539,plain,
! [X0,X1,X2,X3] :
( k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(ennf_transformation,[],[f2106]) ).
fof(f34540,plain,
! [X0,X1,X2,X3] :
( k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(flattening,[],[f34539]) ).
fof(f34541,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(f34542,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,[],[f34541]) ).
fof(f34573,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(f34574,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,[],[f34573]) ).
fof(f34575,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(f34576,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,[],[f34575]) ).
fof(f34579,plain,
! [X0] :
( ! [X1] :
( l1_pre_topc(X1)
| ~ m2_tsp_1(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34364]) ).
fof(f34592,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(f34593,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,[],[f34592]) ).
fof(f34623,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| u1_struct_0(X1) != X3
| ? [X4] :
( k5_subset_1(u1_struct_0(X0),X3,k4_tex_4(X0,X4)) != k1_struct_0(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X4))
& m1_subset_1(X4,u1_struct_0(X0)) )
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34413]) ).
fof(f34624,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| u1_struct_0(X1) != X3
| ? [X4] :
( k5_subset_1(u1_struct_0(X0),X3,k4_tex_4(X0,X4)) != k1_struct_0(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X4))
& m1_subset_1(X4,u1_struct_0(X0)) )
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f34623]) ).
fof(f34627,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(f34628,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,[],[f34627]) ).
fof(f34631,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(f34632,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,[],[f34631]) ).
fof(f34633,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(f34634,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,[],[f34633]) ).
fof(f34817,plain,
! [X0,X1,X2] :
( k4_relset_1(X0,X1,X2) = k1_relat_1(X2)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1495]) ).
fof(f35650,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(f35651,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,[],[f35650]) ).
fof(f35706,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(f35707,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,[],[f35706]) ).
fof(f35970,plain,
! [X0,X1,X2,X3] :
( r2_hidden(k1_funct_1(X3,X2),X1)
| ~ r2_hidden(X2,k4_relset_1(X0,X1,X3))
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X3,X0,X1) ),
inference(ennf_transformation,[],[f1543]) ).
fof(f35971,plain,
! [X0,X1,X2,X3] :
( r2_hidden(k1_funct_1(X3,X2),X1)
| ~ r2_hidden(X2,k4_relset_1(X0,X1,X3))
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X3,X0,X1) ),
inference(flattening,[],[f35970]) ).
fof(f36447,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k1_relat_1(X2) = k2_pre_topc(X0)
& r1_tarski(k2_relat_1(X2),k2_pre_topc(X1)) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_struct_0(X1) )
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f18585]) ).
fof(f36448,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k1_relat_1(X2) = k2_pre_topc(X0)
& r1_tarski(k2_relat_1(X2),k2_pre_topc(X1)) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_struct_0(X1) )
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f36447]) ).
fof(f36479,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f18263]) ).
fof(f37459,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f18318]) ).
fof(f37460,plain,
! [X0] :
( ( v3_struct_0(X0)
<=> v1_xboole_0(u1_struct_0(X0)) )
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f17598]) ).
fof(f37791,plain,
( ( ~ v1_funct_1(sK86)
| ~ v1_funct_2(sK86,u1_struct_0(sK84),u1_struct_0(sK85))
| ~ v5_pre_topc(sK86,sK84,sK85)
| ~ m2_relset_1(sK86,u1_struct_0(sK84),u1_struct_0(sK85)) )
& ! [X3] :
( r2_hidden(k8_funct_2(u1_struct_0(sK84),u1_struct_0(sK85),sK86,X3),k4_tex_4(sK84,X3))
| ~ m1_subset_1(X3,u1_struct_0(sK84)) )
& v1_funct_1(sK86)
& v1_funct_2(sK86,u1_struct_0(sK84),u1_struct_0(sK85))
& m2_relset_1(sK86,u1_struct_0(sK84),u1_struct_0(sK85))
& ~ v3_struct_0(sK85)
& v2_tsp_2(sK85,sK84)
& m2_tsp_1(sK85,sK84)
& ~ v3_struct_0(sK84)
& v2_pre_topc(sK84)
& l1_pre_topc(sK84) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK84,sK85,sK86]),skolemize(X0,sK84),skolemize(X1,sK85),skolemize(X2,sK86)],[f34505]) ).
fof(f37831,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,[],[f34574]) ).
fof(f37832,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,[],[f37831]) ).
fof(f37833,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,[],[f37832]) ).
fof(f37834,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(sK110(X0,X1)),u1_pre_topc(sK110(X0,X1)))
& m2_tsp_1(X1,sK110(X0,X1))
& ~ v3_struct_0(sK110(X0,X1))
& v2_t_0topsp(sK110(X0,X1))
& m2_tsp_1(sK110(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,[sK110]),skolemize(X2,sK110(X0,X1))],[f37833]) ).
fof(f37839,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,[],[f34593]) ).
fof(f37864,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| u1_struct_0(X1) != X3
| ( k5_subset_1(u1_struct_0(X0),X3,k4_tex_4(X0,sK127(X0,X1,X2,X3))) != k1_struct_0(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,sK127(X0,X1,X2,X3)))
& m1_subset_1(sK127(X0,X1,X2,X3),u1_struct_0(X0)) )
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK127]),skolemize(X4,sK127(X0,X1,X2,X3))],[f34624]) ).
fof(f37868,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,[],[f34628]) ).
fof(f37869,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,[],[f37868]) ).
fof(f37870,plain,
! [X0] :
( ! [X1] :
( ( ( v1_tsp_1(X1,X0)
| ( k1_struct_0(X0,sK130(X0,X1)) != k5_subset_1(u1_struct_0(X0),X1,k4_tex_4(X0,sK130(X0,X1)))
& r2_hidden(sK130(X0,X1),X1)
& m1_subset_1(sK130(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,[sK130]),skolemize(X2,sK130(X0,X1))],[f37869]) ).
fof(f37967,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(f38295,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,[],[f35707]) ).
fof(f39054,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,[],[f37460]) ).
fof(f39116,plain,
l1_pre_topc(sK84),
inference(cnf_transformation,[],[f37791]) ).
fof(f39117,plain,
v2_pre_topc(sK84),
inference(cnf_transformation,[],[f37791]) ).
fof(f39118,plain,
~ v3_struct_0(sK84),
inference(cnf_transformation,[],[f37791]) ).
fof(f39119,plain,
m2_tsp_1(sK85,sK84),
inference(cnf_transformation,[],[f37791]) ).
fof(f39120,plain,
v2_tsp_2(sK85,sK84),
inference(cnf_transformation,[],[f37791]) ).
fof(f39121,plain,
~ v3_struct_0(sK85),
inference(cnf_transformation,[],[f37791]) ).
fof(f39122,plain,
m2_relset_1(sK86,u1_struct_0(sK84),u1_struct_0(sK85)),
inference(cnf_transformation,[],[f37791]) ).
fof(f39123,plain,
v1_funct_2(sK86,u1_struct_0(sK84),u1_struct_0(sK85)),
inference(cnf_transformation,[],[f37791]) ).
fof(f39124,plain,
v1_funct_1(sK86),
inference(cnf_transformation,[],[f37791]) ).
fof(f39125,plain,
! [X3] :
( r2_hidden(k8_funct_2(u1_struct_0(sK84),u1_struct_0(sK85),sK86,X3),k4_tex_4(sK84,X3))
| ~ m1_subset_1(X3,u1_struct_0(sK84)) ),
inference(cnf_transformation,[],[f37791]) ).
fof(f39126,plain,
( ~ v1_funct_1(sK86)
| ~ v1_funct_2(sK86,u1_struct_0(sK84),u1_struct_0(sK85))
| ~ v5_pre_topc(sK86,sK84,sK85)
| ~ m2_relset_1(sK86,u1_struct_0(sK84),u1_struct_0(sK85)) ),
inference(cnf_transformation,[],[f37791]) ).
fof(f39137,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(cnf_transformation,[],[f34513]) ).
fof(f39138,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f34515]) ).
fof(f39185,plain,
! [X2,X3,X0,X1] :
( k1_funct_1(X2,X3) = k8_funct_2(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) ),
inference(cnf_transformation,[],[f34540]) ).
fof(f39186,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,[],[f34542]) ).
fof(f39243,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,[],[f37834]) ).
fof(f39249,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,[],[f34576]) ).
fof(f39253,plain,
! [X0,X1] :
( ~ m2_tsp_1(X1,X0)
| l1_pre_topc(X1)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f34579]) ).
fof(f39270,plain,
! [X2,X0,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(cnf_transformation,[],[f37839]) ).
fof(f39356,plain,
! [X2,X3,X0,X1] :
( u1_struct_0(X1) != X3
| v5_pre_topc(X2,X0,X1)
| m1_subset_1(sK127(X0,X1,X2,X3),u1_struct_0(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f37864]) ).
fof(f39357,plain,
! [X2,X3,X0,X1] :
( ~ v2_pre_topc(X0)
| u1_struct_0(X1) != X3
| k5_subset_1(u1_struct_0(X0),X3,k4_tex_4(X0,sK127(X0,X1,X2,X3))) != k1_struct_0(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,sK127(X0,X1,X2,X3)))
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| v5_pre_topc(X2,X0,X1)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f37864]) ).
fof(f39367,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,[],[f37870]) ).
fof(f39378,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,[],[f34632]) ).
fof(f39379,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,[],[f34634]) ).
fof(f39687,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| k1_relat_1(X2) = k4_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f34817]) ).
fof(f39689,plain,
! [X2,X0,X1] :
( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f37967]) ).
fof(f41134,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,[],[f35651]) ).
fof(f41179,plain,
! [X2,X0,X1] :
( k2_tex_4(X0,X1) = k2_tex_4(X0,X2)
| ~ 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(cnf_transformation,[],[f38295]) ).
fof(f41180,plain,
! [X2,X0,X1] :
( ~ l1_pre_topc(X0)
| 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)
| r2_hidden(X2,k2_tex_4(X0,X1)) ),
inference(cnf_transformation,[],[f38295]) ).
fof(f41617,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_1(X3)
| ~ r2_hidden(X2,k4_relset_1(X0,X1,X3))
| r2_hidden(k1_funct_1(X3,X2),X1)
| ~ m2_relset_1(X3,X0,X1) ),
inference(cnf_transformation,[],[f35971]) ).
fof(f42288,plain,
! [X0] : k1_tarski(X0) = k2_tarski(X0,X0),
inference(cnf_transformation,[],[f258]) ).
fof(f42301,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| k1_relat_1(X2) = k2_pre_topc(X0)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f36448]) ).
fof(f42334,plain,
! [X0] :
( u1_struct_0(X0) = k2_pre_topc(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f36479]) ).
fof(f44136,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f37459]) ).
fof(f44139,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f39054]) ).
fof(f44683,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,[],[f41134,f42288]) ).
fof(f45218,definition,
sF844 = u1_struct_0(sK84),
introduced(definition,[new_symbols(definition,[sF844])],[function_definition]) ).
fof(f45219,plain,
u1_struct_0(sK84) = sF844,
inference(reorient_equations,[],[f45218]) ).
fof(f45220,definition,
sF845 = u1_struct_0(sK85),
introduced(definition,[new_symbols(definition,[sF845])],[function_definition]) ).
fof(f45221,plain,
u1_struct_0(sK85) = sF845,
inference(reorient_equations,[],[f45220]) ).
fof(f45222,plain,
( ~ v1_funct_1(sK86)
| ~ v1_funct_2(sK86,sF844,sF845)
| ~ v5_pre_topc(sK86,sK84,sK85)
| ~ m2_relset_1(sK86,sF844,sF845) ),
inference(definition_folding,[],[f39126,f45221,f45219,f45221,f45219]) ).
fof(f45223,definition,
! [X3] : sF846(X3) = k8_funct_2(sF844,sF845,sK86,X3),
introduced(definition,[new_symbols(definition,[sF846])],[function_definition]) ).
fof(f45224,plain,
! [X3] : k8_funct_2(sF844,sF845,sK86,X3) = sF846(X3),
inference(reorient_equations,[],[f45223]) ).
fof(f45225,definition,
! [X3] : sF847(X3) = k4_tex_4(sK84,X3),
introduced(definition,[new_symbols(definition,[sF847])],[function_definition]) ).
fof(f45226,plain,
! [X3] : k4_tex_4(sK84,X3) = sF847(X3),
inference(reorient_equations,[],[f45225]) ).
fof(f45227,plain,
! [X3] :
( r2_hidden(sF846(X3),sF847(X3))
| ~ m1_subset_1(X3,sF844) ),
inference(definition_folding,[],[f39125,f45219,f45226,f45224,f45221,f45219]) ).
fof(f45228,plain,
v1_funct_2(sK86,sF844,sF845),
inference(definition_folding,[],[f39123,f45221,f45219]) ).
fof(f45229,plain,
m2_relset_1(sK86,sF844,sF845),
inference(definition_folding,[],[f39122,f45221,f45219]) ).
fof(f45332,definition,
( spl848_18
<=> m2_relset_1(sK86,sF844,sF845) ),
introduced(definition,[new_symbols(definition,[spl848_18])],[avatar_definition]) ).
fof(f45336,definition,
( spl848_19
<=> v5_pre_topc(sK86,sK84,sK85) ),
introduced(definition,[new_symbols(definition,[spl848_19])],[avatar_definition]) ).
fof(f45340,definition,
( spl848_20
<=> v1_funct_2(sK86,sF844,sF845) ),
introduced(definition,[new_symbols(definition,[spl848_20])],[avatar_definition]) ).
fof(f45344,definition,
( spl848_21
<=> v1_funct_1(sK86) ),
introduced(definition,[new_symbols(definition,[spl848_21])],[avatar_definition]) ).
fof(f45345,plain,
( v1_funct_1(sK86)
| ~ spl848_21 ),
inference(avatar_component_clause,[],[f45344]) ).
fof(f45347,plain,
( ~ spl848_18
| ~ spl848_19
| ~ spl848_20
| ~ spl848_21 ),
inference(avatar_split_clause,[],[f45222,f45344,f45340,f45336,f45332]) ).
fof(f45348,plain,
spl848_20,
inference(avatar_split_clause,[],[f45228,f45340]) ).
fof(f45349,plain,
spl848_18,
inference(avatar_split_clause,[],[f45229,f45332]) ).
fof(f45350,plain,
spl848_21,
inference(avatar_split_clause,[],[f39124,f45344]) ).
fof(f45351,plain,
! [X0] :
( m1_subset_1(sF847(X0),k1_zfmisc_1(u1_struct_0(sK84)))
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84)
| ~ m1_subset_1(X0,u1_struct_0(sK84)) ),
inference(superposition,[],[f39379,f45226]) ).
fof(f45356,definition,
( spl848_22
<=> l1_pre_topc(sK85) ),
introduced(definition,[new_symbols(definition,[spl848_22])],[avatar_definition]) ).
fof(f45364,definition,
( spl848_24
<=> v3_struct_0(sK85) ),
introduced(definition,[new_symbols(definition,[spl848_24])],[avatar_definition]) ).
fof(f45365,plain,
( ~ v3_struct_0(sK85)
| spl848_24 ),
inference(avatar_component_clause,[],[f45364]) ).
fof(f45371,plain,
! [X0] :
( m1_subset_1(sF847(X0),k1_zfmisc_1(sF844))
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84)
| ~ m1_subset_1(X0,u1_struct_0(sK84)) ),
inference(forward_demodulation,[],[f45351,f45219]) ).
fof(f45373,definition,
( spl848_26
<=> l1_pre_topc(sK84) ),
introduced(definition,[new_symbols(definition,[spl848_26])],[avatar_definition]) ).
fof(f45374,plain,
( l1_pre_topc(sK84)
| ~ spl848_26 ),
inference(avatar_component_clause,[],[f45373]) ).
fof(f45377,definition,
( spl848_27
<=> v2_pre_topc(sK84) ),
introduced(definition,[new_symbols(definition,[spl848_27])],[avatar_definition]) ).
fof(f45378,plain,
( v2_pre_topc(sK84)
| ~ spl848_27 ),
inference(avatar_component_clause,[],[f45377]) ).
fof(f45381,definition,
( spl848_28
<=> v3_struct_0(sK84) ),
introduced(definition,[new_symbols(definition,[spl848_28])],[avatar_definition]) ).
fof(f45382,plain,
( ~ v3_struct_0(sK84)
| spl848_28 ),
inference(avatar_component_clause,[],[f45381]) ).
fof(f45385,definition,
( spl848_29
<=> ! [X0] :
( m1_subset_1(sF847(X0),k1_zfmisc_1(sF844))
| ~ m1_subset_1(X0,sF844) ) ),
introduced(definition,[new_symbols(definition,[spl848_29])],[avatar_definition]) ).
fof(f45386,plain,
( ! [X0] :
( m1_subset_1(sF847(X0),k1_zfmisc_1(sF844))
| ~ m1_subset_1(X0,sF844) )
| ~ spl848_29 ),
inference(avatar_component_clause,[],[f45385]) ).
fof(f45388,plain,
! [X0] :
( ~ m1_subset_1(X0,sF844)
| m1_subset_1(sF847(X0),k1_zfmisc_1(sF844))
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84) ),
inference(forward_demodulation,[],[f45371,f45219]) ).
fof(f45389,plain,
( ~ spl848_26
| ~ spl848_27
| spl848_28
| spl848_29 ),
inference(avatar_split_clause,[],[f45388,f45385,f45381,f45377,f45373]) ).
fof(f45392,plain,
spl848_27,
inference(avatar_split_clause,[],[f39117,f45377]) ).
fof(f45395,plain,
spl848_26,
inference(avatar_split_clause,[],[f39116,f45373]) ).
fof(f45398,plain,
~ spl848_28,
inference(avatar_split_clause,[],[f39118,f45381]) ).
fof(f45399,plain,
! [X0] :
( m1_subset_1(sF846(X0),sF845)
| v1_xboole_0(sF844)
| ~ v1_funct_1(sK86)
| ~ v1_funct_2(sK86,sF844,sF845)
| ~ m1_relset_1(sK86,sF844,sF845)
| ~ m1_subset_1(X0,sF844) ),
inference(superposition,[],[f39186,f45224]) ).
fof(f45401,definition,
( spl848_30
<=> m1_relset_1(sK86,sF844,sF845) ),
introduced(definition,[new_symbols(definition,[spl848_30])],[avatar_definition]) ).
fof(f45402,plain,
( m1_relset_1(sK86,sF844,sF845)
| ~ spl848_30 ),
inference(avatar_component_clause,[],[f45401]) ).
fof(f45403,plain,
( ~ m1_relset_1(sK86,sF844,sF845)
| spl848_30 ),
inference(avatar_component_clause,[],[f45401]) ).
fof(f45405,definition,
( spl848_31
<=> v1_xboole_0(sF844) ),
introduced(definition,[new_symbols(definition,[spl848_31])],[avatar_definition]) ).
fof(f45406,plain,
( ~ v1_xboole_0(sF844)
| spl848_31 ),
inference(avatar_component_clause,[],[f45405]) ).
fof(f45409,definition,
( spl848_32
<=> ! [X0] :
( m1_subset_1(sF846(X0),sF845)
| ~ m1_subset_1(X0,sF844) ) ),
introduced(definition,[new_symbols(definition,[spl848_32])],[avatar_definition]) ).
fof(f45410,plain,
( ! [X0] :
( m1_subset_1(sF846(X0),sF845)
| ~ m1_subset_1(X0,sF844) )
| ~ spl848_32 ),
inference(avatar_component_clause,[],[f45409]) ).
fof(f45411,plain,
( ~ spl848_30
| ~ spl848_20
| ~ spl848_21
| spl848_31
| spl848_32 ),
inference(avatar_split_clause,[],[f45399,f45409,f45405,f45344,f45340,f45401]) ).
fof(f45412,plain,
( l1_pre_topc(sK85)
| ~ l1_pre_topc(sK84) ),
inference(resolution,[],[f39253,f39119]) ).
fof(f45413,plain,
( ~ spl848_26
| spl848_22 ),
inference(avatar_split_clause,[],[f45412,f45356,f45373]) ).
fof(f45414,plain,
! [X0] :
( sF846(X0) = k1_funct_1(sK86,X0)
| v1_xboole_0(sF844)
| ~ v1_funct_1(sK86)
| ~ v1_funct_2(sK86,sF844,sF845)
| ~ m1_relset_1(sK86,sF844,sF845)
| ~ m1_subset_1(X0,sF844) ),
inference(superposition,[],[f39185,f45224]) ).
fof(f45419,definition,
( spl848_33
<=> ! [X0] :
( sF846(X0) = k1_funct_1(sK86,X0)
| ~ m1_subset_1(X0,sF844) ) ),
introduced(definition,[new_symbols(definition,[spl848_33])],[avatar_definition]) ).
fof(f45420,plain,
( ! [X0] :
( sF846(X0) = k1_funct_1(sK86,X0)
| ~ m1_subset_1(X0,sF844) )
| ~ spl848_33 ),
inference(avatar_component_clause,[],[f45419]) ).
fof(f45422,plain,
( ~ spl848_30
| ~ spl848_20
| ~ spl848_21
| spl848_31
| spl848_33 ),
inference(avatar_split_clause,[],[f45414,f45419,f45405,f45344,f45340,f45401]) ).
fof(f45423,plain,
! [X0] :
( m1_subset_1(sF845,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_tsp_1(sK85,X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(superposition,[],[f39249,f45221]) ).
fof(f45437,plain,
~ spl848_24,
inference(avatar_split_clause,[],[f39121,f45364]) ).
fof(f45458,plain,
( ~ m2_relset_1(sK86,sF844,sF845)
| spl848_30 ),
inference(resolution,[],[f45403,f39689]) ).
fof(f45459,plain,
( ~ spl848_18
| spl848_30 ),
inference(avatar_split_clause,[],[f45458,f45401,f45332]) ).
fof(f45461,plain,
( m1_subset_1(sF845,k1_zfmisc_1(sF844))
| ~ m2_tsp_1(sK85,sK84)
| v3_struct_0(sK84)
| ~ l1_pre_topc(sK84) ),
inference(superposition,[],[f45423,f45219]) ).
fof(f45463,definition,
( spl848_40
<=> m2_tsp_1(sK85,sK84) ),
introduced(definition,[new_symbols(definition,[spl848_40])],[avatar_definition]) ).
fof(f45467,definition,
( spl848_41
<=> m1_subset_1(sF845,k1_zfmisc_1(sF844)) ),
introduced(definition,[new_symbols(definition,[spl848_41])],[avatar_definition]) ).
fof(f45469,plain,
( m1_subset_1(sF845,k1_zfmisc_1(sF844))
| ~ spl848_41 ),
inference(avatar_component_clause,[],[f45467]) ).
fof(f45470,plain,
( ~ spl848_26
| spl848_28
| ~ spl848_40
| spl848_41 ),
inference(avatar_split_clause,[],[f45461,f45467,f45463,f45381,f45373]) ).
fof(f45578,definition,
( spl848_58
<=> v2_tsp_2(sK85,sK84) ),
introduced(definition,[new_symbols(definition,[spl848_58])],[avatar_definition]) ).
fof(f45579,plain,
( v2_tsp_2(sK85,sK84)
| ~ spl848_58 ),
inference(avatar_component_clause,[],[f45578]) ).
fof(f45597,plain,
( v2_t_0topsp(sK85)
| v3_struct_0(sK85)
| ~ m2_tsp_1(sK85,sK84)
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84) ),
inference(resolution,[],[f39243,f39120]) ).
fof(f45599,definition,
( spl848_62
<=> v2_t_0topsp(sK85) ),
introduced(definition,[new_symbols(definition,[spl848_62])],[avatar_definition]) ).
fof(f45601,plain,
( v2_t_0topsp(sK85)
| ~ spl848_62 ),
inference(avatar_component_clause,[],[f45599]) ).
fof(f45602,plain,
( ~ spl848_26
| ~ spl848_27
| spl848_28
| ~ spl848_40
| spl848_24
| spl848_62 ),
inference(avatar_split_clause,[],[f45597,f45599,f45364,f45463,f45381,f45377,f45373]) ).
fof(f45606,definition,
( spl848_63
<=> l1_struct_0(sK84) ),
introduced(definition,[new_symbols(definition,[spl848_63])],[avatar_definition]) ).
fof(f45608,plain,
( ~ l1_struct_0(sK84)
| spl848_63 ),
inference(avatar_component_clause,[],[f45606]) ).
fof(f45614,definition,
( spl848_65
<=> l1_struct_0(sK85) ),
introduced(definition,[new_symbols(definition,[spl848_65])],[avatar_definition]) ).
fof(f45616,plain,
( ~ l1_struct_0(sK85)
| spl848_65 ),
inference(avatar_component_clause,[],[f45614]) ).
fof(f45621,plain,
( ~ l1_pre_topc(sK85)
| spl848_65 ),
inference(resolution,[],[f45616,f44136]) ).
fof(f45622,plain,
( ~ spl848_22
| spl848_65 ),
inference(avatar_split_clause,[],[f45621,f45614,f45356]) ).
fof(f45623,plain,
( ~ l1_pre_topc(sK84)
| spl848_63 ),
inference(resolution,[],[f45608,f44136]) ).
fof(f45624,plain,
( ~ spl848_26
| spl848_63 ),
inference(avatar_split_clause,[],[f45623,f45606,f45373]) ).
fof(f45643,plain,
! [X2,X0,X1] :
( m1_subset_1(sK127(X1,X2,X0,u1_struct_0(X2)),u1_struct_0(X1))
| v5_pre_topc(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))
| ~ 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,[],[f39356]) ).
fof(f45652,plain,
! [X0,X1] :
( m1_subset_1(sK127(X0,sK85,X1,sF845),u1_struct_0(X0))
| v5_pre_topc(X1,X0,sK85)
| ~ m1_subset_1(sF845,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),sF845)
| ~ m2_relset_1(X1,u1_struct_0(X0),sF845)
| v3_struct_0(sK85)
| ~ v2_tsp_2(sK85,X0)
| ~ m2_tsp_1(sK85,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(superposition,[],[f45643,f45221]) ).
fof(f45665,definition,
( spl848_71
<=> ! [X0,X1] :
( m1_subset_1(sK127(X0,sK85,X1,sF845),u1_struct_0(X0))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ m2_tsp_1(sK85,X0)
| ~ v2_tsp_2(sK85,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),sF845)
| ~ v1_funct_2(X1,u1_struct_0(X0),sF845)
| ~ v1_funct_1(X1)
| ~ m1_subset_1(sF845,k1_zfmisc_1(u1_struct_0(X0)))
| v5_pre_topc(X1,X0,sK85) ) ),
introduced(definition,[new_symbols(definition,[spl848_71])],[avatar_definition]) ).
fof(f45666,plain,
( ! [X0,X1] :
( m1_subset_1(sK127(X0,sK85,X1,sF845),u1_struct_0(X0))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ m2_tsp_1(sK85,X0)
| ~ v2_tsp_2(sK85,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),sF845)
| ~ v1_funct_2(X1,u1_struct_0(X0),sF845)
| ~ v1_funct_1(X1)
| ~ m1_subset_1(sF845,k1_zfmisc_1(u1_struct_0(X0)))
| v5_pre_topc(X1,X0,sK85) )
| ~ spl848_71 ),
inference(avatar_component_clause,[],[f45665]) ).
fof(f45667,plain,
( spl848_24
| spl848_71 ),
inference(avatar_split_clause,[],[f45652,f45665,f45364]) ).
fof(f45669,plain,
( ! [X0] :
( m1_subset_1(sK127(sK84,sK85,X0,sF845),sF844)
| ~ l1_pre_topc(sK84)
| ~ v2_pre_topc(sK84)
| v3_struct_0(sK84)
| ~ m2_tsp_1(sK85,sK84)
| ~ v2_tsp_2(sK85,sK84)
| ~ m2_relset_1(X0,sF844,sF845)
| ~ v1_funct_2(X0,sF844,sF845)
| ~ v1_funct_1(X0)
| ~ m1_subset_1(sF845,k1_zfmisc_1(sF844))
| v5_pre_topc(X0,sK84,sK85) )
| ~ spl848_71 ),
inference(superposition,[],[f45666,f45219]) ).
fof(f45671,definition,
( spl848_72
<=> ! [X0] :
( m1_subset_1(sK127(sK84,sK85,X0,sF845),sF844)
| v5_pre_topc(X0,sK84,sK85)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF844,sF845)
| ~ m2_relset_1(X0,sF844,sF845) ) ),
introduced(definition,[new_symbols(definition,[spl848_72])],[avatar_definition]) ).
fof(f45672,plain,
( ! [X0] :
( m1_subset_1(sK127(sK84,sK85,X0,sF845),sF844)
| v5_pre_topc(X0,sK84,sK85)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF844,sF845)
| ~ m2_relset_1(X0,sF844,sF845) )
| ~ spl848_72 ),
inference(avatar_component_clause,[],[f45671]) ).
fof(f45673,plain,
( ~ spl848_41
| ~ spl848_58
| ~ spl848_40
| spl848_28
| ~ spl848_27
| ~ spl848_26
| spl848_72
| ~ spl848_71 ),
inference(avatar_split_clause,[],[f45669,f45665,f45671,f45373,f45377,f45381,f45463,f45578,f45467]) ).
fof(f45702,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF847(X1))
| m1_subset_1(X0,sF844)
| ~ m1_subset_1(X1,sF844) )
| ~ spl848_29 ),
inference(resolution,[],[f39137,f45386]) ).
fof(f45708,plain,
( ! [X0] :
( m1_subset_1(sF846(X0),sF844)
| ~ m1_subset_1(X0,sF844)
| ~ m1_subset_1(X0,sF844) )
| ~ spl848_29 ),
inference(resolution,[],[f45702,f45227]) ).
fof(f45709,plain,
( ! [X0] :
( m1_subset_1(sF846(X0),sF844)
| ~ m1_subset_1(X0,sF844) )
| ~ spl848_29 ),
inference(duplicate_literal_removal,[],[f45708]) ).
fof(f45718,definition,
( spl848_74
<=> ! [X0] :
( ~ r2_hidden(X0,sF845)
| m1_subset_1(X0,sF844) ) ),
introduced(definition,[new_symbols(definition,[spl848_74])],[avatar_definition]) ).
fof(f45719,plain,
( ! [X0] :
( m1_subset_1(X0,sF844)
| ~ r2_hidden(X0,sF845) )
| ~ spl848_74 ),
inference(avatar_component_clause,[],[f45718]) ).
fof(f45735,plain,
spl848_40,
inference(avatar_split_clause,[],[f39119,f45463]) ).
fof(f45737,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF845)
| m1_subset_1(X0,sF844) )
| ~ spl848_41 ),
inference(resolution,[],[f45469,f39137]) ).
fof(f45738,plain,
( spl848_74
| ~ spl848_41 ),
inference(avatar_split_clause,[],[f45737,f45467,f45718]) ).
fof(f45741,plain,
spl848_58,
inference(avatar_split_clause,[],[f39120,f45578]) ).
fof(f45777,plain,
! [X2,X0,X1] :
( k2_tex_4(X0,X2) = k4_tex_4(X0,X1)
| ~ r2_hidden(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,[],[f41179,f39378]) ).
fof(f45782,plain,
! [X2,X0,X1] :
( k2_tex_4(X0,X1) = k4_tex_4(X0,X2)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ r2_hidden(X1,k2_tex_4(X0,X2))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(superposition,[],[f39378,f41179]) ).
fof(f45791,plain,
! [X2,X0,X1] :
( k2_tex_4(X0,X1) = k4_tex_4(X0,X2)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ r2_hidden(X1,k2_tex_4(X0,X2))
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(duplicate_literal_removal,[],[f45782]) ).
fof(f45796,plain,
! [X2,X0,X1] :
( k2_tex_4(X0,X2) = k4_tex_4(X0,X1)
| ~ r2_hidden(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)
| ~ v2_pre_topc(X0) ),
inference(duplicate_literal_removal,[],[f45777]) ).
fof(f45893,plain,
! [X2,X3,X0,X1] :
( k2_tex_4(X0,X1) = k4_tex_4(X0,X3)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ r2_hidden(X2,k2_tex_4(X0,X3))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ r2_hidden(X1,k2_tex_4(X0,X2))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(superposition,[],[f45791,f41179]) ).
fof(f45894,plain,
! [X2,X0,X1] :
( k4_tex_4(X0,X1) = k4_tex_4(X0,X2)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ r2_hidden(X1,k2_tex_4(X0,X2))
| ~ m1_subset_1(X1,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(superposition,[],[f45791,f39378]) ).
fof(f45923,plain,
! [X2,X0,X1] :
( k4_tex_4(X0,X1) = k4_tex_4(X0,X2)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ r2_hidden(X1,k2_tex_4(X0,X2))
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(duplicate_literal_removal,[],[f45894]) ).
fof(f45924,plain,
! [X2,X3,X0,X1] :
( ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| k2_tex_4(X0,X1) = k4_tex_4(X0,X3)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ r2_hidden(X2,k2_tex_4(X0,X3))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ r2_hidden(X1,k2_tex_4(X0,X2))
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(duplicate_literal_removal,[],[f45893]) ).
fof(f45940,plain,
! [X0,X1] :
( sF847(X0) = k4_tex_4(sK84,X1)
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84)
| ~ m1_subset_1(X1,u1_struct_0(sK84))
| ~ r2_hidden(X0,k2_tex_4(sK84,X1))
| ~ m1_subset_1(X0,u1_struct_0(sK84)) ),
inference(superposition,[],[f45923,f45226]) ).
fof(f45983,plain,
! [X0,X1] :
( sF847(X0) = sF847(X1)
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84)
| ~ m1_subset_1(X1,u1_struct_0(sK84))
| ~ r2_hidden(X0,k2_tex_4(sK84,X1))
| ~ m1_subset_1(X0,u1_struct_0(sK84)) ),
inference(forward_demodulation,[],[f45940,f45226]) ).
fof(f45987,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,sF844)
| sF847(X0) = sF847(X1)
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84)
| ~ r2_hidden(X0,k2_tex_4(sK84,X1))
| ~ m1_subset_1(X0,u1_struct_0(sK84)) ),
inference(forward_demodulation,[],[f45983,f45219]) ).
fof(f45991,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,sF844)
| ~ m1_subset_1(X1,sF844)
| sF847(X0) = sF847(X1)
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84)
| ~ r2_hidden(X0,k2_tex_4(sK84,X1)) ),
inference(forward_demodulation,[],[f45987,f45219]) ).
fof(f45993,definition,
( spl848_83
<=> ! [X0,X1] :
( ~ m1_subset_1(X0,sF844)
| ~ r2_hidden(X0,k2_tex_4(sK84,X1))
| sF847(X0) = sF847(X1)
| ~ m1_subset_1(X1,sF844) ) ),
introduced(definition,[new_symbols(definition,[spl848_83])],[avatar_definition]) ).
fof(f45994,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,k2_tex_4(sK84,X1))
| ~ m1_subset_1(X0,sF844)
| sF847(X0) = sF847(X1)
| ~ m1_subset_1(X1,sF844) )
| ~ spl848_83 ),
inference(avatar_component_clause,[],[f45993]) ).
fof(f45998,plain,
( ~ spl848_26
| ~ spl848_27
| spl848_28
| spl848_83 ),
inference(avatar_split_clause,[],[f45991,f45993,f45381,f45377,f45373]) ).
fof(f46001,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X1,k4_tex_4(sK84,X0))
| ~ m1_subset_1(X1,sF844)
| sF847(X1) = sF847(X2)
| ~ m1_subset_1(X2,sF844)
| ~ r2_hidden(X2,k4_tex_4(sK84,X0))
| ~ m1_subset_1(X2,u1_struct_0(sK84))
| ~ m1_subset_1(X0,u1_struct_0(sK84))
| v3_struct_0(sK84)
| ~ l1_pre_topc(sK84)
| ~ v2_pre_topc(sK84) )
| ~ spl848_83 ),
inference(superposition,[],[f45994,f45796]) ).
fof(f46004,plain,
( ! [X0,X1] :
( ~ r2_hidden(X1,k4_tex_4(sK84,X0))
| ~ m1_subset_1(X1,sF844)
| sF847(X0) = sF847(X1)
| ~ m1_subset_1(X0,sF844)
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84)
| ~ m1_subset_1(X0,u1_struct_0(sK84)) )
| ~ spl848_83 ),
inference(superposition,[],[f45994,f39378]) ).
fof(f46005,plain,
( ! [X0,X1] :
( ~ r2_hidden(X1,sF847(X0))
| ~ m1_subset_1(X1,sF844)
| sF847(X0) = sF847(X1)
| ~ m1_subset_1(X0,sF844)
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84)
| ~ m1_subset_1(X0,u1_struct_0(sK84)) )
| ~ spl848_83 ),
inference(forward_demodulation,[],[f46004,f45226]) ).
fof(f46009,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X1,sF847(X0))
| ~ m1_subset_1(X1,sF844)
| sF847(X1) = sF847(X2)
| ~ m1_subset_1(X2,sF844)
| ~ r2_hidden(X2,k4_tex_4(sK84,X0))
| ~ m1_subset_1(X2,u1_struct_0(sK84))
| ~ m1_subset_1(X0,u1_struct_0(sK84))
| v3_struct_0(sK84)
| ~ l1_pre_topc(sK84)
| ~ v2_pre_topc(sK84) )
| ~ spl848_83 ),
inference(forward_demodulation,[],[f46001,f45226]) ).
fof(f46012,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF844)
| ~ r2_hidden(X1,sF847(X0))
| ~ m1_subset_1(X1,sF844)
| sF847(X0) = sF847(X1)
| ~ m1_subset_1(X0,sF844)
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84) )
| ~ spl848_83 ),
inference(forward_demodulation,[],[f46005,f45219]) ).
fof(f46013,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF844)
| ~ r2_hidden(X1,sF847(X0))
| ~ m1_subset_1(X1,sF844)
| sF847(X0) = sF847(X1)
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84) )
| ~ spl848_83 ),
inference(duplicate_literal_removal,[],[f46012]) ).
fof(f46017,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X2,sF847(X0))
| ~ r2_hidden(X1,sF847(X0))
| ~ m1_subset_1(X1,sF844)
| sF847(X1) = sF847(X2)
| ~ m1_subset_1(X2,sF844)
| ~ m1_subset_1(X2,u1_struct_0(sK84))
| ~ m1_subset_1(X0,u1_struct_0(sK84))
| v3_struct_0(sK84)
| ~ l1_pre_topc(sK84)
| ~ v2_pre_topc(sK84) )
| ~ spl848_83 ),
inference(forward_demodulation,[],[f46009,f45226]) ).
fof(f46021,definition,
( spl848_84
<=> ! [X0,X1] :
( ~ m1_subset_1(X0,sF844)
| sF847(X0) = sF847(X1)
| ~ m1_subset_1(X1,sF844)
| ~ r2_hidden(X1,sF847(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl848_84])],[avatar_definition]) ).
fof(f46022,plain,
( ! [X0,X1] :
( sF847(X0) = sF847(X1)
| ~ m1_subset_1(X0,sF844)
| ~ m1_subset_1(X1,sF844)
| ~ r2_hidden(X1,sF847(X0)) )
| ~ spl848_84 ),
inference(avatar_component_clause,[],[f46021]) ).
fof(f46023,plain,
( ~ spl848_26
| ~ spl848_27
| spl848_28
| spl848_84
| ~ spl848_83 ),
inference(avatar_split_clause,[],[f46013,f45993,f46021,f45381,f45377,f45373]) ).
fof(f46032,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X2,sF844)
| ~ r2_hidden(X2,sF847(X0))
| ~ r2_hidden(X1,sF847(X0))
| ~ m1_subset_1(X1,sF844)
| sF847(X1) = sF847(X2)
| ~ m1_subset_1(X2,sF844)
| ~ m1_subset_1(X0,u1_struct_0(sK84))
| v3_struct_0(sK84)
| ~ l1_pre_topc(sK84)
| ~ v2_pre_topc(sK84) )
| ~ spl848_83 ),
inference(forward_demodulation,[],[f46017,f45219]) ).
fof(f46033,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X2,sF844)
| ~ r2_hidden(X2,sF847(X0))
| ~ r2_hidden(X1,sF847(X0))
| ~ m1_subset_1(X1,sF844)
| sF847(X1) = sF847(X2)
| ~ m1_subset_1(X0,u1_struct_0(sK84))
| v3_struct_0(sK84)
| ~ l1_pre_topc(sK84)
| ~ v2_pre_topc(sK84) )
| ~ spl848_83 ),
inference(duplicate_literal_removal,[],[f46032]) ).
fof(f46038,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,sF844)
| ~ m1_subset_1(X2,sF844)
| ~ r2_hidden(X2,sF847(X0))
| ~ r2_hidden(X1,sF847(X0))
| ~ m1_subset_1(X1,sF844)
| sF847(X1) = sF847(X2)
| v3_struct_0(sK84)
| ~ l1_pre_topc(sK84)
| ~ v2_pre_topc(sK84) )
| ~ spl848_83 ),
inference(forward_demodulation,[],[f46033,f45219]) ).
fof(f46048,definition,
( spl848_89
<=> ! [X2,X0,X1] :
( ~ m1_subset_1(X0,sF844)
| sF847(X1) = sF847(X2)
| ~ m1_subset_1(X1,sF844)
| ~ r2_hidden(X1,sF847(X0))
| ~ m1_subset_1(X2,sF844)
| ~ r2_hidden(X2,sF847(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl848_89])],[avatar_definition]) ).
fof(f46049,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X2,sF847(X0))
| sF847(X1) = sF847(X2)
| ~ m1_subset_1(X1,sF844)
| ~ r2_hidden(X1,sF847(X0))
| ~ m1_subset_1(X2,sF844)
| ~ m1_subset_1(X0,sF844) )
| ~ spl848_89 ),
inference(avatar_component_clause,[],[f46048]) ).
fof(f46050,plain,
( ~ spl848_27
| ~ spl848_26
| spl848_28
| spl848_89
| ~ spl848_83 ),
inference(avatar_split_clause,[],[f46038,f45993,f46048,f45381,f45373,f45377]) ).
fof(f46259,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,sF844,u1_struct_0(X1))
| ~ v1_funct_1(X0)
| k1_relat_1(X0) = k2_pre_topc(sK84)
| ~ m2_relset_1(X0,sF844,u1_struct_0(X1))
| v3_struct_0(X1)
| ~ l1_struct_0(X1)
| ~ l1_struct_0(sK84) ),
inference(superposition,[],[f42301,f45219]) ).
fof(f46273,definition,
( spl848_101
<=> ! [X0,X1] :
( ~ v1_funct_2(X0,sF844,u1_struct_0(X1))
| ~ l1_struct_0(X1)
| v3_struct_0(X1)
| ~ m2_relset_1(X0,sF844,u1_struct_0(X1))
| k1_relat_1(X0) = k2_pre_topc(sK84)
| ~ v1_funct_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl848_101])],[avatar_definition]) ).
fof(f46274,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X0,sF844,u1_struct_0(X1))
| ~ l1_struct_0(X1)
| v3_struct_0(X1)
| ~ m2_relset_1(X0,sF844,u1_struct_0(X1))
| k1_relat_1(X0) = k2_pre_topc(sK84)
| ~ v1_funct_1(X0) )
| ~ spl848_101 ),
inference(avatar_component_clause,[],[f46273]) ).
fof(f46275,plain,
( ~ spl848_63
| spl848_101 ),
inference(avatar_split_clause,[],[f46259,f46273,f45606]) ).
fof(f46318,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF844,sF845)
| ~ l1_struct_0(sK85)
| v3_struct_0(sK85)
| ~ m2_relset_1(X0,sF844,sF845)
| k1_relat_1(X0) = k2_pre_topc(sK84)
| ~ v1_funct_1(X0) )
| ~ spl848_101 ),
inference(superposition,[],[f46274,f45221]) ).
fof(f46327,definition,
( spl848_108
<=> ! [X0] :
( ~ v1_funct_2(X0,sF844,sF845)
| ~ v1_funct_1(X0)
| k1_relat_1(X0) = k2_pre_topc(sK84)
| ~ m2_relset_1(X0,sF844,sF845) ) ),
introduced(definition,[new_symbols(definition,[spl848_108])],[avatar_definition]) ).
fof(f46328,plain,
( ! [X0] :
( k1_relat_1(X0) = k2_pre_topc(sK84)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF844,sF845)
| ~ m2_relset_1(X0,sF844,sF845) )
| ~ spl848_108 ),
inference(avatar_component_clause,[],[f46327]) ).
fof(f46329,plain,
( spl848_24
| ~ spl848_65
| spl848_108
| ~ spl848_101 ),
inference(avatar_split_clause,[],[f46318,f46273,f46327,f45614,f45364]) ).
fof(f46333,plain,
( ! [X0] :
( k1_relat_1(X0) = u1_struct_0(sK84)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF844,sF845)
| ~ m2_relset_1(X0,sF844,sF845)
| ~ l1_struct_0(sK84) )
| ~ spl848_108 ),
inference(superposition,[],[f46328,f42334]) ).
fof(f46354,plain,
( ! [X0] :
( k1_relat_1(X0) = sF844
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF844,sF845)
| ~ m2_relset_1(X0,sF844,sF845)
| ~ l1_struct_0(sK84) )
| ~ spl848_108 ),
inference(forward_demodulation,[],[f46333,f45219]) ).
fof(f46358,definition,
( spl848_112
<=> ! [X0] :
( k1_relat_1(X0) = sF844
| ~ m2_relset_1(X0,sF844,sF845)
| ~ v1_funct_2(X0,sF844,sF845)
| ~ v1_funct_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl848_112])],[avatar_definition]) ).
fof(f46359,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,sF844,sF845)
| ~ v1_funct_2(X0,sF844,sF845)
| k1_relat_1(X0) = sF844 )
| ~ spl848_112 ),
inference(avatar_component_clause,[],[f46358]) ).
fof(f46361,plain,
( ~ spl848_63
| spl848_112
| ~ spl848_108 ),
inference(avatar_split_clause,[],[f46354,f46327,f46358,f45606]) ).
fof(f46516,plain,
( ~ v1_xboole_0(sF844)
| v3_struct_0(sK84)
| ~ l1_struct_0(sK84) ),
inference(superposition,[],[f44139,f45219]) ).
fof(f46517,plain,
( ~ spl848_63
| spl848_28
| ~ spl848_31 ),
inference(avatar_split_clause,[],[f46516,f45405,f45381,f45606]) ).
fof(f46565,plain,
( ! [X2,X0,X1] :
( u1_struct_0(X0) != X1
| k5_subset_1(u1_struct_0(sK84),X1,k4_tex_4(sK84,sK127(sK84,X0,X2,X1))) != k1_struct_0(X0,k8_funct_2(u1_struct_0(sK84),u1_struct_0(X0),X2,sK127(sK84,X0,X2,X1)))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK84)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK84),u1_struct_0(X0))
| ~ m2_relset_1(X2,u1_struct_0(sK84),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK84)
| ~ m2_tsp_1(X0,sK84)
| v3_struct_0(sK84)
| v5_pre_topc(X2,sK84,X0)
| ~ l1_pre_topc(sK84) )
| ~ spl848_27 ),
inference(resolution,[],[f39357,f45378]) ).
fof(f46566,plain,
( ! [X2,X0,X1] :
( k5_subset_1(sF844,X1,k4_tex_4(sK84,sK127(sK84,X0,X2,X1))) != k1_struct_0(X0,k8_funct_2(sF844,u1_struct_0(X0),X2,sK127(sK84,X0,X2,X1)))
| u1_struct_0(X0) != X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK84)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK84),u1_struct_0(X0))
| ~ m2_relset_1(X2,u1_struct_0(sK84),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK84)
| ~ m2_tsp_1(X0,sK84)
| v3_struct_0(sK84)
| v5_pre_topc(X2,sK84,X0)
| ~ l1_pre_topc(sK84) )
| ~ spl848_27 ),
inference(forward_demodulation,[],[f46565,f45219]) ).
fof(f46567,plain,
( ! [X2,X0,X1] :
( k1_struct_0(X0,k8_funct_2(sF844,u1_struct_0(X0),X2,sK127(sK84,X0,X2,X1))) != k5_subset_1(sF844,X1,sF847(sK127(sK84,X0,X2,X1)))
| u1_struct_0(X0) != X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK84)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK84),u1_struct_0(X0))
| ~ m2_relset_1(X2,u1_struct_0(sK84),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK84)
| ~ m2_tsp_1(X0,sK84)
| v3_struct_0(sK84)
| v5_pre_topc(X2,sK84,X0)
| ~ l1_pre_topc(sK84) )
| ~ spl848_27 ),
inference(forward_demodulation,[],[f46566,f45226]) ).
fof(f46568,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(sF844))
| k1_struct_0(X0,k8_funct_2(sF844,u1_struct_0(X0),X2,sK127(sK84,X0,X2,X1))) != k5_subset_1(sF844,X1,sF847(sK127(sK84,X0,X2,X1)))
| u1_struct_0(X0) != X1
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK84),u1_struct_0(X0))
| ~ m2_relset_1(X2,u1_struct_0(sK84),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK84)
| ~ m2_tsp_1(X0,sK84)
| v3_struct_0(sK84)
| v5_pre_topc(X2,sK84,X0)
| ~ l1_pre_topc(sK84) )
| ~ spl848_27 ),
inference(forward_demodulation,[],[f46567,f45219]) ).
fof(f46569,plain,
( ! [X2,X0,X1] :
( ~ v1_funct_2(X2,sF844,u1_struct_0(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(sF844))
| k1_struct_0(X0,k8_funct_2(sF844,u1_struct_0(X0),X2,sK127(sK84,X0,X2,X1))) != k5_subset_1(sF844,X1,sF847(sK127(sK84,X0,X2,X1)))
| u1_struct_0(X0) != X1
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X2,u1_struct_0(sK84),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK84)
| ~ m2_tsp_1(X0,sK84)
| v3_struct_0(sK84)
| v5_pre_topc(X2,sK84,X0)
| ~ l1_pre_topc(sK84) )
| ~ spl848_27 ),
inference(forward_demodulation,[],[f46568,f45219]) ).
fof(f46570,plain,
( ! [X2,X0,X1] :
( ~ m2_relset_1(X2,sF844,u1_struct_0(X0))
| ~ v1_funct_2(X2,sF844,u1_struct_0(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(sF844))
| k1_struct_0(X0,k8_funct_2(sF844,u1_struct_0(X0),X2,sK127(sK84,X0,X2,X1))) != k5_subset_1(sF844,X1,sF847(sK127(sK84,X0,X2,X1)))
| u1_struct_0(X0) != X1
| ~ v1_funct_1(X2)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK84)
| ~ m2_tsp_1(X0,sK84)
| v3_struct_0(sK84)
| v5_pre_topc(X2,sK84,X0)
| ~ l1_pre_topc(sK84) )
| ~ spl848_27 ),
inference(forward_demodulation,[],[f46569,f45219]) ).
fof(f46572,definition,
( spl848_124
<=> ! [X2,X0,X1] :
( ~ m2_relset_1(X2,sF844,u1_struct_0(X0))
| v5_pre_topc(X2,sK84,X0)
| ~ m2_tsp_1(X0,sK84)
| ~ v2_tsp_2(X0,sK84)
| v3_struct_0(X0)
| ~ v1_funct_1(X2)
| u1_struct_0(X0) != X1
| k1_struct_0(X0,k8_funct_2(sF844,u1_struct_0(X0),X2,sK127(sK84,X0,X2,X1))) != k5_subset_1(sF844,X1,sF847(sK127(sK84,X0,X2,X1)))
| ~ m1_subset_1(X1,k1_zfmisc_1(sF844))
| ~ v1_funct_2(X2,sF844,u1_struct_0(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl848_124])],[avatar_definition]) ).
fof(f46573,plain,
( ! [X2,X0,X1] :
( ~ v2_tsp_2(X0,sK84)
| v5_pre_topc(X2,sK84,X0)
| ~ m2_tsp_1(X0,sK84)
| ~ m2_relset_1(X2,sF844,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_funct_1(X2)
| u1_struct_0(X0) != X1
| k1_struct_0(X0,k8_funct_2(sF844,u1_struct_0(X0),X2,sK127(sK84,X0,X2,X1))) != k5_subset_1(sF844,X1,sF847(sK127(sK84,X0,X2,X1)))
| ~ m1_subset_1(X1,k1_zfmisc_1(sF844))
| ~ v1_funct_2(X2,sF844,u1_struct_0(X0)) )
| ~ spl848_124 ),
inference(avatar_component_clause,[],[f46572]) ).
fof(f46574,plain,
( ~ spl848_26
| spl848_28
| spl848_124
| ~ spl848_27 ),
inference(avatar_split_clause,[],[f46570,f45377,f46572,f45381,f45373]) ).
fof(f46584,plain,
( ! [X0] :
( k2_tarski(X0,X0) = k1_struct_0(sK84,X0)
| ~ l1_struct_0(sK84)
| ~ m1_subset_1(X0,u1_struct_0(sK84)) )
| spl848_28 ),
inference(resolution,[],[f44683,f45382]) ).
fof(f46585,plain,
( ! [X0] :
( k2_tarski(X0,X0) = k1_struct_0(sK85,X0)
| ~ l1_struct_0(sK85)
| ~ m1_subset_1(X0,u1_struct_0(sK85)) )
| spl848_24 ),
inference(resolution,[],[f44683,f45365]) ).
fof(f46586,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF845)
| k2_tarski(X0,X0) = k1_struct_0(sK85,X0)
| ~ l1_struct_0(sK85) )
| spl848_24 ),
inference(forward_demodulation,[],[f46585,f45221]) ).
fof(f46587,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF844)
| k2_tarski(X0,X0) = k1_struct_0(sK84,X0)
| ~ l1_struct_0(sK84) )
| spl848_28 ),
inference(forward_demodulation,[],[f46584,f45219]) ).
fof(f46589,definition,
( spl848_125
<=> ! [X0] :
( ~ m1_subset_1(X0,sF845)
| k2_tarski(X0,X0) = k1_struct_0(sK85,X0) ) ),
introduced(definition,[new_symbols(definition,[spl848_125])],[avatar_definition]) ).
fof(f46590,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF845)
| k2_tarski(X0,X0) = k1_struct_0(sK85,X0) )
| ~ spl848_125 ),
inference(avatar_component_clause,[],[f46589]) ).
fof(f46591,plain,
( ~ spl848_65
| spl848_125
| spl848_24 ),
inference(avatar_split_clause,[],[f46586,f45364,f46589,f45614]) ).
fof(f46593,definition,
( spl848_126
<=> ! [X0] :
( ~ m1_subset_1(X0,sF844)
| k2_tarski(X0,X0) = k1_struct_0(sK84,X0) ) ),
introduced(definition,[new_symbols(definition,[spl848_126])],[avatar_definition]) ).
fof(f46594,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF844)
| k2_tarski(X0,X0) = k1_struct_0(sK84,X0) )
| ~ spl848_126 ),
inference(avatar_component_clause,[],[f46593]) ).
fof(f46595,plain,
( ~ spl848_63
| spl848_126
| spl848_28 ),
inference(avatar_split_clause,[],[f46587,f45381,f46593,f45606]) ).
fof(f46599,plain,
( ! [X0] :
( k2_tarski(sF846(X0),sF846(X0)) = k1_struct_0(sK85,sF846(X0))
| ~ m1_subset_1(X0,sF844) )
| ~ spl848_32
| ~ spl848_125 ),
inference(resolution,[],[f46590,f45410]) ).
fof(f46648,plain,
( ! [X0,X1] :
( v5_pre_topc(X0,sK84,sK85)
| ~ m2_tsp_1(sK85,sK84)
| ~ m2_relset_1(X0,sF844,u1_struct_0(sK85))
| v3_struct_0(sK85)
| ~ v1_funct_1(X0)
| u1_struct_0(sK85) != X1
| k1_struct_0(sK85,k8_funct_2(sF844,u1_struct_0(sK85),X0,sK127(sK84,sK85,X0,X1))) != k5_subset_1(sF844,X1,sF847(sK127(sK84,sK85,X0,X1)))
| ~ m1_subset_1(X1,k1_zfmisc_1(sF844))
| ~ v1_funct_2(X0,sF844,u1_struct_0(sK85)) )
| ~ spl848_58
| ~ spl848_124 ),
inference(resolution,[],[f46573,f45579]) ).
fof(f46649,plain,
( ! [X0,X1] :
( ~ m2_relset_1(X0,sF844,sF845)
| v5_pre_topc(X0,sK84,sK85)
| ~ m2_tsp_1(sK85,sK84)
| v3_struct_0(sK85)
| ~ v1_funct_1(X0)
| u1_struct_0(sK85) != X1
| k1_struct_0(sK85,k8_funct_2(sF844,u1_struct_0(sK85),X0,sK127(sK84,sK85,X0,X1))) != k5_subset_1(sF844,X1,sF847(sK127(sK84,sK85,X0,X1)))
| ~ m1_subset_1(X1,k1_zfmisc_1(sF844))
| ~ v1_funct_2(X0,sF844,u1_struct_0(sK85)) )
| ~ spl848_58
| ~ spl848_124 ),
inference(forward_demodulation,[],[f46648,f45221]) ).
fof(f46650,plain,
( ! [X0,X1] :
( sF845 != X1
| ~ m2_relset_1(X0,sF844,sF845)
| v5_pre_topc(X0,sK84,sK85)
| ~ m2_tsp_1(sK85,sK84)
| v3_struct_0(sK85)
| ~ v1_funct_1(X0)
| k1_struct_0(sK85,k8_funct_2(sF844,u1_struct_0(sK85),X0,sK127(sK84,sK85,X0,X1))) != k5_subset_1(sF844,X1,sF847(sK127(sK84,sK85,X0,X1)))
| ~ m1_subset_1(X1,k1_zfmisc_1(sF844))
| ~ v1_funct_2(X0,sF844,u1_struct_0(sK85)) )
| ~ spl848_58
| ~ spl848_124 ),
inference(forward_demodulation,[],[f46649,f45221]) ).
fof(f46651,plain,
( ! [X0,X1] :
( k5_subset_1(sF844,X1,sF847(sK127(sK84,sK85,X0,X1))) != k1_struct_0(sK85,k8_funct_2(sF844,sF845,X0,sK127(sK84,sK85,X0,X1)))
| sF845 != X1
| ~ m2_relset_1(X0,sF844,sF845)
| v5_pre_topc(X0,sK84,sK85)
| ~ m2_tsp_1(sK85,sK84)
| v3_struct_0(sK85)
| ~ v1_funct_1(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF844))
| ~ v1_funct_2(X0,sF844,u1_struct_0(sK85)) )
| ~ spl848_58
| ~ spl848_124 ),
inference(forward_demodulation,[],[f46650,f45221]) ).
fof(f46652,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X0,sF844,sF845)
| k5_subset_1(sF844,X1,sF847(sK127(sK84,sK85,X0,X1))) != k1_struct_0(sK85,k8_funct_2(sF844,sF845,X0,sK127(sK84,sK85,X0,X1)))
| sF845 != X1
| ~ m2_relset_1(X0,sF844,sF845)
| v5_pre_topc(X0,sK84,sK85)
| ~ m2_tsp_1(sK85,sK84)
| v3_struct_0(sK85)
| ~ v1_funct_1(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF844)) )
| ~ spl848_58
| ~ spl848_124 ),
inference(forward_demodulation,[],[f46651,f45221]) ).
fof(f46654,definition,
( spl848_130
<=> ! [X0,X1] :
( ~ v1_funct_2(X0,sF844,sF845)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF844))
| ~ v1_funct_1(X0)
| v5_pre_topc(X0,sK84,sK85)
| ~ m2_relset_1(X0,sF844,sF845)
| sF845 != X1
| k5_subset_1(sF844,X1,sF847(sK127(sK84,sK85,X0,X1))) != k1_struct_0(sK85,k8_funct_2(sF844,sF845,X0,sK127(sK84,sK85,X0,X1))) ) ),
introduced(definition,[new_symbols(definition,[spl848_130])],[avatar_definition]) ).
fof(f46655,plain,
( ! [X0,X1] :
( ~ v1_funct_1(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF844))
| ~ v1_funct_2(X0,sF844,sF845)
| v5_pre_topc(X0,sK84,sK85)
| ~ m2_relset_1(X0,sF844,sF845)
| sF845 != X1
| k5_subset_1(sF844,X1,sF847(sK127(sK84,sK85,X0,X1))) != k1_struct_0(sK85,k8_funct_2(sF844,sF845,X0,sK127(sK84,sK85,X0,X1))) )
| ~ spl848_130 ),
inference(avatar_component_clause,[],[f46654]) ).
fof(f46656,plain,
( spl848_24
| ~ spl848_40
| spl848_130
| ~ spl848_58
| ~ spl848_124 ),
inference(avatar_split_clause,[],[f46652,f46572,f45578,f46654,f45463,f45364]) ).
fof(f46728,plain,
( ~ m2_relset_1(sK86,sF844,sF845)
| ~ v1_funct_2(sK86,sF844,sF845)
| sF844 = k1_relat_1(sK86)
| ~ spl848_21
| ~ spl848_112 ),
inference(resolution,[],[f46359,f45345]) ).
fof(f46730,definition,
( spl848_138
<=> sF844 = k1_relat_1(sK86) ),
introduced(definition,[new_symbols(definition,[spl848_138])],[avatar_definition]) ).
fof(f46732,plain,
( sF844 = k1_relat_1(sK86)
| ~ spl848_138 ),
inference(avatar_component_clause,[],[f46730]) ).
fof(f46733,plain,
( spl848_138
| ~ spl848_20
| ~ spl848_18
| ~ spl848_21
| ~ spl848_112 ),
inference(avatar_split_clause,[],[f46728,f46358,f45344,f45332,f45340,f46730]) ).
fof(f46735,plain,
( ! [X0] :
( r2_hidden(X0,sF844)
| ~ m1_subset_1(X0,sF844) )
| spl848_31 ),
inference(resolution,[],[f39138,f45406]) ).
fof(f46926,definition,
( spl848_151
<=> m1_subset_1(sK127(sK84,sK85,sK86,sF845),sF844) ),
introduced(definition,[new_symbols(definition,[spl848_151])],[avatar_definition]) ).
fof(f46927,plain,
( m1_subset_1(sK127(sK84,sK85,sK86,sF845),sF844)
| ~ spl848_151 ),
inference(avatar_component_clause,[],[f46926]) ).
fof(f46928,plain,
( ~ m1_subset_1(sK127(sK84,sK85,sK86,sF845),sF844)
| spl848_151 ),
inference(avatar_component_clause,[],[f46926]) ).
fof(f46986,plain,
( v5_pre_topc(sK86,sK84,sK85)
| ~ v1_funct_1(sK86)
| ~ v1_funct_2(sK86,sF844,sF845)
| ~ m2_relset_1(sK86,sF844,sF845)
| ~ spl848_72
| spl848_151 ),
inference(resolution,[],[f46928,f45672]) ).
fof(f46990,plain,
( ~ spl848_18
| ~ spl848_20
| ~ spl848_21
| spl848_19
| ~ spl848_72
| spl848_151 ),
inference(avatar_split_clause,[],[f46986,f46926,f45671,f45336,f45344,f45340,f45332]) ).
fof(f47173,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK84))
| ~ v1_tsp_1(X1,sK84)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK84)))
| v3_struct_0(sK84)
| k1_struct_0(sK84,X0) = k5_subset_1(u1_struct_0(sK84),X1,k4_tex_4(sK84,X0))
| ~ l1_pre_topc(sK84) )
| ~ spl848_27 ),
inference(resolution,[],[f39367,f45378]) ).
fof(f47174,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF844)
| ~ r2_hidden(X0,X1)
| ~ v1_tsp_1(X1,sK84)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK84)))
| v3_struct_0(sK84)
| k1_struct_0(sK84,X0) = k5_subset_1(u1_struct_0(sK84),X1,k4_tex_4(sK84,X0))
| ~ l1_pre_topc(sK84) )
| ~ spl848_27 ),
inference(forward_demodulation,[],[f47173,f45219]) ).
fof(f47175,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(sF844))
| ~ m1_subset_1(X0,sF844)
| ~ r2_hidden(X0,X1)
| ~ v1_tsp_1(X1,sK84)
| v3_struct_0(sK84)
| k1_struct_0(sK84,X0) = k5_subset_1(u1_struct_0(sK84),X1,k4_tex_4(sK84,X0))
| ~ l1_pre_topc(sK84) )
| ~ spl848_27 ),
inference(forward_demodulation,[],[f47174,f45219]) ).
fof(f47176,plain,
( ! [X0,X1] :
( k1_struct_0(sK84,X0) = k5_subset_1(u1_struct_0(sK84),X1,sF847(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(sF844))
| ~ m1_subset_1(X0,sF844)
| ~ r2_hidden(X0,X1)
| ~ v1_tsp_1(X1,sK84)
| v3_struct_0(sK84)
| ~ l1_pre_topc(sK84) )
| ~ spl848_27 ),
inference(forward_demodulation,[],[f47175,f45226]) ).
fof(f47177,plain,
( ! [X0,X1] :
( k1_struct_0(sK84,X0) = k5_subset_1(sF844,X1,sF847(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(sF844))
| ~ m1_subset_1(X0,sF844)
| ~ r2_hidden(X0,X1)
| ~ v1_tsp_1(X1,sK84)
| v3_struct_0(sK84)
| ~ l1_pre_topc(sK84) )
| ~ spl848_27 ),
inference(forward_demodulation,[],[f47176,f45219]) ).
fof(f47179,definition,
( spl848_185
<=> ! [X0,X1] :
( k1_struct_0(sK84,X0) = k5_subset_1(sF844,X1,sF847(X0))
| ~ v1_tsp_1(X1,sK84)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X0,sF844)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF844)) ) ),
introduced(definition,[new_symbols(definition,[spl848_185])],[avatar_definition]) ).
fof(f47180,plain,
( ! [X0,X1] :
( ~ v1_tsp_1(X1,sK84)
| k1_struct_0(sK84,X0) = k5_subset_1(sF844,X1,sF847(X0))
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X0,sF844)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF844)) )
| ~ spl848_185 ),
inference(avatar_component_clause,[],[f47179]) ).
fof(f47181,plain,
( ~ spl848_26
| spl848_28
| spl848_185
| ~ spl848_27 ),
inference(avatar_split_clause,[],[f47177,f45377,f47179,f45381,f45373]) ).
fof(f47260,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF844))
| ~ v1_funct_2(sK86,sF844,sF845)
| v5_pre_topc(sK86,sK84,sK85)
| ~ m2_relset_1(sK86,sF844,sF845)
| sF845 != X0
| k5_subset_1(sF844,X0,sF847(sK127(sK84,sK85,sK86,X0))) != k1_struct_0(sK85,k8_funct_2(sF844,sF845,sK86,sK127(sK84,sK85,sK86,X0))) )
| ~ spl848_21
| ~ spl848_130 ),
inference(resolution,[],[f46655,f45345]) ).
fof(f47261,plain,
( ! [X0] :
( k5_subset_1(sF844,X0,sF847(sK127(sK84,sK85,sK86,X0))) != k1_struct_0(sK85,sF846(sK127(sK84,sK85,sK86,X0)))
| ~ m1_subset_1(X0,k1_zfmisc_1(sF844))
| ~ v1_funct_2(sK86,sF844,sF845)
| v5_pre_topc(sK86,sK84,sK85)
| ~ m2_relset_1(sK86,sF844,sF845)
| sF845 != X0 )
| ~ spl848_21
| ~ spl848_130 ),
inference(forward_demodulation,[],[f47260,f45224]) ).
fof(f47263,definition,
( spl848_192
<=> ! [X0] :
( k5_subset_1(sF844,X0,sF847(sK127(sK84,sK85,sK86,X0))) != k1_struct_0(sK85,sF846(sK127(sK84,sK85,sK86,X0)))
| sF845 != X0
| ~ m1_subset_1(X0,k1_zfmisc_1(sF844)) ) ),
introduced(definition,[new_symbols(definition,[spl848_192])],[avatar_definition]) ).
fof(f47264,plain,
( ! [X0] :
( sF845 != X0
| k5_subset_1(sF844,X0,sF847(sK127(sK84,sK85,sK86,X0))) != k1_struct_0(sK85,sF846(sK127(sK84,sK85,sK86,X0)))
| ~ m1_subset_1(X0,k1_zfmisc_1(sF844)) )
| ~ spl848_192 ),
inference(avatar_component_clause,[],[f47263]) ).
fof(f47265,plain,
( ~ spl848_18
| spl848_19
| ~ spl848_20
| spl848_192
| ~ spl848_21
| ~ spl848_130 ),
inference(avatar_split_clause,[],[f47261,f46654,f45344,f47263,f45340,f45336,f45332]) ).
fof(f47266,plain,
( k5_subset_1(sF844,sF845,sF847(sK127(sK84,sK85,sK86,sF845))) != k1_struct_0(sK85,sF846(sK127(sK84,sK85,sK86,sF845)))
| ~ m1_subset_1(sF845,k1_zfmisc_1(sF844))
| ~ spl848_192 ),
inference(equality_resolution,[],[f47264]) ).
fof(f47268,definition,
( spl848_193
<=> k5_subset_1(sF844,sF845,sF847(sK127(sK84,sK85,sK86,sF845))) = k1_struct_0(sK85,sF846(sK127(sK84,sK85,sK86,sF845))) ),
introduced(definition,[new_symbols(definition,[spl848_193])],[avatar_definition]) ).
fof(f47270,plain,
( k5_subset_1(sF844,sF845,sF847(sK127(sK84,sK85,sK86,sF845))) != k1_struct_0(sK85,sF846(sK127(sK84,sK85,sK86,sF845)))
| spl848_193 ),
inference(avatar_component_clause,[],[f47268]) ).
fof(f47271,plain,
( ~ spl848_41
| ~ spl848_193
| ~ spl848_192 ),
inference(avatar_split_clause,[],[f47266,f47263,f47268,f45467]) ).
fof(f47274,plain,
( ! [X0] :
( k1_struct_0(sK85,sF846(sK127(sK84,sK85,sK86,sF845))) != k5_subset_1(sF844,sF845,sF847(X0))
| ~ m1_subset_1(sK127(sK84,sK85,sK86,sF845),sF844)
| ~ m1_subset_1(X0,sF844)
| ~ r2_hidden(X0,sF847(sK127(sK84,sK85,sK86,sF845))) )
| ~ spl848_84
| spl848_193 ),
inference(superposition,[],[f47270,f46022]) ).
fof(f47276,definition,
( spl848_194
<=> ! [X0] :
( k1_struct_0(sK85,sF846(sK127(sK84,sK85,sK86,sF845))) != k5_subset_1(sF844,sF845,sF847(X0))
| ~ r2_hidden(X0,sF847(sK127(sK84,sK85,sK86,sF845)))
| ~ m1_subset_1(X0,sF844) ) ),
introduced(definition,[new_symbols(definition,[spl848_194])],[avatar_definition]) ).
fof(f47277,plain,
( ! [X0] :
( k1_struct_0(sK85,sF846(sK127(sK84,sK85,sK86,sF845))) != k5_subset_1(sF844,sF845,sF847(X0))
| ~ r2_hidden(X0,sF847(sK127(sK84,sK85,sK86,sF845)))
| ~ m1_subset_1(X0,sF844) )
| ~ spl848_194 ),
inference(avatar_component_clause,[],[f47276]) ).
fof(f47278,plain,
( ~ spl848_151
| spl848_194
| ~ spl848_84
| spl848_193 ),
inference(avatar_split_clause,[],[f47274,f47268,f46021,f47276,f46926]) ).
fof(f47371,plain,
( ! [X0,X1] :
( sF847(X0) = sF847(sF846(X1))
| ~ m1_subset_1(X0,sF844)
| ~ r2_hidden(X0,sF847(X1))
| ~ m1_subset_1(sF846(X1),sF844)
| ~ m1_subset_1(X1,sF844)
| ~ m1_subset_1(X1,sF844) )
| ~ spl848_89 ),
inference(resolution,[],[f46049,f45227]) ).
fof(f47385,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sF846(X1),sF844)
| ~ m1_subset_1(X0,sF844)
| ~ r2_hidden(X0,sF847(X1))
| sF847(X0) = sF847(sF846(X1))
| ~ m1_subset_1(X1,sF844) )
| ~ spl848_89 ),
inference(duplicate_literal_removal,[],[f47371]) ).
fof(f47386,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF844)
| ~ r2_hidden(X0,sF847(X1))
| sF847(X0) = sF847(sF846(X1))
| ~ m1_subset_1(X1,sF844)
| ~ m1_subset_1(X1,sF844) )
| ~ spl848_29
| ~ spl848_89 ),
inference(resolution,[],[f47385,f45709]) ).
fof(f47391,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF847(X1))
| ~ m1_subset_1(X0,sF844)
| sF847(X0) = sF847(sF846(X1))
| ~ m1_subset_1(X1,sF844) )
| ~ spl848_29
| ~ spl848_89 ),
inference(duplicate_literal_removal,[],[f47386]) ).
fof(f47418,plain,
( ! [X0,X1] :
( v1_tsp_1(X0,X1)
| u1_struct_0(sK85) != X0
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(sK85)
| ~ m2_tsp_1(sK85,X1)
| v3_struct_0(X1)
| ~ l1_pre_topc(X1) )
| ~ spl848_62 ),
inference(resolution,[],[f39270,f45601]) ).
fof(f47419,plain,
( ! [X0,X1] :
( sF845 != X0
| v1_tsp_1(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(sK85)
| ~ m2_tsp_1(sK85,X1)
| v3_struct_0(X1)
| ~ l1_pre_topc(X1) )
| ~ spl848_62 ),
inference(forward_demodulation,[],[f47418,f45221]) ).
fof(f47421,definition,
( spl848_204
<=> ! [X0,X1] :
( sF845 != X0
| ~ l1_pre_topc(X1)
| v3_struct_0(X1)
| ~ m2_tsp_1(sK85,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| v1_tsp_1(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl848_204])],[avatar_definition]) ).
fof(f47422,plain,
( ! [X0,X1] :
( sF845 != X0
| ~ l1_pre_topc(X1)
| v3_struct_0(X1)
| ~ m2_tsp_1(sK85,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| v1_tsp_1(X0,X1) )
| ~ spl848_204 ),
inference(avatar_component_clause,[],[f47421]) ).
fof(f47423,plain,
( spl848_24
| spl848_204
| ~ spl848_62 ),
inference(avatar_split_clause,[],[f47419,f45599,f47421,f45364]) ).
fof(f47424,plain,
( ! [X0] :
( v1_tsp_1(sF845,X0)
| v3_struct_0(X0)
| ~ m2_tsp_1(sK85,X0)
| ~ m1_subset_1(sF845,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) )
| ~ spl848_204 ),
inference(equality_resolution,[],[f47422]) ).
fof(f47425,plain,
( ! [X0] :
( v3_struct_0(sK84)
| ~ m2_tsp_1(sK85,sK84)
| ~ m1_subset_1(sF845,k1_zfmisc_1(u1_struct_0(sK84)))
| ~ l1_pre_topc(sK84)
| k1_struct_0(sK84,X0) = k5_subset_1(sF844,sF845,sF847(X0))
| ~ r2_hidden(X0,sF845)
| ~ m1_subset_1(X0,sF844)
| ~ m1_subset_1(sF845,k1_zfmisc_1(sF844)) )
| ~ spl848_185
| ~ spl848_204 ),
inference(resolution,[],[f47424,f47180]) ).
fof(f47426,plain,
( ! [X0] :
( ~ m1_subset_1(sF845,k1_zfmisc_1(sF844))
| v3_struct_0(sK84)
| ~ m2_tsp_1(sK85,sK84)
| ~ l1_pre_topc(sK84)
| k1_struct_0(sK84,X0) = k5_subset_1(sF844,sF845,sF847(X0))
| ~ r2_hidden(X0,sF845)
| ~ m1_subset_1(X0,sF844)
| ~ m1_subset_1(sF845,k1_zfmisc_1(sF844)) )
| ~ spl848_185
| ~ spl848_204 ),
inference(forward_demodulation,[],[f47425,f45219]) ).
fof(f47427,plain,
( ! [X0] :
( ~ m1_subset_1(sF845,k1_zfmisc_1(sF844))
| v3_struct_0(sK84)
| ~ m2_tsp_1(sK85,sK84)
| ~ l1_pre_topc(sK84)
| k1_struct_0(sK84,X0) = k5_subset_1(sF844,sF845,sF847(X0))
| ~ r2_hidden(X0,sF845)
| ~ m1_subset_1(X0,sF844) )
| ~ spl848_185
| ~ spl848_204 ),
inference(duplicate_literal_removal,[],[f47426]) ).
fof(f47429,definition,
( spl848_205
<=> ! [X0] :
( k1_struct_0(sK84,X0) = k5_subset_1(sF844,sF845,sF847(X0))
| ~ m1_subset_1(X0,sF844)
| ~ r2_hidden(X0,sF845) ) ),
introduced(definition,[new_symbols(definition,[spl848_205])],[avatar_definition]) ).
fof(f47430,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF845)
| ~ m1_subset_1(X0,sF844)
| k1_struct_0(sK84,X0) = k5_subset_1(sF844,sF845,sF847(X0)) )
| ~ spl848_205 ),
inference(avatar_component_clause,[],[f47429]) ).
fof(f47431,plain,
( spl848_205
| ~ spl848_26
| ~ spl848_40
| spl848_28
| ~ spl848_41
| ~ spl848_185
| ~ spl848_204 ),
inference(avatar_split_clause,[],[f47427,f47421,f47179,f45467,f45381,f45463,f45373,f47429]) ).
fof(f47621,plain,
( ! [X0,X1] :
( k2_tex_4(sK84,X0) != k2_tex_4(sK84,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK84))
| ~ m1_subset_1(X0,u1_struct_0(sK84))
| v3_struct_0(sK84)
| r2_hidden(X1,k2_tex_4(sK84,X0)) )
| ~ spl848_26 ),
inference(resolution,[],[f41180,f45374]) ).
fof(f47624,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF844)
| k2_tex_4(sK84,X0) != k2_tex_4(sK84,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK84))
| v3_struct_0(sK84)
| r2_hidden(X1,k2_tex_4(sK84,X0)) )
| ~ spl848_26 ),
inference(forward_demodulation,[],[f47621,f45219]) ).
fof(f47626,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF844)
| ~ m1_subset_1(X1,sF844)
| k2_tex_4(sK84,X0) != k2_tex_4(sK84,X1)
| v3_struct_0(sK84)
| r2_hidden(X1,k2_tex_4(sK84,X0)) )
| ~ spl848_26 ),
inference(forward_demodulation,[],[f47624,f45219]) ).
fof(f47632,definition,
( spl848_231
<=> ! [X0,X1] :
( ~ m1_subset_1(X0,sF844)
| r2_hidden(X1,k2_tex_4(sK84,X0))
| k2_tex_4(sK84,X0) != k2_tex_4(sK84,X1)
| ~ m1_subset_1(X1,sF844) ) ),
introduced(definition,[new_symbols(definition,[spl848_231])],[avatar_definition]) ).
fof(f47633,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF844)
| r2_hidden(X1,k2_tex_4(sK84,X0))
| k2_tex_4(sK84,X0) != k2_tex_4(sK84,X1)
| ~ m1_subset_1(X1,sF844) )
| ~ spl848_231 ),
inference(avatar_component_clause,[],[f47632]) ).
fof(f47634,plain,
( spl848_28
| spl848_231
| ~ spl848_26 ),
inference(avatar_split_clause,[],[f47626,f45373,f47632,f45381]) ).
fof(f47652,plain,
( ! [X0,X1] :
( ~ v1_funct_1(X1)
| k2_tex_4(sK84,X0) != k2_tex_4(sK84,sK127(sK84,sK85,X1,sF845))
| ~ m1_subset_1(X0,sF844)
| v5_pre_topc(X1,sK84,sK85)
| r2_hidden(X0,k2_tex_4(sK84,sK127(sK84,sK85,X1,sF845)))
| ~ v1_funct_2(X1,sF844,sF845)
| ~ m2_relset_1(X1,sF844,sF845) )
| ~ spl848_72
| ~ spl848_231 ),
inference(resolution,[],[f47633,f45672]) ).
fof(f47655,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF844)
| r2_hidden(X0,k2_tex_4(sK84,X0))
| k2_tex_4(sK84,X0) != k2_tex_4(sK84,X0) )
| ~ spl848_231 ),
inference(factoring,[],[f47633]) ).
fof(f47656,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF844)
| r2_hidden(X0,k2_tex_4(sK84,X0)) )
| ~ spl848_231 ),
inference(trivial_inequality_removal,[],[f47655]) ).
fof(f47665,plain,
( r2_hidden(sK127(sK84,sK85,sK86,sF845),k2_tex_4(sK84,sK127(sK84,sK85,sK86,sF845)))
| ~ spl848_151
| ~ spl848_231 ),
inference(resolution,[],[f47656,f46927]) ).
fof(f47686,plain,
( r2_hidden(sK127(sK84,sK85,sK86,sF845),k4_tex_4(sK84,sK127(sK84,sK85,sK86,sF845)))
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84)
| ~ m1_subset_1(sK127(sK84,sK85,sK86,sF845),u1_struct_0(sK84))
| ~ spl848_151
| ~ spl848_231 ),
inference(superposition,[],[f47665,f39378]) ).
fof(f47689,plain,
( r2_hidden(sK127(sK84,sK85,sK86,sF845),sF847(sK127(sK84,sK85,sK86,sF845)))
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84)
| ~ m1_subset_1(sK127(sK84,sK85,sK86,sF845),u1_struct_0(sK84))
| ~ spl848_151
| ~ spl848_231 ),
inference(forward_demodulation,[],[f47686,f45226]) ).
fof(f47693,plain,
( ~ m1_subset_1(sK127(sK84,sK85,sK86,sF845),sF844)
| r2_hidden(sK127(sK84,sK85,sK86,sF845),sF847(sK127(sK84,sK85,sK86,sF845)))
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84)
| ~ spl848_151
| ~ spl848_231 ),
inference(forward_demodulation,[],[f47689,f45219]) ).
fof(f47698,definition,
( spl848_232
<=> r2_hidden(sK127(sK84,sK85,sK86,sF845),sF847(sK127(sK84,sK85,sK86,sF845))) ),
introduced(definition,[new_symbols(definition,[spl848_232])],[avatar_definition]) ).
fof(f47700,plain,
( r2_hidden(sK127(sK84,sK85,sK86,sF845),sF847(sK127(sK84,sK85,sK86,sF845)))
| ~ spl848_232 ),
inference(avatar_component_clause,[],[f47698]) ).
fof(f47701,plain,
( ~ spl848_26
| ~ spl848_27
| spl848_28
| spl848_232
| ~ spl848_151
| ~ spl848_151
| ~ spl848_231 ),
inference(avatar_split_clause,[],[f47693,f47632,f46926,f46926,f47698,f45381,f45377,f45373]) ).
fof(f47717,plain,
( ~ m1_subset_1(sK127(sK84,sK85,sK86,sF845),sF844)
| sF847(sK127(sK84,sK85,sK86,sF845)) = sF847(sF846(sK127(sK84,sK85,sK86,sF845)))
| ~ m1_subset_1(sK127(sK84,sK85,sK86,sF845),sF844)
| ~ spl848_29
| ~ spl848_89
| ~ spl848_232 ),
inference(resolution,[],[f47700,f47391]) ).
fof(f47724,plain,
( ~ m1_subset_1(sK127(sK84,sK85,sK86,sF845),sF844)
| sF847(sK127(sK84,sK85,sK86,sF845)) = sF847(sF846(sK127(sK84,sK85,sK86,sF845)))
| ~ spl848_29
| ~ spl848_89
| ~ spl848_232 ),
inference(duplicate_literal_removal,[],[f47717]) ).
fof(f47734,definition,
( spl848_238
<=> sF847(sK127(sK84,sK85,sK86,sF845)) = sF847(sF846(sK127(sK84,sK85,sK86,sF845))) ),
introduced(definition,[new_symbols(definition,[spl848_238])],[avatar_definition]) ).
fof(f47736,plain,
( sF847(sK127(sK84,sK85,sK86,sF845)) = sF847(sF846(sK127(sK84,sK85,sK86,sF845)))
| ~ spl848_238 ),
inference(avatar_component_clause,[],[f47734]) ).
fof(f47737,plain,
( spl848_238
| ~ spl848_151
| ~ spl848_29
| ~ spl848_89
| ~ spl848_232 ),
inference(avatar_split_clause,[],[f47724,f47698,f46048,f45385,f46926,f47734]) ).
fof(f47755,definition,
( spl848_239
<=> m1_subset_1(sF846(sK127(sK84,sK85,sK86,sF845)),sF844) ),
introduced(definition,[new_symbols(definition,[spl848_239])],[avatar_definition]) ).
fof(f47756,plain,
( m1_subset_1(sF846(sK127(sK84,sK85,sK86,sF845)),sF844)
| ~ spl848_239 ),
inference(avatar_component_clause,[],[f47755]) ).
fof(f47757,plain,
( ~ m1_subset_1(sF846(sK127(sK84,sK85,sK86,sF845)),sF844)
| spl848_239 ),
inference(avatar_component_clause,[],[f47755]) ).
fof(f47805,plain,
( ~ m1_subset_1(sK127(sK84,sK85,sK86,sF845),sF844)
| ~ spl848_29
| spl848_239 ),
inference(resolution,[],[f47757,f45709]) ).
fof(f47810,plain,
( ~ spl848_151
| ~ spl848_29
| spl848_239 ),
inference(avatar_split_clause,[],[f47805,f47755,f45385,f46926]) ).
fof(f47816,plain,
( k2_tarski(sF846(sK127(sK84,sK85,sK86,sF845)),sF846(sK127(sK84,sK85,sK86,sF845))) = k1_struct_0(sK84,sF846(sK127(sK84,sK85,sK86,sF845)))
| ~ spl848_126
| ~ spl848_239 ),
inference(resolution,[],[f47756,f46594]) ).
fof(f48231,plain,
( ! [X0] :
( k2_tex_4(sK84,X0) != k2_tex_4(sK84,sK127(sK84,sK85,sK86,sF845))
| ~ m1_subset_1(X0,sF844)
| v5_pre_topc(sK86,sK84,sK85)
| r2_hidden(X0,k2_tex_4(sK84,sK127(sK84,sK85,sK86,sF845)))
| ~ v1_funct_2(sK86,sF844,sF845)
| ~ m2_relset_1(sK86,sF844,sF845) )
| ~ spl848_21
| ~ spl848_72
| ~ spl848_231 ),
inference(resolution,[],[f47652,f45345]) ).
fof(f48233,definition,
( spl848_298
<=> ! [X0] :
( k2_tex_4(sK84,X0) != k2_tex_4(sK84,sK127(sK84,sK85,sK86,sF845))
| r2_hidden(X0,k2_tex_4(sK84,sK127(sK84,sK85,sK86,sF845)))
| ~ m1_subset_1(X0,sF844) ) ),
introduced(definition,[new_symbols(definition,[spl848_298])],[avatar_definition]) ).
fof(f48234,plain,
( ! [X0] :
( r2_hidden(X0,k2_tex_4(sK84,sK127(sK84,sK85,sK86,sF845)))
| k2_tex_4(sK84,X0) != k2_tex_4(sK84,sK127(sK84,sK85,sK86,sF845))
| ~ m1_subset_1(X0,sF844) )
| ~ spl848_298 ),
inference(avatar_component_clause,[],[f48233]) ).
fof(f48235,plain,
( ~ spl848_18
| ~ spl848_20
| spl848_19
| spl848_298
| ~ spl848_21
| ~ spl848_72
| ~ spl848_231 ),
inference(avatar_split_clause,[],[f48231,f47632,f45671,f45344,f48233,f45336,f45340,f45332]) ).
fof(f48238,plain,
( ! [X0] :
( k2_tex_4(sK84,X0) != k2_tex_4(sK84,sK127(sK84,sK85,sK86,sF845))
| ~ m1_subset_1(X0,sF844)
| ~ m1_subset_1(X0,sF844)
| sF847(X0) = sF847(sK127(sK84,sK85,sK86,sF845))
| ~ m1_subset_1(sK127(sK84,sK85,sK86,sF845),sF844) )
| ~ spl848_83
| ~ spl848_298 ),
inference(resolution,[],[f48234,f45994]) ).
fof(f48247,plain,
( ! [X0] :
( r2_hidden(X0,k4_tex_4(sK84,sK127(sK84,sK85,sK86,sF845)))
| k2_tex_4(sK84,X0) != k4_tex_4(sK84,sK127(sK84,sK85,sK86,sF845))
| ~ m1_subset_1(X0,sF844)
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84)
| ~ m1_subset_1(sK127(sK84,sK85,sK86,sF845),u1_struct_0(sK84)) )
| ~ spl848_298 ),
inference(superposition,[],[f48234,f39378]) ).
fof(f48250,plain,
( ! [X0] :
( k2_tex_4(sK84,X0) != k2_tex_4(sK84,sK127(sK84,sK85,sK86,sF845))
| ~ m1_subset_1(X0,sF844)
| sF847(X0) = sF847(sK127(sK84,sK85,sK86,sF845))
| ~ m1_subset_1(sK127(sK84,sK85,sK86,sF845),sF844) )
| ~ spl848_83
| ~ spl848_298 ),
inference(duplicate_literal_removal,[],[f48238]) ).
fof(f48253,plain,
( ! [X0] :
( r2_hidden(X0,sF847(sK127(sK84,sK85,sK86,sF845)))
| k2_tex_4(sK84,X0) != k4_tex_4(sK84,sK127(sK84,sK85,sK86,sF845))
| ~ m1_subset_1(X0,sF844)
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84)
| ~ m1_subset_1(sK127(sK84,sK85,sK86,sF845),u1_struct_0(sK84)) )
| ~ spl848_298 ),
inference(forward_demodulation,[],[f48247,f45226]) ).
fof(f48264,definition,
( spl848_300
<=> ! [X0] :
( k2_tex_4(sK84,X0) != k2_tex_4(sK84,sK127(sK84,sK85,sK86,sF845))
| sF847(X0) = sF847(sK127(sK84,sK85,sK86,sF845))
| ~ m1_subset_1(X0,sF844) ) ),
introduced(definition,[new_symbols(definition,[spl848_300])],[avatar_definition]) ).
fof(f48265,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF844)
| sF847(X0) = sF847(sK127(sK84,sK85,sK86,sF845))
| k2_tex_4(sK84,X0) != k2_tex_4(sK84,sK127(sK84,sK85,sK86,sF845)) )
| ~ spl848_300 ),
inference(avatar_component_clause,[],[f48264]) ).
fof(f48266,plain,
( ~ spl848_151
| spl848_300
| ~ spl848_83
| ~ spl848_298 ),
inference(avatar_split_clause,[],[f48250,f48233,f45993,f48264,f46926]) ).
fof(f48271,plain,
( ! [X0] :
( k2_tex_4(sK84,X0) != sF847(sK127(sK84,sK85,sK86,sF845))
| r2_hidden(X0,sF847(sK127(sK84,sK85,sK86,sF845)))
| ~ m1_subset_1(X0,sF844)
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84)
| ~ m1_subset_1(sK127(sK84,sK85,sK86,sF845),u1_struct_0(sK84)) )
| ~ spl848_298 ),
inference(forward_demodulation,[],[f48253,f45226]) ).
fof(f48276,plain,
( ! [X0] :
( ~ m1_subset_1(sK127(sK84,sK85,sK86,sF845),sF844)
| k2_tex_4(sK84,X0) != sF847(sK127(sK84,sK85,sK86,sF845))
| r2_hidden(X0,sF847(sK127(sK84,sK85,sK86,sF845)))
| ~ m1_subset_1(X0,sF844)
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84) )
| ~ spl848_298 ),
inference(forward_demodulation,[],[f48271,f45219]) ).
fof(f48281,definition,
( spl848_302
<=> ! [X0] :
( k2_tex_4(sK84,X0) != sF847(sK127(sK84,sK85,sK86,sF845))
| ~ m1_subset_1(X0,sF844)
| r2_hidden(X0,sF847(sK127(sK84,sK85,sK86,sF845))) ) ),
introduced(definition,[new_symbols(definition,[spl848_302])],[avatar_definition]) ).
fof(f48282,plain,
( ! [X0] :
( k2_tex_4(sK84,X0) != sF847(sK127(sK84,sK85,sK86,sF845))
| ~ m1_subset_1(X0,sF844)
| r2_hidden(X0,sF847(sK127(sK84,sK85,sK86,sF845))) )
| ~ spl848_302 ),
inference(avatar_component_clause,[],[f48281]) ).
fof(f48283,plain,
( ~ spl848_26
| ~ spl848_27
| spl848_28
| spl848_302
| ~ spl848_151
| ~ spl848_298 ),
inference(avatar_split_clause,[],[f48276,f48233,f46926,f48281,f45381,f45377,f45373]) ).
fof(f48316,plain,
( ! [X0] :
( k4_tex_4(sK84,X0) != sF847(sK127(sK84,sK85,sK86,sF845))
| ~ m1_subset_1(X0,sF844)
| r2_hidden(X0,sF847(sK127(sK84,sK85,sK86,sF845)))
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84)
| ~ m1_subset_1(X0,u1_struct_0(sK84)) )
| ~ spl848_302 ),
inference(superposition,[],[f48282,f39378]) ).
fof(f48326,plain,
( ! [X0] :
( sF847(X0) != sF847(sK127(sK84,sK85,sK86,sF845))
| ~ m1_subset_1(X0,sF844)
| r2_hidden(X0,sF847(sK127(sK84,sK85,sK86,sF845)))
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84)
| ~ m1_subset_1(X0,u1_struct_0(sK84)) )
| ~ spl848_302 ),
inference(forward_demodulation,[],[f48316,f45226]) ).
fof(f48333,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF844)
| sF847(X0) != sF847(sK127(sK84,sK85,sK86,sF845))
| ~ m1_subset_1(X0,sF844)
| r2_hidden(X0,sF847(sK127(sK84,sK85,sK86,sF845)))
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84) )
| ~ spl848_302 ),
inference(forward_demodulation,[],[f48326,f45219]) ).
fof(f48334,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF844)
| sF847(X0) != sF847(sK127(sK84,sK85,sK86,sF845))
| r2_hidden(X0,sF847(sK127(sK84,sK85,sK86,sF845)))
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84) )
| ~ spl848_302 ),
inference(duplicate_literal_removal,[],[f48333]) ).
fof(f48342,definition,
( spl848_306
<=> ! [X0] :
( ~ m1_subset_1(X0,sF844)
| r2_hidden(X0,sF847(sK127(sK84,sK85,sK86,sF845)))
| sF847(X0) != sF847(sK127(sK84,sK85,sK86,sF845)) ) ),
introduced(definition,[new_symbols(definition,[spl848_306])],[avatar_definition]) ).
fof(f48343,plain,
( ! [X0] :
( sF847(X0) != sF847(sK127(sK84,sK85,sK86,sF845))
| r2_hidden(X0,sF847(sK127(sK84,sK85,sK86,sF845)))
| ~ m1_subset_1(X0,sF844) )
| ~ spl848_306 ),
inference(avatar_component_clause,[],[f48342]) ).
fof(f48344,plain,
( ~ spl848_26
| ~ spl848_27
| spl848_28
| spl848_306
| ~ spl848_302 ),
inference(avatar_split_clause,[],[f48334,f48281,f48342,f45381,f45377,f45373]) ).
fof(f48375,plain,
( sF847(sK127(sK84,sK85,sK86,sF845)) != sF847(sK127(sK84,sK85,sK86,sF845))
| r2_hidden(sF846(sK127(sK84,sK85,sK86,sF845)),sF847(sK127(sK84,sK85,sK86,sF845)))
| ~ m1_subset_1(sF846(sK127(sK84,sK85,sK86,sF845)),sF844)
| ~ spl848_238
| ~ spl848_306 ),
inference(superposition,[],[f48343,f47736]) ).
fof(f48384,plain,
( r2_hidden(sF846(sK127(sK84,sK85,sK86,sF845)),sF847(sK127(sK84,sK85,sK86,sF845)))
| ~ m1_subset_1(sF846(sK127(sK84,sK85,sK86,sF845)),sF844)
| ~ spl848_238
| ~ spl848_306 ),
inference(trivial_inequality_removal,[],[f48375]) ).
fof(f48401,definition,
( spl848_315
<=> r2_hidden(sF846(sK127(sK84,sK85,sK86,sF845)),sF847(sK127(sK84,sK85,sK86,sF845))) ),
introduced(definition,[new_symbols(definition,[spl848_315])],[avatar_definition]) ).
fof(f48404,plain,
( ~ spl848_239
| spl848_315
| ~ spl848_238
| ~ spl848_306 ),
inference(avatar_split_clause,[],[f48384,f48342,f47734,f48401,f47755]) ).
fof(f50414,plain,
( k1_struct_0(sK85,sF846(sK127(sK84,sK85,sK86,sF845))) = k1_struct_0(sK84,sF846(sK127(sK84,sK85,sK86,sF845)))
| ~ m1_subset_1(sK127(sK84,sK85,sK86,sF845),sF844)
| ~ spl848_32
| ~ spl848_125
| ~ spl848_126
| ~ spl848_239 ),
inference(superposition,[],[f47816,f46599]) ).
fof(f50417,definition,
( spl848_521
<=> k1_struct_0(sK85,sF846(sK127(sK84,sK85,sK86,sF845))) = k1_struct_0(sK84,sF846(sK127(sK84,sK85,sK86,sF845))) ),
introduced(definition,[new_symbols(definition,[spl848_521])],[avatar_definition]) ).
fof(f50419,plain,
( k1_struct_0(sK85,sF846(sK127(sK84,sK85,sK86,sF845))) = k1_struct_0(sK84,sF846(sK127(sK84,sK85,sK86,sF845)))
| ~ spl848_521 ),
inference(avatar_component_clause,[],[f50417]) ).
fof(f50421,plain,
( ~ spl848_151
| spl848_521
| ~ spl848_32
| ~ spl848_125
| ~ spl848_126
| ~ spl848_239 ),
inference(avatar_split_clause,[],[f50414,f47755,f46593,f46589,f45409,f50417,f46926]) ).
fof(f52844,plain,
( k1_relat_1(sK86) = k4_relset_1(sF844,sF845,sK86)
| ~ spl848_30 ),
inference(resolution,[],[f39687,f45402]) ).
fof(f53140,plain,
( sF844 = k4_relset_1(sF844,sF845,sK86)
| ~ spl848_30
| ~ spl848_138 ),
inference(forward_demodulation,[],[f52844,f46732]) ).
fof(f53609,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,k4_relset_1(X1,X2,sK86))
| r2_hidden(k1_funct_1(sK86,X0),X2)
| ~ m2_relset_1(sK86,X1,X2) )
| ~ spl848_21 ),
inference(resolution,[],[f41617,f45345]) ).
fof(f53613,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF844)
| r2_hidden(k1_funct_1(sK86,X0),sF845)
| ~ m2_relset_1(sK86,sF844,sF845) )
| ~ spl848_21
| ~ spl848_30
| ~ spl848_138 ),
inference(superposition,[],[f53609,f53140]) ).
fof(f53618,definition,
( spl848_704
<=> ! [X0] :
( ~ r2_hidden(X0,sF844)
| r2_hidden(k1_funct_1(sK86,X0),sF845) ) ),
introduced(definition,[new_symbols(definition,[spl848_704])],[avatar_definition]) ).
fof(f53619,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF844)
| r2_hidden(k1_funct_1(sK86,X0),sF845) )
| ~ spl848_704 ),
inference(avatar_component_clause,[],[f53618]) ).
fof(f53620,plain,
( ~ spl848_18
| spl848_704
| ~ spl848_21
| ~ spl848_30
| ~ spl848_138 ),
inference(avatar_split_clause,[],[f53613,f46730,f45401,f45344,f53618,f45332]) ).
fof(f53627,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF844)
| r2_hidden(k1_funct_1(sK86,X0),sF845) )
| spl848_31
| ~ spl848_704 ),
inference(resolution,[],[f53619,f46735]) ).
fof(f53647,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| v5_pre_topc(X0,sK84,sK85)
| r2_hidden(k1_funct_1(sK86,sK127(sK84,sK85,X0,sF845)),sF845)
| ~ v1_funct_2(X0,sF844,sF845)
| ~ m2_relset_1(X0,sF844,sF845) )
| spl848_31
| ~ spl848_72
| ~ spl848_704 ),
inference(resolution,[],[f53627,f45672]) ).
fof(f53741,plain,
( v5_pre_topc(sK86,sK84,sK85)
| r2_hidden(k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845)),sF845)
| ~ v1_funct_2(sK86,sF844,sF845)
| ~ m2_relset_1(sK86,sF844,sF845)
| ~ spl848_21
| spl848_31
| ~ spl848_72
| ~ spl848_704 ),
inference(resolution,[],[f53647,f45345]) ).
fof(f53868,plain,
( ! [X2,X0,X1] :
( v3_struct_0(sK84)
| k2_tex_4(sK84,X0) = k4_tex_4(sK84,X1)
| ~ l1_pre_topc(sK84)
| ~ m1_subset_1(X1,u1_struct_0(sK84))
| ~ r2_hidden(X2,k2_tex_4(sK84,X1))
| ~ m1_subset_1(X2,u1_struct_0(sK84))
| ~ r2_hidden(X0,k2_tex_4(sK84,X2))
| ~ m1_subset_1(X0,u1_struct_0(sK84)) )
| ~ spl848_27 ),
inference(resolution,[],[f45924,f45378]) ).
fof(f53871,plain,
( ! [X2,X0,X1] :
( sF847(X1) = k2_tex_4(sK84,X0)
| v3_struct_0(sK84)
| ~ l1_pre_topc(sK84)
| ~ m1_subset_1(X1,u1_struct_0(sK84))
| ~ r2_hidden(X2,k2_tex_4(sK84,X1))
| ~ m1_subset_1(X2,u1_struct_0(sK84))
| ~ r2_hidden(X0,k2_tex_4(sK84,X2))
| ~ m1_subset_1(X0,u1_struct_0(sK84)) )
| ~ spl848_27 ),
inference(forward_demodulation,[],[f53868,f45226]) ).
fof(f53873,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X1,sF844)
| sF847(X1) = k2_tex_4(sK84,X0)
| v3_struct_0(sK84)
| ~ l1_pre_topc(sK84)
| ~ r2_hidden(X2,k2_tex_4(sK84,X1))
| ~ m1_subset_1(X2,u1_struct_0(sK84))
| ~ r2_hidden(X0,k2_tex_4(sK84,X2))
| ~ m1_subset_1(X0,u1_struct_0(sK84)) )
| ~ spl848_27 ),
inference(forward_demodulation,[],[f53871,f45219]) ).
fof(f53875,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X2,sF844)
| ~ m1_subset_1(X1,sF844)
| sF847(X1) = k2_tex_4(sK84,X0)
| v3_struct_0(sK84)
| ~ l1_pre_topc(sK84)
| ~ r2_hidden(X2,k2_tex_4(sK84,X1))
| ~ r2_hidden(X0,k2_tex_4(sK84,X2))
| ~ m1_subset_1(X0,u1_struct_0(sK84)) )
| ~ spl848_27 ),
inference(forward_demodulation,[],[f53873,f45219]) ).
fof(f53880,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,sF844)
| ~ m1_subset_1(X2,sF844)
| ~ m1_subset_1(X1,sF844)
| sF847(X1) = k2_tex_4(sK84,X0)
| v3_struct_0(sK84)
| ~ l1_pre_topc(sK84)
| ~ r2_hidden(X2,k2_tex_4(sK84,X1))
| ~ r2_hidden(X0,k2_tex_4(sK84,X2)) )
| ~ spl848_27 ),
inference(forward_demodulation,[],[f53875,f45219]) ).
fof(f53882,definition,
( spl848_719
<=> ! [X2,X0,X1] :
( ~ m1_subset_1(X0,sF844)
| ~ r2_hidden(X0,k2_tex_4(sK84,X2))
| ~ m1_subset_1(X1,sF844)
| sF847(X1) = k2_tex_4(sK84,X0)
| ~ m1_subset_1(X2,sF844)
| ~ r2_hidden(X2,k2_tex_4(sK84,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl848_719])],[avatar_definition]) ).
fof(f53883,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,k2_tex_4(sK84,X2))
| ~ m1_subset_1(X0,sF844)
| ~ m1_subset_1(X1,sF844)
| sF847(X1) = k2_tex_4(sK84,X0)
| ~ m1_subset_1(X2,sF844)
| ~ r2_hidden(X2,k2_tex_4(sK84,X1)) )
| ~ spl848_719 ),
inference(avatar_component_clause,[],[f53882]) ).
fof(f53884,plain,
( ~ spl848_26
| spl848_28
| spl848_719
| ~ spl848_27 ),
inference(avatar_split_clause,[],[f53880,f45377,f53882,f45381,f45373]) ).
fof(f53897,plain,
( ! [X0] :
( ~ r2_hidden(X0,k2_tex_4(sK84,X0))
| ~ m1_subset_1(X0,sF844)
| ~ m1_subset_1(X0,sF844)
| sF847(X0) = k2_tex_4(sK84,X0)
| ~ m1_subset_1(X0,sF844) )
| ~ spl848_719 ),
inference(factoring,[],[f53883]) ).
fof(f53904,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X1,k4_tex_4(sK84,X0))
| ~ m1_subset_1(X1,sF844)
| ~ m1_subset_1(X2,sF844)
| k2_tex_4(sK84,X1) = sF847(X2)
| ~ m1_subset_1(X0,sF844)
| ~ r2_hidden(X0,k2_tex_4(sK84,X2))
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84)
| ~ m1_subset_1(X0,u1_struct_0(sK84)) )
| ~ spl848_719 ),
inference(superposition,[],[f53883,f39378]) ).
fof(f53906,plain,
( ! [X0] :
( ~ r2_hidden(X0,k2_tex_4(sK84,X0))
| ~ m1_subset_1(X0,sF844)
| sF847(X0) = k2_tex_4(sK84,X0) )
| ~ spl848_719 ),
inference(duplicate_literal_removal,[],[f53897]) ).
fof(f53909,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X1,sF847(X0))
| ~ m1_subset_1(X1,sF844)
| ~ m1_subset_1(X2,sF844)
| k2_tex_4(sK84,X1) = sF847(X2)
| ~ m1_subset_1(X0,sF844)
| ~ r2_hidden(X0,k2_tex_4(sK84,X2))
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84)
| ~ m1_subset_1(X0,u1_struct_0(sK84)) )
| ~ spl848_719 ),
inference(forward_demodulation,[],[f53904,f45226]) ).
fof(f53917,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,sF844)
| ~ r2_hidden(X1,sF847(X0))
| ~ m1_subset_1(X1,sF844)
| ~ m1_subset_1(X2,sF844)
| k2_tex_4(sK84,X1) = sF847(X2)
| ~ m1_subset_1(X0,sF844)
| ~ r2_hidden(X0,k2_tex_4(sK84,X2))
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84) )
| ~ spl848_719 ),
inference(forward_demodulation,[],[f53909,f45219]) ).
fof(f53918,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,sF844)
| ~ r2_hidden(X1,sF847(X0))
| ~ m1_subset_1(X1,sF844)
| ~ m1_subset_1(X2,sF844)
| k2_tex_4(sK84,X1) = sF847(X2)
| ~ r2_hidden(X0,k2_tex_4(sK84,X2))
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84) )
| ~ spl848_719 ),
inference(duplicate_literal_removal,[],[f53917]) ).
fof(f53927,definition,
( spl848_720
<=> ! [X2,X0,X1] :
( ~ m1_subset_1(X0,sF844)
| ~ r2_hidden(X0,k2_tex_4(sK84,X2))
| k2_tex_4(sK84,X1) = sF847(X2)
| ~ m1_subset_1(X2,sF844)
| ~ m1_subset_1(X1,sF844)
| ~ r2_hidden(X1,sF847(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl848_720])],[avatar_definition]) ).
fof(f53928,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,k2_tex_4(sK84,X2))
| ~ m1_subset_1(X0,sF844)
| k2_tex_4(sK84,X1) = sF847(X2)
| ~ m1_subset_1(X2,sF844)
| ~ m1_subset_1(X1,sF844)
| ~ r2_hidden(X1,sF847(X0)) )
| ~ spl848_720 ),
inference(avatar_component_clause,[],[f53927]) ).
fof(f53929,plain,
( ~ spl848_26
| ~ spl848_27
| spl848_28
| spl848_720
| ~ spl848_719 ),
inference(avatar_split_clause,[],[f53918,f53882,f53927,f45381,f45377,f45373]) ).
fof(f53962,plain,
( ~ m1_subset_1(sK127(sK84,sK85,sK86,sF845),sF844)
| k2_tex_4(sK84,sK127(sK84,sK85,sK86,sF845)) = sF847(sK127(sK84,sK85,sK86,sF845))
| ~ spl848_151
| ~ spl848_231
| ~ spl848_719 ),
inference(resolution,[],[f53906,f47665]) ).
fof(f54104,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X1,k4_tex_4(sK84,X0))
| ~ m1_subset_1(X1,sF844)
| sF847(X0) = k2_tex_4(sK84,X2)
| ~ m1_subset_1(X0,sF844)
| ~ m1_subset_1(X2,sF844)
| ~ r2_hidden(X2,sF847(X1))
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84)
| ~ m1_subset_1(X0,u1_struct_0(sK84)) )
| ~ spl848_720 ),
inference(superposition,[],[f53928,f39378]) ).
fof(f54108,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X1,sF847(X0))
| ~ m1_subset_1(X1,sF844)
| sF847(X0) = k2_tex_4(sK84,X2)
| ~ m1_subset_1(X0,sF844)
| ~ m1_subset_1(X2,sF844)
| ~ r2_hidden(X2,sF847(X1))
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84)
| ~ m1_subset_1(X0,u1_struct_0(sK84)) )
| ~ spl848_720 ),
inference(forward_demodulation,[],[f54104,f45226]) ).
fof(f54120,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,sF844)
| ~ r2_hidden(X1,sF847(X0))
| ~ m1_subset_1(X1,sF844)
| sF847(X0) = k2_tex_4(sK84,X2)
| ~ m1_subset_1(X0,sF844)
| ~ m1_subset_1(X2,sF844)
| ~ r2_hidden(X2,sF847(X1))
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84) )
| ~ spl848_720 ),
inference(forward_demodulation,[],[f54108,f45219]) ).
fof(f54121,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,sF844)
| ~ r2_hidden(X1,sF847(X0))
| ~ m1_subset_1(X1,sF844)
| sF847(X0) = k2_tex_4(sK84,X2)
| ~ m1_subset_1(X2,sF844)
| ~ r2_hidden(X2,sF847(X1))
| v3_struct_0(sK84)
| ~ v2_pre_topc(sK84)
| ~ l1_pre_topc(sK84) )
| ~ spl848_720 ),
inference(duplicate_literal_removal,[],[f54120]) ).
fof(f54130,definition,
( spl848_733
<=> ! [X2,X0,X1] :
( ~ m1_subset_1(X0,sF844)
| ~ r2_hidden(X2,sF847(X1))
| ~ m1_subset_1(X2,sF844)
| sF847(X0) = k2_tex_4(sK84,X2)
| ~ m1_subset_1(X1,sF844)
| ~ r2_hidden(X1,sF847(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl848_733])],[avatar_definition]) ).
fof(f54131,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,sF844)
| ~ r2_hidden(X2,sF847(X1))
| ~ m1_subset_1(X2,sF844)
| sF847(X0) = k2_tex_4(sK84,X2)
| ~ m1_subset_1(X1,sF844)
| ~ r2_hidden(X1,sF847(X0)) )
| ~ spl848_733 ),
inference(avatar_component_clause,[],[f54130]) ).
fof(f54132,plain,
( ~ spl848_26
| ~ spl848_27
| spl848_28
| spl848_733
| ~ spl848_720 ),
inference(avatar_split_clause,[],[f54121,f53927,f54130,f45381,f45377,f45373]) ).
fof(f54166,definition,
( spl848_739
<=> r2_hidden(k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845)),sF845) ),
introduced(definition,[new_symbols(definition,[spl848_739])],[avatar_definition]) ).
fof(f54168,plain,
( r2_hidden(k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845)),sF845)
| ~ spl848_739 ),
inference(avatar_component_clause,[],[f54166]) ).
fof(f54169,plain,
( ~ spl848_18
| ~ spl848_20
| spl848_739
| spl848_19
| ~ spl848_21
| spl848_31
| ~ spl848_72
| ~ spl848_704 ),
inference(avatar_split_clause,[],[f53741,f53618,f45671,f45405,f45344,f45336,f54166,f45340,f45332]) ).
fof(f54182,definition,
( spl848_742
<=> k2_tex_4(sK84,sK127(sK84,sK85,sK86,sF845)) = sF847(sK127(sK84,sK85,sK86,sF845)) ),
introduced(definition,[new_symbols(definition,[spl848_742])],[avatar_definition]) ).
fof(f54184,plain,
( k2_tex_4(sK84,sK127(sK84,sK85,sK86,sF845)) = sF847(sK127(sK84,sK85,sK86,sF845))
| ~ spl848_742 ),
inference(avatar_component_clause,[],[f54182]) ).
fof(f54186,plain,
( spl848_742
| ~ spl848_151
| ~ spl848_151
| ~ spl848_231
| ~ spl848_719 ),
inference(avatar_split_clause,[],[f53962,f53882,f47632,f46926,f46926,f54182]) ).
fof(f54292,definition,
( spl848_751
<=> ! [X0,X1] :
( ~ r2_hidden(X0,sF847(sK127(sK84,sK85,sK86,sF845)))
| k2_tex_4(sK84,X1) = sF847(sK127(sK84,sK85,sK86,sF845))
| ~ r2_hidden(X1,sF847(X0))
| ~ m1_subset_1(X1,sF844)
| ~ m1_subset_1(X0,sF844) ) ),
introduced(definition,[new_symbols(definition,[spl848_751])],[avatar_definition]) ).
fof(f54293,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF844)
| k2_tex_4(sK84,X1) = sF847(sK127(sK84,sK85,sK86,sF845))
| ~ r2_hidden(X1,sF847(X0))
| ~ r2_hidden(X0,sF847(sK127(sK84,sK85,sK86,sF845)))
| ~ m1_subset_1(X0,sF844) )
| ~ spl848_751 ),
inference(avatar_component_clause,[],[f54292]) ).
fof(f54323,plain,
( ~ m1_subset_1(k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845)),sF844)
| k1_struct_0(sK84,k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845))) = k5_subset_1(sF844,sF845,sF847(k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845))))
| ~ spl848_205
| ~ spl848_739 ),
inference(resolution,[],[f54168,f47430]) ).
fof(f54337,definition,
( spl848_753
<=> sF847(sK127(sK84,sK85,sK86,sF845)) = sF847(k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845))) ),
introduced(definition,[new_symbols(definition,[spl848_753])],[avatar_definition]) ).
fof(f54339,plain,
( sF847(sK127(sK84,sK85,sK86,sF845)) = sF847(k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845)))
| ~ spl848_753 ),
inference(avatar_component_clause,[],[f54337]) ).
fof(f54343,definition,
( spl848_754
<=> k1_struct_0(sK84,k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845))) = k5_subset_1(sF844,sF845,sF847(k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845)))) ),
introduced(definition,[new_symbols(definition,[spl848_754])],[avatar_definition]) ).
fof(f54345,plain,
( k1_struct_0(sK84,k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845))) = k5_subset_1(sF844,sF845,sF847(k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845))))
| ~ spl848_754 ),
inference(avatar_component_clause,[],[f54343]) ).
fof(f54347,definition,
( spl848_755
<=> m1_subset_1(k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845)),sF844) ),
introduced(definition,[new_symbols(definition,[spl848_755])],[avatar_definition]) ).
fof(f54348,plain,
( m1_subset_1(k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845)),sF844)
| ~ spl848_755 ),
inference(avatar_component_clause,[],[f54347]) ).
fof(f54349,plain,
( ~ m1_subset_1(k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845)),sF844)
| spl848_755 ),
inference(avatar_component_clause,[],[f54347]) ).
fof(f54350,plain,
( spl848_754
| ~ spl848_755
| ~ spl848_205
| ~ spl848_739 ),
inference(avatar_split_clause,[],[f54323,f54166,f47429,f54347,f54343]) ).
fof(f54352,definition,
( spl848_756
<=> sF847(sK127(sK84,sK85,sK86,sF845)) = k2_tex_4(sK84,k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845))) ),
introduced(definition,[new_symbols(definition,[spl848_756])],[avatar_definition]) ).
fof(f54359,plain,
( ~ r2_hidden(k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845)),sF845)
| ~ spl848_74
| spl848_755 ),
inference(resolution,[],[f54349,f45719]) ).
fof(f54363,plain,
( ~ spl848_739
| ~ spl848_74
| spl848_755 ),
inference(avatar_split_clause,[],[f54359,f54347,f45718,f54166]) ).
fof(f54380,plain,
( sF847(sK127(sK84,sK85,sK86,sF845)) = sF847(k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845)))
| k2_tex_4(sK84,sK127(sK84,sK85,sK86,sF845)) != k2_tex_4(sK84,k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845)))
| ~ spl848_300
| ~ spl848_755 ),
inference(resolution,[],[f54348,f48265]) ).
fof(f54417,definition,
( spl848_761
<=> r2_hidden(k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845)),sF847(sK127(sK84,sK85,sK86,sF845))) ),
introduced(definition,[new_symbols(definition,[spl848_761])],[avatar_definition]) ).
fof(f54419,plain,
( ~ r2_hidden(k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845)),sF847(sK127(sK84,sK85,sK86,sF845)))
| spl848_761 ),
inference(avatar_component_clause,[],[f54417]) ).
fof(f54431,plain,
( sF847(sK127(sK84,sK85,sK86,sF845)) != k2_tex_4(sK84,k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845)))
| sF847(sK127(sK84,sK85,sK86,sF845)) = sF847(k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845)))
| ~ spl848_300
| ~ spl848_742
| ~ spl848_755 ),
inference(forward_demodulation,[],[f54380,f54184]) ).
fof(f54457,plain,
( spl848_753
| ~ spl848_756
| ~ spl848_300
| ~ spl848_742
| ~ spl848_755 ),
inference(avatar_split_clause,[],[f54431,f54347,f54182,f48264,f54352,f54337]) ).
fof(f54467,plain,
( ~ r2_hidden(sF846(sK127(sK84,sK85,sK86,sF845)),sF847(sK127(sK84,sK85,sK86,sF845)))
| ~ m1_subset_1(sK127(sK84,sK85,sK86,sF845),sF844)
| ~ spl848_33
| spl848_761 ),
inference(superposition,[],[f54419,f45420]) ).
fof(f54472,definition,
( spl848_770
<=> ! [X0] :
( ~ r2_hidden(k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845)),sF847(X0))
| ~ r2_hidden(X0,sF847(sK127(sK84,sK85,sK86,sF845)))
| ~ m1_subset_1(X0,sF844) ) ),
introduced(definition,[new_symbols(definition,[spl848_770])],[avatar_definition]) ).
fof(f54473,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF844)
| ~ r2_hidden(X0,sF847(sK127(sK84,sK85,sK86,sF845)))
| ~ r2_hidden(k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845)),sF847(X0)) )
| ~ spl848_770 ),
inference(avatar_component_clause,[],[f54472]) ).
fof(f54483,plain,
( ~ spl848_151
| ~ spl848_315
| ~ spl848_33
| spl848_761 ),
inference(avatar_split_clause,[],[f54467,f54417,f45419,f48401,f46926]) ).
fof(f55157,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF847(X1))
| ~ m1_subset_1(X0,sF844)
| k2_tex_4(sK84,X0) = sF847(sK127(sK84,sK85,sK86,sF845))
| ~ m1_subset_1(X1,sF844)
| ~ r2_hidden(X1,sF847(sK127(sK84,sK85,sK86,sF845))) )
| ~ spl848_151
| ~ spl848_733 ),
inference(resolution,[],[f54131,f46927]) ).
fof(f55168,plain,
( spl848_751
| ~ spl848_151
| ~ spl848_733 ),
inference(avatar_split_clause,[],[f55157,f54130,f46926,f54292]) ).
fof(f55925,plain,
( k5_subset_1(sF844,sF845,sF847(sK127(sK84,sK85,sK86,sF845))) = k1_struct_0(sK84,k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845)))
| ~ spl848_753
| ~ spl848_754 ),
inference(forward_demodulation,[],[f54345,f54339]) ).
fof(f55950,plain,
( ! [X0] :
( sF847(sK127(sK84,sK85,sK86,sF845)) = k2_tex_4(sK84,k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845)))
| ~ r2_hidden(k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845)),sF847(X0))
| ~ r2_hidden(X0,sF847(sK127(sK84,sK85,sK86,sF845)))
| ~ m1_subset_1(X0,sF844) )
| ~ spl848_751
| ~ spl848_755 ),
inference(resolution,[],[f54293,f54348]) ).
fof(f55982,plain,
( spl848_770
| spl848_756
| ~ spl848_751
| ~ spl848_755 ),
inference(avatar_split_clause,[],[f55950,f54347,f54292,f54352,f54472]) ).
fof(f57005,plain,
( ~ r2_hidden(sK127(sK84,sK85,sK86,sF845),sF847(sK127(sK84,sK85,sK86,sF845)))
| ~ r2_hidden(k1_funct_1(sK86,sK127(sK84,sK85,sK86,sF845)),sF847(sK127(sK84,sK85,sK86,sF845)))
| ~ spl848_151
| ~ spl848_770 ),
inference(resolution,[],[f54473,f46927]) ).
fof(f57014,plain,
( ~ spl848_761
| ~ spl848_232
| ~ spl848_151
| ~ spl848_770 ),
inference(avatar_split_clause,[],[f57005,f54472,f46926,f47698,f54417]) ).
fof(f72748,plain,
( k5_subset_1(sF844,sF845,sF847(sK127(sK84,sK85,sK86,sF845))) = k1_struct_0(sK84,sF846(sK127(sK84,sK85,sK86,sF845)))
| ~ m1_subset_1(sK127(sK84,sK85,sK86,sF845),sF844)
| ~ spl848_33
| ~ spl848_753
| ~ spl848_754 ),
inference(superposition,[],[f55925,f45420]) ).
fof(f72769,definition,
( spl848_2248
<=> k5_subset_1(sF844,sF845,sF847(sK127(sK84,sK85,sK86,sF845))) = k1_struct_0(sK84,sF846(sK127(sK84,sK85,sK86,sF845))) ),
introduced(definition,[new_symbols(definition,[spl848_2248])],[avatar_definition]) ).
fof(f72771,plain,
( k5_subset_1(sF844,sF845,sF847(sK127(sK84,sK85,sK86,sF845))) = k1_struct_0(sK84,sF846(sK127(sK84,sK85,sK86,sF845)))
| ~ spl848_2248 ),
inference(avatar_component_clause,[],[f72769]) ).
fof(f72772,plain,
( ~ spl848_151
| spl848_2248
| ~ spl848_33
| ~ spl848_753
| ~ spl848_754 ),
inference(avatar_split_clause,[],[f72748,f54343,f54337,f45419,f72769,f46926]) ).
fof(f72799,plain,
( k1_struct_0(sK85,sF846(sK127(sK84,sK85,sK86,sF845))) != k1_struct_0(sK84,sF846(sK127(sK84,sK85,sK86,sF845)))
| ~ r2_hidden(sK127(sK84,sK85,sK86,sF845),sF847(sK127(sK84,sK85,sK86,sF845)))
| ~ m1_subset_1(sK127(sK84,sK85,sK86,sF845),sF844)
| ~ spl848_194
| ~ spl848_2248 ),
inference(superposition,[],[f47277,f72771]) ).
fof(f72806,plain,
( k1_struct_0(sK84,sF846(sK127(sK84,sK85,sK86,sF845))) != k1_struct_0(sK84,sF846(sK127(sK84,sK85,sK86,sF845)))
| ~ r2_hidden(sK127(sK84,sK85,sK86,sF845),sF847(sK127(sK84,sK85,sK86,sF845)))
| ~ m1_subset_1(sK127(sK84,sK85,sK86,sF845),sF844)
| ~ spl848_194
| ~ spl848_521
| ~ spl848_2248 ),
inference(forward_demodulation,[],[f72799,f50419]) ).
fof(f72807,plain,
( ~ r2_hidden(sK127(sK84,sK85,sK86,sF845),sF847(sK127(sK84,sK85,sK86,sF845)))
| ~ m1_subset_1(sK127(sK84,sK85,sK86,sF845),sF844)
| ~ spl848_194
| ~ spl848_521
| ~ spl848_2248 ),
inference(trivial_inequality_removal,[],[f72806]) ).
fof(f72823,plain,
( ~ spl848_151
| ~ spl848_232
| ~ spl848_194
| ~ spl848_521
| ~ spl848_2248 ),
inference(avatar_split_clause,[],[f72807,f72769,f50417,f47276,f47698,f46926]) ).
cnf(s13,plain,
( ~ spl848_18
| ~ spl848_19
| ~ spl848_20
| ~ spl848_21 ),
inference(sat_conversion,[],[f45347]) ).
cnf(s14,plain,
spl848_20,
inference(sat_conversion,[],[f45348]) ).
cnf(s15,plain,
spl848_18,
inference(sat_conversion,[],[f45349]) ).
cnf(s16,plain,
spl848_21,
inference(sat_conversion,[],[f45350]) ).
cnf(s19,plain,
( ~ spl848_26
| ~ spl848_27
| spl848_28
| spl848_29 ),
inference(sat_conversion,[],[f45389]) ).
cnf(s21,plain,
spl848_27,
inference(sat_conversion,[],[f45392]) ).
cnf(s23,plain,
spl848_26,
inference(sat_conversion,[],[f45395]) ).
cnf(s25,plain,
~ spl848_28,
inference(sat_conversion,[],[f45398]) ).
cnf(s26,plain,
( ~ spl848_20
| ~ spl848_21
| ~ spl848_30
| spl848_31
| spl848_32 ),
inference(sat_conversion,[],[f45411]) ).
cnf(s27,plain,
( spl848_22
| ~ spl848_26 ),
inference(sat_conversion,[],[f45413]) ).
cnf(s29,plain,
( ~ spl848_20
| ~ spl848_21
| ~ spl848_30
| spl848_31
| spl848_33 ),
inference(sat_conversion,[],[f45422]) ).
cnf(s33,plain,
~ spl848_24,
inference(sat_conversion,[],[f45437]) ).
cnf(s36,plain,
( ~ spl848_18
| spl848_30 ),
inference(sat_conversion,[],[f45459]) ).
cnf(s37,plain,
( ~ spl848_26
| spl848_28
| ~ spl848_40
| spl848_41 ),
inference(sat_conversion,[],[f45470]) ).
cnf(s52,plain,
( spl848_24
| ~ spl848_26
| ~ spl848_27
| spl848_28
| ~ spl848_40
| spl848_62 ),
inference(sat_conversion,[],[f45602]) ).
cnf(s55,plain,
( ~ spl848_22
| spl848_65 ),
inference(sat_conversion,[],[f45622]) ).
cnf(s56,plain,
( ~ spl848_26
| spl848_63 ),
inference(sat_conversion,[],[f45624]) ).
cnf(s61,plain,
( spl848_24
| spl848_71 ),
inference(sat_conversion,[],[f45667]) ).
cnf(s62,plain,
( ~ spl848_26
| ~ spl848_27
| spl848_28
| ~ spl848_40
| ~ spl848_41
| ~ spl848_58
| ~ spl848_71
| spl848_72 ),
inference(sat_conversion,[],[f45673]) ).
cnf(s73,plain,
spl848_40,
inference(sat_conversion,[],[f45735]) ).
cnf(s74,plain,
( ~ spl848_41
| spl848_74 ),
inference(sat_conversion,[],[f45738]) ).
cnf(s76,plain,
spl848_58,
inference(sat_conversion,[],[f45741]) ).
cnf(s90,plain,
( ~ spl848_26
| ~ spl848_27
| spl848_28
| spl848_83 ),
inference(sat_conversion,[],[f45998]) ).
cnf(s91,plain,
( ~ spl848_26
| ~ spl848_27
| spl848_28
| ~ spl848_83
| spl848_84 ),
inference(sat_conversion,[],[f46023]) ).
cnf(s96,plain,
( ~ spl848_26
| ~ spl848_27
| spl848_28
| ~ spl848_83
| spl848_89 ),
inference(sat_conversion,[],[f46050]) ).
cnf(s113,plain,
( ~ spl848_63
| spl848_101 ),
inference(sat_conversion,[],[f46275]) ).
cnf(s122,plain,
( spl848_24
| ~ spl848_65
| ~ spl848_101
| spl848_108 ),
inference(sat_conversion,[],[f46329]) ).
cnf(s128,plain,
( ~ spl848_63
| ~ spl848_108
| spl848_112 ),
inference(sat_conversion,[],[f46361]) ).
cnf(s138,plain,
( spl848_28
| ~ spl848_31
| ~ spl848_63 ),
inference(sat_conversion,[],[f46517]) ).
cnf(s144,plain,
( ~ spl848_26
| ~ spl848_27
| spl848_28
| spl848_124 ),
inference(sat_conversion,[],[f46574]) ).
cnf(s145,plain,
( spl848_24
| ~ spl848_65
| spl848_125 ),
inference(sat_conversion,[],[f46591]) ).
cnf(s146,plain,
( spl848_28
| ~ spl848_63
| spl848_126 ),
inference(sat_conversion,[],[f46595]) ).
cnf(s151,plain,
( spl848_24
| ~ spl848_40
| ~ spl848_58
| ~ spl848_124
| spl848_130 ),
inference(sat_conversion,[],[f46656]) ).
cnf(s160,plain,
( ~ spl848_18
| ~ spl848_20
| ~ spl848_21
| ~ spl848_112
| spl848_138 ),
inference(sat_conversion,[],[f46733]) ).
cnf(s183,plain,
( ~ spl848_18
| spl848_19
| ~ spl848_20
| ~ spl848_21
| ~ spl848_72
| spl848_151 ),
inference(sat_conversion,[],[f46990]) ).
cnf(s209,plain,
( ~ spl848_26
| ~ spl848_27
| spl848_28
| spl848_185 ),
inference(sat_conversion,[],[f47181]) ).
cnf(s217,plain,
( ~ spl848_18
| spl848_19
| ~ spl848_20
| ~ spl848_21
| ~ spl848_130
| spl848_192 ),
inference(sat_conversion,[],[f47265]) ).
cnf(s218,plain,
( ~ spl848_41
| ~ spl848_192
| ~ spl848_193 ),
inference(sat_conversion,[],[f47271]) ).
cnf(s219,plain,
( ~ spl848_84
| ~ spl848_151
| spl848_193
| spl848_194 ),
inference(sat_conversion,[],[f47278]) ).
cnf(s228,plain,
( spl848_24
| ~ spl848_62
| spl848_204 ),
inference(sat_conversion,[],[f47423]) ).
cnf(s229,plain,
( ~ spl848_26
| spl848_28
| ~ spl848_40
| ~ spl848_41
| ~ spl848_185
| ~ spl848_204
| spl848_205 ),
inference(sat_conversion,[],[f47431]) ).
cnf(s256,plain,
( ~ spl848_26
| spl848_28
| spl848_231 ),
inference(sat_conversion,[],[f47634]) ).
cnf(s257,plain,
( ~ spl848_151
| ~ spl848_27
| spl848_28
| ~ spl848_26
| ~ spl848_151
| ~ spl848_231
| spl848_232 ),
inference(sat_conversion,[],[f47701]) ).
cnf(s258,plain,
( ~ spl848_26
| ~ spl848_27
| spl848_28
| ~ spl848_151
| ~ spl848_231
| spl848_232 ),
inference(rat,[],[s257]) ).
cnf(s267,plain,
( ~ spl848_29
| ~ spl848_89
| ~ spl848_151
| ~ spl848_232
| spl848_238 ),
inference(sat_conversion,[],[f47737]) ).
cnf(s281,plain,
( ~ spl848_29
| ~ spl848_151
| spl848_239 ),
inference(sat_conversion,[],[f47810]) ).
cnf(s357,plain,
( ~ spl848_18
| spl848_19
| ~ spl848_20
| ~ spl848_21
| ~ spl848_72
| ~ spl848_231
| spl848_298 ),
inference(sat_conversion,[],[f48235]) ).
cnf(s359,plain,
( ~ spl848_83
| ~ spl848_151
| ~ spl848_298
| spl848_300 ),
inference(sat_conversion,[],[f48266]) ).
cnf(s361,plain,
( ~ spl848_26
| ~ spl848_27
| spl848_28
| ~ spl848_151
| ~ spl848_298
| spl848_302 ),
inference(sat_conversion,[],[f48283]) ).
cnf(s367,plain,
( ~ spl848_26
| ~ spl848_27
| spl848_28
| ~ spl848_302
| spl848_306 ),
inference(sat_conversion,[],[f48344]) ).
cnf(s376,plain,
( ~ spl848_238
| ~ spl848_239
| ~ spl848_306
| spl848_315 ),
inference(sat_conversion,[],[f48404]) ).
cnf(s642,plain,
( ~ spl848_32
| ~ spl848_125
| ~ spl848_126
| ~ spl848_151
| ~ spl848_239
| spl848_521 ),
inference(sat_conversion,[],[f50421]) ).
cnf(s928,plain,
( ~ spl848_18
| ~ spl848_21
| ~ spl848_30
| ~ spl848_138
| spl848_704 ),
inference(sat_conversion,[],[f53620]) ).
cnf(s938,plain,
( ~ spl848_26
| ~ spl848_27
| spl848_28
| spl848_719 ),
inference(sat_conversion,[],[f53884]) ).
cnf(s939,plain,
( ~ spl848_26
| ~ spl848_27
| spl848_28
| ~ spl848_719
| spl848_720 ),
inference(sat_conversion,[],[f53929]) ).
cnf(s953,plain,
( ~ spl848_26
| ~ spl848_27
| spl848_28
| ~ spl848_720
| spl848_733 ),
inference(sat_conversion,[],[f54132]) ).
cnf(s962,plain,
( ~ spl848_18
| spl848_19
| ~ spl848_20
| ~ spl848_21
| spl848_31
| ~ spl848_72
| ~ spl848_704
| spl848_739 ),
inference(sat_conversion,[],[f54169]) ).
cnf(s966,plain,
( ~ spl848_151
| ~ spl848_151
| ~ spl848_231
| ~ spl848_719
| spl848_742 ),
inference(sat_conversion,[],[f54186]) ).
cnf(s967,plain,
( ~ spl848_151
| ~ spl848_231
| ~ spl848_719
| spl848_742 ),
inference(rat,[],[s966]) ).
cnf(s981,plain,
( ~ spl848_205
| ~ spl848_739
| spl848_754
| ~ spl848_755 ),
inference(sat_conversion,[],[f54350]) ).
cnf(s984,plain,
( ~ spl848_74
| ~ spl848_739
| spl848_755 ),
inference(sat_conversion,[],[f54363]) ).
cnf(s1000,plain,
( ~ spl848_300
| ~ spl848_742
| spl848_753
| ~ spl848_755
| ~ spl848_756 ),
inference(sat_conversion,[],[f54457]) ).
cnf(s1006,plain,
( ~ spl848_33
| ~ spl848_151
| ~ spl848_315
| spl848_761 ),
inference(sat_conversion,[],[f54483]) ).
cnf(s1103,plain,
( ~ spl848_151
| ~ spl848_733
| spl848_751 ),
inference(sat_conversion,[],[f55168]) ).
cnf(s1225,plain,
( ~ spl848_751
| ~ spl848_755
| spl848_756
| spl848_770 ),
inference(sat_conversion,[],[f55982]) ).
cnf(s1343,plain,
( ~ spl848_151
| ~ spl848_232
| ~ spl848_761
| ~ spl848_770 ),
inference(sat_conversion,[],[f57014]) ).
cnf(s3433,plain,
( ~ spl848_33
| ~ spl848_151
| ~ spl848_753
| ~ spl848_754
| spl848_2248 ),
inference(sat_conversion,[],[f72772]) ).
cnf(s3443,plain,
( ~ spl848_151
| ~ spl848_194
| ~ spl848_232
| ~ spl848_521
| ~ spl848_2248 ),
inference(sat_conversion,[],[f72823]) ).
cnf(s3447,plain,
( ~ spl848_26
| ~ spl848_27
| spl848_28
| ~ spl848_41
| ~ spl848_71
| spl848_72 ),
inference(rat,[],[s62,s76,s73]) ).
cnf(s3448,plain,
( spl848_24
| ~ spl848_26
| ~ spl848_27
| spl848_28
| spl848_62 ),
inference(rat,[],[s52,s73]) ).
cnf(s3450,plain,
( ~ spl848_26
| spl848_28
| spl848_41 ),
inference(rat,[],[s37,s73]) ).
cnf(s3451,plain,
spl848_71,
inference(rat,[],[s61,s33]) ).
cnf(s3456,plain,
spl848_231,
inference(rat,[],[s256,s25,s23]) ).
cnf(s3461,plain,
spl848_63,
inference(rat,[],[s56,s23]) ).
cnf(s3463,plain,
spl848_41,
inference(rat,[],[s3450,s25,s23]) ).
cnf(s3465,plain,
spl848_22,
inference(rat,[],[s27,s23]) ).
cnf(s3467,plain,
spl848_126,
inference(rat,[],[s146,s25,s3461]) ).
cnf(s3468,plain,
spl848_101,
inference(rat,[],[s113,s3461]) ).
cnf(s3471,plain,
~ spl848_31,
inference(rat,[],[s138,s25,s3461]) ).
cnf(s3472,plain,
spl848_74,
inference(rat,[],[s74,s3463]) ).
cnf(s3478,plain,
spl848_65,
inference(rat,[],[s55,s3465]) ).
cnf(s3483,plain,
spl848_125,
inference(rat,[],[s145,s33,s3478]) ).
cnf(s3485,plain,
spl848_108,
inference(rat,[],[s122,s3468,s33,s3478]) ).
cnf(s3490,plain,
spl848_112,
inference(rat,[],[s128,s3461,s3485]) ).
cnf(s3499,plain,
spl848_719,
inference(rat,[],[s938,s23,s25,s21]) ).
cnf(s3502,plain,
spl848_185,
inference(rat,[],[s209,s23,s25,s21]) ).
cnf(s3506,plain,
spl848_124,
inference(rat,[],[s144,s23,s25,s21]) ).
cnf(s3507,plain,
spl848_83,
inference(rat,[],[s90,s23,s25,s21]) ).
cnf(s3511,plain,
spl848_72,
inference(rat,[],[s3447,s3463,s3451,s23,s25,s21]) ).
cnf(s3518,plain,
spl848_62,
inference(rat,[],[s3448,s23,s25,s33,s21]) ).
cnf(s3525,plain,
spl848_720,
inference(rat,[],[s939,s21,s23,s25,s3499]) ).
cnf(s3530,plain,
spl848_130,
inference(rat,[],[s151,s33,s73,s76,s3506]) ).
cnf(s3533,plain,
spl848_89,
inference(rat,[],[s96,s21,s23,s25,s3507]) ).
cnf(s3536,plain,
spl848_84,
inference(rat,[],[s91,s21,s23,s25,s3507]) ).
cnf(s3543,plain,
spl848_204,
inference(rat,[],[s228,s33,s3518]) ).
cnf(s3548,plain,
spl848_733,
inference(rat,[],[s953,s21,s23,s25,s3525]) ).
cnf(s3595,plain,
spl848_205,
inference(rat,[],[s229,s3502,s3463,s23,s25,s73,s3543]) ).
cnf(s3600,plain,
spl848_29,
inference(rat,[],[s19,s25,s21,s23]) ).
cnf(s3603,plain,
spl848_30,
inference(rat,[],[s36,s15]) ).
cnf(s3608,plain,
spl848_138,
inference(rat,[],[s160,s15,s3490,s16,s14]) ).
cnf(s3610,plain,
spl848_33,
inference(rat,[],[s29,s3603,s3471,s16,s14]) ).
cnf(s3611,plain,
spl848_32,
inference(rat,[],[s26,s3603,s3471,s16,s14]) ).
cnf(s3619,plain,
spl848_704,
inference(rat,[],[s928,s3603,s15,s16,s3608]) ).
cnf(s3643,plain,
~ spl848_19,
inference(rat,[],[s13,s16,s14,s15]) ).
cnf(s3644,plain,
spl848_739,
inference(rat,[],[s962,s3619,s14,s3511,s3471,s16,s15,s3643]) ).
cnf(s3645,plain,
spl848_298,
inference(rat,[],[s357,s14,s3456,s3511,s16,s15,s3643]) ).
cnf(s3646,plain,
spl848_192,
inference(rat,[],[s217,s14,s3530,s16,s15,s3643]) ).
cnf(s3647,plain,
spl848_151,
inference(rat,[],[s183,s14,s3511,s16,s15,s3643]) ).
cnf(s3650,plain,
spl848_755,
inference(rat,[],[s984,s3472,s3644]) ).
cnf(s3651,plain,
spl848_754,
inference(rat,[],[s981,s3650,s3595,s3644]) ).
cnf(s3652,plain,
~ spl848_193,
inference(rat,[],[s218,s3463,s3646]) ).
cnf(s3653,plain,
spl848_751,
inference(rat,[],[s1103,s3548,s3647]) ).
cnf(s3655,plain,
spl848_742,
inference(rat,[],[s967,s3499,s3456,s3647]) ).
cnf(s3661,plain,
spl848_300,
inference(rat,[],[s359,s3645,s3507,s3647]) ).
cnf(s3663,plain,
spl848_239,
inference(rat,[],[s281,s3600,s3647]) ).
cnf(s3667,plain,
spl848_302,
inference(rat,[],[s361,s3645,s21,s23,s25,s3647]) ).
cnf(s3670,plain,
spl848_232,
inference(rat,[],[s258,s21,s3456,s23,s25,s3647]) ).
cnf(s3679,plain,
spl848_194,
inference(rat,[],[s219,s3647,s3536,s3652]) ).
cnf(s3705,plain,
spl848_521,
inference(rat,[],[s642,s3647,s3611,s3483,s3467,s3663]) ).
cnf(s3723,plain,
spl848_306,
inference(rat,[],[s367,s21,s23,s25,s3667]) ).
cnf(s3726,plain,
spl848_238,
inference(rat,[],[s267,s3647,s3600,s3533,s3670]) ).
cnf(s3748,plain,
~ spl848_2248,
inference(rat,[],[s3443,s3670,s3705,s3647,s3679]) ).
cnf(s3830,plain,
spl848_315,
inference(rat,[],[s376,s3723,s3663,s3726]) ).
cnf(s3840,plain,
~ spl848_753,
inference(rat,[],[s3433,s3647,s3651,s3610,s3748]) ).
cnf(s3917,plain,
spl848_761,
inference(rat,[],[s1006,s3647,s3610,s3830]) ).
cnf(s3944,plain,
~ spl848_756,
inference(rat,[],[s1000,s3661,s3650,s3655,s3840]) ).
cnf(s3987,plain,
~ spl848_770,
inference(rat,[],[s1343,s3670,s3647,s3917]) ).
cnf(s3992,plain,
$false,
inference(rat,[],[s1225,s3653,s3650,s3987,s3944]) ).
fof(f72824,plain,
$false,
inference(avatar_sat_refutation,[],[s3992]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP032+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.24 % Computer : n018.cluster.edu
% 0.10/0.24 % Model : x86_64 x86_64
% 0.10/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.24 % Memory : 8046.5625MB
% 0.10/0.24 % OS : Linux 6.8.0-71-generic
% 0.10/0.24 % CPULimit : 300
% 0.10/0.24 % WCLimit : 300
% 0.10/0.24 % DateTime : Mon Sep 28 18:57:15 UTC 2026
% 0.10/0.24 % CPUTime :
% 0.10/0.24 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.23/0.29 Running first-order theorem proving
% 0.23/0.29 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 27.25/6.99 % (3670085)Detected formulas, will run a generic FOF schedule.
% 27.25/6.99 % (3670095)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1518173614:i=109:sd=1:ins=1:gsp=on:ss=axioms_2974 on theBenchmark for (2974ds/109Mi)
% 27.25/6.99 % (3670096)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=310893826:i=119:av=off:ss=axioms_2974 on theBenchmark for (2974ds/119Mi)
% 27.25/6.99 % (3670095)Instruction limit reached!
% 27.25/6.99 % (3670095)------------------------------
% 27.25/6.99 % (3670095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.25/6.99 % (3670095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.25/6.99 % (3670095)CaDiCaL version: 2.1.3
% 27.25/6.99 % (3670095)Termination reason: Instruction limit
% 27.25/6.99 % (3670095)Termination phase: SInE selection
% 27.25/6.99 % (3670095)Time elapsed: 0.071 s
% 27.25/6.99 % (3670095)Peak memory usage: 136 MB
% 27.25/6.99 % (3670095)Instructions burned: 111 (million)
% 27.25/6.99 % (3670092)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=4072722224:i=141193_2974 on theBenchmark for (2974ds/141193Mi)
% 27.25/6.99 % (3670093)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=1728710837:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2974 on theBenchmark for (2974ds/134677Mi)
% 27.25/6.99 % (3670094)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=3102457626:i=141695:sd=1:nm=32:gsp=on:ss=included_2974 on theBenchmark for (2974ds/141695Mi)
% 27.25/6.99 % (3670098)dis-21_1_sil=8000:lcm=predicate:random_seed=3623896031:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2974 on theBenchmark for (2974ds/129Mi)
% 27.25/6.99 % (3670097)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=106874658:s2a=on:i=139:gtg=position_2974 on theBenchmark for (2974ds/139Mi)
% 27.25/6.99 % (3670096)Instruction limit reached!
% 27.25/6.99 % (3670096)------------------------------
% 27.25/6.99 % (3670096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.25/6.99 % (3670096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.25/6.99 % (3670096)CaDiCaL version: 2.1.3
% 27.25/6.99 % (3670096)Termination reason: Instruction limit
% 27.25/6.99 % (3670096)Termination phase: SInE selection
% 27.25/6.99 % (3670096)Time elapsed: 0.112 s
% 27.25/6.99 % (3670096)Peak memory usage: 136 MB
% 27.25/6.99 % (3670096)Instructions burned: 119 (million)
% 27.25/6.99 % (3670097)Instruction limit reached!
% 27.25/6.99 % (3670097)------------------------------
% 27.25/6.99 % (3670097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.25/6.99 % (3670097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.25/6.99 % (3670097)CaDiCaL version: 2.1.3
% 27.25/6.99 % (3670097)Termination reason: Instruction limit
% 27.25/6.99 % (3670097)Termination phase: Property scanning
% 27.25/6.99 % (3670097)Time elapsed: 0.119 s
% 27.25/6.99 % (3670097)Peak memory usage: 136 MB
% 27.25/6.99 % (3670097)Instructions burned: 139 (million)
% 27.25/6.99 % (3670098)Instruction limit reached!
% 27.25/6.99 % (3670098)------------------------------
% 27.25/6.99 % (3670098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.25/6.99 % (3670098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.25/6.99 % (3670098)CaDiCaL version: 2.1.3
% 27.25/6.99 % (3670098)Termination reason: Instruction limit
% 27.25/6.99 % (3670098)Termination phase: SInE selection
% 27.25/6.99 % (3670098)Time elapsed: 0.141 s
% 27.25/6.99 % (3670098)Peak memory usage: 136 MB
% 27.25/6.99 % (3670098)Instructions burned: 129 (million)
% 27.25/6.99 % (3670104)lrs+10_1_sil=8000:sp=occurrence:random_seed=259498690:i=285:sd=3:ss=axioms:sgt=8_2971 on theBenchmark for (2971ds/285Mi)
% 27.25/6.99 % (3670107)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1540108278:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2971 on theBenchmark for (2971ds/157Mi)
% 27.25/6.99 % (3670109)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=4082520429:s2a=on:i=248:s2at=1.23:gtg=position_2970 on theBenchmark for (2970ds/248Mi)
% 27.25/6.99 % (3670104)Instruction limit reached!
% 27.25/6.99 % (3670104)------------------------------
% 27.25/6.99 % (3670104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.07/8.65 % (3670104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.07/8.65 % (3670104)CaDiCaL version: 2.1.3
% 39.07/8.65 % (3670104)Termination reason: Instruction limit
% 39.07/8.65 % (3670104)Termination phase: Preprocessing 3
% 39.07/8.65 % (3670104)Time elapsed: 0.194 s
% 39.07/8.65 % (3670104)Peak memory usage: 140 MB
% 39.07/8.65 % (3670104)Instructions burned: 285 (million)
% 39.07/8.65 % (3670108)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4142915655:i=325:sd=1:ss=axioms:sgt=32_2970 on theBenchmark for (2970ds/325Mi)
% 39.07/8.65 % (3670107)Instruction limit reached!
% 39.07/8.65 % (3670107)------------------------------
% 39.07/8.65 % (3670107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.07/8.65 % (3670107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.07/8.65 % (3670107)CaDiCaL version: 2.1.3
% 39.07/8.65 % (3670107)Termination reason: Instruction limit
% 39.07/8.65 % (3670107)Termination phase: Property scanning
% 39.07/8.65 % (3670107)Time elapsed: 0.136 s
% 39.07/8.65 % (3670107)Peak memory usage: 136 MB
% 39.07/8.65 % (3670107)Instructions burned: 157 (million)
% 39.07/8.65 % (3670113)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=361898375:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2967 on theBenchmark for (2967ds/294Mi)
% 39.07/8.65 % (3670109)Instruction limit reached!
% 39.07/8.65 % (3670109)------------------------------
% 39.07/8.65 % (3670109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.07/8.65 % (3670109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.07/8.65 % (3670109)CaDiCaL version: 2.1.3
% 39.07/8.65 % (3670109)Termination reason: Instruction limit
% 39.07/8.65 % (3670109)Termination phase: Property scanning
% 39.07/8.65 % (3670109)Time elapsed: 0.196 s
% 39.07/8.65 % (3670109)Peak memory usage: 136 MB
% 39.07/8.65 % (3670109)Instructions burned: 248 (million)
% 39.07/8.65 % (3670115)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=266542354:i=2350_2967 on theBenchmark for (2967ds/2350Mi)
% 39.07/8.65 % (3670108)Instruction limit reached!
% 39.07/8.65 % (3670108)------------------------------
% 39.07/8.65 % (3670108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.07/8.65 % (3670108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.07/8.65 % (3670108)CaDiCaL version: 2.1.3
% 39.07/8.65 % (3670108)Termination reason: Instruction limit
% 39.07/8.65 % (3670108)Termination phase: Saturation
% 39.07/8.65 % (3670108)Time elapsed: 0.365 s
% 39.07/8.65 % (3670108)Peak memory usage: 142 MB
% 39.07/8.65 % (3670108)Instructions burned: 326 (million)
% 39.07/8.65 % (3670113)Instruction limit reached!
% 39.07/8.65 % (3670113)------------------------------
% 39.07/8.65 % (3670113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.07/8.65 % (3670113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.07/8.65 % (3670113)CaDiCaL version: 2.1.3
% 39.07/8.65 % (3670113)Termination reason: Instruction limit
% 39.07/8.65 % (3670113)Termination phase: SInE selection
% 39.07/8.65 % (3670113)Time elapsed: 0.218 s
% 39.07/8.65 % (3670113)Peak memory usage: 136 MB
% 39.07/8.65 % (3670113)Instructions burned: 294 (million)
% 39.07/8.65 % (3670117)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2751363493:cts=off:i=113:fsr=off:ss=included:sgt=4_2965 on theBenchmark for (2965ds/113Mi)
% 39.07/8.65 % (3670119)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1699128670:i=127:av=off:fsr=off:sup=off_2963 on theBenchmark for (2963ds/127Mi)
% 39.07/8.65 % (3670117)Instruction limit reached!
% 39.07/8.65 % (3670117)------------------------------
% 39.07/8.65 % (3670117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.07/8.65 % (3670117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.07/8.65 % (3670117)CaDiCaL version: 2.1.3
% 39.07/8.65 % (3670117)Termination reason: Instruction limit
% 39.07/8.65 % (3670117)Termination phase: SInE selection
% 39.07/8.65 % (3670117)Time elapsed: 0.128 s
% 39.07/8.65 % (3670117)Peak memory usage: 136 MB
% 39.07/8.65 % (3670117)Instructions burned: 113 (million)
% 39.07/8.65 % (3670119)Instruction limit reached!
% 39.07/8.65 % (3670119)------------------------------
% 39.07/8.65 % (3670119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.07/8.65 % (3670119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.07/8.65 % (3670119)CaDiCaL version: 2.1.3
% 96.96/16.76 % (3670119)Termination reason: Instruction limit
% 96.96/16.76 % (3670119)Termination phase: Preprocessing 1
% 96.96/16.76 % (3670119)Time elapsed: 0.088 s
% 96.96/16.76 % (3670119)Peak memory usage: 137 MB
% 96.96/16.76 % (3670119)Instructions burned: 127 (million)
% 96.96/16.76 % (3670120)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=884224391:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2963 on theBenchmark for (2963ds/114Mi)
% 96.96/16.76 % (3670120)Instruction limit reached!
% 96.96/16.76 % (3670120)------------------------------
% 96.96/16.76 % (3670120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.96/16.76 % (3670120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.96/16.76 % (3670120)CaDiCaL version: 2.1.3
% 96.96/16.76 % (3670120)Termination reason: Instruction limit
% 96.96/16.76 % (3670120)Termination phase: Property scanning
% 96.96/16.76 % (3670120)Time elapsed: 0.096 s
% 96.96/16.76 % (3670120)Peak memory usage: 136 MB
% 96.96/16.76 % (3670120)Instructions burned: 114 (million)
% 96.96/16.76 % (3670126)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=571879005:i=437:sd=1:aac=none:ss=included_2961 on theBenchmark for (2961ds/437Mi)
% 96.96/16.76 % (3670125)lrs+10_1_sil=8000:sp=occurrence:random_seed=2620237920:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2961 on theBenchmark for (2961ds/907Mi)
% 96.96/16.76 % (3670128)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=806742753:i=5202:ss=axioms:sgt=16_2959 on theBenchmark for (2959ds/5202Mi)
% 96.96/16.76 % (3670126)Instruction limit reached!
% 96.96/16.76 % (3670126)------------------------------
% 96.96/16.76 % (3670126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.96/16.76 % (3670126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.96/16.76 % (3670126)CaDiCaL version: 2.1.3
% 96.96/16.76 % (3670126)Termination reason: Instruction limit
% 96.96/16.76 % (3670126)Termination phase: Saturation
% 96.96/16.76 % (3670126)Time elapsed: 0.266 s
% 96.96/16.76 % (3670126)Peak memory usage: 143 MB
% 96.96/16.76 % (3670126)Instructions burned: 439 (million)
% 96.96/16.76 % (3670132)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1083917132:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2956 on theBenchmark for (2956ds/134Mi)
% 96.96/16.76 % (3670132)Instruction limit reached!
% 96.96/16.76 % (3670132)------------------------------
% 96.96/16.76 % (3670132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.96/16.76 % (3670132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.96/16.76 % (3670132)CaDiCaL version: 2.1.3
% 96.96/16.76 % (3670132)Termination reason: Instruction limit
% 96.96/16.76 % (3670132)Termination phase: SInE selection
% 96.96/16.76 % (3670132)Time elapsed: 0.132 s
% 96.96/16.76 % (3670132)Peak memory usage: 136 MB
% 96.96/16.76 % (3670132)Instructions burned: 134 (million)
% 96.96/16.76 % (3670125)Instruction limit reached!
% 96.96/16.76 % (3670125)------------------------------
% 96.96/16.76 % (3670125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.96/16.76 % (3670125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.96/16.76 % (3670125)CaDiCaL version: 2.1.3
% 96.96/16.76 % (3670125)Termination reason: Instruction limit
% 96.96/16.76 % (3670125)Termination phase: Property scanning
% 96.96/16.76 % (3670125)Time elapsed: 0.874 s
% 96.96/16.76 % (3670125)Peak memory usage: 151 MB
% 96.96/16.77 % (3670125)Instructions burned: 908 (million)
% 96.96/16.77 % (3670134)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3895817642:st=8:i=592:sd=3:ep=RST:ss=axioms_2951 on theBenchmark for (2951ds/592Mi)
% 96.96/16.77 % (3670135)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1638323934:st=3:i=13193:sd=3:ss=axioms_2950 on theBenchmark for (2950ds/13193Mi)
% 96.96/16.77 % (3670134)Instruction limit reached!
% 96.96/16.77 % (3670134)------------------------------
% 96.96/16.77 % (3670134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.96/16.77 % (3670134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.96/16.77 % (3670134)CaDiCaL version: 2.1.3
% 96.96/16.77 % (3670134)Termination reason: Instruction limit
% 96.96/16.77 % (3670134)Termination phase: Preprocessing 2
% 96.96/16.77 % (3670134)Time elapsed: 0.678 s
% 96.96/16.77 % (3670134)Peak memory usage: 147 MB
% 96.96/16.77 % (3670134)Instructions burned: 592 (million)
% 96.96/16.77 % (3670138)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=4066724274:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2941 on theBenchmark for (2941ds/125Mi)
% 149.21/24.11 % (3670115)Instruction limit reached!
% 149.21/24.11 % (3670115)------------------------------
% 149.21/24.11 % (3670115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.21/24.11 % (3670115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.21/24.11 % (3670115)CaDiCaL version: 2.1.3
% 149.21/24.11 % (3670115)Termination reason: Instruction limit
% 149.21/24.11 % (3670115)Termination phase: Property scanning
% 149.21/24.11 % (3670115)Time elapsed: 2.557 s
% 149.21/24.11 % (3670115)Peak memory usage: 232 MB
% 149.21/24.11 % (3670115)Instructions burned: 2351 (million)
% 149.21/24.11 % (3670138)Instruction limit reached!
% 149.21/24.11 % (3670138)------------------------------
% 149.21/24.11 % (3670138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.21/24.11 % (3670138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.21/24.11 % (3670138)CaDiCaL version: 2.1.3
% 149.21/24.11 % (3670138)Termination reason: Instruction limit
% 149.21/24.11 % (3670138)Termination phase: Property scanning
% 149.21/24.11 % (3670138)Time elapsed: 0.108 s
% 149.21/24.11 % (3670138)Peak memory usage: 136 MB
% 149.21/24.11 % (3670138)Instructions burned: 126 (million)
% 149.21/24.11 % (3670140)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1356748394:i=134:gtgl=5:slsql=off:gtg=exists_sym_2938 on theBenchmark for (2938ds/134Mi)
% 149.21/24.11 % (3670141)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3816129961:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2937 on theBenchmark for (2937ds/141Mi)
% 149.21/24.11 % (3670140)Instruction limit reached!
% 149.21/24.11 % (3670140)------------------------------
% 149.21/24.11 % (3670140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.21/24.11 % (3670140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.21/24.11 % (3670140)CaDiCaL version: 2.1.3
% 149.21/24.11 % (3670140)Termination reason: Instruction limit
% 149.21/24.11 % (3670140)Termination phase: Property scanning
% 149.21/24.11 % (3670140)Time elapsed: 0.117 s
% 149.21/24.11 % (3670140)Peak memory usage: 136 MB
% 149.21/24.11 % (3670140)Instructions burned: 134 (million)
% 149.21/24.11 % (3670141)Instruction limit reached!
% 149.21/24.11 % (3670141)------------------------------
% 149.21/24.11 % (3670141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.21/24.11 % (3670141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.21/24.11 % (3670141)CaDiCaL version: 2.1.3
% 149.21/24.11 % (3670141)Termination reason: Instruction limit
% 149.21/24.11 % (3670141)Termination phase: SInE selection
% 149.21/24.11 % (3670141)Time elapsed: 0.151 s
% 149.21/24.11 % (3670141)Peak memory usage: 136 MB
% 149.21/24.11 % (3670141)Instructions burned: 141 (million)
% 149.21/24.11 % (3670144)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2602660186:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2934 on theBenchmark for (2934ds/431Mi)
% 149.21/24.11 % (3670145)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=1829018912:i=6060:aac=none:ins=25_2933 on theBenchmark for (2933ds/6060Mi)
% 149.21/24.11 % (3670144)Instruction limit reached!
% 149.21/24.11 % (3670144)------------------------------
% 149.21/24.11 % (3670144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.21/24.11 % (3670144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.21/24.11 % (3670144)CaDiCaL version: 2.1.3
% 149.21/24.11 % (3670144)Termination reason: Instruction limit
% 149.21/24.11 % (3670144)Termination phase: Saturation
% 149.21/24.11 % (3670144)Time elapsed: 0.472 s
% 149.21/24.11 % (3670144)Peak memory usage: 143 MB
% 149.21/24.11 % (3670144)Instructions burned: 431 (million)
% 149.21/24.11 % (3670148)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=960441212:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2926 on theBenchmark for (2926ds/150Mi)
% 149.21/24.11 % (3670148)Instruction limit reached!
% 149.21/24.11 % (3670148)------------------------------
% 149.21/24.11 % (3670148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.21/24.11 % (3670148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.21/24.11 % (3670148)CaDiCaL version: 2.1.3
% 149.21/24.11 % (3670148)Termination reason: Instruction limit
% 198.78/31.08 % (3670148)Termination phase: SInE selection
% 198.78/31.08 % (3670148)Time elapsed: 0.174 s
% 198.78/31.08 % (3670148)Peak memory usage: 135 MB
% 198.78/31.08 % (3670148)Instructions burned: 151 (million)
% 198.78/31.08 % (3670150)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=4196408050:i=14155:bd=all_2922 on theBenchmark for (2922ds/14155Mi)
% 198.78/31.08 % (3670128)Instruction limit reached!
% 198.78/31.08 % (3670128)------------------------------
% 198.78/31.08 % (3670128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 198.78/31.08 % (3670128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.78/31.08 % (3670128)CaDiCaL version: 2.1.3
% 198.78/31.08 % (3670128)Termination reason: Instruction limit
% 198.78/31.08 % (3670128)Termination phase: Saturation
% 198.78/31.08 % (3670128)Time elapsed: 4.961 s
% 198.78/31.08 % (3670128)Peak memory usage: 259 MB
% 198.78/31.08 % (3670128)Instructions burned: 5203 (million)
% 198.78/31.08 % (3670152)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3471688886:i=667:av=off:fsr=off_2907 on theBenchmark for (2907ds/667Mi)
% 198.78/31.08 % (3670152)Instruction limit reached!
% 198.78/31.08 % (3670152)------------------------------
% 198.78/31.08 % (3670152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 198.78/31.08 % (3670152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.78/31.08 % (3670152)CaDiCaL version: 2.1.3
% 198.78/31.08 % (3670152)Termination reason: Instruction limit
% 198.78/31.08 % (3670152)Termination phase: NewCNF
% 198.78/31.08 % (3670152)Time elapsed: 0.824 s
% 198.78/31.08 % (3670152)Peak memory usage: 185 MB
% 198.78/31.08 % (3670152)Instructions burned: 667 (million)
% 198.78/31.08 % (3670154)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=1251042674:s2a=on:i=185:s2at=1.8:fdi=4_2895 on theBenchmark for (2895ds/185Mi)
% 198.78/31.08 % (3670154)Instruction limit reached!
% 198.78/31.08 % (3670154)------------------------------
% 198.78/31.08 % (3670154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 198.78/31.08 % (3670154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.78/31.08 % (3670154)CaDiCaL version: 2.1.3
% 198.78/31.08 % (3670154)Termination reason: Instruction limit
% 198.78/31.08 % (3670154)Termination phase: SInE selection
% 198.78/31.08 % (3670154)Time elapsed: 0.163 s
% 198.78/31.08 % (3670154)Peak memory usage: 136 MB
% 198.78/31.08 % (3670154)Instructions burned: 185 (million)
% 198.78/31.08 % (3670156)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3051277518:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2891 on theBenchmark for (2891ds/193Mi)
% 198.78/31.08 % (3670156)Instruction limit reached!
% 198.78/31.08 % (3670156)------------------------------
% 198.78/31.08 % (3670156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 198.78/31.08 % (3670156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.78/31.08 % (3670156)CaDiCaL version: 2.1.3
% 198.78/31.08 % (3670156)Termination reason: Instruction limit
% 198.78/31.08 % (3670156)Termination phase: SInE selection
% 198.78/31.08 % (3670156)Time elapsed: 0.211 s
% 198.78/31.08 % (3670156)Peak memory usage: 136 MB
% 198.78/31.08 % (3670156)Instructions burned: 193 (million)
% 198.78/31.08 % (3670158)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=210505399:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2887 on theBenchmark for (2887ds/4850Mi)
% 198.78/31.08 % (3670145)Instruction limit reached!
% 198.78/31.08 % (3670145)------------------------------
% 198.78/31.08 % (3670145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 198.78/31.08 % (3670145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.78/31.08 % (3670145)CaDiCaL version: 2.1.3
% 198.78/31.08 % (3670145)Termination reason: Instruction limit
% 198.78/31.08 % (3670145)Termination phase: Function definition elimination
% 198.78/31.08 % (3670145)Time elapsed: 5.925 s
% 198.78/31.08 % (3670145)Peak memory usage: 244 MB
% 198.78/31.08 % (3670145)Instructions burned: 6061 (million)
% 198.78/31.08 % (3670160)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=4262788312:i=12111:sd=1:ss=included_2871 on theBenchmark for (2871ds/12111Mi)
% 198.78/31.08 % (3670158)Instruction limit reached!
% 198.78/31.08 % (3670158)------------------------------
% 198.78/31.08 % (3670158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.03/33.09 % (3670158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.03/33.09 % (3670158)CaDiCaL version: 2.1.3
% 120.03/33.09 % (3670158)Termination reason: Instruction limit
% 120.03/33.09 % (3670158)Termination phase: Property scanning
% 120.03/33.09 % (3670158)Time elapsed: 4.350 s
% 120.03/33.09 % (3670158)Peak memory usage: 217 MB
% 120.03/33.09 % (3670158)Instructions burned: 4850 (million)
% 120.03/33.09 % (3670162)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4203568540:i=319:kws=precedence:fsr=off_2840 on theBenchmark for (2840ds/319Mi)
% 120.03/33.09 % (3670162)Instruction limit reached!
% 120.03/33.09 % (3670162)------------------------------
% 120.03/33.09 % (3670162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.03/33.09 % (3670162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.03/33.09 % (3670162)CaDiCaL version: 2.1.3
% 120.03/33.09 % (3670162)Termination reason: Instruction limit
% 120.03/33.09 % (3670162)Termination phase: Unused predicate definition removal
% 120.03/33.09 % (3670162)Time elapsed: 0.391 s
% 120.03/33.09 % (3670162)Peak memory usage: 142 MB
% 120.03/33.09 % (3670162)Instructions burned: 319 (million)
% 120.03/33.09 % (3670164)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=470094828:i=2064:ep=RST_2834 on theBenchmark for (2834ds/2064Mi)
% 120.03/33.09 % (3670135)Instruction limit reached!
% 120.03/33.09 % (3670135)------------------------------
% 120.03/33.09 % (3670135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.03/33.09 % (3670135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.03/33.09 % (3670135)CaDiCaL version: 2.1.3
% 120.03/33.09 % (3670135)Termination reason: Instruction limit
% 120.03/33.09 % (3670135)Termination phase: Saturation
% 120.03/33.09 % (3670135)Time elapsed: 13.189 s
% 120.03/33.09 % (3670135)Peak memory usage: 344 MB
% 120.03/33.09 % (3670135)Instructions burned: 13194 (million)
% 120.03/33.09 % (3670168)dis-1011_128_sil=32000:random_seed=104568195:i=3706:ep=RST:av=off_2814 on theBenchmark for (2814ds/3706Mi)
% 120.03/33.09 % (3670164)Instruction limit reached!
% 120.03/33.09 % (3670164)------------------------------
% 120.03/33.09 % (3670164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.03/33.09 % (3670164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.03/33.09 % (3670164)CaDiCaL version: 2.1.3
% 120.03/33.09 % (3670164)Termination reason: Instruction limit
% 120.03/33.09 % (3670164)Termination phase: Property scanning
% 120.03/33.09 % (3670164)Time elapsed: 2.233 s
% 120.03/33.09 % (3670164)Peak memory usage: 231 MB
% 120.03/33.09 % (3670164)Instructions burned: 2064 (million)
% 120.03/33.09 % (3670172)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=789602978:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2809 on theBenchmark for (2809ds/757Mi)
% 120.03/33.09 % (3670172)Instruction limit reached!
% 120.03/33.09 % (3670172)------------------------------
% 120.03/33.09 % (3670172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.03/33.09 % (3670172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.03/33.09 % (3670172)CaDiCaL version: 2.1.3
% 120.03/33.09 % (3670172)Termination reason: Instruction limit
% 120.03/33.09 % (3670172)Termination phase: Saturation
% 120.03/33.09 % (3670172)Time elapsed: 0.804 s
% 120.03/33.09 % (3670172)Peak memory usage: 149 MB
% 120.03/33.09 % (3670172)Instructions burned: 757 (million)
% 120.03/33.09 % (3670174)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1148191395:i=13913:ss=axioms:sgt=8_2798 on theBenchmark for (2798ds/13913Mi)
% 120.03/33.09 % (3670168)Instruction limit reached!
% 120.03/33.09 % (3670168)------------------------------
% 120.03/33.09 % (3670168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.03/33.09 % (3670168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.03/33.09 % (3670168)CaDiCaL version: 2.1.3
% 120.03/33.09 % (3670168)Termination reason: Instruction limit
% 120.03/33.09 % (3670168)Termination phase: Function definition elimination
% 120.03/33.09 % (3670168)Time elapsed: 3.547 s
% 120.03/33.09 % (3670168)Peak memory usage: 241 MB
% 120.03/33.09 % (3670168)Instructions burned: 3707 (million)
% 120.03/33.09 % (3670176)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2322171786:i=9925:aac=none_2775 on theBenchmark for (2775ds/9925Mi)
% 120.03/33.09 % (3670150)Instruction limit reached!
% 120.03/33.09 % (3670150)------------------------------
% 120.03/33.09 % (3670150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.03/33.09 % (3670150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.03/33.09 % (3670150)CaDiCaL version: 2.1.3
% 120.03/33.09 % (3670150)Termination reason: Instruction limit
% 120.03/33.09 % (3670150)Termination phase: Saturation
% 120.03/33.09 % (3670150)Time elapsed: 15.244 s
% 120.03/33.09 % (3670150)Peak memory usage: 1298 MB
% 120.03/33.09 % (3670150)Instructions burned: 14157 (million)
% 120.03/33.09 % (3670178)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2861543257:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2765 on theBenchmark for (2765ds/2479Mi)
% 120.03/33.09 % (3670178)Instruction limit reached!
% 120.03/33.09 % (3670178)------------------------------
% 120.03/33.09 % (3670178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.03/33.09 % (3670178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.03/33.09 % (3670178)CaDiCaL version: 2.1.3
% 120.03/33.09 % (3670178)Termination reason: Instruction limit
% 120.03/33.09 % (3670178)Termination phase: Saturation
% 120.03/33.09 % (3670178)Time elapsed: 2.264 s
% 120.03/33.09 % (3670178)Peak memory usage: 154 MB
% 120.03/33.09 % (3670178)Instructions burned: 2479 (million)
% 120.03/33.09 % (3670180)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=4112669160:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2739 on theBenchmark for (2739ds/440Mi)
% 120.03/33.09 % (3670180)Instruction limit reached!
% 120.03/33.09 % (3670180)------------------------------
% 120.03/33.09 % (3670180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.03/33.09 % (3670180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.03/33.09 % (3670180)CaDiCaL version: 2.1.3
% 120.03/33.09 % (3670180)Termination reason: Instruction limit
% 120.03/33.09 % (3670180)Termination phase: Property scanning
% 120.03/33.09 % (3670180)Time elapsed: 0.286 s
% 120.03/33.09 % (3670180)Peak memory usage: 136 MB
% 120.03/33.09 % (3670180)Instructions burned: 441 (million)
% 120.03/33.09 % (3670182)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=399473467:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2734 on theBenchmark for (2734ds/11145Mi)
% 120.03/33.09 % (3670160)Instruction limit reached!
% 120.03/33.09 % (3670160)------------------------------
% 120.03/33.09 % (3670160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.03/33.09 % (3670160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.03/33.09 % (3670160)CaDiCaL version: 2.1.3
% 120.03/33.09 % (3670160)Termination reason: Instruction limit
% 120.03/33.09 % (3670160)Termination phase: Saturation
% 120.03/33.09 % (3670160)Time elapsed: 14.173 s
% 120.03/33.09 % (3670160)Peak memory usage: 258 MB
% 120.03/33.09 % (3670160)Instructions burned: 12111 (million)
% 120.03/33.09 % (3670184)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=2943825468:cts=off:i=3034:av=off:er=known:fsd=on_2726 on theBenchmark for (2726ds/3034Mi)
% 120.03/33.09 % (3670184)Instruction limit reached!
% 120.03/33.09 % (3670184)------------------------------
% 120.03/33.09 % (3670184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.03/33.09 % (3670184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.03/33.09 % (3670184)CaDiCaL version: 2.1.3
% 120.03/33.09 % (3670184)Termination reason: Instruction limit
% 120.03/33.09 % (3670184)Termination phase: Property scanning
% 120.03/33.09 % (3670184)Time elapsed: 1.881 s
% 120.03/33.09 % (3670184)Peak memory usage: 232 MB
% 120.03/33.09 % (3670184)Instructions burned: 3037 (million)
% 120.03/33.09 % (3670339)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=4061122666:st=2:s2a=on:i=524:s2at=2:ss=axioms_2705 on theBenchmark for (2705ds/524Mi)
% 120.03/33.09 % (3670339)Instruction limit reached!
% 120.03/33.09 % (3670339)------------------------------
% 120.03/33.09 % (3670339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.03/33.09 % (3670339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.03/33.09 % (3670339)CaDiCaL version: 2.1.3
% 120.03/33.09 % (3670339)Termination reason: Instruction limit
% 120.03/33.09 % (3670339)Termination phase: SInE selection
% 120.03/33.09 % (3670339)Time elapsed: 0.385 s
% 120.03/33.09 % (3670339)Peak memory usage: 137 MB
% 120.03/33.09 % (3670339)Instructions burned: 525 (million)
% 120.03/33.09 % (3670341)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2598110446:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2699 on theBenchmark for (2699ds/1016Mi)
% 120.03/33.09 % (3670176)Instruction limit reached!
% 120.03/33.09 % (3670176)------------------------------
% 120.03/33.09 % (3670176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.03/33.09 % (3670176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.03/33.09 % (3670176)CaDiCaL version: 2.1.3
% 120.03/33.09 % (3670176)Termination reason: Instruction limit
% 120.03/33.09 % (3670176)Termination phase: Saturation
% 120.03/33.09 % (3670176)Time elapsed: 7.755 s
% 120.03/33.09 % (3670176)Peak memory usage: 659 MB
% 120.03/33.09 % (3670176)Instructions burned: 9928 (million)
% 120.03/33.09 % (3670343)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=8870721:i=14123:bd=preordered:ins=4_2695 on theBenchmark for (2695ds/14123Mi)
% 120.03/33.09 % (3670341)Instruction limit reached!
% 120.03/33.09 % (3670341)------------------------------
% 120.03/33.09 % (3670341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.03/33.09 % (3670341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.03/33.09 % (3670341)CaDiCaL version: 2.1.3
% 120.03/33.09 % (3670341)Termination reason: Instruction limit
% 120.03/33.09 % (3670341)Termination phase: Saturation
% 120.03/33.09 % (3670341)Time elapsed: 0.657 s
% 120.03/33.09 % (3670341)Peak memory usage: 148 MB
% 120.03/33.09 % (3670341)Instructions burned: 1017 (million)
% 120.03/33.09 % (3670345)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2420528886:i=5781:kws=precedence:bd=all:rawr=on_2691 on theBenchmark for (2691ds/5781Mi)
% 120.03/33.09 % (3670182)First to succeed.
% 120.03/33.09 % (3670182)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3670085"
% 120.03/33.09 % (3670174)Instruction limit reached!
% 120.03/33.09 % (3670174)------------------------------
% 120.03/33.09 % (3670174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.03/33.09 % (3670174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.03/33.09 % (3670174)CaDiCaL version: 2.1.3
% 120.03/33.09 % (3670174)Termination reason: Instruction limit
% 120.03/33.09 % (3670174)Termination phase: Saturation
% 120.03/33.09 % (3670174)Time elapsed: 11.602 s
% 120.03/33.09 % (3670174)Peak memory usage: 302 MB
% 120.03/33.09 % (3670174)Instructions burned: 13914 (million)
% 120.03/33.09 % (3670182)Refutation found. Thanks to Tanya!
% 120.03/33.09 % SZS status Theorem for theBenchmark
% 120.03/33.09 % SZS output start Proof for theBenchmark
% See solution above
% 213.34/33.34 % (3670182)------------------------------
% 213.34/33.34 % (3670182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 213.34/33.34 % (3670182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 213.34/33.34 % (3670182)CaDiCaL version: 2.1.3
% 213.34/33.34 % (3670182)Termination reason: Refutation
% 213.34/33.34 % (3670182)Time elapsed: 4.962 s
% 213.34/33.34 % (3670182)Peak memory usage: 258 MB
% 213.34/33.34 % (3670182)Instructions burned: 7073 (million)
% 213.34/33.34 % (3670182)------------------------------
% 213.34/33.34 % (3670182)------------------------------
% 213.34/33.34 % (3670085)Success in time 32.193 s
% 213.34/33.34 % Vampire exiting
%------------------------------------------------------------------------------