%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV485+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n010.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 5.62s 1.17s
% Output : Saturation 5.62s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u521,axiom,
n1 != n0 ).
cnf(u524,axiom,
~ p(n0,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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) ).
cnf(u552,axiom,
~ p(X47,X46,X45,X44,X43,X42,X41,n0,X39,X38,X37,X36,X35,X34,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) ).
cnf(u644,axiom,
~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,n0,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u716,axiom,
~ p(X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,n0,n1,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,n1,X4,X3,X2,X1) ).
cnf(u722,axiom,
~ p(X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,n0,X16,n1,X15,X14,X13,X12,X11,X10,X9,n1,X8,X7,X6,X5,X4,X3,X2,X1) ).
cnf(u728,axiom,
~ p(X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,n0,X17,X16,n1,X15,X14,X13,n1,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1) ).
cnf(u734,axiom,
~ p(X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,n1,n0,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,n1,X1) ).
cnf(u740,axiom,
~ p(X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,n0,n1,X16,X15,X14,X13,X12,X11,X10,n1,X9,X8,X7,X6,X5,X4,X3,X2,X1) ).
cnf(u746,axiom,
~ p(X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,n0,X17,n1,X16,X15,X14,n1,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1) ).
cnf(u752,axiom,
~ p(X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,n1,X16,n0,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,n1,X2,X1) ).
cnf(u758,axiom,
~ p(X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,n1,n0,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,n1,X6,X5,X4,X3,X2,X1) ).
cnf(u764,axiom,
~ p(X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,n0,n1,X17,X16,X15,n1,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1) ).
cnf(u770,axiom,
~ p(X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,n1,X17,X16,n0,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,n1,X3,X2,X1) ).
cnf(u776,axiom,
~ p(X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,n1,X17,n0,X16,X15,X14,X13,X12,X11,X10,X9,X8,n1,X7,X6,X5,X4,X3,X2,X1) ).
cnf(u782,axiom,
~ p(X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,n1,n0,X17,X16,X15,X14,X13,X12,n1,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1) ).
cnf(u788,axiom,
~ p(X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,n1,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0,n0) ).
cnf(u794,axiom,
~ p(X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,n1,n1,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,n0,X3,X2,X1,X0) ).
cnf(u800,axiom,
~ p(X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,n1,X15,n1,X14,X13,X12,X11,X10,X9,X8,n0,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u806,axiom,
~ p(X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,n1,X16,X15,n1,X14,X13,X12,n0,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u812,axiom,
~ p(X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,n1,n1,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,n0,X0) ).
cnf(u824,axiom,
~ p(X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,n1,n1,X15,X14,X13,X12,X11,X10,X9,n0,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u830,axiom,
~ p(X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,n1,X16,n1,X15,X14,X13,n0,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u836,axiom,
~ p(X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,n1,X15,n1,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,n0,X1,X0) ).
cnf(u842,axiom,
~ p(X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,n1,n1,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,n0,X5,X4,X3,X2,X1,X0) ).
cnf(u848,axiom,
~ p(X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,n1,X16,X15,X14,X13,X12,X11,X10,n0,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u854,axiom,
~ p(X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,n1,n1,X16,X15,X14,n0,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u860,axiom,
~ p(X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,n1,X16,X15,n1,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,n0,X2,X1,X0) ).
cnf(u866,axiom,
~ p(X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,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,n0,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u872,axiom,
~ p(X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,n1,n1,X16,X15,X14,X13,X12,X11,n0,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u878,axiom,
~ p(X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,n1,X17,X16,X15,n0,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u884,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,n1,X22,X21,n1,X20,X19,X18,X17,X16,X15,n1,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0,n0) ).
cnf(u890,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,n1,X22,X21,n1,X20,X19,X18,X17,X16,n1,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,n0,X3,X2,X1,X0) ).
cnf(u896,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,n1,X22,X21,n1,X20,X19,X18,X17,n1,X16,X15,X14,X13,X12,X11,X10,X9,X8,n0,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u902,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,n1,X22,X21,n1,X20,X19,X18,n1,X17,X16,X15,X14,X13,X12,n0,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u908,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,n1,X29,X28,n1,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,n1,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,n0,X0) ).
cnf(u914,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,n1,X29,X28,n1,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,n1,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,n0,X4,X3,X2,X1,X0) ).
cnf(u920,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,n1,X29,X28,n1,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,n1,X16,X15,X14,X13,X12,X11,X10,X9,n0,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u926,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,n1,X29,X28,n1,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,n1,X17,X16,X15,X14,X13,n0,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u932,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,n1,X36,X35,n1,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,n1,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,n0,X1,X0) ).
cnf(u944,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,n1,X36,X35,n1,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,n1,X16,X15,X14,X13,X12,X11,X10,n0,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u950,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,n1,X36,X35,n1,X34,X33,X32,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(u956,axiom,
~ p(n1,X43,X42,n1,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,n1,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,n0,X2,X1,X0) ).
cnf(u968,axiom,
~ p(n1,X43,X42,n1,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,n1,X16,X15,X14,X13,X12,X11,n0,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u974,axiom,
~ p(n1,X43,X42,n1,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,n1,X17,X16,X15,n0,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u980,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,n1,X22,X21,X20,n1,X19,X18,X17,X16,X15,n0,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0,n1) ).
cnf(u986,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,n1,X22,X21,X20,n1,X19,X18,X17,X16,n0,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,n1,X3,X2,X1,X0) ).
cnf(u992,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,n1,X22,X21,X20,n1,X19,X18,X17,n0,X16,X15,X14,X13,X12,X11,X10,X9,X8,n1,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u998,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,n1,X22,X21,X20,n1,X19,X18,n0,X17,X16,X15,X14,X13,X12,n1,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u1004,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,n1,X29,X28,X27,n1,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,n0,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,n1,X0) ).
cnf(u1010,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,n1,X29,X28,X27,n1,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,n0,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,n1,X4,X3,X2,X1,X0) ).
cnf(u1016,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,n1,X29,X28,X27,n1,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,n0,X16,X15,X14,X13,X12,X11,X10,X9,n1,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u1022,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,n1,X29,X28,X27,n1,X26,X25,X24,X23,X22,X21,X20,X19,X18,n0,X17,X16,X15,X14,X13,n1,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u1028,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,n1,X36,X35,X34,n1,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,n0,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,n1,X1,X0) ).
cnf(u1034,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,n1,X36,X35,X34,n1,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,n0,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,n1,X5,X4,X3,X2,X1,X0) ).
cnf(u1040,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,n1,X36,X35,X34,n1,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,n0,X16,X15,X14,X13,X12,X11,X10,n1,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u1046,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,n1,X36,X35,X34,n1,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,n0,X17,X16,X15,X14,n1,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u1052,axiom,
~ p(n1,X43,X42,X41,n1,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,n0,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,n1,X2,X1,X0) ).
cnf(u1058,axiom,
~ p(n1,X43,X42,X41,n1,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,n0,X15,X14,X13,X12,X11,X10,X9,X8,X7,n1,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u1064,axiom,
~ p(n1,X43,X42,X41,n1,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,n0,X16,X15,X14,X13,X12,X11,n1,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u1070,axiom,
~ p(n1,X43,X42,X41,n1,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,n0,X17,X16,X15,n1,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u1076,axiom,
~ p(X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,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(u1082,axiom,
~ p(X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,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(u1088,axiom,
~ p(X45,X44,X43,X42,X41,X40,X39,n1,X38,X37,X36,X35,X34,n1,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) ).
cnf(u1100,axiom,
~ p(X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,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(u1106,axiom,
~ p(X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,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(u1112,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,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(u1121,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,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(u1127,axiom,
~ p(X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,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(u1133,axiom,
~ p(X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,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(u1139,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,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(u1148,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,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(u1208,axiom,
~ p(X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,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(u1214,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,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,n1,X3,X2,X1,X0) ).
cnf(u1220,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,n0,X36,X35,X34,X33,X32,X31,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,n1,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u1226,axiom,
~ p(n0,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,n1,X23,n1,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,n1,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u1232,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,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(u1238,axiom,
~ p(X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,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,n1,X4,X3,X2,X1,X0) ).
cnf(u1244,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,n0,X36,X35,X34,X33,X32,X31,n1,X30,n1,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,X5,X4,X3,X2,X1,X0) ).
cnf(u1250,axiom,
~ p(n0,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,n1,X30,n1,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,n1,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u1256,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,n1,X36,n1,X35,X34,X33,X32,X31,X30,X29,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,n1,X1,X0) ).
cnf(u1262,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,n1,X36,n1,X35,X34,X33,X32,n0,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,n1,X5,X4,X3,X2,X1,X0) ).
cnf(u1268,axiom,
~ p(X44,X43,X42,X41,X40,X39,X38,n1,X37,n1,X36,X35,X34,X33,X32,X31,X30,X29,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,X4,X3,X2,X1,X0) ).
cnf(u1274,axiom,
~ p(n0,X43,X42,X41,X40,X39,X38,n1,X37,n1,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,n1,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u1280,axiom,
~ p(n1,X43,n1,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,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,n1,X2,X1,X0) ).
cnf(u1286,axiom,
~ p(n1,X43,n1,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,n0,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,n1,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u1292,axiom,
~ p(n1,X43,n1,X42,X41,X40,X39,n0,X38,X37,X36,X35,X34,X33,X32,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,X5,X4,X3,X2,X1,X0) ).
cnf(u1298,axiom,
~ p(n1,X44,n1,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,n1,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u1304,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,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(u1310,axiom,
~ p(X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,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,n0,X3,X2,X1,X0) ).
cnf(u1316,axiom,
~ p(X42,X41,X40,X39,X38,X37,X36,n1,X35,X34,X33,X32,X31,n1,X30,X29,X28,X27,X26,X25,X24,n1,n1,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,n0,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u1322,axiom,
~ p(n1,X42,X41,X40,X39,X38,n1,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,n1,n1,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,n0,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u1328,axiom,
~ p(X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,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(u1334,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,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,n0,X4,X3,X2,X1,X0) ).
cnf(u1340,axiom,
~ p(X42,X41,X40,X39,X38,X37,X36,n1,X35,X34,X33,X32,X31,n1,n1,n1,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,n0,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u1346,axiom,
~ p(n1,X42,X41,X40,X39,X38,n1,X37,X36,X35,X34,X33,X32,X31,n1,n1,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,n0,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u1352,axiom,
~ p(X42,X41,X40,X39,X38,X37,X36,n1,n1,X35,X34,X33,X32,X31,X30,X29,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,n0,X1,X0) ).
cnf(u1358,axiom,
~ p(X42,X41,X40,X39,X38,X37,X36,n1,n1,X35,X34,X33,X32,X31,n1,X30,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,n0,X5,X4,X3,X2,X1,X0) ).
cnf(u1364,axiom,
~ p(X43,X42,X41,X40,X39,X38,X37,n1,n1,X36,X35,X34,X33,n1,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,n0,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u1376,axiom,
~ p(n1,n1,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,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,n0,X2,X1,X0) ).
cnf(u1382,axiom,
~ p(n1,n1,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,n1,X30,X29,X28,X27,X26,n1,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,n0,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u1388,axiom,
~ p(n1,n1,X42,X41,X40,X39,X38,n1,X37,X36,X35,X34,X33,n1,X32,X31,X30,X29,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,X0) ).
cnf(u10187,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,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44) ).
cnf(u404,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u448,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u12889,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,X23,X24,n0,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38) ).
cnf(u430,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u442,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u284,axiom,
( p(n1,X45,X44,X43,X42,n1,X41,X40,X39,X38,X37,X36,X35,X34,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)
| ~ p(n1,X45,X44,X43,X42,n0,X41,X40,X39,X38,X37,X36,X35,X34,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) ) ).
cnf(u288,axiom,
( p(X44,X43,X42,X41,X40,X39,X38,n1,n0,X37,X36,n1,X35,X34,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)
| ~ p(X44,X43,X42,X41,X40,X39,X38,n1,n0,X37,X36,n0,X35,X34,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) ) ).
cnf(u392,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u452,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u374,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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 = X42
| n1 = X42 ) ).
cnf(u418,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u396,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u281,axiom,
( p(n1,n0,n1,n0,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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)
| ~ p(n1,n0,n0,n0,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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) ) ).
cnf(u422,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u12243,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,X29,X30,X31,X32,n1,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42) ).
cnf(u11992,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,X29,X30,X31,X32,n1,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42) ).
cnf(u13124,axiom,
~ p(n1,X0,n1,n1,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,n0,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,n1,X26,X27,X28,X29,X30,X31,X32,X33,X34,n0,X35,X36,X37,X38,X39,X40,X41) ).
cnf(u440,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u11316,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,X27,X28,X29,X30,n0,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41) ).
cnf(u398,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u410,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u12115,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,n1,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,n0,X40,X41) ).
cnf(u11314,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,X26,n1,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,n0,X39,X40,X41) ).
cnf(u372,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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 = X43
| n1 = X43 ) ).
cnf(u370,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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 = X44
| n1 = X44 ) ).
cnf(u416,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u444,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u326,axiom,
( p(X43,X42,X41,X40,X39,X38,X37,n1,X36,X35,n1,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,n1,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,n1,X5,X4,X3,X2,X1,X0)
| ~ p(X43,X42,X41,X40,X39,X38,X37,n1,X36,X35,n1,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,n1,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,n0,X5,X4,X3,X2,X1,X0) ) ).
cnf(u12578,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,X25,X26,n0,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40) ).
cnf(u282,axiom,
( p(n1,n0,n0,n1,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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)
| ~ p(n1,n0,n0,n0,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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) ) ).
cnf(u285,axiom,
( p(X43,X42,X41,X40,X39,X38,X37,n1,n1,n0,X36,n0,X35,X34,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)
| ~ p(X43,X42,X41,X40,X39,X38,X37,n1,n0,n0,X36,n0,X35,X34,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) ) ).
cnf(u386,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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 = X36
| n1 = X36 ) ).
cnf(u458,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u420,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u283,axiom,
( p(n1,n0,X44,X43,n1,X42,X41,X40,X39,X38,X37,X36,X35,X34,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)
| ~ p(n1,n0,X44,X43,n0,X42,X41,X40,X39,X38,X37,X36,X35,X34,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) ) ).
cnf(u11998,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,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,n1,X36,X37,X38,X39,X40,X41) ).
cnf(u446,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u13472,axiom,
~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,n1,X14,n1,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,n1,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,n0,X39,X40,X41,X42,X43) ).
cnf(u390,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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 = X34
| n1 = X34 ) ).
cnf(u252,axiom,
( p(n1,X42,X41,X40,X39,X38,n1,n1,n1,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,n1,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| ~ p(n1,X42,X41,X40,X39,X38,n1,n1,n1,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,X14,n0,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u11201,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,X26,X27,n1,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42) ).
cnf(u364,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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 = X47
| n1 = X47 ) ).
cnf(u408,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u11194,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,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,n1,X39,X40,X41) ).
cnf(u13260,axiom,
~ p(X0,X1,X2,X3,X4,X5,X6,n1,X7,n1,n1,X8,X9,X10,n0,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,n1,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,n0,X36,X37,X38,X39,X40,X41) ).
cnf(u434,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u12244,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,X27,X28,n1,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42) ).
cnf(u280,axiom,
( p(n1,n1,n0,X43,n0,X42,X41,X40,X39,X38,X37,X36,X35,X34,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)
| ~ p(n1,n0,n0,X43,n0,X42,X41,X40,X39,X38,X37,X36,X35,X34,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) ) ).
cnf(u384,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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 = X37
| n1 = X37 ) ).
cnf(u412,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u456,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u12649,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,X25,X26,n0,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40) ).
cnf(u366,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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 = X46
| n1 = X46 ) ).
cnf(u378,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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 = X40
| n1 = X40 ) ).
cnf(u438,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u11199,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,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,n1,X35,X36,X37,X38,X39,X40,X41) ).
cnf(u287,axiom,
( p(X43,X42,X41,X40,X39,X38,X37,n1,n0,n0,n1,X36,X35,X34,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)
| ~ p(X43,X42,X41,X40,X39,X38,X37,n1,n0,n0,n0,X36,X35,X34,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) ) ).
cnf(u11436,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,X28,X29,X30,X31,n1,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42) ).
cnf(u388,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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 = X35
| n1 = X35 ) ).
cnf(u460,negated_conjecture,
~ p(X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,n1,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ).
cnf(u247,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,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0) ).
cnf(u11434,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,X26,X27,n0,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,n1,X40,X41,X42) ).
cnf(u414,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u426,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u432,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u286,axiom,
( p(X43,X42,X41,X40,X39,X38,X37,n1,n0,n1,n0,X36,X35,X34,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)
| ~ p(X43,X42,X41,X40,X39,X38,X37,n1,n0,n0,n0,X36,X35,X34,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) ) ).
cnf(u402,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u376,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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 = X41
| n1 = X41 ) ).
cnf(u10893,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,X26,X27,n0,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42) ).
cnf(u436,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u346,axiom,
( p(X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,n1,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,n1,X4,X3,X2,X1,X0)
| ~ p(X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,n1,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,n0,X4,X3,X2,X1,X0) ) ).
cnf(u289,axiom,
( p(X45,X44,X43,X42,X41,X40,X39,n1,X38,X37,X36,X35,n1,X34,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)
| ~ p(X45,X44,X43,X42,X41,X40,X39,n1,X38,X37,X36,X35,n0,X34,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) ) ).
cnf(u406,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u380,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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 = X39
| n1 = X39 ) ).
cnf(u248,axiom,
( p(n1,n1,X43,X42,X41,X40,n1,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,n1,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| ~ p(n1,n1,X43,X42,X41,X40,n1,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,X15,n0,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u424,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u10889,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,X25,X26,n0,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41) ).
cnf(u322,axiom,
( p(n1,X43,X42,n1,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,n1,X15,X14,X13,X12,X11,X10,X9,X8,X7,n1,X6,X5,X4,X3,X2,X1,X0)
| ~ p(n1,X43,X42,n1,X41,X40,X39,X38,X37,X36,X35,X34,X33,X32,X31,X30,X29,X28,X27,X26,X25,X24,X23,X22,X21,X20,X19,X18,X17,X16,n1,X15,X14,X13,X12,X11,X10,X9,X8,X7,n0,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u394,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u454,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u11991,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,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,n1,X40,X41) ).
cnf(u368,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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 = X45
| n1 = X45 ) ).
cnf(u400,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u428,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u450,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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(u11437,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,X26,X27,n1,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42) ).
cnf(u382,axiom,
( ~ p(X47,X46,X45,X44,X43,X42,X41,X40,X39,X38,X37,X36,X35,X34,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 = X38
| n1 = X38 ) ).
cnf(u12241,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,X26,X27,n0,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,n1,X41,X42) ).
cnf(u300,axiom,
( p(n1,X45,X44,X43,X42,X41,n0,X40,X39,X38,X37,X36,X35,X34,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)
| ~ p(n1,X45,X44,X43,X42,X41,n1,X40,X39,X38,X37,X36,X35,X34,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) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV485+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 % Computer : n010.cluster.edu
% 0.08/0.21 % Model : x86_64 x86_64
% 0.08/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.21 % Memory : 8046.5625MB
% 0.08/0.21 % OS : Linux 6.8.0-71-generic
% 0.08/0.21 % CPULimit : 300
% 0.08/0.21 % WCLimit : 300
% 0.08/0.21 % DateTime : Mon Sep 28 11:14:48 UTC 2026
% 0.08/0.21 % CPUTime :
% 0.08/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.26 Running first-order model finding
% 0.08/0.26 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.62/1.17 % (1858399)Will run a generic schedule for satisfiability detection.
% 5.62/1.17 % (1858410)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1574081886:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.62/1.17 % (1858409)dis+10_1_sil=32000:sp=arity:random_seed=340552539:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.62/1.17 % (1858406)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1012346872_2999 on theBenchmark for (2999ds/0Mi)
% 5.62/1.17 % (1858411)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3338846699:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.62/1.17 % (1858407)% WARNING: option uhcvi not known.
% 5.62/1.17 % (1858412)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3890430122:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.62/1.17 % (1858408)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2047021764:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.62/1.17 % (1858407)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4048110664:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.62/1.17 % (1858410)Instruction limit reached!
% 5.62/1.17 % (1858410)------------------------------
% 5.62/1.17 % (1858410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.62/1.17 % (1858410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.17 % (1858410)CaDiCaL version: 2.1.3
% 5.62/1.17 % (1858410)Termination reason: Instruction limit
% 5.62/1.17 % (1858410)Termination phase: Saturation
% 5.62/1.17 % (1858410)Time elapsed: 0.047 s
% 5.62/1.17 % (1858410)Peak memory usage: 13 MB
% 5.62/1.17 % (1858410)Instructions burned: 118 (million)
% 5.62/1.17 % (1858424)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2597191096:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 5.62/1.17 % (1858409)Instruction limit reached!
% 5.62/1.17 % (1858409)------------------------------
% 5.62/1.17 % (1858409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.62/1.17 % (1858409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.17 % (1858409)CaDiCaL version: 2.1.3
% 5.62/1.17 % (1858409)Termination reason: Instruction limit
% 5.62/1.17 % (1858409)Termination phase: Saturation
% 5.62/1.17 % (1858409)Time elapsed: 0.082 s
% 5.62/1.17 % (1858409)Peak memory usage: 13 MB
% 5.62/1.17 % (1858409)Instructions burned: 103 (million)
% 5.62/1.17 % (1858411)Instruction limit reached!
% 5.62/1.17 % (1858411)------------------------------
% 5.62/1.17 % (1858411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.62/1.17 % (1858411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.17 % (1858411)CaDiCaL version: 2.1.3
% 5.62/1.17 % (1858411)Termination reason: Instruction limit
% 5.62/1.17 % (1858411)Termination phase: Saturation
% 5.62/1.17 % (1858411)Time elapsed: 0.104 s
% 5.62/1.17 % (1858411)Peak memory usage: 13 MB
% 5.62/1.17 % (1858411)Instructions burned: 131 (million)
% 5.62/1.17 % (1858426)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2443861266:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 5.62/1.17 % (1858428)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=1913310293:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 5.62/1.17 % (1858412)Instruction limit reached!
% 5.62/1.17 % (1858412)------------------------------
% 5.62/1.17 % (1858412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.62/1.17 % (1858412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.17 % (1858412)CaDiCaL version: 2.1.3
% 5.62/1.17 % (1858412)Termination reason: Instruction limit
% 5.62/1.17 % (1858412)Termination phase: Saturation
% 5.62/1.17 % (1858412)Time elapsed: 0.177 s
% 5.62/1.17 % (1858412)Peak memory usage: 13 MB
% 5.62/1.17 % (1858412)Instructions burned: 159 (million)
% 5.62/1.17 % (1858426)Instruction limit reached!
% 5.62/1.17 % (1858426)------------------------------
% 5.62/1.17 % (1858426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.62/1.17 % (1858426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.17 % (1858426)CaDiCaL version: 2.1.3
% 5.62/1.17 % (1858426)Termination reason: Instruction limit
% 5.62/1.17 % (1858426)Termination phase: Saturation
% 5.62/1.17 % (1858426)Time elapsed: 0.098 s
% 5.62/1.17 % (1858426)Peak memory usage: 14 MB
% 5.62/1.17 % (1858426)Instructions burned: 131 (million)
% 5.62/1.17 % (1858431)ott-21_1_sil=16000:fs=off:random_seed=32902396:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 5.62/1.17 % (1858432)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1181093912:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 5.62/1.17 % (1858431)Instruction limit reached!
% 5.62/1.17 % (1858431)------------------------------
% 5.62/1.17 % (1858431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.62/1.17 % (1858431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.17 % (1858431)CaDiCaL version: 2.1.3
% 5.62/1.17 % (1858431)Termination reason: Instruction limit
% 5.62/1.17 % (1858431)Termination phase: Saturation
% 5.62/1.17 % (1858431)Time elapsed: 0.096 s
% 5.62/1.17 % (1858431)Peak memory usage: 12 MB
% 5.62/1.17 % (1858431)Instructions burned: 182 (million)
% 5.62/1.17 % (1858435)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=701401258:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 5.62/1.17 % (1858424)Instruction limit reached!
% 5.62/1.17 % (1858424)------------------------------
% 5.62/1.17 % (1858424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.62/1.17 % (1858424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.17 % (1858424)CaDiCaL version: 2.1.3
% 5.62/1.17 % (1858424)Termination reason: Instruction limit
% 5.62/1.17 % (1858424)Termination phase: Finite model building preprocessing
% 5.62/1.17 % (1858424)Time elapsed: 0.284 s
% 5.62/1.17 % (1858424)Peak memory usage: 13 MB
% 5.62/1.17 % (1858424)Instructions burned: 718 (million)
% 5.62/1.17 % (1858437)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2801772357:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 5.62/1.17 % Detected minimum model sizes of [1]
% 5.62/1.17 % Detected maximum model sizes of [2]
% 5.62/1.17 % TRYING [1]
% 5.62/1.17 % (1858406)Cannot represent all propositional literals internally
% 5.62/1.17 % (1858406)Refutation not found, incomplete strategy
% 5.62/1.17 % (1858406)------------------------------
% 5.62/1.17 % (1858406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.62/1.17 % (1858406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.17 % (1858406)CaDiCaL version: 2.1.3
% 5.62/1.17 % (1858406)Termination reason: Refutation not found, incomplete strategy
% 5.62/1.17 % (1858406)Time elapsed: 0.461 s
% 5.62/1.17 % (1858406)Peak memory usage: 17 MB
% 5.62/1.17 % (1858406)Instructions burned: 822 (million)
% 5.62/1.17 % (1858406)------------------------------
% 5.62/1.17 % (1858406)------------------------------
% 5.62/1.17 % (1858428)Instruction limit reached!
% 5.62/1.17 % (1858428)------------------------------
% 5.62/1.17 % (1858428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.62/1.17 % (1858428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.17 % (1858428)CaDiCaL version: 2.1.3
% 5.62/1.17 % (1858428)Termination reason: Instruction limit
% 5.62/1.17 % (1858428)Termination phase: Saturation
% 5.62/1.17 % (1858428)Time elapsed: 0.328 s
% 5.62/1.17 % (1858428)Peak memory usage: 14 MB
% 5.62/1.17 % (1858428)Instructions burned: 685 (million)
% 5.62/1.17 % (1858432)Instruction limit reached!
% 5.62/1.17 % (1858432)------------------------------
% 5.62/1.17 % (1858432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.62/1.17 % (1858432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.17 % (1858432)CaDiCaL version: 2.1.3
% 5.62/1.17 % (1858432)Termination reason: Instruction limit
% 5.62/1.17 % (1858432)Termination phase: Saturation
% 5.62/1.17 % (1858432)Time elapsed: 0.249 s
% 5.62/1.17 % (1858432)Peak memory usage: 16 MB
% 5.62/1.17 % (1858432)Instructions burned: 477 (million)
% 5.62/1.17 % (1858440)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3046426373:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 5.62/1.17 % (1858441)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=2875015193: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)
% 5.62/1.17 % (1858442)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3204445438:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 5.62/1.17 % (1858437)Instruction limit reached!
% 5.62/1.17 % (1858437)------------------------------
% 5.62/1.17 % (1858437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.62/1.17 % (1858437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.17 % (1858437)CaDiCaL version: 2.1.3
% 5.62/1.17 % (1858437)Termination reason: Instruction limit
% 5.62/1.17 % (1858437)Termination phase: Saturation
% 5.62/1.17 % (1858437)Time elapsed: 0.291 s
% 5.62/1.17 % (1858437)Peak memory usage: 16 MB
% 5.62/1.17 % (1858437)Instructions burned: 1183 (million)
% 5.62/1.17 % (1858500)fmb+10_1_sil=64000:random_seed=2579607326:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 5.62/1.17 % Detected minimum model sizes of [1]
% 5.62/1.17 % Detected maximum model sizes of [2]
% 5.62/1.17 % TRYING [1]
% 5.62/1.17 % (1858435)Cannot represent all propositional literals internally
% 5.62/1.17 % (1858435)Refutation not found, incomplete strategy
% 5.62/1.17 % (1858435)------------------------------
% 5.62/1.17 % (1858435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.62/1.17 % (1858435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.17 % (1858435)CaDiCaL version: 2.1.3
% 5.62/1.17 % (1858435)Termination reason: Refutation not found, incomplete strategy
% 5.62/1.17 % (1858435)Time elapsed: 0.399 s
% 5.62/1.17 % (1858435)Peak memory usage: 16 MB
% 5.62/1.17 % (1858435)Instructions burned: 792 (million)
% 5.62/1.17 % (1858435)------------------------------
% 5.62/1.17 % (1858435)------------------------------
% 5.62/1.17 % (1858533)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2456536389:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi)
% 5.62/1.17 % (1858441)Instruction limit reached!
% 5.62/1.17 % (1858441)------------------------------
% 5.62/1.17 % (1858441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.62/1.17 % (1858441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.17 % (1858441)CaDiCaL version: 2.1.3
% 5.62/1.17 % (1858441)Termination reason: Instruction limit
% 5.62/1.17 % (1858441)Termination phase: Saturation
% 5.62/1.17 % (1858441)Time elapsed: 0.317 s
% 5.62/1.17 % (1858441)Peak memory usage: 14 MB
% 5.62/1.17 % (1858441)Instructions burned: 693 (million)
% 5.62/1.17 % (1858555)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=944362508:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 5.62/1.17 % (1858442) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1858399-1858442"...
% 5.62/1.17 % (1858442)...printing done.
% 5.62/1.17 % SZS status CounterSatisfiable for theBenchmark
% 5.62/1.17 % SZS output start Saturation.
% See solution above
% 5.62/1.17 % SZS output start Definitions and Model Updates.
% 5.62/1.17 % SZS output end Definitions and Model Updates.
% 5.62/1.17 % (1858442)------------------------------
% 5.62/1.17 % (1858442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.62/1.17 % (1858442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.17 % (1858442)CaDiCaL version: 2.1.3
% 5.62/1.17 % (1858442)Termination reason: Satisfiable
% 5.62/1.17 % (1858442)Time elapsed: 0.345 s
% 5.62/1.17 % (1858442)Peak memory usage: 17 MB
% 5.62/1.17 % (1858442)Instructions burned: 692 (million)
% 5.62/1.17 % (1858399)Success in time 0.904 s
% 5.62/1.17 % Vampire exiting
%------------------------------------------------------------------------------