%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP009+5 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:27:57 AM UTC 2026
% Result : Theorem 24.39s 17.95s
% Output : Refutation 43.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 22
% Syntax : Number of formulae : 266 ( 35 unt; 13 def)
% Number of atoms : 1975 ( 43 equ)
% Maximal formula atoms : 23 ( 7 avg)
% Number of connectives : 3223 (1514 ~;1517 |; 100 &)
% ( 20 <=>; 70 =>; 0 <=; 2 <~>)
% Maximal formula depth : 34 ( 11 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 18 ( 16 usr; 14 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 13 con; 0-4 aty)
% Number of variables : 845 ( 0 sgn 797 !; 48 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> ne(arr(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arr_ne) ).
fof(f4,axiom,
! [X0,X1,X2] :
( mem(X2,arr(X0,X1))
=> ! [X3] :
( mem(X3,X0)
=> mem(ap(X2,X3),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ap_tp) ).
fof(f7163,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> ! [X2] :
( ne(X2)
=> ! [X3] :
( ne(X3)
=> mem(c_2Equotient_2E_2D_2D_3E(X0,X1,X2,X3),arr(arr(X0,X2),arr(arr(X1,X3),arr(arr(X2,X1),arr(X0,X3))))) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Equotient_2E_2D_2D_3E) ).
fof(f7164,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> mem(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),arr(arr(X0,arr(X0,bool)),arr(arr(X1,arr(X1,bool)),arr(arr(X0,X1),arr(arr(X0,X1),bool))))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Equotient_2E_3D_3D_3D_3E) ).
fof(f7177,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> ! [X2] :
( mem(X2,arr(X0,arr(X0,bool)))
=> ! [X3] :
( mem(X3,arr(X0,X1))
=> ! [X4] :
( mem(X4,arr(X1,X0))
=> ( p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X1),X2),X3),X4))
=> ! [X5] :
( mem(X5,X0)
=> ! [X6] :
( mem(X6,X0)
=> ( p(ap(ap(X2,X5),X6))
<=> ( p(ap(ap(X2,X5),X5))
& p(ap(ap(X2,X6),X6))
& ap(X3,X5) = ap(X3,X6) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Equotient_2EQUOTIENT__REL) ).
fof(f7185,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> ! [X2] :
( mem(X2,arr(X0,arr(X0,bool)))
=> ! [X3] :
( mem(X3,arr(X0,X1))
=> ! [X4] :
( mem(X4,arr(X1,X0))
=> ( p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X1),X2),X3),X4))
=> ! [X5] :
( mem(X5,X0)
=> ! [X6] :
( mem(X6,X0)
=> ( p(ap(ap(X2,X5),X6))
=> p(ap(ap(X2,X6),X5)) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Equotient_2EQUOTIENT__SYM) ).
fof(f7195,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> ! [X2] :
( ne(X2)
=> ! [X3] :
( ne(X3)
=> ! [X4] :
( mem(X4,arr(X0,arr(X0,bool)))
=> ! [X5] :
( mem(X5,arr(X0,X2))
=> ! [X6] :
( mem(X6,arr(X2,X0))
=> ( p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X2),X4),X5),X6))
=> ! [X7] :
( mem(X7,arr(X1,arr(X1,bool)))
=> ! [X8] :
( mem(X8,arr(X1,X3))
=> ! [X9] :
( mem(X9,arr(X3,X1))
=> ( p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X3),X7),X8),X9))
=> p(ap(ap(ap(c_2Equotient_2EQUOTIENT(arr(X0,X1),arr(X2,X3)),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7)),ap(ap(c_2Equotient_2E_2D_2D_3E(X2,X1,X0,X3),X6),X8)),ap(ap(c_2Equotient_2E_2D_2D_3E(X0,X3,X2,X1),X5),X9))) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Equotient_2EFUN__QUOTIENT) ).
fof(f7197,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( mem(X1,arr(X0,arr(X0,bool)))
=> ! [X2] :
( mem(X2,X0)
=> ( p(ap(ap(c_2Equotient_2Erespects(X0,bool),X1),X2))
<=> p(ap(ap(X1,X2),X2)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Equotient_2ERESPECTS) ).
fof(f7212,conjecture,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> ! [X2] :
( ne(X2)
=> ! [X3] :
( ne(X3)
=> ! [X4] :
( mem(X4,arr(X0,arr(X0,bool)))
=> ! [X5] :
( mem(X5,arr(X0,X2))
=> ! [X6] :
( mem(X6,arr(X2,X0))
=> ( p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X2),X4),X5),X6))
=> ! [X7] :
( mem(X7,arr(X1,arr(X1,bool)))
=> ! [X8] :
( mem(X8,arr(X1,X3))
=> ! [X9] :
( mem(X9,arr(X3,X1))
=> ( p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X3),X7),X8),X9))
=> ! [X10] :
( mem(X10,arr(X0,X1))
=> ! [X11] :
( mem(X11,arr(X0,X1))
=> ( p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7),X10),X11))
<=> ( p(ap(ap(c_2Equotient_2Erespects(arr(X0,X1),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7)),X10))
& p(ap(ap(c_2Equotient_2Erespects(arr(X0,X1),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7)),X11))
& ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X2,X1,X0,X3),X6),X8),X10) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X2,X1,X0,X3),X6),X8),X11) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Equotient_2EFUN__REL__EQ__REL) ).
fof(f7213,negated_conjecture,
~ ! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> ! [X2] :
( ne(X2)
=> ! [X3] :
( ne(X3)
=> ! [X4] :
( mem(X4,arr(X0,arr(X0,bool)))
=> ! [X5] :
( mem(X5,arr(X0,X2))
=> ! [X6] :
( mem(X6,arr(X2,X0))
=> ( p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X2),X4),X5),X6))
=> ! [X7] :
( mem(X7,arr(X1,arr(X1,bool)))
=> ! [X8] :
( mem(X8,arr(X1,X3))
=> ! [X9] :
( mem(X9,arr(X3,X1))
=> ( p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X3),X7),X8),X9))
=> ! [X10] :
( mem(X10,arr(X0,X1))
=> ! [X11] :
( mem(X11,arr(X0,X1))
=> ( p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7),X10),X11))
<=> ( p(ap(ap(c_2Equotient_2Erespects(arr(X0,X1),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7)),X10))
& p(ap(ap(c_2Equotient_2Erespects(arr(X0,X1),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7)),X11))
& ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X2,X1,X0,X3),X6),X8),X10) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X2,X1,X0,X3),X6),X8),X11) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f7212]) ).
fof(f7284,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ? [X6] :
( ? [X7] :
( ? [X8] :
( ? [X9] :
( ? [X10] :
( ? [X11] :
( ( p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7),X10),X11))
<~> ( p(ap(ap(c_2Equotient_2Erespects(arr(X0,X1),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7)),X10))
& p(ap(ap(c_2Equotient_2Erespects(arr(X0,X1),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7)),X11))
& ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X2,X1,X0,X3),X6),X8),X10) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X2,X1,X0,X3),X6),X8),X11) ) )
& mem(X11,arr(X0,X1)) )
& mem(X10,arr(X0,X1)) )
& p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X3),X7),X8),X9))
& mem(X9,arr(X3,X1)) )
& mem(X8,arr(X1,X3)) )
& mem(X7,arr(X1,arr(X1,bool))) )
& p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X2),X4),X5),X6))
& mem(X6,arr(X2,X0)) )
& mem(X5,arr(X0,X2)) )
& mem(X4,arr(X0,arr(X0,bool))) )
& ne(X3) )
& ne(X2) )
& ne(X1) )
& ne(X0) ),
inference(ennf_transformation,[],[f7213]) ).
fof(f7285,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ? [X6] :
( ? [X7] :
( ? [X8] :
( ? [X9] :
( ? [X10] :
( ? [X11] :
( ( p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7),X10),X11))
<~> ( p(ap(ap(c_2Equotient_2Erespects(arr(X0,X1),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7)),X10))
& p(ap(ap(c_2Equotient_2Erespects(arr(X0,X1),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7)),X11))
& ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X2,X1,X0,X3),X6),X8),X10) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X2,X1,X0,X3),X6),X8),X11) ) )
& mem(X11,arr(X0,X1)) )
& mem(X10,arr(X0,X1)) )
& p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X3),X7),X8),X9))
& mem(X9,arr(X3,X1)) )
& mem(X8,arr(X1,X3)) )
& mem(X7,arr(X1,arr(X1,bool))) )
& p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X2),X4),X5),X6))
& mem(X6,arr(X2,X0)) )
& mem(X5,arr(X0,X2)) )
& mem(X4,arr(X0,arr(X0,bool))) )
& ne(X3) )
& ne(X2) )
& ne(X1) )
& ne(X0) ),
inference(flattening,[],[f7284]) ).
fof(f7515,plain,
! [X0] :
( ! [X1] :
( ne(arr(X0,X1))
| ~ ne(X1) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f7516,plain,
! [X0,X1,X2] :
( ! [X3] :
( mem(ap(X2,X3),X1)
| ~ mem(X3,X0) )
| ~ mem(X2,arr(X0,X1)) ),
inference(ennf_transformation,[],[f4]) ).
fof(f7517,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( p(ap(ap(ap(c_2Equotient_2EQUOTIENT(arr(X0,X1),arr(X2,X3)),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7)),ap(ap(c_2Equotient_2E_2D_2D_3E(X2,X1,X0,X3),X6),X8)),ap(ap(c_2Equotient_2E_2D_2D_3E(X0,X3,X2,X1),X5),X9)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X3),X7),X8),X9))
| ~ mem(X9,arr(X3,X1)) )
| ~ mem(X8,arr(X1,X3)) )
| ~ mem(X7,arr(X1,arr(X1,bool))) )
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X2),X4),X5),X6))
| ~ mem(X6,arr(X2,X0)) )
| ~ mem(X5,arr(X0,X2)) )
| ~ mem(X4,arr(X0,arr(X0,bool))) )
| ~ ne(X3) )
| ~ ne(X2) )
| ~ ne(X1) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f7195]) ).
fof(f7518,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( p(ap(ap(ap(c_2Equotient_2EQUOTIENT(arr(X0,X1),arr(X2,X3)),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7)),ap(ap(c_2Equotient_2E_2D_2D_3E(X2,X1,X0,X3),X6),X8)),ap(ap(c_2Equotient_2E_2D_2D_3E(X0,X3,X2,X1),X5),X9)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X3),X7),X8),X9))
| ~ mem(X9,arr(X3,X1)) )
| ~ mem(X8,arr(X1,X3)) )
| ~ mem(X7,arr(X1,arr(X1,bool))) )
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X2),X4),X5),X6))
| ~ mem(X6,arr(X2,X0)) )
| ~ mem(X5,arr(X0,X2)) )
| ~ mem(X4,arr(X0,arr(X0,bool))) )
| ~ ne(X3) )
| ~ ne(X2) )
| ~ ne(X1) )
| ~ ne(X0) ),
inference(flattening,[],[f7517]) ).
fof(f7522,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( mem(c_2Equotient_2E_2D_2D_3E(X0,X1,X2,X3),arr(arr(X0,X2),arr(arr(X1,X3),arr(arr(X2,X1),arr(X0,X3)))))
| ~ ne(X3) )
| ~ ne(X2) )
| ~ ne(X1) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f7163]) ).
fof(f7534,plain,
! [X0] :
( ! [X1] :
( mem(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),arr(arr(X0,arr(X0,bool)),arr(arr(X1,arr(X1,bool)),arr(arr(X0,X1),arr(arr(X0,X1),bool)))))
| ~ ne(X1) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f7164]) ).
fof(f7537,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( p(ap(ap(X2,X6),X5))
| ~ p(ap(ap(X2,X5),X6))
| ~ mem(X6,X0) )
| ~ mem(X5,X0) )
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X1),X2),X3),X4))
| ~ mem(X4,arr(X1,X0)) )
| ~ mem(X3,arr(X0,X1)) )
| ~ mem(X2,arr(X0,arr(X0,bool))) )
| ~ ne(X1) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f7185]) ).
fof(f7538,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( p(ap(ap(X2,X6),X5))
| ~ p(ap(ap(X2,X5),X6))
| ~ mem(X6,X0) )
| ~ mem(X5,X0) )
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X1),X2),X3),X4))
| ~ mem(X4,arr(X1,X0)) )
| ~ mem(X3,arr(X0,X1)) )
| ~ mem(X2,arr(X0,arr(X0,bool))) )
| ~ ne(X1) )
| ~ ne(X0) ),
inference(flattening,[],[f7537]) ).
fof(f7548,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ( p(ap(ap(X2,X5),X6))
<=> ( p(ap(ap(X2,X5),X5))
& p(ap(ap(X2,X6),X6))
& ap(X3,X5) = ap(X3,X6) ) )
| ~ mem(X6,X0) )
| ~ mem(X5,X0) )
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X1),X2),X3),X4))
| ~ mem(X4,arr(X1,X0)) )
| ~ mem(X3,arr(X0,X1)) )
| ~ mem(X2,arr(X0,arr(X0,bool))) )
| ~ ne(X1) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f7177]) ).
fof(f7549,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ( p(ap(ap(X2,X5),X6))
<=> ( p(ap(ap(X2,X5),X5))
& p(ap(ap(X2,X6),X6))
& ap(X3,X5) = ap(X3,X6) ) )
| ~ mem(X6,X0) )
| ~ mem(X5,X0) )
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X1),X2),X3),X4))
| ~ mem(X4,arr(X1,X0)) )
| ~ mem(X3,arr(X0,X1)) )
| ~ mem(X2,arr(X0,arr(X0,bool))) )
| ~ ne(X1) )
| ~ ne(X0) ),
inference(flattening,[],[f7548]) ).
fof(f7557,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( p(ap(ap(c_2Equotient_2Erespects(X0,bool),X1),X2))
<=> p(ap(ap(X1,X2),X2)) )
| ~ mem(X2,X0) )
| ~ mem(X1,arr(X0,arr(X0,bool))) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f7197]) ).
fof(f8913,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ? [X6] :
( ? [X7] :
( ? [X8] :
( ? [X9] :
( ? [X10] :
( ? [X11] :
( ( ~ p(ap(ap(c_2Equotient_2Erespects(arr(X0,X1),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7)),X10))
| ~ p(ap(ap(c_2Equotient_2Erespects(arr(X0,X1),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7)),X11))
| ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X2,X1,X0,X3),X6),X8),X10) != ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X2,X1,X0,X3),X6),X8),X11)
| ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7),X10),X11)) )
& ( ( p(ap(ap(c_2Equotient_2Erespects(arr(X0,X1),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7)),X10))
& p(ap(ap(c_2Equotient_2Erespects(arr(X0,X1),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7)),X11))
& ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X2,X1,X0,X3),X6),X8),X10) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X2,X1,X0,X3),X6),X8),X11) )
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7),X10),X11)) )
& mem(X11,arr(X0,X1)) )
& mem(X10,arr(X0,X1)) )
& p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X3),X7),X8),X9))
& mem(X9,arr(X3,X1)) )
& mem(X8,arr(X1,X3)) )
& mem(X7,arr(X1,arr(X1,bool))) )
& p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X2),X4),X5),X6))
& mem(X6,arr(X2,X0)) )
& mem(X5,arr(X0,X2)) )
& mem(X4,arr(X0,arr(X0,bool))) )
& ne(X3) )
& ne(X2) )
& ne(X1) )
& ne(X0) ),
inference(nnf_transformation,[],[f7285]) ).
fof(f8914,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ? [X6] :
( ? [X7] :
( ? [X8] :
( ? [X9] :
( ? [X10] :
( ? [X11] :
( ( ~ p(ap(ap(c_2Equotient_2Erespects(arr(X0,X1),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7)),X10))
| ~ p(ap(ap(c_2Equotient_2Erespects(arr(X0,X1),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7)),X11))
| ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X2,X1,X0,X3),X6),X8),X10) != ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X2,X1,X0,X3),X6),X8),X11)
| ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7),X10),X11)) )
& ( ( p(ap(ap(c_2Equotient_2Erespects(arr(X0,X1),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7)),X10))
& p(ap(ap(c_2Equotient_2Erespects(arr(X0,X1),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7)),X11))
& ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X2,X1,X0,X3),X6),X8),X10) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X2,X1,X0,X3),X6),X8),X11) )
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7),X10),X11)) )
& mem(X11,arr(X0,X1)) )
& mem(X10,arr(X0,X1)) )
& p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X3),X7),X8),X9))
& mem(X9,arr(X3,X1)) )
& mem(X8,arr(X1,X3)) )
& mem(X7,arr(X1,arr(X1,bool))) )
& p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X2),X4),X5),X6))
& mem(X6,arr(X2,X0)) )
& mem(X5,arr(X0,X2)) )
& mem(X4,arr(X0,arr(X0,bool))) )
& ne(X3) )
& ne(X2) )
& ne(X1) )
& ne(X0) ),
inference(flattening,[],[f8913]) ).
fof(f8915,plain,
( ( ~ p(ap(ap(c_2Equotient_2Erespects(arr(sK150,sK151),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157)),sK160))
| ~ p(ap(ap(c_2Equotient_2Erespects(arr(sK150,sK151),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157)),sK161))
| ap(ap(ap(c_2Equotient_2E_2D_2D_3E(sK152,sK151,sK150,sK153),sK156),sK158),sK160) != ap(ap(ap(c_2Equotient_2E_2D_2D_3E(sK152,sK151,sK150,sK153),sK156),sK158),sK161)
| ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK160),sK161)) )
& ( ( p(ap(ap(c_2Equotient_2Erespects(arr(sK150,sK151),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157)),sK160))
& p(ap(ap(c_2Equotient_2Erespects(arr(sK150,sK151),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157)),sK161))
& ap(ap(ap(c_2Equotient_2E_2D_2D_3E(sK152,sK151,sK150,sK153),sK156),sK158),sK160) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(sK152,sK151,sK150,sK153),sK156),sK158),sK161) )
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK160),sK161)) )
& mem(sK161,arr(sK150,sK151))
& mem(sK160,arr(sK150,sK151))
& p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,sK153),sK157),sK158),sK159))
& mem(sK159,arr(sK153,sK151))
& mem(sK158,arr(sK151,sK153))
& mem(sK157,arr(sK151,arr(sK151,bool)))
& p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,sK152),sK154),sK155),sK156))
& mem(sK156,arr(sK152,sK150))
& mem(sK155,arr(sK150,sK152))
& mem(sK154,arr(sK150,arr(sK150,bool)))
& ne(sK153)
& ne(sK152)
& ne(sK151)
& ne(sK150) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK150,sK151,sK152,sK153,sK154,sK155,sK156,sK157,sK158,sK159,sK160,sK161]),skolemize(X0,sK150),skolemize(X1,sK151),skolemize(X2,sK152),skolemize(X3,sK153),skolemize(X4,sK154),skolemize(X5,sK155),skolemize(X6,sK156),skolemize(X7,sK157),skolemize(X8,sK158),skolemize(X9,sK159),skolemize(X10,sK160),skolemize(X11,sK161)],[f8914]) ).
fof(f9324,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ( ( p(ap(ap(X2,X5),X6))
| ~ p(ap(ap(X2,X5),X5))
| ~ p(ap(ap(X2,X6),X6))
| ap(X3,X5) != ap(X3,X6) )
& ( ( p(ap(ap(X2,X5),X5))
& p(ap(ap(X2,X6),X6))
& ap(X3,X5) = ap(X3,X6) )
| ~ p(ap(ap(X2,X5),X6)) ) )
| ~ mem(X6,X0) )
| ~ mem(X5,X0) )
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X1),X2),X3),X4))
| ~ mem(X4,arr(X1,X0)) )
| ~ mem(X3,arr(X0,X1)) )
| ~ mem(X2,arr(X0,arr(X0,bool))) )
| ~ ne(X1) )
| ~ ne(X0) ),
inference(nnf_transformation,[],[f7549]) ).
fof(f9325,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ( ( p(ap(ap(X2,X5),X6))
| ~ p(ap(ap(X2,X5),X5))
| ~ p(ap(ap(X2,X6),X6))
| ap(X3,X5) != ap(X3,X6) )
& ( ( p(ap(ap(X2,X5),X5))
& p(ap(ap(X2,X6),X6))
& ap(X3,X5) = ap(X3,X6) )
| ~ p(ap(ap(X2,X5),X6)) ) )
| ~ mem(X6,X0) )
| ~ mem(X5,X0) )
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X1),X2),X3),X4))
| ~ mem(X4,arr(X1,X0)) )
| ~ mem(X3,arr(X0,X1)) )
| ~ mem(X2,arr(X0,arr(X0,bool))) )
| ~ ne(X1) )
| ~ ne(X0) ),
inference(flattening,[],[f9324]) ).
fof(f9335,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( p(ap(ap(c_2Equotient_2Erespects(X0,bool),X1),X2))
| ~ p(ap(ap(X1,X2),X2)) )
& ( p(ap(ap(X1,X2),X2))
| ~ p(ap(ap(c_2Equotient_2Erespects(X0,bool),X1),X2)) ) )
| ~ mem(X2,X0) )
| ~ mem(X1,arr(X0,arr(X0,bool))) )
| ~ ne(X0) ),
inference(nnf_transformation,[],[f7557]) ).
fof(f10249,plain,
ne(sK150),
inference(cnf_transformation,[],[f8915]) ).
fof(f10250,plain,
ne(sK151),
inference(cnf_transformation,[],[f8915]) ).
fof(f10251,plain,
ne(sK152),
inference(cnf_transformation,[],[f8915]) ).
fof(f10252,plain,
ne(sK153),
inference(cnf_transformation,[],[f8915]) ).
fof(f10253,plain,
mem(sK154,arr(sK150,arr(sK150,bool))),
inference(cnf_transformation,[],[f8915]) ).
fof(f10254,plain,
mem(sK155,arr(sK150,sK152)),
inference(cnf_transformation,[],[f8915]) ).
fof(f10255,plain,
mem(sK156,arr(sK152,sK150)),
inference(cnf_transformation,[],[f8915]) ).
fof(f10256,plain,
p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,sK152),sK154),sK155),sK156)),
inference(cnf_transformation,[],[f8915]) ).
fof(f10257,plain,
mem(sK157,arr(sK151,arr(sK151,bool))),
inference(cnf_transformation,[],[f8915]) ).
fof(f10258,plain,
mem(sK158,arr(sK151,sK153)),
inference(cnf_transformation,[],[f8915]) ).
fof(f10259,plain,
mem(sK159,arr(sK153,sK151)),
inference(cnf_transformation,[],[f8915]) ).
fof(f10260,plain,
p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,sK153),sK157),sK158),sK159)),
inference(cnf_transformation,[],[f8915]) ).
fof(f10261,plain,
mem(sK160,arr(sK150,sK151)),
inference(cnf_transformation,[],[f8915]) ).
fof(f10262,plain,
mem(sK161,arr(sK150,sK151)),
inference(cnf_transformation,[],[f8915]) ).
fof(f10263,plain,
( ap(ap(ap(c_2Equotient_2E_2D_2D_3E(sK152,sK151,sK150,sK153),sK156),sK158),sK160) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(sK152,sK151,sK150,sK153),sK156),sK158),sK161)
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK160),sK161)) ),
inference(cnf_transformation,[],[f8915]) ).
fof(f10264,plain,
( p(ap(ap(c_2Equotient_2Erespects(arr(sK150,sK151),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157)),sK161))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK160),sK161)) ),
inference(cnf_transformation,[],[f8915]) ).
fof(f10265,plain,
( p(ap(ap(c_2Equotient_2Erespects(arr(sK150,sK151),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157)),sK160))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK160),sK161)) ),
inference(cnf_transformation,[],[f8915]) ).
fof(f10266,plain,
( ~ p(ap(ap(c_2Equotient_2Erespects(arr(sK150,sK151),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157)),sK160))
| ~ p(ap(ap(c_2Equotient_2Erespects(arr(sK150,sK151),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157)),sK161))
| ap(ap(ap(c_2Equotient_2E_2D_2D_3E(sK152,sK151,sK150,sK153),sK156),sK158),sK160) != ap(ap(ap(c_2Equotient_2E_2D_2D_3E(sK152,sK151,sK150,sK153),sK156),sK158),sK161)
| ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK160),sK161)) ),
inference(cnf_transformation,[],[f8915]) ).
fof(f11164,plain,
! [X0,X1] :
( ne(arr(X0,X1))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f7515]) ).
fof(f11165,plain,
! [X2,X3,X0,X1] :
( ~ mem(X2,arr(X0,X1))
| ~ mem(X3,X0)
| mem(ap(X2,X3),X1) ),
inference(cnf_transformation,[],[f7516]) ).
fof(f11166,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( p(ap(ap(ap(c_2Equotient_2EQUOTIENT(arr(X0,X1),arr(X2,X3)),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X4),X7)),ap(ap(c_2Equotient_2E_2D_2D_3E(X2,X1,X0,X3),X6),X8)),ap(ap(c_2Equotient_2E_2D_2D_3E(X0,X3,X2,X1),X5),X9)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X3),X7),X8),X9))
| ~ mem(X9,arr(X3,X1))
| ~ mem(X8,arr(X1,X3))
| ~ mem(X7,arr(X1,arr(X1,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X2),X4),X5),X6))
| ~ mem(X6,arr(X2,X0))
| ~ mem(X5,arr(X0,X2))
| ~ mem(X4,arr(X0,arr(X0,bool)))
| ~ ne(X3)
| ~ ne(X2)
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f7518]) ).
fof(f11171,plain,
! [X2,X3,X0,X1] :
( mem(c_2Equotient_2E_2D_2D_3E(X0,X1,X2,X3),arr(arr(X0,X2),arr(arr(X1,X3),arr(arr(X2,X1),arr(X0,X3)))))
| ~ ne(X3)
| ~ ne(X2)
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f7522]) ).
fof(f11186,plain,
! [X0,X1] :
( mem(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),arr(arr(X0,arr(X0,bool)),arr(arr(X1,arr(X1,bool)),arr(arr(X0,X1),arr(arr(X0,X1),bool)))))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f7534]) ).
fof(f11188,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X1),X2),X3),X4))
| ~ p(ap(ap(X2,X5),X6))
| ~ mem(X6,X0)
| ~ mem(X5,X0)
| p(ap(ap(X2,X6),X5))
| ~ mem(X4,arr(X1,X0))
| ~ mem(X3,arr(X0,X1))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f7538]) ).
fof(f11196,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X1),X2),X3),X4))
| ~ p(ap(ap(X2,X5),X6))
| ~ mem(X6,X0)
| ~ mem(X5,X0)
| ap(X3,X5) = ap(X3,X6)
| ~ mem(X4,arr(X1,X0))
| ~ mem(X3,arr(X0,X1))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f9325]) ).
fof(f11197,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X1),X2),X3),X4))
| ~ p(ap(ap(X2,X5),X6))
| ~ mem(X6,X0)
| ~ mem(X5,X0)
| p(ap(ap(X2,X6),X6))
| ~ mem(X4,arr(X1,X0))
| ~ mem(X3,arr(X0,X1))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f9325]) ).
fof(f11198,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X1),X2),X3),X4))
| ~ p(ap(ap(X2,X5),X6))
| ~ mem(X6,X0)
| ~ mem(X5,X0)
| p(ap(ap(X2,X5),X5))
| ~ mem(X4,arr(X1,X0))
| ~ mem(X3,arr(X0,X1))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f9325]) ).
fof(f11199,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ap(X3,X5) != ap(X3,X6)
| ~ p(ap(ap(X2,X5),X5))
| ~ p(ap(ap(X2,X6),X6))
| p(ap(ap(X2,X5),X6))
| ~ mem(X6,X0)
| ~ mem(X5,X0)
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X1),X2),X3),X4))
| ~ mem(X4,arr(X1,X0))
| ~ mem(X3,arr(X0,X1))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f9325]) ).
fof(f11222,plain,
! [X2,X0,X1] :
( ~ p(ap(ap(c_2Equotient_2Erespects(X0,bool),X1),X2))
| p(ap(ap(X1,X2),X2))
| ~ mem(X2,X0)
| ~ mem(X1,arr(X0,arr(X0,bool)))
| ~ ne(X0) ),
inference(cnf_transformation,[],[f9335]) ).
fof(f11223,plain,
! [X2,X0,X1] :
( ~ mem(X1,arr(X0,arr(X0,bool)))
| ~ p(ap(ap(X1,X2),X2))
| ~ mem(X2,X0)
| p(ap(ap(c_2Equotient_2Erespects(X0,bool),X1),X2))
| ~ ne(X0) ),
inference(cnf_transformation,[],[f9335]) ).
fof(f14481,definition,
( spl700_69
<=> p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK160),sK161)) ),
introduced(definition,[new_symbols(definition,[spl700_69])],[avatar_definition]) ).
fof(f14482,plain,
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK160),sK161))
| spl700_69 ),
inference(avatar_component_clause,[],[f14481]) ).
fof(f14483,plain,
( p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK160),sK161))
| ~ spl700_69 ),
inference(avatar_component_clause,[],[f14481]) ).
fof(f14485,definition,
( spl700_70
<=> ap(ap(ap(c_2Equotient_2E_2D_2D_3E(sK152,sK151,sK150,sK153),sK156),sK158),sK160) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(sK152,sK151,sK150,sK153),sK156),sK158),sK161) ),
introduced(definition,[new_symbols(definition,[spl700_70])],[avatar_definition]) ).
fof(f14486,plain,
( ap(ap(ap(c_2Equotient_2E_2D_2D_3E(sK152,sK151,sK150,sK153),sK156),sK158),sK160) != ap(ap(ap(c_2Equotient_2E_2D_2D_3E(sK152,sK151,sK150,sK153),sK156),sK158),sK161)
| spl700_70 ),
inference(avatar_component_clause,[],[f14485]) ).
fof(f14487,plain,
( ap(ap(ap(c_2Equotient_2E_2D_2D_3E(sK152,sK151,sK150,sK153),sK156),sK158),sK160) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(sK152,sK151,sK150,sK153),sK156),sK158),sK161)
| ~ spl700_70 ),
inference(avatar_component_clause,[],[f14485]) ).
fof(f14488,plain,
( spl700_69
| spl700_70 ),
inference(avatar_split_clause,[],[f10263,f14485,f14481]) ).
fof(f14490,definition,
( spl700_71
<=> p(ap(ap(c_2Equotient_2Erespects(arr(sK150,sK151),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157)),sK161)) ),
introduced(definition,[new_symbols(definition,[spl700_71])],[avatar_definition]) ).
fof(f14491,plain,
( ~ p(ap(ap(c_2Equotient_2Erespects(arr(sK150,sK151),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157)),sK161))
| spl700_71 ),
inference(avatar_component_clause,[],[f14490]) ).
fof(f14492,plain,
( p(ap(ap(c_2Equotient_2Erespects(arr(sK150,sK151),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157)),sK161))
| ~ spl700_71 ),
inference(avatar_component_clause,[],[f14490]) ).
fof(f14493,plain,
( spl700_69
| spl700_71 ),
inference(avatar_split_clause,[],[f10264,f14490,f14481]) ).
fof(f14495,definition,
( spl700_72
<=> p(ap(ap(c_2Equotient_2Erespects(arr(sK150,sK151),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157)),sK160)) ),
introduced(definition,[new_symbols(definition,[spl700_72])],[avatar_definition]) ).
fof(f14496,plain,
( ~ p(ap(ap(c_2Equotient_2Erespects(arr(sK150,sK151),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157)),sK160))
| spl700_72 ),
inference(avatar_component_clause,[],[f14495]) ).
fof(f14497,plain,
( p(ap(ap(c_2Equotient_2Erespects(arr(sK150,sK151),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157)),sK160))
| ~ spl700_72 ),
inference(avatar_component_clause,[],[f14495]) ).
fof(f14498,plain,
( spl700_69
| spl700_72 ),
inference(avatar_split_clause,[],[f10265,f14495,f14481]) ).
fof(f14499,plain,
( ~ spl700_69
| ~ spl700_70
| ~ spl700_71
| ~ spl700_72 ),
inference(avatar_split_clause,[],[f10266,f14495,f14490,f14485,f14481]) ).
fof(f14521,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X5))
| ~ mem(X5,arr(X0,X1))
| ~ mem(X4,arr(X0,X1))
| ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X6,X1,X0,X7),X8),X9),X4) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X6,X1,X0,X7),X8),X9),X5)
| ~ mem(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,X7,X6,X1),X10),X11),arr(arr(X6,X7),arr(X0,X1)))
| ~ mem(ap(ap(c_2Equotient_2E_2D_2D_3E(X6,X1,X0,X7),X8),X9),arr(arr(X0,X1),arr(X6,X7)))
| ~ mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),arr(arr(X0,X1),arr(arr(X0,X1),bool)))
| ~ ne(arr(X6,X7))
| ~ ne(arr(X0,X1))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X7),X3),X9),X11))
| ~ mem(X11,arr(X7,X1))
| ~ mem(X9,arr(X1,X7))
| ~ mem(X3,arr(X1,arr(X1,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X6),X2),X10),X8))
| ~ mem(X8,arr(X6,X0))
| ~ mem(X10,arr(X0,X6))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X7)
| ~ ne(X6)
| ~ ne(X1)
| ~ ne(X0) ),
inference(resolution,[],[f11196,f11166]) ).
fof(f14528,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X5))
| ~ mem(X5,arr(X0,X1))
| ~ mem(X4,arr(X0,X1))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X5),X5))
| ~ mem(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,X6,X7,X1),X8),X9),arr(arr(X7,X6),arr(X0,X1)))
| ~ mem(ap(ap(c_2Equotient_2E_2D_2D_3E(X7,X1,X0,X6),X10),X11),arr(arr(X0,X1),arr(X7,X6)))
| ~ mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),arr(arr(X0,X1),arr(arr(X0,X1),bool)))
| ~ ne(arr(X7,X6))
| ~ ne(arr(X0,X1))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X6),X3),X11),X9))
| ~ mem(X9,arr(X6,X1))
| ~ mem(X11,arr(X1,X6))
| ~ mem(X3,arr(X1,arr(X1,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X7),X2),X8),X10))
| ~ mem(X10,arr(X7,X0))
| ~ mem(X8,arr(X0,X7))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X6)
| ~ ne(X7)
| ~ ne(X1)
| ~ ne(X0) ),
inference(resolution,[],[f11197,f11166]) ).
fof(f14531,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X5))
| ~ mem(X5,arr(X0,X1))
| ~ mem(X4,arr(X0,X1))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X4))
| ~ mem(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,X6,X7,X1),X8),X9),arr(arr(X7,X6),arr(X0,X1)))
| ~ mem(ap(ap(c_2Equotient_2E_2D_2D_3E(X7,X1,X0,X6),X10),X11),arr(arr(X0,X1),arr(X7,X6)))
| ~ mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),arr(arr(X0,X1),arr(arr(X0,X1),bool)))
| ~ ne(arr(X7,X6))
| ~ ne(arr(X0,X1))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X6),X3),X11),X9))
| ~ mem(X9,arr(X6,X1))
| ~ mem(X11,arr(X1,X6))
| ~ mem(X3,arr(X1,arr(X1,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X7),X2),X8),X10))
| ~ mem(X10,arr(X7,X0))
| ~ mem(X8,arr(X0,X7))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X6)
| ~ ne(X7)
| ~ ne(X1)
| ~ ne(X0) ),
inference(resolution,[],[f11198,f11166]) ).
fof(f14534,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X5))
| ~ mem(X5,arr(X0,X1))
| ~ mem(X4,arr(X0,X1))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X5),X4))
| ~ mem(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,X6,X7,X1),X8),X9),arr(arr(X7,X6),arr(X0,X1)))
| ~ mem(ap(ap(c_2Equotient_2E_2D_2D_3E(X7,X1,X0,X6),X10),X11),arr(arr(X0,X1),arr(X7,X6)))
| ~ mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),arr(arr(X0,X1),arr(arr(X0,X1),bool)))
| ~ ne(arr(X7,X6))
| ~ ne(arr(X0,X1))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X6),X3),X11),X9))
| ~ mem(X9,arr(X6,X1))
| ~ mem(X11,arr(X1,X6))
| ~ mem(X3,arr(X1,arr(X1,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X7),X2),X8),X10))
| ~ mem(X10,arr(X7,X0))
| ~ mem(X8,arr(X0,X7))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X6)
| ~ ne(X7)
| ~ ne(X1)
| ~ ne(X0) ),
inference(resolution,[],[f11188,f11166]) ).
fof(f14567,plain,
! [X2,X0,X1] :
( mem(ap(c_2Equotient_2E_3D_3D_3D_3E(X1,X0),X2),arr(arr(X0,arr(X0,bool)),arr(arr(X1,X0),arr(arr(X1,X0),bool))))
| ~ ne(X1)
| ~ mem(X2,arr(X1,arr(X1,bool)))
| ~ ne(X0) ),
inference(resolution,[],[f11186,f11165]) ).
fof(f14590,plain,
! [X2,X3,X0,X1,X4] :
( mem(ap(c_2Equotient_2E_2D_2D_3E(X3,X2,X1,X0),X4),arr(arr(X2,X0),arr(arr(X1,X2),arr(X3,X0))))
| ~ ne(X1)
| ~ ne(X2)
| ~ ne(X3)
| ~ mem(X4,arr(X3,X1))
| ~ ne(X0) ),
inference(resolution,[],[f11171,f11165]) ).
fof(f15155,definition,
( spl700_86
<=> ne(arr(sK150,sK151)) ),
introduced(definition,[new_symbols(definition,[spl700_86])],[avatar_definition]) ).
fof(f15156,plain,
( ne(arr(sK150,sK151))
| ~ spl700_86 ),
inference(avatar_component_clause,[],[f15155]) ).
fof(f15157,plain,
( ~ ne(arr(sK150,sK151))
| spl700_86 ),
inference(avatar_component_clause,[],[f15155]) ).
fof(f15421,plain,
! [X2,X3,X0,X1,X4,X5] :
( mem(ap(ap(c_2Equotient_2E_2D_2D_3E(X2,X1,X0,X4),X3),X5),arr(arr(X0,X1),arr(X2,X4)))
| ~ ne(X1)
| ~ ne(X2)
| ~ mem(X3,arr(X2,X0))
| ~ ne(X4)
| ~ mem(X5,arr(X1,X4))
| ~ ne(X0) ),
inference(resolution,[],[f14590,f11165]) ).
fof(f15582,plain,
! [X2,X3,X0,X1] :
( mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X2),X1),X3),arr(arr(X0,X2),arr(arr(X0,X2),bool)))
| ~ mem(X1,arr(X0,arr(X0,bool)))
| ~ ne(X2)
| ~ mem(X3,arr(X2,arr(X2,bool)))
| ~ ne(X0) ),
inference(resolution,[],[f14567,f11165]) ).
fof(f16466,plain,
( ~ ne(sK151)
| ~ ne(sK150)
| spl700_86 ),
inference(resolution,[],[f15157,f11164]) ).
fof(f16467,plain,
( ~ ne(sK150)
| spl700_86 ),
inference(forward_subsumption_resolution,[],[f16466,f10250]) ).
fof(f16468,plain,
( $false
| spl700_86 ),
inference(forward_subsumption_resolution,[],[f16467,f10249]) ).
fof(f16469,plain,
spl700_86,
inference(avatar_contradiction_clause,[],[f16468]) ).
fof(f17350,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X5))
| ~ mem(X5,arr(X0,X1))
| ~ mem(X4,arr(X0,X1))
| ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X6,X1,X0,X7),X8),X9),X4) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X6,X1,X0,X7),X8),X9),X5)
| ~ mem(ap(ap(c_2Equotient_2E_2D_2D_3E(X6,X1,X0,X7),X8),X9),arr(arr(X0,X1),arr(X6,X7)))
| ~ mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),arr(arr(X0,X1),arr(arr(X0,X1),bool)))
| ~ ne(arr(X6,X7))
| ~ ne(arr(X0,X1))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X7),X3),X9),X11))
| ~ mem(X11,arr(X7,X1))
| ~ mem(X9,arr(X1,X7))
| ~ mem(X3,arr(X1,arr(X1,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X6),X2),X10),X8))
| ~ mem(X8,arr(X6,X0))
| ~ mem(X10,arr(X0,X6))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X7)
| ~ ne(X6)
| ~ ne(X1)
| ~ ne(X0) ),
inference(forward_subsumption_resolution,[],[f14521,f15421]) ).
fof(f17356,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X5))
| ~ mem(X5,arr(X0,X1))
| ~ mem(X4,arr(X0,X1))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X5),X5))
| ~ mem(ap(ap(c_2Equotient_2E_2D_2D_3E(X7,X1,X0,X6),X10),X11),arr(arr(X0,X1),arr(X7,X6)))
| ~ mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),arr(arr(X0,X1),arr(arr(X0,X1),bool)))
| ~ ne(arr(X7,X6))
| ~ ne(arr(X0,X1))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X6),X3),X11),X9))
| ~ mem(X9,arr(X6,X1))
| ~ mem(X11,arr(X1,X6))
| ~ mem(X3,arr(X1,arr(X1,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X7),X2),X8),X10))
| ~ mem(X10,arr(X7,X0))
| ~ mem(X8,arr(X0,X7))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X6)
| ~ ne(X7)
| ~ ne(X1)
| ~ ne(X0) ),
inference(forward_subsumption_resolution,[],[f14528,f15421]) ).
fof(f17359,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X5))
| ~ mem(X5,arr(X0,X1))
| ~ mem(X4,arr(X0,X1))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X4))
| ~ mem(ap(ap(c_2Equotient_2E_2D_2D_3E(X7,X1,X0,X6),X10),X11),arr(arr(X0,X1),arr(X7,X6)))
| ~ mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),arr(arr(X0,X1),arr(arr(X0,X1),bool)))
| ~ ne(arr(X7,X6))
| ~ ne(arr(X0,X1))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X6),X3),X11),X9))
| ~ mem(X9,arr(X6,X1))
| ~ mem(X11,arr(X1,X6))
| ~ mem(X3,arr(X1,arr(X1,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X7),X2),X8),X10))
| ~ mem(X10,arr(X7,X0))
| ~ mem(X8,arr(X0,X7))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X6)
| ~ ne(X7)
| ~ ne(X1)
| ~ ne(X0) ),
inference(forward_subsumption_resolution,[],[f14531,f15421]) ).
fof(f17362,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X5))
| ~ mem(X5,arr(X0,X1))
| ~ mem(X4,arr(X0,X1))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X5),X4))
| ~ mem(ap(ap(c_2Equotient_2E_2D_2D_3E(X7,X1,X0,X6),X10),X11),arr(arr(X0,X1),arr(X7,X6)))
| ~ mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),arr(arr(X0,X1),arr(arr(X0,X1),bool)))
| ~ ne(arr(X7,X6))
| ~ ne(arr(X0,X1))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X6),X3),X11),X9))
| ~ mem(X9,arr(X6,X1))
| ~ mem(X11,arr(X1,X6))
| ~ mem(X3,arr(X1,arr(X1,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X7),X2),X8),X10))
| ~ mem(X10,arr(X7,X0))
| ~ mem(X8,arr(X0,X7))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X6)
| ~ ne(X7)
| ~ ne(X1)
| ~ ne(X0) ),
inference(forward_subsumption_resolution,[],[f14534,f15421]) ).
fof(f17500,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X5))
| ~ mem(X5,arr(X0,X1))
| ~ mem(X4,arr(X0,X1))
| ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X6,X1,X0,X7),X8),X9),X4) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X6,X1,X0,X7),X8),X9),X5)
| ~ mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),arr(arr(X0,X1),arr(arr(X0,X1),bool)))
| ~ ne(arr(X6,X7))
| ~ ne(arr(X0,X1))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X7),X3),X9),X11))
| ~ mem(X11,arr(X7,X1))
| ~ mem(X9,arr(X1,X7))
| ~ mem(X3,arr(X1,arr(X1,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X6),X2),X10),X8))
| ~ mem(X8,arr(X6,X0))
| ~ mem(X10,arr(X0,X6))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X7)
| ~ ne(X6)
| ~ ne(X1)
| ~ ne(X0) ),
inference(forward_subsumption_resolution,[],[f17350,f15421]) ).
fof(f17506,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X5))
| ~ mem(X5,arr(X0,X1))
| ~ mem(X4,arr(X0,X1))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X5),X5))
| ~ mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),arr(arr(X0,X1),arr(arr(X0,X1),bool)))
| ~ ne(arr(X7,X6))
| ~ ne(arr(X0,X1))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X6),X3),X11),X9))
| ~ mem(X9,arr(X6,X1))
| ~ mem(X11,arr(X1,X6))
| ~ mem(X3,arr(X1,arr(X1,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X7),X2),X8),X10))
| ~ mem(X10,arr(X7,X0))
| ~ mem(X8,arr(X0,X7))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X6)
| ~ ne(X7)
| ~ ne(X1)
| ~ ne(X0) ),
inference(forward_subsumption_resolution,[],[f17356,f15421]) ).
fof(f17509,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X5))
| ~ mem(X5,arr(X0,X1))
| ~ mem(X4,arr(X0,X1))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X4))
| ~ mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),arr(arr(X0,X1),arr(arr(X0,X1),bool)))
| ~ ne(arr(X7,X6))
| ~ ne(arr(X0,X1))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X6),X3),X11),X9))
| ~ mem(X9,arr(X6,X1))
| ~ mem(X11,arr(X1,X6))
| ~ mem(X3,arr(X1,arr(X1,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X7),X2),X8),X10))
| ~ mem(X10,arr(X7,X0))
| ~ mem(X8,arr(X0,X7))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X6)
| ~ ne(X7)
| ~ ne(X1)
| ~ ne(X0) ),
inference(forward_subsumption_resolution,[],[f17359,f15421]) ).
fof(f17512,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X5))
| ~ mem(X5,arr(X0,X1))
| ~ mem(X4,arr(X0,X1))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X5),X4))
| ~ mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),arr(arr(X0,X1),arr(arr(X0,X1),bool)))
| ~ ne(arr(X7,X6))
| ~ ne(arr(X0,X1))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X6),X3),X11),X9))
| ~ mem(X9,arr(X6,X1))
| ~ mem(X11,arr(X1,X6))
| ~ mem(X3,arr(X1,arr(X1,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X7),X2),X8),X10))
| ~ mem(X10,arr(X7,X0))
| ~ mem(X8,arr(X0,X7))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X6)
| ~ ne(X7)
| ~ ne(X1)
| ~ ne(X0) ),
inference(forward_subsumption_resolution,[],[f17362,f15421]) ).
fof(f17623,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X5))
| ~ mem(X5,arr(X0,X1))
| ~ mem(X4,arr(X0,X1))
| ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X6,X1,X0,X7),X8),X9),X4) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X6,X1,X0,X7),X8),X9),X5)
| ~ ne(arr(X6,X7))
| ~ ne(arr(X0,X1))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X7),X3),X9),X11))
| ~ mem(X11,arr(X7,X1))
| ~ mem(X9,arr(X1,X7))
| ~ mem(X3,arr(X1,arr(X1,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X6),X2),X10),X8))
| ~ mem(X8,arr(X6,X0))
| ~ mem(X10,arr(X0,X6))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X7)
| ~ ne(X6)
| ~ ne(X1)
| ~ ne(X0) ),
inference(forward_subsumption_resolution,[],[f17500,f15582]) ).
fof(f17629,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X5))
| ~ mem(X5,arr(X0,X1))
| ~ mem(X4,arr(X0,X1))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X5),X5))
| ~ ne(arr(X7,X6))
| ~ ne(arr(X0,X1))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X6),X3),X11),X9))
| ~ mem(X9,arr(X6,X1))
| ~ mem(X11,arr(X1,X6))
| ~ mem(X3,arr(X1,arr(X1,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X7),X2),X8),X10))
| ~ mem(X10,arr(X7,X0))
| ~ mem(X8,arr(X0,X7))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X6)
| ~ ne(X7)
| ~ ne(X1)
| ~ ne(X0) ),
inference(forward_subsumption_resolution,[],[f17506,f15582]) ).
fof(f17632,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X5))
| ~ mem(X5,arr(X0,X1))
| ~ mem(X4,arr(X0,X1))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X4))
| ~ ne(arr(X7,X6))
| ~ ne(arr(X0,X1))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X6),X3),X11),X9))
| ~ mem(X9,arr(X6,X1))
| ~ mem(X11,arr(X1,X6))
| ~ mem(X3,arr(X1,arr(X1,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X7),X2),X8),X10))
| ~ mem(X10,arr(X7,X0))
| ~ mem(X8,arr(X0,X7))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X6)
| ~ ne(X7)
| ~ ne(X1)
| ~ ne(X0) ),
inference(forward_subsumption_resolution,[],[f17509,f15582]) ).
fof(f17635,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X5))
| ~ mem(X5,arr(X0,X1))
| ~ mem(X4,arr(X0,X1))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X5),X4))
| ~ ne(arr(X7,X6))
| ~ ne(arr(X0,X1))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X6),X3),X11),X9))
| ~ mem(X9,arr(X6,X1))
| ~ mem(X11,arr(X1,X6))
| ~ mem(X3,arr(X1,arr(X1,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X7),X2),X8),X10))
| ~ mem(X10,arr(X7,X0))
| ~ mem(X8,arr(X0,X7))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X6)
| ~ ne(X7)
| ~ ne(X1)
| ~ ne(X0) ),
inference(forward_subsumption_resolution,[],[f17512,f15582]) ).
fof(f17652,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X5))
| ~ mem(X5,arr(X0,X1))
| ~ mem(X4,arr(X0,X1))
| ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X6,X1,X0,X7),X8),X9),X4) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X6,X1,X0,X7),X8),X9),X5)
| ~ ne(arr(X0,X1))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X7),X3),X9),X11))
| ~ mem(X11,arr(X7,X1))
| ~ mem(X9,arr(X1,X7))
| ~ mem(X3,arr(X1,arr(X1,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X6),X2),X10),X8))
| ~ mem(X8,arr(X6,X0))
| ~ mem(X10,arr(X0,X6))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X7)
| ~ ne(X6)
| ~ ne(X1)
| ~ ne(X0) ),
inference(forward_subsumption_resolution,[],[f17623,f11164]) ).
fof(f17658,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X5))
| ~ mem(X5,arr(X0,X1))
| ~ mem(X4,arr(X0,X1))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X5),X5))
| ~ ne(arr(X0,X1))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X6),X3),X11),X9))
| ~ mem(X9,arr(X6,X1))
| ~ mem(X11,arr(X1,X6))
| ~ mem(X3,arr(X1,arr(X1,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X7),X2),X8),X10))
| ~ mem(X10,arr(X7,X0))
| ~ mem(X8,arr(X0,X7))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X6)
| ~ ne(X7)
| ~ ne(X1)
| ~ ne(X0) ),
inference(forward_subsumption_resolution,[],[f17629,f11164]) ).
fof(f17661,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X5))
| ~ mem(X5,arr(X0,X1))
| ~ mem(X4,arr(X0,X1))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X4))
| ~ ne(arr(X0,X1))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X6),X3),X11),X9))
| ~ mem(X9,arr(X6,X1))
| ~ mem(X11,arr(X1,X6))
| ~ mem(X3,arr(X1,arr(X1,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X7),X2),X8),X10))
| ~ mem(X10,arr(X7,X0))
| ~ mem(X8,arr(X0,X7))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X6)
| ~ ne(X7)
| ~ ne(X1)
| ~ ne(X0) ),
inference(forward_subsumption_resolution,[],[f17632,f11164]) ).
fof(f17664,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X5))
| ~ mem(X5,arr(X0,X1))
| ~ mem(X4,arr(X0,X1))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X5),X4))
| ~ ne(arr(X0,X1))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X6),X3),X11),X9))
| ~ mem(X9,arr(X6,X1))
| ~ mem(X11,arr(X1,X6))
| ~ mem(X3,arr(X1,arr(X1,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X7),X2),X8),X10))
| ~ mem(X10,arr(X7,X0))
| ~ mem(X8,arr(X0,X7))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X6)
| ~ ne(X7)
| ~ ne(X1)
| ~ ne(X0) ),
inference(forward_subsumption_resolution,[],[f17635,f11164]) ).
fof(f17680,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X5))
| ~ mem(X5,arr(X0,X1))
| ~ mem(X4,arr(X0,X1))
| ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X6,X1,X0,X7),X8),X9),X4) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X6,X1,X0,X7),X8),X9),X5)
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X7),X3),X9),X11))
| ~ mem(X11,arr(X7,X1))
| ~ mem(X9,arr(X1,X7))
| ~ mem(X3,arr(X1,arr(X1,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X6),X2),X10),X8))
| ~ mem(X8,arr(X6,X0))
| ~ mem(X10,arr(X0,X6))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X7)
| ~ ne(X6)
| ~ ne(X1)
| ~ ne(X0) ),
inference(forward_subsumption_resolution,[],[f17652,f11164]) ).
fof(f17686,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X5))
| ~ mem(X5,arr(X0,X1))
| ~ mem(X4,arr(X0,X1))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X5),X5))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X6),X3),X11),X9))
| ~ mem(X9,arr(X6,X1))
| ~ mem(X11,arr(X1,X6))
| ~ mem(X3,arr(X1,arr(X1,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X7),X2),X8),X10))
| ~ mem(X10,arr(X7,X0))
| ~ mem(X8,arr(X0,X7))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X6)
| ~ ne(X7)
| ~ ne(X1)
| ~ ne(X0) ),
inference(forward_subsumption_resolution,[],[f17658,f11164]) ).
fof(f17689,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X5))
| ~ mem(X5,arr(X0,X1))
| ~ mem(X4,arr(X0,X1))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X4))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X6),X3),X11),X9))
| ~ mem(X9,arr(X6,X1))
| ~ mem(X11,arr(X1,X6))
| ~ mem(X3,arr(X1,arr(X1,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X7),X2),X8),X10))
| ~ mem(X10,arr(X7,X0))
| ~ mem(X8,arr(X0,X7))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X6)
| ~ ne(X7)
| ~ ne(X1)
| ~ ne(X0) ),
inference(forward_subsumption_resolution,[],[f17661,f11164]) ).
fof(f17692,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X4),X5))
| ~ mem(X5,arr(X0,X1))
| ~ mem(X4,arr(X0,X1))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(X0,X1),X2),X3),X5),X4))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X6),X3),X11),X9))
| ~ mem(X9,arr(X6,X1))
| ~ mem(X11,arr(X1,X6))
| ~ mem(X3,arr(X1,arr(X1,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X0,X7),X2),X8),X10))
| ~ mem(X10,arr(X7,X0))
| ~ mem(X8,arr(X0,X7))
| ~ mem(X2,arr(X0,arr(X0,bool)))
| ~ ne(X6)
| ~ ne(X7)
| ~ ne(X1)
| ~ ne(X0) ),
inference(forward_subsumption_resolution,[],[f17664,f11164]) ).
fof(f17715,definition,
( spl700_111
<=> ! [X6,X4,X5] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X4),sK154),X5),X6))
| ~ ne(X4)
| ~ mem(X5,arr(sK150,X4))
| ~ mem(X6,arr(X4,sK150)) ) ),
introduced(definition,[new_symbols(definition,[spl700_111])],[avatar_definition]) ).
fof(f17716,plain,
( ! [X6,X4,X5] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X4),sK154),X5),X6))
| ~ ne(X4)
| ~ mem(X5,arr(sK150,X4))
| ~ mem(X6,arr(X4,sK150)) )
| ~ spl700_111 ),
inference(avatar_component_clause,[],[f17715]) ).
fof(f17718,definition,
( spl700_112
<=> ! [X2,X1,X3] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X1),sK157),X2),X3))
| ~ ne(X1)
| ~ mem(X2,arr(sK151,X1))
| ~ mem(X3,arr(X1,sK151)) ) ),
introduced(definition,[new_symbols(definition,[spl700_112])],[avatar_definition]) ).
fof(f17719,plain,
( ! [X2,X3,X1] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X1),sK157),X2),X3))
| ~ ne(X1)
| ~ mem(X2,arr(sK151,X1))
| ~ mem(X3,arr(X1,sK151)) )
| ~ spl700_112 ),
inference(avatar_component_clause,[],[f17718]) ).
fof(f19012,plain,
( ~ ne(sK153)
| ~ mem(sK158,arr(sK151,sK153))
| ~ mem(sK159,arr(sK153,sK151))
| ~ spl700_112 ),
inference(resolution,[],[f17719,f10260]) ).
fof(f19016,plain,
( ~ mem(sK158,arr(sK151,sK153))
| ~ mem(sK159,arr(sK153,sK151))
| ~ spl700_112 ),
inference(forward_subsumption_resolution,[],[f19012,f10252]) ).
fof(f19017,plain,
( ~ mem(sK159,arr(sK153,sK151))
| ~ spl700_112 ),
inference(forward_subsumption_resolution,[],[f19016,f10258]) ).
fof(f19018,plain,
( $false
| ~ spl700_112 ),
inference(forward_subsumption_resolution,[],[f19017,f10259]) ).
fof(f19019,plain,
~ spl700_112,
inference(avatar_contradiction_clause,[],[f19018]) ).
fof(f19054,plain,
( p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK160),sK160))
| ~ mem(sK160,arr(sK150,sK151))
| ~ mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),arr(arr(sK150,sK151),arr(arr(sK150,sK151),bool)))
| ~ ne(arr(sK150,sK151))
| ~ spl700_72 ),
inference(resolution,[],[f14497,f11222]) ).
fof(f19060,plain,
( p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK160),sK160))
| ~ mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),arr(arr(sK150,sK151),arr(arr(sK150,sK151),bool)))
| ~ ne(arr(sK150,sK151))
| ~ spl700_72 ),
inference(forward_subsumption_resolution,[],[f19054,f10261]) ).
fof(f19063,plain,
( p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK160),sK160))
| ~ mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),arr(arr(sK150,sK151),arr(arr(sK150,sK151),bool)))
| ~ spl700_72
| ~ spl700_86 ),
inference(forward_subsumption_resolution,[],[f19060,f15156]) ).
fof(f19067,definition,
( spl700_133
<=> mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),arr(arr(sK150,sK151),arr(arr(sK150,sK151),bool))) ),
introduced(definition,[new_symbols(definition,[spl700_133])],[avatar_definition]) ).
fof(f19068,plain,
( mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),arr(arr(sK150,sK151),arr(arr(sK150,sK151),bool)))
| ~ spl700_133 ),
inference(avatar_component_clause,[],[f19067]) ).
fof(f19069,plain,
( ~ mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),arr(arr(sK150,sK151),arr(arr(sK150,sK151),bool)))
| spl700_133 ),
inference(avatar_component_clause,[],[f19067]) ).
fof(f19071,definition,
( spl700_134
<=> p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK160),sK160)) ),
introduced(definition,[new_symbols(definition,[spl700_134])],[avatar_definition]) ).
fof(f19072,plain,
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK160),sK160))
| spl700_134 ),
inference(avatar_component_clause,[],[f19071]) ).
fof(f19073,plain,
( p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK160),sK160))
| ~ spl700_134 ),
inference(avatar_component_clause,[],[f19071]) ).
fof(f19074,plain,
( ~ spl700_133
| spl700_134
| ~ spl700_72
| ~ spl700_86 ),
inference(avatar_split_clause,[],[f19063,f15155,f14495,f19071,f19067]) ).
fof(f19079,plain,
( ~ mem(sK154,arr(sK150,arr(sK150,bool)))
| ~ ne(sK151)
| ~ mem(sK157,arr(sK151,arr(sK151,bool)))
| ~ ne(sK150)
| spl700_133 ),
inference(resolution,[],[f19069,f15582]) ).
fof(f19080,plain,
( ~ ne(sK151)
| ~ mem(sK157,arr(sK151,arr(sK151,bool)))
| ~ ne(sK150)
| spl700_133 ),
inference(forward_subsumption_resolution,[],[f19079,f10253]) ).
fof(f19081,plain,
( ~ mem(sK157,arr(sK151,arr(sK151,bool)))
| ~ ne(sK150)
| spl700_133 ),
inference(forward_subsumption_resolution,[],[f19080,f10250]) ).
fof(f19082,plain,
( ~ ne(sK150)
| spl700_133 ),
inference(forward_subsumption_resolution,[],[f19081,f10257]) ).
fof(f19083,plain,
( $false
| spl700_133 ),
inference(forward_subsumption_resolution,[],[f19082,f10249]) ).
fof(f19084,plain,
spl700_133,
inference(avatar_contradiction_clause,[],[f19083]) ).
fof(f19085,plain,
( ~ ne(sK152)
| ~ mem(sK155,arr(sK150,sK152))
| ~ mem(sK156,arr(sK152,sK150))
| ~ spl700_111 ),
inference(resolution,[],[f17716,f10256]) ).
fof(f19089,plain,
( ~ mem(sK155,arr(sK150,sK152))
| ~ mem(sK156,arr(sK152,sK150))
| ~ spl700_111 ),
inference(forward_subsumption_resolution,[],[f19085,f10251]) ).
fof(f19090,plain,
( ~ mem(sK156,arr(sK152,sK150))
| ~ spl700_111 ),
inference(forward_subsumption_resolution,[],[f19089,f10254]) ).
fof(f19091,plain,
( $false
| ~ spl700_111 ),
inference(forward_subsumption_resolution,[],[f19090,f10255]) ).
fof(f19092,plain,
~ spl700_111,
inference(avatar_contradiction_clause,[],[f19091]) ).
fof(f19108,plain,
( ! [X0] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),X0),X0))
| ~ mem(X0,arr(sK150,sK151))
| p(ap(ap(c_2Equotient_2Erespects(arr(sK150,sK151),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157)),X0))
| ~ ne(arr(sK150,sK151)) )
| ~ spl700_133 ),
inference(resolution,[],[f19068,f11223]) ).
fof(f19148,plain,
( ! [X0] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),X0),X0))
| ~ mem(X0,arr(sK150,sK151))
| p(ap(ap(c_2Equotient_2Erespects(arr(sK150,sK151),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157)),X0)) )
| ~ spl700_86
| ~ spl700_133 ),
inference(forward_subsumption_resolution,[],[f19108,f15156]) ).
fof(f19226,definition,
( spl700_151
<=> p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK161),sK161)) ),
introduced(definition,[new_symbols(definition,[spl700_151])],[avatar_definition]) ).
fof(f19227,plain,
( p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK161),sK161))
| ~ spl700_151 ),
inference(avatar_component_clause,[],[f19226]) ).
fof(f19228,plain,
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK161),sK161))
| spl700_151 ),
inference(avatar_component_clause,[],[f19226]) ).
fof(f19325,plain,
( p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK161),sK161))
| ~ mem(sK161,arr(sK150,sK151))
| ~ mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),arr(arr(sK150,sK151),arr(arr(sK150,sK151),bool)))
| ~ ne(arr(sK150,sK151))
| ~ spl700_71 ),
inference(resolution,[],[f14492,f11222]) ).
fof(f19332,plain,
( ~ mem(sK161,arr(sK150,sK151))
| ~ mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),arr(arr(sK150,sK151),arr(arr(sK150,sK151),bool)))
| ~ ne(arr(sK150,sK151))
| ~ spl700_71
| spl700_151 ),
inference(forward_subsumption_resolution,[],[f19325,f19228]) ).
fof(f19336,plain,
( ~ mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),arr(arr(sK150,sK151),arr(arr(sK150,sK151),bool)))
| ~ ne(arr(sK150,sK151))
| ~ spl700_71
| spl700_151 ),
inference(forward_subsumption_resolution,[],[f19332,f10262]) ).
fof(f19340,plain,
( ~ ne(arr(sK150,sK151))
| ~ spl700_71
| ~ spl700_133
| spl700_151 ),
inference(forward_subsumption_resolution,[],[f19336,f19068]) ).
fof(f19344,plain,
( $false
| ~ spl700_71
| ~ spl700_86
| ~ spl700_133
| spl700_151 ),
inference(forward_subsumption_resolution,[],[f19340,f15156]) ).
fof(f19345,plain,
( ~ spl700_71
| ~ spl700_86
| ~ spl700_133
| spl700_151 ),
inference(avatar_contradiction_clause,[],[f19344]) ).
fof(f20524,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ mem(sK161,arr(sK150,sK151))
| ~ mem(sK160,arr(sK150,sK151))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK161),sK161))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X0),sK157),X1),X2))
| ~ mem(X2,arr(X0,sK151))
| ~ mem(X1,arr(sK151,X0))
| ~ mem(sK157,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X3),sK154),X4),X5))
| ~ mem(X5,arr(X3,sK150))
| ~ mem(X4,arr(sK150,X3))
| ~ mem(sK154,arr(sK150,arr(sK150,bool)))
| ~ ne(X0)
| ~ ne(X3)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_69 ),
inference(resolution,[],[f14483,f17686]) ).
fof(f20525,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ mem(sK161,arr(sK150,sK151))
| ~ mem(sK160,arr(sK150,sK151))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK160),sK160))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X0),sK157),X1),X2))
| ~ mem(X2,arr(X0,sK151))
| ~ mem(X1,arr(sK151,X0))
| ~ mem(sK157,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X3),sK154),X4),X5))
| ~ mem(X5,arr(X3,sK150))
| ~ mem(X4,arr(sK150,X3))
| ~ mem(sK154,arr(sK150,arr(sK150,bool)))
| ~ ne(X0)
| ~ ne(X3)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_69 ),
inference(resolution,[],[f14483,f17689]) ).
fof(f20526,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ mem(sK161,arr(sK150,sK151))
| ~ mem(sK160,arr(sK150,sK151))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK161),sK160))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X0),sK157),X1),X2))
| ~ mem(X2,arr(X0,sK151))
| ~ mem(X1,arr(sK151,X0))
| ~ mem(sK157,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X3),sK154),X4),X5))
| ~ mem(X5,arr(X3,sK150))
| ~ mem(X4,arr(sK150,X3))
| ~ mem(sK154,arr(sK150,arr(sK150,bool)))
| ~ ne(X0)
| ~ ne(X3)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_69 ),
inference(resolution,[],[f14483,f17692]) ).
fof(f20529,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ mem(sK160,arr(sK150,sK151))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK161),sK160))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X0),sK157),X1),X2))
| ~ mem(X2,arr(X0,sK151))
| ~ mem(X1,arr(sK151,X0))
| ~ mem(sK157,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X3),sK154),X4),X5))
| ~ mem(X5,arr(X3,sK150))
| ~ mem(X4,arr(sK150,X3))
| ~ mem(sK154,arr(sK150,arr(sK150,bool)))
| ~ ne(X0)
| ~ ne(X3)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_69 ),
inference(forward_subsumption_resolution,[],[f20526,f10262]) ).
fof(f20530,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ mem(sK160,arr(sK150,sK151))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK160),sK160))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X0),sK157),X1),X2))
| ~ mem(X2,arr(X0,sK151))
| ~ mem(X1,arr(sK151,X0))
| ~ mem(sK157,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X3),sK154),X4),X5))
| ~ mem(X5,arr(X3,sK150))
| ~ mem(X4,arr(sK150,X3))
| ~ mem(sK154,arr(sK150,arr(sK150,bool)))
| ~ ne(X0)
| ~ ne(X3)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_69 ),
inference(forward_subsumption_resolution,[],[f20525,f10262]) ).
fof(f20531,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ mem(sK160,arr(sK150,sK151))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK161),sK161))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X0),sK157),X1),X2))
| ~ mem(X2,arr(X0,sK151))
| ~ mem(X1,arr(sK151,X0))
| ~ mem(sK157,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X3),sK154),X4),X5))
| ~ mem(X5,arr(X3,sK150))
| ~ mem(X4,arr(sK150,X3))
| ~ mem(sK154,arr(sK150,arr(sK150,bool)))
| ~ ne(X0)
| ~ ne(X3)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_69 ),
inference(forward_subsumption_resolution,[],[f20524,f10262]) ).
fof(f20533,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK161),sK160))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X0),sK157),X1),X2))
| ~ mem(X2,arr(X0,sK151))
| ~ mem(X1,arr(sK151,X0))
| ~ mem(sK157,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X3),sK154),X4),X5))
| ~ mem(X5,arr(X3,sK150))
| ~ mem(X4,arr(sK150,X3))
| ~ mem(sK154,arr(sK150,arr(sK150,bool)))
| ~ ne(X0)
| ~ ne(X3)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_69 ),
inference(forward_subsumption_resolution,[],[f20529,f10261]) ).
fof(f20534,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK160),sK160))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X0),sK157),X1),X2))
| ~ mem(X2,arr(X0,sK151))
| ~ mem(X1,arr(sK151,X0))
| ~ mem(sK157,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X3),sK154),X4),X5))
| ~ mem(X5,arr(X3,sK150))
| ~ mem(X4,arr(sK150,X3))
| ~ mem(sK154,arr(sK150,arr(sK150,bool)))
| ~ ne(X0)
| ~ ne(X3)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_69 ),
inference(forward_subsumption_resolution,[],[f20530,f10261]) ).
fof(f20535,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK161),sK161))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X0),sK157),X1),X2))
| ~ mem(X2,arr(X0,sK151))
| ~ mem(X1,arr(sK151,X0))
| ~ mem(sK157,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X3),sK154),X4),X5))
| ~ mem(X5,arr(X3,sK150))
| ~ mem(X4,arr(sK150,X3))
| ~ mem(sK154,arr(sK150,arr(sK150,bool)))
| ~ ne(X0)
| ~ ne(X3)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_69 ),
inference(forward_subsumption_resolution,[],[f20531,f10261]) ).
fof(f20537,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK161),sK160))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X0),sK157),X1),X2))
| ~ mem(X2,arr(X0,sK151))
| ~ mem(X1,arr(sK151,X0))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X3),sK154),X4),X5))
| ~ mem(X5,arr(X3,sK150))
| ~ mem(X4,arr(sK150,X3))
| ~ mem(sK154,arr(sK150,arr(sK150,bool)))
| ~ ne(X0)
| ~ ne(X3)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_69 ),
inference(forward_subsumption_resolution,[],[f20533,f10257]) ).
fof(f20538,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X0),sK157),X1),X2))
| ~ mem(X2,arr(X0,sK151))
| ~ mem(X1,arr(sK151,X0))
| ~ mem(sK157,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X3),sK154),X4),X5))
| ~ mem(X5,arr(X3,sK150))
| ~ mem(X4,arr(sK150,X3))
| ~ mem(sK154,arr(sK150,arr(sK150,bool)))
| ~ ne(X0)
| ~ ne(X3)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_69
| spl700_134 ),
inference(forward_subsumption_resolution,[],[f20534,f19072]) ).
fof(f20539,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X0),sK157),X1),X2))
| ~ mem(X2,arr(X0,sK151))
| ~ mem(X1,arr(sK151,X0))
| ~ mem(sK157,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X3),sK154),X4),X5))
| ~ mem(X5,arr(X3,sK150))
| ~ mem(X4,arr(sK150,X3))
| ~ mem(sK154,arr(sK150,arr(sK150,bool)))
| ~ ne(X0)
| ~ ne(X3)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_69
| spl700_151 ),
inference(forward_subsumption_resolution,[],[f20535,f19228]) ).
fof(f20541,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK161),sK160))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X0),sK157),X1),X2))
| ~ mem(X2,arr(X0,sK151))
| ~ mem(X1,arr(sK151,X0))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X3),sK154),X4),X5))
| ~ mem(X5,arr(X3,sK150))
| ~ mem(X4,arr(sK150,X3))
| ~ ne(X0)
| ~ ne(X3)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_69 ),
inference(forward_subsumption_resolution,[],[f20537,f10253]) ).
fof(f20542,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X0),sK157),X1),X2))
| ~ mem(X2,arr(X0,sK151))
| ~ mem(X1,arr(sK151,X0))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X3),sK154),X4),X5))
| ~ mem(X5,arr(X3,sK150))
| ~ mem(X4,arr(sK150,X3))
| ~ mem(sK154,arr(sK150,arr(sK150,bool)))
| ~ ne(X0)
| ~ ne(X3)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_69
| spl700_134 ),
inference(forward_subsumption_resolution,[],[f20538,f10257]) ).
fof(f20543,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X0),sK157),X1),X2))
| ~ mem(X2,arr(X0,sK151))
| ~ mem(X1,arr(sK151,X0))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X3),sK154),X4),X5))
| ~ mem(X5,arr(X3,sK150))
| ~ mem(X4,arr(sK150,X3))
| ~ mem(sK154,arr(sK150,arr(sK150,bool)))
| ~ ne(X0)
| ~ ne(X3)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_69
| spl700_151 ),
inference(forward_subsumption_resolution,[],[f20539,f10257]) ).
fof(f20545,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK161),sK160))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X0),sK157),X1),X2))
| ~ mem(X2,arr(X0,sK151))
| ~ mem(X1,arr(sK151,X0))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X3),sK154),X4),X5))
| ~ mem(X5,arr(X3,sK150))
| ~ mem(X4,arr(sK150,X3))
| ~ ne(X0)
| ~ ne(X3)
| ~ ne(sK150) )
| ~ spl700_69 ),
inference(forward_subsumption_resolution,[],[f20541,f10250]) ).
fof(f20546,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X0),sK157),X1),X2))
| ~ mem(X2,arr(X0,sK151))
| ~ mem(X1,arr(sK151,X0))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X3),sK154),X4),X5))
| ~ mem(X5,arr(X3,sK150))
| ~ mem(X4,arr(sK150,X3))
| ~ ne(X0)
| ~ ne(X3)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_69
| spl700_134 ),
inference(forward_subsumption_resolution,[],[f20542,f10253]) ).
fof(f20547,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X0),sK157),X1),X2))
| ~ mem(X2,arr(X0,sK151))
| ~ mem(X1,arr(sK151,X0))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X3),sK154),X4),X5))
| ~ mem(X5,arr(X3,sK150))
| ~ mem(X4,arr(sK150,X3))
| ~ ne(X0)
| ~ ne(X3)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_69
| spl700_151 ),
inference(forward_subsumption_resolution,[],[f20543,f10253]) ).
fof(f20549,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK161),sK160))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X0),sK157),X1),X2))
| ~ mem(X2,arr(X0,sK151))
| ~ mem(X1,arr(sK151,X0))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X3),sK154),X4),X5))
| ~ mem(X5,arr(X3,sK150))
| ~ mem(X4,arr(sK150,X3))
| ~ ne(X0)
| ~ ne(X3) )
| ~ spl700_69 ),
inference(forward_subsumption_resolution,[],[f20545,f10249]) ).
fof(f20550,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X0),sK157),X1),X2))
| ~ mem(X2,arr(X0,sK151))
| ~ mem(X1,arr(sK151,X0))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X3),sK154),X4),X5))
| ~ mem(X5,arr(X3,sK150))
| ~ mem(X4,arr(sK150,X3))
| ~ ne(X0)
| ~ ne(X3)
| ~ ne(sK150) )
| ~ spl700_69
| spl700_134 ),
inference(forward_subsumption_resolution,[],[f20546,f10250]) ).
fof(f20551,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X0),sK157),X1),X2))
| ~ mem(X2,arr(X0,sK151))
| ~ mem(X1,arr(sK151,X0))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X3),sK154),X4),X5))
| ~ mem(X5,arr(X3,sK150))
| ~ mem(X4,arr(sK150,X3))
| ~ ne(X0)
| ~ ne(X3)
| ~ ne(sK150) )
| ~ spl700_69
| spl700_151 ),
inference(forward_subsumption_resolution,[],[f20547,f10250]) ).
fof(f20554,definition,
( spl700_193
<=> p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK161),sK160)) ),
introduced(definition,[new_symbols(definition,[spl700_193])],[avatar_definition]) ).
fof(f20556,plain,
( p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK161),sK160))
| ~ spl700_193 ),
inference(avatar_component_clause,[],[f20554]) ).
fof(f20557,plain,
( spl700_111
| spl700_112
| spl700_193
| ~ spl700_69 ),
inference(avatar_split_clause,[],[f20549,f14481,f20554,f17718,f17715]) ).
fof(f20558,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X0),sK157),X1),X2))
| ~ mem(X2,arr(X0,sK151))
| ~ mem(X1,arr(sK151,X0))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X3),sK154),X4),X5))
| ~ mem(X5,arr(X3,sK150))
| ~ mem(X4,arr(sK150,X3))
| ~ ne(X0)
| ~ ne(X3) )
| ~ spl700_69
| spl700_134 ),
inference(forward_subsumption_resolution,[],[f20550,f10249]) ).
fof(f20559,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X0),sK157),X1),X2))
| ~ mem(X2,arr(X0,sK151))
| ~ mem(X1,arr(sK151,X0))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X3),sK154),X4),X5))
| ~ mem(X5,arr(X3,sK150))
| ~ mem(X4,arr(sK150,X3))
| ~ ne(X0)
| ~ ne(X3) )
| ~ spl700_69
| spl700_151 ),
inference(forward_subsumption_resolution,[],[f20551,f10249]) ).
fof(f20560,plain,
( spl700_111
| spl700_112
| ~ spl700_69
| spl700_134 ),
inference(avatar_split_clause,[],[f20558,f19071,f14481,f17718,f17715]) ).
fof(f20561,plain,
( spl700_111
| spl700_112
| ~ spl700_69
| spl700_151 ),
inference(avatar_split_clause,[],[f20559,f19226,f14481,f17718,f17715]) ).
fof(f20666,plain,
( ~ mem(sK160,arr(sK150,sK151))
| p(ap(ap(c_2Equotient_2Erespects(arr(sK150,sK151),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157)),sK160))
| ~ spl700_86
| ~ spl700_133
| ~ spl700_134 ),
inference(resolution,[],[f19073,f19148]) ).
fof(f20726,plain,
( ~ mem(sK161,arr(sK150,sK151))
| p(ap(ap(c_2Equotient_2Erespects(arr(sK150,sK151),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157)),sK161))
| ~ spl700_86
| ~ spl700_133
| ~ spl700_151 ),
inference(resolution,[],[f19227,f19148]) ).
fof(f20919,plain,
( ! [X2,X3,X0,X1,X4] :
( ap(ap(ap(c_2Equotient_2E_2D_2D_3E(sK152,sK151,sK150,sK153),sK156),sK158),sK160) != ap(ap(ap(c_2Equotient_2E_2D_2D_3E(sK152,sK151,sK150,sK153),sK156),sK158),X0)
| ~ p(ap(ap(X1,X0),X0))
| ~ p(ap(ap(X1,sK161),sK161))
| p(ap(ap(X1,X0),sK161))
| ~ mem(sK161,X2)
| ~ mem(X0,X2)
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X2,X3),X1),ap(ap(c_2Equotient_2E_2D_2D_3E(sK152,sK151,sK150,sK153),sK156),sK158)),X4))
| ~ mem(X4,arr(X3,X2))
| ~ mem(ap(ap(c_2Equotient_2E_2D_2D_3E(sK152,sK151,sK150,sK153),sK156),sK158),arr(X2,X3))
| ~ mem(X1,arr(X2,arr(X2,bool)))
| ~ ne(X3)
| ~ ne(X2) )
| ~ spl700_70 ),
inference(superposition,[],[f11199,f14487]) ).
fof(f20995,plain,
( ! [X2,X3,X0,X1] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(X1,X2),X0),ap(ap(c_2Equotient_2E_2D_2D_3E(sK152,sK151,sK150,sK153),sK156),sK158)),X3))
| ~ p(ap(ap(X0,sK161),sK161))
| p(ap(ap(X0,sK160),sK161))
| ~ mem(sK161,X1)
| ~ mem(sK160,X1)
| ~ p(ap(ap(X0,sK160),sK160))
| ~ mem(X3,arr(X2,X1))
| ~ mem(ap(ap(c_2Equotient_2E_2D_2D_3E(sK152,sK151,sK150,sK153),sK156),sK158),arr(X1,X2))
| ~ mem(X0,arr(X1,arr(X1,bool)))
| ~ ne(X2)
| ~ ne(X1) )
| ~ spl700_70 ),
inference(equality_resolution,[],[f20919]) ).
fof(f21113,plain,
( ! [X2,X3,X0,X1] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK161),sK161))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK161))
| ~ mem(sK161,arr(sK150,sK151))
| ~ mem(sK160,arr(sK150,sK151))
| ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK160))
| ~ mem(ap(ap(c_2Equotient_2E_2D_2D_3E(sK150,sK153,sK152,sK151),X2),X3),arr(arr(sK152,sK153),arr(sK150,sK151)))
| ~ mem(ap(ap(c_2Equotient_2E_2D_2D_3E(sK152,sK151,sK150,sK153),sK156),sK158),arr(arr(sK150,sK151),arr(sK152,sK153)))
| ~ mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),arr(arr(sK150,sK151),arr(arr(sK150,sK151),bool)))
| ~ ne(arr(sK152,sK153))
| ~ ne(arr(sK150,sK151))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,sK153),X1),sK158),X3))
| ~ mem(X3,arr(sK153,sK151))
| ~ mem(sK158,arr(sK151,sK153))
| ~ mem(X1,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,sK152),X0),X2),sK156))
| ~ mem(sK156,arr(sK152,sK150))
| ~ mem(X2,arr(sK150,sK152))
| ~ mem(X0,arr(sK150,arr(sK150,bool)))
| ~ ne(sK153)
| ~ ne(sK152)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_70 ),
inference(resolution,[],[f20995,f11166]) ).
fof(f21114,plain,
( ! [X2,X3,X0,X1] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK161),sK161))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK161))
| ~ mem(sK161,arr(sK150,sK151))
| ~ mem(sK160,arr(sK150,sK151))
| ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK160))
| ~ mem(ap(ap(c_2Equotient_2E_2D_2D_3E(sK150,sK153,sK152,sK151),X2),X3),arr(arr(sK152,sK153),arr(sK150,sK151)))
| ~ mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),arr(arr(sK150,sK151),arr(arr(sK150,sK151),bool)))
| ~ ne(arr(sK152,sK153))
| ~ ne(arr(sK150,sK151))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,sK153),X1),sK158),X3))
| ~ mem(X3,arr(sK153,sK151))
| ~ mem(sK158,arr(sK151,sK153))
| ~ mem(X1,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,sK152),X0),X2),sK156))
| ~ mem(sK156,arr(sK152,sK150))
| ~ mem(X2,arr(sK150,sK152))
| ~ mem(X0,arr(sK150,arr(sK150,bool)))
| ~ ne(sK153)
| ~ ne(sK152)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_70 ),
inference(forward_subsumption_resolution,[],[f21113,f15421]) ).
fof(f21115,plain,
( ! [X2,X3,X0,X1] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK161),sK161))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK161))
| ~ mem(sK161,arr(sK150,sK151))
| ~ mem(sK160,arr(sK150,sK151))
| ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK160))
| ~ mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),arr(arr(sK150,sK151),arr(arr(sK150,sK151),bool)))
| ~ ne(arr(sK152,sK153))
| ~ ne(arr(sK150,sK151))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,sK153),X1),sK158),X3))
| ~ mem(X3,arr(sK153,sK151))
| ~ mem(sK158,arr(sK151,sK153))
| ~ mem(X1,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,sK152),X0),X2),sK156))
| ~ mem(sK156,arr(sK152,sK150))
| ~ mem(X2,arr(sK150,sK152))
| ~ mem(X0,arr(sK150,arr(sK150,bool)))
| ~ ne(sK153)
| ~ ne(sK152)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_70 ),
inference(forward_subsumption_resolution,[],[f21114,f15421]) ).
fof(f21116,plain,
( ! [X2,X3,X0,X1] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK161),sK161))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK161))
| ~ mem(sK161,arr(sK150,sK151))
| ~ mem(sK160,arr(sK150,sK151))
| ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK160))
| ~ mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),arr(arr(sK150,sK151),arr(arr(sK150,sK151),bool)))
| ~ ne(arr(sK150,sK151))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,sK153),X1),sK158),X3))
| ~ mem(X3,arr(sK153,sK151))
| ~ mem(sK158,arr(sK151,sK153))
| ~ mem(X1,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,sK152),X0),X2),sK156))
| ~ mem(sK156,arr(sK152,sK150))
| ~ mem(X2,arr(sK150,sK152))
| ~ mem(X0,arr(sK150,arr(sK150,bool)))
| ~ ne(sK153)
| ~ ne(sK152)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_70 ),
inference(forward_subsumption_resolution,[],[f21115,f11164]) ).
fof(f21117,plain,
( ! [X2,X3,X0,X1] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK161),sK161))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK161))
| ~ mem(sK161,arr(sK150,sK151))
| ~ mem(sK160,arr(sK150,sK151))
| ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK160))
| ~ mem(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),arr(arr(sK150,sK151),arr(arr(sK150,sK151),bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,sK153),X1),sK158),X3))
| ~ mem(X3,arr(sK153,sK151))
| ~ mem(sK158,arr(sK151,sK153))
| ~ mem(X1,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,sK152),X0),X2),sK156))
| ~ mem(sK156,arr(sK152,sK150))
| ~ mem(X2,arr(sK150,sK152))
| ~ mem(X0,arr(sK150,arr(sK150,bool)))
| ~ ne(sK153)
| ~ ne(sK152)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_70 ),
inference(forward_subsumption_resolution,[],[f21116,f11164]) ).
fof(f21118,plain,
( ! [X2,X3,X0,X1] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK161),sK161))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK161))
| ~ mem(sK161,arr(sK150,sK151))
| ~ mem(sK160,arr(sK150,sK151))
| ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK160))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,sK153),X1),sK158),X3))
| ~ mem(X3,arr(sK153,sK151))
| ~ mem(sK158,arr(sK151,sK153))
| ~ mem(X1,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,sK152),X0),X2),sK156))
| ~ mem(sK156,arr(sK152,sK150))
| ~ mem(X2,arr(sK150,sK152))
| ~ mem(X0,arr(sK150,arr(sK150,bool)))
| ~ ne(sK153)
| ~ ne(sK152)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_70 ),
inference(forward_subsumption_resolution,[],[f21117,f15582]) ).
fof(f21119,plain,
( ! [X2,X3,X0,X1] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK161),sK161))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK161))
| ~ mem(sK160,arr(sK150,sK151))
| ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK160))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,sK153),X1),sK158),X3))
| ~ mem(X3,arr(sK153,sK151))
| ~ mem(sK158,arr(sK151,sK153))
| ~ mem(X1,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,sK152),X0),X2),sK156))
| ~ mem(sK156,arr(sK152,sK150))
| ~ mem(X2,arr(sK150,sK152))
| ~ mem(X0,arr(sK150,arr(sK150,bool)))
| ~ ne(sK153)
| ~ ne(sK152)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_70 ),
inference(forward_subsumption_resolution,[],[f21118,f10262]) ).
fof(f21120,plain,
( ! [X2,X3,X0,X1] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK161),sK161))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK161))
| ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK160))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,sK153),X1),sK158),X3))
| ~ mem(X3,arr(sK153,sK151))
| ~ mem(sK158,arr(sK151,sK153))
| ~ mem(X1,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,sK152),X0),X2),sK156))
| ~ mem(sK156,arr(sK152,sK150))
| ~ mem(X2,arr(sK150,sK152))
| ~ mem(X0,arr(sK150,arr(sK150,bool)))
| ~ ne(sK153)
| ~ ne(sK152)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_70 ),
inference(forward_subsumption_resolution,[],[f21119,f10261]) ).
fof(f21121,plain,
( ! [X2,X3,X0,X1] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK161),sK161))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK161))
| ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK160))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,sK153),X1),sK158),X3))
| ~ mem(X3,arr(sK153,sK151))
| ~ mem(X1,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,sK152),X0),X2),sK156))
| ~ mem(sK156,arr(sK152,sK150))
| ~ mem(X2,arr(sK150,sK152))
| ~ mem(X0,arr(sK150,arr(sK150,bool)))
| ~ ne(sK153)
| ~ ne(sK152)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_70 ),
inference(forward_subsumption_resolution,[],[f21120,f10258]) ).
fof(f21122,plain,
( ! [X2,X3,X0,X1] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK161),sK161))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK161))
| ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK160))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,sK153),X1),sK158),X3))
| ~ mem(X3,arr(sK153,sK151))
| ~ mem(X1,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,sK152),X0),X2),sK156))
| ~ mem(X2,arr(sK150,sK152))
| ~ mem(X0,arr(sK150,arr(sK150,bool)))
| ~ ne(sK153)
| ~ ne(sK152)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_70 ),
inference(forward_subsumption_resolution,[],[f21121,f10255]) ).
fof(f21123,plain,
( ! [X2,X3,X0,X1] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK161),sK161))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK161))
| ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK160))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,sK153),X1),sK158),X3))
| ~ mem(X3,arr(sK153,sK151))
| ~ mem(X1,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,sK152),X0),X2),sK156))
| ~ mem(X2,arr(sK150,sK152))
| ~ mem(X0,arr(sK150,arr(sK150,bool)))
| ~ ne(sK152)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_70 ),
inference(forward_subsumption_resolution,[],[f21122,f10252]) ).
fof(f21124,plain,
( ! [X2,X3,X0,X1] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK161),sK161))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK161))
| ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK160))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,sK153),X1),sK158),X3))
| ~ mem(X3,arr(sK153,sK151))
| ~ mem(X1,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,sK152),X0),X2),sK156))
| ~ mem(X2,arr(sK150,sK152))
| ~ mem(X0,arr(sK150,arr(sK150,bool)))
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_70 ),
inference(forward_subsumption_resolution,[],[f21123,f10251]) ).
fof(f21125,plain,
( ! [X2,X3,X0,X1] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK161),sK161))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK161))
| ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK160))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,sK153),X1),sK158),X3))
| ~ mem(X3,arr(sK153,sK151))
| ~ mem(X1,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,sK152),X0),X2),sK156))
| ~ mem(X2,arr(sK150,sK152))
| ~ mem(X0,arr(sK150,arr(sK150,bool)))
| ~ ne(sK150) )
| ~ spl700_70 ),
inference(forward_subsumption_resolution,[],[f21124,f10250]) ).
fof(f21126,plain,
( ! [X2,X3,X0,X1] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK161),sK161))
| p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK161))
| ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),X0),X1),sK160),sK160))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,sK153),X1),sK158),X3))
| ~ mem(X3,arr(sK153,sK151))
| ~ mem(X1,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,sK152),X0),X2),sK156))
| ~ mem(X2,arr(sK150,sK152))
| ~ mem(X0,arr(sK150,arr(sK150,bool))) )
| ~ spl700_70 ),
inference(forward_subsumption_resolution,[],[f21125,f10249]) ).
fof(f21127,plain,
( ! [X0,X1] :
( p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK160),sK161))
| ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK160),sK160))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,sK153),sK157),sK158),X0))
| ~ mem(X0,arr(sK153,sK151))
| ~ mem(sK157,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,sK152),sK154),X1),sK156))
| ~ mem(X1,arr(sK150,sK152))
| ~ mem(sK154,arr(sK150,arr(sK150,bool))) )
| ~ spl700_70
| ~ spl700_151 ),
inference(resolution,[],[f21126,f19227]) ).
fof(f21128,plain,
( ! [X0,X1] :
( ~ p(ap(ap(ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157),sK160),sK160))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,sK153),sK157),sK158),X0))
| ~ mem(X0,arr(sK153,sK151))
| ~ mem(sK157,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,sK152),sK154),X1),sK156))
| ~ mem(X1,arr(sK150,sK152))
| ~ mem(sK154,arr(sK150,arr(sK150,bool))) )
| spl700_69
| ~ spl700_70
| ~ spl700_151 ),
inference(forward_subsumption_resolution,[],[f21127,f14482]) ).
fof(f21129,plain,
( ! [X0,X1] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,sK153),sK157),sK158),X0))
| ~ mem(X0,arr(sK153,sK151))
| ~ mem(sK157,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,sK152),sK154),X1),sK156))
| ~ mem(X1,arr(sK150,sK152))
| ~ mem(sK154,arr(sK150,arr(sK150,bool))) )
| spl700_69
| ~ spl700_70
| ~ spl700_134
| ~ spl700_151 ),
inference(forward_subsumption_resolution,[],[f21128,f19073]) ).
fof(f21130,plain,
( ! [X0,X1] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,sK153),sK157),sK158),X0))
| ~ mem(X0,arr(sK153,sK151))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,sK152),sK154),X1),sK156))
| ~ mem(X1,arr(sK150,sK152))
| ~ mem(sK154,arr(sK150,arr(sK150,bool))) )
| spl700_69
| ~ spl700_70
| ~ spl700_134
| ~ spl700_151 ),
inference(forward_subsumption_resolution,[],[f21129,f10257]) ).
fof(f21131,plain,
( ! [X0,X1] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,sK153),sK157),sK158),X0))
| ~ mem(X0,arr(sK153,sK151))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,sK152),sK154),X1),sK156))
| ~ mem(X1,arr(sK150,sK152)) )
| spl700_69
| ~ spl700_70
| ~ spl700_134
| ~ spl700_151 ),
inference(forward_subsumption_resolution,[],[f21130,f10253]) ).
fof(f21133,definition,
( spl700_210
<=> ! [X1] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,sK152),sK154),X1),sK156))
| ~ mem(X1,arr(sK150,sK152)) ) ),
introduced(definition,[new_symbols(definition,[spl700_210])],[avatar_definition]) ).
fof(f21134,plain,
( ! [X1] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,sK152),sK154),X1),sK156))
| ~ mem(X1,arr(sK150,sK152)) )
| ~ spl700_210 ),
inference(avatar_component_clause,[],[f21133]) ).
fof(f21136,definition,
( spl700_211
<=> ! [X0] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,sK153),sK157),sK158),X0))
| ~ mem(X0,arr(sK153,sK151)) ) ),
introduced(definition,[new_symbols(definition,[spl700_211])],[avatar_definition]) ).
fof(f21137,plain,
( ! [X0] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,sK153),sK157),sK158),X0))
| ~ mem(X0,arr(sK153,sK151)) )
| ~ spl700_211 ),
inference(avatar_component_clause,[],[f21136]) ).
fof(f21138,plain,
( spl700_210
| spl700_211
| spl700_69
| ~ spl700_70
| ~ spl700_134
| ~ spl700_151 ),
inference(avatar_split_clause,[],[f21131,f19226,f19071,f14485,f14481,f21136,f21133]) ).
fof(f21139,plain,
( ~ mem(sK159,arr(sK153,sK151))
| ~ spl700_211 ),
inference(resolution,[],[f21137,f10260]) ).
fof(f21140,plain,
( $false
| ~ spl700_211 ),
inference(forward_subsumption_resolution,[],[f21139,f10259]) ).
fof(f21141,plain,
~ spl700_211,
inference(avatar_contradiction_clause,[],[f21140]) ).
fof(f21142,plain,
( ~ mem(sK155,arr(sK150,sK152))
| ~ spl700_210 ),
inference(resolution,[],[f21134,f10256]) ).
fof(f21143,plain,
( $false
| ~ spl700_210 ),
inference(forward_subsumption_resolution,[],[f21142,f10254]) ).
fof(f21144,plain,
~ spl700_210,
inference(avatar_contradiction_clause,[],[f21143]) ).
fof(f21152,plain,
( p(ap(ap(c_2Equotient_2Erespects(arr(sK150,sK151),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157)),sK160))
| ~ spl700_86
| ~ spl700_133
| ~ spl700_134 ),
inference(forward_subsumption_resolution,[],[f20666,f10261]) ).
fof(f21154,plain,
( $false
| spl700_72
| ~ spl700_86
| ~ spl700_133
| ~ spl700_134 ),
inference(forward_subsumption_resolution,[],[f21152,f14496]) ).
fof(f21155,plain,
( spl700_72
| ~ spl700_86
| ~ spl700_133
| ~ spl700_134 ),
inference(avatar_contradiction_clause,[],[f21154]) ).
fof(f21162,plain,
( p(ap(ap(c_2Equotient_2Erespects(arr(sK150,sK151),bool),ap(ap(c_2Equotient_2E_3D_3D_3D_3E(sK150,sK151),sK154),sK157)),sK161))
| ~ spl700_86
| ~ spl700_133
| ~ spl700_151 ),
inference(forward_subsumption_resolution,[],[f20726,f10262]) ).
fof(f21163,plain,
( $false
| spl700_71
| ~ spl700_86
| ~ spl700_133
| ~ spl700_151 ),
inference(forward_subsumption_resolution,[],[f21162,f14491]) ).
fof(f21164,plain,
( spl700_71
| ~ spl700_86
| ~ spl700_133
| ~ spl700_151 ),
inference(avatar_contradiction_clause,[],[f21163]) ).
fof(f21175,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ mem(sK160,arr(sK150,sK151))
| ~ mem(sK161,arr(sK150,sK151))
| ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,sK151,sK150,X1),X2),X3),sK160) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,sK151,sK150,X1),X2),X3),sK161)
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X1),sK157),X3),X4))
| ~ mem(X4,arr(X1,sK151))
| ~ mem(X3,arr(sK151,X1))
| ~ mem(sK157,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X0),sK154),X5),X2))
| ~ mem(X2,arr(X0,sK150))
| ~ mem(X5,arr(sK150,X0))
| ~ mem(sK154,arr(sK150,arr(sK150,bool)))
| ~ ne(X1)
| ~ ne(X0)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_193 ),
inference(resolution,[],[f20556,f17680]) ).
fof(f21182,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ mem(sK161,arr(sK150,sK151))
| ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,sK151,sK150,X1),X2),X3),sK160) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,sK151,sK150,X1),X2),X3),sK161)
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X1),sK157),X3),X4))
| ~ mem(X4,arr(X1,sK151))
| ~ mem(X3,arr(sK151,X1))
| ~ mem(sK157,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X0),sK154),X5),X2))
| ~ mem(X2,arr(X0,sK150))
| ~ mem(X5,arr(sK150,X0))
| ~ mem(sK154,arr(sK150,arr(sK150,bool)))
| ~ ne(X1)
| ~ ne(X0)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_193 ),
inference(forward_subsumption_resolution,[],[f21175,f10261]) ).
fof(f21184,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,sK151,sK150,X1),X2),X3),sK160) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,sK151,sK150,X1),X2),X3),sK161)
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X1),sK157),X3),X4))
| ~ mem(X4,arr(X1,sK151))
| ~ mem(X3,arr(sK151,X1))
| ~ mem(sK157,arr(sK151,arr(sK151,bool)))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X0),sK154),X5),X2))
| ~ mem(X2,arr(X0,sK150))
| ~ mem(X5,arr(sK150,X0))
| ~ mem(sK154,arr(sK150,arr(sK150,bool)))
| ~ ne(X1)
| ~ ne(X0)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_193 ),
inference(forward_subsumption_resolution,[],[f21182,f10262]) ).
fof(f21186,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,sK151,sK150,X1),X2),X3),sK160) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,sK151,sK150,X1),X2),X3),sK161)
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X1),sK157),X3),X4))
| ~ mem(X4,arr(X1,sK151))
| ~ mem(X3,arr(sK151,X1))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X0),sK154),X5),X2))
| ~ mem(X2,arr(X0,sK150))
| ~ mem(X5,arr(sK150,X0))
| ~ mem(sK154,arr(sK150,arr(sK150,bool)))
| ~ ne(X1)
| ~ ne(X0)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_193 ),
inference(forward_subsumption_resolution,[],[f21184,f10257]) ).
fof(f21188,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,sK151,sK150,X1),X2),X3),sK160) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,sK151,sK150,X1),X2),X3),sK161)
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X1),sK157),X3),X4))
| ~ mem(X4,arr(X1,sK151))
| ~ mem(X3,arr(sK151,X1))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X0),sK154),X5),X2))
| ~ mem(X2,arr(X0,sK150))
| ~ mem(X5,arr(sK150,X0))
| ~ ne(X1)
| ~ ne(X0)
| ~ ne(sK151)
| ~ ne(sK150) )
| ~ spl700_193 ),
inference(forward_subsumption_resolution,[],[f21186,f10253]) ).
fof(f21190,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,sK151,sK150,X1),X2),X3),sK160) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,sK151,sK150,X1),X2),X3),sK161)
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X1),sK157),X3),X4))
| ~ mem(X4,arr(X1,sK151))
| ~ mem(X3,arr(sK151,X1))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X0),sK154),X5),X2))
| ~ mem(X2,arr(X0,sK150))
| ~ mem(X5,arr(sK150,X0))
| ~ ne(X1)
| ~ ne(X0)
| ~ ne(sK150) )
| ~ spl700_193 ),
inference(forward_subsumption_resolution,[],[f21188,f10250]) ).
fof(f21192,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK151,X1),sK157),X3),X4))
| ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,sK151,sK150,X1),X2),X3),sK160) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,sK151,sK150,X1),X2),X3),sK161)
| ~ mem(X4,arr(X1,sK151))
| ~ mem(X3,arr(sK151,X1))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X0),sK154),X5),X2))
| ~ mem(X2,arr(X0,sK150))
| ~ mem(X5,arr(sK150,X0))
| ~ ne(X1)
| ~ ne(X0) )
| ~ spl700_193 ),
inference(forward_subsumption_resolution,[],[f21190,f10249]) ).
fof(f21210,plain,
( ! [X2,X0,X1] :
( ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,sK151,sK150,sK153),X1),sK158),sK161) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,sK151,sK150,sK153),X1),sK158),sK160)
| ~ mem(sK159,arr(sK153,sK151))
| ~ mem(sK158,arr(sK151,sK153))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X0),sK154),X2),X1))
| ~ mem(X1,arr(X0,sK150))
| ~ mem(X2,arr(sK150,X0))
| ~ ne(sK153)
| ~ ne(X0) )
| ~ spl700_193 ),
inference(resolution,[],[f21192,f10260]) ).
fof(f21214,plain,
( ! [X2,X0,X1] :
( ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,sK151,sK150,sK153),X1),sK158),sK161) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,sK151,sK150,sK153),X1),sK158),sK160)
| ~ mem(sK158,arr(sK151,sK153))
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X0),sK154),X2),X1))
| ~ mem(X1,arr(X0,sK150))
| ~ mem(X2,arr(sK150,X0))
| ~ ne(sK153)
| ~ ne(X0) )
| ~ spl700_193 ),
inference(forward_subsumption_resolution,[],[f21210,f10259]) ).
fof(f21215,plain,
( ! [X2,X0,X1] :
( ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,sK151,sK150,sK153),X1),sK158),sK161) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,sK151,sK150,sK153),X1),sK158),sK160)
| ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X0),sK154),X2),X1))
| ~ mem(X1,arr(X0,sK150))
| ~ mem(X2,arr(sK150,X0))
| ~ ne(sK153)
| ~ ne(X0) )
| ~ spl700_193 ),
inference(forward_subsumption_resolution,[],[f21214,f10258]) ).
fof(f21216,plain,
( ! [X2,X0,X1] :
( ~ p(ap(ap(ap(c_2Equotient_2EQUOTIENT(sK150,X0),sK154),X2),X1))
| ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,sK151,sK150,sK153),X1),sK158),sK161) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(X0,sK151,sK150,sK153),X1),sK158),sK160)
| ~ mem(X1,arr(X0,sK150))
| ~ mem(X2,arr(sK150,X0))
| ~ ne(X0) )
| ~ spl700_193 ),
inference(forward_subsumption_resolution,[],[f21215,f10252]) ).
fof(f21217,plain,
( ap(ap(ap(c_2Equotient_2E_2D_2D_3E(sK152,sK151,sK150,sK153),sK156),sK158),sK160) = ap(ap(ap(c_2Equotient_2E_2D_2D_3E(sK152,sK151,sK150,sK153),sK156),sK158),sK161)
| ~ mem(sK156,arr(sK152,sK150))
| ~ mem(sK155,arr(sK150,sK152))
| ~ ne(sK152)
| ~ spl700_193 ),
inference(resolution,[],[f21216,f10256]) ).
fof(f21221,plain,
( ~ mem(sK156,arr(sK152,sK150))
| ~ mem(sK155,arr(sK150,sK152))
| ~ ne(sK152)
| spl700_70
| ~ spl700_193 ),
inference(forward_subsumption_resolution,[],[f21217,f14486]) ).
fof(f21222,plain,
( ~ mem(sK155,arr(sK150,sK152))
| ~ ne(sK152)
| spl700_70
| ~ spl700_193 ),
inference(forward_subsumption_resolution,[],[f21221,f10255]) ).
fof(f21223,plain,
( ~ ne(sK152)
| spl700_70
| ~ spl700_193 ),
inference(forward_subsumption_resolution,[],[f21222,f10254]) ).
fof(f21224,plain,
( $false
| spl700_70
| ~ spl700_193 ),
inference(forward_subsumption_resolution,[],[f21223,f10251]) ).
fof(f21225,plain,
( spl700_70
| ~ spl700_193 ),
inference(avatar_contradiction_clause,[],[f21224]) ).
cnf(s72,plain,
( spl700_69
| spl700_70 ),
inference(sat_conversion,[],[f14488]) ).
cnf(s73,plain,
( spl700_69
| spl700_71 ),
inference(sat_conversion,[],[f14493]) ).
cnf(s74,plain,
( spl700_69
| spl700_72 ),
inference(sat_conversion,[],[f14498]) ).
cnf(s75,plain,
( ~ spl700_69
| ~ spl700_70
| ~ spl700_71
| ~ spl700_72 ),
inference(sat_conversion,[],[f14499]) ).
cnf(s111,plain,
spl700_86,
inference(sat_conversion,[],[f16469]) ).
cnf(s143,plain,
~ spl700_112,
inference(sat_conversion,[],[f19019]) ).
cnf(s150,plain,
( ~ spl700_72
| ~ spl700_86
| ~ spl700_133
| spl700_134 ),
inference(sat_conversion,[],[f19074]) ).
cnf(s151,plain,
spl700_133,
inference(sat_conversion,[],[f19084]) ).
cnf(s152,plain,
~ spl700_111,
inference(sat_conversion,[],[f19092]) ).
cnf(s168,plain,
( ~ spl700_71
| ~ spl700_86
| ~ spl700_133
| spl700_151 ),
inference(sat_conversion,[],[f19345]) ).
cnf(s221,plain,
( ~ spl700_69
| spl700_111
| spl700_112
| spl700_193 ),
inference(sat_conversion,[],[f20557]) ).
cnf(s222,plain,
( ~ spl700_69
| spl700_111
| spl700_112
| spl700_134 ),
inference(sat_conversion,[],[f20560]) ).
cnf(s223,plain,
( ~ spl700_69
| spl700_111
| spl700_112
| spl700_151 ),
inference(sat_conversion,[],[f20561]) ).
cnf(s240,plain,
( spl700_69
| ~ spl700_70
| ~ spl700_134
| ~ spl700_151
| spl700_210
| spl700_211 ),
inference(sat_conversion,[],[f21138]) ).
cnf(s241,plain,
~ spl700_211,
inference(sat_conversion,[],[f21141]) ).
cnf(s242,plain,
~ spl700_210,
inference(sat_conversion,[],[f21144]) ).
cnf(s246,plain,
( spl700_72
| ~ spl700_86
| ~ spl700_133
| ~ spl700_134 ),
inference(sat_conversion,[],[f21155]) ).
cnf(s250,plain,
( spl700_71
| ~ spl700_86
| ~ spl700_133
| ~ spl700_151 ),
inference(sat_conversion,[],[f21164]) ).
cnf(s252,plain,
( spl700_70
| ~ spl700_193 ),
inference(sat_conversion,[],[f21225]) ).
cnf(s253,plain,
( spl700_69
| ~ spl700_70
| ~ spl700_134
| ~ spl700_151 ),
inference(rat,[],[s240,s241,s242]) ).
cnf(s264,plain,
( ~ spl700_72
| ~ spl700_86
| spl700_134 ),
inference(rat,[],[s150,s151]) ).
cnf(s309,plain,
spl700_69,
inference(rat,[],[s253,s168,s264,s72,s73,s74,s151,s111]) ).
cnf(s310,plain,
spl700_151,
inference(rat,[],[s223,s143,s152,s309]) ).
cnf(s311,plain,
spl700_134,
inference(rat,[],[s222,s143,s152,s309]) ).
cnf(s312,plain,
spl700_193,
inference(rat,[],[s221,s143,s152,s309]) ).
cnf(s316,plain,
spl700_71,
inference(rat,[],[s250,s111,s151,s310]) ).
cnf(s319,plain,
spl700_72,
inference(rat,[],[s246,s111,s151,s311]) ).
cnf(s320,plain,
spl700_70,
inference(rat,[],[s252,s312]) ).
cnf(s328,plain,
$false,
inference(rat,[],[s75,s309,s320,s316,s319]) ).
fof(f21226,plain,
$false,
inference(avatar_sat_refutation,[],[s328]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP009+5 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/10.40 % Computer : n014.cluster.edu
% 0.12/10.40 % Model : x86_64 x86_64
% 0.12/10.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/10.40 % Memory : 8046.5625MB
% 0.12/10.40 % OS : Linux 6.8.0-71-generic
% 0.12/10.40 % CPULimit : 300
% 0.12/10.40 % WCLimit : 300
% 0.12/10.40 % DateTime : Sun Sep 27 11:55:57 UTC 2026
% 0.12/10.41 % CPUTime :
% 0.12/10.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/10.44 Running first-order theorem proving
% 0.12/10.44 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.04/13.96 % (675562)Detected formulas, will run a generic FOF schedule.
% 14.04/13.96 % (675569)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=1740628911:i=141695:sd=1:nm=32:gsp=on:ss=included_2988 on theBenchmark for (2988ds/141695Mi)
% 14.04/13.96 % (675570)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4255490258:i=109:sd=1:ins=1:gsp=on:ss=axioms_2988 on theBenchmark for (2988ds/109Mi)
% 14.04/13.96 % (675568)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=1439145597:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2988 on theBenchmark for (2988ds/134677Mi)
% 14.04/13.96 % (675571)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2661678885:i=119:av=off:ss=axioms_2988 on theBenchmark for (2988ds/119Mi)
% 14.04/13.96 % (675567)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=2172696696:i=141193_2988 on theBenchmark for (2988ds/141193Mi)
% 14.04/13.96 % (675573)dis-21_1_sil=8000:lcm=predicate:random_seed=287608569:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2988 on theBenchmark for (2988ds/129Mi)
% 14.04/13.96 % (675572)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=707707631:s2a=on:i=139:gtg=position_2988 on theBenchmark for (2988ds/139Mi)
% 14.04/13.96 % (675572)Instruction limit reached!
% 14.04/13.96 % (675572)------------------------------
% 14.04/13.96 % (675572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.04/13.96 % (675572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.04/13.96 % (675572)CaDiCaL version: 2.1.3
% 14.04/13.96 % (675572)Termination reason: Instruction limit
% 14.04/13.96 % (675572)Termination phase: Property scanning
% 14.04/13.96 % (675572)Time elapsed: 0.053 s
% 14.04/13.96 % (675572)Peak memory usage: 102 MB
% 14.04/13.96 % (675572)Instructions burned: 140 (million)
% 14.04/13.96 % (675570)Instruction limit reached!
% 14.04/13.96 % (675570)------------------------------
% 14.04/13.96 % (675570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.04/13.96 % (675570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.04/13.96 % (675570)CaDiCaL version: 2.1.3
% 14.04/13.96 % (675570)Termination reason: Instruction limit
% 14.04/13.96 % (675570)Termination phase: General splitting
% 14.04/13.96 % (675570)Time elapsed: 0.071 s
% 14.04/13.96 % (675570)Peak memory usage: 105 MB
% 14.04/13.96 % (675570)Instructions burned: 111 (million)
% 14.04/13.96 % (675571)Instruction limit reached!
% 14.04/13.96 % (675571)------------------------------
% 14.04/13.96 % (675571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.04/13.96 % (675571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.04/13.96 % (675571)CaDiCaL version: 2.1.3
% 14.04/13.96 % (675571)Termination reason: Instruction limit
% 14.04/13.96 % (675571)Termination phase: Preprocessing 3
% 14.04/13.96 % (675571)Time elapsed: 0.081 s
% 14.04/13.96 % (675571)Peak memory usage: 105 MB
% 14.04/13.96 % (675571)Instructions burned: 119 (million)
% 14.04/13.96 % (675573)Instruction limit reached!
% 14.04/13.96 % (675573)------------------------------
% 14.04/13.96 % (675573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.04/13.96 % (675573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.04/13.96 % (675573)CaDiCaL version: 2.1.3
% 14.04/13.96 % (675573)Termination reason: Instruction limit
% 14.04/13.96 % (675573)Termination phase: Preprocessing 1
% 14.04/13.96 % (675573)Time elapsed: 0.082 s
% 14.04/13.96 % (675573)Peak memory usage: 103 MB
% 14.04/13.96 % (675573)Instructions burned: 129 (million)
% 14.04/13.96 % (675581)lrs+10_1_sil=8000:sp=occurrence:random_seed=3046693669:i=285:sd=3:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/285Mi)
% 14.04/13.96 % (675582)lrs+10_1_sil=32000:urr=on:br=off:random_seed=376229871:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/157Mi)
% 14.04/13.96 % (675583)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3773584072:i=325:sd=1:ss=axioms:sgt=32_2986 on theBenchmark for (2986ds/325Mi)
% 14.04/13.96 % (675584)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=2043269307:s2a=on:i=248:s2at=1.23:gtg=position_2986 on theBenchmark for (2986ds/248Mi)
% 14.04/13.96 % (675582)Instruction limit reached!
% 14.04/13.96 % (675582)------------------------------
% 22.91/15.06 % (675582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.91/15.06 % (675582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.91/15.06 % (675582)CaDiCaL version: 2.1.3
% 22.91/15.06 % (675582)Termination reason: Instruction limit
% 22.91/15.06 % (675582)Termination phase: Property scanning
% 22.91/15.06 % (675582)Time elapsed: 0.059 s
% 22.91/15.06 % (675582)Peak memory usage: 102 MB
% 22.91/15.06 % (675582)Instructions burned: 157 (million)
% 22.91/15.06 % (675584)Instruction limit reached!
% 22.91/15.06 % (675584)------------------------------
% 22.91/15.06 % (675584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.91/15.06 % (675584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.91/15.06 % (675584)CaDiCaL version: 2.1.3
% 22.91/15.06 % (675584)Termination reason: Instruction limit
% 22.91/15.06 % (675584)Termination phase: Property scanning
% 22.91/15.06 % (675584)Time elapsed: 0.094 s
% 22.91/15.06 % (675584)Peak memory usage: 103 MB
% 22.91/15.06 % (675584)Instructions burned: 250 (million)
% 22.91/15.06 % (675581)Instruction limit reached!
% 22.91/15.06 % (675581)------------------------------
% 22.91/15.06 % (675581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.91/15.06 % (675581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.91/15.06 % (675581)CaDiCaL version: 2.1.3
% 22.91/15.06 % (675581)Termination reason: Instruction limit
% 22.91/15.06 % (675581)Termination phase: Saturation
% 22.91/15.06 % (675581)Time elapsed: 0.174 s
% 22.91/15.06 % (675581)Peak memory usage: 110 MB
% 22.91/15.06 % (675581)Instructions burned: 286 (million)
% 22.91/15.06 % (675583)Instruction limit reached!
% 22.91/15.06 % (675583)------------------------------
% 22.91/15.06 % (675583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.91/15.06 % (675583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.91/15.06 % (675583)CaDiCaL version: 2.1.3
% 22.91/15.06 % (675583)Termination reason: Instruction limit
% 22.91/15.06 % (675583)Termination phase: Saturation
% 22.91/15.06 % (675583)Time elapsed: 0.207 s
% 22.91/15.06 % (675583)Peak memory usage: 109 MB
% 22.91/15.06 % (675583)Instructions burned: 325 (million)
% 22.91/15.06 % (675589)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4234705599:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2984 on theBenchmark for (2984ds/294Mi)
% 22.91/15.06 % (675590)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2811572893:i=2350_2983 on theBenchmark for (2983ds/2350Mi)
% 22.91/15.06 % (675591)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2028543097:cts=off:i=113:fsr=off:ss=included:sgt=4_2983 on theBenchmark for (2983ds/113Mi)
% 22.91/15.06 % (675592)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2284067585:i=127:av=off:fsr=off:sup=off_2982 on theBenchmark for (2982ds/127Mi)
% 22.91/15.06 % (675589)Instruction limit reached!
% 22.91/15.06 % (675589)------------------------------
% 22.91/15.06 % (675589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.91/15.06 % (675589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.91/15.06 % (675589)CaDiCaL version: 2.1.3
% 22.91/15.06 % (675589)Termination reason: Instruction limit
% 22.91/15.06 % (675589)Termination phase: Saturation
% 22.91/15.06 % (675589)Time elapsed: 0.173 s
% 22.91/15.06 % (675589)Peak memory usage: 109 MB
% 22.91/15.06 % (675589)Instructions burned: 295 (million)
% 22.91/15.06 % (675591)Instruction limit reached!
% 22.91/15.06 % (675591)------------------------------
% 22.91/15.06 % (675591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.91/15.06 % (675591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.91/15.06 % (675591)CaDiCaL version: 2.1.3
% 22.91/15.06 % (675591)Termination reason: Instruction limit
% 22.91/15.06 % (675591)Termination phase: Preprocessing 3
% 22.91/15.06 % (675591)Time elapsed: 0.080 s
% 22.91/15.06 % (675591)Peak memory usage: 105 MB
% 22.91/15.06 % (675591)Instructions burned: 114 (million)
% 22.91/15.06 % (675592)Instruction limit reached!
% 22.91/15.06 % (675592)------------------------------
% 22.91/15.06 % (675592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.91/15.06 % (675592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.91/15.06 % (675592)CaDiCaL version: 2.1.3
% 22.91/15.06 % (675592)Termination reason: Instruction limit
% 22.91/15.06 % (675592)Termination phase: Preprocessing 2
% 22.91/15.06 % (675592)Time elapsed: 0.094 s
% 24.39/17.95 % (675592)Peak memory usage: 104 MB
% 24.39/17.95 % (675592)Instructions burned: 128 (million)
% 24.39/17.95 % (675597)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1500444629:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2980 on theBenchmark for (2980ds/114Mi)
% 24.39/17.95 % (675598)lrs+10_1_sil=8000:sp=occurrence:random_seed=3552893666:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2980 on theBenchmark for (2980ds/907Mi)
% 24.39/17.95 % (675597)Instruction limit reached!
% 24.39/17.95 % (675597)------------------------------
% 24.39/17.95 % (675597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.39/17.95 % (675597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.39/17.95 % (675597)CaDiCaL version: 2.1.3
% 24.39/17.95 % (675597)Termination reason: Instruction limit
% 24.39/17.95 % (675597)Termination phase: Property scanning
% 24.39/17.95 % (675597)Time elapsed: 0.045 s
% 24.39/17.95 % (675597)Peak memory usage: 103 MB
% 24.39/17.95 % (675597)Instructions burned: 117 (million)
% 24.39/17.95 % (675599)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1204899631:i=437:sd=1:aac=none:ss=included_2980 on theBenchmark for (2980ds/437Mi)
% 24.39/17.95 % (675602)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1703993028:i=5202:ss=axioms:sgt=16_2978 on theBenchmark for (2978ds/5202Mi)
% 24.39/17.95 % (675599)Instruction limit reached!
% 24.39/17.95 % (675599)------------------------------
% 24.39/17.95 % (675599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.39/17.95 % (675599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.39/17.95 % (675599)CaDiCaL version: 2.1.3
% 24.39/17.95 % (675599)Termination reason: Instruction limit
% 24.39/17.95 % (675599)Termination phase: Saturation
% 24.39/17.95 % (675599)Time elapsed: 0.255 s
% 24.39/17.95 % (675599)Peak memory usage: 111 MB
% 24.39/17.95 % (675599)Instructions burned: 438 (million)
% 24.39/17.95 % (675605)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3721438672:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2976 on theBenchmark for (2976ds/134Mi)
% 24.39/17.95 % (675598)Instruction limit reached!
% 24.39/17.95 % (675598)------------------------------
% 24.39/17.95 % (675598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.39/17.95 % (675598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.39/17.95 % (675598)CaDiCaL version: 2.1.3
% 24.39/17.95 % (675598)Termination reason: Instruction limit
% 24.39/17.95 % (675598)Termination phase: Saturation
% 24.39/17.95 % (675598)Time elapsed: 0.508 s
% 24.39/17.95 % (675598)Peak memory usage: 119 MB
% 24.39/17.95 % (675598)Instructions burned: 907 (million)
% 24.39/17.95 % (675605)Instruction limit reached!
% 24.39/17.95 % (675605)------------------------------
% 24.39/17.95 % (675605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.39/17.95 % (675605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.39/17.95 % (675605)CaDiCaL version: 2.1.3
% 24.39/17.95 % (675605)Termination reason: Instruction limit
% 24.39/17.95 % (675605)Termination phase: Property scanning
% 24.39/17.95 % (675605)Time elapsed: 0.091 s
% 24.39/17.95 % (675605)Peak memory usage: 105 MB
% 24.39/17.95 % (675605)Instructions burned: 135 (million)
% 24.39/17.95 % (675607)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=438044449:st=8:i=592:sd=3:ep=RST:ss=axioms_2974 on theBenchmark for (2974ds/592Mi)
% 24.39/17.95 % (675608)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=354832113:st=3:i=13193:sd=3:ss=axioms_2973 on theBenchmark for (2973ds/13193Mi)
% 24.39/17.95 % (675590)Instruction limit reached!
% 24.39/17.95 % (675590)------------------------------
% 24.39/17.95 % (675590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.39/17.95 % (675590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.39/17.95 % (675590)CaDiCaL version: 2.1.3
% 24.39/17.95 % (675590)Termination reason: Instruction limit
% 24.39/17.95 % (675590)Termination phase: Property scanning
% 24.39/17.95 % (675590)Time elapsed: 1.106 s
% 24.39/17.95 % (675590)Peak memory usage: 152 MB
% 24.39/17.95 % (675590)Instructions burned: 2353 (million)
% 24.39/17.95 % (675607)Instruction limit reached!
% 24.39/17.95 % (675607)------------------------------
% 24.39/17.95 % (675607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.39/17.95 % (675607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.39/17.95 % (675607)CaDiCaL version: 2.1.3
% 24.39/17.95 % (675607)Termination reason: Instruction limit
% 24.39/17.95 % (675607)Termination phase: Property scanning
% 24.39/17.95 % (675607)Time elapsed: 0.313 s
% 24.39/17.95 % (675607)Peak memory usage: 113 MB
% 24.39/17.95 % (675607)Instructions burned: 593 (million)
% 24.39/17.95 % (675611)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=1413017636:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2970 on theBenchmark for (2970ds/125Mi)
% 24.39/17.95 % (675611)Instruction limit reached!
% 24.39/17.95 % (675611)------------------------------
% 24.39/17.95 % (675611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.39/17.95 % (675611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.39/17.95 % (675611)CaDiCaL version: 2.1.3
% 24.39/17.95 % (675611)Termination reason: Instruction limit
% 24.39/17.95 % (675611)Termination phase: Property scanning
% 24.39/17.95 % (675611)Time elapsed: 0.048 s
% 24.39/17.95 % (675611)Peak memory usage: 103 MB
% 24.39/17.95 % (675611)Instructions burned: 125 (million)
% 24.39/17.95 % (675612)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2590118882:i=134:gtgl=5:slsql=off:gtg=exists_sym_2969 on theBenchmark for (2969ds/134Mi)
% 24.39/17.95 % (675612)Instruction limit reached!
% 24.39/17.95 % (675612)------------------------------
% 24.39/17.95 % (675612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.39/17.95 % (675612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.39/17.95 % (675612)CaDiCaL version: 2.1.3
% 24.39/17.95 % (675612)Termination reason: Instruction limit
% 24.39/17.95 % (675612)Termination phase: Property scanning
% 24.39/17.95 % (675612)Time elapsed: 0.051 s
% 24.39/17.95 % (675612)Peak memory usage: 103 MB
% 24.39/17.95 % (675612)Instructions burned: 134 (million)
% 24.39/17.95 % (675614)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1276174962:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/141Mi)
% 24.39/17.95 % (675614)Instruction limit reached!
% 24.39/17.95 % (675614)------------------------------
% 24.39/17.95 % (675614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.39/17.95 % (675614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.39/17.95 % (675614)CaDiCaL version: 2.1.3
% 24.39/17.95 % (675614)Termination reason: Instruction limit
% 24.39/17.95 % (675614)Termination phase: Saturation
% 24.39/17.95 % (675614)Time elapsed: 0.088 s
% 24.39/17.95 % (675614)Peak memory usage: 107 MB
% 24.39/17.95 % (675614)Instructions burned: 141 (million)
% 24.39/17.95 % (675616)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1515884571:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2967 on theBenchmark for (2967ds/431Mi)
% 24.39/17.95 % (675618)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=2888002170:i=6060:aac=none:ins=25_2966 on theBenchmark for (2966ds/6060Mi)
% 24.39/17.95 % (675616)Instruction limit reached!
% 24.39/17.95 % (675616)------------------------------
% 24.39/17.95 % (675616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.39/17.95 % (675616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.39/17.95 % (675616)CaDiCaL version: 2.1.3
% 24.39/17.95 % (675616)Termination reason: Instruction limit
% 24.39/17.95 % (675616)Termination phase: Saturation
% 24.39/17.95 % (675616)Time elapsed: 0.242 s
% 24.39/17.95 % (675616)Peak memory usage: 112 MB
% 24.39/17.95 % (675616)Instructions burned: 431 (million)
% 24.39/17.95 % (675621)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=2177320790:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2962 on theBenchmark for (2962ds/150Mi)
% 24.39/17.95 % (675621)Instruction limit reached!
% 24.39/17.95 % (675621)------------------------------
% 24.39/17.95 % (675621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.39/17.95 % (675621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.39/17.95 % (675621)CaDiCaL version: 2.1.3
% 24.39/17.95 % (675621)Termination reason: Instruction limit
% 24.39/17.95 % (675621)Termination phase: Preprocessing 1
% 24.39/17.95 % (675621)Time elapsed: 0.105 s
% 24.39/17.95 % (675621)Peak memory usage: 103 MB
% 24.39/17.95 % (675621)Instructions burned: 150 (million)
% 24.39/17.95 % (675623)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3777626640:i=14155:bd=all_2960 on theBenchmark for (2960ds/14155Mi)
% 24.39/17.95 % (675602)Instruction limit reached!
% 24.39/17.95 % (675602)------------------------------
% 24.39/17.95 % (675602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.39/17.95 % (675602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.39/17.95 % (675602)CaDiCaL version: 2.1.3
% 24.39/17.95 % (675602)Termination reason: Instruction limit
% 24.39/17.95 % (675602)Termination phase: Saturation
% 24.39/17.95 % (675602)Time elapsed: 3.462 s
% 24.39/17.95 % (675602)Peak memory usage: 386 MB
% 24.39/17.95 % (675602)Instructions burned: 5203 (million)
% 24.39/17.95 % (675626)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=4064203138:i=667:av=off:fsr=off_2942 on theBenchmark for (2942ds/667Mi)
% 24.39/17.95 % (675626)Instruction limit reached!
% 24.39/17.95 % (675626)------------------------------
% 24.39/17.95 % (675626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.39/17.95 % (675626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.39/17.95 % (675626)CaDiCaL version: 2.1.3
% 24.39/17.95 % (675626)Termination reason: Instruction limit
% 24.39/17.95 % (675626)Termination phase: NewCNF
% 24.39/17.95 % (675626)Time elapsed: 0.437 s
% 24.39/17.95 % (675626)Peak memory usage: 126 MB
% 24.39/17.95 % (675626)Instructions burned: 668 (million)
% 24.39/17.95 % (675628)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=161725725:s2a=on:i=185:s2at=1.8:fdi=4_2936 on theBenchmark for (2936ds/185Mi)
% 24.39/17.95 % (675608)First to succeed.
% 24.39/17.95 % (675608)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-675562"
% 24.39/17.95 % (675628)Instruction limit reached!
% 24.39/17.95 % (675628)------------------------------
% 24.39/17.95 % (675628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.39/17.95 % (675628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.39/17.95 % (675628)CaDiCaL version: 2.1.3
% 24.39/17.95 % (675628)Termination reason: Instruction limit
% 24.39/17.95 % (675628)Termination phase: Preprocessing 1
% 24.39/17.95 % (675628)Time elapsed: 0.130 s
% 24.39/17.95 % (675628)Peak memory usage: 102 MB
% 24.39/17.95 % (675628)Instructions burned: 186 (million)
% 24.39/17.95 % (675630)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=982433405:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2932 on theBenchmark for (2932ds/193Mi)
% 24.39/17.95 % (675608)Refutation found. Thanks to Tanya!
% 24.39/17.95 % SZS status Theorem for theBenchmark
% 24.39/17.95 % SZS output start Proof for theBenchmark
% See solution above
% 43.51/18.15 % (675608)------------------------------
% 43.51/18.15 % (675608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.51/18.15 % (675608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.51/18.15 % (675608)CaDiCaL version: 2.1.3
% 43.51/18.15 % (675608)Termination reason: Refutation
% 43.51/18.15 % (675608)Time elapsed: 3.853 s
% 43.51/18.15 % (675608)Peak memory usage: 205 MB
% 43.51/18.15 % (675608)Instructions burned: 6483 (million)
% 43.51/18.15 % (675608)------------------------------
% 43.51/18.15 % (675608)------------------------------
% 43.51/18.15 % (675562)Success in time 7.059 s
% 43.51/18.15 % Vampire exiting
%------------------------------------------------------------------------------