%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : COM145+1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n008.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 09:39:40 AM UTC 2026
% Result : Theorem 46.65s 12.63s
% Output : Refutation 86.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 61
% Syntax : Number of formulae : 563 ( 41 unt; 37 def)
% Number of atoms : 2058 ( 678 equ)
% Maximal formula atoms : 29 ( 3 avg)
% Number of connectives : 2601 (1106 ~;1189 |; 240 &)
% ( 31 <=>; 35 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 6 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 42 ( 40 usr; 32 prp; 0-3 aty)
% Number of functors : 53 ( 53 usr; 6 con; 0-3 aty)
% Number of variables : 881 ( 0 sgn 656 !; 225 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( vabs(X0,X1,X2) = vabs(X3,X4,X5)
=> ( X0 = X3
& X1 = X4
& X2 = X5 ) )
& ( ( X0 = X3
& X1 = X4
& X2 = X5 )
=> vabs(X0,X1,X2) = vabs(X3,X4,X5) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-abs') ).
fof(f3,axiom,
! [X0,X1,X2,X3] :
( ( vapp(X0,X1) = vapp(X2,X3)
=> ( X0 = X2
& X1 = X3 ) )
& ( ( X0 = X2
& X1 = X3 )
=> vapp(X0,X1) = vapp(X2,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-app') ).
fof(f4,axiom,
! [X0,X1,X2,X3] : vvar(X0) != vabs(X1,X2,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-var-abs') ).
fof(f5,axiom,
! [X0,X1,X2] : vvar(X0) != vapp(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-var-app') ).
fof(f6,axiom,
! [X0,X1,X2,X3,X4] : vabs(X0,X1,X2) != vapp(X3,X4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-abs-app') ).
fof(f7,axiom,
! [X0,X1,X2,X3] :
( X3 = vabs(X0,X1,X2)
=> visValue(X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',isValue0) ).
fof(f8,axiom,
! [X0,X1] :
( X1 = vvar(X0)
=> ~ visValue(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',isValue1) ).
fof(f9,axiom,
! [X0,X1,X2] :
( X2 = vapp(X0,X1)
=> ~ visValue(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',isValue2) ).
fof(f38,axiom,
! [X0] : vnoExp != vsomeExp(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-noExp-someExp') ).
fof(f39,axiom,
! [X0] :
( X0 = vnoExp
=> ~ visSomeExp(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',isSomeExp0) ).
fof(f41,axiom,
! [X0,X1,X2] :
( X0 = vsomeExp(X2)
=> ( X1 = vgetSomeExp(X0)
=> X1 = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',getSomeExp0) ).
fof(f42,axiom,
! [X0,X1,X2] :
( X1 = vvar(X0)
=> ( X2 = vreduce(X1)
=> X2 = vnoExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reduce0) ).
fof(f43,axiom,
! [X0,X1,X2,X3,X4] :
( X3 = vabs(X0,X1,X2)
=> ( X4 = vreduce(X3)
=> X4 = vnoExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reduce1) ).
fof(f44,axiom,
! [X0,X1,X2,X3,X4,X5,X6] :
( X1 = vapp(vabs(X3,X4,X5),X0)
=> ( ( X6 = vreduce(X0)
& visSomeExp(X6) )
=> ( X2 = vreduce(X1)
=> X2 = vsomeExp(vapp(vabs(X3,X4,X5),vgetSomeExp(X6))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reduce2) ).
fof(f45,axiom,
! [X0,X1,X2,X3,X4,X5,X6] :
( X2 = vapp(vabs(X4,X0,X6),X5)
=> ( ( X1 = vreduce(X5)
& ~ visSomeExp(X1)
& visValue(X5) )
=> ( X3 = vreduce(X2)
=> X3 = vsomeExp(vsubst(X4,X5,X6)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reduce3) ).
fof(f48,axiom,
! [X0,X1,X2,X3,X4] :
( ( X3 = vapp(X1,X0)
& ! [X5,X6,X7] : X1 != vabs(X5,X6,X7) )
=> ( ( X2 = vreduce(X1)
& ~ visSomeExp(X2) )
=> ( X4 = vreduce(X3)
=> X4 = vnoExp ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reduce6) ).
fof(f49,axiom,
! [X0,X1] :
( vreduce(X0) = X1
=> ( ? [X2] :
( X0 = vvar(X2)
& X1 = vnoExp )
| ? [X2,X3,X4] :
( X0 = vabs(X2,X3,X4)
& X1 = vnoExp )
| ? [X5,X2,X3,X6,X7] :
( X0 = vapp(vabs(X2,X3,X6),X5)
& X7 = vreduce(X5)
& visSomeExp(X7)
& X1 = vsomeExp(vapp(vabs(X2,X3,X6),vgetSomeExp(X7))) )
| ? [X3,X7,X2,X5,X6] :
( X0 = vapp(vabs(X2,X3,X6),X5)
& X7 = vreduce(X5)
& ~ visSomeExp(X7)
& visValue(X5)
& X1 = vsomeExp(vsubst(X2,X5,X6)) )
| ? [X2,X3,X6,X7,X5] :
( X0 = vapp(vabs(X2,X3,X6),X5)
& X7 = vreduce(X5)
& ~ visSomeExp(X7)
& ~ visValue(X5)
& X1 = vnoExp )
| ? [X6,X8,X5] :
( X0 = vapp(X6,X5)
& ! [X9,X10,X11] : X6 != vabs(X9,X10,X11)
& X8 = vreduce(X6)
& visSomeExp(X8)
& X1 = vsomeExp(vapp(vgetSomeExp(X8),X5)) )
| ? [X5,X6,X8] :
( X0 = vapp(X6,X5)
& ! [X9,X10,X11] : X6 != vabs(X9,X10,X11)
& X8 = vreduce(X6)
& ~ visSomeExp(X8)
& X1 = vnoExp ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduce-INV') ).
fof(f50,axiom,
! [X0,X1,X2,X3] :
( ( varrow(X0,X1) = varrow(X2,X3)
=> ( X0 = X2
& X1 = X3 ) )
& ( ( X0 = X2
& X1 = X3 )
=> varrow(X0,X1) = varrow(X2,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-arrow') ).
fof(f53,axiom,
! [X0,X1,X2,X3,X4] :
( ( vtcheck(X1,X2,varrow(X0,X4))
& vtcheck(X1,X3,X0) )
=> vtcheck(X1,vapp(X2,X3),X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','T-app') ).
fof(f54,axiom,
! [X0,X1,X2] :
( vtcheck(X2,X0,X1)
=> ( ? [X3] :
( X0 = vvar(X3)
& vlookup(X3,X2) = vsomeType(X1) )
| ? [X3,X4,X5,X6] :
( X0 = vabs(X3,X5,X4)
& X1 = varrow(X5,X6)
& vtcheck(vbind(X3,X5,X2),X4,X6) )
| ? [X7,X4,X8] :
( X0 = vapp(X7,X4)
& vtcheck(X2,X7,varrow(X8,X1))
& vtcheck(X2,X4,X8) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','T-inv') ).
fof(f56,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( vtcheck(X1,X3,X0)
& vtcheck(vbind(X2,X0,X1),X4,X5) )
=> vtcheck(X1,vsubst(X2,X3,X4),X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','T-subst') ).
fof(f59,axiom,
! [X0,X1,X2] :
( ( vreduce(ve1) = vsomeExp(X1)
& vtcheck(X0,ve1,X2) )
=> vtcheck(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','T-Preservation-T-app-IH1') ).
fof(f60,axiom,
! [X0,X1,X2] :
( ( vreduce(ve2) = vsomeExp(X1)
& vtcheck(X0,ve2,X2) )
=> vtcheck(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','T-Preservation-T-app-IH2') ).
fof(f61,conjecture,
! [X0,X1,X2] :
( ( vreduce(vapp(ve1,ve2)) = vsomeExp(X1)
& vtcheck(X0,vapp(ve1,ve2),X2) )
=> vtcheck(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','T-Preservation-T-app') ).
fof(f62,negated_conjecture,
~ ! [X0,X1,X2] :
( ( vreduce(vapp(ve1,ve2)) = vsomeExp(X1)
& vtcheck(X0,vapp(ve1,ve2),X2) )
=> vtcheck(X0,X1,X2) ),
inference(negated_conjecture,[status(cth)],[f61]) ).
fof(f68,plain,
! [X0,X1] :
( vreduce(X0) = X1
=> ( ? [X2] :
( X0 = vvar(X2)
& X1 = vnoExp )
| ? [X3,X4,X5] :
( vabs(X3,X4,X5) = X0
& X1 = vnoExp )
| ? [X6,X7,X8,X9,X10] :
( vapp(vabs(X7,X8,X9),X6) = X0
& vreduce(X6) = X10
& visSomeExp(X10)
& vsomeExp(vapp(vabs(X7,X8,X9),vgetSomeExp(X10))) = X1 )
| ? [X11,X12,X13,X14,X15] :
( vapp(vabs(X13,X11,X15),X14) = X0
& vreduce(X14) = X12
& ~ visSomeExp(X12)
& visValue(X14)
& vsomeExp(vsubst(X13,X14,X15)) = X1 )
| ? [X16,X17,X18,X19,X20] :
( vapp(vabs(X16,X17,X18),X20) = X0
& vreduce(X20) = X19
& ~ visSomeExp(X19)
& ~ visValue(X20)
& X1 = vnoExp )
| ? [X21,X22,X23] :
( vapp(X21,X23) = X0
& ! [X24,X25,X26] : vabs(X24,X25,X26) != X21
& vreduce(X21) = X22
& visSomeExp(X22)
& vsomeExp(vapp(vgetSomeExp(X22),X23)) = X1 )
| ? [X27,X28,X29] :
( vapp(X28,X27) = X0
& ! [X30,X31,X32] : vabs(X30,X31,X32) != X28
& vreduce(X28) = X29
& ~ visSomeExp(X29)
& X1 = vnoExp ) ) ),
inference(rectify,[],[f49]) ).
fof(f69,plain,
! [X0,X1,X2] :
( vtcheck(X2,X0,X1)
=> ( ? [X3] :
( X0 = vvar(X3)
& vlookup(X3,X2) = vsomeType(X1) )
| ? [X4,X5,X6,X7] :
( vabs(X4,X6,X5) = X0
& varrow(X6,X7) = X1
& vtcheck(vbind(X4,X6,X2),X5,X7) )
| ? [X8,X9,X10] :
( vapp(X8,X9) = X0
& vtcheck(X2,X8,varrow(X10,X1))
& vtcheck(X2,X9,X10) ) ) ),
inference(rectify,[],[f54]) ).
fof(f71,plain,
! [X0,X1,X2,X3,X4,X5] :
( ( ( X0 = X3
& X1 = X4
& X2 = X5 )
| vabs(X0,X1,X2) != vabs(X3,X4,X5) )
& ( vabs(X0,X1,X2) = vabs(X3,X4,X5)
| X0 != X3
| X1 != X4
| X2 != X5 ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f72,plain,
! [X0,X1,X2,X3,X4,X5] :
( ( ( X0 = X3
& X1 = X4
& X2 = X5 )
| vabs(X0,X1,X2) != vabs(X3,X4,X5) )
& ( vabs(X0,X1,X2) = vabs(X3,X4,X5)
| X0 != X3
| X1 != X4
| X2 != X5 ) ),
inference(flattening,[],[f71]) ).
fof(f73,plain,
! [X0,X1,X2,X3] :
( ( ( X0 = X2
& X1 = X3 )
| vapp(X0,X1) != vapp(X2,X3) )
& ( vapp(X0,X1) = vapp(X2,X3)
| X0 != X2
| X1 != X3 ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f74,plain,
! [X0,X1,X2,X3] :
( ( ( X0 = X2
& X1 = X3 )
| vapp(X0,X1) != vapp(X2,X3) )
& ( vapp(X0,X1) = vapp(X2,X3)
| X0 != X2
| X1 != X3 ) ),
inference(flattening,[],[f73]) ).
fof(f75,plain,
! [X0,X1,X2,X3] :
( visValue(X3)
| vabs(X0,X1,X2) != X3 ),
inference(ennf_transformation,[],[f7]) ).
fof(f76,plain,
! [X0,X1] :
( ~ visValue(X1)
| vvar(X0) != X1 ),
inference(ennf_transformation,[],[f8]) ).
fof(f77,plain,
! [X0,X1,X2] :
( ~ visValue(X2)
| vapp(X0,X1) != X2 ),
inference(ennf_transformation,[],[f9]) ).
fof(f119,plain,
! [X0] :
( ~ visSomeExp(X0)
| vnoExp != X0 ),
inference(ennf_transformation,[],[f39]) ).
fof(f121,plain,
! [X0,X1,X2] :
( X1 = X2
| vgetSomeExp(X0) != X1
| vsomeExp(X2) != X0 ),
inference(ennf_transformation,[],[f41]) ).
fof(f122,plain,
! [X0,X1,X2] :
( X1 = X2
| vgetSomeExp(X0) != X1
| vsomeExp(X2) != X0 ),
inference(flattening,[],[f121]) ).
fof(f123,plain,
! [X0,X1,X2] :
( X2 = vnoExp
| vreduce(X1) != X2
| vvar(X0) != X1 ),
inference(ennf_transformation,[],[f42]) ).
fof(f124,plain,
! [X0,X1,X2] :
( X2 = vnoExp
| vreduce(X1) != X2
| vvar(X0) != X1 ),
inference(flattening,[],[f123]) ).
fof(f125,plain,
! [X0,X1,X2,X3,X4] :
( X4 = vnoExp
| vreduce(X3) != X4
| vabs(X0,X1,X2) != X3 ),
inference(ennf_transformation,[],[f43]) ).
fof(f126,plain,
! [X0,X1,X2,X3,X4] :
( X4 = vnoExp
| vreduce(X3) != X4
| vabs(X0,X1,X2) != X3 ),
inference(flattening,[],[f125]) ).
fof(f127,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( X2 = vsomeExp(vapp(vabs(X3,X4,X5),vgetSomeExp(X6)))
| vreduce(X1) != X2
| vreduce(X0) != X6
| ~ visSomeExp(X6)
| vapp(vabs(X3,X4,X5),X0) != X1 ),
inference(ennf_transformation,[],[f44]) ).
fof(f128,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( X2 = vsomeExp(vapp(vabs(X3,X4,X5),vgetSomeExp(X6)))
| vreduce(X1) != X2
| vreduce(X0) != X6
| ~ visSomeExp(X6)
| vapp(vabs(X3,X4,X5),X0) != X1 ),
inference(flattening,[],[f127]) ).
fof(f129,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( X3 = vsomeExp(vsubst(X4,X5,X6))
| vreduce(X2) != X3
| vreduce(X5) != X1
| visSomeExp(X1)
| ~ visValue(X5)
| vapp(vabs(X4,X0,X6),X5) != X2 ),
inference(ennf_transformation,[],[f45]) ).
fof(f130,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( X3 = vsomeExp(vsubst(X4,X5,X6))
| vreduce(X2) != X3
| vreduce(X5) != X1
| visSomeExp(X1)
| ~ visValue(X5)
| vapp(vabs(X4,X0,X6),X5) != X2 ),
inference(flattening,[],[f129]) ).
fof(f135,plain,
! [X0,X1,X2,X3,X4] :
( X4 = vnoExp
| vreduce(X3) != X4
| vreduce(X1) != X2
| visSomeExp(X2)
| vapp(X1,X0) != X3
| ? [X5,X6,X7] : vabs(X5,X6,X7) = X1 ),
inference(ennf_transformation,[],[f48]) ).
fof(f136,plain,
! [X0,X1,X2,X3,X4] :
( X4 = vnoExp
| vreduce(X3) != X4
| vreduce(X1) != X2
| visSomeExp(X2)
| vapp(X1,X0) != X3
| ? [X5,X6,X7] : vabs(X5,X6,X7) = X1 ),
inference(flattening,[],[f135]) ).
fof(f137,plain,
! [X0,X1] :
( ? [X2] :
( X0 = vvar(X2)
& X1 = vnoExp )
| ? [X3,X4,X5] :
( vabs(X3,X4,X5) = X0
& X1 = vnoExp )
| ? [X6,X7,X8,X9,X10] :
( vapp(vabs(X7,X8,X9),X6) = X0
& vreduce(X6) = X10
& visSomeExp(X10)
& vsomeExp(vapp(vabs(X7,X8,X9),vgetSomeExp(X10))) = X1 )
| ? [X11,X12,X13,X14,X15] :
( vapp(vabs(X13,X11,X15),X14) = X0
& vreduce(X14) = X12
& ~ visSomeExp(X12)
& visValue(X14)
& vsomeExp(vsubst(X13,X14,X15)) = X1 )
| ? [X16,X17,X18,X19,X20] :
( vapp(vabs(X16,X17,X18),X20) = X0
& vreduce(X20) = X19
& ~ visSomeExp(X19)
& ~ visValue(X20)
& X1 = vnoExp )
| ? [X21,X22,X23] :
( vapp(X21,X23) = X0
& ! [X24,X25,X26] : vabs(X24,X25,X26) != X21
& vreduce(X21) = X22
& visSomeExp(X22)
& vsomeExp(vapp(vgetSomeExp(X22),X23)) = X1 )
| ? [X27,X28,X29] :
( vapp(X28,X27) = X0
& ! [X30,X31,X32] : vabs(X30,X31,X32) != X28
& vreduce(X28) = X29
& ~ visSomeExp(X29)
& X1 = vnoExp )
| vreduce(X0) != X1 ),
inference(ennf_transformation,[],[f68]) ).
fof(f138,plain,
! [X0,X1] :
( ? [X2] :
( X0 = vvar(X2)
& X1 = vnoExp )
| ? [X3,X4,X5] :
( vabs(X3,X4,X5) = X0
& X1 = vnoExp )
| ? [X6,X7,X8,X9,X10] :
( vapp(vabs(X7,X8,X9),X6) = X0
& vreduce(X6) = X10
& visSomeExp(X10)
& vsomeExp(vapp(vabs(X7,X8,X9),vgetSomeExp(X10))) = X1 )
| ? [X11,X12,X13,X14,X15] :
( vapp(vabs(X13,X11,X15),X14) = X0
& vreduce(X14) = X12
& ~ visSomeExp(X12)
& visValue(X14)
& vsomeExp(vsubst(X13,X14,X15)) = X1 )
| ? [X16,X17,X18,X19,X20] :
( vapp(vabs(X16,X17,X18),X20) = X0
& vreduce(X20) = X19
& ~ visSomeExp(X19)
& ~ visValue(X20)
& X1 = vnoExp )
| ? [X21,X22,X23] :
( vapp(X21,X23) = X0
& ! [X24,X25,X26] : vabs(X24,X25,X26) != X21
& vreduce(X21) = X22
& visSomeExp(X22)
& vsomeExp(vapp(vgetSomeExp(X22),X23)) = X1 )
| ? [X27,X28,X29] :
( vapp(X28,X27) = X0
& ! [X30,X31,X32] : vabs(X30,X31,X32) != X28
& vreduce(X28) = X29
& ~ visSomeExp(X29)
& X1 = vnoExp )
| vreduce(X0) != X1 ),
inference(flattening,[],[f137]) ).
fof(f139,plain,
! [X0,X1,X2,X3] :
( ( ( X0 = X2
& X1 = X3 )
| varrow(X0,X1) != varrow(X2,X3) )
& ( varrow(X0,X1) = varrow(X2,X3)
| X0 != X2
| X1 != X3 ) ),
inference(ennf_transformation,[],[f50]) ).
fof(f140,plain,
! [X0,X1,X2,X3] :
( ( ( X0 = X2
& X1 = X3 )
| varrow(X0,X1) != varrow(X2,X3) )
& ( varrow(X0,X1) = varrow(X2,X3)
| X0 != X2
| X1 != X3 ) ),
inference(flattening,[],[f139]) ).
fof(f143,plain,
! [X0,X1,X2,X3,X4] :
( vtcheck(X1,vapp(X2,X3),X4)
| ~ vtcheck(X1,X2,varrow(X0,X4))
| ~ vtcheck(X1,X3,X0) ),
inference(ennf_transformation,[],[f53]) ).
fof(f144,plain,
! [X0,X1,X2,X3,X4] :
( vtcheck(X1,vapp(X2,X3),X4)
| ~ vtcheck(X1,X2,varrow(X0,X4))
| ~ vtcheck(X1,X3,X0) ),
inference(flattening,[],[f143]) ).
fof(f145,plain,
! [X0,X1,X2] :
( ? [X3] :
( X0 = vvar(X3)
& vlookup(X3,X2) = vsomeType(X1) )
| ? [X4,X5,X6,X7] :
( vabs(X4,X6,X5) = X0
& varrow(X6,X7) = X1
& vtcheck(vbind(X4,X6,X2),X5,X7) )
| ? [X8,X9,X10] :
( vapp(X8,X9) = X0
& vtcheck(X2,X8,varrow(X10,X1))
& vtcheck(X2,X9,X10) )
| ~ vtcheck(X2,X0,X1) ),
inference(ennf_transformation,[],[f69]) ).
fof(f146,plain,
! [X0,X1,X2] :
( ? [X3] :
( X0 = vvar(X3)
& vlookup(X3,X2) = vsomeType(X1) )
| ? [X4,X5,X6,X7] :
( vabs(X4,X6,X5) = X0
& varrow(X6,X7) = X1
& vtcheck(vbind(X4,X6,X2),X5,X7) )
| ? [X8,X9,X10] :
( vapp(X8,X9) = X0
& vtcheck(X2,X8,varrow(X10,X1))
& vtcheck(X2,X9,X10) )
| ~ vtcheck(X2,X0,X1) ),
inference(flattening,[],[f145]) ).
fof(f149,plain,
! [X0,X1,X2,X3,X4,X5] :
( vtcheck(X1,vsubst(X2,X3,X4),X5)
| ~ vtcheck(X1,X3,X0)
| ~ vtcheck(vbind(X2,X0,X1),X4,X5) ),
inference(ennf_transformation,[],[f56]) ).
fof(f150,plain,
! [X0,X1,X2,X3,X4,X5] :
( vtcheck(X1,vsubst(X2,X3,X4),X5)
| ~ vtcheck(X1,X3,X0)
| ~ vtcheck(vbind(X2,X0,X1),X4,X5) ),
inference(flattening,[],[f149]) ).
fof(f155,plain,
! [X0,X1,X2] :
( vtcheck(X0,X1,X2)
| vsomeExp(X1) != vreduce(ve1)
| ~ vtcheck(X0,ve1,X2) ),
inference(ennf_transformation,[],[f59]) ).
fof(f156,plain,
! [X0,X1,X2] :
( vtcheck(X0,X1,X2)
| vsomeExp(X1) != vreduce(ve1)
| ~ vtcheck(X0,ve1,X2) ),
inference(flattening,[],[f155]) ).
fof(f157,plain,
! [X0,X1,X2] :
( vtcheck(X0,X1,X2)
| vsomeExp(X1) != vreduce(ve2)
| ~ vtcheck(X0,ve2,X2) ),
inference(ennf_transformation,[],[f60]) ).
fof(f158,plain,
! [X0,X1,X2] :
( vtcheck(X0,X1,X2)
| vsomeExp(X1) != vreduce(ve2)
| ~ vtcheck(X0,ve2,X2) ),
inference(flattening,[],[f157]) ).
fof(f159,plain,
? [X0,X1,X2] :
( ~ vtcheck(X0,X1,X2)
& vreduce(vapp(ve1,ve2)) = vsomeExp(X1)
& vtcheck(X0,vapp(ve1,ve2),X2) ),
inference(ennf_transformation,[],[f62]) ).
fof(f160,plain,
? [X0,X1,X2] :
( ~ vtcheck(X0,X1,X2)
& vreduce(vapp(ve1,ve2)) = vsomeExp(X1)
& vtcheck(X0,vapp(ve1,ve2),X2) ),
inference(flattening,[],[f159]) ).
fof(f170,definition,
! [X0,X1] :
( ? [X27,X28,X29] :
( vapp(X28,X27) = X0
& ! [X30,X31,X32] : vabs(X30,X31,X32) != X28
& vreduce(X28) = X29
& ~ visSomeExp(X29)
& X1 = vnoExp )
| ~ sP7(X0,X1) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f171,definition,
! [X0,X1] :
( ? [X21,X22,X23] :
( vapp(X21,X23) = X0
& ! [X24,X25,X26] : vabs(X24,X25,X26) != X21
& vreduce(X21) = X22
& visSomeExp(X22)
& vsomeExp(vapp(vgetSomeExp(X22),X23)) = X1 )
| ~ sP8(X0,X1) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f172,definition,
! [X0,X1] :
( ? [X16,X17,X18,X19,X20] :
( vapp(vabs(X16,X17,X18),X20) = X0
& vreduce(X20) = X19
& ~ visSomeExp(X19)
& ~ visValue(X20)
& X1 = vnoExp )
| ~ sP9(X0,X1) ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f173,definition,
! [X0,X1] :
( ? [X11,X12,X13,X14,X15] :
( vapp(vabs(X13,X11,X15),X14) = X0
& vreduce(X14) = X12
& ~ visSomeExp(X12)
& visValue(X14)
& vsomeExp(vsubst(X13,X14,X15)) = X1 )
| ~ sP10(X0,X1) ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f174,definition,
! [X0,X1] :
( ? [X6,X7,X8,X9,X10] :
( vapp(vabs(X7,X8,X9),X6) = X0
& vreduce(X6) = X10
& visSomeExp(X10)
& vsomeExp(vapp(vabs(X7,X8,X9),vgetSomeExp(X10))) = X1 )
| ~ sP11(X0,X1) ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f175,plain,
! [X0,X1] :
( ? [X2] :
( X0 = vvar(X2)
& X1 = vnoExp )
| ? [X3,X4,X5] :
( vabs(X3,X4,X5) = X0
& X1 = vnoExp )
| sP11(X0,X1)
| sP10(X0,X1)
| sP9(X0,X1)
| sP8(X0,X1)
| sP7(X0,X1)
| vreduce(X0) != X1 ),
inference(definition_folding,[],[f138,f174,f173,f172,f171,f170]) ).
fof(f176,definition,
! [X0,X1,X2] :
( ? [X8,X9,X10] :
( vapp(X8,X9) = X0
& vtcheck(X2,X8,varrow(X10,X1))
& vtcheck(X2,X9,X10) )
| ~ sP12(X0,X1,X2) ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f177,plain,
! [X0,X1,X2] :
( ? [X3] :
( X0 = vvar(X3)
& vlookup(X3,X2) = vsomeType(X1) )
| ? [X4,X5,X6,X7] :
( vabs(X4,X6,X5) = X0
& varrow(X6,X7) = X1
& vtcheck(vbind(X4,X6,X2),X5,X7) )
| sP12(X0,X1,X2)
| ~ vtcheck(X2,X0,X1) ),
inference(definition_folding,[],[f146,f176]) ).
fof(f202,plain,
! [X0,X1,X2,X3,X4] :
( X4 = vnoExp
| vreduce(X3) != X4
| vreduce(X1) != X2
| visSomeExp(X2)
| vapp(X1,X0) != X3
| vabs(sK51(X1),sK52(X1),sK53(X1)) = X1 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK51,sK52,sK53]),skolemize(X5,sK51(X1)),skolemize(X6,sK52(X1)),skolemize(X7,sK53(X1))],[f136]) ).
fof(f203,plain,
! [X0,X1] :
( ? [X6,X7,X8,X9,X10] :
( vapp(vabs(X7,X8,X9),X6) = X0
& vreduce(X6) = X10
& visSomeExp(X10)
& vsomeExp(vapp(vabs(X7,X8,X9),vgetSomeExp(X10))) = X1 )
| ~ sP11(X0,X1) ),
inference(nnf_transformation,[],[f174]) ).
fof(f204,plain,
! [X0,X1] :
( ? [X2,X3,X4,X5,X6] :
( vapp(vabs(X3,X4,X5),X2) = X0
& vreduce(X2) = X6
& visSomeExp(X6)
& vsomeExp(vapp(vabs(X3,X4,X5),vgetSomeExp(X6))) = X1 )
| ~ sP11(X0,X1) ),
inference(rectify,[],[f203]) ).
fof(f205,plain,
! [X0,X1] :
( ( vapp(vabs(sK55(X0,X1),sK56(X0,X1),sK57(X0,X1)),sK54(X0,X1)) = X0
& sK58(X0,X1) = vreduce(sK54(X0,X1))
& visSomeExp(sK58(X0,X1))
& vsomeExp(vapp(vabs(sK55(X0,X1),sK56(X0,X1),sK57(X0,X1)),vgetSomeExp(sK58(X0,X1)))) = X1 )
| ~ sP11(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK54,sK55,sK56,sK57,sK58]),skolemize(X2,sK54(X0,X1)),skolemize(X3,sK55(X0,X1)),skolemize(X4,sK56(X0,X1)),skolemize(X5,sK57(X0,X1)),skolemize(X6,sK58(X0,X1))],[f204]) ).
fof(f206,plain,
! [X0,X1] :
( ? [X11,X12,X13,X14,X15] :
( vapp(vabs(X13,X11,X15),X14) = X0
& vreduce(X14) = X12
& ~ visSomeExp(X12)
& visValue(X14)
& vsomeExp(vsubst(X13,X14,X15)) = X1 )
| ~ sP10(X0,X1) ),
inference(nnf_transformation,[],[f173]) ).
fof(f207,plain,
! [X0,X1] :
( ? [X2,X3,X4,X5,X6] :
( vapp(vabs(X4,X2,X6),X5) = X0
& vreduce(X5) = X3
& ~ visSomeExp(X3)
& visValue(X5)
& vsomeExp(vsubst(X4,X5,X6)) = X1 )
| ~ sP10(X0,X1) ),
inference(rectify,[],[f206]) ).
fof(f208,plain,
! [X0,X1] :
( ( vapp(vabs(sK61(X0,X1),sK59(X0,X1),sK63(X0,X1)),sK62(X0,X1)) = X0
& sK60(X0,X1) = vreduce(sK62(X0,X1))
& ~ visSomeExp(sK60(X0,X1))
& visValue(sK62(X0,X1))
& vsomeExp(vsubst(sK61(X0,X1),sK62(X0,X1),sK63(X0,X1))) = X1 )
| ~ sP10(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK59,sK60,sK61,sK62,sK63]),skolemize(X2,sK59(X0,X1)),skolemize(X3,sK60(X0,X1)),skolemize(X4,sK61(X0,X1)),skolemize(X5,sK62(X0,X1)),skolemize(X6,sK63(X0,X1))],[f207]) ).
fof(f209,plain,
! [X0,X1] :
( ? [X16,X17,X18,X19,X20] :
( vapp(vabs(X16,X17,X18),X20) = X0
& vreduce(X20) = X19
& ~ visSomeExp(X19)
& ~ visValue(X20)
& X1 = vnoExp )
| ~ sP9(X0,X1) ),
inference(nnf_transformation,[],[f172]) ).
fof(f210,plain,
! [X0,X1] :
( ? [X2,X3,X4,X5,X6] :
( vapp(vabs(X2,X3,X4),X6) = X0
& vreduce(X6) = X5
& ~ visSomeExp(X5)
& ~ visValue(X6)
& X1 = vnoExp )
| ~ sP9(X0,X1) ),
inference(rectify,[],[f209]) ).
fof(f211,plain,
! [X0,X1] :
( ( vapp(vabs(sK64(X0,X1),sK65(X0,X1),sK66(X0,X1)),sK68(X0,X1)) = X0
& sK67(X0,X1) = vreduce(sK68(X0,X1))
& ~ visSomeExp(sK67(X0,X1))
& ~ visValue(sK68(X0,X1))
& X1 = vnoExp )
| ~ sP9(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK64,sK65,sK66,sK67,sK68]),skolemize(X2,sK64(X0,X1)),skolemize(X3,sK65(X0,X1)),skolemize(X4,sK66(X0,X1)),skolemize(X5,sK67(X0,X1)),skolemize(X6,sK68(X0,X1))],[f210]) ).
fof(f212,plain,
! [X0,X1] :
( ? [X21,X22,X23] :
( vapp(X21,X23) = X0
& ! [X24,X25,X26] : vabs(X24,X25,X26) != X21
& vreduce(X21) = X22
& visSomeExp(X22)
& vsomeExp(vapp(vgetSomeExp(X22),X23)) = X1 )
| ~ sP8(X0,X1) ),
inference(nnf_transformation,[],[f171]) ).
fof(f213,plain,
! [X0,X1] :
( ? [X2,X3,X4] :
( vapp(X2,X4) = X0
& ! [X5,X6,X7] : vabs(X5,X6,X7) != X2
& vreduce(X2) = X3
& visSomeExp(X3)
& vsomeExp(vapp(vgetSomeExp(X3),X4)) = X1 )
| ~ sP8(X0,X1) ),
inference(rectify,[],[f212]) ).
fof(f214,plain,
! [X0,X1] :
( ( vapp(sK69(X0,X1),sK71(X0,X1)) = X0
& ! [X5,X6,X7] : vabs(X5,X6,X7) != sK69(X0,X1)
& sK70(X0,X1) = vreduce(sK69(X0,X1))
& visSomeExp(sK70(X0,X1))
& vsomeExp(vapp(vgetSomeExp(sK70(X0,X1)),sK71(X0,X1))) = X1 )
| ~ sP8(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK69,sK70,sK71]),skolemize(X2,sK69(X0,X1)),skolemize(X3,sK70(X0,X1)),skolemize(X4,sK71(X0,X1))],[f213]) ).
fof(f215,plain,
! [X0,X1] :
( ? [X27,X28,X29] :
( vapp(X28,X27) = X0
& ! [X30,X31,X32] : vabs(X30,X31,X32) != X28
& vreduce(X28) = X29
& ~ visSomeExp(X29)
& X1 = vnoExp )
| ~ sP7(X0,X1) ),
inference(nnf_transformation,[],[f170]) ).
fof(f216,plain,
! [X0,X1] :
( ? [X2,X3,X4] :
( vapp(X3,X2) = X0
& ! [X5,X6,X7] : vabs(X5,X6,X7) != X3
& vreduce(X3) = X4
& ~ visSomeExp(X4)
& X1 = vnoExp )
| ~ sP7(X0,X1) ),
inference(rectify,[],[f215]) ).
fof(f217,plain,
! [X0,X1] :
( ( vapp(sK73(X0,X1),sK72(X0,X1)) = X0
& ! [X5,X6,X7] : vabs(X5,X6,X7) != sK73(X0,X1)
& sK74(X0,X1) = vreduce(sK73(X0,X1))
& ~ visSomeExp(sK74(X0,X1))
& X1 = vnoExp )
| ~ sP7(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK72,sK73,sK74]),skolemize(X2,sK72(X0,X1)),skolemize(X3,sK73(X0,X1)),skolemize(X4,sK74(X0,X1))],[f216]) ).
fof(f218,plain,
! [X0,X1] :
( ( vvar(sK75(X0,X1)) = X0
& X1 = vnoExp )
| ( vabs(sK76(X0,X1),sK77(X0,X1),sK78(X0,X1)) = X0
& X1 = vnoExp )
| sP11(X0,X1)
| sP10(X0,X1)
| sP9(X0,X1)
| sP8(X0,X1)
| sP7(X0,X1)
| vreduce(X0) != X1 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK75,sK76,sK77,sK78]),skolemize(X2,sK75(X0,X1)),skolemize(X3,sK76(X0,X1)),skolemize(X4,sK77(X0,X1)),skolemize(X5,sK78(X0,X1))],[f175]) ).
fof(f219,plain,
! [X0,X1,X2] :
( ? [X8,X9,X10] :
( vapp(X8,X9) = X0
& vtcheck(X2,X8,varrow(X10,X1))
& vtcheck(X2,X9,X10) )
| ~ sP12(X0,X1,X2) ),
inference(nnf_transformation,[],[f176]) ).
fof(f220,plain,
! [X0,X1,X2] :
( ? [X3,X4,X5] :
( vapp(X3,X4) = X0
& vtcheck(X2,X3,varrow(X5,X1))
& vtcheck(X2,X4,X5) )
| ~ sP12(X0,X1,X2) ),
inference(rectify,[],[f219]) ).
fof(f221,plain,
! [X0,X1,X2] :
( ( vapp(sK79(X0,X1,X2),sK80(X0,X1,X2)) = X0
& vtcheck(X2,sK79(X0,X1,X2),varrow(sK81(X0,X1,X2),X1))
& vtcheck(X2,sK80(X0,X1,X2),sK81(X0,X1,X2)) )
| ~ sP12(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK79,sK80,sK81]),skolemize(X3,sK79(X0,X1,X2)),skolemize(X4,sK80(X0,X1,X2)),skolemize(X5,sK81(X0,X1,X2))],[f220]) ).
fof(f222,plain,
! [X0,X1,X2] :
( ( vvar(sK82(X0,X1,X2)) = X0
& vsomeType(X1) = vlookup(sK82(X0,X1,X2),X2) )
| ( vabs(sK83(X0,X1,X2),sK85(X0,X1,X2),sK84(X0,X1,X2)) = X0
& varrow(sK85(X0,X1,X2),sK86(X0,X1,X2)) = X1
& vtcheck(vbind(sK83(X0,X1,X2),sK85(X0,X1,X2),X2),sK84(X0,X1,X2),sK86(X0,X1,X2)) )
| sP12(X0,X1,X2)
| ~ vtcheck(X2,X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK82,sK83,sK84,sK85,sK86]),skolemize(X3,sK82(X0,X1,X2)),skolemize(X4,sK83(X0,X1,X2)),skolemize(X5,sK84(X0,X1,X2)),skolemize(X6,sK85(X0,X1,X2)),skolemize(X7,sK86(X0,X1,X2))],[f177]) ).
fof(f223,plain,
( ~ vtcheck(sK87,sK88,sK89)
& vreduce(vapp(ve1,ve2)) = vsomeExp(sK88)
& vtcheck(sK87,vapp(ve1,ve2),sK89) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK87,sK88,sK89]),skolemize(X0,sK87),skolemize(X1,sK88),skolemize(X2,sK89)],[f160]) ).
fof(f227,plain,
! [X2,X3,X0,X1,X4,X5] :
( X2 = X5
| vabs(X0,X1,X2) != vabs(X3,X4,X5) ),
inference(cnf_transformation,[],[f72]) ).
fof(f228,plain,
! [X2,X3,X0,X1,X4,X5] :
( X1 = X4
| vabs(X0,X1,X2) != vabs(X3,X4,X5) ),
inference(cnf_transformation,[],[f72]) ).
fof(f229,plain,
! [X2,X3,X0,X1,X4,X5] :
( X0 = X3
| vabs(X0,X1,X2) != vabs(X3,X4,X5) ),
inference(cnf_transformation,[],[f72]) ).
fof(f231,plain,
! [X2,X3,X0,X1] :
( X1 = X3
| vapp(X0,X1) != vapp(X2,X3) ),
inference(cnf_transformation,[],[f74]) ).
fof(f232,plain,
! [X2,X3,X0,X1] :
( X0 = X2
| vapp(X0,X1) != vapp(X2,X3) ),
inference(cnf_transformation,[],[f74]) ).
fof(f233,plain,
! [X2,X3,X0,X1] : vvar(X0) != vabs(X1,X2,X3),
inference(cnf_transformation,[],[f4]) ).
fof(f234,plain,
! [X2,X0,X1] : vvar(X0) != vapp(X1,X2),
inference(cnf_transformation,[],[f5]) ).
fof(f235,plain,
! [X2,X3,X0,X1,X4] : vabs(X0,X1,X2) != vapp(X3,X4),
inference(cnf_transformation,[],[f6]) ).
fof(f236,plain,
! [X2,X3,X0,X1] :
( visValue(X3)
| vabs(X0,X1,X2) != X3 ),
inference(cnf_transformation,[],[f75]) ).
fof(f237,plain,
! [X0,X1] :
( ~ visValue(X1)
| vvar(X0) != X1 ),
inference(cnf_transformation,[],[f76]) ).
fof(f238,plain,
! [X2,X0,X1] :
( ~ visValue(X2)
| vapp(X0,X1) != X2 ),
inference(cnf_transformation,[],[f77]) ).
fof(f318,plain,
! [X0] : vnoExp != vsomeExp(X0),
inference(cnf_transformation,[],[f38]) ).
fof(f319,plain,
! [X0] :
( ~ visSomeExp(X0)
| vnoExp != X0 ),
inference(cnf_transformation,[],[f119]) ).
fof(f321,plain,
! [X2,X0,X1] :
( X1 = X2
| vgetSomeExp(X0) != X1
| vsomeExp(X2) != X0 ),
inference(cnf_transformation,[],[f122]) ).
fof(f322,plain,
! [X2,X0,X1] :
( vnoExp = X2
| vreduce(X1) != X2
| vvar(X0) != X1 ),
inference(cnf_transformation,[],[f124]) ).
fof(f323,plain,
! [X2,X3,X0,X1,X4] :
( vnoExp = X4
| vreduce(X3) != X4
| vabs(X0,X1,X2) != X3 ),
inference(cnf_transformation,[],[f126]) ).
fof(f324,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( vsomeExp(vapp(vabs(X3,X4,X5),vgetSomeExp(X6))) = X2
| vreduce(X1) != X2
| vreduce(X0) != X6
| ~ visSomeExp(X6)
| vapp(vabs(X3,X4,X5),X0) != X1 ),
inference(cnf_transformation,[],[f128]) ).
fof(f325,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( vsomeExp(vsubst(X4,X5,X6)) = X3
| vreduce(X2) != X3
| vreduce(X5) != X1
| visSomeExp(X1)
| ~ visValue(X5)
| vapp(vabs(X4,X0,X6),X5) != X2 ),
inference(cnf_transformation,[],[f130]) ).
fof(f328,plain,
! [X2,X3,X0,X1,X4] :
( vnoExp = X4
| vreduce(X3) != X4
| vreduce(X1) != X2
| visSomeExp(X2)
| vapp(X1,X0) != X3
| vabs(sK51(X1),sK52(X1),sK53(X1)) = X1 ),
inference(cnf_transformation,[],[f202]) ).
fof(f329,plain,
! [X0,X1] :
( vsomeExp(vapp(vabs(sK55(X0,X1),sK56(X0,X1),sK57(X0,X1)),vgetSomeExp(sK58(X0,X1)))) = X1
| ~ sP11(X0,X1) ),
inference(cnf_transformation,[],[f205]) ).
fof(f330,plain,
! [X0,X1] :
( visSomeExp(sK58(X0,X1))
| ~ sP11(X0,X1) ),
inference(cnf_transformation,[],[f205]) ).
fof(f331,plain,
! [X0,X1] :
( sK58(X0,X1) = vreduce(sK54(X0,X1))
| ~ sP11(X0,X1) ),
inference(cnf_transformation,[],[f205]) ).
fof(f332,plain,
! [X0,X1] :
( vapp(vabs(sK55(X0,X1),sK56(X0,X1),sK57(X0,X1)),sK54(X0,X1)) = X0
| ~ sP11(X0,X1) ),
inference(cnf_transformation,[],[f205]) ).
fof(f333,plain,
! [X0,X1] :
( vsomeExp(vsubst(sK61(X0,X1),sK62(X0,X1),sK63(X0,X1))) = X1
| ~ sP10(X0,X1) ),
inference(cnf_transformation,[],[f208]) ).
fof(f334,plain,
! [X0,X1] :
( visValue(sK62(X0,X1))
| ~ sP10(X0,X1) ),
inference(cnf_transformation,[],[f208]) ).
fof(f337,plain,
! [X0,X1] :
( vapp(vabs(sK61(X0,X1),sK59(X0,X1),sK63(X0,X1)),sK62(X0,X1)) = X0
| ~ sP10(X0,X1) ),
inference(cnf_transformation,[],[f208]) ).
fof(f338,plain,
! [X0,X1] :
( vnoExp = X1
| ~ sP9(X0,X1) ),
inference(cnf_transformation,[],[f211]) ).
fof(f343,plain,
! [X0,X1] :
( vsomeExp(vapp(vgetSomeExp(sK70(X0,X1)),sK71(X0,X1))) = X1
| ~ sP8(X0,X1) ),
inference(cnf_transformation,[],[f214]) ).
fof(f345,plain,
! [X0,X1] :
( sK70(X0,X1) = vreduce(sK69(X0,X1))
| ~ sP8(X0,X1) ),
inference(cnf_transformation,[],[f214]) ).
fof(f346,plain,
! [X0,X1,X6,X7,X5] :
( vabs(X5,X6,X7) != sK69(X0,X1)
| ~ sP8(X0,X1) ),
inference(cnf_transformation,[],[f214]) ).
fof(f347,plain,
! [X0,X1] :
( vapp(sK69(X0,X1),sK71(X0,X1)) = X0
| ~ sP8(X0,X1) ),
inference(cnf_transformation,[],[f214]) ).
fof(f348,plain,
! [X0,X1] :
( vnoExp = X1
| ~ sP7(X0,X1) ),
inference(cnf_transformation,[],[f217]) ).
fof(f353,plain,
! [X0,X1] :
( vnoExp = X1
| vnoExp = X1
| sP11(X0,X1)
| sP10(X0,X1)
| sP9(X0,X1)
| sP8(X0,X1)
| sP7(X0,X1)
| vreduce(X0) != X1 ),
inference(cnf_transformation,[],[f218]) ).
fof(f355,plain,
! [X0,X1] :
( vvar(sK75(X0,X1)) = X0
| vnoExp = X1
| sP11(X0,X1)
| sP10(X0,X1)
| sP9(X0,X1)
| sP8(X0,X1)
| sP7(X0,X1)
| vreduce(X0) != X1 ),
inference(cnf_transformation,[],[f218]) ).
fof(f358,plain,
! [X2,X3,X0,X1] :
( X1 = X3
| varrow(X0,X1) != varrow(X2,X3) ),
inference(cnf_transformation,[],[f140]) ).
fof(f359,plain,
! [X2,X3,X0,X1] :
( X0 = X2
| varrow(X0,X1) != varrow(X2,X3) ),
inference(cnf_transformation,[],[f140]) ).
fof(f362,plain,
! [X2,X3,X0,X1,X4] :
( vtcheck(X1,vapp(X2,X3),X4)
| ~ vtcheck(X1,X2,varrow(X0,X4))
| ~ vtcheck(X1,X3,X0) ),
inference(cnf_transformation,[],[f144]) ).
fof(f363,plain,
! [X2,X0,X1] :
( vtcheck(X2,sK80(X0,X1,X2),sK81(X0,X1,X2))
| ~ sP12(X0,X1,X2) ),
inference(cnf_transformation,[],[f221]) ).
fof(f364,plain,
! [X2,X0,X1] :
( vtcheck(X2,sK79(X0,X1,X2),varrow(sK81(X0,X1,X2),X1))
| ~ sP12(X0,X1,X2) ),
inference(cnf_transformation,[],[f221]) ).
fof(f365,plain,
! [X2,X0,X1] :
( vapp(sK79(X0,X1,X2),sK80(X0,X1,X2)) = X0
| ~ sP12(X0,X1,X2) ),
inference(cnf_transformation,[],[f221]) ).
fof(f369,plain,
! [X2,X0,X1] :
( vvar(sK82(X0,X1,X2)) = X0
| vtcheck(vbind(sK83(X0,X1,X2),sK85(X0,X1,X2),X2),sK84(X0,X1,X2),sK86(X0,X1,X2))
| sP12(X0,X1,X2)
| ~ vtcheck(X2,X0,X1) ),
inference(cnf_transformation,[],[f222]) ).
fof(f370,plain,
! [X2,X0,X1] :
( vvar(sK82(X0,X1,X2)) = X0
| varrow(sK85(X0,X1,X2),sK86(X0,X1,X2)) = X1
| sP12(X0,X1,X2)
| ~ vtcheck(X2,X0,X1) ),
inference(cnf_transformation,[],[f222]) ).
fof(f371,plain,
! [X2,X0,X1] :
( vvar(sK82(X0,X1,X2)) = X0
| vabs(sK83(X0,X1,X2),sK85(X0,X1,X2),sK84(X0,X1,X2)) = X0
| sP12(X0,X1,X2)
| ~ vtcheck(X2,X0,X1) ),
inference(cnf_transformation,[],[f222]) ).
fof(f373,plain,
! [X2,X3,X0,X1,X4,X5] :
( vtcheck(X1,vsubst(X2,X3,X4),X5)
| ~ vtcheck(X1,X3,X0)
| ~ vtcheck(vbind(X2,X0,X1),X4,X5) ),
inference(cnf_transformation,[],[f150]) ).
fof(f376,plain,
! [X2,X0,X1] :
( vtcheck(X0,X1,X2)
| vsomeExp(X1) != vreduce(ve1)
| ~ vtcheck(X0,ve1,X2) ),
inference(cnf_transformation,[],[f156]) ).
fof(f377,plain,
! [X2,X0,X1] :
( vtcheck(X0,X1,X2)
| vsomeExp(X1) != vreduce(ve2)
| ~ vtcheck(X0,ve2,X2) ),
inference(cnf_transformation,[],[f158]) ).
fof(f378,plain,
vtcheck(sK87,vapp(ve1,ve2),sK89),
inference(cnf_transformation,[],[f223]) ).
fof(f379,plain,
vreduce(vapp(ve1,ve2)) = vsomeExp(sK88),
inference(cnf_transformation,[],[f223]) ).
fof(f380,plain,
~ vtcheck(sK87,sK88,sK89),
inference(cnf_transformation,[],[f223]) ).
fof(f387,plain,
! [X2,X0,X1] : visValue(vabs(X0,X1,X2)),
inference(equality_resolution,[],[f236]) ).
fof(f388,plain,
! [X0] : ~ visValue(vvar(X0)),
inference(equality_resolution,[],[f237]) ).
fof(f389,plain,
! [X0,X1] : ~ visValue(vapp(X0,X1)),
inference(equality_resolution,[],[f238]) ).
fof(f463,plain,
~ visSomeExp(vnoExp),
inference(equality_resolution,[],[f319]) ).
fof(f465,plain,
! [X2,X0] :
( vgetSomeExp(X0) = X2
| vsomeExp(X2) != X0 ),
inference(equality_resolution,[],[f321]) ).
fof(f466,plain,
! [X2] : vgetSomeExp(vsomeExp(X2)) = X2,
inference(equality_resolution,[],[f465]) ).
fof(f467,plain,
! [X0,X1] :
( vnoExp = vreduce(X1)
| vvar(X0) != X1 ),
inference(equality_resolution,[],[f322]) ).
fof(f468,plain,
! [X0] : vnoExp = vreduce(vvar(X0)),
inference(equality_resolution,[],[f467]) ).
fof(f469,plain,
! [X2,X3,X0,X1] :
( vnoExp = vreduce(X3)
| vabs(X0,X1,X2) != X3 ),
inference(equality_resolution,[],[f323]) ).
fof(f470,plain,
! [X2,X0,X1] : vnoExp = vreduce(vabs(X0,X1,X2)),
inference(equality_resolution,[],[f469]) ).
fof(f471,plain,
! [X3,X0,X1,X6,X4,X5] :
( vreduce(X1) = vsomeExp(vapp(vabs(X3,X4,X5),vgetSomeExp(X6)))
| vreduce(X0) != X6
| ~ visSomeExp(X6)
| vapp(vabs(X3,X4,X5),X0) != X1 ),
inference(equality_resolution,[],[f324]) ).
fof(f472,plain,
! [X3,X0,X1,X4,X5] :
( vreduce(X1) = vsomeExp(vapp(vabs(X3,X4,X5),vgetSomeExp(vreduce(X0))))
| ~ visSomeExp(vreduce(X0))
| vapp(vabs(X3,X4,X5),X0) != X1 ),
inference(equality_resolution,[],[f471]) ).
fof(f473,plain,
! [X3,X0,X4,X5] :
( vsomeExp(vapp(vabs(X3,X4,X5),vgetSomeExp(vreduce(X0)))) = vreduce(vapp(vabs(X3,X4,X5),X0))
| ~ visSomeExp(vreduce(X0)) ),
inference(equality_resolution,[],[f472]) ).
fof(f474,plain,
! [X2,X0,X1,X6,X4,X5] :
( vreduce(X2) = vsomeExp(vsubst(X4,X5,X6))
| vreduce(X5) != X1
| visSomeExp(X1)
| ~ visValue(X5)
| vapp(vabs(X4,X0,X6),X5) != X2 ),
inference(equality_resolution,[],[f325]) ).
fof(f475,plain,
! [X2,X0,X6,X4,X5] :
( vreduce(X2) = vsomeExp(vsubst(X4,X5,X6))
| visSomeExp(vreduce(X5))
| ~ visValue(X5)
| vapp(vabs(X4,X0,X6),X5) != X2 ),
inference(equality_resolution,[],[f474]) ).
fof(f476,plain,
! [X0,X6,X4,X5] :
( vsomeExp(vsubst(X4,X5,X6)) = vreduce(vapp(vabs(X4,X0,X6),X5))
| visSomeExp(vreduce(X5))
| ~ visValue(X5) ),
inference(equality_resolution,[],[f475]) ).
fof(f483,plain,
! [X2,X3,X0,X1] :
( vnoExp = vreduce(X3)
| vreduce(X1) != X2
| visSomeExp(X2)
| vapp(X1,X0) != X3
| vabs(sK51(X1),sK52(X1),sK53(X1)) = X1 ),
inference(equality_resolution,[],[f328]) ).
fof(f484,plain,
! [X3,X0,X1] :
( vnoExp = vreduce(X3)
| visSomeExp(vreduce(X1))
| vapp(X1,X0) != X3
| vabs(sK51(X1),sK52(X1),sK53(X1)) = X1 ),
inference(equality_resolution,[],[f483]) ).
fof(f485,plain,
! [X0,X1] :
( vnoExp = vreduce(vapp(X1,X0))
| visSomeExp(vreduce(X1))
| vabs(sK51(X1),sK52(X1),sK53(X1)) = X1 ),
inference(equality_resolution,[],[f484]) ).
fof(f487,plain,
! [X0] :
( vvar(sK75(X0,vreduce(X0))) = X0
| vnoExp = vreduce(X0)
| sP11(X0,vreduce(X0))
| sP10(X0,vreduce(X0))
| sP9(X0,vreduce(X0))
| sP8(X0,vreduce(X0))
| sP7(X0,vreduce(X0)) ),
inference(equality_resolution,[],[f355]) ).
fof(f489,plain,
! [X0] :
( vnoExp = vreduce(X0)
| vnoExp = vreduce(X0)
| sP11(X0,vreduce(X0))
| sP10(X0,vreduce(X0))
| sP9(X0,vreduce(X0))
| sP8(X0,vreduce(X0))
| sP7(X0,vreduce(X0)) ),
inference(equality_resolution,[],[f353]) ).
fof(f492,plain,
! [X0] :
( vnoExp = vreduce(X0)
| sP11(X0,vreduce(X0))
| sP10(X0,vreduce(X0))
| sP9(X0,vreduce(X0))
| sP8(X0,vreduce(X0))
| sP7(X0,vreduce(X0)) ),
inference(duplicate_literal_removal,[],[f489]) ).
fof(f493,plain,
( vnoExp = vsomeExp(sK88)
| visSomeExp(vreduce(ve1))
| ve1 = vabs(sK51(ve1),sK52(ve1),sK53(ve1)) ),
inference(superposition,[],[f379,f485]) ).
fof(f512,plain,
( vapp(ve1,ve2) = vvar(sK75(vapp(ve1,ve2),vsomeExp(sK88)))
| vnoExp = vsomeExp(sK88)
| sP11(vapp(ve1,ve2),vsomeExp(sK88))
| sP10(vapp(ve1,ve2),vsomeExp(sK88))
| sP9(vapp(ve1,ve2),vsomeExp(sK88))
| sP8(vapp(ve1,ve2),vsomeExp(sK88))
| sP7(vapp(ve1,ve2),vsomeExp(sK88)) ),
inference(superposition,[],[f487,f379]) ).
fof(f551,plain,
( vapp(ve1,ve2) = vvar(sK75(vapp(ve1,ve2),vsomeExp(sK88)))
| vnoExp = vsomeExp(sK88)
| sP11(vapp(ve1,ve2),vsomeExp(sK88))
| sP10(vapp(ve1,ve2),vsomeExp(sK88))
| sP8(vapp(ve1,ve2),vsomeExp(sK88))
| sP7(vapp(ve1,ve2),vsomeExp(sK88)) ),
inference(forward_subsumption_resolution,[],[f512,f338]) ).
fof(f567,plain,
( visSomeExp(vreduce(ve1))
| ve1 = vabs(sK51(ve1),sK52(ve1),sK53(ve1)) ),
inference(forward_subsumption_resolution,[],[f493,f318]) ).
fof(f587,plain,
( vapp(ve1,ve2) = vvar(sK75(vapp(ve1,ve2),vsomeExp(sK88)))
| vnoExp = vsomeExp(sK88)
| sP11(vapp(ve1,ve2),vsomeExp(sK88))
| sP10(vapp(ve1,ve2),vsomeExp(sK88))
| sP8(vapp(ve1,ve2),vsomeExp(sK88)) ),
inference(forward_subsumption_resolution,[],[f551,f348]) ).
fof(f600,definition,
( spl90_1
<=> ve1 = vabs(sK51(ve1),sK52(ve1),sK53(ve1)) ),
introduced(definition,[new_symbols(definition,[spl90_1])],[avatar_definition]) ).
fof(f601,plain,
( ve1 = vabs(sK51(ve1),sK52(ve1),sK53(ve1))
| ~ spl90_1 ),
inference(avatar_component_clause,[],[f600]) ).
fof(f603,definition,
( spl90_2
<=> visSomeExp(vreduce(ve1)) ),
introduced(definition,[new_symbols(definition,[spl90_2])],[avatar_definition]) ).
fof(f604,plain,
( visSomeExp(vreduce(ve1))
| ~ spl90_2 ),
inference(avatar_component_clause,[],[f603]) ).
fof(f609,plain,
( spl90_1
| spl90_2 ),
inference(avatar_split_clause,[],[f567,f603,f600]) ).
fof(f629,plain,
( vnoExp = vsomeExp(sK88)
| sP11(vapp(ve1,ve2),vsomeExp(sK88))
| sP10(vapp(ve1,ve2),vsomeExp(sK88))
| sP8(vapp(ve1,ve2),vsomeExp(sK88)) ),
inference(forward_subsumption_resolution,[],[f587,f234]) ).
fof(f631,definition,
( spl90_3
<=> sP8(vapp(ve1,ve2),vsomeExp(sK88)) ),
introduced(definition,[new_symbols(definition,[spl90_3])],[avatar_definition]) ).
fof(f632,plain,
( sP8(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_3 ),
inference(avatar_component_clause,[],[f631]) ).
fof(f637,definition,
( spl90_5
<=> sP10(vapp(ve1,ve2),vsomeExp(sK88)) ),
introduced(definition,[new_symbols(definition,[spl90_5])],[avatar_definition]) ).
fof(f638,plain,
( sP10(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_5 ),
inference(avatar_component_clause,[],[f637]) ).
fof(f640,definition,
( spl90_6
<=> sP11(vapp(ve1,ve2),vsomeExp(sK88)) ),
introduced(definition,[new_symbols(definition,[spl90_6])],[avatar_definition]) ).
fof(f641,plain,
( sP11(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_6 ),
inference(avatar_component_clause,[],[f640]) ).
fof(f676,plain,
( sP11(vapp(ve1,ve2),vsomeExp(sK88))
| sP10(vapp(ve1,ve2),vsomeExp(sK88))
| sP8(vapp(ve1,ve2),vsomeExp(sK88)) ),
inference(forward_subsumption_resolution,[],[f629,f318]) ).
fof(f693,plain,
( spl90_3
| spl90_5
| spl90_6 ),
inference(avatar_split_clause,[],[f676,f640,f637,f631]) ).
fof(f711,plain,
( vapp(ve1,ve2) = vvar(sK82(vapp(ve1,ve2),sK89,sK87))
| vapp(ve1,ve2) = vabs(sK83(vapp(ve1,ve2),sK89,sK87),sK85(vapp(ve1,ve2),sK89,sK87),sK84(vapp(ve1,ve2),sK89,sK87))
| sP12(vapp(ve1,ve2),sK89,sK87) ),
inference(resolution,[],[f378,f371]) ).
fof(f715,plain,
( vapp(ve1,ve2) = vabs(sK83(vapp(ve1,ve2),sK89,sK87),sK85(vapp(ve1,ve2),sK89,sK87),sK84(vapp(ve1,ve2),sK89,sK87))
| sP12(vapp(ve1,ve2),sK89,sK87) ),
inference(forward_subsumption_resolution,[],[f711,f234]) ).
fof(f720,definition,
( spl90_8
<=> sP12(vapp(ve1,ve2),sK89,sK87) ),
introduced(definition,[new_symbols(definition,[spl90_8])],[avatar_definition]) ).
fof(f721,plain,
( sP12(vapp(ve1,ve2),sK89,sK87)
| ~ spl90_8 ),
inference(avatar_component_clause,[],[f720]) ).
fof(f733,plain,
sP12(vapp(ve1,ve2),sK89,sK87),
inference(forward_subsumption_resolution,[],[f715,f235]) ).
fof(f737,plain,
spl90_8,
inference(avatar_split_clause,[],[f733,f720]) ).
fof(f755,plain,
( vtcheck(sK87,sK80(vapp(ve1,ve2),sK89,sK87),sK81(vapp(ve1,ve2),sK89,sK87))
| ~ spl90_8 ),
inference(resolution,[],[f721,f363]) ).
fof(f757,plain,
( vapp(ve1,ve2) = vapp(sK79(vapp(ve1,ve2),sK89,sK87),sK80(vapp(ve1,ve2),sK89,sK87))
| ~ spl90_8 ),
inference(resolution,[],[f721,f365]) ).
fof(f758,plain,
( ! [X0,X1] :
( ~ vtcheck(sK87,X0,varrow(sK81(vapp(ve1,ve2),sK89,sK87),X1))
| vtcheck(sK87,vapp(X0,sK80(vapp(ve1,ve2),sK89,sK87)),X1) )
| ~ spl90_8 ),
inference(resolution,[],[f755,f362]) ).
fof(f764,plain,
( sK80(vapp(ve1,ve2),sK89,sK87) = vvar(sK82(sK80(vapp(ve1,ve2),sK89,sK87),sK81(vapp(ve1,ve2),sK89,sK87),sK87))
| sK80(vapp(ve1,ve2),sK89,sK87) = vabs(sK83(sK80(vapp(ve1,ve2),sK89,sK87),sK81(vapp(ve1,ve2),sK89,sK87),sK87),sK85(sK80(vapp(ve1,ve2),sK89,sK87),sK81(vapp(ve1,ve2),sK89,sK87),sK87),sK84(sK80(vapp(ve1,ve2),sK89,sK87),sK81(vapp(ve1,ve2),sK89,sK87),sK87))
| sP12(sK80(vapp(ve1,ve2),sK89,sK87),sK81(vapp(ve1,ve2),sK89,sK87),sK87)
| ~ spl90_8 ),
inference(resolution,[],[f755,f371]) ).
fof(f769,definition,
( spl90_16
<=> sP12(sK80(vapp(ve1,ve2),sK89,sK87),sK81(vapp(ve1,ve2),sK89,sK87),sK87) ),
introduced(definition,[new_symbols(definition,[spl90_16])],[avatar_definition]) ).
fof(f770,plain,
( sP12(sK80(vapp(ve1,ve2),sK89,sK87),sK81(vapp(ve1,ve2),sK89,sK87),sK87)
| ~ spl90_16 ),
inference(avatar_component_clause,[],[f769]) ).
fof(f772,definition,
( spl90_17
<=> sK80(vapp(ve1,ve2),sK89,sK87) = vabs(sK83(sK80(vapp(ve1,ve2),sK89,sK87),sK81(vapp(ve1,ve2),sK89,sK87),sK87),sK85(sK80(vapp(ve1,ve2),sK89,sK87),sK81(vapp(ve1,ve2),sK89,sK87),sK87),sK84(sK80(vapp(ve1,ve2),sK89,sK87),sK81(vapp(ve1,ve2),sK89,sK87),sK87)) ),
introduced(definition,[new_symbols(definition,[spl90_17])],[avatar_definition]) ).
fof(f773,plain,
( sK80(vapp(ve1,ve2),sK89,sK87) = vabs(sK83(sK80(vapp(ve1,ve2),sK89,sK87),sK81(vapp(ve1,ve2),sK89,sK87),sK87),sK85(sK80(vapp(ve1,ve2),sK89,sK87),sK81(vapp(ve1,ve2),sK89,sK87),sK87),sK84(sK80(vapp(ve1,ve2),sK89,sK87),sK81(vapp(ve1,ve2),sK89,sK87),sK87))
| ~ spl90_17 ),
inference(avatar_component_clause,[],[f772]) ).
fof(f775,definition,
( spl90_18
<=> sK80(vapp(ve1,ve2),sK89,sK87) = vvar(sK82(sK80(vapp(ve1,ve2),sK89,sK87),sK81(vapp(ve1,ve2),sK89,sK87),sK87)) ),
introduced(definition,[new_symbols(definition,[spl90_18])],[avatar_definition]) ).
fof(f776,plain,
( sK80(vapp(ve1,ve2),sK89,sK87) = vvar(sK82(sK80(vapp(ve1,ve2),sK89,sK87),sK81(vapp(ve1,ve2),sK89,sK87),sK87))
| ~ spl90_18 ),
inference(avatar_component_clause,[],[f775]) ).
fof(f777,plain,
( spl90_16
| spl90_17
| spl90_18
| ~ spl90_8 ),
inference(avatar_split_clause,[],[f764,f720,f775,f772,f769]) ).
fof(f939,plain,
( ! [X0,X1] :
( vapp(X0,X1) != vapp(ve1,ve2)
| sK80(vapp(ve1,ve2),sK89,sK87) = X1 )
| ~ spl90_8 ),
inference(superposition,[],[f231,f757]) ).
fof(f941,plain,
( ! [X0,X1] :
( vapp(X0,X1) != vapp(ve1,ve2)
| sK79(vapp(ve1,ve2),sK89,sK87) = X0 )
| ~ spl90_8 ),
inference(superposition,[],[f232,f757]) ).
fof(f950,plain,
( vnoExp = vreduce(vapp(ve1,ve2))
| visSomeExp(vreduce(sK79(vapp(ve1,ve2),sK89,sK87)))
| sK79(vapp(ve1,ve2),sK89,sK87) = vabs(sK51(sK79(vapp(ve1,ve2),sK89,sK87)),sK52(sK79(vapp(ve1,ve2),sK89,sK87)),sK53(sK79(vapp(ve1,ve2),sK89,sK87)))
| ~ spl90_8 ),
inference(superposition,[],[f485,f757]) ).
fof(f951,plain,
( vnoExp = vsomeExp(sK88)
| visSomeExp(vreduce(sK79(vapp(ve1,ve2),sK89,sK87)))
| sK79(vapp(ve1,ve2),sK89,sK87) = vabs(sK51(sK79(vapp(ve1,ve2),sK89,sK87)),sK52(sK79(vapp(ve1,ve2),sK89,sK87)),sK53(sK79(vapp(ve1,ve2),sK89,sK87)))
| ~ spl90_8 ),
inference(forward_demodulation,[],[f950,f379]) ).
fof(f952,plain,
( visSomeExp(vreduce(sK79(vapp(ve1,ve2),sK89,sK87)))
| sK79(vapp(ve1,ve2),sK89,sK87) = vabs(sK51(sK79(vapp(ve1,ve2),sK89,sK87)),sK52(sK79(vapp(ve1,ve2),sK89,sK87)),sK53(sK79(vapp(ve1,ve2),sK89,sK87)))
| ~ spl90_8 ),
inference(forward_subsumption_resolution,[],[f951,f318]) ).
fof(f954,definition,
( spl90_22
<=> sK79(vapp(ve1,ve2),sK89,sK87) = vabs(sK51(sK79(vapp(ve1,ve2),sK89,sK87)),sK52(sK79(vapp(ve1,ve2),sK89,sK87)),sK53(sK79(vapp(ve1,ve2),sK89,sK87))) ),
introduced(definition,[new_symbols(definition,[spl90_22])],[avatar_definition]) ).
fof(f955,plain,
( sK79(vapp(ve1,ve2),sK89,sK87) = vabs(sK51(sK79(vapp(ve1,ve2),sK89,sK87)),sK52(sK79(vapp(ve1,ve2),sK89,sK87)),sK53(sK79(vapp(ve1,ve2),sK89,sK87)))
| ~ spl90_22 ),
inference(avatar_component_clause,[],[f954]) ).
fof(f957,definition,
( spl90_23
<=> visSomeExp(vreduce(sK79(vapp(ve1,ve2),sK89,sK87))) ),
introduced(definition,[new_symbols(definition,[spl90_23])],[avatar_definition]) ).
fof(f958,plain,
( visSomeExp(vreduce(sK79(vapp(ve1,ve2),sK89,sK87)))
| ~ spl90_23 ),
inference(avatar_component_clause,[],[f957]) ).
fof(f959,plain,
( spl90_22
| spl90_23
| ~ spl90_8 ),
inference(avatar_split_clause,[],[f952,f720,f957,f954]) ).
fof(f969,plain,
( ve2 = sK80(vapp(ve1,ve2),sK89,sK87)
| ~ spl90_8 ),
inference(equality_resolution,[],[f939]) ).
fof(f988,plain,
( ve1 = sK79(vapp(ve1,ve2),sK89,sK87)
| ~ spl90_8 ),
inference(equality_resolution,[],[f941]) ).
fof(f1000,plain,
( visSomeExp(vnoExp)
| sP11(ve1,vreduce(ve1))
| sP10(ve1,vreduce(ve1))
| sP9(ve1,vreduce(ve1))
| sP8(ve1,vreduce(ve1))
| sP7(ve1,vreduce(ve1))
| ~ spl90_2 ),
inference(superposition,[],[f604,f492]) ).
fof(f1005,plain,
( sP11(ve1,vreduce(ve1))
| sP10(ve1,vreduce(ve1))
| sP9(ve1,vreduce(ve1))
| sP8(ve1,vreduce(ve1))
| sP7(ve1,vreduce(ve1))
| ~ spl90_2 ),
inference(forward_subsumption_resolution,[],[f1000,f463]) ).
fof(f1014,definition,
( spl90_26
<=> sP7(ve1,vreduce(ve1)) ),
introduced(definition,[new_symbols(definition,[spl90_26])],[avatar_definition]) ).
fof(f1015,plain,
( sP7(ve1,vreduce(ve1))
| ~ spl90_26 ),
inference(avatar_component_clause,[],[f1014]) ).
fof(f1017,definition,
( spl90_27
<=> sP8(ve1,vreduce(ve1)) ),
introduced(definition,[new_symbols(definition,[spl90_27])],[avatar_definition]) ).
fof(f1018,plain,
( sP8(ve1,vreduce(ve1))
| ~ spl90_27 ),
inference(avatar_component_clause,[],[f1017]) ).
fof(f1020,definition,
( spl90_28
<=> sP9(ve1,vreduce(ve1)) ),
introduced(definition,[new_symbols(definition,[spl90_28])],[avatar_definition]) ).
fof(f1021,plain,
( sP9(ve1,vreduce(ve1))
| ~ spl90_28 ),
inference(avatar_component_clause,[],[f1020]) ).
fof(f1023,definition,
( spl90_29
<=> sP10(ve1,vreduce(ve1)) ),
introduced(definition,[new_symbols(definition,[spl90_29])],[avatar_definition]) ).
fof(f1024,plain,
( sP10(ve1,vreduce(ve1))
| ~ spl90_29 ),
inference(avatar_component_clause,[],[f1023]) ).
fof(f1026,definition,
( spl90_30
<=> sP11(ve1,vreduce(ve1)) ),
introduced(definition,[new_symbols(definition,[spl90_30])],[avatar_definition]) ).
fof(f1027,plain,
( sP11(ve1,vreduce(ve1))
| ~ spl90_30 ),
inference(avatar_component_clause,[],[f1026]) ).
fof(f1036,plain,
( spl90_26
| spl90_27
| spl90_28
| spl90_29
| spl90_30
| ~ spl90_2 ),
inference(avatar_split_clause,[],[f1005,f603,f1026,f1023,f1020,f1017,f1014]) ).
fof(f1045,plain,
( vtcheck(sK87,ve2,sK81(vapp(ve1,ve2),sK89,sK87))
| ~ spl90_8 ),
inference(superposition,[],[f755,f969]) ).
fof(f1050,plain,
( ! [X0] :
( vsomeExp(X0) != vreduce(ve2)
| vtcheck(sK87,X0,sK81(vapp(ve1,ve2),sK89,sK87)) )
| ~ spl90_8 ),
inference(resolution,[],[f1045,f377]) ).
fof(f1065,definition,
( spl90_35
<=> ve2 = vabs(sK83(ve2,sK81(vapp(ve1,ve2),sK89,sK87),sK87),sK85(ve2,sK81(vapp(ve1,ve2),sK89,sK87),sK87),sK84(ve2,sK81(vapp(ve1,ve2),sK89,sK87),sK87)) ),
introduced(definition,[new_symbols(definition,[spl90_35])],[avatar_definition]) ).
fof(f1066,plain,
( ve2 = vabs(sK83(ve2,sK81(vapp(ve1,ve2),sK89,sK87),sK87),sK85(ve2,sK81(vapp(ve1,ve2),sK89,sK87),sK87),sK84(ve2,sK81(vapp(ve1,ve2),sK89,sK87),sK87))
| ~ spl90_35 ),
inference(avatar_component_clause,[],[f1065]) ).
fof(f1068,definition,
( spl90_36
<=> ve2 = vvar(sK82(ve2,sK81(vapp(ve1,ve2),sK89,sK87),sK87)) ),
introduced(definition,[new_symbols(definition,[spl90_36])],[avatar_definition]) ).
fof(f1069,plain,
( ve2 = vvar(sK82(ve2,sK81(vapp(ve1,ve2),sK89,sK87),sK87))
| ~ spl90_36 ),
inference(avatar_component_clause,[],[f1068]) ).
fof(f1089,plain,
( vtcheck(sK87,ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89))
| ~ sP12(vapp(ve1,ve2),sK89,sK87)
| ~ spl90_8 ),
inference(superposition,[],[f364,f988]) ).
fof(f1092,plain,
( vtcheck(sK87,ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89))
| ~ spl90_8 ),
inference(forward_subsumption_resolution,[],[f1089,f721]) ).
fof(f1093,plain,
( ! [X0] :
( vsomeExp(X0) != vreduce(ve1)
| vtcheck(sK87,X0,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89)) )
| ~ spl90_8 ),
inference(resolution,[],[f1092,f376]) ).
fof(f1094,plain,
( ! [X0] :
( ~ vtcheck(sK87,X0,sK81(vapp(ve1,ve2),sK89,sK87))
| vtcheck(sK87,vapp(ve1,X0),sK89) )
| ~ spl90_8 ),
inference(resolution,[],[f1092,f362]) ).
fof(f1100,plain,
( ve1 = vvar(sK82(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87))
| varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89) = varrow(sK85(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),sK86(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87))
| sP12(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87)
| ~ spl90_8 ),
inference(resolution,[],[f1092,f370]) ).
fof(f1101,plain,
( ve1 = vvar(sK82(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87))
| ve1 = vabs(sK83(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),sK85(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),sK84(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87))
| sP12(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87)
| ~ spl90_8 ),
inference(resolution,[],[f1092,f371]) ).
fof(f1106,definition,
( spl90_40
<=> sP12(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87) ),
introduced(definition,[new_symbols(definition,[spl90_40])],[avatar_definition]) ).
fof(f1107,plain,
( sP12(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87)
| ~ spl90_40 ),
inference(avatar_component_clause,[],[f1106]) ).
fof(f1109,definition,
( spl90_41
<=> ve1 = vabs(sK83(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),sK85(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),sK84(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87)) ),
introduced(definition,[new_symbols(definition,[spl90_41])],[avatar_definition]) ).
fof(f1110,plain,
( ve1 = vabs(sK83(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),sK85(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),sK84(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87))
| ~ spl90_41 ),
inference(avatar_component_clause,[],[f1109]) ).
fof(f1112,definition,
( spl90_42
<=> ve1 = vvar(sK82(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87)) ),
introduced(definition,[new_symbols(definition,[spl90_42])],[avatar_definition]) ).
fof(f1113,plain,
( ve1 = vvar(sK82(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87))
| ~ spl90_42 ),
inference(avatar_component_clause,[],[f1112]) ).
fof(f1114,plain,
( spl90_40
| spl90_41
| spl90_42
| ~ spl90_8 ),
inference(avatar_split_clause,[],[f1101,f720,f1112,f1109,f1106]) ).
fof(f1116,definition,
( spl90_43
<=> varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89) = varrow(sK85(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),sK86(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87)) ),
introduced(definition,[new_symbols(definition,[spl90_43])],[avatar_definition]) ).
fof(f1117,plain,
( varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89) = varrow(sK85(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),sK86(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87))
| ~ spl90_43 ),
inference(avatar_component_clause,[],[f1116]) ).
fof(f1118,plain,
( spl90_40
| spl90_43
| spl90_42
| ~ spl90_8 ),
inference(avatar_split_clause,[],[f1100,f720,f1112,f1116,f1106]) ).
fof(f1235,plain,
( ve1 = vapp(sK79(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),sK80(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87))
| ~ spl90_40 ),
inference(resolution,[],[f1107,f365]) ).
fof(f1247,plain,
( sK80(vapp(ve1,ve2),sK89,sK87) = vapp(sK79(sK80(vapp(ve1,ve2),sK89,sK87),sK81(vapp(ve1,ve2),sK89,sK87),sK87),sK80(sK80(vapp(ve1,ve2),sK89,sK87),sK81(vapp(ve1,ve2),sK89,sK87),sK87))
| ~ spl90_16 ),
inference(resolution,[],[f770,f365]) ).
fof(f1248,plain,
( sP12(ve2,sK81(vapp(ve1,ve2),sK89,sK87),sK87)
| ~ spl90_8
| ~ spl90_16 ),
inference(superposition,[],[f770,f969]) ).
fof(f1249,plain,
( ve2 = vapp(sK79(ve2,sK81(vapp(ve1,ve2),sK89,sK87),sK87),sK80(ve2,sK81(vapp(ve1,ve2),sK89,sK87),sK87))
| ~ spl90_8
| ~ spl90_16 ),
inference(forward_demodulation,[],[f1247,f969]) ).
fof(f1259,plain,
( ~ visValue(ve2)
| ~ spl90_8
| ~ spl90_16 ),
inference(superposition,[],[f389,f1249]) ).
fof(f1276,definition,
( spl90_51
<=> vnoExp = vreduce(ve2) ),
introduced(definition,[new_symbols(definition,[spl90_51])],[avatar_definition]) ).
fof(f1277,plain,
( vnoExp = vreduce(ve2)
| ~ spl90_51 ),
inference(avatar_component_clause,[],[f1276]) ).
fof(f1279,plain,
( ve2 = vabs(sK83(ve2,sK81(vapp(ve1,ve2),sK89,sK87),sK87),sK85(ve2,sK81(vapp(ve1,ve2),sK89,sK87),sK87),sK84(ve2,sK81(vapp(ve1,ve2),sK89,sK87),sK87))
| ~ spl90_8
| ~ spl90_17 ),
inference(forward_demodulation,[],[f773,f969]) ).
fof(f1282,plain,
( spl90_35
| ~ spl90_8
| ~ spl90_17 ),
inference(avatar_split_clause,[],[f1279,f772,f720,f1065]) ).
fof(f1285,plain,
( ve2 = vvar(sK82(ve2,sK81(vapp(ve1,ve2),sK89,sK87),sK87))
| ~ spl90_8
| ~ spl90_18 ),
inference(forward_demodulation,[],[f776,f969]) ).
fof(f1287,plain,
( spl90_36
| ~ spl90_8
| ~ spl90_18 ),
inference(avatar_split_clause,[],[f1285,f775,f720,f1068]) ).
fof(f1297,plain,
( ~ visValue(ve2)
| ~ spl90_36 ),
inference(superposition,[],[f388,f1069]) ).
fof(f1303,plain,
( vnoExp = vreduce(ve2)
| ~ spl90_36 ),
inference(superposition,[],[f468,f1069]) ).
fof(f1304,plain,
( spl90_51
| ~ spl90_36 ),
inference(avatar_split_clause,[],[f1303,f1068,f1276]) ).
fof(f1665,plain,
( ! [X2,X0,X1] :
( vabs(X0,X1,X2) != sK79(vapp(ve1,ve2),sK89,sK87)
| sK53(sK79(vapp(ve1,ve2),sK89,sK87)) = X2 )
| ~ spl90_22 ),
inference(superposition,[],[f227,f955]) ).
fof(f1667,plain,
( ! [X2,X0,X1] :
( vabs(X0,X1,X2) != sK79(vapp(ve1,ve2),sK89,sK87)
| sK52(sK79(vapp(ve1,ve2),sK89,sK87)) = X1 )
| ~ spl90_22 ),
inference(superposition,[],[f228,f955]) ).
fof(f1669,plain,
( ! [X2,X0,X1] :
( vabs(X0,X1,X2) != sK79(vapp(ve1,ve2),sK89,sK87)
| sK51(sK79(vapp(ve1,ve2),sK89,sK87)) = X0 )
| ~ spl90_22 ),
inference(superposition,[],[f229,f955]) ).
fof(f1681,plain,
( ! [X0] :
( vsomeExp(vapp(sK79(vapp(ve1,ve2),sK89,sK87),vgetSomeExp(vreduce(X0)))) = vreduce(vapp(sK79(vapp(ve1,ve2),sK89,sK87),X0))
| ~ visSomeExp(vreduce(X0)) )
| ~ spl90_22 ),
inference(superposition,[],[f473,f955]) ).
fof(f1682,plain,
( ! [X0] :
( vreduce(vapp(sK79(vapp(ve1,ve2),sK89,sK87),X0)) = vsomeExp(vsubst(sK51(sK79(vapp(ve1,ve2),sK89,sK87)),X0,sK53(sK79(vapp(ve1,ve2),sK89,sK87))))
| visSomeExp(vreduce(X0))
| ~ visValue(X0) )
| ~ spl90_22 ),
inference(superposition,[],[f476,f955]) ).
fof(f1685,plain,
( ! [X0] :
( visSomeExp(vreduce(X0))
| vreduce(vapp(ve1,X0)) = vsomeExp(vsubst(sK51(ve1),X0,sK53(ve1)))
| ~ visValue(X0) )
| ~ spl90_8
| ~ spl90_22 ),
inference(forward_demodulation,[],[f1682,f988]) ).
fof(f1686,plain,
( ! [X0] :
( ~ visSomeExp(vreduce(X0))
| vreduce(vapp(ve1,X0)) = vsomeExp(vapp(ve1,vgetSomeExp(vreduce(X0)))) )
| ~ spl90_8
| ~ spl90_22 ),
inference(forward_demodulation,[],[f1681,f988]) ).
fof(f1698,plain,
( ! [X2,X0,X1] :
( vabs(X0,X1,X2) != ve1
| sK51(sK79(vapp(ve1,ve2),sK89,sK87)) = X0 )
| ~ spl90_8
| ~ spl90_22 ),
inference(forward_demodulation,[],[f1669,f988]) ).
fof(f1700,plain,
( ! [X2,X0,X1] :
( vabs(X0,X1,X2) != ve1
| sK52(sK79(vapp(ve1,ve2),sK89,sK87)) = X1 )
| ~ spl90_8
| ~ spl90_22 ),
inference(forward_demodulation,[],[f1667,f988]) ).
fof(f1702,plain,
( ! [X2,X0,X1] :
( vabs(X0,X1,X2) != ve1
| sK53(sK79(vapp(ve1,ve2),sK89,sK87)) = X2 )
| ~ spl90_8
| ~ spl90_22 ),
inference(forward_demodulation,[],[f1665,f988]) ).
fof(f1707,plain,
( ! [X2,X0,X1] :
( vabs(X0,X1,X2) != ve1
| sK51(ve1) = X0 )
| ~ spl90_8
| ~ spl90_22 ),
inference(forward_demodulation,[],[f1698,f988]) ).
fof(f1709,plain,
( ! [X2,X0,X1] :
( vabs(X0,X1,X2) != ve1
| sK52(ve1) = X1 )
| ~ spl90_8
| ~ spl90_22 ),
inference(forward_demodulation,[],[f1700,f988]) ).
fof(f1711,plain,
( ! [X2,X0,X1] :
( vabs(X0,X1,X2) != ve1
| sK53(ve1) = X2 )
| ~ spl90_8
| ~ spl90_22 ),
inference(forward_demodulation,[],[f1702,f988]) ).
fof(f1762,plain,
( visSomeExp(vreduce(ve1))
| ~ spl90_8
| ~ spl90_23 ),
inference(forward_demodulation,[],[f958,f988]) ).
fof(f1763,plain,
( spl90_2
| ~ spl90_8
| ~ spl90_23 ),
inference(avatar_split_clause,[],[f1762,f957,f720,f603]) ).
fof(f1935,plain,
( ! [X2,X0,X1] : vabs(X0,X1,X2) != ve1
| ~ spl90_40 ),
inference(superposition,[],[f235,f1235]) ).
fof(f1937,plain,
( ~ visValue(ve1)
| ~ spl90_40 ),
inference(superposition,[],[f389,f1235]) ).
fof(f1954,definition,
( spl90_77
<=> vnoExp = vreduce(ve1) ),
introduced(definition,[new_symbols(definition,[spl90_77])],[avatar_definition]) ).
fof(f1955,plain,
( vnoExp = vreduce(ve1)
| ~ spl90_77 ),
inference(avatar_component_clause,[],[f1954]) ).
fof(f1973,plain,
( vnoExp = vreduce(ve1)
| ~ spl90_41 ),
inference(superposition,[],[f470,f1110]) ).
fof(f1977,plain,
( spl90_77
| ~ spl90_41 ),
inference(avatar_split_clause,[],[f1973,f1109,f1954]) ).
fof(f1983,plain,
( ~ visValue(ve1)
| ~ spl90_42 ),
inference(superposition,[],[f388,f1113]) ).
fof(f1989,plain,
( vnoExp = vreduce(ve1)
| ~ spl90_42 ),
inference(superposition,[],[f468,f1113]) ).
fof(f1990,plain,
( spl90_77
| ~ spl90_42 ),
inference(avatar_split_clause,[],[f1989,f1112,f1954]) ).
fof(f2181,plain,
( vapp(ve1,ve2) = vapp(sK69(vapp(ve1,ve2),vsomeExp(sK88)),sK71(vapp(ve1,ve2),vsomeExp(sK88)))
| ~ spl90_3 ),
inference(resolution,[],[f632,f347]) ).
fof(f2299,plain,
( vapp(ve1,ve2) != vapp(ve1,ve2)
| sK79(vapp(ve1,ve2),sK89,sK87) = sK69(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_3
| ~ spl90_8 ),
inference(superposition,[],[f941,f2181]) ).
fof(f2300,plain,
( sK79(vapp(ve1,ve2),sK89,sK87) = sK69(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_3
| ~ spl90_8 ),
inference(trivial_inequality_removal,[],[f2299]) ).
fof(f2302,plain,
( ve1 = sK69(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_3
| ~ spl90_8 ),
inference(forward_demodulation,[],[f2300,f988]) ).
fof(f2311,plain,
( ! [X2,X0,X1] :
( vabs(X0,X1,X2) != ve1
| ~ sP8(vapp(ve1,ve2),vsomeExp(sK88)) )
| ~ spl90_3
| ~ spl90_8 ),
inference(superposition,[],[f346,f2302]) ).
fof(f2511,plain,
( ! [X0] : vvar(X0) != ve1
| ~ spl90_1 ),
inference(superposition,[],[f233,f601]) ).
fof(f2516,plain,
( visValue(ve1)
| ~ spl90_1 ),
inference(superposition,[],[f387,f601]) ).
fof(f2526,plain,
( $false
| ~ spl90_1
| ~ spl90_40 ),
inference(forward_subsumption_resolution,[],[f2516,f1937]) ).
fof(f2527,plain,
( ~ spl90_1
| ~ spl90_40 ),
inference(avatar_contradiction_clause,[],[f2526]) ).
fof(f2605,plain,
( visValue(ve2)
| ~ spl90_35 ),
inference(superposition,[],[f387,f1066]) ).
fof(f2610,plain,
( vnoExp = vreduce(ve2)
| ~ spl90_35 ),
inference(superposition,[],[f470,f1066]) ).
fof(f2614,plain,
( spl90_51
| ~ spl90_35 ),
inference(avatar_split_clause,[],[f2610,f1065,f1276]) ).
fof(f2734,plain,
( ! [X2,X0,X1] : vabs(X0,X1,X2) != ve1
| ~ spl90_3
| ~ spl90_8 ),
inference(forward_subsumption_resolution,[],[f2311,f632]) ).
fof(f2735,plain,
( visSomeExp(vnoExp)
| ~ spl90_2
| ~ spl90_77 ),
inference(superposition,[],[f604,f1955]) ).
fof(f2759,plain,
( $false
| ~ spl90_2
| ~ spl90_77 ),
inference(forward_subsumption_resolution,[],[f2735,f463]) ).
fof(f2760,plain,
( ~ spl90_2
| ~ spl90_77 ),
inference(avatar_contradiction_clause,[],[f2759]) ).
fof(f2777,plain,
( $false
| ~ spl90_1
| ~ spl90_3
| ~ spl90_8 ),
inference(forward_subsumption_resolution,[],[f601,f2734]) ).
fof(f2778,plain,
( ~ spl90_1
| ~ spl90_3
| ~ spl90_8 ),
inference(avatar_contradiction_clause,[],[f2777]) ).
fof(f3038,plain,
( sK58(vapp(ve1,ve2),vsomeExp(sK88)) = vreduce(sK54(vapp(ve1,ve2),vsomeExp(sK88)))
| ~ spl90_6 ),
inference(resolution,[],[f641,f331]) ).
fof(f3039,plain,
( vapp(ve1,ve2) = vapp(vabs(sK55(vapp(ve1,ve2),vsomeExp(sK88)),sK56(vapp(ve1,ve2),vsomeExp(sK88)),sK57(vapp(ve1,ve2),vsomeExp(sK88))),sK54(vapp(ve1,ve2),vsomeExp(sK88)))
| ~ spl90_6 ),
inference(resolution,[],[f641,f332]) ).
fof(f3228,plain,
( vapp(ve1,ve2) != vapp(ve1,ve2)
| sK80(vapp(ve1,ve2),sK89,sK87) = sK54(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_6
| ~ spl90_8 ),
inference(superposition,[],[f939,f3039]) ).
fof(f3229,plain,
( vapp(ve1,ve2) != vapp(ve1,ve2)
| sK79(vapp(ve1,ve2),sK89,sK87) = vabs(sK55(vapp(ve1,ve2),vsomeExp(sK88)),sK56(vapp(ve1,ve2),vsomeExp(sK88)),sK57(vapp(ve1,ve2),vsomeExp(sK88)))
| ~ spl90_6
| ~ spl90_8 ),
inference(superposition,[],[f941,f3039]) ).
fof(f3231,plain,
( sK79(vapp(ve1,ve2),sK89,sK87) = vabs(sK55(vapp(ve1,ve2),vsomeExp(sK88)),sK56(vapp(ve1,ve2),vsomeExp(sK88)),sK57(vapp(ve1,ve2),vsomeExp(sK88)))
| ~ spl90_6
| ~ spl90_8 ),
inference(trivial_inequality_removal,[],[f3229]) ).
fof(f3232,plain,
( sK80(vapp(ve1,ve2),sK89,sK87) = sK54(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_6
| ~ spl90_8 ),
inference(trivial_inequality_removal,[],[f3228]) ).
fof(f3233,plain,
( ve1 = vabs(sK55(vapp(ve1,ve2),vsomeExp(sK88)),sK56(vapp(ve1,ve2),vsomeExp(sK88)),sK57(vapp(ve1,ve2),vsomeExp(sK88)))
| ~ spl90_6
| ~ spl90_8 ),
inference(forward_demodulation,[],[f3231,f988]) ).
fof(f3234,plain,
( ve2 = sK54(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_6
| ~ spl90_8 ),
inference(forward_demodulation,[],[f3232,f969]) ).
fof(f3247,plain,
( vreduce(ve2) = sK58(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_6
| ~ spl90_8 ),
inference(superposition,[],[f3038,f3234]) ).
fof(f3254,plain,
( visSomeExp(vreduce(ve2))
| ~ sP11(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_6
| ~ spl90_8 ),
inference(superposition,[],[f330,f3247]) ).
fof(f3255,plain,
( visSomeExp(vreduce(ve2))
| ~ spl90_6
| ~ spl90_8 ),
inference(forward_subsumption_resolution,[],[f3254,f641]) ).
fof(f3279,plain,
( vnoExp = vreduce(ve1)
| ~ spl90_6
| ~ spl90_8 ),
inference(superposition,[],[f470,f3233]) ).
fof(f3289,plain,
( visSomeExp(vnoExp)
| sP11(ve2,vreduce(ve2))
| sP10(ve2,vreduce(ve2))
| sP9(ve2,vreduce(ve2))
| sP8(ve2,vreduce(ve2))
| sP7(ve2,vreduce(ve2))
| ~ spl90_6
| ~ spl90_8 ),
inference(superposition,[],[f3255,f492]) ).
fof(f3294,plain,
( sP11(ve2,vreduce(ve2))
| sP10(ve2,vreduce(ve2))
| sP9(ve2,vreduce(ve2))
| sP8(ve2,vreduce(ve2))
| sP7(ve2,vreduce(ve2))
| ~ spl90_6
| ~ spl90_8 ),
inference(forward_subsumption_resolution,[],[f3289,f463]) ).
fof(f3299,definition,
( spl90_108
<=> sP7(ve2,vreduce(ve2)) ),
introduced(definition,[new_symbols(definition,[spl90_108])],[avatar_definition]) ).
fof(f3300,plain,
( sP7(ve2,vreduce(ve2))
| ~ spl90_108 ),
inference(avatar_component_clause,[],[f3299]) ).
fof(f3302,definition,
( spl90_109
<=> sP8(ve2,vreduce(ve2)) ),
introduced(definition,[new_symbols(definition,[spl90_109])],[avatar_definition]) ).
fof(f3303,plain,
( sP8(ve2,vreduce(ve2))
| ~ spl90_109 ),
inference(avatar_component_clause,[],[f3302]) ).
fof(f3305,definition,
( spl90_110
<=> sP9(ve2,vreduce(ve2)) ),
introduced(definition,[new_symbols(definition,[spl90_110])],[avatar_definition]) ).
fof(f3306,plain,
( sP9(ve2,vreduce(ve2))
| ~ spl90_110 ),
inference(avatar_component_clause,[],[f3305]) ).
fof(f3308,definition,
( spl90_111
<=> sP10(ve2,vreduce(ve2)) ),
introduced(definition,[new_symbols(definition,[spl90_111])],[avatar_definition]) ).
fof(f3309,plain,
( sP10(ve2,vreduce(ve2))
| ~ spl90_111 ),
inference(avatar_component_clause,[],[f3308]) ).
fof(f3311,definition,
( spl90_112
<=> sP11(ve2,vreduce(ve2)) ),
introduced(definition,[new_symbols(definition,[spl90_112])],[avatar_definition]) ).
fof(f3312,plain,
( sP11(ve2,vreduce(ve2))
| ~ spl90_112 ),
inference(avatar_component_clause,[],[f3311]) ).
fof(f3313,plain,
( spl90_108
| spl90_109
| spl90_110
| spl90_111
| spl90_112
| ~ spl90_6
| ~ spl90_8 ),
inference(avatar_split_clause,[],[f3294,f720,f640,f3311,f3308,f3305,f3302,f3299]) ).
fof(f3846,plain,
( visSomeExp(vnoExp)
| ~ spl90_6
| ~ spl90_8
| ~ spl90_51 ),
inference(superposition,[],[f3255,f1277]) ).
fof(f3866,plain,
( visSomeExp(vnoExp)
| vreduce(vapp(ve1,ve2)) = vsomeExp(vsubst(sK51(ve1),ve2,sK53(ve1)))
| ~ visValue(ve2)
| ~ spl90_8
| ~ spl90_22
| ~ spl90_51 ),
inference(superposition,[],[f1685,f1277]) ).
fof(f3867,plain,
( vreduce(vapp(ve1,ve2)) = vsomeExp(vsubst(sK51(ve1),ve2,sK53(ve1)))
| ~ visValue(ve2)
| ~ spl90_8
| ~ spl90_22
| ~ spl90_51 ),
inference(forward_subsumption_resolution,[],[f3866,f463]) ).
fof(f3877,plain,
( $false
| ~ spl90_6
| ~ spl90_8
| ~ spl90_51 ),
inference(forward_subsumption_resolution,[],[f3846,f463]) ).
fof(f3878,plain,
( ~ spl90_6
| ~ spl90_8
| ~ spl90_51 ),
inference(avatar_contradiction_clause,[],[f3877]) ).
fof(f3879,plain,
( vreduce(vapp(ve1,ve2)) = vsomeExp(vsubst(sK51(ve1),ve2,sK53(ve1)))
| ~ spl90_8
| ~ spl90_22
| ~ spl90_35
| ~ spl90_51 ),
inference(forward_subsumption_resolution,[],[f3867,f2605]) ).
fof(f3913,plain,
( vsomeExp(sK88) = vsomeExp(vsubst(sK51(ve1),ve2,sK53(ve1)))
| ~ spl90_8
| ~ spl90_22
| ~ spl90_35
| ~ spl90_51 ),
inference(forward_demodulation,[],[f3879,f379]) ).
fof(f3920,plain,
( vgetSomeExp(vsomeExp(sK88)) = vsubst(sK51(ve1),ve2,sK53(ve1))
| ~ spl90_8
| ~ spl90_22
| ~ spl90_35
| ~ spl90_51 ),
inference(superposition,[],[f466,f3913]) ).
fof(f3923,plain,
( sK88 = vsubst(sK51(ve1),ve2,sK53(ve1))
| ~ spl90_8
| ~ spl90_22
| ~ spl90_35
| ~ spl90_51 ),
inference(forward_demodulation,[],[f3920,f466]) ).
fof(f3924,plain,
( ! [X2,X0,X1] :
( ~ vtcheck(vbind(sK51(ve1),X2,X0),sK53(ve1),X1)
| ~ vtcheck(X0,ve2,X2)
| vtcheck(X0,sK88,X1) )
| ~ spl90_8
| ~ spl90_22
| ~ spl90_35
| ~ spl90_51 ),
inference(superposition,[],[f373,f3923]) ).
fof(f4013,plain,
( vapp(ve1,ve2) = vapp(vabs(sK61(vapp(ve1,ve2),vsomeExp(sK88)),sK59(vapp(ve1,ve2),vsomeExp(sK88)),sK63(vapp(ve1,ve2),vsomeExp(sK88))),sK62(vapp(ve1,ve2),vsomeExp(sK88)))
| ~ spl90_5 ),
inference(resolution,[],[f638,f337]) ).
fof(f4469,plain,
( vapp(ve1,ve2) != vapp(ve1,ve2)
| sK80(vapp(ve1,ve2),sK89,sK87) = sK62(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_5
| ~ spl90_8 ),
inference(superposition,[],[f939,f4013]) ).
fof(f4473,plain,
( sK80(vapp(ve1,ve2),sK89,sK87) = sK62(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_5
| ~ spl90_8 ),
inference(trivial_inequality_removal,[],[f4469]) ).
fof(f4475,plain,
( ve2 = sK62(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_5
| ~ spl90_8 ),
inference(forward_demodulation,[],[f4473,f969]) ).
fof(f4483,plain,
( visValue(ve2)
| ~ sP10(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_5
| ~ spl90_8 ),
inference(superposition,[],[f334,f4475]) ).
fof(f4488,plain,
( ~ sP10(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_5
| ~ spl90_8
| ~ spl90_16 ),
inference(forward_subsumption_resolution,[],[f4483,f1259]) ).
fof(f4492,plain,
( $false
| ~ spl90_5
| ~ spl90_8
| ~ spl90_16 ),
inference(forward_subsumption_resolution,[],[f4488,f638]) ).
fof(f4493,plain,
( ~ spl90_5
| ~ spl90_8
| ~ spl90_16 ),
inference(avatar_contradiction_clause,[],[f4492]) ).
fof(f4501,plain,
( vsomeExp(sK88) = vsomeExp(vapp(vgetSomeExp(sK70(vapp(ve1,ve2),vsomeExp(sK88))),sK71(vapp(ve1,ve2),vsomeExp(sK88))))
| ~ spl90_3 ),
inference(resolution,[],[f632,f343]) ).
fof(f4503,plain,
( sK70(vapp(ve1,ve2),vsomeExp(sK88)) = vreduce(sK69(vapp(ve1,ve2),vsomeExp(sK88)))
| ~ spl90_3 ),
inference(resolution,[],[f632,f345]) ).
fof(f4505,plain,
( vapp(ve1,ve2) = vapp(sK69(vapp(ve1,ve2),vsomeExp(sK88)),sK71(vapp(ve1,ve2),vsomeExp(sK88)))
| ~ spl90_3 ),
inference(resolution,[],[f632,f347]) ).
fof(f4515,plain,
( vgetSomeExp(vsomeExp(sK88)) = vapp(vgetSomeExp(sK70(vapp(ve1,ve2),vsomeExp(sK88))),sK71(vapp(ve1,ve2),vsomeExp(sK88)))
| ~ spl90_3 ),
inference(superposition,[],[f466,f4501]) ).
fof(f4518,plain,
( sK88 = vapp(vgetSomeExp(sK70(vapp(ve1,ve2),vsomeExp(sK88))),sK71(vapp(ve1,ve2),vsomeExp(sK88)))
| ~ spl90_3 ),
inference(forward_demodulation,[],[f4515,f466]) ).
fof(f4626,plain,
( vapp(ve1,ve2) != vapp(ve1,ve2)
| sK80(vapp(ve1,ve2),sK89,sK87) = sK71(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_3
| ~ spl90_8 ),
inference(superposition,[],[f939,f4505]) ).
fof(f4627,plain,
( vapp(ve1,ve2) != vapp(ve1,ve2)
| sK79(vapp(ve1,ve2),sK89,sK87) = sK69(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_3
| ~ spl90_8 ),
inference(superposition,[],[f941,f4505]) ).
fof(f4628,plain,
( sK79(vapp(ve1,ve2),sK89,sK87) = sK69(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_3
| ~ spl90_8 ),
inference(trivial_inequality_removal,[],[f4627]) ).
fof(f4629,plain,
( sK80(vapp(ve1,ve2),sK89,sK87) = sK71(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_3
| ~ spl90_8 ),
inference(trivial_inequality_removal,[],[f4626]) ).
fof(f4630,plain,
( ve1 = sK69(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_3
| ~ spl90_8 ),
inference(forward_demodulation,[],[f4628,f988]) ).
fof(f4631,plain,
( ve2 = sK71(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_3
| ~ spl90_8 ),
inference(forward_demodulation,[],[f4629,f969]) ).
fof(f4637,plain,
( vreduce(ve1) = sK70(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_3
| ~ spl90_8 ),
inference(superposition,[],[f4503,f4630]) ).
fof(f5168,plain,
( vnoExp = vreduce(ve2)
| ~ spl90_110 ),
inference(resolution,[],[f3306,f338]) ).
fof(f5262,plain,
( ! [X0,X1] :
( varrow(X0,X1) != varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89)
| sK86(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87) = X1 )
| ~ spl90_43 ),
inference(superposition,[],[f358,f1117]) ).
fof(f5339,plain,
( sK88 = vapp(vgetSomeExp(sK70(vapp(ve1,ve2),vsomeExp(sK88))),ve2)
| ~ spl90_3
| ~ spl90_8 ),
inference(superposition,[],[f4518,f4631]) ).
fof(f5378,plain,
( sK88 = vapp(vgetSomeExp(vreduce(ve1)),ve2)
| ~ spl90_3
| ~ spl90_8 ),
inference(forward_demodulation,[],[f5339,f4637]) ).
fof(f5555,plain,
( vnoExp = vreduce(ve1)
| ~ spl90_26 ),
inference(resolution,[],[f1015,f348]) ).
fof(f5563,plain,
( spl90_77
| ~ spl90_26 ),
inference(avatar_split_clause,[],[f5555,f1014,f1954]) ).
fof(f5564,plain,
( vnoExp = vreduce(ve1)
| ~ spl90_28 ),
inference(resolution,[],[f1021,f338]) ).
fof(f5572,plain,
( spl90_77
| ~ spl90_28 ),
inference(avatar_split_clause,[],[f5564,f1020,f1954]) ).
fof(f6562,plain,
( vreduce(ve1) = vsomeExp(vsubst(sK61(ve1,vreduce(ve1)),sK62(ve1,vreduce(ve1)),sK63(ve1,vreduce(ve1))))
| ~ spl90_29 ),
inference(resolution,[],[f1024,f333]) ).
fof(f6743,plain,
( vgetSomeExp(vreduce(ve1)) = vsubst(sK61(ve1,vreduce(ve1)),sK62(ve1,vreduce(ve1)),sK63(ve1,vreduce(ve1)))
| ~ spl90_29 ),
inference(superposition,[],[f466,f6562]) ).
fof(f6783,plain,
( vreduce(ve1) = vsomeExp(vgetSomeExp(vreduce(ve1)))
| ~ spl90_29 ),
inference(superposition,[],[f6562,f6743]) ).
fof(f6881,plain,
( vreduce(ve1) != vreduce(ve1)
| vtcheck(sK87,vgetSomeExp(vreduce(ve1)),varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89))
| ~ spl90_8
| ~ spl90_29 ),
inference(superposition,[],[f1093,f6783]) ).
fof(f6883,plain,
( vtcheck(sK87,vgetSomeExp(vreduce(ve1)),varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89))
| ~ spl90_8
| ~ spl90_29 ),
inference(trivial_inequality_removal,[],[f6881]) ).
fof(f7275,plain,
( vtcheck(sK87,vapp(vgetSomeExp(vreduce(ve1)),sK80(vapp(ve1,ve2),sK89,sK87)),sK89)
| ~ spl90_8
| ~ spl90_29 ),
inference(resolution,[],[f758,f6883]) ).
fof(f7298,plain,
( vtcheck(sK87,vapp(vgetSomeExp(vreduce(ve1)),ve2),sK89)
| ~ spl90_8
| ~ spl90_29 ),
inference(forward_demodulation,[],[f7275,f969]) ).
fof(f7304,plain,
( vtcheck(sK87,sK88,sK89)
| ~ spl90_3
| ~ spl90_8
| ~ spl90_29 ),
inference(forward_demodulation,[],[f7298,f5378]) ).
fof(f7305,plain,
( $false
| ~ spl90_3
| ~ spl90_8
| ~ spl90_29 ),
inference(forward_subsumption_resolution,[],[f7304,f380]) ).
fof(f7306,plain,
( ~ spl90_3
| ~ spl90_8
| ~ spl90_29 ),
inference(avatar_contradiction_clause,[],[f7305]) ).
fof(f7573,plain,
( vreduce(ve1) = vsomeExp(vapp(vgetSomeExp(sK70(ve1,vreduce(ve1))),sK71(ve1,vreduce(ve1))))
| ~ spl90_27 ),
inference(resolution,[],[f1018,f343]) ).
fof(f7788,plain,
( ! [X0,X1] :
( vreduce(ve1) != vreduce(ve1)
| vtcheck(X0,vapp(vgetSomeExp(sK70(ve1,vreduce(ve1))),sK71(ve1,vreduce(ve1))),X1)
| ~ vtcheck(X0,ve1,X1) )
| ~ spl90_27 ),
inference(superposition,[],[f376,f7573]) ).
fof(f7791,plain,
( vgetSomeExp(vreduce(ve1)) = vapp(vgetSomeExp(sK70(ve1,vreduce(ve1))),sK71(ve1,vreduce(ve1)))
| ~ spl90_27 ),
inference(superposition,[],[f466,f7573]) ).
fof(f7796,plain,
( ! [X0,X1] :
( vtcheck(X0,vapp(vgetSomeExp(sK70(ve1,vreduce(ve1))),sK71(ve1,vreduce(ve1))),X1)
| ~ vtcheck(X0,ve1,X1) )
| ~ spl90_27 ),
inference(trivial_inequality_removal,[],[f7788]) ).
fof(f7800,plain,
( ! [X0,X1] :
( vtcheck(X0,vgetSomeExp(vreduce(ve1)),X1)
| ~ vtcheck(X0,ve1,X1) )
| ~ spl90_27 ),
inference(forward_demodulation,[],[f7796,f7791]) ).
fof(f7820,plain,
( ! [X0] :
( ~ vtcheck(sK87,ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),X0))
| vtcheck(sK87,vapp(vgetSomeExp(vreduce(ve1)),sK80(vapp(ve1,ve2),sK89,sK87)),X0) )
| ~ spl90_8
| ~ spl90_27 ),
inference(resolution,[],[f7800,f758]) ).
fof(f7825,plain,
( ! [X0] :
( vtcheck(sK87,vapp(vgetSomeExp(vreduce(ve1)),ve2),X0)
| ~ vtcheck(sK87,ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),X0)) )
| ~ spl90_8
| ~ spl90_27 ),
inference(forward_demodulation,[],[f7820,f969]) ).
fof(f7826,plain,
( ! [X0] :
( ~ vtcheck(sK87,ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),X0))
| vtcheck(sK87,sK88,X0) )
| ~ spl90_3
| ~ spl90_8
| ~ spl90_27 ),
inference(forward_demodulation,[],[f7825,f5378]) ).
fof(f7827,plain,
( vtcheck(sK87,sK88,sK89)
| ~ spl90_3
| ~ spl90_8
| ~ spl90_27 ),
inference(resolution,[],[f7826,f1092]) ).
fof(f7831,plain,
( $false
| ~ spl90_3
| ~ spl90_8
| ~ spl90_27 ),
inference(forward_subsumption_resolution,[],[f7827,f380]) ).
fof(f7832,plain,
( ~ spl90_3
| ~ spl90_8
| ~ spl90_27 ),
inference(avatar_contradiction_clause,[],[f7831]) ).
fof(f10152,plain,
( vapp(ve1,ve2) = vapp(vabs(sK61(vapp(ve1,ve2),vsomeExp(sK88)),sK59(vapp(ve1,ve2),vsomeExp(sK88)),sK63(vapp(ve1,ve2),vsomeExp(sK88))),sK62(vapp(ve1,ve2),vsomeExp(sK88)))
| ~ spl90_5 ),
inference(resolution,[],[f638,f337]) ).
fof(f10253,plain,
( vapp(ve1,ve2) != vapp(ve1,ve2)
| sK80(vapp(ve1,ve2),sK89,sK87) = sK62(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_5
| ~ spl90_8 ),
inference(superposition,[],[f939,f10152]) ).
fof(f10254,plain,
( vapp(ve1,ve2) != vapp(ve1,ve2)
| sK79(vapp(ve1,ve2),sK89,sK87) = vabs(sK61(vapp(ve1,ve2),vsomeExp(sK88)),sK59(vapp(ve1,ve2),vsomeExp(sK88)),sK63(vapp(ve1,ve2),vsomeExp(sK88)))
| ~ spl90_5
| ~ spl90_8 ),
inference(superposition,[],[f941,f10152]) ).
fof(f10256,plain,
( sK79(vapp(ve1,ve2),sK89,sK87) = vabs(sK61(vapp(ve1,ve2),vsomeExp(sK88)),sK59(vapp(ve1,ve2),vsomeExp(sK88)),sK63(vapp(ve1,ve2),vsomeExp(sK88)))
| ~ spl90_5
| ~ spl90_8 ),
inference(trivial_inequality_removal,[],[f10254]) ).
fof(f10257,plain,
( sK80(vapp(ve1,ve2),sK89,sK87) = sK62(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_5
| ~ spl90_8 ),
inference(trivial_inequality_removal,[],[f10253]) ).
fof(f10258,plain,
( ve1 = vabs(sK61(vapp(ve1,ve2),vsomeExp(sK88)),sK59(vapp(ve1,ve2),vsomeExp(sK88)),sK63(vapp(ve1,ve2),vsomeExp(sK88)))
| ~ spl90_5
| ~ spl90_8 ),
inference(forward_demodulation,[],[f10256,f988]) ).
fof(f10259,plain,
( ve2 = sK62(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_5
| ~ spl90_8 ),
inference(forward_demodulation,[],[f10257,f969]) ).
fof(f10261,plain,
( $false
| ~ spl90_5
| ~ spl90_8
| ~ spl90_40 ),
inference(forward_subsumption_resolution,[],[f10258,f1935]) ).
fof(f10262,plain,
( ~ spl90_5
| ~ spl90_8
| ~ spl90_40 ),
inference(avatar_contradiction_clause,[],[f10261]) ).
fof(f10764,plain,
( visValue(ve2)
| ~ sP10(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_5
| ~ spl90_8 ),
inference(superposition,[],[f334,f10259]) ).
fof(f10769,plain,
( ~ sP10(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_5
| ~ spl90_8
| ~ spl90_36 ),
inference(forward_subsumption_resolution,[],[f10764,f1297]) ).
fof(f10772,plain,
( $false
| ~ spl90_5
| ~ spl90_8
| ~ spl90_36 ),
inference(forward_subsumption_resolution,[],[f10769,f638]) ).
fof(f10773,plain,
( ~ spl90_5
| ~ spl90_8
| ~ spl90_36 ),
inference(avatar_contradiction_clause,[],[f10772]) ).
fof(f11674,plain,
( ve1 != ve1
| sK53(ve1) = sK84(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87)
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41 ),
inference(superposition,[],[f1711,f1110]) ).
fof(f11676,plain,
( sK53(ve1) = sK84(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87)
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41 ),
inference(trivial_inequality_removal,[],[f11674]) ).
fof(f11752,plain,
( ve1 = vabs(sK83(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),sK85(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),sK53(ve1))
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41 ),
inference(superposition,[],[f1110,f11676]) ).
fof(f11755,plain,
( vtcheck(vbind(sK83(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),sK85(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),sK87),sK53(ve1),sK86(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87))
| ve1 = vvar(sK82(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87))
| sP12(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87)
| ~ vtcheck(sK87,ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89))
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41 ),
inference(superposition,[],[f369,f11676]) ).
fof(f11758,plain,
( vtcheck(vbind(sK83(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),sK85(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),sK87),sK53(ve1),sK86(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87))
| sP12(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87)
| ~ vtcheck(sK87,ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89))
| ~ spl90_1
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41 ),
inference(forward_subsumption_resolution,[],[f11755,f2511]) ).
fof(f11761,plain,
( vtcheck(vbind(sK83(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),sK85(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),sK87),sK53(ve1),sK86(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87))
| sP12(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87)
| ~ spl90_1
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41 ),
inference(forward_subsumption_resolution,[],[f11758,f1092]) ).
fof(f11763,definition,
( spl90_402
<=> vtcheck(vbind(sK83(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),sK85(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),sK87),sK53(ve1),sK86(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87)) ),
introduced(definition,[new_symbols(definition,[spl90_402])],[avatar_definition]) ).
fof(f11764,plain,
( vtcheck(vbind(sK83(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),sK85(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),sK87),sK53(ve1),sK86(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87))
| ~ spl90_402 ),
inference(avatar_component_clause,[],[f11763]) ).
fof(f11766,plain,
( spl90_40
| spl90_402
| ~ spl90_1
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41 ),
inference(avatar_split_clause,[],[f11761,f1109,f954,f720,f600,f11763,f1106]) ).
fof(f11959,plain,
( ve1 != ve1
| sK52(ve1) = sK85(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87)
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41 ),
inference(superposition,[],[f1709,f11752]) ).
fof(f11960,plain,
( sK52(ve1) = sK85(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87)
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41 ),
inference(trivial_inequality_removal,[],[f11959]) ).
fof(f12015,plain,
( varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89) = varrow(sK52(ve1),sK86(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87))
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43 ),
inference(superposition,[],[f1117,f11960]) ).
fof(f12308,plain,
( ve1 != ve1
| sK51(ve1) = sK83(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87)
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41 ),
inference(superposition,[],[f1707,f11752]) ).
fof(f12309,plain,
( sK51(ve1) = sK83(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87)
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41 ),
inference(trivial_inequality_removal,[],[f12308]) ).
fof(f14310,plain,
( ! [X0,X1] :
( varrow(X0,X1) != varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89)
| sK52(ve1) = X0 )
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43 ),
inference(superposition,[],[f359,f12015]) ).
fof(f16281,plain,
( vtcheck(vbind(sK51(ve1),sK85(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),sK87),sK53(ve1),sK86(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87))
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41
| ~ spl90_402 ),
inference(superposition,[],[f11764,f12309]) ).
fof(f16292,plain,
( vtcheck(vbind(sK51(ve1),sK52(ve1),sK87),sK53(ve1),sK86(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87))
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41
| ~ spl90_402 ),
inference(forward_demodulation,[],[f16281,f11960]) ).
fof(f21839,plain,
( sK52(ve1) = sK81(vapp(ve1,ve2),sK89,sK87)
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43 ),
inference(equality_resolution,[],[f14310]) ).
fof(f21874,plain,
( vtcheck(sK87,ve2,sK52(ve1))
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43 ),
inference(superposition,[],[f1045,f21839]) ).
fof(f21879,plain,
( ! [X0] :
( vtcheck(sK87,vapp(ve1,X0),sK89)
| ~ vtcheck(sK87,X0,sK52(ve1)) )
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43 ),
inference(superposition,[],[f1094,f21839]) ).
fof(f23732,plain,
( ~ vtcheck(sK87,ve2,sK52(ve1))
| vtcheck(sK87,sK88,sK86(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87))
| ~ spl90_8
| ~ spl90_22
| ~ spl90_35
| ~ spl90_41
| ~ spl90_51
| ~ spl90_402 ),
inference(resolution,[],[f16292,f3924]) ).
fof(f23748,plain,
( vtcheck(sK87,sK88,sK86(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87))
| ~ spl90_8
| ~ spl90_22
| ~ spl90_35
| ~ spl90_41
| ~ spl90_43
| ~ spl90_51
| ~ spl90_402 ),
inference(forward_subsumption_resolution,[],[f23732,f21874]) ).
fof(f23751,plain,
( vtcheck(sK87,sK88,sK86(ve1,varrow(sK52(ve1),sK89),sK87))
| ~ spl90_8
| ~ spl90_22
| ~ spl90_35
| ~ spl90_41
| ~ spl90_43
| ~ spl90_51
| ~ spl90_402 ),
inference(forward_demodulation,[],[f23748,f21839]) ).
fof(f26344,plain,
( $false
| ~ spl90_1
| ~ spl90_42 ),
inference(forward_subsumption_resolution,[],[f1983,f2516]) ).
fof(f26345,plain,
( ~ spl90_1
| ~ spl90_42 ),
inference(avatar_contradiction_clause,[],[f26344]) ).
fof(f34348,plain,
( sK89 = sK86(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87)
| ~ spl90_43 ),
inference(equality_resolution,[],[f5262]) ).
fof(f34349,plain,
( sK89 = sK86(ve1,varrow(sK52(ve1),sK89),sK87)
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43 ),
inference(forward_demodulation,[],[f34348,f21839]) ).
fof(f34374,plain,
( vtcheck(sK87,sK88,sK89)
| ~ spl90_8
| ~ spl90_22
| ~ spl90_35
| ~ spl90_41
| ~ spl90_43
| ~ spl90_51
| ~ spl90_402 ),
inference(superposition,[],[f23751,f34349]) ).
fof(f34397,plain,
( $false
| ~ spl90_8
| ~ spl90_22
| ~ spl90_35
| ~ spl90_41
| ~ spl90_43
| ~ spl90_51
| ~ spl90_402 ),
inference(forward_subsumption_resolution,[],[f34374,f380]) ).
fof(f34398,plain,
( ~ spl90_8
| ~ spl90_22
| ~ spl90_35
| ~ spl90_41
| ~ spl90_43
| ~ spl90_51
| ~ spl90_402 ),
inference(avatar_contradiction_clause,[],[f34397]) ).
fof(f34420,plain,
( sP12(ve2,sK52(ve1),sK87)
| ~ spl90_8
| ~ spl90_16
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43 ),
inference(forward_demodulation,[],[f1248,f21839]) ).
fof(f34984,plain,
( ve2 = vapp(sK79(ve2,sK52(ve1),sK87),sK80(ve2,sK52(ve1),sK87))
| ~ spl90_8
| ~ spl90_16
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43 ),
inference(resolution,[],[f34420,f365]) ).
fof(f34985,plain,
( vreduce(vapp(ve1,ve2)) = vsomeExp(vapp(ve1,vgetSomeExp(vreduce(ve2))))
| ~ spl90_6
| ~ spl90_8
| ~ spl90_22 ),
inference(resolution,[],[f3255,f1686]) ).
fof(f34991,plain,
( vsomeExp(sK88) = vsomeExp(vapp(ve1,vgetSomeExp(vreduce(ve2))))
| ~ spl90_6
| ~ spl90_8
| ~ spl90_22 ),
inference(forward_demodulation,[],[f34985,f379]) ).
fof(f35011,plain,
( ! [X0,X1] :
( vapp(X0,X1) != ve2
| sK79(ve2,sK52(ve1),sK87) = X0 )
| ~ spl90_8
| ~ spl90_16
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43 ),
inference(superposition,[],[f232,f34984]) ).
fof(f35077,plain,
( vgetSomeExp(vsomeExp(sK88)) = vapp(ve1,vgetSomeExp(vreduce(ve2)))
| ~ spl90_6
| ~ spl90_8
| ~ spl90_22 ),
inference(superposition,[],[f466,f34991]) ).
fof(f35086,plain,
( sK88 = vapp(ve1,vgetSomeExp(vreduce(ve2)))
| ~ spl90_6
| ~ spl90_8
| ~ spl90_22 ),
inference(forward_demodulation,[],[f35077,f466]) ).
fof(f35145,plain,
( vtcheck(sK87,sK88,sK89)
| ~ vtcheck(sK87,vgetSomeExp(vreduce(ve2)),sK52(ve1))
| ~ spl90_6
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43 ),
inference(superposition,[],[f21879,f35086]) ).
fof(f35176,plain,
( ~ vtcheck(sK87,vgetSomeExp(vreduce(ve2)),sK52(ve1))
| ~ spl90_6
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43 ),
inference(forward_subsumption_resolution,[],[f35145,f380]) ).
fof(f35178,definition,
( spl90_969
<=> vtcheck(sK87,vgetSomeExp(vreduce(ve2)),sK52(ve1)) ),
introduced(definition,[new_symbols(definition,[spl90_969])],[avatar_definition]) ).
fof(f35179,plain,
( ~ vtcheck(sK87,vgetSomeExp(vreduce(ve2)),sK52(ve1))
| spl90_969 ),
inference(avatar_component_clause,[],[f35178]) ).
fof(f35188,plain,
( ~ spl90_969
| ~ spl90_6
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43 ),
inference(avatar_split_clause,[],[f35176,f1116,f1109,f954,f720,f640,f35178]) ).
fof(f36781,plain,
( vreduce(ve2) = vsomeExp(vapp(vgetSomeExp(sK70(ve2,vreduce(ve2))),sK71(ve2,vreduce(ve2))))
| ~ spl90_109 ),
inference(resolution,[],[f3303,f343]) ).
fof(f36950,plain,
( vgetSomeExp(vreduce(ve2)) = vapp(vgetSomeExp(sK70(ve2,vreduce(ve2))),sK71(ve2,vreduce(ve2)))
| ~ spl90_109 ),
inference(superposition,[],[f466,f36781]) ).
fof(f36951,plain,
( vreduce(ve2) != vreduce(ve2)
| vtcheck(sK87,vapp(vgetSomeExp(sK70(ve2,vreduce(ve2))),sK71(ve2,vreduce(ve2))),sK81(vapp(ve1,ve2),sK89,sK87))
| ~ spl90_8
| ~ spl90_109 ),
inference(superposition,[],[f1050,f36781]) ).
fof(f36963,plain,
( vtcheck(sK87,vapp(vgetSomeExp(sK70(ve2,vreduce(ve2))),sK71(ve2,vreduce(ve2))),sK81(vapp(ve1,ve2),sK89,sK87))
| ~ spl90_8
| ~ spl90_109 ),
inference(trivial_inequality_removal,[],[f36951]) ).
fof(f36971,plain,
( vtcheck(sK87,vapp(vgetSomeExp(sK70(ve2,vreduce(ve2))),sK71(ve2,vreduce(ve2))),sK52(ve1))
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43
| ~ spl90_109 ),
inference(forward_demodulation,[],[f36963,f21839]) ).
fof(f36976,plain,
( vtcheck(sK87,vgetSomeExp(vreduce(ve2)),sK52(ve1))
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43
| ~ spl90_109 ),
inference(forward_demodulation,[],[f36971,f36950]) ).
fof(f36977,plain,
( $false
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43
| ~ spl90_109
| spl90_969 ),
inference(forward_subsumption_resolution,[],[f36976,f35179]) ).
fof(f36978,plain,
( ~ spl90_8
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43
| ~ spl90_109
| spl90_969 ),
inference(avatar_contradiction_clause,[],[f36977]) ).
fof(f36979,plain,
( spl90_51
| ~ spl90_110 ),
inference(avatar_split_clause,[],[f5168,f3305,f1276]) ).
fof(f36981,plain,
( vreduce(ve2) = vsomeExp(vsubst(sK61(ve2,vreduce(ve2)),sK62(ve2,vreduce(ve2)),sK63(ve2,vreduce(ve2))))
| ~ spl90_111 ),
inference(resolution,[],[f3309,f333]) ).
fof(f38028,plain,
( vgetSomeExp(vreduce(ve2)) = vsubst(sK61(ve2,vreduce(ve2)),sK62(ve2,vreduce(ve2)),sK63(ve2,vreduce(ve2)))
| ~ spl90_111 ),
inference(superposition,[],[f466,f36981]) ).
fof(f38029,plain,
( vreduce(ve2) != vreduce(ve2)
| vtcheck(sK87,vsubst(sK61(ve2,vreduce(ve2)),sK62(ve2,vreduce(ve2)),sK63(ve2,vreduce(ve2))),sK81(vapp(ve1,ve2),sK89,sK87))
| ~ spl90_8
| ~ spl90_111 ),
inference(superposition,[],[f1050,f36981]) ).
fof(f38042,plain,
( vtcheck(sK87,vsubst(sK61(ve2,vreduce(ve2)),sK62(ve2,vreduce(ve2)),sK63(ve2,vreduce(ve2))),sK81(vapp(ve1,ve2),sK89,sK87))
| ~ spl90_8
| ~ spl90_111 ),
inference(trivial_inequality_removal,[],[f38029]) ).
fof(f38050,plain,
( vtcheck(sK87,vsubst(sK61(ve2,vreduce(ve2)),sK62(ve2,vreduce(ve2)),sK63(ve2,vreduce(ve2))),sK52(ve1))
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43
| ~ spl90_111 ),
inference(forward_demodulation,[],[f38042,f21839]) ).
fof(f38055,plain,
( vtcheck(sK87,vgetSomeExp(vreduce(ve2)),sK52(ve1))
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43
| ~ spl90_111 ),
inference(forward_demodulation,[],[f38050,f38028]) ).
fof(f38056,plain,
( $false
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43
| ~ spl90_111
| spl90_969 ),
inference(forward_subsumption_resolution,[],[f38055,f35179]) ).
fof(f38057,plain,
( ~ spl90_8
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43
| ~ spl90_111
| spl90_969 ),
inference(avatar_contradiction_clause,[],[f38056]) ).
fof(f38058,plain,
( vnoExp = vreduce(ve2)
| ~ spl90_108 ),
inference(resolution,[],[f3300,f348]) ).
fof(f38066,plain,
( spl90_51
| ~ spl90_108 ),
inference(avatar_split_clause,[],[f38058,f3299,f1276]) ).
fof(f38070,plain,
( ve2 = vapp(vabs(sK55(ve2,vreduce(ve2)),sK56(ve2,vreduce(ve2)),sK57(ve2,vreduce(ve2))),sK54(ve2,vreduce(ve2)))
| ~ spl90_112 ),
inference(resolution,[],[f3312,f332]) ).
fof(f43768,plain,
( ve2 != ve2
| sK79(ve2,sK52(ve1),sK87) = vabs(sK55(ve2,vreduce(ve2)),sK56(ve2,vreduce(ve2)),sK57(ve2,vreduce(ve2)))
| ~ spl90_8
| ~ spl90_16
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43
| ~ spl90_112 ),
inference(superposition,[],[f35011,f38070]) ).
fof(f43774,plain,
( sK79(ve2,sK52(ve1),sK87) = vabs(sK55(ve2,vreduce(ve2)),sK56(ve2,vreduce(ve2)),sK57(ve2,vreduce(ve2)))
| ~ spl90_8
| ~ spl90_16
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43
| ~ spl90_112 ),
inference(trivial_inequality_removal,[],[f43768]) ).
fof(f43819,plain,
( vreduce(ve2) = vsomeExp(vapp(sK79(ve2,sK52(ve1),sK87),vgetSomeExp(sK58(ve2,vreduce(ve2)))))
| ~ sP11(ve2,vreduce(ve2))
| ~ spl90_8
| ~ spl90_16
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43
| ~ spl90_112 ),
inference(superposition,[],[f329,f43774]) ).
fof(f43863,plain,
( vreduce(ve2) = vsomeExp(vapp(sK79(ve2,sK52(ve1),sK87),vgetSomeExp(sK58(ve2,vreduce(ve2)))))
| ~ spl90_8
| ~ spl90_16
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43
| ~ spl90_112 ),
inference(forward_subsumption_resolution,[],[f43819,f3312]) ).
fof(f43903,plain,
( vgetSomeExp(vreduce(ve2)) = vapp(sK79(ve2,sK52(ve1),sK87),vgetSomeExp(sK58(ve2,vreduce(ve2))))
| ~ spl90_8
| ~ spl90_16
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43
| ~ spl90_112 ),
inference(superposition,[],[f466,f43863]) ).
fof(f43904,plain,
( vreduce(ve2) != vreduce(ve2)
| vtcheck(sK87,vapp(sK79(ve2,sK52(ve1),sK87),vgetSomeExp(sK58(ve2,vreduce(ve2)))),sK81(vapp(ve1,ve2),sK89,sK87))
| ~ spl90_8
| ~ spl90_16
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43
| ~ spl90_112 ),
inference(superposition,[],[f1050,f43863]) ).
fof(f43929,plain,
( vtcheck(sK87,vapp(sK79(ve2,sK52(ve1),sK87),vgetSomeExp(sK58(ve2,vreduce(ve2)))),sK81(vapp(ve1,ve2),sK89,sK87))
| ~ spl90_8
| ~ spl90_16
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43
| ~ spl90_112 ),
inference(trivial_inequality_removal,[],[f43904]) ).
fof(f43936,plain,
( vtcheck(sK87,vapp(sK79(ve2,sK52(ve1),sK87),vgetSomeExp(sK58(ve2,vreduce(ve2)))),sK52(ve1))
| ~ spl90_8
| ~ spl90_16
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43
| ~ spl90_112 ),
inference(forward_demodulation,[],[f43929,f21839]) ).
fof(f43941,plain,
( vtcheck(sK87,vgetSomeExp(vreduce(ve2)),sK52(ve1))
| ~ spl90_8
| ~ spl90_16
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43
| ~ spl90_112 ),
inference(forward_demodulation,[],[f43936,f43903]) ).
fof(f43942,plain,
( $false
| ~ spl90_8
| ~ spl90_16
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43
| ~ spl90_112
| spl90_969 ),
inference(forward_subsumption_resolution,[],[f43941,f35179]) ).
fof(f43943,plain,
( ~ spl90_8
| ~ spl90_16
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43
| ~ spl90_112
| spl90_969 ),
inference(avatar_contradiction_clause,[],[f43942]) ).
fof(f44130,plain,
( spl90_77
| ~ spl90_6
| ~ spl90_8 ),
inference(avatar_split_clause,[],[f3279,f720,f640,f1954]) ).
fof(f44591,plain,
( vsomeExp(sK88) = vsomeExp(vapp(vgetSomeExp(sK70(vapp(ve1,ve2),vsomeExp(sK88))),sK71(vapp(ve1,ve2),vsomeExp(sK88))))
| ~ spl90_3 ),
inference(resolution,[],[f632,f343]) ).
fof(f44593,plain,
( sK70(vapp(ve1,ve2),vsomeExp(sK88)) = vreduce(sK69(vapp(ve1,ve2),vsomeExp(sK88)))
| ~ spl90_3 ),
inference(resolution,[],[f632,f345]) ).
fof(f44595,plain,
( vapp(ve1,ve2) = vapp(sK69(vapp(ve1,ve2),vsomeExp(sK88)),sK71(vapp(ve1,ve2),vsomeExp(sK88)))
| ~ spl90_3 ),
inference(resolution,[],[f632,f347]) ).
fof(f44606,plain,
( ve1 = vapp(sK79(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),sK80(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87))
| ~ spl90_40 ),
inference(resolution,[],[f1107,f365]) ).
fof(f44613,plain,
( vgetSomeExp(vsomeExp(sK88)) = vapp(vgetSomeExp(sK70(vapp(ve1,ve2),vsomeExp(sK88))),sK71(vapp(ve1,ve2),vsomeExp(sK88)))
| ~ spl90_3 ),
inference(superposition,[],[f466,f44591]) ).
fof(f44635,plain,
( sK88 = vapp(vgetSomeExp(sK70(vapp(ve1,ve2),vsomeExp(sK88))),sK71(vapp(ve1,ve2),vsomeExp(sK88)))
| ~ spl90_3 ),
inference(forward_demodulation,[],[f44613,f466]) ).
fof(f44728,plain,
( vapp(ve1,ve2) != vapp(ve1,ve2)
| sK80(vapp(ve1,ve2),sK89,sK87) = sK71(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_3
| ~ spl90_8 ),
inference(superposition,[],[f939,f44595]) ).
fof(f44729,plain,
( vapp(ve1,ve2) != vapp(ve1,ve2)
| sK79(vapp(ve1,ve2),sK89,sK87) = sK69(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_3
| ~ spl90_8 ),
inference(superposition,[],[f941,f44595]) ).
fof(f44735,plain,
( sK79(vapp(ve1,ve2),sK89,sK87) = sK69(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_3
| ~ spl90_8 ),
inference(trivial_inequality_removal,[],[f44729]) ).
fof(f44736,plain,
( sK80(vapp(ve1,ve2),sK89,sK87) = sK71(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_3
| ~ spl90_8 ),
inference(trivial_inequality_removal,[],[f44728]) ).
fof(f44762,plain,
( ve1 = sK69(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_3
| ~ spl90_8 ),
inference(forward_demodulation,[],[f44735,f988]) ).
fof(f44763,plain,
( ve2 = sK71(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_3
| ~ spl90_8 ),
inference(forward_demodulation,[],[f44736,f969]) ).
fof(f44768,plain,
( vreduce(ve1) = sK70(vapp(ve1,ve2),vsomeExp(sK88))
| ~ spl90_3
| ~ spl90_8 ),
inference(superposition,[],[f44593,f44762]) ).
fof(f44853,plain,
( ! [X0,X1] :
( vapp(X0,X1) != ve1
| sK79(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87) = X0 )
| ~ spl90_40 ),
inference(superposition,[],[f232,f44606]) ).
fof(f45425,plain,
( ve1 = vapp(vabs(sK55(ve1,vreduce(ve1)),sK56(ve1,vreduce(ve1)),sK57(ve1,vreduce(ve1))),sK54(ve1,vreduce(ve1)))
| ~ spl90_30 ),
inference(resolution,[],[f1027,f332]) ).
fof(f45712,plain,
( sK88 = vapp(vgetSomeExp(sK70(vapp(ve1,ve2),vsomeExp(sK88))),ve2)
| ~ spl90_3
| ~ spl90_8 ),
inference(superposition,[],[f44635,f44763]) ).
fof(f45747,plain,
( sK88 = vapp(vgetSomeExp(vreduce(ve1)),ve2)
| ~ spl90_3
| ~ spl90_8 ),
inference(forward_demodulation,[],[f45712,f44768]) ).
fof(f50250,plain,
( ve1 != ve1
| sK79(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87) = vabs(sK55(ve1,vreduce(ve1)),sK56(ve1,vreduce(ve1)),sK57(ve1,vreduce(ve1)))
| ~ spl90_30
| ~ spl90_40 ),
inference(superposition,[],[f44853,f45425]) ).
fof(f50270,plain,
( sK79(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87) = vabs(sK55(ve1,vreduce(ve1)),sK56(ve1,vreduce(ve1)),sK57(ve1,vreduce(ve1)))
| ~ spl90_30
| ~ spl90_40 ),
inference(trivial_inequality_removal,[],[f50250]) ).
fof(f50285,plain,
( vreduce(ve1) = vsomeExp(vapp(sK79(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),vgetSomeExp(sK58(ve1,vreduce(ve1)))))
| ~ sP11(ve1,vreduce(ve1))
| ~ spl90_30
| ~ spl90_40 ),
inference(superposition,[],[f329,f50270]) ).
fof(f50321,plain,
( vreduce(ve1) = vsomeExp(vapp(sK79(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),vgetSomeExp(sK58(ve1,vreduce(ve1)))))
| ~ spl90_30
| ~ spl90_40 ),
inference(forward_subsumption_resolution,[],[f50285,f1027]) ).
fof(f50338,plain,
( ! [X0,X1] :
( vreduce(ve1) != vreduce(ve1)
| vtcheck(X0,vapp(sK79(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),vgetSomeExp(sK58(ve1,vreduce(ve1)))),X1)
| ~ vtcheck(X0,ve1,X1) )
| ~ spl90_30
| ~ spl90_40 ),
inference(superposition,[],[f376,f50321]) ).
fof(f50341,plain,
( vgetSomeExp(vreduce(ve1)) = vapp(sK79(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),vgetSomeExp(sK58(ve1,vreduce(ve1))))
| ~ spl90_30
| ~ spl90_40 ),
inference(superposition,[],[f466,f50321]) ).
fof(f50368,plain,
( ! [X0,X1] :
( vtcheck(X0,vapp(sK79(ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),sK89),sK87),vgetSomeExp(sK58(ve1,vreduce(ve1)))),X1)
| ~ vtcheck(X0,ve1,X1) )
| ~ spl90_30
| ~ spl90_40 ),
inference(trivial_inequality_removal,[],[f50338]) ).
fof(f50369,plain,
( ! [X0,X1] :
( vtcheck(X0,vgetSomeExp(vreduce(ve1)),X1)
| ~ vtcheck(X0,ve1,X1) )
| ~ spl90_30
| ~ spl90_40 ),
inference(forward_demodulation,[],[f50368,f50341]) ).
fof(f50399,plain,
( ! [X0] :
( ~ vtcheck(sK87,ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),X0))
| vtcheck(sK87,vapp(vgetSomeExp(vreduce(ve1)),sK80(vapp(ve1,ve2),sK89,sK87)),X0) )
| ~ spl90_8
| ~ spl90_30
| ~ spl90_40 ),
inference(resolution,[],[f50369,f758]) ).
fof(f50406,plain,
( ! [X0] :
( vtcheck(sK87,vapp(vgetSomeExp(vreduce(ve1)),ve2),X0)
| ~ vtcheck(sK87,ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),X0)) )
| ~ spl90_8
| ~ spl90_30
| ~ spl90_40 ),
inference(forward_demodulation,[],[f50399,f969]) ).
fof(f50420,plain,
( ! [X0] :
( ~ vtcheck(sK87,ve1,varrow(sK81(vapp(ve1,ve2),sK89,sK87),X0))
| vtcheck(sK87,sK88,X0) )
| ~ spl90_3
| ~ spl90_8
| ~ spl90_30
| ~ spl90_40 ),
inference(forward_demodulation,[],[f50406,f45747]) ).
fof(f50421,plain,
( vtcheck(sK87,sK88,sK89)
| ~ spl90_3
| ~ spl90_8
| ~ spl90_30
| ~ spl90_40 ),
inference(resolution,[],[f50420,f1092]) ).
fof(f50425,plain,
( $false
| ~ spl90_3
| ~ spl90_8
| ~ spl90_30
| ~ spl90_40 ),
inference(forward_subsumption_resolution,[],[f50421,f380]) ).
fof(f50426,plain,
( ~ spl90_3
| ~ spl90_8
| ~ spl90_30
| ~ spl90_40 ),
inference(avatar_contradiction_clause,[],[f50425]) ).
cnf(s2,plain,
( spl90_1
| spl90_2 ),
inference(sat_conversion,[],[f609]) ).
cnf(s29,plain,
( spl90_3
| spl90_5
| spl90_6 ),
inference(sat_conversion,[],[f693]) ).
cnf(s38,plain,
spl90_8,
inference(sat_conversion,[],[f737]) ).
cnf(s41,plain,
( ~ spl90_8
| spl90_16
| spl90_17
| spl90_18 ),
inference(sat_conversion,[],[f777]) ).
cnf(s47,plain,
( ~ spl90_8
| spl90_22
| spl90_23 ),
inference(sat_conversion,[],[f959]) ).
cnf(s51,plain,
( ~ spl90_2
| spl90_26
| spl90_27
| spl90_28
| spl90_29
| spl90_30 ),
inference(sat_conversion,[],[f1036]) ).
cnf(s59,plain,
( ~ spl90_8
| spl90_40
| spl90_41
| spl90_42 ),
inference(sat_conversion,[],[f1114]) ).
cnf(s60,plain,
( ~ spl90_8
| spl90_40
| spl90_42
| spl90_43 ),
inference(sat_conversion,[],[f1118]) ).
cnf(s68,plain,
( ~ spl90_8
| ~ spl90_17
| spl90_35 ),
inference(sat_conversion,[],[f1282]) ).
cnf(s71,plain,
( ~ spl90_8
| ~ spl90_18
| spl90_36 ),
inference(sat_conversion,[],[f1287]) ).
cnf(s76,plain,
( ~ spl90_36
| spl90_51 ),
inference(sat_conversion,[],[f1304]) ).
cnf(s145,plain,
( spl90_2
| ~ spl90_8
| ~ spl90_23 ),
inference(sat_conversion,[],[f1763]) ).
cnf(s164,plain,
( ~ spl90_41
| spl90_77 ),
inference(sat_conversion,[],[f1977]) ).
cnf(s165,plain,
( ~ spl90_42
| spl90_77 ),
inference(sat_conversion,[],[f1990]) ).
cnf(s201,plain,
( ~ spl90_1
| ~ spl90_40 ),
inference(sat_conversion,[],[f2527]) ).
cnf(s203,plain,
( ~ spl90_35
| spl90_51 ),
inference(sat_conversion,[],[f2614]) ).
cnf(s213,plain,
( ~ spl90_2
| ~ spl90_77 ),
inference(sat_conversion,[],[f2760]) ).
cnf(s221,plain,
( ~ spl90_1
| ~ spl90_3
| ~ spl90_8 ),
inference(sat_conversion,[],[f2778]) ).
cnf(s252,plain,
( ~ spl90_6
| ~ spl90_8
| spl90_108
| spl90_109
| spl90_110
| spl90_111
| spl90_112 ),
inference(sat_conversion,[],[f3313]) ).
cnf(s268,plain,
( ~ spl90_6
| ~ spl90_8
| ~ spl90_51 ),
inference(sat_conversion,[],[f3878]) ).
cnf(s341,plain,
( ~ spl90_5
| ~ spl90_8
| ~ spl90_16 ),
inference(sat_conversion,[],[f4493]) ).
cnf(s410,plain,
( ~ spl90_26
| spl90_77 ),
inference(sat_conversion,[],[f5563]) ).
cnf(s411,plain,
( ~ spl90_28
| spl90_77 ),
inference(sat_conversion,[],[f5572]) ).
cnf(s615,plain,
( ~ spl90_3
| ~ spl90_8
| ~ spl90_29 ),
inference(sat_conversion,[],[f7306]) ).
cnf(s677,plain,
( ~ spl90_3
| ~ spl90_8
| ~ spl90_27 ),
inference(sat_conversion,[],[f7832]) ).
cnf(s845,plain,
( ~ spl90_5
| ~ spl90_8
| ~ spl90_40 ),
inference(sat_conversion,[],[f10262]) ).
cnf(s881,plain,
( ~ spl90_5
| ~ spl90_8
| ~ spl90_36 ),
inference(sat_conversion,[],[f10773]) ).
cnf(s937,plain,
( ~ spl90_1
| ~ spl90_8
| ~ spl90_22
| spl90_40
| ~ spl90_41
| spl90_402 ),
inference(sat_conversion,[],[f11766]) ).
cnf(s1600,plain,
( ~ spl90_1
| ~ spl90_42 ),
inference(sat_conversion,[],[f26345]) ).
cnf(s1967,plain,
( ~ spl90_8
| ~ spl90_22
| ~ spl90_35
| ~ spl90_41
| ~ spl90_43
| ~ spl90_51
| ~ spl90_402 ),
inference(sat_conversion,[],[f34398]) ).
cnf(s2019,plain,
( ~ spl90_6
| ~ spl90_8
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43
| ~ spl90_969 ),
inference(sat_conversion,[],[f35188]) ).
cnf(s2133,plain,
( ~ spl90_8
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43
| ~ spl90_109
| spl90_969 ),
inference(sat_conversion,[],[f36978]) ).
cnf(s2134,plain,
( spl90_51
| ~ spl90_110 ),
inference(sat_conversion,[],[f36979]) ).
cnf(s2222,plain,
( ~ spl90_8
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43
| ~ spl90_111
| spl90_969 ),
inference(sat_conversion,[],[f38057]) ).
cnf(s2223,plain,
( spl90_51
| ~ spl90_108 ),
inference(sat_conversion,[],[f38066]) ).
cnf(s2674,plain,
( ~ spl90_8
| ~ spl90_16
| ~ spl90_22
| ~ spl90_41
| ~ spl90_43
| ~ spl90_112
| spl90_969 ),
inference(sat_conversion,[],[f43943]) ).
cnf(s2732,plain,
( ~ spl90_6
| ~ spl90_8
| spl90_77 ),
inference(sat_conversion,[],[f44130]) ).
cnf(s3059,plain,
( ~ spl90_3
| ~ spl90_8
| ~ spl90_30
| ~ spl90_40 ),
inference(sat_conversion,[],[f50426]) ).
cnf(s3208,plain,
~ spl90_2,
inference(rat,[],[s51,s615,s677,s3059,s29,s845,s59,s2732,s164,s165,s410,s411,s213,s38]) ).
cnf(s3209,plain,
~ spl90_23,
inference(rat,[],[s145,s38,s3208]) ).
cnf(s3210,plain,
spl90_1,
inference(rat,[],[s2,s3208]) ).
cnf(s3211,plain,
spl90_22,
inference(rat,[],[s47,s38,s3209]) ).
cnf(s3212,plain,
~ spl90_42,
inference(rat,[],[s1600,s3210]) ).
cnf(s3216,plain,
~ spl90_3,
inference(rat,[],[s221,s38,s3210]) ).
cnf(s3217,plain,
~ spl90_40,
inference(rat,[],[s201,s3210]) ).
cnf(s3221,plain,
spl90_43,
inference(rat,[],[s60,s3212,s38,s3217]) ).
cnf(s3222,plain,
spl90_41,
inference(rat,[],[s59,s3212,s38,s3217]) ).
cnf(s3234,plain,
spl90_402,
inference(rat,[],[s937,s3217,s3211,s3210,s38,s3222]) ).
cnf(s3236,plain,
~ spl90_6,
inference(rat,[],[s41,s2674,s71,s68,s252,s76,s203,s2134,s2223,s2133,s2222,s268,s2019,s38,s3222,s3221,s3211]) ).
cnf(s3237,plain,
spl90_5,
inference(rat,[],[s29,s3216,s3236]) ).
cnf(s3239,plain,
~ spl90_36,
inference(rat,[],[s881,s38,s3237]) ).
cnf(s3241,plain,
~ spl90_16,
inference(rat,[],[s341,s38,s3237]) ).
cnf(s3242,plain,
~ spl90_18,
inference(rat,[],[s71,s38,s3239]) ).
cnf(s3245,plain,
spl90_17,
inference(rat,[],[s41,s3241,s38,s3242]) ).
cnf(s3248,plain,
spl90_35,
inference(rat,[],[s68,s38,s3245]) ).
cnf(s3254,plain,
spl90_51,
inference(rat,[],[s203,s3248]) ).
cnf(s3255,plain,
$false,
inference(rat,[],[s1967,s3234,s3211,s3221,s3222,s38,s3254,s3248]) ).
fof(f50427,plain,
$false,
inference(avatar_sat_refutation,[],[s3255]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COM145+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.17 % Computer : n008.cluster.edu
% 0.10/0.17 % Model : x86_64 x86_64
% 0.10/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.17 % Memory : 8046.5625MB
% 0.10/0.17 % OS : Linux 6.8.0-71-generic
% 0.10/0.17 % CPULimit : 300
% 0.10/0.17 % WCLimit : 300
% 0.10/0.17 % DateTime : Mon Sep 28 21:56:40 UTC 2026
% 0.10/0.17 % CPUTime :
% 0.10/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.21 Running first-order theorem proving
% 0.10/0.21 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
% 9.35/1.88 % (2696723)Detected formulas, will run a generic FOF schedule.
% 9.35/1.88 % (2696733)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=843151191:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 9.35/1.88 % (2696730)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=3973587713:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 9.35/1.88 % (2696731)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3658472229:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 9.35/1.88 % (2696732)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2847483648:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 9.35/1.88 % (2696729)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=2967159996:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 9.35/1.88 % (2696728)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=2526652664:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 9.35/1.88 % (2696731)Refutation not found, incomplete strategy
% 9.35/1.88 % (2696731)------------------------------
% 9.35/1.88 % (2696731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.35/1.88 % (2696731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.35/1.88 % (2696731)CaDiCaL version: 2.1.3
% 9.35/1.88 % (2696731)Termination reason: Refutation not found, incomplete strategy
% 9.35/1.88 % (2696731)Time elapsed: 0.002 s
% 9.35/1.88 % (2696731)Peak memory usage: 88 MB
% 9.35/1.88 % (2696731)Instructions burned: 1 (million)
% 9.35/1.88 % (2696732)Refutation not found, incomplete strategy
% 9.35/1.88 % (2696732)------------------------------
% 9.35/1.88 % (2696732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.35/1.88 % (2696732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.35/1.88 % (2696732)CaDiCaL version: 2.1.3
% 9.35/1.88 % (2696732)Termination reason: Refutation not found, incomplete strategy
% 9.35/1.88 % (2696732)Time elapsed: 0.002 s
% 9.35/1.88 % (2696732)Peak memory usage: 88 MB
% 9.35/1.88 % (2696732)Instructions burned: 2 (million)
% 9.35/1.88 % (2696734)dis-21_1_sil=8000:lcm=predicate:random_seed=3658222532:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 9.35/1.88 % (2696733)Instruction limit reached!
% 9.35/1.88 % (2696733)------------------------------
% 9.35/1.88 % (2696733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.35/1.88 % (2696733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.35/1.88 % (2696733)CaDiCaL version: 2.1.3
% 9.35/1.88 % (2696733)Termination reason: Instruction limit
% 9.35/1.88 % (2696733)Termination phase: Saturation
% 9.35/1.88 % (2696733)Time elapsed: 0.049 s
% 9.35/1.88 % (2696733)Peak memory usage: 90 MB
% 9.35/1.88 % (2696733)Instructions burned: 139 (million)
% 9.35/1.88 % (2696734)Instruction limit reached!
% 9.35/1.88 % (2696734)------------------------------
% 9.35/1.88 % (2696734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.35/1.88 % (2696734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.35/1.88 % (2696734)CaDiCaL version: 2.1.3
% 9.35/1.88 % (2696734)Termination reason: Instruction limit
% 9.35/1.88 % (2696734)Termination phase: Saturation
% 9.35/1.88 % (2696734)Time elapsed: 0.075 s
% 9.35/1.88 % (2696734)Peak memory usage: 89 MB
% 9.35/1.88 % (2696734)Instructions burned: 131 (million)
% 9.35/1.88 % (2696742)lrs+10_1_sil=8000:sp=occurrence:random_seed=1899560641:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 9.35/1.88 % (2696742)Refutation not found, incomplete strategy
% 9.35/1.88 % (2696742)------------------------------
% 9.35/1.88 % (2696742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.35/1.88 % (2696742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.35/1.88 % (2696742)CaDiCaL version: 2.1.3
% 9.35/1.88 % (2696742)Termination reason: Refutation not found, incomplete strategy
% 9.35/1.88 % (2696742)Time elapsed: 0.001 s
% 9.35/1.88 % (2696742)Peak memory usage: 88 MB
% 9.35/1.88 % (2696742)Instructions burned: 2 (million)
% 9.35/1.88 % (2696743)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1089995379:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 17.80/3.02 % (2696731)------------------------------
% 17.80/3.02 % (2696731)------------------------------
% 17.80/3.02 % (2696732)------------------------------
% 17.80/3.02 % (2696732)------------------------------
% 17.80/3.02 % (2696742)------------------------------
% 17.80/3.02 % (2696742)------------------------------
% 17.80/3.02 % (2696743)Instruction limit reached!
% 17.80/3.02 % (2696743)------------------------------
% 17.80/3.02 % (2696743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.80/3.02 % (2696743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.80/3.02 % (2696743)CaDiCaL version: 2.1.3
% 17.80/3.02 % (2696743)Termination reason: Instruction limit
% 17.80/3.02 % (2696743)Termination phase: Saturation
% 17.80/3.02 % (2696743)Time elapsed: 0.091 s
% 17.80/3.02 % (2696743)Peak memory usage: 90 MB
% 17.80/3.02 % (2696743)Instructions burned: 157 (million)
% 17.80/3.02 % (2696748)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1233756341:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 17.80/3.02 % (2696746)lrs+1011_1_sil=32000:sp=occurrence:random_seed=71842284:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 17.80/3.02 % (2696747)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=113415849:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 17.80/3.02 % (2696748)Instruction limit reached!
% 17.80/3.02 % (2696748)------------------------------
% 17.80/3.02 % (2696748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.80/3.02 % (2696748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.80/3.02 % (2696748)CaDiCaL version: 2.1.3
% 17.80/3.02 % (2696748)Termination reason: Instruction limit
% 17.80/3.02 % (2696748)Termination phase: Saturation
% 17.80/3.02 % (2696748)Time elapsed: 0.088 s
% 17.80/3.02 % (2696748)Peak memory usage: 90 MB
% 17.80/3.02 % (2696748)Instructions burned: 296 (million)
% 17.80/3.02 % (2696749)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1955586460:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 17.80/3.02 % (2696747)Instruction limit reached!
% 17.80/3.02 % (2696747)------------------------------
% 17.80/3.02 % (2696747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.80/3.02 % (2696747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.80/3.02 % (2696747)CaDiCaL version: 2.1.3
% 17.80/3.02 % (2696747)Termination reason: Instruction limit
% 17.80/3.02 % (2696747)Termination phase: Saturation
% 17.80/3.02 % (2696747)Time elapsed: 0.122 s
% 17.80/3.02 % (2696747)Peak memory usage: 92 MB
% 17.80/3.02 % (2696747)Instructions burned: 249 (million)
% 17.80/3.02 % (2696753)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1831169228:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 17.80/3.02 % (2696753)Instruction limit reached!
% 17.80/3.02 % (2696753)------------------------------
% 17.80/3.02 % (2696753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.80/3.02 % (2696753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.80/3.02 % (2696753)CaDiCaL version: 2.1.3
% 17.80/3.02 % (2696753)Termination reason: Instruction limit
% 17.80/3.02 % (2696753)Termination phase: Saturation
% 17.80/3.02 % (2696753)Time elapsed: 0.039 s
% 17.80/3.02 % (2696753)Peak memory usage: 89 MB
% 17.80/3.02 % (2696753)Instructions burned: 116 (million)
% 17.80/3.02 % (2696746)Instruction limit reached!
% 17.80/3.02 % (2696746)------------------------------
% 17.80/3.02 % (2696746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.80/3.02 % (2696746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.80/3.02 % (2696746)CaDiCaL version: 2.1.3
% 17.80/3.02 % (2696746)Termination reason: Instruction limit
% 17.80/3.02 % (2696746)Termination phase: Saturation
% 17.80/3.02 % (2696746)Time elapsed: 0.191 s
% 17.80/3.02 % (2696746)Peak memory usage: 92 MB
% 17.80/3.02 % (2696746)Instructions burned: 326 (million)
% 17.80/3.02 % (2696757)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=299829056:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 17.80/3.02 % (2696755)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3709883096:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 34.84/5.34 % (2696757)Refutation not found, incomplete strategy
% 34.84/5.34 % (2696757)------------------------------
% 34.84/5.34 % (2696757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.84/5.34 % (2696757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.84/5.34 % (2696757)CaDiCaL version: 2.1.3
% 34.84/5.34 % (2696757)Termination reason: Refutation not found, incomplete strategy
% 34.84/5.34 % (2696757)Time elapsed: 0.001 s
% 34.84/5.34 % (2696757)Peak memory usage: 89 MB
% 34.84/5.34 % (2696757)Instructions burned: 3 (million)
% 34.84/5.34 % (2696755)Instruction limit reached!
% 34.84/5.34 % (2696755)------------------------------
% 34.84/5.34 % (2696755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.84/5.34 % (2696755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.84/5.34 % (2696755)CaDiCaL version: 2.1.3
% 34.84/5.34 % (2696755)Termination reason: Instruction limit
% 34.84/5.34 % (2696755)Termination phase: Saturation
% 34.84/5.34 % (2696755)Time elapsed: 0.064 s
% 34.84/5.34 % (2696755)Peak memory usage: 88 MB
% 34.84/5.34 % (2696755)Instructions burned: 127 (million)
% 34.84/5.34 % (2696758)lrs+10_1_sil=8000:sp=occurrence:random_seed=2465496831:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 34.84/5.34 % (2696757)------------------------------
% 34.84/5.34 % (2696757)------------------------------
% 34.84/5.34 % (2696761)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1050459458:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 34.84/5.34 % (2696761)Refutation not found, incomplete strategy
% 34.84/5.34 % (2696761)------------------------------
% 34.84/5.34 % (2696761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.84/5.34 % (2696761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.84/5.34 % (2696761)CaDiCaL version: 2.1.3
% 34.84/5.34 % (2696761)Termination reason: Refutation not found, incomplete strategy
% 34.84/5.34 % (2696761)Time elapsed: 0.003 s
% 34.84/5.34 % (2696761)Peak memory usage: 88 MB
% 34.84/5.34 % (2696761)Instructions burned: 2 (million)
% 34.84/5.34 % (2696763)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4173189582:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 34.84/5.34 % (2696761)------------------------------
% 34.84/5.34 % (2696761)------------------------------
% 34.84/5.34 % (2696758)Instruction limit reached!
% 34.84/5.34 % (2696758)------------------------------
% 34.84/5.34 % (2696758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.84/5.34 % (2696758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.84/5.34 % (2696758)CaDiCaL version: 2.1.3
% 34.84/5.34 % (2696758)Termination reason: Instruction limit
% 34.84/5.34 % (2696758)Termination phase: Saturation
% 34.84/5.34 % (2696758)Time elapsed: 0.503 s
% 34.84/5.34 % (2696758)Peak memory usage: 96 MB
% 34.84/5.34 % (2696758)Instructions burned: 907 (million)
% 34.84/5.34 % (2696766)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2518161619:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 34.84/5.34 % (2696766)Instruction limit reached!
% 34.84/5.34 % (2696766)------------------------------
% 34.84/5.34 % (2696766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.84/5.34 % (2696766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.84/5.34 % (2696766)CaDiCaL version: 2.1.3
% 34.84/5.34 % (2696766)Termination reason: Instruction limit
% 34.84/5.34 % (2696766)Termination phase: Saturation
% 34.84/5.34 % (2696766)Time elapsed: 0.076 s
% 34.84/5.34 % (2696766)Peak memory usage: 90 MB
% 34.84/5.34 % (2696766)Instructions burned: 136 (million)
% 34.84/5.34 % (2696767)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1577077954:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 34.84/5.34 % (2696767)Refutation not found, incomplete strategy
% 34.84/5.34 % (2696767)------------------------------
% 34.84/5.34 % (2696767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.84/5.34 % (2696767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.84/5.34 % (2696767)CaDiCaL version: 2.1.3
% 34.84/5.34 % (2696767)Termination reason: Refutation not found, incomplete strategy
% 34.84/5.34 % (2696767)Time elapsed: 0.007 s
% 34.84/5.34 % (2696767)Peak memory usage: 88 MB
% 34.84/5.34 % (2696767)Instructions burned: 11 (million)
% 64.58/9.57 % (2696769)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=930978780:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 64.58/9.57 % (2696767)------------------------------
% 64.58/9.57 % (2696767)------------------------------
% 64.58/9.57 % (2696772)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=889800049:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/125Mi)
% 64.58/9.57 % (2696772)Instruction limit reached!
% 64.58/9.57 % (2696772)------------------------------
% 64.58/9.57 % (2696772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.58/9.57 % (2696772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.58/9.57 % (2696772)CaDiCaL version: 2.1.3
% 64.58/9.57 % (2696772)Termination reason: Instruction limit
% 64.58/9.57 % (2696772)Termination phase: Saturation
% 64.58/9.57 % (2696772)Time elapsed: 0.068 s
% 64.58/9.57 % (2696772)Peak memory usage: 90 MB
% 64.58/9.57 % (2696772)Instructions burned: 126 (million)
% 64.58/9.57 % (2696774)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=98558293:i=134:gtgl=5:slsql=off:gtg=exists_sym_2980 on theBenchmark for (2980ds/134Mi)
% 64.58/9.57 % (2696749)Instruction limit reached!
% 64.58/9.57 % (2696749)------------------------------
% 64.58/9.57 % (2696749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.58/9.57 % (2696749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.58/9.57 % (2696749)CaDiCaL version: 2.1.3
% 64.58/9.57 % (2696749)Termination reason: Instruction limit
% 64.58/9.57 % (2696749)Termination phase: Saturation
% 64.58/9.57 % (2696749)Time elapsed: 1.506 s
% 64.58/9.57 % (2696749)Peak memory usage: 141 MB
% 64.58/9.57 % (2696749)Instructions burned: 2351 (million)
% 64.58/9.57 % (2696774)Instruction limit reached!
% 64.58/9.57 % (2696774)------------------------------
% 64.58/9.57 % (2696774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.58/9.57 % (2696774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.58/9.57 % (2696774)CaDiCaL version: 2.1.3
% 64.58/9.57 % (2696774)Termination reason: Instruction limit
% 64.58/9.57 % (2696774)Termination phase: Saturation
% 64.58/9.57 % (2696774)Time elapsed: 0.086 s
% 64.58/9.57 % (2696774)Peak memory usage: 90 MB
% 64.58/9.57 % (2696774)Instructions burned: 134 (million)
% 64.58/9.57 % (2696776)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4017605232:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/141Mi)
% 64.58/9.57 % (2696776)Refutation not found, incomplete strategy
% 64.58/9.57 % (2696776)------------------------------
% 64.58/9.57 % (2696776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.58/9.57 % (2696776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.58/9.57 % (2696776)CaDiCaL version: 2.1.3
% 64.58/9.57 % (2696776)Termination reason: Refutation not found, incomplete strategy
% 64.58/9.57 % (2696776)Time elapsed: 0.002 s
% 64.58/9.57 % (2696776)Peak memory usage: 88 MB
% 64.58/9.57 % (2696776)Instructions burned: 1 (million)
% 64.58/9.57 % (2696777)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3185677457:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2978 on theBenchmark for (2978ds/431Mi)
% 64.58/9.57 % (2696777)Instruction limit reached!
% 64.58/9.57 % (2696777)------------------------------
% 64.58/9.57 % (2696777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.58/9.57 % (2696777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.58/9.57 % (2696777)CaDiCaL version: 2.1.3
% 64.58/9.57 % (2696777)Termination reason: Instruction limit
% 64.58/9.57 % (2696777)Termination phase: Saturation
% 64.58/9.57 % (2696777)Time elapsed: 0.225 s
% 64.58/9.57 % (2696777)Peak memory usage: 91 MB
% 64.58/9.57 % (2696777)Instructions burned: 431 (million)
% 64.58/9.57 % (2696776)------------------------------
% 64.58/9.57 % (2696776)------------------------------
% 64.58/9.57 % (2696780)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=841876082:i=6060:aac=none:ins=25_2975 on theBenchmark for (2975ds/6060Mi)
% 64.58/9.57 % (2696781)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=3894257927:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2975 on theBenchmark for (2975ds/150Mi)
% 75.54/11.12 % (2696763)Instruction limit reached!
% 75.54/11.12 % (2696763)------------------------------
% 75.54/11.12 % (2696763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.54/11.12 % (2696763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.54/11.12 % (2696763)CaDiCaL version: 2.1.3
% 75.54/11.12 % (2696763)Termination reason: Instruction limit
% 75.54/11.12 % (2696763)Termination phase: Saturation
% 75.54/11.12 % (2696763)Time elapsed: 1.634 s
% 75.54/11.12 % (2696763)Peak memory usage: 150 MB
% 75.54/11.12 % (2696763)Instructions burned: 5204 (million)
% 75.54/11.12 % (2696781)Instruction limit reached!
% 75.54/11.12 % (2696781)------------------------------
% 75.54/11.12 % (2696781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.54/11.12 % (2696781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.54/11.12 % (2696781)CaDiCaL version: 2.1.3
% 75.54/11.12 % (2696781)Termination reason: Instruction limit
% 75.54/11.12 % (2696781)Termination phase: Saturation
% 75.54/11.12 % (2696781)Time elapsed: 0.087 s
% 75.54/11.12 % (2696781)Peak memory usage: 90 MB
% 75.54/11.12 % (2696781)Instructions burned: 152 (million)
% 75.54/11.12 % (2696784)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1191901218:i=14155:bd=all_2973 on theBenchmark for (2973ds/14155Mi)
% 75.54/11.12 % (2696785)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1461846846:i=667:av=off:fsr=off_2972 on theBenchmark for (2972ds/667Mi)
% 75.54/11.12 % (2696785)Instruction limit reached!
% 75.54/11.12 % (2696785)------------------------------
% 75.54/11.12 % (2696785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.54/11.12 % (2696785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.54/11.12 % (2696785)CaDiCaL version: 2.1.3
% 75.54/11.12 % (2696785)Termination reason: Instruction limit
% 75.54/11.12 % (2696785)Termination phase: Saturation
% 75.54/11.12 % (2696785)Time elapsed: 0.267 s
% 75.54/11.12 % (2696785)Peak memory usage: 91 MB
% 75.54/11.12 % (2696785)Instructions burned: 667 (million)
% 75.54/11.12 % (2696788)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=1506833591:s2a=on:i=185:s2at=1.8:fdi=4_2968 on theBenchmark for (2968ds/185Mi)
% 75.54/11.12 % (2696788)Instruction limit reached!
% 75.54/11.12 % (2696788)------------------------------
% 75.54/11.12 % (2696788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.54/11.12 % (2696788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.54/11.12 % (2696788)CaDiCaL version: 2.1.3
% 75.54/11.12 % (2696788)Termination reason: Instruction limit
% 75.54/11.12 % (2696788)Termination phase: Saturation
% 75.54/11.12 % (2696788)Time elapsed: 0.087 s
% 75.54/11.12 % (2696788)Peak memory usage: 90 MB
% 75.54/11.12 % (2696788)Instructions burned: 186 (million)
% 75.54/11.12 % (2696790)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=122796037:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2966 on theBenchmark for (2966ds/193Mi)
% 75.54/11.12 % (2696790)Refutation not found, incomplete strategy
% 75.54/11.12 % (2696790)------------------------------
% 75.54/11.12 % (2696790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.54/11.12 % (2696790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.54/11.12 % (2696790)CaDiCaL version: 2.1.3
% 75.54/11.12 % (2696790)Termination reason: Refutation not found, incomplete strategy
% 75.54/11.12 % (2696790)Time elapsed: 0.003 s
% 75.54/11.12 % (2696790)Peak memory usage: 89 MB
% 75.54/11.12 % (2696790)Instructions burned: 3 (million)
% 75.54/11.12 % (2696790)------------------------------
% 75.54/11.12 % (2696790)------------------------------
% 75.54/11.12 % (2696792)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1346781972:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2963 on theBenchmark for (2963ds/4850Mi)
% 75.54/11.12 % (2696780)Instruction limit reached!
% 75.54/11.12 % (2696780)------------------------------
% 75.54/11.12 % (2696780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.54/11.12 % (2696780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.54/11.12 % (2696780)CaDiCaL version: 2.1.3
% 75.54/11.12 % (2696780)Termination reason: Instruction limit
% 75.54/11.12 % (2696780)Termination phase: Saturation
% 46.65/12.63 % (2696780)Time elapsed: 2.339 s
% 46.65/12.63 % (2696780)Peak memory usage: 167 MB
% 46.65/12.63 % (2696780)Instructions burned: 6060 (million)
% 46.65/12.63 % (2696794)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2001999012:i=12111:sd=1:ss=included_2950 on theBenchmark for (2950ds/12111Mi)
% 46.65/12.63 % (2696792)Instruction limit reached!
% 46.65/12.63 % (2696792)------------------------------
% 46.65/12.63 % (2696792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.65/12.63 % (2696792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.65/12.63 % (2696792)CaDiCaL version: 2.1.3
% 46.65/12.63 % (2696792)Termination reason: Instruction limit
% 46.65/12.63 % (2696792)Termination phase: Saturation
% 46.65/12.63 % (2696792)Time elapsed: 3.213 s
% 46.65/12.63 % (2696792)Peak memory usage: 138 MB
% 46.65/12.63 % (2696792)Instructions burned: 4850 (million)
% 46.65/12.63 % (2696796)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2231676445:i=319:kws=precedence:fsr=off_2929 on theBenchmark for (2929ds/319Mi)
% 46.65/12.63 % (2696796)Instruction limit reached!
% 46.65/12.63 % (2696796)------------------------------
% 46.65/12.63 % (2696796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.65/12.63 % (2696796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.65/12.63 % (2696796)CaDiCaL version: 2.1.3
% 46.65/12.63 % (2696796)Termination reason: Instruction limit
% 46.65/12.63 % (2696796)Termination phase: Saturation
% 46.65/12.63 % (2696796)Time elapsed: 0.185 s
% 46.65/12.63 % (2696796)Peak memory usage: 93 MB
% 46.65/12.63 % (2696796)Instructions burned: 320 (million)
% 46.65/12.63 % (2696798)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1852652972:i=2064:ep=RST_2926 on theBenchmark for (2926ds/2064Mi)
% 46.65/12.63 % (2696794)Instruction limit reached!
% 46.65/12.63 % (2696794)------------------------------
% 46.65/12.63 % (2696794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.65/12.63 % (2696794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.65/12.63 % (2696794)CaDiCaL version: 2.1.3
% 46.65/12.63 % (2696794)Termination reason: Instruction limit
% 46.65/12.63 % (2696794)Termination phase: Saturation
% 46.65/12.63 % (2696794)Time elapsed: 3.346 s
% 46.65/12.63 % (2696794)Peak memory usage: 244 MB
% 46.65/12.63 % (2696794)Instructions burned: 12111 (million)
% 46.65/12.63 % (2696798)Instruction limit reached!
% 46.65/12.63 % (2696798)------------------------------
% 46.65/12.63 % (2696798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.65/12.63 % (2696798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.65/12.63 % (2696798)CaDiCaL version: 2.1.3
% 46.65/12.63 % (2696798)Termination reason: Instruction limit
% 46.65/12.63 % (2696798)Termination phase: Saturation
% 46.65/12.63 % (2696798)Time elapsed: 0.966 s
% 46.65/12.63 % (2696798)Peak memory usage: 98 MB
% 46.65/12.63 % (2696798)Instructions burned: 2064 (million)
% 46.65/12.63 % (2696800)dis-1011_128_sil=32000:random_seed=2815588679:i=3706:ep=RST:av=off_2915 on theBenchmark for (2915ds/3706Mi)
% 46.65/12.63 % (2696801)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3911587941:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2915 on theBenchmark for (2915ds/757Mi)
% 46.65/12.63 % (2696801)Instruction limit reached!
% 46.65/12.63 % (2696801)------------------------------
% 46.65/12.63 % (2696801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.65/12.63 % (2696801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.65/12.63 % (2696801)CaDiCaL version: 2.1.3
% 46.65/12.63 % (2696801)Termination reason: Instruction limit
% 46.65/12.63 % (2696801)Termination phase: Saturation
% 46.65/12.63 % (2696801)Time elapsed: 0.393 s
% 46.65/12.63 % (2696801)Peak memory usage: 93 MB
% 46.65/12.63 % (2696801)Instructions burned: 757 (million)
% 46.65/12.63 % (2696804)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3428252399:i=13913:ss=axioms:sgt=8_2910 on theBenchmark for (2910ds/13913Mi)
% 46.65/12.63 % (2696800)Instruction limit reached!
% 46.65/12.63 % (2696800)------------------------------
% 46.65/12.63 % (2696800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.65/12.63 % (2696800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.65/12.63 % (2696800)CaDiCaL version: 2.1.3
% 46.65/12.63 % (2696800)Termination reason: Instruction limit
% 46.65/12.63 % (2696800)Termination phase: Saturation
% 46.65/12.63 % (2696800)Time elapsed: 0.640 s
% 46.65/12.63 % (2696800)Peak memory usage: 88 MB
% 46.65/12.63 % (2696800)Instructions burned: 3713 (million)
% 46.65/12.63 % (2696806)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3579414958:i=9925:aac=none_2908 on theBenchmark for (2908ds/9925Mi)
% 46.65/12.63 % (2696804)Refutation not found, incomplete strategy
% 46.65/12.63 % (2696804)------------------------------
% 46.65/12.63 % (2696804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.65/12.63 % (2696804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.65/12.63 % (2696804)CaDiCaL version: 2.1.3
% 46.65/12.63 % (2696804)Termination reason: Refutation not found, incomplete strategy
% 46.65/12.63 % (2696804)Time elapsed: 0.572 s
% 46.65/12.63 % (2696804)Peak memory usage: 128 MB
% 46.65/12.63 % (2696804)Instructions burned: 865 (million)
% 46.65/12.63 % (2696769)Instruction limit reached!
% 46.65/12.63 % (2696769)------------------------------
% 46.65/12.63 % (2696769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.65/12.63 % (2696769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.65/12.63 % (2696769)CaDiCaL version: 2.1.3
% 46.65/12.63 % (2696769)Termination reason: Instruction limit
% 46.65/12.63 % (2696769)Termination phase: Saturation
% 46.65/12.63 % (2696769)Time elapsed: 8.199 s
% 46.65/12.63 % (2696769)Peak memory usage: 228 MB
% 46.65/12.63 % (2696769)Instructions burned: 13194 (million)
% 46.65/12.63 % (2696808)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=214733255:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2902 on theBenchmark for (2902ds/2479Mi)
% 46.65/12.63 % (2696808)Refutation not found, incomplete strategy
% 46.65/12.63 % (2696808)------------------------------
% 46.65/12.63 % (2696808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.65/12.63 % (2696808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.65/12.63 % (2696808)CaDiCaL version: 2.1.3
% 46.65/12.63 % (2696808)Termination reason: Refutation not found, incomplete strategy
% 46.65/12.63 % (2696808)Time elapsed: 0.002 s
% 46.65/12.63 % (2696808)Peak memory usage: 89 MB
% 46.65/12.63 % (2696808)Instructions burned: 1 (million)
% 46.65/12.63 % (2696804)------------------------------
% 46.65/12.63 % (2696804)------------------------------
% 46.65/12.63 % (2696784)Instruction limit reached!
% 46.65/12.63 % (2696784)------------------------------
% 46.65/12.63 % (2696784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.65/12.63 % (2696784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.65/12.63 % (2696784)CaDiCaL version: 2.1.3
% 46.65/12.63 % (2696784)Termination reason: Instruction limit
% 46.65/12.63 % (2696784)Termination phase: Saturation
% 46.65/12.63 % (2696784)Time elapsed: 7.310 s
% 46.65/12.63 % (2696784)Peak memory usage: 256 MB
% 46.65/12.63 % (2696784)Instructions burned: 14156 (million)
% 46.65/12.63 % (2696810)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1565675751:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2900 on theBenchmark for (2900ds/440Mi)
% 46.65/12.63 % (2696808)------------------------------
% 46.65/12.63 % (2696808)------------------------------
% 46.65/12.63 % (2696812)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=4290187070:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2899 on theBenchmark for (2899ds/11145Mi)
% 46.65/12.63 % (2696813)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=2553344919:cts=off:i=3034:av=off:er=known:fsd=on_2898 on theBenchmark for (2898ds/3034Mi)
% 46.65/12.63 % (2696810)Instruction limit reached!
% 46.65/12.63 % (2696810)------------------------------
% 46.65/12.63 % (2696810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.65/12.63 % (2696810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.65/12.63 % (2696810)CaDiCaL version: 2.1.3
% 46.65/12.63 % (2696810)Termination reason: Instruction limit
% 46.65/12.63 % (2696810)Termination phase: Saturation
% 46.65/12.63 % (2696810)Time elapsed: 0.254 s
% 46.65/12.63 % (2696810)Peak memory usage: 96 MB
% 46.65/12.63 % (2696810)Instructions burned: 440 (million)
% 46.65/12.63 % (2696816)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2700219638:st=2:s2a=on:i=524:s2at=2:ss=axioms_2896 on theBenchmark for (2896ds/524Mi)
% 46.65/12.63 % (2696816)Instruction limit reached!
% 46.65/12.63 % (2696816)------------------------------
% 46.65/12.63 % (2696816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.65/12.63 % (2696816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.65/12.63 % (2696816)CaDiCaL version: 2.1.3
% 46.65/12.63 % (2696816)Termination reason: Instruction limit
% 46.65/12.63 % (2696816)Termination phase: Saturation
% 46.65/12.63 % (2696816)Time elapsed: 0.268 s
% 46.65/12.63 % (2696816)Peak memory usage: 92 MB
% 46.65/12.63 % (2696816)Instructions burned: 525 (million)
% 46.65/12.63 % (2696818)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1469095523:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2892 on theBenchmark for (2892ds/1016Mi)
% 46.65/12.63 % (2696818)Instruction limit reached!
% 46.65/12.63 % (2696818)------------------------------
% 46.65/12.63 % (2696818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.65/12.63 % (2696818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.65/12.63 % (2696818)CaDiCaL version: 2.1.3
% 46.65/12.63 % (2696818)Termination reason: Instruction limit
% 46.65/12.63 % (2696818)Termination phase: Saturation
% 46.65/12.63 % (2696818)Time elapsed: 0.567 s
% 46.65/12.63 % (2696818)Peak memory usage: 102 MB
% 46.65/12.63 % (2696818)Instructions burned: 1018 (million)
% 46.65/12.63 % (2696820)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2992538637:i=14123:bd=preordered:ins=4_2885 on theBenchmark for (2885ds/14123Mi)
% 46.65/12.63 % (2696806)First to succeed.
% 46.65/12.63 % (2696813)Instruction limit reached!
% 46.65/12.63 % (2696813)------------------------------
% 46.65/12.63 % (2696813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.65/12.63 % (2696813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.65/12.63 % (2696813)CaDiCaL version: 2.1.3
% 46.65/12.63 % (2696813)Termination reason: Instruction limit
% 46.65/12.63 % (2696813)Termination phase: Saturation
% 46.65/12.63 % (2696813)Time elapsed: 1.746 s
% 46.65/12.63 % (2696813)Peak memory usage: 133 MB
% 46.65/12.63 % (2696813)Instructions burned: 3034 (million)
% 46.65/12.63 % (2696806)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2696723"
% 46.65/12.63 % (2696822)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1790951290:i=5781:kws=precedence:bd=all:rawr=on_2879 on theBenchmark for (2879ds/5781Mi)
% 46.65/12.63 % (2696806)Refutation found. Thanks to Tanya!
% 46.65/12.63 % SZS status Theorem for theBenchmark
% 46.65/12.63 % SZS output start Proof for theBenchmark
% See solution above
% 86.95/12.82 % (2696806)------------------------------
% 86.95/12.82 % (2696806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.95/12.82 % (2696806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.95/12.82 % (2696806)CaDiCaL version: 2.1.3
% 86.95/12.82 % (2696806)Termination reason: Refutation
% 86.95/12.82 % (2696806)Time elapsed: 2.778 s
% 86.95/12.82 % (2696806)Peak memory usage: 180 MB
% 86.95/12.82 % (2696806)Instructions burned: 8097 (million)
% 86.95/12.82 % (2696806)------------------------------
% 86.95/12.82 % (2696806)------------------------------
% 86.95/12.82 % (2696723)Success in time 12.22 s
% 86.95/12.82 % Vampire exiting
%------------------------------------------------------------------------------