%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP634+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:15:10 AM UTC 2026
% Result : Theorem 25.67s 7.91s
% Output : Refutation 46.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 39
% Syntax : Number of formulae : 385 ( 45 unt; 15 def)
% Number of atoms : 2048 ( 122 equ)
% Maximal formula atoms : 17 ( 5 avg)
% Number of connectives : 2914 (1251 ~;1381 |; 208 &)
% ( 23 <=>; 51 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 30 ( 28 usr; 16 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 2 con; 0-3 aty)
% Number of variables : 274 ( 0 sgn 266 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18896,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))
=> ( ( k1_group_1(X0,X1,X2) = X1
| k1_group_1(X0,X2,X1) = X1 )
=> X2 = k2_group_1(X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t15_group_1) ).
fof(f18989,axiom,
! [X0] :
( l1_group_1(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_group_1) ).
fof(f18991,axiom,
! [X0] :
( l1_group_1(X0)
=> ( v1_group_1(X0)
=> X0 = g1_group_1(u1_struct_0(X0),u1_group_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',abstractness_v1_group_1) ).
fof(f18992,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& l1_group_1(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> m1_subset_1(k1_group_1(X0,X1,X2),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_group_1) ).
fof(f20339,axiom,
! [X0] :
( l1_struct_0(X0)
=> ( v3_realset2(X0)
<=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> X1 = X2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d7_realset2) ).
fof(f21806,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> v4_group_1(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_group_2) ).
fof(f21862,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> m1_subset_1(X2,u1_struct_0(X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t51_group_2) ).
fof(f21863,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_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))
=> ! [X3] :
( m1_group_2(X3,X0)
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X3))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(X3))
=> ( ( X4 = X1
& X5 = X2 )
=> k1_group_1(X3,X4,X5) = k1_group_1(X0,X1,X2) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t52_group_2) ).
fof(f21874,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> m1_group_2(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t63_group_2) ).
fof(f21885,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> k6_group_2(X0) = g1_group_1(u1_struct_0(X0),u1_group_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_group_2) ).
fof(f22007,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& l1_group_1(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_group_2) ).
fof(f25683,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ( m1_group_2(X1,k10_group_5(X0))
=> ( v1_group_3(X1,X0)
& m1_group_2(X1,X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t91_group_5) ).
fof(f25686,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& v7_group_1(X0)
& l1_group_1(X0) )
<=> k10_group_5(X0) = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t94_group_5) ).
fof(f26893,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& v1_group_3(X1,X0)
& m1_group_2(X1,X0) )
=> ( ~ v3_struct_0(k6_group_6(X0,X1))
& v1_group_1(k6_group_6(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_group_6) ).
fof(f26894,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& v1_group_3(X1,X0)
& m1_group_2(X1,X0) )
=> ( ~ v3_struct_0(k6_group_6(X0,X1))
& v1_group_1(k6_group_6(X0,X1))
& v2_group_1(k6_group_6(X0,X1))
& v3_group_1(k6_group_6(X0,X1))
& v4_group_1(k6_group_6(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc5_group_6) ).
fof(f26992,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> v3_realset2(k6_group_6(X0,k6_group_2(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t83_group_6) ).
fof(f26996,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v1_group_1(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
=> ( ( r2_group_6(X0,X1)
& v3_realset2(X0) )
=> v3_realset2(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t87_group_6) ).
fof(f27007,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& ~ v3_struct_0(X1)
& v1_group_1(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
=> ( r2_group_6(X0,X1)
=> r2_group_6(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetry_r2_group_6) ).
fof(f27017,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& v1_group_3(X1,X0)
& m1_group_2(X1,X0) )
=> l1_group_1(k6_group_6(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k6_group_6) ).
fof(f33387,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k3_autgroup(X0))
& v1_group_1(k3_autgroup(X0))
& v3_group_1(k3_autgroup(X0))
& v4_group_1(k3_autgroup(X0))
& l1_group_1(k3_autgroup(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_autgroup) ).
fof(f33389,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( v1_group_1(k5_autgroup(X0))
& v1_group_3(k5_autgroup(X0),k3_autgroup(X0))
& m1_group_2(k5_autgroup(X0),k3_autgroup(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_autgroup) ).
fof(f33416,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( v1_group_1(X1)
& v1_group_3(X1,k3_autgroup(X0))
& m1_group_2(X1,k3_autgroup(X0)) )
=> ( X1 = k5_autgroup(X0)
<=> u1_struct_0(X1) = k4_autgroup(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_autgroup) ).
fof(f33430,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> r2_group_6(k5_autgroup(X0),k6_group_6(X0,k10_group_5(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t31_autgroup) ).
fof(f33431,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& v7_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(k5_autgroup(X0)))
=> X1 = k2_group_1(k5_autgroup(X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t32_autgroup) ).
fof(f33432,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& v7_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(k5_autgroup(X0)))
=> X1 = k2_group_1(k5_autgroup(X0)) ) ) ),
inference(negated_conjecture,[status(cth)],[f33431]) ).
fof(f33841,plain,
? [X0] :
( ? [X1] :
( k2_group_1(k5_autgroup(X0)) != X1
& m1_subset_1(X1,u1_struct_0(k5_autgroup(X0))) )
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& v7_group_1(X0)
& l1_group_1(X0)
& ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(ennf_transformation,[],[f33432]) ).
fof(f33842,plain,
? [X0] :
( ? [X1] :
( k2_group_1(k5_autgroup(X0)) != X1
& m1_subset_1(X1,u1_struct_0(k5_autgroup(X0))) )
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& v7_group_1(X0)
& l1_group_1(X0)
& ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(flattening,[],[f33841]) ).
fof(f33849,plain,
! [X0] :
( ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& l1_group_1(X1) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f22007]) ).
fof(f33850,plain,
! [X0] :
( ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& l1_group_1(X1) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f33849]) ).
fof(f33855,plain,
! [X0] :
( m1_group_2(X0,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f21874]) ).
fof(f33856,plain,
! [X0] :
( m1_group_2(X0,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f33855]) ).
fof(f33859,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f21862]) ).
fof(f33860,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f33859]) ).
fof(f33863,plain,
! [X0] :
( ! [X1] :
( v4_group_1(X1)
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f21806]) ).
fof(f33864,plain,
! [X0] :
( ! [X1] :
( v4_group_1(X1)
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f33863]) ).
fof(f33931,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X2 = k2_group_1(X0)
| ( k1_group_1(X0,X1,X2) != X1
& k1_group_1(X0,X2,X1) != 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,[],[f18896]) ).
fof(f33932,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X2 = k2_group_1(X0)
| ( k1_group_1(X0,X1,X2) != X1
& k1_group_1(X0,X2,X1) != 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,[],[f33931]) ).
fof(f33941,plain,
! [X0] :
( r2_group_6(k5_autgroup(X0),k6_group_6(X0,k10_group_5(X0)))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f33430]) ).
fof(f33942,plain,
! [X0] :
( r2_group_6(k5_autgroup(X0),k6_group_6(X0,k10_group_5(X0)))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f33941]) ).
fof(f33949,plain,
! [X0] :
( ! [X1] :
( ( X1 = k5_autgroup(X0)
<=> u1_struct_0(X1) = k4_autgroup(X0) )
| ~ v1_group_1(X1)
| ~ v1_group_3(X1,k3_autgroup(X0))
| ~ m1_group_2(X1,k3_autgroup(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f33416]) ).
fof(f33950,plain,
! [X0] :
( ! [X1] :
( ( X1 = k5_autgroup(X0)
<=> u1_struct_0(X1) = k4_autgroup(X0) )
| ~ v1_group_1(X1)
| ~ v1_group_3(X1,k3_autgroup(X0))
| ~ m1_group_2(X1,k3_autgroup(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f33949]) ).
fof(f33951,plain,
! [X0] :
( ( v1_group_1(k5_autgroup(X0))
& v1_group_3(k5_autgroup(X0),k3_autgroup(X0))
& m1_group_2(k5_autgroup(X0),k3_autgroup(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f33389]) ).
fof(f33952,plain,
! [X0] :
( ( v1_group_1(k5_autgroup(X0))
& v1_group_3(k5_autgroup(X0),k3_autgroup(X0))
& m1_group_2(k5_autgroup(X0),k3_autgroup(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f33951]) ).
fof(f33992,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( k1_group_1(X3,X4,X5) = k1_group_1(X0,X1,X2)
| X1 != X4
| X2 != X5
| ~ m1_subset_1(X5,u1_struct_0(X3)) )
| ~ m1_subset_1(X4,u1_struct_0(X3)) )
| ~ m1_group_2(X3,X0) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f21863]) ).
fof(f33993,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( k1_group_1(X3,X4,X5) = k1_group_1(X0,X1,X2)
| X1 != X4
| X2 != X5
| ~ m1_subset_1(X5,u1_struct_0(X3)) )
| ~ m1_subset_1(X4,u1_struct_0(X3)) )
| ~ m1_group_2(X3,X0) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f33992]) ).
fof(f34086,plain,
! [X0,X1] :
( l1_group_1(k6_group_6(X0,X1))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(X1,X0) ),
inference(ennf_transformation,[],[f27017]) ).
fof(f34087,plain,
! [X0,X1] :
( l1_group_1(k6_group_6(X0,X1))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(X1,X0) ),
inference(flattening,[],[f34086]) ).
fof(f34098,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k6_group_6(X0,X1))
& v1_group_1(k6_group_6(X0,X1))
& v2_group_1(k6_group_6(X0,X1))
& v3_group_1(k6_group_6(X0,X1))
& v4_group_1(k6_group_6(X0,X1)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(X1,X0) ),
inference(ennf_transformation,[],[f26894]) ).
fof(f34099,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k6_group_6(X0,X1))
& v1_group_1(k6_group_6(X0,X1))
& v2_group_1(k6_group_6(X0,X1))
& v3_group_1(k6_group_6(X0,X1))
& v4_group_1(k6_group_6(X0,X1)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(X1,X0) ),
inference(flattening,[],[f34098]) ).
fof(f34100,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k6_group_6(X0,X1))
& v1_group_1(k6_group_6(X0,X1)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(X1,X0) ),
inference(ennf_transformation,[],[f26893]) ).
fof(f34101,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k6_group_6(X0,X1))
& v1_group_1(k6_group_6(X0,X1)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(X1,X0) ),
inference(flattening,[],[f34100]) ).
fof(f34294,plain,
! [X0,X1,X2] :
( m1_subset_1(k1_group_1(X0,X1,X2),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f18992]) ).
fof(f34295,plain,
! [X0,X1,X2] :
( m1_subset_1(k1_group_1(X0,X1,X2),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f34294]) ).
fof(f34849,plain,
! [X0,X1] :
( r2_group_6(X1,X0)
| ~ r2_group_6(X0,X1)
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X1)
| ~ v1_group_1(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(ennf_transformation,[],[f27007]) ).
fof(f34850,plain,
! [X0,X1] :
( r2_group_6(X1,X0)
| ~ r2_group_6(X0,X1)
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X1)
| ~ v1_group_1(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(flattening,[],[f34849]) ).
fof(f34853,plain,
! [X0] :
( ! [X1] :
( v3_realset2(X1)
| ~ r2_group_6(X0,X1)
| ~ v3_realset2(X0)
| v3_struct_0(X1)
| ~ v1_group_1(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f26996]) ).
fof(f34854,plain,
! [X0] :
( ! [X1] :
( v3_realset2(X1)
| ~ r2_group_6(X0,X1)
| ~ v3_realset2(X0)
| v3_struct_0(X1)
| ~ v1_group_1(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f34853]) ).
fof(f34869,plain,
! [X0] :
( ( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& v7_group_1(X0)
& l1_group_1(X0) )
<=> k10_group_5(X0) = X0 )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f25686]) ).
fof(f34870,plain,
! [X0] :
( ( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& v7_group_1(X0)
& l1_group_1(X0) )
<=> k10_group_5(X0) = X0 )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f34869]) ).
fof(f34875,plain,
! [X0] :
( ! [X1] :
( ( v1_group_3(X1,X0)
& m1_group_2(X1,X0) )
| ~ m1_group_2(X1,k10_group_5(X0))
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f25683]) ).
fof(f34876,plain,
! [X0] :
( ! [X1] :
( ( v1_group_3(X1,X0)
& m1_group_2(X1,X0) )
| ~ m1_group_2(X1,k10_group_5(X0))
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f34875]) ).
fof(f34881,plain,
! [X0] :
( v3_realset2(k6_group_6(X0,k6_group_2(X0)))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f26992]) ).
fof(f34882,plain,
! [X0] :
( v3_realset2(k6_group_6(X0,k6_group_2(X0)))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f34881]) ).
fof(f35021,plain,
! [X0] :
( ( ~ v3_struct_0(k3_autgroup(X0))
& v1_group_1(k3_autgroup(X0))
& v3_group_1(k3_autgroup(X0))
& v4_group_1(k3_autgroup(X0))
& l1_group_1(k3_autgroup(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f33387]) ).
fof(f35022,plain,
! [X0] :
( ( ~ v3_struct_0(k3_autgroup(X0))
& v1_group_1(k3_autgroup(X0))
& v3_group_1(k3_autgroup(X0))
& v4_group_1(k3_autgroup(X0))
& l1_group_1(k3_autgroup(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f35021]) ).
fof(f37625,plain,
! [X0] :
( ( v3_realset2(X0)
<=> ! [X1] :
( ! [X2] :
( X1 = X2
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) ) )
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f20339]) ).
fof(f37629,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f18989]) ).
fof(f39310,plain,
! [X0] :
( k6_group_2(X0) = g1_group_1(u1_struct_0(X0),u1_group_1(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f21885]) ).
fof(f39311,plain,
! [X0] :
( k6_group_2(X0) = g1_group_1(u1_struct_0(X0),u1_group_1(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f39310]) ).
fof(f40576,plain,
! [X0] :
( X0 = g1_group_1(u1_struct_0(X0),u1_group_1(X0))
| ~ v1_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f18991]) ).
fof(f40577,plain,
! [X0] :
( X0 = g1_group_1(u1_struct_0(X0),u1_group_1(X0))
| ~ v1_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f40576]) ).
fof(f40899,plain,
( sK222 != k2_group_1(k5_autgroup(sK221))
& m1_subset_1(sK222,u1_struct_0(k5_autgroup(sK221)))
& ~ v3_struct_0(sK221)
& v3_group_1(sK221)
& v4_group_1(sK221)
& v7_group_1(sK221)
& l1_group_1(sK221)
& ~ v3_struct_0(sK221)
& v1_group_1(sK221)
& v3_group_1(sK221)
& v4_group_1(sK221)
& l1_group_1(sK221) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK221,sK222]),skolemize(X0,sK221),skolemize(X1,sK222)],[f33842]) ).
fof(f40944,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k5_autgroup(X0)
| u1_struct_0(X1) != k4_autgroup(X0) )
& ( u1_struct_0(X1) = k4_autgroup(X0)
| k5_autgroup(X0) != X1 ) )
| ~ v1_group_1(X1)
| ~ v1_group_3(X1,k3_autgroup(X0))
| ~ m1_group_2(X1,k3_autgroup(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(nnf_transformation,[],[f33950]) ).
fof(f41247,plain,
! [X0] :
( ( ( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& v7_group_1(X0)
& l1_group_1(X0) )
| k10_group_5(X0) != X0 )
& ( k10_group_5(X0) = X0
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ v7_group_1(X0)
| ~ l1_group_1(X0) ) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(nnf_transformation,[],[f34870]) ).
fof(f41248,plain,
! [X0] :
( ( ( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& v7_group_1(X0)
& l1_group_1(X0) )
| k10_group_5(X0) != X0 )
& ( k10_group_5(X0) = X0
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ v7_group_1(X0)
| ~ l1_group_1(X0) ) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f41247]) ).
fof(f42248,plain,
! [X0] :
( ( ( v3_realset2(X0)
| ? [X1] :
( ? [X2] :
( X1 != X2
& m1_subset_1(X2,u1_struct_0(X0)) )
& m1_subset_1(X1,u1_struct_0(X0)) ) )
& ( ! [X1] :
( ! [X2] :
( X1 = X2
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| ~ v3_realset2(X0) ) )
| ~ l1_struct_0(X0) ),
inference(nnf_transformation,[],[f37625]) ).
fof(f42249,plain,
! [X0] :
( ( ( v3_realset2(X0)
| ? [X1] :
( ? [X2] :
( X1 != X2
& m1_subset_1(X2,u1_struct_0(X0)) )
& m1_subset_1(X1,u1_struct_0(X0)) ) )
& ( ! [X3] :
( ! [X4] :
( X3 = X4
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ v3_realset2(X0) ) )
| ~ l1_struct_0(X0) ),
inference(rectify,[],[f42248]) ).
fof(f42250,plain,
! [X0] :
( ( ( v3_realset2(X0)
| ( sK1152(X0) != sK1153(X0)
& m1_subset_1(sK1153(X0),u1_struct_0(X0))
& m1_subset_1(sK1152(X0),u1_struct_0(X0)) ) )
& ( ! [X3] :
( ! [X4] :
( X3 = X4
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ v3_realset2(X0) ) )
| ~ l1_struct_0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1152,sK1153]),skolemize(X1,sK1152(X0)),skolemize(X2,sK1153(X0))],[f42249]) ).
fof(f42994,plain,
l1_group_1(sK221),
inference(cnf_transformation,[],[f40899]) ).
fof(f42995,plain,
v4_group_1(sK221),
inference(cnf_transformation,[],[f40899]) ).
fof(f42996,plain,
v3_group_1(sK221),
inference(cnf_transformation,[],[f40899]) ).
fof(f42997,plain,
v1_group_1(sK221),
inference(cnf_transformation,[],[f40899]) ).
fof(f42998,plain,
~ v3_struct_0(sK221),
inference(cnf_transformation,[],[f40899]) ).
fof(f43000,plain,
v7_group_1(sK221),
inference(cnf_transformation,[],[f40899]) ).
fof(f43004,plain,
m1_subset_1(sK222,u1_struct_0(k5_autgroup(sK221))),
inference(cnf_transformation,[],[f40899]) ).
fof(f43005,plain,
sK222 != k2_group_1(k5_autgroup(sK221)),
inference(cnf_transformation,[],[f40899]) ).
fof(f43014,plain,
! [X0,X1] :
( ~ m1_group_2(X1,X0)
| l1_group_1(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33850]) ).
fof(f43015,plain,
! [X0,X1] :
( ~ m1_group_2(X1,X0)
| v3_group_1(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33850]) ).
fof(f43016,plain,
! [X0,X1] :
( ~ m1_group_2(X1,X0)
| ~ v3_struct_0(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33850]) ).
fof(f43019,plain,
! [X0] :
( m1_group_2(X0,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33856]) ).
fof(f43021,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(X1))
| m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33860]) ).
fof(f43024,plain,
! [X0,X1] :
( ~ m1_group_2(X1,X0)
| v4_group_1(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33864]) ).
fof(f43185,plain,
! [X2,X0,X1] :
( k1_group_1(X0,X2,X1) != X1
| k2_group_1(X0) = X2
| ~ 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(cnf_transformation,[],[f33932]) ).
fof(f43197,plain,
! [X0] :
( r2_group_6(k5_autgroup(X0),k6_group_6(X0,k10_group_5(X0)))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33942]) ).
fof(f43201,plain,
! [X0,X1] :
( u1_struct_0(X1) = k4_autgroup(X0)
| k5_autgroup(X0) != X1
| ~ v1_group_1(X1)
| ~ v1_group_3(X1,k3_autgroup(X0))
| ~ m1_group_2(X1,k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f40944]) ).
fof(f43203,plain,
! [X0] :
( m1_group_2(k5_autgroup(X0),k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33952]) ).
fof(f43204,plain,
! [X0] :
( v1_group_3(k5_autgroup(X0),k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33952]) ).
fof(f43205,plain,
! [X0] :
( v1_group_1(k5_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33952]) ).
fof(f43271,plain,
! [X2,X3,X0,X1,X4,X5] :
( k1_group_1(X0,X1,X2) = k1_group_1(X3,X4,X5)
| X1 != X4
| X2 != X5
| ~ m1_subset_1(X5,u1_struct_0(X3))
| ~ m1_subset_1(X4,u1_struct_0(X3))
| ~ m1_group_2(X3,X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33993]) ).
fof(f43398,plain,
! [X0,X1] :
( l1_group_1(k6_group_6(X0,X1))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(X1,X0) ),
inference(cnf_transformation,[],[f34087]) ).
fof(f43411,plain,
! [X0,X1] :
( v4_group_1(k6_group_6(X0,X1))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(X1,X0) ),
inference(cnf_transformation,[],[f34099]) ).
fof(f43412,plain,
! [X0,X1] :
( v3_group_1(k6_group_6(X0,X1))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(X1,X0) ),
inference(cnf_transformation,[],[f34099]) ).
fof(f43416,plain,
! [X0,X1] :
( v1_group_1(k6_group_6(X0,X1))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(X1,X0) ),
inference(cnf_transformation,[],[f34101]) ).
fof(f43417,plain,
! [X0,X1] :
( ~ v3_struct_0(k6_group_6(X0,X1))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v1_group_3(X1,X0)
| ~ m1_group_2(X1,X0) ),
inference(cnf_transformation,[],[f34101]) ).
fof(f43658,plain,
! [X2,X0,X1] :
( m1_subset_1(k1_group_1(X0,X1,X2),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f34295]) ).
fof(f44413,plain,
! [X0,X1] :
( ~ r2_group_6(X0,X1)
| r2_group_6(X1,X0)
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X1)
| ~ v1_group_1(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(cnf_transformation,[],[f34850]) ).
fof(f44415,plain,
! [X0,X1] :
( ~ r2_group_6(X0,X1)
| v3_realset2(X1)
| ~ v3_realset2(X0)
| v3_struct_0(X1)
| ~ v1_group_1(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f34854]) ).
fof(f44429,plain,
! [X0] :
( k10_group_5(X0) = X0
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ v7_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f41248]) ).
fof(f44439,plain,
! [X0,X1] :
( ~ m1_group_2(X1,k10_group_5(X0))
| v1_group_3(X1,X0)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f34876]) ).
fof(f44445,plain,
! [X0] :
( v3_realset2(k6_group_6(X0,k6_group_2(X0)))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f34882]) ).
fof(f44629,plain,
! [X0] :
( l1_group_1(k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f35022]) ).
fof(f44630,plain,
! [X0] :
( v4_group_1(k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f35022]) ).
fof(f44631,plain,
! [X0] :
( v3_group_1(k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f35022]) ).
fof(f44633,plain,
! [X0] :
( ~ v3_struct_0(k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f35022]) ).
fof(f48513,plain,
! [X3,X0,X4] :
( ~ m1_subset_1(X4,u1_struct_0(X0))
| X3 = X4
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ v3_realset2(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f42250]) ).
fof(f48524,plain,
! [X0] :
( ~ l1_group_1(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f37629]) ).
fof(f50468,plain,
! [X0] :
( ~ v4_group_1(X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| g1_group_1(u1_struct_0(X0),u1_group_1(X0)) = k6_group_2(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f39311]) ).
fof(f52036,plain,
! [X0] :
( ~ v1_group_1(X0)
| g1_group_1(u1_struct_0(X0),u1_group_1(X0)) = X0
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f40577]) ).
fof(f53170,plain,
! [X0] :
( k4_autgroup(X0) = u1_struct_0(k5_autgroup(X0))
| ~ v1_group_1(k5_autgroup(X0))
| ~ v1_group_3(k5_autgroup(X0),k3_autgroup(X0))
| ~ m1_group_2(k5_autgroup(X0),k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f43201]) ).
fof(f53175,plain,
! [X2,X3,X0,X4,X5] :
( k1_group_1(X3,X4,X5) = k1_group_1(X0,X4,X2)
| X2 != X5
| ~ m1_subset_1(X5,u1_struct_0(X3))
| ~ m1_subset_1(X4,u1_struct_0(X3))
| ~ m1_group_2(X3,X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f43271]) ).
fof(f53176,plain,
! [X3,X0,X4,X5] :
( ~ m1_subset_1(X5,u1_struct_0(X3))
| k1_group_1(X3,X4,X5) = k1_group_1(X0,X4,X5)
| ~ m1_subset_1(X4,u1_struct_0(X3))
| ~ m1_group_2(X3,X0)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f53175]) ).
fof(f54043,plain,
! [X0] :
( ~ v7_group_1(X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| k10_group_5(X0) = X0
| ~ l1_group_1(X0)
| ~ v1_group_1(X0) ),
inference(duplicate_literal_removal,[],[f44429]) ).
fof(f54656,plain,
! [X0] :
( k4_autgroup(X0) = u1_struct_0(k5_autgroup(X0))
| ~ v1_group_3(k5_autgroup(X0),k3_autgroup(X0))
| ~ m1_group_2(k5_autgroup(X0),k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f53170,f43205]) ).
fof(f54766,plain,
! [X0] :
( k4_autgroup(X0) = u1_struct_0(k5_autgroup(X0))
| ~ m1_group_2(k5_autgroup(X0),k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f54656,f43204]) ).
fof(f54810,plain,
! [X0] :
( ~ v4_group_1(X0)
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| k4_autgroup(X0) = u1_struct_0(k5_autgroup(X0))
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f54766,f43203]) ).
fof(f54842,plain,
! [X0] :
( ~ m1_group_2(k5_autgroup(sK221),X0)
| m1_subset_1(sK222,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(resolution,[],[f43021,f43004]) ).
fof(f54849,plain,
! [X0] :
( ~ v3_struct_0(k5_autgroup(X0))
| v3_struct_0(k3_autgroup(X0))
| ~ v3_group_1(k3_autgroup(X0))
| ~ l1_group_1(k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(resolution,[],[f43016,f43203]) ).
fof(f54873,plain,
( v3_struct_0(sK221)
| ~ v1_group_1(sK221)
| ~ v3_group_1(sK221)
| u1_struct_0(k5_autgroup(sK221)) = k4_autgroup(sK221)
| ~ l1_group_1(sK221) ),
inference(resolution,[],[f54810,f42995]) ).
fof(f54886,plain,
! [X0] :
( v3_group_1(k5_autgroup(X0))
| v3_struct_0(k3_autgroup(X0))
| ~ v3_group_1(k3_autgroup(X0))
| ~ l1_group_1(k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(resolution,[],[f43015,f43203]) ).
fof(f54908,plain,
! [X0] :
( l1_group_1(k5_autgroup(X0))
| v3_struct_0(k3_autgroup(X0))
| ~ v3_group_1(k3_autgroup(X0))
| ~ l1_group_1(k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(resolution,[],[f43014,f43203]) ).
fof(f54937,plain,
! [X0] :
( v4_group_1(k5_autgroup(X0))
| v3_struct_0(k3_autgroup(X0))
| ~ v3_group_1(k3_autgroup(X0))
| ~ v4_group_1(k3_autgroup(X0))
| ~ l1_group_1(k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(resolution,[],[f43024,f43203]) ).
fof(f54959,plain,
( v3_struct_0(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| sK221 = k10_group_5(sK221)
| ~ l1_group_1(sK221)
| ~ v1_group_1(sK221) ),
inference(resolution,[],[f54043,f43000]) ).
fof(f54990,plain,
( ~ v1_group_1(sK221)
| ~ v3_group_1(sK221)
| u1_struct_0(k5_autgroup(sK221)) = k4_autgroup(sK221)
| ~ l1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f54873,f42998]) ).
fof(f55003,plain,
( ~ v3_group_1(sK221)
| u1_struct_0(k5_autgroup(sK221)) = k4_autgroup(sK221)
| ~ l1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f54990,f42997]) ).
fof(f55012,plain,
( u1_struct_0(k5_autgroup(sK221)) = k4_autgroup(sK221)
| ~ l1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f55003,f42996]) ).
fof(f55018,plain,
u1_struct_0(k5_autgroup(sK221)) = k4_autgroup(sK221),
inference(forward_subsumption_resolution,[],[f55012,f42994]) ).
fof(f55026,definition,
( spl1552_78
<=> l1_group_1(k5_autgroup(sK221)) ),
introduced(definition,[new_symbols(definition,[spl1552_78])],[avatar_definition]) ).
fof(f55027,plain,
( l1_group_1(k5_autgroup(sK221))
| ~ spl1552_78 ),
inference(avatar_component_clause,[],[f55026]) ).
fof(f55028,plain,
( ~ l1_group_1(k5_autgroup(sK221))
| spl1552_78 ),
inference(avatar_component_clause,[],[f55026]) ).
fof(f55030,definition,
( spl1552_79
<=> v4_group_1(k5_autgroup(sK221)) ),
introduced(definition,[new_symbols(definition,[spl1552_79])],[avatar_definition]) ).
fof(f55031,plain,
( v4_group_1(k5_autgroup(sK221))
| ~ spl1552_79 ),
inference(avatar_component_clause,[],[f55030]) ).
fof(f55032,plain,
( ~ v4_group_1(k5_autgroup(sK221))
| spl1552_79 ),
inference(avatar_component_clause,[],[f55030]) ).
fof(f55034,definition,
( spl1552_80
<=> v3_group_1(k5_autgroup(sK221)) ),
introduced(definition,[new_symbols(definition,[spl1552_80])],[avatar_definition]) ).
fof(f55035,plain,
( v3_group_1(k5_autgroup(sK221))
| ~ spl1552_80 ),
inference(avatar_component_clause,[],[f55034]) ).
fof(f55036,plain,
( ~ v3_group_1(k5_autgroup(sK221))
| spl1552_80 ),
inference(avatar_component_clause,[],[f55034]) ).
fof(f55038,definition,
( spl1552_81
<=> v3_struct_0(k5_autgroup(sK221)) ),
introduced(definition,[new_symbols(definition,[spl1552_81])],[avatar_definition]) ).
fof(f55039,plain,
( ~ v3_struct_0(k5_autgroup(sK221))
| spl1552_81 ),
inference(avatar_component_clause,[],[f55038]) ).
fof(f55040,plain,
( v3_struct_0(k5_autgroup(sK221))
| ~ spl1552_81 ),
inference(avatar_component_clause,[],[f55038]) ).
fof(f55064,plain,
m1_subset_1(sK222,k4_autgroup(sK221)),
inference(superposition,[],[f43004,f55018]) ).
fof(f55098,definition,
( spl1552_84
<=> l1_struct_0(k5_autgroup(sK221)) ),
introduced(definition,[new_symbols(definition,[spl1552_84])],[avatar_definition]) ).
fof(f55099,plain,
( l1_struct_0(k5_autgroup(sK221))
| ~ spl1552_84 ),
inference(avatar_component_clause,[],[f55098]) ).
fof(f55100,plain,
( ~ l1_struct_0(k5_autgroup(sK221))
| spl1552_84 ),
inference(avatar_component_clause,[],[f55098]) ).
fof(f55177,plain,
! [X0] :
( ~ v3_struct_0(k5_autgroup(X0))
| ~ v3_group_1(k3_autgroup(X0))
| ~ l1_group_1(k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f54849,f44633]) ).
fof(f55183,plain,
! [X0] :
( v3_group_1(k5_autgroup(X0))
| ~ v3_group_1(k3_autgroup(X0))
| ~ l1_group_1(k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f54886,f44633]) ).
fof(f55187,plain,
! [X0] :
( l1_group_1(k5_autgroup(X0))
| ~ v3_group_1(k3_autgroup(X0))
| ~ l1_group_1(k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f54908,f44633]) ).
fof(f55195,plain,
! [X0] :
( v4_group_1(k5_autgroup(X0))
| ~ v3_group_1(k3_autgroup(X0))
| ~ v4_group_1(k3_autgroup(X0))
| ~ l1_group_1(k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f54937,f44633]) ).
fof(f55197,plain,
( ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| sK221 = k10_group_5(sK221)
| ~ l1_group_1(sK221)
| ~ v1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f54959,f42998]) ).
fof(f55204,definition,
( spl1552_95
<=> v1_group_1(k5_autgroup(sK221)) ),
introduced(definition,[new_symbols(definition,[spl1552_95])],[avatar_definition]) ).
fof(f55205,plain,
( v1_group_1(k5_autgroup(sK221))
| ~ spl1552_95 ),
inference(avatar_component_clause,[],[f55204]) ).
fof(f55206,plain,
( ~ v1_group_1(k5_autgroup(sK221))
| spl1552_95 ),
inference(avatar_component_clause,[],[f55204]) ).
fof(f55224,plain,
! [X0] :
( ~ v3_struct_0(k5_autgroup(X0))
| ~ l1_group_1(k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f55177,f44631]) ).
fof(f55229,plain,
! [X0] :
( v3_group_1(k5_autgroup(X0))
| ~ l1_group_1(k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f55183,f44631]) ).
fof(f55230,plain,
! [X0] :
( l1_group_1(k5_autgroup(X0))
| ~ l1_group_1(k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f55187,f44631]) ).
fof(f55237,plain,
! [X0] :
( v4_group_1(k5_autgroup(X0))
| ~ v4_group_1(k3_autgroup(X0))
| ~ l1_group_1(k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f55195,f44631]) ).
fof(f55238,plain,
( ~ v4_group_1(sK221)
| sK221 = k10_group_5(sK221)
| ~ l1_group_1(sK221)
| ~ v1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f55197,f42996]) ).
fof(f55248,plain,
! [X0] :
( ~ v3_struct_0(k5_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f55224,f44629]) ).
fof(f55253,plain,
! [X0] :
( v3_group_1(k5_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f55229,f44629]) ).
fof(f55254,plain,
! [X0] :
( l1_group_1(k5_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f55230,f44629]) ).
fof(f55260,plain,
! [X0] :
( v4_group_1(k5_autgroup(X0))
| ~ l1_group_1(k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f55237,f44630]) ).
fof(f55261,plain,
( sK221 = k10_group_5(sK221)
| ~ l1_group_1(sK221)
| ~ v1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f55238,f42995]) ).
fof(f55272,plain,
! [X0] :
( v4_group_1(k5_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f55260,f44629]) ).
fof(f55273,plain,
( sK221 = k10_group_5(sK221)
| ~ v1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f55261,f42994]) ).
fof(f55276,plain,
sK221 = k10_group_5(sK221),
inference(forward_subsumption_resolution,[],[f55273,f42997]) ).
fof(f55314,plain,
! [X0] :
( ~ m1_group_2(X0,sK221)
| v1_group_3(X0,sK221)
| ~ m1_group_2(X0,sK221)
| v3_struct_0(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221) ),
inference(superposition,[],[f44439,f55276]) ).
fof(f55315,plain,
( r2_group_6(k5_autgroup(sK221),k6_group_6(sK221,sK221))
| v3_struct_0(sK221)
| ~ v1_group_1(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221) ),
inference(superposition,[],[f43197,f55276]) ).
fof(f55316,plain,
! [X0] :
( ~ m1_group_2(X0,sK221)
| v1_group_3(X0,sK221)
| v3_struct_0(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221) ),
inference(duplicate_literal_removal,[],[f55314]) ).
fof(f55317,plain,
( r2_group_6(k5_autgroup(sK221),k6_group_6(sK221,sK221))
| ~ v1_group_1(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f55315,f42998]) ).
fof(f55318,plain,
! [X0] :
( ~ m1_group_2(X0,sK221)
| v1_group_3(X0,sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f55316,f42998]) ).
fof(f55319,plain,
( r2_group_6(k5_autgroup(sK221),k6_group_6(sK221,sK221))
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f55317,f42997]) ).
fof(f55320,plain,
! [X0] :
( ~ m1_group_2(X0,sK221)
| v1_group_3(X0,sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f55318,f42996]) ).
fof(f55321,plain,
( r2_group_6(k5_autgroup(sK221),k6_group_6(sK221,sK221))
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f55319,f42996]) ).
fof(f55322,plain,
! [X0] :
( ~ m1_group_2(X0,sK221)
| v1_group_3(X0,sK221)
| ~ l1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f55320,f42995]) ).
fof(f55323,plain,
( r2_group_6(k5_autgroup(sK221),k6_group_6(sK221,sK221))
| ~ l1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f55321,f42995]) ).
fof(f55324,plain,
! [X0] :
( ~ m1_group_2(X0,sK221)
| v1_group_3(X0,sK221) ),
inference(forward_subsumption_resolution,[],[f55322,f42994]) ).
fof(f55325,plain,
r2_group_6(k5_autgroup(sK221),k6_group_6(sK221,sK221)),
inference(forward_subsumption_resolution,[],[f55323,f42994]) ).
fof(f55337,plain,
( v3_struct_0(sK221)
| ~ v1_group_1(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| spl1552_95 ),
inference(resolution,[],[f55206,f43205]) ).
fof(f55338,plain,
( ~ v1_group_1(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| spl1552_95 ),
inference(forward_subsumption_resolution,[],[f55337,f42998]) ).
fof(f55339,plain,
( ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| spl1552_95 ),
inference(forward_subsumption_resolution,[],[f55338,f42997]) ).
fof(f55340,plain,
( ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| spl1552_95 ),
inference(forward_subsumption_resolution,[],[f55339,f42996]) ).
fof(f55341,plain,
( ~ l1_group_1(sK221)
| spl1552_95 ),
inference(forward_subsumption_resolution,[],[f55340,f42995]) ).
fof(f55342,plain,
( $false
| spl1552_95 ),
inference(forward_subsumption_resolution,[],[f55341,f42994]) ).
fof(f55343,plain,
spl1552_95,
inference(avatar_contradiction_clause,[],[f55342]) ).
fof(f55406,plain,
( r2_group_6(k6_group_6(sK221,sK221),k5_autgroup(sK221))
| v3_struct_0(k5_autgroup(sK221))
| ~ v1_group_1(k5_autgroup(sK221))
| ~ v3_group_1(k5_autgroup(sK221))
| ~ v4_group_1(k5_autgroup(sK221))
| ~ l1_group_1(k5_autgroup(sK221))
| v3_struct_0(k6_group_6(sK221,sK221))
| ~ v1_group_1(k6_group_6(sK221,sK221))
| ~ v3_group_1(k6_group_6(sK221,sK221))
| ~ v4_group_1(k6_group_6(sK221,sK221))
| ~ l1_group_1(k6_group_6(sK221,sK221)) ),
inference(resolution,[],[f55325,f44413]) ).
fof(f55414,plain,
( v1_group_3(sK221,sK221)
| v3_struct_0(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221) ),
inference(resolution,[],[f55324,f43019]) ).
fof(f55415,plain,
( v1_group_3(sK221,sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f55414,f42998]) ).
fof(f55416,plain,
( v1_group_3(sK221,sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f55415,f42996]) ).
fof(f55417,plain,
( v1_group_3(sK221,sK221)
| ~ l1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f55416,f42995]) ).
fof(f55418,plain,
v1_group_3(sK221,sK221),
inference(forward_subsumption_resolution,[],[f55417,f42994]) ).
fof(f55419,plain,
( v3_struct_0(sK221)
| ~ v1_group_1(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| spl1552_78 ),
inference(resolution,[],[f55254,f55028]) ).
fof(f55421,plain,
( ~ v1_group_1(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| spl1552_78 ),
inference(forward_subsumption_resolution,[],[f55419,f42998]) ).
fof(f55422,plain,
( ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| spl1552_78 ),
inference(forward_subsumption_resolution,[],[f55421,f42997]) ).
fof(f55423,plain,
( ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| spl1552_78 ),
inference(forward_subsumption_resolution,[],[f55422,f42996]) ).
fof(f55424,plain,
( ~ l1_group_1(sK221)
| spl1552_78 ),
inference(forward_subsumption_resolution,[],[f55423,f42995]) ).
fof(f55425,plain,
( $false
| spl1552_78 ),
inference(forward_subsumption_resolution,[],[f55424,f42994]) ).
fof(f55426,plain,
spl1552_78,
inference(avatar_contradiction_clause,[],[f55425]) ).
fof(f55438,plain,
( v3_struct_0(sK221)
| ~ v1_group_1(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| ~ spl1552_81 ),
inference(resolution,[],[f55040,f55248]) ).
fof(f55439,plain,
( ~ v1_group_1(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| ~ spl1552_81 ),
inference(forward_subsumption_resolution,[],[f55438,f42998]) ).
fof(f55440,plain,
( ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| ~ spl1552_81 ),
inference(forward_subsumption_resolution,[],[f55439,f42997]) ).
fof(f55441,plain,
( ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| ~ spl1552_81 ),
inference(forward_subsumption_resolution,[],[f55440,f42996]) ).
fof(f55442,plain,
( ~ l1_group_1(sK221)
| ~ spl1552_81 ),
inference(forward_subsumption_resolution,[],[f55441,f42995]) ).
fof(f55443,plain,
( $false
| ~ spl1552_81 ),
inference(forward_subsumption_resolution,[],[f55442,f42994]) ).
fof(f55444,plain,
~ spl1552_81,
inference(avatar_contradiction_clause,[],[f55443]) ).
fof(f55445,plain,
( l1_struct_0(k5_autgroup(sK221))
| ~ spl1552_78 ),
inference(resolution,[],[f55027,f48524]) ).
fof(f55446,plain,
( $false
| ~ spl1552_78
| spl1552_84 ),
inference(forward_subsumption_resolution,[],[f55445,f55100]) ).
fof(f55447,plain,
( ~ spl1552_78
| spl1552_84 ),
inference(avatar_contradiction_clause,[],[f55446]) ).
fof(f55450,plain,
( v3_struct_0(sK221)
| ~ v1_group_1(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| spl1552_79 ),
inference(resolution,[],[f55272,f55032]) ).
fof(f55459,plain,
( ~ v1_group_1(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| spl1552_79 ),
inference(forward_subsumption_resolution,[],[f55450,f42998]) ).
fof(f55464,plain,
( ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| spl1552_79 ),
inference(forward_subsumption_resolution,[],[f55459,f42997]) ).
fof(f55469,plain,
( ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| spl1552_79 ),
inference(forward_subsumption_resolution,[],[f55464,f42996]) ).
fof(f55473,plain,
( ~ l1_group_1(sK221)
| spl1552_79 ),
inference(forward_subsumption_resolution,[],[f55469,f42995]) ).
fof(f55474,plain,
( $false
| spl1552_79 ),
inference(forward_subsumption_resolution,[],[f55473,f42994]) ).
fof(f55475,plain,
spl1552_79,
inference(avatar_contradiction_clause,[],[f55474]) ).
fof(f55480,plain,
( v3_struct_0(sK221)
| ~ v1_group_1(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| spl1552_80 ),
inference(resolution,[],[f55036,f55253]) ).
fof(f55481,plain,
( ~ v1_group_1(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| spl1552_80 ),
inference(forward_subsumption_resolution,[],[f55480,f42998]) ).
fof(f55482,plain,
( ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| spl1552_80 ),
inference(forward_subsumption_resolution,[],[f55481,f42997]) ).
fof(f55483,plain,
( ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| spl1552_80 ),
inference(forward_subsumption_resolution,[],[f55482,f42996]) ).
fof(f55484,plain,
( ~ l1_group_1(sK221)
| spl1552_80 ),
inference(forward_subsumption_resolution,[],[f55483,f42995]) ).
fof(f55485,plain,
( $false
| spl1552_80 ),
inference(forward_subsumption_resolution,[],[f55484,f42994]) ).
fof(f55486,plain,
spl1552_80,
inference(avatar_contradiction_clause,[],[f55485]) ).
fof(f55519,plain,
( r2_group_6(k6_group_6(sK221,sK221),k5_autgroup(sK221))
| ~ v1_group_1(k5_autgroup(sK221))
| ~ v3_group_1(k5_autgroup(sK221))
| ~ v4_group_1(k5_autgroup(sK221))
| ~ l1_group_1(k5_autgroup(sK221))
| v3_struct_0(k6_group_6(sK221,sK221))
| ~ v1_group_1(k6_group_6(sK221,sK221))
| ~ v3_group_1(k6_group_6(sK221,sK221))
| ~ v4_group_1(k6_group_6(sK221,sK221))
| ~ l1_group_1(k6_group_6(sK221,sK221))
| spl1552_81 ),
inference(forward_subsumption_resolution,[],[f55406,f55039]) ).
fof(f55555,plain,
( r2_group_6(k6_group_6(sK221,sK221),k5_autgroup(sK221))
| ~ v3_group_1(k5_autgroup(sK221))
| ~ v4_group_1(k5_autgroup(sK221))
| ~ l1_group_1(k5_autgroup(sK221))
| v3_struct_0(k6_group_6(sK221,sK221))
| ~ v1_group_1(k6_group_6(sK221,sK221))
| ~ v3_group_1(k6_group_6(sK221,sK221))
| ~ v4_group_1(k6_group_6(sK221,sK221))
| ~ l1_group_1(k6_group_6(sK221,sK221))
| spl1552_81
| ~ spl1552_95 ),
inference(forward_subsumption_resolution,[],[f55519,f55205]) ).
fof(f55591,plain,
( r2_group_6(k6_group_6(sK221,sK221),k5_autgroup(sK221))
| ~ v4_group_1(k5_autgroup(sK221))
| ~ l1_group_1(k5_autgroup(sK221))
| v3_struct_0(k6_group_6(sK221,sK221))
| ~ v1_group_1(k6_group_6(sK221,sK221))
| ~ v3_group_1(k6_group_6(sK221,sK221))
| ~ v4_group_1(k6_group_6(sK221,sK221))
| ~ l1_group_1(k6_group_6(sK221,sK221))
| ~ spl1552_80
| spl1552_81
| ~ spl1552_95 ),
inference(forward_subsumption_resolution,[],[f55555,f55035]) ).
fof(f55627,plain,
( r2_group_6(k6_group_6(sK221,sK221),k5_autgroup(sK221))
| ~ l1_group_1(k5_autgroup(sK221))
| v3_struct_0(k6_group_6(sK221,sK221))
| ~ v1_group_1(k6_group_6(sK221,sK221))
| ~ v3_group_1(k6_group_6(sK221,sK221))
| ~ v4_group_1(k6_group_6(sK221,sK221))
| ~ l1_group_1(k6_group_6(sK221,sK221))
| ~ spl1552_79
| ~ spl1552_80
| spl1552_81
| ~ spl1552_95 ),
inference(forward_subsumption_resolution,[],[f55591,f55031]) ).
fof(f55658,plain,
( r2_group_6(k6_group_6(sK221,sK221),k5_autgroup(sK221))
| v3_struct_0(k6_group_6(sK221,sK221))
| ~ v1_group_1(k6_group_6(sK221,sK221))
| ~ v3_group_1(k6_group_6(sK221,sK221))
| ~ v4_group_1(k6_group_6(sK221,sK221))
| ~ l1_group_1(k6_group_6(sK221,sK221))
| ~ spl1552_78
| ~ spl1552_79
| ~ spl1552_80
| spl1552_81
| ~ spl1552_95 ),
inference(forward_subsumption_resolution,[],[f55627,f55027]) ).
fof(f55674,definition,
( spl1552_103
<=> l1_group_1(k6_group_6(sK221,sK221)) ),
introduced(definition,[new_symbols(definition,[spl1552_103])],[avatar_definition]) ).
fof(f55675,plain,
( l1_group_1(k6_group_6(sK221,sK221))
| ~ spl1552_103 ),
inference(avatar_component_clause,[],[f55674]) ).
fof(f55676,plain,
( ~ l1_group_1(k6_group_6(sK221,sK221))
| spl1552_103 ),
inference(avatar_component_clause,[],[f55674]) ).
fof(f55678,definition,
( spl1552_104
<=> v4_group_1(k6_group_6(sK221,sK221)) ),
introduced(definition,[new_symbols(definition,[spl1552_104])],[avatar_definition]) ).
fof(f55679,plain,
( v4_group_1(k6_group_6(sK221,sK221))
| ~ spl1552_104 ),
inference(avatar_component_clause,[],[f55678]) ).
fof(f55680,plain,
( ~ v4_group_1(k6_group_6(sK221,sK221))
| spl1552_104 ),
inference(avatar_component_clause,[],[f55678]) ).
fof(f55682,definition,
( spl1552_105
<=> v3_group_1(k6_group_6(sK221,sK221)) ),
introduced(definition,[new_symbols(definition,[spl1552_105])],[avatar_definition]) ).
fof(f55683,plain,
( v3_group_1(k6_group_6(sK221,sK221))
| ~ spl1552_105 ),
inference(avatar_component_clause,[],[f55682]) ).
fof(f55684,plain,
( ~ v3_group_1(k6_group_6(sK221,sK221))
| spl1552_105 ),
inference(avatar_component_clause,[],[f55682]) ).
fof(f55686,definition,
( spl1552_106
<=> v1_group_1(k6_group_6(sK221,sK221)) ),
introduced(definition,[new_symbols(definition,[spl1552_106])],[avatar_definition]) ).
fof(f55687,plain,
( v1_group_1(k6_group_6(sK221,sK221))
| ~ spl1552_106 ),
inference(avatar_component_clause,[],[f55686]) ).
fof(f55688,plain,
( ~ v1_group_1(k6_group_6(sK221,sK221))
| spl1552_106 ),
inference(avatar_component_clause,[],[f55686]) ).
fof(f55690,definition,
( spl1552_107
<=> v3_struct_0(k6_group_6(sK221,sK221)) ),
introduced(definition,[new_symbols(definition,[spl1552_107])],[avatar_definition]) ).
fof(f55691,plain,
( ~ v3_struct_0(k6_group_6(sK221,sK221))
| spl1552_107 ),
inference(avatar_component_clause,[],[f55690]) ).
fof(f55692,plain,
( v3_struct_0(k6_group_6(sK221,sK221))
| ~ spl1552_107 ),
inference(avatar_component_clause,[],[f55690]) ).
fof(f55694,definition,
( spl1552_108
<=> r2_group_6(k6_group_6(sK221,sK221),k5_autgroup(sK221)) ),
introduced(definition,[new_symbols(definition,[spl1552_108])],[avatar_definition]) ).
fof(f55696,plain,
( r2_group_6(k6_group_6(sK221,sK221),k5_autgroup(sK221))
| ~ spl1552_108 ),
inference(avatar_component_clause,[],[f55694]) ).
fof(f55697,plain,
( ~ spl1552_103
| ~ spl1552_104
| ~ spl1552_105
| ~ spl1552_106
| spl1552_107
| spl1552_108
| ~ spl1552_78
| ~ spl1552_79
| ~ spl1552_80
| spl1552_81
| ~ spl1552_95 ),
inference(avatar_split_clause,[],[f55658,f55204,f55038,f55034,f55030,f55026,f55694,f55690,f55686,f55682,f55678,f55674]) ).
fof(f56770,plain,
! [X0] :
( sK222 = X0
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK221)))
| ~ v3_realset2(k5_autgroup(sK221))
| ~ l1_struct_0(k5_autgroup(sK221)) ),
inference(resolution,[],[f48513,f43004]) ).
fof(f56777,plain,
( ! [X0] :
( sK222 = X0
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK221)))
| ~ v3_realset2(k5_autgroup(sK221)) )
| ~ spl1552_84 ),
inference(forward_subsumption_resolution,[],[f56770,f55099]) ).
fof(f56784,definition,
( spl1552_167
<=> v3_realset2(k5_autgroup(sK221)) ),
introduced(definition,[new_symbols(definition,[spl1552_167])],[avatar_definition]) ).
fof(f56786,plain,
( ~ v3_realset2(k5_autgroup(sK221))
| spl1552_167 ),
inference(avatar_component_clause,[],[f56784]) ).
fof(f56799,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK221))
| sK222 = X0
| ~ v3_realset2(k5_autgroup(sK221)) )
| ~ spl1552_84 ),
inference(forward_demodulation,[],[f56777,f55018]) ).
fof(f56817,definition,
( spl1552_175
<=> ! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK221))
| sK222 = X0 ) ),
introduced(definition,[new_symbols(definition,[spl1552_175])],[avatar_definition]) ).
fof(f56818,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK221))
| sK222 = X0 )
| ~ spl1552_175 ),
inference(avatar_component_clause,[],[f56817]) ).
fof(f56819,plain,
( ~ spl1552_167
| spl1552_175
| ~ spl1552_84 ),
inference(avatar_split_clause,[],[f56799,f55098,f56817,f56784]) ).
fof(f57242,plain,
( v3_struct_0(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| ~ v1_group_3(sK221,sK221)
| ~ m1_group_2(sK221,sK221)
| spl1552_103 ),
inference(resolution,[],[f55676,f43398]) ).
fof(f57243,plain,
( v3_struct_0(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| ~ v1_group_3(sK221,sK221)
| spl1552_103 ),
inference(forward_subsumption_resolution,[],[f57242,f43019]) ).
fof(f57244,plain,
( ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| ~ v1_group_3(sK221,sK221)
| spl1552_103 ),
inference(forward_subsumption_resolution,[],[f57243,f42998]) ).
fof(f57245,plain,
( ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| ~ v1_group_3(sK221,sK221)
| spl1552_103 ),
inference(forward_subsumption_resolution,[],[f57244,f42996]) ).
fof(f57246,plain,
( ~ l1_group_1(sK221)
| ~ v1_group_3(sK221,sK221)
| spl1552_103 ),
inference(forward_subsumption_resolution,[],[f57245,f42995]) ).
fof(f57247,plain,
( ~ v1_group_3(sK221,sK221)
| spl1552_103 ),
inference(forward_subsumption_resolution,[],[f57246,f42994]) ).
fof(f57248,plain,
( $false
| spl1552_103 ),
inference(forward_subsumption_resolution,[],[f57247,f55418]) ).
fof(f57249,plain,
spl1552_103,
inference(avatar_contradiction_clause,[],[f57248]) ).
fof(f57250,plain,
( v3_struct_0(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| ~ v1_group_3(sK221,sK221)
| ~ m1_group_2(sK221,sK221)
| ~ spl1552_107 ),
inference(resolution,[],[f55692,f43417]) ).
fof(f57251,plain,
( v3_struct_0(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| ~ v1_group_3(sK221,sK221)
| ~ spl1552_107 ),
inference(forward_subsumption_resolution,[],[f57250,f43019]) ).
fof(f57252,plain,
( ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| ~ v1_group_3(sK221,sK221)
| ~ spl1552_107 ),
inference(forward_subsumption_resolution,[],[f57251,f42998]) ).
fof(f57253,plain,
( ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| ~ v1_group_3(sK221,sK221)
| ~ spl1552_107 ),
inference(forward_subsumption_resolution,[],[f57252,f42996]) ).
fof(f57254,plain,
( ~ l1_group_1(sK221)
| ~ v1_group_3(sK221,sK221)
| ~ spl1552_107 ),
inference(forward_subsumption_resolution,[],[f57253,f42995]) ).
fof(f57255,plain,
( ~ v1_group_3(sK221,sK221)
| ~ spl1552_107 ),
inference(forward_subsumption_resolution,[],[f57254,f42994]) ).
fof(f57256,plain,
( $false
| ~ spl1552_107 ),
inference(forward_subsumption_resolution,[],[f57255,f55418]) ).
fof(f57257,plain,
~ spl1552_107,
inference(avatar_contradiction_clause,[],[f57256]) ).
fof(f57285,definition,
( spl1552_192
<=> v3_realset2(k6_group_6(sK221,sK221)) ),
introduced(definition,[new_symbols(definition,[spl1552_192])],[avatar_definition]) ).
fof(f57286,plain,
( v3_realset2(k6_group_6(sK221,sK221))
| ~ spl1552_192 ),
inference(avatar_component_clause,[],[f57285]) ).
fof(f57287,plain,
( ~ v3_realset2(k6_group_6(sK221,sK221))
| spl1552_192 ),
inference(avatar_component_clause,[],[f57285]) ).
fof(f57311,plain,
( v3_struct_0(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| ~ v1_group_3(sK221,sK221)
| ~ m1_group_2(sK221,sK221)
| spl1552_105 ),
inference(resolution,[],[f55684,f43412]) ).
fof(f57312,plain,
( v3_struct_0(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| ~ v1_group_3(sK221,sK221)
| spl1552_105 ),
inference(forward_subsumption_resolution,[],[f57311,f43019]) ).
fof(f57313,plain,
( ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| ~ v1_group_3(sK221,sK221)
| spl1552_105 ),
inference(forward_subsumption_resolution,[],[f57312,f42998]) ).
fof(f57314,plain,
( ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| ~ v1_group_3(sK221,sK221)
| spl1552_105 ),
inference(forward_subsumption_resolution,[],[f57313,f42996]) ).
fof(f57315,plain,
( ~ l1_group_1(sK221)
| ~ v1_group_3(sK221,sK221)
| spl1552_105 ),
inference(forward_subsumption_resolution,[],[f57314,f42995]) ).
fof(f57316,plain,
( ~ v1_group_3(sK221,sK221)
| spl1552_105 ),
inference(forward_subsumption_resolution,[],[f57315,f42994]) ).
fof(f57317,plain,
( $false
| spl1552_105 ),
inference(forward_subsumption_resolution,[],[f57316,f55418]) ).
fof(f57318,plain,
spl1552_105,
inference(avatar_contradiction_clause,[],[f57317]) ).
fof(f57467,plain,
! [X0,X1] :
( k1_group_1(k5_autgroup(sK221),X0,sK222) = k1_group_1(X1,X0,sK222)
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK221)))
| ~ m1_group_2(k5_autgroup(sK221),X1)
| ~ m1_subset_1(sK222,u1_struct_0(X1))
| ~ m1_subset_1(X0,u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ l1_group_1(X1) ),
inference(resolution,[],[f53176,f43004]) ).
fof(f57476,plain,
! [X0,X1] :
( k1_group_1(k5_autgroup(sK221),X0,sK222) = k1_group_1(X1,X0,sK222)
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK221)))
| ~ m1_group_2(k5_autgroup(sK221),X1)
| ~ m1_subset_1(sK222,u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ l1_group_1(X1) ),
inference(forward_subsumption_resolution,[],[f57467,f43021]) ).
fof(f57487,plain,
! [X0,X1] :
( k1_group_1(k5_autgroup(sK221),X0,sK222) = k1_group_1(X1,X0,sK222)
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK221)))
| ~ m1_group_2(k5_autgroup(sK221),X1)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ l1_group_1(X1) ),
inference(forward_subsumption_resolution,[],[f57476,f54842]) ).
fof(f57494,plain,
! [X0,X1] :
( ~ m1_group_2(k5_autgroup(sK221),X1)
| k1_group_1(k5_autgroup(sK221),X0,sK222) = k1_group_1(X1,X0,sK222)
| ~ m1_subset_1(X0,k4_autgroup(sK221))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ l1_group_1(X1) ),
inference(forward_demodulation,[],[f57487,f55018]) ).
fof(f57500,plain,
! [X0] :
( k1_group_1(k5_autgroup(sK221),X0,sK222) = k1_group_1(k3_autgroup(sK221),X0,sK222)
| ~ m1_subset_1(X0,k4_autgroup(sK221))
| v3_struct_0(k3_autgroup(sK221))
| ~ v3_group_1(k3_autgroup(sK221))
| ~ l1_group_1(k3_autgroup(sK221))
| v3_struct_0(sK221)
| ~ v1_group_1(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221) ),
inference(resolution,[],[f57494,f43203]) ).
fof(f57506,plain,
! [X0] :
( k1_group_1(k5_autgroup(sK221),X0,sK222) = k1_group_1(k3_autgroup(sK221),X0,sK222)
| ~ m1_subset_1(X0,k4_autgroup(sK221))
| ~ v3_group_1(k3_autgroup(sK221))
| ~ l1_group_1(k3_autgroup(sK221))
| v3_struct_0(sK221)
| ~ v1_group_1(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f57500,f44633]) ).
fof(f57508,plain,
! [X0] :
( k1_group_1(k5_autgroup(sK221),X0,sK222) = k1_group_1(k3_autgroup(sK221),X0,sK222)
| ~ m1_subset_1(X0,k4_autgroup(sK221))
| ~ l1_group_1(k3_autgroup(sK221))
| v3_struct_0(sK221)
| ~ v1_group_1(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f57506,f44631]) ).
fof(f57509,plain,
! [X0] :
( k1_group_1(k5_autgroup(sK221),X0,sK222) = k1_group_1(k3_autgroup(sK221),X0,sK222)
| ~ m1_subset_1(X0,k4_autgroup(sK221))
| v3_struct_0(sK221)
| ~ v1_group_1(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f57508,f44629]) ).
fof(f57510,plain,
! [X0] :
( k1_group_1(k5_autgroup(sK221),X0,sK222) = k1_group_1(k3_autgroup(sK221),X0,sK222)
| ~ m1_subset_1(X0,k4_autgroup(sK221))
| ~ v1_group_1(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f57509,f42998]) ).
fof(f57511,plain,
! [X0] :
( k1_group_1(k5_autgroup(sK221),X0,sK222) = k1_group_1(k3_autgroup(sK221),X0,sK222)
| ~ m1_subset_1(X0,k4_autgroup(sK221))
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f57510,f42997]) ).
fof(f57512,plain,
! [X0] :
( k1_group_1(k5_autgroup(sK221),X0,sK222) = k1_group_1(k3_autgroup(sK221),X0,sK222)
| ~ m1_subset_1(X0,k4_autgroup(sK221))
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f57511,f42996]) ).
fof(f57513,plain,
! [X0] :
( k1_group_1(k5_autgroup(sK221),X0,sK222) = k1_group_1(k3_autgroup(sK221),X0,sK222)
| ~ m1_subset_1(X0,k4_autgroup(sK221))
| ~ l1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f57512,f42995]) ).
fof(f57514,plain,
! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK221))
| k1_group_1(k5_autgroup(sK221),X0,sK222) = k1_group_1(k3_autgroup(sK221),X0,sK222) ),
inference(forward_subsumption_resolution,[],[f57513,f42994]) ).
fof(f57515,plain,
k1_group_1(k5_autgroup(sK221),sK222,sK222) = k1_group_1(k3_autgroup(sK221),sK222,sK222),
inference(resolution,[],[f57514,f55064]) ).
fof(f57522,plain,
( sK222 != k1_group_1(k3_autgroup(sK221),sK222,sK222)
| sK222 = k2_group_1(k5_autgroup(sK221))
| ~ m1_subset_1(sK222,u1_struct_0(k5_autgroup(sK221)))
| ~ m1_subset_1(sK222,u1_struct_0(k5_autgroup(sK221)))
| v3_struct_0(k5_autgroup(sK221))
| ~ v3_group_1(k5_autgroup(sK221))
| ~ v4_group_1(k5_autgroup(sK221))
| ~ l1_group_1(k5_autgroup(sK221)) ),
inference(superposition,[],[f43185,f57515]) ).
fof(f57523,plain,
( sK222 != k1_group_1(k3_autgroup(sK221),sK222,sK222)
| sK222 = k2_group_1(k5_autgroup(sK221))
| ~ m1_subset_1(sK222,u1_struct_0(k5_autgroup(sK221)))
| v3_struct_0(k5_autgroup(sK221))
| ~ v3_group_1(k5_autgroup(sK221))
| ~ v4_group_1(k5_autgroup(sK221))
| ~ l1_group_1(k5_autgroup(sK221)) ),
inference(duplicate_literal_removal,[],[f57522]) ).
fof(f57525,plain,
( sK222 != k1_group_1(k3_autgroup(sK221),sK222,sK222)
| ~ m1_subset_1(sK222,u1_struct_0(k5_autgroup(sK221)))
| v3_struct_0(k5_autgroup(sK221))
| ~ v3_group_1(k5_autgroup(sK221))
| ~ v4_group_1(k5_autgroup(sK221))
| ~ l1_group_1(k5_autgroup(sK221)) ),
inference(forward_subsumption_resolution,[],[f57523,f43005]) ).
fof(f57527,plain,
( sK222 != k1_group_1(k3_autgroup(sK221),sK222,sK222)
| v3_struct_0(k5_autgroup(sK221))
| ~ v3_group_1(k5_autgroup(sK221))
| ~ v4_group_1(k5_autgroup(sK221))
| ~ l1_group_1(k5_autgroup(sK221)) ),
inference(forward_subsumption_resolution,[],[f57525,f43004]) ).
fof(f57529,plain,
( sK222 != k1_group_1(k3_autgroup(sK221),sK222,sK222)
| ~ v3_group_1(k5_autgroup(sK221))
| ~ v4_group_1(k5_autgroup(sK221))
| ~ l1_group_1(k5_autgroup(sK221))
| spl1552_81 ),
inference(forward_subsumption_resolution,[],[f57527,f55039]) ).
fof(f57531,plain,
( sK222 != k1_group_1(k3_autgroup(sK221),sK222,sK222)
| ~ v4_group_1(k5_autgroup(sK221))
| ~ l1_group_1(k5_autgroup(sK221))
| ~ spl1552_80
| spl1552_81 ),
inference(forward_subsumption_resolution,[],[f57529,f55035]) ).
fof(f57533,plain,
( sK222 != k1_group_1(k3_autgroup(sK221),sK222,sK222)
| ~ l1_group_1(k5_autgroup(sK221))
| ~ spl1552_79
| ~ spl1552_80
| spl1552_81 ),
inference(forward_subsumption_resolution,[],[f57531,f55031]) ).
fof(f57535,plain,
( sK222 != k1_group_1(k3_autgroup(sK221),sK222,sK222)
| ~ spl1552_78
| ~ spl1552_79
| ~ spl1552_80
| spl1552_81 ),
inference(forward_subsumption_resolution,[],[f57533,f55027]) ).
fof(f57842,plain,
( v3_struct_0(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| ~ v1_group_3(sK221,sK221)
| ~ m1_group_2(sK221,sK221)
| spl1552_104 ),
inference(resolution,[],[f43411,f55680]) ).
fof(f57863,plain,
( v3_struct_0(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| ~ v1_group_3(sK221,sK221)
| spl1552_104 ),
inference(forward_subsumption_resolution,[],[f57842,f43019]) ).
fof(f57874,plain,
( ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| ~ v1_group_3(sK221,sK221)
| spl1552_104 ),
inference(forward_subsumption_resolution,[],[f57863,f42998]) ).
fof(f57885,plain,
( ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| ~ v1_group_3(sK221,sK221)
| spl1552_104 ),
inference(forward_subsumption_resolution,[],[f57874,f42996]) ).
fof(f57893,plain,
( ~ l1_group_1(sK221)
| ~ v1_group_3(sK221,sK221)
| spl1552_104 ),
inference(forward_subsumption_resolution,[],[f57885,f42995]) ).
fof(f57894,plain,
( ~ v1_group_3(sK221,sK221)
| spl1552_104 ),
inference(forward_subsumption_resolution,[],[f57893,f42994]) ).
fof(f57895,plain,
( $false
| spl1552_104 ),
inference(forward_subsumption_resolution,[],[f57894,f55418]) ).
fof(f57896,plain,
spl1552_104,
inference(avatar_contradiction_clause,[],[f57895]) ).
fof(f57925,plain,
( v3_struct_0(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| ~ v1_group_3(sK221,sK221)
| ~ m1_group_2(sK221,sK221)
| spl1552_106 ),
inference(resolution,[],[f55688,f43416]) ).
fof(f57926,plain,
( v3_struct_0(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| ~ v1_group_3(sK221,sK221)
| spl1552_106 ),
inference(forward_subsumption_resolution,[],[f57925,f43019]) ).
fof(f57927,plain,
( ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| ~ v1_group_3(sK221,sK221)
| spl1552_106 ),
inference(forward_subsumption_resolution,[],[f57926,f42998]) ).
fof(f57928,plain,
( ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| ~ v1_group_3(sK221,sK221)
| spl1552_106 ),
inference(forward_subsumption_resolution,[],[f57927,f42996]) ).
fof(f57929,plain,
( ~ l1_group_1(sK221)
| ~ v1_group_3(sK221,sK221)
| spl1552_106 ),
inference(forward_subsumption_resolution,[],[f57928,f42995]) ).
fof(f57930,plain,
( ~ v1_group_3(sK221,sK221)
| spl1552_106 ),
inference(forward_subsumption_resolution,[],[f57929,f42994]) ).
fof(f57931,plain,
( $false
| spl1552_106 ),
inference(forward_subsumption_resolution,[],[f57930,f55418]) ).
fof(f57932,plain,
spl1552_106,
inference(avatar_contradiction_clause,[],[f57931]) ).
fof(f58044,plain,
( sK221 = g1_group_1(u1_struct_0(sK221),u1_group_1(sK221))
| ~ l1_group_1(sK221) ),
inference(resolution,[],[f52036,f42997]) ).
fof(f58045,plain,
sK221 = g1_group_1(u1_struct_0(sK221),u1_group_1(sK221)),
inference(forward_subsumption_resolution,[],[f58044,f42994]) ).
fof(f59350,plain,
( m1_subset_1(k1_group_1(k3_autgroup(sK221),sK222,sK222),u1_struct_0(k5_autgroup(sK221)))
| v3_struct_0(k5_autgroup(sK221))
| ~ l1_group_1(k5_autgroup(sK221))
| ~ m1_subset_1(sK222,u1_struct_0(k5_autgroup(sK221)))
| ~ m1_subset_1(sK222,u1_struct_0(k5_autgroup(sK221))) ),
inference(superposition,[],[f43658,f57515]) ).
fof(f59359,plain,
( m1_subset_1(k1_group_1(k3_autgroup(sK221),sK222,sK222),u1_struct_0(k5_autgroup(sK221)))
| v3_struct_0(k5_autgroup(sK221))
| ~ l1_group_1(k5_autgroup(sK221))
| ~ m1_subset_1(sK222,u1_struct_0(k5_autgroup(sK221))) ),
inference(duplicate_literal_removal,[],[f59350]) ).
fof(f59373,plain,
( m1_subset_1(k1_group_1(k3_autgroup(sK221),sK222,sK222),u1_struct_0(k5_autgroup(sK221)))
| ~ l1_group_1(k5_autgroup(sK221))
| ~ m1_subset_1(sK222,u1_struct_0(k5_autgroup(sK221)))
| spl1552_81 ),
inference(forward_subsumption_resolution,[],[f59359,f55039]) ).
fof(f59386,plain,
( m1_subset_1(k1_group_1(k3_autgroup(sK221),sK222,sK222),u1_struct_0(k5_autgroup(sK221)))
| ~ m1_subset_1(sK222,u1_struct_0(k5_autgroup(sK221)))
| ~ spl1552_78
| spl1552_81 ),
inference(forward_subsumption_resolution,[],[f59373,f55027]) ).
fof(f59394,plain,
( m1_subset_1(k1_group_1(k3_autgroup(sK221),sK222,sK222),u1_struct_0(k5_autgroup(sK221)))
| ~ spl1552_78
| spl1552_81 ),
inference(forward_subsumption_resolution,[],[f59386,f43004]) ).
fof(f59398,plain,
( m1_subset_1(k1_group_1(k3_autgroup(sK221),sK222,sK222),k4_autgroup(sK221))
| ~ spl1552_78
| spl1552_81 ),
inference(forward_demodulation,[],[f59394,f55018]) ).
fof(f59424,plain,
( v3_realset2(k5_autgroup(sK221))
| ~ v3_realset2(k6_group_6(sK221,sK221))
| v3_struct_0(k5_autgroup(sK221))
| ~ v1_group_1(k5_autgroup(sK221))
| ~ v3_group_1(k5_autgroup(sK221))
| ~ v4_group_1(k5_autgroup(sK221))
| ~ l1_group_1(k5_autgroup(sK221))
| v3_struct_0(k6_group_6(sK221,sK221))
| ~ v1_group_1(k6_group_6(sK221,sK221))
| ~ v3_group_1(k6_group_6(sK221,sK221))
| ~ v4_group_1(k6_group_6(sK221,sK221))
| ~ l1_group_1(k6_group_6(sK221,sK221))
| ~ spl1552_108 ),
inference(resolution,[],[f44415,f55696]) ).
fof(f60473,plain,
( v3_struct_0(sK221)
| ~ v3_group_1(sK221)
| g1_group_1(u1_struct_0(sK221),u1_group_1(sK221)) = k6_group_2(sK221)
| ~ l1_group_1(sK221) ),
inference(resolution,[],[f50468,f42995]) ).
fof(f60474,plain,
( ~ v3_group_1(sK221)
| g1_group_1(u1_struct_0(sK221),u1_group_1(sK221)) = k6_group_2(sK221)
| ~ l1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f60473,f42998]) ).
fof(f60484,plain,
( g1_group_1(u1_struct_0(sK221),u1_group_1(sK221)) = k6_group_2(sK221)
| ~ l1_group_1(sK221) ),
inference(forward_subsumption_resolution,[],[f60474,f42996]) ).
fof(f60494,plain,
g1_group_1(u1_struct_0(sK221),u1_group_1(sK221)) = k6_group_2(sK221),
inference(forward_subsumption_resolution,[],[f60484,f42994]) ).
fof(f60504,plain,
sK221 = k6_group_2(sK221),
inference(forward_demodulation,[],[f60494,f58045]) ).
fof(f60513,plain,
( v3_realset2(k6_group_6(sK221,sK221))
| v3_struct_0(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221) ),
inference(superposition,[],[f44445,f60504]) ).
fof(f60523,plain,
( v3_struct_0(sK221)
| ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| spl1552_192 ),
inference(forward_subsumption_resolution,[],[f60513,f57287]) ).
fof(f60524,plain,
( ~ v3_group_1(sK221)
| ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| spl1552_192 ),
inference(forward_subsumption_resolution,[],[f60523,f42998]) ).
fof(f60525,plain,
( ~ v4_group_1(sK221)
| ~ l1_group_1(sK221)
| spl1552_192 ),
inference(forward_subsumption_resolution,[],[f60524,f42996]) ).
fof(f60526,plain,
( ~ l1_group_1(sK221)
| spl1552_192 ),
inference(forward_subsumption_resolution,[],[f60525,f42995]) ).
fof(f60527,plain,
( $false
| spl1552_192 ),
inference(forward_subsumption_resolution,[],[f60526,f42994]) ).
fof(f60528,plain,
spl1552_192,
inference(avatar_contradiction_clause,[],[f60527]) ).
fof(f60529,plain,
( ~ v3_realset2(k6_group_6(sK221,sK221))
| v3_struct_0(k5_autgroup(sK221))
| ~ v1_group_1(k5_autgroup(sK221))
| ~ v3_group_1(k5_autgroup(sK221))
| ~ v4_group_1(k5_autgroup(sK221))
| ~ l1_group_1(k5_autgroup(sK221))
| v3_struct_0(k6_group_6(sK221,sK221))
| ~ v1_group_1(k6_group_6(sK221,sK221))
| ~ v3_group_1(k6_group_6(sK221,sK221))
| ~ v4_group_1(k6_group_6(sK221,sK221))
| ~ l1_group_1(k6_group_6(sK221,sK221))
| ~ spl1552_108
| spl1552_167 ),
inference(forward_subsumption_resolution,[],[f59424,f56786]) ).
fof(f60530,plain,
( v3_struct_0(k5_autgroup(sK221))
| ~ v1_group_1(k5_autgroup(sK221))
| ~ v3_group_1(k5_autgroup(sK221))
| ~ v4_group_1(k5_autgroup(sK221))
| ~ l1_group_1(k5_autgroup(sK221))
| v3_struct_0(k6_group_6(sK221,sK221))
| ~ v1_group_1(k6_group_6(sK221,sK221))
| ~ v3_group_1(k6_group_6(sK221,sK221))
| ~ v4_group_1(k6_group_6(sK221,sK221))
| ~ l1_group_1(k6_group_6(sK221,sK221))
| ~ spl1552_108
| spl1552_167
| ~ spl1552_192 ),
inference(forward_subsumption_resolution,[],[f60529,f57286]) ).
fof(f60531,plain,
( ~ v1_group_1(k5_autgroup(sK221))
| ~ v3_group_1(k5_autgroup(sK221))
| ~ v4_group_1(k5_autgroup(sK221))
| ~ l1_group_1(k5_autgroup(sK221))
| v3_struct_0(k6_group_6(sK221,sK221))
| ~ v1_group_1(k6_group_6(sK221,sK221))
| ~ v3_group_1(k6_group_6(sK221,sK221))
| ~ v4_group_1(k6_group_6(sK221,sK221))
| ~ l1_group_1(k6_group_6(sK221,sK221))
| spl1552_81
| ~ spl1552_108
| spl1552_167
| ~ spl1552_192 ),
inference(forward_subsumption_resolution,[],[f60530,f55039]) ).
fof(f60532,plain,
( ~ v3_group_1(k5_autgroup(sK221))
| ~ v4_group_1(k5_autgroup(sK221))
| ~ l1_group_1(k5_autgroup(sK221))
| v3_struct_0(k6_group_6(sK221,sK221))
| ~ v1_group_1(k6_group_6(sK221,sK221))
| ~ v3_group_1(k6_group_6(sK221,sK221))
| ~ v4_group_1(k6_group_6(sK221,sK221))
| ~ l1_group_1(k6_group_6(sK221,sK221))
| spl1552_81
| ~ spl1552_95
| ~ spl1552_108
| spl1552_167
| ~ spl1552_192 ),
inference(forward_subsumption_resolution,[],[f60531,f55205]) ).
fof(f60533,plain,
( ~ v4_group_1(k5_autgroup(sK221))
| ~ l1_group_1(k5_autgroup(sK221))
| v3_struct_0(k6_group_6(sK221,sK221))
| ~ v1_group_1(k6_group_6(sK221,sK221))
| ~ v3_group_1(k6_group_6(sK221,sK221))
| ~ v4_group_1(k6_group_6(sK221,sK221))
| ~ l1_group_1(k6_group_6(sK221,sK221))
| ~ spl1552_80
| spl1552_81
| ~ spl1552_95
| ~ spl1552_108
| spl1552_167
| ~ spl1552_192 ),
inference(forward_subsumption_resolution,[],[f60532,f55035]) ).
fof(f60534,plain,
( ~ l1_group_1(k5_autgroup(sK221))
| v3_struct_0(k6_group_6(sK221,sK221))
| ~ v1_group_1(k6_group_6(sK221,sK221))
| ~ v3_group_1(k6_group_6(sK221,sK221))
| ~ v4_group_1(k6_group_6(sK221,sK221))
| ~ l1_group_1(k6_group_6(sK221,sK221))
| ~ spl1552_79
| ~ spl1552_80
| spl1552_81
| ~ spl1552_95
| ~ spl1552_108
| spl1552_167
| ~ spl1552_192 ),
inference(forward_subsumption_resolution,[],[f60533,f55031]) ).
fof(f60535,plain,
( v3_struct_0(k6_group_6(sK221,sK221))
| ~ v1_group_1(k6_group_6(sK221,sK221))
| ~ v3_group_1(k6_group_6(sK221,sK221))
| ~ v4_group_1(k6_group_6(sK221,sK221))
| ~ l1_group_1(k6_group_6(sK221,sK221))
| ~ spl1552_78
| ~ spl1552_79
| ~ spl1552_80
| spl1552_81
| ~ spl1552_95
| ~ spl1552_108
| spl1552_167
| ~ spl1552_192 ),
inference(forward_subsumption_resolution,[],[f60534,f55027]) ).
fof(f60536,plain,
( ~ v1_group_1(k6_group_6(sK221,sK221))
| ~ v3_group_1(k6_group_6(sK221,sK221))
| ~ v4_group_1(k6_group_6(sK221,sK221))
| ~ l1_group_1(k6_group_6(sK221,sK221))
| ~ spl1552_78
| ~ spl1552_79
| ~ spl1552_80
| spl1552_81
| ~ spl1552_95
| spl1552_107
| ~ spl1552_108
| spl1552_167
| ~ spl1552_192 ),
inference(forward_subsumption_resolution,[],[f60535,f55691]) ).
fof(f60537,plain,
( ~ v3_group_1(k6_group_6(sK221,sK221))
| ~ v4_group_1(k6_group_6(sK221,sK221))
| ~ l1_group_1(k6_group_6(sK221,sK221))
| ~ spl1552_78
| ~ spl1552_79
| ~ spl1552_80
| spl1552_81
| ~ spl1552_95
| ~ spl1552_106
| spl1552_107
| ~ spl1552_108
| spl1552_167
| ~ spl1552_192 ),
inference(forward_subsumption_resolution,[],[f60536,f55687]) ).
fof(f60538,plain,
( ~ v4_group_1(k6_group_6(sK221,sK221))
| ~ l1_group_1(k6_group_6(sK221,sK221))
| ~ spl1552_78
| ~ spl1552_79
| ~ spl1552_80
| spl1552_81
| ~ spl1552_95
| ~ spl1552_105
| ~ spl1552_106
| spl1552_107
| ~ spl1552_108
| spl1552_167
| ~ spl1552_192 ),
inference(forward_subsumption_resolution,[],[f60537,f55683]) ).
fof(f60539,plain,
( ~ l1_group_1(k6_group_6(sK221,sK221))
| ~ spl1552_78
| ~ spl1552_79
| ~ spl1552_80
| spl1552_81
| ~ spl1552_95
| ~ spl1552_104
| ~ spl1552_105
| ~ spl1552_106
| spl1552_107
| ~ spl1552_108
| spl1552_167
| ~ spl1552_192 ),
inference(forward_subsumption_resolution,[],[f60538,f55679]) ).
fof(f60540,plain,
( $false
| ~ spl1552_78
| ~ spl1552_79
| ~ spl1552_80
| spl1552_81
| ~ spl1552_95
| ~ spl1552_103
| ~ spl1552_104
| ~ spl1552_105
| ~ spl1552_106
| spl1552_107
| ~ spl1552_108
| spl1552_167
| ~ spl1552_192 ),
inference(forward_subsumption_resolution,[],[f60539,f55675]) ).
fof(f60541,plain,
( ~ spl1552_78
| ~ spl1552_79
| ~ spl1552_80
| spl1552_81
| ~ spl1552_95
| ~ spl1552_103
| ~ spl1552_104
| ~ spl1552_105
| ~ spl1552_106
| spl1552_107
| ~ spl1552_108
| spl1552_167
| ~ spl1552_192 ),
inference(avatar_contradiction_clause,[],[f60540]) ).
fof(f60543,plain,
( sK222 = k1_group_1(k3_autgroup(sK221),sK222,sK222)
| ~ spl1552_78
| spl1552_81
| ~ spl1552_175 ),
inference(resolution,[],[f56818,f59398]) ).
fof(f60549,plain,
( $false
| ~ spl1552_78
| ~ spl1552_79
| ~ spl1552_80
| spl1552_81
| ~ spl1552_175 ),
inference(forward_subsumption_resolution,[],[f60543,f57535]) ).
fof(f60550,plain,
( ~ spl1552_78
| ~ spl1552_79
| ~ spl1552_80
| spl1552_81
| ~ spl1552_175 ),
inference(avatar_contradiction_clause,[],[f60549]) ).
cnf(s78,plain,
spl1552_95,
inference(sat_conversion,[],[f55343]) ).
cnf(s84,plain,
spl1552_78,
inference(sat_conversion,[],[f55426]) ).
cnf(s87,plain,
~ spl1552_81,
inference(sat_conversion,[],[f55444]) ).
cnf(s88,plain,
( ~ spl1552_78
| spl1552_84 ),
inference(sat_conversion,[],[f55447]) ).
cnf(s89,plain,
spl1552_79,
inference(sat_conversion,[],[f55475]) ).
cnf(s90,plain,
spl1552_80,
inference(sat_conversion,[],[f55486]) ).
cnf(s91,plain,
( ~ spl1552_78
| ~ spl1552_79
| ~ spl1552_80
| spl1552_81
| ~ spl1552_95
| ~ spl1552_103
| ~ spl1552_104
| ~ spl1552_105
| ~ spl1552_106
| spl1552_107
| spl1552_108 ),
inference(sat_conversion,[],[f55697]) ).
cnf(s147,plain,
( ~ spl1552_84
| ~ spl1552_167
| spl1552_175 ),
inference(sat_conversion,[],[f56819]) ).
cnf(s163,plain,
spl1552_103,
inference(sat_conversion,[],[f57249]) ).
cnf(s164,plain,
~ spl1552_107,
inference(sat_conversion,[],[f57257]) ).
cnf(s170,plain,
spl1552_105,
inference(sat_conversion,[],[f57318]) ).
cnf(s175,plain,
spl1552_104,
inference(sat_conversion,[],[f57896]) ).
cnf(s176,plain,
spl1552_106,
inference(sat_conversion,[],[f57932]) ).
cnf(s260,plain,
spl1552_192,
inference(sat_conversion,[],[f60528]) ).
cnf(s261,plain,
( ~ spl1552_78
| ~ spl1552_79
| ~ spl1552_80
| spl1552_81
| ~ spl1552_95
| ~ spl1552_103
| ~ spl1552_104
| ~ spl1552_105
| ~ spl1552_106
| spl1552_107
| ~ spl1552_108
| spl1552_167
| ~ spl1552_192 ),
inference(sat_conversion,[],[f60541]) ).
cnf(s263,plain,
( ~ spl1552_78
| ~ spl1552_79
| ~ spl1552_80
| spl1552_81
| ~ spl1552_175 ),
inference(sat_conversion,[],[f60550]) ).
cnf(s281,plain,
( ~ spl1552_78
| ~ spl1552_79
| ~ spl1552_80
| spl1552_81
| ~ spl1552_95
| spl1552_108 ),
inference(rat,[],[s91,s164,s176,s170,s175,s163]) ).
cnf(s284,plain,
~ spl1552_175,
inference(rat,[],[s263,s87,s89,s90,s84]) ).
cnf(s286,plain,
spl1552_84,
inference(rat,[],[s88,s84]) ).
cnf(s288,plain,
~ spl1552_167,
inference(rat,[],[s147,s284,s286]) ).
cnf(s292,plain,
~ spl1552_108,
inference(rat,[],[s261,s260,s288,s84,s164,s176,s170,s175,s163,s87,s89,s90,s78]) ).
cnf(s303,plain,
$false,
inference(rat,[],[s281,s84,s87,s89,s90,s292,s78]) ).
fof(f60553,plain,
$false,
inference(avatar_sat_refutation,[],[s303]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP634+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.36 % Computer : n009.cluster.edu
% 0.12/0.36 % Model : x86_64 x86_64
% 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.36 % Memory : 8046.5625MB
% 0.12/0.36 % OS : Linux 6.8.0-71-generic
% 0.12/0.36 % CPULimit : 300
% 0.12/0.36 % WCLimit : 300
% 0.12/0.36 % DateTime : Sun Sep 27 10:19:51 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.16/0.40 Running first-order theorem proving
% 0.16/0.40 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
% 14.93/3.56 % (1815934)Detected formulas, will run a generic FOF schedule.
% 14.93/3.56 % (1816080)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3742556684:i=119:av=off:ss=axioms_2991 on theBenchmark for (2991ds/119Mi)
% 14.93/3.56 % (1816082)dis-21_1_sil=8000:lcm=predicate:random_seed=1711393343:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2991 on theBenchmark for (2991ds/129Mi)
% 14.93/3.56 % (1816077)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=1140944985:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2991 on theBenchmark for (2991ds/134677Mi)
% 14.93/3.56 % (1816078)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=261736254:i=141695:sd=1:nm=32:gsp=on:ss=included_2991 on theBenchmark for (2991ds/141695Mi)
% 14.93/3.56 % (1816076)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=2624350943:i=141193_2991 on theBenchmark for (2991ds/141193Mi)
% 14.93/3.56 % (1816079)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1220665419:i=109:sd=1:ins=1:gsp=on:ss=axioms_2991 on theBenchmark for (2991ds/109Mi)
% 14.93/3.56 % (1816081)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2403807941:s2a=on:i=139:gtg=position_2991 on theBenchmark for (2991ds/139Mi)
% 14.93/3.56 % (1816081)Instruction limit reached!
% 14.93/3.56 % (1816081)------------------------------
% 14.93/3.56 % (1816081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.93/3.56 % (1816081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.93/3.56 % (1816081)CaDiCaL version: 2.1.3
% 14.93/3.56 % (1816081)Termination reason: Instruction limit
% 14.93/3.56 % (1816081)Termination phase: Property scanning
% 14.93/3.56 % (1816081)Time elapsed: 0.060 s
% 14.93/3.56 % (1816081)Peak memory usage: 133 MB
% 14.93/3.56 % (1816081)Instructions burned: 140 (million)
% 14.93/3.56 % (1816079)Instruction limit reached!
% 14.93/3.56 % (1816079)------------------------------
% 14.93/3.56 % (1816079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.93/3.56 % (1816079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.93/3.56 % (1816079)CaDiCaL version: 2.1.3
% 14.93/3.56 % (1816079)Termination reason: Instruction limit
% 14.93/3.56 % (1816079)Termination phase: SInE selection
% 14.93/3.56 % (1816079)Time elapsed: 0.081 s
% 14.93/3.56 % (1816079)Peak memory usage: 133 MB
% 14.93/3.56 % (1816079)Instructions burned: 110 (million)
% 14.93/3.56 % (1816080)Instruction limit reached!
% 14.93/3.56 % (1816080)------------------------------
% 14.93/3.56 % (1816080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.93/3.56 % (1816080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.93/3.56 % (1816080)CaDiCaL version: 2.1.3
% 14.93/3.56 % (1816080)Termination reason: Instruction limit
% 14.93/3.56 % (1816080)Termination phase: SInE selection
% 14.93/3.56 % (1816080)Time elapsed: 0.088 s
% 14.93/3.56 % (1816080)Peak memory usage: 133 MB
% 14.93/3.56 % (1816080)Instructions burned: 119 (million)
% 14.93/3.56 % (1816082)Instruction limit reached!
% 14.93/3.56 % (1816082)------------------------------
% 14.93/3.56 % (1816082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.93/3.56 % (1816082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.93/3.56 % (1816082)CaDiCaL version: 2.1.3
% 14.93/3.56 % (1816082)Termination reason: Instruction limit
% 14.93/3.56 % (1816082)Termination phase: SInE selection
% 14.93/3.56 % (1816082)Time elapsed: 0.090 s
% 14.93/3.56 % (1816082)Peak memory usage: 133 MB
% 14.93/3.56 % (1816082)Instructions burned: 129 (million)
% 14.93/3.56 % (1816090)lrs+10_1_sil=8000:sp=occurrence:random_seed=3816771776:i=285:sd=3:ss=axioms:sgt=8_2989 on theBenchmark for (2989ds/285Mi)
% 14.93/3.56 % (1816091)lrs+10_1_sil=32000:urr=on:br=off:random_seed=320838609:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/157Mi)
% 14.93/3.56 % (1816092)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2884790655:i=325:sd=1:ss=axioms:sgt=32_2988 on theBenchmark for (2988ds/325Mi)
% 14.93/3.56 % (1816093)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=2646815328:s2a=on:i=248:s2at=1.23:gtg=position_2988 on theBenchmark for (2988ds/248Mi)
% 14.93/3.56 % (1816091)Instruction limit reached!
% 22.98/4.73 % (1816091)------------------------------
% 22.98/4.73 % (1816091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.98/4.73 % (1816091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.98/4.73 % (1816091)CaDiCaL version: 2.1.3
% 22.98/4.73 % (1816091)Termination reason: Instruction limit
% 22.98/4.73 % (1816091)Termination phase: Property scanning
% 22.98/4.73 % (1816091)Time elapsed: 0.069 s
% 22.98/4.73 % (1816091)Peak memory usage: 133 MB
% 22.98/4.73 % (1816091)Instructions burned: 158 (million)
% 22.98/4.73 % (1816093)Instruction limit reached!
% 22.98/4.73 % (1816093)------------------------------
% 22.98/4.73 % (1816093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.98/4.73 % (1816093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.98/4.73 % (1816093)CaDiCaL version: 2.1.3
% 22.98/4.73 % (1816093)Termination reason: Instruction limit
% 22.98/4.73 % (1816093)Termination phase: Property scanning
% 22.98/4.73 % (1816093)Time elapsed: 0.105 s
% 22.98/4.73 % (1816093)Peak memory usage: 133 MB
% 22.98/4.73 % (1816093)Instructions burned: 250 (million)
% 22.98/4.73 % (1816090)Instruction limit reached!
% 22.98/4.73 % (1816090)------------------------------
% 22.98/4.73 % (1816090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.98/4.73 % (1816090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.98/4.73 % (1816090)CaDiCaL version: 2.1.3
% 22.98/4.73 % (1816090)Termination reason: Instruction limit
% 22.98/4.73 % (1816090)Termination phase: Property scanning
% 22.98/4.73 % (1816090)Time elapsed: 0.148 s
% 22.98/4.73 % (1816090)Peak memory usage: 138 MB
% 22.98/4.73 % (1816090)Instructions burned: 289 (million)
% 22.98/4.73 % (1816092)Refutation not found, incomplete strategy
% 22.98/4.73 % (1816092)------------------------------
% 22.98/4.73 % (1816092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.98/4.73 % (1816092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.98/4.73 % (1816092)CaDiCaL version: 2.1.3
% 22.98/4.73 % (1816092)Termination reason: Refutation not found, incomplete strategy
% 22.98/4.73 % (1816092)Time elapsed: 0.190 s
% 22.98/4.73 % (1816092)Peak memory usage: 139 MB
% 22.98/4.73 % (1816092)Instructions burned: 235 (million)
% 22.98/4.73 % (1816098)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=58711228:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2986 on theBenchmark for (2986ds/294Mi)
% 22.98/4.73 % (1816100)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2338989633:cts=off:i=113:fsr=off:ss=included:sgt=4_2985 on theBenchmark for (2985ds/113Mi)
% 22.98/4.73 % (1816099)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2918546723:i=2350_2986 on theBenchmark for (2986ds/2350Mi)
% 22.98/4.73 % (1816100)Instruction limit reached!
% 22.98/4.73 % (1816100)------------------------------
% 22.98/4.73 % (1816100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.98/4.73 % (1816100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.98/4.73 % (1816100)CaDiCaL version: 2.1.3
% 22.98/4.73 % (1816100)Termination reason: Instruction limit
% 22.98/4.73 % (1816100)Termination phase: SInE selection
% 22.98/4.73 % (1816100)Time elapsed: 0.049 s
% 22.98/4.73 % (1816100)Peak memory usage: 133 MB
% 22.98/4.73 % (1816100)Instructions burned: 114 (million)
% 22.98/4.73 % (1816098)Instruction limit reached!
% 22.98/4.73 % (1816098)------------------------------
% 22.98/4.73 % (1816098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.98/4.73 % (1816098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.98/4.73 % (1816098)CaDiCaL version: 2.1.3
% 22.98/4.73 % (1816098)Termination reason: Instruction limit
% 22.98/4.73 % (1816098)Termination phase: SInE selection
% 22.98/4.73 % (1816098)Time elapsed: 0.188 s
% 22.98/4.73 % (1816098)Peak memory usage: 134 MB
% 22.98/4.73 % (1816098)Instructions burned: 295 (million)
% 22.98/4.73 % (1816104)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1387526557:i=127:av=off:fsr=off:sup=off_2984 on theBenchmark for (2984ds/127Mi)
% 22.98/4.73 % (1816092)------------------------------
% 22.98/4.73 % (1816092)------------------------------
% 22.98/4.73 % (1816104)Instruction limit reached!
% 22.98/4.73 % (1816104)------------------------------
% 22.98/4.73 % (1816104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.98/4.73 % (1816104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.67/7.91 % (1816104)CaDiCaL version: 2.1.3
% 25.67/7.91 % (1816104)Termination reason: Instruction limit
% 25.67/7.91 % (1816104)Termination phase: Preprocessing 1
% 25.67/7.91 % (1816104)Time elapsed: 0.057 s
% 25.67/7.91 % (1816104)Peak memory usage: 136 MB
% 25.67/7.91 % (1816104)Instructions burned: 127 (million)
% 25.67/7.91 % (1816106)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3121582327:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2982 on theBenchmark for (2982ds/114Mi)
% 25.67/7.91 % (1816108)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=540875024:i=437:sd=1:aac=none:ss=included_2982 on theBenchmark for (2982ds/437Mi)
% 25.67/7.91 % (1816107)lrs+10_1_sil=8000:sp=occurrence:random_seed=3619643155:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2982 on theBenchmark for (2982ds/907Mi)
% 25.67/7.91 % (1816106)Instruction limit reached!
% 25.67/7.91 % (1816106)------------------------------
% 25.67/7.91 % (1816106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.67/7.91 % (1816106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.67/7.91 % (1816106)CaDiCaL version: 2.1.3
% 25.67/7.91 % (1816106)Termination reason: Instruction limit
% 25.67/7.91 % (1816106)Termination phase: Property scanning
% 25.67/7.91 % (1816106)Time elapsed: 0.053 s
% 25.67/7.91 % (1816106)Peak memory usage: 133 MB
% 25.67/7.91 % (1816106)Instructions burned: 115 (million)
% 25.67/7.91 % (1816108)Instruction limit reached!
% 25.67/7.91 % (1816108)------------------------------
% 25.67/7.91 % (1816108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.67/7.91 % (1816108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.67/7.91 % (1816108)CaDiCaL version: 2.1.3
% 25.67/7.91 % (1816108)Termination reason: Instruction limit
% 25.67/7.91 % (1816108)Termination phase: Saturation
% 25.67/7.91 % (1816108)Time elapsed: 0.166 s
% 25.67/7.91 % (1816108)Peak memory usage: 141 MB
% 25.67/7.91 % (1816108)Instructions burned: 438 (million)
% 25.67/7.91 % (1816112)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=120664126:i=5202:ss=axioms:sgt=16_2980 on theBenchmark for (2980ds/5202Mi)
% 25.67/7.91 % (1816113)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=737672140:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2979 on theBenchmark for (2979ds/134Mi)
% 25.67/7.91 % (1816113)Instruction limit reached!
% 25.67/7.91 % (1816113)------------------------------
% 25.67/7.91 % (1816113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.67/7.91 % (1816113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.67/7.91 % (1816113)CaDiCaL version: 2.1.3
% 25.67/7.91 % (1816113)Termination reason: Instruction limit
% 25.67/7.91 % (1816113)Termination phase: SInE selection
% 25.67/7.91 % (1816113)Time elapsed: 0.102 s
% 25.67/7.91 % (1816113)Peak memory usage: 133 MB
% 25.67/7.91 % (1816113)Instructions burned: 135 (million)
% 25.67/7.91 % (1816107)Instruction limit reached!
% 25.67/7.91 % (1816107)------------------------------
% 25.67/7.91 % (1816107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.67/7.91 % (1816107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.67/7.91 % (1816107)CaDiCaL version: 2.1.3
% 25.67/7.91 % (1816107)Termination reason: Instruction limit
% 25.67/7.91 % (1816107)Termination phase: Property scanning
% 25.67/7.91 % (1816107)Time elapsed: 0.566 s
% 25.67/7.91 % (1816107)Peak memory usage: 154 MB
% 25.67/7.91 % (1816107)Instructions burned: 907 (million)
% 25.67/7.91 % (1816116)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3201404237:st=8:i=592:sd=3:ep=RST:ss=axioms_2976 on theBenchmark for (2976ds/592Mi)
% 25.67/7.91 % (1816117)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=961036603:st=3:i=13193:sd=3:ss=axioms_2975 on theBenchmark for (2975ds/13193Mi)
% 25.67/7.91 % (1816116)Instruction limit reached!
% 25.67/7.91 % (1816116)------------------------------
% 25.67/7.91 % (1816116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.67/7.91 % (1816116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.67/7.91 % (1816116)CaDiCaL version: 2.1.3
% 25.67/7.91 % (1816116)Termination reason: Instruction limit
% 25.67/7.91 % (1816116)Termination phase: Preprocessing 2
% 25.67/7.91 % (1816116)Time elapsed: 0.451 s
% 25.67/7.91 % (1816116)Peak memory usage: 151 MB
% 25.67/7.91 % (1816116)Instructions burned: 592 (million)
% 25.67/7.91 % (1816099)Instruction limit reached!
% 25.67/7.91 % (1816099)------------------------------
% 25.67/7.91 % (1816099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.67/7.91 % (1816099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.67/7.91 % (1816099)CaDiCaL version: 2.1.3
% 25.67/7.91 % (1816099)Termination reason: Instruction limit
% 25.67/7.91 % (1816099)Termination phase: Property scanning
% 25.67/7.91 % (1816099)Time elapsed: 1.426 s
% 25.67/7.91 % (1816099)Peak memory usage: 227 MB
% 25.67/7.91 % (1816099)Instructions burned: 2351 (million)
% 25.67/7.91 % (1816120)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=3741617578:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2970 on theBenchmark for (2970ds/125Mi)
% 25.67/7.91 % (1816121)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1080071585:i=134:gtgl=5:slsql=off:gtg=exists_sym_2970 on theBenchmark for (2970ds/134Mi)
% 25.67/7.91 % (1816120)Instruction limit reached!
% 25.67/7.91 % (1816120)------------------------------
% 25.67/7.91 % (1816120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.67/7.91 % (1816120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.67/7.91 % (1816120)CaDiCaL version: 2.1.3
% 25.67/7.91 % (1816120)Termination reason: Instruction limit
% 25.67/7.91 % (1816120)Termination phase: Property scanning
% 25.67/7.91 % (1816120)Time elapsed: 0.057 s
% 25.67/7.91 % (1816120)Peak memory usage: 133 MB
% 25.67/7.91 % (1816120)Instructions burned: 125 (million)
% 25.67/7.91 % (1816121)Instruction limit reached!
% 25.67/7.91 % (1816121)------------------------------
% 25.67/7.91 % (1816121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.67/7.91 % (1816121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.67/7.91 % (1816121)CaDiCaL version: 2.1.3
% 25.67/7.91 % (1816121)Termination reason: Instruction limit
% 25.67/7.91 % (1816121)Termination phase: Property scanning
% 25.67/7.91 % (1816121)Time elapsed: 0.061 s
% 25.67/7.91 % (1816121)Peak memory usage: 133 MB
% 25.67/7.91 % (1816121)Instructions burned: 136 (million)
% 25.67/7.91 % (1816124)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1139360884:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/141Mi)
% 25.67/7.91 % (1816125)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4152230429:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2967 on theBenchmark for (2967ds/431Mi)
% 25.67/7.91 % (1816124)Instruction limit reached!
% 25.67/7.91 % (1816124)------------------------------
% 25.67/7.91 % (1816124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.67/7.91 % (1816124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.67/7.91 % (1816124)CaDiCaL version: 2.1.3
% 25.67/7.91 % (1816124)Termination reason: Instruction limit
% 25.67/7.91 % (1816124)Termination phase: SInE selection
% 25.67/7.91 % (1816124)Time elapsed: 0.107 s
% 25.67/7.91 % (1816124)Peak memory usage: 133 MB
% 25.67/7.91 % (1816124)Instructions burned: 141 (million)
% 25.67/7.91 % (1816125)Refutation not found, incomplete strategy
% 25.67/7.91 % (1816125)------------------------------
% 25.67/7.91 % (1816125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.67/7.91 % (1816125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.67/7.91 % (1816125)CaDiCaL version: 2.1.3
% 25.67/7.91 % (1816125)Termination reason: Refutation not found, incomplete strategy
% 25.67/7.91 % (1816125)Time elapsed: 0.190 s
% 25.67/7.91 % (1816125)Peak memory usage: 139 MB
% 25.67/7.91 % (1816125)Instructions burned: 232 (million)
% 25.67/7.91 % (1816128)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=205564038:i=6060:aac=none:ins=25_2965 on theBenchmark for (2965ds/6060Mi)
% 25.67/7.91 % (1816125)------------------------------
% 25.67/7.91 % (1816125)------------------------------
% 25.67/7.91 % (1816130)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=3327004649:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2961 on theBenchmark for (2961ds/150Mi)
% 25.67/7.91 % (1816130)Instruction limit reached!
% 25.67/7.91 % (1816130)------------------------------
% 25.67/7.91 % (1816130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.67/7.91 % (1816130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.67/7.91 % (1816130)CaDiCaL version: 2.1.3
% 25.67/7.91 % (1816130)Termination reason: Instruction limit
% 25.67/7.91 % (1816130)Termination phase: SInE selection
% 25.67/7.91 % (1816130)Time elapsed: 0.120 s
% 25.67/7.91 % (1816130)Peak memory usage: 133 MB
% 25.67/7.91 % (1816130)Instructions burned: 151 (million)
% 25.67/7.91 % (1816132)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3949430042:i=14155:bd=all_2958 on theBenchmark for (2958ds/14155Mi)
% 25.67/7.91 % (1816112)Instruction limit reached!
% 25.67/7.91 % (1816112)------------------------------
% 25.67/7.91 % (1816112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.67/7.91 % (1816112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.67/7.91 % (1816112)CaDiCaL version: 2.1.3
% 25.67/7.91 % (1816112)Termination reason: Instruction limit
% 25.67/7.91 % (1816112)Termination phase: Saturation
% 25.67/7.91 % (1816112)Time elapsed: 3.032 s
% 25.67/7.91 % (1816112)Peak memory usage: 258 MB
% 25.67/7.91 % (1816112)Instructions burned: 5203 (million)
% 25.67/7.91 % (1816134)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2349279371:i=667:av=off:fsr=off_2948 on theBenchmark for (2948ds/667Mi)
% 25.67/7.91 % (1816134)Instruction limit reached!
% 25.67/7.91 % (1816134)------------------------------
% 25.67/7.91 % (1816134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.67/7.91 % (1816134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.67/7.91 % (1816134)CaDiCaL version: 2.1.3
% 25.67/7.91 % (1816134)Termination reason: Instruction limit
% 25.67/7.91 % (1816134)Termination phase: NewCNF
% 25.67/7.91 % (1816134)Time elapsed: 0.544 s
% 25.67/7.91 % (1816134)Peak memory usage: 183 MB
% 25.67/7.91 % (1816134)Instructions burned: 667 (million)
% 25.67/7.91 % (1816136)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=148803642:s2a=on:i=185:s2at=1.8:fdi=4_2941 on theBenchmark for (2941ds/185Mi)
% 25.67/7.91 % (1816136)Instruction limit reached!
% 25.67/7.91 % (1816136)------------------------------
% 25.67/7.91 % (1816136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.67/7.91 % (1816136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.67/7.91 % (1816136)CaDiCaL version: 2.1.3
% 25.67/7.91 % (1816136)Termination reason: Instruction limit
% 25.67/7.91 % (1816136)Termination phase: SInE selection
% 25.67/7.91 % (1816136)Time elapsed: 0.131 s
% 25.67/7.91 % (1816136)Peak memory usage: 133 MB
% 25.67/7.91 % (1816136)Instructions burned: 185 (million)
% 25.67/7.91 % (1816138)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2293820278:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2938 on theBenchmark for (2938ds/193Mi)
% 25.67/7.91 % (1816138)Instruction limit reached!
% 25.67/7.91 % (1816138)------------------------------
% 25.67/7.91 % (1816138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.67/7.91 % (1816138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.67/7.91 % (1816138)CaDiCaL version: 2.1.3
% 25.67/7.91 % (1816138)Termination reason: Instruction limit
% 25.67/7.91 % (1816138)Termination phase: SInE selection
% 25.67/7.91 % (1816138)Time elapsed: 0.152 s
% 25.67/7.91 % (1816138)Peak memory usage: 134 MB
% 25.67/7.91 % (1816138)Instructions burned: 193 (million)
% 25.67/7.91 % (1816140)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3162021163:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2934 on theBenchmark for (2934ds/4850Mi)
% 25.67/7.91 % (1816117)First to succeed.
% 25.67/7.91 % (1816117)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1815934"
% 25.67/7.91 % (1816117)Refutation found. Thanks to Tanya!
% 25.67/7.91 % SZS status Theorem for theBenchmark
% 25.67/7.91 % SZS output start Proof for theBenchmark
% See solution above
% 46.45/8.12 % (1816117)------------------------------
% 46.45/8.12 % (1816117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.45/8.12 % (1816117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.45/8.12 % (1816117)CaDiCaL version: 2.1.3
% 46.45/8.12 % (1816117)Termination reason: Refutation
% 46.45/8.12 % (1816117)Time elapsed: 4.311 s
% 46.45/8.12 % (1816117)Peak memory usage: 314 MB
% 46.45/8.12 % (1816117)Instructions burned: 7023 (million)
% 46.45/8.12 % (1816117)------------------------------
% 46.45/8.12 % (1816117)------------------------------
% 46.45/8.12 % (1815934)Success in time 7.301 s
% 46.45/8.12 % Vampire exiting
%------------------------------------------------------------------------------