%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM437+5 : 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 : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:24:18 PM UTC 2026
% Result : Theorem 136.73s 29.13s
% Output : Refutation 136.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 10
% Syntax : Number of formulae : 102 ( 14 unt; 6 def)
% Number of atoms : 566 ( 64 equ)
% Maximal formula atoms : 29 ( 5 avg)
% Number of connectives : 645 ( 181 ~; 227 |; 173 &)
% ( 29 <=>; 35 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 7 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 4 con; 0-2 aty)
% Number of variables : 190 ( 0 sgn 154 !; 36 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f32,axiom,
! [X0] :
( ( aSet0(X0)
& ! [X1] :
( aElementOf0(X1,X0)
=> aSubsetOf0(X1,cS1395) ) )
=> ! [X1] :
( X1 = sbsmnsldt0(X0)
<=> ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X1)
<=> ( aInteger0(X2)
& ? [X3] :
( aElementOf0(X3,X0)
& aElementOf0(X2,X3) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mUnionSet) ).
fof(f34,axiom,
! [X0,X1] :
( ( aInteger0(X0)
& aInteger0(X1)
& X1 != sz00 )
=> ! [X2] :
( X2 = szAzrzSzezqlpdtcmdtrp0(X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aInteger0(X3)
& sdteqdtlpzmzozddtrp0(X3,X0,X1) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mArSeq) ).
fof(f37,axiom,
( aSet0(xS)
& ! [X0] :
( aElementOf0(X0,xS)
=> ( aSet0(cS1395)
& ! [X1] :
( aElementOf0(X1,cS1395)
<=> aInteger0(X1) )
& aSet0(X0)
& ! [X1] :
( aElementOf0(X1,X0)
=> aElementOf0(X1,cS1395) )
& aSubsetOf0(X0,cS1395)
& ! [X1] :
( aElementOf0(X1,X0)
=> ? [X2] :
( aInteger0(X2)
& X2 != sz00
& aSet0(szAzrzSzezqlpdtcmdtrp0(X1,X2))
& ! [X3] :
( ( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
=> ( aInteger0(X3)
& ? [X4] :
( aInteger0(X4)
& sdtasdt0(X2,X4) = sdtpldt0(X3,smndt0(X1)) )
& aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
& sdteqdtlpzmzozddtrp0(X3,X1,X2) ) )
& ( ( aInteger0(X3)
& ( ? [X4] :
( aInteger0(X4)
& sdtasdt0(X2,X4) = sdtpldt0(X3,smndt0(X1)) )
| aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
| sdteqdtlpzmzozddtrp0(X3,X1,X2) ) )
=> aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2)) ) )
& ! [X3] :
( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
=> aElementOf0(X3,X0) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),X0) ) )
& isOpen0(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1750) ).
fof(f38,conjecture,
( ( aSet0(sbsmnsldt0(xS))
& ! [X0] :
( aElementOf0(X0,sbsmnsldt0(xS))
<=> ( aInteger0(X0)
& ? [X1] :
( aElementOf0(X1,xS)
& aElementOf0(X0,X1) ) ) ) )
=> ( ! [X0] :
( aElementOf0(X0,sbsmnsldt0(xS))
=> ? [X1] :
( aInteger0(X1)
& X1 != sz00
& ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(X0,X1))
& ! [X2] :
( ( aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1))
=> ( aInteger0(X2)
& ? [X3] :
( aInteger0(X3)
& sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(X0)) )
& aDivisorOf0(X1,sdtpldt0(X2,smndt0(X0)))
& sdteqdtlpzmzozddtrp0(X2,X0,X1) ) )
& ( ( aInteger0(X2)
& ( ? [X3] :
( aInteger0(X3)
& sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(X0)) )
| aDivisorOf0(X1,sdtpldt0(X2,smndt0(X0)))
| sdteqdtlpzmzozddtrp0(X2,X0,X1) ) )
=> aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1)) ) ) )
=> ( ! [X2] :
( aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1))
=> aElementOf0(X2,sbsmnsldt0(xS)) )
| aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X0,X1),sbsmnsldt0(xS)) ) ) ) )
| isOpen0(sbsmnsldt0(xS)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f39,negated_conjecture,
~ ( ( aSet0(sbsmnsldt0(xS))
& ! [X0] :
( aElementOf0(X0,sbsmnsldt0(xS))
<=> ( aInteger0(X0)
& ? [X1] :
( aElementOf0(X1,xS)
& aElementOf0(X0,X1) ) ) ) )
=> ( ! [X0] :
( aElementOf0(X0,sbsmnsldt0(xS))
=> ? [X1] :
( aInteger0(X1)
& X1 != sz00
& ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(X0,X1))
& ! [X2] :
( ( aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1))
=> ( aInteger0(X2)
& ? [X3] :
( aInteger0(X3)
& sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(X0)) )
& aDivisorOf0(X1,sdtpldt0(X2,smndt0(X0)))
& sdteqdtlpzmzozddtrp0(X2,X0,X1) ) )
& ( ( aInteger0(X2)
& ( ? [X3] :
( aInteger0(X3)
& sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(X0)) )
| aDivisorOf0(X1,sdtpldt0(X2,smndt0(X0)))
| sdteqdtlpzmzozddtrp0(X2,X0,X1) ) )
=> aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1)) ) ) )
=> ( ! [X2] :
( aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1))
=> aElementOf0(X2,sbsmnsldt0(xS)) )
| aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X0,X1),sbsmnsldt0(xS)) ) ) ) )
| isOpen0(sbsmnsldt0(xS)) ) ),
inference(negated_conjecture,[status(cth)],[f38]) ).
fof(f40,plain,
! [X0] :
( ( aSet0(X0)
& ! [X1] :
( aElementOf0(X1,X0)
=> aSubsetOf0(X1,cS1395) ) )
=> ! [X2] :
( sbsmnsldt0(X0) = X2
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aInteger0(X3)
& ? [X4] :
( aElementOf0(X4,X0)
& aElementOf0(X3,X4) ) ) ) ) ) ),
inference(rectify,[],[f32]) ).
fof(f41,plain,
( aSet0(xS)
& ! [X0] :
( aElementOf0(X0,xS)
=> ( aSet0(cS1395)
& ! [X1] :
( aElementOf0(X1,cS1395)
<=> aInteger0(X1) )
& aSet0(X0)
& ! [X2] :
( aElementOf0(X2,X0)
=> aElementOf0(X2,cS1395) )
& aSubsetOf0(X0,cS1395)
& ! [X3] :
( aElementOf0(X3,X0)
=> ? [X4] :
( aInteger0(X4)
& sz00 != X4
& aSet0(szAzrzSzezqlpdtcmdtrp0(X3,X4))
& ! [X5] :
( ( aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(X3,X4))
=> ( aInteger0(X5)
& ? [X6] :
( aInteger0(X6)
& sdtasdt0(X4,X6) = sdtpldt0(X5,smndt0(X3)) )
& aDivisorOf0(X4,sdtpldt0(X5,smndt0(X3)))
& sdteqdtlpzmzozddtrp0(X5,X3,X4) ) )
& ( ( aInteger0(X5)
& ( ? [X7] :
( aInteger0(X7)
& sdtpldt0(X5,smndt0(X3)) = sdtasdt0(X4,X7) )
| aDivisorOf0(X4,sdtpldt0(X5,smndt0(X3)))
| sdteqdtlpzmzozddtrp0(X5,X3,X4) ) )
=> aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(X3,X4)) ) )
& ! [X8] :
( aElementOf0(X8,szAzrzSzezqlpdtcmdtrp0(X3,X4))
=> aElementOf0(X8,X0) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X3,X4),X0) ) )
& isOpen0(X0) ) ) ),
inference(rectify,[],[f37]) ).
fof(f42,plain,
~ ( ( aSet0(sbsmnsldt0(xS))
& ! [X0] :
( aElementOf0(X0,sbsmnsldt0(xS))
<=> ( aInteger0(X0)
& ? [X1] :
( aElementOf0(X1,xS)
& aElementOf0(X0,X1) ) ) ) )
=> ( ! [X2] :
( aElementOf0(X2,sbsmnsldt0(xS))
=> ? [X3] :
( aInteger0(X3)
& sz00 != X3
& ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(X2,X3))
& ! [X4] :
( ( aElementOf0(X4,szAzrzSzezqlpdtcmdtrp0(X2,X3))
=> ( aInteger0(X4)
& ? [X5] :
( aInteger0(X5)
& sdtasdt0(X3,X5) = sdtpldt0(X4,smndt0(X2)) )
& aDivisorOf0(X3,sdtpldt0(X4,smndt0(X2)))
& sdteqdtlpzmzozddtrp0(X4,X2,X3) ) )
& ( ( aInteger0(X4)
& ( ? [X6] :
( aInteger0(X6)
& sdtpldt0(X4,smndt0(X2)) = sdtasdt0(X3,X6) )
| aDivisorOf0(X3,sdtpldt0(X4,smndt0(X2)))
| sdteqdtlpzmzozddtrp0(X4,X2,X3) ) )
=> aElementOf0(X4,szAzrzSzezqlpdtcmdtrp0(X2,X3)) ) ) )
=> ( ! [X7] :
( aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(X2,X3))
=> aElementOf0(X7,sbsmnsldt0(xS)) )
| aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X2,X3),sbsmnsldt0(xS)) ) ) ) )
| isOpen0(sbsmnsldt0(xS)) ) ),
inference(rectify,[],[f39]) ).
fof(f88,plain,
! [X0] :
( ! [X2] :
( sbsmnsldt0(X0) = X2
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aInteger0(X3)
& ? [X4] :
( aElementOf0(X4,X0)
& aElementOf0(X3,X4) ) ) ) ) )
| ~ aSet0(X0)
| ? [X1] :
( ~ aSubsetOf0(X1,cS1395)
& aElementOf0(X1,X0) ) ),
inference(ennf_transformation,[],[f40]) ).
fof(f89,plain,
! [X0] :
( ! [X2] :
( sbsmnsldt0(X0) = X2
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aInteger0(X3)
& ? [X4] :
( aElementOf0(X4,X0)
& aElementOf0(X3,X4) ) ) ) ) )
| ~ aSet0(X0)
| ? [X1] :
( ~ aSubsetOf0(X1,cS1395)
& aElementOf0(X1,X0) ) ),
inference(flattening,[],[f88]) ).
fof(f91,plain,
! [X0,X1] :
( ! [X2] :
( X2 = szAzrzSzezqlpdtcmdtrp0(X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aInteger0(X3)
& sdteqdtlpzmzozddtrp0(X3,X0,X1) ) ) ) )
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1 ),
inference(ennf_transformation,[],[f34]) ).
fof(f92,plain,
! [X0,X1] :
( ! [X2] :
( X2 = szAzrzSzezqlpdtcmdtrp0(X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aInteger0(X3)
& sdteqdtlpzmzozddtrp0(X3,X0,X1) ) ) ) )
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1 ),
inference(flattening,[],[f91]) ).
fof(f95,plain,
( aSet0(xS)
& ! [X0] :
( ( aSet0(cS1395)
& ! [X1] :
( aElementOf0(X1,cS1395)
<=> aInteger0(X1) )
& aSet0(X0)
& ! [X2] :
( aElementOf0(X2,cS1395)
| ~ aElementOf0(X2,X0) )
& aSubsetOf0(X0,cS1395)
& ! [X3] :
( ? [X4] :
( aInteger0(X4)
& sz00 != X4
& aSet0(szAzrzSzezqlpdtcmdtrp0(X3,X4))
& ! [X5] :
( ( ( aInteger0(X5)
& ? [X6] :
( aInteger0(X6)
& sdtasdt0(X4,X6) = sdtpldt0(X5,smndt0(X3)) )
& aDivisorOf0(X4,sdtpldt0(X5,smndt0(X3)))
& sdteqdtlpzmzozddtrp0(X5,X3,X4) )
| ~ aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(X3,X4)) )
& ( aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(X3,X4))
| ~ aInteger0(X5)
| ( ! [X7] :
( ~ aInteger0(X7)
| sdtpldt0(X5,smndt0(X3)) != sdtasdt0(X4,X7) )
& ~ aDivisorOf0(X4,sdtpldt0(X5,smndt0(X3)))
& ~ sdteqdtlpzmzozddtrp0(X5,X3,X4) ) ) )
& ! [X8] :
( aElementOf0(X8,X0)
| ~ aElementOf0(X8,szAzrzSzezqlpdtcmdtrp0(X3,X4)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X3,X4),X0) )
| ~ aElementOf0(X3,X0) )
& isOpen0(X0) )
| ~ aElementOf0(X0,xS) ) ),
inference(ennf_transformation,[],[f41]) ).
fof(f96,plain,
( aSet0(xS)
& ! [X0] :
( ( aSet0(cS1395)
& ! [X1] :
( aElementOf0(X1,cS1395)
<=> aInteger0(X1) )
& aSet0(X0)
& ! [X2] :
( aElementOf0(X2,cS1395)
| ~ aElementOf0(X2,X0) )
& aSubsetOf0(X0,cS1395)
& ! [X3] :
( ? [X4] :
( aInteger0(X4)
& sz00 != X4
& aSet0(szAzrzSzezqlpdtcmdtrp0(X3,X4))
& ! [X5] :
( ( ( aInteger0(X5)
& ? [X6] :
( aInteger0(X6)
& sdtasdt0(X4,X6) = sdtpldt0(X5,smndt0(X3)) )
& aDivisorOf0(X4,sdtpldt0(X5,smndt0(X3)))
& sdteqdtlpzmzozddtrp0(X5,X3,X4) )
| ~ aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(X3,X4)) )
& ( aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(X3,X4))
| ~ aInteger0(X5)
| ( ! [X7] :
( ~ aInteger0(X7)
| sdtpldt0(X5,smndt0(X3)) != sdtasdt0(X4,X7) )
& ~ aDivisorOf0(X4,sdtpldt0(X5,smndt0(X3)))
& ~ sdteqdtlpzmzozddtrp0(X5,X3,X4) ) ) )
& ! [X8] :
( aElementOf0(X8,X0)
| ~ aElementOf0(X8,szAzrzSzezqlpdtcmdtrp0(X3,X4)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X3,X4),X0) )
| ~ aElementOf0(X3,X0) )
& isOpen0(X0) )
| ~ aElementOf0(X0,xS) ) ),
inference(flattening,[],[f95]) ).
fof(f97,plain,
( ? [X2] :
( ! [X3] :
( ~ aInteger0(X3)
| sz00 = X3
| ( ? [X7] :
( ~ aElementOf0(X7,sbsmnsldt0(xS))
& aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(X2,X3)) )
& ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X2,X3),sbsmnsldt0(xS))
& aSet0(szAzrzSzezqlpdtcmdtrp0(X2,X3))
& ! [X4] :
( ( ( aInteger0(X4)
& ? [X5] :
( aInteger0(X5)
& sdtasdt0(X3,X5) = sdtpldt0(X4,smndt0(X2)) )
& aDivisorOf0(X3,sdtpldt0(X4,smndt0(X2)))
& sdteqdtlpzmzozddtrp0(X4,X2,X3) )
| ~ aElementOf0(X4,szAzrzSzezqlpdtcmdtrp0(X2,X3)) )
& ( aElementOf0(X4,szAzrzSzezqlpdtcmdtrp0(X2,X3))
| ~ aInteger0(X4)
| ( ! [X6] :
( ~ aInteger0(X6)
| sdtpldt0(X4,smndt0(X2)) != sdtasdt0(X3,X6) )
& ~ aDivisorOf0(X3,sdtpldt0(X4,smndt0(X2)))
& ~ sdteqdtlpzmzozddtrp0(X4,X2,X3) ) ) ) ) )
& aElementOf0(X2,sbsmnsldt0(xS)) )
& ~ isOpen0(sbsmnsldt0(xS))
& aSet0(sbsmnsldt0(xS))
& ! [X0] :
( aElementOf0(X0,sbsmnsldt0(xS))
<=> ( aInteger0(X0)
& ? [X1] :
( aElementOf0(X1,xS)
& aElementOf0(X0,X1) ) ) ) ),
inference(ennf_transformation,[],[f42]) ).
fof(f98,plain,
( ? [X2] :
( ! [X3] :
( ~ aInteger0(X3)
| sz00 = X3
| ( ? [X7] :
( ~ aElementOf0(X7,sbsmnsldt0(xS))
& aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(X2,X3)) )
& ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X2,X3),sbsmnsldt0(xS))
& aSet0(szAzrzSzezqlpdtcmdtrp0(X2,X3))
& ! [X4] :
( ( ( aInteger0(X4)
& ? [X5] :
( aInteger0(X5)
& sdtasdt0(X3,X5) = sdtpldt0(X4,smndt0(X2)) )
& aDivisorOf0(X3,sdtpldt0(X4,smndt0(X2)))
& sdteqdtlpzmzozddtrp0(X4,X2,X3) )
| ~ aElementOf0(X4,szAzrzSzezqlpdtcmdtrp0(X2,X3)) )
& ( aElementOf0(X4,szAzrzSzezqlpdtcmdtrp0(X2,X3))
| ~ aInteger0(X4)
| ( ! [X6] :
( ~ aInteger0(X6)
| sdtpldt0(X4,smndt0(X2)) != sdtasdt0(X3,X6) )
& ~ aDivisorOf0(X3,sdtpldt0(X4,smndt0(X2)))
& ~ sdteqdtlpzmzozddtrp0(X4,X2,X3) ) ) ) ) )
& aElementOf0(X2,sbsmnsldt0(xS)) )
& ~ isOpen0(sbsmnsldt0(xS))
& aSet0(sbsmnsldt0(xS))
& ! [X0] :
( aElementOf0(X0,sbsmnsldt0(xS))
<=> ( aInteger0(X0)
& ? [X1] :
( aElementOf0(X1,xS)
& aElementOf0(X0,X1) ) ) ) ),
inference(flattening,[],[f97]) ).
fof(f162,plain,
! [X2,X3,X0,X4] :
( ~ aSubsetOf0(sK5(X0),cS1395)
| ~ aSet0(X0)
| ~ aElementOf0(X3,X4)
| ~ aElementOf0(X4,X0)
| ~ aInteger0(X3)
| aElementOf0(X3,X2)
| sbsmnsldt0(X0) != X2 ),
inference(cnf_transformation,[],[f89]) ).
fof(f168,plain,
! [X2,X3,X0,X4] :
( aElementOf0(sK5(X0),X0)
| ~ aSet0(X0)
| ~ aElementOf0(X3,X4)
| ~ aElementOf0(X4,X0)
| ~ aInteger0(X3)
| aElementOf0(X3,X2)
| sbsmnsldt0(X0) != X2 ),
inference(cnf_transformation,[],[f89]) ).
fof(f185,plain,
! [X2,X3,X0,X1] :
( sz00 = X1
| ~ aInteger0(X1)
| ~ aInteger0(X0)
| aInteger0(X3)
| ~ aElementOf0(X3,X2)
| szAzrzSzezqlpdtcmdtrp0(X0,X1) != X2 ),
inference(cnf_transformation,[],[f92]) ).
fof(f206,plain,
! [X3,X0,X8] :
( ~ aElementOf0(X0,xS)
| ~ aElementOf0(X3,X0)
| ~ aElementOf0(X8,szAzrzSzezqlpdtcmdtrp0(X3,sK13(X0,X3)))
| aElementOf0(X8,X0) ),
inference(cnf_transformation,[],[f96]) ).
fof(f209,plain,
! [X3,X0] :
( ~ aElementOf0(X0,xS)
| ~ aElementOf0(X3,X0)
| sz00 != sK13(X0,X3) ),
inference(cnf_transformation,[],[f96]) ).
fof(f210,plain,
! [X3,X0] :
( ~ aElementOf0(X0,xS)
| ~ aElementOf0(X3,X0)
| aInteger0(sK13(X0,X3)) ),
inference(cnf_transformation,[],[f96]) ).
fof(f215,plain,
! [X0] :
( ~ aElementOf0(X0,xS)
| aSubsetOf0(X0,cS1395) ),
inference(cnf_transformation,[],[f96]) ).
fof(f218,plain,
aSet0(xS),
inference(cnf_transformation,[],[f96]) ).
fof(f227,plain,
! [X3] :
( aElementOf0(sK17(X3),szAzrzSzezqlpdtcmdtrp0(sK15,X3))
| sz00 = X3
| ~ aInteger0(X3) ),
inference(cnf_transformation,[],[f98]) ).
fof(f228,plain,
! [X3] :
( ~ aElementOf0(sK17(X3),sbsmnsldt0(xS))
| sz00 = X3
| ~ aInteger0(X3) ),
inference(cnf_transformation,[],[f98]) ).
fof(f232,plain,
! [X0] :
( aElementOf0(X0,sK16(X0))
| ~ aElementOf0(X0,sbsmnsldt0(xS)) ),
inference(cnf_transformation,[],[f98]) ).
fof(f233,plain,
! [X0] :
( aElementOf0(sK16(X0),xS)
| ~ aElementOf0(X0,sbsmnsldt0(xS)) ),
inference(cnf_transformation,[],[f98]) ).
fof(f234,plain,
! [X0] :
( aInteger0(X0)
| ~ aElementOf0(X0,sbsmnsldt0(xS)) ),
inference(cnf_transformation,[],[f98]) ).
fof(f235,plain,
aElementOf0(sK15,sbsmnsldt0(xS)),
inference(cnf_transformation,[],[f98]) ).
fof(f258,plain,
! [X3,X0,X4] :
( aElementOf0(sK5(X0),X0)
| ~ aSet0(X0)
| ~ aElementOf0(X3,X4)
| ~ aElementOf0(X4,X0)
| ~ aInteger0(X3)
| aElementOf0(X3,sbsmnsldt0(X0)) ),
inference(equality_resolution,[],[f168]) ).
fof(f261,plain,
! [X3,X0,X4] :
( ~ aSubsetOf0(sK5(X0),cS1395)
| ~ aSet0(X0)
| ~ aElementOf0(X3,X4)
| ~ aElementOf0(X4,X0)
| ~ aInteger0(X3)
| aElementOf0(X3,sbsmnsldt0(X0)) ),
inference(equality_resolution,[],[f162]) ).
fof(f268,plain,
! [X3,X0,X1] :
( sz00 = X1
| ~ aInteger0(X1)
| ~ aInteger0(X0)
| aInteger0(X3)
| ~ aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X0,X1)) ),
inference(equality_resolution,[],[f185]) ).
fof(f307,plain,
! [X3,X0,X4] :
( ~ aElementOf0(X3,sbsmnsldt0(X0))
| ~ aSet0(X0)
| aElementOf0(X3,X4)
| aElementOf0(X4,X0)
| ~ aInteger0(X3)
| ~ aElementOf0(sK5(X0),X0) ),
inference(consistent_polarity_flipping,[],[f258]) ).
fof(f313,plain,
! [X3,X0,X4] :
( ~ aElementOf0(X3,sbsmnsldt0(X0))
| ~ aSet0(X0)
| aElementOf0(X3,X4)
| aElementOf0(X4,X0)
| ~ aInteger0(X3)
| aSubsetOf0(sK5(X0),cS1395) ),
inference(consistent_polarity_flipping,[],[f261]) ).
fof(f328,plain,
! [X3,X0,X1] :
( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X0,X1))
| ~ aInteger0(X1)
| ~ aInteger0(X0)
| aInteger0(X3)
| sz00 = X1 ),
inference(consistent_polarity_flipping,[],[f268]) ).
fof(f339,plain,
! [X0] :
( ~ aSubsetOf0(X0,cS1395)
| aElementOf0(X0,xS) ),
inference(consistent_polarity_flipping,[],[f215]) ).
fof(f344,plain,
! [X3,X0] :
( aInteger0(sK13(X0,X3))
| aElementOf0(X3,X0)
| aElementOf0(X0,xS) ),
inference(consistent_polarity_flipping,[],[f210]) ).
fof(f345,plain,
! [X3,X0] :
( sz00 != sK13(X0,X3)
| aElementOf0(X3,X0)
| aElementOf0(X0,xS) ),
inference(consistent_polarity_flipping,[],[f209]) ).
fof(f348,plain,
! [X3,X0,X8] :
( aElementOf0(X8,szAzrzSzezqlpdtcmdtrp0(X3,sK13(X0,X3)))
| aElementOf0(X3,X0)
| aElementOf0(X0,xS)
| ~ aElementOf0(X8,X0) ),
inference(consistent_polarity_flipping,[],[f206]) ).
fof(f357,plain,
~ aElementOf0(sK15,sbsmnsldt0(xS)),
inference(consistent_polarity_flipping,[],[f235]) ).
fof(f358,plain,
! [X0] :
( aElementOf0(X0,sbsmnsldt0(xS))
| aInteger0(X0) ),
inference(consistent_polarity_flipping,[],[f234]) ).
fof(f359,plain,
! [X0] :
( ~ aElementOf0(sK16(X0),xS)
| aElementOf0(X0,sbsmnsldt0(xS)) ),
inference(consistent_polarity_flipping,[],[f233]) ).
fof(f360,plain,
! [X0] :
( ~ aElementOf0(X0,sK16(X0))
| aElementOf0(X0,sbsmnsldt0(xS)) ),
inference(consistent_polarity_flipping,[],[f232]) ).
fof(f363,plain,
! [X3] :
( aElementOf0(sK17(X3),sbsmnsldt0(xS))
| sz00 = X3
| ~ aInteger0(X3) ),
inference(consistent_polarity_flipping,[],[f228]) ).
fof(f364,plain,
! [X3] :
( ~ aElementOf0(sK17(X3),szAzrzSzezqlpdtcmdtrp0(sK15,X3))
| sz00 = X3
| ~ aInteger0(X3) ),
inference(consistent_polarity_flipping,[],[f227]) ).
fof(f406,plain,
aInteger0(sK15),
inference(resolution,[],[f358,f357]) ).
fof(f1190,plain,
! [X0] :
( ~ aInteger0(X0)
| ~ aInteger0(sK15)
| aInteger0(sK17(X0))
| sz00 = X0
| sz00 = X0
| ~ aInteger0(X0) ),
inference(resolution,[],[f328,f364]) ).
fof(f1191,plain,
! [X0] :
( ~ aInteger0(X0)
| ~ aInteger0(sK15)
| aInteger0(sK17(X0))
| sz00 = X0 ),
inference(duplicate_literal_removal,[],[f1190]) ).
fof(f1194,plain,
! [X0] :
( ~ aInteger0(X0)
| aInteger0(sK17(X0))
| sz00 = X0 ),
inference(forward_subsumption_resolution,[],[f1191,f406]) ).
fof(f1296,definition,
( spl19_95
<=> aElementOf0(sK5(xS),xS) ),
introduced(definition,[new_symbols(definition,[spl19_95])],[avatar_definition]) ).
fof(f1378,definition,
( spl19_103
<=> aSubsetOf0(sK5(xS),cS1395) ),
introduced(definition,[new_symbols(definition,[spl19_103])],[avatar_definition]) ).
fof(f1380,plain,
( aSubsetOf0(sK5(xS),cS1395)
| ~ spl19_103 ),
inference(avatar_component_clause,[],[f1378]) ).
fof(f1471,plain,
! [X0] :
( aElementOf0(sK15,X0)
| aElementOf0(X0,xS)
| ~ aElementOf0(sK17(sK13(X0,sK15)),X0)
| sz00 = sK13(X0,sK15)
| ~ aInteger0(sK13(X0,sK15)) ),
inference(resolution,[],[f348,f364]) ).
fof(f1472,plain,
! [X0] :
( aElementOf0(sK15,X0)
| aElementOf0(X0,xS)
| ~ aElementOf0(sK17(sK13(X0,sK15)),X0)
| ~ aInteger0(sK13(X0,sK15)) ),
inference(forward_subsumption_resolution,[],[f1471,f345]) ).
fof(f1476,plain,
! [X0] :
( ~ aElementOf0(sK17(sK13(X0,sK15)),X0)
| aElementOf0(X0,xS)
| aElementOf0(sK15,X0) ),
inference(forward_subsumption_resolution,[],[f1472,f344]) ).
fof(f1713,plain,
! [X0,X1] :
( ~ aSet0(xS)
| aElementOf0(sK17(X0),X1)
| aElementOf0(X1,xS)
| ~ aInteger0(sK17(X0))
| ~ aElementOf0(sK5(xS),xS)
| sz00 = X0
| ~ aInteger0(X0) ),
inference(resolution,[],[f307,f363]) ).
fof(f1720,plain,
! [X0,X1] :
( aElementOf0(sK17(X0),X1)
| aElementOf0(X1,xS)
| ~ aInteger0(sK17(X0))
| ~ aElementOf0(sK5(xS),xS)
| sz00 = X0
| ~ aInteger0(X0) ),
inference(forward_subsumption_resolution,[],[f1713,f218]) ).
fof(f1724,definition,
( spl19_131
<=> ! [X0,X1] :
( aElementOf0(sK17(X0),X1)
| ~ aInteger0(X0)
| sz00 = X0
| ~ aInteger0(sK17(X0))
| aElementOf0(X1,xS) ) ),
introduced(definition,[new_symbols(definition,[spl19_131])],[avatar_definition]) ).
fof(f1725,plain,
( ! [X0,X1] :
( aElementOf0(sK17(X0),X1)
| ~ aInteger0(X0)
| sz00 = X0
| ~ aInteger0(sK17(X0))
| aElementOf0(X1,xS) )
| ~ spl19_131 ),
inference(avatar_component_clause,[],[f1724]) ).
fof(f1726,plain,
( ~ spl19_95
| spl19_131 ),
inference(avatar_split_clause,[],[f1720,f1724,f1296]) ).
fof(f1730,plain,
! [X0,X1] :
( ~ aSet0(xS)
| aElementOf0(sK17(X0),X1)
| aElementOf0(X1,xS)
| ~ aInteger0(sK17(X0))
| aSubsetOf0(sK5(xS),cS1395)
| sz00 = X0
| ~ aInteger0(X0) ),
inference(resolution,[],[f313,f363]) ).
fof(f1737,plain,
! [X0,X1] :
( aElementOf0(sK17(X0),X1)
| aElementOf0(X1,xS)
| ~ aInteger0(sK17(X0))
| aSubsetOf0(sK5(xS),cS1395)
| sz00 = X0
| ~ aInteger0(X0) ),
inference(forward_subsumption_resolution,[],[f1730,f218]) ).
fof(f1740,plain,
( spl19_103
| spl19_131 ),
inference(avatar_split_clause,[],[f1737,f1724,f1378]) ).
fof(f6372,plain,
( aElementOf0(sK5(xS),xS)
| ~ spl19_103 ),
inference(resolution,[],[f1380,f339]) ).
fof(f6386,plain,
( ! [X0,X1] :
( aElementOf0(sK17(X0),X1)
| ~ aInteger0(X0)
| sz00 = X0
| aElementOf0(X1,xS) )
| ~ spl19_131 ),
inference(forward_subsumption_resolution,[],[f1725,f1194]) ).
fof(f6390,plain,
( ! [X0] :
( ~ aInteger0(sK13(X0,sK15))
| sz00 = sK13(X0,sK15)
| aElementOf0(X0,xS)
| aElementOf0(X0,xS)
| aElementOf0(sK15,X0) )
| ~ spl19_131 ),
inference(resolution,[],[f6386,f1476]) ).
fof(f6410,plain,
( ! [X0] :
( ~ aInteger0(sK13(X0,sK15))
| sz00 = sK13(X0,sK15)
| aElementOf0(X0,xS)
| aElementOf0(sK15,X0) )
| ~ spl19_131 ),
inference(duplicate_literal_removal,[],[f6390]) ).
fof(f6425,plain,
( ! [X0] :
( sz00 = sK13(X0,sK15)
| aElementOf0(X0,xS)
| aElementOf0(sK15,X0) )
| ~ spl19_131 ),
inference(forward_subsumption_resolution,[],[f6410,f344]) ).
fof(f6428,plain,
( ! [X0] :
( aElementOf0(X0,xS)
| aElementOf0(sK15,X0) )
| ~ spl19_131 ),
inference(forward_subsumption_resolution,[],[f6425,f345]) ).
fof(f6766,definition,
( spl19_513
<=> ! [X0] :
( aElementOf0(sK15,X0)
| aElementOf0(X0,xS) ) ),
introduced(definition,[new_symbols(definition,[spl19_513])],[avatar_definition]) ).
fof(f6767,plain,
( ! [X0] :
( aElementOf0(sK15,X0)
| aElementOf0(X0,xS) )
| ~ spl19_513 ),
inference(avatar_component_clause,[],[f6766]) ).
fof(f26353,plain,
( spl19_513
| ~ spl19_131 ),
inference(avatar_split_clause,[],[f6428,f1724,f6766]) ).
fof(f26706,plain,
( spl19_95
| ~ spl19_103 ),
inference(avatar_split_clause,[],[f6372,f1378,f1296]) ).
fof(f171772,definition,
( spl19_11954
<=> aElementOf0(sK15,sK16(sK15)) ),
introduced(definition,[new_symbols(definition,[spl19_11954])],[avatar_definition]) ).
fof(f171773,plain,
( ~ aElementOf0(sK15,sK16(sK15))
| spl19_11954 ),
inference(avatar_component_clause,[],[f171772]) ).
fof(f171774,plain,
( aElementOf0(sK15,sK16(sK15))
| ~ spl19_11954 ),
inference(avatar_component_clause,[],[f171772]) ).
fof(f172532,plain,
( aElementOf0(sK15,sbsmnsldt0(xS))
| ~ spl19_11954 ),
inference(resolution,[],[f171774,f360]) ).
fof(f172533,plain,
( $false
| ~ spl19_11954 ),
inference(forward_subsumption_resolution,[],[f172532,f357]) ).
fof(f172534,plain,
~ spl19_11954,
inference(avatar_contradiction_clause,[],[f172533]) ).
fof(f244446,definition,
( spl19_16070
<=> aElementOf0(sK16(sK15),xS) ),
introduced(definition,[new_symbols(definition,[spl19_16070])],[avatar_definition]) ).
fof(f244447,plain,
( ~ aElementOf0(sK16(sK15),xS)
| spl19_16070 ),
inference(avatar_component_clause,[],[f244446]) ).
fof(f244448,plain,
( aElementOf0(sK16(sK15),xS)
| ~ spl19_16070 ),
inference(avatar_component_clause,[],[f244446]) ).
fof(f521520,plain,
( aElementOf0(sK15,sbsmnsldt0(xS))
| ~ spl19_16070 ),
inference(resolution,[],[f244448,f359]) ).
fof(f521527,plain,
( $false
| ~ spl19_16070 ),
inference(forward_subsumption_resolution,[],[f521520,f357]) ).
fof(f521528,plain,
~ spl19_16070,
inference(avatar_contradiction_clause,[],[f521527]) ).
fof(f521544,plain,
( aElementOf0(sK15,sK16(sK15))
| ~ spl19_513
| spl19_16070 ),
inference(resolution,[],[f244447,f6767]) ).
fof(f521656,plain,
( $false
| ~ spl19_513
| spl19_11954
| spl19_16070 ),
inference(forward_subsumption_resolution,[],[f521544,f171773]) ).
fof(f521657,plain,
( ~ spl19_513
| spl19_11954
| spl19_16070 ),
inference(avatar_contradiction_clause,[],[f521656]) ).
cnf(s105,plain,
( ~ spl19_95
| spl19_131 ),
inference(sat_conversion,[],[f1726]) ).
cnf(s108,plain,
( spl19_103
| spl19_131 ),
inference(sat_conversion,[],[f1740]) ).
cnf(s1931,plain,
( ~ spl19_131
| spl19_513 ),
inference(sat_conversion,[],[f26353]) ).
cnf(s2047,plain,
( spl19_95
| ~ spl19_103 ),
inference(sat_conversion,[],[f26706]) ).
cnf(s15050,plain,
~ spl19_11954,
inference(sat_conversion,[],[f172534]) ).
cnf(s39253,plain,
~ spl19_16070,
inference(sat_conversion,[],[f521528]) ).
cnf(s39254,plain,
( ~ spl19_513
| spl19_11954
| spl19_16070 ),
inference(sat_conversion,[],[f521657]) ).
cnf(s39309,plain,
~ spl19_513,
inference(rat,[],[s39254,s39253,s15050]) ).
cnf(s39333,plain,
~ spl19_131,
inference(rat,[],[s1931,s39309]) ).
cnf(s39337,plain,
spl19_103,
inference(rat,[],[s108,s39333]) ).
cnf(s39338,plain,
spl19_95,
inference(rat,[],[s2047,s39337]) ).
cnf(s39351,plain,
$false,
inference(rat,[],[s105,s39333,s39338]) ).
fof(f521665,plain,
$false,
inference(avatar_sat_refutation,[],[s39351]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM437+5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.36 % Computer : n016.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 27 19:59:17 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.39 Running first-order model finding
% 0.13/0.39 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
% 14.86/2.54 % (2955503)Will run a generic schedule for satisfiability detection.
% 14.86/2.54 % (2955511)dis+10_1_sil=32000:sp=arity:random_seed=1164291929:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.86/2.54 % (2955509)% WARNING: option uhcvi not known.
% 14.86/2.54 % (2955508)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3384267737_2999 on theBenchmark for (2999ds/0Mi)
% 14.86/2.54 % (2955509)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=557662911:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.86/2.54 % (2955510)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2490587799:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.86/2.54 % (2955514)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3401719607:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.86/2.54 % (2955512)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3639113683:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.86/2.54 % (2955513)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2760617883:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.86/2.54 % TRYING [1]
% 14.86/2.54 % TRYING [2]
% 14.86/2.54 % TRYING [3]
% 14.86/2.54 % (2955511)Instruction limit reached!
% 14.86/2.54 % (2955511)------------------------------
% 14.86/2.54 % (2955511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.86/2.54 % (2955511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.86/2.54 % (2955511)CaDiCaL version: 2.1.3
% 14.86/2.54 % (2955511)Termination reason: Instruction limit
% 14.86/2.54 % (2955511)Termination phase: Saturation
% 14.86/2.54 % (2955511)Time elapsed: 0.034 s
% 14.86/2.54 % (2955511)Peak memory usage: 13 MB
% 14.86/2.54 % (2955511)Instructions burned: 105 (million)
% 14.86/2.54 % (2955522)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1808262722:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.86/2.54 % TRYING [4]
% 14.86/2.54 % TRYING [1]
% 14.86/2.54 % TRYING [2]
% 14.86/2.54 % TRYING [3]
% 14.86/2.54 % TRYING [4]
% 14.86/2.54 % (2955512)Instruction limit reached!
% 14.86/2.54 % (2955512)------------------------------
% 14.86/2.54 % (2955512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.86/2.54 % (2955512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.86/2.54 % (2955512)CaDiCaL version: 2.1.3
% 14.86/2.54 % (2955512)Termination reason: Instruction limit
% 14.86/2.54 % (2955512)Termination phase: Saturation
% 14.86/2.54 % (2955512)Time elapsed: 0.069 s
% 14.86/2.54 % (2955512)Peak memory usage: 12 MB
% 14.86/2.54 % (2955512)Instructions burned: 118 (million)
% 14.86/2.54 % (2955513)Instruction limit reached!
% 14.86/2.54 % (2955513)------------------------------
% 14.86/2.54 % (2955513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.86/2.54 % (2955513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.86/2.54 % (2955513)CaDiCaL version: 2.1.3
% 14.86/2.54 % (2955513)Termination reason: Instruction limit
% 14.86/2.54 % (2955513)Termination phase: Saturation
% 14.86/2.54 % (2955513)Time elapsed: 0.077 s
% 14.86/2.54 % (2955513)Peak memory usage: 13 MB
% 14.86/2.54 % (2955513)Instructions burned: 131 (million)
% 14.86/2.54 % (2955514)Instruction limit reached!
% 14.86/2.54 % (2955514)------------------------------
% 14.86/2.54 % (2955514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.86/2.54 % (2955514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.86/2.54 % (2955514)CaDiCaL version: 2.1.3
% 14.86/2.54 % (2955514)Termination reason: Instruction limit
% 14.86/2.54 % (2955514)Termination phase: Saturation
% 14.86/2.54 % (2955514)Time elapsed: 0.086 s
% 14.86/2.54 % (2955514)Peak memory usage: 15 MB
% 14.86/2.54 % (2955514)Instructions burned: 160 (million)
% 14.86/2.54 % (2955524)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1631863126:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 14.86/2.54 % TRYING [5]
% 14.86/2.54 % (2955525)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=195657275:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.86/2.54 % TRYING [5]
% 14.86/2.54 % (2955526)ott-21_1_sil=16000:fs=off:random_seed=729963667:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.86/2.54 % (2955524)Instruction limit reached!
% 14.86/2.54 % (2955524)------------------------------
% 14.86/2.54 % (2955524)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.79/6.31 % (2955524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.79/6.31 % (2955524)CaDiCaL version: 2.1.3
% 41.79/6.31 % (2955524)Termination reason: Instruction limit
% 41.79/6.31 % (2955524)Termination phase: Saturation
% 41.79/6.31 % (2955524)Time elapsed: 0.076 s
% 41.79/6.31 % (2955524)Peak memory usage: 13 MB
% 41.79/6.31 % (2955524)Instructions burned: 132 (million)
% 41.79/6.31 % (2955530)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=588615743:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 41.79/6.31 % (2955526)Instruction limit reached!
% 41.79/6.31 % (2955526)------------------------------
% 41.79/6.31 % (2955526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.79/6.31 % (2955526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.79/6.31 % (2955526)CaDiCaL version: 2.1.3
% 41.79/6.31 % (2955526)Termination reason: Instruction limit
% 41.79/6.31 % (2955526)Termination phase: Saturation
% 41.79/6.31 % (2955526)Time elapsed: 0.088 s
% 41.79/6.31 % (2955526)Peak memory usage: 12 MB
% 41.79/6.31 % (2955526)Instructions burned: 182 (million)
% 41.79/6.31 % TRYING [6]
% 41.79/6.31 % (2955522)Instruction limit reached!
% 41.79/6.31 % (2955522)------------------------------
% 41.79/6.31 % (2955522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.79/6.31 % (2955522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.79/6.31 % (2955522)CaDiCaL version: 2.1.3
% 41.79/6.31 % (2955522)Termination reason: Instruction limit
% 41.79/6.31 % (2955522)Termination phase: Finite model building constraint generation
% 41.79/6.31 % (2955522)Time elapsed: 0.168 s
% 41.79/6.31 % (2955522)Peak memory usage: 33 MB
% 41.79/6.31 % (2955522)Instructions burned: 728 (million)
% 41.79/6.31 % (2955532)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2880443729:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 41.79/6.31 % (2955533)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3743270045:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 41.79/6.31 % TRYING [1]
% 41.79/6.31 % TRYING [2]
% 41.79/6.31 % TRYING [3]
% 41.79/6.31 % TRYING [6]
% 41.79/6.31 % TRYING [4]
% 41.79/6.31 % (2955525)Instruction limit reached!
% 41.79/6.31 % (2955525)------------------------------
% 41.79/6.31 % (2955525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.79/6.31 % (2955525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.79/6.31 % (2955525)CaDiCaL version: 2.1.3
% 41.79/6.31 % (2955525)Termination reason: Instruction limit
% 41.79/6.31 % (2955525)Termination phase: Saturation
% 41.79/6.31 % (2955525)Time elapsed: 0.304 s
% 41.79/6.31 % (2955525)Peak memory usage: 16 MB
% 41.79/6.31 % (2955525)Instructions burned: 685 (million)
% 41.79/6.31 % (2955536)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1478855831:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 41.79/6.31 % TRYING [5]
% 41.79/6.31 % (2955530)Instruction limit reached!
% 41.79/6.31 % (2955530)------------------------------
% 41.79/6.31 % (2955530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.79/6.31 % (2955530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.79/6.31 % (2955530)CaDiCaL version: 2.1.3
% 41.79/6.31 % (2955530)Termination reason: Instruction limit
% 41.79/6.31 % (2955530)Termination phase: Saturation
% 41.79/6.31 % (2955530)Time elapsed: 0.321 s
% 41.79/6.31 % (2955530)Peak memory usage: 15 MB
% 41.79/6.31 % (2955530)Instructions burned: 477 (million)
% 41.79/6.31 % (2955538)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=285436578: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)
% 41.79/6.31 % (2955532)Instruction limit reached!
% 41.79/6.31 % (2955532)------------------------------
% 41.79/6.31 % (2955532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.79/6.31 % (2955532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.79/6.31 % (2955532)CaDiCaL version: 2.1.3
% 41.79/6.31 % (2955532)Termination reason: Instruction limit
% 41.79/6.31 % (2955532)Termination phase: Finite model building constraint generation
% 41.79/6.31 % (2955532)Time elapsed: 0.337 s
% 41.79/6.31 % (2955532)Peak memory usage: 24 MB
% 41.79/6.31 % (2955532)Instructions burned: 865 (million)
% 41.79/6.31 % (2955540)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3658942886:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 41.79/6.31 % (2955533)Instruction limit reached!
% 83.14/12.16 % (2955533)------------------------------
% 83.14/12.16 % (2955533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.14/12.16 % (2955533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.14/12.16 % (2955533)CaDiCaL version: 2.1.3
% 83.14/12.16 % (2955533)Termination reason: Instruction limit
% 83.14/12.16 % (2955533)Termination phase: Saturation
% 83.14/12.16 % (2955533)Time elapsed: 0.367 s
% 83.14/12.16 % (2955533)Peak memory usage: 24 MB
% 83.14/12.16 % (2955533)Instructions burned: 1181 (million)
% 83.14/12.16 % (2955542)fmb+10_1_sil=64000:random_seed=3200996354:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 83.14/12.16 % TRYING [1]
% 83.14/12.16 % TRYING [2]
% 83.14/12.16 % TRYING [3]
% 83.14/12.16 % TRYING [4]
% 83.14/12.16 % TRYING [14]
% 83.14/12.16 % TRYING [5]
% 83.14/12.16 % (2955536)Instruction limit reached!
% 83.14/12.16 % (2955536)------------------------------
% 83.14/12.16 % (2955536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.14/12.16 % (2955536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.14/12.16 % (2955536)CaDiCaL version: 2.1.3
% 83.14/12.16 % (2955536)Termination reason: Instruction limit
% 83.14/12.16 % (2955536)Termination phase: Finite model building constraint generation
% 83.14/12.16 % (2955536)Time elapsed: 0.373 s
% 83.14/12.16 % (2955536)Peak memory usage: 90 MB
% 83.14/12.16 % (2955536)Instructions burned: 891 (million)
% 83.14/12.16 % TRYING [7]
% 83.14/12.16 % (2955544)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=453165649:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 83.14/12.16 % TRYING [20]
% 83.14/12.16 % (2955538)Instruction limit reached!
% 83.14/12.16 % (2955538)------------------------------
% 83.14/12.16 % (2955538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.14/12.16 % (2955538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.14/12.16 % (2955538)CaDiCaL version: 2.1.3
% 83.14/12.16 % (2955538)Termination reason: Instruction limit
% 83.14/12.16 % (2955538)Termination phase: Saturation
% 83.14/12.16 % (2955538)Time elapsed: 0.420 s
% 83.14/12.16 % (2955538)Peak memory usage: 20 MB
% 83.14/12.16 % (2955538)Instructions burned: 693 (million)
% 83.14/12.16 % TRYING [6]
% 83.14/12.16 % (2955546)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=795146440:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 83.14/12.16 % TRYING [8]
% 83.14/12.16 % (2955540)Instruction limit reached!
% 83.14/12.16 % (2955540)------------------------------
% 83.14/12.16 % (2955540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.14/12.16 % (2955540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.14/12.16 % (2955540)CaDiCaL version: 2.1.3
% 83.14/12.16 % (2955540)Termination reason: Instruction limit
% 83.14/12.16 % (2955540)Termination phase: Saturation
% 83.14/12.16 % (2955540)Time elapsed: 0.498 s
% 83.14/12.16 % (2955540)Peak memory usage: 20 MB
% 83.14/12.16 % (2955540)Instructions burned: 882 (million)
% 83.14/12.16 % (2955548)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1373652125:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 83.14/12.16 % (2955546)Instruction limit reached!
% 83.14/12.16 % (2955546)------------------------------
% 83.14/12.16 % (2955546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.14/12.16 % (2955546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.14/12.16 % (2955546)CaDiCaL version: 2.1.3
% 83.14/12.16 % (2955546)Termination reason: Instruction limit
% 83.14/12.16 % (2955546)Termination phase: Finite model building constraint generation
% 83.14/12.16 % (2955546)Time elapsed: 0.345 s
% 83.14/12.16 % (2955546)Peak memory usage: 79 MB
% 83.14/12.16 % (2955546)Instructions burned: 921 (million)
% 83.14/12.16 % (2955550)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1233041527:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 83.14/12.16 % (2955550)Instruction limit reached!
% 83.14/12.16 % (2955550)------------------------------
% 83.14/12.16 % (2955550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.14/12.16 % (2955550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.14/12.16 % (2955550)CaDiCaL version: 2.1.3
% 83.14/12.16 % (2955550)Termination reason: Instruction limit
% 83.14/12.16 % (2955550)Termination phase: Saturation
% 83.14/12.16 % (2955550)Time elapsed: 0.746 s
% 83.14/12.16 % (2955550)Peak memory usage: 24 MB
% 83.14/12.16 % (2955550)Instructions burned: 1474 (million)
% 83.14/12.16 % (2955552)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=174941252:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 136.73/29.13 % TRYING [77]
% 136.73/29.13 % TRYING [7]
% 136.73/29.13 % TRYING [8]
% 136.73/29.13 % (2955548)Instruction limit reached!
% 136.73/29.13 % (2955548)------------------------------
% 136.73/29.13 % (2955548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.73/29.13 % (2955548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.73/29.13 % (2955548)CaDiCaL version: 2.1.3
% 136.73/29.13 % (2955548)Termination reason: Instruction limit
% 136.73/29.13 % (2955548)Termination phase: Saturation
% 136.73/29.13 % (2955548)Time elapsed: 2.691 s
% 136.73/29.13 % (2955548)Peak memory usage: 32 MB
% 136.73/29.13 % (2955548)Instructions burned: 5132 (million)
% 136.73/29.13 % (2955554)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2276760729:fmbsr=2.30978:i=2174_2961 on theBenchmark for (2961ds/2174Mi)
% 136.73/29.13 % TRYING [16]
% 136.73/29.13 % (2955544)Instruction limit reached!
% 136.73/29.13 % (2955544)------------------------------
% 136.73/29.13 % (2955544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.73/29.13 % (2955544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.73/29.13 % (2955544)CaDiCaL version: 2.1.3
% 136.73/29.13 % (2955544)Termination reason: Instruction limit
% 136.73/29.13 % (2955544)Termination phase: Finite model building constraint generation
% 136.73/29.13 % (2955544)Time elapsed: 3.253 s
% 136.73/29.13 % (2955544)Peak memory usage: 519 MB
% 136.73/29.13 % (2955544)Instructions burned: 9518 (million)
% 136.73/29.13 % (2955556)ott-2_1_sil=16000:newcnf=on:random_seed=4091407903:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2958 on theBenchmark for (2958ds/869Mi)
% 136.73/29.13 % TRYING [8]
% 136.73/29.13 % (2955552)Instruction limit reached!
% 136.73/29.13 % (2955552)------------------------------
% 136.73/29.13 % (2955552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.73/29.13 % (2955552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.73/29.13 % (2955552)CaDiCaL version: 2.1.3
% 136.73/29.13 % (2955552)Termination reason: Instruction limit
% 136.73/29.13 % (2955552)Termination phase: Finite model building constraint generation
% 136.73/29.13 % (2955552)Time elapsed: 2.182 s
% 136.73/29.13 % (2955552)Peak memory usage: 406 MB
% 136.73/29.13 % (2955552)Instructions burned: 6325 (million)
% 136.73/29.13 % (2955558)ott+10_1_sil=32000:tgt=ground:random_seed=1445952796:i=5114:av=off_2956 on theBenchmark for (2956ds/5114Mi)
% 136.73/29.13 % (2955554)Instruction limit reached!
% 136.73/29.13 % (2955554)------------------------------
% 136.73/29.13 % (2955554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.73/29.13 % (2955554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.73/29.13 % (2955554)CaDiCaL version: 2.1.3
% 136.73/29.13 % (2955554)Termination reason: Instruction limit
% 136.73/29.13 % (2955554)Termination phase: Finite model building constraint generation
% 136.73/29.13 % (2955554)Time elapsed: 0.767 s
% 136.73/29.13 % (2955554)Peak memory usage: 136 MB
% 136.73/29.13 % (2955554)Instructions burned: 2182 (million)
% 136.73/29.13 % (2955556)Instruction limit reached!
% 136.73/29.13 % (2955556)------------------------------
% 136.73/29.13 % (2955556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.73/29.13 % (2955556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.73/29.13 % (2955556)CaDiCaL version: 2.1.3
% 136.73/29.13 % (2955556)Termination reason: Instruction limit
% 136.73/29.13 % (2955556)Termination phase: Saturation
% 136.73/29.13 % (2955556)Time elapsed: 0.425 s
% 136.73/29.13 % (2955556)Peak memory usage: 21 MB
% 136.73/29.13 % (2955556)Instructions burned: 869 (million)
% 136.73/29.13 % (2955560)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1695519395:i=54282_2953 on theBenchmark for (2953ds/54282Mi)
% 136.73/29.13 % (2955561)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1896060622:i=3512:aac=none_2953 on theBenchmark for (2953ds/3512Mi)
% 136.73/29.13 % TRYING [1]
% 136.73/29.13 % TRYING [2]
% 136.73/29.13 % TRYING [3]
% 136.73/29.13 % TRYING [4]
% 136.73/29.13 % TRYING [5]
% 136.73/29.13 % TRYING [6]
% 136.73/29.13 % TRYING [7]
% 136.73/29.13 % (2955542)Instruction limit reached!
% 136.73/29.13 % (2955542)------------------------------
% 136.73/29.13 % (2955542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.73/29.13 % (2955542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.73/29.13 % (2955542)CaDiCaL version: 2.1.3
% 136.73/29.13 % (2955542)Termination reason: Instruction limit
% 136.73/29.13 % (2955542)Termination phase: Finite model building SAT solving
% 136.73/29.13 % (2955542)Time elapsed: 5.277 s
% 136.73/29.13 % (2955542)Peak memory usage: 149 MB
% 136.73/29.13 % (2955542)Instructions burned: 22061 (million)
% 136.73/29.13 % (2955564)dis+21_1_sil=32000:sas=cadical:random_seed=2560539295:i=3773:amm=off_2940 on theBenchmark for (2940ds/3773Mi)
% 136.73/29.13 % (2955561)Instruction limit reached!
% 136.73/29.13 % (2955561)------------------------------
% 136.73/29.13 % (2955561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.73/29.13 % (2955561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.73/29.13 % (2955561)CaDiCaL version: 2.1.3
% 136.73/29.13 % (2955561)Termination reason: Instruction limit
% 136.73/29.13 % (2955561)Termination phase: Saturation
% 136.73/29.13 % (2955561)Time elapsed: 1.965 s
% 136.73/29.13 % (2955561)Peak memory usage: 34 MB
% 136.73/29.13 % (2955561)Instructions burned: 3517 (million)
% 136.73/29.13 % (2955566)ott+11_1_sil=16000:gs=on:random_seed=3907641889:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2933 on theBenchmark for (2933ds/2251Mi)
% 136.73/29.13 % (2955564)Instruction limit reached!
% 136.73/29.13 % (2955564)------------------------------
% 136.73/29.13 % (2955564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.73/29.13 % (2955564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.73/29.13 % (2955564)CaDiCaL version: 2.1.3
% 136.73/29.13 % (2955564)Termination reason: Instruction limit
% 136.73/29.13 % (2955564)Termination phase: Saturation
% 136.73/29.13 % (2955564)Time elapsed: 1.145 s
% 136.73/29.13 % (2955564)Peak memory usage: 41 MB
% 136.73/29.13 % (2955564)Instructions burned: 3775 (million)
% 136.73/29.13 % (2955568)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1451761912:fmbsr=1.6:i=67534_2929 on theBenchmark for (2929ds/67534Mi)
% 136.73/29.13 % TRYING [7]
% 136.73/29.13 % (2955558)Instruction limit reached!
% 136.73/29.13 % (2955558)------------------------------
% 136.73/29.13 % (2955558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.73/29.13 % (2955558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.73/29.13 % (2955558)CaDiCaL version: 2.1.3
% 136.73/29.13 % (2955558)Termination reason: Instruction limit
% 136.73/29.13 % (2955558)Termination phase: Saturation
% 136.73/29.13 % (2955558)Time elapsed: 2.972 s
% 136.73/29.13 % (2955558)Peak memory usage: 64 MB
% 136.73/29.13 % (2955558)Instructions burned: 5114 (million)
% 136.73/29.13 % (2955570)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1135382843:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2926 on theBenchmark for (2926ds/4591Mi)
% 136.73/29.13 % TRYING [8]
% 136.73/29.13 % (2955566)Instruction limit reached!
% 136.73/29.13 % (2955566)------------------------------
% 136.73/29.13 % (2955566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.73/29.13 % (2955566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.73/29.13 % (2955566)CaDiCaL version: 2.1.3
% 136.73/29.13 % (2955566)Termination reason: Instruction limit
% 136.73/29.13 % (2955566)Termination phase: Saturation
% 136.73/29.13 % (2955566)Time elapsed: 0.932 s
% 136.73/29.13 % (2955566)Peak memory usage: 17 MB
% 136.73/29.13 % (2955566)Instructions burned: 2253 (million)
% 136.73/29.13 % (2955572)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3117662382:i=29340_2924 on theBenchmark for (2924ds/29340Mi)
% 136.73/29.13 % TRYING [8]
% 136.73/29.13 % (2955570)Instruction limit reached!
% 136.73/29.13 % (2955570)------------------------------
% 136.73/29.13 % (2955570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.73/29.13 % (2955570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.73/29.13 % (2955570)CaDiCaL version: 2.1.3
% 136.73/29.13 % (2955570)Termination reason: Instruction limit
% 136.73/29.13 % (2955570)Termination phase: Saturation
% 136.73/29.13 % (2955570)Time elapsed: 1.675 s
% 136.73/29.13 % (2955570)Peak memory usage: 20 MB
% 136.73/29.13 % (2955570)Instructions burned: 4591 (million)
% 136.73/29.13 % (2955574)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1253568727:i=5211_2909 on theBenchmark for (2909ds/5211Mi)
% 136.73/29.13 % (2955574)Instruction limit reached!
% 136.73/29.13 % (2955574)------------------------------
% 136.73/29.13 % (2955574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.73/29.13 % (2955574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.73/29.13 % (2955574)CaDiCaL version: 2.1.3
% 136.73/29.13 % (2955574)Termination reason: Instruction limit
% 136.73/29.13 % (2955574)Termination phase: Saturation
% 136.73/29.13 % (2955574)Time elapsed: 2.646 s
% 136.73/29.13 % (2955574)Peak memory usage: 46 MB
% 136.73/29.13 % (2955574)Instructions burned: 5211 (million)
% 136.73/29.13 % (2955576)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2379422460:i=5497:nm=2_2882 on theBenchmark for (2882ds/5497Mi)
% 136.73/29.13 % TRYING [17]
% 136.73/29.13 % (2955576)Instruction limit reached!
% 136.73/29.13 % (2955576)------------------------------
% 136.73/29.13 % (2955576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.73/29.13 % (2955576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.73/29.13 % (2955576)CaDiCaL version: 2.1.3
% 136.73/29.13 % (2955576)Termination reason: Instruction limit
% 136.73/29.13 % (2955576)Termination phase: Finite model building constraint generation
% 136.73/29.13 % (2955576)Time elapsed: 1.954 s
% 136.73/29.13 % (2955576)Peak memory usage: 344 MB
% 136.73/29.13 % (2955576)Instructions burned: 5499 (million)
% 136.73/29.13 % (2955578)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=397095560:fmbsr=2:i=46332_2862 on theBenchmark for (2862ds/46332Mi)
% 136.73/29.13 % TRYING [15]
% 136.73/29.13 % TRYING [9]
% 136.73/29.13 % TRYING [9]
% 136.73/29.13 % (2955572)Instruction limit reached!
% 136.73/29.13 % (2955572)------------------------------
% 136.73/29.13 % (2955572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.73/29.13 % (2955572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.73/29.13 % (2955572)CaDiCaL version: 2.1.3
% 136.73/29.13 % (2955572)Termination reason: Instruction limit
% 136.73/29.13 % (2955572)Termination phase: Saturation
% 136.73/29.13 % (2955572)Time elapsed: 13.367 s
% 136.73/29.13 % (2955572)Peak memory usage: 238 MB
% 136.73/29.13 % (2955572)Instructions burned: 29341 (million)
% 136.73/29.13 % (2955580)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4140468078:i=14071_2790 on theBenchmark for (2790ds/14071Mi)
% 136.73/29.13 % TRYING [12]
% 136.73/29.13 % TRYING [9]
% 136.73/29.13 % (2955580)Instruction limit reached!
% 136.73/29.13 % (2955580)------------------------------
% 136.73/29.13 % (2955580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.73/29.13 % (2955580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.73/29.13 % (2955580)CaDiCaL version: 2.1.3
% 136.73/29.13 % (2955580)Termination reason: Instruction limit
% 136.73/29.13 % (2955580)Termination phase: Finite model building constraint generation
% 136.73/29.13 % (2955580)Time elapsed: 5.862 s
% 136.73/29.13 % (2955580)Peak memory usage: 835 MB
% 136.73/29.13 % (2955580)Instructions burned: 14073 (million)
% 136.73/29.13 % (2955582)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3966847263:i=22565:add=on:rawr=on_2730 on theBenchmark for (2730ds/22565Mi)
% 136.73/29.13 % (2955509) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2955503-2955509"...
% 136.73/29.13 % (2955509)...printing done.
% 136.73/29.13 % (2955509)Refutation found. Thanks to Tanya!
% 136.73/29.13 % SZS status Theorem for theBenchmark
% 136.73/29.13 % SZS output start Proof for theBenchmark
% See solution above
% 136.73/29.14 % (2955509)------------------------------
% 136.73/29.14 % (2955509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.73/29.14 % (2955509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.73/29.14 % (2955509)CaDiCaL version: 2.1.3
% 136.73/29.14 % (2955509)Termination reason: Refutation
% 136.73/29.14 % (2955509)Time elapsed: 28.403 s
% 136.73/29.14 % (2955509)Peak memory usage: 257 MB
% 136.73/29.14 % (2955509)Instructions burned: 51010 (million)
% 136.73/29.14 % (2955503)Success in time 28.736 s
% 136.73/29.14 % Vampire exiting
%------------------------------------------------------------------------------