%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV484+2 : 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 : n018.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 01:24:24 PM UTC 2026
% Result : CounterSatisfiable 3.16s 0.78s
% Output : Saturation 3.16s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u361,axiom,
n1 != n0 ).
cnf(u364,axiom,
~ p(n0,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u392,axiom,
~ p(X33,X32,X31,X30,X29,X28,X27,n0,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u500,axiom,
~ p(X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,n0,n1,X3,n1,X2,X1) ).
cnf(u506,axiom,
~ p(X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,n1,n0,X3,X2,n1,X1) ).
cnf(u512,axiom,
~ p(X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,n1,X2,X1,X0,n0) ).
cnf(u518,axiom,
~ p(X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,n1,n1,X2,n0,X1,X0) ).
cnf(u524,axiom,
~ p(X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,n1,n1,X2,X1,n0,X0) ).
cnf(u530,axiom,
~ p(X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,n1,X3,n0,X2,X1,X0) ).
cnf(u536,axiom,
~ p(X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,n1,X8,X7,n1,X6,X5,X4,X3,n1,X2,X1,X0,n0) ).
cnf(u542,axiom,
~ p(X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,n1,X8,X7,n1,X6,X5,X4,n1,X3,X2,n0,X1,X0) ).
cnf(u548,axiom,
~ p(X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,n1,X15,X14,n1,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,n1,X2,X1,n0,X0) ).
cnf(u554,axiom,
~ p(X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,n1,X15,X14,n1,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,n1,X3,n0,X2,X1,X0) ).
cnf(u560,axiom,
~ p(X29,X28,X27,X26,X25,X24,X23,n1,X22,X21,n1,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,n1,X2,X1,X0,n0) ).
cnf(u566,axiom,
~ p(X29,X28,X27,X26,X25,X24,X23,n1,X22,X21,n1,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,n1,X3,X2,n0,X1,X0) ).
cnf(u572,axiom,
~ p(n1,X29,X28,n1,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,n1,X2,X1,n0,X0) ).
cnf(u578,axiom,
~ p(n1,X29,X28,n1,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,n1,X3,n0,X2,X1,X0) ).
cnf(u584,axiom,
~ p(X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,n1,X8,X7,X6,n1,X5,X4,X3,n0,X2,X1,X0,n1) ).
cnf(u590,axiom,
~ p(X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,n1,X8,X7,X6,n1,X5,X4,n0,X3,X2,n1,X1,X0) ).
cnf(u596,axiom,
~ p(X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,n1,X15,X14,X13,n1,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,n0,X2,X1,n1,X0) ).
cnf(u602,axiom,
~ p(X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,n1,X15,X14,X13,n1,X12,X11,X10,X9,X8,X7,X6,X5,X4,n0,X3,n1,X2,X1,X0) ).
cnf(u608,axiom,
~ p(X29,X28,X27,X26,X25,X24,X23,n1,X22,X21,X20,n1,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,n0,X2,X1,X0,n1) ).
cnf(u614,axiom,
~ p(X29,X28,X27,X26,X25,X24,X23,n1,X22,X21,X20,n1,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,n0,X3,X2,n1,X1,X0) ).
cnf(u620,axiom,
~ p(n1,X29,X28,X27,n1,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,n0,X2,X1,n1,X0) ).
cnf(u626,axiom,
~ p(n1,X29,X28,X27,n1,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,n0,X3,n1,X2,X1,X0) ).
cnf(u632,axiom,
~ p(X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,n1,X10,X9,X8,X7,X6,n1,X5,X4,X3,X2,X1,X0) ).
cnf(u638,axiom,
~ p(X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,n1,X17,X16,X15,X14,X13,n1,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u644,axiom,
~ p(X31,X30,X29,X28,X27,X26,X25,n1,X24,X23,X22,X21,X20,n1,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u656,axiom,
~ p(X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,n1,X10,X9,X8,X7,n0,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u662,axiom,
~ p(X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,n1,n0,X9,X8,n0,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u668,axiom,
~ p(X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,n1,n0,n0,n0,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u677,axiom,
~ p(X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,n1,n0,n0,X8,n0,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u683,axiom,
~ p(X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,n1,X17,X16,X15,X14,n0,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u689,axiom,
~ p(X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,n1,n0,X16,X15,n0,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u695,axiom,
~ p(X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,n1,n0,n0,n0,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u704,axiom,
~ p(X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,n1,n0,n0,X15,n0,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u764,axiom,
~ p(X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,n1,X9,n1,X8,X7,X6,X5,X4,X3,X2,X1,X0,n1) ).
cnf(u770,axiom,
~ p(X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,n0,X15,X14,X13,X12,X11,X10,n1,X9,n1,X8,X7,X6,X5,X4,X3,X2,n1,X1,X0) ).
cnf(u776,axiom,
~ p(X29,X28,X27,X26,X25,X24,X23,n0,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,n1,X9,n1,X8,X7,X6,X5,X4,X3,X2,X1,X0,n1) ).
cnf(u782,axiom,
~ p(n0,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,n1,X9,n1,X8,X7,X6,X5,X4,X3,X2,n1,X1,X0) ).
cnf(u788,axiom,
~ p(X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,n1,X15,n1,X14,X13,X12,X11,n0,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,n1,X0) ).
cnf(u794,axiom,
~ p(X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,n1,X16,n1,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,n1,X2,X1,X0) ).
cnf(u800,axiom,
~ p(X29,X28,X27,X26,X25,X24,X23,n0,X22,X21,X20,X19,X18,X17,n1,X16,n1,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,n1,X0) ).
cnf(u806,axiom,
~ p(n0,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,n1,X16,n1,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,n1,X2,X1,X0) ).
cnf(u812,axiom,
~ p(X29,X28,X27,X26,X25,X24,X23,n1,X22,n1,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,n0,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0,n1) ).
cnf(u818,axiom,
~ p(X29,X28,X27,X26,X25,X24,X23,n1,X22,n1,X21,X20,X19,X18,n0,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,n1,X1,X0) ).
cnf(u824,axiom,
~ p(X30,X29,X28,X27,X26,X25,X24,n1,X23,n1,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0,n1) ).
cnf(u830,axiom,
~ p(n0,X29,X28,X27,X26,X25,X24,n1,X23,n1,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,n1,X1,X0) ).
cnf(u836,axiom,
~ p(n1,X29,n1,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,n0,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,n1,X0) ).
cnf(u842,axiom,
~ p(n1,X29,n1,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,n0,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,n1,X2,X1,X0) ).
cnf(u848,axiom,
~ p(n1,X29,n1,X28,X27,X26,X25,n0,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,n1,X0) ).
cnf(u854,axiom,
~ p(n1,X30,n1,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,n1,X2,X1,X0) ).
cnf(u860,axiom,
~ p(X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,n1,n1,X8,X7,X6,X5,n1,X4,X3,X2,X1,X0,n0) ).
cnf(u866,axiom,
~ p(X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,n1,X14,X13,X12,X11,X10,n1,n1,n1,X9,X8,X7,X6,X5,X4,X3,X2,n0,X1,X0) ).
cnf(u872,axiom,
~ p(X28,X27,X26,X25,X24,X23,X22,n1,X21,X20,X19,X18,X17,n1,X16,X15,X14,X13,X12,X11,X10,n1,n1,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0,n0) ).
cnf(u878,axiom,
~ p(n1,X28,X27,X26,X25,X24,n1,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,n1,n1,X9,X8,X7,X6,X5,X4,X3,X2,n0,X1,X0) ).
cnf(u884,axiom,
~ p(X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,n1,n1,X14,X13,X12,X11,X10,n1,X9,X8,X7,X6,X5,n1,X4,X3,X2,X1,n0,X0) ).
cnf(u890,axiom,
~ p(X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,n1,n1,X15,X14,X13,X12,n1,X11,X10,X9,X8,X7,X6,X5,X4,X3,n0,X2,X1,X0) ).
cnf(u896,axiom,
~ p(X28,X27,X26,X25,X24,X23,X22,n1,X21,X20,X19,X18,X17,n1,n1,n1,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,n0,X0) ).
cnf(u902,axiom,
~ p(n1,X28,X27,X26,X25,X24,n1,X23,X22,X21,X20,X19,X18,X17,n1,n1,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,n0,X2,X1,X0) ).
cnf(u908,axiom,
~ p(X28,X27,X26,X25,X24,X23,X22,n1,n1,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,n1,X9,X8,X7,X6,X5,n1,X4,X3,X2,X1,X0,n0) ).
cnf(u914,axiom,
~ p(X28,X27,X26,X25,X24,X23,X22,n1,n1,X21,X20,X19,X18,X17,n1,X16,X15,X14,X13,X12,n1,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,n0,X1,X0) ).
cnf(u920,axiom,
~ p(X29,X28,X27,X26,X25,X24,X23,n1,n1,X22,X21,X20,X19,n1,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0,n0) ).
cnf(u932,axiom,
~ p(n1,n1,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,n1,X9,X8,X7,X6,X5,n1,X4,X3,X2,X1,n0,X0) ).
cnf(u938,axiom,
~ p(n1,n1,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,n1,X16,X15,X14,X13,X12,n1,X11,X10,X9,X8,X7,X6,X5,X4,X3,n0,X2,X1,X0) ).
cnf(u944,axiom,
~ p(n1,n1,X28,X27,X26,X25,X24,n1,X23,X22,X21,X20,X19,n1,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,n0,X0) ).
cnf(u4131,axiom,
~ p(X0,n1,n1,X1,n1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30) ).
cnf(u5605,axiom,
~ p(n1,X0,X1,X2,X3,X4,n1,n1,n1,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,n0,n1,X24,n0,X25,X26) ).
cnf(u5442,axiom,
~ p(n1,n0,n0,X0,n0,X1,n1,X2,X3,X4,X5,X6,X7,X8,n1,X9,n1,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,n0,X23,X24,X25) ).
cnf(u276,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X18
| n1 = X18 ) ).
cnf(u288,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X12
| n1 = X12 ) ).
cnf(u172,axiom,
( p(n1,X28,X27,X26,X25,X24,n1,n1,n1,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,n1,X1,X0)
| ~ p(n1,X28,X27,X26,X25,X24,n1,n1,n1,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,n0,X1,X0) ) ).
cnf(u4871,axiom,
~ p(n1,n0,X0,X1,n0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,n0,X26,X27,n1,X28) ).
cnf(u302,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X5
| n1 = X5 ) ).
cnf(u314,negated_conjecture,
~ p(X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,n1,X4,X3,X2,X1,X0) ).
cnf(u201,axiom,
( p(n1,n0,n1,n0,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| ~ p(n1,n0,n0,n0,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u264,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X24
| n1 = X24 ) ).
cnf(u5209,axiom,
~ p(X0,X1,X2,X3,X4,X5,X6,n1,n0,n0,n0,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,n0,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,n1) ).
cnf(u286,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X13
| n1 = X13 ) ).
cnf(u4730,axiom,
~ p(n1,n0,n0,n0,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,n1,X26,X27,X28) ).
cnf(u290,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X11
| n1 = X11 ) ).
cnf(u246,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X33
| n1 = X33 ) ).
cnf(u205,axiom,
( p(X29,X28,X27,X26,X25,X24,X23,n1,n1,n0,X22,n0,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| ~ p(X29,X28,X27,X26,X25,X24,X23,n1,n0,n0,X22,n0,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u5214,axiom,
~ p(X0,X1,X2,X3,X4,X5,X6,n1,n0,n0,n0,X7,X8,X9,n0,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,n1,X26,X27) ).
cnf(u268,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X22
| n1 = X22 ) ).
cnf(u208,axiom,
( p(X30,X29,X28,X27,X26,X25,X24,n1,n0,X23,X22,n1,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| ~ p(X30,X29,X28,X27,X26,X25,X24,n1,n0,X23,X22,n0,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u203,axiom,
( p(n1,n0,X30,X29,n1,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| ~ p(n1,n0,X30,X29,n0,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u294,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X9
| n1 = X9 ) ).
cnf(u4601,axiom,
~ p(n1,n1,X0,X1,X2,X3,n1,X4,X5,X6,X7,X8,X9,X10,n1,X11,n1,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,n0,X25,X26,X27) ).
cnf(u312,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X0
| n1 = X0 ) ).
cnf(u207,axiom,
( p(X29,X28,X27,X26,X25,X24,X23,n1,n0,n0,n1,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| ~ p(X29,X28,X27,X26,X25,X24,X23,n1,n0,n0,n0,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u270,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X21
| n1 = X21 ) ).
cnf(u282,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X15
| n1 = X15 ) ).
cnf(u258,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X27
| n1 = X27 ) ).
cnf(u292,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X10
| n1 = X10 ) ).
cnf(u304,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X4
| n1 = X4 ) ).
cnf(u5603,axiom,
~ p(n1,X0,X1,X2,X3,X4,n1,n1,n1,n1,X5,X6,X7,X8,n0,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,n0,X25,X26) ).
cnf(u262,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X25
| n1 = X25 ) ).
cnf(u202,axiom,
( p(n1,n0,n0,n1,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| ~ p(n1,n0,n0,n0,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u280,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X16
| n1 = X16 ) ).
cnf(u5811,axiom,
~ p(n1,X0,X1,X2,X3,X4,n1,n1,n0,n0,X5,n0,X6,X7,X8,X9,X10,X11,X12,X13,X14,n1,X15,X16,X17,n1,X18,X19,n0,X20,X21,n0,X22,X23) ).
cnf(u306,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X3
| n1 = X3 ) ).
cnf(u206,axiom,
( p(X29,X28,X27,X26,X25,X24,X23,n1,n0,n1,n0,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| ~ p(X29,X28,X27,X26,X25,X24,X23,n1,n0,n0,n0,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u284,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X14
| n1 = X14 ) ).
cnf(u310,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X1
| n1 = X1 ) ).
cnf(u250,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X31
| n1 = X31 ) ).
cnf(u5642,axiom,
~ p(n1,X0,X1,X2,X3,X4,n1,n1,n1,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,n1,X17,X18,X19,n1,X20,X21,n0,X22,X23,n0,X24,X25) ).
cnf(u5657,axiom,
~ p(n1,X0,X1,X2,X3,X4,n1,n1,n1,X5,X6,X7,X8,X9,n0,X10,X11,X12,X13,X14,X15,n1,X16,n1,X17,X18,X19,X20,X21,X22,X23,n0,X24,X25) ).
cnf(u260,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X26
| n1 = X26 ) ).
cnf(u272,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X20
| n1 = X20 ) ).
cnf(u5803,axiom,
~ p(n1,X0,X1,X2,X3,X4,n1,n1,n0,n0,X5,n0,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,n0,n1,X22,n0,X23,X24) ).
cnf(u200,axiom,
( p(n1,n1,n0,X29,n0,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| ~ p(n1,n0,n0,X29,n0,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u4872,axiom,
~ p(n1,n0,X0,X1,n0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,n0,X25,n1,X26,X27,X28) ).
cnf(u4800,axiom,
~ p(n1,n0,n0,n0,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,n1,X25,X26,n0,X27) ).
cnf(u5599,axiom,
~ p(n1,X0,X1,X2,X3,X4,n1,n1,n1,X5,X6,n1,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,n0,X23,X24,n0,X25,X26) ).
cnf(u298,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X7
| n1 = X7 ) ).
cnf(u220,axiom,
( p(n1,X31,X30,X29,X28,X27,n0,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| ~ p(n1,X31,X30,X29,X28,X27,n1,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u254,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X29
| n1 = X29 ) ).
cnf(u4725,axiom,
~ p(n1,n0,n0,n0,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,n0,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,n1,X27) ).
cnf(u4728,axiom,
~ p(n1,n0,n0,n0,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,n0,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,n1,X25,X26,X27) ).
cnf(u204,axiom,
( p(n1,X31,X30,X29,X28,n1,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| ~ p(n1,X31,X30,X29,X28,n0,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u5819,axiom,
~ p(n1,X0,X1,X2,X3,X4,n1,n1,n0,n0,X5,n0,X6,X7,n0,X8,X9,X10,X11,X12,X13,n1,X14,n1,X15,X16,X17,X18,X19,X20,X21,n0,X22,X23) ).
cnf(u167,axiom,
p(n1,n0,n0,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0) ).
cnf(u274,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X19
| n1 = X19 ) ).
cnf(u256,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X28
| n1 = X28 ) ).
cnf(u5210,axiom,
~ p(X0,X1,X2,X3,X4,X5,X6,n1,n0,n0,n0,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,n1) ).
cnf(u5364,axiom,
~ p(X0,X1,X2,X3,X4,X5,X6,n1,n0,X7,X8,n0,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,n0,X26,X27,X28,n1) ).
cnf(u4597,axiom,
~ p(n1,n1,X0,X1,X2,X3,n1,X4,X5,X6,X7,X8,X9,X10,n1,X11,X12,X13,n1,X14,X15,X16,X17,X18,X19,X20,X21,X22,n0,X23,n0,X24,X25,X26) ).
cnf(u308,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X2
| n1 = X2 ) ).
cnf(u248,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X32
| n1 = X32 ) ).
cnf(u4544,axiom,
~ p(n1,n1,X0,X1,n1,X2,n1,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,n0,X24,n0,X25,X26,X27) ).
cnf(u5360,axiom,
~ p(n1,n0,n0,X0,n0,X1,n1,X2,X3,X4,X5,X6,X7,X8,n1,X9,X10,X11,n1,X12,X13,X14,X15,X16,X17,X18,X19,X20,n0,X21,n0,X22,X23,X24) ).
cnf(u278,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X17
| n1 = X17 ) ).
cnf(u296,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X8
| n1 = X8 ) ).
cnf(u252,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X30
| n1 = X30 ) ).
cnf(u4548,axiom,
~ p(n1,n1,n1,X0,X1,X2,n1,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,n0,X26,X27,X28) ).
cnf(u266,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X23
| n1 = X23 ) ).
cnf(u4546,axiom,
~ p(n1,n1,n1,X0,X1,X2,n1,X3,X4,X5,X6,X7,X8,X9,n0,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,n0,X25,X26,X27) ).
cnf(u5365,axiom,
~ p(X0,X1,X2,X3,X4,X5,X6,n1,n0,X7,X8,n0,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,n0,X25,X26,n1,X27,X28) ).
cnf(u209,axiom,
( p(X31,X30,X29,X28,X27,X26,X25,n1,X24,X23,X22,X21,n1,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| ~ p(X31,X30,X29,X28,X27,X26,X25,n1,X24,X23,X22,X21,n0,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u300,axiom,
( ~ p(X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| n0 = X6
| n1 = X6 ) ).
cnf(u168,axiom,
( p(n1,n1,X29,X28,X27,X26,n1,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,n1,X2,X1,X0)
| ~ p(n1,n1,X29,X28,X27,X26,n1,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,n0,X2,X1,X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV484+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.16 % Computer : n018.cluster.edu
% 0.07/0.16 % Model : x86_64 x86_64
% 0.07/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.16 % Memory : 8046.5625MB
% 0.07/0.16 % OS : Linux 6.8.0-71-generic
% 0.07/0.16 % CPULimit : 300
% 0.07/0.16 % WCLimit : 300
% 0.07/0.16 % DateTime : Mon Sep 28 11:14:25 UTC 2026
% 0.07/0.17 % CPUTime :
% 0.07/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.19 Running first-order model finding
% 0.07/0.19 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
% 3.16/0.78 % (3308275)Will run a generic schedule for satisfiability detection.
% 3.16/0.78 % (3308282)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4051194351:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.16/0.78 % (3308280)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2916056333_2999 on theBenchmark for (2999ds/0Mi)
% 3.16/0.78 % (3308283)dis+10_1_sil=32000:sp=arity:random_seed=1459878857:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.16/0.78 % (3308284)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=889470366:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.16/0.78 % (3308286)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2299642565:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.16/0.78 % (3308285)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=131734444:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.16/0.78 % (3308281)% WARNING: option uhcvi not known.
% 3.16/0.78 % (3308281)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2704934872:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.16/0.78 % (3308283)Instruction limit reached!
% 3.16/0.78 % (3308283)------------------------------
% 3.16/0.78 % (3308283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.78 % (3308283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.78 % (3308283)CaDiCaL version: 2.1.3
% 3.16/0.78 % (3308283)Termination reason: Instruction limit
% 3.16/0.78 % (3308283)Termination phase: Saturation
% 3.16/0.78 % (3308283)Time elapsed: 0.047 s
% 3.16/0.78 % (3308283)Peak memory usage: 12 MB
% 3.16/0.78 % (3308283)Instructions burned: 103 (million)
% 3.16/0.78 % (3308284)Instruction limit reached!
% 3.16/0.78 % (3308284)------------------------------
% 3.16/0.78 % (3308284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.78 % (3308284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.78 % (3308284)CaDiCaL version: 2.1.3
% 3.16/0.78 % (3308284)Termination reason: Instruction limit
% 3.16/0.78 % (3308284)Termination phase: Saturation
% 3.16/0.78 % (3308284)Time elapsed: 0.056 s
% 3.16/0.78 % (3308284)Peak memory usage: 13 MB
% 3.16/0.78 % (3308284)Instructions burned: 116 (million)
% 3.16/0.78 % (3308285)Instruction limit reached!
% 3.16/0.78 % (3308285)------------------------------
% 3.16/0.78 % (3308285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.78 % (3308285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.78 % (3308285)CaDiCaL version: 2.1.3
% 3.16/0.78 % (3308285)Termination reason: Instruction limit
% 3.16/0.78 % (3308285)Termination phase: Saturation
% 3.16/0.78 % (3308285)Time elapsed: 0.061 s
% 3.16/0.78 % (3308285)Peak memory usage: 12 MB
% 3.16/0.78 % (3308285)Instructions burned: 131 (million)
% 3.16/0.78 % (3308294)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4203845486:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.16/0.78 % (3308286)Instruction limit reached!
% 3.16/0.78 % (3308286)------------------------------
% 3.16/0.78 % (3308286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.78 % (3308286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.78 % (3308286)CaDiCaL version: 2.1.3
% 3.16/0.78 % (3308286)Termination reason: Instruction limit
% 3.16/0.78 % (3308286)Termination phase: Saturation
% 3.16/0.78 % (3308286)Time elapsed: 0.074 s
% 3.16/0.78 % (3308286)Peak memory usage: 13 MB
% 3.16/0.78 % (3308286)Instructions burned: 159 (million)
% 3.16/0.78 % (3308295)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1201847429:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.16/0.78 % (3308296)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=195344996:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 3.16/0.78 % (3308299)ott-21_1_sil=16000:fs=off:random_seed=1645076817:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 3.16/0.78 % (3308295)Instruction limit reached!
% 3.16/0.78 % (3308295)------------------------------
% 3.16/0.78 % (3308295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.78 % (3308295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.78 % (3308295)CaDiCaL version: 2.1.3
% 3.16/0.78 % (3308295)Termination reason: Instruction limit
% 3.16/0.78 % (3308295)Termination phase: Saturation
% 3.16/0.78 % (3308295)Time elapsed: 0.061 s
% 3.16/0.78 % (3308295)Peak memory usage: 13 MB
% 3.16/0.78 % (3308295)Instructions burned: 133 (million)
% 3.16/0.78 % Detected minimum model sizes of [1]
% 3.16/0.78 % Detected maximum model sizes of [2]
% 3.16/0.78 % TRYING [1]
% 3.16/0.78 % (3308280)Cannot represent all propositional literals internally
% 3.16/0.78 % (3308280)Refutation not found, incomplete strategy
% 3.16/0.78 % (3308280)------------------------------
% 3.16/0.78 % (3308280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.78 % (3308280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.78 % (3308280)CaDiCaL version: 2.1.3
% 3.16/0.78 % (3308280)Termination reason: Refutation not found, incomplete strategy
% 3.16/0.78 % (3308280)Time elapsed: 0.155 s
% 3.16/0.78 % (3308280)Peak memory usage: 14 MB
% 3.16/0.78 % (3308280)Instructions burned: 338 (million)
% 3.16/0.78 % (3308280)------------------------------
% 3.16/0.78 % (3308280)------------------------------
% 3.16/0.78 % (3308302)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3808926449:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 3.16/0.78 % (3308304)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2949105618:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 3.16/0.78 % (3308299)Instruction limit reached!
% 3.16/0.78 % (3308299)------------------------------
% 3.16/0.78 % (3308299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.78 % (3308299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.78 % (3308299)CaDiCaL version: 2.1.3
% 3.16/0.78 % (3308299)Termination reason: Instruction limit
% 3.16/0.78 % (3308299)Termination phase: Saturation
% 3.16/0.78 % (3308299)Time elapsed: 0.093 s
% 3.16/0.78 % (3308299)Peak memory usage: 12 MB
% 3.16/0.78 % (3308299)Instructions burned: 182 (million)
% 3.16/0.78 % (3308306)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2544306485:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 3.16/0.78 % Detected minimum model sizes of [1]
% 3.16/0.78 % Detected maximum model sizes of [3]
% 3.16/0.78 % TRYING [1]
% 3.16/0.78 % (3308294)Cannot represent all propositional literals internally
% 3.16/0.78 % (3308294)Refutation not found, incomplete strategy
% 3.16/0.78 % (3308294)------------------------------
% 3.16/0.78 % (3308294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.78 % (3308294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.78 % (3308294)CaDiCaL version: 2.1.3
% 3.16/0.78 % (3308294)Termination reason: Refutation not found, incomplete strategy
% 3.16/0.78 % (3308294)Time elapsed: 0.160 s
% 3.16/0.78 % (3308294)Peak memory usage: 13 MB
% 3.16/0.78 % (3308294)Instructions burned: 362 (million)
% 3.16/0.78 % (3308294)------------------------------
% 3.16/0.78 % (3308294)------------------------------
% 3.16/0.78 % (3308308)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3099244496:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 3.16/0.78 % Detected minimum model sizes of [1]
% 3.16/0.78 % Detected maximum model sizes of [2]
% 3.16/0.78 % TRYING [1]
% 3.16/0.78 % (3308304)Cannot represent all propositional literals internally
% 3.16/0.78 % (3308304)Refutation not found, incomplete strategy
% 3.16/0.78 % (3308304)------------------------------
% 3.16/0.78 % (3308304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.78 % (3308304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.78 % (3308304)CaDiCaL version: 2.1.3
% 3.16/0.78 % (3308304)Termination reason: Refutation not found, incomplete strategy
% 3.16/0.78 % (3308304)Time elapsed: 0.150 s
% 3.16/0.78 % (3308304)Peak memory usage: 13 MB
% 3.16/0.78 % (3308304)Instructions burned: 323 (million)
% 3.16/0.78 % (3308304)------------------------------
% 3.16/0.78 % (3308304)------------------------------
% 3.16/0.78 % (3308310)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=2480713489:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 3.16/0.78 % (3308296)Instruction limit reached!
% 3.16/0.78 % (3308296)------------------------------
% 3.16/0.78 % (3308296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.78 % (3308296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.78 % (3308296)CaDiCaL version: 2.1.3
% 3.16/0.78 % (3308296)Termination reason: Instruction limit
% 3.16/0.78 % (3308296)Termination phase: Saturation
% 3.16/0.78 % (3308296)Time elapsed: 0.304 s
% 3.16/0.78 % (3308296)Peak memory usage: 14 MB
% 3.16/0.78 % (3308296)Instructions burned: 684 (million)
% 3.16/0.78 % (3308302)Instruction limit reached!
% 3.16/0.78 % (3308302)------------------------------
% 3.16/0.78 % (3308302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.78 % (3308302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.78 % (3308302)CaDiCaL version: 2.1.3
% 3.16/0.78 % (3308302)Termination reason: Instruction limit
% 3.16/0.78 % (3308302)Termination phase: Saturation
% 3.16/0.78 % (3308302)Time elapsed: 0.231 s
% 3.16/0.78 % (3308302)Peak memory usage: 15 MB
% 3.16/0.78 % (3308302)Instructions burned: 478 (million)
% 3.16/0.78 % Detected minimum model sizes of [1]
% 3.16/0.78 % Detected maximum model sizes of [2]
% 3.16/0.78 % fmb_start_size (= 14) larger than a detected sort maximum size!
% 3.16/0.78 % (3308308)Refutation not found, incomplete strategy
% 3.16/0.78 % (3308308)------------------------------
% 3.16/0.78 % (3308308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.78 % (3308308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.78 % (3308308)CaDiCaL version: 2.1.3
% 3.16/0.78 % (3308308)Termination reason: Refutation not found, incomplete strategy
% 3.16/0.78 % (3308308)Time elapsed: 0.149 s
% 3.16/0.78 % (3308308)Peak memory usage: 13 MB
% 3.16/0.78 % (3308308)Instructions burned: 322 (million)
% 3.16/0.78 % (3308308)------------------------------
% 3.16/0.78 % (3308308)------------------------------
% 3.16/0.78 % (3308312)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4029119468:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi)
% 3.16/0.78 % (3308313)fmb+10_1_sil=64000:random_seed=627316537:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 3.16/0.78 % (3308314)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1318265324:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 3.16/0.78 % (3308312) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3308275-3308312"...
% 3.16/0.78 % (3308312)...printing done.
% 3.16/0.78 % SZS status CounterSatisfiable for theBenchmark
% 3.16/0.78 % SZS output start Saturation.
% See solution above
% 3.16/0.78 % SZS output start Definitions and Model Updates.
% 3.16/0.78 % SZS output end Definitions and Model Updates.
% 3.16/0.78 % (3308312)------------------------------
% 3.16/0.78 % (3308312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.78 % (3308312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.78 % (3308312)CaDiCaL version: 2.1.3
% 3.16/0.78 % (3308312)Termination reason: Satisfiable
% 3.16/0.78 % (3308312)Time elapsed: 0.127 s
% 3.16/0.78 % (3308312)Peak memory usage: 14 MB
% 3.16/0.78 % (3308312)Instructions burned: 258 (million)
% 3.16/0.78 % (3308275)Success in time 0.583 s
% 3.16/0.78 % Vampire exiting
%------------------------------------------------------------------------------