%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SCT170+2 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n004.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 12:37:06 PM UTC 2026
% Result : Theorem 11.42s 2.54s
% Output : Refutation 12.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 34
% Syntax : Number of formulae : 184 ( 64 unt; 17 def)
% Number of atoms : 642 ( 171 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 762 ( 304 ~; 373 |; 55 &)
% ( 13 <=>; 16 =>; 0 <=; 1 <~>)
% Maximal formula depth : 18 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 11 ( 9 usr; 6 prp; 0-5 aty)
% Number of functors : 54 ( 54 usr; 30 con; 0-2 aty)
% Number of variables : 185 ( 0 sgn 182 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f202,axiom,
is_Arr723427730le_alt(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gsy_v_a____) ).
fof(f203,axiom,
is_Arr723427730le_alt(b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gsy_v_b____) ).
fof(f204,axiom,
is_Arr723427730le_alt(c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gsy_v_c____) ).
fof(f205,axiom,
hBOOL(hAPP_f147218624l_bool(hAPP_f621397159l_bool(member1265098019t_bool,p),arrow_583275979e_Prof)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0__096P_A_058_AProf_096) ).
fof(f209,axiom,
hBOOL(hAPP_l300482276t_bool(distin85347314le_alt,hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,a),hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,b),hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,c),nil_Ar1135217151le_alt))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_dist) ).
fof(f217,axiom,
! [X0,X1,X2,X3,X4] :
( ( is_Arr723427730le_alt(X0)
& is_Arr723427730le_alt(X1)
& is_Arr723427730le_alt(X3)
& is_Arr723427730le_alt(X4) )
=> ( X3 != X4
=> ( hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,X2),arrow_912654623le_Lin))
=> ( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X1)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,X2),X3),X4)))
<=> ( X0 != X1
& ( X1 = X3
=> hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X4)),X2)) )
& ( X1 != X3
=> ( ( X0 = X3
=> ( X1 = X4
| hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X4),X1)),X2)) ) )
& ( X0 != X3
=> hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X1)),X2)) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_in__below) ).
fof(f243,axiom,
! [X0,X1] : hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X0),X1) != nil_Ar1135217151le_alt,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_list_Osimps_I3_J) ).
fof(f248,axiom,
! [X0,X1] : X0 != hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X1),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_43_not__Cons__self) ).
fof(f319,axiom,
! [X0,X1,X2,X3] :
( hBOOL(hAPP_f147218624l_bool(hAPP_f621397159l_bool(member1265098019t_bool,X1),pi_Arr1801471756t_bool(X2,hAPP_f1639180358l_bool(cOMBK_350223551e_indi,X3))))
=> ( hBOOL(hAPP_f160177134l_bool(hAPP_A45661955l_bool(member161528657e_indi,X0),X2))
=> hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,hAPP_A340536322t_bool(X1,X0)),X3)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_114_funcset__mem) ).
fof(f467,axiom,
! [X0] : insert1969589781le_alt(X0,nil_Ar1135217151le_alt) = hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X0),nil_Ar1135217151le_alt),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_262_insert__Nil) ).
fof(f494,axiom,
arrow_583275979e_Prof = pi_Arr1801471756t_bool(top_to207207712i_bool,hAPP_f1639180358l_bool(cOMBK_350223551e_indi,arrow_912654623le_Lin)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_289_Prof__def) ).
fof(f499,axiom,
! [X0,X1] :
( X1 != nil_Ar1135217151le_alt
=> last_A1066338328le_alt(hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X0),X1)) = last_A1066338328le_alt(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_294_last__ConsR) ).
fof(f513,axiom,
! [X0,X1] :
( is_Arr723427730le_alt(X0)
=> ( ( X1 = nil_Ar1135217151le_alt
=> last_A1066338328le_alt(hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X0),X1)) = X0 )
& ( X1 != nil_Ar1135217151le_alt
=> last_A1066338328le_alt(hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X0),X1)) = last_A1066338328le_alt(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_308_last_Osimps) ).
fof(f529,axiom,
! [X0] : hBOOL(hAPP_f160177134l_bool(hAPP_A45661955l_bool(member161528657e_indi,X0),top_to207207712i_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_324_iso__tuple__UNIV__I) ).
fof(f761,axiom,
! [X0,X1] :
( hBOOL(hAPP_l300482276t_bool(distin85347314le_alt,hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X0),X1)))
<=> ( ~ hBOOL(hAPP_f87553445l_bool(hAPP_A86021709l_bool(member2080870050le_alt,X0),set_Ar426477344le_alt(X1)))
& hBOOL(hAPP_l300482276t_bool(distin85347314le_alt,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_556_distinct_Osimps_I2_J) ).
fof(f777,axiom,
! [X0] :
( X0 != nil_Ar1135217151le_alt
=> hBOOL(hAPP_f87553445l_bool(hAPP_A86021709l_bool(member2080870050le_alt,last_A1066338328le_alt(X0)),set_Ar426477344le_alt(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_572_last__in__set) ).
fof(f1012,conjecture,
! [X0] :
( is_Arr859726945e_indi(X0)
=> ( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,a),b)),hAPP_A340536322t_bool(p,X0)))
<=> hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,a),c)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,hAPP_A340536322t_bool(p,X0)),c),b))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f1013,negated_conjecture,
~ ! [X0] :
( is_Arr859726945e_indi(X0)
=> ( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,a),b)),hAPP_A340536322t_bool(p,X0)))
<=> hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,a),c)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,hAPP_A340536322t_bool(p,X0)),c),b))) ) ),
inference(negated_conjecture,[status(cth)],[f1012]) ).
fof(f1121,plain,
! [X0,X1,X2,X3,X4] :
( ( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X1)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,X2),X3),X4)))
<=> ( X0 != X1
& ( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X4)),X2))
| X1 != X3 )
& ( ( ( X1 = X4
| hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X4),X1)),X2))
| X0 != X3 )
& ( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X1)),X2))
| X0 = X3 ) )
| X1 = X3 ) ) )
| ~ hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,X2),arrow_912654623le_Lin))
| X3 = X4
| ~ is_Arr723427730le_alt(X0)
| ~ is_Arr723427730le_alt(X1)
| ~ is_Arr723427730le_alt(X3)
| ~ is_Arr723427730le_alt(X4) ),
inference(ennf_transformation,[],[f217]) ).
fof(f1122,plain,
! [X0,X1,X2,X3,X4] :
( ( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X1)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,X2),X3),X4)))
<=> ( X0 != X1
& ( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X4)),X2))
| X1 != X3 )
& ( ( ( X1 = X4
| hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X4),X1)),X2))
| X0 != X3 )
& ( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X1)),X2))
| X0 = X3 ) )
| X1 = X3 ) ) )
| ~ hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,X2),arrow_912654623le_Lin))
| X3 = X4
| ~ is_Arr723427730le_alt(X0)
| ~ is_Arr723427730le_alt(X1)
| ~ is_Arr723427730le_alt(X3)
| ~ is_Arr723427730le_alt(X4) ),
inference(flattening,[],[f1121]) ).
fof(f1292,plain,
! [X0,X1,X2,X3] :
( hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,hAPP_A340536322t_bool(X1,X0)),X3))
| ~ hBOOL(hAPP_f160177134l_bool(hAPP_A45661955l_bool(member161528657e_indi,X0),X2))
| ~ hBOOL(hAPP_f147218624l_bool(hAPP_f621397159l_bool(member1265098019t_bool,X1),pi_Arr1801471756t_bool(X2,hAPP_f1639180358l_bool(cOMBK_350223551e_indi,X3)))) ),
inference(ennf_transformation,[],[f319]) ).
fof(f1293,plain,
! [X0,X1,X2,X3] :
( hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,hAPP_A340536322t_bool(X1,X0)),X3))
| ~ hBOOL(hAPP_f160177134l_bool(hAPP_A45661955l_bool(member161528657e_indi,X0),X2))
| ~ hBOOL(hAPP_f147218624l_bool(hAPP_f621397159l_bool(member1265098019t_bool,X1),pi_Arr1801471756t_bool(X2,hAPP_f1639180358l_bool(cOMBK_350223551e_indi,X3)))) ),
inference(flattening,[],[f1292]) ).
fof(f1578,plain,
! [X0,X1] :
( last_A1066338328le_alt(hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X0),X1)) = last_A1066338328le_alt(X1)
| nil_Ar1135217151le_alt = X1 ),
inference(ennf_transformation,[],[f499]) ).
fof(f1580,plain,
! [X0,X1] :
( ( ( last_A1066338328le_alt(hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X0),X1)) = X0
| nil_Ar1135217151le_alt != X1 )
& ( last_A1066338328le_alt(hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X0),X1)) = last_A1066338328le_alt(X1)
| nil_Ar1135217151le_alt = X1 ) )
| ~ is_Arr723427730le_alt(X0) ),
inference(ennf_transformation,[],[f513]) ).
fof(f1801,plain,
! [X0] :
( hBOOL(hAPP_f87553445l_bool(hAPP_A86021709l_bool(member2080870050le_alt,last_A1066338328le_alt(X0)),set_Ar426477344le_alt(X0)))
| nil_Ar1135217151le_alt = X0 ),
inference(ennf_transformation,[],[f777]) ).
fof(f2001,plain,
? [X0] :
( ( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,a),b)),hAPP_A340536322t_bool(p,X0)))
<~> hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,a),c)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,hAPP_A340536322t_bool(p,X0)),c),b))) )
& is_Arr859726945e_indi(X0) ),
inference(ennf_transformation,[],[f1013]) ).
fof(f2002,definition,
! [X4,X1,X2,X3,X0] :
( sP0(X4,X1,X2,X3,X0)
<=> ( ( ( X1 = X4
| hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X4),X1)),X2))
| X0 != X3 )
& ( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X1)),X2))
| X0 = X3 ) )
| X1 = X3 ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f2003,plain,
! [X0,X1,X2,X3,X4] :
( ( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X1)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,X2),X3),X4)))
<=> ( X0 != X1
& ( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X4)),X2))
| X1 != X3 )
& sP0(X4,X1,X2,X3,X0) ) )
| ~ hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,X2),arrow_912654623le_Lin))
| X3 = X4
| ~ is_Arr723427730le_alt(X0)
| ~ is_Arr723427730le_alt(X1)
| ~ is_Arr723427730le_alt(X3)
| ~ is_Arr723427730le_alt(X4) ),
inference(definition_folding,[],[f1122,f2002]) ).
fof(f2020,plain,
! [X4,X1,X2,X3,X0] :
( ( sP0(X4,X1,X2,X3,X0)
| ( ( ( X1 != X4
& ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X4),X1)),X2))
& X0 = X3 )
| ( ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X1)),X2))
& X0 != X3 ) )
& X1 != X3 ) )
& ( ( ( X1 = X4
| hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X4),X1)),X2))
| X0 != X3 )
& ( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X1)),X2))
| X0 = X3 ) )
| X1 = X3
| ~ sP0(X4,X1,X2,X3,X0) ) ),
inference(nnf_transformation,[],[f2002]) ).
fof(f2021,plain,
! [X4,X1,X2,X3,X0] :
( ( sP0(X4,X1,X2,X3,X0)
| ( ( ( X1 != X4
& ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X4),X1)),X2))
& X0 = X3 )
| ( ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X1)),X2))
& X0 != X3 ) )
& X1 != X3 ) )
& ( ( ( X1 = X4
| hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X4),X1)),X2))
| X0 != X3 )
& ( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X1)),X2))
| X0 = X3 ) )
| X1 = X3
| ~ sP0(X4,X1,X2,X3,X0) ) ),
inference(flattening,[],[f2020]) ).
fof(f2022,plain,
! [X0,X1,X2,X3,X4] :
( ( sP0(X0,X1,X2,X3,X4)
| ( ( ( X0 != X1
& ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X1)),X2))
& X3 = X4 )
| ( ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X4),X1)),X2))
& X3 != X4 ) )
& X1 != X3 ) )
& ( ( ( X0 = X1
| hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X1)),X2))
| X3 != X4 )
& ( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X4),X1)),X2))
| X3 = X4 ) )
| X1 = X3
| ~ sP0(X0,X1,X2,X3,X4) ) ),
inference(rectify,[],[f2021]) ).
fof(f2023,plain,
! [X0,X1,X2,X3,X4] :
( ( ( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X1)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,X2),X3),X4)))
| X0 = X1
| ( ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X4)),X2))
& X1 = X3 )
| ~ sP0(X4,X1,X2,X3,X0) )
& ( ( X0 != X1
& ( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X4)),X2))
| X1 != X3 )
& sP0(X4,X1,X2,X3,X0) )
| ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X1)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,X2),X3),X4))) ) )
| ~ hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,X2),arrow_912654623le_Lin))
| X3 = X4
| ~ is_Arr723427730le_alt(X0)
| ~ is_Arr723427730le_alt(X1)
| ~ is_Arr723427730le_alt(X3)
| ~ is_Arr723427730le_alt(X4) ),
inference(nnf_transformation,[],[f2003]) ).
fof(f2024,plain,
! [X0,X1,X2,X3,X4] :
( ( ( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X1)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,X2),X3),X4)))
| X0 = X1
| ( ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X4)),X2))
& X1 = X3 )
| ~ sP0(X4,X1,X2,X3,X0) )
& ( ( X0 != X1
& ( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X4)),X2))
| X1 != X3 )
& sP0(X4,X1,X2,X3,X0) )
| ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X1)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,X2),X3),X4))) ) )
| ~ hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,X2),arrow_912654623le_Lin))
| X3 = X4
| ~ is_Arr723427730le_alt(X0)
| ~ is_Arr723427730le_alt(X1)
| ~ is_Arr723427730le_alt(X3)
| ~ is_Arr723427730le_alt(X4) ),
inference(flattening,[],[f2023]) ).
fof(f2339,plain,
! [X0,X1] :
( ( hBOOL(hAPP_l300482276t_bool(distin85347314le_alt,hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X0),X1)))
| hBOOL(hAPP_f87553445l_bool(hAPP_A86021709l_bool(member2080870050le_alt,X0),set_Ar426477344le_alt(X1)))
| ~ hBOOL(hAPP_l300482276t_bool(distin85347314le_alt,X1)) )
& ( ( ~ hBOOL(hAPP_f87553445l_bool(hAPP_A86021709l_bool(member2080870050le_alt,X0),set_Ar426477344le_alt(X1)))
& hBOOL(hAPP_l300482276t_bool(distin85347314le_alt,X1)) )
| ~ hBOOL(hAPP_l300482276t_bool(distin85347314le_alt,hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X0),X1))) ) ),
inference(nnf_transformation,[],[f761]) ).
fof(f2340,plain,
! [X0,X1] :
( ( hBOOL(hAPP_l300482276t_bool(distin85347314le_alt,hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X0),X1)))
| hBOOL(hAPP_f87553445l_bool(hAPP_A86021709l_bool(member2080870050le_alt,X0),set_Ar426477344le_alt(X1)))
| ~ hBOOL(hAPP_l300482276t_bool(distin85347314le_alt,X1)) )
& ( ( ~ hBOOL(hAPP_f87553445l_bool(hAPP_A86021709l_bool(member2080870050le_alt,X0),set_Ar426477344le_alt(X1)))
& hBOOL(hAPP_l300482276t_bool(distin85347314le_alt,X1)) )
| ~ hBOOL(hAPP_l300482276t_bool(distin85347314le_alt,hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X0),X1))) ) ),
inference(flattening,[],[f2339]) ).
fof(f2414,plain,
? [X0] :
( ( ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,a),c)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,hAPP_A340536322t_bool(p,X0)),c),b)))
| ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,a),b)),hAPP_A340536322t_bool(p,X0))) )
& ( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,a),c)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,hAPP_A340536322t_bool(p,X0)),c),b)))
| hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,a),b)),hAPP_A340536322t_bool(p,X0))) )
& is_Arr859726945e_indi(X0) ),
inference(nnf_transformation,[],[f2001]) ).
fof(f2415,plain,
? [X0] :
( ( ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,a),c)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,hAPP_A340536322t_bool(p,X0)),c),b)))
| ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,a),b)),hAPP_A340536322t_bool(p,X0))) )
& ( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,a),c)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,hAPP_A340536322t_bool(p,X0)),c),b)))
| hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,a),b)),hAPP_A340536322t_bool(p,X0))) )
& is_Arr859726945e_indi(X0) ),
inference(flattening,[],[f2414]) ).
fof(f2416,plain,
( ( ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,a),c)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,hAPP_A340536322t_bool(p,sK296)),c),b)))
| ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,a),b)),hAPP_A340536322t_bool(p,sK296))) )
& ( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,a),c)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,hAPP_A340536322t_bool(p,sK296)),c),b)))
| hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,a),b)),hAPP_A340536322t_bool(p,sK296))) )
& is_Arr859726945e_indi(sK296) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK296]),skolemize(X0,sK296)],[f2415]) ).
fof(f2618,plain,
is_Arr723427730le_alt(a),
inference(cnf_transformation,[],[f202]) ).
fof(f2619,plain,
is_Arr723427730le_alt(b),
inference(cnf_transformation,[],[f203]) ).
fof(f2620,plain,
is_Arr723427730le_alt(c),
inference(cnf_transformation,[],[f204]) ).
fof(f2621,plain,
hBOOL(hAPP_f147218624l_bool(hAPP_f621397159l_bool(member1265098019t_bool,p),arrow_583275979e_Prof)),
inference(cnf_transformation,[],[f205]) ).
fof(f2625,plain,
hBOOL(hAPP_l300482276t_bool(distin85347314le_alt,hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,a),hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,b),hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,c),nil_Ar1135217151le_alt))))),
inference(cnf_transformation,[],[f209]) ).
fof(f2649,plain,
! [X2,X3,X0,X1,X4] :
( sP0(X0,X1,X2,X3,X4)
| X1 != X3 ),
inference(cnf_transformation,[],[f2022]) ).
fof(f2657,plain,
! [X2,X3,X0,X1,X4] :
( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X4)),X2))
| X1 != X3
| ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X1)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,X2),X3),X4)))
| ~ hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,X2),arrow_912654623le_Lin))
| X3 = X4
| ~ is_Arr723427730le_alt(X0)
| ~ is_Arr723427730le_alt(X1)
| ~ is_Arr723427730le_alt(X3)
| ~ is_Arr723427730le_alt(X4) ),
inference(cnf_transformation,[],[f2024]) ).
fof(f2660,plain,
! [X2,X3,X0,X1,X4] :
( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X1)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,X2),X3),X4)))
| X0 = X1
| ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X4)),X2))
| ~ sP0(X4,X1,X2,X3,X0)
| ~ hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,X2),arrow_912654623le_Lin))
| X3 = X4
| ~ is_Arr723427730le_alt(X0)
| ~ is_Arr723427730le_alt(X1)
| ~ is_Arr723427730le_alt(X3)
| ~ is_Arr723427730le_alt(X4) ),
inference(cnf_transformation,[],[f2024]) ).
fof(f2747,plain,
! [X0,X1] : nil_Ar1135217151le_alt != hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X0),X1),
inference(cnf_transformation,[],[f243]) ).
fof(f2758,plain,
! [X0,X1] : hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X1),X0) != X0,
inference(cnf_transformation,[],[f248]) ).
fof(f2841,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP_f147218624l_bool(hAPP_f621397159l_bool(member1265098019t_bool,X1),pi_Arr1801471756t_bool(X2,hAPP_f1639180358l_bool(cOMBK_350223551e_indi,X3))))
| ~ hBOOL(hAPP_f160177134l_bool(hAPP_A45661955l_bool(member161528657e_indi,X0),X2))
| hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,hAPP_A340536322t_bool(X1,X0)),X3)) ),
inference(cnf_transformation,[],[f1293]) ).
fof(f3209,plain,
! [X0] : hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X0),nil_Ar1135217151le_alt) = insert1969589781le_alt(X0,nil_Ar1135217151le_alt),
inference(cnf_transformation,[],[f467]) ).
fof(f3256,plain,
arrow_583275979e_Prof = pi_Arr1801471756t_bool(top_to207207712i_bool,hAPP_f1639180358l_bool(cOMBK_350223551e_indi,arrow_912654623le_Lin)),
inference(cnf_transformation,[],[f494]) ).
fof(f3267,plain,
! [X0,X1] :
( last_A1066338328le_alt(hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X0),X1)) = last_A1066338328le_alt(X1)
| nil_Ar1135217151le_alt = X1 ),
inference(cnf_transformation,[],[f1578]) ).
fof(f3284,plain,
! [X0,X1] :
( last_A1066338328le_alt(hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X0),X1)) = X0
| nil_Ar1135217151le_alt != X1
| ~ is_Arr723427730le_alt(X0) ),
inference(cnf_transformation,[],[f1580]) ).
fof(f3309,plain,
! [X0] : hBOOL(hAPP_f160177134l_bool(hAPP_A45661955l_bool(member161528657e_indi,X0),top_to207207712i_bool)),
inference(cnf_transformation,[],[f529]) ).
fof(f3731,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_l300482276t_bool(distin85347314le_alt,hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X0),X1)))
| hBOOL(hAPP_l300482276t_bool(distin85347314le_alt,X1)) ),
inference(cnf_transformation,[],[f2340]) ).
fof(f3732,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_l300482276t_bool(distin85347314le_alt,hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X0),X1)))
| ~ hBOOL(hAPP_f87553445l_bool(hAPP_A86021709l_bool(member2080870050le_alt,X0),set_Ar426477344le_alt(X1))) ),
inference(cnf_transformation,[],[f2340]) ).
fof(f3763,plain,
! [X0] :
( hBOOL(hAPP_f87553445l_bool(hAPP_A86021709l_bool(member2080870050le_alt,last_A1066338328le_alt(X0)),set_Ar426477344le_alt(X0)))
| nil_Ar1135217151le_alt = X0 ),
inference(cnf_transformation,[],[f1801]) ).
fof(f4130,plain,
( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,a),c)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,hAPP_A340536322t_bool(p,sK296)),c),b)))
| hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,a),b)),hAPP_A340536322t_bool(p,sK296))) ),
inference(cnf_transformation,[],[f2416]) ).
fof(f4131,plain,
( ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,a),c)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,hAPP_A340536322t_bool(p,sK296)),c),b)))
| ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,a),b)),hAPP_A340536322t_bool(p,sK296))) ),
inference(cnf_transformation,[],[f2416]) ).
fof(f4196,plain,
! [X2,X3,X0,X4] : sP0(X0,X3,X2,X3,X4),
inference(equality_resolution,[],[f2649]) ).
fof(f4199,plain,
! [X2,X3,X0,X4] :
( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X4)),X2))
| ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X3)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,X2),X3),X4)))
| ~ hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,X2),arrow_912654623le_Lin))
| X3 = X4
| ~ is_Arr723427730le_alt(X0)
| ~ is_Arr723427730le_alt(X3)
| ~ is_Arr723427730le_alt(X3)
| ~ is_Arr723427730le_alt(X4) ),
inference(equality_resolution,[],[f2657]) ).
fof(f4227,plain,
! [X0] :
( ~ is_Arr723427730le_alt(X0)
| last_A1066338328le_alt(hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X0),nil_Ar1135217151le_alt)) = X0 ),
inference(equality_resolution,[],[f3284]) ).
fof(f4328,definition,
sF297 = hAPP_A1171966089le_alt(produc1456060119le_alt,a),
introduced(definition,[new_symbols(definition,[sF297])],[function_definition]) ).
fof(f4329,plain,
hAPP_A1171966089le_alt(produc1456060119le_alt,a) = sF297,
inference(reorient_equations,[],[f4328]) ).
fof(f4330,definition,
sF298 = hAPP_A1561816353le_alt(sF297,c),
introduced(definition,[new_symbols(definition,[sF298])],[function_definition]) ).
fof(f4331,plain,
hAPP_A1561816353le_alt(sF297,c) = sF298,
inference(reorient_equations,[],[f4330]) ).
fof(f4332,definition,
sF299 = hAPP_P1151433609l_bool(member720722004le_alt,sF298),
introduced(definition,[new_symbols(definition,[sF299])],[function_definition]) ).
fof(f4333,plain,
hAPP_P1151433609l_bool(member720722004le_alt,sF298) = sF299,
inference(reorient_equations,[],[f4332]) ).
fof(f4334,definition,
sF300 = hAPP_A340536322t_bool(p,sK296),
introduced(definition,[new_symbols(definition,[sF300])],[function_definition]) ).
fof(f4335,plain,
hAPP_A340536322t_bool(p,sK296) = sF300,
inference(reorient_equations,[],[f4334]) ).
fof(f4336,definition,
sF301 = hAPP_f684072049t_bool(arrow_207701375_below,sF300),
introduced(definition,[new_symbols(definition,[sF301])],[function_definition]) ).
fof(f4337,plain,
hAPP_f684072049t_bool(arrow_207701375_below,sF300) = sF301,
inference(reorient_equations,[],[f4336]) ).
fof(f4338,definition,
sF302 = hAPP_A28770973t_bool(sF301,c),
introduced(definition,[new_symbols(definition,[sF302])],[function_definition]) ).
fof(f4339,plain,
hAPP_A28770973t_bool(sF301,c) = sF302,
inference(reorient_equations,[],[f4338]) ).
fof(f4340,definition,
sF303 = hAPP_A1014090479t_bool(sF302,b),
introduced(definition,[new_symbols(definition,[sF303])],[function_definition]) ).
fof(f4341,plain,
hAPP_A1014090479t_bool(sF302,b) = sF303,
inference(reorient_equations,[],[f4340]) ).
fof(f4342,definition,
sF304 = hAPP_f1733357041l_bool(sF299,sF303),
introduced(definition,[new_symbols(definition,[sF304])],[function_definition]) ).
fof(f4343,plain,
hAPP_f1733357041l_bool(sF299,sF303) = sF304,
inference(reorient_equations,[],[f4342]) ).
fof(f4344,definition,
sF305 = hAPP_A1561816353le_alt(sF297,b),
introduced(definition,[new_symbols(definition,[sF305])],[function_definition]) ).
fof(f4345,plain,
hAPP_A1561816353le_alt(sF297,b) = sF305,
inference(reorient_equations,[],[f4344]) ).
fof(f4346,definition,
sF306 = hAPP_P1151433609l_bool(member720722004le_alt,sF305),
introduced(definition,[new_symbols(definition,[sF306])],[function_definition]) ).
fof(f4347,plain,
hAPP_P1151433609l_bool(member720722004le_alt,sF305) = sF306,
inference(reorient_equations,[],[f4346]) ).
fof(f4348,definition,
sF307 = hAPP_f1733357041l_bool(sF306,sF300),
introduced(definition,[new_symbols(definition,[sF307])],[function_definition]) ).
fof(f4349,plain,
hAPP_f1733357041l_bool(sF306,sF300) = sF307,
inference(reorient_equations,[],[f4348]) ).
fof(f4350,plain,
( ~ hBOOL(sF304)
| ~ hBOOL(sF307) ),
inference(definition_folding,[],[f4131,f4349,f4335,f4347,f4345,f4329,f4343,f4341,f4339,f4337,f4335,f4333,f4331,f4329]) ).
fof(f4351,plain,
( hBOOL(sF304)
| hBOOL(sF307) ),
inference(definition_folding,[],[f4130,f4349,f4335,f4347,f4345,f4329,f4343,f4341,f4339,f4337,f4335,f4333,f4331,f4329]) ).
fof(f4367,plain,
! [X2,X3,X0,X4] :
( ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X3)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,X2),X3),X4)))
| hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(hAPP_A1171966089le_alt(produc1456060119le_alt,X0),X4)),X2))
| ~ hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,X2),arrow_912654623le_Lin))
| X3 = X4
| ~ is_Arr723427730le_alt(X0)
| ~ is_Arr723427730le_alt(X3)
| ~ is_Arr723427730le_alt(X4) ),
inference(duplicate_literal_removal,[],[f4199]) ).
fof(f4378,definition,
( spl308_1
<=> hBOOL(sF307) ),
introduced(definition,[new_symbols(definition,[spl308_1])],[avatar_definition]) ).
fof(f4379,plain,
( ~ hBOOL(sF307)
| spl308_1 ),
inference(avatar_component_clause,[],[f4378]) ).
fof(f4380,plain,
( hBOOL(sF307)
| ~ spl308_1 ),
inference(avatar_component_clause,[],[f4378]) ).
fof(f4382,definition,
( spl308_2
<=> hBOOL(sF304) ),
introduced(definition,[new_symbols(definition,[spl308_2])],[avatar_definition]) ).
fof(f4383,plain,
( ~ hBOOL(sF304)
| spl308_2 ),
inference(avatar_component_clause,[],[f4382]) ).
fof(f4384,plain,
( hBOOL(sF304)
| ~ spl308_2 ),
inference(avatar_component_clause,[],[f4382]) ).
fof(f4385,plain,
( spl308_1
| spl308_2 ),
inference(avatar_split_clause,[],[f4351,f4382,f4378]) ).
fof(f4386,plain,
( ~ spl308_1
| ~ spl308_2 ),
inference(avatar_split_clause,[],[f4350,f4382,f4378]) ).
fof(f4450,plain,
hBOOL(hAPP_l300482276t_bool(distin85347314le_alt,hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,a),hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,b),insert1969589781le_alt(c,nil_Ar1135217151le_alt))))),
inference(forward_demodulation,[],[f2625,f3209]) ).
fof(f4453,definition,
( spl308_16
<=> hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,sF300),arrow_912654623le_Lin)) ),
introduced(definition,[new_symbols(definition,[spl308_16])],[avatar_definition]) ).
fof(f4454,plain,
( hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,sF300),arrow_912654623le_Lin))
| ~ spl308_16 ),
inference(avatar_component_clause,[],[f4453]) ).
fof(f4455,plain,
( ~ hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,sF300),arrow_912654623le_Lin))
| spl308_16 ),
inference(avatar_component_clause,[],[f4453]) ).
fof(f4469,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X0)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,X1),X0),X2)))
| hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X2)),X1))
| ~ hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,X1),arrow_912654623le_Lin))
| X0 = X2
| ~ is_Arr723427730le_alt(a)
| ~ is_Arr723427730le_alt(X0)
| ~ is_Arr723427730le_alt(X2) ),
inference(superposition,[],[f4367,f4329]) ).
fof(f4474,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X0)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,X1),X0),X2)))
| hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X2)),X1))
| ~ hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,X1),arrow_912654623le_Lin))
| X0 = X2
| ~ is_Arr723427730le_alt(X0)
| ~ is_Arr723427730le_alt(X2) ),
inference(forward_subsumption_resolution,[],[f4469,f2618]) ).
fof(f4483,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,sF298),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,X0),c),X1)))
| hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X1)),X0))
| ~ hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,X0),arrow_912654623le_Lin))
| c = X1
| ~ is_Arr723427730le_alt(c)
| ~ is_Arr723427730le_alt(X1) ),
inference(superposition,[],[f4474,f4331]) ).
fof(f4487,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,sF298),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,X0),c),X1)))
| hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X1)),X0))
| ~ hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,X0),arrow_912654623le_Lin))
| c = X1
| ~ is_Arr723427730le_alt(X1) ),
inference(forward_subsumption_resolution,[],[f4483,f2620]) ).
fof(f4489,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_f1733357041l_bool(sF299,hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,X0),c),X1)))
| hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X1)),X0))
| ~ hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,X0),arrow_912654623le_Lin))
| c = X1
| ~ is_Arr723427730le_alt(X1) ),
inference(forward_demodulation,[],[f4487,f4333]) ).
fof(f4491,plain,
! [X0] :
( ~ hBOOL(hAPP_f1733357041l_bool(sF299,hAPP_A1014090479t_bool(hAPP_A28770973t_bool(sF301,c),X0)))
| hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X0)),sF300))
| ~ hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,sF300),arrow_912654623le_Lin))
| c = X0
| ~ is_Arr723427730le_alt(X0) ),
inference(superposition,[],[f4489,f4337]) ).
fof(f4503,definition,
( spl308_18
<=> a = c ),
introduced(definition,[new_symbols(definition,[spl308_18])],[avatar_definition]) ).
fof(f4504,plain,
( a != c
| spl308_18 ),
inference(avatar_component_clause,[],[f4503]) ).
fof(f4505,plain,
( a = c
| ~ spl308_18 ),
inference(avatar_component_clause,[],[f4503]) ).
fof(f4523,plain,
! [X2,X3,X0,X1] :
( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X0)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,X1),X2),X3)))
| a = X0
| ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X3)),X1))
| ~ sP0(X3,X0,X1,X2,a)
| ~ hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,X1),arrow_912654623le_Lin))
| X2 = X3
| ~ is_Arr723427730le_alt(a)
| ~ is_Arr723427730le_alt(X0)
| ~ is_Arr723427730le_alt(X2)
| ~ is_Arr723427730le_alt(X3) ),
inference(superposition,[],[f2660,f4329]) ).
fof(f4526,plain,
! [X2,X3,X0,X1] :
( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X0)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(hAPP_f684072049t_bool(arrow_207701375_below,X1),X2),X3)))
| a = X0
| ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X3)),X1))
| ~ sP0(X3,X0,X1,X2,a)
| ~ hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,X1),arrow_912654623le_Lin))
| X2 = X3
| ~ is_Arr723427730le_alt(X0)
| ~ is_Arr723427730le_alt(X2)
| ~ is_Arr723427730le_alt(X3) ),
inference(forward_subsumption_resolution,[],[f4523,f2618]) ).
fof(f4530,plain,
! [X2,X0,X1] :
( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X0)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(sF301,X1),X2)))
| a = X0
| ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X2)),sF300))
| ~ sP0(X2,X0,sF300,X1,a)
| ~ hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,sF300),arrow_912654623le_Lin))
| X1 = X2
| ~ is_Arr723427730le_alt(X0)
| ~ is_Arr723427730le_alt(X1)
| ~ is_Arr723427730le_alt(X2) ),
inference(superposition,[],[f4526,f4337]) ).
fof(f4578,plain,
hBOOL(hAPP_l300482276t_bool(distin85347314le_alt,hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,b),insert1969589781le_alt(c,nil_Ar1135217151le_alt)))),
inference(resolution,[],[f3731,f4450]) ).
fof(f4618,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_f147218624l_bool(hAPP_f621397159l_bool(member1265098019t_bool,X0),arrow_583275979e_Prof))
| ~ hBOOL(hAPP_f160177134l_bool(hAPP_A45661955l_bool(member161528657e_indi,X1),top_to207207712i_bool))
| hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,hAPP_A340536322t_bool(X0,X1)),arrow_912654623le_Lin)) ),
inference(superposition,[],[f2841,f3256]) ).
fof(f4619,plain,
! [X0,X1] :
( hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,hAPP_A340536322t_bool(X0,X1)),arrow_912654623le_Lin))
| ~ hBOOL(hAPP_f147218624l_bool(hAPP_f621397159l_bool(member1265098019t_bool,X0),arrow_583275979e_Prof)) ),
inference(forward_subsumption_resolution,[],[f4618,f3309]) ).
fof(f4620,plain,
( hBOOL(hAPP_f560517119l_bool(hAPP_f1332197581l_bool(member1704306684t_bool,sF300),arrow_912654623le_Lin))
| ~ hBOOL(hAPP_f147218624l_bool(hAPP_f621397159l_bool(member1265098019t_bool,p),arrow_583275979e_Prof)) ),
inference(superposition,[],[f4619,f4335]) ).
fof(f4621,plain,
( ~ hBOOL(hAPP_f147218624l_bool(hAPP_f621397159l_bool(member1265098019t_bool,p),arrow_583275979e_Prof))
| spl308_16 ),
inference(forward_subsumption_resolution,[],[f4620,f4455]) ).
fof(f4622,plain,
( $false
| spl308_16 ),
inference(forward_subsumption_resolution,[],[f4621,f2621]) ).
fof(f4623,plain,
spl308_16,
inference(avatar_contradiction_clause,[],[f4622]) ).
fof(f4628,plain,
( ! [X0] :
( ~ hBOOL(hAPP_f1733357041l_bool(sF299,hAPP_A1014090479t_bool(hAPP_A28770973t_bool(sF301,c),X0)))
| hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X0)),sF300))
| c = X0
| ~ is_Arr723427730le_alt(X0) )
| ~ spl308_16 ),
inference(forward_subsumption_resolution,[],[f4491,f4454]) ).
fof(f4631,plain,
( ! [X2,X0,X1] :
( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X0)),hAPP_A1014090479t_bool(hAPP_A28770973t_bool(sF301,X1),X2)))
| a = X0
| ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X2)),sF300))
| ~ sP0(X2,X0,sF300,X1,a)
| X1 = X2
| ~ is_Arr723427730le_alt(X0)
| ~ is_Arr723427730le_alt(X1)
| ~ is_Arr723427730le_alt(X2) )
| ~ spl308_16 ),
inference(forward_subsumption_resolution,[],[f4530,f4454]) ).
fof(f4633,plain,
( ! [X0] :
( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X0)),sF300))
| ~ hBOOL(hAPP_f1733357041l_bool(sF299,hAPP_A1014090479t_bool(sF302,X0)))
| c = X0
| ~ is_Arr723427730le_alt(X0) )
| ~ spl308_16 ),
inference(forward_demodulation,[],[f4628,f4339]) ).
fof(f4694,plain,
( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,sF305),sF300))
| ~ hBOOL(hAPP_f1733357041l_bool(sF299,hAPP_A1014090479t_bool(sF302,b)))
| b = c
| ~ is_Arr723427730le_alt(b)
| ~ spl308_16 ),
inference(superposition,[],[f4633,f4345]) ).
fof(f4695,plain,
( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,sF305),sF300))
| ~ hBOOL(hAPP_f1733357041l_bool(sF299,hAPP_A1014090479t_bool(sF302,b)))
| b = c
| ~ spl308_16 ),
inference(forward_subsumption_resolution,[],[f4694,f2619]) ).
fof(f4696,plain,
( hBOOL(hAPP_f1733357041l_bool(sF306,sF300))
| ~ hBOOL(hAPP_f1733357041l_bool(sF299,hAPP_A1014090479t_bool(sF302,b)))
| b = c
| ~ spl308_16 ),
inference(forward_demodulation,[],[f4695,f4347]) ).
fof(f4697,plain,
( hBOOL(sF307)
| ~ hBOOL(hAPP_f1733357041l_bool(sF299,hAPP_A1014090479t_bool(sF302,b)))
| b = c
| ~ spl308_16 ),
inference(forward_demodulation,[],[f4696,f4349]) ).
fof(f4698,plain,
( ~ hBOOL(hAPP_f1733357041l_bool(sF299,hAPP_A1014090479t_bool(sF302,b)))
| b = c
| spl308_1
| ~ spl308_16 ),
inference(forward_subsumption_resolution,[],[f4697,f4379]) ).
fof(f4699,plain,
( ~ hBOOL(hAPP_f1733357041l_bool(sF299,sF303))
| b = c
| spl308_1
| ~ spl308_16 ),
inference(forward_demodulation,[],[f4698,f4341]) ).
fof(f4700,plain,
( ~ hBOOL(sF304)
| b = c
| spl308_1
| ~ spl308_16 ),
inference(forward_demodulation,[],[f4699,f4343]) ).
fof(f4701,plain,
( b = c
| spl308_1
| ~ spl308_2
| ~ spl308_16 ),
inference(forward_subsumption_resolution,[],[f4700,f4384]) ).
fof(f4735,plain,
~ hBOOL(hAPP_f87553445l_bool(hAPP_A86021709l_bool(member2080870050le_alt,a),set_Ar426477344le_alt(hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,b),insert1969589781le_alt(c,nil_Ar1135217151le_alt))))),
inference(resolution,[],[f3732,f4450]) ).
fof(f4738,plain,
~ hBOOL(hAPP_f87553445l_bool(hAPP_A86021709l_bool(member2080870050le_alt,b),set_Ar426477344le_alt(insert1969589781le_alt(c,nil_Ar1135217151le_alt)))),
inference(resolution,[],[f3732,f4578]) ).
fof(f4739,plain,
( ~ hBOOL(hAPP_f87553445l_bool(hAPP_A86021709l_bool(member2080870050le_alt,b),set_Ar426477344le_alt(insert1969589781le_alt(b,nil_Ar1135217151le_alt))))
| spl308_1
| ~ spl308_2
| ~ spl308_16 ),
inference(forward_demodulation,[],[f4738,f4701]) ).
fof(f4749,plain,
! [X0] : nil_Ar1135217151le_alt != insert1969589781le_alt(X0,nil_Ar1135217151le_alt),
inference(superposition,[],[f2758,f3209]) ).
fof(f4772,plain,
b = last_A1066338328le_alt(hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,b),nil_Ar1135217151le_alt)),
inference(resolution,[],[f4227,f2619]) ).
fof(f4773,plain,
a = last_A1066338328le_alt(hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,a),nil_Ar1135217151le_alt)),
inference(resolution,[],[f4227,f2618]) ).
fof(f4774,plain,
a = last_A1066338328le_alt(insert1969589781le_alt(a,nil_Ar1135217151le_alt)),
inference(forward_demodulation,[],[f4773,f3209]) ).
fof(f4775,plain,
b = last_A1066338328le_alt(insert1969589781le_alt(b,nil_Ar1135217151le_alt)),
inference(forward_demodulation,[],[f4772,f3209]) ).
fof(f4778,plain,
( hBOOL(hAPP_f87553445l_bool(hAPP_A86021709l_bool(member2080870050le_alt,b),set_Ar426477344le_alt(insert1969589781le_alt(b,nil_Ar1135217151le_alt))))
| nil_Ar1135217151le_alt = insert1969589781le_alt(b,nil_Ar1135217151le_alt) ),
inference(superposition,[],[f3763,f4775]) ).
fof(f4779,plain,
( nil_Ar1135217151le_alt = insert1969589781le_alt(b,nil_Ar1135217151le_alt)
| spl308_1
| ~ spl308_2
| ~ spl308_16 ),
inference(forward_subsumption_resolution,[],[f4778,f4739]) ).
fof(f4780,plain,
( $false
| spl308_1
| ~ spl308_2
| ~ spl308_16 ),
inference(forward_subsumption_resolution,[],[f4779,f4749]) ).
fof(f4781,plain,
( spl308_1
| ~ spl308_2
| ~ spl308_16 ),
inference(avatar_contradiction_clause,[],[f4780]) ).
fof(f4783,plain,
hBOOL(hAPP_f87553445l_bool(hAPP_A86021709l_bool(member2080870050le_alt,b),set_Ar426477344le_alt(insert1969589781le_alt(b,nil_Ar1135217151le_alt)))),
inference(forward_subsumption_resolution,[],[f4778,f4749]) ).
fof(f4785,definition,
( spl308_20
<=> b = c ),
introduced(definition,[new_symbols(definition,[spl308_20])],[avatar_definition]) ).
fof(f4786,plain,
( b != c
| spl308_20 ),
inference(avatar_component_clause,[],[f4785]) ).
fof(f4787,plain,
( b = c
| ~ spl308_20 ),
inference(avatar_component_clause,[],[f4785]) ).
fof(f4856,plain,
( ! [X0,X1] :
( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X0)),hAPP_A1014090479t_bool(sF302,X1)))
| a = X0
| ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X1)),sF300))
| ~ sP0(X1,X0,sF300,c,a)
| c = X1
| ~ is_Arr723427730le_alt(X0)
| ~ is_Arr723427730le_alt(c)
| ~ is_Arr723427730le_alt(X1) )
| ~ spl308_16 ),
inference(superposition,[],[f4631,f4339]) ).
fof(f4860,plain,
( ! [X0,X1] :
( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X0)),hAPP_A1014090479t_bool(sF302,X1)))
| a = X0
| ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X1)),sF300))
| ~ sP0(X1,X0,sF300,c,a)
| c = X1
| ~ is_Arr723427730le_alt(X0)
| ~ is_Arr723427730le_alt(X1) )
| ~ spl308_16 ),
inference(forward_subsumption_resolution,[],[f4856,f2620]) ).
fof(f4933,plain,
! [X0,X1] :
( hBOOL(hAPP_f87553445l_bool(hAPP_A86021709l_bool(member2080870050le_alt,last_A1066338328le_alt(X0)),set_Ar426477344le_alt(hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X1),X0))))
| nil_Ar1135217151le_alt = hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X1),X0)
| nil_Ar1135217151le_alt = X0 ),
inference(superposition,[],[f3763,f3267]) ).
fof(f4934,plain,
! [X0,X1] :
( hBOOL(hAPP_f87553445l_bool(hAPP_A86021709l_bool(member2080870050le_alt,last_A1066338328le_alt(X0)),set_Ar426477344le_alt(hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X1),X0))))
| nil_Ar1135217151le_alt = X0 ),
inference(forward_subsumption_resolution,[],[f4933,f2747]) ).
fof(f4938,plain,
! [X0] :
( hBOOL(hAPP_f87553445l_bool(hAPP_A86021709l_bool(member2080870050le_alt,a),set_Ar426477344le_alt(hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X0),insert1969589781le_alt(a,nil_Ar1135217151le_alt)))))
| nil_Ar1135217151le_alt = insert1969589781le_alt(a,nil_Ar1135217151le_alt) ),
inference(superposition,[],[f4934,f4774]) ).
fof(f4947,plain,
! [X0] : hBOOL(hAPP_f87553445l_bool(hAPP_A86021709l_bool(member2080870050le_alt,a),set_Ar426477344le_alt(hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,X0),insert1969589781le_alt(a,nil_Ar1135217151le_alt))))),
inference(forward_subsumption_resolution,[],[f4938,f4749]) ).
fof(f5014,plain,
( ~ hBOOL(hAPP_f87553445l_bool(hAPP_A86021709l_bool(member2080870050le_alt,b),set_Ar426477344le_alt(insert1969589781le_alt(b,nil_Ar1135217151le_alt))))
| ~ spl308_20 ),
inference(superposition,[],[f4738,f4787]) ).
fof(f5015,plain,
( $false
| ~ spl308_20 ),
inference(forward_subsumption_resolution,[],[f5014,f4783]) ).
fof(f5016,plain,
~ spl308_20,
inference(avatar_contradiction_clause,[],[f5015]) ).
fof(f5043,plain,
( ! [X0] :
( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,sF298),hAPP_A1014090479t_bool(sF302,X0)))
| a = c
| ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X0)),sF300))
| ~ sP0(X0,c,sF300,c,a)
| c = X0
| ~ is_Arr723427730le_alt(c)
| ~ is_Arr723427730le_alt(X0) )
| ~ spl308_16 ),
inference(superposition,[],[f4860,f4331]) ).
fof(f5048,plain,
( ! [X0] :
( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,sF298),hAPP_A1014090479t_bool(sF302,X0)))
| ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X0)),sF300))
| ~ sP0(X0,c,sF300,c,a)
| c = X0
| ~ is_Arr723427730le_alt(c)
| ~ is_Arr723427730le_alt(X0) )
| ~ spl308_16
| spl308_18 ),
inference(forward_subsumption_resolution,[],[f5043,f4504]) ).
fof(f5051,plain,
( ! [X0] :
( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,sF298),hAPP_A1014090479t_bool(sF302,X0)))
| ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X0)),sF300))
| ~ sP0(X0,c,sF300,c,a)
| c = X0
| ~ is_Arr723427730le_alt(X0) )
| ~ spl308_16
| spl308_18 ),
inference(forward_subsumption_resolution,[],[f5048,f2620]) ).
fof(f5054,plain,
( ! [X0] :
( hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,sF298),hAPP_A1014090479t_bool(sF302,X0)))
| ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X0)),sF300))
| c = X0
| ~ is_Arr723427730le_alt(X0) )
| ~ spl308_16
| spl308_18 ),
inference(forward_subsumption_resolution,[],[f5051,f4196]) ).
fof(f5056,plain,
( ! [X0] :
( ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,hAPP_A1561816353le_alt(sF297,X0)),sF300))
| hBOOL(hAPP_f1733357041l_bool(sF299,hAPP_A1014090479t_bool(sF302,X0)))
| c = X0
| ~ is_Arr723427730le_alt(X0) )
| ~ spl308_16
| spl308_18 ),
inference(forward_demodulation,[],[f5054,f4333]) ).
fof(f5060,plain,
( ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,sF305),sF300))
| hBOOL(hAPP_f1733357041l_bool(sF299,hAPP_A1014090479t_bool(sF302,b)))
| b = c
| ~ is_Arr723427730le_alt(b)
| ~ spl308_16
| spl308_18 ),
inference(superposition,[],[f5056,f4345]) ).
fof(f5062,plain,
( ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,sF305),sF300))
| hBOOL(hAPP_f1733357041l_bool(sF299,hAPP_A1014090479t_bool(sF302,b)))
| ~ is_Arr723427730le_alt(b)
| ~ spl308_16
| spl308_18
| spl308_20 ),
inference(forward_subsumption_resolution,[],[f5060,f4786]) ).
fof(f5063,plain,
( ~ hBOOL(hAPP_f1733357041l_bool(hAPP_P1151433609l_bool(member720722004le_alt,sF305),sF300))
| hBOOL(hAPP_f1733357041l_bool(sF299,hAPP_A1014090479t_bool(sF302,b)))
| ~ spl308_16
| spl308_18
| spl308_20 ),
inference(forward_subsumption_resolution,[],[f5062,f2619]) ).
fof(f5064,plain,
( ~ hBOOL(hAPP_f1733357041l_bool(sF306,sF300))
| hBOOL(hAPP_f1733357041l_bool(sF299,hAPP_A1014090479t_bool(sF302,b)))
| ~ spl308_16
| spl308_18
| spl308_20 ),
inference(forward_demodulation,[],[f5063,f4347]) ).
fof(f5065,plain,
( ~ hBOOL(sF307)
| hBOOL(hAPP_f1733357041l_bool(sF299,hAPP_A1014090479t_bool(sF302,b)))
| ~ spl308_16
| spl308_18
| spl308_20 ),
inference(forward_demodulation,[],[f5064,f4349]) ).
fof(f5066,plain,
( hBOOL(hAPP_f1733357041l_bool(sF299,hAPP_A1014090479t_bool(sF302,b)))
| ~ spl308_1
| ~ spl308_16
| spl308_18
| spl308_20 ),
inference(forward_subsumption_resolution,[],[f5065,f4380]) ).
fof(f5067,plain,
( hBOOL(hAPP_f1733357041l_bool(sF299,sF303))
| ~ spl308_1
| ~ spl308_16
| spl308_18
| spl308_20 ),
inference(forward_demodulation,[],[f5066,f4341]) ).
fof(f5068,plain,
( hBOOL(sF304)
| ~ spl308_1
| ~ spl308_16
| spl308_18
| spl308_20 ),
inference(forward_demodulation,[],[f5067,f4343]) ).
fof(f5069,plain,
( $false
| ~ spl308_1
| spl308_2
| ~ spl308_16
| spl308_18
| spl308_20 ),
inference(forward_subsumption_resolution,[],[f5068,f4383]) ).
fof(f5070,plain,
( ~ spl308_1
| spl308_2
| ~ spl308_16
| spl308_18
| spl308_20 ),
inference(avatar_contradiction_clause,[],[f5069]) ).
fof(f5079,plain,
( ~ hBOOL(hAPP_f87553445l_bool(hAPP_A86021709l_bool(member2080870050le_alt,a),set_Ar426477344le_alt(hAPP_l372964747le_alt(hAPP_A1660609715le_alt(cons_A77766063le_alt,b),insert1969589781le_alt(a,nil_Ar1135217151le_alt)))))
| ~ spl308_18 ),
inference(superposition,[],[f4735,f4505]) ).
fof(f5088,plain,
( $false
| ~ spl308_18 ),
inference(forward_subsumption_resolution,[],[f5079,f4947]) ).
fof(f5089,plain,
~ spl308_18,
inference(avatar_contradiction_clause,[],[f5088]) ).
cnf(s1,plain,
( spl308_1
| spl308_2 ),
inference(sat_conversion,[],[f4385]) ).
cnf(s2,plain,
( ~ spl308_1
| ~ spl308_2 ),
inference(sat_conversion,[],[f4386]) ).
cnf(s23,plain,
spl308_16,
inference(sat_conversion,[],[f4623]) ).
cnf(s25,plain,
( spl308_1
| ~ spl308_2
| ~ spl308_16 ),
inference(sat_conversion,[],[f4781]) ).
cnf(s27,plain,
~ spl308_20,
inference(sat_conversion,[],[f5016]) ).
cnf(s30,plain,
( ~ spl308_1
| spl308_2
| ~ spl308_16
| spl308_18
| spl308_20 ),
inference(sat_conversion,[],[f5070]) ).
cnf(s32,plain,
~ spl308_18,
inference(sat_conversion,[],[f5089]) ).
cnf(s33,plain,
( ~ spl308_1
| spl308_2
| ~ spl308_16
| spl308_20 ),
inference(rat,[],[s30,s32]) ).
cnf(s38,plain,
spl308_1,
inference(rat,[],[s1,s25,s23]) ).
cnf(s39,plain,
spl308_2,
inference(rat,[],[s33,s27,s23,s38]) ).
cnf(s40,plain,
$false,
inference(rat,[],[s2,s39,s38]) ).
fof(f5092,plain,
$false,
inference(avatar_sat_refutation,[],[s40]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT170+2 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.36 % Computer : n004.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 23:55:22 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.42/2.53 % (4013089)Detected formulas, will run a generic FOF schedule.
% 11.42/2.53 % (4013095)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=2824046057:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.42/2.53 % (4013097)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1111229571:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.42/2.53 % (4013098)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=163068939:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.42/2.53 % (4013099)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2836951020:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.42/2.53 % (4013094)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=333915421:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.42/2.53 % (4013100)dis-21_1_sil=8000:lcm=predicate:random_seed=2766786617:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 11.42/2.53 % (4013096)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=3019910341:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.42/2.53 % (4013097)Refutation not found, incomplete strategy
% 11.42/2.53 % (4013097)------------------------------
% 11.42/2.53 % (4013097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.42/2.53 % (4013097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.42/2.53 % (4013097)CaDiCaL version: 2.1.3
% 11.42/2.53 % (4013097)Termination reason: Refutation not found, incomplete strategy
% 11.42/2.53 % (4013097)Time elapsed: 0.010 s
% 11.42/2.53 % (4013097)Peak memory usage: 90 MB
% 11.42/2.53 % (4013097)Instructions burned: 13 (million)
% 11.42/2.53 % (4013100)Instruction limit reached!
% 11.42/2.53 % (4013100)------------------------------
% 11.42/2.53 % (4013100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.42/2.53 % (4013100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.42/2.53 % (4013100)CaDiCaL version: 2.1.3
% 11.42/2.53 % (4013100)Termination reason: Instruction limit
% 11.42/2.53 % (4013100)Termination phase: Saturation
% 11.42/2.53 % (4013100)Time elapsed: 0.059 s
% 11.42/2.53 % (4013100)Peak memory usage: 91 MB
% 11.42/2.53 % (4013100)Instructions burned: 130 (million)
% 11.42/2.53 % (4013099)Instruction limit reached!
% 11.42/2.53 % (4013099)------------------------------
% 11.42/2.53 % (4013099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.42/2.53 % (4013099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.42/2.53 % (4013099)CaDiCaL version: 2.1.3
% 11.42/2.53 % (4013099)Termination reason: Instruction limit
% 11.42/2.53 % (4013099)Termination phase: Saturation
% 11.42/2.53 % (4013099)Time elapsed: 0.067 s
% 11.42/2.53 % (4013099)Peak memory usage: 91 MB
% 11.42/2.53 % (4013099)Instructions burned: 139 (million)
% 11.42/2.53 % (4013098)Instruction limit reached!
% 11.42/2.53 % (4013098)------------------------------
% 11.42/2.53 % (4013098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.42/2.53 % (4013098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.42/2.53 % (4013098)CaDiCaL version: 2.1.3
% 11.42/2.53 % (4013098)Termination reason: Instruction limit
% 11.42/2.53 % (4013098)Termination phase: Saturation
% 11.42/2.53 % (4013098)Time elapsed: 0.072 s
% 11.42/2.53 % (4013098)Peak memory usage: 90 MB
% 11.42/2.53 % (4013098)Instructions burned: 119 (million)
% 11.42/2.53 % (4013109)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2699584684:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 11.42/2.53 % (4013108)lrs+10_1_sil=8000:sp=occurrence:random_seed=3506371595:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 11.42/2.53 % (4013110)lrs+1011_1_sil=32000:sp=occurrence:random_seed=868195818:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 11.42/2.53 % (4013109)Refutation not found, incomplete strategy
% 11.42/2.53 % (4013109)------------------------------
% 11.42/2.53 % (4013109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.42/2.53 % (4013109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.42/2.53 % (4013109)CaDiCaL version: 2.1.3
% 11.42/2.53 % (4013109)Termination reason: Refutation not found, incomplete strategy
% 11.42/2.53 % (4013109)Time elapsed: 0.043 s
% 11.42/2.53 % (4013109)Peak memory usage: 90 MB
% 11.42/2.53 % (4013109)Instructions burned: 81 (million)
% 11.42/2.53 % (4013097)------------------------------
% 11.42/2.53 % (4013097)------------------------------
% 11.42/2.53 % (4013108)Instruction limit reached!
% 11.42/2.53 % (4013108)------------------------------
% 11.42/2.53 % (4013108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.42/2.53 % (4013108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.42/2.53 % (4013108)CaDiCaL version: 2.1.3
% 11.42/2.53 % (4013108)Termination reason: Instruction limit
% 11.42/2.53 % (4013108)Termination phase: Saturation
% 11.42/2.53 % (4013108)Time elapsed: 0.173 s
% 11.42/2.53 % (4013108)Peak memory usage: 92 MB
% 11.42/2.53 % (4013108)Instructions burned: 286 (million)
% 11.42/2.53 % (4013110)Instruction limit reached!
% 11.42/2.53 % (4013110)------------------------------
% 11.42/2.53 % (4013110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.42/2.53 % (4013110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.42/2.53 % (4013110)CaDiCaL version: 2.1.3
% 11.42/2.53 % (4013110)Termination reason: Instruction limit
% 11.42/2.53 % (4013110)Termination phase: Saturation
% 11.42/2.53 % (4013110)Time elapsed: 0.181 s
% 11.42/2.53 % (4013110)Peak memory usage: 91 MB
% 11.42/2.53 % (4013110)Instructions burned: 327 (million)
% 11.42/2.53 % (4013114)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=2096102646:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 11.42/2.53 % (4013109)------------------------------
% 11.42/2.53 % (4013109)------------------------------
% 11.42/2.53 % (4013115)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=872909996:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 11.42/2.53 % (4013116)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2704797639:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 11.42/2.53 % (4013114)Instruction limit reached!
% 11.42/2.53 % (4013114)------------------------------
% 11.42/2.53 % (4013114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.42/2.53 % (4013114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.42/2.53 % (4013114)CaDiCaL version: 2.1.3
% 11.42/2.53 % (4013114)Termination reason: Instruction limit
% 11.42/2.53 % (4013114)Termination phase: Saturation
% 11.42/2.53 % (4013114)Time elapsed: 0.122 s
% 11.42/2.53 % (4013114)Peak memory usage: 93 MB
% 11.42/2.53 % (4013114)Instructions burned: 248 (million)
% 11.42/2.53 % (4013118)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3838976875:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 11.42/2.53 % (4013115)Instruction limit reached!
% 11.42/2.53 % (4013115)------------------------------
% 11.42/2.53 % (4013115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.42/2.53 % (4013115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.42/2.53 % (4013115)CaDiCaL version: 2.1.3
% 11.42/2.53 % (4013115)Termination reason: Instruction limit
% 11.42/2.53 % (4013115)Termination phase: Saturation
% 11.42/2.53 % (4013115)Time elapsed: 0.126 s
% 11.42/2.53 % (4013115)Peak memory usage: 91 MB
% 11.42/2.53 % (4013115)Instructions burned: 296 (million)
% 11.42/2.53 % (4013121)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=843755037:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 11.42/2.53 % (4013118)Instruction limit reached!
% 11.42/2.53 % (4013118)------------------------------
% 11.42/2.53 % (4013118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.42/2.53 % (4013118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.42/2.53 % (4013118)CaDiCaL version: 2.1.3
% 11.42/2.53 % (4013118)Termination reason: Instruction limit
% 11.42/2.53 % (4013118)Termination phase: Saturation
% 11.42/2.53 % (4013118)Time elapsed: 0.055 s
% 11.42/2.53 % (4013118)Peak memory usage: 91 MB
% 11.42/2.53 % (4013118)Instructions burned: 113 (million)
% 11.42/2.53 % (4013121)Instruction limit reached!
% 11.42/2.53 % (4013121)------------------------------
% 11.42/2.53 % (4013121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.42/2.53 % (4013121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.42/2.53 % (4013121)CaDiCaL version: 2.1.3
% 11.42/2.53 % (4013121)Termination reason: Instruction limit
% 11.42/2.53 % (4013121)Termination phase: Saturation
% 11.42/2.53 % (4013121)Time elapsed: 0.059 s
% 11.42/2.53 % (4013121)Peak memory usage: 90 MB
% 11.42/2.53 % (4013121)Instructions burned: 128 (million)
% 11.42/2.53 % (4013123)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3810712763:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 11.42/2.53 % (4013125)lrs+10_1_sil=8000:sp=occurrence:random_seed=959781288:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 11.42/2.53 % (4013123)Instruction limit reached!
% 11.42/2.53 % (4013123)------------------------------
% 11.42/2.53 % (4013123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.42/2.53 % (4013123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.42/2.53 % (4013123)CaDiCaL version: 2.1.3
% 11.42/2.53 % (4013123)Termination reason: Instruction limit
% 11.42/2.53 % (4013123)Termination phase: Saturation
% 11.42/2.54 % (4013123)Time elapsed: 0.054 s
% 11.42/2.54 % (4013123)Peak memory usage: 90 MB
% 11.42/2.54 % (4013123)Instructions burned: 116 (million)
% 11.42/2.54 % (4013126)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3812023846:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 11.42/2.54 % (4013129)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2519645829:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 11.42/2.54 % (4013126)Instruction limit reached!
% 11.42/2.54 % (4013126)------------------------------
% 11.42/2.54 % (4013126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.42/2.54 % (4013126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.42/2.54 % (4013126)CaDiCaL version: 2.1.3
% 11.42/2.54 % (4013126)Termination reason: Instruction limit
% 11.42/2.54 % (4013126)Termination phase: Saturation
% 11.42/2.54 % (4013126)Time elapsed: 0.233 s
% 11.42/2.54 % (4013126)Peak memory usage: 96 MB
% 11.42/2.54 % (4013126)Instructions burned: 439 (million)
% 11.42/2.54 % (4013132)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1690343723:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 11.42/2.54 % (4013094)First to succeed.
% 11.42/2.54 % (4013094)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-4013089"
% 11.42/2.54 % (4013132)Instruction limit reached!
% 11.42/2.54 % (4013132)------------------------------
% 11.42/2.54 % (4013132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.42/2.54 % (4013132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.42/2.54 % (4013132)CaDiCaL version: 2.1.3
% 11.42/2.54 % (4013132)Termination reason: Instruction limit
% 11.42/2.54 % (4013132)Termination phase: Saturation
% 11.42/2.54 % (4013132)Time elapsed: 0.069 s
% 11.42/2.54 % (4013132)Peak memory usage: 92 MB
% 11.42/2.54 % (4013132)Instructions burned: 134 (million)
% 11.42/2.54 % (4013125)Instruction limit reached!
% 11.42/2.54 % (4013125)------------------------------
% 11.42/2.54 % (4013125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.42/2.54 % (4013125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.42/2.54 % (4013125)CaDiCaL version: 2.1.3
% 11.42/2.54 % (4013125)Termination reason: Instruction limit
% 11.42/2.54 % (4013125)Termination phase: Saturation
% 11.42/2.54 % (4013125)Time elapsed: 0.517 s
% 11.42/2.54 % (4013125)Peak memory usage: 96 MB
% 11.42/2.54 % (4013125)Instructions burned: 908 (million)
% 11.42/2.54 % (4013134)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1215146158:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 11.42/2.54 % (4013135)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1212214881:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi)
% 11.42/2.54 % (4013094)Refutation found. Thanks to Tanya!
% 11.42/2.54 % SZS status Theorem for theBenchmark
% 11.42/2.54 % SZS output start Proof for theBenchmark
% See solution above
% 12.17/2.73 % (4013094)------------------------------
% 12.17/2.73 % (4013094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.17/2.73 % (4013094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.17/2.73 % (4013094)CaDiCaL version: 2.1.3
% 12.17/2.73 % (4013094)Termination reason: Refutation
% 12.17/2.73 % (4013094)Time elapsed: 1.216 s
% 12.17/2.73 % (4013094)Peak memory usage: 161 MB
% 12.17/2.73 % (4013094)Instructions burned: 2037 (million)
% 12.17/2.73 % (4013094)------------------------------
% 12.17/2.73 % (4013094)------------------------------
% 12.17/2.73 % (4013089)Success in time 1.689 s
% 12.17/2.73 % Vampire exiting
%------------------------------------------------------------------------------