%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SCT170+3 : 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 : n020.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:07 PM UTC 2026
% Result : Theorem 22.92s 4.37s
% Output : Refutation 23.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 33
% Syntax : Number of formulae : 180 ( 57 unt; 18 def)
% Number of atoms : 652 ( 162 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 803 ( 331 ~; 389 |; 53 &)
% ( 14 <=>; 15 =>; 0 <=; 1 <~>)
% Maximal formula depth : 18 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 12 ( 10 usr; 7 prp; 0-5 aty)
% Number of functors : 53 ( 53 usr; 30 con; 0-2 aty)
% Number of variables : 189 ( 0 sgn 186 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f232,axiom,
is_Arr1861959080le_alt(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gsy_v_a____) ).
fof(f233,axiom,
is_Arr1861959080le_alt(b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gsy_v_b____) ).
fof(f234,axiom,
is_Arr1861959080le_alt(c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gsy_v_c____) ).
fof(f235,axiom,
hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,p),arrow_1721807329e_Prof)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0__096P_A_058_AProf_096) ).
fof(f239,axiom,
hBOOL(hAPP_l1386638586t_bool(distin1223878664le_alt,hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,a),hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,b),hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,c),nil_Ar126264853le_alt))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_dist) ).
fof(f247,axiom,
! [X0,X1,X2,X3,X4] :
( ( is_Arr1861959080le_alt(X0)
& is_Arr1861959080le_alt(X1)
& is_Arr1861959080le_alt(X3)
& is_Arr1861959080le_alt(X4) )
=> ( X3 != X4
=> ( hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,X2),arrow_1681063817le_Lin))
=> ( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X1)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,X2),X3),X4)))
<=> ( X0 != X1
& ( X1 = X3
=> hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X4)),X2)) )
& ( X1 != X3
=> ( ( X0 = X3
=> ( X1 = X4
| hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X4),X1)),X2)) ) )
& ( X0 != X3
=> hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X1)),X2)) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_in__below) ).
fof(f273,axiom,
! [X0,X1] : hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,X0),X1) != nil_Ar126264853le_alt,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_list_Osimps_I3_J) ).
fof(f365,axiom,
! [X0,X1,X2,X3] :
( hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,X1),pi_Arr990697634t_bool(X2,hAPP_f1659309744l_bool(cOMBK_657557929e_indi,X3))))
=> ( hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,X0),X2))
=> hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,hAPP_A1677245848t_bool(X1,X0)),X3)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_130_funcset__mem) ).
fof(f575,axiom,
arrow_1721807329e_Prof = pi_Arr990697634t_bool(top_to1576102282i_bool,hAPP_f1659309744l_bool(cOMBK_657557929e_indi,arrow_1681063817le_Lin)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_340_Prof__def) ).
fof(f592,axiom,
! [X0,X1] :
( is_Arr1861959080le_alt(X0)
=> ( X1 = nil_Ar126264853le_alt
=> last_A57386030le_alt(hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,X0),X1)) = X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_357_last__ConsL) ).
fof(f593,axiom,
! [X0,X1] :
( X1 != nil_Ar126264853le_alt
=> last_A57386030le_alt(hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,X0),X1)) = last_A57386030le_alt(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_358_last__ConsR) ).
fof(f611,axiom,
! [X0] : hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,X0),top_to1576102282i_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_376_UNIV__I) ).
fof(f943,axiom,
! [X0,X1] :
( hBOOL(hAPP_l1386638586t_bool(distin1223878664le_alt,hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,X0),X1)))
<=> ( ~ hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,X0),set_Ar1565008694le_alt(X1)))
& hBOOL(hAPP_l1386638586t_bool(distin1223878664le_alt,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_708_distinct_Osimps_I2_J) ).
fof(f960,axiom,
! [X0] :
( X0 != nil_Ar126264853le_alt
=> hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,last_A57386030le_alt(X0)),set_Ar1565008694le_alt(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_725_last__in__set) ).
fof(f1579,conjecture,
! [X0] :
( is_Arr43961803e_indi(X0)
=> ( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),b)),hAPP_A1677245848t_bool(p,X0)))
<=> hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),c)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,hAPP_A1677245848t_bool(p,X0)),c),b))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f1580,negated_conjecture,
~ ! [X0] :
( is_Arr43961803e_indi(X0)
=> ( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),b)),hAPP_A1677245848t_bool(p,X0)))
<=> hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),c)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,hAPP_A1677245848t_bool(p,X0)),c),b))) ) ),
inference(negated_conjecture,[status(cth)],[f1579]) ).
fof(f1702,plain,
! [X0,X1,X2,X3,X4] :
( ( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X1)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,X2),X3),X4)))
<=> ( X0 != X1
& ( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X4)),X2))
| X1 != X3 )
& ( ( ( X1 = X4
| hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X4),X1)),X2))
| X0 != X3 )
& ( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X1)),X2))
| X0 = X3 ) )
| X1 = X3 ) ) )
| ~ hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,X2),arrow_1681063817le_Lin))
| X3 = X4
| ~ is_Arr1861959080le_alt(X0)
| ~ is_Arr1861959080le_alt(X1)
| ~ is_Arr1861959080le_alt(X3)
| ~ is_Arr1861959080le_alt(X4) ),
inference(ennf_transformation,[],[f247]) ).
fof(f1703,plain,
! [X0,X1,X2,X3,X4] :
( ( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X1)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,X2),X3),X4)))
<=> ( X0 != X1
& ( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X4)),X2))
| X1 != X3 )
& ( ( ( X1 = X4
| hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X4),X1)),X2))
| X0 != X3 )
& ( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X1)),X2))
| X0 = X3 ) )
| X1 = X3 ) ) )
| ~ hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,X2),arrow_1681063817le_Lin))
| X3 = X4
| ~ is_Arr1861959080le_alt(X0)
| ~ is_Arr1861959080le_alt(X1)
| ~ is_Arr1861959080le_alt(X3)
| ~ is_Arr1861959080le_alt(X4) ),
inference(flattening,[],[f1702]) ).
fof(f1905,plain,
! [X0,X1,X2,X3] :
( hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,hAPP_A1677245848t_bool(X1,X0)),X3))
| ~ hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,X0),X2))
| ~ hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,X1),pi_Arr990697634t_bool(X2,hAPP_f1659309744l_bool(cOMBK_657557929e_indi,X3)))) ),
inference(ennf_transformation,[],[f365]) ).
fof(f1906,plain,
! [X0,X1,X2,X3] :
( hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,hAPP_A1677245848t_bool(X1,X0)),X3))
| ~ hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,X0),X2))
| ~ hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,X1),pi_Arr990697634t_bool(X2,hAPP_f1659309744l_bool(cOMBK_657557929e_indi,X3)))) ),
inference(flattening,[],[f1905]) ).
fof(f2243,plain,
! [X0,X1] :
( last_A57386030le_alt(hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,X0),X1)) = X0
| nil_Ar126264853le_alt != X1
| ~ is_Arr1861959080le_alt(X0) ),
inference(ennf_transformation,[],[f592]) ).
fof(f2244,plain,
! [X0,X1] :
( last_A57386030le_alt(hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,X0),X1)) = X0
| nil_Ar126264853le_alt != X1
| ~ is_Arr1861959080le_alt(X0) ),
inference(flattening,[],[f2243]) ).
fof(f2245,plain,
! [X0,X1] :
( last_A57386030le_alt(hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,X0),X1)) = last_A57386030le_alt(X1)
| nil_Ar126264853le_alt = X1 ),
inference(ennf_transformation,[],[f593]) ).
fof(f2557,plain,
! [X0] :
( hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,last_A57386030le_alt(X0)),set_Ar1565008694le_alt(X0)))
| nil_Ar126264853le_alt = X0 ),
inference(ennf_transformation,[],[f960]) ).
fof(f3090,plain,
? [X0] :
( ( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),b)),hAPP_A1677245848t_bool(p,X0)))
<~> hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),c)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,hAPP_A1677245848t_bool(p,X0)),c),b))) )
& is_Arr43961803e_indi(X0) ),
inference(ennf_transformation,[],[f1580]) ).
fof(f3091,definition,
! [X4,X1,X2,X3,X0] :
( sP0(X4,X1,X2,X3,X0)
<=> ( ( ( X1 = X4
| hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X4),X1)),X2))
| X0 != X3 )
& ( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X1)),X2))
| X0 = X3 ) )
| X1 = X3 ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f3092,plain,
! [X0,X1,X2,X3,X4] :
( ( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X1)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,X2),X3),X4)))
<=> ( X0 != X1
& ( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X4)),X2))
| X1 != X3 )
& sP0(X4,X1,X2,X3,X0) ) )
| ~ hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,X2),arrow_1681063817le_Lin))
| X3 = X4
| ~ is_Arr1861959080le_alt(X0)
| ~ is_Arr1861959080le_alt(X1)
| ~ is_Arr1861959080le_alt(X3)
| ~ is_Arr1861959080le_alt(X4) ),
inference(definition_folding,[],[f1703,f3091]) ).
fof(f3119,plain,
! [X4,X1,X2,X3,X0] :
( ( sP0(X4,X1,X2,X3,X0)
| ( ( ( X1 != X4
& ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X4),X1)),X2))
& X0 = X3 )
| ( ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X1)),X2))
& X0 != X3 ) )
& X1 != X3 ) )
& ( ( ( X1 = X4
| hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X4),X1)),X2))
| X0 != X3 )
& ( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X1)),X2))
| X0 = X3 ) )
| X1 = X3
| ~ sP0(X4,X1,X2,X3,X0) ) ),
inference(nnf_transformation,[],[f3091]) ).
fof(f3120,plain,
! [X4,X1,X2,X3,X0] :
( ( sP0(X4,X1,X2,X3,X0)
| ( ( ( X1 != X4
& ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X4),X1)),X2))
& X0 = X3 )
| ( ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X1)),X2))
& X0 != X3 ) )
& X1 != X3 ) )
& ( ( ( X1 = X4
| hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X4),X1)),X2))
| X0 != X3 )
& ( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X1)),X2))
| X0 = X3 ) )
| X1 = X3
| ~ sP0(X4,X1,X2,X3,X0) ) ),
inference(flattening,[],[f3119]) ).
fof(f3121,plain,
! [X0,X1,X2,X3,X4] :
( ( sP0(X0,X1,X2,X3,X4)
| ( ( ( X0 != X1
& ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X1)),X2))
& X3 = X4 )
| ( ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X4),X1)),X2))
& X3 != X4 ) )
& X1 != X3 ) )
& ( ( ( X0 = X1
| hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X1)),X2))
| X3 != X4 )
& ( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X4),X1)),X2))
| X3 = X4 ) )
| X1 = X3
| ~ sP0(X0,X1,X2,X3,X4) ) ),
inference(rectify,[],[f3120]) ).
fof(f3122,plain,
! [X0,X1,X2,X3,X4] :
( ( ( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X1)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,X2),X3),X4)))
| X0 = X1
| ( ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X4)),X2))
& X1 = X3 )
| ~ sP0(X4,X1,X2,X3,X0) )
& ( ( X0 != X1
& ( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X4)),X2))
| X1 != X3 )
& sP0(X4,X1,X2,X3,X0) )
| ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X1)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,X2),X3),X4))) ) )
| ~ hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,X2),arrow_1681063817le_Lin))
| X3 = X4
| ~ is_Arr1861959080le_alt(X0)
| ~ is_Arr1861959080le_alt(X1)
| ~ is_Arr1861959080le_alt(X3)
| ~ is_Arr1861959080le_alt(X4) ),
inference(nnf_transformation,[],[f3092]) ).
fof(f3123,plain,
! [X0,X1,X2,X3,X4] :
( ( ( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X1)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,X2),X3),X4)))
| X0 = X1
| ( ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X4)),X2))
& X1 = X3 )
| ~ sP0(X4,X1,X2,X3,X0) )
& ( ( X0 != X1
& ( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X4)),X2))
| X1 != X3 )
& sP0(X4,X1,X2,X3,X0) )
| ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X1)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,X2),X3),X4))) ) )
| ~ hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,X2),arrow_1681063817le_Lin))
| X3 = X4
| ~ is_Arr1861959080le_alt(X0)
| ~ is_Arr1861959080le_alt(X1)
| ~ is_Arr1861959080le_alt(X3)
| ~ is_Arr1861959080le_alt(X4) ),
inference(flattening,[],[f3122]) ).
fof(f3507,plain,
! [X0,X1] :
( ( hBOOL(hAPP_l1386638586t_bool(distin1223878664le_alt,hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,X0),X1)))
| hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,X0),set_Ar1565008694le_alt(X1)))
| ~ hBOOL(hAPP_l1386638586t_bool(distin1223878664le_alt,X1)) )
& ( ( ~ hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,X0),set_Ar1565008694le_alt(X1)))
& hBOOL(hAPP_l1386638586t_bool(distin1223878664le_alt,X1)) )
| ~ hBOOL(hAPP_l1386638586t_bool(distin1223878664le_alt,hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,X0),X1))) ) ),
inference(nnf_transformation,[],[f943]) ).
fof(f3508,plain,
! [X0,X1] :
( ( hBOOL(hAPP_l1386638586t_bool(distin1223878664le_alt,hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,X0),X1)))
| hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,X0),set_Ar1565008694le_alt(X1)))
| ~ hBOOL(hAPP_l1386638586t_bool(distin1223878664le_alt,X1)) )
& ( ( ~ hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,X0),set_Ar1565008694le_alt(X1)))
& hBOOL(hAPP_l1386638586t_bool(distin1223878664le_alt,X1)) )
| ~ hBOOL(hAPP_l1386638586t_bool(distin1223878664le_alt,hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,X0),X1))) ) ),
inference(flattening,[],[f3507]) ).
fof(f3866,plain,
? [X0] :
( ( ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),c)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,hAPP_A1677245848t_bool(p,X0)),c),b)))
| ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),b)),hAPP_A1677245848t_bool(p,X0))) )
& ( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),c)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,hAPP_A1677245848t_bool(p,X0)),c),b)))
| hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),b)),hAPP_A1677245848t_bool(p,X0))) )
& is_Arr43961803e_indi(X0) ),
inference(nnf_transformation,[],[f3090]) ).
fof(f3867,plain,
? [X0] :
( ( ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),c)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,hAPP_A1677245848t_bool(p,X0)),c),b)))
| ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),b)),hAPP_A1677245848t_bool(p,X0))) )
& ( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),c)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,hAPP_A1677245848t_bool(p,X0)),c),b)))
| hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),b)),hAPP_A1677245848t_bool(p,X0))) )
& is_Arr43961803e_indi(X0) ),
inference(flattening,[],[f3866]) ).
fof(f3868,plain,
( ( ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),c)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,hAPP_A1677245848t_bool(p,sK592)),c),b)))
| ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),b)),hAPP_A1677245848t_bool(p,sK592))) )
& ( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),c)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,hAPP_A1677245848t_bool(p,sK592)),c),b)))
| hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),b)),hAPP_A1677245848t_bool(p,sK592))) )
& is_Arr43961803e_indi(sK592) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK592]),skolemize(X0,sK592)],[f3867]) ).
fof(f4100,plain,
is_Arr1861959080le_alt(a),
inference(cnf_transformation,[],[f232]) ).
fof(f4101,plain,
is_Arr1861959080le_alt(b),
inference(cnf_transformation,[],[f233]) ).
fof(f4102,plain,
is_Arr1861959080le_alt(c),
inference(cnf_transformation,[],[f234]) ).
fof(f4103,plain,
hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,p),arrow_1721807329e_Prof)),
inference(cnf_transformation,[],[f235]) ).
fof(f4107,plain,
hBOOL(hAPP_l1386638586t_bool(distin1223878664le_alt,hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,a),hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,b),hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,c),nil_Ar126264853le_alt))))),
inference(cnf_transformation,[],[f239]) ).
fof(f4131,plain,
! [X2,X3,X0,X1,X4] :
( sP0(X0,X1,X2,X3,X4)
| X1 != X3 ),
inference(cnf_transformation,[],[f3121]) ).
fof(f4139,plain,
! [X2,X3,X0,X1,X4] :
( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X4)),X2))
| X1 != X3
| ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X1)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,X2),X3),X4)))
| ~ hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,X2),arrow_1681063817le_Lin))
| X3 = X4
| ~ is_Arr1861959080le_alt(X0)
| ~ is_Arr1861959080le_alt(X1)
| ~ is_Arr1861959080le_alt(X3)
| ~ is_Arr1861959080le_alt(X4) ),
inference(cnf_transformation,[],[f3123]) ).
fof(f4142,plain,
! [X2,X3,X0,X1,X4] :
( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X1)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,X2),X3),X4)))
| X0 = X1
| ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X4)),X2))
| ~ sP0(X4,X1,X2,X3,X0)
| ~ hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,X2),arrow_1681063817le_Lin))
| X3 = X4
| ~ is_Arr1861959080le_alt(X0)
| ~ is_Arr1861959080le_alt(X1)
| ~ is_Arr1861959080le_alt(X3)
| ~ is_Arr1861959080le_alt(X4) ),
inference(cnf_transformation,[],[f3123]) ).
fof(f4229,plain,
! [X0,X1] : nil_Ar126264853le_alt != hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,X0),X1),
inference(cnf_transformation,[],[f273]) ).
fof(f4339,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,X1),pi_Arr990697634t_bool(X2,hAPP_f1659309744l_bool(cOMBK_657557929e_indi,X3))))
| ~ hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,X0),X2))
| hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,hAPP_A1677245848t_bool(X1,X0)),X3)) ),
inference(cnf_transformation,[],[f1906]) ).
fof(f4825,plain,
arrow_1721807329e_Prof = pi_Arr990697634t_bool(top_to1576102282i_bool,hAPP_f1659309744l_bool(cOMBK_657557929e_indi,arrow_1681063817le_Lin)),
inference(cnf_transformation,[],[f575]) ).
fof(f4850,plain,
! [X0,X1] :
( last_A57386030le_alt(hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,X0),X1)) = X0
| nil_Ar126264853le_alt != X1
| ~ is_Arr1861959080le_alt(X0) ),
inference(cnf_transformation,[],[f2244]) ).
fof(f4851,plain,
! [X0,X1] :
( last_A57386030le_alt(hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,X0),X1)) = last_A57386030le_alt(X1)
| nil_Ar126264853le_alt = X1 ),
inference(cnf_transformation,[],[f2245]) ).
fof(f4878,plain,
! [X0] : hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,X0),top_to1576102282i_bool)),
inference(cnf_transformation,[],[f611]) ).
fof(f5470,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_l1386638586t_bool(distin1223878664le_alt,hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,X0),X1)))
| hBOOL(hAPP_l1386638586t_bool(distin1223878664le_alt,X1)) ),
inference(cnf_transformation,[],[f3508]) ).
fof(f5471,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_l1386638586t_bool(distin1223878664le_alt,hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,X0),X1)))
| ~ hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,X0),set_Ar1565008694le_alt(X1))) ),
inference(cnf_transformation,[],[f3508]) ).
fof(f5503,plain,
! [X0] :
( hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,last_A57386030le_alt(X0)),set_Ar1565008694le_alt(X0)))
| nil_Ar126264853le_alt = X0 ),
inference(cnf_transformation,[],[f2557]) ).
fof(f6554,plain,
( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),c)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,hAPP_A1677245848t_bool(p,sK592)),c),b)))
| hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),b)),hAPP_A1677245848t_bool(p,sK592))) ),
inference(cnf_transformation,[],[f3868]) ).
fof(f6555,plain,
( ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),c)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,hAPP_A1677245848t_bool(p,sK592)),c),b)))
| ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,a),b)),hAPP_A1677245848t_bool(p,sK592))) ),
inference(cnf_transformation,[],[f3868]) ).
fof(f6625,plain,
! [X2,X3,X0,X4] : sP0(X0,X3,X2,X3,X4),
inference(equality_resolution,[],[f4131]) ).
fof(f6628,plain,
! [X2,X3,X0,X4] :
( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X4)),X2))
| ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X3)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,X2),X3),X4)))
| ~ hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,X2),arrow_1681063817le_Lin))
| X3 = X4
| ~ is_Arr1861959080le_alt(X0)
| ~ is_Arr1861959080le_alt(X3)
| ~ is_Arr1861959080le_alt(X3)
| ~ is_Arr1861959080le_alt(X4) ),
inference(equality_resolution,[],[f4139]) ).
fof(f6655,plain,
! [X0] :
( ~ is_Arr1861959080le_alt(X0)
| last_A57386030le_alt(hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,X0),nil_Ar126264853le_alt)) = X0 ),
inference(equality_resolution,[],[f4850]) ).
fof(f6917,definition,
sF593 = hAPP_A1505516597le_alt(produc1400112471le_alt,a),
introduced(definition,[new_symbols(definition,[sF593])],[function_definition]) ).
fof(f6918,plain,
hAPP_A1505516597le_alt(produc1400112471le_alt,a) = sF593,
inference(reorient_equations,[],[f6917]) ).
fof(f6919,definition,
sF594 = hAPP_A702847159le_alt(sF593,c),
introduced(definition,[new_symbols(definition,[sF594])],[function_definition]) ).
fof(f6920,plain,
hAPP_A702847159le_alt(sF593,c) = sF594,
inference(reorient_equations,[],[f6919]) ).
fof(f6921,definition,
sF595 = hAPP_P229966473l_bool(member1441201108le_alt,sF594),
introduced(definition,[new_symbols(definition,[sF595])],[function_definition]) ).
fof(f6922,plain,
hAPP_P229966473l_bool(member1441201108le_alt,sF594) = sF595,
inference(reorient_equations,[],[f6921]) ).
fof(f6923,definition,
sF596 = hAPP_A1677245848t_bool(p,sK592),
introduced(definition,[new_symbols(definition,[sF596])],[function_definition]) ).
fof(f6924,plain,
hAPP_A1677245848t_bool(p,sK592) = sF596,
inference(reorient_equations,[],[f6923]) ).
fof(f6925,definition,
sF597 = hAPP_f344580165t_bool(arrow_1539419881_below,sF596),
introduced(definition,[new_symbols(definition,[sF597])],[function_definition]) ).
fof(f6926,plain,
hAPP_f344580165t_bool(arrow_1539419881_below,sF596) = sF597,
inference(reorient_equations,[],[f6925]) ).
fof(f6927,definition,
sF598 = hAPP_A1941004017t_bool(sF597,c),
introduced(definition,[new_symbols(definition,[sF598])],[function_definition]) ).
fof(f6928,plain,
hAPP_A1941004017t_bool(sF597,c) = sF598,
inference(reorient_equations,[],[f6927]) ).
fof(f6929,definition,
sF599 = hAPP_A568203993t_bool(sF598,b),
introduced(definition,[new_symbols(definition,[sF599])],[function_definition]) ).
fof(f6930,plain,
hAPP_A568203993t_bool(sF598,b) = sF599,
inference(reorient_equations,[],[f6929]) ).
fof(f6931,definition,
sF600 = hAPP_f592646513l_bool(sF595,sF599),
introduced(definition,[new_symbols(definition,[sF600])],[function_definition]) ).
fof(f6932,plain,
hAPP_f592646513l_bool(sF595,sF599) = sF600,
inference(reorient_equations,[],[f6931]) ).
fof(f6933,definition,
sF601 = hAPP_A702847159le_alt(sF593,b),
introduced(definition,[new_symbols(definition,[sF601])],[function_definition]) ).
fof(f6934,plain,
hAPP_A702847159le_alt(sF593,b) = sF601,
inference(reorient_equations,[],[f6933]) ).
fof(f6935,definition,
sF602 = hAPP_P229966473l_bool(member1441201108le_alt,sF601),
introduced(definition,[new_symbols(definition,[sF602])],[function_definition]) ).
fof(f6936,plain,
hAPP_P229966473l_bool(member1441201108le_alt,sF601) = sF602,
inference(reorient_equations,[],[f6935]) ).
fof(f6937,definition,
sF603 = hAPP_f592646513l_bool(sF602,sF596),
introduced(definition,[new_symbols(definition,[sF603])],[function_definition]) ).
fof(f6938,plain,
hAPP_f592646513l_bool(sF602,sF596) = sF603,
inference(reorient_equations,[],[f6937]) ).
fof(f6939,plain,
( ~ hBOOL(sF600)
| ~ hBOOL(sF603) ),
inference(definition_folding,[],[f6555,f6938,f6924,f6936,f6934,f6918,f6932,f6930,f6928,f6926,f6924,f6922,f6920,f6918]) ).
fof(f6940,plain,
( hBOOL(sF600)
| hBOOL(sF603) ),
inference(definition_folding,[],[f6554,f6938,f6924,f6936,f6934,f6918,f6932,f6930,f6928,f6926,f6924,f6922,f6920,f6918]) ).
fof(f6958,plain,
! [X2,X3,X0,X4] :
( ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X3)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,X2),X3),X4)))
| hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,X0),X4)),X2))
| ~ hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,X2),arrow_1681063817le_Lin))
| X3 = X4
| ~ is_Arr1861959080le_alt(X0)
| ~ is_Arr1861959080le_alt(X3)
| ~ is_Arr1861959080le_alt(X4) ),
inference(duplicate_literal_removal,[],[f6628]) ).
fof(f6969,definition,
( spl604_1
<=> hBOOL(sF603) ),
introduced(definition,[new_symbols(definition,[spl604_1])],[avatar_definition]) ).
fof(f6970,plain,
( ~ hBOOL(sF603)
| spl604_1 ),
inference(avatar_component_clause,[],[f6969]) ).
fof(f6971,plain,
( hBOOL(sF603)
| ~ spl604_1 ),
inference(avatar_component_clause,[],[f6969]) ).
fof(f6973,definition,
( spl604_2
<=> hBOOL(sF600) ),
introduced(definition,[new_symbols(definition,[spl604_2])],[avatar_definition]) ).
fof(f6974,plain,
( ~ hBOOL(sF600)
| spl604_2 ),
inference(avatar_component_clause,[],[f6973]) ).
fof(f6975,plain,
( hBOOL(sF600)
| ~ spl604_2 ),
inference(avatar_component_clause,[],[f6973]) ).
fof(f6976,plain,
( spl604_1
| spl604_2 ),
inference(avatar_split_clause,[],[f6940,f6973,f6969]) ).
fof(f6977,plain,
( ~ spl604_1
| ~ spl604_2 ),
inference(avatar_split_clause,[],[f6939,f6973,f6969]) ).
fof(f7167,definition,
( spl604_32
<=> hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,sF596),arrow_1681063817le_Lin)) ),
introduced(definition,[new_symbols(definition,[spl604_32])],[avatar_definition]) ).
fof(f7168,plain,
( hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,sF596),arrow_1681063817le_Lin))
| ~ spl604_32 ),
inference(avatar_component_clause,[],[f7167]) ).
fof(f7169,plain,
( ~ hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,sF596),arrow_1681063817le_Lin))
| spl604_32 ),
inference(avatar_component_clause,[],[f7167]) ).
fof(f7183,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(sF593,X0)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,X1),X0),X2)))
| hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(sF593,X2)),X1))
| ~ hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,X1),arrow_1681063817le_Lin))
| X0 = X2
| ~ is_Arr1861959080le_alt(a)
| ~ is_Arr1861959080le_alt(X0)
| ~ is_Arr1861959080le_alt(X2) ),
inference(superposition,[],[f6958,f6918]) ).
fof(f7188,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(sF593,X0)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,X1),X0),X2)))
| hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(sF593,X2)),X1))
| ~ hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,X1),arrow_1681063817le_Lin))
| X0 = X2
| ~ is_Arr1861959080le_alt(X0)
| ~ is_Arr1861959080le_alt(X2) ),
inference(forward_subsumption_resolution,[],[f7183,f4100]) ).
fof(f7226,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,sF594),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,X0),c),X1)))
| hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(sF593,X1)),X0))
| ~ hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,X0),arrow_1681063817le_Lin))
| c = X1
| ~ is_Arr1861959080le_alt(c)
| ~ is_Arr1861959080le_alt(X1) ),
inference(superposition,[],[f7188,f6920]) ).
fof(f7228,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,sF594),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,X0),c),X1)))
| hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(sF593,X1)),X0))
| ~ hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,X0),arrow_1681063817le_Lin))
| c = X1
| ~ is_Arr1861959080le_alt(X1) ),
inference(forward_subsumption_resolution,[],[f7226,f4102]) ).
fof(f7230,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_f592646513l_bool(sF595,hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,X0),c),X1)))
| hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(sF593,X1)),X0))
| ~ hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,X0),arrow_1681063817le_Lin))
| c = X1
| ~ is_Arr1861959080le_alt(X1) ),
inference(forward_demodulation,[],[f7228,f6922]) ).
fof(f7232,plain,
! [X0] :
( ~ hBOOL(hAPP_f592646513l_bool(sF595,hAPP_A568203993t_bool(hAPP_A1941004017t_bool(sF597,c),X0)))
| hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(sF593,X0)),sF596))
| ~ hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,sF596),arrow_1681063817le_Lin))
| c = X0
| ~ is_Arr1861959080le_alt(X0) ),
inference(superposition,[],[f7230,f6926]) ).
fof(f7234,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,X0),arrow_1721807329e_Prof))
| ~ hBOOL(hAPP_f1599966040l_bool(hAPP_A1602262231l_bool(member1493247163e_indi,X1),top_to1576102282i_bool))
| hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,hAPP_A1677245848t_bool(X0,X1)),arrow_1681063817le_Lin)) ),
inference(superposition,[],[f4339,f4825]) ).
fof(f7235,plain,
! [X0,X1] :
( hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,hAPP_A1677245848t_bool(X0,X1)),arrow_1681063817le_Lin))
| ~ hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,X0),arrow_1721807329e_Prof)) ),
inference(forward_subsumption_resolution,[],[f7234,f4878]) ).
fof(f7236,plain,
( hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,sF596),arrow_1681063817le_Lin))
| ~ hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,p),arrow_1721807329e_Prof)) ),
inference(superposition,[],[f7235,f6924]) ).
fof(f7237,plain,
( ~ hBOOL(hAPP_f777333846l_bool(hAPP_f461621971l_bool(member760917689t_bool,p),arrow_1721807329e_Prof))
| spl604_32 ),
inference(forward_subsumption_resolution,[],[f7236,f7169]) ).
fof(f7238,plain,
( $false
| spl604_32 ),
inference(forward_subsumption_resolution,[],[f7237,f4103]) ).
fof(f7239,plain,
spl604_32,
inference(avatar_contradiction_clause,[],[f7238]) ).
fof(f7243,plain,
( ! [X0] :
( ~ hBOOL(hAPP_f592646513l_bool(sF595,hAPP_A568203993t_bool(hAPP_A1941004017t_bool(sF597,c),X0)))
| hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(sF593,X0)),sF596))
| c = X0
| ~ is_Arr1861959080le_alt(X0) )
| ~ spl604_32 ),
inference(forward_subsumption_resolution,[],[f7232,f7168]) ).
fof(f7245,plain,
( ! [X0] :
( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(sF593,X0)),sF596))
| ~ hBOOL(hAPP_f592646513l_bool(sF595,hAPP_A568203993t_bool(sF598,X0)))
| c = X0
| ~ is_Arr1861959080le_alt(X0) )
| ~ spl604_32 ),
inference(forward_demodulation,[],[f7243,f6928]) ).
fof(f7248,plain,
( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,sF601),sF596))
| ~ hBOOL(hAPP_f592646513l_bool(sF595,hAPP_A568203993t_bool(sF598,b)))
| b = c
| ~ is_Arr1861959080le_alt(b)
| ~ spl604_32 ),
inference(superposition,[],[f7245,f6934]) ).
fof(f7249,plain,
( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,sF601),sF596))
| ~ hBOOL(hAPP_f592646513l_bool(sF595,hAPP_A568203993t_bool(sF598,b)))
| b = c
| ~ spl604_32 ),
inference(forward_subsumption_resolution,[],[f7248,f4101]) ).
fof(f7250,plain,
( hBOOL(hAPP_f592646513l_bool(sF602,sF596))
| ~ hBOOL(hAPP_f592646513l_bool(sF595,hAPP_A568203993t_bool(sF598,b)))
| b = c
| ~ spl604_32 ),
inference(forward_demodulation,[],[f7249,f6936]) ).
fof(f7251,plain,
( hBOOL(sF603)
| ~ hBOOL(hAPP_f592646513l_bool(sF595,hAPP_A568203993t_bool(sF598,b)))
| b = c
| ~ spl604_32 ),
inference(forward_demodulation,[],[f7250,f6938]) ).
fof(f7252,plain,
( ~ hBOOL(hAPP_f592646513l_bool(sF595,hAPP_A568203993t_bool(sF598,b)))
| b = c
| spl604_1
| ~ spl604_32 ),
inference(forward_subsumption_resolution,[],[f7251,f6970]) ).
fof(f7253,plain,
( ~ hBOOL(hAPP_f592646513l_bool(sF595,sF599))
| b = c
| spl604_1
| ~ spl604_32 ),
inference(forward_demodulation,[],[f7252,f6930]) ).
fof(f7254,plain,
( ~ hBOOL(sF600)
| b = c
| spl604_1
| ~ spl604_32 ),
inference(forward_demodulation,[],[f7253,f6932]) ).
fof(f7255,plain,
( b = c
| spl604_1
| ~ spl604_2
| ~ spl604_32 ),
inference(forward_subsumption_resolution,[],[f7254,f6975]) ).
fof(f7269,plain,
~ hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,a),set_Ar1565008694le_alt(hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,b),hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,c),nil_Ar126264853le_alt))))),
inference(resolution,[],[f5471,f4107]) ).
fof(f7272,plain,
hBOOL(hAPP_l1386638586t_bool(distin1223878664le_alt,hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,b),hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,c),nil_Ar126264853le_alt)))),
inference(resolution,[],[f5470,f4107]) ).
fof(f7274,plain,
( hBOOL(hAPP_l1386638586t_bool(distin1223878664le_alt,hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,b),hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,b),nil_Ar126264853le_alt))))
| spl604_1
| ~ spl604_2
| ~ spl604_32 ),
inference(forward_demodulation,[],[f7272,f7255]) ).
fof(f7276,plain,
( ~ hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,b),set_Ar1565008694le_alt(hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,b),nil_Ar126264853le_alt))))
| spl604_1
| ~ spl604_2
| ~ spl604_32 ),
inference(resolution,[],[f7274,f5471]) ).
fof(f7292,plain,
b = last_A57386030le_alt(hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,b),nil_Ar126264853le_alt)),
inference(resolution,[],[f6655,f4101]) ).
fof(f7293,plain,
a = last_A57386030le_alt(hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,a),nil_Ar126264853le_alt)),
inference(resolution,[],[f6655,f4100]) ).
fof(f7295,plain,
( hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,b),set_Ar1565008694le_alt(hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,b),nil_Ar126264853le_alt))))
| nil_Ar126264853le_alt = hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,b),nil_Ar126264853le_alt) ),
inference(superposition,[],[f5503,f7292]) ).
fof(f7296,plain,
( nil_Ar126264853le_alt = hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,b),nil_Ar126264853le_alt)
| spl604_1
| ~ spl604_2
| ~ spl604_32 ),
inference(forward_subsumption_resolution,[],[f7295,f7276]) ).
fof(f7297,plain,
( $false
| spl604_1
| ~ spl604_2
| ~ spl604_32 ),
inference(forward_subsumption_resolution,[],[f7296,f4229]) ).
fof(f7298,plain,
( spl604_1
| ~ spl604_2
| ~ spl604_32 ),
inference(avatar_contradiction_clause,[],[f7297]) ).
fof(f7300,plain,
hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,b),set_Ar1565008694le_alt(hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,b),nil_Ar126264853le_alt)))),
inference(forward_subsumption_resolution,[],[f7295,f4229]) ).
fof(f7302,definition,
( spl604_34
<=> b = c ),
introduced(definition,[new_symbols(definition,[spl604_34])],[avatar_definition]) ).
fof(f7303,plain,
( b != c
| spl604_34 ),
inference(avatar_component_clause,[],[f7302]) ).
fof(f7304,plain,
( b = c
| ~ spl604_34 ),
inference(avatar_component_clause,[],[f7302]) ).
fof(f7333,plain,
! [X2,X3,X0,X1] :
( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(sF593,X0)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,X1),X2),X3)))
| a = X0
| ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(sF593,X3)),X1))
| ~ sP0(X3,X0,X1,X2,a)
| ~ hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,X1),arrow_1681063817le_Lin))
| X2 = X3
| ~ is_Arr1861959080le_alt(a)
| ~ is_Arr1861959080le_alt(X0)
| ~ is_Arr1861959080le_alt(X2)
| ~ is_Arr1861959080le_alt(X3) ),
inference(superposition,[],[f4142,f6918]) ).
fof(f7339,plain,
! [X2,X3,X0,X1] :
( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(sF593,X0)),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,X1),X2),X3)))
| a = X0
| ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(sF593,X3)),X1))
| ~ sP0(X3,X0,X1,X2,a)
| ~ hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,X1),arrow_1681063817le_Lin))
| X2 = X3
| ~ is_Arr1861959080le_alt(X0)
| ~ is_Arr1861959080le_alt(X2)
| ~ is_Arr1861959080le_alt(X3) ),
inference(forward_subsumption_resolution,[],[f7333,f4100]) ).
fof(f7346,plain,
! [X2,X0,X1] :
( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,sF594),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,X0),X1),X2)))
| a = c
| ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(sF593,X2)),X0))
| ~ sP0(X2,c,X0,X1,a)
| ~ hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,X0),arrow_1681063817le_Lin))
| X1 = X2
| ~ is_Arr1861959080le_alt(c)
| ~ is_Arr1861959080le_alt(X1)
| ~ is_Arr1861959080le_alt(X2) ),
inference(superposition,[],[f7339,f6920]) ).
fof(f7350,plain,
! [X2,X0,X1] :
( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,sF594),hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,X0),X1),X2)))
| a = c
| ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(sF593,X2)),X0))
| ~ sP0(X2,c,X0,X1,a)
| ~ hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,X0),arrow_1681063817le_Lin))
| X1 = X2
| ~ is_Arr1861959080le_alt(X1)
| ~ is_Arr1861959080le_alt(X2) ),
inference(forward_subsumption_resolution,[],[f7346,f4102]) ).
fof(f7352,plain,
! [X2,X0,X1] :
( hBOOL(hAPP_f592646513l_bool(sF595,hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,X0),X1),X2)))
| a = c
| ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(sF593,X2)),X0))
| ~ sP0(X2,c,X0,X1,a)
| ~ hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,X0),arrow_1681063817le_Lin))
| X1 = X2
| ~ is_Arr1861959080le_alt(X1)
| ~ is_Arr1861959080le_alt(X2) ),
inference(forward_demodulation,[],[f7350,f6922]) ).
fof(f7364,plain,
~ hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,b),set_Ar1565008694le_alt(hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,c),nil_Ar126264853le_alt)))),
inference(resolution,[],[f7272,f5471]) ).
fof(f7366,plain,
( ~ hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,b),set_Ar1565008694le_alt(hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,b),nil_Ar126264853le_alt))))
| ~ spl604_34 ),
inference(forward_demodulation,[],[f7364,f7304]) ).
fof(f7368,plain,
( $false
| ~ spl604_34 ),
inference(forward_subsumption_resolution,[],[f7366,f7300]) ).
fof(f7369,plain,
~ spl604_34,
inference(avatar_contradiction_clause,[],[f7368]) ).
fof(f7371,definition,
( spl604_36
<=> a = c ),
introduced(definition,[new_symbols(definition,[spl604_36])],[avatar_definition]) ).
fof(f7373,plain,
( a = c
| ~ spl604_36 ),
inference(avatar_component_clause,[],[f7371]) ).
fof(f7375,definition,
( spl604_37
<=> ! [X2,X0,X1] :
( hBOOL(hAPP_f592646513l_bool(sF595,hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,X0),X1),X2)))
| ~ is_Arr1861959080le_alt(X2)
| ~ is_Arr1861959080le_alt(X1)
| X1 = X2
| ~ hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,X0),arrow_1681063817le_Lin))
| ~ sP0(X2,c,X0,X1,a)
| ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(sF593,X2)),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl604_37])],[avatar_definition]) ).
fof(f7376,plain,
( ! [X2,X0,X1] :
( hBOOL(hAPP_f592646513l_bool(sF595,hAPP_A568203993t_bool(hAPP_A1941004017t_bool(hAPP_f344580165t_bool(arrow_1539419881_below,X0),X1),X2)))
| ~ is_Arr1861959080le_alt(X2)
| ~ is_Arr1861959080le_alt(X1)
| X1 = X2
| ~ hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,X0),arrow_1681063817le_Lin))
| ~ sP0(X2,c,X0,X1,a)
| ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(sF593,X2)),X0)) )
| ~ spl604_37 ),
inference(avatar_component_clause,[],[f7375]) ).
fof(f7377,plain,
( spl604_36
| spl604_37 ),
inference(avatar_split_clause,[],[f7352,f7375,f7371]) ).
fof(f7383,plain,
( ~ hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,a),set_Ar1565008694le_alt(hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,b),hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,a),nil_Ar126264853le_alt)))))
| ~ spl604_36 ),
inference(superposition,[],[f7269,f7373]) ).
fof(f7399,plain,
! [X0,X1] :
( hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,last_A57386030le_alt(X0)),set_Ar1565008694le_alt(hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,X1),X0))))
| nil_Ar126264853le_alt = hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,X1),X0)
| nil_Ar126264853le_alt = X0 ),
inference(superposition,[],[f5503,f4851]) ).
fof(f7400,plain,
! [X0,X1] :
( hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,last_A57386030le_alt(X0)),set_Ar1565008694le_alt(hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,X1),X0))))
| nil_Ar126264853le_alt = X0 ),
inference(forward_subsumption_resolution,[],[f7399,f4229]) ).
fof(f7403,plain,
! [X0] :
( hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,a),set_Ar1565008694le_alt(hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,X0),hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,a),nil_Ar126264853le_alt)))))
| nil_Ar126264853le_alt = hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,a),nil_Ar126264853le_alt) ),
inference(superposition,[],[f7400,f7293]) ).
fof(f7406,plain,
! [X0] : hBOOL(hAPP_f2013399995l_bool(hAPP_A297543629l_bool(member1071917752le_alt,a),set_Ar1565008694le_alt(hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,X0),hAPP_l726444215le_alt(hAPP_A408086601le_alt(cons_A1216297413le_alt,a),nil_Ar126264853le_alt))))),
inference(forward_subsumption_resolution,[],[f7403,f4229]) ).
fof(f7410,plain,
( $false
| ~ spl604_36 ),
inference(resolution,[],[f7406,f7383]) ).
fof(f7411,plain,
~ spl604_36,
inference(avatar_contradiction_clause,[],[f7410]) ).
fof(f7413,plain,
( ! [X0,X1] :
( hBOOL(hAPP_f592646513l_bool(sF595,hAPP_A568203993t_bool(hAPP_A1941004017t_bool(sF597,X0),X1)))
| ~ is_Arr1861959080le_alt(X1)
| ~ is_Arr1861959080le_alt(X0)
| X0 = X1
| ~ hBOOL(hAPP_f1749234559l_bool(hAPP_f566237389l_bool(member496995196t_bool,sF596),arrow_1681063817le_Lin))
| ~ sP0(X1,c,sF596,X0,a)
| ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(sF593,X1)),sF596)) )
| ~ spl604_37 ),
inference(superposition,[],[f7376,f6926]) ).
fof(f7415,plain,
( ! [X0,X1] :
( ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(sF593,X1)),sF596))
| ~ is_Arr1861959080le_alt(X1)
| ~ is_Arr1861959080le_alt(X0)
| X0 = X1
| ~ sP0(X1,c,sF596,X0,a)
| hBOOL(hAPP_f592646513l_bool(sF595,hAPP_A568203993t_bool(hAPP_A1941004017t_bool(sF597,X0),X1))) )
| ~ spl604_32
| ~ spl604_37 ),
inference(forward_subsumption_resolution,[],[f7413,f7168]) ).
fof(f7890,plain,
( ! [X0] :
( ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,sF601),sF596))
| ~ is_Arr1861959080le_alt(b)
| ~ is_Arr1861959080le_alt(X0)
| b = X0
| ~ sP0(b,c,sF596,X0,a)
| hBOOL(hAPP_f592646513l_bool(sF595,hAPP_A568203993t_bool(hAPP_A1941004017t_bool(sF597,X0),b))) )
| ~ spl604_32
| ~ spl604_37 ),
inference(superposition,[],[f7415,f6934]) ).
fof(f7894,plain,
( ! [X0] :
( ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,sF601),sF596))
| ~ is_Arr1861959080le_alt(X0)
| b = X0
| ~ sP0(b,c,sF596,X0,a)
| hBOOL(hAPP_f592646513l_bool(sF595,hAPP_A568203993t_bool(hAPP_A1941004017t_bool(sF597,X0),b))) )
| ~ spl604_32
| ~ spl604_37 ),
inference(forward_subsumption_resolution,[],[f7890,f4101]) ).
fof(f7896,plain,
( ! [X0] :
( ~ hBOOL(hAPP_f592646513l_bool(sF602,sF596))
| ~ is_Arr1861959080le_alt(X0)
| b = X0
| ~ sP0(b,c,sF596,X0,a)
| hBOOL(hAPP_f592646513l_bool(sF595,hAPP_A568203993t_bool(hAPP_A1941004017t_bool(sF597,X0),b))) )
| ~ spl604_32
| ~ spl604_37 ),
inference(forward_demodulation,[],[f7894,f6936]) ).
fof(f7897,plain,
( ! [X0] :
( ~ hBOOL(sF603)
| ~ is_Arr1861959080le_alt(X0)
| b = X0
| ~ sP0(b,c,sF596,X0,a)
| hBOOL(hAPP_f592646513l_bool(sF595,hAPP_A568203993t_bool(hAPP_A1941004017t_bool(sF597,X0),b))) )
| ~ spl604_32
| ~ spl604_37 ),
inference(forward_demodulation,[],[f7896,f6938]) ).
fof(f7898,plain,
( ! [X0] :
( hBOOL(hAPP_f592646513l_bool(sF595,hAPP_A568203993t_bool(hAPP_A1941004017t_bool(sF597,X0),b)))
| b = X0
| ~ sP0(b,c,sF596,X0,a)
| ~ is_Arr1861959080le_alt(X0) )
| ~ spl604_1
| ~ spl604_32
| ~ spl604_37 ),
inference(forward_subsumption_resolution,[],[f7897,f6971]) ).
fof(f7899,plain,
( hBOOL(hAPP_f592646513l_bool(sF595,hAPP_A568203993t_bool(sF598,b)))
| b = c
| ~ sP0(b,c,sF596,c,a)
| ~ is_Arr1861959080le_alt(c)
| ~ spl604_1
| ~ spl604_32
| ~ spl604_37 ),
inference(superposition,[],[f7898,f6928]) ).
fof(f7900,plain,
( hBOOL(hAPP_f592646513l_bool(sF595,hAPP_A568203993t_bool(sF598,b)))
| ~ sP0(b,c,sF596,c,a)
| ~ is_Arr1861959080le_alt(c)
| ~ spl604_1
| ~ spl604_32
| spl604_34
| ~ spl604_37 ),
inference(forward_subsumption_resolution,[],[f7899,f7303]) ).
fof(f7901,plain,
( hBOOL(hAPP_f592646513l_bool(sF595,hAPP_A568203993t_bool(sF598,b)))
| ~ is_Arr1861959080le_alt(c)
| ~ spl604_1
| ~ spl604_32
| spl604_34
| ~ spl604_37 ),
inference(forward_subsumption_resolution,[],[f7900,f6625]) ).
fof(f7902,plain,
( hBOOL(hAPP_f592646513l_bool(sF595,hAPP_A568203993t_bool(sF598,b)))
| ~ spl604_1
| ~ spl604_32
| spl604_34
| ~ spl604_37 ),
inference(forward_subsumption_resolution,[],[f7901,f4102]) ).
fof(f7903,plain,
( hBOOL(hAPP_f592646513l_bool(sF595,sF599))
| ~ spl604_1
| ~ spl604_32
| spl604_34
| ~ spl604_37 ),
inference(forward_demodulation,[],[f7902,f6930]) ).
fof(f7904,plain,
( hBOOL(sF600)
| ~ spl604_1
| ~ spl604_32
| spl604_34
| ~ spl604_37 ),
inference(forward_demodulation,[],[f7903,f6932]) ).
fof(f7905,plain,
( $false
| ~ spl604_1
| spl604_2
| ~ spl604_32
| spl604_34
| ~ spl604_37 ),
inference(forward_subsumption_resolution,[],[f7904,f6974]) ).
fof(f7906,plain,
( ~ spl604_1
| spl604_2
| ~ spl604_32
| spl604_34
| ~ spl604_37 ),
inference(avatar_contradiction_clause,[],[f7905]) ).
cnf(s1,plain,
( spl604_1
| spl604_2 ),
inference(sat_conversion,[],[f6976]) ).
cnf(s2,plain,
( ~ spl604_1
| ~ spl604_2 ),
inference(sat_conversion,[],[f6977]) ).
cnf(s38,plain,
spl604_32,
inference(sat_conversion,[],[f7239]) ).
cnf(s39,plain,
( spl604_1
| ~ spl604_2
| ~ spl604_32 ),
inference(sat_conversion,[],[f7298]) ).
cnf(s41,plain,
~ spl604_34,
inference(sat_conversion,[],[f7369]) ).
cnf(s42,plain,
( spl604_36
| spl604_37 ),
inference(sat_conversion,[],[f7377]) ).
cnf(s43,plain,
~ spl604_36,
inference(sat_conversion,[],[f7411]) ).
cnf(s54,plain,
( ~ spl604_1
| spl604_2
| ~ spl604_32
| spl604_34
| ~ spl604_37 ),
inference(sat_conversion,[],[f7906]) ).
cnf(s59,plain,
spl604_37,
inference(rat,[],[s42,s43]) ).
cnf(s69,plain,
spl604_1,
inference(rat,[],[s1,s39,s38]) ).
cnf(s70,plain,
spl604_2,
inference(rat,[],[s54,s59,s41,s38,s69]) ).
cnf(s72,plain,
$false,
inference(rat,[],[s2,s70,s69]) ).
fof(f7907,plain,
$false,
inference(avatar_sat_refutation,[],[s72]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT170+3 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.16/0.42 % Computer : n020.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Sun Sep 27 23:56:34 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.42 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.23/0.48 Running first-order theorem proving
% 0.23/0.48 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
% 19.37/3.91 % (3891946)Detected formulas, will run a generic FOF schedule.
% 19.37/3.91 % (3891956)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1238197792:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 19.37/3.91 % (3891954)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3604782112:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 19.37/3.91 % (3891953)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=1223912350:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 19.37/3.91 % (3891952)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=1208501250:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 19.37/3.91 % (3891955)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1888732465:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 19.37/3.91 % (3891951)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=3897437657:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 19.37/3.91 % (3891956)Instruction limit reached!
% 19.37/3.91 % (3891956)------------------------------
% 19.37/3.91 % (3891956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.37/3.91 % (3891956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.37/3.91 % (3891956)CaDiCaL version: 2.1.3
% 19.37/3.91 % (3891956)Termination reason: Instruction limit
% 19.37/3.91 % (3891956)Termination phase: Property scanning
% 19.37/3.91 % (3891956)Time elapsed: 0.065 s
% 19.37/3.91 % (3891956)Peak memory usage: 90 MB
% 19.37/3.91 % (3891956)Instructions burned: 139 (million)
% 19.37/3.91 % (3891954)Refutation not found, incomplete strategy
% 19.37/3.91 % (3891954)------------------------------
% 19.37/3.91 % (3891954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.37/3.91 % (3891954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.37/3.91 % (3891954)CaDiCaL version: 2.1.3
% 19.37/3.91 % (3891954)Termination reason: Refutation not found, incomplete strategy
% 19.37/3.91 % (3891954)Time elapsed: 0.019 s
% 19.37/3.91 % (3891954)Peak memory usage: 90 MB
% 19.37/3.91 % (3891954)Instructions burned: 16 (million)
% 19.37/3.91 % (3891957)dis-21_1_sil=8000:lcm=predicate:random_seed=3318418031: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)
% 19.37/3.91 % (3891955)Instruction limit reached!
% 19.37/3.91 % (3891955)------------------------------
% 19.37/3.91 % (3891955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.37/3.91 % (3891955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.37/3.91 % (3891955)CaDiCaL version: 2.1.3
% 19.37/3.91 % (3891955)Termination reason: Instruction limit
% 19.37/3.91 % (3891955)Termination phase: Saturation
% 19.37/3.91 % (3891955)Time elapsed: 0.113 s
% 19.37/3.91 % (3891955)Peak memory usage: 90 MB
% 19.37/3.91 % (3891955)Instructions burned: 119 (million)
% 19.37/3.91 % (3891957)Instruction limit reached!
% 19.37/3.91 % (3891957)------------------------------
% 19.37/3.91 % (3891957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.37/3.91 % (3891957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.37/3.91 % (3891957)CaDiCaL version: 2.1.3
% 19.37/3.91 % (3891957)Termination reason: Instruction limit
% 19.37/3.91 % (3891957)Termination phase: Property scanning
% 19.37/3.91 % (3891957)Time elapsed: 0.109 s
% 19.37/3.91 % (3891957)Peak memory usage: 90 MB
% 19.37/3.91 % (3891957)Instructions burned: 129 (million)
% 19.37/3.91 % (3891964)lrs+10_1_sil=8000:sp=occurrence:random_seed=2699860745:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 19.37/3.91 % (3891966)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4202674403:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 19.37/3.91 % (3891967)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2363237477:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 19.37/3.91 % (3891966)Refutation not found, incomplete strategy
% 19.37/3.91 % (3891966)------------------------------
% 19.37/3.91 % (3891966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.37/3.91 % (3891966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.92/4.37 % (3891966)CaDiCaL version: 2.1.3
% 22.92/4.37 % (3891966)Termination reason: Refutation not found, incomplete strategy
% 22.92/4.37 % (3891966)Time elapsed: 0.042 s
% 22.92/4.37 % (3891966)Peak memory usage: 91 MB
% 22.92/4.37 % (3891966)Instructions burned: 90 (million)
% 22.92/4.37 % (3891954)------------------------------
% 22.92/4.37 % (3891954)------------------------------
% 22.92/4.37 % (3891964)Instruction limit reached!
% 22.92/4.37 % (3891964)------------------------------
% 22.92/4.37 % (3891964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.92/4.37 % (3891964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.92/4.37 % (3891964)CaDiCaL version: 2.1.3
% 22.92/4.37 % (3891964)Termination reason: Instruction limit
% 22.92/4.37 % (3891964)Termination phase: Saturation
% 22.92/4.37 % (3891964)Time elapsed: 0.271 s
% 22.92/4.37 % (3891964)Peak memory usage: 93 MB
% 22.92/4.37 % (3891964)Instructions burned: 286 (million)
% 22.92/4.37 % (3891967)Instruction limit reached!
% 22.92/4.37 % (3891967)------------------------------
% 22.92/4.37 % (3891967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.92/4.37 % (3891967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.92/4.37 % (3891967)CaDiCaL version: 2.1.3
% 22.92/4.37 % (3891967)Termination reason: Instruction limit
% 22.92/4.37 % (3891967)Termination phase: Saturation
% 22.92/4.37 % (3891967)Time elapsed: 0.234 s
% 22.92/4.37 % (3891967)Peak memory usage: 93 MB
% 22.92/4.37 % (3891967)Instructions burned: 326 (million)
% 22.92/4.37 % (3891966)------------------------------
% 22.92/4.37 % (3891966)------------------------------
% 22.92/4.37 % (3891971)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=2046557915:s2a=on:i=248:s2at=1.23:gtg=position_2992 on theBenchmark for (2992ds/248Mi)
% 22.92/4.37 % (3891974)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2557032414:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2991 on theBenchmark for (2991ds/294Mi)
% 22.92/4.37 % (3891976)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2852598160:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 22.92/4.37 % (3891975)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2131937715:i=2350_2990 on theBenchmark for (2990ds/2350Mi)
% 22.92/4.37 % (3891976)Instruction limit reached!
% 22.92/4.37 % (3891976)------------------------------
% 22.92/4.37 % (3891976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.92/4.37 % (3891976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.92/4.37 % (3891976)CaDiCaL version: 2.1.3
% 22.92/4.37 % (3891976)Termination reason: Instruction limit
% 22.92/4.37 % (3891976)Termination phase: Property scanning
% 22.92/4.37 % (3891976)Time elapsed: 0.053 s
% 22.92/4.37 % (3891976)Peak memory usage: 90 MB
% 22.92/4.37 % (3891976)Instructions burned: 114 (million)
% 22.92/4.37 % (3891971)Instruction limit reached!
% 22.92/4.37 % (3891971)------------------------------
% 22.92/4.37 % (3891971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.92/4.37 % (3891971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.92/4.37 % (3891971)CaDiCaL version: 2.1.3
% 22.92/4.37 % (3891971)Termination reason: Instruction limit
% 22.92/4.37 % (3891971)Termination phase: Saturation
% 22.92/4.37 % (3891971)Time elapsed: 0.218 s
% 22.92/4.37 % (3891971)Peak memory usage: 93 MB
% 22.92/4.37 % (3891971)Instructions burned: 249 (million)
% 22.92/4.37 % (3891974)Instruction limit reached!
% 22.92/4.37 % (3891974)------------------------------
% 22.92/4.37 % (3891974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.92/4.37 % (3891974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.92/4.37 % (3891974)CaDiCaL version: 2.1.3
% 22.92/4.37 % (3891974)Termination reason: Instruction limit
% 22.92/4.37 % (3891974)Termination phase: Saturation
% 22.92/4.37 % (3891974)Time elapsed: 0.266 s
% 22.92/4.37 % (3891974)Peak memory usage: 92 MB
% 22.92/4.37 % (3891974)Instructions burned: 295 (million)
% 22.92/4.37 % (3891981)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4252377548:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 22.92/4.37 % (3891982)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1341847619:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi)
% 22.92/4.37 % (3891981)Instruction limit reached!
% 22.92/4.37 % (3891981)------------------------------
% 22.92/4.37 % (3891981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.92/4.37 % (3891981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.92/4.37 % (3891981)CaDiCaL version: 2.1.3
% 22.92/4.37 % (3891981)Termination reason: Instruction limit
% 22.92/4.37 % (3891981)Termination phase: Property scanning
% 22.92/4.37 % (3891981)Time elapsed: 0.112 s
% 22.92/4.37 % (3891981)Peak memory usage: 89 MB
% 22.92/4.37 % (3891981)Instructions burned: 127 (million)
% 22.92/4.37 % (3891982)Instruction limit reached!
% 22.92/4.37 % (3891982)------------------------------
% 22.92/4.37 % (3891982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.92/4.37 % (3891982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.92/4.37 % (3891982)CaDiCaL version: 2.1.3
% 22.92/4.37 % (3891982)Termination reason: Instruction limit
% 22.92/4.37 % (3891982)Termination phase: Saturation
% 22.92/4.37 % (3891982)Time elapsed: 0.101 s
% 22.92/4.37 % (3891982)Peak memory usage: 91 MB
% 22.92/4.37 % (3891982)Instructions burned: 114 (million)
% 22.92/4.37 % (3891983)lrs+10_1_sil=8000:sp=occurrence:random_seed=4235832690:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2986 on theBenchmark for (2986ds/907Mi)
% 22.92/4.37 % (3891986)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=621045398:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 22.92/4.37 % (3891987)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1868823429:i=5202:ss=axioms:sgt=16_2983 on theBenchmark for (2983ds/5202Mi)
% 22.92/4.37 % (3891986)Instruction limit reached!
% 22.92/4.37 % (3891986)------------------------------
% 22.92/4.37 % (3891986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.92/4.37 % (3891986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.92/4.37 % (3891986)CaDiCaL version: 2.1.3
% 22.92/4.37 % (3891986)Termination reason: Instruction limit
% 22.92/4.37 % (3891986)Termination phase: Saturation
% 22.92/4.37 % (3891986)Time elapsed: 0.391 s
% 22.92/4.37 % (3891986)Peak memory usage: 97 MB
% 22.92/4.37 % (3891986)Instructions burned: 438 (million)
% 22.92/4.37 % (3891975)Instruction limit reached!
% 22.92/4.37 % (3891975)------------------------------
% 22.92/4.37 % (3891975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.92/4.37 % (3891975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.92/4.37 % (3891975)CaDiCaL version: 2.1.3
% 22.92/4.37 % (3891975)Termination reason: Instruction limit
% 22.92/4.37 % (3891975)Termination phase: Saturation
% 22.92/4.37 % (3891975)Time elapsed: 1.241 s
% 22.92/4.37 % (3891975)Peak memory usage: 170 MB
% 22.92/4.37 % (3891975)Instructions burned: 2352 (million)
% 22.92/4.37 % (3891991)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2311505713:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2977 on theBenchmark for (2977ds/134Mi)
% 22.92/4.37 % (3891983)Instruction limit reached!
% 22.92/4.37 % (3891983)------------------------------
% 22.92/4.37 % (3891983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.92/4.37 % (3891983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.92/4.37 % (3891983)CaDiCaL version: 2.1.3
% 22.92/4.37 % (3891983)Termination reason: Instruction limit
% 22.92/4.37 % (3891983)Termination phase: Saturation
% 22.92/4.37 % (3891983)Time elapsed: 0.891 s
% 22.92/4.37 % (3891983)Peak memory usage: 99 MB
% 22.92/4.37 % (3891983)Instructions burned: 907 (million)
% 22.92/4.37 % (3891991)Instruction limit reached!
% 22.92/4.37 % (3891991)------------------------------
% 22.92/4.37 % (3891991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.92/4.37 % (3891991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.92/4.37 % (3891991)CaDiCaL version: 2.1.3
% 22.92/4.37 % (3891991)Termination reason: Instruction limit
% 22.92/4.37 % (3891991)Termination phase: Property scanning
% 22.92/4.37 % (3891991)Time elapsed: 0.115 s
% 22.92/4.37 % (3891991)Peak memory usage: 90 MB
% 22.92/4.37 % (3891991)Instructions burned: 135 (million)
% 22.92/4.37 % (3891992)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2132083809:st=8:i=592:sd=3:ep=RST:ss=axioms_2975 on theBenchmark for (2975ds/592Mi)
% 22.92/4.37 % (3891994)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3209845835:st=3:i=13193:sd=3:ss=axioms_2974 on theBenchmark for (2974ds/13193Mi)
% 22.92/4.37 % (3891995)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=2900933953:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/125Mi)
% 22.92/4.37 % (3891951)First to succeed.
% 22.92/4.37 % (3891951)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3891946"
% 22.92/4.37 % (3891992)Instruction limit reached!
% 22.92/4.37 % (3891992)------------------------------
% 22.92/4.37 % (3891992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.92/4.37 % (3891992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.92/4.37 % (3891992)CaDiCaL version: 2.1.3
% 22.92/4.37 % (3891992)Termination reason: Instruction limit
% 22.92/4.37 % (3891992)Termination phase: Saturation
% 22.92/4.37 % (3891992)Time elapsed: 0.334 s
% 22.92/4.37 % (3891992)Peak memory usage: 96 MB
% 22.92/4.37 % (3891992)Instructions burned: 592 (million)
% 22.92/4.37 % (3891995)Instruction limit reached!
% 22.92/4.37 % (3891995)------------------------------
% 22.92/4.37 % (3891995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.92/4.37 % (3891995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.92/4.37 % (3891995)CaDiCaL version: 2.1.3
% 22.92/4.37 % (3891995)Termination reason: Instruction limit
% 22.92/4.37 % (3891995)Termination phase: Saturation
% 22.92/4.37 % (3891995)Time elapsed: 0.113 s
% 22.92/4.37 % (3891995)Peak memory usage: 92 MB
% 22.92/4.37 % (3891995)Instructions burned: 125 (million)
% 22.92/4.37 % (3892001)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3077204335:i=134:gtgl=5:slsql=off:gtg=exists_sym_2970 on theBenchmark for (2970ds/134Mi)
% 22.92/4.37 % (3892002)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3851355426:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/141Mi)
% 22.92/4.37 % (3891951)Refutation found. Thanks to Tanya!
% 22.92/4.37 % SZS status Theorem for theBenchmark
% 22.92/4.37 % SZS output start Proof for theBenchmark
% See solution above
% 23.89/4.65 % (3891951)------------------------------
% 23.89/4.65 % (3891951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.89/4.65 % (3891951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.89/4.65 % (3891951)CaDiCaL version: 2.1.3
% 23.89/4.65 % (3891951)Termination reason: Refutation
% 23.89/4.65 % (3891951)Time elapsed: 2.556 s
% 23.89/4.65 % (3891951)Peak memory usage: 159 MB
% 23.89/4.65 % (3891951)Instructions burned: 2632 (million)
% 23.89/4.65 % (3891951)------------------------------
% 23.89/4.65 % (3891951)------------------------------
% 23.89/4.65 % (3891946)Success in time 3.347 s
% 23.89/4.65 % Vampire exiting
%------------------------------------------------------------------------------