%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT363+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n009.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 11:47:21 AM UTC 2026
% Result : Theorem 3.20s 1.36s
% Output : Refutation 4.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 37
% Syntax : Number of formulae : 355 ( 34 unt; 24 def)
% Number of atoms : 1783 ( 45 equ)
% Maximal formula atoms : 17 ( 5 avg)
% Number of connectives : 2617 (1189 ~;1240 |; 124 &)
% ( 33 <=>; 29 =>; 0 <=; 2 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 39 ( 37 usr; 25 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 3 con; 0-4 aty)
% Number of variables : 244 ( 0 sgn 228 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_pre_topc(X1)
& l1_pre_topc(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)) )
=> ( v2_waybel34(X2,X0,X1)
<=> v1_t_0topsp(k8_waybel18(X0,X1,X2),X0,k7_waybel18(X0,X1,X2)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t26_waybel34) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_pre_topc(X1)
& l1_pre_topc(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)) )
=> ( v2_waybel34(X2,X0,X1)
<=> v1_t_0topsp(k8_waybel18(X0,X1,X2),X0,k7_waybel18(X0,X1,X2)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f32,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( l1_pre_topc(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)) )
=> ( v1_t_0topsp(X2,X0,X1)
<=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v3_pre_topc(X3,X0)
=> v3_pre_topc(k4_pre_topc(X0,X1,X2,X3),X1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_t_0topsp) ).
fof(f33,axiom,
! [X0] :
( l1_struct_0(X0)
=> ! [X1] :
( l1_pre_topc(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)) )
=> k7_waybel18(X0,X1,X2) = k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d6_waybel18) ).
fof(f34,axiom,
! [X0] :
( l1_struct_0(X0)
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& l1_pre_topc(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)) )
=> k8_waybel18(X0,X1,X2) = X2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d7_waybel18) ).
fof(f35,axiom,
! [X0] :
( ( v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( v2_pre_topc(X1)
& l1_pre_topc(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)) )
=> ( v2_waybel34(X2,X0,X1)
<=> ! [X3] :
( ( v3_pre_topc(X3,X0)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( v3_pre_topc(k4_pre_topc(X0,X1,X2,X3),k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)))
& m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(k3_pre_topc(X1,k1_yellow_2(X0,X1,X2))))) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d9_waybel34) ).
fof(f43,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)) )
=> m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_pre_topc) ).
fof(f44,axiom,
! [X0,X1,X2] :
( ( l1_struct_0(X0)
& l1_pre_topc(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)) )
=> m1_pre_topc(k7_waybel18(X0,X1,X2),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k7_waybel18) ).
fof(f45,axiom,
! [X0,X1,X2] :
( ( l1_struct_0(X0)
& ~ v3_struct_0(X1)
& l1_pre_topc(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)) )
=> ( v1_funct_1(k8_waybel18(X0,X1,X2))
& v1_funct_2(k8_waybel18(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k7_waybel18(X0,X1,X2)))
& m2_relset_1(k8_waybel18(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k7_waybel18(X0,X1,X2))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k8_waybel18) ).
fof(f48,axiom,
! [X0] :
( l1_pre_topc(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f50,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m1_pre_topc(X1,X0)
=> l1_pre_topc(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_pre_topc) ).
fof(f91,axiom,
! [X0,X1,X2] :
( ( 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)) )
=> k1_yellow_2(X0,X1,X2) = k2_relat_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k1_yellow_2) ).
fof(f92,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/sandbox/benchmark/theBenchmark.p',redefinition_k4_pre_topc) ).
fof(f94,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f123,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( v2_waybel34(X2,X0,X1)
<~> v1_t_0topsp(k8_waybel18(X0,X1,X2),X0,k7_waybel18(X0,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)) )
& ~ v3_struct_0(X1)
& v2_pre_topc(X1)
& l1_pre_topc(X1) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f124,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( v2_waybel34(X2,X0,X1)
<~> v1_t_0topsp(k8_waybel18(X0,X1,X2),X0,k7_waybel18(X0,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)) )
& ~ v3_struct_0(X1)
& v2_pre_topc(X1)
& l1_pre_topc(X1) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(flattening,[],[f123]) ).
fof(f158,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v1_t_0topsp(X2,X0,X1)
<=> ! [X3] :
( v3_pre_topc(k4_pre_topc(X0,X1,X2,X3),X1)
| ~ v3_pre_topc(X3,X0)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ l1_pre_topc(X1) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f32]) ).
fof(f159,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v1_t_0topsp(X2,X0,X1)
<=> ! [X3] :
( v3_pre_topc(k4_pre_topc(X0,X1,X2,X3),X1)
| ~ v3_pre_topc(X3,X0)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ l1_pre_topc(X1) )
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f158]) ).
fof(f160,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k7_waybel18(X0,X1,X2) = k3_pre_topc(X1,k1_yellow_2(X0,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)) )
| ~ l1_pre_topc(X1) )
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f33]) ).
fof(f161,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k7_waybel18(X0,X1,X2) = k3_pre_topc(X1,k1_yellow_2(X0,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)) )
| ~ l1_pre_topc(X1) )
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f160]) ).
fof(f162,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k8_waybel18(X0,X1,X2) = 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)) )
| v3_struct_0(X1)
| ~ l1_pre_topc(X1) )
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f34]) ).
fof(f163,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k8_waybel18(X0,X1,X2) = 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)) )
| v3_struct_0(X1)
| ~ l1_pre_topc(X1) )
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f162]) ).
fof(f164,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v2_waybel34(X2,X0,X1)
<=> ! [X3] :
( ( v3_pre_topc(k4_pre_topc(X0,X1,X2,X3),k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)))
& m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(k3_pre_topc(X1,k1_yellow_2(X0,X1,X2))))) )
| ~ v3_pre_topc(X3,X0)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1) )
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f35]) ).
fof(f165,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v2_waybel34(X2,X0,X1)
<=> ! [X3] :
( ( v3_pre_topc(k4_pre_topc(X0,X1,X2,X3),k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)))
& m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(k3_pre_topc(X1,k1_yellow_2(X0,X1,X2))))) )
| ~ v3_pre_topc(X3,X0)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1) )
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f164]) ).
fof(f171,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))
| ~ 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,[],[f43]) ).
fof(f172,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))
| ~ 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,[],[f171]) ).
fof(f173,plain,
! [X0,X1,X2] :
( m1_pre_topc(k7_waybel18(X0,X1,X2),X1)
| ~ l1_struct_0(X0)
| ~ l1_pre_topc(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,[],[f44]) ).
fof(f174,plain,
! [X0,X1,X2] :
( m1_pre_topc(k7_waybel18(X0,X1,X2),X1)
| ~ l1_struct_0(X0)
| ~ l1_pre_topc(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,[],[f173]) ).
fof(f175,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k8_waybel18(X0,X1,X2))
& v1_funct_2(k8_waybel18(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k7_waybel18(X0,X1,X2)))
& m2_relset_1(k8_waybel18(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k7_waybel18(X0,X1,X2))) )
| ~ l1_struct_0(X0)
| v3_struct_0(X1)
| ~ l1_pre_topc(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,[],[f45]) ).
fof(f176,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k8_waybel18(X0,X1,X2))
& v1_funct_2(k8_waybel18(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k7_waybel18(X0,X1,X2)))
& m2_relset_1(k8_waybel18(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k7_waybel18(X0,X1,X2))) )
| ~ l1_struct_0(X0)
| v3_struct_0(X1)
| ~ l1_pre_topc(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,[],[f175]) ).
fof(f179,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f48]) ).
fof(f180,plain,
! [X0] :
( ! [X1] :
( l1_pre_topc(X1)
| ~ m1_pre_topc(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f50]) ).
fof(f219,plain,
! [X0,X1,X2] :
( k1_yellow_2(X0,X1,X2) = k2_relat_1(X2)
| ~ 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,[],[f91]) ).
fof(f220,plain,
! [X0,X1,X2] :
( k1_yellow_2(X0,X1,X2) = k2_relat_1(X2)
| ~ 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,[],[f219]) ).
fof(f221,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,[],[f92]) ).
fof(f222,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,[],[f221]) ).
fof(f239,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ v1_t_0topsp(k8_waybel18(X0,X1,X2),X0,k7_waybel18(X0,X1,X2))
| ~ v2_waybel34(X2,X0,X1) )
& ( v1_t_0topsp(k8_waybel18(X0,X1,X2),X0,k7_waybel18(X0,X1,X2))
| v2_waybel34(X2,X0,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)
& v2_pre_topc(X1)
& l1_pre_topc(X1) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f124]) ).
fof(f240,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ v1_t_0topsp(k8_waybel18(X0,X1,X2),X0,k7_waybel18(X0,X1,X2))
| ~ v2_waybel34(X2,X0,X1) )
& ( v1_t_0topsp(k8_waybel18(X0,X1,X2),X0,k7_waybel18(X0,X1,X2))
| v2_waybel34(X2,X0,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)
& v2_pre_topc(X1)
& l1_pre_topc(X1) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(flattening,[],[f239]) ).
fof(f241,plain,
( ( ~ v1_t_0topsp(k8_waybel18(sK2,sK3,sK4),sK2,k7_waybel18(sK2,sK3,sK4))
| ~ v2_waybel34(sK4,sK2,sK3) )
& ( v1_t_0topsp(k8_waybel18(sK2,sK3,sK4),sK2,k7_waybel18(sK2,sK3,sK4))
| v2_waybel34(sK4,sK2,sK3) )
& v1_funct_1(sK4)
& v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
& m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
& ~ v3_struct_0(sK3)
& v2_pre_topc(sK3)
& l1_pre_topc(sK3)
& ~ v3_struct_0(sK2)
& v2_pre_topc(sK2)
& l1_pre_topc(sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4)],[f240]) ).
fof(f244,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v1_t_0topsp(X2,X0,X1)
| ? [X3] :
( ~ v3_pre_topc(k4_pre_topc(X0,X1,X2,X3),X1)
& v3_pre_topc(X3,X0)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ! [X3] :
( v3_pre_topc(k4_pre_topc(X0,X1,X2,X3),X1)
| ~ v3_pre_topc(X3,X0)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v1_t_0topsp(X2,X0,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)) )
| ~ l1_pre_topc(X1) )
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f159]) ).
fof(f245,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v1_t_0topsp(X2,X0,X1)
| ? [X3] :
( ~ v3_pre_topc(k4_pre_topc(X0,X1,X2,X3),X1)
& v3_pre_topc(X3,X0)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ! [X4] :
( v3_pre_topc(k4_pre_topc(X0,X1,X2,X4),X1)
| ~ v3_pre_topc(X4,X0)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v1_t_0topsp(X2,X0,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)) )
| ~ l1_pre_topc(X1) )
| ~ l1_pre_topc(X0) ),
inference(rectify,[],[f244]) ).
fof(f246,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v1_t_0topsp(X2,X0,X1)
| ( ~ v3_pre_topc(k4_pre_topc(X0,X1,X2,sK5(X0,X1,X2)),X1)
& v3_pre_topc(sK5(X0,X1,X2),X0)
& m1_subset_1(sK5(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ! [X4] :
( v3_pre_topc(k4_pre_topc(X0,X1,X2,X4),X1)
| ~ v3_pre_topc(X4,X0)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v1_t_0topsp(X2,X0,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)) )
| ~ l1_pre_topc(X1) )
| ~ l1_pre_topc(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X3,sK5(X0,X1,X2))],[f245]) ).
fof(f247,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v2_waybel34(X2,X0,X1)
| ? [X3] :
( ( ~ v3_pre_topc(k4_pre_topc(X0,X1,X2,X3),k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)))
| ~ m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(k3_pre_topc(X1,k1_yellow_2(X0,X1,X2))))) )
& v3_pre_topc(X3,X0)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ! [X3] :
( ( v3_pre_topc(k4_pre_topc(X0,X1,X2,X3),k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)))
& m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(k3_pre_topc(X1,k1_yellow_2(X0,X1,X2))))) )
| ~ v3_pre_topc(X3,X0)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v2_waybel34(X2,X0,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)) )
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1) )
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f165]) ).
fof(f248,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v2_waybel34(X2,X0,X1)
| ? [X3] :
( ( ~ v3_pre_topc(k4_pre_topc(X0,X1,X2,X3),k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)))
| ~ m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(k3_pre_topc(X1,k1_yellow_2(X0,X1,X2))))) )
& v3_pre_topc(X3,X0)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ! [X4] :
( ( v3_pre_topc(k4_pre_topc(X0,X1,X2,X4),k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)))
& m1_subset_1(k4_pre_topc(X0,X1,X2,X4),k1_zfmisc_1(u1_struct_0(k3_pre_topc(X1,k1_yellow_2(X0,X1,X2))))) )
| ~ v3_pre_topc(X4,X0)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v2_waybel34(X2,X0,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)) )
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1) )
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(rectify,[],[f247]) ).
fof(f249,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v2_waybel34(X2,X0,X1)
| ( ( ~ v3_pre_topc(k4_pre_topc(X0,X1,X2,sK6(X0,X1,X2)),k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)))
| ~ m1_subset_1(k4_pre_topc(X0,X1,X2,sK6(X0,X1,X2)),k1_zfmisc_1(u1_struct_0(k3_pre_topc(X1,k1_yellow_2(X0,X1,X2))))) )
& v3_pre_topc(sK6(X0,X1,X2),X0)
& m1_subset_1(sK6(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ! [X4] :
( ( v3_pre_topc(k4_pre_topc(X0,X1,X2,X4),k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)))
& m1_subset_1(k4_pre_topc(X0,X1,X2,X4),k1_zfmisc_1(u1_struct_0(k3_pre_topc(X1,k1_yellow_2(X0,X1,X2))))) )
| ~ v3_pre_topc(X4,X0)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v2_waybel34(X2,X0,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)) )
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1) )
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X3,sK6(X0,X1,X2))],[f248]) ).
fof(f278,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,[],[f94]) ).
fof(f279,plain,
l1_pre_topc(sK2),
inference(cnf_transformation,[],[f241]) ).
fof(f280,plain,
v2_pre_topc(sK2),
inference(cnf_transformation,[],[f241]) ).
fof(f282,plain,
l1_pre_topc(sK3),
inference(cnf_transformation,[],[f241]) ).
fof(f283,plain,
v2_pre_topc(sK3),
inference(cnf_transformation,[],[f241]) ).
fof(f284,plain,
~ v3_struct_0(sK3),
inference(cnf_transformation,[],[f241]) ).
fof(f285,plain,
m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)),
inference(cnf_transformation,[],[f241]) ).
fof(f286,plain,
v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3)),
inference(cnf_transformation,[],[f241]) ).
fof(f287,plain,
v1_funct_1(sK4),
inference(cnf_transformation,[],[f241]) ).
fof(f288,plain,
( v1_t_0topsp(k8_waybel18(sK2,sK3,sK4),sK2,k7_waybel18(sK2,sK3,sK4))
| v2_waybel34(sK4,sK2,sK3) ),
inference(cnf_transformation,[],[f241]) ).
fof(f289,plain,
( ~ v1_t_0topsp(k8_waybel18(sK2,sK3,sK4),sK2,k7_waybel18(sK2,sK3,sK4))
| ~ v2_waybel34(sK4,sK2,sK3) ),
inference(cnf_transformation,[],[f241]) ).
fof(f341,plain,
! [X2,X0,X1,X4] :
( v3_pre_topc(k4_pre_topc(X0,X1,X2,X4),X1)
| ~ v3_pre_topc(X4,X0)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_t_0topsp(X2,X0,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))
| ~ l1_pre_topc(X1)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f246]) ).
fof(f342,plain,
! [X2,X0,X1] :
( m1_subset_1(sK5(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)))
| v1_t_0topsp(X2,X0,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))
| ~ l1_pre_topc(X1)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f246]) ).
fof(f343,plain,
! [X2,X0,X1] :
( v3_pre_topc(sK5(X0,X1,X2),X0)
| v1_t_0topsp(X2,X0,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))
| ~ l1_pre_topc(X1)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f246]) ).
fof(f344,plain,
! [X2,X0,X1] :
( v1_t_0topsp(X2,X0,X1)
| ~ v3_pre_topc(k4_pre_topc(X0,X1,X2,sK5(X0,X1,X2)),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))
| ~ l1_pre_topc(X1)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f246]) ).
fof(f345,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| k7_waybel18(X0,X1,X2) = k3_pre_topc(X1,k1_yellow_2(X0,X1,X2))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ l1_pre_topc(X1)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f161]) ).
fof(f346,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| k8_waybel18(X0,X1,X2) = X2
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ l1_pre_topc(X1)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f163]) ).
fof(f348,plain,
! [X2,X0,X1,X4] :
( ~ v2_waybel34(X2,X0,X1)
| ~ v3_pre_topc(X4,X0)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)))
| v3_pre_topc(k4_pre_topc(X0,X1,X2,X4),k3_pre_topc(X1,k1_yellow_2(X0,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))
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f249]) ).
fof(f349,plain,
! [X2,X0,X1] :
( m1_subset_1(sK6(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)))
| v2_waybel34(X2,X0,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))
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f249]) ).
fof(f350,plain,
! [X2,X0,X1] :
( v3_pre_topc(sK6(X0,X1,X2),X0)
| v2_waybel34(X2,X0,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))
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f249]) ).
fof(f351,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v3_pre_topc(k4_pre_topc(X0,X1,X2,sK6(X0,X1,X2)),k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)))
| ~ m1_subset_1(k4_pre_topc(X0,X1,X2,sK6(X0,X1,X2)),k1_zfmisc_1(u1_struct_0(k3_pre_topc(X1,k1_yellow_2(X0,X1,X2)))))
| ~ v1_funct_1(X2)
| v2_waybel34(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f249]) ).
fof(f357,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))
| ~ 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,[],[f172]) ).
fof(f358,plain,
! [X2,X0,X1] :
( m1_pre_topc(k7_waybel18(X0,X1,X2),X1)
| ~ l1_struct_0(X0)
| ~ l1_pre_topc(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,[],[f174]) ).
fof(f359,plain,
! [X2,X0,X1] :
( m2_relset_1(k8_waybel18(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k7_waybel18(X0,X1,X2)))
| ~ l1_struct_0(X0)
| v3_struct_0(X1)
| ~ l1_pre_topc(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,[],[f176]) ).
fof(f360,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ l1_struct_0(X0)
| v3_struct_0(X1)
| ~ l1_pre_topc(X1)
| ~ v1_funct_1(X2)
| v1_funct_2(k8_waybel18(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k7_waybel18(X0,X1,X2)))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f176]) ).
fof(f363,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f179]) ).
fof(f364,plain,
! [X0,X1] :
( l1_pre_topc(X1)
| ~ m1_pre_topc(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f180]) ).
fof(f462,plain,
! [X2,X0,X1] :
( k1_yellow_2(X0,X1,X2) = k2_relat_1(X2)
| ~ 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,[],[f220]) ).
fof(f463,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f222]) ).
fof(f465,plain,
! [X2,X0,X1] :
( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f278]) ).
fof(f477,definition,
( spl34_1
<=> v2_waybel34(sK4,sK2,sK3) ),
introduced(definition,[new_symbols(definition,[spl34_1])],[avatar_definition]) ).
fof(f478,plain,
( ~ v2_waybel34(sK4,sK2,sK3)
| spl34_1 ),
inference(avatar_component_clause,[],[f477]) ).
fof(f479,plain,
( v2_waybel34(sK4,sK2,sK3)
| ~ spl34_1 ),
inference(avatar_component_clause,[],[f477]) ).
fof(f481,definition,
( spl34_2
<=> v1_t_0topsp(k8_waybel18(sK2,sK3,sK4),sK2,k7_waybel18(sK2,sK3,sK4)) ),
introduced(definition,[new_symbols(definition,[spl34_2])],[avatar_definition]) ).
fof(f482,plain,
( ~ v1_t_0topsp(k8_waybel18(sK2,sK3,sK4),sK2,k7_waybel18(sK2,sK3,sK4))
| spl34_2 ),
inference(avatar_component_clause,[],[f481]) ).
fof(f483,plain,
( v1_t_0topsp(k8_waybel18(sK2,sK3,sK4),sK2,k7_waybel18(sK2,sK3,sK4))
| ~ spl34_2 ),
inference(avatar_component_clause,[],[f481]) ).
fof(f484,plain,
( spl34_1
| spl34_2 ),
inference(avatar_split_clause,[],[f288,f481,f477]) ).
fof(f485,plain,
( ~ spl34_1
| ~ spl34_2 ),
inference(avatar_split_clause,[],[f289,f481,f477]) ).
fof(f556,plain,
( ~ v1_funct_1(sK4)
| sK4 = k8_waybel18(sK2,sK3,sK4)
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ l1_pre_topc(sK3)
| ~ l1_struct_0(sK2) ),
inference(resolution,[],[f346,f286]) ).
fof(f557,plain,
( sK4 = k8_waybel18(sK2,sK3,sK4)
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ l1_pre_topc(sK3)
| ~ l1_struct_0(sK2) ),
inference(forward_subsumption_resolution,[],[f556,f287]) ).
fof(f558,plain,
( sK4 = k8_waybel18(sK2,sK3,sK4)
| v3_struct_0(sK3)
| ~ l1_pre_topc(sK3)
| ~ l1_struct_0(sK2) ),
inference(forward_subsumption_resolution,[],[f557,f285]) ).
fof(f559,plain,
( sK4 = k8_waybel18(sK2,sK3,sK4)
| ~ l1_pre_topc(sK3)
| ~ l1_struct_0(sK2) ),
inference(forward_subsumption_resolution,[],[f558,f284]) ).
fof(f560,plain,
( sK4 = k8_waybel18(sK2,sK3,sK4)
| ~ l1_struct_0(sK2) ),
inference(forward_subsumption_resolution,[],[f559,f282]) ).
fof(f562,definition,
( spl34_3
<=> l1_struct_0(sK2) ),
introduced(definition,[new_symbols(definition,[spl34_3])],[avatar_definition]) ).
fof(f563,plain,
( l1_struct_0(sK2)
| ~ spl34_3 ),
inference(avatar_component_clause,[],[f562]) ).
fof(f564,plain,
( ~ l1_struct_0(sK2)
| spl34_3 ),
inference(avatar_component_clause,[],[f562]) ).
fof(f566,definition,
( spl34_4
<=> sK4 = k8_waybel18(sK2,sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl34_4])],[avatar_definition]) ).
fof(f568,plain,
( sK4 = k8_waybel18(sK2,sK3,sK4)
| ~ spl34_4 ),
inference(avatar_component_clause,[],[f566]) ).
fof(f569,plain,
( ~ spl34_3
| spl34_4 ),
inference(avatar_split_clause,[],[f560,f566,f562]) ).
fof(f570,plain,
( ~ l1_pre_topc(sK2)
| spl34_3 ),
inference(resolution,[],[f564,f363]) ).
fof(f571,plain,
( $false
| spl34_3 ),
inference(forward_subsumption_resolution,[],[f570,f279]) ).
fof(f572,plain,
spl34_3,
inference(avatar_contradiction_clause,[],[f571]) ).
fof(f577,plain,
! [X0] :
( ~ l1_struct_0(sK2)
| ~ l1_struct_0(sK3)
| ~ v1_funct_1(sK4)
| k4_pre_topc(sK2,sK3,sK4,X0) = k9_relat_1(sK4,X0)
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(resolution,[],[f463,f286]) ).
fof(f578,plain,
( ! [X0] :
( ~ l1_struct_0(sK3)
| ~ v1_funct_1(sK4)
| k4_pre_topc(sK2,sK3,sK4,X0) = k9_relat_1(sK4,X0)
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) )
| ~ spl34_3 ),
inference(forward_subsumption_resolution,[],[f577,f563]) ).
fof(f579,plain,
( ! [X0] :
( ~ l1_struct_0(sK3)
| k4_pre_topc(sK2,sK3,sK4,X0) = k9_relat_1(sK4,X0)
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) )
| ~ spl34_3 ),
inference(forward_subsumption_resolution,[],[f578,f287]) ).
fof(f581,definition,
( spl34_5
<=> m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
introduced(definition,[new_symbols(definition,[spl34_5])],[avatar_definition]) ).
fof(f582,plain,
( m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl34_5 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f583,plain,
( ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| spl34_5 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f585,definition,
( spl34_6
<=> ! [X0] : k4_pre_topc(sK2,sK3,sK4,X0) = k9_relat_1(sK4,X0) ),
introduced(definition,[new_symbols(definition,[spl34_6])],[avatar_definition]) ).
fof(f586,plain,
( ! [X0] : k4_pre_topc(sK2,sK3,sK4,X0) = k9_relat_1(sK4,X0)
| ~ spl34_6 ),
inference(avatar_component_clause,[],[f585]) ).
fof(f588,definition,
( spl34_7
<=> l1_struct_0(sK3) ),
introduced(definition,[new_symbols(definition,[spl34_7])],[avatar_definition]) ).
fof(f589,plain,
( l1_struct_0(sK3)
| ~ spl34_7 ),
inference(avatar_component_clause,[],[f588]) ).
fof(f590,plain,
( ~ l1_struct_0(sK3)
| spl34_7 ),
inference(avatar_component_clause,[],[f588]) ).
fof(f591,plain,
( ~ spl34_5
| spl34_6
| ~ spl34_7
| ~ spl34_3 ),
inference(avatar_split_clause,[],[f579,f562,f588,f585,f581]) ).
fof(f592,plain,
( ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| spl34_5 ),
inference(resolution,[],[f583,f465]) ).
fof(f593,plain,
( $false
| spl34_5 ),
inference(forward_subsumption_resolution,[],[f592,f285]) ).
fof(f594,plain,
spl34_5,
inference(avatar_contradiction_clause,[],[f593]) ).
fof(f595,plain,
( ~ l1_pre_topc(sK3)
| spl34_7 ),
inference(resolution,[],[f590,f363]) ).
fof(f596,plain,
( $false
| spl34_7 ),
inference(forward_subsumption_resolution,[],[f595,f282]) ).
fof(f597,plain,
spl34_7,
inference(avatar_contradiction_clause,[],[f596]) ).
fof(f598,plain,
( ~ v1_funct_1(sK4)
| k7_waybel18(sK2,sK3,sK4) = k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ l1_pre_topc(sK3)
| ~ l1_struct_0(sK2) ),
inference(resolution,[],[f345,f286]) ).
fof(f599,plain,
( k7_waybel18(sK2,sK3,sK4) = k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ l1_pre_topc(sK3)
| ~ l1_struct_0(sK2) ),
inference(forward_subsumption_resolution,[],[f598,f287]) ).
fof(f600,plain,
( k7_waybel18(sK2,sK3,sK4) = k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4))
| ~ l1_pre_topc(sK3)
| ~ l1_struct_0(sK2) ),
inference(forward_subsumption_resolution,[],[f599,f285]) ).
fof(f601,plain,
( k7_waybel18(sK2,sK3,sK4) = k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4))
| ~ l1_struct_0(sK2) ),
inference(forward_subsumption_resolution,[],[f600,f282]) ).
fof(f602,plain,
( k7_waybel18(sK2,sK3,sK4) = k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4))
| ~ spl34_3 ),
inference(forward_subsumption_resolution,[],[f601,f563]) ).
fof(f609,plain,
( m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k7_waybel18(sK2,sK3,sK4)))
| ~ l1_struct_0(sK2)
| v3_struct_0(sK3)
| ~ l1_pre_topc(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl34_4 ),
inference(superposition,[],[f359,f568]) ).
fof(f610,plain,
( m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k7_waybel18(sK2,sK3,sK4)))
| v3_struct_0(sK3)
| ~ l1_pre_topc(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl34_3
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f609,f563]) ).
fof(f611,plain,
( m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k7_waybel18(sK2,sK3,sK4)))
| ~ l1_pre_topc(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl34_3
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f610,f284]) ).
fof(f612,plain,
( m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k7_waybel18(sK2,sK3,sK4)))
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl34_3
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f611,f282]) ).
fof(f613,plain,
( m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k7_waybel18(sK2,sK3,sK4)))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl34_3
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f612,f287]) ).
fof(f614,plain,
( m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k7_waybel18(sK2,sK3,sK4)))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl34_3
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f613,f286]) ).
fof(f615,plain,
( m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k7_waybel18(sK2,sK3,sK4)))
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5 ),
inference(forward_subsumption_resolution,[],[f614,f582]) ).
fof(f616,plain,
( ~ l1_struct_0(sK2)
| v3_struct_0(sK3)
| ~ l1_pre_topc(sK3)
| ~ v1_funct_1(sK4)
| v1_funct_2(k8_waybel18(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(k7_waybel18(sK2,sK3,sK4)))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(resolution,[],[f360,f286]) ).
fof(f617,plain,
( v3_struct_0(sK3)
| ~ l1_pre_topc(sK3)
| ~ v1_funct_1(sK4)
| v1_funct_2(k8_waybel18(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(k7_waybel18(sK2,sK3,sK4)))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl34_3 ),
inference(forward_subsumption_resolution,[],[f616,f563]) ).
fof(f618,plain,
( ~ l1_pre_topc(sK3)
| ~ v1_funct_1(sK4)
| v1_funct_2(k8_waybel18(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(k7_waybel18(sK2,sK3,sK4)))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl34_3 ),
inference(forward_subsumption_resolution,[],[f617,f284]) ).
fof(f619,plain,
( ~ v1_funct_1(sK4)
| v1_funct_2(k8_waybel18(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(k7_waybel18(sK2,sK3,sK4)))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl34_3 ),
inference(forward_subsumption_resolution,[],[f618,f282]) ).
fof(f620,plain,
( v1_funct_2(k8_waybel18(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(k7_waybel18(sK2,sK3,sK4)))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl34_3 ),
inference(forward_subsumption_resolution,[],[f619,f287]) ).
fof(f621,plain,
( v1_funct_2(k8_waybel18(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(k7_waybel18(sK2,sK3,sK4)))
| ~ spl34_3
| ~ spl34_5 ),
inference(forward_subsumption_resolution,[],[f620,f582]) ).
fof(f622,plain,
( v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(k7_waybel18(sK2,sK3,sK4)))
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5 ),
inference(forward_demodulation,[],[f621,f568]) ).
fof(f625,plain,
( ! [X0] :
( ~ l1_struct_0(sK2)
| ~ l1_struct_0(k7_waybel18(sK2,sK3,sK4))
| ~ v1_funct_1(sK4)
| k9_relat_1(sK4,X0) = k4_pre_topc(sK2,k7_waybel18(sK2,sK3,sK4),sK4,X0)
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k7_waybel18(sK2,sK3,sK4))) )
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5 ),
inference(resolution,[],[f622,f463]) ).
fof(f628,plain,
( ! [X0] :
( ~ l1_struct_0(k7_waybel18(sK2,sK3,sK4))
| ~ v1_funct_1(sK4)
| k9_relat_1(sK4,X0) = k4_pre_topc(sK2,k7_waybel18(sK2,sK3,sK4),sK4,X0)
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k7_waybel18(sK2,sK3,sK4))) )
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5 ),
inference(forward_subsumption_resolution,[],[f625,f563]) ).
fof(f632,plain,
( ! [X0] :
( ~ l1_struct_0(k7_waybel18(sK2,sK3,sK4))
| k9_relat_1(sK4,X0) = k4_pre_topc(sK2,k7_waybel18(sK2,sK3,sK4),sK4,X0)
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k7_waybel18(sK2,sK3,sK4))) )
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5 ),
inference(forward_subsumption_resolution,[],[f628,f287]) ).
fof(f636,definition,
( spl34_8
<=> l1_pre_topc(k7_waybel18(sK2,sK3,sK4)) ),
introduced(definition,[new_symbols(definition,[spl34_8])],[avatar_definition]) ).
fof(f637,plain,
( l1_pre_topc(k7_waybel18(sK2,sK3,sK4))
| ~ spl34_8 ),
inference(avatar_component_clause,[],[f636]) ).
fof(f638,plain,
( ~ l1_pre_topc(k7_waybel18(sK2,sK3,sK4))
| spl34_8 ),
inference(avatar_component_clause,[],[f636]) ).
fof(f644,definition,
( spl34_10
<=> m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k7_waybel18(sK2,sK3,sK4))) ),
introduced(definition,[new_symbols(definition,[spl34_10])],[avatar_definition]) ).
fof(f645,plain,
( m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k7_waybel18(sK2,sK3,sK4)))
| ~ spl34_10 ),
inference(avatar_component_clause,[],[f644]) ).
fof(f653,definition,
( spl34_12
<=> m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k7_waybel18(sK2,sK3,sK4))) ),
introduced(definition,[new_symbols(definition,[spl34_12])],[avatar_definition]) ).
fof(f654,plain,
( m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k7_waybel18(sK2,sK3,sK4)))
| ~ spl34_12 ),
inference(avatar_component_clause,[],[f653]) ).
fof(f655,plain,
( ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k7_waybel18(sK2,sK3,sK4)))
| spl34_12 ),
inference(avatar_component_clause,[],[f653]) ).
fof(f657,definition,
( spl34_13
<=> ! [X0] : k9_relat_1(sK4,X0) = k4_pre_topc(sK2,k7_waybel18(sK2,sK3,sK4),sK4,X0) ),
introduced(definition,[new_symbols(definition,[spl34_13])],[avatar_definition]) ).
fof(f658,plain,
( ! [X0] : k9_relat_1(sK4,X0) = k4_pre_topc(sK2,k7_waybel18(sK2,sK3,sK4),sK4,X0)
| ~ spl34_13 ),
inference(avatar_component_clause,[],[f657]) ).
fof(f660,definition,
( spl34_14
<=> l1_struct_0(k7_waybel18(sK2,sK3,sK4)) ),
introduced(definition,[new_symbols(definition,[spl34_14])],[avatar_definition]) ).
fof(f661,plain,
( l1_struct_0(k7_waybel18(sK2,sK3,sK4))
| ~ spl34_14 ),
inference(avatar_component_clause,[],[f660]) ).
fof(f662,plain,
( ~ l1_struct_0(k7_waybel18(sK2,sK3,sK4))
| spl34_14 ),
inference(avatar_component_clause,[],[f660]) ).
fof(f663,plain,
( ~ spl34_12
| spl34_13
| ~ spl34_14
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5 ),
inference(avatar_split_clause,[],[f632,f581,f566,f562,f660,f657,f653]) ).
fof(f674,plain,
( ! [X0] :
( ~ m1_pre_topc(k7_waybel18(sK2,sK3,sK4),X0)
| ~ l1_pre_topc(X0) )
| spl34_8 ),
inference(resolution,[],[f638,f364]) ).
fof(f696,plain,
( ~ l1_pre_topc(sK3)
| ~ l1_struct_0(sK2)
| ~ l1_pre_topc(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| spl34_8 ),
inference(resolution,[],[f674,f358]) ).
fof(f697,plain,
( ~ l1_pre_topc(sK3)
| ~ l1_struct_0(sK2)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| spl34_8 ),
inference(duplicate_literal_removal,[],[f696]) ).
fof(f698,plain,
( ~ l1_struct_0(sK2)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| spl34_8 ),
inference(forward_subsumption_resolution,[],[f697,f282]) ).
fof(f699,plain,
( ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl34_3
| spl34_8 ),
inference(forward_subsumption_resolution,[],[f698,f563]) ).
fof(f700,plain,
( ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl34_3
| spl34_8 ),
inference(forward_subsumption_resolution,[],[f699,f287]) ).
fof(f701,plain,
( ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl34_3
| spl34_8 ),
inference(forward_subsumption_resolution,[],[f700,f286]) ).
fof(f702,plain,
( $false
| ~ spl34_3
| ~ spl34_5
| spl34_8 ),
inference(forward_subsumption_resolution,[],[f701,f582]) ).
fof(f703,plain,
( ~ spl34_3
| ~ spl34_5
| spl34_8 ),
inference(avatar_contradiction_clause,[],[f702]) ).
fof(f705,plain,
( ~ v3_pre_topc(k4_pre_topc(sK2,sK3,sK4,sK6(sK2,sK3,sK4)),k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))
| ~ m1_subset_1(k4_pre_topc(sK2,sK3,sK4,sK6(sK2,sK3,sK4)),k1_zfmisc_1(u1_struct_0(k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))))
| ~ v1_funct_1(sK4)
| v2_waybel34(sK4,sK2,sK3)
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_pre_topc(sK3)
| ~ l1_pre_topc(sK3)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2) ),
inference(resolution,[],[f351,f286]) ).
fof(f708,plain,
( ~ v3_pre_topc(k4_pre_topc(sK2,sK3,sK4,sK6(sK2,sK3,sK4)),k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))
| ~ m1_subset_1(k4_pre_topc(sK2,sK3,sK4,sK6(sK2,sK3,sK4)),k1_zfmisc_1(u1_struct_0(k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))))
| v2_waybel34(sK4,sK2,sK3)
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_pre_topc(sK3)
| ~ l1_pre_topc(sK3)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2) ),
inference(forward_subsumption_resolution,[],[f705,f287]) ).
fof(f710,plain,
( ~ v3_pre_topc(k4_pre_topc(sK2,sK3,sK4,sK6(sK2,sK3,sK4)),k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))
| ~ m1_subset_1(k4_pre_topc(sK2,sK3,sK4,sK6(sK2,sK3,sK4)),k1_zfmisc_1(u1_struct_0(k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_pre_topc(sK3)
| ~ l1_pre_topc(sK3)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| spl34_1 ),
inference(forward_subsumption_resolution,[],[f708,f478]) ).
fof(f712,plain,
( ~ v3_pre_topc(k4_pre_topc(sK2,sK3,sK4,sK6(sK2,sK3,sK4)),k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))
| ~ m1_subset_1(k4_pre_topc(sK2,sK3,sK4,sK6(sK2,sK3,sK4)),k1_zfmisc_1(u1_struct_0(k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))))
| ~ v2_pre_topc(sK3)
| ~ l1_pre_topc(sK3)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| spl34_1 ),
inference(forward_subsumption_resolution,[],[f710,f285]) ).
fof(f714,plain,
( ~ v3_pre_topc(k4_pre_topc(sK2,sK3,sK4,sK6(sK2,sK3,sK4)),k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))
| ~ m1_subset_1(k4_pre_topc(sK2,sK3,sK4,sK6(sK2,sK3,sK4)),k1_zfmisc_1(u1_struct_0(k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))))
| ~ l1_pre_topc(sK3)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| spl34_1 ),
inference(forward_subsumption_resolution,[],[f712,f283]) ).
fof(f732,plain,
( ~ v3_pre_topc(k4_pre_topc(sK2,sK3,sK4,sK6(sK2,sK3,sK4)),k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))
| ~ m1_subset_1(k4_pre_topc(sK2,sK3,sK4,sK6(sK2,sK3,sK4)),k1_zfmisc_1(u1_struct_0(k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))))
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| spl34_1 ),
inference(forward_subsumption_resolution,[],[f714,f282]) ).
fof(f733,plain,
( ~ v3_pre_topc(k4_pre_topc(sK2,sK3,sK4,sK6(sK2,sK3,sK4)),k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))
| ~ m1_subset_1(k4_pre_topc(sK2,sK3,sK4,sK6(sK2,sK3,sK4)),k1_zfmisc_1(u1_struct_0(k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))))
| ~ l1_pre_topc(sK2)
| spl34_1 ),
inference(forward_subsumption_resolution,[],[f732,f280]) ).
fof(f734,plain,
( ~ v3_pre_topc(k4_pre_topc(sK2,sK3,sK4,sK6(sK2,sK3,sK4)),k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))
| ~ m1_subset_1(k4_pre_topc(sK2,sK3,sK4,sK6(sK2,sK3,sK4)),k1_zfmisc_1(u1_struct_0(k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))))
| spl34_1 ),
inference(forward_subsumption_resolution,[],[f733,f279]) ).
fof(f735,plain,
( ~ v3_pre_topc(k9_relat_1(sK4,sK6(sK2,sK3,sK4)),k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))
| ~ m1_subset_1(k4_pre_topc(sK2,sK3,sK4,sK6(sK2,sK3,sK4)),k1_zfmisc_1(u1_struct_0(k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))))
| spl34_1
| ~ spl34_6 ),
inference(forward_demodulation,[],[f734,f586]) ).
fof(f736,plain,
( ~ m1_subset_1(k9_relat_1(sK4,sK6(sK2,sK3,sK4)),k1_zfmisc_1(u1_struct_0(k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))))
| ~ v3_pre_topc(k9_relat_1(sK4,sK6(sK2,sK3,sK4)),k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))
| spl34_1
| ~ spl34_6 ),
inference(forward_demodulation,[],[f735,f586]) ).
fof(f738,definition,
( spl34_23
<=> v3_pre_topc(k9_relat_1(sK4,sK6(sK2,sK3,sK4)),k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4))) ),
introduced(definition,[new_symbols(definition,[spl34_23])],[avatar_definition]) ).
fof(f740,plain,
( ~ v3_pre_topc(k9_relat_1(sK4,sK6(sK2,sK3,sK4)),k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))
| spl34_23 ),
inference(avatar_component_clause,[],[f738]) ).
fof(f742,definition,
( spl34_24
<=> m1_subset_1(k9_relat_1(sK4,sK6(sK2,sK3,sK4)),k1_zfmisc_1(u1_struct_0(k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4))))) ),
introduced(definition,[new_symbols(definition,[spl34_24])],[avatar_definition]) ).
fof(f744,plain,
( ~ m1_subset_1(k9_relat_1(sK4,sK6(sK2,sK3,sK4)),k1_zfmisc_1(u1_struct_0(k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))))
| spl34_24 ),
inference(avatar_component_clause,[],[f742]) ).
fof(f745,plain,
( ~ spl34_23
| ~ spl34_24
| spl34_1
| ~ spl34_6 ),
inference(avatar_split_clause,[],[f736,f585,f477,f742,f738]) ).
fof(f756,plain,
( k7_waybel18(sK2,sK3,sK4) = k3_pre_topc(sK3,k2_relat_1(sK4))
| ~ l1_struct_0(sK2)
| ~ l1_struct_0(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl34_3 ),
inference(superposition,[],[f602,f462]) ).
fof(f765,plain,
( k7_waybel18(sK2,sK3,sK4) = k3_pre_topc(sK3,k2_relat_1(sK4))
| ~ l1_struct_0(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl34_3 ),
inference(forward_subsumption_resolution,[],[f756,f563]) ).
fof(f782,plain,
( k7_waybel18(sK2,sK3,sK4) = k3_pre_topc(sK3,k2_relat_1(sK4))
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl34_3
| ~ spl34_7 ),
inference(forward_subsumption_resolution,[],[f765,f589]) ).
fof(f789,plain,
( k7_waybel18(sK2,sK3,sK4) = k3_pre_topc(sK3,k2_relat_1(sK4))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl34_3
| ~ spl34_7 ),
inference(forward_subsumption_resolution,[],[f782,f287]) ).
fof(f790,plain,
( k7_waybel18(sK2,sK3,sK4) = k3_pre_topc(sK3,k2_relat_1(sK4))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl34_3
| ~ spl34_7 ),
inference(forward_subsumption_resolution,[],[f789,f286]) ).
fof(f791,plain,
( k7_waybel18(sK2,sK3,sK4) = k3_pre_topc(sK3,k2_relat_1(sK4))
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7 ),
inference(forward_subsumption_resolution,[],[f790,f582]) ).
fof(f792,plain,
( ~ v3_pre_topc(k9_relat_1(sK4,sK6(sK2,sK3,sK4)),k7_waybel18(sK2,sK3,sK4))
| ~ spl34_3
| spl34_23 ),
inference(forward_demodulation,[],[f740,f602]) ).
fof(f834,plain,
( spl34_10
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5 ),
inference(avatar_split_clause,[],[f615,f581,f566,f562,f644]) ).
fof(f847,plain,
( ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k7_waybel18(sK2,sK3,sK4)))
| spl34_12 ),
inference(resolution,[],[f655,f465]) ).
fof(f848,plain,
( $false
| ~ spl34_10
| spl34_12 ),
inference(forward_subsumption_resolution,[],[f847,f645]) ).
fof(f849,plain,
( ~ spl34_10
| spl34_12 ),
inference(avatar_contradiction_clause,[],[f848]) ).
fof(f854,plain,
( ~ l1_pre_topc(k7_waybel18(sK2,sK3,sK4))
| spl34_14 ),
inference(resolution,[],[f662,f363]) ).
fof(f855,plain,
( $false
| ~ spl34_8
| spl34_14 ),
inference(forward_subsumption_resolution,[],[f854,f637]) ).
fof(f856,plain,
( ~ spl34_8
| spl34_14 ),
inference(avatar_contradiction_clause,[],[f855]) ).
fof(f1193,definition,
( spl34_49
<=> v3_pre_topc(sK6(sK2,sK3,sK4),sK2) ),
introduced(definition,[new_symbols(definition,[spl34_49])],[avatar_definition]) ).
fof(f1194,plain,
( v3_pre_topc(sK6(sK2,sK3,sK4),sK2)
| ~ spl34_49 ),
inference(avatar_component_clause,[],[f1193]) ).
fof(f1195,plain,
( ~ v3_pre_topc(sK6(sK2,sK3,sK4),sK2)
| spl34_49 ),
inference(avatar_component_clause,[],[f1193]) ).
fof(f1197,definition,
( spl34_50
<=> m1_subset_1(sK6(sK2,sK3,sK4),k1_zfmisc_1(u1_struct_0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl34_50])],[avatar_definition]) ).
fof(f1199,plain,
( ~ m1_subset_1(sK6(sK2,sK3,sK4),k1_zfmisc_1(u1_struct_0(sK2)))
| spl34_50 ),
inference(avatar_component_clause,[],[f1197]) ).
fof(f1202,plain,
( v2_waybel34(sK4,sK2,sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_pre_topc(sK3)
| ~ l1_pre_topc(sK3)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| spl34_49 ),
inference(resolution,[],[f1195,f350]) ).
fof(f1205,plain,
( ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_pre_topc(sK3)
| ~ l1_pre_topc(sK3)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| spl34_1
| spl34_49 ),
inference(forward_subsumption_resolution,[],[f1202,f478]) ).
fof(f1207,plain,
( ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_pre_topc(sK3)
| ~ l1_pre_topc(sK3)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| spl34_1
| spl34_49 ),
inference(forward_subsumption_resolution,[],[f1205,f287]) ).
fof(f1213,plain,
( ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_pre_topc(sK3)
| ~ l1_pre_topc(sK3)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| spl34_1
| spl34_49 ),
inference(forward_subsumption_resolution,[],[f1207,f286]) ).
fof(f1214,plain,
( ~ v2_pre_topc(sK3)
| ~ l1_pre_topc(sK3)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| spl34_1
| spl34_49 ),
inference(forward_subsumption_resolution,[],[f1213,f285]) ).
fof(f1215,plain,
( ~ l1_pre_topc(sK3)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| spl34_1
| spl34_49 ),
inference(forward_subsumption_resolution,[],[f1214,f283]) ).
fof(f1216,plain,
( ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| spl34_1
| spl34_49 ),
inference(forward_subsumption_resolution,[],[f1215,f282]) ).
fof(f1217,plain,
( ~ l1_pre_topc(sK2)
| spl34_1
| spl34_49 ),
inference(forward_subsumption_resolution,[],[f1216,f280]) ).
fof(f1218,plain,
( $false
| spl34_1
| spl34_49 ),
inference(forward_subsumption_resolution,[],[f1217,f279]) ).
fof(f1219,plain,
( spl34_1
| spl34_49 ),
inference(avatar_contradiction_clause,[],[f1218]) ).
fof(f1424,plain,
( v2_waybel34(sK4,sK2,sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_pre_topc(sK3)
| ~ l1_pre_topc(sK3)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| spl34_50 ),
inference(resolution,[],[f1199,f349]) ).
fof(f1428,plain,
( ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_pre_topc(sK3)
| ~ l1_pre_topc(sK3)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| spl34_1
| spl34_50 ),
inference(forward_subsumption_resolution,[],[f1424,f478]) ).
fof(f1429,plain,
( ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_pre_topc(sK3)
| ~ l1_pre_topc(sK3)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| spl34_1
| spl34_50 ),
inference(forward_subsumption_resolution,[],[f1428,f287]) ).
fof(f1430,plain,
( ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_pre_topc(sK3)
| ~ l1_pre_topc(sK3)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| spl34_1
| spl34_50 ),
inference(forward_subsumption_resolution,[],[f1429,f286]) ).
fof(f1431,plain,
( ~ v2_pre_topc(sK3)
| ~ l1_pre_topc(sK3)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| spl34_1
| spl34_50 ),
inference(forward_subsumption_resolution,[],[f1430,f285]) ).
fof(f1432,plain,
( ~ l1_pre_topc(sK3)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| spl34_1
| spl34_50 ),
inference(forward_subsumption_resolution,[],[f1431,f283]) ).
fof(f1433,plain,
( ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2)
| spl34_1
| spl34_50 ),
inference(forward_subsumption_resolution,[],[f1432,f282]) ).
fof(f1434,plain,
( ~ l1_pre_topc(sK2)
| spl34_1
| spl34_50 ),
inference(forward_subsumption_resolution,[],[f1433,f280]) ).
fof(f1435,plain,
( $false
| spl34_1
| spl34_50 ),
inference(forward_subsumption_resolution,[],[f1434,f279]) ).
fof(f1436,plain,
( spl34_1
| spl34_50 ),
inference(avatar_contradiction_clause,[],[f1435]) ).
fof(f1442,plain,
( v1_t_0topsp(sK4,sK2,k7_waybel18(sK2,sK3,sK4))
| ~ spl34_2
| ~ spl34_4 ),
inference(forward_demodulation,[],[f483,f568]) ).
fof(f1549,plain,
( v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_7 ),
inference(superposition,[],[f622,f791]) ).
fof(f1550,plain,
( l1_pre_topc(k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_8 ),
inference(superposition,[],[f637,f791]) ).
fof(f1554,plain,
( m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_12 ),
inference(superposition,[],[f654,f791]) ).
fof(f1555,plain,
( l1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_14 ),
inference(superposition,[],[f661,f791]) ).
fof(f1562,plain,
( ~ v3_pre_topc(k9_relat_1(sK4,sK6(sK2,sK3,sK4)),k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| spl34_23 ),
inference(superposition,[],[f792,f791]) ).
fof(f1563,plain,
( v1_t_0topsp(sK4,sK2,k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ spl34_2
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_7 ),
inference(superposition,[],[f1442,f791]) ).
fof(f1564,plain,
( m2_relset_1(k8_waybel18(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ l1_struct_0(sK2)
| v3_struct_0(sK3)
| ~ l1_pre_topc(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7 ),
inference(superposition,[],[f359,f791]) ).
fof(f1567,plain,
( m2_relset_1(k8_waybel18(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| v3_struct_0(sK3)
| ~ l1_pre_topc(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7 ),
inference(forward_subsumption_resolution,[],[f1564,f563]) ).
fof(f1569,plain,
( m2_relset_1(k8_waybel18(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ l1_pre_topc(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7 ),
inference(forward_subsumption_resolution,[],[f1567,f284]) ).
fof(f1571,plain,
( m2_relset_1(k8_waybel18(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7 ),
inference(forward_subsumption_resolution,[],[f1569,f282]) ).
fof(f1573,plain,
( m2_relset_1(k8_waybel18(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7 ),
inference(forward_subsumption_resolution,[],[f1571,f287]) ).
fof(f1575,plain,
( m2_relset_1(k8_waybel18(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7 ),
inference(forward_subsumption_resolution,[],[f1573,f286]) ).
fof(f1576,plain,
( m2_relset_1(k8_waybel18(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7 ),
inference(forward_subsumption_resolution,[],[f1575,f582]) ).
fof(f1577,plain,
( m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_7 ),
inference(forward_demodulation,[],[f1576,f568]) ).
fof(f1582,plain,
( ! [X0] : k9_relat_1(sK4,X0) = k4_pre_topc(sK2,k3_pre_topc(sK3,k2_relat_1(sK4)),sK4,X0)
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_13 ),
inference(forward_demodulation,[],[f658,f791]) ).
fof(f1584,plain,
( ! [X0] :
( v3_pre_topc(k9_relat_1(sK4,X0),k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ v3_pre_topc(X0,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v1_t_0topsp(sK4,sK2,k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ l1_pre_topc(k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ l1_pre_topc(sK2) )
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_13 ),
inference(superposition,[],[f341,f1582]) ).
fof(f1585,plain,
( ! [X0] :
( m1_subset_1(k9_relat_1(sK4,X0),k1_zfmisc_1(u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4)))))
| ~ l1_struct_0(sK2)
| ~ l1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4)))) )
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_13 ),
inference(superposition,[],[f357,f1582]) ).
fof(f1586,plain,
( ! [X0] :
( m1_subset_1(k9_relat_1(sK4,X0),k1_zfmisc_1(u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4)))))
| ~ l1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4)))) )
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_13 ),
inference(forward_subsumption_resolution,[],[f1585,f563]) ).
fof(f1587,plain,
( ! [X0] :
( v3_pre_topc(k9_relat_1(sK4,X0),k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ v3_pre_topc(X0,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v1_t_0topsp(sK4,sK2,k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ l1_pre_topc(k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ l1_pre_topc(sK2) )
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_13 ),
inference(forward_subsumption_resolution,[],[f1584,f287]) ).
fof(f1588,plain,
( ! [X0] :
( m1_subset_1(k9_relat_1(sK4,X0),k1_zfmisc_1(u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4)))))
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4)))) )
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_13
| ~ spl34_14 ),
inference(forward_subsumption_resolution,[],[f1586,f1555]) ).
fof(f1589,plain,
( ! [X0] :
( v3_pre_topc(k9_relat_1(sK4,X0),k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ v3_pre_topc(X0,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v1_t_0topsp(sK4,sK2,k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ l1_pre_topc(sK2) )
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_8
| ~ spl34_13 ),
inference(forward_subsumption_resolution,[],[f1587,f1550]) ).
fof(f1590,plain,
( ! [X0] :
( m1_subset_1(k9_relat_1(sK4,X0),k1_zfmisc_1(u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4)))))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4)))) )
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_13
| ~ spl34_14 ),
inference(forward_subsumption_resolution,[],[f1588,f287]) ).
fof(f1591,plain,
( ! [X0] :
( v3_pre_topc(k9_relat_1(sK4,X0),k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ v3_pre_topc(X0,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v1_t_0topsp(sK4,sK2,k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4)))) )
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_8
| ~ spl34_13 ),
inference(forward_subsumption_resolution,[],[f1589,f279]) ).
fof(f1593,definition,
( spl34_83
<=> m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4)))) ),
introduced(definition,[new_symbols(definition,[spl34_83])],[avatar_definition]) ).
fof(f1597,definition,
( spl34_84
<=> v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4)))) ),
introduced(definition,[new_symbols(definition,[spl34_84])],[avatar_definition]) ).
fof(f1598,plain,
( v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ spl34_84 ),
inference(avatar_component_clause,[],[f1597]) ).
fof(f1601,definition,
( spl34_85
<=> ! [X0] : m1_subset_1(k9_relat_1(sK4,X0),k1_zfmisc_1(u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))) ),
introduced(definition,[new_symbols(definition,[spl34_85])],[avatar_definition]) ).
fof(f1602,plain,
( ! [X0] : m1_subset_1(k9_relat_1(sK4,X0),k1_zfmisc_1(u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4)))))
| ~ spl34_85 ),
inference(avatar_component_clause,[],[f1601]) ).
fof(f1603,plain,
( ~ spl34_83
| ~ spl34_84
| spl34_85
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_13
| ~ spl34_14 ),
inference(avatar_split_clause,[],[f1590,f660,f657,f588,f581,f562,f1601,f1597,f1593]) ).
fof(f1605,definition,
( spl34_86
<=> m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4)))) ),
introduced(definition,[new_symbols(definition,[spl34_86])],[avatar_definition]) ).
fof(f1606,plain,
( m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ spl34_86 ),
inference(avatar_component_clause,[],[f1605]) ).
fof(f1609,definition,
( spl34_87
<=> v1_t_0topsp(sK4,sK2,k3_pre_topc(sK3,k2_relat_1(sK4))) ),
introduced(definition,[new_symbols(definition,[spl34_87])],[avatar_definition]) ).
fof(f1611,plain,
( ~ v1_t_0topsp(sK4,sK2,k3_pre_topc(sK3,k2_relat_1(sK4)))
| spl34_87 ),
inference(avatar_component_clause,[],[f1609]) ).
fof(f1613,definition,
( spl34_88
<=> ! [X0] :
( v3_pre_topc(k9_relat_1(sK4,X0),k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v3_pre_topc(X0,sK2) ) ),
introduced(definition,[new_symbols(definition,[spl34_88])],[avatar_definition]) ).
fof(f1614,plain,
( ! [X0] :
( v3_pre_topc(k9_relat_1(sK4,X0),k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v3_pre_topc(X0,sK2) )
| ~ spl34_88 ),
inference(avatar_component_clause,[],[f1613]) ).
fof(f1615,plain,
( ~ spl34_86
| ~ spl34_84
| ~ spl34_87
| spl34_88
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_8
| ~ spl34_13 ),
inference(avatar_split_clause,[],[f1591,f657,f636,f588,f581,f562,f1613,f1609,f1597,f1605]) ).
fof(f1789,plain,
( spl34_87
| ~ spl34_2
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_7 ),
inference(avatar_split_clause,[],[f1563,f588,f581,f566,f562,f481,f1609]) ).
fof(f1801,plain,
( spl34_84
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_7 ),
inference(avatar_split_clause,[],[f1549,f588,f581,f566,f562,f1597]) ).
fof(f1814,plain,
( spl34_83
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_12 ),
inference(avatar_split_clause,[],[f1554,f653,f588,f581,f562,f1593]) ).
fof(f1821,plain,
( spl34_86
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_7 ),
inference(avatar_split_clause,[],[f1577,f588,f581,f566,f562,f1605]) ).
fof(f1932,plain,
( ~ m1_subset_1(sK6(sK2,sK3,sK4),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v3_pre_topc(sK6(sK2,sK3,sK4),sK2)
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| spl34_23
| ~ spl34_88 ),
inference(resolution,[],[f1614,f1562]) ).
fof(f1933,plain,
( ~ m1_subset_1(sK6(sK2,sK3,sK4),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| spl34_23
| ~ spl34_49
| ~ spl34_88 ),
inference(forward_subsumption_resolution,[],[f1932,f1194]) ).
fof(f1934,plain,
( ~ spl34_50
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| spl34_23
| ~ spl34_49
| ~ spl34_88 ),
inference(avatar_split_clause,[],[f1933,f1613,f1193,f738,f588,f581,f562,f1197]) ).
fof(f1936,plain,
( ~ m1_subset_1(k9_relat_1(sK4,sK6(sK2,sK3,sK4)),k1_zfmisc_1(u1_struct_0(k7_waybel18(sK2,sK3,sK4))))
| ~ spl34_3
| spl34_24 ),
inference(forward_demodulation,[],[f744,f602]) ).
fof(f1939,plain,
( ~ m1_subset_1(k9_relat_1(sK4,sK6(sK2,sK3,sK4)),k1_zfmisc_1(u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4)))))
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| spl34_24 ),
inference(forward_demodulation,[],[f1936,f791]) ).
fof(f1941,plain,
( $false
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| spl34_24
| ~ spl34_85 ),
inference(forward_subsumption_resolution,[],[f1939,f1602]) ).
fof(f1942,plain,
( ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| spl34_24
| ~ spl34_85 ),
inference(avatar_contradiction_clause,[],[f1941]) ).
fof(f1946,plain,
( ~ v1_t_0topsp(k8_waybel18(sK2,sK3,sK4),sK2,k3_pre_topc(sK3,k2_relat_1(sK4)))
| spl34_2
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7 ),
inference(forward_demodulation,[],[f482,f791]) ).
fof(f1949,plain,
( ~ v1_t_0topsp(sK4,sK2,k3_pre_topc(sK3,k2_relat_1(sK4)))
| spl34_2
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_7 ),
inference(forward_demodulation,[],[f1946,f568]) ).
fof(f1952,plain,
( ~ spl34_87
| spl34_2
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_7 ),
inference(avatar_split_clause,[],[f1949,f588,f581,f566,f562,f481,f1609]) ).
fof(f1963,plain,
( ! [X0] :
( ~ v3_pre_topc(X0,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v3_pre_topc(k4_pre_topc(sK2,sK3,sK4,X0),k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_pre_topc(sK3)
| ~ l1_pre_topc(sK3)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2) )
| ~ spl34_1 ),
inference(resolution,[],[f479,f348]) ).
fof(f1964,plain,
( ! [X0] :
( ~ v3_pre_topc(X0,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v3_pre_topc(k4_pre_topc(sK2,sK3,sK4,X0),k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_pre_topc(sK3)
| ~ l1_pre_topc(sK3)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2) )
| ~ spl34_1 ),
inference(forward_subsumption_resolution,[],[f1963,f287]) ).
fof(f1966,plain,
( ! [X0] :
( ~ v3_pre_topc(X0,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v3_pre_topc(k4_pre_topc(sK2,sK3,sK4,X0),k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_pre_topc(sK3)
| ~ l1_pre_topc(sK3)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2) )
| ~ spl34_1 ),
inference(forward_subsumption_resolution,[],[f1964,f286]) ).
fof(f1968,plain,
( ! [X0] :
( ~ v3_pre_topc(X0,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v3_pre_topc(k4_pre_topc(sK2,sK3,sK4,X0),k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))
| ~ v2_pre_topc(sK3)
| ~ l1_pre_topc(sK3)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2) )
| ~ spl34_1 ),
inference(forward_subsumption_resolution,[],[f1966,f285]) ).
fof(f1970,plain,
( ! [X0] :
( ~ v3_pre_topc(X0,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v3_pre_topc(k4_pre_topc(sK2,sK3,sK4,X0),k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))
| ~ l1_pre_topc(sK3)
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2) )
| ~ spl34_1 ),
inference(forward_subsumption_resolution,[],[f1968,f283]) ).
fof(f1972,plain,
( ! [X0] :
( ~ v3_pre_topc(X0,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v3_pre_topc(k4_pre_topc(sK2,sK3,sK4,X0),k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))
| ~ v2_pre_topc(sK2)
| ~ l1_pre_topc(sK2) )
| ~ spl34_1 ),
inference(forward_subsumption_resolution,[],[f1970,f282]) ).
fof(f1974,plain,
( ! [X0] :
( ~ v3_pre_topc(X0,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v3_pre_topc(k4_pre_topc(sK2,sK3,sK4,X0),k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4)))
| ~ l1_pre_topc(sK2) )
| ~ spl34_1 ),
inference(forward_subsumption_resolution,[],[f1972,f280]) ).
fof(f1976,plain,
( ! [X0] :
( ~ v3_pre_topc(X0,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2)))
| v3_pre_topc(k4_pre_topc(sK2,sK3,sK4,X0),k3_pre_topc(sK3,k1_yellow_2(sK2,sK3,sK4))) )
| ~ spl34_1 ),
inference(forward_subsumption_resolution,[],[f1974,f279]) ).
fof(f1978,plain,
( ! [X0] :
( v3_pre_topc(k4_pre_topc(sK2,sK3,sK4,X0),k7_waybel18(sK2,sK3,sK4))
| ~ v3_pre_topc(X0,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2))) )
| ~ spl34_1
| ~ spl34_3 ),
inference(forward_demodulation,[],[f1976,f602]) ).
fof(f1980,plain,
( ! [X0] :
( v3_pre_topc(k4_pre_topc(sK2,sK3,sK4,X0),k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ v3_pre_topc(X0,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2))) )
| ~ spl34_1
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7 ),
inference(forward_demodulation,[],[f1978,f791]) ).
fof(f1982,plain,
( ! [X0] :
( v3_pre_topc(k9_relat_1(sK4,X0),k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ v3_pre_topc(X0,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2))) )
| ~ spl34_1
| ~ spl34_3
| ~ spl34_5
| ~ spl34_6
| ~ spl34_7 ),
inference(forward_demodulation,[],[f1980,f586]) ).
fof(f1984,plain,
( spl34_88
| ~ spl34_1
| ~ spl34_3
| ~ spl34_5
| ~ spl34_6
| ~ spl34_7 ),
inference(avatar_split_clause,[],[f1982,f588,f585,f581,f562,f477,f1613]) ).
fof(f1994,plain,
( ~ v3_pre_topc(k4_pre_topc(sK2,k3_pre_topc(sK3,k2_relat_1(sK4)),sK4,sK5(sK2,k3_pre_topc(sK3,k2_relat_1(sK4)),sK4)),k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ l1_pre_topc(k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ l1_pre_topc(sK2)
| spl34_87 ),
inference(resolution,[],[f1611,f344]) ).
fof(f1995,plain,
( ~ v3_pre_topc(k4_pre_topc(sK2,k3_pre_topc(sK3,k2_relat_1(sK4)),sK4,sK5(sK2,k3_pre_topc(sK3,k2_relat_1(sK4)),sK4)),k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ l1_pre_topc(k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ l1_pre_topc(sK2)
| spl34_87 ),
inference(forward_subsumption_resolution,[],[f1994,f287]) ).
fof(f1996,plain,
( ~ v3_pre_topc(k4_pre_topc(sK2,k3_pre_topc(sK3,k2_relat_1(sK4)),sK4,sK5(sK2,k3_pre_topc(sK3,k2_relat_1(sK4)),sK4)),k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ l1_pre_topc(k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ l1_pre_topc(sK2)
| ~ spl34_84
| spl34_87 ),
inference(forward_subsumption_resolution,[],[f1995,f1598]) ).
fof(f1997,plain,
( ~ v3_pre_topc(k4_pre_topc(sK2,k3_pre_topc(sK3,k2_relat_1(sK4)),sK4,sK5(sK2,k3_pre_topc(sK3,k2_relat_1(sK4)),sK4)),k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ l1_pre_topc(k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ l1_pre_topc(sK2)
| ~ spl34_84
| ~ spl34_86
| spl34_87 ),
inference(forward_subsumption_resolution,[],[f1996,f1606]) ).
fof(f1998,plain,
( ~ v3_pre_topc(k4_pre_topc(sK2,k3_pre_topc(sK3,k2_relat_1(sK4)),sK4,sK5(sK2,k3_pre_topc(sK3,k2_relat_1(sK4)),sK4)),k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ l1_pre_topc(sK2)
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_8
| ~ spl34_84
| ~ spl34_86
| spl34_87 ),
inference(forward_subsumption_resolution,[],[f1997,f1550]) ).
fof(f1999,plain,
( ~ v3_pre_topc(k4_pre_topc(sK2,k3_pre_topc(sK3,k2_relat_1(sK4)),sK4,sK5(sK2,k3_pre_topc(sK3,k2_relat_1(sK4)),sK4)),k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_8
| ~ spl34_84
| ~ spl34_86
| spl34_87 ),
inference(forward_subsumption_resolution,[],[f1998,f279]) ).
fof(f2000,plain,
( ~ v3_pre_topc(k9_relat_1(sK4,sK5(sK2,k3_pre_topc(sK3,k2_relat_1(sK4)),sK4)),k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_8
| ~ spl34_13
| ~ spl34_84
| ~ spl34_86
| spl34_87 ),
inference(forward_demodulation,[],[f1999,f1582]) ).
fof(f2371,plain,
( ~ m1_subset_1(sK5(sK2,k3_pre_topc(sK3,k2_relat_1(sK4)),sK4),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ v3_pre_topc(sK5(sK2,k3_pre_topc(sK3,k2_relat_1(sK4)),sK4),sK2)
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_8
| ~ spl34_13
| ~ spl34_84
| ~ spl34_86
| spl34_87
| ~ spl34_88 ),
inference(resolution,[],[f2000,f1614]) ).
fof(f2375,definition,
( spl34_149
<=> v3_pre_topc(sK5(sK2,k3_pre_topc(sK3,k2_relat_1(sK4)),sK4),sK2) ),
introduced(definition,[new_symbols(definition,[spl34_149])],[avatar_definition]) ).
fof(f2377,plain,
( ~ v3_pre_topc(sK5(sK2,k3_pre_topc(sK3,k2_relat_1(sK4)),sK4),sK2)
| spl34_149 ),
inference(avatar_component_clause,[],[f2375]) ).
fof(f2379,definition,
( spl34_150
<=> m1_subset_1(sK5(sK2,k3_pre_topc(sK3,k2_relat_1(sK4)),sK4),k1_zfmisc_1(u1_struct_0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl34_150])],[avatar_definition]) ).
fof(f2381,plain,
( ~ m1_subset_1(sK5(sK2,k3_pre_topc(sK3,k2_relat_1(sK4)),sK4),k1_zfmisc_1(u1_struct_0(sK2)))
| spl34_150 ),
inference(avatar_component_clause,[],[f2379]) ).
fof(f2382,plain,
( ~ spl34_149
| ~ spl34_150
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_8
| ~ spl34_13
| ~ spl34_84
| ~ spl34_86
| spl34_87
| ~ spl34_88 ),
inference(avatar_split_clause,[],[f2371,f1613,f1609,f1605,f1597,f657,f636,f588,f581,f562,f2379,f2375]) ).
fof(f2970,plain,
( v1_t_0topsp(sK4,sK2,k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ l1_pre_topc(k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ l1_pre_topc(sK2)
| spl34_149 ),
inference(resolution,[],[f2377,f343]) ).
fof(f2973,plain,
( ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ l1_pre_topc(k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ l1_pre_topc(sK2)
| spl34_87
| spl34_149 ),
inference(forward_subsumption_resolution,[],[f2970,f1611]) ).
fof(f2975,plain,
( ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ l1_pre_topc(k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ l1_pre_topc(sK2)
| spl34_87
| spl34_149 ),
inference(forward_subsumption_resolution,[],[f2973,f287]) ).
fof(f2981,plain,
( ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ l1_pre_topc(k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ l1_pre_topc(sK2)
| ~ spl34_84
| spl34_87
| spl34_149 ),
inference(forward_subsumption_resolution,[],[f2975,f1598]) ).
fof(f2982,plain,
( ~ l1_pre_topc(k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ l1_pre_topc(sK2)
| ~ spl34_84
| ~ spl34_86
| spl34_87
| spl34_149 ),
inference(forward_subsumption_resolution,[],[f2981,f1606]) ).
fof(f2983,plain,
( ~ l1_pre_topc(sK2)
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_8
| ~ spl34_84
| ~ spl34_86
| spl34_87
| spl34_149 ),
inference(forward_subsumption_resolution,[],[f2982,f1550]) ).
fof(f2984,plain,
( $false
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_8
| ~ spl34_84
| ~ spl34_86
| spl34_87
| spl34_149 ),
inference(forward_subsumption_resolution,[],[f2983,f279]) ).
fof(f2985,plain,
( ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_8
| ~ spl34_84
| ~ spl34_86
| spl34_87
| spl34_149 ),
inference(avatar_contradiction_clause,[],[f2984]) ).
fof(f3108,plain,
( v1_t_0topsp(sK4,sK2,k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ l1_pre_topc(k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ l1_pre_topc(sK2)
| spl34_150 ),
inference(resolution,[],[f2381,f342]) ).
fof(f3112,plain,
( ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ l1_pre_topc(k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ l1_pre_topc(sK2)
| spl34_87
| spl34_150 ),
inference(forward_subsumption_resolution,[],[f3108,f1611]) ).
fof(f3113,plain,
( ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ l1_pre_topc(k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ l1_pre_topc(sK2)
| spl34_87
| spl34_150 ),
inference(forward_subsumption_resolution,[],[f3112,f287]) ).
fof(f3114,plain,
( ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(k3_pre_topc(sK3,k2_relat_1(sK4))))
| ~ l1_pre_topc(k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ l1_pre_topc(sK2)
| ~ spl34_84
| spl34_87
| spl34_150 ),
inference(forward_subsumption_resolution,[],[f3113,f1598]) ).
fof(f3115,plain,
( ~ l1_pre_topc(k3_pre_topc(sK3,k2_relat_1(sK4)))
| ~ l1_pre_topc(sK2)
| ~ spl34_84
| ~ spl34_86
| spl34_87
| spl34_150 ),
inference(forward_subsumption_resolution,[],[f3114,f1606]) ).
fof(f3116,plain,
( ~ l1_pre_topc(sK2)
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_8
| ~ spl34_84
| ~ spl34_86
| spl34_87
| spl34_150 ),
inference(forward_subsumption_resolution,[],[f3115,f1550]) ).
fof(f3117,plain,
( $false
| ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_8
| ~ spl34_84
| ~ spl34_86
| spl34_87
| spl34_150 ),
inference(forward_subsumption_resolution,[],[f3116,f279]) ).
fof(f3118,plain,
( ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_8
| ~ spl34_84
| ~ spl34_86
| spl34_87
| spl34_150 ),
inference(avatar_contradiction_clause,[],[f3117]) ).
cnf(s1,plain,
( spl34_1
| spl34_2 ),
inference(sat_conversion,[],[f484]) ).
cnf(s2,plain,
( ~ spl34_1
| ~ spl34_2 ),
inference(sat_conversion,[],[f485]) ).
cnf(s3,plain,
( ~ spl34_3
| spl34_4 ),
inference(sat_conversion,[],[f569]) ).
cnf(s4,plain,
spl34_3,
inference(sat_conversion,[],[f572]) ).
cnf(s5,plain,
( ~ spl34_3
| ~ spl34_5
| spl34_6
| ~ spl34_7 ),
inference(sat_conversion,[],[f591]) ).
cnf(s6,plain,
spl34_5,
inference(sat_conversion,[],[f594]) ).
cnf(s7,plain,
spl34_7,
inference(sat_conversion,[],[f597]) ).
cnf(s9,plain,
( ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_12
| spl34_13
| ~ spl34_14 ),
inference(sat_conversion,[],[f663]) ).
cnf(s13,plain,
( ~ spl34_3
| ~ spl34_5
| spl34_8 ),
inference(sat_conversion,[],[f703]) ).
cnf(s15,plain,
( spl34_1
| ~ spl34_6
| ~ spl34_23
| ~ spl34_24 ),
inference(sat_conversion,[],[f745]) ).
cnf(s22,plain,
( ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| spl34_10 ),
inference(sat_conversion,[],[f834]) ).
cnf(s24,plain,
( ~ spl34_10
| spl34_12 ),
inference(sat_conversion,[],[f849]) ).
cnf(s26,plain,
( ~ spl34_8
| spl34_14 ),
inference(sat_conversion,[],[f856]) ).
cnf(s52,plain,
( spl34_1
| spl34_49 ),
inference(sat_conversion,[],[f1219]) ).
cnf(s63,plain,
( spl34_1
| spl34_50 ),
inference(sat_conversion,[],[f1436]) ).
cnf(s73,plain,
( ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_13
| ~ spl34_14
| ~ spl34_83
| ~ spl34_84
| spl34_85 ),
inference(sat_conversion,[],[f1603]) ).
cnf(s74,plain,
( ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_8
| ~ spl34_13
| ~ spl34_84
| ~ spl34_86
| ~ spl34_87
| spl34_88 ),
inference(sat_conversion,[],[f1615]) ).
cnf(s90,plain,
( ~ spl34_2
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_7
| spl34_87 ),
inference(sat_conversion,[],[f1789]) ).
cnf(s92,plain,
( ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_7
| spl34_84 ),
inference(sat_conversion,[],[f1801]) ).
cnf(s96,plain,
( ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_12
| spl34_83 ),
inference(sat_conversion,[],[f1814]) ).
cnf(s97,plain,
( ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_7
| spl34_86 ),
inference(sat_conversion,[],[f1821]) ).
cnf(s106,plain,
( ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| spl34_23
| ~ spl34_49
| ~ spl34_50
| ~ spl34_88 ),
inference(sat_conversion,[],[f1934]) ).
cnf(s107,plain,
( ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| spl34_24
| ~ spl34_85 ),
inference(sat_conversion,[],[f1942]) ).
cnf(s108,plain,
( spl34_2
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_7
| ~ spl34_87 ),
inference(sat_conversion,[],[f1952]) ).
cnf(s110,plain,
( ~ spl34_1
| ~ spl34_3
| ~ spl34_5
| ~ spl34_6
| ~ spl34_7
| spl34_88 ),
inference(sat_conversion,[],[f1984]) ).
cnf(s151,plain,
( ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_8
| ~ spl34_13
| ~ spl34_84
| ~ spl34_86
| spl34_87
| ~ spl34_88
| ~ spl34_149
| ~ spl34_150 ),
inference(sat_conversion,[],[f2382]) ).
cnf(s189,plain,
( ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_8
| ~ spl34_84
| ~ spl34_86
| spl34_87
| spl34_149 ),
inference(sat_conversion,[],[f2985]) ).
cnf(s200,plain,
( ~ spl34_3
| ~ spl34_5
| ~ spl34_7
| ~ spl34_8
| ~ spl34_84
| ~ spl34_86
| spl34_87
| spl34_150 ),
inference(sat_conversion,[],[f3118]) ).
cnf(s247,plain,
( ~ spl34_3
| spl34_6 ),
inference(rat,[],[s5,s7,s6]) ).
cnf(s250,plain,
spl34_8,
inference(rat,[],[s13,s6,s4]) ).
cnf(s251,plain,
spl34_6,
inference(rat,[],[s247,s4]) ).
cnf(s255,plain,
spl34_14,
inference(rat,[],[s26,s250]) ).
cnf(s256,plain,
spl34_4,
inference(rat,[],[s3,s4]) ).
cnf(s257,plain,
spl34_86,
inference(rat,[],[s97,s4,s7,s6,s256]) ).
cnf(s258,plain,
spl34_84,
inference(rat,[],[s92,s4,s7,s6,s256]) ).
cnf(s259,plain,
spl34_10,
inference(rat,[],[s22,s4,s6,s256]) ).
cnf(s260,plain,
spl34_12,
inference(rat,[],[s24,s259]) ).
cnf(s262,plain,
spl34_83,
inference(rat,[],[s96,s4,s6,s7,s260]) ).
cnf(s263,plain,
spl34_13,
inference(rat,[],[s9,s255,s256,s4,s6,s260]) ).
cnf(s266,plain,
spl34_85,
inference(rat,[],[s73,s262,s258,s255,s4,s6,s7,s263]) ).
cnf(s270,plain,
spl34_24,
inference(rat,[],[s107,s4,s6,s7,s266]) ).
cnf(s276,plain,
spl34_1,
inference(rat,[],[s74,s90,s106,s1,s15,s52,s63,s7,s6,s4,s250,s257,s258,s263,s256,s251,s270]) ).
cnf(s277,plain,
spl34_88,
inference(rat,[],[s110,s251,s7,s4,s6,s276]) ).
cnf(s278,plain,
~ spl34_2,
inference(rat,[],[s2,s276]) ).
cnf(s279,plain,
~ spl34_87,
inference(rat,[],[s108,s256,s7,s6,s4,s278]) ).
cnf(s280,plain,
spl34_150,
inference(rat,[],[s200,s258,s257,s250,s4,s6,s7,s279]) ).
cnf(s281,plain,
spl34_149,
inference(rat,[],[s189,s258,s257,s250,s4,s6,s7,s279]) ).
cnf(s282,plain,
$false,
inference(rat,[],[s151,s280,s277,s263,s258,s257,s250,s4,s6,s7,s281,s279]) ).
fof(f3119,plain,
$false,
inference(avatar_sat_refutation,[],[s282]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT363+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n009.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 15:02:14 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.41 Running first-order theorem proving
% 0.13/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.20/1.36 % (2127567)Detected formulas, will run a generic FOF schedule.
% 3.20/1.36 % (2127574)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=3520905077:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.20/1.36 % (2127575)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1393437519:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.20/1.36 % (2127576)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=743840270:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.20/1.36 % (2127573)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=3643637604:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.20/1.36 % (2127572)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=2668752807:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.20/1.36 % (2127578)dis-21_1_sil=8000:lcm=predicate:random_seed=1827408293:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 3.20/1.36 % (2127577)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2774227025:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.20/1.36 % (2127575)Refutation not found, incomplete strategy
% 3.20/1.36 % (2127575)------------------------------
% 3.20/1.36 % (2127575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.20/1.36 % (2127575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.20/1.36 % (2127575)CaDiCaL version: 2.1.3
% 3.20/1.36 % (2127575)Termination reason: Refutation not found, incomplete strategy
% 3.20/1.36 % (2127575)Time elapsed: 0.004 s
% 3.20/1.36 % (2127575)Peak memory usage: 88 MB
% 3.20/1.36 % (2127575)Instructions burned: 5 (million)
% 3.20/1.36 % (2127576)Instruction limit reached!
% 3.20/1.36 % (2127576)------------------------------
% 3.20/1.36 % (2127576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.20/1.36 % (2127576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.20/1.36 % (2127576)CaDiCaL version: 2.1.3
% 3.20/1.36 % (2127576)Termination reason: Instruction limit
% 3.20/1.36 % (2127576)Termination phase: Saturation
% 3.20/1.36 % (2127576)Time elapsed: 0.062 s
% 3.20/1.36 % (2127576)Peak memory usage: 88 MB
% 3.20/1.36 % (2127576)Instructions burned: 120 (million)
% 3.20/1.36 % (2127577)First to succeed.
% 3.20/1.36 % (2127577)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2127567"
% 3.20/1.36 % (2127578)Instruction limit reached!
% 3.20/1.36 % (2127578)------------------------------
% 3.20/1.36 % (2127578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.20/1.36 % (2127578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.20/1.36 % (2127578)CaDiCaL version: 2.1.3
% 3.20/1.36 % (2127578)Termination reason: Instruction limit
% 3.20/1.36 % (2127578)Termination phase: Saturation
% 3.20/1.36 % (2127578)Time elapsed: 0.077 s
% 3.20/1.36 % (2127578)Peak memory usage: 93 MB
% 3.20/1.36 % (2127578)Instructions burned: 129 (million)
% 3.20/1.36 % (2127586)lrs+10_1_sil=8000:sp=occurrence:random_seed=279921746:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 3.20/1.36 % (2127587)lrs+10_1_sil=32000:urr=on:br=off:random_seed=910772387:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 3.20/1.36 % (2127587)Refutation not found, incomplete strategy
% 3.20/1.36 % (2127587)------------------------------
% 3.20/1.36 % (2127587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.20/1.36 % (2127587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.20/1.36 % (2127587)CaDiCaL version: 2.1.3
% 3.20/1.36 % (2127587)Termination reason: Refutation not found, incomplete strategy
% 3.20/1.36 % (2127587)Time elapsed: 0.004 s
% 3.20/1.36 % (2127587)Peak memory usage: 89 MB
% 3.20/1.36 % (2127587)Instructions burned: 5 (million)
% 3.20/1.36 % (2127575)------------------------------
% 3.20/1.36 % (2127575)------------------------------
% 3.20/1.36 % (2127577)Refutation found. Thanks to Tanya!
% 3.20/1.36 % SZS status Theorem for theBenchmark
% 3.20/1.36 % SZS output start Proof for theBenchmark
% See solution above
% 4.03/1.45 % (2127577)------------------------------
% 4.03/1.45 % (2127577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.03/1.45 % (2127577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.03/1.45 % (2127577)CaDiCaL version: 2.1.3
% 4.03/1.45 % (2127577)Termination reason: Refutation
% 4.03/1.45 % (2127577)Time elapsed: 0.072 s
% 4.03/1.45 % (2127577)Peak memory usage: 91 MB
% 4.03/1.45 % (2127577)Instructions burned: 104 (million)
% 4.03/1.45 % (2127577)------------------------------
% 4.03/1.45 % (2127577)------------------------------
% 4.03/1.45 % (2127567)Success in time 0.502 s
% 4.03/1.45 % Vampire exiting
%------------------------------------------------------------------------------