%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : COM019+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n013.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:40:09 AM UTC 2026
% Result : Theorem 27.97s 4.28s
% Output : Refutation 27.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 21
% Syntax : Number of formulae : 194 ( 28 unt; 10 def)
% Number of atoms : 928 ( 72 equ)
% Maximal formula atoms : 33 ( 4 avg)
% Number of connectives : 1204 ( 470 ~; 497 |; 209 &)
% ( 13 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 11 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 192 ( 0 sgn 150 !; 42 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f7,axiom,
! [X0,X1,X2,X3] :
( ( aElement0(X0)
& aRewritingSystem0(X1)
& aElement0(X2)
& aElement0(X3) )
=> ( ( sdtmndtplgtdt0(X0,X1,X2)
& sdtmndtplgtdt0(X2,X1,X3) )
=> sdtmndtplgtdt0(X0,X1,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mTCTrans) ).
fof(f8,axiom,
! [X0,X1,X2] :
( ( aElement0(X0)
& aRewritingSystem0(X1)
& aElement0(X2) )
=> ( sdtmndtasgtdt0(X0,X1,X2)
<=> ( X0 = X2
| sdtmndtplgtdt0(X0,X1,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mTCRDef) ).
fof(f9,axiom,
! [X0,X1,X2,X3] :
( ( aElement0(X0)
& aRewritingSystem0(X1)
& aElement0(X2)
& aElement0(X3) )
=> ( ( sdtmndtasgtdt0(X0,X1,X2)
& sdtmndtasgtdt0(X2,X1,X3) )
=> sdtmndtasgtdt0(X0,X1,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mTCRTrans) ).
fof(f15,axiom,
aRewritingSystem0(xR),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__656) ).
fof(f16,axiom,
( ! [X0,X1,X2] :
( ( aElement0(X0)
& aElement0(X1)
& aElement0(X2)
& aReductOfIn0(X1,X0,xR)
& aReductOfIn0(X2,X0,xR) )
=> ? [X3] :
( aElement0(X3)
& ( X1 = X3
| ( ( aReductOfIn0(X3,X1,xR)
| ? [X4] :
( aElement0(X4)
& aReductOfIn0(X4,X1,xR)
& sdtmndtplgtdt0(X4,xR,X3) ) )
& sdtmndtplgtdt0(X1,xR,X3) ) )
& sdtmndtasgtdt0(X1,xR,X3)
& ( X2 = X3
| ( ( aReductOfIn0(X3,X2,xR)
| ? [X4] :
( aElement0(X4)
& aReductOfIn0(X4,X2,xR)
& sdtmndtplgtdt0(X4,xR,X3) ) )
& sdtmndtplgtdt0(X2,xR,X3) ) )
& sdtmndtasgtdt0(X2,xR,X3) ) )
& isLocallyConfluent0(xR)
& ! [X0,X1] :
( ( aElement0(X0)
& aElement0(X1) )
=> ( ( aReductOfIn0(X1,X0,xR)
| ? [X2] :
( aElement0(X2)
& aReductOfIn0(X2,X0,xR)
& sdtmndtplgtdt0(X2,xR,X1) )
| sdtmndtplgtdt0(X0,xR,X1) )
=> iLess0(X1,X0) ) )
& isTerminating0(xR) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__656_01) ).
fof(f17,axiom,
( aElement0(xa)
& aElement0(xb)
& aElement0(xc) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__731) ).
fof(f18,axiom,
! [X0,X1,X2] :
( ( aElement0(X0)
& aElement0(X1)
& aElement0(X2)
& ( X0 = X1
| aReductOfIn0(X1,X0,xR)
| ? [X3] :
( aElement0(X3)
& aReductOfIn0(X3,X0,xR)
& sdtmndtplgtdt0(X3,xR,X1) )
| sdtmndtplgtdt0(X0,xR,X1)
| sdtmndtasgtdt0(X0,xR,X1) )
& ( X0 = X2
| aReductOfIn0(X2,X0,xR)
| ? [X3] :
( aElement0(X3)
& aReductOfIn0(X3,X0,xR)
& sdtmndtplgtdt0(X3,xR,X2) )
| sdtmndtplgtdt0(X0,xR,X2)
| sdtmndtasgtdt0(X0,xR,X2) ) )
=> ( iLess0(X0,xa)
=> ? [X3] :
( aElement0(X3)
& ( X1 = X3
| ( ( aReductOfIn0(X3,X1,xR)
| ? [X4] :
( aElement0(X4)
& aReductOfIn0(X4,X1,xR)
& sdtmndtplgtdt0(X4,xR,X3) ) )
& sdtmndtplgtdt0(X1,xR,X3) ) )
& sdtmndtasgtdt0(X1,xR,X3)
& ( X2 = X3
| ( ( aReductOfIn0(X3,X2,xR)
| ? [X4] :
( aElement0(X4)
& aReductOfIn0(X4,X2,xR)
& sdtmndtplgtdt0(X4,xR,X3) ) )
& sdtmndtplgtdt0(X2,xR,X3) ) )
& sdtmndtasgtdt0(X2,xR,X3) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__715) ).
fof(f20,axiom,
( aElement0(xu)
& aReductOfIn0(xu,xa,xR)
& ( xu = xb
| ( ( aReductOfIn0(xb,xu,xR)
| ? [X0] :
( aElement0(X0)
& aReductOfIn0(X0,xu,xR)
& sdtmndtplgtdt0(X0,xR,xb) ) )
& sdtmndtplgtdt0(xu,xR,xb) ) )
& sdtmndtasgtdt0(xu,xR,xb) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__755) ).
fof(f22,axiom,
( aElement0(xw)
& ( xu = xw
| ( ( aReductOfIn0(xw,xu,xR)
| ? [X0] :
( aElement0(X0)
& aReductOfIn0(X0,xu,xR)
& sdtmndtplgtdt0(X0,xR,xw) ) )
& sdtmndtplgtdt0(xu,xR,xw) ) )
& sdtmndtasgtdt0(xu,xR,xw)
& ( xv = xw
| ( ( aReductOfIn0(xw,xv,xR)
| ? [X0] :
( aElement0(X0)
& aReductOfIn0(X0,xv,xR)
& sdtmndtplgtdt0(X0,xR,xw) ) )
& sdtmndtplgtdt0(xv,xR,xw) ) )
& sdtmndtasgtdt0(xv,xR,xw) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__799) ).
fof(f23,axiom,
( aElement0(xd)
& ( xw = xd
| ( ( aReductOfIn0(xd,xw,xR)
| ? [X0] :
( aElement0(X0)
& aReductOfIn0(X0,xw,xR)
& sdtmndtplgtdt0(X0,xR,xd) ) )
& sdtmndtplgtdt0(xw,xR,xd) ) )
& sdtmndtasgtdt0(xw,xR,xd)
& ~ ? [X0] : aReductOfIn0(X0,xd,xR)
& aNormalFormOfIn0(xd,xw,xR) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__818) ).
fof(f24,conjecture,
( xb = xd
| aReductOfIn0(xd,xb,xR)
| ? [X0] :
( aElement0(X0)
& aReductOfIn0(X0,xb,xR)
& sdtmndtplgtdt0(X0,xR,xd) )
| sdtmndtplgtdt0(xb,xR,xd)
| sdtmndtasgtdt0(xb,xR,xd) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f25,negated_conjecture,
~ ( xb = xd
| aReductOfIn0(xd,xb,xR)
| ? [X0] :
( aElement0(X0)
& aReductOfIn0(X0,xb,xR)
& sdtmndtplgtdt0(X0,xR,xd) )
| sdtmndtplgtdt0(xb,xR,xd)
| sdtmndtasgtdt0(xb,xR,xd) ),
inference(negated_conjecture,[status(cth)],[f24]) ).
fof(f26,plain,
( ! [X0,X1,X2] :
( ( aElement0(X0)
& aElement0(X1)
& aElement0(X2)
& aReductOfIn0(X1,X0,xR)
& aReductOfIn0(X2,X0,xR) )
=> ? [X3] :
( aElement0(X3)
& ( X1 = X3
| ( ( aReductOfIn0(X3,X1,xR)
| ? [X4] :
( aElement0(X4)
& aReductOfIn0(X4,X1,xR)
& sdtmndtplgtdt0(X4,xR,X3) ) )
& sdtmndtplgtdt0(X1,xR,X3) ) )
& sdtmndtasgtdt0(X1,xR,X3)
& ( X2 = X3
| ( ( aReductOfIn0(X3,X2,xR)
| ? [X5] :
( aElement0(X5)
& aReductOfIn0(X5,X2,xR)
& sdtmndtplgtdt0(X5,xR,X3) ) )
& sdtmndtplgtdt0(X2,xR,X3) ) )
& sdtmndtasgtdt0(X2,xR,X3) ) )
& isLocallyConfluent0(xR)
& ! [X6,X7] :
( ( aElement0(X6)
& aElement0(X7) )
=> ( ( aReductOfIn0(X7,X6,xR)
| ? [X8] :
( aElement0(X8)
& aReductOfIn0(X8,X6,xR)
& sdtmndtplgtdt0(X8,xR,X7) )
| sdtmndtplgtdt0(X6,xR,X7) )
=> iLess0(X7,X6) ) )
& isTerminating0(xR) ),
inference(rectify,[],[f16]) ).
fof(f27,plain,
! [X0,X1,X2] :
( ( aElement0(X0)
& aElement0(X1)
& aElement0(X2)
& ( X0 = X1
| aReductOfIn0(X1,X0,xR)
| ? [X3] :
( aElement0(X3)
& aReductOfIn0(X3,X0,xR)
& sdtmndtplgtdt0(X3,xR,X1) )
| sdtmndtplgtdt0(X0,xR,X1)
| sdtmndtasgtdt0(X0,xR,X1) )
& ( X0 = X2
| aReductOfIn0(X2,X0,xR)
| ? [X4] :
( aElement0(X4)
& aReductOfIn0(X4,X0,xR)
& sdtmndtplgtdt0(X4,xR,X2) )
| sdtmndtplgtdt0(X0,xR,X2)
| sdtmndtasgtdt0(X0,xR,X2) ) )
=> ( iLess0(X0,xa)
=> ? [X5] :
( aElement0(X5)
& ( X1 = X5
| ( ( aReductOfIn0(X5,X1,xR)
| ? [X6] :
( aElement0(X6)
& aReductOfIn0(X6,X1,xR)
& sdtmndtplgtdt0(X6,xR,X5) ) )
& sdtmndtplgtdt0(X1,xR,X5) ) )
& sdtmndtasgtdt0(X1,xR,X5)
& ( X2 = X5
| ( ( aReductOfIn0(X5,X2,xR)
| ? [X7] :
( aElement0(X7)
& aReductOfIn0(X7,X2,xR)
& sdtmndtplgtdt0(X7,xR,X5) ) )
& sdtmndtplgtdt0(X2,xR,X5) ) )
& sdtmndtasgtdt0(X2,xR,X5) ) ) ),
inference(rectify,[],[f18]) ).
fof(f29,plain,
( aElement0(xw)
& ( xu = xw
| ( ( aReductOfIn0(xw,xu,xR)
| ? [X0] :
( aElement0(X0)
& aReductOfIn0(X0,xu,xR)
& sdtmndtplgtdt0(X0,xR,xw) ) )
& sdtmndtplgtdt0(xu,xR,xw) ) )
& sdtmndtasgtdt0(xu,xR,xw)
& ( xv = xw
| ( ( aReductOfIn0(xw,xv,xR)
| ? [X1] :
( aElement0(X1)
& aReductOfIn0(X1,xv,xR)
& sdtmndtplgtdt0(X1,xR,xw) ) )
& sdtmndtplgtdt0(xv,xR,xw) ) )
& sdtmndtasgtdt0(xv,xR,xw) ),
inference(rectify,[],[f22]) ).
fof(f30,plain,
( aElement0(xd)
& ( xw = xd
| ( ( aReductOfIn0(xd,xw,xR)
| ? [X0] :
( aElement0(X0)
& aReductOfIn0(X0,xw,xR)
& sdtmndtplgtdt0(X0,xR,xd) ) )
& sdtmndtplgtdt0(xw,xR,xd) ) )
& sdtmndtasgtdt0(xw,xR,xd)
& ~ ? [X1] : aReductOfIn0(X1,xd,xR)
& aNormalFormOfIn0(xd,xw,xR) ),
inference(rectify,[],[f23]) ).
fof(f41,plain,
! [X0,X1,X2,X3] :
( sdtmndtplgtdt0(X0,X1,X3)
| ~ sdtmndtplgtdt0(X0,X1,X2)
| ~ sdtmndtplgtdt0(X2,X1,X3)
| ~ aElement0(X0)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X2)
| ~ aElement0(X3) ),
inference(ennf_transformation,[],[f7]) ).
fof(f42,plain,
! [X0,X1,X2,X3] :
( sdtmndtplgtdt0(X0,X1,X3)
| ~ sdtmndtplgtdt0(X0,X1,X2)
| ~ sdtmndtplgtdt0(X2,X1,X3)
| ~ aElement0(X0)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X2)
| ~ aElement0(X3) ),
inference(flattening,[],[f41]) ).
fof(f43,plain,
! [X0,X1,X2] :
( ( sdtmndtasgtdt0(X0,X1,X2)
<=> ( X0 = X2
| sdtmndtplgtdt0(X0,X1,X2) ) )
| ~ aElement0(X0)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X2) ),
inference(ennf_transformation,[],[f8]) ).
fof(f44,plain,
! [X0,X1,X2] :
( ( sdtmndtasgtdt0(X0,X1,X2)
<=> ( X0 = X2
| sdtmndtplgtdt0(X0,X1,X2) ) )
| ~ aElement0(X0)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X2) ),
inference(flattening,[],[f43]) ).
fof(f45,plain,
! [X0,X1,X2,X3] :
( sdtmndtasgtdt0(X0,X1,X3)
| ~ sdtmndtasgtdt0(X0,X1,X2)
| ~ sdtmndtasgtdt0(X2,X1,X3)
| ~ aElement0(X0)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X2)
| ~ aElement0(X3) ),
inference(ennf_transformation,[],[f9]) ).
fof(f46,plain,
! [X0,X1,X2,X3] :
( sdtmndtasgtdt0(X0,X1,X3)
| ~ sdtmndtasgtdt0(X0,X1,X2)
| ~ sdtmndtasgtdt0(X2,X1,X3)
| ~ aElement0(X0)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X2)
| ~ aElement0(X3) ),
inference(flattening,[],[f45]) ).
fof(f57,plain,
( ! [X0,X1,X2] :
( ? [X3] :
( aElement0(X3)
& ( X1 = X3
| ( ( aReductOfIn0(X3,X1,xR)
| ? [X4] :
( aElement0(X4)
& aReductOfIn0(X4,X1,xR)
& sdtmndtplgtdt0(X4,xR,X3) ) )
& sdtmndtplgtdt0(X1,xR,X3) ) )
& sdtmndtasgtdt0(X1,xR,X3)
& ( X2 = X3
| ( ( aReductOfIn0(X3,X2,xR)
| ? [X5] :
( aElement0(X5)
& aReductOfIn0(X5,X2,xR)
& sdtmndtplgtdt0(X5,xR,X3) ) )
& sdtmndtplgtdt0(X2,xR,X3) ) )
& sdtmndtasgtdt0(X2,xR,X3) )
| ~ aElement0(X0)
| ~ aElement0(X1)
| ~ aElement0(X2)
| ~ aReductOfIn0(X1,X0,xR)
| ~ aReductOfIn0(X2,X0,xR) )
& isLocallyConfluent0(xR)
& ! [X6,X7] :
( iLess0(X7,X6)
| ( ~ aReductOfIn0(X7,X6,xR)
& ! [X8] :
( ~ aElement0(X8)
| ~ aReductOfIn0(X8,X6,xR)
| ~ sdtmndtplgtdt0(X8,xR,X7) )
& ~ sdtmndtplgtdt0(X6,xR,X7) )
| ~ aElement0(X6)
| ~ aElement0(X7) )
& isTerminating0(xR) ),
inference(ennf_transformation,[],[f26]) ).
fof(f58,plain,
( ! [X0,X1,X2] :
( ? [X3] :
( aElement0(X3)
& ( X1 = X3
| ( ( aReductOfIn0(X3,X1,xR)
| ? [X4] :
( aElement0(X4)
& aReductOfIn0(X4,X1,xR)
& sdtmndtplgtdt0(X4,xR,X3) ) )
& sdtmndtplgtdt0(X1,xR,X3) ) )
& sdtmndtasgtdt0(X1,xR,X3)
& ( X2 = X3
| ( ( aReductOfIn0(X3,X2,xR)
| ? [X5] :
( aElement0(X5)
& aReductOfIn0(X5,X2,xR)
& sdtmndtplgtdt0(X5,xR,X3) ) )
& sdtmndtplgtdt0(X2,xR,X3) ) )
& sdtmndtasgtdt0(X2,xR,X3) )
| ~ aElement0(X0)
| ~ aElement0(X1)
| ~ aElement0(X2)
| ~ aReductOfIn0(X1,X0,xR)
| ~ aReductOfIn0(X2,X0,xR) )
& isLocallyConfluent0(xR)
& ! [X6,X7] :
( iLess0(X7,X6)
| ( ~ aReductOfIn0(X7,X6,xR)
& ! [X8] :
( ~ aElement0(X8)
| ~ aReductOfIn0(X8,X6,xR)
| ~ sdtmndtplgtdt0(X8,xR,X7) )
& ~ sdtmndtplgtdt0(X6,xR,X7) )
| ~ aElement0(X6)
| ~ aElement0(X7) )
& isTerminating0(xR) ),
inference(flattening,[],[f57]) ).
fof(f59,plain,
! [X0,X1,X2] :
( ? [X5] :
( aElement0(X5)
& ( X1 = X5
| ( ( aReductOfIn0(X5,X1,xR)
| ? [X6] :
( aElement0(X6)
& aReductOfIn0(X6,X1,xR)
& sdtmndtplgtdt0(X6,xR,X5) ) )
& sdtmndtplgtdt0(X1,xR,X5) ) )
& sdtmndtasgtdt0(X1,xR,X5)
& ( X2 = X5
| ( ( aReductOfIn0(X5,X2,xR)
| ? [X7] :
( aElement0(X7)
& aReductOfIn0(X7,X2,xR)
& sdtmndtplgtdt0(X7,xR,X5) ) )
& sdtmndtplgtdt0(X2,xR,X5) ) )
& sdtmndtasgtdt0(X2,xR,X5) )
| ~ iLess0(X0,xa)
| ~ aElement0(X0)
| ~ aElement0(X1)
| ~ aElement0(X2)
| ( X0 != X1
& ~ aReductOfIn0(X1,X0,xR)
& ! [X3] :
( ~ aElement0(X3)
| ~ aReductOfIn0(X3,X0,xR)
| ~ sdtmndtplgtdt0(X3,xR,X1) )
& ~ sdtmndtplgtdt0(X0,xR,X1)
& ~ sdtmndtasgtdt0(X0,xR,X1) )
| ( X0 != X2
& ~ aReductOfIn0(X2,X0,xR)
& ! [X4] :
( ~ aElement0(X4)
| ~ aReductOfIn0(X4,X0,xR)
| ~ sdtmndtplgtdt0(X4,xR,X2) )
& ~ sdtmndtplgtdt0(X0,xR,X2)
& ~ sdtmndtasgtdt0(X0,xR,X2) ) ),
inference(ennf_transformation,[],[f27]) ).
fof(f60,plain,
! [X0,X1,X2] :
( ? [X5] :
( aElement0(X5)
& ( X1 = X5
| ( ( aReductOfIn0(X5,X1,xR)
| ? [X6] :
( aElement0(X6)
& aReductOfIn0(X6,X1,xR)
& sdtmndtplgtdt0(X6,xR,X5) ) )
& sdtmndtplgtdt0(X1,xR,X5) ) )
& sdtmndtasgtdt0(X1,xR,X5)
& ( X2 = X5
| ( ( aReductOfIn0(X5,X2,xR)
| ? [X7] :
( aElement0(X7)
& aReductOfIn0(X7,X2,xR)
& sdtmndtplgtdt0(X7,xR,X5) ) )
& sdtmndtplgtdt0(X2,xR,X5) ) )
& sdtmndtasgtdt0(X2,xR,X5) )
| ~ iLess0(X0,xa)
| ~ aElement0(X0)
| ~ aElement0(X1)
| ~ aElement0(X2)
| ( X0 != X1
& ~ aReductOfIn0(X1,X0,xR)
& ! [X3] :
( ~ aElement0(X3)
| ~ aReductOfIn0(X3,X0,xR)
| ~ sdtmndtplgtdt0(X3,xR,X1) )
& ~ sdtmndtplgtdt0(X0,xR,X1)
& ~ sdtmndtasgtdt0(X0,xR,X1) )
| ( X0 != X2
& ~ aReductOfIn0(X2,X0,xR)
& ! [X4] :
( ~ aElement0(X4)
| ~ aReductOfIn0(X4,X0,xR)
| ~ sdtmndtplgtdt0(X4,xR,X2) )
& ~ sdtmndtplgtdt0(X0,xR,X2)
& ~ sdtmndtasgtdt0(X0,xR,X2) ) ),
inference(flattening,[],[f59]) ).
fof(f61,plain,
( aElement0(xd)
& ( xw = xd
| ( ( aReductOfIn0(xd,xw,xR)
| ? [X0] :
( aElement0(X0)
& aReductOfIn0(X0,xw,xR)
& sdtmndtplgtdt0(X0,xR,xd) ) )
& sdtmndtplgtdt0(xw,xR,xd) ) )
& sdtmndtasgtdt0(xw,xR,xd)
& ! [X1] : ~ aReductOfIn0(X1,xd,xR)
& aNormalFormOfIn0(xd,xw,xR) ),
inference(ennf_transformation,[],[f30]) ).
fof(f62,plain,
( xb != xd
& ~ aReductOfIn0(xd,xb,xR)
& ! [X0] :
( ~ aElement0(X0)
| ~ aReductOfIn0(X0,xb,xR)
| ~ sdtmndtplgtdt0(X0,xR,xd) )
& ~ sdtmndtplgtdt0(xb,xR,xd)
& ~ sdtmndtasgtdt0(xb,xR,xd) ),
inference(ennf_transformation,[],[f25]) ).
fof(f69,plain,
! [X2,X3,X0,X1] :
( sdtmndtplgtdt0(X0,X1,X3)
| ~ aElement0(X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0)
| ~ sdtmndtplgtdt0(X2,X1,X3)
| ~ sdtmndtplgtdt0(X0,X1,X2)
| ~ aElement0(X3) ),
inference(cnf_transformation,[],[f42]) ).
fof(f70,plain,
! [X2,X0,X1] :
( ~ sdtmndtasgtdt0(X0,X1,X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0)
| sdtmndtplgtdt0(X0,X1,X2)
| X0 = X2
| ~ aElement0(X2) ),
inference(cnf_transformation,[],[f44]) ).
fof(f71,plain,
! [X2,X0,X1] :
( sdtmndtasgtdt0(X0,X1,X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0)
| ~ sdtmndtplgtdt0(X0,X1,X2)
| ~ aElement0(X2) ),
inference(cnf_transformation,[],[f44]) ).
fof(f72,plain,
! [X2,X0,X1] :
( ~ aElement0(X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0)
| X0 != X2
| sdtmndtasgtdt0(X0,X1,X2) ),
inference(cnf_transformation,[],[f44]) ).
fof(f73,plain,
! [X2,X3,X0,X1] :
( sdtmndtasgtdt0(X0,X1,X3)
| ~ aElement0(X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0)
| ~ sdtmndtasgtdt0(X2,X1,X3)
| ~ sdtmndtasgtdt0(X0,X1,X2)
| ~ aElement0(X3) ),
inference(cnf_transformation,[],[f46]) ).
fof(f102,plain,
aRewritingSystem0(xR),
inference(cnf_transformation,[],[f15]) ).
fof(f116,plain,
! [X6,X7] :
( ~ aReductOfIn0(X7,X6,xR)
| ~ aElement0(X6)
| ~ aElement0(X7)
| iLess0(X7,X6) ),
inference(cnf_transformation,[],[f58]) ).
fof(f120,plain,
aElement0(xb),
inference(cnf_transformation,[],[f17]) ).
fof(f121,plain,
aElement0(xa),
inference(cnf_transformation,[],[f17]) ).
fof(f123,plain,
! [X2,X1] :
( aReductOfIn0(sK19(X1,X2),X1,xR)
| aReductOfIn0(sK17(X1,X2),X1,xR)
| sK17(X1,X2) = X1
| ~ sP16(X2,X1) ),
inference(cnf_transformation,[],[f60]) ).
fof(f130,plain,
! [X2,X1] :
( sdtmndtasgtdt0(X2,xR,sK17(X1,X2))
| ~ sP16(X2,X1) ),
inference(cnf_transformation,[],[f60]) ).
fof(f151,plain,
! [X2,X0,X1] :
( sP16(X2,X1)
| ~ sdtmndtplgtdt0(X0,xR,X1)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0)
| ~ iLess0(X0,xa)
| ~ sdtmndtplgtdt0(X0,xR,X2) ),
inference(cnf_transformation,[],[f60]) ).
fof(f155,plain,
! [X2,X0,X1] :
( sP16(X2,X1)
| ~ sdtmndtplgtdt0(X0,xR,X1)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0)
| ~ iLess0(X0,xa)
| ~ sdtmndtasgtdt0(X0,xR,X2) ),
inference(cnf_transformation,[],[f60]) ).
fof(f167,plain,
( aReductOfIn0(sK22,xu,xR)
| aReductOfIn0(xb,xu,xR)
| xb = xu ),
inference(cnf_transformation,[],[f20]) ).
fof(f169,plain,
( sdtmndtplgtdt0(xu,xR,xb)
| xb = xu ),
inference(cnf_transformation,[],[f20]) ).
fof(f170,plain,
sdtmndtasgtdt0(xu,xR,xb),
inference(cnf_transformation,[],[f20]) ).
fof(f171,plain,
aReductOfIn0(xu,xa,xR),
inference(cnf_transformation,[],[f20]) ).
fof(f172,plain,
aElement0(xu),
inference(cnf_transformation,[],[f20]) ).
fof(f186,plain,
( sdtmndtplgtdt0(xu,xR,xw)
| xu = xw ),
inference(cnf_transformation,[],[f29]) ).
fof(f189,plain,
sdtmndtasgtdt0(xu,xR,xw),
inference(cnf_transformation,[],[f29]) ).
fof(f190,plain,
aElement0(xw),
inference(cnf_transformation,[],[f29]) ).
fof(f194,plain,
( sdtmndtplgtdt0(xw,xR,xd)
| xw = xd ),
inference(cnf_transformation,[],[f61]) ).
fof(f196,plain,
! [X1] : ~ aReductOfIn0(X1,xd,xR),
inference(cnf_transformation,[],[f61]) ).
fof(f197,plain,
sdtmndtasgtdt0(xw,xR,xd),
inference(cnf_transformation,[],[f61]) ).
fof(f198,plain,
aElement0(xd),
inference(cnf_transformation,[],[f61]) ).
fof(f200,plain,
~ sdtmndtasgtdt0(xb,xR,xd),
inference(cnf_transformation,[],[f62]) ).
fof(f204,plain,
! [X2,X1] :
( ~ aElement0(X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X2)
| sdtmndtasgtdt0(X2,X1,X2) ),
inference(equality_resolution,[],[f72]) ).
fof(f224,plain,
! [X2,X1] :
( sdtmndtasgtdt0(X2,X1,X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X2) ),
inference(duplicate_literal_removal,[],[f204]) ).
fof(f244,definition,
( spl27_5
<=> xb = xu ),
introduced(definition,[new_symbols(definition,[spl27_5])],[avatar_definition]) ).
fof(f245,plain,
( xb != xu
| spl27_5 ),
inference(avatar_component_clause,[],[f244]) ).
fof(f246,plain,
( xb = xu
| ~ spl27_5 ),
inference(avatar_component_clause,[],[f244]) ).
fof(f248,definition,
( spl27_6
<=> sdtmndtplgtdt0(xu,xR,xb) ),
introduced(definition,[new_symbols(definition,[spl27_6])],[avatar_definition]) ).
fof(f250,plain,
( sdtmndtplgtdt0(xu,xR,xb)
| ~ spl27_6 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f251,plain,
( spl27_5
| spl27_6 ),
inference(avatar_split_clause,[],[f169,f248,f244]) ).
fof(f272,definition,
( spl27_9
<=> xu = xw ),
introduced(definition,[new_symbols(definition,[spl27_9])],[avatar_definition]) ).
fof(f274,plain,
( xu = xw
| ~ spl27_9 ),
inference(avatar_component_clause,[],[f272]) ).
fof(f276,definition,
( spl27_10
<=> sdtmndtplgtdt0(xu,xR,xw) ),
introduced(definition,[new_symbols(definition,[spl27_10])],[avatar_definition]) ).
fof(f278,plain,
( sdtmndtplgtdt0(xu,xR,xw)
| ~ spl27_10 ),
inference(avatar_component_clause,[],[f276]) ).
fof(f279,plain,
( spl27_9
| spl27_10 ),
inference(avatar_split_clause,[],[f186,f276,f272]) ).
fof(f307,definition,
( spl27_13
<=> xw = xd ),
introduced(definition,[new_symbols(definition,[spl27_13])],[avatar_definition]) ).
fof(f309,plain,
( xw = xd
| ~ spl27_13 ),
inference(avatar_component_clause,[],[f307]) ).
fof(f311,definition,
( spl27_14
<=> sdtmndtplgtdt0(xw,xR,xd) ),
introduced(definition,[new_symbols(definition,[spl27_14])],[avatar_definition]) ).
fof(f313,plain,
( sdtmndtplgtdt0(xw,xR,xd)
| ~ spl27_14 ),
inference(avatar_component_clause,[],[f311]) ).
fof(f314,plain,
( spl27_13
| spl27_14 ),
inference(avatar_split_clause,[],[f194,f311,f307]) ).
fof(f385,plain,
( ! [X0] : ~ aReductOfIn0(X0,xw,xR)
| ~ spl27_13 ),
inference(superposition,[],[f196,f309]) ).
fof(f452,plain,
( ~ aElement0(xa)
| ~ aElement0(xu)
| iLess0(xu,xa) ),
inference(resolution,[],[f116,f171]) ).
fof(f457,plain,
( ~ aElement0(xu)
| iLess0(xu,xa) ),
inference(forward_subsumption_resolution,[],[f452,f121]) ).
fof(f462,plain,
iLess0(xu,xa),
inference(forward_subsumption_resolution,[],[f457,f172]) ).
fof(f475,plain,
( aReductOfIn0(sK22,xu,xR)
| aReductOfIn0(xb,xu,xR)
| spl27_5 ),
inference(forward_subsumption_resolution,[],[f167,f245]) ).
fof(f476,plain,
( aReductOfIn0(sK22,xw,xR)
| aReductOfIn0(xb,xu,xR)
| spl27_5
| ~ spl27_9 ),
inference(forward_demodulation,[],[f475,f274]) ).
fof(f477,plain,
( aReductOfIn0(xb,xu,xR)
| spl27_5
| ~ spl27_9
| ~ spl27_13 ),
inference(forward_subsumption_resolution,[],[f476,f385]) ).
fof(f478,plain,
( aReductOfIn0(xb,xw,xR)
| spl27_5
| ~ spl27_9
| ~ spl27_13 ),
inference(forward_demodulation,[],[f477,f274]) ).
fof(f479,plain,
( $false
| spl27_5
| ~ spl27_9
| ~ spl27_13 ),
inference(forward_subsumption_resolution,[],[f478,f385]) ).
fof(f480,plain,
( spl27_5
| ~ spl27_9
| ~ spl27_13 ),
inference(avatar_contradiction_clause,[],[f479]) ).
fof(f800,plain,
! [X0] :
( aReductOfIn0(sK17(xd,X0),xd,xR)
| xd = sK17(xd,X0)
| ~ sP16(X0,xd) ),
inference(resolution,[],[f123,f196]) ).
fof(f813,plain,
! [X0] :
( ~ sP16(X0,xd)
| xd = sK17(xd,X0) ),
inference(forward_subsumption_resolution,[],[f800,f196]) ).
fof(f936,plain,
! [X0] :
( ~ aElement0(X0)
| ~ aRewritingSystem0(xR)
| ~ aElement0(xb)
| ~ sdtmndtasgtdt0(X0,xR,xd)
| ~ sdtmndtasgtdt0(xb,xR,X0)
| ~ aElement0(xd) ),
inference(resolution,[],[f73,f200]) ).
fof(f939,plain,
! [X2,X3,X0,X1] :
( ~ aElement0(X0)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X2)
| ~ sdtmndtasgtdt0(X0,X1,X3)
| ~ sdtmndtasgtdt0(X2,X1,X0)
| ~ aElement0(X3)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X2)
| sdtmndtplgtdt0(X2,X1,X3)
| X2 = X3
| ~ aElement0(X3) ),
inference(resolution,[],[f73,f70]) ).
fof(f940,plain,
! [X2,X3,X0,X1] :
( sdtmndtplgtdt0(X2,X1,X3)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X2)
| ~ sdtmndtasgtdt0(X0,X1,X3)
| ~ sdtmndtasgtdt0(X2,X1,X0)
| ~ aElement0(X3)
| ~ aElement0(X0)
| X2 = X3 ),
inference(duplicate_literal_removal,[],[f939]) ).
fof(f945,plain,
! [X0] :
( ~ aElement0(X0)
| ~ aElement0(xb)
| ~ sdtmndtasgtdt0(X0,xR,xd)
| ~ sdtmndtasgtdt0(xb,xR,X0)
| ~ aElement0(xd) ),
inference(forward_subsumption_resolution,[],[f936,f102]) ).
fof(f946,plain,
! [X0] :
( ~ aElement0(X0)
| ~ sdtmndtasgtdt0(X0,xR,xd)
| ~ sdtmndtasgtdt0(xb,xR,X0)
| ~ aElement0(xd) ),
inference(forward_subsumption_resolution,[],[f945,f120]) ).
fof(f947,plain,
! [X0] :
( ~ sdtmndtasgtdt0(xb,xR,X0)
| ~ sdtmndtasgtdt0(X0,xR,xd)
| ~ aElement0(X0) ),
inference(forward_subsumption_resolution,[],[f946,f198]) ).
fof(f949,plain,
! [X0] :
( ~ sdtmndtasgtdt0(X0,xR,xd)
| ~ aElement0(X0)
| ~ aRewritingSystem0(xR)
| ~ aElement0(xb)
| ~ sdtmndtplgtdt0(xb,xR,X0)
| ~ aElement0(X0) ),
inference(resolution,[],[f947,f71]) ).
fof(f956,plain,
! [X0] :
( ~ sdtmndtasgtdt0(X0,xR,xd)
| ~ aElement0(X0)
| ~ aRewritingSystem0(xR)
| ~ aElement0(xb)
| ~ sdtmndtplgtdt0(xb,xR,X0) ),
inference(duplicate_literal_removal,[],[f949]) ).
fof(f960,plain,
! [X0] :
( ~ sdtmndtasgtdt0(X0,xR,xd)
| ~ aElement0(X0)
| ~ aElement0(xb)
| ~ sdtmndtplgtdt0(xb,xR,X0) ),
inference(forward_subsumption_resolution,[],[f956,f102]) ).
fof(f964,plain,
! [X0] :
( ~ sdtmndtasgtdt0(X0,xR,xd)
| ~ aElement0(X0)
| ~ sdtmndtplgtdt0(xb,xR,X0) ),
inference(forward_subsumption_resolution,[],[f960,f120]) ).
fof(f1129,plain,
( ~ aElement0(xw)
| ~ sdtmndtplgtdt0(xb,xR,xw) ),
inference(resolution,[],[f964,f197]) ).
fof(f1137,plain,
~ sdtmndtplgtdt0(xb,xR,xw),
inference(forward_subsumption_resolution,[],[f1129,f190]) ).
fof(f2039,plain,
! [X0,X1] :
( xd = sK17(xd,X0)
| ~ sdtmndtplgtdt0(X1,xR,xd)
| ~ aElement0(X0)
| ~ aElement0(xd)
| ~ aElement0(X1)
| ~ iLess0(X1,xa)
| ~ sdtmndtplgtdt0(X1,xR,X0) ),
inference(resolution,[],[f813,f151]) ).
fof(f2052,plain,
! [X0,X1] :
( ~ sdtmndtplgtdt0(X1,xR,xd)
| ~ sdtmndtplgtdt0(X1,xR,X0)
| ~ aElement0(X0)
| ~ aElement0(X1)
| ~ iLess0(X1,xa)
| xd = sK17(xd,X0) ),
inference(forward_subsumption_resolution,[],[f2039,f198]) ).
fof(f3797,plain,
! [X0] :
( ~ aRewritingSystem0(xR)
| ~ aElement0(xb)
| ~ sdtmndtasgtdt0(X0,xR,xw)
| ~ sdtmndtasgtdt0(xb,xR,X0)
| ~ aElement0(xw)
| ~ aElement0(X0)
| xb = xw ),
inference(resolution,[],[f940,f1137]) ).
fof(f3877,plain,
! [X0] :
( ~ aElement0(xb)
| ~ sdtmndtasgtdt0(X0,xR,xw)
| ~ sdtmndtasgtdt0(xb,xR,X0)
| ~ aElement0(xw)
| ~ aElement0(X0)
| xb = xw ),
inference(forward_subsumption_resolution,[],[f3797,f102]) ).
fof(f3923,plain,
! [X0] :
( ~ sdtmndtasgtdt0(X0,xR,xw)
| ~ sdtmndtasgtdt0(xb,xR,X0)
| ~ aElement0(xw)
| ~ aElement0(X0)
| xb = xw ),
inference(forward_subsumption_resolution,[],[f3877,f120]) ).
fof(f3950,plain,
! [X0] :
( ~ sdtmndtasgtdt0(X0,xR,xw)
| ~ sdtmndtasgtdt0(xb,xR,X0)
| ~ aElement0(X0)
| xb = xw ),
inference(forward_subsumption_resolution,[],[f3923,f190]) ).
fof(f3953,definition,
( spl27_35
<=> xb = xw ),
introduced(definition,[new_symbols(definition,[spl27_35])],[avatar_definition]) ).
fof(f3955,plain,
( xb = xw
| ~ spl27_35 ),
inference(avatar_component_clause,[],[f3953]) ).
fof(f3957,definition,
( spl27_36
<=> ! [X0] :
( ~ sdtmndtasgtdt0(X0,xR,xw)
| ~ aElement0(X0)
| ~ sdtmndtasgtdt0(xb,xR,X0) ) ),
introduced(definition,[new_symbols(definition,[spl27_36])],[avatar_definition]) ).
fof(f3958,plain,
( ! [X0] :
( ~ sdtmndtasgtdt0(xb,xR,X0)
| ~ sdtmndtasgtdt0(X0,xR,xw)
| ~ aElement0(X0) )
| ~ spl27_36 ),
inference(avatar_component_clause,[],[f3957]) ).
fof(f3959,plain,
( spl27_35
| spl27_36 ),
inference(avatar_split_clause,[],[f3950,f3957,f3953]) ).
fof(f4075,plain,
( ~ sdtmndtasgtdt0(xw,xR,xd)
| ~ spl27_35 ),
inference(superposition,[],[f200,f3955]) ).
fof(f4167,plain,
( $false
| ~ spl27_35 ),
inference(forward_subsumption_resolution,[],[f4075,f197]) ).
fof(f4168,plain,
~ spl27_35,
inference(avatar_contradiction_clause,[],[f4167]) ).
fof(f4393,plain,
( ~ sdtmndtasgtdt0(xb,xR,xw)
| ~ aElement0(xb)
| ~ aRewritingSystem0(xR)
| ~ aElement0(xb)
| ~ spl27_36 ),
inference(resolution,[],[f3958,f224]) ).
fof(f4402,plain,
( ~ sdtmndtasgtdt0(xb,xR,xw)
| ~ aElement0(xb)
| ~ aRewritingSystem0(xR)
| ~ spl27_36 ),
inference(duplicate_literal_removal,[],[f4393]) ).
fof(f4406,plain,
( ~ sdtmndtasgtdt0(xb,xR,xw)
| ~ aRewritingSystem0(xR)
| ~ spl27_36 ),
inference(forward_subsumption_resolution,[],[f4402,f120]) ).
fof(f4410,plain,
( ~ sdtmndtasgtdt0(xb,xR,xw)
| ~ spl27_36 ),
inference(forward_subsumption_resolution,[],[f4406,f102]) ).
fof(f22799,definition,
( spl27_81
<=> xd = sK17(xd,xb) ),
introduced(definition,[new_symbols(definition,[spl27_81])],[avatar_definition]) ).
fof(f22800,plain,
( xd != sK17(xd,xb)
| spl27_81 ),
inference(avatar_component_clause,[],[f22799]) ).
fof(f22801,plain,
( xd = sK17(xd,xb)
| ~ spl27_81 ),
inference(avatar_component_clause,[],[f22799]) ).
fof(f25032,plain,
( sdtmndtasgtdt0(xb,xR,xd)
| ~ sP16(xb,xd)
| ~ spl27_81 ),
inference(superposition,[],[f130,f22801]) ).
fof(f25078,plain,
( ~ sP16(xb,xd)
| ~ spl27_81 ),
inference(forward_subsumption_resolution,[],[f25032,f200]) ).
fof(f25130,plain,
( ! [X0] :
( ~ sdtmndtplgtdt0(X0,xR,xd)
| ~ aElement0(xb)
| ~ aElement0(xd)
| ~ aElement0(X0)
| ~ iLess0(X0,xa)
| ~ sdtmndtasgtdt0(X0,xR,xb) )
| ~ spl27_81 ),
inference(resolution,[],[f25078,f155]) ).
fof(f25141,plain,
( ! [X0] :
( ~ sdtmndtplgtdt0(X0,xR,xd)
| ~ aElement0(xd)
| ~ aElement0(X0)
| ~ iLess0(X0,xa)
| ~ sdtmndtasgtdt0(X0,xR,xb) )
| ~ spl27_81 ),
inference(forward_subsumption_resolution,[],[f25130,f120]) ).
fof(f25154,plain,
( ! [X0] :
( ~ sdtmndtasgtdt0(X0,xR,xb)
| ~ aElement0(X0)
| ~ iLess0(X0,xa)
| ~ sdtmndtplgtdt0(X0,xR,xd) )
| ~ spl27_81 ),
inference(forward_subsumption_resolution,[],[f25141,f198]) ).
fof(f35078,plain,
( ~ aElement0(xu)
| ~ iLess0(xu,xa)
| ~ sdtmndtplgtdt0(xu,xR,xd)
| ~ spl27_81 ),
inference(resolution,[],[f25154,f170]) ).
fof(f35088,plain,
( ~ iLess0(xu,xa)
| ~ sdtmndtplgtdt0(xu,xR,xd)
| ~ spl27_81 ),
inference(forward_subsumption_resolution,[],[f35078,f172]) ).
fof(f35091,plain,
( ~ sdtmndtplgtdt0(xu,xR,xd)
| ~ spl27_81 ),
inference(forward_subsumption_resolution,[],[f35088,f462]) ).
fof(f35467,plain,
( ! [X0] :
( ~ aElement0(X0)
| ~ aRewritingSystem0(xR)
| ~ aElement0(xu)
| ~ sdtmndtplgtdt0(X0,xR,xd)
| ~ sdtmndtplgtdt0(xu,xR,X0)
| ~ aElement0(xd) )
| ~ spl27_81 ),
inference(resolution,[],[f35091,f69]) ).
fof(f35471,plain,
( ! [X0] :
( ~ aElement0(X0)
| ~ aElement0(xu)
| ~ sdtmndtplgtdt0(X0,xR,xd)
| ~ sdtmndtplgtdt0(xu,xR,X0)
| ~ aElement0(xd) )
| ~ spl27_81 ),
inference(forward_subsumption_resolution,[],[f35467,f102]) ).
fof(f35474,plain,
( ! [X0] :
( ~ aElement0(X0)
| ~ sdtmndtplgtdt0(X0,xR,xd)
| ~ sdtmndtplgtdt0(xu,xR,X0)
| ~ aElement0(xd) )
| ~ spl27_81 ),
inference(forward_subsumption_resolution,[],[f35471,f172]) ).
fof(f35477,plain,
( ! [X0] :
( ~ sdtmndtplgtdt0(xu,xR,X0)
| ~ sdtmndtplgtdt0(X0,xR,xd)
| ~ aElement0(X0) )
| ~ spl27_81 ),
inference(forward_subsumption_resolution,[],[f35474,f198]) ).
fof(f35532,plain,
( ~ sdtmndtplgtdt0(xw,xR,xd)
| ~ aElement0(xw)
| ~ spl27_10
| ~ spl27_81 ),
inference(resolution,[],[f35477,f278]) ).
fof(f35558,plain,
( ~ aElement0(xw)
| ~ spl27_10
| ~ spl27_14
| ~ spl27_81 ),
inference(forward_subsumption_resolution,[],[f35532,f313]) ).
fof(f35566,plain,
( $false
| ~ spl27_10
| ~ spl27_14
| ~ spl27_81 ),
inference(forward_subsumption_resolution,[],[f35558,f190]) ).
fof(f35567,plain,
( ~ spl27_10
| ~ spl27_14
| ~ spl27_81 ),
inference(avatar_contradiction_clause,[],[f35566]) ).
fof(f35629,plain,
( ~ sdtmndtplgtdt0(xw,xR,xd)
| ~ spl27_9
| ~ spl27_81 ),
inference(superposition,[],[f35091,f274]) ).
fof(f35635,plain,
( $false
| ~ spl27_9
| ~ spl27_14
| ~ spl27_81 ),
inference(forward_subsumption_resolution,[],[f35629,f313]) ).
fof(f35636,plain,
( ~ spl27_9
| ~ spl27_14
| ~ spl27_81 ),
inference(avatar_contradiction_clause,[],[f35635]) ).
fof(f44799,definition,
( spl27_120
<=> sdtmndtplgtdt0(xu,xR,xd) ),
introduced(definition,[new_symbols(definition,[spl27_120])],[avatar_definition]) ).
fof(f44800,plain,
( sdtmndtplgtdt0(xu,xR,xd)
| ~ spl27_120 ),
inference(avatar_component_clause,[],[f44799]) ).
fof(f44801,plain,
( ~ sdtmndtplgtdt0(xu,xR,xd)
| spl27_120 ),
inference(avatar_component_clause,[],[f44799]) ).
fof(f46081,plain,
( ! [X0] :
( ~ aElement0(X0)
| ~ aRewritingSystem0(xR)
| ~ aElement0(xu)
| ~ sdtmndtplgtdt0(X0,xR,xd)
| ~ sdtmndtplgtdt0(xu,xR,X0)
| ~ aElement0(xd) )
| spl27_120 ),
inference(resolution,[],[f44801,f69]) ).
fof(f46085,plain,
( ! [X0] :
( ~ aElement0(X0)
| ~ aElement0(xu)
| ~ sdtmndtplgtdt0(X0,xR,xd)
| ~ sdtmndtplgtdt0(xu,xR,X0)
| ~ aElement0(xd) )
| spl27_120 ),
inference(forward_subsumption_resolution,[],[f46081,f102]) ).
fof(f46088,plain,
( ! [X0] :
( ~ aElement0(X0)
| ~ sdtmndtplgtdt0(X0,xR,xd)
| ~ sdtmndtplgtdt0(xu,xR,X0)
| ~ aElement0(xd) )
| spl27_120 ),
inference(forward_subsumption_resolution,[],[f46085,f172]) ).
fof(f46091,plain,
( ! [X0] :
( ~ sdtmndtplgtdt0(xu,xR,X0)
| ~ sdtmndtplgtdt0(X0,xR,xd)
| ~ aElement0(X0) )
| spl27_120 ),
inference(forward_subsumption_resolution,[],[f46088,f198]) ).
fof(f46492,plain,
( ~ sdtmndtplgtdt0(xw,xR,xd)
| ~ aElement0(xw)
| ~ spl27_10
| spl27_120 ),
inference(resolution,[],[f46091,f278]) ).
fof(f46518,plain,
( ~ aElement0(xw)
| ~ spl27_10
| ~ spl27_14
| spl27_120 ),
inference(forward_subsumption_resolution,[],[f46492,f313]) ).
fof(f46526,plain,
( $false
| ~ spl27_10
| ~ spl27_14
| spl27_120 ),
inference(forward_subsumption_resolution,[],[f46518,f190]) ).
fof(f46527,plain,
( ~ spl27_10
| ~ spl27_14
| spl27_120 ),
inference(avatar_contradiction_clause,[],[f46526]) ).
fof(f46881,plain,
( ! [X0] :
( ~ sdtmndtplgtdt0(xu,xR,X0)
| ~ aElement0(X0)
| ~ aElement0(xu)
| ~ iLess0(xu,xa)
| xd = sK17(xd,X0) )
| ~ spl27_120 ),
inference(resolution,[],[f44800,f2052]) ).
fof(f46930,plain,
( ! [X0] :
( ~ sdtmndtplgtdt0(xu,xR,X0)
| ~ aElement0(X0)
| ~ iLess0(xu,xa)
| xd = sK17(xd,X0) )
| ~ spl27_120 ),
inference(forward_subsumption_resolution,[],[f46881,f172]) ).
fof(f46938,plain,
( ! [X0] :
( ~ sdtmndtplgtdt0(xu,xR,X0)
| ~ aElement0(X0)
| xd = sK17(xd,X0) )
| ~ spl27_120 ),
inference(forward_subsumption_resolution,[],[f46930,f462]) ).
fof(f57494,plain,
( ~ aElement0(xb)
| xd = sK17(xd,xb)
| ~ spl27_6
| ~ spl27_120 ),
inference(resolution,[],[f46938,f250]) ).
fof(f57530,plain,
( xd = sK17(xd,xb)
| ~ spl27_6
| ~ spl27_120 ),
inference(forward_subsumption_resolution,[],[f57494,f120]) ).
fof(f57541,plain,
( $false
| ~ spl27_6
| spl27_81
| ~ spl27_120 ),
inference(forward_subsumption_resolution,[],[f57530,f22800]) ).
fof(f57542,plain,
( ~ spl27_6
| spl27_81
| ~ spl27_120 ),
inference(avatar_contradiction_clause,[],[f57541]) ).
fof(f57617,plain,
( ~ sdtmndtplgtdt0(xw,xR,xd)
| ~ spl27_9
| spl27_120 ),
inference(forward_demodulation,[],[f44801,f274]) ).
fof(f57618,plain,
( $false
| ~ spl27_9
| ~ spl27_14
| spl27_120 ),
inference(forward_subsumption_resolution,[],[f57617,f313]) ).
fof(f57619,plain,
( ~ spl27_9
| ~ spl27_14
| spl27_120 ),
inference(avatar_contradiction_clause,[],[f57618]) ).
fof(f57796,plain,
( ~ sdtmndtasgtdt0(xu,xR,xw)
| ~ spl27_5
| ~ spl27_36 ),
inference(superposition,[],[f4410,f246]) ).
fof(f57918,plain,
( $false
| ~ spl27_5
| ~ spl27_36 ),
inference(forward_subsumption_resolution,[],[f57796,f189]) ).
fof(f57919,plain,
( ~ spl27_5
| ~ spl27_36 ),
inference(avatar_contradiction_clause,[],[f57918]) ).
fof(f59341,plain,
( ~ sdtmndtplgtdt0(xu,xR,xw)
| ~ spl27_13
| ~ spl27_81 ),
inference(forward_demodulation,[],[f35091,f309]) ).
fof(f59342,plain,
( $false
| ~ spl27_10
| ~ spl27_13
| ~ spl27_81 ),
inference(forward_subsumption_resolution,[],[f59341,f278]) ).
fof(f59343,plain,
( ~ spl27_10
| ~ spl27_13
| ~ spl27_81 ),
inference(avatar_contradiction_clause,[],[f59342]) ).
fof(f59345,plain,
( ~ sdtmndtplgtdt0(xu,xR,xw)
| ~ spl27_13
| spl27_120 ),
inference(forward_demodulation,[],[f44801,f309]) ).
fof(f59348,plain,
( $false
| ~ spl27_10
| ~ spl27_13
| spl27_120 ),
inference(forward_subsumption_resolution,[],[f59345,f278]) ).
fof(f59349,plain,
( ~ spl27_10
| ~ spl27_13
| spl27_120 ),
inference(avatar_contradiction_clause,[],[f59348]) ).
cnf(s3,plain,
( spl27_5
| spl27_6 ),
inference(sat_conversion,[],[f251]) ).
cnf(s5,plain,
( spl27_9
| spl27_10 ),
inference(sat_conversion,[],[f279]) ).
cnf(s8,plain,
( spl27_13
| spl27_14 ),
inference(sat_conversion,[],[f314]) ).
cnf(s18,plain,
( spl27_5
| ~ spl27_9
| ~ spl27_13 ),
inference(sat_conversion,[],[f480]) ).
cnf(s28,plain,
( spl27_35
| spl27_36 ),
inference(sat_conversion,[],[f3959]) ).
cnf(s33,plain,
~ spl27_35,
inference(sat_conversion,[],[f4168]) ).
cnf(s108,plain,
( ~ spl27_10
| ~ spl27_14
| ~ spl27_81 ),
inference(sat_conversion,[],[f35567]) ).
cnf(s110,plain,
( ~ spl27_9
| ~ spl27_14
| ~ spl27_81 ),
inference(sat_conversion,[],[f35636]) ).
cnf(s139,plain,
( ~ spl27_10
| ~ spl27_14
| spl27_120 ),
inference(sat_conversion,[],[f46527]) ).
cnf(s151,plain,
( ~ spl27_6
| spl27_81
| ~ spl27_120 ),
inference(sat_conversion,[],[f57542]) ).
cnf(s152,plain,
( ~ spl27_9
| ~ spl27_14
| spl27_120 ),
inference(sat_conversion,[],[f57619]) ).
cnf(s154,plain,
( ~ spl27_5
| ~ spl27_36 ),
inference(sat_conversion,[],[f57919]) ).
cnf(s158,plain,
( ~ spl27_10
| ~ spl27_13
| ~ spl27_81 ),
inference(sat_conversion,[],[f59343]) ).
cnf(s159,plain,
( ~ spl27_10
| ~ spl27_13
| spl27_120 ),
inference(sat_conversion,[],[f59349]) ).
cnf(s167,plain,
spl27_36,
inference(rat,[],[s28,s33]) ).
cnf(s168,plain,
~ spl27_5,
inference(rat,[],[s154,s167]) ).
cnf(s177,plain,
( ~ spl27_9
| ~ spl27_13 ),
inference(rat,[],[s18,s168]) ).
cnf(s179,plain,
spl27_6,
inference(rat,[],[s3,s168]) ).
cnf(s180,plain,
( ~ spl27_14
| ~ spl27_10 ),
inference(rat,[],[s151,s108,s139,s179]) ).
cnf(s181,plain,
( ~ spl27_13
| ~ spl27_10 ),
inference(rat,[],[s151,s158,s159,s179]) ).
cnf(s182,plain,
~ spl27_10,
inference(rat,[],[s181,s8,s180]) ).
cnf(s183,plain,
spl27_9,
inference(rat,[],[s5,s182]) ).
cnf(s184,plain,
~ spl27_13,
inference(rat,[],[s177,s183]) ).
cnf(s186,plain,
spl27_14,
inference(rat,[],[s8,s184]) ).
cnf(s187,plain,
spl27_120,
inference(rat,[],[s152,s183,s186]) ).
cnf(s188,plain,
~ spl27_81,
inference(rat,[],[s110,s183,s186]) ).
cnf(s189,plain,
$false,
inference(rat,[],[s151,s179,s187,s188]) ).
fof(f59353,plain,
$false,
inference(avatar_sat_refutation,[],[s189]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM019+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20 % Computer : n013.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 21:45:51 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.23 Running first-order model finding
% 0.08/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.88/3.26 % (1612655)Will run a generic schedule for satisfiability detection.
% 20.88/3.26 % (1612662)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=62641059:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 20.88/3.26 % (1612661)% WARNING: option uhcvi not known.
% 20.88/3.26 % (1612660)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1462286383_2999 on theBenchmark for (2999ds/0Mi)
% 20.88/3.26 % (1612661)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1005436698:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 20.88/3.26 % (1612663)dis+10_1_sil=32000:sp=arity:random_seed=4250885630:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 20.88/3.26 % (1612664)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=806439236:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 20.88/3.26 % (1612665)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2509835965:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 20.88/3.26 % (1612666)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1079487929:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 20.88/3.26 % TRYING [1]
% 20.88/3.26 % TRYING [2]
% 20.88/3.26 % TRYING [3]
% 20.88/3.26 % TRYING [4]
% 20.88/3.26 % TRYING [5]
% 20.88/3.26 % TRYING [6]
% 20.88/3.26 % (1612663)Instruction limit reached!
% 20.88/3.26 % (1612663)------------------------------
% 20.88/3.26 % (1612663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.88/3.26 % (1612663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.26 % (1612663)CaDiCaL version: 2.1.3
% 20.88/3.26 % (1612663)Termination reason: Instruction limit
% 20.88/3.26 % (1612663)Termination phase: Saturation
% 20.88/3.26 % (1612663)Time elapsed: 0.062 s
% 20.88/3.26 % (1612663)Peak memory usage: 12 MB
% 20.88/3.26 % (1612663)Instructions burned: 103 (million)
% 20.88/3.26 % (1612664)Instruction limit reached!
% 20.88/3.26 % (1612664)------------------------------
% 20.88/3.26 % (1612664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.88/3.26 % (1612664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.26 % (1612664)CaDiCaL version: 2.1.3
% 20.88/3.26 % (1612664)Termination reason: Instruction limit
% 20.88/3.26 % (1612664)Termination phase: Saturation
% 20.88/3.26 % (1612664)Time elapsed: 0.066 s
% 20.88/3.26 % (1612664)Peak memory usage: 12 MB
% 20.88/3.26 % (1612664)Instructions burned: 117 (million)
% 20.88/3.26 % (1612674)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1204661187:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 20.88/3.26 % (1612665)Instruction limit reached!
% 20.88/3.26 % (1612665)------------------------------
% 20.88/3.26 % (1612665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.88/3.26 % (1612665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.26 % (1612665)CaDiCaL version: 2.1.3
% 20.88/3.26 % (1612665)Termination reason: Instruction limit
% 20.88/3.26 % (1612665)Termination phase: Saturation
% 20.88/3.26 % (1612665)Time elapsed: 0.075 s
% 20.88/3.26 % (1612665)Peak memory usage: 14 MB
% 20.88/3.26 % (1612665)Instructions burned: 132 (million)
% 20.88/3.26 % (1612675)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2417060656:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 20.88/3.26 % TRYING [1]
% 20.88/3.26 % TRYING [2]
% 20.88/3.26 % TRYING [3]
% 20.88/3.26 % TRYING [4]
% 20.88/3.26 % TRYING [7]
% 20.88/3.26 % (1612678)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1044475047:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 20.88/3.26 % TRYING [5]
% 20.88/3.26 % (1612666)Instruction limit reached!
% 20.88/3.26 % (1612666)------------------------------
% 20.88/3.26 % (1612666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.88/3.26 % (1612666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.26 % (1612666)CaDiCaL version: 2.1.3
% 20.88/3.26 % (1612666)Termination reason: Instruction limit
% 20.88/3.26 % (1612666)Termination phase: Saturation
% 20.88/3.26 % (1612666)Time elapsed: 0.134 s
% 20.88/3.26 % (1612666)Peak memory usage: 14 MB
% 20.88/3.26 % (1612666)Instructions burned: 159 (million)
% 20.88/3.26 % (1612675)Instruction limit reached!
% 20.88/3.26 % (1612675)------------------------------
% 20.88/3.26 % (1612675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.88/3.26 % (1612675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.97/4.28 % (1612675)CaDiCaL version: 2.1.3
% 27.97/4.28 % (1612675)Termination reason: Instruction limit
% 27.97/4.28 % (1612675)Termination phase: Saturation
% 27.97/4.28 % (1612675)Time elapsed: 0.078 s
% 27.97/4.28 % (1612675)Peak memory usage: 14 MB
% 27.97/4.28 % (1612675)Instructions burned: 132 (million)
% 27.97/4.28 % (1612680)ott-21_1_sil=16000:fs=off:random_seed=1556426303:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 27.97/4.28 % TRYING [8]
% 27.97/4.28 % (1612686)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1147086198:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 27.97/4.28 % TRYING [6]
% 27.97/4.28 % TRYING [9]
% 27.97/4.28 % (1612680)Instruction limit reached!
% 27.97/4.28 % (1612680)------------------------------
% 27.97/4.28 % (1612680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.97/4.28 % (1612680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.97/4.28 % (1612680)CaDiCaL version: 2.1.3
% 27.97/4.28 % (1612680)Termination reason: Instruction limit
% 27.97/4.28 % (1612680)Termination phase: Saturation
% 27.97/4.28 % (1612680)Time elapsed: 0.113 s
% 27.97/4.28 % (1612680)Peak memory usage: 13 MB
% 27.97/4.28 % (1612680)Instructions burned: 180 (million)
% 27.97/4.28 % (1612711)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=696324024:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 27.97/4.28 % TRYING [1]
% 27.97/4.28 % TRYING [2]
% 27.97/4.28 % TRYING [3]
% 27.97/4.28 % TRYING [4]
% 27.97/4.28 % TRYING [5]
% 27.97/4.28 % (1612674)Instruction limit reached!
% 27.97/4.28 % (1612674)------------------------------
% 27.97/4.28 % (1612674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.97/4.28 % (1612674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.97/4.28 % (1612674)CaDiCaL version: 2.1.3
% 27.97/4.28 % (1612674)Termination reason: Instruction limit
% 27.97/4.28 % (1612674)Termination phase: Finite model building SAT solving
% 27.97/4.28 % (1612674)Time elapsed: 0.312 s
% 27.97/4.28 % (1612674)Peak memory usage: 27 MB
% 27.97/4.28 % (1612674)Instructions burned: 715 (million)
% 27.97/4.28 % (1612745)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1267695031:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 27.97/4.28 % TRYING [10]
% 27.97/4.28 % TRYING [6]
% 27.97/4.28 % (1612686)Instruction limit reached!
% 27.97/4.28 % (1612686)------------------------------
% 27.97/4.28 % (1612686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.97/4.28 % (1612686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.97/4.28 % (1612686)CaDiCaL version: 2.1.3
% 27.97/4.28 % (1612686)Termination reason: Instruction limit
% 27.97/4.28 % (1612686)Termination phase: Saturation
% 27.97/4.28 % (1612686)Time elapsed: 0.326 s
% 27.97/4.28 % (1612686)Peak memory usage: 15 MB
% 27.97/4.28 % (1612686)Instructions burned: 478 (million)
% 27.97/4.28 % (1612678)Instruction limit reached!
% 27.97/4.28 % (1612678)------------------------------
% 27.97/4.28 % (1612678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.97/4.28 % (1612678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.97/4.28 % (1612678)CaDiCaL version: 2.1.3
% 27.97/4.28 % (1612678)Termination reason: Instruction limit
% 27.97/4.28 % (1612678)Termination phase: Saturation
% 27.97/4.28 % (1612678)Time elapsed: 0.420 s
% 27.97/4.28 % (1612678)Peak memory usage: 20 MB
% 27.97/4.28 % (1612678)Instructions burned: 693 (million)
% 27.97/4.28 % (1612771)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1920461283:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 27.97/4.28 % (1612777)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1596760000:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 27.97/4.28 % TRYING [7]
% 27.97/4.28 % TRYING [14]
% 27.97/4.28 % TRYING [11]
% 27.97/4.28 % (1612711)Instruction limit reached!
% 27.97/4.28 % (1612711)------------------------------
% 27.97/4.28 % (1612711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.97/4.28 % (1612711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.97/4.28 % (1612711)CaDiCaL version: 2.1.3
% 27.97/4.28 % (1612711)Termination reason: Instruction limit
% 27.97/4.28 % (1612711)Termination phase: Finite model building SAT solving
% 27.97/4.28 % (1612711)Time elapsed: 0.371 s
% 27.97/4.28 % (1612711)Peak memory usage: 21 MB
% 27.97/4.28 % (1612711)Instructions burned: 866 (million)
% 27.97/4.28 % (1612810)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=141280244:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 27.97/4.28 % (1612771)Instruction limit reached!
% 27.97/4.28 % (1612771)------------------------------
% 27.97/4.28 % (1612771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.97/4.28 % (1612771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.97/4.28 % (1612771)CaDiCaL version: 2.1.3
% 27.97/4.28 % (1612771)Termination reason: Instruction limit
% 27.97/4.28 % (1612771)Termination phase: Finite model building constraint generation
% 27.97/4.28 % (1612771)Time elapsed: 0.572 s
% 27.97/4.28 % (1612771)Peak memory usage: 73 MB
% 27.97/4.28 % (1612771)Instructions burned: 889 (million)
% 27.97/4.28 % (1612777)Instruction limit reached!
% 27.97/4.28 % (1612777)------------------------------
% 27.97/4.28 % (1612777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.97/4.28 % (1612777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.97/4.28 % (1612777)CaDiCaL version: 2.1.3
% 27.97/4.28 % (1612777)Termination reason: Instruction limit
% 27.97/4.28 % (1612777)Termination phase: Saturation
% 27.97/4.28 % (1612777)Time elapsed: 0.560 s
% 27.97/4.28 % (1612777)Peak memory usage: 21 MB
% 27.97/4.28 % (1612777)Instructions burned: 692 (million)
% 27.97/4.28 % (1612849)fmb+10_1_sil=64000:random_seed=1459909205:i=22061:nm=2:gsp=on_2988 on theBenchmark for (2988ds/22061Mi)
% 27.97/4.28 % TRYING [1]
% 27.97/4.28 % TRYING [2]
% 27.97/4.28 % TRYING [3]
% 27.97/4.28 % TRYING [4]
% 27.97/4.28 % (1612851)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4224652272:i=9515:nm=5_2988 on theBenchmark for (2988ds/9515Mi)
% 27.97/4.28 % TRYING [20]
% 27.97/4.28 % TRYING [5]
% 27.97/4.28 % TRYING [12]
% 27.97/4.28 % TRYING [6]
% 27.97/4.28 % (1612745)Instruction limit reached!
% 27.97/4.28 % (1612745)------------------------------
% 27.97/4.28 % (1612745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.97/4.28 % (1612745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.97/4.28 % (1612745)CaDiCaL version: 2.1.3
% 27.97/4.28 % (1612745)Termination reason: Instruction limit
% 27.97/4.28 % (1612745)Termination phase: Saturation
% 27.97/4.28 % (1612745)Time elapsed: 0.965 s
% 27.97/4.28 % (1612745)Peak memory usage: 22 MB
% 27.97/4.28 % (1612745)Instructions burned: 1179 (million)
% 27.97/4.28 % TRYING [7]
% 27.97/4.28 % (1612856)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1064000691:fmbsr=1.7:i=920_2985 on theBenchmark for (2985ds/920Mi)
% 27.97/4.28 % TRYING [8]
% 27.97/4.28 % (1612810)Instruction limit reached!
% 27.97/4.28 % (1612810)------------------------------
% 27.97/4.28 % (1612810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.97/4.28 % (1612810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.97/4.28 % (1612810)CaDiCaL version: 2.1.3
% 27.97/4.28 % (1612810)Termination reason: Instruction limit
% 27.97/4.28 % (1612810)Termination phase: Saturation
% 27.97/4.28 % (1612810)Time elapsed: 0.795 s
% 27.97/4.28 % (1612810)Peak memory usage: 20 MB
% 27.97/4.28 % (1612810)Instructions burned: 880 (million)
% 27.97/4.28 % (1612860)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=641121746:i=5131_2984 on theBenchmark for (2984ds/5131Mi)
% 27.97/4.28 % TRYING [9]
% 27.97/4.28 % TRYING [8]
% 27.97/4.28 % TRYING [10]
% 27.97/4.28 % TRYING [9]
% 27.97/4.28 % TRYING [13]
% 27.97/4.28 % (1612856)Instruction limit reached!
% 27.97/4.28 % (1612856)------------------------------
% 27.97/4.28 % (1612856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.97/4.28 % (1612856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.97/4.28 % (1612856)CaDiCaL version: 2.1.3
% 27.97/4.28 % (1612856)Termination reason: Instruction limit
% 27.97/4.28 % (1612856)Termination phase: Finite model building constraint generation
% 27.97/4.28 % (1612856)Time elapsed: 0.721 s
% 27.97/4.28 % (1612856)Peak memory usage: 40 MB
% 27.97/4.28 % (1612856)Instructions burned: 920 (million)
% 27.97/4.28 % (1612868)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2382821195:i=1472:ins=7:fdi=8:gsp=on_2978 on theBenchmark for (2978ds/1472Mi)
% 27.97/4.28 % TRYING [10]
% 27.97/4.28 % TRYING [14]
% 27.97/4.28 % TRYING [11]
% 27.97/4.28 % (1612868)Instruction limit reached!
% 27.97/4.28 % (1612868)------------------------------
% 27.97/4.28 % (1612868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.97/4.28 % (1612868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.97/4.28 % (1612868)CaDiCaL version: 2.1.3
% 27.97/4.28 % (1612868)Termination reason: Instruction limit
% 27.97/4.28 % (1612868)Termination phase: Saturation
% 27.97/4.28 % (1612868)Time elapsed: 0.806 s
% 27.97/4.28 % (1612868)Peak memory usage: 29 MB
% 27.97/4.28 % (1612868)Instructions burned: 1473 (million)
% 27.97/4.28 % (1612913)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2142895018:i=6324_2969 on theBenchmark for (2969ds/6324Mi)
% 27.97/4.28 % TRYING [77]
% 27.97/4.28 % TRYING [15]
% 27.97/4.28 % TRYING [12]
% 27.97/4.28 % (1612860) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1612655-1612860"...
% 27.97/4.28 % (1612860)...printing done.
% 27.97/4.28 % (1612860)Refutation found. Thanks to Tanya!
% 27.97/4.28 % SZS status Theorem for theBenchmark
% 27.97/4.28 % SZS output start Proof for theBenchmark
% See solution above
% 27.97/4.29 % (1612860)------------------------------
% 27.97/4.29 % (1612860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.97/4.29 % (1612860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.97/4.29 % (1612860)CaDiCaL version: 2.1.3
% 27.97/4.29 % (1612860)Termination reason: Refutation
% 27.97/4.29 % (1612860)Time elapsed: 2.417 s
% 27.97/4.29 % (1612860)Peak memory usage: 25 MB
% 27.97/4.29 % (1612860)Instructions burned: 4025 (million)
% 27.97/4.29 % (1612655)Success in time 4.043 s
% 27.97/4.29 % Vampire exiting
%------------------------------------------------------------------------------