%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP629+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:15:06 AM UTC 2026
% Result : Theorem 92.78s 27.94s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 49
% Syntax : Number of formulae : 435 ( 64 unt; 26 def)
% Number of atoms : 2122 ( 206 equ)
% Maximal formula atoms : 27 ( 4 avg)
% Number of connectives : 3033 (1346 ~;1532 |; 93 &)
% ( 26 <=>; 36 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 37 ( 35 usr; 20 prp; 0-4 aty)
% Number of functors : 23 ( 23 usr; 10 con; 0-5 aty)
% Number of variables : 507 ( 0 sgn 501 !; 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] :
( m1_subset_1(X1,u1_struct_0(X0))
=> k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,k3_group_1(X0,X1)),k6_autgroup(X0,X1)) = k6_autgroup(X0,k2_group_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t26_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] :
( m1_subset_1(X1,u1_struct_0(X0))
=> k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,k3_group_1(X0,X1)),k6_autgroup(X0,X1)) = k6_autgroup(X0,k2_group_1(X0)) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f9,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> v1_relat_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(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_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
=> ( X2 = k6_autgroup(X0,X1)
<=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> k8_funct_2(u1_struct_0(X0),u1_struct_0(X0),X2,X3) = k2_group_3(X0,X3,X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d6_autgroup) ).
fof(f18,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_group_1(X0) )
=> m1_subset_1(k2_group_1(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_group_1) ).
fof(f19,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> m1_subset_1(k2_group_3(X0,X1,X2),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_group_3) ).
fof(f21,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> m1_subset_1(k3_group_1(X0,X1),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_group_1) ).
fof(f22,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> m1_fraenkel(k4_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_autgroup) ).
fof(f24,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> m2_fraenkel(k6_autgroup(X0,X1),u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k6_autgroup) ).
fof(f25,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/sandbox2/benchmark/theBenchmark.p',dt_k7_funct_2) ).
fof(f27,axiom,
! [X0] :
( l1_group_1(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_group_1) ).
fof(f32,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/sandbox2/benchmark/theBenchmark.p',dt_m2_fraenkel) ).
fof(f33,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f45,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f46,axiom,
v1_xboole_0(k1_xboole_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_xboole_0) ).
fof(f62,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/sandbox2/benchmark/theBenchmark.p',redefinition_k7_funct_2) ).
fof(f63,axiom,
! [X0,X1,X2,X3] :
( ( ~ v1_xboole_0(X0)
& v1_funct_1(X2)
& v1_funct_2(X2,X0,X1)
& m1_relset_1(X2,X0,X1)
& m1_subset_1(X3,X0) )
=> k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k8_funct_2) ).
fof(f64,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/sandbox2/benchmark/theBenchmark.p',redefinition_m2_fraenkel) ).
fof(f65,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f67,axiom,
! [X0,X1,X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,X0,X1)
& m2_relset_1(X2,X0,X1) )
=> ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m2_relset_1(X3,X0,X1) )
=> ( ! [X4] :
( m1_subset_1(X4,X0)
=> k1_funct_1(X2,X4) = k1_funct_1(X3,X4) )
=> X2 = X3 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t113_funct_2) ).
fof(f69,axiom,
! [X0,X1,X2,X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m2_relset_1(X3,X0,X1) )
=> ! [X4] :
( ( v1_relat_1(X4)
& v1_funct_1(X4) )
=> ( r2_hidden(X2,X0)
=> ( X1 = k1_xboole_0
| k1_funct_1(k5_relat_1(X3,X4),X2) = k1_funct_1(X4,k1_funct_1(X3,X2)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t21_funct_2) ).
fof(f70,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> k8_funct_2(u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,k2_group_1(X0)),X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t25_autgroup) ).
fof(f71,axiom,
! [X0,X1] :
( m1_subset_1(X0,X1)
=> ( v1_xboole_0(X1)
| r2_hidden(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
fof(f72,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( k2_group_3(X0,k2_group_3(X0,X1,X2),k3_group_1(X0,X2)) = X1
& k2_group_3(X0,k2_group_3(X0,X1,k3_group_1(X0,X2)),X2) = X1 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t30_group_3) ).
fof(f86,plain,
? [X0] :
( ? [X1] :
( k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,k3_group_1(X0,X1)),k6_autgroup(X0,X1)) != k6_autgroup(X0,k2_group_1(X0))
& m1_subset_1(X1,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,[],[f2]) ).
fof(f87,plain,
? [X0] :
( ? [X1] :
( k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,k3_group_1(X0,X1)),k6_autgroup(X0,X1)) != k6_autgroup(X0,k2_group_1(X0))
& m1_subset_1(X1,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,[],[f86]) ).
fof(f97,plain,
! [X0,X1,X2] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f9]) ).
fof(f104,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k6_autgroup(X0,X1)
<=> ! [X3] :
( k8_funct_2(u1_struct_0(X0),u1_struct_0(X0),X2,X3) = k2_group_3(X0,X3,X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0)) )
| ~ m1_subset_1(X1,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,[],[f13]) ).
fof(f105,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k6_autgroup(X0,X1)
<=> ! [X3] :
( k8_funct_2(u1_struct_0(X0),u1_struct_0(X0),X2,X3) = k2_group_3(X0,X3,X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0)) )
| ~ m1_subset_1(X1,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,[],[f104]) ).
fof(f108,plain,
! [X0] :
( m1_subset_1(k2_group_1(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f109,plain,
! [X0] :
( m1_subset_1(k2_group_1(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f108]) ).
fof(f110,plain,
! [X0,X1,X2] :
( m1_subset_1(k2_group_3(X0,X1,X2),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f19]) ).
fof(f111,plain,
! [X0,X1,X2] :
( m1_subset_1(k2_group_3(X0,X1,X2),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f110]) ).
fof(f112,plain,
! [X0,X1] :
( m1_subset_1(k3_group_1(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f21]) ).
fof(f113,plain,
! [X0,X1] :
( m1_subset_1(k3_group_1(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f112]) ).
fof(f114,plain,
! [X0] :
( m1_fraenkel(k4_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,[],[f22]) ).
fof(f115,plain,
! [X0] :
( m1_fraenkel(k4_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,[],[f114]) ).
fof(f118,plain,
! [X0,X1] :
( m2_fraenkel(k6_autgroup(X0,X1),u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f24]) ).
fof(f119,plain,
! [X0,X1] :
( m2_fraenkel(k6_autgroup(X0,X1),u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f118]) ).
fof(f120,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,[],[f25]) ).
fof(f121,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,[],[f120]) ).
fof(f124,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f27]) ).
fof(f126,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,[],[f32]) ).
fof(f127,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,[],[f126]) ).
fof(f128,plain,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f33]) ).
fof(f136,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f45]) ).
fof(f137,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f136]) ).
fof(f142,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,[],[f62]) ).
fof(f143,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,[],[f142]) ).
fof(f144,plain,
! [X0,X1,X2,X3] :
( k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(ennf_transformation,[],[f63]) ).
fof(f145,plain,
! [X0,X1,X2,X3] :
( k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(flattening,[],[f144]) ).
fof(f146,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,[],[f64]) ).
fof(f147,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,[],[f146]) ).
fof(f148,plain,
! [X0,X1,X2] :
( ! [X3] :
( X2 = X3
| ? [X4] :
( k1_funct_1(X2,X4) != k1_funct_1(X3,X4)
& m1_subset_1(X4,X0) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f67]) ).
fof(f149,plain,
! [X0,X1,X2] :
( ! [X3] :
( X2 = X3
| ? [X4] :
( k1_funct_1(X2,X4) != k1_funct_1(X3,X4)
& m1_subset_1(X4,X0) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(flattening,[],[f148]) ).
fof(f151,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( X1 = k1_xboole_0
| k1_funct_1(k5_relat_1(X3,X4),X2) = k1_funct_1(X4,k1_funct_1(X3,X2))
| ~ r2_hidden(X2,X0)
| ~ v1_relat_1(X4)
| ~ v1_funct_1(X4) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1) ),
inference(ennf_transformation,[],[f69]) ).
fof(f152,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( X1 = k1_xboole_0
| k1_funct_1(k5_relat_1(X3,X4),X2) = k1_funct_1(X4,k1_funct_1(X3,X2))
| ~ r2_hidden(X2,X0)
| ~ v1_relat_1(X4)
| ~ v1_funct_1(X4) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1) ),
inference(flattening,[],[f151]) ).
fof(f153,plain,
! [X0] :
( ! [X1] :
( k8_funct_2(u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,k2_group_1(X0)),X1) = X1
| ~ m1_subset_1(X1,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,[],[f70]) ).
fof(f154,plain,
! [X0] :
( ! [X1] :
( k8_funct_2(u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,k2_group_1(X0)),X1) = X1
| ~ m1_subset_1(X1,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,[],[f153]) ).
fof(f155,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(ennf_transformation,[],[f71]) ).
fof(f156,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(flattening,[],[f155]) ).
fof(f157,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k2_group_3(X0,k2_group_3(X0,X1,X2),k3_group_1(X0,X2)) = X1
& k2_group_3(X0,k2_group_3(X0,X1,k3_group_1(X0,X2)),X2) = X1 )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f72]) ).
fof(f158,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k2_group_3(X0,k2_group_3(X0,X1,X2),k3_group_1(X0,X2)) = X1
& k2_group_3(X0,k2_group_3(X0,X1,k3_group_1(X0,X2)),X2) = X1 )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f157]) ).
fof(f166,plain,
m1_subset_1(sK1,u1_struct_0(sK0)),
inference(cnf_transformation,[],[f87]) ).
fof(f167,plain,
k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),k6_autgroup(sK0,k3_group_1(sK0,sK1)),k6_autgroup(sK0,sK1)) != k6_autgroup(sK0,k2_group_1(sK0)),
inference(cnf_transformation,[],[f87]) ).
fof(f168,plain,
l1_group_1(sK0),
inference(cnf_transformation,[],[f87]) ).
fof(f169,plain,
v4_group_1(sK0),
inference(cnf_transformation,[],[f87]) ).
fof(f170,plain,
v3_group_1(sK0),
inference(cnf_transformation,[],[f87]) ).
fof(f171,plain,
v1_group_1(sK0),
inference(cnf_transformation,[],[f87]) ).
fof(f172,plain,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f87]) ).
fof(f179,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(cnf_transformation,[],[f97]) ).
fof(f183,plain,
! [X2,X3,X0,X1] :
( k6_autgroup(X0,X1) != X2
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| k8_funct_2(u1_struct_0(X0),u1_struct_0(X0),X2,X3) = k2_group_3(X0,X3,X1)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f105]) ).
fof(f188,plain,
! [X0] :
( m1_subset_1(k2_group_1(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f109]) ).
fof(f189,plain,
! [X2,X0,X1] :
( m1_subset_1(k2_group_3(X0,X1,X2),u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f111]) ).
fof(f190,plain,
! [X0,X1] :
( m1_subset_1(k3_group_1(X0,X1),u1_struct_0(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f113]) ).
fof(f191,plain,
! [X0] :
( m1_fraenkel(k4_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,[],[f115]) ).
fof(f193,plain,
! [X0,X1] :
( m2_fraenkel(k6_autgroup(X0,X1),u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f119]) ).
fof(f194,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,[],[f121]) ).
fof(f195,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,[],[f121]) ).
fof(f196,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,[],[f121]) ).
fof(f198,plain,
! [X0] :
( ~ l1_group_1(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f201,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,[],[f127]) ).
fof(f202,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,[],[f127]) ).
fof(f203,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,[],[f127]) ).
fof(f204,plain,
! [X2,X0,X1] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f128]) ).
fof(f219,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f137]) ).
fof(f220,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[],[f46]) ).
fof(f258,plain,
! [X2,X3,X0,X1,X4] :
( k7_funct_2(X0,X1,X2,X3,X4) = k5_relat_1(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,[],[f143]) ).
fof(f259,plain,
! [X2,X3,X0,X1] :
( k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| ~ m1_relset_1(X2,X0,X1)
| ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| v1_xboole_0(X0)
| ~ m1_subset_1(X3,X0) ),
inference(cnf_transformation,[],[f145]) ).
fof(f260,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,[],[f147]) ).
fof(f261,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,[],[f147]) ).
fof(f263,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f65]) ).
fof(f265,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(sK24(X0,X2,X3),X0)
| ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X3,X0,X1)
| ~ v1_funct_2(X3,X0,X1)
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,X0,X1)
| X2 = X3 ),
inference(cnf_transformation,[],[f149]) ).
fof(f266,plain,
! [X2,X3,X0,X1] :
( k1_funct_1(X2,sK24(X0,X2,X3)) != k1_funct_1(X3,sK24(X0,X2,X3))
| ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X3,X0,X1)
| ~ v1_funct_2(X3,X0,X1)
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,X0,X1)
| X2 = X3 ),
inference(cnf_transformation,[],[f149]) ).
fof(f268,plain,
! [X2,X3,X0,X1,X4] :
( k1_funct_1(k5_relat_1(X3,X4),X2) = k1_funct_1(X4,k1_funct_1(X3,X2))
| ~ v1_funct_2(X3,X0,X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_1(X4)
| ~ v1_relat_1(X4)
| ~ r2_hidden(X2,X0)
| ~ m2_relset_1(X3,X0,X1)
| k1_xboole_0 = X1 ),
inference(cnf_transformation,[],[f152]) ).
fof(f269,plain,
! [X0,X1] :
( k8_funct_2(u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,k2_group_1(X0)),X1) = X1
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f154]) ).
fof(f270,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,X1)
| r2_hidden(X0,X1)
| v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f156]) ).
fof(f271,plain,
! [X2,X0,X1] :
( k2_group_3(X0,k2_group_3(X0,X1,k3_group_1(X0,X2)),X2) = X1
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f158]) ).
fof(f279,definition,
sF25 = u1_struct_0(sK0),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f280,plain,
u1_struct_0(sK0) = sF25,
inference(reorient_equations,[],[f279]) ).
fof(f281,definition,
sF26 = k3_group_1(sK0,sK1),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f282,plain,
k3_group_1(sK0,sK1) = sF26,
inference(reorient_equations,[],[f281]) ).
fof(f283,definition,
sF27 = k6_autgroup(sK0,sF26),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f284,plain,
k6_autgroup(sK0,sF26) = sF27,
inference(reorient_equations,[],[f283]) ).
fof(f285,definition,
sF28 = k6_autgroup(sK0,sK1),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f286,plain,
k6_autgroup(sK0,sK1) = sF28,
inference(reorient_equations,[],[f285]) ).
fof(f287,definition,
sF29 = k7_funct_2(sF25,sF25,sF25,sF27,sF28),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
fof(f288,plain,
k7_funct_2(sF25,sF25,sF25,sF27,sF28) = sF29,
inference(reorient_equations,[],[f287]) ).
fof(f289,definition,
sF30 = k2_group_1(sK0),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f290,plain,
k2_group_1(sK0) = sF30,
inference(reorient_equations,[],[f289]) ).
fof(f291,definition,
sF31 = k6_autgroup(sK0,sF30),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
fof(f292,plain,
k6_autgroup(sK0,sF30) = sF31,
inference(reorient_equations,[],[f291]) ).
fof(f293,plain,
sF29 != sF31,
inference(definition_folding,[],[f167,f292,f290,f288,f286,f284,f282,f280,f280,f280]) ).
fof(f294,plain,
m1_subset_1(sK1,sF25),
inference(definition_folding,[],[f166,f280]) ).
fof(f295,plain,
( m1_subset_1(sF26,u1_struct_0(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(superposition,[],[f190,f282]) ).
fof(f298,plain,
( m1_subset_1(sF26,u1_struct_0(sK0))
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f295,f168]) ).
fof(f300,plain,
( m1_subset_1(sF26,u1_struct_0(sK0))
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f298,f169]) ).
fof(f302,plain,
( m1_subset_1(sF26,u1_struct_0(sK0))
| v3_struct_0(sK0)
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f300,f170]) ).
fof(f304,plain,
( m1_subset_1(sF26,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f302,f172]) ).
fof(f305,plain,
( m1_subset_1(sF26,sF25)
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_demodulation,[],[f304,f280]) ).
fof(f306,plain,
( ~ m1_subset_1(sK1,sF25)
| m1_subset_1(sF26,sF25) ),
inference(forward_demodulation,[],[f305,f280]) ).
fof(f307,plain,
m1_subset_1(sF26,sF25),
inference(forward_subsumption_resolution,[],[f306,f294]) ).
fof(f308,plain,
( m2_fraenkel(sF31,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sF30,u1_struct_0(sK0)) ),
inference(superposition,[],[f193,f292]) ).
fof(f309,plain,
( m2_fraenkel(sF28,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(superposition,[],[f193,f286]) ).
fof(f310,plain,
( m2_fraenkel(sF27,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sF26,u1_struct_0(sK0)) ),
inference(superposition,[],[f193,f284]) ).
fof(f313,plain,
( m2_fraenkel(sF27,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sF26,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f310,f168]) ).
fof(f314,plain,
( m2_fraenkel(sF28,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f309,f168]) ).
fof(f315,plain,
( m2_fraenkel(sF31,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sF30,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f308,f168]) ).
fof(f317,plain,
( m2_fraenkel(sF27,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sF26,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f313,f169]) ).
fof(f318,plain,
( m2_fraenkel(sF28,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f314,f169]) ).
fof(f319,plain,
( m2_fraenkel(sF31,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sF30,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f315,f169]) ).
fof(f321,plain,
( m2_fraenkel(sF27,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sF26,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f317,f170]) ).
fof(f322,plain,
( m2_fraenkel(sF28,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f318,f170]) ).
fof(f323,plain,
( m2_fraenkel(sF31,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sF30,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f319,f170]) ).
fof(f325,plain,
( m2_fraenkel(sF27,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| v3_struct_0(sK0)
| ~ m1_subset_1(sF26,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f321,f171]) ).
fof(f326,plain,
( m2_fraenkel(sF28,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| v3_struct_0(sK0)
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f322,f171]) ).
fof(f327,plain,
( m2_fraenkel(sF31,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| v3_struct_0(sK0)
| ~ m1_subset_1(sF30,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f323,f171]) ).
fof(f329,plain,
( m2_fraenkel(sF27,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ m1_subset_1(sF26,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f325,f172]) ).
fof(f330,plain,
( m2_fraenkel(sF28,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f326,f172]) ).
fof(f331,plain,
( m2_fraenkel(sF31,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ m1_subset_1(sF30,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f327,f172]) ).
fof(f332,plain,
( m2_fraenkel(sF27,sF25,sF25,k4_autgroup(sK0))
| ~ m1_subset_1(sF26,u1_struct_0(sK0)) ),
inference(forward_demodulation,[],[f329,f280]) ).
fof(f333,plain,
( m2_fraenkel(sF28,sF25,sF25,k4_autgroup(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_demodulation,[],[f330,f280]) ).
fof(f334,plain,
( m2_fraenkel(sF31,sF25,sF25,k4_autgroup(sK0))
| ~ m1_subset_1(sF30,u1_struct_0(sK0)) ),
inference(forward_demodulation,[],[f331,f280]) ).
fof(f335,plain,
( ~ m1_subset_1(sF26,sF25)
| m2_fraenkel(sF27,sF25,sF25,k4_autgroup(sK0)) ),
inference(forward_demodulation,[],[f332,f280]) ).
fof(f336,plain,
( ~ m1_subset_1(sK1,sF25)
| m2_fraenkel(sF28,sF25,sF25,k4_autgroup(sK0)) ),
inference(forward_demodulation,[],[f333,f280]) ).
fof(f337,plain,
( ~ m1_subset_1(sF30,sF25)
| m2_fraenkel(sF31,sF25,sF25,k4_autgroup(sK0)) ),
inference(forward_demodulation,[],[f334,f280]) ).
fof(f338,plain,
m2_fraenkel(sF27,sF25,sF25,k4_autgroup(sK0)),
inference(forward_subsumption_resolution,[],[f335,f307]) ).
fof(f339,plain,
m2_fraenkel(sF28,sF25,sF25,k4_autgroup(sK0)),
inference(forward_subsumption_resolution,[],[f336,f294]) ).
fof(f360,plain,
! [X0] :
( k2_group_3(sK0,k2_group_3(sK0,X0,sF26),sK1) = X0
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l1_group_1(sK0) ),
inference(superposition,[],[f271,f282]) ).
fof(f365,plain,
! [X0] :
( k2_group_3(sK0,k2_group_3(sK0,X0,sF26),sK1) = X0
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f360,f169]) ).
fof(f367,plain,
! [X0] :
( k2_group_3(sK0,k2_group_3(sK0,X0,sF26),sK1) = X0
| v3_struct_0(sK0)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f365,f170]) ).
fof(f369,plain,
! [X0] :
( k2_group_3(sK0,k2_group_3(sK0,X0,sF26),sK1) = X0
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f367,f172]) ).
fof(f371,plain,
! [X0] :
( k2_group_3(sK0,k2_group_3(sK0,X0,sF26),sK1) = X0
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f369,f168]) ).
fof(f372,plain,
! [X0] :
( ~ m1_subset_1(X0,sF25)
| k2_group_3(sK0,k2_group_3(sK0,X0,sF26),sK1) = X0
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_demodulation,[],[f371,f280]) ).
fof(f373,plain,
! [X0] :
( ~ m1_subset_1(sK1,sF25)
| ~ m1_subset_1(X0,sF25)
| k2_group_3(sK0,k2_group_3(sK0,X0,sF26),sK1) = X0 ),
inference(forward_demodulation,[],[f372,f280]) ).
fof(f374,plain,
! [X0] :
( k2_group_3(sK0,k2_group_3(sK0,X0,sF26),sK1) = X0
| ~ m1_subset_1(X0,sF25) ),
inference(forward_subsumption_resolution,[],[f373,f294]) ).
fof(f389,definition,
( spl32_1
<=> m2_fraenkel(sF31,sF25,sF25,k4_autgroup(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_1])],[avatar_definition]) ).
fof(f391,plain,
( m2_fraenkel(sF31,sF25,sF25,k4_autgroup(sK0))
| ~ spl32_1 ),
inference(avatar_component_clause,[],[f389]) ).
fof(f393,definition,
( spl32_2
<=> m1_subset_1(sF30,sF25) ),
introduced(definition,[new_symbols(definition,[spl32_2])],[avatar_definition]) ).
fof(f394,plain,
( m1_subset_1(sF30,sF25)
| ~ spl32_2 ),
inference(avatar_component_clause,[],[f393]) ).
fof(f395,plain,
( ~ m1_subset_1(sF30,sF25)
| spl32_2 ),
inference(avatar_component_clause,[],[f393]) ).
fof(f396,plain,
( spl32_1
| ~ spl32_2 ),
inference(avatar_split_clause,[],[f337,f393,f389]) ).
fof(f397,plain,
! [X0] :
( k8_funct_2(sF25,sF25,k6_autgroup(sK0,k2_group_1(sK0)),X0) = X0
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(X0,sF25)
| ~ l1_group_1(sK0) ),
inference(superposition,[],[f269,f280]) ).
fof(f400,plain,
! [X0] :
( k8_funct_2(sF25,sF25,k6_autgroup(sK0,k2_group_1(sK0)),X0) = X0
| ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(X0,sF25)
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f397,f169]) ).
fof(f402,plain,
! [X0] :
( k8_funct_2(sF25,sF25,k6_autgroup(sK0,k2_group_1(sK0)),X0) = X0
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(X0,sF25)
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f400,f170]) ).
fof(f404,plain,
! [X0] :
( k8_funct_2(sF25,sF25,k6_autgroup(sK0,k2_group_1(sK0)),X0) = X0
| v3_struct_0(sK0)
| ~ m1_subset_1(X0,sF25)
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f402,f171]) ).
fof(f406,plain,
! [X0] :
( k8_funct_2(sF25,sF25,k6_autgroup(sK0,k2_group_1(sK0)),X0) = X0
| ~ m1_subset_1(X0,sF25)
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f404,f172]) ).
fof(f408,plain,
! [X0] :
( k8_funct_2(sF25,sF25,k6_autgroup(sK0,k2_group_1(sK0)),X0) = X0
| ~ m1_subset_1(X0,sF25) ),
inference(forward_subsumption_resolution,[],[f406,f168]) ).
fof(f410,plain,
! [X0] :
( k8_funct_2(sF25,sF25,k6_autgroup(sK0,sF30),X0) = X0
| ~ m1_subset_1(X0,sF25) ),
inference(forward_demodulation,[],[f408,f290]) ).
fof(f412,plain,
! [X0] :
( k8_funct_2(sF25,sF25,sF31,X0) = X0
| ~ m1_subset_1(X0,sF25) ),
inference(forward_demodulation,[],[f410,f292]) ).
fof(f417,plain,
l1_struct_0(sK0),
inference(resolution,[],[f198,f168]) ).
fof(f419,plain,
! [X0,X1] :
( v1_xboole_0(u1_struct_0(X0))
| ~ m1_fraenkel(k4_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| v1_funct_1(k6_autgroup(X0,X1))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(resolution,[],[f203,f193]) ).
fof(f421,plain,
( v1_xboole_0(sF25)
| ~ m1_fraenkel(k4_autgroup(sK0),sF25,sF25)
| v1_funct_1(sF27) ),
inference(resolution,[],[f203,f338]) ).
fof(f422,plain,
( v1_xboole_0(sF25)
| ~ m1_fraenkel(k4_autgroup(sK0),sF25,sF25)
| v1_funct_1(sF28) ),
inference(resolution,[],[f203,f339]) ).
fof(f423,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| v1_funct_1(k6_autgroup(X0,X1))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0)
| v1_xboole_0(u1_struct_0(X0)) ),
inference(forward_subsumption_resolution,[],[f419,f191]) ).
fof(f424,plain,
! [X0,X1] :
( v1_xboole_0(u1_struct_0(X0))
| ~ m1_fraenkel(k4_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| v1_funct_2(k6_autgroup(X0,X1),u1_struct_0(X0),u1_struct_0(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(resolution,[],[f202,f193]) ).
fof(f426,plain,
( v1_xboole_0(sF25)
| ~ m1_fraenkel(k4_autgroup(sK0),sF25,sF25)
| v1_funct_2(sF27,sF25,sF25) ),
inference(resolution,[],[f202,f338]) ).
fof(f427,plain,
( v1_xboole_0(sF25)
| ~ m1_fraenkel(k4_autgroup(sK0),sF25,sF25)
| v1_funct_2(sF28,sF25,sF25) ),
inference(resolution,[],[f202,f339]) ).
fof(f428,plain,
! [X0,X1] :
( v1_funct_2(k6_autgroup(X0,X1),u1_struct_0(X0),u1_struct_0(X0))
| v1_xboole_0(u1_struct_0(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(forward_subsumption_resolution,[],[f424,f191]) ).
fof(f472,plain,
( m1_subset_1(sF30,u1_struct_0(sK0))
| v3_struct_0(sK0)
| ~ l1_group_1(sK0) ),
inference(superposition,[],[f188,f290]) ).
fof(f475,plain,
( m1_subset_1(sF30,u1_struct_0(sK0))
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f472,f172]) ).
fof(f477,plain,
m1_subset_1(sF30,u1_struct_0(sK0)),
inference(forward_subsumption_resolution,[],[f475,f168]) ).
fof(f479,plain,
m1_subset_1(sF30,sF25),
inference(forward_demodulation,[],[f477,f280]) ).
fof(f482,plain,
( $false
| spl32_2 ),
inference(forward_subsumption_resolution,[],[f479,f395]) ).
fof(f483,plain,
spl32_2,
inference(avatar_contradiction_clause,[],[f482]) ).
fof(f488,plain,
( v1_xboole_0(sF25)
| m1_subset_1(sF27,k4_autgroup(sK0))
| ~ m1_fraenkel(k4_autgroup(sK0),sF25,sF25) ),
inference(resolution,[],[f261,f338]) ).
fof(f489,plain,
( v1_xboole_0(sF25)
| m1_subset_1(sF28,k4_autgroup(sK0))
| ~ m1_fraenkel(k4_autgroup(sK0),sF25,sF25) ),
inference(resolution,[],[f261,f339]) ).
fof(f490,plain,
( v1_xboole_0(sF25)
| m1_subset_1(sF31,k4_autgroup(sK0))
| ~ m1_fraenkel(k4_autgroup(sK0),sF25,sF25)
| ~ spl32_1 ),
inference(resolution,[],[f261,f391]) ).
fof(f493,plain,
! [X2,X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X2)
| ~ m1_fraenkel(X2,X3,X0)
| v1_xboole_0(X0)
| ~ m1_fraenkel(X2,X3,X0)
| v1_funct_2(X1,X3,X0) ),
inference(resolution,[],[f260,f202]) ).
fof(f494,plain,
! [X2,X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X2)
| ~ m1_fraenkel(X2,X3,X0)
| v1_xboole_0(X0)
| ~ m1_fraenkel(X2,X3,X0)
| v1_funct_1(X1) ),
inference(resolution,[],[f260,f203]) ).
fof(f495,plain,
! [X2,X3,X0,X1] :
( ~ m1_fraenkel(X2,X3,X0)
| ~ m1_subset_1(X1,X2)
| v1_xboole_0(X0)
| v1_funct_1(X1) ),
inference(duplicate_literal_removal,[],[f494]) ).
fof(f496,plain,
! [X2,X3,X0,X1] :
( ~ m1_fraenkel(X2,X3,X0)
| ~ m1_subset_1(X1,X2)
| v1_xboole_0(X0)
| v1_funct_2(X1,X3,X0) ),
inference(duplicate_literal_removal,[],[f493]) ).
fof(f498,plain,
( m1_fraenkel(k4_autgroup(sK0),sF25,sF25)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0) ),
inference(superposition,[],[f191,f280]) ).
fof(f499,plain,
( m1_fraenkel(k4_autgroup(sK0),sF25,sF25)
| ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f498,f169]) ).
fof(f500,plain,
( m1_fraenkel(k4_autgroup(sK0),sF25,sF25)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f499,f170]) ).
fof(f501,plain,
( m1_fraenkel(k4_autgroup(sK0),sF25,sF25)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f500,f171]) ).
fof(f502,plain,
( m1_fraenkel(k4_autgroup(sK0),sF25,sF25)
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f501,f172]) ).
fof(f503,plain,
m1_fraenkel(k4_autgroup(sK0),sF25,sF25),
inference(forward_subsumption_resolution,[],[f502,f168]) ).
fof(f511,plain,
! [X0,X1] :
( m1_subset_1(k2_group_3(sK0,X0,X1),sF25)
| ~ m1_subset_1(X0,sF25)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(X1,sF25) ),
inference(superposition,[],[f189,f280]) ).
fof(f514,plain,
! [X0,X1] :
( m1_subset_1(k2_group_3(sK0,X0,X1),sF25)
| ~ m1_subset_1(X0,sF25)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(X1,sF25) ),
inference(forward_subsumption_resolution,[],[f511,f168]) ).
fof(f518,plain,
! [X0,X1] :
( m1_subset_1(k2_group_3(sK0,X0,X1),sF25)
| ~ m1_subset_1(X0,sF25)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(X1,sF25) ),
inference(forward_subsumption_resolution,[],[f514,f169]) ).
fof(f522,plain,
! [X0,X1] :
( m1_subset_1(k2_group_3(sK0,X0,X1),sF25)
| ~ m1_subset_1(X0,sF25)
| v3_struct_0(sK0)
| ~ m1_subset_1(X1,sF25) ),
inference(forward_subsumption_resolution,[],[f518,f170]) ).
fof(f526,plain,
! [X0,X1] :
( m1_subset_1(k2_group_3(sK0,X0,X1),sF25)
| ~ m1_subset_1(X0,sF25)
| ~ m1_subset_1(X1,sF25) ),
inference(forward_subsumption_resolution,[],[f522,f172]) ).
fof(f550,plain,
! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK0))
| v1_xboole_0(sF25)
| v1_funct_1(X0) ),
inference(resolution,[],[f495,f503]) ).
fof(f551,plain,
! [X0,X1] :
( sF31 != X0
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sF30,u1_struct_0(sK0))
| ~ m2_fraenkel(X0,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| k8_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),X0,X1) = k2_group_3(sK0,X1,sF30)
| ~ l1_group_1(sK0) ),
inference(superposition,[],[f183,f292]) ).
fof(f554,plain,
! [X2,X0,X1] :
( ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m2_fraenkel(k6_autgroup(X0,X1),u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| k8_funct_2(u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,X1),X2) = k2_group_3(X0,X2,X1)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f183]) ).
fof(f555,plain,
! [X2,X0,X1] :
( k8_funct_2(u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,X1),X2) = k2_group_3(X0,X2,X1)
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f554,f193]) ).
fof(f558,plain,
! [X0,X1] :
( sF31 != X0
| ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sF30,u1_struct_0(sK0))
| ~ m2_fraenkel(X0,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| k8_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),X0,X1) = k2_group_3(sK0,X1,sF30)
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f551,f169]) ).
fof(f561,plain,
! [X0,X1] :
( sF31 != X0
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sF30,u1_struct_0(sK0))
| ~ m2_fraenkel(X0,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| k8_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),X0,X1) = k2_group_3(sK0,X1,sF30)
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f558,f170]) ).
fof(f564,plain,
! [X0,X1] :
( sF31 != X0
| v3_struct_0(sK0)
| ~ m1_subset_1(sF30,u1_struct_0(sK0))
| ~ m2_fraenkel(X0,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| k8_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),X0,X1) = k2_group_3(sK0,X1,sF30)
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f561,f171]) ).
fof(f567,plain,
! [X0,X1] :
( sF31 != X0
| ~ m1_subset_1(sF30,u1_struct_0(sK0))
| ~ m2_fraenkel(X0,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| k8_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),X0,X1) = k2_group_3(sK0,X1,sF30)
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f564,f172]) ).
fof(f570,plain,
! [X0,X1] :
( sF31 != X0
| ~ m1_subset_1(sF30,u1_struct_0(sK0))
| ~ m2_fraenkel(X0,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| k8_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),X0,X1) = k2_group_3(sK0,X1,sF30) ),
inference(forward_subsumption_resolution,[],[f567,f168]) ).
fof(f573,plain,
! [X0,X1] :
( ~ m1_subset_1(sF30,sF25)
| sF31 != X0
| ~ m2_fraenkel(X0,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| k8_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),X0,X1) = k2_group_3(sK0,X1,sF30) ),
inference(forward_demodulation,[],[f570,f280]) ).
fof(f576,plain,
( ! [X0,X1] :
( sF31 != X0
| ~ m2_fraenkel(X0,u1_struct_0(sK0),u1_struct_0(sK0),k4_autgroup(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| k8_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),X0,X1) = k2_group_3(sK0,X1,sF30) )
| ~ spl32_2 ),
inference(forward_subsumption_resolution,[],[f573,f394]) ).
fof(f579,plain,
( ! [X0,X1] :
( ~ m2_fraenkel(X0,sF25,sF25,k4_autgroup(sK0))
| sF31 != X0
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| k8_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),X0,X1) = k2_group_3(sK0,X1,sF30) )
| ~ spl32_2 ),
inference(forward_demodulation,[],[f576,f280]) ).
fof(f582,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF25)
| ~ m2_fraenkel(X0,sF25,sF25,k4_autgroup(sK0))
| sF31 != X0
| k8_funct_2(u1_struct_0(sK0),u1_struct_0(sK0),X0,X1) = k2_group_3(sK0,X1,sF30) )
| ~ spl32_2 ),
inference(forward_demodulation,[],[f579,f280]) ).
fof(f585,plain,
( ! [X0,X1] :
( sF31 != X0
| ~ m1_subset_1(X1,sF25)
| ~ m2_fraenkel(X0,sF25,sF25,k4_autgroup(sK0))
| k2_group_3(sK0,X1,sF30) = k8_funct_2(sF25,sF25,X0,X1) )
| ~ spl32_2 ),
inference(forward_demodulation,[],[f582,f280]) ).
fof(f598,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF25)
| ~ m2_fraenkel(sF31,sF25,sF25,k4_autgroup(sK0))
| k8_funct_2(sF25,sF25,sF31,X0) = k2_group_3(sK0,X0,sF30) )
| ~ spl32_2 ),
inference(equality_resolution,[],[f585]) ).
fof(f599,plain,
( ! [X0] :
( k8_funct_2(sF25,sF25,sF31,X0) = k2_group_3(sK0,X0,sF30)
| ~ m1_subset_1(X0,sF25) )
| ~ spl32_1
| ~ spl32_2 ),
inference(forward_subsumption_resolution,[],[f598,f391]) ).
fof(f602,plain,
( ! [X0] :
( k2_group_3(sK0,X0,sF30) = X0
| ~ m1_subset_1(X0,sF25)
| ~ m1_subset_1(X0,sF25) )
| ~ spl32_1
| ~ spl32_2 ),
inference(superposition,[],[f412,f599]) ).
fof(f605,plain,
( ! [X0] :
( k2_group_3(sK0,X0,sF30) = X0
| ~ m1_subset_1(X0,sF25) )
| ~ spl32_1
| ~ spl32_2 ),
inference(duplicate_literal_removal,[],[f602]) ).
fof(f675,plain,
( sF29 = k5_relat_1(sF27,sF28)
| ~ v1_funct_2(sF28,sF25,sF25)
| ~ v1_funct_1(sF28)
| ~ m1_relset_1(sF27,sF25,sF25)
| ~ v1_funct_2(sF27,sF25,sF25)
| ~ v1_funct_1(sF27)
| v1_xboole_0(sF25)
| ~ m1_relset_1(sF28,sF25,sF25) ),
inference(superposition,[],[f288,f258]) ).
fof(f752,plain,
( ~ v1_xboole_0(sF25)
| v3_struct_0(sK0)
| ~ l1_struct_0(sK0) ),
inference(superposition,[],[f219,f280]) ).
fof(f753,plain,
( ~ v1_xboole_0(sF25)
| ~ l1_struct_0(sK0) ),
inference(forward_subsumption_resolution,[],[f752,f172]) ).
fof(f754,plain,
~ v1_xboole_0(sF25),
inference(forward_subsumption_resolution,[],[f753,f417]) ).
fof(f757,plain,
( v1_xboole_0(sF25)
| ~ m1_fraenkel(k4_autgroup(sK0),sF25,sF25)
| m2_relset_1(sF27,sF25,sF25) ),
inference(resolution,[],[f201,f338]) ).
fof(f758,plain,
( v1_xboole_0(sF25)
| ~ m1_fraenkel(k4_autgroup(sK0),sF25,sF25)
| m2_relset_1(sF28,sF25,sF25) ),
inference(resolution,[],[f201,f339]) ).
fof(f759,plain,
( v1_xboole_0(sF25)
| ~ m1_fraenkel(k4_autgroup(sK0),sF25,sF25)
| m2_relset_1(sF31,sF25,sF25)
| ~ spl32_1 ),
inference(resolution,[],[f201,f391]) ).
fof(f762,plain,
( ~ m1_fraenkel(k4_autgroup(sK0),sF25,sF25)
| m2_relset_1(sF31,sF25,sF25)
| ~ spl32_1 ),
inference(forward_subsumption_resolution,[],[f759,f754]) ).
fof(f763,plain,
( ~ m1_fraenkel(k4_autgroup(sK0),sF25,sF25)
| m2_relset_1(sF28,sF25,sF25) ),
inference(forward_subsumption_resolution,[],[f758,f754]) ).
fof(f764,plain,
( ~ m1_fraenkel(k4_autgroup(sK0),sF25,sF25)
| m2_relset_1(sF27,sF25,sF25) ),
inference(forward_subsumption_resolution,[],[f757,f754]) ).
fof(f767,plain,
( m2_relset_1(sF31,sF25,sF25)
| ~ spl32_1 ),
inference(forward_subsumption_resolution,[],[f762,f503]) ).
fof(f768,plain,
m2_relset_1(sF28,sF25,sF25),
inference(forward_subsumption_resolution,[],[f763,f503]) ).
fof(f769,plain,
m2_relset_1(sF27,sF25,sF25),
inference(forward_subsumption_resolution,[],[f764,f503]) ).
fof(f775,definition,
( spl32_3
<=> m1_fraenkel(k4_autgroup(sK0),sF25,sF25) ),
introduced(definition,[new_symbols(definition,[spl32_3])],[avatar_definition]) ).
fof(f777,plain,
( ~ m1_fraenkel(k4_autgroup(sK0),sF25,sF25)
| spl32_3 ),
inference(avatar_component_clause,[],[f775]) ).
fof(f779,definition,
( spl32_4
<=> m1_subset_1(sF28,k4_autgroup(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_4])],[avatar_definition]) ).
fof(f781,plain,
( m1_subset_1(sF28,k4_autgroup(sK0))
| ~ spl32_4 ),
inference(avatar_component_clause,[],[f779]) ).
fof(f783,definition,
( spl32_5
<=> v1_xboole_0(sF25) ),
introduced(definition,[new_symbols(definition,[spl32_5])],[avatar_definition]) ).
fof(f785,plain,
( v1_xboole_0(sF25)
| ~ spl32_5 ),
inference(avatar_component_clause,[],[f783]) ).
fof(f786,plain,
( ~ spl32_3
| spl32_4
| spl32_5 ),
inference(avatar_split_clause,[],[f489,f783,f779,f775]) ).
fof(f787,plain,
( $false
| spl32_3 ),
inference(forward_subsumption_resolution,[],[f777,f503]) ).
fof(f788,plain,
spl32_3,
inference(avatar_contradiction_clause,[],[f787]) ).
fof(f789,plain,
( $false
| ~ spl32_5 ),
inference(forward_subsumption_resolution,[],[f785,f754]) ).
fof(f790,plain,
~ spl32_5,
inference(avatar_contradiction_clause,[],[f789]) ).
fof(f803,plain,
! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK0))
| v1_xboole_0(sF25)
| v1_funct_2(X0,sF25,sF25) ),
inference(resolution,[],[f496,f503]) ).
fof(f804,plain,
! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK0))
| v1_funct_2(X0,sF25,sF25) ),
inference(forward_subsumption_resolution,[],[f803,f754]) ).
fof(f805,plain,
( v1_funct_2(sF28,sF25,sF25)
| ~ spl32_4 ),
inference(resolution,[],[f804,f781]) ).
fof(f813,plain,
! [X2,X0,X1] :
( k2_group_3(X0,X1,X2) = k1_funct_1(k6_autgroup(X0,X2),X1)
| ~ m1_relset_1(k6_autgroup(X0,X2),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(k6_autgroup(X0,X2),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(k6_autgroup(X0,X2))
| v1_xboole_0(u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(superposition,[],[f259,f555]) ).
fof(f814,plain,
! [X2,X0,X1] :
( k2_group_3(X0,X1,X2) = k1_funct_1(k6_autgroup(X0,X2),X1)
| ~ m1_relset_1(k6_autgroup(X0,X2),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(k6_autgroup(X0,X2),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(k6_autgroup(X0,X2))
| v1_xboole_0(u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(duplicate_literal_removal,[],[f813]) ).
fof(f818,plain,
! [X2,X0,X1] :
( k2_group_3(X0,X1,X2) = k1_funct_1(k6_autgroup(X0,X2),X1)
| ~ m1_relset_1(k6_autgroup(X0,X2),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(k6_autgroup(X0,X2))
| v1_xboole_0(u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f814,f428]) ).
fof(f826,plain,
! [X2,X0,X1] :
( k2_group_3(X0,X1,X2) = k1_funct_1(k6_autgroup(X0,X2),X1)
| ~ m1_relset_1(k6_autgroup(X0,X2),u1_struct_0(X0),u1_struct_0(X0))
| v1_xboole_0(u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f818,f423]) ).
fof(f942,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,X1,X2)
| v1_relat_1(X0) ),
inference(resolution,[],[f204,f179]) ).
fof(f963,plain,
( v1_funct_1(sF29)
| ~ v1_funct_2(sF28,sF25,sF25)
| ~ v1_funct_1(sF28)
| ~ m1_relset_1(sF27,sF25,sF25)
| ~ v1_funct_2(sF27,sF25,sF25)
| ~ v1_funct_1(sF27)
| v1_xboole_0(sF25)
| ~ m1_relset_1(sF28,sF25,sF25) ),
inference(superposition,[],[f196,f288]) ).
fof(f966,plain,
( v1_funct_1(sF29)
| ~ v1_funct_1(sF28)
| ~ m1_relset_1(sF27,sF25,sF25)
| ~ v1_funct_2(sF27,sF25,sF25)
| ~ v1_funct_1(sF27)
| v1_xboole_0(sF25)
| ~ m1_relset_1(sF28,sF25,sF25)
| ~ spl32_4 ),
inference(forward_subsumption_resolution,[],[f963,f805]) ).
fof(f967,plain,
( v1_funct_1(sF29)
| ~ v1_funct_1(sF28)
| ~ m1_relset_1(sF27,sF25,sF25)
| ~ v1_funct_2(sF27,sF25,sF25)
| ~ v1_funct_1(sF27)
| ~ m1_relset_1(sF28,sF25,sF25)
| ~ spl32_4 ),
inference(forward_subsumption_resolution,[],[f966,f754]) ).
fof(f968,plain,
( v1_funct_2(sF29,sF25,sF25)
| ~ v1_funct_2(sF28,sF25,sF25)
| ~ v1_funct_1(sF28)
| ~ m1_relset_1(sF27,sF25,sF25)
| ~ v1_funct_2(sF27,sF25,sF25)
| ~ v1_funct_1(sF27)
| v1_xboole_0(sF25)
| ~ m1_relset_1(sF28,sF25,sF25) ),
inference(superposition,[],[f195,f288]) ).
fof(f971,plain,
( v1_funct_2(sF29,sF25,sF25)
| ~ v1_funct_1(sF28)
| ~ m1_relset_1(sF27,sF25,sF25)
| ~ v1_funct_2(sF27,sF25,sF25)
| ~ v1_funct_1(sF27)
| v1_xboole_0(sF25)
| ~ m1_relset_1(sF28,sF25,sF25)
| ~ spl32_4 ),
inference(forward_subsumption_resolution,[],[f968,f805]) ).
fof(f972,plain,
( v1_funct_2(sF29,sF25,sF25)
| ~ v1_funct_1(sF28)
| ~ m1_relset_1(sF27,sF25,sF25)
| ~ v1_funct_2(sF27,sF25,sF25)
| ~ v1_funct_1(sF27)
| ~ m1_relset_1(sF28,sF25,sF25)
| ~ spl32_4 ),
inference(forward_subsumption_resolution,[],[f971,f754]) ).
fof(f974,definition,
( spl32_8
<=> ! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK0))
| v1_funct_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl32_8])],[avatar_definition]) ).
fof(f975,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK0))
| v1_funct_1(X0) )
| ~ spl32_8 ),
inference(avatar_component_clause,[],[f974]) ).
fof(f976,plain,
( spl32_5
| spl32_8 ),
inference(avatar_split_clause,[],[f550,f974,f783]) ).
fof(f977,plain,
( v1_funct_1(sF28)
| ~ spl32_4
| ~ spl32_8 ),
inference(resolution,[],[f975,f781]) ).
fof(f978,plain,
( m1_relset_1(sF31,sF25,sF25)
| ~ spl32_1 ),
inference(resolution,[],[f263,f767]) ).
fof(f979,plain,
m1_relset_1(sF28,sF25,sF25),
inference(resolution,[],[f263,f768]) ).
fof(f980,plain,
m1_relset_1(sF27,sF25,sF25),
inference(resolution,[],[f263,f769]) ).
fof(f1017,definition,
( spl32_10
<=> m1_subset_1(sF27,k4_autgroup(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_10])],[avatar_definition]) ).
fof(f1019,plain,
( m1_subset_1(sF27,k4_autgroup(sK0))
| ~ spl32_10 ),
inference(avatar_component_clause,[],[f1017]) ).
fof(f1020,plain,
( ~ spl32_3
| spl32_10
| spl32_5 ),
inference(avatar_split_clause,[],[f488,f783,f1017,f775]) ).
fof(f1021,plain,
( v1_funct_1(sF27)
| ~ spl32_8
| ~ spl32_10 ),
inference(resolution,[],[f1019,f975]) ).
fof(f1022,plain,
( v1_funct_2(sF27,sF25,sF25)
| ~ spl32_10 ),
inference(resolution,[],[f1019,f804]) ).
fof(f1048,definition,
( spl32_11
<=> m1_subset_1(sF31,k4_autgroup(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_11])],[avatar_definition]) ).
fof(f1050,plain,
( m1_subset_1(sF31,k4_autgroup(sK0))
| ~ spl32_11 ),
inference(avatar_component_clause,[],[f1048]) ).
fof(f1051,plain,
( ~ spl32_3
| spl32_11
| spl32_5
| ~ spl32_1 ),
inference(avatar_split_clause,[],[f490,f389,f783,f1048,f775]) ).
fof(f1052,plain,
( v1_funct_1(sF31)
| ~ spl32_8
| ~ spl32_11 ),
inference(resolution,[],[f1050,f975]) ).
fof(f1053,plain,
( v1_funct_2(sF31,sF25,sF25)
| ~ spl32_11 ),
inference(resolution,[],[f1050,f804]) ).
fof(f1134,plain,
v1_relat_1(sF28),
inference(resolution,[],[f942,f768]) ).
fof(f1137,definition,
( spl32_16
<=> v1_funct_1(sF28) ),
introduced(definition,[new_symbols(definition,[spl32_16])],[avatar_definition]) ).
fof(f1139,plain,
( v1_funct_1(sF28)
| ~ spl32_16 ),
inference(avatar_component_clause,[],[f1137]) ).
fof(f1140,plain,
( spl32_16
| ~ spl32_3
| spl32_5 ),
inference(avatar_split_clause,[],[f422,f783,f775,f1137]) ).
fof(f1160,definition,
( spl32_17
<=> v1_funct_2(sF28,sF25,sF25) ),
introduced(definition,[new_symbols(definition,[spl32_17])],[avatar_definition]) ).
fof(f1162,plain,
( v1_funct_2(sF28,sF25,sF25)
| ~ spl32_17 ),
inference(avatar_component_clause,[],[f1160]) ).
fof(f1163,plain,
( spl32_17
| ~ spl32_3
| spl32_5 ),
inference(avatar_split_clause,[],[f427,f783,f775,f1160]) ).
fof(f1565,plain,
( m2_relset_1(sF29,sF25,sF25)
| ~ v1_funct_2(sF28,sF25,sF25)
| ~ v1_funct_1(sF28)
| ~ m1_relset_1(sF27,sF25,sF25)
| ~ v1_funct_2(sF27,sF25,sF25)
| ~ v1_funct_1(sF27)
| v1_xboole_0(sF25)
| ~ m1_relset_1(sF28,sF25,sF25) ),
inference(superposition,[],[f194,f288]) ).
fof(f1568,plain,
( m2_relset_1(sF29,sF25,sF25)
| ~ v1_funct_1(sF28)
| ~ m1_relset_1(sF27,sF25,sF25)
| ~ v1_funct_2(sF27,sF25,sF25)
| ~ v1_funct_1(sF27)
| v1_xboole_0(sF25)
| ~ m1_relset_1(sF28,sF25,sF25)
| ~ spl32_17 ),
inference(forward_subsumption_resolution,[],[f1565,f1162]) ).
fof(f1569,plain,
( m2_relset_1(sF29,sF25,sF25)
| ~ m1_relset_1(sF27,sF25,sF25)
| ~ v1_funct_2(sF27,sF25,sF25)
| ~ v1_funct_1(sF27)
| v1_xboole_0(sF25)
| ~ m1_relset_1(sF28,sF25,sF25)
| ~ spl32_4
| ~ spl32_8
| ~ spl32_17 ),
inference(forward_subsumption_resolution,[],[f1568,f977]) ).
fof(f1570,plain,
( m2_relset_1(sF29,sF25,sF25)
| ~ v1_funct_2(sF27,sF25,sF25)
| ~ v1_funct_1(sF27)
| v1_xboole_0(sF25)
| ~ m1_relset_1(sF28,sF25,sF25)
| ~ spl32_4
| ~ spl32_8
| ~ spl32_17 ),
inference(forward_subsumption_resolution,[],[f1569,f980]) ).
fof(f1571,plain,
( m2_relset_1(sF29,sF25,sF25)
| ~ v1_funct_1(sF27)
| v1_xboole_0(sF25)
| ~ m1_relset_1(sF28,sF25,sF25)
| ~ spl32_4
| ~ spl32_8
| ~ spl32_10
| ~ spl32_17 ),
inference(forward_subsumption_resolution,[],[f1570,f1022]) ).
fof(f1572,plain,
( m2_relset_1(sF29,sF25,sF25)
| v1_xboole_0(sF25)
| ~ m1_relset_1(sF28,sF25,sF25)
| ~ spl32_4
| ~ spl32_8
| ~ spl32_10
| ~ spl32_17 ),
inference(forward_subsumption_resolution,[],[f1571,f1021]) ).
fof(f1573,plain,
( m2_relset_1(sF29,sF25,sF25)
| ~ m1_relset_1(sF28,sF25,sF25)
| ~ spl32_4
| ~ spl32_8
| ~ spl32_10
| ~ spl32_17 ),
inference(forward_subsumption_resolution,[],[f1572,f754]) ).
fof(f1574,plain,
( m2_relset_1(sF29,sF25,sF25)
| ~ spl32_4
| ~ spl32_8
| ~ spl32_10
| ~ spl32_17 ),
inference(forward_subsumption_resolution,[],[f1573,f979]) ).
fof(f1579,plain,
! [X0] :
( k2_group_3(sK0,X0,sK1) = k1_funct_1(sF28,X0)
| ~ m1_relset_1(sF28,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ v4_group_1(sK0)
| ~ l1_group_1(sK0) ),
inference(superposition,[],[f826,f286]) ).
fof(f1580,plain,
! [X0] :
( k2_group_3(sK0,X0,sF26) = k1_funct_1(sF27,X0)
| ~ m1_relset_1(sF27,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sF26,u1_struct_0(sK0))
| ~ v4_group_1(sK0)
| ~ l1_group_1(sK0) ),
inference(superposition,[],[f826,f284]) ).
fof(f1581,plain,
! [X0] :
( k1_funct_1(sF31,X0) = k2_group_3(sK0,X0,sF30)
| ~ m1_relset_1(sF31,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ v3_group_1(sK0)
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sF30,u1_struct_0(sK0))
| ~ v4_group_1(sK0)
| ~ l1_group_1(sK0) ),
inference(superposition,[],[f826,f292]) ).
fof(f1582,plain,
! [X0] :
( k1_funct_1(sF31,X0) = k2_group_3(sK0,X0,sF30)
| ~ m1_relset_1(sF31,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sF30,u1_struct_0(sK0))
| ~ v4_group_1(sK0)
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1581,f170]) ).
fof(f1583,plain,
! [X0] :
( k2_group_3(sK0,X0,sF26) = k1_funct_1(sF27,X0)
| ~ m1_relset_1(sF27,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sF26,u1_struct_0(sK0))
| ~ v4_group_1(sK0)
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1580,f170]) ).
fof(f1584,plain,
! [X0] :
( k2_group_3(sK0,X0,sK1) = k1_funct_1(sF28,X0)
| ~ m1_relset_1(sF28,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ v1_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ v4_group_1(sK0)
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1579,f170]) ).
fof(f1586,plain,
! [X0] :
( k1_funct_1(sF31,X0) = k2_group_3(sK0,X0,sF30)
| ~ m1_relset_1(sF31,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| v3_struct_0(sK0)
| ~ m1_subset_1(sF30,u1_struct_0(sK0))
| ~ v4_group_1(sK0)
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1582,f171]) ).
fof(f1587,plain,
! [X0] :
( k2_group_3(sK0,X0,sF26) = k1_funct_1(sF27,X0)
| ~ m1_relset_1(sF27,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| v3_struct_0(sK0)
| ~ m1_subset_1(sF26,u1_struct_0(sK0))
| ~ v4_group_1(sK0)
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1583,f171]) ).
fof(f1588,plain,
! [X0] :
( k2_group_3(sK0,X0,sK1) = k1_funct_1(sF28,X0)
| ~ m1_relset_1(sF28,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| v3_struct_0(sK0)
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ v4_group_1(sK0)
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1584,f171]) ).
fof(f1590,plain,
! [X0] :
( k1_funct_1(sF31,X0) = k2_group_3(sK0,X0,sF30)
| ~ m1_relset_1(sF31,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sF30,u1_struct_0(sK0))
| ~ v4_group_1(sK0)
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1586,f172]) ).
fof(f1591,plain,
! [X0] :
( k2_group_3(sK0,X0,sF26) = k1_funct_1(sF27,X0)
| ~ m1_relset_1(sF27,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sF26,u1_struct_0(sK0))
| ~ v4_group_1(sK0)
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1587,f172]) ).
fof(f1592,plain,
! [X0] :
( k2_group_3(sK0,X0,sK1) = k1_funct_1(sF28,X0)
| ~ m1_relset_1(sF28,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ v4_group_1(sK0)
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1588,f172]) ).
fof(f1594,plain,
! [X0] :
( k1_funct_1(sF31,X0) = k2_group_3(sK0,X0,sF30)
| ~ m1_relset_1(sF31,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sF30,u1_struct_0(sK0))
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1590,f169]) ).
fof(f1595,plain,
! [X0] :
( k2_group_3(sK0,X0,sF26) = k1_funct_1(sF27,X0)
| ~ m1_relset_1(sF27,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sF26,u1_struct_0(sK0))
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1591,f169]) ).
fof(f1596,plain,
! [X0] :
( k2_group_3(sK0,X0,sK1) = k1_funct_1(sF28,X0)
| ~ m1_relset_1(sF28,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1592,f169]) ).
fof(f1598,plain,
! [X0] :
( k1_funct_1(sF31,X0) = k2_group_3(sK0,X0,sF30)
| ~ m1_relset_1(sF31,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sF30,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f1594,f168]) ).
fof(f1599,plain,
! [X0] :
( k2_group_3(sK0,X0,sF26) = k1_funct_1(sF27,X0)
| ~ m1_relset_1(sF27,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sF26,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f1595,f168]) ).
fof(f1600,plain,
! [X0] :
( k2_group_3(sK0,X0,sK1) = k1_funct_1(sF28,X0)
| ~ m1_relset_1(sF28,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f1596,f168]) ).
fof(f1602,plain,
! [X0] :
( ~ m1_relset_1(sF31,sF25,sF25)
| k1_funct_1(sF31,X0) = k2_group_3(sK0,X0,sF30)
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sF30,u1_struct_0(sK0)) ),
inference(forward_demodulation,[],[f1598,f280]) ).
fof(f1603,plain,
! [X0] :
( ~ m1_relset_1(sF27,sF25,sF25)
| k2_group_3(sK0,X0,sF26) = k1_funct_1(sF27,X0)
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sF26,u1_struct_0(sK0)) ),
inference(forward_demodulation,[],[f1599,f280]) ).
fof(f1604,plain,
! [X0] :
( ~ m1_relset_1(sF28,sF25,sF25)
| k2_group_3(sK0,X0,sK1) = k1_funct_1(sF28,X0)
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_demodulation,[],[f1600,f280]) ).
fof(f1606,plain,
( ! [X0] :
( k1_funct_1(sF31,X0) = k2_group_3(sK0,X0,sF30)
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sF30,u1_struct_0(sK0)) )
| ~ spl32_1 ),
inference(forward_subsumption_resolution,[],[f1602,f978]) ).
fof(f1607,plain,
! [X0] :
( k2_group_3(sK0,X0,sF26) = k1_funct_1(sF27,X0)
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sF26,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f1603,f980]) ).
fof(f1608,plain,
! [X0] :
( k2_group_3(sK0,X0,sK1) = k1_funct_1(sF28,X0)
| v1_xboole_0(u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f1604,f979]) ).
fof(f1610,plain,
( ! [X0] :
( v1_xboole_0(sF25)
| k1_funct_1(sF31,X0) = k2_group_3(sK0,X0,sF30)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sF30,u1_struct_0(sK0)) )
| ~ spl32_1 ),
inference(forward_demodulation,[],[f1606,f280]) ).
fof(f1611,plain,
! [X0] :
( v1_xboole_0(sF25)
| k2_group_3(sK0,X0,sF26) = k1_funct_1(sF27,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sF26,u1_struct_0(sK0)) ),
inference(forward_demodulation,[],[f1607,f280]) ).
fof(f1612,plain,
! [X0] :
( v1_xboole_0(sF25)
| k2_group_3(sK0,X0,sK1) = k1_funct_1(sF28,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_demodulation,[],[f1608,f280]) ).
fof(f1614,plain,
( ! [X0] :
( k1_funct_1(sF31,X0) = k2_group_3(sK0,X0,sF30)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sF30,u1_struct_0(sK0)) )
| ~ spl32_1 ),
inference(forward_subsumption_resolution,[],[f1610,f754]) ).
fof(f1615,plain,
! [X0] :
( k2_group_3(sK0,X0,sF26) = k1_funct_1(sF27,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sF26,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f1611,f754]) ).
fof(f1616,plain,
! [X0] :
( k2_group_3(sK0,X0,sK1) = k1_funct_1(sF28,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f1612,f754]) ).
fof(f1618,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF25)
| k1_funct_1(sF31,X0) = k2_group_3(sK0,X0,sF30)
| ~ m1_subset_1(sF30,u1_struct_0(sK0)) )
| ~ spl32_1 ),
inference(forward_demodulation,[],[f1614,f280]) ).
fof(f1619,plain,
! [X0] :
( ~ m1_subset_1(X0,sF25)
| k2_group_3(sK0,X0,sF26) = k1_funct_1(sF27,X0)
| ~ m1_subset_1(sF26,u1_struct_0(sK0)) ),
inference(forward_demodulation,[],[f1615,f280]) ).
fof(f1620,plain,
! [X0] :
( ~ m1_subset_1(X0,sF25)
| k2_group_3(sK0,X0,sK1) = k1_funct_1(sF28,X0)
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_demodulation,[],[f1616,f280]) ).
fof(f1622,plain,
( ! [X0] :
( ~ m1_subset_1(sF30,sF25)
| ~ m1_subset_1(X0,sF25)
| k1_funct_1(sF31,X0) = k2_group_3(sK0,X0,sF30) )
| ~ spl32_1 ),
inference(forward_demodulation,[],[f1618,f280]) ).
fof(f1623,plain,
! [X0] :
( ~ m1_subset_1(sF26,sF25)
| ~ m1_subset_1(X0,sF25)
| k2_group_3(sK0,X0,sF26) = k1_funct_1(sF27,X0) ),
inference(forward_demodulation,[],[f1619,f280]) ).
fof(f1624,plain,
! [X0] :
( ~ m1_subset_1(sK1,sF25)
| ~ m1_subset_1(X0,sF25)
| k2_group_3(sK0,X0,sK1) = k1_funct_1(sF28,X0) ),
inference(forward_demodulation,[],[f1620,f280]) ).
fof(f1626,plain,
( ! [X0] :
( k1_funct_1(sF31,X0) = k2_group_3(sK0,X0,sF30)
| ~ m1_subset_1(X0,sF25) )
| ~ spl32_1
| ~ spl32_2 ),
inference(forward_subsumption_resolution,[],[f1622,f394]) ).
fof(f1627,plain,
! [X0] :
( k2_group_3(sK0,X0,sF26) = k1_funct_1(sF27,X0)
| ~ m1_subset_1(X0,sF25) ),
inference(forward_subsumption_resolution,[],[f1623,f307]) ).
fof(f1628,plain,
! [X0] :
( k2_group_3(sK0,X0,sK1) = k1_funct_1(sF28,X0)
| ~ m1_subset_1(X0,sF25) ),
inference(forward_subsumption_resolution,[],[f1624,f294]) ).
fof(f1632,plain,
! [X0] :
( k2_group_3(sK0,k1_funct_1(sF27,X0),sK1) = X0
| ~ m1_subset_1(X0,sF25)
| ~ m1_subset_1(X0,sF25) ),
inference(superposition,[],[f374,f1627]) ).
fof(f1633,plain,
! [X0] :
( m1_subset_1(k1_funct_1(sF27,X0),sF25)
| ~ m1_subset_1(X0,sF25)
| ~ m1_subset_1(sF26,sF25)
| ~ m1_subset_1(X0,sF25) ),
inference(superposition,[],[f526,f1627]) ).
fof(f1639,plain,
! [X0] :
( m1_subset_1(k1_funct_1(sF27,X0),sF25)
| ~ m1_subset_1(X0,sF25)
| ~ m1_subset_1(sF26,sF25) ),
inference(duplicate_literal_removal,[],[f1633]) ).
fof(f1640,plain,
! [X0] :
( k2_group_3(sK0,k1_funct_1(sF27,X0),sK1) = X0
| ~ m1_subset_1(X0,sF25) ),
inference(duplicate_literal_removal,[],[f1632]) ).
fof(f1645,plain,
! [X0] :
( m1_subset_1(k1_funct_1(sF27,X0),sF25)
| ~ m1_subset_1(X0,sF25) ),
inference(forward_subsumption_resolution,[],[f1639,f307]) ).
fof(f1674,plain,
( ! [X0] :
( k1_funct_1(sF31,X0) = X0
| ~ m1_subset_1(X0,sF25)
| ~ m1_subset_1(X0,sF25) )
| ~ spl32_1
| ~ spl32_2 ),
inference(superposition,[],[f605,f1626]) ).
fof(f1684,plain,
( ! [X0] :
( k1_funct_1(sF31,X0) = X0
| ~ m1_subset_1(X0,sF25) )
| ~ spl32_1
| ~ spl32_2 ),
inference(duplicate_literal_removal,[],[f1674]) ).
fof(f2118,plain,
! [X0] :
( k1_funct_1(sF28,k1_funct_1(sF27,X0)) = X0
| ~ m1_subset_1(k1_funct_1(sF27,X0),sF25)
| ~ m1_subset_1(X0,sF25) ),
inference(superposition,[],[f1628,f1640]) ).
fof(f2126,plain,
! [X0] :
( k1_funct_1(sF28,k1_funct_1(sF27,X0)) = X0
| ~ m1_subset_1(X0,sF25) ),
inference(forward_subsumption_resolution,[],[f2118,f1645]) ).
fof(f2515,definition,
( spl32_30
<=> v1_funct_1(sF27) ),
introduced(definition,[new_symbols(definition,[spl32_30])],[avatar_definition]) ).
fof(f2518,plain,
( spl32_30
| ~ spl32_3
| spl32_5 ),
inference(avatar_split_clause,[],[f421,f783,f775,f2515]) ).
fof(f2614,definition,
( spl32_31
<=> v1_funct_2(sF27,sF25,sF25) ),
introduced(definition,[new_symbols(definition,[spl32_31])],[avatar_definition]) ).
fof(f2616,plain,
( v1_funct_2(sF27,sF25,sF25)
| ~ spl32_31 ),
inference(avatar_component_clause,[],[f2614]) ).
fof(f2617,plain,
( spl32_31
| ~ spl32_3
| spl32_5 ),
inference(avatar_split_clause,[],[f426,f783,f775,f2614]) ).
fof(f3198,plain,
( ! [X2,X0,X1] :
( sK24(X0,sF31,X1) != k1_funct_1(X1,sK24(X0,sF31,X1))
| ~ v1_funct_2(sF31,X0,X2)
| ~ v1_funct_1(sF31)
| ~ m2_relset_1(X1,X0,X2)
| ~ v1_funct_2(X1,X0,X2)
| ~ v1_funct_1(X1)
| ~ m2_relset_1(sF31,X0,X2)
| sF31 = X1
| ~ m1_subset_1(sK24(X0,sF31,X1),sF25) )
| ~ spl32_1
| ~ spl32_2 ),
inference(superposition,[],[f266,f1684]) ).
fof(f3206,plain,
( ! [X2,X0,X1] :
( sK24(X0,sF31,X1) != k1_funct_1(X1,sK24(X0,sF31,X1))
| ~ v1_funct_2(sF31,X0,X2)
| ~ m2_relset_1(X1,X0,X2)
| ~ v1_funct_2(X1,X0,X2)
| ~ v1_funct_1(X1)
| ~ m2_relset_1(sF31,X0,X2)
| sF31 = X1
| ~ m1_subset_1(sK24(X0,sF31,X1),sF25) )
| ~ spl32_1
| ~ spl32_2
| ~ spl32_8
| ~ spl32_11 ),
inference(forward_subsumption_resolution,[],[f3198,f1052]) ).
fof(f7075,plain,
! [X2,X3,X0,X1] :
( r2_hidden(sK24(X1,X0,X3),X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X3,X1,X2)
| ~ v1_funct_2(X3,X1,X2)
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X0,X1,X2)
| X0 = X3
| ~ v1_funct_2(X0,X1,X2)
| v1_xboole_0(X1) ),
inference(resolution,[],[f265,f270]) ).
fof(f13743,definition,
( spl32_93
<=> m1_relset_1(sF28,sF25,sF25) ),
introduced(definition,[new_symbols(definition,[spl32_93])],[avatar_definition]) ).
fof(f13745,plain,
( ~ m1_relset_1(sF28,sF25,sF25)
| spl32_93 ),
inference(avatar_component_clause,[],[f13743]) ).
fof(f13750,plain,
( $false
| spl32_93 ),
inference(forward_subsumption_resolution,[],[f13745,f979]) ).
fof(f13751,plain,
spl32_93,
inference(avatar_contradiction_clause,[],[f13750]) ).
fof(f15304,definition,
( spl32_101
<=> m1_relset_1(sF27,sF25,sF25) ),
introduced(definition,[new_symbols(definition,[spl32_101])],[avatar_definition]) ).
fof(f15306,plain,
( ~ m1_relset_1(sF27,sF25,sF25)
| spl32_101 ),
inference(avatar_component_clause,[],[f15304]) ).
fof(f15311,plain,
( $false
| spl32_101 ),
inference(forward_subsumption_resolution,[],[f15306,f980]) ).
fof(f15312,plain,
spl32_101,
inference(avatar_contradiction_clause,[],[f15311]) ).
fof(f17489,definition,
( spl32_108
<=> v1_funct_2(sF29,sF25,sF25) ),
introduced(definition,[new_symbols(definition,[spl32_108])],[avatar_definition]) ).
fof(f17491,plain,
( v1_funct_2(sF29,sF25,sF25)
| ~ spl32_108 ),
inference(avatar_component_clause,[],[f17489]) ).
fof(f17493,definition,
( spl32_109
<=> v1_funct_1(sF29) ),
introduced(definition,[new_symbols(definition,[spl32_109])],[avatar_definition]) ).
fof(f17494,plain,
( v1_funct_1(sF29)
| ~ spl32_109 ),
inference(avatar_component_clause,[],[f17493]) ).
fof(f29434,plain,
( ~ spl32_93
| ~ spl32_30
| ~ spl32_31
| ~ spl32_101
| ~ spl32_16
| spl32_109
| ~ spl32_4 ),
inference(avatar_split_clause,[],[f967,f779,f17493,f1137,f15304,f2614,f2515,f13743]) ).
fof(f30506,plain,
( ~ spl32_93
| ~ spl32_30
| ~ spl32_31
| ~ spl32_101
| ~ spl32_16
| spl32_108
| ~ spl32_4 ),
inference(avatar_split_clause,[],[f972,f779,f17489,f1137,f15304,f2614,f2515,f13743]) ).
fof(f36653,definition,
( spl32_190
<=> sF29 = k5_relat_1(sF27,sF28) ),
introduced(definition,[new_symbols(definition,[spl32_190])],[avatar_definition]) ).
fof(f36655,plain,
( sF29 = k5_relat_1(sF27,sF28)
| ~ spl32_190 ),
inference(avatar_component_clause,[],[f36653]) ).
fof(f36656,plain,
( ~ spl32_93
| spl32_5
| ~ spl32_30
| ~ spl32_31
| ~ spl32_101
| ~ spl32_16
| ~ spl32_17
| spl32_190 ),
inference(avatar_split_clause,[],[f675,f36653,f1160,f1137,f15304,f2614,f2515,f783,f13743]) ).
fof(f36661,plain,
( ! [X2,X0,X1] :
( k1_funct_1(sF28,k1_funct_1(sF27,X0)) = k1_funct_1(sF29,X0)
| ~ v1_funct_2(sF27,X1,X2)
| ~ v1_funct_1(sF27)
| ~ v1_funct_1(sF28)
| ~ v1_relat_1(sF28)
| ~ r2_hidden(X0,X1)
| ~ m2_relset_1(sF27,X1,X2)
| k1_xboole_0 = X2 )
| ~ spl32_190 ),
inference(superposition,[],[f268,f36655]) ).
fof(f36675,plain,
( ! [X2,X0,X1] :
( k1_funct_1(sF28,k1_funct_1(sF27,X0)) = k1_funct_1(sF29,X0)
| ~ v1_funct_2(sF27,X1,X2)
| ~ v1_funct_1(sF28)
| ~ v1_relat_1(sF28)
| ~ r2_hidden(X0,X1)
| ~ m2_relset_1(sF27,X1,X2)
| k1_xboole_0 = X2 )
| ~ spl32_8
| ~ spl32_10
| ~ spl32_190 ),
inference(forward_subsumption_resolution,[],[f36661,f1021]) ).
fof(f36681,plain,
( ! [X2,X0,X1] :
( k1_funct_1(sF28,k1_funct_1(sF27,X0)) = k1_funct_1(sF29,X0)
| ~ v1_funct_2(sF27,X1,X2)
| ~ v1_relat_1(sF28)
| ~ r2_hidden(X0,X1)
| ~ m2_relset_1(sF27,X1,X2)
| k1_xboole_0 = X2 )
| ~ spl32_8
| ~ spl32_10
| ~ spl32_16
| ~ spl32_190 ),
inference(forward_subsumption_resolution,[],[f36675,f1139]) ).
fof(f36682,plain,
( ! [X2,X0,X1] :
( k1_funct_1(sF28,k1_funct_1(sF27,X0)) = k1_funct_1(sF29,X0)
| ~ v1_funct_2(sF27,X1,X2)
| ~ r2_hidden(X0,X1)
| ~ m2_relset_1(sF27,X1,X2)
| k1_xboole_0 = X2 )
| ~ spl32_8
| ~ spl32_10
| ~ spl32_16
| ~ spl32_190 ),
inference(forward_subsumption_resolution,[],[f36681,f1134]) ).
fof(f36694,plain,
( ! [X2,X0,X1] :
( k1_funct_1(sF29,X0) = X0
| ~ m1_subset_1(X0,sF25)
| ~ v1_funct_2(sF27,X1,X2)
| ~ r2_hidden(X0,X1)
| ~ m2_relset_1(sF27,X1,X2)
| k1_xboole_0 = X2 )
| ~ spl32_8
| ~ spl32_10
| ~ spl32_16
| ~ spl32_190 ),
inference(superposition,[],[f2126,f36682]) ).
fof(f36721,plain,
( ! [X2,X3,X0,X1] :
( sK24(X0,sF31,sF29) != sK24(X0,sF31,sF29)
| ~ v1_funct_2(sF31,X0,X1)
| ~ m2_relset_1(sF29,X0,X1)
| ~ v1_funct_2(sF29,X0,X1)
| ~ v1_funct_1(sF29)
| ~ m2_relset_1(sF31,X0,X1)
| sF29 = sF31
| ~ m1_subset_1(sK24(X0,sF31,sF29),sF25)
| ~ m1_subset_1(sK24(X0,sF31,sF29),sF25)
| ~ v1_funct_2(sF27,X2,X3)
| ~ r2_hidden(sK24(X0,sF31,sF29),X2)
| ~ m2_relset_1(sF27,X2,X3)
| k1_xboole_0 = X3 )
| ~ spl32_1
| ~ spl32_2
| ~ spl32_8
| ~ spl32_10
| ~ spl32_11
| ~ spl32_16
| ~ spl32_190 ),
inference(superposition,[],[f3206,f36694]) ).
fof(f36730,plain,
( ! [X2,X3,X0,X1] :
( sK24(X0,sF31,sF29) != sK24(X0,sF31,sF29)
| ~ v1_funct_2(sF31,X0,X1)
| ~ m2_relset_1(sF29,X0,X1)
| ~ v1_funct_2(sF29,X0,X1)
| ~ v1_funct_1(sF29)
| ~ m2_relset_1(sF31,X0,X1)
| sF29 = sF31
| ~ m1_subset_1(sK24(X0,sF31,sF29),sF25)
| ~ v1_funct_2(sF27,X2,X3)
| ~ r2_hidden(sK24(X0,sF31,sF29),X2)
| ~ m2_relset_1(sF27,X2,X3)
| k1_xboole_0 = X3 )
| ~ spl32_1
| ~ spl32_2
| ~ spl32_8
| ~ spl32_10
| ~ spl32_11
| ~ spl32_16
| ~ spl32_190 ),
inference(duplicate_literal_removal,[],[f36721]) ).
fof(f36731,plain,
( ! [X2,X3,X0,X1] :
( ~ v1_funct_2(sF31,X0,X1)
| ~ m2_relset_1(sF29,X0,X1)
| ~ v1_funct_2(sF29,X0,X1)
| ~ v1_funct_1(sF29)
| ~ m2_relset_1(sF31,X0,X1)
| sF29 = sF31
| ~ m1_subset_1(sK24(X0,sF31,sF29),sF25)
| ~ v1_funct_2(sF27,X2,X3)
| ~ r2_hidden(sK24(X0,sF31,sF29),X2)
| ~ m2_relset_1(sF27,X2,X3)
| k1_xboole_0 = X3 )
| ~ spl32_1
| ~ spl32_2
| ~ spl32_8
| ~ spl32_10
| ~ spl32_11
| ~ spl32_16
| ~ spl32_190 ),
inference(trivial_inequality_removal,[],[f36730]) ).
fof(f36743,plain,
( ! [X2,X3,X0,X1] :
( ~ v1_funct_2(sF31,X0,X1)
| ~ m2_relset_1(sF29,X0,X1)
| ~ v1_funct_2(sF29,X0,X1)
| ~ m2_relset_1(sF31,X0,X1)
| sF29 = sF31
| ~ m1_subset_1(sK24(X0,sF31,sF29),sF25)
| ~ v1_funct_2(sF27,X2,X3)
| ~ r2_hidden(sK24(X0,sF31,sF29),X2)
| ~ m2_relset_1(sF27,X2,X3)
| k1_xboole_0 = X3 )
| ~ spl32_1
| ~ spl32_2
| ~ spl32_8
| ~ spl32_10
| ~ spl32_11
| ~ spl32_16
| ~ spl32_109
| ~ spl32_190 ),
inference(forward_subsumption_resolution,[],[f36731,f17494]) ).
fof(f36758,plain,
( ! [X2,X3,X0,X1] :
( ~ r2_hidden(sK24(X0,sF31,sF29),X2)
| ~ m2_relset_1(sF29,X0,X1)
| ~ v1_funct_2(sF29,X0,X1)
| ~ m2_relset_1(sF31,X0,X1)
| ~ m1_subset_1(sK24(X0,sF31,sF29),sF25)
| ~ v1_funct_2(sF27,X2,X3)
| ~ v1_funct_2(sF31,X0,X1)
| ~ m2_relset_1(sF27,X2,X3)
| k1_xboole_0 = X3 )
| ~ spl32_1
| ~ spl32_2
| ~ spl32_8
| ~ spl32_10
| ~ spl32_11
| ~ spl32_16
| ~ spl32_109
| ~ spl32_190 ),
inference(forward_subsumption_resolution,[],[f36743,f293]) ).
fof(f36767,plain,
( ! [X2,X3,X0,X1] :
( ~ m2_relset_1(sF29,X0,X1)
| ~ v1_funct_2(sF29,X0,X1)
| ~ m2_relset_1(sF31,X0,X1)
| ~ m1_subset_1(sK24(X0,sF31,sF29),sF25)
| ~ v1_funct_2(sF27,X0,X2)
| ~ v1_funct_2(sF31,X0,X1)
| ~ m2_relset_1(sF27,X0,X2)
| k1_xboole_0 = X2
| ~ v1_funct_1(sF31)
| ~ m2_relset_1(sF29,X0,X3)
| ~ v1_funct_2(sF29,X0,X3)
| ~ v1_funct_1(sF29)
| ~ m2_relset_1(sF31,X0,X3)
| sF29 = sF31
| ~ v1_funct_2(sF31,X0,X3)
| v1_xboole_0(X0) )
| ~ spl32_1
| ~ spl32_2
| ~ spl32_8
| ~ spl32_10
| ~ spl32_11
| ~ spl32_16
| ~ spl32_109
| ~ spl32_190 ),
inference(resolution,[],[f36758,f7075]) ).
fof(f36768,plain,
( ! [X2,X3,X0,X1] :
( ~ m2_relset_1(sF29,X0,X1)
| ~ v1_funct_2(sF29,X0,X1)
| ~ m2_relset_1(sF31,X0,X1)
| ~ m1_subset_1(sK24(X0,sF31,sF29),sF25)
| ~ v1_funct_2(sF27,X0,X2)
| ~ v1_funct_2(sF31,X0,X1)
| ~ m2_relset_1(sF27,X0,X2)
| k1_xboole_0 = X2
| ~ m2_relset_1(sF29,X0,X3)
| ~ v1_funct_2(sF29,X0,X3)
| ~ v1_funct_1(sF29)
| ~ m2_relset_1(sF31,X0,X3)
| sF29 = sF31
| ~ v1_funct_2(sF31,X0,X3)
| v1_xboole_0(X0) )
| ~ spl32_1
| ~ spl32_2
| ~ spl32_8
| ~ spl32_10
| ~ spl32_11
| ~ spl32_16
| ~ spl32_109
| ~ spl32_190 ),
inference(forward_subsumption_resolution,[],[f36767,f1052]) ).
fof(f36769,plain,
( ! [X2,X3,X0,X1] :
( ~ m2_relset_1(sF29,X0,X1)
| ~ v1_funct_2(sF29,X0,X1)
| ~ m2_relset_1(sF31,X0,X1)
| ~ m1_subset_1(sK24(X0,sF31,sF29),sF25)
| ~ v1_funct_2(sF27,X0,X2)
| ~ v1_funct_2(sF31,X0,X1)
| ~ m2_relset_1(sF27,X0,X2)
| k1_xboole_0 = X2
| ~ m2_relset_1(sF29,X0,X3)
| ~ v1_funct_2(sF29,X0,X3)
| ~ m2_relset_1(sF31,X0,X3)
| sF29 = sF31
| ~ v1_funct_2(sF31,X0,X3)
| v1_xboole_0(X0) )
| ~ spl32_1
| ~ spl32_2
| ~ spl32_8
| ~ spl32_10
| ~ spl32_11
| ~ spl32_16
| ~ spl32_109
| ~ spl32_190 ),
inference(forward_subsumption_resolution,[],[f36768,f17494]) ).
fof(f36770,plain,
( ! [X2,X3,X0,X1] :
( ~ m1_subset_1(sK24(X0,sF31,sF29),sF25)
| ~ v1_funct_2(sF29,X0,X1)
| ~ m2_relset_1(sF31,X0,X1)
| ~ m2_relset_1(sF29,X0,X1)
| ~ v1_funct_2(sF27,X0,X2)
| ~ v1_funct_2(sF31,X0,X1)
| ~ m2_relset_1(sF27,X0,X2)
| k1_xboole_0 = X2
| ~ m2_relset_1(sF29,X0,X3)
| ~ v1_funct_2(sF29,X0,X3)
| ~ m2_relset_1(sF31,X0,X3)
| ~ v1_funct_2(sF31,X0,X3)
| v1_xboole_0(X0) )
| ~ spl32_1
| ~ spl32_2
| ~ spl32_8
| ~ spl32_10
| ~ spl32_11
| ~ spl32_16
| ~ spl32_109
| ~ spl32_190 ),
inference(forward_subsumption_resolution,[],[f36769,f293]) ).
fof(f36775,plain,
( ! [X2,X3,X0,X1] :
( ~ v1_funct_2(sF29,sF25,X0)
| ~ m2_relset_1(sF31,sF25,X0)
| ~ m2_relset_1(sF29,sF25,X0)
| ~ v1_funct_2(sF27,sF25,X1)
| ~ v1_funct_2(sF31,sF25,X0)
| ~ m2_relset_1(sF27,sF25,X1)
| k1_xboole_0 = X1
| ~ m2_relset_1(sF29,sF25,X2)
| ~ v1_funct_2(sF29,sF25,X2)
| ~ m2_relset_1(sF31,sF25,X2)
| ~ v1_funct_2(sF31,sF25,X2)
| v1_xboole_0(sF25)
| ~ v1_funct_2(sF31,sF25,X3)
| ~ v1_funct_1(sF31)
| ~ m2_relset_1(sF29,sF25,X3)
| ~ v1_funct_2(sF29,sF25,X3)
| ~ v1_funct_1(sF29)
| ~ m2_relset_1(sF31,sF25,X3)
| sF29 = sF31 )
| ~ spl32_1
| ~ spl32_2
| ~ spl32_8
| ~ spl32_10
| ~ spl32_11
| ~ spl32_16
| ~ spl32_109
| ~ spl32_190 ),
inference(resolution,[],[f36770,f265]) ).
fof(f36776,plain,
( ! [X2,X3,X0,X1] :
( ~ v1_funct_2(sF29,sF25,X0)
| ~ m2_relset_1(sF31,sF25,X0)
| ~ m2_relset_1(sF29,sF25,X0)
| ~ v1_funct_2(sF27,sF25,X1)
| ~ v1_funct_2(sF31,sF25,X0)
| ~ m2_relset_1(sF27,sF25,X1)
| k1_xboole_0 = X1
| ~ m2_relset_1(sF29,sF25,X2)
| ~ v1_funct_2(sF29,sF25,X2)
| ~ m2_relset_1(sF31,sF25,X2)
| ~ v1_funct_2(sF31,sF25,X2)
| ~ v1_funct_2(sF31,sF25,X3)
| ~ v1_funct_1(sF31)
| ~ m2_relset_1(sF29,sF25,X3)
| ~ v1_funct_2(sF29,sF25,X3)
| ~ v1_funct_1(sF29)
| ~ m2_relset_1(sF31,sF25,X3)
| sF29 = sF31 )
| ~ spl32_1
| ~ spl32_2
| ~ spl32_8
| ~ spl32_10
| ~ spl32_11
| ~ spl32_16
| ~ spl32_109
| ~ spl32_190 ),
inference(forward_subsumption_resolution,[],[f36775,f754]) ).
fof(f36777,plain,
( ! [X2,X3,X0,X1] :
( ~ v1_funct_2(sF29,sF25,X0)
| ~ m2_relset_1(sF31,sF25,X0)
| ~ m2_relset_1(sF29,sF25,X0)
| ~ v1_funct_2(sF27,sF25,X1)
| ~ v1_funct_2(sF31,sF25,X0)
| ~ m2_relset_1(sF27,sF25,X1)
| k1_xboole_0 = X1
| ~ m2_relset_1(sF29,sF25,X2)
| ~ v1_funct_2(sF29,sF25,X2)
| ~ m2_relset_1(sF31,sF25,X2)
| ~ v1_funct_2(sF31,sF25,X2)
| ~ v1_funct_2(sF31,sF25,X3)
| ~ m2_relset_1(sF29,sF25,X3)
| ~ v1_funct_2(sF29,sF25,X3)
| ~ v1_funct_1(sF29)
| ~ m2_relset_1(sF31,sF25,X3)
| sF29 = sF31 )
| ~ spl32_1
| ~ spl32_2
| ~ spl32_8
| ~ spl32_10
| ~ spl32_11
| ~ spl32_16
| ~ spl32_109
| ~ spl32_190 ),
inference(forward_subsumption_resolution,[],[f36776,f1052]) ).
fof(f36778,plain,
( ! [X2,X3,X0,X1] :
( ~ v1_funct_2(sF29,sF25,X0)
| ~ m2_relset_1(sF31,sF25,X0)
| ~ m2_relset_1(sF29,sF25,X0)
| ~ v1_funct_2(sF27,sF25,X1)
| ~ v1_funct_2(sF31,sF25,X0)
| ~ m2_relset_1(sF27,sF25,X1)
| k1_xboole_0 = X1
| ~ m2_relset_1(sF29,sF25,X2)
| ~ v1_funct_2(sF29,sF25,X2)
| ~ m2_relset_1(sF31,sF25,X2)
| ~ v1_funct_2(sF31,sF25,X2)
| ~ v1_funct_2(sF31,sF25,X3)
| ~ m2_relset_1(sF29,sF25,X3)
| ~ v1_funct_2(sF29,sF25,X3)
| ~ m2_relset_1(sF31,sF25,X3)
| sF29 = sF31 )
| ~ spl32_1
| ~ spl32_2
| ~ spl32_8
| ~ spl32_10
| ~ spl32_11
| ~ spl32_16
| ~ spl32_109
| ~ spl32_190 ),
inference(forward_subsumption_resolution,[],[f36777,f17494]) ).
fof(f36779,plain,
( ! [X2,X3,X0,X1] :
( ~ v1_funct_2(sF29,sF25,X0)
| ~ m2_relset_1(sF31,sF25,X0)
| ~ m2_relset_1(sF29,sF25,X0)
| ~ v1_funct_2(sF27,sF25,X1)
| ~ v1_funct_2(sF31,sF25,X0)
| ~ m2_relset_1(sF27,sF25,X1)
| k1_xboole_0 = X1
| ~ m2_relset_1(sF29,sF25,X2)
| ~ v1_funct_2(sF29,sF25,X2)
| ~ m2_relset_1(sF31,sF25,X2)
| ~ v1_funct_2(sF31,sF25,X2)
| ~ v1_funct_2(sF31,sF25,X3)
| ~ m2_relset_1(sF29,sF25,X3)
| ~ v1_funct_2(sF29,sF25,X3)
| ~ m2_relset_1(sF31,sF25,X3) )
| ~ spl32_1
| ~ spl32_2
| ~ spl32_8
| ~ spl32_10
| ~ spl32_11
| ~ spl32_16
| ~ spl32_109
| ~ spl32_190 ),
inference(forward_subsumption_resolution,[],[f36778,f293]) ).
fof(f37367,definition,
( spl32_196
<=> ! [X3] :
( ~ v1_funct_2(sF31,sF25,X3)
| ~ m2_relset_1(sF31,sF25,X3)
| ~ v1_funct_2(sF29,sF25,X3)
| ~ m2_relset_1(sF29,sF25,X3) ) ),
introduced(definition,[new_symbols(definition,[spl32_196])],[avatar_definition]) ).
fof(f37368,plain,
( ! [X3] :
( ~ m2_relset_1(sF31,sF25,X3)
| ~ v1_funct_2(sF31,sF25,X3)
| ~ v1_funct_2(sF29,sF25,X3)
| ~ m2_relset_1(sF29,sF25,X3) )
| ~ spl32_196 ),
inference(avatar_component_clause,[],[f37367]) ).
fof(f37370,definition,
( spl32_197
<=> ! [X1] :
( ~ v1_funct_2(sF27,sF25,X1)
| k1_xboole_0 = X1
| ~ m2_relset_1(sF27,sF25,X1) ) ),
introduced(definition,[new_symbols(definition,[spl32_197])],[avatar_definition]) ).
fof(f37371,plain,
( ! [X1] :
( ~ m2_relset_1(sF27,sF25,X1)
| k1_xboole_0 = X1
| ~ v1_funct_2(sF27,sF25,X1) )
| ~ spl32_197 ),
inference(avatar_component_clause,[],[f37370]) ).
fof(f37372,plain,
( spl32_196
| spl32_196
| spl32_197
| spl32_196
| ~ spl32_1
| ~ spl32_2
| ~ spl32_8
| ~ spl32_10
| ~ spl32_11
| ~ spl32_16
| ~ spl32_109
| ~ spl32_190 ),
inference(avatar_split_clause,[],[f36779,f36653,f17493,f1137,f1048,f1017,f974,f393,f389,f37367,f37370,f37367,f37367]) ).
fof(f37373,plain,
( ~ v1_funct_2(sF31,sF25,sF25)
| ~ v1_funct_2(sF29,sF25,sF25)
| ~ m2_relset_1(sF29,sF25,sF25)
| ~ spl32_1
| ~ spl32_196 ),
inference(resolution,[],[f37368,f767]) ).
fof(f37374,plain,
( ~ v1_funct_2(sF29,sF25,sF25)
| ~ m2_relset_1(sF29,sF25,sF25)
| ~ spl32_1
| ~ spl32_11
| ~ spl32_196 ),
inference(forward_subsumption_resolution,[],[f37373,f1053]) ).
fof(f37375,plain,
( ~ m2_relset_1(sF29,sF25,sF25)
| ~ spl32_1
| ~ spl32_11
| ~ spl32_108
| ~ spl32_196 ),
inference(forward_subsumption_resolution,[],[f37374,f17491]) ).
fof(f37376,plain,
( $false
| ~ spl32_1
| ~ spl32_4
| ~ spl32_8
| ~ spl32_10
| ~ spl32_11
| ~ spl32_17
| ~ spl32_108
| ~ spl32_196 ),
inference(forward_subsumption_resolution,[],[f37375,f1574]) ).
fof(f37377,plain,
( ~ spl32_1
| ~ spl32_4
| ~ spl32_8
| ~ spl32_10
| ~ spl32_11
| ~ spl32_17
| ~ spl32_108
| ~ spl32_196 ),
inference(avatar_contradiction_clause,[],[f37376]) ).
fof(f37378,plain,
( k1_xboole_0 = sF25
| ~ v1_funct_2(sF27,sF25,sF25)
| ~ spl32_197 ),
inference(resolution,[],[f37371,f769]) ).
fof(f37379,plain,
( k1_xboole_0 = sF25
| ~ spl32_31
| ~ spl32_197 ),
inference(forward_subsumption_resolution,[],[f37378,f2616]) ).
fof(f37396,plain,
( ~ v1_xboole_0(k1_xboole_0)
| ~ spl32_31
| ~ spl32_197 ),
inference(superposition,[],[f754,f37379]) ).
fof(f37675,plain,
( $false
| ~ spl32_31
| ~ spl32_197 ),
inference(forward_subsumption_resolution,[],[f37396,f220]) ).
fof(f37676,plain,
( ~ spl32_31
| ~ spl32_197 ),
inference(avatar_contradiction_clause,[],[f37675]) ).
cnf(s1,plain,
( spl32_1
| ~ spl32_2 ),
inference(sat_conversion,[],[f396]) ).
cnf(s3,plain,
spl32_2,
inference(sat_conversion,[],[f483]) ).
cnf(s4,plain,
( ~ spl32_3
| spl32_4
| spl32_5 ),
inference(sat_conversion,[],[f786]) ).
cnf(s5,plain,
spl32_3,
inference(sat_conversion,[],[f788]) ).
cnf(s6,plain,
~ spl32_5,
inference(sat_conversion,[],[f790]) ).
cnf(s8,plain,
( spl32_5
| spl32_8 ),
inference(sat_conversion,[],[f976]) ).
cnf(s11,plain,
( ~ spl32_3
| spl32_5
| spl32_10 ),
inference(sat_conversion,[],[f1020]) ).
cnf(s12,plain,
( ~ spl32_1
| ~ spl32_3
| spl32_5
| spl32_11 ),
inference(sat_conversion,[],[f1051]) ).
cnf(s16,plain,
( ~ spl32_3
| spl32_5
| spl32_16 ),
inference(sat_conversion,[],[f1140]) ).
cnf(s17,plain,
( ~ spl32_3
| spl32_5
| spl32_17 ),
inference(sat_conversion,[],[f1163]) ).
cnf(s29,plain,
( ~ spl32_3
| spl32_5
| spl32_30 ),
inference(sat_conversion,[],[f2518]) ).
cnf(s31,plain,
( ~ spl32_3
| spl32_5
| spl32_31 ),
inference(sat_conversion,[],[f2617]) ).
cnf(s126,plain,
spl32_93,
inference(sat_conversion,[],[f13751]) ).
cnf(s134,plain,
spl32_101,
inference(sat_conversion,[],[f15312]) ).
cnf(s206,plain,
( ~ spl32_4
| ~ spl32_16
| ~ spl32_30
| ~ spl32_31
| ~ spl32_93
| ~ spl32_101
| spl32_109 ),
inference(sat_conversion,[],[f29434]) ).
cnf(s208,plain,
( ~ spl32_4
| ~ spl32_16
| ~ spl32_30
| ~ spl32_31
| ~ spl32_93
| ~ spl32_101
| spl32_108 ),
inference(sat_conversion,[],[f30506]) ).
cnf(s221,plain,
( spl32_5
| ~ spl32_16
| ~ spl32_17
| ~ spl32_30
| ~ spl32_31
| ~ spl32_93
| ~ spl32_101
| spl32_190 ),
inference(sat_conversion,[],[f36656]) ).
cnf(s225,plain,
( spl32_196
| spl32_196
| ~ spl32_8
| ~ spl32_10
| ~ spl32_11
| ~ spl32_16
| ~ spl32_109
| ~ spl32_190
| ~ spl32_1
| ~ spl32_2
| spl32_196
| spl32_197 ),
inference(sat_conversion,[],[f37372]) ).
cnf(s226,plain,
( ~ spl32_1
| ~ spl32_2
| ~ spl32_8
| ~ spl32_10
| ~ spl32_11
| ~ spl32_16
| ~ spl32_109
| ~ spl32_190
| spl32_196
| spl32_197 ),
inference(rat,[],[s225]) ).
cnf(s227,plain,
( ~ spl32_1
| ~ spl32_4
| ~ spl32_8
| ~ spl32_10
| ~ spl32_11
| ~ spl32_17
| ~ spl32_108
| ~ spl32_196 ),
inference(sat_conversion,[],[f37377]) ).
cnf(s228,plain,
( ~ spl32_31
| ~ spl32_197 ),
inference(sat_conversion,[],[f37676]) ).
cnf(s253,plain,
spl32_8,
inference(rat,[],[s8,s6]) ).
cnf(s257,plain,
spl32_31,
inference(rat,[],[s31,s6,s5]) ).
cnf(s258,plain,
spl32_30,
inference(rat,[],[s29,s6,s5]) ).
cnf(s259,plain,
spl32_17,
inference(rat,[],[s17,s6,s5]) ).
cnf(s260,plain,
spl32_16,
inference(rat,[],[s16,s6,s5]) ).
cnf(s261,plain,
spl32_10,
inference(rat,[],[s11,s6,s5]) ).
cnf(s262,plain,
~ spl32_197,
inference(rat,[],[s228,s257]) ).
cnf(s264,plain,
spl32_190,
inference(rat,[],[s221,s259,s134,s126,s257,s258,s6,s260]) ).
cnf(s269,plain,
spl32_4,
inference(rat,[],[s4,s6,s5]) ).
cnf(s270,plain,
spl32_108,
inference(rat,[],[s208,s260,s134,s126,s257,s258,s269]) ).
cnf(s271,plain,
spl32_109,
inference(rat,[],[s206,s260,s134,s126,s257,s258,s269]) ).
cnf(s278,plain,
spl32_1,
inference(rat,[],[s1,s3]) ).
cnf(s289,plain,
spl32_11,
inference(rat,[],[s12,s5,s6,s278]) ).
cnf(s298,plain,
~ spl32_196,
inference(rat,[],[s227,s278,s270,s259,s269,s261,s253,s289]) ).
cnf(s299,plain,
$false,
inference(rat,[],[s226,s262,s278,s264,s271,s260,s3,s261,s253,s298,s289]) ).
fof(f37677,plain,
$false,
inference(avatar_sat_refutation,[],[s299]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP629+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n018.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 10:17:24 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.70/2.14 % (2110804)Detected formulas, will run a generic FOF schedule.
% 10.70/2.14 % (2110812)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1134886033:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.70/2.14 % (2110809)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1248448588:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.70/2.14 % (2110813)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3001036683:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.70/2.14 % (2110811)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1447426216:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.70/2.14 % (2110810)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3213834269:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.70/2.14 % (2110812)Refutation not found, incomplete strategy
% 10.70/2.14 % (2110812)------------------------------
% 10.70/2.14 % (2110812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.14 % (2110812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.14 % (2110812)CaDiCaL version: 2.1.3
% 10.70/2.14 % (2110812)Termination reason: Refutation not found, incomplete strategy
% 10.70/2.14 % (2110812)Time elapsed: 0.002 s
% 10.70/2.14 % (2110812)Peak memory usage: 88 MB
% 10.70/2.14 % (2110812)Instructions burned: 1 (million)
% 10.70/2.14 % (2110814)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=766579930:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.70/2.14 % (2110815)dis-21_1_sil=8000:lcm=predicate:random_seed=1292093227:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 10.70/2.14 % (2110813)Instruction limit reached!
% 10.70/2.14 % (2110813)------------------------------
% 10.70/2.14 % (2110813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.14 % (2110813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.14 % (2110813)CaDiCaL version: 2.1.3
% 10.70/2.14 % (2110813)Termination reason: Instruction limit
% 10.70/2.14 % (2110813)Termination phase: Saturation
% 10.70/2.14 % (2110813)Time elapsed: 0.063 s
% 10.70/2.14 % (2110813)Peak memory usage: 88 MB
% 10.70/2.14 % (2110813)Instructions burned: 121 (million)
% 10.70/2.14 % (2110815)Instruction limit reached!
% 10.70/2.14 % (2110815)------------------------------
% 10.70/2.14 % (2110815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.14 % (2110815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.14 % (2110815)CaDiCaL version: 2.1.3
% 10.70/2.14 % (2110815)Termination reason: Instruction limit
% 10.70/2.14 % (2110815)Termination phase: Saturation
% 10.70/2.14 % (2110815)Time elapsed: 0.071 s
% 10.70/2.14 % (2110815)Peak memory usage: 90 MB
% 10.70/2.14 % (2110815)Instructions burned: 129 (million)
% 10.70/2.14 % (2110814)Instruction limit reached!
% 10.70/2.14 % (2110814)------------------------------
% 10.70/2.14 % (2110814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.14 % (2110814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.14 % (2110814)CaDiCaL version: 2.1.3
% 10.70/2.14 % (2110814)Termination reason: Instruction limit
% 10.70/2.14 % (2110814)Termination phase: Saturation
% 10.70/2.14 % (2110814)Time elapsed: 0.099 s
% 10.70/2.14 % (2110814)Peak memory usage: 90 MB
% 10.70/2.14 % (2110814)Instructions burned: 140 (million)
% 10.70/2.14 % (2110823)lrs+10_1_sil=8000:sp=occurrence:random_seed=2889910957:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 10.70/2.14 % (2110824)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3493109628:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 10.70/2.14 % (2110825)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3014531881:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 10.70/2.14 % (2110812)------------------------------
% 10.70/2.14 % (2110812)------------------------------
% 10.70/2.14 % (2110824)Instruction limit reached!
% 10.70/2.14 % (2110824)------------------------------
% 10.70/2.14 % (2110824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.00/2.99 % (2110824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.00/2.99 % (2110824)CaDiCaL version: 2.1.3
% 15.00/2.99 % (2110824)Termination reason: Instruction limit
% 15.00/2.99 % (2110824)Termination phase: Saturation
% 15.00/2.99 % (2110824)Time elapsed: 0.075 s
% 15.00/2.99 % (2110824)Peak memory usage: 90 MB
% 15.00/2.99 % (2110824)Instructions burned: 159 (million)
% 15.00/2.99 % (2110825)Instruction limit reached!
% 15.00/2.99 % (2110825)------------------------------
% 15.00/2.99 % (2110825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.00/2.99 % (2110825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.00/2.99 % (2110825)CaDiCaL version: 2.1.3
% 15.00/2.99 % (2110825)Termination reason: Instruction limit
% 15.00/2.99 % (2110825)Termination phase: Saturation
% 15.00/2.99 % (2110825)Time elapsed: 0.125 s
% 15.00/2.99 % (2110825)Peak memory usage: 92 MB
% 15.00/2.99 % (2110825)Instructions burned: 328 (million)
% 15.00/2.99 % (2110829)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=39475485:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 15.00/2.99 % (2110823)Instruction limit reached!
% 15.00/2.99 % (2110823)------------------------------
% 15.00/2.99 % (2110823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.00/2.99 % (2110823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.00/2.99 % (2110823)CaDiCaL version: 2.1.3
% 15.00/2.99 % (2110823)Termination reason: Instruction limit
% 15.00/2.99 % (2110823)Termination phase: Saturation
% 15.00/2.99 % (2110823)Time elapsed: 0.173 s
% 15.00/2.99 % (2110823)Peak memory usage: 91 MB
% 15.00/2.99 % (2110823)Instructions burned: 285 (million)
% 15.00/2.99 % (2110830)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=310970498:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 15.00/2.99 % (2110830)Refutation not found, incomplete strategy
% 15.00/2.99 % (2110830)------------------------------
% 15.00/2.99 % (2110830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.00/2.99 % (2110830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.00/2.99 % (2110830)CaDiCaL version: 2.1.3
% 15.00/2.99 % (2110830)Termination reason: Refutation not found, incomplete strategy
% 15.00/2.99 % (2110830)Time elapsed: 0.004 s
% 15.00/2.99 % (2110830)Peak memory usage: 88 MB
% 15.00/2.99 % (2110830)Instructions burned: 5 (million)
% 15.00/2.99 % (2110831)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2361173301:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 15.00/2.99 % (2110829)Instruction limit reached!
% 15.00/2.99 % (2110829)------------------------------
% 15.00/2.99 % (2110829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.00/2.99 % (2110829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.00/2.99 % (2110829)CaDiCaL version: 2.1.3
% 15.00/2.99 % (2110829)Termination reason: Instruction limit
% 15.00/2.99 % (2110829)Termination phase: Saturation
% 15.00/2.99 % (2110829)Time elapsed: 0.124 s
% 15.00/2.99 % (2110829)Peak memory usage: 91 MB
% 15.00/2.99 % (2110829)Instructions burned: 249 (million)
% 15.00/2.99 % (2110833)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2552812434:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 15.00/2.99 % (2110833)Instruction limit reached!
% 15.00/2.99 % (2110833)------------------------------
% 15.00/2.99 % (2110833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.00/2.99 % (2110833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.00/2.99 % (2110833)CaDiCaL version: 2.1.3
% 15.00/2.99 % (2110833)Termination reason: Instruction limit
% 15.00/2.99 % (2110833)Termination phase: Saturation
% 15.00/2.99 % (2110833)Time elapsed: 0.078 s
% 15.00/2.99 % (2110833)Peak memory usage: 91 MB
% 15.00/2.99 % (2110833)Instructions burned: 114 (million)
% 15.00/2.99 % (2110836)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3755955051:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 15.00/2.99 % (2110830)------------------------------
% 15.00/2.99 % (2110830)------------------------------
% 15.00/2.99 % (2110836)Instruction limit reached!
% 15.00/2.99 % (2110836)------------------------------
% 15.00/2.99 % (2110836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.00/2.99 % (2110836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.21/5.20 % (2110836)CaDiCaL version: 2.1.3
% 32.21/5.20 % (2110836)Termination reason: Instruction limit
% 32.21/5.20 % (2110836)Termination phase: Saturation
% 32.21/5.20 % (2110836)Time elapsed: 0.066 s
% 32.21/5.20 % (2110836)Peak memory usage: 89 MB
% 32.21/5.20 % (2110836)Instructions burned: 127 (million)
% 32.21/5.20 % (2110838)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=352026728:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 32.21/5.20 % (2110840)lrs+10_1_sil=8000:sp=occurrence:random_seed=913559302:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 32.21/5.20 % (2110838)Instruction limit reached!
% 32.21/5.20 % (2110838)------------------------------
% 32.21/5.20 % (2110838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.21/5.20 % (2110838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.21/5.20 % (2110838)CaDiCaL version: 2.1.3
% 32.21/5.20 % (2110838)Termination reason: Instruction limit
% 32.21/5.20 % (2110838)Termination phase: Saturation
% 32.21/5.20 % (2110838)Time elapsed: 0.062 s
% 32.21/5.20 % (2110838)Peak memory usage: 89 MB
% 32.21/5.20 % (2110838)Instructions burned: 114 (million)
% 32.21/5.20 % (2110841)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2471722243:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 32.21/5.20 % (2110841)Refutation not found, incomplete strategy
% 32.21/5.20 % (2110841)------------------------------
% 32.21/5.20 % (2110841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.21/5.20 % (2110841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.21/5.20 % (2110841)CaDiCaL version: 2.1.3
% 32.21/5.20 % (2110841)Termination reason: Refutation not found, incomplete strategy
% 32.21/5.20 % (2110841)Time elapsed: 0.005 s
% 32.21/5.20 % (2110841)Peak memory usage: 88 MB
% 32.21/5.20 % (2110841)Instructions burned: 6 (million)
% 32.21/5.20 % (2110844)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=653879302:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 32.21/5.20 % (2110841)------------------------------
% 32.21/5.20 % (2110841)------------------------------
% 32.21/5.20 % (2110847)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=809132222:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 32.21/5.20 % (2110847)Instruction limit reached!
% 32.21/5.20 % (2110847)------------------------------
% 32.21/5.20 % (2110847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.21/5.20 % (2110847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.21/5.20 % (2110847)CaDiCaL version: 2.1.3
% 32.21/5.20 % (2110847)Termination reason: Instruction limit
% 32.21/5.20 % (2110847)Termination phase: Saturation
% 32.21/5.20 % (2110847)Time elapsed: 0.079 s
% 32.21/5.20 % (2110847)Peak memory usage: 91 MB
% 32.21/5.20 % (2110847)Instructions burned: 140 (million)
% 32.21/5.20 % (2110840)Instruction limit reached!
% 32.21/5.20 % (2110840)------------------------------
% 32.21/5.20 % (2110840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.21/5.20 % (2110840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.21/5.20 % (2110840)CaDiCaL version: 2.1.3
% 32.21/5.20 % (2110840)Termination reason: Instruction limit
% 32.21/5.20 % (2110840)Termination phase: Saturation
% 32.21/5.20 % (2110840)Time elapsed: 0.507 s
% 32.21/5.20 % (2110840)Peak memory usage: 99 MB
% 32.21/5.20 % (2110840)Instructions burned: 907 (million)
% 32.21/5.20 % (2110831)Instruction limit reached!
% 32.21/5.20 % (2110831)------------------------------
% 32.21/5.20 % (2110831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.21/5.20 % (2110831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.21/5.20 % (2110831)CaDiCaL version: 2.1.3
% 32.21/5.20 % (2110831)Termination reason: Instruction limit
% 32.21/5.20 % (2110831)Termination phase: Saturation
% 32.21/5.20 % (2110831)Time elapsed: 0.862 s
% 32.21/5.20 % (2110831)Peak memory usage: 142 MB
% 32.21/5.20 % (2110831)Instructions burned: 2352 (million)
% 32.21/5.20 % (2110849)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2777985224:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 32.21/5.20 % (2110851)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=956702347:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi)
% 64.55/9.71 % (2110850)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4032086949:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 64.55/9.71 % (2110851)Instruction limit reached!
% 64.55/9.71 % (2110851)------------------------------
% 64.55/9.71 % (2110851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.55/9.71 % (2110851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.55/9.71 % (2110851)CaDiCaL version: 2.1.3
% 64.55/9.71 % (2110851)Termination reason: Instruction limit
% 64.55/9.71 % (2110851)Termination phase: Saturation
% 64.55/9.71 % (2110851)Time elapsed: 0.046 s
% 64.55/9.71 % (2110851)Peak memory usage: 91 MB
% 64.55/9.71 % (2110851)Instructions burned: 125 (million)
% 64.55/9.71 % (2110855)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1269218420:i=134:gtgl=5:slsql=off:gtg=exists_sym_2984 on theBenchmark for (2984ds/134Mi)
% 64.55/9.71 % (2110855)Instruction limit reached!
% 64.55/9.71 % (2110855)------------------------------
% 64.55/9.71 % (2110855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.55/9.71 % (2110855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.55/9.71 % (2110855)CaDiCaL version: 2.1.3
% 64.55/9.71 % (2110855)Termination reason: Instruction limit
% 64.55/9.71 % (2110855)Termination phase: Saturation
% 64.55/9.71 % (2110855)Time elapsed: 0.044 s
% 64.55/9.71 % (2110855)Peak memory usage: 90 MB
% 64.55/9.71 % (2110855)Instructions burned: 134 (million)
% 64.55/9.71 % (2110857)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1144609038:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/141Mi)
% 64.55/9.71 % (2110849)Instruction limit reached!
% 64.55/9.71 % (2110849)------------------------------
% 64.55/9.71 % (2110849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.55/9.71 % (2110849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.55/9.71 % (2110849)CaDiCaL version: 2.1.3
% 64.55/9.71 % (2110849)Termination reason: Instruction limit
% 64.55/9.71 % (2110849)Termination phase: Saturation
% 64.55/9.71 % (2110849)Time elapsed: 0.288 s
% 64.55/9.71 % (2110849)Peak memory usage: 92 MB
% 64.55/9.71 % (2110849)Instructions burned: 593 (million)
% 64.55/9.71 % (2110857)Instruction limit reached!
% 64.55/9.71 % (2110857)------------------------------
% 64.55/9.71 % (2110857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.55/9.71 % (2110857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.55/9.71 % (2110857)CaDiCaL version: 2.1.3
% 64.55/9.71 % (2110857)Termination reason: Instruction limit
% 64.55/9.71 % (2110857)Termination phase: Saturation
% 64.55/9.71 % (2110857)Time elapsed: 0.035 s
% 64.55/9.71 % (2110857)Peak memory usage: 90 MB
% 64.55/9.71 % (2110857)Instructions burned: 141 (million)
% 64.55/9.71 % (2110860)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=4234330603:i=6060:aac=none:ins=25_2981 on theBenchmark for (2981ds/6060Mi)
% 64.55/9.71 % (2110859)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3889443414:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2981 on theBenchmark for (2981ds/431Mi)
% 64.55/9.71 % (2110859)Refutation not found, incomplete strategy
% 64.55/9.71 % (2110859)------------------------------
% 64.55/9.71 % (2110859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.55/9.71 % (2110859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.55/9.71 % (2110859)CaDiCaL version: 2.1.3
% 64.55/9.71 % (2110859)Termination reason: Refutation not found, incomplete strategy
% 64.55/9.71 % (2110859)Time elapsed: 0.003 s
% 64.55/9.71 % (2110859)Peak memory usage: 88 MB
% 64.55/9.71 % (2110859)Instructions burned: 3 (million)
% 64.55/9.71 % (2110859)------------------------------
% 64.55/9.71 % (2110859)------------------------------
% 64.55/9.71 % (2110863)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=661175054:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2978 on theBenchmark for (2978ds/150Mi)
% 64.55/9.71 % (2110863)Instruction limit reached!
% 64.55/9.71 % (2110863)------------------------------
% 64.55/9.71 % (2110863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.32/13.59 % (2110863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.32/13.59 % (2110863)CaDiCaL version: 2.1.3
% 91.32/13.59 % (2110863)Termination reason: Instruction limit
% 91.32/13.59 % (2110863)Termination phase: Saturation
% 91.32/13.59 % (2110863)Time elapsed: 0.074 s
% 91.32/13.59 % (2110863)Peak memory usage: 91 MB
% 91.32/13.59 % (2110863)Instructions burned: 151 (million)
% 91.32/13.59 % (2110865)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1079356431:i=14155:bd=all_2976 on theBenchmark for (2976ds/14155Mi)
% 91.32/13.59 % (2110860)Instruction limit reached!
% 91.32/13.59 % (2110860)------------------------------
% 91.32/13.59 % (2110860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.32/13.59 % (2110860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.32/13.59 % (2110860)CaDiCaL version: 2.1.3
% 91.32/13.59 % (2110860)Termination reason: Instruction limit
% 91.32/13.59 % (2110860)Termination phase: Saturation
% 91.32/13.59 % (2110860)Time elapsed: 2.014 s
% 91.32/13.59 % (2110860)Peak memory usage: 162 MB
% 91.32/13.59 % (2110860)Instructions burned: 6062 (million)
% 91.32/13.59 % (2110844)Instruction limit reached!
% 91.32/13.59 % (2110844)------------------------------
% 91.32/13.59 % (2110844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.32/13.59 % (2110844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.32/13.59 % (2110844)CaDiCaL version: 2.1.3
% 91.32/13.59 % (2110844)Termination reason: Instruction limit
% 91.32/13.59 % (2110844)Termination phase: Saturation
% 91.32/13.59 % (2110844)Time elapsed: 2.929 s
% 91.32/13.59 % (2110844)Peak memory usage: 159 MB
% 91.32/13.59 % (2110844)Instructions burned: 5203 (million)
% 91.32/13.59 % (2110867)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1980503420:i=667:av=off:fsr=off_2960 on theBenchmark for (2960ds/667Mi)
% 91.32/13.59 % (2110868)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1164696892:s2a=on:i=185:s2at=1.8:fdi=4_2960 on theBenchmark for (2960ds/185Mi)
% 91.32/13.59 % (2110868)Instruction limit reached!
% 91.32/13.59 % (2110868)------------------------------
% 91.32/13.59 % (2110868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.32/13.59 % (2110868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.32/13.59 % (2110868)CaDiCaL version: 2.1.3
% 91.32/13.59 % (2110868)Termination reason: Instruction limit
% 91.32/13.59 % (2110868)Termination phase: Saturation
% 91.32/13.59 % (2110868)Time elapsed: 0.092 s
% 91.32/13.59 % (2110868)Peak memory usage: 91 MB
% 91.32/13.59 % (2110868)Instructions burned: 186 (million)
% 91.32/13.59 % (2110867)Instruction limit reached!
% 91.32/13.59 % (2110867)------------------------------
% 91.32/13.59 % (2110867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.32/13.59 % (2110867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.32/13.59 % (2110867)CaDiCaL version: 2.1.3
% 91.32/13.59 % (2110867)Termination reason: Instruction limit
% 91.32/13.59 % (2110867)Termination phase: Saturation
% 91.32/13.59 % (2110867)Time elapsed: 0.187 s
% 91.32/13.59 % (2110867)Peak memory usage: 108 MB
% 91.32/13.59 % (2110867)Instructions burned: 668 (million)
% 91.32/13.59 % (2110872)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1650628611:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2957 on theBenchmark for (2957ds/4850Mi)
% 91.32/13.59 % (2110871)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=791737744:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2957 on theBenchmark for (2957ds/193Mi)
% 91.32/13.59 % (2110871)Instruction limit reached!
% 91.32/13.59 % (2110871)------------------------------
% 91.32/13.59 % (2110871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.32/13.59 % (2110871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.32/13.59 % (2110871)CaDiCaL version: 2.1.3
% 91.32/13.59 % (2110871)Termination reason: Instruction limit
% 91.32/13.59 % (2110871)Termination phase: Saturation
% 91.32/13.59 % (2110871)Time elapsed: 0.094 s
% 91.32/13.59 % (2110871)Peak memory usage: 89 MB
% 91.32/13.59 % (2110871)Instructions burned: 194 (million)
% 91.32/13.59 % (2110875)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1533389561:i=12111:sd=1:ss=included_2955 on theBenchmark for (2955ds/12111Mi)
% 124.98/18.27 % (2110872)Instruction limit reached!
% 124.98/18.27 % (2110872)------------------------------
% 124.98/18.27 % (2110872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.98/18.27 % (2110872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.98/18.27 % (2110872)CaDiCaL version: 2.1.3
% 124.98/18.27 % (2110872)Termination reason: Instruction limit
% 124.98/18.27 % (2110872)Termination phase: Saturation
% 124.98/18.27 % (2110872)Time elapsed: 1.482 s
% 124.98/18.27 % (2110872)Peak memory usage: 128 MB
% 124.98/18.27 % (2110872)Instructions burned: 4851 (million)
% 124.98/18.27 % (2110877)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2886078286:i=319:kws=precedence:fsr=off_2942 on theBenchmark for (2942ds/319Mi)
% 124.98/18.27 % (2110877)Instruction limit reached!
% 124.98/18.27 % (2110877)------------------------------
% 124.98/18.27 % (2110877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.98/18.27 % (2110877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.98/18.27 % (2110877)CaDiCaL version: 2.1.3
% 124.98/18.27 % (2110877)Termination reason: Instruction limit
% 124.98/18.27 % (2110877)Termination phase: Saturation
% 124.98/18.27 % (2110877)Time elapsed: 0.115 s
% 124.98/18.27 % (2110877)Peak memory usage: 92 MB
% 124.98/18.27 % (2110877)Instructions burned: 321 (million)
% 124.98/18.27 % (2110879)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=4002808472:i=2064:ep=RST_2939 on theBenchmark for (2939ds/2064Mi)
% 124.98/18.27 % (2110879)Instruction limit reached!
% 124.98/18.27 % (2110879)------------------------------
% 124.98/18.27 % (2110879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.98/18.27 % (2110879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.98/18.27 % (2110879)CaDiCaL version: 2.1.3
% 124.98/18.27 % (2110879)Termination reason: Instruction limit
% 124.98/18.27 % (2110879)Termination phase: Saturation
% 124.98/18.27 % (2110879)Time elapsed: 0.586 s
% 124.98/18.27 % (2110879)Peak memory usage: 111 MB
% 124.98/18.27 % (2110879)Instructions burned: 2064 (million)
% 124.98/18.27 % (2110881)dis-1011_128_sil=32000:random_seed=2257845446:i=3706:ep=RST:av=off_2933 on theBenchmark for (2933ds/3706Mi)
% 124.98/18.27 % (2110881)Instruction limit reached!
% 124.98/18.27 % (2110881)------------------------------
% 124.98/18.27 % (2110881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.98/18.27 % (2110881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.98/18.27 % (2110881)CaDiCaL version: 2.1.3
% 124.98/18.27 % (2110881)Termination reason: Instruction limit
% 124.98/18.27 % (2110881)Termination phase: Saturation
% 124.98/18.27 % (2110881)Time elapsed: 0.745 s
% 124.98/18.27 % (2110881)Peak memory usage: 90 MB
% 124.98/18.27 % (2110881)Instructions burned: 3712 (million)
% 124.98/18.27 % (2110883)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1267448262:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2924 on theBenchmark for (2924ds/757Mi)
% 124.98/18.27 % (2110883)Refutation not found, incomplete strategy
% 124.98/18.27 % (2110883)------------------------------
% 124.98/18.27 % (2110883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.98/18.27 % (2110883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.98/18.27 % (2110883)CaDiCaL version: 2.1.3
% 124.98/18.27 % (2110883)Termination reason: Refutation not found, incomplete strategy
% 124.98/18.27 % (2110883)Time elapsed: 0.002 s
% 124.98/18.27 % (2110883)Peak memory usage: 89 MB
% 124.98/18.27 % (2110883)Instructions burned: 5 (million)
% 124.98/18.27 % (2110883)------------------------------
% 124.98/18.27 % (2110883)------------------------------
% 124.98/18.27 % (2110885)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2561300296:i=13913:ss=axioms:sgt=8_2922 on theBenchmark for (2922ds/13913Mi)
% 124.98/18.27 % (2110850)Instruction limit reached!
% 124.98/18.27 % (2110850)------------------------------
% 124.98/18.27 % (2110850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.98/18.27 % (2110850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.98/18.27 % (2110850)CaDiCaL version: 2.1.3
% 124.98/18.27 % (2110850)Termination reason: Instruction limit
% 124.98/18.27 % (2110850)Termination phase: Saturation
% 124.98/18.27 % (2110850)Time elapsed: 7.391 s
% 124.98/18.27 % (2110850)Peak memory usage: 249 MB
% 124.98/18.27 % (2110850)Instructions burned: 13194 (million)
% 124.98/18.27 % (2110887)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2124667143:i=9925:aac=none_2910 on theBenchmark for (2910ds/9925Mi)
% 135.30/19.77 % (2110865)Instruction limit reached!
% 135.30/19.77 % (2110865)------------------------------
% 135.30/19.77 % (2110865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 135.30/19.77 % (2110865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.30/19.77 % (2110865)CaDiCaL version: 2.1.3
% 135.30/19.77 % (2110865)Termination reason: Instruction limit
% 135.30/19.77 % (2110865)Termination phase: Saturation
% 135.30/19.77 % (2110865)Time elapsed: 7.835 s
% 135.30/19.77 % (2110865)Peak memory usage: 211 MB
% 135.30/19.77 % (2110865)Instructions burned: 14156 (million)
% 135.30/19.77 % (2110889)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=679908474:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2896 on theBenchmark for (2896ds/2479Mi)
% 135.30/19.77 % (2110889)Refutation not found, incomplete strategy
% 135.30/19.77 % (2110889)------------------------------
% 135.30/19.77 % (2110889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 135.30/19.77 % (2110889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.30/19.77 % (2110889)CaDiCaL version: 2.1.3
% 135.30/19.77 % (2110889)Termination reason: Refutation not found, incomplete strategy
% 135.30/19.77 % (2110889)Time elapsed: 0.003 s
% 135.30/19.77 % (2110889)Peak memory usage: 88 MB
% 135.30/19.77 % (2110889)Instructions burned: 3 (million)
% 135.30/19.77 % (2110889)------------------------------
% 135.30/19.77 % (2110889)------------------------------
% 135.30/19.77 % (2110891)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2511201546:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2892 on theBenchmark for (2892ds/440Mi)
% 135.30/19.77 % (2110891)Instruction limit reached!
% 135.30/19.77 % (2110891)------------------------------
% 135.30/19.77 % (2110891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 135.30/19.77 % (2110891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.30/19.77 % (2110891)CaDiCaL version: 2.1.3
% 135.30/19.77 % (2110891)Termination reason: Instruction limit
% 135.30/19.77 % (2110891)Termination phase: Saturation
% 135.30/19.77 % (2110891)Time elapsed: 0.215 s
% 135.30/19.77 % (2110891)Peak memory usage: 92 MB
% 135.30/19.77 % (2110891)Instructions burned: 442 (million)
% 135.30/19.77 % (2110893)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1191723547:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2889 on theBenchmark for (2889ds/11145Mi)
% 135.30/19.77 % (2110885)Instruction limit reached!
% 135.30/19.77 % (2110885)------------------------------
% 135.30/19.77 % (2110885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 135.30/19.77 % (2110885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.30/19.77 % (2110885)CaDiCaL version: 2.1.3
% 135.30/19.77 % (2110885)Termination reason: Instruction limit
% 135.30/19.77 % (2110885)Termination phase: Saturation
% 135.30/19.77 % (2110885)Time elapsed: 4.516 s
% 135.30/19.77 % (2110885)Peak memory usage: 246 MB
% 135.30/19.77 % (2110885)Instructions burned: 13914 (million)
% 135.30/19.77 % (2110895)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=2699849945:cts=off:i=3034:av=off:er=known:fsd=on_2876 on theBenchmark for (2876ds/3034Mi)
% 135.30/19.77 % (2110875)Instruction limit reached!
% 135.30/19.77 % (2110875)------------------------------
% 135.30/19.77 % (2110875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 135.30/19.77 % (2110875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.30/19.77 % (2110875)CaDiCaL version: 2.1.3
% 135.30/19.77 % (2110875)Termination reason: Instruction limit
% 135.30/19.77 % (2110875)Termination phase: Saturation
% 135.30/19.77 % (2110875)Time elapsed: 7.989 s
% 135.30/19.77 % (2110875)Peak memory usage: 238 MB
% 135.30/19.77 % (2110875)Instructions burned: 12112 (million)
% 135.30/19.77 % (2110897)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=630606338:st=2:s2a=on:i=524:s2at=2:ss=axioms_2873 on theBenchmark for (2873ds/524Mi)
% 135.30/19.77 % (2110897)Instruction limit reached!
% 135.30/19.77 % (2110897)------------------------------
% 135.30/19.77 % (2110897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 135.30/19.77 % (2110897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.30/19.77 % (2110897)CaDiCaL version: 2.1.3
% 135.30/19.77 % (2110897)Termination reason: Instruction limit
% 167.55/24.25 % (2110897)Termination phase: Saturation
% 167.55/24.25 % (2110897)Time elapsed: 0.256 s
% 167.55/24.25 % (2110897)Peak memory usage: 96 MB
% 167.55/24.25 % (2110897)Instructions burned: 525 (million)
% 167.55/24.25 % (2110899)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3657551486:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2870 on theBenchmark for (2870ds/1016Mi)
% 167.55/24.25 % (2110895)Instruction limit reached!
% 167.55/24.25 % (2110895)------------------------------
% 167.55/24.25 % (2110895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 167.55/24.25 % (2110895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 167.55/24.25 % (2110895)CaDiCaL version: 2.1.3
% 167.55/24.25 % (2110895)Termination reason: Instruction limit
% 167.55/24.25 % (2110895)Termination phase: Saturation
% 167.55/24.25 % (2110895)Time elapsed: 0.985 s
% 167.55/24.25 % (2110895)Peak memory usage: 144 MB
% 167.55/24.25 % (2110895)Instructions burned: 3036 (million)
% 167.55/24.25 % (2110901)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=4064485445:i=14123:bd=preordered:ins=4_2865 on theBenchmark for (2865ds/14123Mi)
% 167.55/24.25 % (2110899)Instruction limit reached!
% 167.55/24.25 % (2110899)------------------------------
% 167.55/24.25 % (2110899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 167.55/24.25 % (2110899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 167.55/24.25 % (2110899)CaDiCaL version: 2.1.3
% 167.55/24.25 % (2110899)Termination reason: Instruction limit
% 167.55/24.25 % (2110899)Termination phase: Saturation
% 167.55/24.25 % (2110899)Time elapsed: 0.590 s
% 167.55/24.25 % (2110899)Peak memory usage: 97 MB
% 167.55/24.25 % (2110899)Instructions burned: 1017 (million)
% 167.55/24.25 % (2110903)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3507557382:i=5781:kws=precedence:bd=all:rawr=on_2862 on theBenchmark for (2862ds/5781Mi)
% 167.55/24.25 % (2110887)Instruction limit reached!
% 167.55/24.25 % (2110887)------------------------------
% 167.55/24.25 % (2110887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 167.55/24.25 % (2110887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 167.55/24.25 % (2110887)CaDiCaL version: 2.1.3
% 167.55/24.25 % (2110887)Termination reason: Instruction limit
% 167.55/24.25 % (2110887)Termination phase: Saturation
% 167.55/24.25 % (2110887)Time elapsed: 6.288 s
% 167.55/24.25 % (2110887)Peak memory usage: 190 MB
% 167.55/24.25 % (2110887)Instructions burned: 9926 (million)
% 167.55/24.25 % (2110905)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=1567122861:i=2448:gtgl=5:bd=preordered:gtg=all_2845 on theBenchmark for (2845ds/2448Mi)
% 167.55/24.25 % (2110903)Instruction limit reached!
% 167.55/24.25 % (2110903)------------------------------
% 167.55/24.25 % (2110903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 167.55/24.25 % (2110903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 167.55/24.25 % (2110903)CaDiCaL version: 2.1.3
% 167.55/24.25 % (2110903)Termination reason: Instruction limit
% 167.55/24.25 % (2110903)Termination phase: Saturation
% 167.55/24.25 % (2110903)Time elapsed: 2.970 s
% 167.55/24.25 % (2110903)Peak memory usage: 112 MB
% 167.55/24.25 % (2110903)Instructions burned: 5781 (million)
% 167.55/24.25 % (2110905)Instruction limit reached!
% 167.55/24.25 % (2110905)------------------------------
% 167.55/24.25 % (2110905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 167.55/24.25 % (2110905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 167.55/24.25 % (2110905)CaDiCaL version: 2.1.3
% 167.55/24.25 % (2110905)Termination reason: Instruction limit
% 167.55/24.25 % (2110905)Termination phase: Saturation
% 167.55/24.25 % (2110905)Time elapsed: 1.378 s
% 167.55/24.25 % (2110905)Peak memory usage: 145 MB
% 167.55/24.25 % (2110905)Instructions burned: 2450 (million)
% 167.55/24.25 % (2110907)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3780682786:i=3223:kws=precedence:fgj=on:av=off_2831 on theBenchmark for (2831ds/3223Mi)
% 167.55/24.25 % (2110908)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=1021855388:st=5.6:i=2033:sd=3:ss=axioms_2830 on theBenchmark for (2830ds/2033Mi)
% 167.55/24.25 % (2110908)Refutation not found, incomplete strategy
% 167.55/24.25 % (2110908)------------------------------
% 167.55/24.25 % (2110908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.78/27.94 % (2110908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.78/27.94 % (2110908)CaDiCaL version: 2.1.3
% 92.78/27.94 % (2110908)Termination reason: Refutation not found, incomplete strategy
% 92.78/27.94 % (2110908)Time elapsed: 0.615 s
% 92.78/27.94 % (2110908)Peak memory usage: 129 MB
% 92.78/27.94 % (2110908)Instructions burned: 913 (million)
% 92.78/27.94 % (2110901)Instruction limit reached!
% 92.78/27.94 % (2110901)------------------------------
% 92.78/27.94 % (2110901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.78/27.94 % (2110901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.78/27.94 % (2110901)CaDiCaL version: 2.1.3
% 92.78/27.94 % (2110901)Termination reason: Instruction limit
% 92.78/27.94 % (2110901)Termination phase: Saturation
% 92.78/27.94 % (2110901)Time elapsed: 4.181 s
% 92.78/27.94 % (2110901)Peak memory usage: 197 MB
% 92.78/27.94 % (2110901)Instructions burned: 14126 (million)
% 92.78/27.94 % (2110911)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=1257985919:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2822 on theBenchmark for (2822ds/2055Mi)
% 92.78/27.94 % (2110908)------------------------------
% 92.78/27.94 % (2110908)------------------------------
% 92.78/27.94 % (2110893)Instruction limit reached!
% 92.78/27.94 % (2110893)------------------------------
% 92.78/27.94 % (2110893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.78/27.94 % (2110893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.78/27.94 % (2110893)CaDiCaL version: 2.1.3
% 92.78/27.94 % (2110893)Termination reason: Instruction limit
% 92.78/27.94 % (2110893)Termination phase: Saturation
% 92.78/27.94 % (2110893)Time elapsed: 6.825 s
% 92.78/27.94 % (2110893)Peak memory usage: 209 MB
% 92.78/27.94 % (2110893)Instructions burned: 11147 (million)
% 92.78/27.94 % (2110913)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=3840064888:i=21611:sd=3:ss=axioms_2820 on theBenchmark for (2820ds/21611Mi)
% 92.78/27.94 % (2110915)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=948257552:i=4835:sd=13:ss=axioms:sgt=23_2819 on theBenchmark for (2819ds/4835Mi)
% 92.78/27.94 % (2110911)Instruction limit reached!
% 92.78/27.94 % (2110911)------------------------------
% 92.78/27.94 % (2110911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.78/27.94 % (2110911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.78/27.94 % (2110911)CaDiCaL version: 2.1.3
% 92.78/27.94 % (2110911)Termination reason: Instruction limit
% 92.78/27.94 % (2110911)Termination phase: Saturation
% 92.78/27.94 % (2110911)Time elapsed: 0.671 s
% 92.78/27.94 % (2110911)Peak memory usage: 132 MB
% 92.78/27.94 % (2110911)Instructions burned: 2057 (million)
% 92.78/27.94 % (2110917)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=2829741703:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2814 on theBenchmark for (2814ds/797Mi)
% 92.78/27.94 % (2110917)Instruction limit reached!
% 92.78/27.94 % (2110917)------------------------------
% 92.78/27.94 % (2110917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.78/27.94 % (2110917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.78/27.94 % (2110917)CaDiCaL version: 2.1.3
% 92.78/27.94 % (2110917)Termination reason: Instruction limit
% 92.78/27.94 % (2110917)Termination phase: Saturation
% 92.78/27.94 % (2110917)Time elapsed: 0.219 s
% 92.78/27.94 % (2110917)Peak memory usage: 104 MB
% 92.78/27.94 % (2110917)Instructions burned: 801 (million)
% 92.78/27.94 % (2110919)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2782172087:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2811 on theBenchmark for (2811ds/2326Mi)
% 92.78/27.94 % (2110907)Instruction limit reached!
% 92.78/27.94 % (2110907)------------------------------
% 92.78/27.94 % (2110907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.78/27.94 % (2110907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.78/27.94 % (2110907)CaDiCaL version: 2.1.3
% 92.78/27.94 % (2110907)Termination reason: Instruction limit
% 92.78/27.94 % (2110907)Termination phase: Saturation
% 92.78/27.94 % (2110907)Time elapsed: 2.092 s
% 92.78/27.94 % (2110907)Peak memory usage: 148 MB
% 92.78/27.94 % (2110907)Instructions burned: 3223 (million)
% 92.78/27.94 % (2110921)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=1986747031:i=6038:nm=6_2809 on theBenchmark for (2809ds/6038Mi)
% 92.78/27.94 % (2110919)Instruction limit reached!
% 92.78/27.94 % (2110919)------------------------------
% 92.78/27.94 % (2110919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.78/27.94 % (2110919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.78/27.94 % (2110919)CaDiCaL version: 2.1.3
% 92.78/27.94 % (2110919)Termination reason: Instruction limit
% 92.78/27.94 % (2110919)Termination phase: Saturation
% 92.78/27.94 % (2110919)Time elapsed: 0.504 s
% 92.78/27.94 % (2110919)Peak memory usage: 91 MB
% 92.78/27.94 % (2110919)Instructions burned: 2331 (million)
% 92.78/27.94 % (2110923)lrs+10_1_sil=32000:sp=occurrence:random_seed=1709718724:st=2:i=33334:sd=3:ss=included:sgt=32_2805 on theBenchmark for (2805ds/33334Mi)
% 92.78/27.94 % (2110915)Instruction limit reached!
% 92.78/27.94 % (2110915)------------------------------
% 92.78/27.94 % (2110915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.78/27.94 % (2110915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.78/27.94 % (2110915)CaDiCaL version: 2.1.3
% 92.78/27.94 % (2110915)Termination reason: Instruction limit
% 92.78/27.94 % (2110915)Termination phase: Saturation
% 92.78/27.94 % (2110915)Time elapsed: 2.746 s
% 92.78/27.94 % (2110915)Peak memory usage: 124 MB
% 92.78/27.94 % (2110915)Instructions burned: 4835 (million)
% 92.78/27.94 % (2110925)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=2062349798:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2790 on theBenchmark for (2790ds/1008Mi)
% 92.78/27.94 % (2110925)Instruction limit reached!
% 92.78/27.94 % (2110925)------------------------------
% 92.78/27.94 % (2110925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.78/27.94 % (2110925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.78/27.94 % (2110925)CaDiCaL version: 2.1.3
% 92.78/27.94 % (2110925)Termination reason: Instruction limit
% 92.78/27.94 % (2110925)Termination phase: Saturation
% 92.78/27.94 % (2110925)Time elapsed: 0.481 s
% 92.78/27.94 % (2110925)Peak memory usage: 99 MB
% 92.78/27.94 % (2110925)Instructions burned: 1008 (million)
% 92.78/27.94 % (2110927)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=906491291:i=8327:s2at=5:bd=preordered_2784 on theBenchmark for (2784ds/8327Mi)
% 92.78/27.94 % (2110921)Instruction limit reached!
% 92.78/27.94 % (2110921)------------------------------
% 92.78/27.94 % (2110921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.78/27.94 % (2110921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.78/27.94 % (2110921)CaDiCaL version: 2.1.3
% 92.78/27.94 % (2110921)Termination reason: Instruction limit
% 92.78/27.94 % (2110921)Termination phase: Saturation
% 92.78/27.94 % (2110921)Time elapsed: 3.213 s
% 92.78/27.94 % (2110921)Peak memory usage: 175 MB
% 92.78/27.94 % (2110921)Instructions burned: 6040 (million)
% 92.78/27.94 % (2110929)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=2320445490:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2776 on theBenchmark for (2776ds/1083Mi)
% 92.78/27.94 % (2110929)Instruction limit reached!
% 92.78/27.94 % (2110929)------------------------------
% 92.78/27.94 % (2110929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.78/27.94 % (2110929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.78/27.94 % (2110929)CaDiCaL version: 2.1.3
% 92.78/27.94 % (2110929)Termination reason: Instruction limit
% 92.78/27.94 % (2110929)Termination phase: Saturation
% 92.78/27.94 % (2110929)Time elapsed: 0.436 s
% 92.78/27.94 % (2110929)Peak memory usage: 97 MB
% 92.78/27.94 % (2110929)Instructions burned: 1086 (million)
% 92.78/27.94 % (2110931)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=4274665678:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2770 on theBenchmark for (2770ds/1084Mi)
% 92.78/27.94 % (2110931)Instruction limit reached!
% 92.78/27.94 % (2110931)------------------------------
% 92.78/27.94 % (2110931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.78/27.94 % (2110931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.78/27.94 % (2110931)CaDiCaL version: 2.1.3
% 92.78/27.94 % (2110931)Termination reason: Instruction limit
% 92.78/27.94 % (2110931)Termination phase: Saturation
% 92.78/27.94 % (2110931)Time elapsed: 0.548 s
% 92.78/27.94 % (2110931)Peak memory usage: 99 MB
% 92.78/27.94 % (2110931)Instructions burned: 1084 (million)
% 92.78/27.94 % (2110933)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=4171242716:i=6995:s2at=5:gtg=all_2763 on theBenchmark for (2763ds/6995Mi)
% 92.78/27.94 % (2110927)Instruction limit reached!
% 92.78/27.94 % (2110927)------------------------------
% 92.78/27.94 % (2110927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.78/27.94 % (2110927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.78/27.94 % (2110927)CaDiCaL version: 2.1.3
% 92.78/27.94 % (2110927)Termination reason: Instruction limit
% 92.78/27.94 % (2110927)Termination phase: Saturation
% 92.78/27.94 % (2110927)Time elapsed: 4.905 s
% 92.78/27.94 % (2110927)Peak memory usage: 181 MB
% 92.78/27.94 % (2110927)Instructions burned: 8328 (million)
% 92.78/27.94 % (2110935)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=2657915564:st=2:i=6225:sd=15:ss=axioms_2734 on theBenchmark for (2734ds/6225Mi)
% 92.78/27.94 % (2110933)First to succeed.
% 92.78/27.94 % (2110933)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2110804"
% 92.78/27.94 % (2110933)Refutation found. Thanks to Tanya!
% 92.78/27.94 % SZS status Theorem for theBenchmark
% 92.78/27.94 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/28.14 % (2110933)------------------------------
% 0.17/28.14 % (2110933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/28.14 % (2110933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/28.14 % (2110933)CaDiCaL version: 2.1.3
% 0.17/28.14 % (2110933)Termination reason: Refutation
% 0.17/28.14 % (2110933)Time elapsed: 3.194 s
% 0.17/28.14 % (2110933)Peak memory usage: 158 MB
% 0.17/28.14 % (2110933)Instructions burned: 5361 (million)
% 0.17/28.14 % (2110933)------------------------------
% 0.17/28.14 % (2110933)------------------------------
% 0.17/28.14 % (2110804)Success in time 27.332 s
% 0.17/28.14 % Vampire exiting
%------------------------------------------------------------------------------