%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRP621+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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 10:18:15 AM UTC 2026
% Result : Theorem 6.12s 3.64s
% Output : Refutation 6.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 25
% Syntax : Number of formulae : 288 ( 22 unt; 8 def)
% Number of atoms : 2079 ( 37 equ)
% Maximal formula atoms : 27 ( 7 avg)
% Number of connectives : 3097 (1306 ~;1574 |; 159 &)
% ( 23 <=>; 35 =>; 0 <=; 0 <~>)
% Maximal formula depth : 29 ( 9 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 30 ( 28 usr; 9 prp; 0-4 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-5 aty)
% Number of variables : 265 ( 0 sgn 259 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
=> ! [X2] :
( m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
=> m2_fraenkel(k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X2,X1),u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_autgroup) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
=> ! [X2] :
( m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
=> m2_fraenkel(k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X2,X1),u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f13,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0))
=> ( X1 = k1_autgroup(X0)
<=> ( ! [X2] :
( m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),X1)
=> ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X2,X0,X0)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) ) )
& ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X2,X0,X0)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( r2_hidden(X2,X1)
<=> ( v2_funct_1(X2)
& v3_group_6(X2,X0,X0) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_autgroup) ).
fof(f15,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> m1_fraenkel(k1_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_autgroup) ).
fof(f20,axiom,
! [X0,X1,X2,X3,X4] :
( ( ~ v1_xboole_0(X1)
& v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m1_relset_1(X3,X0,X1)
& v1_funct_1(X4)
& v1_funct_2(X4,X1,X2)
& m1_relset_1(X4,X1,X2) )
=> ( v1_funct_1(k7_funct_2(X0,X1,X2,X3,X4))
& v1_funct_2(k7_funct_2(X0,X1,X2,X3,X4),X0,X2)
& m2_relset_1(k7_funct_2(X0,X1,X2,X3,X4),X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k7_funct_2) ).
fof(f21,axiom,
! [X0,X1,X2,X3,X4] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1)
& ~ v3_struct_0(X2)
& v3_group_1(X2)
& v4_group_1(X2)
& l1_group_1(X2)
& v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X3,X0,X1)
& m1_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X4)
& v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
& v1_group_6(X4,X1,X2)
& m1_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) )
=> ( v1_funct_1(k8_group_6(X0,X1,X2,X3,X4))
& v1_funct_2(k8_group_6(X0,X1,X2,X3,X4),u1_struct_0(X0),u1_struct_0(X2))
& v1_group_6(k8_group_6(X0,X1,X2,X3,X4),X0,X2)
& m2_relset_1(k8_group_6(X0,X1,X2,X3,X4),u1_struct_0(X0),u1_struct_0(X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k8_group_6) ).
fof(f22,axiom,
! [X0] :
( l1_group_1(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_group_1) ).
fof(f24,axiom,
! [X0,X1,X2] :
( m1_fraenkel(X2,X0,X1)
=> ( ~ v1_xboole_0(X2)
& v1_fraenkel(X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_fraenkel) ).
fof(f27,axiom,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X1)
& m1_fraenkel(X2,X0,X1) )
=> ! [X3] :
( m2_fraenkel(X3,X0,X1,X2)
=> ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m2_relset_1(X3,X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_fraenkel) ).
fof(f40,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f58,axiom,
! [X0,X1,X2,X3,X4] :
( ( ~ v1_xboole_0(X1)
& v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m1_relset_1(X3,X0,X1)
& v1_funct_1(X4)
& v1_funct_2(X4,X1,X2)
& m1_relset_1(X4,X1,X2) )
=> k7_funct_2(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k7_funct_2) ).
fof(f59,axiom,
! [X0,X1,X2,X3,X4] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1)
& ~ v3_struct_0(X2)
& v3_group_1(X2)
& v4_group_1(X2)
& l1_group_1(X2)
& v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X3,X0,X1)
& m1_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X4)
& v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
& v1_group_6(X4,X1,X2)
& m1_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) )
=> k8_group_6(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k8_group_6) ).
fof(f60,axiom,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X1)
& m1_fraenkel(X2,X0,X1) )
=> ! [X3] :
( m2_fraenkel(X3,X0,X1,X2)
<=> m1_subset_1(X3,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_fraenkel) ).
fof(f61,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(f63,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_subset) ).
fof(f64,axiom,
! [X0,X1] :
( m1_subset_1(X0,X1)
=> ( v1_xboole_0(X1)
| r2_hidden(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_subset) ).
fof(f67,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X1,X0,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( r2_hidden(X1,k1_autgroup(X0))
<=> v4_group_6(X1,X0,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_autgroup) ).
fof(f70,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& v3_group_1(X2)
& v4_group_1(X2)
& l1_group_1(X2) )
=> ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X3,X0,X1)
& m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
=> ! [X4] :
( ( v1_funct_1(X4)
& v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
& v1_group_6(X4,X1,X2)
& m2_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) )
=> ( ( v4_group_6(X3,X0,X1)
& v4_group_6(X4,X1,X2) )
=> v4_group_6(k8_group_6(X0,X1,X2,X3,X4),X0,X2) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t74_group_6) ).
fof(f73,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0))
=> ( X1 = k1_autgroup(X0)
<=> ( ! [X2] :
( m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),X1)
=> ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X2,X0,X0)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) ) )
& ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X3,X0,X0)
& m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( r2_hidden(X3,X1)
<=> ( v2_funct_1(X3)
& v3_group_6(X3,X0,X0) ) ) ) ) ) ) ),
inference(rectify,[],[f13]) ).
fof(f78,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ m2_fraenkel(k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X2,X1),u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
& m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) )
& m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) )
& ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f79,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ m2_fraenkel(k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X2,X1),u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
& m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) )
& m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) )
& ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(flattening,[],[f78]) ).
fof(f96,plain,
! [X0] :
( ! [X1] :
( ( X1 = k1_autgroup(X0)
<=> ( ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X2,X0,X0)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),X1) )
& ! [X3] :
( ( r2_hidden(X3,X1)
<=> ( v2_funct_1(X3)
& v3_group_6(X3,X0,X0) ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(X3,X0,X0)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X0)) ) ) )
| ~ m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f73]) ).
fof(f97,plain,
! [X0] :
( ! [X1] :
( ( X1 = k1_autgroup(X0)
<=> ( ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X2,X0,X0)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),X1) )
& ! [X3] :
( ( r2_hidden(X3,X1)
<=> ( v2_funct_1(X3)
& v3_group_6(X3,X0,X0) ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(X3,X0,X0)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X0)) ) ) )
| ~ m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f96]) ).
fof(f100,plain,
! [X0] :
( m1_fraenkel(k1_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f101,plain,
! [X0] :
( m1_fraenkel(k1_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f100]) ).
fof(f104,plain,
! [X0,X1,X2,X3,X4] :
( ( v1_funct_1(k7_funct_2(X0,X1,X2,X3,X4))
& v1_funct_2(k7_funct_2(X0,X1,X2,X3,X4),X0,X2)
& m2_relset_1(k7_funct_2(X0,X1,X2,X3,X4),X0,X2) )
| v1_xboole_0(X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,X1,X2)
| ~ m1_relset_1(X4,X1,X2) ),
inference(ennf_transformation,[],[f20]) ).
fof(f105,plain,
! [X0,X1,X2,X3,X4] :
( ( v1_funct_1(k7_funct_2(X0,X1,X2,X3,X4))
& v1_funct_2(k7_funct_2(X0,X1,X2,X3,X4),X0,X2)
& m2_relset_1(k7_funct_2(X0,X1,X2,X3,X4),X0,X2) )
| v1_xboole_0(X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,X1,X2)
| ~ m1_relset_1(X4,X1,X2) ),
inference(flattening,[],[f104]) ).
fof(f106,plain,
! [X0,X1,X2,X3,X4] :
( ( v1_funct_1(k8_group_6(X0,X1,X2,X3,X4))
& v1_funct_2(k8_group_6(X0,X1,X2,X3,X4),u1_struct_0(X0),u1_struct_0(X2))
& v1_group_6(k8_group_6(X0,X1,X2,X3,X4),X0,X2)
& m2_relset_1(k8_group_6(X0,X1,X2,X3,X4),u1_struct_0(X0),u1_struct_0(X2)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| ~ m1_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_group_6(X4,X1,X2)
| ~ m1_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(ennf_transformation,[],[f21]) ).
fof(f107,plain,
! [X0,X1,X2,X3,X4] :
( ( v1_funct_1(k8_group_6(X0,X1,X2,X3,X4))
& v1_funct_2(k8_group_6(X0,X1,X2,X3,X4),u1_struct_0(X0),u1_struct_0(X2))
& v1_group_6(k8_group_6(X0,X1,X2,X3,X4),X0,X2)
& m2_relset_1(k8_group_6(X0,X1,X2,X3,X4),u1_struct_0(X0),u1_struct_0(X2)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| ~ m1_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_group_6(X4,X1,X2)
| ~ m1_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(flattening,[],[f106]) ).
fof(f108,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f22]) ).
fof(f109,plain,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X2)
& v1_fraenkel(X2) )
| ~ m1_fraenkel(X2,X0,X1) ),
inference(ennf_transformation,[],[f24]) ).
fof(f110,plain,
! [X0,X1,X2] :
( ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m2_relset_1(X3,X0,X1) )
| ~ m2_fraenkel(X3,X0,X1,X2) )
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(ennf_transformation,[],[f27]) ).
fof(f111,plain,
! [X0,X1,X2] :
( ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m2_relset_1(X3,X0,X1) )
| ~ m2_fraenkel(X3,X0,X1,X2) )
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(flattening,[],[f110]) ).
fof(f120,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f40]) ).
fof(f121,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f120]) ).
fof(f128,plain,
! [X0,X1,X2,X3,X4] :
( k7_funct_2(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4)
| v1_xboole_0(X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,X1,X2)
| ~ m1_relset_1(X4,X1,X2) ),
inference(ennf_transformation,[],[f58]) ).
fof(f129,plain,
! [X0,X1,X2,X3,X4] :
( k7_funct_2(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4)
| v1_xboole_0(X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,X1,X2)
| ~ m1_relset_1(X4,X1,X2) ),
inference(flattening,[],[f128]) ).
fof(f130,plain,
! [X0,X1,X2,X3,X4] :
( k8_group_6(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| ~ m1_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_group_6(X4,X1,X2)
| ~ m1_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(ennf_transformation,[],[f59]) ).
fof(f131,plain,
! [X0,X1,X2,X3,X4] :
( k8_group_6(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| ~ m1_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_group_6(X4,X1,X2)
| ~ m1_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(flattening,[],[f130]) ).
fof(f132,plain,
! [X0,X1,X2] :
( ! [X3] :
( m2_fraenkel(X3,X0,X1,X2)
<=> m1_subset_1(X3,X2) )
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(ennf_transformation,[],[f60]) ).
fof(f133,plain,
! [X0,X1,X2] :
( ! [X3] :
( m2_fraenkel(X3,X0,X1,X2)
<=> m1_subset_1(X3,X2) )
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(flattening,[],[f132]) ).
fof(f134,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f63]) ).
fof(f135,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(ennf_transformation,[],[f64]) ).
fof(f136,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(flattening,[],[f135]) ).
fof(f140,plain,
! [X0] :
( ! [X1] :
( ( r2_hidden(X1,k1_autgroup(X0))
<=> v4_group_6(X1,X0,X0) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(X1,X0,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f67]) ).
fof(f141,plain,
! [X0] :
( ! [X1] :
( ( r2_hidden(X1,k1_autgroup(X0))
<=> v4_group_6(X1,X0,X0) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(X1,X0,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f140]) ).
fof(f144,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( v4_group_6(k8_group_6(X0,X1,X2,X3,X4),X0,X2)
| ~ v4_group_6(X3,X0,X1)
| ~ v4_group_6(X4,X1,X2)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_group_6(X4,X1,X2)
| ~ m2_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2) )
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f70]) ).
fof(f145,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( v4_group_6(k8_group_6(X0,X1,X2,X3,X4),X0,X2)
| ~ v4_group_6(X3,X0,X1)
| ~ v4_group_6(X4,X1,X2)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_group_6(X4,X1,X2)
| ~ m2_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2) )
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f144]) ).
fof(f148,plain,
m2_fraenkel(sK2,u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0)),
inference(cnf_transformation,[],[f79]) ).
fof(f149,plain,
~ m2_fraenkel(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),sK2,sK1),u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0)),
inference(cnf_transformation,[],[f79]) ).
fof(f150,plain,
m2_fraenkel(sK1,u1_struct_0(sK0),u1_struct_0(sK0),k1_autgroup(sK0)),
inference(cnf_transformation,[],[f79]) ).
fof(f151,plain,
l1_group_1(sK0),
inference(cnf_transformation,[],[f79]) ).
fof(f152,plain,
v4_group_1(sK0),
inference(cnf_transformation,[],[f79]) ).
fof(f153,plain,
v3_group_1(sK0),
inference(cnf_transformation,[],[f79]) ).
fof(f154,plain,
v1_group_1(sK0),
inference(cnf_transformation,[],[f79]) ).
fof(f155,plain,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f79]) ).
fof(f181,plain,
! [X2,X0,X1] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0)
| ~ m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),X1)
| v1_group_6(X2,X0,X0)
| k1_autgroup(X0) != X1 ),
inference(cnf_transformation,[],[f97]) ).
fof(f190,plain,
! [X0] :
( m1_fraenkel(k1_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f101]) ).
fof(f192,plain,
! [X2,X3,X0,X1,X4] :
( m2_relset_1(k7_funct_2(X0,X1,X2,X3,X4),X0,X2)
| ~ v1_funct_2(X4,X1,X2)
| ~ v1_funct_1(X4)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_2(X3,X0,X1)
| ~ v1_funct_1(X3)
| v1_xboole_0(X1)
| ~ m1_relset_1(X4,X1,X2) ),
inference(cnf_transformation,[],[f105]) ).
fof(f193,plain,
! [X2,X3,X0,X1,X4] :
( v1_funct_2(k7_funct_2(X0,X1,X2,X3,X4),X0,X2)
| ~ v1_funct_2(X4,X1,X2)
| ~ v1_funct_1(X4)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_2(X3,X0,X1)
| ~ v1_funct_1(X3)
| v1_xboole_0(X1)
| ~ m1_relset_1(X4,X1,X2) ),
inference(cnf_transformation,[],[f105]) ).
fof(f194,plain,
! [X2,X3,X0,X1,X4] :
( v1_funct_1(k7_funct_2(X0,X1,X2,X3,X4))
| ~ v1_funct_2(X4,X1,X2)
| ~ v1_funct_1(X4)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_2(X3,X0,X1)
| ~ v1_funct_1(X3)
| v1_xboole_0(X1)
| ~ m1_relset_1(X4,X1,X2) ),
inference(cnf_transformation,[],[f105]) ).
fof(f196,plain,
! [X2,X3,X0,X1,X4] :
( v1_group_6(k8_group_6(X0,X1,X2,X3,X4),X0,X2)
| ~ v1_group_6(X4,X1,X2)
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_1(X4)
| ~ m1_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X3)
| ~ l1_group_1(X2)
| ~ v4_group_1(X2)
| ~ v3_group_1(X2)
| v3_struct_0(X2)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f107]) ).
fof(f199,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f108]) ).
fof(f201,plain,
! [X2,X0,X1] :
( ~ m1_fraenkel(X2,X0,X1)
| ~ v1_xboole_0(X2) ),
inference(cnf_transformation,[],[f109]) ).
fof(f202,plain,
! [X2,X3,X0,X1] :
( ~ m2_fraenkel(X3,X0,X1,X2)
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1)
| m2_relset_1(X3,X0,X1) ),
inference(cnf_transformation,[],[f111]) ).
fof(f203,plain,
! [X2,X3,X0,X1] :
( ~ m2_fraenkel(X3,X0,X1,X2)
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1)
| v1_funct_2(X3,X0,X1) ),
inference(cnf_transformation,[],[f111]) ).
fof(f204,plain,
! [X2,X3,X0,X1] :
( ~ m2_fraenkel(X3,X0,X1,X2)
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1)
| v1_funct_1(X3) ),
inference(cnf_transformation,[],[f111]) ).
fof(f220,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f121]) ).
fof(f268,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_relset_1(X4,X1,X2)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,X1,X2)
| ~ v1_funct_2(X3,X0,X1)
| ~ v1_funct_1(X3)
| v1_xboole_0(X1)
| k7_funct_2(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4) ),
inference(cnf_transformation,[],[f129]) ).
fof(f269,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ m1_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_1(X4)
| ~ v1_group_6(X4,X1,X2)
| ~ v1_group_6(X3,X0,X1)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X3)
| ~ l1_group_1(X2)
| ~ v4_group_1(X2)
| ~ v3_group_1(X2)
| v3_struct_0(X2)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| k8_group_6(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4) ),
inference(cnf_transformation,[],[f131]) ).
fof(f270,plain,
! [X2,X3,X0,X1] :
( m2_fraenkel(X3,X0,X1,X2)
| v1_xboole_0(X1)
| ~ m1_subset_1(X3,X2)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
fof(f271,plain,
! [X2,X3,X0,X1] :
( ~ m2_fraenkel(X3,X0,X1,X2)
| v1_xboole_0(X1)
| m1_subset_1(X3,X2)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
fof(f273,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f61]) ).
fof(f275,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f134]) ).
fof(f276,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,X1)
| r2_hidden(X0,X1)
| v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f136]) ).
fof(f279,plain,
! [X0,X1] :
( ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0)
| ~ l1_group_1(X0)
| ~ v1_group_6(X1,X0,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ v4_group_6(X1,X0,X0)
| r2_hidden(X1,k1_autgroup(X0)) ),
inference(cnf_transformation,[],[f141]) ).
fof(f280,plain,
! [X0,X1] :
( ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0)
| ~ l1_group_1(X0)
| ~ v1_group_6(X1,X0,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| v4_group_6(X1,X0,X0)
| ~ r2_hidden(X1,k1_autgroup(X0)) ),
inference(cnf_transformation,[],[f141]) ).
fof(f283,plain,
! [X2,X3,X0,X1,X4] :
( v4_group_6(k8_group_6(X0,X1,X2,X3,X4),X0,X2)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ l1_group_1(X2)
| ~ v4_group_1(X2)
| ~ v3_group_1(X2)
| v3_struct_0(X2)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_group_6(X4,X1,X2)
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_1(X4)
| ~ v4_group_6(X4,X1,X2)
| ~ v4_group_6(X3,X0,X1)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f145]) ).
fof(f288,plain,
! [X2,X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0)
| ~ m1_fraenkel(k1_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| v1_group_6(X2,X0,X0) ),
inference(equality_resolution,[],[f181]) ).
fof(f297,plain,
! [X2,X0] :
( ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0)
| ~ l1_group_1(X0)
| v1_group_6(X2,X0,X0) ),
inference(forward_subsumption_resolution,[],[f288,f190]) ).
fof(f401,plain,
( v1_xboole_0(u1_struct_0(sK0))
| ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| v1_funct_1(sK2) ),
inference(resolution,[],[f204,f148]) ).
fof(f402,plain,
( v1_xboole_0(u1_struct_0(sK0))
| ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| v1_funct_1(sK1) ),
inference(resolution,[],[f204,f150]) ).
fof(f404,definition,
( spl27_1
<=> v1_funct_1(sK1) ),
introduced(definition,[new_symbols(definition,[spl27_1])],[avatar_definition]) ).
fof(f406,plain,
( v1_funct_1(sK1)
| ~ spl27_1 ),
inference(avatar_component_clause,[],[f404]) ).
fof(f408,definition,
( spl27_2
<=> m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0)) ),
introduced(definition,[new_symbols(definition,[spl27_2])],[avatar_definition]) ).
fof(f409,plain,
( m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_2 ),
inference(avatar_component_clause,[],[f408]) ).
fof(f410,plain,
( ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| spl27_2 ),
inference(avatar_component_clause,[],[f408]) ).
fof(f412,definition,
( spl27_3
<=> v1_xboole_0(u1_struct_0(sK0)) ),
introduced(definition,[new_symbols(definition,[spl27_3])],[avatar_definition]) ).
fof(f413,plain,
( ~ v1_xboole_0(u1_struct_0(sK0))
| spl27_3 ),
inference(avatar_component_clause,[],[f412]) ).
fof(f414,plain,
( v1_xboole_0(u1_struct_0(sK0))
| ~ spl27_3 ),
inference(avatar_component_clause,[],[f412]) ).
fof(f415,plain,
( spl27_1
| ~ spl27_2
| spl27_3 ),
inference(avatar_split_clause,[],[f402,f412,f408,f404]) ).
fof(f417,definition,
( spl27_4
<=> v1_funct_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl27_4])],[avatar_definition]) ).
fof(f419,plain,
( v1_funct_1(sK2)
| ~ spl27_4 ),
inference(avatar_component_clause,[],[f417]) ).
fof(f420,plain,
( spl27_4
| ~ spl27_2
| spl27_3 ),
inference(avatar_split_clause,[],[f401,f412,f408,f417]) ).
fof(f431,plain,
( v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),sK2,sK1),k1_autgroup(sK0))
| ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolution,[],[f270,f149]) ).
fof(f434,plain,
( v1_xboole_0(u1_struct_0(sK0))
| m1_subset_1(sK2,k1_autgroup(sK0))
| ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolution,[],[f271,f148]) ).
fof(f435,plain,
( v1_xboole_0(u1_struct_0(sK0))
| m1_subset_1(sK1,k1_autgroup(sK0))
| ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolution,[],[f271,f150]) ).
fof(f440,plain,
( v1_xboole_0(u1_struct_0(sK0))
| ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolution,[],[f202,f148]) ).
fof(f441,plain,
( v1_xboole_0(u1_struct_0(sK0))
| ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolution,[],[f202,f150]) ).
fof(f446,plain,
( v1_xboole_0(u1_struct_0(sK0))
| ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolution,[],[f203,f148]) ).
fof(f447,plain,
( v1_xboole_0(u1_struct_0(sK0))
| ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolution,[],[f203,f150]) ).
fof(f550,plain,
( ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| spl27_2 ),
inference(resolution,[],[f190,f410]) ).
fof(f553,plain,
( ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| spl27_2 ),
inference(forward_subsumption_resolution,[],[f550,f152]) ).
fof(f554,plain,
( ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| spl27_2 ),
inference(forward_subsumption_resolution,[],[f553,f153]) ).
fof(f555,plain,
( v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| spl27_2 ),
inference(forward_subsumption_resolution,[],[f554,f154]) ).
fof(f556,plain,
( ~ l1_group_1(sK0)
| spl27_2 ),
inference(forward_subsumption_resolution,[],[f555,f155]) ).
fof(f557,plain,
( $false
| spl27_2 ),
inference(forward_subsumption_resolution,[],[f556,f151]) ).
fof(f558,plain,
spl27_2,
inference(avatar_contradiction_clause,[],[f557]) ).
fof(f559,plain,
( v3_struct_0(sK0)
| ~ l1_struct_0(sK0)
| ~ spl27_3 ),
inference(resolution,[],[f414,f220]) ).
fof(f572,plain,
( ~ l1_struct_0(sK0)
| ~ spl27_3 ),
inference(forward_subsumption_resolution,[],[f559,f155]) ).
fof(f573,plain,
( ~ l1_group_1(sK0)
| ~ spl27_3 ),
inference(resolution,[],[f572,f199]) ).
fof(f574,plain,
( $false
| ~ spl27_3 ),
inference(forward_subsumption_resolution,[],[f573,f151]) ).
fof(f575,plain,
~ spl27_3,
inference(avatar_contradiction_clause,[],[f574]) ).
fof(f576,plain,
( ~ m1_subset_1(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),sK2,sK1),k1_autgroup(sK0))
| ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f431,f413]) ).
fof(f577,plain,
( m1_subset_1(sK1,k1_autgroup(sK0))
| ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f435,f413]) ).
fof(f578,plain,
( m1_subset_1(sK2,k1_autgroup(sK0))
| ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f434,f413]) ).
fof(f579,plain,
( ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f441,f413]) ).
fof(f580,plain,
( ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f440,f413]) ).
fof(f581,plain,
( ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f447,f413]) ).
fof(f582,plain,
( ~ m1_fraenkel(k1_autgroup(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f446,f413]) ).
fof(f583,plain,
( ~ m1_subset_1(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),sK2,sK1),k1_autgroup(sK0))
| ~ spl27_2
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f576,f409]) ).
fof(f584,plain,
( m1_subset_1(sK1,k1_autgroup(sK0))
| ~ spl27_2
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f577,f409]) ).
fof(f585,plain,
( m1_subset_1(sK2,k1_autgroup(sK0))
| ~ spl27_2
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f578,f409]) ).
fof(f586,plain,
( m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_2
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f579,f409]) ).
fof(f587,plain,
( m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_2
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f580,f409]) ).
fof(f588,plain,
( v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_2
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f581,f409]) ).
fof(f589,plain,
( v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_2
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f582,f409]) ).
fof(f590,plain,
( r2_hidden(sK1,k1_autgroup(sK0))
| v1_xboole_0(k1_autgroup(sK0))
| ~ spl27_2
| spl27_3 ),
inference(resolution,[],[f584,f276]) ).
fof(f603,definition,
( spl27_10
<=> v1_xboole_0(k1_autgroup(sK0)) ),
introduced(definition,[new_symbols(definition,[spl27_10])],[avatar_definition]) ).
fof(f604,plain,
( ~ v1_xboole_0(k1_autgroup(sK0))
| spl27_10 ),
inference(avatar_component_clause,[],[f603]) ).
fof(f605,plain,
( v1_xboole_0(k1_autgroup(sK0))
| ~ spl27_10 ),
inference(avatar_component_clause,[],[f603]) ).
fof(f607,definition,
( spl27_11
<=> r2_hidden(sK1,k1_autgroup(sK0)) ),
introduced(definition,[new_symbols(definition,[spl27_11])],[avatar_definition]) ).
fof(f609,plain,
( r2_hidden(sK1,k1_autgroup(sK0))
| ~ spl27_11 ),
inference(avatar_component_clause,[],[f607]) ).
fof(f610,plain,
( spl27_10
| spl27_11
| ~ spl27_2
| spl27_3 ),
inference(avatar_split_clause,[],[f590,f412,f408,f607,f603]) ).
fof(f611,plain,
( r2_hidden(sK2,k1_autgroup(sK0))
| v1_xboole_0(k1_autgroup(sK0))
| ~ spl27_2
| spl27_3 ),
inference(resolution,[],[f585,f276]) ).
fof(f615,plain,
( m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_2
| spl27_3 ),
inference(resolution,[],[f586,f273]) ).
fof(f618,plain,
( m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_2
| spl27_3 ),
inference(resolution,[],[f587,f273]) ).
fof(f649,plain,
( ~ v1_xboole_0(k1_autgroup(sK0))
| ~ spl27_2 ),
inference(resolution,[],[f409,f201]) ).
fof(f654,plain,
( $false
| ~ spl27_2
| ~ spl27_10 ),
inference(forward_subsumption_resolution,[],[f649,f605]) ).
fof(f655,plain,
( ~ spl27_2
| ~ spl27_10 ),
inference(avatar_contradiction_clause,[],[f654]) ).
fof(f656,plain,
( r2_hidden(sK2,k1_autgroup(sK0))
| ~ spl27_2
| spl27_3
| spl27_10 ),
inference(forward_subsumption_resolution,[],[f611,f604]) ).
fof(f658,plain,
( ~ r2_hidden(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),sK2,sK1),k1_autgroup(sK0))
| ~ spl27_2
| spl27_3 ),
inference(resolution,[],[f583,f275]) ).
fof(f729,plain,
( ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| v1_group_6(sK2,sK0,sK0) ),
inference(resolution,[],[f297,f148]) ).
fof(f730,plain,
( ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| v1_group_6(sK1,sK0,sK0) ),
inference(resolution,[],[f297,f150]) ).
fof(f735,plain,
( ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| v1_group_6(sK1,sK0,sK0) ),
inference(forward_subsumption_resolution,[],[f730,f152]) ).
fof(f736,plain,
( ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| v1_group_6(sK2,sK0,sK0) ),
inference(forward_subsumption_resolution,[],[f729,f152]) ).
fof(f737,plain,
( ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| v1_group_6(sK1,sK0,sK0) ),
inference(forward_subsumption_resolution,[],[f735,f153]) ).
fof(f738,plain,
( ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| v1_group_6(sK2,sK0,sK0) ),
inference(forward_subsumption_resolution,[],[f736,f153]) ).
fof(f739,plain,
( v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| v1_group_6(sK1,sK0,sK0) ),
inference(forward_subsumption_resolution,[],[f737,f154]) ).
fof(f740,plain,
( v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| v1_group_6(sK2,sK0,sK0) ),
inference(forward_subsumption_resolution,[],[f738,f154]) ).
fof(f741,plain,
( ~ l1_group_1(sK0)
| v1_group_6(sK1,sK0,sK0) ),
inference(forward_subsumption_resolution,[],[f739,f155]) ).
fof(f742,plain,
( ~ l1_group_1(sK0)
| v1_group_6(sK2,sK0,sK0) ),
inference(forward_subsumption_resolution,[],[f740,f155]) ).
fof(f743,plain,
v1_group_6(sK1,sK0,sK0),
inference(forward_subsumption_resolution,[],[f741,f151]) ).
fof(f744,plain,
v1_group_6(sK2,sK0,sK0),
inference(forward_subsumption_resolution,[],[f742,f151]) ).
fof(f891,plain,
( ! [X0,X1] :
( ~ m1_relset_1(X0,u1_struct_0(sK0),X1)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK0),X1)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| v1_xboole_0(u1_struct_0(sK0))
| k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),X1,sK2,X0) = k5_relat_1(sK2,X0) )
| ~ spl27_2
| spl27_3 ),
inference(resolution,[],[f268,f618]) ).
fof(f896,plain,
( ! [X0,X1] :
( ~ m1_relset_1(X0,u1_struct_0(sK0),X1)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK0),X1)
| ~ v1_funct_1(sK2)
| v1_xboole_0(u1_struct_0(sK0))
| k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),X1,sK2,X0) = k5_relat_1(sK2,X0) )
| ~ spl27_2
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f891,f589]) ).
fof(f906,plain,
( ! [X0,X1] :
( ~ m1_relset_1(X0,u1_struct_0(sK0),X1)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK0),X1)
| v1_xboole_0(u1_struct_0(sK0))
| k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),X1,sK2,X0) = k5_relat_1(sK2,X0) )
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f896,f419]) ).
fof(f913,plain,
( ! [X0,X1] :
( ~ m1_relset_1(X0,u1_struct_0(sK0),X1)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK0),X1)
| k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),X1,sK2,X0) = k5_relat_1(sK2,X0) )
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f906,f413]) ).
fof(f917,plain,
( ~ v1_funct_1(sK1)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),sK2,sK1) = k5_relat_1(sK2,sK1)
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(resolution,[],[f913,f615]) ).
fof(f928,plain,
( ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),sK2,sK1) = k5_relat_1(sK2,sK1)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f917,f406]) ).
fof(f932,plain,
( k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),sK2,sK1) = k5_relat_1(sK2,sK1)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f928,f588]) ).
fof(f1005,plain,
( ~ r2_hidden(k5_relat_1(sK2,sK1),k1_autgroup(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(superposition,[],[f658,f932]) ).
fof(f1008,plain,
( v1_funct_2(k5_relat_1(sK2,sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(superposition,[],[f193,f932]) ).
fof(f1009,plain,
( m2_relset_1(k5_relat_1(sK2,sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(superposition,[],[f192,f932]) ).
fof(f1010,plain,
( v1_funct_1(k5_relat_1(sK2,sK1))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(superposition,[],[f194,f932]) ).
fof(f1011,plain,
( v1_funct_1(k5_relat_1(sK2,sK1))
| ~ v1_funct_1(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1010,f588]) ).
fof(f1012,plain,
( m2_relset_1(k5_relat_1(sK2,sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1009,f588]) ).
fof(f1013,plain,
( v1_funct_2(k5_relat_1(sK2,sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1008,f588]) ).
fof(f1014,plain,
( v1_funct_1(k5_relat_1(sK2,sK1))
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1011,f406]) ).
fof(f1015,plain,
( m2_relset_1(k5_relat_1(sK2,sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1012,f406]) ).
fof(f1016,plain,
( v1_funct_2(k5_relat_1(sK2,sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1013,f406]) ).
fof(f1017,plain,
( v1_funct_1(k5_relat_1(sK2,sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1014,f618]) ).
fof(f1018,plain,
( m2_relset_1(k5_relat_1(sK2,sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1015,f618]) ).
fof(f1019,plain,
( v1_funct_2(k5_relat_1(sK2,sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1016,f618]) ).
fof(f1020,plain,
( v1_funct_1(k5_relat_1(sK2,sK1))
| ~ v1_funct_1(sK2)
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1017,f589]) ).
fof(f1021,plain,
( m2_relset_1(k5_relat_1(sK2,sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1018,f589]) ).
fof(f1022,plain,
( v1_funct_2(k5_relat_1(sK2,sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1019,f589]) ).
fof(f1023,plain,
( v1_funct_1(k5_relat_1(sK2,sK1))
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1020,f419]) ).
fof(f1024,plain,
( m2_relset_1(k5_relat_1(sK2,sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1021,f419]) ).
fof(f1025,plain,
( v1_funct_2(k5_relat_1(sK2,sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1022,f419]) ).
fof(f1026,plain,
( v1_funct_1(k5_relat_1(sK2,sK1))
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1023,f413]) ).
fof(f1027,plain,
( m2_relset_1(k5_relat_1(sK2,sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1024,f413]) ).
fof(f1028,plain,
( v1_funct_2(k5_relat_1(sK2,sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1025,f413]) ).
fof(f1029,plain,
( v1_funct_1(k5_relat_1(sK2,sK1))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1026,f615]) ).
fof(f1030,plain,
( m2_relset_1(k5_relat_1(sK2,sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1027,f615]) ).
fof(f1031,plain,
( v1_funct_2(k5_relat_1(sK2,sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1028,f615]) ).
fof(f1828,plain,
( ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v1_group_6(k5_relat_1(sK2,sK1),sK0,sK0)
| ~ v1_funct_2(k5_relat_1(sK2,sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k5_relat_1(sK2,sK1))
| ~ v4_group_6(k5_relat_1(sK2,sK1),sK0,sK0)
| r2_hidden(k5_relat_1(sK2,sK1),k1_autgroup(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(resolution,[],[f279,f1030]) ).
fof(f1843,plain,
( ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v1_group_6(k5_relat_1(sK2,sK1),sK0,sK0)
| ~ v1_funct_2(k5_relat_1(sK2,sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k5_relat_1(sK2,sK1))
| ~ v4_group_6(k5_relat_1(sK2,sK1),sK0,sK0)
| r2_hidden(k5_relat_1(sK2,sK1),k1_autgroup(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1828,f152]) ).
fof(f1850,plain,
( ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v1_group_6(k5_relat_1(sK2,sK1),sK0,sK0)
| ~ v1_funct_2(k5_relat_1(sK2,sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k5_relat_1(sK2,sK1))
| ~ v4_group_6(k5_relat_1(sK2,sK1),sK0,sK0)
| r2_hidden(k5_relat_1(sK2,sK1),k1_autgroup(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1843,f153]) ).
fof(f1857,plain,
( v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v1_group_6(k5_relat_1(sK2,sK1),sK0,sK0)
| ~ v1_funct_2(k5_relat_1(sK2,sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k5_relat_1(sK2,sK1))
| ~ v4_group_6(k5_relat_1(sK2,sK1),sK0,sK0)
| r2_hidden(k5_relat_1(sK2,sK1),k1_autgroup(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1850,f154]) ).
fof(f1863,plain,
( ~ l1_group_1(sK0)
| ~ v1_group_6(k5_relat_1(sK2,sK1),sK0,sK0)
| ~ v1_funct_2(k5_relat_1(sK2,sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k5_relat_1(sK2,sK1))
| ~ v4_group_6(k5_relat_1(sK2,sK1),sK0,sK0)
| r2_hidden(k5_relat_1(sK2,sK1),k1_autgroup(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1857,f155]) ).
fof(f1869,plain,
( ~ v1_group_6(k5_relat_1(sK2,sK1),sK0,sK0)
| ~ v1_funct_2(k5_relat_1(sK2,sK1),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k5_relat_1(sK2,sK1))
| ~ v4_group_6(k5_relat_1(sK2,sK1),sK0,sK0)
| r2_hidden(k5_relat_1(sK2,sK1),k1_autgroup(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1863,f151]) ).
fof(f1875,plain,
( ~ v1_group_6(k5_relat_1(sK2,sK1),sK0,sK0)
| ~ v1_funct_1(k5_relat_1(sK2,sK1))
| ~ v4_group_6(k5_relat_1(sK2,sK1),sK0,sK0)
| r2_hidden(k5_relat_1(sK2,sK1),k1_autgroup(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1869,f1031]) ).
fof(f1881,plain,
( ~ v1_group_6(k5_relat_1(sK2,sK1),sK0,sK0)
| ~ v4_group_6(k5_relat_1(sK2,sK1),sK0,sK0)
| r2_hidden(k5_relat_1(sK2,sK1),k1_autgroup(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1875,f1029]) ).
fof(f1887,plain,
( ~ v1_group_6(k5_relat_1(sK2,sK1),sK0,sK0)
| ~ v4_group_6(k5_relat_1(sK2,sK1),sK0,sK0)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1881,f1005]) ).
fof(f1914,definition,
( spl27_63
<=> v4_group_6(k5_relat_1(sK2,sK1),sK0,sK0) ),
introduced(definition,[new_symbols(definition,[spl27_63])],[avatar_definition]) ).
fof(f1916,plain,
( ~ v4_group_6(k5_relat_1(sK2,sK1),sK0,sK0)
| spl27_63 ),
inference(avatar_component_clause,[],[f1914]) ).
fof(f1918,definition,
( spl27_64
<=> v1_group_6(k5_relat_1(sK2,sK1),sK0,sK0) ),
introduced(definition,[new_symbols(definition,[spl27_64])],[avatar_definition]) ).
fof(f1920,plain,
( ~ v1_group_6(k5_relat_1(sK2,sK1),sK0,sK0)
| spl27_64 ),
inference(avatar_component_clause,[],[f1918]) ).
fof(f1921,plain,
( ~ spl27_63
| ~ spl27_64
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(avatar_split_clause,[],[f1887,f417,f412,f408,f404,f1918,f1914]) ).
fof(f2085,plain,
( ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| v4_group_6(sK1,sK0,sK0)
| ~ r2_hidden(sK1,k1_autgroup(sK0))
| ~ spl27_2
| spl27_3 ),
inference(resolution,[],[f280,f586]) ).
fof(f2086,plain,
( ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v1_group_6(sK2,sK0,sK0)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| v4_group_6(sK2,sK0,sK0)
| ~ r2_hidden(sK2,k1_autgroup(sK0))
| ~ spl27_2
| spl27_3 ),
inference(resolution,[],[f280,f587]) ).
fof(f2088,plain,
( ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v1_group_6(sK2,sK0,sK0)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| v4_group_6(sK2,sK0,sK0)
| ~ r2_hidden(sK2,k1_autgroup(sK0))
| ~ spl27_2
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f2086,f152]) ).
fof(f2089,plain,
( ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| v4_group_6(sK1,sK0,sK0)
| ~ r2_hidden(sK1,k1_autgroup(sK0))
| ~ spl27_2
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f2085,f152]) ).
fof(f2091,plain,
( ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v1_group_6(sK2,sK0,sK0)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| v4_group_6(sK2,sK0,sK0)
| ~ r2_hidden(sK2,k1_autgroup(sK0))
| ~ spl27_2
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f2088,f153]) ).
fof(f2092,plain,
( ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| v4_group_6(sK1,sK0,sK0)
| ~ r2_hidden(sK1,k1_autgroup(sK0))
| ~ spl27_2
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f2089,f153]) ).
fof(f2094,plain,
( v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v1_group_6(sK2,sK0,sK0)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| v4_group_6(sK2,sK0,sK0)
| ~ r2_hidden(sK2,k1_autgroup(sK0))
| ~ spl27_2
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f2091,f154]) ).
fof(f2095,plain,
( v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| v4_group_6(sK1,sK0,sK0)
| ~ r2_hidden(sK1,k1_autgroup(sK0))
| ~ spl27_2
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f2092,f154]) ).
fof(f2096,plain,
( ~ l1_group_1(sK0)
| ~ v1_group_6(sK2,sK0,sK0)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| v4_group_6(sK2,sK0,sK0)
| ~ r2_hidden(sK2,k1_autgroup(sK0))
| ~ spl27_2
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f2094,f155]) ).
fof(f2097,plain,
( ~ l1_group_1(sK0)
| ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| v4_group_6(sK1,sK0,sK0)
| ~ r2_hidden(sK1,k1_autgroup(sK0))
| ~ spl27_2
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f2095,f155]) ).
fof(f2098,plain,
( ~ v1_group_6(sK2,sK0,sK0)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| v4_group_6(sK2,sK0,sK0)
| ~ r2_hidden(sK2,k1_autgroup(sK0))
| ~ spl27_2
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f2096,f151]) ).
fof(f2099,plain,
( ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| v4_group_6(sK1,sK0,sK0)
| ~ r2_hidden(sK1,k1_autgroup(sK0))
| ~ spl27_2
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f2097,f151]) ).
fof(f2100,plain,
( ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| v4_group_6(sK2,sK0,sK0)
| ~ r2_hidden(sK2,k1_autgroup(sK0))
| ~ spl27_2
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f2098,f744]) ).
fof(f2101,plain,
( ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| v4_group_6(sK1,sK0,sK0)
| ~ r2_hidden(sK1,k1_autgroup(sK0))
| ~ spl27_2
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f2099,f743]) ).
fof(f2102,plain,
( ~ v1_funct_1(sK2)
| v4_group_6(sK2,sK0,sK0)
| ~ r2_hidden(sK2,k1_autgroup(sK0))
| ~ spl27_2
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f2100,f589]) ).
fof(f2103,plain,
( ~ v1_funct_1(sK1)
| v4_group_6(sK1,sK0,sK0)
| ~ r2_hidden(sK1,k1_autgroup(sK0))
| ~ spl27_2
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f2101,f588]) ).
fof(f2104,plain,
( v4_group_6(sK2,sK0,sK0)
| ~ r2_hidden(sK2,k1_autgroup(sK0))
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f2102,f419]) ).
fof(f2105,plain,
( v4_group_6(sK1,sK0,sK0)
| ~ r2_hidden(sK1,k1_autgroup(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f2103,f406]) ).
fof(f2106,plain,
( v4_group_6(sK2,sK0,sK0)
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_10 ),
inference(forward_subsumption_resolution,[],[f2104,f656]) ).
fof(f2107,plain,
( v4_group_6(sK1,sK0,sK0)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_11 ),
inference(forward_subsumption_resolution,[],[f2105,f609]) ).
fof(f10756,plain,
( ! [X0,X1] :
( ~ m1_relset_1(X0,u1_struct_0(sK0),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(X1))
| ~ v1_funct_1(X0)
| ~ v1_group_6(X0,sK0,X1)
| ~ v1_group_6(sK2,sK0,sK0)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| k5_relat_1(sK2,X0) = k8_group_6(sK0,sK0,X1,sK2,X0) )
| ~ spl27_2
| spl27_3 ),
inference(resolution,[],[f269,f618]) ).
fof(f10777,plain,
( ! [X0,X1] :
( ~ m1_relset_1(X0,u1_struct_0(sK0),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(X1))
| ~ v1_funct_1(X0)
| ~ v1_group_6(X0,sK0,X1)
| ~ v1_group_6(sK2,sK0,sK0)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| k5_relat_1(sK2,X0) = k8_group_6(sK0,sK0,X1,sK2,X0) )
| ~ spl27_2
| spl27_3 ),
inference(duplicate_literal_removal,[],[f10756]) ).
fof(f10845,plain,
( ! [X0,X1] :
( ~ m1_relset_1(X0,u1_struct_0(sK0),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(X1))
| ~ v1_funct_1(X0)
| ~ v1_group_6(X0,sK0,X1)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| k5_relat_1(sK2,X0) = k8_group_6(sK0,sK0,X1,sK2,X0) )
| ~ spl27_2
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f10777,f744]) ).
fof(f10876,plain,
( ! [X0,X1] :
( ~ m1_relset_1(X0,u1_struct_0(sK0),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(X1))
| ~ v1_funct_1(X0)
| ~ v1_group_6(X0,sK0,X1)
| ~ v1_funct_1(sK2)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| k5_relat_1(sK2,X0) = k8_group_6(sK0,sK0,X1,sK2,X0) )
| ~ spl27_2
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f10845,f589]) ).
fof(f10905,plain,
( ! [X0,X1] :
( ~ m1_relset_1(X0,u1_struct_0(sK0),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(X1))
| ~ v1_funct_1(X0)
| ~ v1_group_6(X0,sK0,X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| k5_relat_1(sK2,X0) = k8_group_6(sK0,sK0,X1,sK2,X0) )
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f10876,f419]) ).
fof(f10931,plain,
( ! [X0,X1] :
( ~ m1_relset_1(X0,u1_struct_0(sK0),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(X1))
| ~ v1_funct_1(X0)
| ~ v1_group_6(X0,sK0,X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| k5_relat_1(sK2,X0) = k8_group_6(sK0,sK0,X1,sK2,X0) )
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f10905,f151]) ).
fof(f10955,plain,
( ! [X0,X1] :
( ~ m1_relset_1(X0,u1_struct_0(sK0),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(X1))
| ~ v1_funct_1(X0)
| ~ v1_group_6(X0,sK0,X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| k5_relat_1(sK2,X0) = k8_group_6(sK0,sK0,X1,sK2,X0) )
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f10931,f152]) ).
fof(f10979,plain,
( ! [X0,X1] :
( ~ m1_relset_1(X0,u1_struct_0(sK0),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(X1))
| ~ v1_funct_1(X0)
| ~ v1_group_6(X0,sK0,X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| v3_struct_0(sK0)
| k5_relat_1(sK2,X0) = k8_group_6(sK0,sK0,X1,sK2,X0) )
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f10955,f153]) ).
fof(f11006,plain,
( ! [X0,X1] :
( ~ m1_relset_1(X0,u1_struct_0(sK0),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(X1))
| ~ v1_funct_1(X0)
| ~ v1_group_6(X0,sK0,X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| k5_relat_1(sK2,X0) = k8_group_6(sK0,sK0,X1,sK2,X0) )
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f10979,f155]) ).
fof(f11123,plain,
( ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ v1_group_6(sK1,sK0,sK0)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| k5_relat_1(sK2,sK1) = k8_group_6(sK0,sK0,sK0,sK2,sK1)
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(resolution,[],[f11006,f615]) ).
fof(f11146,plain,
( ~ v1_funct_1(sK1)
| ~ v1_group_6(sK1,sK0,sK0)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| k5_relat_1(sK2,sK1) = k8_group_6(sK0,sK0,sK0,sK2,sK1)
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f11123,f588]) ).
fof(f11153,plain,
( ~ v1_group_6(sK1,sK0,sK0)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| k5_relat_1(sK2,sK1) = k8_group_6(sK0,sK0,sK0,sK2,sK1)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f11146,f406]) ).
fof(f11157,plain,
( ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| k5_relat_1(sK2,sK1) = k8_group_6(sK0,sK0,sK0,sK2,sK1)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f11153,f743]) ).
fof(f11161,plain,
( ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| k5_relat_1(sK2,sK1) = k8_group_6(sK0,sK0,sK0,sK2,sK1)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f11157,f151]) ).
fof(f11164,plain,
( ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| k5_relat_1(sK2,sK1) = k8_group_6(sK0,sK0,sK0,sK2,sK1)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f11161,f152]) ).
fof(f11167,plain,
( v3_struct_0(sK0)
| k5_relat_1(sK2,sK1) = k8_group_6(sK0,sK0,sK0,sK2,sK1)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f11164,f153]) ).
fof(f11178,plain,
( k5_relat_1(sK2,sK1) = k8_group_6(sK0,sK0,sK0,sK2,sK1)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f11167,f155]) ).
fof(f11491,plain,
( v1_group_6(k5_relat_1(sK2,sK1),sK0,sK0)
| ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK2,sK0,sK0)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(superposition,[],[f196,f11178]) ).
fof(f11494,plain,
( v1_group_6(k5_relat_1(sK2,sK1),sK0,sK0)
| ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK2,sK0,sK0)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(duplicate_literal_removal,[],[f11491]) ).
fof(f11495,plain,
( ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK2,sK0,sK0)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_64 ),
inference(forward_subsumption_resolution,[],[f11494,f1920]) ).
fof(f11496,plain,
( ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK2,sK0,sK0)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_64 ),
inference(forward_subsumption_resolution,[],[f11495,f743]) ).
fof(f11497,plain,
( ~ v1_funct_1(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK2,sK0,sK0)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_64 ),
inference(forward_subsumption_resolution,[],[f11496,f588]) ).
fof(f11498,plain,
( ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK2,sK0,sK0)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_64 ),
inference(forward_subsumption_resolution,[],[f11497,f406]) ).
fof(f11499,plain,
( ~ v1_group_6(sK2,sK0,sK0)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_64 ),
inference(forward_subsumption_resolution,[],[f11498,f618]) ).
fof(f11500,plain,
( ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_64 ),
inference(forward_subsumption_resolution,[],[f11499,f744]) ).
fof(f11501,plain,
( ~ v1_funct_1(sK2)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_64 ),
inference(forward_subsumption_resolution,[],[f11500,f589]) ).
fof(f11502,plain,
( ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_64 ),
inference(forward_subsumption_resolution,[],[f11501,f419]) ).
fof(f11503,plain,
( ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_64 ),
inference(forward_subsumption_resolution,[],[f11502,f151]) ).
fof(f11504,plain,
( ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_64 ),
inference(forward_subsumption_resolution,[],[f11503,f152]) ).
fof(f11505,plain,
( v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_64 ),
inference(forward_subsumption_resolution,[],[f11504,f153]) ).
fof(f11506,plain,
( ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_64 ),
inference(forward_subsumption_resolution,[],[f11505,f155]) ).
fof(f11507,plain,
( $false
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_64 ),
inference(forward_subsumption_resolution,[],[f11506,f615]) ).
fof(f11508,plain,
( ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_64 ),
inference(avatar_contradiction_clause,[],[f11507]) ).
fof(f12071,plain,
( v4_group_6(k5_relat_1(sK2,sK1),sK0,sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK2,sK0,sK0)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ v4_group_6(sK1,sK0,sK0)
| ~ v4_group_6(sK2,sK0,sK0)
| ~ l1_group_1(sK0)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(superposition,[],[f283,f11178]) ).
fof(f12076,plain,
( v4_group_6(k5_relat_1(sK2,sK1),sK0,sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK2,sK0,sK0)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ v4_group_6(sK1,sK0,sK0)
| ~ v4_group_6(sK2,sK0,sK0)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4 ),
inference(duplicate_literal_removal,[],[f12071]) ).
fof(f12080,plain,
( ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK2,sK0,sK0)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ v4_group_6(sK1,sK0,sK0)
| ~ v4_group_6(sK2,sK0,sK0)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_63 ),
inference(forward_subsumption_resolution,[],[f12076,f1916]) ).
fof(f12084,plain,
( ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK2,sK0,sK0)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ v4_group_6(sK1,sK0,sK0)
| ~ v4_group_6(sK2,sK0,sK0)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_63 ),
inference(forward_subsumption_resolution,[],[f12080,f152]) ).
fof(f12088,plain,
( v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK2,sK0,sK0)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ v4_group_6(sK1,sK0,sK0)
| ~ v4_group_6(sK2,sK0,sK0)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_63 ),
inference(forward_subsumption_resolution,[],[f12084,f153]) ).
fof(f12092,plain,
( ~ l1_group_1(sK0)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK2,sK0,sK0)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ v4_group_6(sK1,sK0,sK0)
| ~ v4_group_6(sK2,sK0,sK0)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_63 ),
inference(forward_subsumption_resolution,[],[f12088,f155]) ).
fof(f12096,plain,
( ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK2,sK0,sK0)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ v4_group_6(sK1,sK0,sK0)
| ~ v4_group_6(sK2,sK0,sK0)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_63 ),
inference(forward_subsumption_resolution,[],[f12092,f151]) ).
fof(f12100,plain,
( ~ v1_group_6(sK2,sK0,sK0)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ v4_group_6(sK1,sK0,sK0)
| ~ v4_group_6(sK2,sK0,sK0)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_63 ),
inference(forward_subsumption_resolution,[],[f12096,f587]) ).
fof(f12104,plain,
( ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ v4_group_6(sK1,sK0,sK0)
| ~ v4_group_6(sK2,sK0,sK0)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_63 ),
inference(forward_subsumption_resolution,[],[f12100,f744]) ).
fof(f12108,plain,
( ~ v1_funct_1(sK2)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ v4_group_6(sK1,sK0,sK0)
| ~ v4_group_6(sK2,sK0,sK0)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_63 ),
inference(forward_subsumption_resolution,[],[f12104,f589]) ).
fof(f12112,plain,
( ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ v4_group_6(sK1,sK0,sK0)
| ~ v4_group_6(sK2,sK0,sK0)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_63 ),
inference(forward_subsumption_resolution,[],[f12108,f419]) ).
fof(f12117,plain,
( ~ v1_group_6(sK1,sK0,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ v4_group_6(sK1,sK0,sK0)
| ~ v4_group_6(sK2,sK0,sK0)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_63 ),
inference(forward_subsumption_resolution,[],[f12112,f586]) ).
fof(f12121,plain,
( ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ v4_group_6(sK1,sK0,sK0)
| ~ v4_group_6(sK2,sK0,sK0)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_63 ),
inference(forward_subsumption_resolution,[],[f12117,f743]) ).
fof(f12123,plain,
( ~ v1_funct_1(sK1)
| ~ v4_group_6(sK1,sK0,sK0)
| ~ v4_group_6(sK2,sK0,sK0)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_63 ),
inference(forward_subsumption_resolution,[],[f12121,f588]) ).
fof(f12125,plain,
( ~ v4_group_6(sK1,sK0,sK0)
| ~ v4_group_6(sK2,sK0,sK0)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_63 ),
inference(forward_subsumption_resolution,[],[f12123,f406]) ).
fof(f12127,plain,
( ~ v4_group_6(sK2,sK0,sK0)
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| ~ spl27_11
| spl27_63 ),
inference(forward_subsumption_resolution,[],[f12125,f2107]) ).
fof(f12130,plain,
( $false
| ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_10
| ~ spl27_11
| spl27_63 ),
inference(forward_subsumption_resolution,[],[f12127,f2106]) ).
fof(f12131,plain,
( ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_10
| ~ spl27_11
| spl27_63 ),
inference(avatar_contradiction_clause,[],[f12130]) ).
cnf(s1,plain,
( spl27_1
| ~ spl27_2
| spl27_3 ),
inference(sat_conversion,[],[f415]) ).
cnf(s2,plain,
( ~ spl27_2
| spl27_3
| spl27_4 ),
inference(sat_conversion,[],[f420]) ).
cnf(s5,plain,
spl27_2,
inference(sat_conversion,[],[f558]) ).
cnf(s6,plain,
~ spl27_3,
inference(sat_conversion,[],[f575]) ).
cnf(s8,plain,
( ~ spl27_2
| spl27_3
| spl27_10
| spl27_11 ),
inference(sat_conversion,[],[f610]) ).
cnf(s11,plain,
( ~ spl27_2
| ~ spl27_10 ),
inference(sat_conversion,[],[f655]) ).
cnf(s35,plain,
( ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| ~ spl27_63
| ~ spl27_64 ),
inference(sat_conversion,[],[f1921]) ).
cnf(s332,plain,
( ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_64 ),
inference(sat_conversion,[],[f11508]) ).
cnf(s343,plain,
( ~ spl27_1
| ~ spl27_2
| spl27_3
| ~ spl27_4
| spl27_10
| ~ spl27_11
| spl27_63 ),
inference(sat_conversion,[],[f12131]) ).
cnf(s365,plain,
~ spl27_10,
inference(rat,[],[s11,s5]) ).
cnf(s368,plain,
spl27_11,
inference(rat,[],[s8,s5,s6,s365]) ).
cnf(s369,plain,
spl27_4,
inference(rat,[],[s2,s6,s5]) ).
cnf(s384,plain,
spl27_1,
inference(rat,[],[s1,s6,s5]) ).
cnf(s385,plain,
spl27_63,
inference(rat,[],[s343,s369,s368,s365,s5,s6,s384]) ).
cnf(s389,plain,
spl27_64,
inference(rat,[],[s332,s369,s5,s6,s384]) ).
cnf(s390,plain,
$false,
inference(rat,[],[s35,s389,s369,s5,s6,s385,s384]) ).
fof(f12132,plain,
$false,
inference(avatar_sat_refutation,[],[s390]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP621+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.36 % Computer : n014.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 27 10:09:07 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.40 Running first-order model finding
% 0.11/0.40 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.09/2.47 % (575005)Will run a generic schedule for satisfiability detection.
% 14.09/2.47 % (575023)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1562504536:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.09/2.47 % (575018)% WARNING: option uhcvi not known.
% 14.09/2.47 % (575017)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2875896989_2999 on theBenchmark for (2999ds/0Mi)
% 14.09/2.47 % (575019)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2448584033:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.09/2.47 % (575020)dis+10_1_sil=32000:sp=arity:random_seed=724363623:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.09/2.47 % (575021)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=397623942:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.09/2.47 % (575022)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1724798797:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.09/2.47 % (575018)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1207371745:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.09/2.47 % TRYING [1]
% 14.09/2.47 % TRYING [2]
% 14.09/2.47 % TRYING [3]
% 14.09/2.47 % (575023)Instruction limit reached!
% 14.09/2.47 % (575023)------------------------------
% 14.09/2.47 % (575023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.09/2.47 % (575023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.09/2.47 % (575023)CaDiCaL version: 2.1.3
% 14.09/2.47 % (575023)Termination reason: Instruction limit
% 14.09/2.47 % (575023)Termination phase: Saturation
% 14.09/2.47 % (575023)Time elapsed: 0.051 s
% 14.09/2.47 % (575023)Peak memory usage: 13 MB
% 14.09/2.47 % (575023)Instructions burned: 161 (million)
% 14.09/2.47 % (575050)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4191601390:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.09/2.47 % TRYING [1]
% 14.09/2.47 % TRYING [2]
% 14.09/2.47 % TRYING [3]
% 14.09/2.47 % (575020)Instruction limit reached!
% 14.09/2.47 % (575020)------------------------------
% 14.09/2.47 % (575020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.09/2.47 % (575020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.09/2.47 % (575020)CaDiCaL version: 2.1.3
% 14.09/2.47 % (575020)Termination reason: Instruction limit
% 14.09/2.47 % (575020)Termination phase: Saturation
% 14.09/2.47 % (575020)Time elapsed: 0.067 s
% 14.09/2.47 % (575020)Peak memory usage: 12 MB
% 14.09/2.47 % (575020)Instructions burned: 103 (million)
% 14.09/2.47 % TRYING [4]
% 14.09/2.47 % (575021)Instruction limit reached!
% 14.09/2.47 % (575021)------------------------------
% 14.09/2.47 % (575021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.09/2.47 % (575021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.09/2.47 % (575021)CaDiCaL version: 2.1.3
% 14.09/2.47 % (575021)Termination reason: Instruction limit
% 14.09/2.47 % (575021)Termination phase: Saturation
% 14.09/2.47 % (575021)Time elapsed: 0.072 s
% 14.09/2.47 % (575021)Peak memory usage: 13 MB
% 14.09/2.47 % (575021)Instructions burned: 116 (million)
% 14.09/2.47 % (575022)Instruction limit reached!
% 14.09/2.47 % (575022)------------------------------
% 14.09/2.47 % (575022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.09/2.47 % (575022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.09/2.47 % (575022)CaDiCaL version: 2.1.3
% 14.09/2.47 % (575022)Termination reason: Instruction limit
% 14.09/2.47 % (575022)Termination phase: Saturation
% 14.09/2.47 % (575022)Time elapsed: 0.074 s
% 14.09/2.47 % (575022)Peak memory usage: 13 MB
% 14.09/2.47 % (575022)Instructions burned: 132 (million)
% 14.09/2.47 % TRYING [4]
% 14.09/2.47 % (575060)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1069850356:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 14.09/2.47 % (575063)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2682338895:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.09/2.47 % (575065)ott-21_1_sil=16000:fs=off:random_seed=357674753:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.09/2.47 % (575060)Instruction limit reached!
% 14.09/2.47 % (575060)------------------------------
% 14.09/2.47 % (575060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.09/2.47 % (575060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/3.64 % (575060)CaDiCaL version: 2.1.3
% 6.12/3.64 % (575060)Termination reason: Instruction limit
% 6.12/3.64 % (575060)Termination phase: Saturation
% 6.12/3.64 % (575060)Time elapsed: 0.077 s
% 6.12/3.64 % (575060)Peak memory usage: 14 MB
% 6.12/3.64 % (575060)Instructions burned: 133 (million)
% 6.12/3.64 % (575098)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3902266015:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 6.12/3.64 % (575065)Instruction limit reached!
% 6.12/3.64 % (575065)------------------------------
% 6.12/3.64 % (575065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/3.64 % (575065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/3.64 % (575065)CaDiCaL version: 2.1.3
% 6.12/3.64 % (575065)Termination reason: Instruction limit
% 6.12/3.64 % (575065)Termination phase: Saturation
% 6.12/3.64 % (575065)Time elapsed: 0.103 s
% 6.12/3.64 % (575065)Peak memory usage: 13 MB
% 6.12/3.64 % (575065)Instructions burned: 181 (million)
% 6.12/3.64 % (575050)Instruction limit reached!
% 6.12/3.64 % (575050)------------------------------
% 6.12/3.64 % (575050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/3.64 % (575050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/3.64 % (575050)CaDiCaL version: 2.1.3
% 6.12/3.64 % (575050)Termination reason: Instruction limit
% 6.12/3.64 % (575050)Termination phase: Finite model building constraint generation
% 6.12/3.64 % (575050)Time elapsed: 0.154 s
% 6.12/3.64 % (575050)Peak memory usage: 33 MB
% 6.12/3.64 % (575050)Instructions burned: 714 (million)
% 6.12/3.64 % (575108)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2413452561:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 6.12/3.64 % (575113)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2536057680:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 6.12/3.64 % TRYING [1]
% 6.12/3.64 % TRYING [2]
% 6.12/3.64 % TRYING [3]
% 6.12/3.64 % TRYING [5]
% 6.12/3.64 % TRYING [4]
% 6.12/3.64 % (575098)Instruction limit reached!
% 6.12/3.64 % (575098)------------------------------
% 6.12/3.64 % (575098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/3.64 % (575098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/3.64 % (575098)CaDiCaL version: 2.1.3
% 6.12/3.64 % (575098)Termination reason: Instruction limit
% 6.12/3.64 % (575098)Termination phase: Saturation
% 6.12/3.64 % (575098)Time elapsed: 0.334 s
% 6.12/3.64 % (575098)Peak memory usage: 15 MB
% 6.12/3.64 % (575098)Instructions burned: 477 (million)
% 6.12/3.64 % (575063)Instruction limit reached!
% 6.12/3.64 % (575063)------------------------------
% 6.12/3.64 % (575063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/3.64 % (575063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/3.64 % (575063)CaDiCaL version: 2.1.3
% 6.12/3.64 % (575063)Termination reason: Instruction limit
% 6.12/3.64 % (575063)Termination phase: Saturation
% 6.12/3.64 % (575063)Time elapsed: 0.443 s
% 6.12/3.64 % (575063)Peak memory usage: 20 MB
% 6.12/3.64 % (575063)Instructions burned: 685 (million)
% 6.12/3.64 % (575222)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=715040830:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 6.12/3.64 % (575231)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3233769256:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 6.12/3.64 % (575108)Instruction limit reached!
% 6.12/3.64 % (575108)------------------------------
% 6.12/3.64 % (575108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/3.64 % (575108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/3.64 % (575108)CaDiCaL version: 2.1.3
% 6.12/3.64 % (575108)Termination reason: Instruction limit
% 6.12/3.64 % (575108)Termination phase: Finite model building SAT solving
% 6.12/3.64 % (575108)Time elapsed: 0.343 s
% 6.12/3.64 % (575108)Peak memory usage: 36 MB
% 6.12/3.64 % (575108)Instructions burned: 865 (million)
% 6.12/3.64 % (575246)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1901351359:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 6.12/3.64 % (575113)Instruction limit reached!
% 6.12/3.64 % (575113)------------------------------
% 6.12/3.64 % (575113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/3.64 % (575113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/3.64 % (575113)CaDiCaL version: 2.1.3
% 6.12/3.64 % (575113)Termination reason: Instruction limit
% 6.12/3.64 % (575113)Termination phase: Saturation
% 6.12/3.64 % (575113)Time elapsed: 0.374 s
% 6.12/3.64 % (575113)Peak memory usage: 25 MB
% 6.12/3.64 % (575113)Instructions burned: 1181 (million)
% 6.12/3.64 % (575264)fmb+10_1_sil=64000:random_seed=4260632726:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 6.12/3.64 % TRYING [1]
% 6.12/3.64 % TRYING [2]
% 6.12/3.64 % TRYING [3]
% 6.12/3.64 % TRYING [4]
% 6.12/3.64 % TRYING [5]
% 6.12/3.64 % (575222)Instruction limit reached!
% 6.12/3.64 % (575222)------------------------------
% 6.12/3.64 % (575222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/3.64 % (575222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/3.64 % (575222)CaDiCaL version: 2.1.3
% 6.12/3.64 % (575222)Termination reason: Instruction limit
% 6.12/3.64 % (575222)Termination phase: Finite model building constraint generation
% 6.12/3.64 % (575222)Time elapsed: 0.412 s
% 6.12/3.64 % (575222)Peak memory usage: 106 MB
% 6.12/3.64 % (575222)Instructions burned: 891 (million)
% 6.12/3.64 % (575231)Instruction limit reached!
% 6.12/3.64 % (575231)------------------------------
% 6.12/3.64 % (575231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/3.64 % (575231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/3.64 % (575231)CaDiCaL version: 2.1.3
% 6.12/3.64 % (575231)Termination reason: Instruction limit
% 6.12/3.64 % (575231)Termination phase: Saturation
% 6.12/3.64 % (575231)Time elapsed: 0.428 s
% 6.12/3.64 % (575231)Peak memory usage: 20 MB
% 6.12/3.64 % (575231)Instructions burned: 693 (million)
% 6.12/3.64 % (575429)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1215007468:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 6.12/3.64 % TRYING [20]
% 6.12/3.64 % TRYING [6]
% 6.12/3.64 % (575441)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2119722399:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 6.12/3.64 % TRYING [8]
% 6.12/3.64 % (575246)Instruction limit reached!
% 6.12/3.64 % (575246)------------------------------
% 6.12/3.64 % (575246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/3.64 % (575246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/3.64 % (575246)CaDiCaL version: 2.1.3
% 6.12/3.64 % (575246)Termination reason: Instruction limit
% 6.12/3.64 % (575246)Termination phase: Saturation
% 6.12/3.64 % (575246)Time elapsed: 0.497 s
% 6.12/3.64 % (575246)Peak memory usage: 20 MB
% 6.12/3.64 % (575246)Instructions burned: 879 (million)
% 6.12/3.64 % (575485)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=705912641:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 6.12/3.64 % (575441)Instruction limit reached!
% 6.12/3.64 % (575441)------------------------------
% 6.12/3.64 % (575441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/3.64 % (575441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/3.64 % (575441)CaDiCaL version: 2.1.3
% 6.12/3.64 % (575441)Termination reason: Instruction limit
% 6.12/3.64 % (575441)Termination phase: Finite model building constraint generation
% 6.12/3.64 % (575441)Time elapsed: 0.289 s
% 6.12/3.64 % (575441)Peak memory usage: 36 MB
% 6.12/3.64 % (575441)Instructions burned: 921 (million)
% 6.12/3.64 % (575585)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=382939578:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 6.12/3.64 % TRYING [6]
% 6.12/3.64 % (575585)Instruction limit reached!
% 6.12/3.64 % (575585)------------------------------
% 6.12/3.64 % (575585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/3.64 % (575585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/3.64 % (575585)CaDiCaL version: 2.1.3
% 6.12/3.64 % (575585)Termination reason: Instruction limit
% 6.12/3.64 % (575585)Termination phase: Saturation
% 6.12/3.64 % (575585)Time elapsed: 0.672 s
% 6.12/3.64 % (575585)Peak memory usage: 23 MB
% 6.12/3.64 % (575585)Instructions burned: 1472 (million)
% 6.12/3.64 % (575894)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=396800593:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 6.12/3.64 % (575894)Cannot represent all propositional literals internally
% 6.12/3.64 % (575894)Refutation not found, incomplete strategy
% 6.12/3.64 % (575894)------------------------------
% 6.12/3.64 % (575894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/3.64 % (575894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/3.64 % (575894)CaDiCaL version: 2.1.3
% 6.12/3.64 % (575894)Termination reason: Refutation not found, incomplete strategy
% 6.12/3.64 % (575894)Time elapsed: 0.016 s
% 6.12/3.64 % (575894)Peak memory usage: 11 MB
% 6.12/3.64 % (575894)Instructions burned: 31 (million)
% 6.12/3.64 % (575894)------------------------------
% 6.12/3.64 % (575894)------------------------------
% 6.12/3.64 % (575913)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=963863665:fmbsr=2.30978:i=2174_2979 on theBenchmark for (2979ds/2174Mi)
% 6.12/3.64 % TRYING [16]
% 6.12/3.64 % (575913)Instruction limit reached!
% 6.12/3.64 % (575913)------------------------------
% 6.12/3.64 % (575913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/3.64 % (575913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/3.64 % (575913)CaDiCaL version: 2.1.3
% 6.12/3.64 % (575913)Termination reason: Instruction limit
% 6.12/3.64 % (575913)Termination phase: Finite model building constraint generation
% 6.12/3.64 % (575913)Time elapsed: 0.747 s
% 6.12/3.64 % (575913)Peak memory usage: 124 MB
% 6.12/3.64 % (575913)Instructions burned: 2176 (million)
% 6.12/3.64 % (576256)ott-2_1_sil=16000:newcnf=on:random_seed=68486156:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2971 on theBenchmark for (2971ds/869Mi)
% 6.12/3.64 % (576256) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-575005-576256"...
% 6.12/3.64 % (576256)...printing done.
% 6.12/3.64 % (576256)Refutation found. Thanks to Tanya!
% 6.12/3.64 % SZS status Theorem for theBenchmark
% 6.12/3.64 % SZS output start Proof for theBenchmark
% See solution above
% 6.12/3.65 % (576256)------------------------------
% 6.12/3.65 % (576256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/3.65 % (576256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/3.65 % (576256)CaDiCaL version: 2.1.3
% 6.12/3.65 % (576256)Termination reason: Refutation
% 6.12/3.65 % (576256)Time elapsed: 0.313 s
% 6.12/3.65 % (576256)Peak memory usage: 19 MB
% 6.12/3.65 % (576256)Instructions burned: 524 (million)
% 6.12/3.65 % (575005)Success in time 3.236 s
% 6.12/3.65 % Vampire exiting
%------------------------------------------------------------------------------