%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : TOP036+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 : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 02:34:00 PM UTC 2026
% Result : Theorem 105.62s 22.88s
% Output : Refutation 153.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 93
% Syntax : Number of formulae : 534 ( 86 unt; 58 def)
% Number of atoms : 2362 ( 205 equ)
% Maximal formula atoms : 16 ( 4 avg)
% Number of connectives : 3225 (1397 ~;1565 |; 135 &)
% ( 67 <=>; 61 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 72 ( 70 usr; 53 prp; 0-3 aty)
% Number of functors : 31 ( 31 usr; 9 con; 0-4 aty)
% Number of variables : 494 ( 0 sgn 486 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f38,axiom,
! [X0,X1] :
( X0 = X1
<=> ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(f258,axiom,
! [X0] : k2_tarski(X0,X0) = k1_tarski(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f675,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_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(f865,axiom,
! [X0,X1,X2] :
( v1_relat_1(X2)
=> ( r1_tarski(X0,X1)
=> r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t156_relat_1) ).
fof(f1055,axiom,
! [X0,X1] :
( ( v1_relat_1(X1)
& v1_funct_1(X1) )
=> ( r2_hidden(X0,k1_relat_1(X1))
=> k9_relat_1(X1,k1_tarski(X0)) = k1_tarski(k1_funct_1(X1,X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t117_funct_1) ).
fof(f1084,axiom,
! [X0,X1] :
( ( v1_relat_1(X1)
& v1_funct_1(X1) )
=> r1_tarski(k9_relat_1(X1,k10_relat_1(X1,X0)),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t145_funct_1) ).
fof(f1196,axiom,
! [X0,X1,X2] :
( ( v1_relat_1(X2)
& v1_funct_1(X2) )
=> ( r2_hidden(X0,k10_relat_1(X2,X1))
<=> ( r2_hidden(k4_tarski(X0,k1_funct_1(X2,X0)),X2)
& r2_hidden(k1_funct_1(X2,X0),X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t87_grfunc_1) ).
fof(f1422,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> v1_relat_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f1481,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_relset_1) ).
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(f1569,axiom,
! [X0,X1,X2] :
( ( v1_funct_1(X2)
& m2_relset_1(X2,X0,X1) )
=> k10_relat_1(X2,X1) = k4_relset_1(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t53_partfun1) ).
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(f18264,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> r2_hidden(X1,k2_pre_topc(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_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(f18325,axiom,
! [X0,X1,X2,X3] :
( ( l1_struct_0(X0)
& l1_struct_0(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k4_pre_topc) ).
fof(f18327,axiom,
! [X0,X1,X2,X3] :
( ( l1_struct_0(X0)
& l1_struct_0(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> k5_pre_topc(X0,X1,X2,X3) = k10_relat_1(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k5_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(f34200,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> r1_tarski(k1_struct_0(X0,X1),k2_tex_4(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t20_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(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(f34366,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_tsp_1) ).
fof(f34372,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0)
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m1_pre_topc(X1,X0) )
=> ( v1_funct_1(k3_tsp_2(X0,X1))
& v1_funct_2(k3_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k3_tsp_2(X0,X1),X0,X1)
& m2_relset_1(k3_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_tsp_2) ).
fof(f34373,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0)
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m1_pre_topc(X1,X0) )
=> k3_tsp_2(X0,X1) = k1_tsp_2(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k3_tsp_2) ).
fof(f34422,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v3_borsuk_1(X2,X0,X1)
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X1))
=> ( X3 = X4
=> k5_pre_topc(X0,X1,X2,k1_struct_0(X1,X4)) = k4_tex_4(X0,X3) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l36_tsp_2) ).
fof(f34424,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( X2 = k1_tsp_2(X0,X1)
<=> v3_borsuk_1(X2,X0,X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d9_tsp_2) ).
fof(f34426,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] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ( X2 = X3
=> k5_pre_topc(X0,X1,k1_tsp_2(X0,X1),k1_struct_0(X1,X3)) = k4_tex_4(X0,X2) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t25_tsp_2) ).
fof(f34429,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( X2 = k3_tsp_2(X0,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)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d11_tsp_2) ).
fof(f34430,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] :
( m1_subset_1(X2,u1_struct_0(X0))
=> k5_pre_topc(X0,X1,k3_tsp_2(X0,X1),k1_struct_0(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),k3_tsp_2(X0,X1),X2))) = k4_tex_4(X0,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t27_tsp_2) ).
fof(f34431,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> k4_pre_topc(X0,X1,k3_tsp_2(X0,X1),k1_struct_0(X0,X2)) = k4_pre_topc(X0,X1,k3_tsp_2(X0,X1),k4_tex_4(X0,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t28_tsp_2) ).
fof(f34432,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> k4_pre_topc(X0,X1,k3_tsp_2(X0,X1),k1_struct_0(X0,X2)) = k4_pre_topc(X0,X1,k3_tsp_2(X0,X1),k4_tex_4(X0,X2)) ) ) ),
inference(negated_conjecture,[status(cth)],[f34431]) ).
fof(f34578,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( k4_pre_topc(X0,X1,k3_tsp_2(X0,X1),k1_struct_0(X0,X2)) != k4_pre_topc(X0,X1,k3_tsp_2(X0,X1),k4_tex_4(X0,X2))
& m1_subset_1(X2,u1_struct_0(X0)) )
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34432]) ).
fof(f34579,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( k4_pre_topc(X0,X1,k3_tsp_2(X0,X1),k1_struct_0(X0,X2)) != k4_pre_topc(X0,X1,k3_tsp_2(X0,X1),k4_tex_4(X0,X2))
& m1_subset_1(X2,u1_struct_0(X0)) )
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(flattening,[],[f34578]) ).
fof(f34594,plain,
! [X0] :
( ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34366]) ).
fof(f34596,plain,
! [X0] :
( ! [X1] :
( l1_pre_topc(X1)
| ~ m2_tsp_1(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34364]) ).
fof(f34647,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(f34648,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,[],[f34647]) ).
fof(f34677,plain,
! [X0,X1,X2,X3] :
( k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f18325]) ).
fof(f34678,plain,
! [X0,X1,X2,X3] :
( k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f34677]) ).
fof(f34681,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( k5_pre_topc(X0,X1,X2,k1_struct_0(X1,X4)) = k4_tex_4(X0,X3)
| X3 != X4
| ~ m1_subset_1(X4,u1_struct_0(X1)) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ v3_borsuk_1(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34422]) ).
fof(f34682,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( k5_pre_topc(X0,X1,X2,k1_struct_0(X1,X4)) = k4_tex_4(X0,X3)
| X3 != X4
| ~ m1_subset_1(X4,u1_struct_0(X1)) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ v3_borsuk_1(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f34681]) ).
fof(f34701,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(f34702,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,[],[f34701]) ).
fof(f34703,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(f34704,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,[],[f34703]) ).
fof(f34709,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k5_pre_topc(X0,X1,k3_tsp_2(X0,X1),k1_struct_0(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),k3_tsp_2(X0,X1),X2))) = k4_tex_4(X0,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34430]) ).
fof(f34710,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k5_pre_topc(X0,X1,k3_tsp_2(X0,X1),k1_struct_0(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),k3_tsp_2(X0,X1),X2))) = k4_tex_4(X0,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f34709]) ).
fof(f34711,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k3_tsp_2(X0,X1)
<=> ! [X3] :
( r2_hidden(k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X3),k4_tex_4(X0,X3))
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34429]) ).
fof(f34712,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k3_tsp_2(X0,X1)
<=> ! [X3] :
( r2_hidden(k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X3),k4_tex_4(X0,X3))
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f34711]) ).
fof(f34713,plain,
! [X0,X1] :
( k3_tsp_2(X0,X1) = k1_tsp_2(X0,X1)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(ennf_transformation,[],[f34373]) ).
fof(f34714,plain,
! [X0,X1] :
( k3_tsp_2(X0,X1) = k1_tsp_2(X0,X1)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(flattening,[],[f34713]) ).
fof(f34715,plain,
! [X0,X1] :
( ( v1_funct_1(k3_tsp_2(X0,X1))
& v1_funct_2(k3_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k3_tsp_2(X0,X1),X0,X1)
& m2_relset_1(k3_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(ennf_transformation,[],[f34372]) ).
fof(f34716,plain,
! [X0,X1] :
( ( v1_funct_1(k3_tsp_2(X0,X1))
& v1_funct_2(k3_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k3_tsp_2(X0,X1),X0,X1)
& m2_relset_1(k3_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(flattening,[],[f34715]) ).
fof(f34779,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(f34780,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(flattening,[],[f34779]) ).
fof(f35276,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f675]) ).
fof(f35601,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f18318]) ).
fof(f35602,plain,
! [X0] :
( ( v3_struct_0(X0)
<=> v1_xboole_0(u1_struct_0(X0)) )
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f17598]) ).
fof(f35711,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(f35712,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,[],[f35711]) ).
fof(f36021,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(f36022,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,[],[f36021]) ).
fof(f36053,plain,
! [X0] :
( ! [X1] :
( r2_hidden(X1,k2_pre_topc(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f18264]) ).
fof(f36054,plain,
! [X0] :
( ! [X1] :
( r2_hidden(X1,k2_pre_topc(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f36053]) ).
fof(f36055,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f18263]) ).
fof(f36290,plain,
! [X0,X1] :
( r1_tarski(k9_relat_1(X1,k10_relat_1(X1,X0)),X0)
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(ennf_transformation,[],[f1084]) ).
fof(f36291,plain,
! [X0,X1] :
( r1_tarski(k9_relat_1(X1,k10_relat_1(X1,X0)),X0)
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(flattening,[],[f36290]) ).
fof(f36304,plain,
! [X0,X1] :
( k9_relat_1(X1,k1_tarski(X0)) = k1_tarski(k1_funct_1(X1,X0))
| ~ r2_hidden(X0,k1_relat_1(X1))
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(ennf_transformation,[],[f1055]) ).
fof(f36305,plain,
! [X0,X1] :
( k9_relat_1(X1,k1_tarski(X0)) = k1_tarski(k1_funct_1(X1,X0))
| ~ r2_hidden(X0,k1_relat_1(X1))
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(flattening,[],[f36304]) ).
fof(f36316,plain,
! [X0,X1,X2] :
( r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1))
| ~ r1_tarski(X0,X1)
| ~ v1_relat_1(X2) ),
inference(ennf_transformation,[],[f865]) ).
fof(f36317,plain,
! [X0,X1,X2] :
( r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1))
| ~ r1_tarski(X0,X1)
| ~ v1_relat_1(X2) ),
inference(flattening,[],[f36316]) ).
fof(f36334,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(f36364,plain,
! [X0,X1,X2,X3] :
( k5_pre_topc(X0,X1,X2,X3) = k10_relat_1(X2,X3)
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f18327]) ).
fof(f36365,plain,
! [X0,X1,X2,X3] :
( k5_pre_topc(X0,X1,X2,X3) = k10_relat_1(X2,X3)
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f36364]) ).
fof(f36482,plain,
! [X0] :
( ! [X1] :
( r1_tarski(k1_struct_0(X0,X1),k2_tex_4(X0,X1))
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34200]) ).
fof(f36483,plain,
! [X0] :
( ! [X1] :
( r1_tarski(k1_struct_0(X0,X1),k2_tex_4(X0,X1))
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f36482]) ).
fof(f36490,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k5_pre_topc(X0,X1,k1_tsp_2(X0,X1),k1_struct_0(X1,X3)) = k4_tex_4(X0,X2)
| X2 != X3
| ~ m1_subset_1(X3,u1_struct_0(X1)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34426]) ).
fof(f36491,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k5_pre_topc(X0,X1,k1_tsp_2(X0,X1),k1_struct_0(X1,X3)) = k4_tex_4(X0,X2)
| X2 != X3
| ~ m1_subset_1(X3,u1_struct_0(X1)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f36490]) ).
fof(f36494,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k1_tsp_2(X0,X1)
<=> v3_borsuk_1(X2,X0,X1) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34424]) ).
fof(f36495,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k1_tsp_2(X0,X1)
<=> v3_borsuk_1(X2,X0,X1) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f36494]) ).
fof(f36516,plain,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1481]) ).
fof(f36517,plain,
! [X0,X1,X2] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f1422]) ).
fof(f39421,plain,
! [X0,X1,X2] :
( k10_relat_1(X2,X1) = k4_relset_1(X0,X1,X2)
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1569]) ).
fof(f39422,plain,
! [X0,X1,X2] :
( k10_relat_1(X2,X1) = k4_relset_1(X0,X1,X2)
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X2,X0,X1) ),
inference(flattening,[],[f39421]) ).
fof(f39423,plain,
! [X0,X1,X2] :
( ( r2_hidden(X0,k10_relat_1(X2,X1))
<=> ( r2_hidden(k4_tarski(X0,k1_funct_1(X2,X0)),X2)
& r2_hidden(k1_funct_1(X2,X0),X1) ) )
| ~ v1_relat_1(X2)
| ~ v1_funct_1(X2) ),
inference(ennf_transformation,[],[f1196]) ).
fof(f39424,plain,
! [X0,X1,X2] :
( ( r2_hidden(X0,k10_relat_1(X2,X1))
<=> ( r2_hidden(k4_tarski(X0,k1_funct_1(X2,X0)),X2)
& r2_hidden(k1_funct_1(X2,X0),X1) ) )
| ~ v1_relat_1(X2)
| ~ v1_funct_1(X2) ),
inference(flattening,[],[f39423]) ).
fof(f40009,plain,
( k4_pre_topc(sK174,sK175,k3_tsp_2(sK174,sK175),k1_struct_0(sK174,sK176)) != k4_pre_topc(sK174,sK175,k3_tsp_2(sK174,sK175),k4_tex_4(sK174,sK176))
& m1_subset_1(sK176,u1_struct_0(sK174))
& ~ v3_struct_0(sK175)
& v2_tsp_2(sK175,sK174)
& m2_tsp_1(sK175,sK174)
& ~ v3_struct_0(sK174)
& v2_pre_topc(sK174)
& l1_pre_topc(sK174) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK174,sK175,sK176]),skolemize(X0,sK174),skolemize(X1,sK175),skolemize(X2,sK176)],[f34579]) ).
fof(f40029,plain,
! [X0] :
( ! [X1] :
( ( m2_tsp_1(X1,X0)
| ~ m1_pre_topc(X1,X0) )
& ( m1_pre_topc(X1,X0)
| ~ m2_tsp_1(X1,X0) ) )
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f34594]) ).
fof(f40110,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k3_tsp_2(X0,X1)
| ? [X3] :
( ~ r2_hidden(k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X3),k4_tex_4(X0,X3))
& m1_subset_1(X3,u1_struct_0(X0)) ) )
& ( ! [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)) )
| k3_tsp_2(X0,X1) != X2 ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f34712]) ).
fof(f40111,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k3_tsp_2(X0,X1)
| ? [X3] :
( ~ r2_hidden(k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X3),k4_tex_4(X0,X3))
& m1_subset_1(X3,u1_struct_0(X0)) ) )
& ( ! [X4] :
( r2_hidden(k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X4),k4_tex_4(X0,X4))
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| k3_tsp_2(X0,X1) != X2 ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(rectify,[],[f40110]) ).
fof(f40112,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k3_tsp_2(X0,X1)
| ( ~ r2_hidden(k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,sK226(X0,X1,X2)),k4_tex_4(X0,sK226(X0,X1,X2)))
& m1_subset_1(sK226(X0,X1,X2),u1_struct_0(X0)) ) )
& ( ! [X4] :
( r2_hidden(k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X4),k4_tex_4(X0,X4))
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| k3_tsp_2(X0,X1) != X2 ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK226]),skolemize(X3,sK226(X0,X1,X2))],[f40111]) ).
fof(f40332,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(nnf_transformation,[],[f38]) ).
fof(f40333,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(flattening,[],[f40332]) ).
fof(f40430,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,[],[f35602]) ).
fof(f40780,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(f40849,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k1_tsp_2(X0,X1)
| ~ v3_borsuk_1(X2,X0,X1) )
& ( v3_borsuk_1(X2,X0,X1)
| k1_tsp_2(X0,X1) != X2 ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f36495]) ).
fof(f41934,plain,
! [X0,X1,X2] :
( ( ( r2_hidden(X0,k10_relat_1(X2,X1))
| ~ r2_hidden(k4_tarski(X0,k1_funct_1(X2,X0)),X2)
| ~ r2_hidden(k1_funct_1(X2,X0),X1) )
& ( ( r2_hidden(k4_tarski(X0,k1_funct_1(X2,X0)),X2)
& r2_hidden(k1_funct_1(X2,X0),X1) )
| ~ r2_hidden(X0,k10_relat_1(X2,X1)) ) )
| ~ v1_relat_1(X2)
| ~ v1_funct_1(X2) ),
inference(nnf_transformation,[],[f39424]) ).
fof(f41935,plain,
! [X0,X1,X2] :
( ( ( r2_hidden(X0,k10_relat_1(X2,X1))
| ~ r2_hidden(k4_tarski(X0,k1_funct_1(X2,X0)),X2)
| ~ r2_hidden(k1_funct_1(X2,X0),X1) )
& ( ( r2_hidden(k4_tarski(X0,k1_funct_1(X2,X0)),X2)
& r2_hidden(k1_funct_1(X2,X0),X1) )
| ~ r2_hidden(X0,k10_relat_1(X2,X1)) ) )
| ~ v1_relat_1(X2)
| ~ v1_funct_1(X2) ),
inference(flattening,[],[f41934]) ).
fof(f42078,plain,
l1_pre_topc(sK174),
inference(cnf_transformation,[],[f40009]) ).
fof(f42079,plain,
v2_pre_topc(sK174),
inference(cnf_transformation,[],[f40009]) ).
fof(f42080,plain,
~ v3_struct_0(sK174),
inference(cnf_transformation,[],[f40009]) ).
fof(f42081,plain,
m2_tsp_1(sK175,sK174),
inference(cnf_transformation,[],[f40009]) ).
fof(f42082,plain,
v2_tsp_2(sK175,sK174),
inference(cnf_transformation,[],[f40009]) ).
fof(f42083,plain,
~ v3_struct_0(sK175),
inference(cnf_transformation,[],[f40009]) ).
fof(f42084,plain,
m1_subset_1(sK176,u1_struct_0(sK174)),
inference(cnf_transformation,[],[f40009]) ).
fof(f42085,plain,
k4_pre_topc(sK174,sK175,k3_tsp_2(sK174,sK175),k1_struct_0(sK174,sK176)) != k4_pre_topc(sK174,sK175,k3_tsp_2(sK174,sK175),k4_tex_4(sK174,sK176)),
inference(cnf_transformation,[],[f40009]) ).
fof(f42116,plain,
! [X0,X1] :
( m1_pre_topc(X1,X0)
| ~ m2_tsp_1(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f40029]) ).
fof(f42119,plain,
! [X0,X1] :
( ~ m2_tsp_1(X1,X0)
| l1_pre_topc(X1)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f34596]) ).
fof(f42224,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,[],[f34648]) ).
fof(f42269,plain,
! [X2,X3,X0,X1] :
( k9_relat_1(X2,X3) = k4_pre_topc(X0,X1,X2,X3)
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f34678]) ).
fof(f42271,plain,
! [X2,X3,X0,X1,X4] :
( X3 != X4
| k4_tex_4(X0,X3) = k5_pre_topc(X0,X1,X2,k1_struct_0(X1,X4))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ v3_borsuk_1(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f34682]) ).
fof(f42310,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,[],[f34702]) ).
fof(f42311,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,[],[f34704]) ).
fof(f42335,plain,
! [X2,X0,X1] :
( k4_tex_4(X0,X2) = k5_pre_topc(X0,X1,k3_tsp_2(X0,X1),k1_struct_0(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),k3_tsp_2(X0,X1),X2)))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f34710]) ).
fof(f42336,plain,
! [X2,X0,X1,X4] :
( k3_tsp_2(X0,X1) != X2
| ~ m1_subset_1(X4,u1_struct_0(X0))
| r2_hidden(k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X4),k4_tex_4(X0,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))
| 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,[],[f40112]) ).
fof(f42339,plain,
! [X0,X1] :
( k1_tsp_2(X0,X1) = k3_tsp_2(X0,X1)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f34714]) ).
fof(f42340,plain,
! [X0,X1] :
( m2_relset_1(k3_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f34716]) ).
fof(f42341,plain,
! [X0,X1] :
( v5_pre_topc(k3_tsp_2(X0,X1),X0,X1)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f34716]) ).
fof(f42342,plain,
! [X0,X1] :
( v1_funct_2(k3_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f34716]) ).
fof(f42343,plain,
! [X0,X1] :
( v1_funct_1(k3_tsp_2(X0,X1))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f34716]) ).
fof(f42453,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(cnf_transformation,[],[f34780]) ).
fof(f43271,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f35276]) ).
fof(f43334,plain,
! [X0,X1] :
( ~ r1_tarski(X1,X0)
| ~ r1_tarski(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f40333]) ).
fof(f43770,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f35601]) ).
fof(f43773,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f40430]) ).
fof(f43920,plain,
! [X2,X3,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| k1_funct_1(X2,X3) = k8_funct_2(X0,X1,X2,X3)
| ~ m1_subset_1(X3,X0) ),
inference(cnf_transformation,[],[f35712]) ).
fof(f44500,plain,
! [X2,X0,X1] :
( v3_struct_0(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))
| k1_relat_1(X2) = k2_pre_topc(X0)
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f36022]) ).
fof(f44533,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| r2_hidden(X1,k2_pre_topc(X0))
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f36054]) ).
fof(f44534,plain,
! [X0] :
( u1_struct_0(X0) = k2_pre_topc(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f36055]) ).
fof(f44958,plain,
! [X0,X1] :
( ~ v1_relat_1(X1)
| r1_tarski(k9_relat_1(X1,k10_relat_1(X1,X0)),X0)
| ~ v1_funct_1(X1) ),
inference(cnf_transformation,[],[f36291]) ).
fof(f44965,plain,
! [X0,X1] :
( k1_tarski(k1_funct_1(X1,X0)) = k9_relat_1(X1,k1_tarski(X0))
| ~ r2_hidden(X0,k1_relat_1(X1))
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(cnf_transformation,[],[f36305]) ).
fof(f44980,plain,
! [X2,X0,X1] :
( r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1))
| ~ r1_tarski(X0,X1)
| ~ v1_relat_1(X2) ),
inference(cnf_transformation,[],[f36317]) ).
fof(f45023,plain,
! [X2,X0,X1] :
( k1_relat_1(X2) = k4_relset_1(X0,X1,X2)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f36334]) ).
fof(f45025,plain,
! [X2,X0,X1] :
( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f40780]) ).
fof(f45068,plain,
! [X2,X3,X0,X1] :
( ~ l1_struct_0(X0)
| k10_relat_1(X2,X3) = k5_pre_topc(X0,X1,X2,X3)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f36365]) ).
fof(f45232,plain,
! [X0,X1] :
( r1_tarski(k1_struct_0(X0,X1),k2_tex_4(X0,X1))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f36483]) ).
fof(f45239,plain,
! [X2,X3,X0,X1] :
( X2 != X3
| k4_tex_4(X0,X2) = k5_pre_topc(X0,X1,k1_tsp_2(X0,X1),k1_struct_0(X1,X3))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f36491]) ).
fof(f45241,plain,
! [X2,X0,X1] :
( ~ v2_tsp_2(X1,X0)
| k1_tsp_2(X0,X1) != X2
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| v3_borsuk_1(X2,X0,X1)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f40849]) ).
fof(f45265,plain,
! [X2,X0,X1] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f36516]) ).
fof(f45266,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(cnf_transformation,[],[f36517]) ).
fof(f47062,plain,
! [X0] : k1_tarski(X0) = k2_tarski(X0,X0),
inference(cnf_transformation,[],[f258]) ).
fof(f49723,plain,
! [X2,X0,X1] :
( k10_relat_1(X2,X1) = k4_relset_1(X0,X1,X2)
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f39422]) ).
fof(f49724,plain,
! [X2,X0,X1] :
( ~ v1_relat_1(X2)
| ~ r2_hidden(X0,k10_relat_1(X2,X1))
| r2_hidden(k1_funct_1(X2,X0),X1)
| ~ v1_funct_1(X2) ),
inference(cnf_transformation,[],[f41935]) ).
fof(f50290,plain,
! [X0,X1] :
( k1_struct_0(X0,X1) = k2_tarski(X1,X1)
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(definition_unfolding,[],[f42224,f47062]) ).
fof(f50684,plain,
! [X0,X1] :
( ~ v1_relat_1(X1)
| ~ r2_hidden(X0,k1_relat_1(X1))
| k2_tarski(k1_funct_1(X1,X0),k1_funct_1(X1,X0)) = k9_relat_1(X1,k2_tarski(X0,X0))
| ~ v1_funct_1(X1) ),
inference(definition_unfolding,[],[f44965,f47062,f47062]) ).
fof(f51428,definition,
sF1282 = k3_tsp_2(sK174,sK175),
introduced(definition,[new_symbols(definition,[sF1282])],[function_definition]) ).
fof(f51429,plain,
k3_tsp_2(sK174,sK175) = sF1282,
inference(reorient_equations,[],[f51428]) ).
fof(f51430,definition,
sF1283 = k1_struct_0(sK174,sK176),
introduced(definition,[new_symbols(definition,[sF1283])],[function_definition]) ).
fof(f51431,plain,
k1_struct_0(sK174,sK176) = sF1283,
inference(reorient_equations,[],[f51430]) ).
fof(f51432,definition,
sF1284 = k4_pre_topc(sK174,sK175,sF1282,sF1283),
introduced(definition,[new_symbols(definition,[sF1284])],[function_definition]) ).
fof(f51433,plain,
k4_pre_topc(sK174,sK175,sF1282,sF1283) = sF1284,
inference(reorient_equations,[],[f51432]) ).
fof(f51434,definition,
sF1285 = k4_tex_4(sK174,sK176),
introduced(definition,[new_symbols(definition,[sF1285])],[function_definition]) ).
fof(f51435,plain,
k4_tex_4(sK174,sK176) = sF1285,
inference(reorient_equations,[],[f51434]) ).
fof(f51436,definition,
sF1286 = k4_pre_topc(sK174,sK175,sF1282,sF1285),
introduced(definition,[new_symbols(definition,[sF1286])],[function_definition]) ).
fof(f51437,plain,
k4_pre_topc(sK174,sK175,sF1282,sF1285) = sF1286,
inference(reorient_equations,[],[f51436]) ).
fof(f51438,plain,
sF1284 != sF1286,
inference(definition_folding,[],[f42085,f51437,f51435,f51429,f51433,f51431,f51429]) ).
fof(f51439,definition,
sF1287 = u1_struct_0(sK174),
introduced(definition,[new_symbols(definition,[sF1287])],[function_definition]) ).
fof(f51440,plain,
u1_struct_0(sK174) = sF1287,
inference(reorient_equations,[],[f51439]) ).
fof(f51441,plain,
m1_subset_1(sK176,sF1287),
inference(definition_folding,[],[f42084,f51440]) ).
fof(f51523,plain,
( sF1284 = k9_relat_1(sF1282,sF1283)
| ~ l1_struct_0(sK174)
| ~ l1_struct_0(sK175)
| ~ v1_funct_1(sF1282)
| ~ v1_funct_2(sF1282,u1_struct_0(sK174),u1_struct_0(sK175))
| ~ m1_relset_1(sF1282,u1_struct_0(sK174),u1_struct_0(sK175)) ),
inference(superposition,[],[f42269,f51433]) ).
fof(f51524,plain,
( sF1286 = k9_relat_1(sF1282,sF1285)
| ~ l1_struct_0(sK174)
| ~ l1_struct_0(sK175)
| ~ v1_funct_1(sF1282)
| ~ v1_funct_2(sF1282,u1_struct_0(sK174),u1_struct_0(sK175))
| ~ m1_relset_1(sF1282,u1_struct_0(sK174),u1_struct_0(sK175)) ),
inference(superposition,[],[f42269,f51437]) ).
fof(f51529,plain,
( ~ v1_funct_2(sF1282,sF1287,u1_struct_0(sK175))
| sF1286 = k9_relat_1(sF1282,sF1285)
| ~ l1_struct_0(sK174)
| ~ l1_struct_0(sK175)
| ~ v1_funct_1(sF1282)
| ~ m1_relset_1(sF1282,u1_struct_0(sK174),u1_struct_0(sK175)) ),
inference(forward_demodulation,[],[f51524,f51440]) ).
fof(f51530,plain,
( ~ v1_funct_2(sF1282,sF1287,u1_struct_0(sK175))
| sF1284 = k9_relat_1(sF1282,sF1283)
| ~ l1_struct_0(sK174)
| ~ l1_struct_0(sK175)
| ~ v1_funct_1(sF1282)
| ~ m1_relset_1(sF1282,u1_struct_0(sK174),u1_struct_0(sK175)) ),
inference(forward_demodulation,[],[f51523,f51440]) ).
fof(f51533,plain,
( ~ m1_relset_1(sF1282,sF1287,u1_struct_0(sK175))
| ~ v1_funct_2(sF1282,sF1287,u1_struct_0(sK175))
| sF1286 = k9_relat_1(sF1282,sF1285)
| ~ l1_struct_0(sK174)
| ~ l1_struct_0(sK175)
| ~ v1_funct_1(sF1282) ),
inference(forward_demodulation,[],[f51529,f51440]) ).
fof(f51534,plain,
( ~ m1_relset_1(sF1282,sF1287,u1_struct_0(sK175))
| ~ v1_funct_2(sF1282,sF1287,u1_struct_0(sK175))
| sF1284 = k9_relat_1(sF1282,sF1283)
| ~ l1_struct_0(sK174)
| ~ l1_struct_0(sK175)
| ~ v1_funct_1(sF1282) ),
inference(forward_demodulation,[],[f51530,f51440]) ).
fof(f51536,definition,
( spl1288_13
<=> v1_funct_1(sF1282) ),
introduced(definition,[new_symbols(definition,[spl1288_13])],[avatar_definition]) ).
fof(f51537,plain,
( v1_funct_1(sF1282)
| ~ spl1288_13 ),
inference(avatar_component_clause,[],[f51536]) ).
fof(f51540,definition,
( spl1288_14
<=> l1_struct_0(sK175) ),
introduced(definition,[new_symbols(definition,[spl1288_14])],[avatar_definition]) ).
fof(f51541,plain,
( l1_struct_0(sK175)
| ~ spl1288_14 ),
inference(avatar_component_clause,[],[f51540]) ).
fof(f51542,plain,
( ~ l1_struct_0(sK175)
| spl1288_14 ),
inference(avatar_component_clause,[],[f51540]) ).
fof(f51544,definition,
( spl1288_15
<=> l1_struct_0(sK174) ),
introduced(definition,[new_symbols(definition,[spl1288_15])],[avatar_definition]) ).
fof(f51545,plain,
( l1_struct_0(sK174)
| ~ spl1288_15 ),
inference(avatar_component_clause,[],[f51544]) ).
fof(f51546,plain,
( ~ l1_struct_0(sK174)
| spl1288_15 ),
inference(avatar_component_clause,[],[f51544]) ).
fof(f51548,definition,
( spl1288_16
<=> sF1286 = k9_relat_1(sF1282,sF1285) ),
introduced(definition,[new_symbols(definition,[spl1288_16])],[avatar_definition]) ).
fof(f51550,plain,
( sF1286 = k9_relat_1(sF1282,sF1285)
| ~ spl1288_16 ),
inference(avatar_component_clause,[],[f51548]) ).
fof(f51552,definition,
( spl1288_17
<=> v1_funct_2(sF1282,sF1287,u1_struct_0(sK175)) ),
introduced(definition,[new_symbols(definition,[spl1288_17])],[avatar_definition]) ).
fof(f51556,definition,
( spl1288_18
<=> m1_relset_1(sF1282,sF1287,u1_struct_0(sK175)) ),
introduced(definition,[new_symbols(definition,[spl1288_18])],[avatar_definition]) ).
fof(f51557,plain,
( m1_relset_1(sF1282,sF1287,u1_struct_0(sK175))
| ~ spl1288_18 ),
inference(avatar_component_clause,[],[f51556]) ).
fof(f51558,plain,
( ~ m1_relset_1(sF1282,sF1287,u1_struct_0(sK175))
| spl1288_18 ),
inference(avatar_component_clause,[],[f51556]) ).
fof(f51561,definition,
( spl1288_19
<=> sF1284 = k9_relat_1(sF1282,sF1283) ),
introduced(definition,[new_symbols(definition,[spl1288_19])],[avatar_definition]) ).
fof(f51563,plain,
( sF1284 = k9_relat_1(sF1282,sF1283)
| ~ spl1288_19 ),
inference(avatar_component_clause,[],[f51561]) ).
fof(f51565,plain,
( ~ spl1288_13
| ~ spl1288_14
| ~ spl1288_15
| spl1288_16
| ~ spl1288_17
| ~ spl1288_18 ),
inference(avatar_split_clause,[],[f51533,f51556,f51552,f51548,f51544,f51540,f51536]) ).
fof(f51566,plain,
( ~ spl1288_13
| ~ spl1288_14
| ~ spl1288_15
| spl1288_19
| ~ spl1288_17
| ~ spl1288_18 ),
inference(avatar_split_clause,[],[f51534,f51556,f51552,f51561,f51544,f51540,f51536]) ).
fof(f51567,plain,
( m2_relset_1(sF1282,u1_struct_0(sK174),u1_struct_0(sK175))
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174)
| v3_struct_0(sK175)
| ~ v2_tsp_2(sK175,sK174)
| ~ m1_pre_topc(sK175,sK174) ),
inference(superposition,[],[f42340,f51429]) ).
fof(f51571,definition,
( spl1288_20
<=> v3_struct_0(sK174) ),
introduced(definition,[new_symbols(definition,[spl1288_20])],[avatar_definition]) ).
fof(f51572,plain,
( ~ v3_struct_0(sK174)
| spl1288_20 ),
inference(avatar_component_clause,[],[f51571]) ).
fof(f51579,definition,
( spl1288_22
<=> l1_pre_topc(sK174) ),
introduced(definition,[new_symbols(definition,[spl1288_22])],[avatar_definition]) ).
fof(f51583,definition,
( spl1288_23
<=> v2_pre_topc(sK174) ),
introduced(definition,[new_symbols(definition,[spl1288_23])],[avatar_definition]) ).
fof(f51584,plain,
( v2_pre_topc(sK174)
| ~ spl1288_23 ),
inference(avatar_component_clause,[],[f51583]) ).
fof(f51590,plain,
( m2_relset_1(sF1282,sF1287,u1_struct_0(sK175))
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174)
| v3_struct_0(sK175)
| ~ v2_tsp_2(sK175,sK174)
| ~ m1_pre_topc(sK175,sK174) ),
inference(forward_demodulation,[],[f51567,f51440]) ).
fof(f51592,definition,
( spl1288_25
<=> m1_pre_topc(sK175,sK174) ),
introduced(definition,[new_symbols(definition,[spl1288_25])],[avatar_definition]) ).
fof(f51594,plain,
( ~ m1_pre_topc(sK175,sK174)
| spl1288_25 ),
inference(avatar_component_clause,[],[f51592]) ).
fof(f51596,definition,
( spl1288_26
<=> v2_tsp_2(sK175,sK174) ),
introduced(definition,[new_symbols(definition,[spl1288_26])],[avatar_definition]) ).
fof(f51597,plain,
( v2_tsp_2(sK175,sK174)
| ~ spl1288_26 ),
inference(avatar_component_clause,[],[f51596]) ).
fof(f51600,definition,
( spl1288_27
<=> v3_struct_0(sK175) ),
introduced(definition,[new_symbols(definition,[spl1288_27])],[avatar_definition]) ).
fof(f51601,plain,
( ~ v3_struct_0(sK175)
| spl1288_27 ),
inference(avatar_component_clause,[],[f51600]) ).
fof(f51604,definition,
( spl1288_28
<=> m2_relset_1(sF1282,sF1287,u1_struct_0(sK175)) ),
introduced(definition,[new_symbols(definition,[spl1288_28])],[avatar_definition]) ).
fof(f51606,plain,
( m2_relset_1(sF1282,sF1287,u1_struct_0(sK175))
| ~ spl1288_28 ),
inference(avatar_component_clause,[],[f51604]) ).
fof(f51607,plain,
( ~ spl1288_25
| ~ spl1288_26
| spl1288_27
| ~ spl1288_22
| ~ spl1288_23
| spl1288_20
| spl1288_28 ),
inference(avatar_split_clause,[],[f51590,f51604,f51571,f51583,f51579,f51600,f51596,f51592]) ).
fof(f51610,plain,
~ spl1288_20,
inference(avatar_split_clause,[],[f42080,f51571]) ).
fof(f51613,plain,
spl1288_22,
inference(avatar_split_clause,[],[f42078,f51579]) ).
fof(f51616,plain,
spl1288_23,
inference(avatar_split_clause,[],[f42079,f51583]) ).
fof(f51617,plain,
( v1_funct_2(sF1282,u1_struct_0(sK174),u1_struct_0(sK175))
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174)
| v3_struct_0(sK175)
| ~ v2_tsp_2(sK175,sK174)
| ~ m1_pre_topc(sK175,sK174) ),
inference(superposition,[],[f42342,f51429]) ).
fof(f51628,plain,
( v1_funct_2(sF1282,sF1287,u1_struct_0(sK175))
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174)
| v3_struct_0(sK175)
| ~ v2_tsp_2(sK175,sK174)
| ~ m1_pre_topc(sK175,sK174) ),
inference(forward_demodulation,[],[f51617,f51440]) ).
fof(f51629,plain,
( ~ spl1288_25
| ~ spl1288_26
| spl1288_27
| ~ spl1288_22
| ~ spl1288_23
| spl1288_20
| spl1288_17 ),
inference(avatar_split_clause,[],[f51628,f51552,f51571,f51583,f51579,f51600,f51596,f51592]) ).
fof(f51630,plain,
( l1_pre_topc(sK175)
| ~ l1_pre_topc(sK174) ),
inference(resolution,[],[f42119,f42081]) ).
fof(f51632,definition,
( spl1288_31
<=> l1_pre_topc(sK175) ),
introduced(definition,[new_symbols(definition,[spl1288_31])],[avatar_definition]) ).
fof(f51635,plain,
( ~ spl1288_22
| spl1288_31 ),
inference(avatar_split_clause,[],[f51630,f51632,f51579]) ).
fof(f51669,plain,
( ~ m2_tsp_1(sK175,sK174)
| ~ l1_pre_topc(sK174)
| spl1288_25 ),
inference(resolution,[],[f51594,f42116]) ).
fof(f51671,definition,
( spl1288_37
<=> m2_tsp_1(sK175,sK174) ),
introduced(definition,[new_symbols(definition,[spl1288_37])],[avatar_definition]) ).
fof(f51674,plain,
( ~ spl1288_22
| ~ spl1288_37
| spl1288_25 ),
inference(avatar_split_clause,[],[f51669,f51592,f51671,f51579]) ).
fof(f51677,plain,
spl1288_37,
inference(avatar_split_clause,[],[f42081,f51671]) ).
fof(f51692,definition,
( spl1288_40
<=> m1_subset_1(sK176,sF1287) ),
introduced(definition,[new_symbols(definition,[spl1288_40])],[avatar_definition]) ).
fof(f51693,plain,
( m1_subset_1(sK176,sF1287)
| ~ spl1288_40 ),
inference(avatar_component_clause,[],[f51692]) ).
fof(f51698,plain,
spl1288_40,
inference(avatar_split_clause,[],[f51441,f51692]) ).
fof(f51699,plain,
( v1_funct_1(sF1282)
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174)
| v3_struct_0(sK175)
| ~ v2_tsp_2(sK175,sK174)
| ~ m1_pre_topc(sK175,sK174) ),
inference(superposition,[],[f42343,f51429]) ).
fof(f51700,plain,
( ~ spl1288_25
| ~ spl1288_26
| spl1288_27
| ~ spl1288_22
| ~ spl1288_23
| spl1288_20
| spl1288_13 ),
inference(avatar_split_clause,[],[f51699,f51536,f51571,f51583,f51579,f51600,f51596,f51592]) ).
fof(f51701,plain,
( v5_pre_topc(sF1282,sK174,sK175)
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174)
| v3_struct_0(sK175)
| ~ v2_tsp_2(sK175,sK174)
| ~ m1_pre_topc(sK175,sK174) ),
inference(superposition,[],[f42341,f51429]) ).
fof(f51703,definition,
( spl1288_41
<=> v5_pre_topc(sF1282,sK174,sK175) ),
introduced(definition,[new_symbols(definition,[spl1288_41])],[avatar_definition]) ).
fof(f51706,plain,
( ~ spl1288_25
| ~ spl1288_26
| spl1288_27
| ~ spl1288_22
| ~ spl1288_23
| spl1288_20
| spl1288_41 ),
inference(avatar_split_clause,[],[f51701,f51703,f51571,f51583,f51579,f51600,f51596,f51592]) ).
fof(f51719,plain,
spl1288_26,
inference(avatar_split_clause,[],[f42082,f51596]) ).
fof(f51722,plain,
~ spl1288_27,
inference(avatar_split_clause,[],[f42083,f51600]) ).
fof(f51723,plain,
( ~ l1_pre_topc(sK174)
| spl1288_15 ),
inference(resolution,[],[f43770,f51546]) ).
fof(f51724,plain,
( ~ spl1288_22
| spl1288_15 ),
inference(avatar_split_clause,[],[f51723,f51544,f51579]) ).
fof(f51725,plain,
( ~ l1_pre_topc(sK175)
| spl1288_14 ),
inference(resolution,[],[f51542,f43770]) ).
fof(f51726,plain,
( ~ spl1288_31
| spl1288_14 ),
inference(avatar_split_clause,[],[f51725,f51540,f51632]) ).
fof(f51786,plain,
! [X0] :
( k4_tex_4(sK174,X0) = k5_pre_topc(sK174,sK175,sF1282,k1_struct_0(sK175,k8_funct_2(u1_struct_0(sK174),u1_struct_0(sK175),sF1282,X0)))
| ~ m1_subset_1(X0,u1_struct_0(sK174))
| v3_struct_0(sK175)
| ~ v2_tsp_2(sK175,sK174)
| ~ m2_tsp_1(sK175,sK174)
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174) ),
inference(superposition,[],[f42335,f51429]) ).
fof(f51787,plain,
! [X0] :
( k4_tex_4(sK174,X0) = k5_pre_topc(sK174,sK175,sF1282,k1_struct_0(sK175,k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0)))
| ~ m1_subset_1(X0,u1_struct_0(sK174))
| v3_struct_0(sK175)
| ~ v2_tsp_2(sK175,sK174)
| ~ m2_tsp_1(sK175,sK174)
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174) ),
inference(forward_demodulation,[],[f51786,f51440]) ).
fof(f51796,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1287)
| k4_tex_4(sK174,X0) = k5_pre_topc(sK174,sK175,sF1282,k1_struct_0(sK175,k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0)))
| v3_struct_0(sK175)
| ~ v2_tsp_2(sK175,sK174)
| ~ m2_tsp_1(sK175,sK174)
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174) ),
inference(forward_demodulation,[],[f51787,f51440]) ).
fof(f51798,definition,
( spl1288_55
<=> ! [X0] :
( ~ m1_subset_1(X0,sF1287)
| k4_tex_4(sK174,X0) = k5_pre_topc(sK174,sK175,sF1282,k1_struct_0(sK175,k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0))) ) ),
introduced(definition,[new_symbols(definition,[spl1288_55])],[avatar_definition]) ).
fof(f51799,plain,
( ! [X0] :
( k4_tex_4(sK174,X0) = k5_pre_topc(sK174,sK175,sF1282,k1_struct_0(sK175,k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0)))
| ~ m1_subset_1(X0,sF1287) )
| ~ spl1288_55 ),
inference(avatar_component_clause,[],[f51798]) ).
fof(f51800,plain,
( ~ spl1288_22
| ~ spl1288_23
| spl1288_20
| ~ spl1288_37
| ~ spl1288_26
| spl1288_27
| spl1288_55 ),
inference(avatar_split_clause,[],[f51796,f51798,f51600,f51596,f51671,f51571,f51583,f51579]) ).
fof(f51802,plain,
( ~ m2_relset_1(sF1282,sF1287,u1_struct_0(sK175))
| spl1288_18 ),
inference(resolution,[],[f45025,f51558]) ).
fof(f51803,plain,
( ~ spl1288_28
| spl1288_18 ),
inference(avatar_split_clause,[],[f51802,f51556,f51604]) ).
fof(f51827,plain,
! [X2,X0,X1] :
( k4_tex_4(X0,X1) = k5_pre_topc(X0,X2,k1_tsp_2(X0,X2),k1_struct_0(X2,X1))
| ~ m1_subset_1(X1,u1_struct_0(X2))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X2)
| ~ v2_tsp_2(X2,X0)
| ~ m2_tsp_1(X2,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(equality_resolution,[],[f45239]) ).
fof(f51897,definition,
( spl1288_66
<=> v3_borsuk_1(sF1282,sK174,sK175) ),
introduced(definition,[new_symbols(definition,[spl1288_66])],[avatar_definition]) ).
fof(f51899,plain,
( ~ v3_borsuk_1(sF1282,sK174,sK175)
| spl1288_66 ),
inference(avatar_component_clause,[],[f51897]) ).
fof(f51901,definition,
( spl1288_67
<=> sF1282 = k1_tsp_2(sK174,sK175) ),
introduced(definition,[new_symbols(definition,[spl1288_67])],[avatar_definition]) ).
fof(f51902,plain,
( sF1282 != k1_tsp_2(sK174,sK175)
| spl1288_67 ),
inference(avatar_component_clause,[],[f51901]) ).
fof(f51903,plain,
( sF1282 = k1_tsp_2(sK174,sK175)
| ~ spl1288_67 ),
inference(avatar_component_clause,[],[f51901]) ).
fof(f51922,plain,
( ! [X0] :
( r1_tarski(sF1284,k9_relat_1(sF1282,X0))
| ~ r1_tarski(sF1283,X0)
| ~ v1_relat_1(sF1282) )
| ~ spl1288_19 ),
inference(superposition,[],[f44980,f51563]) ).
fof(f51926,definition,
( spl1288_70
<=> v1_relat_1(sF1282) ),
introduced(definition,[new_symbols(definition,[spl1288_70])],[avatar_definition]) ).
fof(f51927,plain,
( v1_relat_1(sF1282)
| ~ spl1288_70 ),
inference(avatar_component_clause,[],[f51926]) ).
fof(f51928,plain,
( ~ v1_relat_1(sF1282)
| spl1288_70 ),
inference(avatar_component_clause,[],[f51926]) ).
fof(f51938,definition,
( spl1288_73
<=> ! [X0] :
( r1_tarski(sF1284,k9_relat_1(sF1282,X0))
| ~ r1_tarski(sF1283,X0) ) ),
introduced(definition,[new_symbols(definition,[spl1288_73])],[avatar_definition]) ).
fof(f51939,plain,
( ! [X0] :
( r1_tarski(sF1284,k9_relat_1(sF1282,X0))
| ~ r1_tarski(sF1283,X0) )
| ~ spl1288_73 ),
inference(avatar_component_clause,[],[f51938]) ).
fof(f51940,plain,
( ~ spl1288_70
| spl1288_73
| ~ spl1288_19 ),
inference(avatar_split_clause,[],[f51922,f51561,f51938,f51926]) ).
fof(f51954,plain,
( sF1283 = k2_tarski(sK176,sK176)
| v3_struct_0(sK174)
| ~ l1_struct_0(sK174)
| ~ m1_subset_1(sK176,u1_struct_0(sK174)) ),
inference(superposition,[],[f50290,f51431]) ).
fof(f51963,plain,
! [X2,X0,X1] :
( k4_tex_4(X1,X0) = k5_pre_topc(X1,X2,k1_tsp_2(X1,X2),k2_tarski(X0,X0))
| ~ m1_subset_1(X0,u1_struct_0(X2))
| ~ m1_subset_1(X0,u1_struct_0(X1))
| 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)
| v3_struct_0(X2)
| ~ l1_struct_0(X2)
| ~ m1_subset_1(X0,u1_struct_0(X2)) ),
inference(superposition,[],[f51827,f50290]) ).
fof(f51964,plain,
! [X2,X0,X1] :
( ~ v2_tsp_2(X2,X1)
| ~ m1_subset_1(X0,u1_struct_0(X2))
| ~ m1_subset_1(X0,u1_struct_0(X1))
| v3_struct_0(X2)
| k4_tex_4(X1,X0) = k5_pre_topc(X1,X2,k1_tsp_2(X1,X2),k2_tarski(X0,X0))
| ~ m2_tsp_1(X2,X1)
| v3_struct_0(X1)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1)
| ~ l1_struct_0(X2) ),
inference(duplicate_literal_removal,[],[f51963]) ).
fof(f51973,plain,
( ~ m1_subset_1(sK176,sF1287)
| sF1283 = k2_tarski(sK176,sK176)
| v3_struct_0(sK174)
| ~ l1_struct_0(sK174) ),
inference(forward_demodulation,[],[f51954,f51440]) ).
fof(f51979,definition,
( spl1288_76
<=> sF1283 = k2_tarski(sK176,sK176) ),
introduced(definition,[new_symbols(definition,[spl1288_76])],[avatar_definition]) ).
fof(f51981,plain,
( sF1283 = k2_tarski(sK176,sK176)
| ~ spl1288_76 ),
inference(avatar_component_clause,[],[f51979]) ).
fof(f51983,plain,
( ~ spl1288_15
| spl1288_20
| spl1288_76
| ~ spl1288_40 ),
inference(avatar_split_clause,[],[f51973,f51692,f51979,f51571,f51544]) ).
fof(f52167,plain,
( ~ v1_xboole_0(sF1287)
| v3_struct_0(sK174)
| ~ l1_struct_0(sK174) ),
inference(superposition,[],[f43773,f51440]) ).
fof(f52169,definition,
( spl1288_91
<=> v1_xboole_0(sF1287) ),
introduced(definition,[new_symbols(definition,[spl1288_91])],[avatar_definition]) ).
fof(f52172,plain,
( ~ spl1288_15
| spl1288_20
| ~ spl1288_91 ),
inference(avatar_split_clause,[],[f52167,f52169,f51571,f51544]) ).
fof(f52201,plain,
( r1_tarski(sF1283,k2_tex_4(sK174,sK176))
| ~ m1_subset_1(sK176,u1_struct_0(sK174))
| v3_struct_0(sK174)
| ~ l1_pre_topc(sK174) ),
inference(superposition,[],[f45232,f51431]) ).
fof(f52212,plain,
( ~ m1_subset_1(sK176,sF1287)
| r1_tarski(sF1283,k2_tex_4(sK174,sK176))
| v3_struct_0(sK174)
| ~ l1_pre_topc(sK174) ),
inference(forward_demodulation,[],[f52201,f51440]) ).
fof(f52214,definition,
( spl1288_95
<=> r1_tarski(sF1283,k2_tex_4(sK174,sK176)) ),
introduced(definition,[new_symbols(definition,[spl1288_95])],[avatar_definition]) ).
fof(f52216,plain,
( r1_tarski(sF1283,k2_tex_4(sK174,sK176))
| ~ spl1288_95 ),
inference(avatar_component_clause,[],[f52214]) ).
fof(f52217,plain,
( ~ spl1288_22
| spl1288_20
| spl1288_95
| ~ spl1288_40 ),
inference(avatar_split_clause,[],[f52212,f51692,f52214,f51571,f51579]) ).
fof(f52219,plain,
( r1_tarski(sF1283,k4_tex_4(sK174,sK176))
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174)
| ~ m1_subset_1(sK176,u1_struct_0(sK174))
| ~ spl1288_95 ),
inference(superposition,[],[f52216,f42310]) ).
fof(f52220,plain,
( r1_tarski(sF1283,sF1285)
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174)
| ~ m1_subset_1(sK176,u1_struct_0(sK174))
| ~ spl1288_95 ),
inference(forward_demodulation,[],[f52219,f51435]) ).
fof(f52230,plain,
( ~ m1_subset_1(sK176,sF1287)
| r1_tarski(sF1283,sF1285)
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174)
| ~ spl1288_95 ),
inference(forward_demodulation,[],[f52220,f51440]) ).
fof(f52232,definition,
( spl1288_98
<=> r1_tarski(sF1283,sF1285) ),
introduced(definition,[new_symbols(definition,[spl1288_98])],[avatar_definition]) ).
fof(f52234,plain,
( r1_tarski(sF1283,sF1285)
| ~ spl1288_98 ),
inference(avatar_component_clause,[],[f52232]) ).
fof(f52235,plain,
( ~ spl1288_22
| ~ spl1288_23
| spl1288_20
| spl1288_98
| ~ spl1288_40
| ~ spl1288_95 ),
inference(avatar_split_clause,[],[f52230,f52214,f51692,f52232,f51571,f51583,f51579]) ).
fof(f52291,plain,
! [X2,X0,X1] :
( ~ v2_pre_topc(X1)
| m1_subset_1(X0,u1_struct_0(X1))
| v3_struct_0(X1)
| ~ r2_hidden(X0,k4_tex_4(X1,X2))
| ~ l1_pre_topc(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1)) ),
inference(resolution,[],[f42453,f42311]) ).
fof(f52299,plain,
! [X2,X0,X1] :
( r2_hidden(k8_funct_2(u1_struct_0(X1),u1_struct_0(X2),k3_tsp_2(X1,X2),X0),k4_tex_4(X1,X0))
| ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ v1_funct_1(k3_tsp_2(X1,X2))
| ~ v1_funct_2(k3_tsp_2(X1,X2),u1_struct_0(X1),u1_struct_0(X2))
| ~ v5_pre_topc(k3_tsp_2(X1,X2),X1,X2)
| ~ m2_relset_1(k3_tsp_2(X1,X2),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,[],[f42336]) ).
fof(f52310,plain,
! [X0] :
( r2_hidden(k8_funct_2(u1_struct_0(sK174),u1_struct_0(sK175),sF1282,X0),k4_tex_4(sK174,X0))
| ~ m1_subset_1(X0,u1_struct_0(sK174))
| ~ v1_funct_1(sF1282)
| ~ v1_funct_2(sF1282,u1_struct_0(sK174),u1_struct_0(sK175))
| ~ v5_pre_topc(sF1282,sK174,sK175)
| ~ m2_relset_1(sF1282,u1_struct_0(sK174),u1_struct_0(sK175))
| v3_struct_0(sK175)
| ~ v2_tsp_2(sK175,sK174)
| ~ m2_tsp_1(sK175,sK174)
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174) ),
inference(superposition,[],[f52299,f51429]) ).
fof(f52313,plain,
! [X0] :
( r2_hidden(k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0),k4_tex_4(sK174,X0))
| ~ m1_subset_1(X0,u1_struct_0(sK174))
| ~ v1_funct_1(sF1282)
| ~ v1_funct_2(sF1282,u1_struct_0(sK174),u1_struct_0(sK175))
| ~ v5_pre_topc(sF1282,sK174,sK175)
| ~ m2_relset_1(sF1282,u1_struct_0(sK174),u1_struct_0(sK175))
| v3_struct_0(sK175)
| ~ v2_tsp_2(sK175,sK174)
| ~ m2_tsp_1(sK175,sK174)
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174) ),
inference(forward_demodulation,[],[f52310,f51440]) ).
fof(f52323,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1287)
| r2_hidden(k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0),k4_tex_4(sK174,X0))
| ~ v1_funct_1(sF1282)
| ~ v1_funct_2(sF1282,u1_struct_0(sK174),u1_struct_0(sK175))
| ~ v5_pre_topc(sF1282,sK174,sK175)
| ~ m2_relset_1(sF1282,u1_struct_0(sK174),u1_struct_0(sK175))
| v3_struct_0(sK175)
| ~ v2_tsp_2(sK175,sK174)
| ~ m2_tsp_1(sK175,sK174)
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174) ),
inference(forward_demodulation,[],[f52313,f51440]) ).
fof(f52325,plain,
! [X0] :
( ~ v1_funct_2(sF1282,sF1287,u1_struct_0(sK175))
| ~ m1_subset_1(X0,sF1287)
| r2_hidden(k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0),k4_tex_4(sK174,X0))
| ~ v1_funct_1(sF1282)
| ~ v5_pre_topc(sF1282,sK174,sK175)
| ~ m2_relset_1(sF1282,u1_struct_0(sK174),u1_struct_0(sK175))
| v3_struct_0(sK175)
| ~ v2_tsp_2(sK175,sK174)
| ~ m2_tsp_1(sK175,sK174)
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174) ),
inference(forward_demodulation,[],[f52323,f51440]) ).
fof(f52327,plain,
! [X0] :
( ~ m2_relset_1(sF1282,sF1287,u1_struct_0(sK175))
| ~ v1_funct_2(sF1282,sF1287,u1_struct_0(sK175))
| ~ m1_subset_1(X0,sF1287)
| r2_hidden(k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0),k4_tex_4(sK174,X0))
| ~ v1_funct_1(sF1282)
| ~ v5_pre_topc(sF1282,sK174,sK175)
| v3_struct_0(sK175)
| ~ v2_tsp_2(sK175,sK174)
| ~ m2_tsp_1(sK175,sK174)
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174) ),
inference(forward_demodulation,[],[f52325,f51440]) ).
fof(f52333,definition,
( spl1288_110
<=> ! [X0] :
( ~ m1_subset_1(X0,sF1287)
| r2_hidden(k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0),k4_tex_4(sK174,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl1288_110])],[avatar_definition]) ).
fof(f52334,plain,
( ! [X0] :
( r2_hidden(k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0),k4_tex_4(sK174,X0))
| ~ m1_subset_1(X0,sF1287) )
| ~ spl1288_110 ),
inference(avatar_component_clause,[],[f52333]) ).
fof(f52335,plain,
( ~ spl1288_22
| ~ spl1288_23
| spl1288_20
| ~ spl1288_37
| ~ spl1288_26
| spl1288_27
| ~ spl1288_41
| ~ spl1288_13
| spl1288_110
| ~ spl1288_17
| ~ spl1288_28 ),
inference(avatar_split_clause,[],[f52327,f51604,f51552,f52333,f51536,f51703,f51600,f51596,f51671,f51571,f51583,f51579]) ).
fof(f52336,plain,
( r2_hidden(k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,sK176),sF1285)
| ~ m1_subset_1(sK176,sF1287)
| ~ spl1288_110 ),
inference(superposition,[],[f52334,f51435]) ).
fof(f52338,definition,
( spl1288_111
<=> r2_hidden(k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,sK176),sF1285) ),
introduced(definition,[new_symbols(definition,[spl1288_111])],[avatar_definition]) ).
fof(f52340,plain,
( r2_hidden(k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,sK176),sF1285)
| ~ spl1288_111 ),
inference(avatar_component_clause,[],[f52338]) ).
fof(f52341,plain,
( ~ spl1288_40
| spl1288_111
| ~ spl1288_110 ),
inference(avatar_split_clause,[],[f52336,f52333,f52338,f51692]) ).
fof(f52350,plain,
! [X2,X3,X0,X1] :
( k4_tex_4(X0,X1) = k5_pre_topc(X0,X2,X3,k1_struct_0(X2,X1))
| ~ m1_subset_1(X1,u1_struct_0(X2))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v3_borsuk_1(X3,X0,X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X2))
| ~ v5_pre_topc(X3,X0,X2)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ v2_tsp_2(X2,X0)
| ~ m2_tsp_1(X2,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(equality_resolution,[],[f42271]) ).
fof(f52357,plain,
( ! [X0] :
( k4_tex_4(sK174,X0) = k4_tex_4(sK174,k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0))
| ~ m1_subset_1(k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0),u1_struct_0(sK175))
| ~ m1_subset_1(k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0),u1_struct_0(sK174))
| ~ v3_borsuk_1(sF1282,sK174,sK175)
| ~ v1_funct_1(sF1282)
| ~ v1_funct_2(sF1282,u1_struct_0(sK174),u1_struct_0(sK175))
| ~ v5_pre_topc(sF1282,sK174,sK175)
| ~ m2_relset_1(sF1282,u1_struct_0(sK174),u1_struct_0(sK175))
| v3_struct_0(sK175)
| ~ v2_tsp_2(sK175,sK174)
| ~ m2_tsp_1(sK175,sK174)
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174)
| ~ m1_subset_1(X0,sF1287) )
| ~ spl1288_55 ),
inference(superposition,[],[f52350,f51799]) ).
fof(f52477,plain,
( ! [X2,X0,X1] :
( k10_relat_1(X0,X1) = k5_pre_topc(sK174,X2,X0,X1)
| ~ l1_struct_0(X2)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK174),u1_struct_0(X2))
| ~ m1_relset_1(X0,u1_struct_0(sK174),u1_struct_0(X2)) )
| ~ spl1288_15 ),
inference(resolution,[],[f45068,f51545]) ).
fof(f52480,plain,
( ! [X2,X0,X1] :
( ~ v1_funct_2(X0,sF1287,u1_struct_0(X2))
| k10_relat_1(X0,X1) = k5_pre_topc(sK174,X2,X0,X1)
| ~ l1_struct_0(X2)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(sK174),u1_struct_0(X2)) )
| ~ spl1288_15 ),
inference(forward_demodulation,[],[f52477,f51440]) ).
fof(f52481,plain,
( ! [X2,X0,X1] :
( ~ l1_struct_0(X2)
| ~ v1_funct_2(X0,sF1287,u1_struct_0(X2))
| k10_relat_1(X0,X1) = k5_pre_topc(sK174,X2,X0,X1)
| ~ m1_relset_1(X0,sF1287,u1_struct_0(X2))
| ~ v1_funct_1(X0) )
| ~ spl1288_15 ),
inference(forward_demodulation,[],[f52480,f51440]) ).
fof(f52490,plain,
( ! [X0,X1] :
( ~ m1_relset_1(X0,sF1287,u1_struct_0(sK175))
| k10_relat_1(X0,X1) = k5_pre_topc(sK174,sK175,X0,X1)
| ~ v1_funct_2(X0,sF1287,u1_struct_0(sK175))
| ~ v1_funct_1(X0) )
| ~ spl1288_14
| ~ spl1288_15 ),
inference(resolution,[],[f52481,f51541]) ).
fof(f52499,plain,
( ! [X0] :
( k10_relat_1(sF1282,X0) = k5_pre_topc(sK174,sK175,sF1282,X0)
| ~ v1_funct_2(sF1282,sF1287,u1_struct_0(sK175))
| ~ v1_funct_1(sF1282) )
| ~ spl1288_14
| ~ spl1288_15
| ~ spl1288_18 ),
inference(resolution,[],[f52490,f51557]) ).
fof(f52501,definition,
( spl1288_125
<=> ! [X0] : k10_relat_1(sF1282,X0) = k5_pre_topc(sK174,sK175,sF1282,X0) ),
introduced(definition,[new_symbols(definition,[spl1288_125])],[avatar_definition]) ).
fof(f52502,plain,
( ! [X0] : k10_relat_1(sF1282,X0) = k5_pre_topc(sK174,sK175,sF1282,X0)
| ~ spl1288_125 ),
inference(avatar_component_clause,[],[f52501]) ).
fof(f52503,plain,
( ~ spl1288_13
| ~ spl1288_17
| spl1288_125
| ~ spl1288_14
| ~ spl1288_15
| ~ spl1288_18 ),
inference(avatar_split_clause,[],[f52499,f51556,f51544,f51540,f52501,f51552,f51536]) ).
fof(f52553,plain,
( ! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sK174))
| v3_struct_0(sK174)
| ~ r2_hidden(X0,k4_tex_4(sK174,X1))
| ~ l1_pre_topc(sK174)
| ~ m1_subset_1(X1,u1_struct_0(sK174)) )
| ~ spl1288_23 ),
inference(resolution,[],[f52291,f51584]) ).
fof(f52559,plain,
( ! [X0,X1] :
( m1_subset_1(X0,sF1287)
| v3_struct_0(sK174)
| ~ r2_hidden(X0,k4_tex_4(sK174,X1))
| ~ l1_pre_topc(sK174)
| ~ m1_subset_1(X1,u1_struct_0(sK174)) )
| ~ spl1288_23 ),
inference(forward_demodulation,[],[f52553,f51440]) ).
fof(f52560,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF1287)
| m1_subset_1(X0,sF1287)
| v3_struct_0(sK174)
| ~ r2_hidden(X0,k4_tex_4(sK174,X1))
| ~ l1_pre_topc(sK174) )
| ~ spl1288_23 ),
inference(forward_demodulation,[],[f52559,f51440]) ).
fof(f52562,definition,
( spl1288_133
<=> ! [X0,X1] :
( ~ m1_subset_1(X1,sF1287)
| m1_subset_1(X0,sF1287)
| ~ r2_hidden(X0,k4_tex_4(sK174,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl1288_133])],[avatar_definition]) ).
fof(f52563,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF1287)
| m1_subset_1(X0,sF1287)
| ~ r2_hidden(X0,k4_tex_4(sK174,X1)) )
| ~ spl1288_133 ),
inference(avatar_component_clause,[],[f52562]) ).
fof(f52564,plain,
( ~ spl1288_22
| spl1288_20
| spl1288_133
| ~ spl1288_23 ),
inference(avatar_split_clause,[],[f52560,f51583,f52562,f51571,f51579]) ).
fof(f52587,plain,
( ! [X0] :
( m1_subset_1(X0,sF1287)
| ~ r2_hidden(X0,k4_tex_4(sK174,sK176)) )
| ~ spl1288_40
| ~ spl1288_133 ),
inference(resolution,[],[f52563,f51693]) ).
fof(f52588,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF1285)
| m1_subset_1(X0,sF1287) )
| ~ spl1288_40
| ~ spl1288_133 ),
inference(forward_demodulation,[],[f52587,f51435]) ).
fof(f52589,plain,
( m1_subset_1(k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,sK176),sF1287)
| ~ spl1288_40
| ~ spl1288_111
| ~ spl1288_133 ),
inference(resolution,[],[f52588,f52340]) ).
fof(f52642,plain,
! [X2,X0,X1] :
( v1_relat_1(X0)
| ~ m2_relset_1(X0,X1,X2) ),
inference(resolution,[],[f45265,f45266]) ).
fof(f52644,plain,
( ! [X0,X1] : ~ m2_relset_1(sF1282,X0,X1)
| spl1288_70 ),
inference(resolution,[],[f52642,f51928]) ).
fof(f52646,plain,
( $false
| ~ spl1288_28
| spl1288_70 ),
inference(backward_subsumption_resolution,[],[f51606,f52644]) ).
fof(f52648,plain,
( ~ spl1288_28
| spl1288_70 ),
inference(avatar_contradiction_clause,[],[f52646]) ).
fof(f52657,definition,
( spl1288_142
<=> sF1284 = sF1286 ),
introduced(definition,[new_symbols(definition,[spl1288_142])],[avatar_definition]) ).
fof(f52661,definition,
( spl1288_143
<=> r1_tarski(sF1286,sF1284) ),
introduced(definition,[new_symbols(definition,[spl1288_143])],[avatar_definition]) ).
fof(f52666,plain,
( ! [X0] :
( ~ r1_tarski(sF1283,X0)
| ~ r1_tarski(k9_relat_1(sF1282,X0),sF1284)
| sF1284 = k9_relat_1(sF1282,X0) )
| ~ spl1288_73 ),
inference(resolution,[],[f51939,f43334]) ).
fof(f53116,plain,
( ! [X0] :
( k1_tsp_2(sK174,sK175) != X0
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK174),u1_struct_0(sK175))
| ~ v5_pre_topc(X0,sK174,sK175)
| ~ m2_relset_1(X0,u1_struct_0(sK174),u1_struct_0(sK175))
| v3_struct_0(sK175)
| v3_borsuk_1(X0,sK174,sK175)
| ~ m2_tsp_1(sK175,sK174)
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174) )
| ~ spl1288_26 ),
inference(resolution,[],[f45241,f51597]) ).
fof(f53117,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF1287,u1_struct_0(sK175))
| k1_tsp_2(sK174,sK175) != X0
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK174,sK175)
| ~ m2_relset_1(X0,u1_struct_0(sK174),u1_struct_0(sK175))
| v3_struct_0(sK175)
| v3_borsuk_1(X0,sK174,sK175)
| ~ m2_tsp_1(sK175,sK174)
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174) )
| ~ spl1288_26 ),
inference(forward_demodulation,[],[f53116,f51440]) ).
fof(f53118,plain,
( ! [X0] :
( ~ m2_relset_1(X0,sF1287,u1_struct_0(sK175))
| ~ v1_funct_2(X0,sF1287,u1_struct_0(sK175))
| k1_tsp_2(sK174,sK175) != X0
| ~ v1_funct_1(X0)
| ~ v5_pre_topc(X0,sK174,sK175)
| v3_struct_0(sK175)
| v3_borsuk_1(X0,sK174,sK175)
| ~ m2_tsp_1(sK175,sK174)
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174) )
| ~ spl1288_26 ),
inference(forward_demodulation,[],[f53117,f51440]) ).
fof(f53120,definition,
( spl1288_186
<=> ! [X0] :
( ~ m2_relset_1(X0,sF1287,u1_struct_0(sK175))
| v3_borsuk_1(X0,sK174,sK175)
| ~ v5_pre_topc(X0,sK174,sK175)
| ~ v1_funct_1(X0)
| k1_tsp_2(sK174,sK175) != X0
| ~ v1_funct_2(X0,sF1287,u1_struct_0(sK175)) ) ),
introduced(definition,[new_symbols(definition,[spl1288_186])],[avatar_definition]) ).
fof(f53121,plain,
( ! [X0] :
( v3_borsuk_1(X0,sK174,sK175)
| ~ m2_relset_1(X0,sF1287,u1_struct_0(sK175))
| ~ v5_pre_topc(X0,sK174,sK175)
| ~ v1_funct_1(X0)
| k1_tsp_2(sK174,sK175) != X0
| ~ v1_funct_2(X0,sF1287,u1_struct_0(sK175)) )
| ~ spl1288_186 ),
inference(avatar_component_clause,[],[f53120]) ).
fof(f53122,plain,
( ~ spl1288_22
| ~ spl1288_23
| spl1288_20
| ~ spl1288_37
| spl1288_27
| spl1288_186
| ~ spl1288_26 ),
inference(avatar_split_clause,[],[f53118,f51596,f53120,f51600,f51671,f51571,f51583,f51579]) ).
fof(f53169,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK174))
| r2_hidden(X0,k2_pre_topc(sK174))
| ~ l1_struct_0(sK174) )
| spl1288_20 ),
inference(resolution,[],[f44533,f51572]) ).
fof(f53175,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF1287)
| r2_hidden(X0,k2_pre_topc(sK174))
| ~ l1_struct_0(sK174) )
| spl1288_20 ),
inference(forward_demodulation,[],[f53169,f51440]) ).
fof(f53177,definition,
( spl1288_193
<=> ! [X0] :
( ~ m1_subset_1(X0,sF1287)
| r2_hidden(X0,k2_pre_topc(sK174)) ) ),
introduced(definition,[new_symbols(definition,[spl1288_193])],[avatar_definition]) ).
fof(f53178,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF1287)
| r2_hidden(X0,k2_pre_topc(sK174)) )
| ~ spl1288_193 ),
inference(avatar_component_clause,[],[f53177]) ).
fof(f53179,plain,
( ~ spl1288_15
| spl1288_193
| spl1288_20 ),
inference(avatar_split_clause,[],[f53175,f51571,f53177,f51544]) ).
fof(f53181,plain,
( r2_hidden(sK176,k2_pre_topc(sK174))
| ~ spl1288_40
| ~ spl1288_193 ),
inference(resolution,[],[f53178,f51693]) ).
fof(f53188,plain,
( r2_hidden(sK176,u1_struct_0(sK174))
| ~ l1_struct_0(sK174)
| ~ spl1288_40
| ~ spl1288_193 ),
inference(superposition,[],[f53181,f44534]) ).
fof(f53189,plain,
( r2_hidden(sK176,sF1287)
| ~ l1_struct_0(sK174)
| ~ spl1288_40
| ~ spl1288_193 ),
inference(forward_demodulation,[],[f53188,f51440]) ).
fof(f53191,definition,
( spl1288_195
<=> r2_hidden(sK176,sF1287) ),
introduced(definition,[new_symbols(definition,[spl1288_195])],[avatar_definition]) ).
fof(f53194,plain,
( ~ spl1288_15
| spl1288_195
| ~ spl1288_40
| ~ spl1288_193 ),
inference(avatar_split_clause,[],[f53189,f53177,f51692,f53191,f51544]) ).
fof(f53318,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X0,X2,X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,X2,X1)
| k1_relat_1(X0) = k10_relat_1(X0,X1) ),
inference(superposition,[],[f49723,f45023]) ).
fof(f53321,plain,
( ~ v1_funct_1(sF1282)
| ~ m2_relset_1(sF1282,sF1287,u1_struct_0(sK175))
| k1_relat_1(sF1282) = k10_relat_1(sF1282,u1_struct_0(sK175))
| ~ spl1288_18 ),
inference(resolution,[],[f53318,f51557]) ).
fof(f53324,definition,
( spl1288_210
<=> k1_relat_1(sF1282) = k10_relat_1(sF1282,u1_struct_0(sK175)) ),
introduced(definition,[new_symbols(definition,[spl1288_210])],[avatar_definition]) ).
fof(f53326,plain,
( k1_relat_1(sF1282) = k10_relat_1(sF1282,u1_struct_0(sK175))
| ~ spl1288_210 ),
inference(avatar_component_clause,[],[f53324]) ).
fof(f53327,plain,
( spl1288_210
| ~ spl1288_28
| ~ spl1288_13
| ~ spl1288_18 ),
inference(avatar_split_clause,[],[f53321,f51556,f51536,f51604,f53324]) ).
fof(f53976,plain,
( ~ m2_relset_1(sF1282,sF1287,u1_struct_0(sK175))
| ~ v5_pre_topc(sF1282,sK174,sK175)
| ~ v1_funct_1(sF1282)
| sF1282 != k1_tsp_2(sK174,sK175)
| ~ v1_funct_2(sF1282,sF1287,u1_struct_0(sK175))
| spl1288_66
| ~ spl1288_186 ),
inference(resolution,[],[f53121,f51899]) ).
fof(f53977,plain,
( ~ spl1288_17
| ~ spl1288_67
| ~ spl1288_13
| ~ spl1288_41
| ~ spl1288_28
| spl1288_66
| ~ spl1288_186 ),
inference(avatar_split_clause,[],[f53976,f53120,f51897,f51604,f51703,f51536,f51901,f51552]) ).
fof(f53978,plain,
( k3_tsp_2(sK174,sK175) != sF1282
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174)
| v3_struct_0(sK175)
| ~ v2_tsp_2(sK175,sK174)
| ~ m1_pre_topc(sK175,sK174)
| spl1288_67 ),
inference(superposition,[],[f51902,f42339]) ).
fof(f53979,plain,
( sF1282 != sF1282
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174)
| v3_struct_0(sK175)
| ~ v2_tsp_2(sK175,sK174)
| ~ m1_pre_topc(sK175,sK174)
| spl1288_67 ),
inference(forward_demodulation,[],[f53978,f51429]) ).
fof(f53980,plain,
( v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174)
| v3_struct_0(sK175)
| ~ v2_tsp_2(sK175,sK174)
| ~ m1_pre_topc(sK175,sK174)
| spl1288_67 ),
inference(trivial_inequality_removal,[],[f53979]) ).
fof(f53981,plain,
( ~ spl1288_25
| ~ spl1288_26
| spl1288_27
| ~ spl1288_22
| ~ spl1288_23
| spl1288_20
| spl1288_67 ),
inference(avatar_split_clause,[],[f53980,f51901,f51571,f51583,f51579,f51600,f51596,f51592]) ).
fof(f53983,plain,
( ! [X0] :
( ~ m1_subset_1(k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0),sF1287)
| k4_tex_4(sK174,X0) = k4_tex_4(sK174,k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0))
| ~ m1_subset_1(k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0),u1_struct_0(sK175))
| ~ v3_borsuk_1(sF1282,sK174,sK175)
| ~ v1_funct_1(sF1282)
| ~ v1_funct_2(sF1282,u1_struct_0(sK174),u1_struct_0(sK175))
| ~ v5_pre_topc(sF1282,sK174,sK175)
| ~ m2_relset_1(sF1282,u1_struct_0(sK174),u1_struct_0(sK175))
| v3_struct_0(sK175)
| ~ v2_tsp_2(sK175,sK174)
| ~ m2_tsp_1(sK175,sK174)
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174)
| ~ m1_subset_1(X0,sF1287) )
| ~ spl1288_55 ),
inference(forward_demodulation,[],[f52357,f51440]) ).
fof(f53988,plain,
( ! [X0] :
( ~ v1_funct_2(sF1282,sF1287,u1_struct_0(sK175))
| ~ m1_subset_1(k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0),sF1287)
| k4_tex_4(sK174,X0) = k4_tex_4(sK174,k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0))
| ~ m1_subset_1(k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0),u1_struct_0(sK175))
| ~ v3_borsuk_1(sF1282,sK174,sK175)
| ~ v1_funct_1(sF1282)
| ~ v5_pre_topc(sF1282,sK174,sK175)
| ~ m2_relset_1(sF1282,u1_struct_0(sK174),u1_struct_0(sK175))
| v3_struct_0(sK175)
| ~ v2_tsp_2(sK175,sK174)
| ~ m2_tsp_1(sK175,sK174)
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174)
| ~ m1_subset_1(X0,sF1287) )
| ~ spl1288_55 ),
inference(forward_demodulation,[],[f53983,f51440]) ).
fof(f53992,plain,
( ! [X0] :
( ~ m2_relset_1(sF1282,sF1287,u1_struct_0(sK175))
| ~ v1_funct_2(sF1282,sF1287,u1_struct_0(sK175))
| ~ m1_subset_1(k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0),sF1287)
| k4_tex_4(sK174,X0) = k4_tex_4(sK174,k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0))
| ~ m1_subset_1(k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0),u1_struct_0(sK175))
| ~ v3_borsuk_1(sF1282,sK174,sK175)
| ~ v1_funct_1(sF1282)
| ~ v5_pre_topc(sF1282,sK174,sK175)
| v3_struct_0(sK175)
| ~ v2_tsp_2(sK175,sK174)
| ~ m2_tsp_1(sK175,sK174)
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174)
| ~ m1_subset_1(X0,sF1287) )
| ~ spl1288_55 ),
inference(forward_demodulation,[],[f53988,f51440]) ).
fof(f53996,definition,
( spl1288_288
<=> ! [X0] :
( ~ m1_subset_1(k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0),sF1287)
| ~ m1_subset_1(k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0),u1_struct_0(sK175))
| ~ m1_subset_1(X0,sF1287)
| k4_tex_4(sK174,X0) = k4_tex_4(sK174,k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl1288_288])],[avatar_definition]) ).
fof(f53997,plain,
( ! [X0] :
( ~ m1_subset_1(k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0),sF1287)
| ~ m1_subset_1(k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0),u1_struct_0(sK175))
| ~ m1_subset_1(X0,sF1287)
| k4_tex_4(sK174,X0) = k4_tex_4(sK174,k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0)) )
| ~ spl1288_288 ),
inference(avatar_component_clause,[],[f53996]) ).
fof(f53999,plain,
( ~ spl1288_22
| ~ spl1288_23
| spl1288_20
| ~ spl1288_37
| ~ spl1288_26
| spl1288_27
| ~ spl1288_41
| ~ spl1288_13
| ~ spl1288_66
| spl1288_288
| ~ spl1288_17
| ~ spl1288_28
| ~ spl1288_55 ),
inference(avatar_split_clause,[],[f53992,f51798,f51604,f51552,f53996,f51897,f51536,f51703,f51600,f51596,f51671,f51571,f51583,f51579]) ).
fof(f54062,plain,
( ~ r1_tarski(k9_relat_1(sF1282,sF1285),sF1284)
| sF1284 = k9_relat_1(sF1282,sF1285)
| ~ spl1288_73
| ~ spl1288_98 ),
inference(resolution,[],[f52666,f52234]) ).
fof(f54080,plain,
( ~ r1_tarski(sF1286,sF1284)
| sF1284 = k9_relat_1(sF1282,sF1285)
| ~ spl1288_16
| ~ spl1288_73
| ~ spl1288_98 ),
inference(forward_demodulation,[],[f54062,f51550]) ).
fof(f54423,plain,
( sF1284 = sF1286
| ~ r1_tarski(sF1286,sF1284)
| ~ spl1288_16
| ~ spl1288_73
| ~ spl1288_98 ),
inference(forward_demodulation,[],[f54080,f51550]) ).
fof(f54424,plain,
( ~ spl1288_143
| spl1288_142
| ~ spl1288_16
| ~ spl1288_73
| ~ spl1288_98 ),
inference(avatar_split_clause,[],[f54423,f52232,f51938,f51548,f52657,f52661]) ).
fof(f54459,plain,
~ spl1288_142,
inference(avatar_split_clause,[],[f51438,f52657]) ).
fof(f57230,plain,
( ! [X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(sK175))
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(sK175))
| k1_relat_1(X0) = k2_pre_topc(X1)
| ~ l1_struct_0(sK175)
| ~ l1_struct_0(X1) )
| spl1288_27 ),
inference(resolution,[],[f44500,f51601]) ).
fof(f57237,definition,
( spl1288_632
<=> ! [X0,X1] :
( ~ v1_funct_1(X0)
| ~ l1_struct_0(X1)
| k1_relat_1(X0) = k2_pre_topc(X1)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(sK175))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(sK175)) ) ),
introduced(definition,[new_symbols(definition,[spl1288_632])],[avatar_definition]) ).
fof(f57238,plain,
( ! [X0,X1] :
( ~ l1_struct_0(X1)
| ~ v1_funct_1(X0)
| k1_relat_1(X0) = k2_pre_topc(X1)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(sK175))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(sK175)) )
| ~ spl1288_632 ),
inference(avatar_component_clause,[],[f57237]) ).
fof(f57239,plain,
( ~ spl1288_14
| spl1288_632
| spl1288_27 ),
inference(avatar_split_clause,[],[f57230,f51600,f57237,f51540]) ).
fof(f57247,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| k1_relat_1(X0) = k2_pre_topc(sK174)
| ~ m2_relset_1(X0,u1_struct_0(sK174),u1_struct_0(sK175))
| ~ v1_funct_2(X0,u1_struct_0(sK174),u1_struct_0(sK175)) )
| ~ spl1288_15
| ~ spl1288_632 ),
inference(resolution,[],[f57238,f51545]) ).
fof(f57249,plain,
( ! [X0] :
( ~ m2_relset_1(X0,sF1287,u1_struct_0(sK175))
| ~ v1_funct_1(X0)
| k1_relat_1(X0) = k2_pre_topc(sK174)
| ~ v1_funct_2(X0,u1_struct_0(sK174),u1_struct_0(sK175)) )
| ~ spl1288_15
| ~ spl1288_632 ),
inference(forward_demodulation,[],[f57247,f51440]) ).
fof(f57250,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,sF1287,u1_struct_0(sK175))
| ~ v1_funct_2(X0,sF1287,u1_struct_0(sK175))
| k1_relat_1(X0) = k2_pre_topc(sK174) )
| ~ spl1288_15
| ~ spl1288_632 ),
inference(forward_demodulation,[],[f57249,f51440]) ).
fof(f57254,plain,
( ~ m2_relset_1(sF1282,sF1287,u1_struct_0(sK175))
| ~ v1_funct_2(sF1282,sF1287,u1_struct_0(sK175))
| k1_relat_1(sF1282) = k2_pre_topc(sK174)
| ~ spl1288_13
| ~ spl1288_15
| ~ spl1288_632 ),
inference(resolution,[],[f57250,f51537]) ).
fof(f57256,definition,
( spl1288_634
<=> k1_relat_1(sF1282) = k2_pre_topc(sK174) ),
introduced(definition,[new_symbols(definition,[spl1288_634])],[avatar_definition]) ).
fof(f57258,plain,
( k1_relat_1(sF1282) = k2_pre_topc(sK174)
| ~ spl1288_634 ),
inference(avatar_component_clause,[],[f57256]) ).
fof(f57259,plain,
( spl1288_634
| ~ spl1288_17
| ~ spl1288_28
| ~ spl1288_13
| ~ spl1288_15
| ~ spl1288_632 ),
inference(avatar_split_clause,[],[f57254,f57237,f51544,f51536,f51604,f51552,f57256]) ).
fof(f57260,plain,
( u1_struct_0(sK174) = k1_relat_1(sF1282)
| ~ l1_struct_0(sK174)
| ~ spl1288_634 ),
inference(superposition,[],[f57258,f44534]) ).
fof(f57279,plain,
( sF1287 = k1_relat_1(sF1282)
| ~ l1_struct_0(sK174)
| ~ spl1288_634 ),
inference(forward_demodulation,[],[f57260,f51440]) ).
fof(f57281,definition,
( spl1288_637
<=> sF1287 = k1_relat_1(sF1282) ),
introduced(definition,[new_symbols(definition,[spl1288_637])],[avatar_definition]) ).
fof(f57283,plain,
( sF1287 = k1_relat_1(sF1282)
| ~ spl1288_637 ),
inference(avatar_component_clause,[],[f57281]) ).
fof(f57285,plain,
( ~ spl1288_15
| spl1288_637
| ~ spl1288_634 ),
inference(avatar_split_clause,[],[f57279,f57256,f57281,f51544]) ).
fof(f59095,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,k10_relat_1(sF1282,X1))
| r2_hidden(k1_funct_1(sF1282,X0),X1)
| ~ v1_funct_1(sF1282) )
| ~ spl1288_70 ),
inference(resolution,[],[f49724,f51927]) ).
fof(f59097,definition,
( spl1288_815
<=> ! [X0,X1] :
( ~ r2_hidden(X0,k10_relat_1(sF1282,X1))
| r2_hidden(k1_funct_1(sF1282,X0),X1) ) ),
introduced(definition,[new_symbols(definition,[spl1288_815])],[avatar_definition]) ).
fof(f59098,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,k10_relat_1(sF1282,X1))
| r2_hidden(k1_funct_1(sF1282,X0),X1) )
| ~ spl1288_815 ),
inference(avatar_component_clause,[],[f59097]) ).
fof(f59099,plain,
( ~ spl1288_13
| spl1288_815
| ~ spl1288_70 ),
inference(avatar_split_clause,[],[f59095,f51926,f59097,f51536]) ).
fof(f59104,plain,
( ! [X0] :
( ~ r2_hidden(X0,k1_relat_1(sF1282))
| r2_hidden(k1_funct_1(sF1282,X0),u1_struct_0(sK175)) )
| ~ spl1288_210
| ~ spl1288_815 ),
inference(superposition,[],[f59098,f53326]) ).
fof(f59111,plain,
( ! [X0] :
( r2_hidden(k1_funct_1(sF1282,X0),u1_struct_0(sK175))
| ~ r2_hidden(X0,sF1287) )
| ~ spl1288_210
| ~ spl1288_637
| ~ spl1288_815 ),
inference(forward_demodulation,[],[f59104,f57283]) ).
fof(f59568,plain,
( ! [X0] :
( v1_xboole_0(sF1287)
| ~ v1_funct_1(sF1282)
| ~ v1_funct_2(sF1282,sF1287,u1_struct_0(sK175))
| k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0) = k1_funct_1(sF1282,X0)
| ~ m1_subset_1(X0,sF1287) )
| ~ spl1288_18 ),
inference(resolution,[],[f43920,f51557]) ).
fof(f59570,definition,
( spl1288_859
<=> ! [X0] :
( k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0) = k1_funct_1(sF1282,X0)
| ~ m1_subset_1(X0,sF1287) ) ),
introduced(definition,[new_symbols(definition,[spl1288_859])],[avatar_definition]) ).
fof(f59571,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF1287)
| k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,X0) = k1_funct_1(sF1282,X0) )
| ~ spl1288_859 ),
inference(avatar_component_clause,[],[f59570]) ).
fof(f59572,plain,
( spl1288_859
| ~ spl1288_17
| ~ spl1288_13
| spl1288_91
| ~ spl1288_18 ),
inference(avatar_split_clause,[],[f59568,f51556,f52169,f51536,f51552,f59570]) ).
fof(f59575,plain,
( k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,sK176) = k1_funct_1(sF1282,sK176)
| ~ spl1288_40
| ~ spl1288_859 ),
inference(resolution,[],[f59571,f51693]) ).
fof(f59740,plain,
( ~ m1_subset_1(k1_funct_1(sF1282,sK176),sF1287)
| ~ m1_subset_1(k1_funct_1(sF1282,sK176),u1_struct_0(sK175))
| ~ m1_subset_1(sK176,sF1287)
| k4_tex_4(sK174,sK176) = k4_tex_4(sK174,k1_funct_1(sF1282,sK176))
| ~ spl1288_40
| ~ spl1288_288
| ~ spl1288_859 ),
inference(superposition,[],[f53997,f59575]) ).
fof(f59741,plain,
( r2_hidden(k1_funct_1(sF1282,sK176),k4_tex_4(sK174,sK176))
| ~ m1_subset_1(sK176,sF1287)
| ~ spl1288_40
| ~ spl1288_110
| ~ spl1288_859 ),
inference(superposition,[],[f52334,f59575]) ).
fof(f59744,plain,
( r2_hidden(k1_funct_1(sF1282,sK176),sF1285)
| ~ m1_subset_1(sK176,sF1287)
| ~ spl1288_40
| ~ spl1288_110
| ~ spl1288_859 ),
inference(forward_demodulation,[],[f59741,f51435]) ).
fof(f59745,plain,
( sF1285 = k4_tex_4(sK174,k1_funct_1(sF1282,sK176))
| ~ m1_subset_1(k1_funct_1(sF1282,sK176),sF1287)
| ~ m1_subset_1(k1_funct_1(sF1282,sK176),u1_struct_0(sK175))
| ~ m1_subset_1(sK176,sF1287)
| ~ spl1288_40
| ~ spl1288_288
| ~ spl1288_859 ),
inference(forward_demodulation,[],[f59740,f51435]) ).
fof(f59748,definition,
( spl1288_877
<=> r2_hidden(k1_funct_1(sF1282,sK176),sF1285) ),
introduced(definition,[new_symbols(definition,[spl1288_877])],[avatar_definition]) ).
fof(f59750,plain,
( r2_hidden(k1_funct_1(sF1282,sK176),sF1285)
| ~ spl1288_877 ),
inference(avatar_component_clause,[],[f59748]) ).
fof(f59751,plain,
( ~ spl1288_40
| spl1288_877
| ~ spl1288_40
| ~ spl1288_110
| ~ spl1288_859 ),
inference(avatar_split_clause,[],[f59744,f59570,f52333,f51692,f59748,f51692]) ).
fof(f59753,definition,
( spl1288_878
<=> m1_subset_1(k1_funct_1(sF1282,sK176),u1_struct_0(sK175)) ),
introduced(definition,[new_symbols(definition,[spl1288_878])],[avatar_definition]) ).
fof(f59755,plain,
( ~ m1_subset_1(k1_funct_1(sF1282,sK176),u1_struct_0(sK175))
| spl1288_878 ),
inference(avatar_component_clause,[],[f59753]) ).
fof(f59757,definition,
( spl1288_879
<=> m1_subset_1(k1_funct_1(sF1282,sK176),sF1287) ),
introduced(definition,[new_symbols(definition,[spl1288_879])],[avatar_definition]) ).
fof(f59761,definition,
( spl1288_880
<=> sF1285 = k4_tex_4(sK174,k1_funct_1(sF1282,sK176)) ),
introduced(definition,[new_symbols(definition,[spl1288_880])],[avatar_definition]) ).
fof(f59763,plain,
( sF1285 = k4_tex_4(sK174,k1_funct_1(sF1282,sK176))
| ~ spl1288_880 ),
inference(avatar_component_clause,[],[f59761]) ).
fof(f59764,plain,
( ~ spl1288_40
| ~ spl1288_878
| ~ spl1288_879
| spl1288_880
| ~ spl1288_40
| ~ spl1288_288
| ~ spl1288_859 ),
inference(avatar_split_clause,[],[f59745,f59570,f53996,f51692,f59761,f59757,f59753,f51692]) ).
fof(f59777,plain,
( ~ r2_hidden(k1_funct_1(sF1282,sK176),u1_struct_0(sK175))
| spl1288_878 ),
inference(resolution,[],[f59755,f43271]) ).
fof(f59794,plain,
( m1_subset_1(k1_funct_1(sF1282,sK176),sF1287)
| ~ spl1288_40
| ~ spl1288_133
| ~ spl1288_877 ),
inference(resolution,[],[f59750,f52588]) ).
fof(f59795,plain,
( spl1288_879
| ~ spl1288_40
| ~ spl1288_133
| ~ spl1288_877 ),
inference(avatar_split_clause,[],[f59794,f59748,f52562,f51692,f59757]) ).
fof(f60384,plain,
( ~ r2_hidden(sK176,sF1287)
| ~ spl1288_210
| ~ spl1288_637
| ~ spl1288_815
| spl1288_878 ),
inference(resolution,[],[f59777,f59111]) ).
fof(f60388,plain,
( ~ spl1288_195
| ~ spl1288_210
| ~ spl1288_637
| ~ spl1288_815
| spl1288_878 ),
inference(avatar_split_clause,[],[f60384,f59753,f59097,f57281,f53324,f53191]) ).
fof(f61697,plain,
( ! [X0] :
( ~ r2_hidden(X0,k1_relat_1(sF1282))
| k2_tarski(k1_funct_1(sF1282,X0),k1_funct_1(sF1282,X0)) = k9_relat_1(sF1282,k2_tarski(X0,X0))
| ~ v1_funct_1(sF1282) )
| ~ spl1288_70 ),
inference(resolution,[],[f50684,f51927]) ).
fof(f61698,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF1287)
| k2_tarski(k1_funct_1(sF1282,X0),k1_funct_1(sF1282,X0)) = k9_relat_1(sF1282,k2_tarski(X0,X0))
| ~ v1_funct_1(sF1282) )
| ~ spl1288_70
| ~ spl1288_637 ),
inference(forward_demodulation,[],[f61697,f57283]) ).
fof(f61700,definition,
( spl1288_1077
<=> ! [X0] :
( ~ r2_hidden(X0,sF1287)
| k2_tarski(k1_funct_1(sF1282,X0),k1_funct_1(sF1282,X0)) = k9_relat_1(sF1282,k2_tarski(X0,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl1288_1077])],[avatar_definition]) ).
fof(f61701,plain,
( ! [X0] :
( k2_tarski(k1_funct_1(sF1282,X0),k1_funct_1(sF1282,X0)) = k9_relat_1(sF1282,k2_tarski(X0,X0))
| ~ r2_hidden(X0,sF1287) )
| ~ spl1288_1077 ),
inference(avatar_component_clause,[],[f61700]) ).
fof(f61702,plain,
( ~ spl1288_13
| spl1288_1077
| ~ spl1288_70
| ~ spl1288_637 ),
inference(avatar_split_clause,[],[f61698,f57281,f51926,f61700,f51536]) ).
fof(f69045,plain,
( ! [X0] :
( r1_tarski(k9_relat_1(sF1282,k10_relat_1(sF1282,X0)),X0)
| ~ v1_funct_1(sF1282) )
| ~ spl1288_70 ),
inference(resolution,[],[f44958,f51927]) ).
fof(f69047,definition,
( spl1288_1479
<=> ! [X0] : r1_tarski(k9_relat_1(sF1282,k10_relat_1(sF1282,X0)),X0) ),
introduced(definition,[new_symbols(definition,[spl1288_1479])],[avatar_definition]) ).
fof(f69048,plain,
( ! [X0] : r1_tarski(k9_relat_1(sF1282,k10_relat_1(sF1282,X0)),X0)
| ~ spl1288_1479 ),
inference(avatar_component_clause,[],[f69047]) ).
fof(f69049,plain,
( ~ spl1288_13
| spl1288_1479
| ~ spl1288_70 ),
inference(avatar_split_clause,[],[f69045,f51926,f69047,f51536]) ).
fof(f74101,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK175))
| ~ m1_subset_1(X0,u1_struct_0(sK174))
| v3_struct_0(sK175)
| k4_tex_4(sK174,X0) = k5_pre_topc(sK174,sK175,k1_tsp_2(sK174,sK175),k2_tarski(X0,X0))
| ~ m2_tsp_1(sK175,sK174)
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174)
| ~ l1_struct_0(sK175) )
| ~ spl1288_26 ),
inference(resolution,[],[f51964,f51597]) ).
fof(f74102,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF1287)
| ~ m1_subset_1(X0,u1_struct_0(sK175))
| v3_struct_0(sK175)
| k4_tex_4(sK174,X0) = k5_pre_topc(sK174,sK175,k1_tsp_2(sK174,sK175),k2_tarski(X0,X0))
| ~ m2_tsp_1(sK175,sK174)
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174)
| ~ l1_struct_0(sK175) )
| ~ spl1288_26 ),
inference(forward_demodulation,[],[f74101,f51440]) ).
fof(f74103,plain,
( ! [X0] :
( k4_tex_4(sK174,X0) = k5_pre_topc(sK174,sK175,sF1282,k2_tarski(X0,X0))
| ~ m1_subset_1(X0,sF1287)
| ~ m1_subset_1(X0,u1_struct_0(sK175))
| v3_struct_0(sK175)
| ~ m2_tsp_1(sK175,sK174)
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174)
| ~ l1_struct_0(sK175) )
| ~ spl1288_26
| ~ spl1288_67 ),
inference(forward_demodulation,[],[f74102,f51903]) ).
fof(f74104,plain,
( ! [X0] :
( k4_tex_4(sK174,X0) = k10_relat_1(sF1282,k2_tarski(X0,X0))
| ~ m1_subset_1(X0,sF1287)
| ~ m1_subset_1(X0,u1_struct_0(sK175))
| v3_struct_0(sK175)
| ~ m2_tsp_1(sK175,sK174)
| v3_struct_0(sK174)
| ~ v2_pre_topc(sK174)
| ~ l1_pre_topc(sK174)
| ~ l1_struct_0(sK175) )
| ~ spl1288_26
| ~ spl1288_67
| ~ spl1288_125 ),
inference(forward_demodulation,[],[f74103,f52502]) ).
fof(f74106,definition,
( spl1288_1805
<=> ! [X0] :
( k4_tex_4(sK174,X0) = k10_relat_1(sF1282,k2_tarski(X0,X0))
| ~ m1_subset_1(X0,u1_struct_0(sK175))
| ~ m1_subset_1(X0,sF1287) ) ),
introduced(definition,[new_symbols(definition,[spl1288_1805])],[avatar_definition]) ).
fof(f74107,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF1287)
| ~ m1_subset_1(X0,u1_struct_0(sK175))
| k4_tex_4(sK174,X0) = k10_relat_1(sF1282,k2_tarski(X0,X0)) )
| ~ spl1288_1805 ),
inference(avatar_component_clause,[],[f74106]) ).
fof(f74108,plain,
( ~ spl1288_14
| ~ spl1288_22
| ~ spl1288_23
| spl1288_20
| ~ spl1288_37
| spl1288_27
| spl1288_1805
| ~ spl1288_26
| ~ spl1288_67
| ~ spl1288_125 ),
inference(avatar_split_clause,[],[f74104,f52501,f51901,f51596,f74106,f51600,f51671,f51571,f51583,f51579,f51540]) ).
fof(f74114,plain,
( ~ m1_subset_1(k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,sK176),u1_struct_0(sK175))
| k4_tex_4(sK174,k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,sK176)) = k10_relat_1(sF1282,k2_tarski(k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,sK176),k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,sK176)))
| ~ spl1288_40
| ~ spl1288_111
| ~ spl1288_133
| ~ spl1288_1805 ),
inference(resolution,[],[f74107,f52589]) ).
fof(f74124,plain,
( ~ m1_subset_1(k1_funct_1(sF1282,sK176),u1_struct_0(sK175))
| k4_tex_4(sK174,k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,sK176)) = k10_relat_1(sF1282,k2_tarski(k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,sK176),k8_funct_2(sF1287,u1_struct_0(sK175),sF1282,sK176)))
| ~ spl1288_40
| ~ spl1288_111
| ~ spl1288_133
| ~ spl1288_859
| ~ spl1288_1805 ),
inference(forward_demodulation,[],[f74114,f59575]) ).
fof(f74131,plain,
( k4_tex_4(sK174,k1_funct_1(sF1282,sK176)) = k10_relat_1(sF1282,k2_tarski(k1_funct_1(sF1282,sK176),k1_funct_1(sF1282,sK176)))
| ~ m1_subset_1(k1_funct_1(sF1282,sK176),u1_struct_0(sK175))
| ~ spl1288_40
| ~ spl1288_111
| ~ spl1288_133
| ~ spl1288_859
| ~ spl1288_1805 ),
inference(forward_demodulation,[],[f74124,f59575]) ).
fof(f74135,definition,
( spl1288_1806
<=> sF1285 = k10_relat_1(sF1282,k2_tarski(k1_funct_1(sF1282,sK176),k1_funct_1(sF1282,sK176))) ),
introduced(definition,[new_symbols(definition,[spl1288_1806])],[avatar_definition]) ).
fof(f74137,plain,
( sF1285 = k10_relat_1(sF1282,k2_tarski(k1_funct_1(sF1282,sK176),k1_funct_1(sF1282,sK176)))
| ~ spl1288_1806 ),
inference(avatar_component_clause,[],[f74135]) ).
fof(f74150,plain,
( sF1285 = k10_relat_1(sF1282,k2_tarski(k1_funct_1(sF1282,sK176),k1_funct_1(sF1282,sK176)))
| ~ m1_subset_1(k1_funct_1(sF1282,sK176),u1_struct_0(sK175))
| ~ spl1288_40
| ~ spl1288_111
| ~ spl1288_133
| ~ spl1288_859
| ~ spl1288_880
| ~ spl1288_1805 ),
inference(forward_demodulation,[],[f74131,f59763]) ).
fof(f74154,plain,
( ~ spl1288_878
| spl1288_1806
| ~ spl1288_40
| ~ spl1288_111
| ~ spl1288_133
| ~ spl1288_859
| ~ spl1288_880
| ~ spl1288_1805 ),
inference(avatar_split_clause,[],[f74150,f74106,f59761,f59570,f52562,f52338,f51692,f74135,f59753]) ).
fof(f74163,plain,
( sF1285 = k10_relat_1(sF1282,k9_relat_1(sF1282,k2_tarski(sK176,sK176)))
| ~ r2_hidden(sK176,sF1287)
| ~ spl1288_1077
| ~ spl1288_1806 ),
inference(superposition,[],[f74137,f61701]) ).
fof(f74190,plain,
( sF1285 = k10_relat_1(sF1282,k9_relat_1(sF1282,sF1283))
| ~ r2_hidden(sK176,sF1287)
| ~ spl1288_76
| ~ spl1288_1077
| ~ spl1288_1806 ),
inference(forward_demodulation,[],[f74163,f51981]) ).
fof(f74191,plain,
( sF1285 = k10_relat_1(sF1282,sF1284)
| ~ r2_hidden(sK176,sF1287)
| ~ spl1288_19
| ~ spl1288_76
| ~ spl1288_1077
| ~ spl1288_1806 ),
inference(forward_demodulation,[],[f74190,f51563]) ).
fof(f74193,definition,
( spl1288_1809
<=> sF1285 = k10_relat_1(sF1282,sF1284) ),
introduced(definition,[new_symbols(definition,[spl1288_1809])],[avatar_definition]) ).
fof(f74195,plain,
( sF1285 = k10_relat_1(sF1282,sF1284)
| ~ spl1288_1809 ),
inference(avatar_component_clause,[],[f74193]) ).
fof(f74196,plain,
( ~ spl1288_195
| spl1288_1809
| ~ spl1288_19
| ~ spl1288_76
| ~ spl1288_1077
| ~ spl1288_1806 ),
inference(avatar_split_clause,[],[f74191,f74135,f61700,f51979,f51561,f74193,f53191]) ).
fof(f74217,plain,
( r1_tarski(k9_relat_1(sF1282,sF1285),sF1284)
| ~ spl1288_1479
| ~ spl1288_1809 ),
inference(superposition,[],[f69048,f74195]) ).
fof(f74218,plain,
( r1_tarski(sF1286,sF1284)
| ~ spl1288_16
| ~ spl1288_1479
| ~ spl1288_1809 ),
inference(forward_demodulation,[],[f74217,f51550]) ).
fof(f74225,plain,
( spl1288_143
| ~ spl1288_16
| ~ spl1288_1479
| ~ spl1288_1809 ),
inference(avatar_split_clause,[],[f74218,f74193,f69047,f51548,f52661]) ).
cnf(s10,plain,
( ~ spl1288_13
| ~ spl1288_14
| ~ spl1288_15
| spl1288_16
| ~ spl1288_17
| ~ spl1288_18 ),
inference(sat_conversion,[],[f51565]) ).
cnf(s11,plain,
( ~ spl1288_13
| ~ spl1288_14
| ~ spl1288_15
| ~ spl1288_17
| ~ spl1288_18
| spl1288_19 ),
inference(sat_conversion,[],[f51566]) ).
cnf(s14,plain,
( spl1288_20
| ~ spl1288_22
| ~ spl1288_23
| ~ spl1288_25
| ~ spl1288_26
| spl1288_27
| spl1288_28 ),
inference(sat_conversion,[],[f51607]) ).
cnf(s16,plain,
~ spl1288_20,
inference(sat_conversion,[],[f51610]) ).
cnf(s18,plain,
spl1288_22,
inference(sat_conversion,[],[f51613]) ).
cnf(s20,plain,
spl1288_23,
inference(sat_conversion,[],[f51616]) ).
cnf(s23,plain,
( spl1288_17
| spl1288_20
| ~ spl1288_22
| ~ spl1288_23
| ~ spl1288_25
| ~ spl1288_26
| spl1288_27 ),
inference(sat_conversion,[],[f51629]) ).
cnf(s24,plain,
( ~ spl1288_22
| spl1288_31 ),
inference(sat_conversion,[],[f51635]) ).
cnf(s30,plain,
( ~ spl1288_22
| spl1288_25
| ~ spl1288_37 ),
inference(sat_conversion,[],[f51674]) ).
cnf(s32,plain,
spl1288_37,
inference(sat_conversion,[],[f51677]) ).
cnf(s36,plain,
spl1288_40,
inference(sat_conversion,[],[f51698]) ).
cnf(s37,plain,
( spl1288_13
| spl1288_20
| ~ spl1288_22
| ~ spl1288_23
| ~ spl1288_25
| ~ spl1288_26
| spl1288_27 ),
inference(sat_conversion,[],[f51700]) ).
cnf(s38,plain,
( spl1288_20
| ~ spl1288_22
| ~ spl1288_23
| ~ spl1288_25
| ~ spl1288_26
| spl1288_27
| spl1288_41 ),
inference(sat_conversion,[],[f51706]) ).
cnf(s42,plain,
spl1288_26,
inference(sat_conversion,[],[f51719]) ).
cnf(s44,plain,
~ spl1288_27,
inference(sat_conversion,[],[f51722]) ).
cnf(s45,plain,
( spl1288_15
| ~ spl1288_22 ),
inference(sat_conversion,[],[f51724]) ).
cnf(s46,plain,
( spl1288_14
| ~ spl1288_31 ),
inference(sat_conversion,[],[f51726]) ).
cnf(s56,plain,
( spl1288_20
| ~ spl1288_22
| ~ spl1288_23
| ~ spl1288_26
| spl1288_27
| ~ spl1288_37
| spl1288_55 ),
inference(sat_conversion,[],[f51800]) ).
cnf(s57,plain,
( spl1288_18
| ~ spl1288_28 ),
inference(sat_conversion,[],[f51803]) ).
cnf(s72,plain,
( ~ spl1288_19
| ~ spl1288_70
| spl1288_73 ),
inference(sat_conversion,[],[f51940]) ).
cnf(s76,plain,
( ~ spl1288_15
| spl1288_20
| ~ spl1288_40
| spl1288_76 ),
inference(sat_conversion,[],[f51983]) ).
cnf(s94,plain,
( ~ spl1288_15
| spl1288_20
| ~ spl1288_91 ),
inference(sat_conversion,[],[f52172]) ).
cnf(s98,plain,
( spl1288_20
| ~ spl1288_22
| ~ spl1288_40
| spl1288_95 ),
inference(sat_conversion,[],[f52217]) ).
cnf(s100,plain,
( spl1288_20
| ~ spl1288_22
| ~ spl1288_23
| ~ spl1288_40
| ~ spl1288_95
| spl1288_98 ),
inference(sat_conversion,[],[f52235]) ).
cnf(s110,plain,
( ~ spl1288_13
| ~ spl1288_17
| spl1288_20
| ~ spl1288_22
| ~ spl1288_23
| ~ spl1288_26
| spl1288_27
| ~ spl1288_28
| ~ spl1288_37
| ~ spl1288_41
| spl1288_110 ),
inference(sat_conversion,[],[f52335]) ).
cnf(s111,plain,
( ~ spl1288_40
| ~ spl1288_110
| spl1288_111 ),
inference(sat_conversion,[],[f52341]) ).
cnf(s127,plain,
( ~ spl1288_13
| ~ spl1288_14
| ~ spl1288_15
| ~ spl1288_17
| ~ spl1288_18
| spl1288_125 ),
inference(sat_conversion,[],[f52503]) ).
cnf(s135,plain,
( spl1288_20
| ~ spl1288_22
| ~ spl1288_23
| spl1288_133 ),
inference(sat_conversion,[],[f52564]) ).
cnf(s146,plain,
( ~ spl1288_28
| spl1288_70 ),
inference(sat_conversion,[],[f52648]) ).
cnf(s211,plain,
( spl1288_20
| ~ spl1288_22
| ~ spl1288_23
| ~ spl1288_26
| spl1288_27
| ~ spl1288_37
| spl1288_186 ),
inference(sat_conversion,[],[f53122]) ).
cnf(s218,plain,
( ~ spl1288_15
| spl1288_20
| spl1288_193 ),
inference(sat_conversion,[],[f53179]) ).
cnf(s220,plain,
( ~ spl1288_15
| ~ spl1288_40
| ~ spl1288_193
| spl1288_195 ),
inference(sat_conversion,[],[f53194]) ).
cnf(s229,plain,
( ~ spl1288_13
| ~ spl1288_18
| ~ spl1288_28
| spl1288_210 ),
inference(sat_conversion,[],[f53327]) ).
cnf(s296,plain,
( ~ spl1288_13
| ~ spl1288_17
| ~ spl1288_28
| ~ spl1288_41
| spl1288_66
| ~ spl1288_67
| ~ spl1288_186 ),
inference(sat_conversion,[],[f53977]) ).
cnf(s297,plain,
( spl1288_20
| ~ spl1288_22
| ~ spl1288_23
| ~ spl1288_25
| ~ spl1288_26
| spl1288_27
| spl1288_67 ),
inference(sat_conversion,[],[f53981]) ).
cnf(s300,plain,
( ~ spl1288_13
| ~ spl1288_17
| spl1288_20
| ~ spl1288_22
| ~ spl1288_23
| ~ spl1288_26
| spl1288_27
| ~ spl1288_28
| ~ spl1288_37
| ~ spl1288_41
| ~ spl1288_55
| ~ spl1288_66
| spl1288_288 ),
inference(sat_conversion,[],[f53999]) ).
cnf(s354,plain,
( ~ spl1288_16
| ~ spl1288_73
| ~ spl1288_98
| spl1288_142
| ~ spl1288_143 ),
inference(sat_conversion,[],[f54424]) ).
cnf(s360,plain,
~ spl1288_142,
inference(sat_conversion,[],[f54459]) ).
cnf(s718,plain,
( ~ spl1288_14
| spl1288_27
| spl1288_632 ),
inference(sat_conversion,[],[f57239]) ).
cnf(s720,plain,
( ~ spl1288_13
| ~ spl1288_15
| ~ spl1288_17
| ~ spl1288_28
| ~ spl1288_632
| spl1288_634 ),
inference(sat_conversion,[],[f57259]) ).
cnf(s724,plain,
( ~ spl1288_15
| ~ spl1288_634
| spl1288_637 ),
inference(sat_conversion,[],[f57285]) ).
cnf(s933,plain,
( ~ spl1288_13
| ~ spl1288_70
| spl1288_815 ),
inference(sat_conversion,[],[f59099]) ).
cnf(s991,plain,
( ~ spl1288_13
| ~ spl1288_17
| ~ spl1288_18
| spl1288_91
| spl1288_859 ),
inference(sat_conversion,[],[f59572]) ).
cnf(s1013,plain,
( ~ spl1288_40
| ~ spl1288_40
| ~ spl1288_110
| ~ spl1288_859
| spl1288_877 ),
inference(sat_conversion,[],[f59751]) ).
cnf(s1014,plain,
( ~ spl1288_40
| ~ spl1288_110
| ~ spl1288_859
| spl1288_877 ),
inference(rat,[],[s1013]) ).
cnf(s1015,plain,
( ~ spl1288_40
| ~ spl1288_40
| ~ spl1288_288
| ~ spl1288_859
| ~ spl1288_878
| ~ spl1288_879
| spl1288_880 ),
inference(sat_conversion,[],[f59764]) ).
cnf(s1016,plain,
( ~ spl1288_40
| ~ spl1288_288
| ~ spl1288_859
| ~ spl1288_878
| ~ spl1288_879
| spl1288_880 ),
inference(rat,[],[s1015]) ).
cnf(s1022,plain,
( ~ spl1288_40
| ~ spl1288_133
| ~ spl1288_877
| spl1288_879 ),
inference(sat_conversion,[],[f59795]) ).
cnf(s1102,plain,
( ~ spl1288_195
| ~ spl1288_210
| ~ spl1288_637
| ~ spl1288_815
| spl1288_878 ),
inference(sat_conversion,[],[f60388]) ).
cnf(s1291,plain,
( ~ spl1288_13
| ~ spl1288_70
| ~ spl1288_637
| spl1288_1077 ),
inference(sat_conversion,[],[f61702]) ).
cnf(s1927,plain,
( ~ spl1288_13
| ~ spl1288_70
| spl1288_1479 ),
inference(sat_conversion,[],[f69049]) ).
cnf(s2605,plain,
( ~ spl1288_14
| spl1288_20
| ~ spl1288_22
| ~ spl1288_23
| ~ spl1288_26
| spl1288_27
| ~ spl1288_37
| ~ spl1288_67
| ~ spl1288_125
| spl1288_1805 ),
inference(sat_conversion,[],[f74108]) ).
cnf(s2609,plain,
( ~ spl1288_40
| ~ spl1288_111
| ~ spl1288_133
| ~ spl1288_859
| ~ spl1288_878
| ~ spl1288_880
| ~ spl1288_1805
| spl1288_1806 ),
inference(sat_conversion,[],[f74154]) ).
cnf(s2613,plain,
( ~ spl1288_19
| ~ spl1288_76
| ~ spl1288_195
| ~ spl1288_1077
| ~ spl1288_1806
| spl1288_1809 ),
inference(sat_conversion,[],[f74196]) ).
cnf(s2614,plain,
( ~ spl1288_16
| spl1288_143
| ~ spl1288_1479
| ~ spl1288_1809 ),
inference(sat_conversion,[],[f74225]) ).
cnf(s2630,plain,
( ~ spl1288_16
| ~ spl1288_73
| ~ spl1288_98
| ~ spl1288_143 ),
inference(rat,[],[s354,s360]) ).
cnf(s2632,plain,
( spl1288_20
| ~ spl1288_22
| ~ spl1288_23
| ~ spl1288_25
| spl1288_41 ),
inference(rat,[],[s38,s44,s42]) ).
cnf(s2633,plain,
( spl1288_13
| spl1288_20
| ~ spl1288_22
| ~ spl1288_23
| ~ spl1288_25 ),
inference(rat,[],[s37,s44,s42]) ).
cnf(s2636,plain,
( ~ spl1288_22
| spl1288_25 ),
inference(rat,[],[s30,s32]) ).
cnf(s2637,plain,
( spl1288_17
| spl1288_20
| ~ spl1288_22
| ~ spl1288_23
| ~ spl1288_25 ),
inference(rat,[],[s23,s44,s42]) ).
cnf(s2645,plain,
spl1288_15,
inference(rat,[],[s45,s18]) ).
cnf(s2646,plain,
spl1288_25,
inference(rat,[],[s2636,s18]) ).
cnf(s2647,plain,
spl1288_31,
inference(rat,[],[s24,s18]) ).
cnf(s2670,plain,
spl1288_14,
inference(rat,[],[s46,s2647]) ).
cnf(s2681,plain,
spl1288_632,
inference(rat,[],[s718,s44,s2670]) ).
cnf(s2734,plain,
spl1288_67,
inference(rat,[],[s297,s2646,s44,s42,s18,s20,s16]) ).
cnf(s2738,plain,
spl1288_193,
inference(rat,[],[s218,s2645,s16]) ).
cnf(s2739,plain,
spl1288_186,
inference(rat,[],[s211,s18,s32,s44,s42,s20,s16]) ).
cnf(s2745,plain,
spl1288_133,
inference(rat,[],[s135,s18,s20,s16]) ).
cnf(s2761,plain,
spl1288_95,
inference(rat,[],[s98,s18,s36,s16]) ).
cnf(s2763,plain,
~ spl1288_91,
inference(rat,[],[s94,s2645,s16]) ).
cnf(s2768,plain,
spl1288_76,
inference(rat,[],[s76,s2645,s36,s16]) ).
cnf(s2777,plain,
spl1288_55,
inference(rat,[],[s56,s18,s32,s44,s42,s20,s16]) ).
cnf(s2787,plain,
spl1288_41,
inference(rat,[],[s2632,s2646,s18,s20,s16]) ).
cnf(s2788,plain,
spl1288_13,
inference(rat,[],[s2633,s2646,s20,s18,s16]) ).
cnf(s2793,plain,
spl1288_17,
inference(rat,[],[s2637,s2646,s20,s18,s16]) ).
cnf(s2810,plain,
spl1288_195,
inference(rat,[],[s220,s2645,s36,s2738]) ).
cnf(s2818,plain,
spl1288_98,
inference(rat,[],[s100,s16,s18,s36,s20,s2761]) ).
cnf(s2947,plain,
spl1288_28,
inference(rat,[],[s14,s44,s42,s2646,s20,s18,s16]) ).
cnf(s2948,plain,
spl1288_70,
inference(rat,[],[s146,s2947]) ).
cnf(s2949,plain,
spl1288_18,
inference(rat,[],[s57,s2947]) ).
cnf(s2950,plain,
spl1288_634,
inference(rat,[],[s720,s2793,s2681,s2788,s2645,s2947]) ).
cnf(s2951,plain,
spl1288_66,
inference(rat,[],[s296,s2739,s2734,s2793,s2787,s2788,s2947]) ).
cnf(s2952,plain,
spl1288_110,
inference(rat,[],[s110,s2793,s2787,s32,s2788,s44,s42,s20,s18,s16,s2947]) ).
cnf(s2953,plain,
spl1288_1479,
inference(rat,[],[s1927,s2788,s2948]) ).
cnf(s2956,plain,
spl1288_815,
inference(rat,[],[s933,s2788,s2948]) ).
cnf(s2966,plain,
spl1288_210,
inference(rat,[],[s229,s2947,s2788,s2949]) ).
cnf(s2969,plain,
spl1288_859,
inference(rat,[],[s991,s2793,s2763,s2788,s2949]) ).
cnf(s2971,plain,
spl1288_125,
inference(rat,[],[s127,s2793,s2788,s2670,s2645,s2949]) ).
cnf(s2974,plain,
spl1288_637,
inference(rat,[],[s724,s2645,s2950]) ).
cnf(s2977,plain,
spl1288_288,
inference(rat,[],[s300,s2947,s2793,s2777,s2787,s32,s2788,s44,s42,s20,s18,s16,s2951]) ).
cnf(s2978,plain,
spl1288_111,
inference(rat,[],[s111,s36,s2952]) ).
cnf(s2984,plain,
spl1288_877,
inference(rat,[],[s1014,s2952,s36,s2969]) ).
cnf(s2990,plain,
spl1288_1805,
inference(rat,[],[s2605,s2734,s16,s2670,s32,s44,s42,s20,s18,s2971]) ).
cnf(s3012,plain,
spl1288_1077,
inference(rat,[],[s1291,s2948,s2788,s2974]) ).
cnf(s3013,plain,
spl1288_878,
inference(rat,[],[s1102,s2966,s2956,s2810,s2974]) ).
cnf(s3018,plain,
spl1288_879,
inference(rat,[],[s1022,s2745,s36,s2984]) ).
cnf(s3050,plain,
spl1288_880,
inference(rat,[],[s1016,s3013,s2977,s2969,s36,s3018]) ).
cnf(s3064,plain,
spl1288_1806,
inference(rat,[],[s2609,s3013,s2990,s2978,s2969,s2745,s36,s3050]) ).
cnf(s3070,plain,
spl1288_19,
inference(rat,[],[s11,s2949,s2793,s2645,s2670,s2788]) ).
cnf(s3071,plain,
spl1288_1809,
inference(rat,[],[s2613,s3064,s3012,s2768,s2810,s3070]) ).
cnf(s3079,plain,
spl1288_73,
inference(rat,[],[s72,s2948,s3070]) ).
cnf(s3084,plain,
spl1288_16,
inference(rat,[],[s10,s2949,s2793,s2645,s2670,s2788]) ).
cnf(s3085,plain,
spl1288_143,
inference(rat,[],[s2614,s3071,s2953,s3084]) ).
cnf(s3091,plain,
$false,
inference(rat,[],[s2630,s3079,s2818,s3085,s3084]) ).
fof(f74226,plain,
$false,
inference(avatar_sat_refutation,[],[s3091]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP036+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.20 % Computer : n011.cluster.edu
% 0.06/0.20 % Model : x86_64 x86_64
% 0.06/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.20 % Memory : 8046.5625MB
% 0.06/0.20 % OS : Linux 6.8.0-71-generic
% 0.06/0.20 % CPULimit : 300
% 0.06/0.20 % WCLimit : 300
% 0.06/0.20 % DateTime : Mon Sep 28 18:59:10 UTC 2026
% 0.06/0.21 % CPUTime :
% 0.06/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.24 Running first-order theorem proving
% 0.06/0.24 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
% 15.77/3.43 % (3662978)Detected formulas, will run a generic FOF schedule.
% 15.77/3.43 % (3662987)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=645094810:i=119:av=off:ss=axioms_2991 on theBenchmark for (2991ds/119Mi)
% 15.77/3.43 % (3662983)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=723274540:i=141193_2991 on theBenchmark for (2991ds/141193Mi)
% 15.77/3.43 % (3662988)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1650660860:s2a=on:i=139:gtg=position_2991 on theBenchmark for (2991ds/139Mi)
% 15.77/3.43 % (3662984)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=1981988948:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2991 on theBenchmark for (2991ds/134677Mi)
% 15.77/3.43 % (3662985)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=1841140931:i=141695:sd=1:nm=32:gsp=on:ss=included_2991 on theBenchmark for (2991ds/141695Mi)
% 15.77/3.43 % (3662986)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4098131857:i=109:sd=1:ins=1:gsp=on:ss=axioms_2991 on theBenchmark for (2991ds/109Mi)
% 15.77/3.43 % (3662989)dis-21_1_sil=8000:lcm=predicate:random_seed=4228614906:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2991 on theBenchmark for (2991ds/129Mi)
% 15.77/3.43 % (3662988)Instruction limit reached!
% 15.77/3.43 % (3662988)------------------------------
% 15.77/3.43 % (3662988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.77/3.43 % (3662988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.77/3.43 % (3662988)CaDiCaL version: 2.1.3
% 15.77/3.43 % (3662988)Termination reason: Instruction limit
% 15.77/3.43 % (3662988)Termination phase: Property scanning
% 15.77/3.43 % (3662988)Time elapsed: 0.062 s
% 15.77/3.43 % (3662988)Peak memory usage: 136 MB
% 15.77/3.43 % (3662988)Instructions burned: 139 (million)
% 15.77/3.43 % (3662989)Instruction limit reached!
% 15.77/3.43 % (3662989)------------------------------
% 15.77/3.43 % (3662989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.77/3.43 % (3662989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.77/3.43 % (3662989)CaDiCaL version: 2.1.3
% 15.77/3.43 % (3662989)Termination reason: Instruction limit
% 15.77/3.43 % (3662989)Termination phase: SInE selection
% 15.77/3.43 % (3662989)Time elapsed: 0.065 s
% 15.77/3.43 % (3662989)Peak memory usage: 136 MB
% 15.77/3.43 % (3662989)Instructions burned: 129 (million)
% 15.77/3.43 % (3662986)Instruction limit reached!
% 15.77/3.43 % (3662986)------------------------------
% 15.77/3.43 % (3662986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.77/3.43 % (3662986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.77/3.43 % (3662986)CaDiCaL version: 2.1.3
% 15.77/3.43 % (3662986)Termination reason: Instruction limit
% 15.77/3.43 % (3662986)Termination phase: SInE selection
% 15.77/3.43 % (3662986)Time elapsed: 0.079 s
% 15.77/3.43 % (3662986)Peak memory usage: 135 MB
% 15.77/3.43 % (3662986)Instructions burned: 109 (million)
% 15.77/3.43 % (3662987)Instruction limit reached!
% 15.77/3.43 % (3662987)------------------------------
% 15.77/3.43 % (3662987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.77/3.43 % (3662987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.77/3.43 % (3662987)CaDiCaL version: 2.1.3
% 15.77/3.43 % (3662987)Termination reason: Instruction limit
% 15.77/3.43 % (3662987)Termination phase: SInE selection
% 15.77/3.43 % (3662987)Time elapsed: 0.085 s
% 15.77/3.43 % (3662987)Peak memory usage: 135 MB
% 15.77/3.43 % (3662987)Instructions burned: 119 (million)
% 15.77/3.43 % (3662998)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2857900079:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/157Mi)
% 15.77/3.43 % (3662997)lrs+10_1_sil=8000:sp=occurrence:random_seed=1861082228:i=285:sd=3:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/285Mi)
% 15.77/3.43 % (3662998)Instruction limit reached!
% 15.77/3.43 % (3662998)------------------------------
% 15.77/3.43 % (3662998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.77/3.43 % (3662998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.77/3.43 % (3662998)CaDiCaL version: 2.1.3
% 15.77/3.43 % (3662998)Termination reason: Instruction limit
% 22.79/4.50 % (3662998)Termination phase: Property scanning
% 22.79/4.50 % (3662998)Time elapsed: 0.038 s
% 22.79/4.50 % (3662998)Peak memory usage: 136 MB
% 22.79/4.50 % (3662998)Instructions burned: 157 (million)
% 22.79/4.50 % (3662999)lrs+1011_1_sil=32000:sp=occurrence:random_seed=201356591:i=325:sd=1:ss=axioms:sgt=32_2988 on theBenchmark for (2988ds/325Mi)
% 22.79/4.50 % (3663000)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=3906469081:s2a=on:i=248:s2at=1.23:gtg=position_2988 on theBenchmark for (2988ds/248Mi)
% 22.79/4.50 % (3663003)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2555838750:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2987 on theBenchmark for (2987ds/294Mi)
% 22.79/4.50 % (3663000)Instruction limit reached!
% 22.79/4.50 % (3663000)------------------------------
% 22.79/4.50 % (3663000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.79/4.50 % (3663000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.79/4.50 % (3663000)CaDiCaL version: 2.1.3
% 22.79/4.50 % (3663000)Termination reason: Instruction limit
% 22.79/4.50 % (3663000)Termination phase: Property scanning
% 22.79/4.50 % (3663000)Time elapsed: 0.107 s
% 22.79/4.50 % (3663000)Peak memory usage: 136 MB
% 22.79/4.50 % (3663000)Instructions burned: 248 (million)
% 22.79/4.50 % (3662997)Instruction limit reached!
% 22.79/4.50 % (3662997)------------------------------
% 22.79/4.50 % (3662997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.79/4.50 % (3662997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.79/4.50 % (3662997)CaDiCaL version: 2.1.3
% 22.79/4.50 % (3662997)Termination reason: Instruction limit
% 22.79/4.50 % (3662997)Termination phase: Preprocessing 3
% 22.79/4.50 % (3662997)Time elapsed: 0.230 s
% 22.79/4.50 % (3662997)Peak memory usage: 140 MB
% 22.79/4.50 % (3662997)Instructions burned: 286 (million)
% 22.79/4.50 % (3663003)Instruction limit reached!
% 22.79/4.50 % (3663003)------------------------------
% 22.79/4.50 % (3663003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.79/4.50 % (3663003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.79/4.50 % (3663003)CaDiCaL version: 2.1.3
% 22.79/4.50 % (3663003)Termination reason: Instruction limit
% 22.79/4.50 % (3663003)Termination phase: SInE selection
% 22.79/4.50 % (3663003)Time elapsed: 0.104 s
% 22.79/4.50 % (3663003)Peak memory usage: 136 MB
% 22.79/4.50 % (3663003)Instructions burned: 295 (million)
% 22.79/4.50 % (3662999)Instruction limit reached!
% 22.79/4.50 % (3662999)------------------------------
% 22.79/4.50 % (3662999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.79/4.50 % (3662999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.79/4.50 % (3662999)CaDiCaL version: 2.1.3
% 22.79/4.50 % (3662999)Termination reason: Instruction limit
% 22.79/4.50 % (3662999)Termination phase: Saturation
% 22.79/4.50 % (3662999)Time elapsed: 0.250 s
% 22.79/4.50 % (3662999)Peak memory usage: 142 MB
% 22.79/4.50 % (3662999)Instructions burned: 326 (million)
% 22.79/4.50 % (3663007)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=450093413:i=2350_2986 on theBenchmark for (2986ds/2350Mi)
% 22.79/4.50 % (3663009)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2301814431:i=127:av=off:fsr=off:sup=off_2985 on theBenchmark for (2985ds/127Mi)
% 22.79/4.50 % (3663008)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1604033510:cts=off:i=113:fsr=off:ss=included:sgt=4_2985 on theBenchmark for (2985ds/113Mi)
% 22.79/4.50 % (3663009)Instruction limit reached!
% 22.79/4.50 % (3663009)------------------------------
% 22.79/4.50 % (3663009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.79/4.50 % (3663009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.79/4.50 % (3663009)CaDiCaL version: 2.1.3
% 22.79/4.50 % (3663009)Termination reason: Instruction limit
% 22.79/4.50 % (3663009)Termination phase: Preprocessing 1
% 22.79/4.50 % (3663009)Time elapsed: 0.058 s
% 22.79/4.50 % (3663009)Peak memory usage: 137 MB
% 22.79/4.50 % (3663009)Instructions burned: 128 (million)
% 22.79/4.50 % (3663010)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2690106610:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2984 on theBenchmark for (2984ds/114Mi)
% 22.79/4.50 % (3663008)Instruction limit reached!
% 22.79/4.50 % (3663008)------------------------------
% 22.79/4.50 % (3663008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.86/10.34 % (3663008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.86/10.34 % (3663008)CaDiCaL version: 2.1.3
% 64.86/10.34 % (3663008)Termination reason: Instruction limit
% 64.86/10.34 % (3663008)Termination phase: SInE selection
% 64.86/10.34 % (3663008)Time elapsed: 0.086 s
% 64.86/10.34 % (3663008)Peak memory usage: 136 MB
% 64.86/10.34 % (3663008)Instructions burned: 113 (million)
% 64.86/10.34 % (3663010)Instruction limit reached!
% 64.86/10.34 % (3663010)------------------------------
% 64.86/10.34 % (3663010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.86/10.34 % (3663010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.86/10.34 % (3663010)CaDiCaL version: 2.1.3
% 64.86/10.34 % (3663010)Termination reason: Instruction limit
% 64.86/10.34 % (3663010)Termination phase: Property scanning
% 64.86/10.34 % (3663010)Time elapsed: 0.052 s
% 64.86/10.34 % (3663010)Peak memory usage: 136 MB
% 64.86/10.34 % (3663010)Instructions burned: 114 (million)
% 64.86/10.34 % (3663014)lrs+10_1_sil=8000:sp=occurrence:random_seed=757654613:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2983 on theBenchmark for (2983ds/907Mi)
% 64.86/10.34 % (3663016)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1248751260:i=437:sd=1:aac=none:ss=included_2982 on theBenchmark for (2982ds/437Mi)
% 64.86/10.34 % (3663017)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2451803019:i=5202:ss=axioms:sgt=16_2982 on theBenchmark for (2982ds/5202Mi)
% 64.86/10.34 % (3663014)Instruction limit reached!
% 64.86/10.34 % (3663014)------------------------------
% 64.86/10.34 % (3663014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.86/10.34 % (3663014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.86/10.34 % (3663014)CaDiCaL version: 2.1.3
% 64.86/10.34 % (3663014)Termination reason: Instruction limit
% 64.86/10.34 % (3663014)Termination phase: Property scanning
% 64.86/10.34 % (3663014)Time elapsed: 0.353 s
% 64.86/10.34 % (3663014)Peak memory usage: 158 MB
% 64.86/10.34 % (3663014)Instructions burned: 908 (million)
% 64.86/10.34 % (3663016)Instruction limit reached!
% 64.86/10.34 % (3663016)------------------------------
% 64.86/10.34 % (3663016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.86/10.34 % (3663016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.86/10.34 % (3663016)CaDiCaL version: 2.1.3
% 64.86/10.34 % (3663016)Termination reason: Instruction limit
% 64.86/10.34 % (3663016)Termination phase: Saturation
% 64.86/10.34 % (3663016)Time elapsed: 0.306 s
% 64.86/10.34 % (3663016)Peak memory usage: 144 MB
% 64.86/10.34 % (3663016)Instructions burned: 438 (million)
% 64.86/10.34 % (3663021)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=770340445:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2978 on theBenchmark for (2978ds/134Mi)
% 64.86/10.34 % (3663022)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=148884533:st=8:i=592:sd=3:ep=RST:ss=axioms_2978 on theBenchmark for (2978ds/592Mi)
% 64.86/10.34 % (3663021)Instruction limit reached!
% 64.86/10.34 % (3663021)------------------------------
% 64.86/10.34 % (3663021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.86/10.34 % (3663021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.86/10.34 % (3663021)CaDiCaL version: 2.1.3
% 64.86/10.34 % (3663021)Termination reason: Instruction limit
% 64.86/10.34 % (3663021)Termination phase: SInE selection
% 64.86/10.34 % (3663021)Time elapsed: 0.104 s
% 64.86/10.34 % (3663021)Peak memory usage: 136 MB
% 64.86/10.34 % (3663021)Instructions burned: 135 (million)
% 64.86/10.34 % (3663025)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=682311928:st=3:i=13193:sd=3:ss=axioms_2975 on theBenchmark for (2975ds/13193Mi)
% 64.86/10.34 % (3663022)Instruction limit reached!
% 64.86/10.34 % (3663022)------------------------------
% 64.86/10.34 % (3663022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.86/10.34 % (3663022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.86/10.34 % (3663022)CaDiCaL version: 2.1.3
% 64.86/10.34 % (3663022)Termination reason: Instruction limit
% 64.86/10.34 % (3663022)Termination phase: Preprocessing 2
% 64.86/10.34 % (3663022)Time elapsed: 0.463 s
% 64.86/10.34 % (3663022)Peak memory usage: 142 MB
% 64.86/10.34 % (3663022)Instructions burned: 592 (million)
% 64.86/10.34 % (3663027)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=2670696942:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2971 on theBenchmark for (2971ds/125Mi)
% 95.40/14.67 % (3663027)Instruction limit reached!
% 95.40/14.67 % (3663027)------------------------------
% 95.40/14.67 % (3663027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.40/14.67 % (3663027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.40/14.67 % (3663027)CaDiCaL version: 2.1.3
% 95.40/14.67 % (3663027)Termination reason: Instruction limit
% 95.40/14.67 % (3663027)Termination phase: Property scanning
% 95.40/14.67 % (3663027)Time elapsed: 0.057 s
% 95.40/14.67 % (3663027)Peak memory usage: 136 MB
% 95.40/14.67 % (3663027)Instructions burned: 127 (million)
% 95.40/14.67 % (3663007)Instruction limit reached!
% 95.40/14.67 % (3663007)------------------------------
% 95.40/14.67 % (3663007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.40/14.67 % (3663007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.40/14.67 % (3663007)CaDiCaL version: 2.1.3
% 95.40/14.67 % (3663007)Termination reason: Instruction limit
% 95.40/14.67 % (3663007)Termination phase: Property scanning
% 95.40/14.67 % (3663007)Time elapsed: 1.499 s
% 95.40/14.67 % (3663007)Peak memory usage: 232 MB
% 95.40/14.67 % (3663007)Instructions burned: 2351 (million)
% 95.40/14.67 % (3663029)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=150145459:i=134:gtgl=5:slsql=off:gtg=exists_sym_2969 on theBenchmark for (2969ds/134Mi)
% 95.40/14.67 % (3663030)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2609503878:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/141Mi)
% 95.40/14.67 % (3663029)Instruction limit reached!
% 95.40/14.67 % (3663029)------------------------------
% 95.40/14.67 % (3663029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.40/14.67 % (3663029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.40/14.67 % (3663029)CaDiCaL version: 2.1.3
% 95.40/14.67 % (3663029)Termination reason: Instruction limit
% 95.40/14.67 % (3663029)Termination phase: Property scanning
% 95.40/14.67 % (3663029)Time elapsed: 0.061 s
% 95.40/14.67 % (3663029)Peak memory usage: 136 MB
% 95.40/14.67 % (3663029)Instructions burned: 135 (million)
% 95.40/14.67 % (3663030)Instruction limit reached!
% 95.40/14.67 % (3663030)------------------------------
% 95.40/14.67 % (3663030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.40/14.67 % (3663030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.40/14.67 % (3663030)CaDiCaL version: 2.1.3
% 95.40/14.67 % (3663030)Termination reason: Instruction limit
% 95.40/14.67 % (3663030)Termination phase: SInE selection
% 95.40/14.67 % (3663030)Time elapsed: 0.109 s
% 95.40/14.67 % (3663030)Peak memory usage: 136 MB
% 95.40/14.67 % (3663030)Instructions burned: 141 (million)
% 95.40/14.67 % (3663033)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1518159569:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2967 on theBenchmark for (2967ds/431Mi)
% 95.40/14.67 % (3663034)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=1970459325:i=6060:aac=none:ins=25_2966 on theBenchmark for (2966ds/6060Mi)
% 95.40/14.67 % (3663033)Instruction limit reached!
% 95.40/14.67 % (3663033)------------------------------
% 95.40/14.67 % (3663033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.40/14.67 % (3663033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.40/14.67 % (3663033)CaDiCaL version: 2.1.3
% 95.40/14.67 % (3663033)Termination reason: Instruction limit
% 95.40/14.67 % (3663033)Termination phase: Saturation
% 95.40/14.67 % (3663033)Time elapsed: 0.312 s
% 95.40/14.67 % (3663033)Peak memory usage: 143 MB
% 95.40/14.67 % (3663033)Instructions burned: 431 (million)
% 95.40/14.67 % (3663037)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=1196361464:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2962 on theBenchmark for (2962ds/150Mi)
% 95.40/14.67 % (3663037)Instruction limit reached!
% 95.40/14.67 % (3663037)------------------------------
% 95.40/14.67 % (3663037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.40/14.67 % (3663037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.40/14.67 % (3663037)CaDiCaL version: 2.1.3
% 95.40/14.67 % (3663037)Termination reason: Instruction limit
% 127.77/19.23 % (3663037)Termination phase: SInE selection
% 127.77/19.23 % (3663037)Time elapsed: 0.119 s
% 127.77/19.23 % (3663037)Peak memory usage: 136 MB
% 127.77/19.23 % (3663037)Instructions burned: 150 (million)
% 127.77/19.23 % (3663039)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1173145571:i=14155:bd=all_2959 on theBenchmark for (2959ds/14155Mi)
% 127.77/19.23 % (3663017)Instruction limit reached!
% 127.77/19.23 % (3663017)------------------------------
% 127.77/19.23 % (3663017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.77/19.23 % (3663017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.77/19.23 % (3663017)CaDiCaL version: 2.1.3
% 127.77/19.23 % (3663017)Termination reason: Instruction limit
% 127.77/19.23 % (3663017)Termination phase: Saturation
% 127.77/19.23 % (3663017)Time elapsed: 3.911 s
% 127.77/19.23 % (3663017)Peak memory usage: 620 MB
% 127.77/19.23 % (3663017)Instructions burned: 5202 (million)
% 127.77/19.23 % (3663042)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2584120846:i=667:av=off:fsr=off_2941 on theBenchmark for (2941ds/667Mi)
% 127.77/19.23 % (3663042)Instruction limit reached!
% 127.77/19.23 % (3663042)------------------------------
% 127.77/19.23 % (3663042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.77/19.23 % (3663042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.77/19.23 % (3663042)CaDiCaL version: 2.1.3
% 127.77/19.23 % (3663042)Termination reason: Instruction limit
% 127.77/19.23 % (3663042)Termination phase: NewCNF
% 127.77/19.23 % (3663042)Time elapsed: 0.551 s
% 127.77/19.23 % (3663042)Peak memory usage: 185 MB
% 127.77/19.23 % (3663042)Instructions burned: 667 (million)
% 127.77/19.23 % (3663044)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=1923913872:s2a=on:i=185:s2at=1.8:fdi=4_2933 on theBenchmark for (2933ds/185Mi)
% 127.77/19.23 % (3663044)Instruction limit reached!
% 127.77/19.23 % (3663044)------------------------------
% 127.77/19.23 % (3663044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.77/19.23 % (3663044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.77/19.23 % (3663044)CaDiCaL version: 2.1.3
% 127.77/19.23 % (3663044)Termination reason: Instruction limit
% 127.77/19.23 % (3663044)Termination phase: SInE selection
% 127.77/19.23 % (3663044)Time elapsed: 0.132 s
% 127.77/19.23 % (3663044)Peak memory usage: 136 MB
% 127.77/19.23 % (3663044)Instructions burned: 186 (million)
% 127.77/19.23 % (3663046)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2075588993:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2930 on theBenchmark for (2930ds/193Mi)
% 127.77/19.23 % (3663046)Instruction limit reached!
% 127.77/19.23 % (3663046)------------------------------
% 127.77/19.23 % (3663046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.77/19.23 % (3663046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.77/19.23 % (3663046)CaDiCaL version: 2.1.3
% 127.77/19.23 % (3663046)Termination reason: Instruction limit
% 127.77/19.23 % (3663046)Termination phase: SInE selection
% 127.77/19.23 % (3663046)Time elapsed: 0.155 s
% 127.77/19.23 % (3663046)Peak memory usage: 136 MB
% 127.77/19.23 % (3663046)Instructions burned: 196 (million)
% 127.77/19.23 % (3663034)Instruction limit reached!
% 127.77/19.23 % (3663034)------------------------------
% 127.77/19.23 % (3663034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.77/19.23 % (3663034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.77/19.23 % (3663034)CaDiCaL version: 2.1.3
% 127.77/19.23 % (3663034)Termination reason: Instruction limit
% 127.77/19.23 % (3663034)Termination phase: Function definition elimination
% 127.77/19.23 % (3663034)Time elapsed: 3.804 s
% 127.77/19.23 % (3663034)Peak memory usage: 244 MB
% 127.77/19.23 % (3663034)Instructions burned: 6061 (million)
% 127.77/19.23 % (3663048)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3093307199:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2927 on theBenchmark for (2927ds/4850Mi)
% 127.77/19.23 % (3663049)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3410505554:i=12111:sd=1:ss=included_2926 on theBenchmark for (2926ds/12111Mi)
% 127.77/19.23 % (3663048)Instruction limit reached!
% 127.77/19.23 % (3663048)------------------------------
% 127.77/19.23 % (3663048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.62/22.88 % (3663048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.62/22.88 % (3663048)CaDiCaL version: 2.1.3
% 105.62/22.88 % (3663048)Termination reason: Instruction limit
% 105.62/22.88 % (3663048)Termination phase: Property scanning
% 105.62/22.88 % (3663048)Time elapsed: 2.460 s
% 105.62/22.88 % (3663048)Peak memory usage: 217 MB
% 105.62/22.88 % (3663048)Instructions burned: 4852 (million)
% 105.62/22.88 % (3663052)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4266667270:i=319:kws=precedence:fsr=off_2900 on theBenchmark for (2900ds/319Mi)
% 105.62/22.88 % (3663052)Instruction limit reached!
% 105.62/22.88 % (3663052)------------------------------
% 105.62/22.88 % (3663052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.62/22.88 % (3663052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.62/22.88 % (3663052)CaDiCaL version: 2.1.3
% 105.62/22.88 % (3663052)Termination reason: Instruction limit
% 105.62/22.88 % (3663052)Termination phase: Unused predicate definition removal
% 105.62/22.88 % (3663052)Time elapsed: 0.261 s
% 105.62/22.88 % (3663052)Peak memory usage: 142 MB
% 105.62/22.88 % (3663052)Instructions burned: 319 (million)
% 105.62/22.88 % (3663054)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=4093975067:i=2064:ep=RST_2896 on theBenchmark for (2896ds/2064Mi)
% 105.62/22.88 % (3663025)Instruction limit reached!
% 105.62/22.88 % (3663025)------------------------------
% 105.62/22.88 % (3663025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.62/22.88 % (3663025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.62/22.88 % (3663025)CaDiCaL version: 2.1.3
% 105.62/22.88 % (3663025)Termination reason: Instruction limit
% 105.62/22.88 % (3663025)Termination phase: Saturation
% 105.62/22.88 % (3663025)Time elapsed: 8.090 s
% 105.62/22.88 % (3663025)Peak memory usage: 407 MB
% 105.62/22.88 % (3663025)Instructions burned: 13194 (million)
% 105.62/22.88 % (3663056)dis-1011_128_sil=32000:random_seed=1876851614:i=3706:ep=RST:av=off_2892 on theBenchmark for (2892ds/3706Mi)
% 105.62/22.88 % (3663054)Instruction limit reached!
% 105.62/22.88 % (3663054)------------------------------
% 105.62/22.88 % (3663054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.62/22.88 % (3663054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.62/22.88 % (3663054)CaDiCaL version: 2.1.3
% 105.62/22.88 % (3663054)Termination reason: Instruction limit
% 105.62/22.88 % (3663054)Termination phase: Property scanning
% 105.62/22.88 % (3663054)Time elapsed: 1.318 s
% 105.62/22.88 % (3663054)Peak memory usage: 231 MB
% 105.62/22.88 % (3663054)Instructions burned: 2065 (million)
% 105.62/22.88 % (3663058)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=711388107:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2880 on theBenchmark for (2880ds/757Mi)
% 105.62/22.88 % (3663058)Instruction limit reached!
% 105.62/22.88 % (3663058)------------------------------
% 105.62/22.88 % (3663058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.62/22.88 % (3663058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.62/22.88 % (3663058)CaDiCaL version: 2.1.3
% 105.62/22.88 % (3663058)Termination reason: Instruction limit
% 105.62/22.88 % (3663058)Termination phase: Saturation
% 105.62/22.88 % (3663058)Time elapsed: 0.516 s
% 105.62/22.88 % (3663058)Peak memory usage: 148 MB
% 105.62/22.88 % (3663058)Instructions burned: 758 (million)
% 105.62/22.88 % (3663060)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3450657193:i=13913:ss=axioms:sgt=8_2873 on theBenchmark for (2873ds/13913Mi)
% 105.62/22.88 % (3663056)Instruction limit reached!
% 105.62/22.88 % (3663056)------------------------------
% 105.62/22.88 % (3663056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.62/22.88 % (3663056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.62/22.88 % (3663056)CaDiCaL version: 2.1.3
% 105.62/22.88 % (3663056)Termination reason: Instruction limit
% 105.62/22.88 % (3663056)Termination phase: Function definition elimination
% 105.62/22.88 % (3663056)Time elapsed: 2.046 s
% 105.62/22.88 % (3663056)Peak memory usage: 241 MB
% 105.62/22.88 % (3663056)Instructions burned: 3706 (million)
% 105.62/22.88 % (3663062)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=896493564:i=9925:aac=none_2870 on theBenchmark for (2870ds/9925Mi)
% 105.62/22.88 % (3663039)Instruction limit reached!
% 105.62/22.88 % (3663039)------------------------------
% 105.62/22.88 % (3663039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.62/22.88 % (3663039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.62/22.88 % (3663039)CaDiCaL version: 2.1.3
% 105.62/22.88 % (3663039)Termination reason: Instruction limit
% 105.62/22.88 % (3663039)Termination phase: Saturation
% 105.62/22.88 % (3663039)Time elapsed: 9.986 s
% 105.62/22.88 % (3663039)Peak memory usage: 1279 MB
% 105.62/22.88 % (3663039)Instructions burned: 14158 (million)
% 105.62/22.88 % (3663064)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3556302206:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2856 on theBenchmark for (2856ds/2479Mi)
% 105.62/22.88 % (3663064)Instruction limit reached!
% 105.62/22.88 % (3663064)------------------------------
% 105.62/22.88 % (3663064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.62/22.88 % (3663064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.62/22.88 % (3663064)CaDiCaL version: 2.1.3
% 105.62/22.88 % (3663064)Termination reason: Instruction limit
% 105.62/22.88 % (3663064)Termination phase: Saturation
% 105.62/22.88 % (3663064)Time elapsed: 1.441 s
% 105.62/22.88 % (3663064)Peak memory usage: 156 MB
% 105.62/22.88 % (3663064)Instructions burned: 2480 (million)
% 105.62/22.88 % (3663066)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=733684123:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2840 on theBenchmark for (2840ds/440Mi)
% 105.62/22.88 % (3663066)Instruction limit reached!
% 105.62/22.88 % (3663066)------------------------------
% 105.62/22.88 % (3663066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.62/22.88 % (3663066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.62/22.88 % (3663066)CaDiCaL version: 2.1.3
% 105.62/22.88 % (3663066)Termination reason: Instruction limit
% 105.62/22.88 % (3663066)Termination phase: Property scanning
% 105.62/22.88 % (3663066)Time elapsed: 0.185 s
% 105.62/22.88 % (3663066)Peak memory usage: 136 MB
% 105.62/22.88 % (3663066)Instructions burned: 440 (million)
% 105.62/22.88 % (3663068)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=4047287532:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2836 on theBenchmark for (2836ds/11145Mi)
% 105.62/22.88 % (3663049)Instruction limit reached!
% 105.62/22.88 % (3663049)------------------------------
% 105.62/22.88 % (3663049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.62/22.88 % (3663049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.62/22.88 % (3663049)CaDiCaL version: 2.1.3
% 105.62/22.88 % (3663049)Termination reason: Instruction limit
% 105.62/22.88 % (3663049)Termination phase: Saturation
% 105.62/22.88 % (3663049)Time elapsed: 9.128 s
% 105.62/22.88 % (3663049)Peak memory usage: 264 MB
% 105.62/22.88 % (3663049)Instructions burned: 12112 (million)
% 105.62/22.88 % (3663070)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=2206615245:cts=off:i=3034:av=off:er=known:fsd=on_2833 on theBenchmark for (2833ds/3034Mi)
% 105.62/22.88 % (3663062)Instruction limit reached!
% 105.62/22.88 % (3663062)------------------------------
% 105.62/22.88 % (3663062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.62/22.88 % (3663062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.62/22.88 % (3663062)CaDiCaL version: 2.1.3
% 105.62/22.88 % (3663062)Termination reason: Instruction limit
% 105.62/22.88 % (3663062)Termination phase: Saturation
% 105.62/22.88 % (3663062)Time elapsed: 5.431 s
% 105.62/22.88 % (3663062)Peak memory usage: 660 MB
% 105.62/22.88 % (3663062)Instructions burned: 9925 (million)
% 105.62/22.88 % (3663070)Instruction limit reached!
% 105.62/22.88 % (3663070)------------------------------
% 105.62/22.88 % (3663070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.62/22.88 % (3663070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.62/22.88 % (3663070)CaDiCaL version: 2.1.3
% 105.62/22.88 % (3663070)Termination reason: Instruction limit
% 105.62/22.88 % (3663070)Termination phase: Property scanning
% 105.62/22.88 % (3663070)Time elapsed: 1.747 s
% 105.62/22.88 % (3663070)Peak memory usage: 232 MB
% 105.62/22.88 % (3663070)Instructions burned: 3034 (million)
% 105.62/22.88 % (3663072)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1291528195:st=2:s2a=on:i=524:s2at=2:ss=axioms_2813 on theBenchmark for (2813ds/524Mi)
% 105.62/22.88 % (3663073)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=880464423:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2813 on theBenchmark for (2813ds/1016Mi)
% 105.62/22.88 % (3663072)Instruction limit reached!
% 105.62/22.88 % (3663072)------------------------------
% 105.62/22.88 % (3663072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.62/22.88 % (3663072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.62/22.88 % (3663072)CaDiCaL version: 2.1.3
% 105.62/22.88 % (3663072)Termination reason: Instruction limit
% 105.62/22.88 % (3663072)Termination phase: SInE selection
% 105.62/22.88 % (3663072)Time elapsed: 0.383 s
% 105.62/22.88 % (3663072)Peak memory usage: 137 MB
% 105.62/22.88 % (3663072)Instructions burned: 525 (million)
% 105.62/22.88 % (3663076)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2931890437:i=14123:bd=preordered:ins=4_2808 on theBenchmark for (2808ds/14123Mi)
% 105.62/22.88 % (3663073)Instruction limit reached!
% 105.62/22.88 % (3663073)------------------------------
% 105.62/22.88 % (3663073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.62/22.88 % (3663073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.62/22.88 % (3663073)CaDiCaL version: 2.1.3
% 105.62/22.88 % (3663073)Termination reason: Instruction limit
% 105.62/22.88 % (3663073)Termination phase: Saturation
% 105.62/22.88 % (3663073)Time elapsed: 0.645 s
% 105.62/22.88 % (3663073)Peak memory usage: 147 MB
% 105.62/22.88 % (3663073)Instructions burned: 1018 (million)
% 105.62/22.88 % (3663078)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3941489806:i=5781:kws=precedence:bd=all:rawr=on_2805 on theBenchmark for (2805ds/5781Mi)
% 105.62/22.88 % (3663060)Instruction limit reached!
% 105.62/22.88 % (3663060)------------------------------
% 105.62/22.88 % (3663060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.62/22.88 % (3663060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.62/22.88 % (3663060)CaDiCaL version: 2.1.3
% 105.62/22.88 % (3663060)Termination reason: Instruction limit
% 105.62/22.88 % (3663060)Termination phase: Saturation
% 105.62/22.88 % (3663060)Time elapsed: 8.536 s
% 105.62/22.88 % (3663060)Peak memory usage: 297 MB
% 105.62/22.88 % (3663060)Instructions burned: 13913 (million)
% 105.62/22.88 % (3663080)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=1243437424:i=2448:gtgl=5:bd=preordered:gtg=all_2786 on theBenchmark for (2786ds/2448Mi)
% 105.62/22.88 % (3663068)First to succeed.
% 105.62/22.88 % (3663068)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3662978"
% 105.62/22.88 % (3663068)Refutation found. Thanks to Tanya!
% 105.62/22.88 % SZS status Theorem for theBenchmark
% 105.62/22.88 % SZS output start Proof for theBenchmark
% See solution above
% 153.40/23.10 % (3663068)------------------------------
% 153.40/23.10 % (3663068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.40/23.10 % (3663068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.40/23.10 % (3663068)CaDiCaL version: 2.1.3
% 153.40/23.10 % (3663068)Termination reason: Refutation
% 153.40/23.10 % (3663068)Time elapsed: 5.465 s
% 153.40/23.10 % (3663068)Peak memory usage: 292 MB
% 153.40/23.10 % (3663068)Instructions burned: 8174 (million)
% 153.40/23.10 % (3663068)------------------------------
% 153.40/23.10 % (3663068)------------------------------
% 153.40/23.10 % (3662978)Success in time 22.449 s
% 153.40/23.10 % Vampire exiting
%------------------------------------------------------------------------------