%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PUZ138+2 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:31:42 PM UTC 2026
% Result : Satisfiable 9.94s 2.45s
% Output : Saturation 10.56s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u31311,axiom,
~ p(n9,n9,n9) ).
cnf(u31315,axiom,
~ p(n9,n8,n9) ).
cnf(u31319,axiom,
~ p(n9,n7,n9) ).
cnf(u31323,axiom,
~ p(n8,n9,n9) ).
cnf(u31327,axiom,
~ p(n8,n8,n9) ).
cnf(u31331,axiom,
~ p(n8,n7,n9) ).
cnf(u31335,axiom,
~ p(n7,n9,n9) ).
cnf(u31340,axiom,
p(n7,n8,n9) ).
cnf(u31343,axiom,
~ p(n7,n7,n9) ).
cnf(u31349,axiom,
p(n9,n9,n8) ).
cnf(u31352,axiom,
~ p(n9,n8,n8) ).
cnf(u31356,axiom,
~ p(n9,n7,n8) ).
cnf(u31360,axiom,
~ p(n8,n9,n8) ).
cnf(u31364,axiom,
~ p(n8,n8,n8) ).
cnf(u31368,axiom,
~ p(n8,n7,n8) ).
cnf(u31372,axiom,
~ p(n7,n9,n8) ).
cnf(u31376,axiom,
~ p(n7,n8,n8) ).
cnf(u31380,axiom,
~ p(n7,n7,n8) ).
cnf(u31385,axiom,
~ p(n9,n9,n7) ).
cnf(u31389,axiom,
~ p(n9,n8,n7) ).
cnf(u31393,axiom,
~ p(n9,n7,n7) ).
cnf(u31398,axiom,
p(n8,n9,n7) ).
cnf(u31401,axiom,
~ p(n8,n8,n7) ).
cnf(u31405,axiom,
~ p(n8,n7,n7) ).
cnf(u31409,axiom,
~ p(n7,n9,n7) ).
cnf(u31413,axiom,
~ p(n7,n8,n7) ).
cnf(u31417,axiom,
~ p(n7,n7,n7) ).
cnf(u31422,axiom,
~ p(n9,n9,n6) ).
cnf(u31426,axiom,
~ p(n9,n8,n6) ).
cnf(u31430,axiom,
~ p(n9,n7,n6) ).
cnf(u31434,axiom,
~ p(n8,n9,n6) ).
cnf(u31439,axiom,
p(n8,n8,n6) ).
cnf(u31442,axiom,
~ p(n8,n7,n6) ).
cnf(u31446,axiom,
~ p(n7,n9,n6) ).
cnf(u31450,axiom,
~ p(n7,n8,n6) ).
cnf(u31454,axiom,
~ p(n7,n7,n6) ).
cnf(u31459,axiom,
~ p(n9,n9,n4) ).
cnf(u31463,axiom,
~ p(n9,n8,n4) ).
cnf(u31467,axiom,
~ p(n9,n7,n4) ).
cnf(u31471,axiom,
~ p(n8,n9,n4) ).
cnf(u31475,axiom,
~ p(n8,n8,n4) ).
cnf(u31479,axiom,
~ p(n8,n7,n4) ).
cnf(u31484,axiom,
p(n7,n9,n4) ).
cnf(u31487,axiom,
~ p(n7,n8,n4) ).
cnf(u31491,axiom,
~ p(n7,n7,n4) ).
cnf(u31496,axiom,
~ p(n9,n9,n3) ).
cnf(u31501,axiom,
p(n9,n8,n3) ).
cnf(u31504,axiom,
~ p(n9,n7,n3) ).
cnf(u31508,axiom,
~ p(n8,n9,n3) ).
cnf(u31512,axiom,
~ p(n8,n8,n3) ).
cnf(u31516,axiom,
~ p(n8,n7,n3) ).
cnf(u31520,axiom,
~ p(n7,n9,n3) ).
cnf(u31524,axiom,
~ p(n7,n8,n3) ).
cnf(u31528,axiom,
~ p(n7,n7,n3) ).
cnf(u31533,axiom,
~ p(n9,n9,n2) ).
cnf(u31537,axiom,
~ p(n9,n8,n2) ).
cnf(u31542,axiom,
p(n9,n7,n2) ).
cnf(u31545,axiom,
~ p(n8,n9,n2) ).
cnf(u31549,axiom,
~ p(n8,n8,n2) ).
cnf(u31553,axiom,
~ p(n8,n7,n2) ).
cnf(u31557,axiom,
~ p(n7,n9,n2) ).
cnf(u31561,axiom,
~ p(n7,n8,n2) ).
cnf(u31565,axiom,
~ p(n7,n7,n2) ).
cnf(u31570,axiom,
~ p(n9,n9,n1) ).
cnf(u31574,axiom,
~ p(n9,n8,n1) ).
cnf(u31578,axiom,
~ p(n9,n7,n1) ).
cnf(u31582,axiom,
~ p(n8,n9,n1) ).
cnf(u31586,axiom,
~ p(n8,n8,n1) ).
cnf(u31590,axiom,
~ p(n8,n7,n1) ).
cnf(u31594,axiom,
~ p(n7,n9,n1) ).
cnf(u31598,axiom,
~ p(n7,n8,n1) ).
cnf(u31603,axiom,
p(n7,n7,n1) ).
cnf(u31607,axiom,
~ p(n9,n6,n9) ).
cnf(u31611,axiom,
~ p(n9,n5,n9) ).
cnf(u31616,axiom,
p(n9,n4,n9) ).
cnf(u31619,axiom,
~ p(n8,n6,n9) ).
cnf(u31623,axiom,
~ p(n8,n5,n9) ).
cnf(u31627,axiom,
~ p(n8,n4,n9) ).
cnf(u31631,axiom,
~ p(n7,n6,n9) ).
cnf(u31635,axiom,
~ p(n7,n5,n9) ).
cnf(u31639,axiom,
~ p(n7,n4,n9) ).
cnf(u31644,axiom,
~ p(n9,n6,n8) ).
cnf(u31648,axiom,
~ p(n9,n5,n8) ).
cnf(u31652,axiom,
~ p(n9,n4,n8) ).
cnf(u31657,axiom,
p(n8,n6,n8) ).
cnf(u31660,axiom,
~ p(n8,n5,n8) ).
cnf(u31664,axiom,
~ p(n8,n4,n8) ).
cnf(u31668,axiom,
~ p(n7,n6,n8) ).
cnf(u31672,axiom,
~ p(n7,n5,n8) ).
cnf(u31676,axiom,
~ p(n7,n4,n8) ).
cnf(u31681,axiom,
~ p(n9,n6,n7) ).
cnf(u31685,axiom,
~ p(n9,n5,n7) ).
cnf(u31689,axiom,
~ p(n9,n4,n7) ).
cnf(u31693,axiom,
~ p(n8,n6,n7) ).
cnf(u31697,axiom,
~ p(n8,n5,n7) ).
cnf(u31701,axiom,
~ p(n8,n4,n7) ).
cnf(u31706,axiom,
p(n7,n6,n7) ).
cnf(u31709,axiom,
~ p(n7,n5,n7) ).
cnf(u31713,axiom,
~ p(n7,n4,n7) ).
cnf(u31718,axiom,
~ p(n9,n6,n3) ).
cnf(u31722,axiom,
~ p(n9,n5,n3) ).
cnf(u31726,axiom,
~ p(n9,n4,n3) ).
cnf(u31730,axiom,
~ p(n8,n6,n3) ).
cnf(u31734,axiom,
~ p(n8,n5,n3) ).
cnf(u31738,axiom,
~ p(n8,n4,n3) ).
cnf(u31742,axiom,
~ p(n7,n6,n3) ).
cnf(u31747,axiom,
p(n7,n5,n3) ).
cnf(u31750,axiom,
~ p(n7,n4,n3) ).
cnf(u31755,axiom,
~ p(n9,n6,n2) ).
cnf(u31759,axiom,
~ p(n9,n5,n2) ).
cnf(u31763,axiom,
~ p(n9,n4,n2) ).
cnf(u31767,axiom,
~ p(n8,n6,n2) ).
cnf(u31771,axiom,
~ p(n8,n5,n2) ).
cnf(u31776,axiom,
p(n8,n4,n2) ).
cnf(u31779,axiom,
~ p(n7,n6,n2) ).
cnf(u31783,axiom,
~ p(n7,n5,n2) ).
cnf(u31787,axiom,
~ p(n7,n4,n2) ).
cnf(u31792,axiom,
~ p(n9,n6,n1) ).
cnf(u31797,axiom,
p(n9,n5,n1) ).
cnf(u31800,axiom,
~ p(n9,n4,n1) ).
cnf(u31804,axiom,
~ p(n8,n6,n1) ).
cnf(u31808,axiom,
~ p(n8,n5,n1) ).
cnf(u31812,axiom,
~ p(n8,n4,n1) ).
cnf(u31816,axiom,
~ p(n7,n6,n1) ).
cnf(u31820,axiom,
~ p(n7,n5,n1) ).
cnf(u31824,axiom,
~ p(n7,n4,n1) ).
cnf(u31829,axiom,
~ p(n9,n3,n6) ).
cnf(u31833,axiom,
~ p(n9,n2,n6) ).
cnf(u31837,axiom,
~ p(n9,n1,n6) ).
cnf(u31841,axiom,
~ p(n8,n3,n6) ).
cnf(u31845,axiom,
~ p(n8,n2,n6) ).
cnf(u31849,axiom,
~ p(n8,n1,n6) ).
cnf(u31853,axiom,
~ p(n7,n3,n6) ).
cnf(u31857,axiom,
~ p(n7,n2,n6) ).
cnf(u31862,axiom,
p(n7,n1,n6) ).
cnf(u31867,axiom,
p(n9,n3,n5) ).
cnf(u31870,axiom,
~ p(n9,n2,n5) ).
cnf(u31874,axiom,
~ p(n9,n1,n5) ).
cnf(u31878,axiom,
~ p(n8,n3,n5) ).
cnf(u31882,axiom,
~ p(n8,n2,n5) ).
cnf(u31886,axiom,
~ p(n8,n1,n5) ).
cnf(u31890,axiom,
~ p(n7,n3,n5) ).
cnf(u31894,axiom,
~ p(n7,n2,n5) ).
cnf(u31898,axiom,
~ p(n7,n1,n5) ).
cnf(u31903,axiom,
~ p(n9,n3,n3) ).
cnf(u31907,axiom,
~ p(n9,n2,n3) ).
cnf(u31911,axiom,
~ p(n9,n1,n3) ).
cnf(u31916,axiom,
p(n8,n3,n3) ).
cnf(u31919,axiom,
~ p(n8,n2,n3) ).
cnf(u31923,axiom,
~ p(n8,n1,n3) ).
cnf(u31927,axiom,
~ p(n7,n3,n3) ).
cnf(u31931,axiom,
~ p(n7,n2,n3) ).
cnf(u31935,axiom,
~ p(n7,n1,n3) ).
cnf(u31940,axiom,
~ p(n9,n3,n2) ).
cnf(u31944,axiom,
~ p(n9,n2,n2) ).
cnf(u31948,axiom,
~ p(n9,n1,n2) ).
cnf(u31952,axiom,
~ p(n8,n3,n2) ).
cnf(u31956,axiom,
~ p(n8,n2,n2) ).
cnf(u31960,axiom,
~ p(n8,n1,n2) ).
cnf(u31964,axiom,
~ p(n7,n3,n2) ).
cnf(u31969,axiom,
p(n7,n2,n2) ).
cnf(u31972,axiom,
~ p(n7,n1,n2) ).
cnf(u31977,axiom,
~ p(n9,n3,n1) ).
cnf(u31981,axiom,
~ p(n9,n2,n1) ).
cnf(u31985,axiom,
~ p(n9,n1,n1) ).
cnf(u31989,axiom,
~ p(n8,n3,n1) ).
cnf(u31994,axiom,
p(n8,n2,n1) ).
cnf(u31997,axiom,
~ p(n8,n1,n1) ).
cnf(u32001,axiom,
~ p(n7,n3,n1) ).
cnf(u32005,axiom,
~ p(n7,n2,n1) ).
cnf(u32009,axiom,
~ p(n7,n1,n1) ).
cnf(u32014,axiom,
~ p(n6,n9,n9) ).
cnf(u32018,axiom,
~ p(n6,n8,n9) ).
cnf(u32022,axiom,
~ p(n6,n7,n9) ).
cnf(u32027,axiom,
p(n5,n9,n9) ).
cnf(u32030,axiom,
~ p(n5,n8,n9) ).
cnf(u32034,axiom,
~ p(n5,n7,n9) ).
cnf(u32038,axiom,
~ p(n4,n9,n9) ).
cnf(u32042,axiom,
~ p(n4,n8,n9) ).
cnf(u32046,axiom,
~ p(n4,n7,n9) ).
cnf(u32051,axiom,
~ p(n6,n9,n7) ).
cnf(u32055,axiom,
~ p(n6,n8,n7) ).
cnf(u32059,axiom,
~ p(n6,n7,n7) ).
cnf(u32063,axiom,
~ p(n5,n9,n7) ).
cnf(u32067,axiom,
~ p(n5,n8,n7) ).
cnf(u32071,axiom,
~ p(n5,n7,n7) ).
cnf(u32075,axiom,
~ p(n4,n9,n7) ).
cnf(u32080,axiom,
p(n4,n8,n7) ).
cnf(u32083,axiom,
~ p(n4,n7,n7) ).
cnf(u32088,axiom,
~ p(n6,n9,n6) ).
cnf(u32092,axiom,
~ p(n6,n8,n6) ).
cnf(u32096,axiom,
~ p(n6,n7,n6) ).
cnf(u32100,axiom,
~ p(n5,n9,n6) ).
cnf(u32104,axiom,
~ p(n5,n8,n6) ).
cnf(u32108,axiom,
~ p(n5,n7,n6) ).
cnf(u32112,axiom,
~ p(n4,n9,n6) ).
cnf(u32116,axiom,
~ p(n4,n8,n6) ).
cnf(u32121,axiom,
p(n4,n7,n6) ).
cnf(u32125,axiom,
~ p(n6,n9,n4) ).
cnf(u32130,axiom,
p(n6,n8,n4) ).
cnf(u32133,axiom,
~ p(n6,n7,n4) ).
cnf(u32137,axiom,
~ p(n5,n9,n4) ).
cnf(u32141,axiom,
~ p(n5,n8,n4) ).
cnf(u32145,axiom,
~ p(n5,n7,n4) ).
cnf(u32149,axiom,
~ p(n4,n9,n4) ).
cnf(u32153,axiom,
~ p(n4,n8,n4) ).
cnf(u32157,axiom,
~ p(n4,n7,n4) ).
cnf(u32162,axiom,
~ p(n6,n9,n3) ).
cnf(u32166,axiom,
~ p(n6,n8,n3) ).
cnf(u32171,axiom,
p(n6,n7,n3) ).
cnf(u32174,axiom,
~ p(n5,n9,n3) ).
cnf(u32178,axiom,
~ p(n5,n8,n3) ).
cnf(u32182,axiom,
~ p(n5,n7,n3) ).
cnf(u32186,axiom,
~ p(n4,n9,n3) ).
cnf(u32190,axiom,
~ p(n4,n8,n3) ).
cnf(u32194,axiom,
~ p(n4,n7,n3) ).
cnf(u32199,axiom,
~ p(n6,n9,n2) ).
cnf(u32203,axiom,
~ p(n6,n8,n2) ).
cnf(u32207,axiom,
~ p(n6,n7,n2) ).
cnf(u32211,axiom,
~ p(n5,n9,n2) ).
cnf(u32216,axiom,
p(n5,n8,n2) ).
cnf(u32219,axiom,
~ p(n5,n7,n2) ).
cnf(u32223,axiom,
~ p(n4,n9,n2) ).
cnf(u32227,axiom,
~ p(n4,n8,n2) ).
cnf(u32231,axiom,
~ p(n4,n7,n2) ).
cnf(u32237,axiom,
p(n6,n9,n1) ).
cnf(u32240,axiom,
~ p(n6,n8,n1) ).
cnf(u32244,axiom,
~ p(n6,n7,n1) ).
cnf(u32248,axiom,
~ p(n5,n9,n1) ).
cnf(u32252,axiom,
~ p(n5,n8,n1) ).
cnf(u32256,axiom,
~ p(n5,n7,n1) ).
cnf(u32260,axiom,
~ p(n4,n9,n1) ).
cnf(u32264,axiom,
~ p(n4,n8,n1) ).
cnf(u32268,axiom,
~ p(n4,n7,n1) ).
cnf(u32273,axiom,
~ p(n6,n6,n6) ).
cnf(u32277,axiom,
~ p(n6,n5,n6) ).
cnf(u32282,axiom,
p(n6,n4,n6) ).
cnf(u32285,axiom,
~ p(n5,n6,n6) ).
cnf(u32289,axiom,
~ p(n5,n5,n6) ).
cnf(u32293,axiom,
~ p(n5,n4,n6) ).
cnf(u32297,axiom,
~ p(n4,n6,n6) ).
cnf(u32301,axiom,
~ p(n4,n5,n6) ).
cnf(u32305,axiom,
~ p(n4,n4,n6) ).
cnf(u32310,axiom,
~ p(n6,n6,n5) ).
cnf(u32315,axiom,
p(n6,n5,n5) ).
cnf(u32318,axiom,
~ p(n6,n4,n5) ).
cnf(u32322,axiom,
~ p(n5,n6,n5) ).
cnf(u32326,axiom,
~ p(n5,n5,n5) ).
cnf(u32330,axiom,
~ p(n5,n4,n5) ).
cnf(u32334,axiom,
~ p(n4,n6,n5) ).
cnf(u32338,axiom,
~ p(n4,n5,n5) ).
cnf(u32342,axiom,
~ p(n4,n4,n5) ).
cnf(u32347,axiom,
~ p(n6,n6,n4) ).
cnf(u32351,axiom,
~ p(n6,n5,n4) ).
cnf(u32355,axiom,
~ p(n6,n4,n4) ).
cnf(u32359,axiom,
~ p(n5,n6,n4) ).
cnf(u32363,axiom,
~ p(n5,n5,n4) ).
cnf(u32367,axiom,
~ p(n5,n4,n4) ).
cnf(u32372,axiom,
p(n4,n6,n4) ).
cnf(u32375,axiom,
~ p(n4,n5,n4) ).
cnf(u32379,axiom,
~ p(n4,n4,n4) ).
cnf(u32384,axiom,
~ p(n6,n6,n3) ).
cnf(u32388,axiom,
~ p(n6,n5,n3) ).
cnf(u32392,axiom,
~ p(n6,n4,n3) ).
cnf(u32397,axiom,
p(n5,n6,n3) ).
cnf(u32400,axiom,
~ p(n5,n5,n3) ).
cnf(u32404,axiom,
~ p(n5,n4,n3) ).
cnf(u32408,axiom,
~ p(n4,n6,n3) ).
cnf(u32412,axiom,
~ p(n4,n5,n3) ).
cnf(u32416,axiom,
~ p(n4,n4,n3) ).
cnf(u32421,axiom,
~ p(n6,n6,n2) ).
cnf(u32425,axiom,
~ p(n6,n5,n2) ).
cnf(u32429,axiom,
~ p(n6,n4,n2) ).
cnf(u32433,axiom,
~ p(n5,n6,n2) ).
cnf(u32437,axiom,
~ p(n5,n5,n2) ).
cnf(u32441,axiom,
~ p(n5,n4,n2) ).
cnf(u32445,axiom,
~ p(n4,n6,n2) ).
cnf(u32450,axiom,
p(n4,n5,n2) ).
cnf(u32453,axiom,
~ p(n4,n4,n2) ).
cnf(u32458,axiom,
~ p(n6,n6,n1) ).
cnf(u32462,axiom,
~ p(n6,n5,n1) ).
cnf(u32466,axiom,
~ p(n6,n4,n1) ).
cnf(u32470,axiom,
~ p(n5,n6,n1) ).
cnf(u32474,axiom,
~ p(n5,n5,n1) ).
cnf(u32479,axiom,
p(n5,n4,n1) ).
cnf(u32482,axiom,
~ p(n4,n6,n1) ).
cnf(u32486,axiom,
~ p(n4,n5,n1) ).
cnf(u32490,axiom,
~ p(n4,n4,n1) ).
cnf(u32495,axiom,
~ p(n6,n3,n9) ).
cnf(u32499,axiom,
~ p(n6,n2,n9) ).
cnf(u32503,axiom,
~ p(n6,n1,n9) ).
cnf(u32507,axiom,
~ p(n5,n3,n9) ).
cnf(u32511,axiom,
~ p(n5,n2,n9) ).
cnf(u32515,axiom,
~ p(n5,n1,n9) ).
cnf(u32519,axiom,
~ p(n4,n3,n9) ).
cnf(u32524,axiom,
p(n4,n2,n9) ).
cnf(u32527,axiom,
~ p(n4,n1,n9) ).
cnf(u32532,axiom,
~ p(n6,n3,n8) ).
cnf(u32537,axiom,
p(n6,n2,n8) ).
cnf(u32540,axiom,
~ p(n6,n1,n8) ).
cnf(u32544,axiom,
~ p(n5,n3,n8) ).
cnf(u32548,axiom,
~ p(n5,n2,n8) ).
cnf(u32552,axiom,
~ p(n5,n1,n8) ).
cnf(u32556,axiom,
~ p(n4,n3,n8) ).
cnf(u32560,axiom,
~ p(n4,n2,n8) ).
cnf(u32564,axiom,
~ p(n4,n1,n8) ).
cnf(u32570,axiom,
p(n6,n3,n7) ).
cnf(u32573,axiom,
~ p(n6,n2,n7) ).
cnf(u32577,axiom,
~ p(n6,n1,n7) ).
cnf(u32581,axiom,
~ p(n5,n3,n7) ).
cnf(u32585,axiom,
~ p(n5,n2,n7) ).
cnf(u32589,axiom,
~ p(n5,n1,n7) ).
cnf(u32593,axiom,
~ p(n4,n3,n7) ).
cnf(u32597,axiom,
~ p(n4,n2,n7) ).
cnf(u32601,axiom,
~ p(n4,n1,n7) ).
cnf(u32606,axiom,
~ p(n6,n3,n5) ).
cnf(u32610,axiom,
~ p(n6,n2,n5) ).
cnf(u32614,axiom,
~ p(n6,n1,n5) ).
cnf(u32618,axiom,
~ p(n5,n3,n5) ).
cnf(u32622,axiom,
~ p(n5,n2,n5) ).
cnf(u32627,axiom,
p(n5,n1,n5) ).
cnf(u32630,axiom,
~ p(n4,n3,n5) ).
cnf(u32634,axiom,
~ p(n4,n2,n5) ).
cnf(u32638,axiom,
~ p(n4,n1,n5) ).
cnf(u32643,axiom,
~ p(n6,n3,n4) ).
cnf(u32647,axiom,
~ p(n6,n2,n4) ).
cnf(u32651,axiom,
~ p(n6,n1,n4) ).
cnf(u32656,axiom,
p(n5,n3,n4) ).
cnf(u32659,axiom,
~ p(n5,n2,n4) ).
cnf(u32663,axiom,
~ p(n5,n1,n4) ).
cnf(u32667,axiom,
~ p(n4,n3,n4) ).
cnf(u32671,axiom,
~ p(n4,n2,n4) ).
cnf(u32675,axiom,
~ p(n4,n1,n4) ).
cnf(u32680,axiom,
~ p(n6,n3,n3) ).
cnf(u32684,axiom,
~ p(n6,n2,n3) ).
cnf(u32688,axiom,
~ p(n6,n1,n3) ).
cnf(u32692,axiom,
~ p(n5,n3,n3) ).
cnf(u32696,axiom,
~ p(n5,n2,n3) ).
cnf(u32700,axiom,
~ p(n5,n1,n3) ).
cnf(u32704,axiom,
~ p(n4,n3,n3) ).
cnf(u32708,axiom,
~ p(n4,n2,n3) ).
cnf(u32713,axiom,
p(n4,n1,n3) ).
cnf(u32717,axiom,
~ p(n6,n3,n2) ).
cnf(u32721,axiom,
~ p(n6,n2,n2) ).
cnf(u32726,axiom,
p(n6,n1,n2) ).
cnf(u32729,axiom,
~ p(n5,n3,n2) ).
cnf(u32733,axiom,
~ p(n5,n2,n2) ).
cnf(u32737,axiom,
~ p(n5,n1,n2) ).
cnf(u32741,axiom,
~ p(n4,n3,n2) ).
cnf(u32745,axiom,
~ p(n4,n2,n2) ).
cnf(u32749,axiom,
~ p(n4,n1,n2) ).
cnf(u32754,axiom,
~ p(n3,n9,n9) ).
cnf(u32758,axiom,
~ p(n3,n8,n9) ).
cnf(u32762,axiom,
~ p(n3,n7,n9) ).
cnf(u32766,axiom,
~ p(n2,n9,n9) ).
cnf(u32770,axiom,
~ p(n2,n8,n9) ).
cnf(u32775,axiom,
p(n2,n7,n9) ).
cnf(u32778,axiom,
~ p(n1,n9,n9) ).
cnf(u32782,axiom,
~ p(n1,n8,n9) ).
cnf(u32786,axiom,
~ p(n1,n7,n9) ).
cnf(u32791,axiom,
~ p(n3,n9,n8) ).
cnf(u32796,axiom,
p(n3,n8,n8) ).
cnf(u32799,axiom,
~ p(n3,n7,n8) ).
cnf(u32803,axiom,
~ p(n2,n9,n8) ).
cnf(u32807,axiom,
~ p(n2,n8,n8) ).
cnf(u32811,axiom,
~ p(n2,n7,n8) ).
cnf(u32815,axiom,
~ p(n1,n9,n8) ).
cnf(u32819,axiom,
~ p(n1,n8,n8) ).
cnf(u32823,axiom,
~ p(n1,n7,n8) ).
cnf(u32828,axiom,
~ p(n3,n9,n7) ).
cnf(u32832,axiom,
~ p(n3,n8,n7) ).
cnf(u32836,axiom,
~ p(n3,n7,n7) ).
cnf(u32840,axiom,
~ p(n2,n9,n7) ).
cnf(u32844,axiom,
~ p(n2,n8,n7) ).
cnf(u32848,axiom,
~ p(n2,n7,n7) ).
cnf(u32852,axiom,
~ p(n1,n9,n7) ).
cnf(u32856,axiom,
~ p(n1,n8,n7) ).
cnf(u32861,axiom,
p(n1,n7,n7) ).
cnf(u32866,axiom,
p(n3,n9,n6) ).
cnf(u32869,axiom,
~ p(n3,n8,n6) ).
cnf(u32873,axiom,
~ p(n3,n7,n6) ).
cnf(u32877,axiom,
~ p(n2,n9,n6) ).
cnf(u32881,axiom,
~ p(n2,n8,n6) ).
cnf(u32885,axiom,
~ p(n2,n7,n6) ).
cnf(u32889,axiom,
~ p(n1,n9,n6) ).
cnf(u32893,axiom,
~ p(n1,n8,n6) ).
cnf(u32897,axiom,
~ p(n1,n7,n6) ).
cnf(u32902,axiom,
~ p(n3,n9,n5) ).
cnf(u32906,axiom,
~ p(n3,n8,n5) ).
cnf(u32910,axiom,
~ p(n3,n7,n5) ).
cnf(u32914,axiom,
~ p(n2,n9,n5) ).
cnf(u32919,axiom,
p(n2,n8,n5) ).
cnf(u32922,axiom,
~ p(n2,n7,n5) ).
cnf(u32926,axiom,
~ p(n1,n9,n5) ).
cnf(u32930,axiom,
~ p(n1,n8,n5) ).
cnf(u32934,axiom,
~ p(n1,n7,n5) ).
cnf(u32939,axiom,
~ p(n3,n6,n9) ).
cnf(u32944,axiom,
p(n3,n5,n9) ).
cnf(u32947,axiom,
~ p(n3,n4,n9) ).
cnf(u32951,axiom,
~ p(n2,n6,n9) ).
cnf(u32955,axiom,
~ p(n2,n5,n9) ).
cnf(u32959,axiom,
~ p(n2,n4,n9) ).
cnf(u32963,axiom,
~ p(n1,n6,n9) ).
cnf(u32967,axiom,
~ p(n1,n5,n9) ).
cnf(u32971,axiom,
~ p(n1,n4,n9) ).
cnf(u32976,axiom,
~ p(n3,n6,n8) ).
cnf(u32980,axiom,
~ p(n3,n5,n8) ).
cnf(u32984,axiom,
~ p(n3,n4,n8) ).
cnf(u32988,axiom,
~ p(n2,n6,n8) ).
cnf(u32993,axiom,
p(n2,n5,n8) ).
cnf(u32996,axiom,
~ p(n2,n4,n8) ).
cnf(u33000,axiom,
~ p(n1,n6,n8) ).
cnf(u33004,axiom,
~ p(n1,n5,n8) ).
cnf(u33008,axiom,
~ p(n1,n4,n8) ).
cnf(u33013,axiom,
~ p(n3,n6,n7) ).
cnf(u33017,axiom,
~ p(n3,n5,n7) ).
cnf(u33021,axiom,
~ p(n3,n4,n7) ).
cnf(u33025,axiom,
~ p(n2,n6,n7) ).
cnf(u33029,axiom,
~ p(n2,n5,n7) ).
cnf(u33034,axiom,
p(n2,n4,n7) ).
cnf(u33037,axiom,
~ p(n1,n6,n7) ).
cnf(u33041,axiom,
~ p(n1,n5,n7) ).
cnf(u33045,axiom,
~ p(n1,n4,n7) ).
cnf(u33050,axiom,
~ p(n3,n6,n6) ).
cnf(u33054,axiom,
~ p(n3,n5,n6) ).
cnf(u33058,axiom,
~ p(n3,n4,n6) ).
cnf(u33062,axiom,
~ p(n2,n6,n6) ).
cnf(u33066,axiom,
~ p(n2,n5,n6) ).
cnf(u33070,axiom,
~ p(n2,n4,n6) ).
cnf(u33074,axiom,
~ p(n1,n6,n6) ).
cnf(u33079,axiom,
p(n1,n5,n6) ).
cnf(u33082,axiom,
~ p(n1,n4,n6) ).
cnf(u33087,axiom,
~ p(n3,n6,n5) ).
cnf(u33091,axiom,
~ p(n3,n5,n5) ).
cnf(u33095,axiom,
~ p(n3,n4,n5) ).
cnf(u33099,axiom,
~ p(n2,n6,n5) ).
cnf(u33103,axiom,
~ p(n2,n5,n5) ).
cnf(u33107,axiom,
~ p(n2,n4,n5) ).
cnf(u33112,axiom,
p(n1,n6,n5) ).
cnf(u33115,axiom,
~ p(n1,n5,n5) ).
cnf(u33119,axiom,
~ p(n1,n4,n5) ).
cnf(u33124,axiom,
~ p(n3,n6,n4) ).
cnf(u33128,axiom,
~ p(n3,n5,n4) ).
cnf(u33132,axiom,
~ p(n3,n4,n4) ).
cnf(u33136,axiom,
~ p(n2,n6,n4) ).
cnf(u33140,axiom,
~ p(n2,n5,n4) ).
cnf(u33144,axiom,
~ p(n2,n4,n4) ).
cnf(u33148,axiom,
~ p(n1,n6,n4) ).
cnf(u33152,axiom,
~ p(n1,n5,n4) ).
cnf(u33157,axiom,
p(n1,n4,n4) ).
cnf(u33161,axiom,
~ p(n3,n6,n2) ).
cnf(u33165,axiom,
~ p(n3,n5,n2) ).
cnf(u33169,axiom,
~ p(n3,n4,n2) ).
cnf(u33174,axiom,
p(n2,n6,n2) ).
cnf(u33177,axiom,
~ p(n2,n5,n2) ).
cnf(u33181,axiom,
~ p(n2,n4,n2) ).
cnf(u33185,axiom,
~ p(n1,n6,n2) ).
cnf(u33189,axiom,
~ p(n1,n5,n2) ).
cnf(u33193,axiom,
~ p(n1,n4,n2) ).
cnf(u33199,axiom,
p(n3,n6,n1) ).
cnf(u33202,axiom,
~ p(n3,n5,n1) ).
cnf(u33206,axiom,
~ p(n3,n4,n1) ).
cnf(u33210,axiom,
~ p(n2,n6,n1) ).
cnf(u33214,axiom,
~ p(n2,n5,n1) ).
cnf(u33218,axiom,
~ p(n2,n4,n1) ).
cnf(u33222,axiom,
~ p(n1,n6,n1) ).
cnf(u33226,axiom,
~ p(n1,n5,n1) ).
cnf(u33230,axiom,
~ p(n1,n4,n1) ).
cnf(u33235,axiom,
~ p(n3,n3,n9) ).
cnf(u33239,axiom,
~ p(n3,n2,n9) ).
cnf(u33243,axiom,
~ p(n3,n1,n9) ).
cnf(u33247,axiom,
~ p(n2,n3,n9) ).
cnf(u33251,axiom,
~ p(n2,n2,n9) ).
cnf(u33255,axiom,
~ p(n2,n1,n9) ).
cnf(u33260,axiom,
p(n1,n3,n9) ).
cnf(u33263,axiom,
~ p(n1,n2,n9) ).
cnf(u33267,axiom,
~ p(n1,n1,n9) ).
cnf(u33272,axiom,
~ p(n3,n3,n8) ).
cnf(u33276,axiom,
~ p(n3,n2,n8) ).
cnf(u33280,axiom,
~ p(n3,n1,n8) ).
cnf(u33284,axiom,
~ p(n2,n3,n8) ).
cnf(u33288,axiom,
~ p(n2,n2,n8) ).
cnf(u33292,axiom,
~ p(n2,n1,n8) ).
cnf(u33296,axiom,
~ p(n1,n3,n8) ).
cnf(u33300,axiom,
~ p(n1,n2,n8) ).
cnf(u33305,axiom,
p(n1,n1,n8) ).
cnf(u33309,axiom,
~ p(n3,n3,n7) ).
cnf(u33313,axiom,
~ p(n3,n2,n7) ).
cnf(u33318,axiom,
p(n3,n1,n7) ).
cnf(u33321,axiom,
~ p(n2,n3,n7) ).
cnf(u33325,axiom,
~ p(n2,n2,n7) ).
cnf(u33329,axiom,
~ p(n2,n1,n7) ).
cnf(u33333,axiom,
~ p(n1,n3,n7) ).
cnf(u33337,axiom,
~ p(n1,n2,n7) ).
cnf(u33341,axiom,
~ p(n1,n1,n7) ).
cnf(u33346,axiom,
~ p(n3,n3,n6) ).
cnf(u33350,axiom,
~ p(n3,n2,n6) ).
cnf(u33354,axiom,
~ p(n3,n1,n6) ).
cnf(u33359,axiom,
p(n2,n3,n6) ).
cnf(u33362,axiom,
~ p(n2,n2,n6) ).
cnf(u33366,axiom,
~ p(n2,n1,n6) ).
cnf(u33370,axiom,
~ p(n1,n3,n6) ).
cnf(u33374,axiom,
~ p(n1,n2,n6) ).
cnf(u33378,axiom,
~ p(n1,n1,n6) ).
cnf(u33383,axiom,
~ p(n3,n3,n5) ).
cnf(u33388,axiom,
p(n3,n2,n5) ).
cnf(u33391,axiom,
~ p(n3,n1,n5) ).
cnf(u33395,axiom,
~ p(n2,n3,n5) ).
cnf(u33399,axiom,
~ p(n2,n2,n5) ).
cnf(u33403,axiom,
~ p(n2,n1,n5) ).
cnf(u33407,axiom,
~ p(n1,n3,n5) ).
cnf(u33411,axiom,
~ p(n1,n2,n5) ).
cnf(u33415,axiom,
~ p(n1,n1,n5) ).
cnf(u33420,axiom,
~ p(n3,n3,n4) ).
cnf(u33424,axiom,
~ p(n3,n2,n4) ).
cnf(u33428,axiom,
~ p(n3,n1,n4) ).
cnf(u33432,axiom,
~ p(n2,n3,n4) ).
cnf(u33437,axiom,
p(n2,n2,n4) ).
cnf(u33440,axiom,
~ p(n2,n1,n4) ).
cnf(u33444,axiom,
~ p(n1,n3,n4) ).
cnf(u33448,axiom,
~ p(n1,n2,n4) ).
cnf(u33452,axiom,
~ p(n1,n1,n4) ).
cnf(u33457,axiom,
~ p(n3,n3,n3) ).
cnf(u33461,axiom,
~ p(n3,n2,n3) ).
cnf(u33465,axiom,
~ p(n3,n1,n3) ).
cnf(u33469,axiom,
~ p(n2,n3,n3) ).
cnf(u33473,axiom,
~ p(n2,n2,n3) ).
cnf(u33477,axiom,
~ p(n2,n1,n3) ).
cnf(u33481,axiom,
~ p(n1,n3,n3) ).
cnf(u33486,axiom,
p(n1,n2,n3) ).
cnf(u33489,axiom,
~ p(n1,n1,n3) ).
cnf(u33494,axiom,
~ p(n3,n3,n1) ).
cnf(u33498,axiom,
~ p(n3,n2,n1) ).
cnf(u33502,axiom,
~ p(n3,n1,n1) ).
cnf(u33506,axiom,
~ p(n2,n3,n1) ).
cnf(u33510,axiom,
~ p(n2,n2,n1) ).
cnf(u33515,axiom,
p(n2,n1,n1) ).
cnf(u33518,axiom,
~ p(n1,n3,n1) ).
cnf(u33522,axiom,
~ p(n1,n2,n1) ).
cnf(u33526,axiom,
~ p(n1,n1,n1) ).
cnf(u33531,axiom,
~ p(n9,n9,n5) ).
cnf(u33536,axiom,
~ p(n9,n8,n5) ).
cnf(u33541,axiom,
~ p(n9,n7,n5) ).
cnf(u33546,axiom,
~ p(n9,n5,n6) ).
cnf(u33550,axiom,
~ p(n9,n5,n5) ).
cnf(u33554,axiom,
~ p(n9,n5,n4) ).
cnf(u33559,axiom,
~ p(n9,n4,n6) ).
cnf(u33563,axiom,
~ p(n9,n4,n5) ).
cnf(u33567,axiom,
~ p(n9,n4,n4) ).
cnf(u33572,axiom,
~ p(n9,n3,n9) ).
cnf(u33576,axiom,
~ p(n9,n3,n8) ).
cnf(u33580,axiom,
~ p(n9,n3,n7) ).
cnf(u33584,axiom,
~ p(n9,n3,n4) ).
cnf(u33589,axiom,
~ p(n8,n9,n5) ).
cnf(u33594,axiom,
~ p(n8,n8,n5) ).
cnf(u33599,axiom,
~ p(n8,n6,n6) ).
cnf(u33603,axiom,
~ p(n8,n6,n5) ).
cnf(u33607,axiom,
~ p(n8,n6,n4) ).
cnf(u33612,axiom,
~ p(n8,n4,n6) ).
cnf(u33616,axiom,
~ p(n8,n4,n5) ).
cnf(u33620,axiom,
~ p(n8,n4,n4) ).
cnf(u33625,axiom,
~ p(n8,n3,n9) ).
cnf(u33629,axiom,
~ p(n8,n3,n8) ).
cnf(u33633,axiom,
~ p(n8,n3,n7) ).
cnf(u33637,axiom,
~ p(n8,n3,n4) ).
cnf(u33642,axiom,
~ p(n8,n2,n9) ).
cnf(u33646,axiom,
~ p(n8,n2,n8) ).
cnf(u33650,axiom,
~ p(n8,n2,n7) ).
cnf(u33654,axiom,
~ p(n8,n2,n4) ).
cnf(u33659,axiom,
~ p(n7,n9,n5) ).
cnf(u33664,axiom,
~ p(n7,n8,n5) ).
cnf(u33669,axiom,
~ p(n7,n7,n5) ).
cnf(u33674,axiom,
~ p(n7,n6,n6) ).
cnf(u33678,axiom,
~ p(n7,n6,n5) ).
cnf(u33682,axiom,
~ p(n7,n6,n4) ).
cnf(u33687,axiom,
~ p(n7,n5,n6) ).
cnf(u33691,axiom,
~ p(n7,n5,n5) ).
cnf(u33695,axiom,
~ p(n7,n5,n4) ).
cnf(u33700,axiom,
~ p(n7,n2,n9) ).
cnf(u33704,axiom,
~ p(n7,n2,n8) ).
cnf(u33708,axiom,
~ p(n7,n2,n7) ).
cnf(u33712,axiom,
~ p(n7,n2,n4) ).
cnf(u33717,axiom,
~ p(n7,n1,n9) ).
cnf(u33721,axiom,
~ p(n7,n1,n8) ).
cnf(u33725,axiom,
~ p(n7,n1,n7) ).
cnf(u33729,axiom,
~ p(n7,n1,n4) ).
cnf(u33734,axiom,
~ p(n6,n9,n8) ).
cnf(u33738,axiom,
~ p(n6,n9,n5) ).
cnf(u33743,axiom,
~ p(n6,n8,n8) ).
cnf(u33747,axiom,
~ p(n6,n8,n5) ).
cnf(u33752,axiom,
~ p(n6,n7,n8) ).
cnf(u33756,axiom,
~ p(n6,n7,n5) ).
cnf(u33761,axiom,
~ p(n6,n5,n9) ).
cnf(u33765,axiom,
~ p(n6,n5,n8) ).
cnf(u33769,axiom,
~ p(n6,n5,n7) ).
cnf(u33774,axiom,
~ p(n6,n4,n9) ).
cnf(u33778,axiom,
~ p(n6,n4,n8) ).
cnf(u33782,axiom,
~ p(n6,n4,n7) ).
cnf(u33787,axiom,
~ p(n6,n3,n6) ).
cnf(u33791,axiom,
~ p(n6,n3,n1) ).
cnf(u33796,axiom,
~ p(n6,n2,n6) ).
cnf(u33800,axiom,
~ p(n6,n2,n1) ).
cnf(u33805,axiom,
~ p(n6,n1,n6) ).
cnf(u33809,axiom,
~ p(n6,n1,n1) ).
cnf(u33814,axiom,
~ p(n5,n9,n8) ).
cnf(u33818,axiom,
~ p(n5,n9,n5) ).
cnf(u33823,axiom,
~ p(n5,n8,n8) ).
cnf(u33827,axiom,
~ p(n5,n8,n5) ).
cnf(u33832,axiom,
~ p(n5,n6,n9) ).
cnf(u33836,axiom,
~ p(n5,n6,n8) ).
cnf(u33840,axiom,
~ p(n5,n6,n7) ).
cnf(u33845,axiom,
~ p(n5,n4,n9) ).
cnf(u33849,axiom,
~ p(n5,n4,n8) ).
cnf(u33853,axiom,
~ p(n5,n4,n7) ).
cnf(u33858,axiom,
~ p(n5,n3,n6) ).
cnf(u33862,axiom,
~ p(n5,n3,n1) ).
cnf(u33867,axiom,
~ p(n5,n1,n6) ).
cnf(u33871,axiom,
~ p(n5,n1,n1) ).
cnf(u33876,axiom,
~ p(n4,n8,n8) ).
cnf(u33880,axiom,
~ p(n4,n8,n5) ).
cnf(u33885,axiom,
~ p(n4,n7,n8) ).
cnf(u33889,axiom,
~ p(n4,n7,n5) ).
cnf(u33894,axiom,
~ p(n4,n6,n9) ).
cnf(u33898,axiom,
~ p(n4,n6,n8) ).
cnf(u33902,axiom,
~ p(n4,n6,n7) ).
cnf(u33907,axiom,
~ p(n4,n5,n9) ).
cnf(u33911,axiom,
~ p(n4,n5,n8) ).
cnf(u33915,axiom,
~ p(n4,n5,n7) ).
cnf(u33920,axiom,
~ p(n4,n2,n6) ).
cnf(u33924,axiom,
~ p(n4,n2,n1) ).
cnf(u33929,axiom,
~ p(n4,n1,n6) ).
cnf(u33933,axiom,
~ p(n4,n1,n1) ).
cnf(u33938,axiom,
~ p(n3,n9,n4) ).
cnf(u33942,axiom,
~ p(n3,n9,n3) ).
cnf(u33946,axiom,
~ p(n3,n9,n2) ).
cnf(u33950,axiom,
~ p(n3,n9,n1) ).
cnf(u33955,axiom,
~ p(n3,n8,n4) ).
cnf(u33959,axiom,
~ p(n3,n8,n3) ).
cnf(u33963,axiom,
~ p(n3,n8,n2) ).
cnf(u33967,axiom,
~ p(n3,n8,n1) ).
cnf(u33972,axiom,
~ p(n3,n6,n3) ).
cnf(u33977,axiom,
~ p(n3,n5,n3) ).
cnf(u33982,axiom,
~ p(n3,n2,n2) ).
cnf(u33987,axiom,
~ p(n3,n1,n2) ).
cnf(u33992,axiom,
~ p(n2,n8,n4) ).
cnf(u33996,axiom,
~ p(n2,n8,n3) ).
cnf(u34000,axiom,
~ p(n2,n8,n2) ).
cnf(u34004,axiom,
~ p(n2,n8,n1) ).
cnf(u34009,axiom,
~ p(n2,n7,n4) ).
cnf(u34013,axiom,
~ p(n2,n7,n3) ).
cnf(u34017,axiom,
~ p(n2,n7,n2) ).
cnf(u34021,axiom,
~ p(n2,n7,n1) ).
cnf(u34026,axiom,
~ p(n2,n6,n3) ).
cnf(u34031,axiom,
~ p(n2,n5,n3) ).
cnf(u34036,axiom,
~ p(n2,n4,n3) ).
cnf(u34041,axiom,
~ p(n2,n3,n2) ).
cnf(u34046,axiom,
~ p(n2,n2,n2) ).
cnf(u34051,axiom,
~ p(n2,n1,n2) ).
cnf(u34056,axiom,
~ p(n1,n7,n4) ).
cnf(u34060,axiom,
~ p(n1,n7,n3) ).
cnf(u34064,axiom,
~ p(n1,n7,n2) ).
cnf(u34068,axiom,
~ p(n1,n7,n1) ).
cnf(u34073,axiom,
~ p(n1,n6,n3) ).
cnf(u34078,axiom,
~ p(n1,n5,n3) ).
cnf(u34083,axiom,
~ p(n1,n4,n3) ).
cnf(u34088,axiom,
~ p(n1,n3,n2) ).
cnf(u34093,axiom,
~ p(n1,n2,n2) ).
cnf(u34098,axiom,
~ p(n1,n1,n2) ).
cnf(u34104,axiom,
~ p(n4,n9,n8) ).
cnf(u34111,axiom,
~ p(n2,n9,n4) ).
cnf(u34115,axiom,
~ p(n1,n9,n4) ).
cnf(u34120,axiom,
~ p(n2,n9,n1) ).
cnf(u34124,axiom,
~ p(n1,n9,n1) ).
cnf(u34134,axiom,
~ p(n1,n8,n4) ).
cnf(u34139,axiom,
~ p(n1,n8,n3) ).
cnf(u34144,axiom,
~ p(n1,n8,n2) ).
cnf(u34152,axiom,
~ p(n3,n7,n3) ).
cnf(u34157,axiom,
~ p(n3,n7,n2) ).
cnf(u34162,axiom,
~ p(n3,n7,n1) ).
cnf(u34167,axiom,
~ p(n6,n6,n8) ).
cnf(u34172,axiom,
~ p(n6,n6,n7) ).
cnf(u34177,axiom,
~ p(n9,n6,n5) ).
cnf(u34182,axiom,
~ p(n9,n6,n4) ).
cnf(u34190,axiom,
~ p(n5,n5,n9) ).
cnf(u34195,axiom,
~ p(n5,n5,n8) ).
cnf(u34200,axiom,
~ p(n8,n5,n6) ).
cnf(u34205,axiom,
~ p(n8,n5,n5) ).
cnf(u34213,axiom,
~ p(n4,n4,n9) ).
cnf(u34218,axiom,
~ p(n4,n4,n7) ).
cnf(u34223,axiom,
~ p(n7,n4,n6) ).
cnf(u34228,axiom,
~ p(n7,n4,n4) ).
cnf(u34235,axiom,
~ p(n7,n3,n9) ).
cnf(u34240,axiom,
~ p(n7,n3,n7) ).
cnf(u34245,axiom,
~ p(n4,n3,n6) ).
cnf(u34251,axiom,
~ p(n7,n3,n4) ).
cnf(u34257,axiom,
~ p(n9,n2,n9) ).
cnf(u34262,axiom,
~ p(n9,n2,n8) ).
cnf(u34268,axiom,
~ p(n9,n2,n4) ).
cnf(u34275,axiom,
~ p(n5,n2,n1) ).
cnf(u34280,axiom,
~ p(n9,n1,n8) ).
cnf(u34284,axiom,
~ p(n8,n1,n8) ).
cnf(u34289,axiom,
~ p(n9,n1,n7) ).
cnf(u34293,axiom,
~ p(n8,n1,n7) ).
cnf(u34303,axiom,
~ p(n9,n1,n9) ).
cnf(u34335,axiom,
~ p(n5,n7,n5) ).
cnf(u34362,axiom,
~ p(n2,n9,n2) ).
cnf(u34374,axiom,
~ p(n1,n9,n3) ).
cnf(u34745,axiom,
~ p(n8,n1,n4) ).
cnf(u31305,axiom,
p(n8,n7,n5) ).
cnf(u31290,axiom,
p(n2,n9,n3) ).
cnf(u31289,axiom,
p(n1,n9,n2) ).
cnf(u31302,axiom,
p(n7,n4,n5) ).
cnf(u31291,axiom,
p(n3,n3,n2) ).
cnf(u31292,axiom,
p(n3,n4,n3) ).
cnf(u31301,axiom,
p(n7,n3,n8) ).
cnf(u31294,axiom,
p(n4,n3,n1) ).
cnf(u31296,axiom,
p(n4,n9,n5) ).
cnf(u31299,axiom,
p(n5,n7,n8) ).
cnf(u31303,axiom,
p(n8,n1,n9) ).
cnf(u31288,axiom,
p(n1,n8,n1) ).
cnf(u31304,axiom,
p(n8,n5,n4) ).
cnf(u31295,axiom,
p(n4,n4,n8) ).
cnf(u31300,axiom,
p(n6,n6,n9) ).
cnf(u31306,axiom,
p(n9,n1,n4) ).
cnf(u31293,axiom,
p(n3,n7,n4) ).
cnf(u31307,axiom,
p(n9,n2,n7) ).
cnf(u31297,axiom,
p(n5,n2,n6) ).
cnf(u31298,axiom,
p(n5,n5,n7) ).
cnf(u31308,axiom,
p(n9,n6,n6) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ138+2 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n003.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 22:47:12 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.48/1.94 % (998064)Detected formulas, will run a generic FOF schedule.
% 3.48/1.94 % (998115)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3112883325:i=119:av=off:ss=axioms_2997 on theBenchmark for (2997ds/119Mi)
% 3.48/1.94 % (998115)Refutation not found, incomplete strategy
% 3.48/1.94 % (998115)------------------------------
% 3.48/1.94 % (998115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.48/1.94 % (998115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.48/1.94 % (998115)CaDiCaL version: 2.1.3
% 3.48/1.94 % (998115)Termination reason: Refutation not found, incomplete strategy
% 3.48/1.94 % (998115)Time elapsed: 0.010 s
% 3.48/1.94 % (998115)Peak memory usage: 90 MB
% 3.48/1.94 % (998115)Instructions burned: 33 (million)
% 3.48/1.94 % (998112)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3375543922:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2997 on theBenchmark for (2997ds/134677Mi)
% 3.48/1.94 % (998113)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1283649054:i=141695:sd=1:nm=32:gsp=on:ss=included_2997 on theBenchmark for (2997ds/141695Mi)
% 3.48/1.94 % (998111)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=376647226:i=141193_2997 on theBenchmark for (2997ds/141193Mi)
% 3.48/1.94 % (998114)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3753872170:i=109:sd=1:ins=1:gsp=on:ss=axioms_2997 on theBenchmark for (2997ds/109Mi)
% 3.48/1.94 % (998116)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4040602137:s2a=on:i=139:gtg=position_2997 on theBenchmark for (2997ds/139Mi)
% 3.48/1.94 % (998117)dis-21_1_sil=8000:lcm=predicate:random_seed=2265381244:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2997 on theBenchmark for (2997ds/129Mi)
% 3.48/1.94 % (998114)Refutation not found, incomplete strategy
% 3.48/1.94 % (998114)------------------------------
% 3.48/1.94 % (998114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.48/1.94 % (998114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.48/1.94 % (998114)CaDiCaL version: 2.1.3
% 3.48/1.94 % (998114)Termination reason: Refutation not found, incomplete strategy
% 3.48/1.94 % (998114)Time elapsed: 0.018 s
% 3.48/1.94 % (998114)Peak memory usage: 90 MB
% 3.48/1.94 % (998114)Instructions burned: 33 (million)
% 3.48/1.94 % (998116)Instruction limit reached!
% 3.48/1.94 % (998116)------------------------------
% 3.48/1.94 % (998116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.48/1.94 % (998116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.48/1.94 % (998116)CaDiCaL version: 2.1.3
% 3.48/1.94 % (998116)Termination reason: Instruction limit
% 3.48/1.94 % (998116)Termination phase: Unused predicate definition removal
% 3.48/1.94 % (998116)Time elapsed: 0.061 s
% 3.48/1.94 % (998116)Peak memory usage: 89 MB
% 3.48/1.94 % (998116)Instructions burned: 139 (million)
% 3.48/1.94 % (998117)Instruction limit reached!
% 3.48/1.94 % (998117)------------------------------
% 3.48/1.94 % (998117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.48/1.94 % (998117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.48/1.94 % (998117)CaDiCaL version: 2.1.3
% 3.48/1.94 % (998117)Termination reason: Instruction limit
% 3.48/1.94 % (998117)Termination phase: Preprocessing 3
% 3.48/1.94 % (998117)Time elapsed: 0.067 s
% 3.48/1.94 % (998117)Peak memory usage: 91 MB
% 3.48/1.94 % (998117)Instructions burned: 130 (million)
% 3.48/1.94 % (998115)------------------------------
% 3.48/1.94 % (998115)------------------------------
% 3.48/1.94 % (998126)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3692793528:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 3.48/1.94 % (998125)lrs+10_1_sil=8000:sp=occurrence:random_seed=1354576003:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 3.48/1.94 % (998127)lrs+1011_1_sil=32000:sp=occurrence:random_seed=993660307:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 3.48/1.94 % (998125)Refutation not found, incomplete strategy
% 3.48/1.94 % (998125)------------------------------
% 3.48/1.94 % (998125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.59/2.27 % (998125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.59/2.27 % (998125)CaDiCaL version: 2.1.3
% 8.59/2.27 % (998125)Termination reason: Refutation not found, incomplete strategy
% 8.59/2.27 % (998125)Time elapsed: 0.018 s
% 8.59/2.27 % (998125)Peak memory usage: 91 MB
% 8.59/2.27 % (998125)Instructions burned: 33 (million)
% 8.59/2.27 % (998127)Refutation not found, incomplete strategy
% 8.59/2.27 % (998127)------------------------------
% 8.59/2.27 % (998127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.59/2.27 % (998127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.59/2.27 % (998127)CaDiCaL version: 2.1.3
% 8.59/2.27 % (998127)Termination reason: Refutation not found, incomplete strategy
% 8.59/2.27 % (998127)Time elapsed: 0.009 s
% 8.59/2.27 % (998127)Peak memory usage: 91 MB
% 8.59/2.27 % (998127)Instructions burned: 33 (million)
% 8.59/2.27 % (998126)Refutation not found, incomplete strategy
% 8.59/2.27 % (998126)------------------------------
% 8.59/2.27 % (998126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.59/2.27 % (998126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.59/2.27 % (998126)CaDiCaL version: 2.1.3
% 8.59/2.27 % (998126)Termination reason: Refutation not found, incomplete strategy
% 8.59/2.27 % (998126)Time elapsed: 0.052 s
% 8.59/2.27 % (998126)Peak memory usage: 91 MB
% 8.59/2.27 % (998126)Instructions burned: 123 (million)
% 8.59/2.27 % (998114)------------------------------
% 8.59/2.27 % (998114)------------------------------
% 8.59/2.27 % (998127)------------------------------
% 8.59/2.27 % (998127)------------------------------
% 8.59/2.27 % (998131)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=4037250678:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 8.59/2.27 % (998132)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=594490448:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2992 on theBenchmark for (2992ds/294Mi)
% 8.59/2.27 % (998125)------------------------------
% 8.59/2.27 % (998125)------------------------------
% 8.59/2.27 % (998132)Refutation not found, incomplete strategy
% 8.59/2.27 % (998132)------------------------------
% 8.59/2.27 % (998132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.59/2.27 % (998132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.59/2.27 % (998132)CaDiCaL version: 2.1.3
% 8.59/2.27 % (998132)Termination reason: Refutation not found, incomplete strategy
% 8.59/2.27 % (998132)Time elapsed: 0.014 s
% 8.59/2.27 % (998132)Peak memory usage: 91 MB
% 8.59/2.27 % (998132)Instructions burned: 51 (million)
% 8.59/2.27 [W927 22:47:14.317701727 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.59/2.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.59/2.27 [W927 22:47:14.317744541 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.59/2.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.59/2.27 [W927 22:47:14.317791728 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.59/2.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.59/2.27 [W927 22:47:14.317803102 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.59/2.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.59/2.27 [W927 22:47:14.317831139 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.59/2.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.59/2.27 [W927 22:47:14.317843806 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.30/2.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.30/2.32 % (998126)------------------------------
% 9.30/2.32 % (998126)------------------------------
% 9.30/2.32 [W927 22:47:14.344841085 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.30/2.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.30/2.32 [W927 22:47:14.344875236 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.30/2.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.30/2.32 [W927 22:47:14.344912303 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.30/2.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.30/2.32 [W927 22:47:14.344924496 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.30/2.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.30/2.32 [W927 22:47:14.344951423 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.30/2.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.30/2.32 [W927 22:47:14.344962690 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.30/2.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.30/2.32 % (998131)Instruction limit reached!
% 9.30/2.32 % (998131)------------------------------
% 9.30/2.32 % (998131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.30/2.32 % (998131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.30/2.32 % (998131)CaDiCaL version: 2.1.3
% 9.30/2.32 % (998131)Termination reason: Instruction limit
% 9.30/2.32 % (998131)Termination phase: Property scanning
% 9.30/2.32 % (998131)Time elapsed: 0.114 s
% 9.30/2.32 % (998131)Peak memory usage: 93 MB
% 9.30/2.32 % (998131)Instructions burned: 251 (million)
% 9.30/2.32 % (998135)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=873325019:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 9.30/2.32 % (998132)------------------------------
% 9.30/2.32 % (998132)------------------------------
% 9.30/2.32 % (998136)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=411498125:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 9.30/2.32 % (998137)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2544011471:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 9.30/2.32 % (998136)Instruction limit reached!
% 9.30/2.32 % (998136)------------------------------
% 9.30/2.32 % (998136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.30/2.32 % (998136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.30/2.32 % (998136)CaDiCaL version: 2.1.3
% 9.30/2.32 % (998136)Termination reason: Instruction limit
% 9.30/2.32 % (998136)Termination phase: Preprocessing 3
% 9.30/2.32 % (998136)Time elapsed: 0.066 s
% 9.30/2.32 % (998136)Peak memory usage: 91 MB
% 9.30/2.32 % (998136)Instructions burned: 113 (million)
% 9.30/2.32 % (998139)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1413728919:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 9.30/2.32 % (998137)Instruction limit reached!
% 9.30/2.32 % (998137)------------------------------
% 9.30/2.32 % (998137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.94/2.45 % (998137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.94/2.45 % (998137)CaDiCaL version: 2.1.3
% 9.94/2.45 % (998137)Termination reason: Instruction limit
% 9.94/2.45 % (998137)Termination phase: Property scanning
% 9.94/2.45 % (998137)Time elapsed: 0.062 s
% 9.94/2.45 % (998137)Peak memory usage: 92 MB
% 9.94/2.45 % (998137)Instructions burned: 129 (million)
% 9.94/2.45 % (998139)Instruction limit reached!
% 9.94/2.45 % (998139)------------------------------
% 9.94/2.45 % (998139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.94/2.45 % (998139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.94/2.45 % (998139)CaDiCaL version: 2.1.3
% 9.94/2.45 % (998139)Termination reason: Instruction limit
% 9.94/2.45 % (998139)Termination phase: SInE selection
% 9.94/2.45 % (998139)Time elapsed: 0.023 s
% 9.94/2.45 % (998139)Peak memory usage: 89 MB
% 9.94/2.45 % (998139)Instructions burned: 115 (million)
% 9.94/2.45 % (998145)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=205079173:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 9.94/2.45 % (998142)lrs+10_1_sil=8000:sp=occurrence:random_seed=366667861:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 9.94/2.45 % (998144)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2109064375:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 9.94/2.45 % (998142)Refutation not found, incomplete strategy
% 9.94/2.45 % (998142)------------------------------
% 9.94/2.45 % (998142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.94/2.45 % (998142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.94/2.45 % (998142)CaDiCaL version: 2.1.3
% 9.94/2.45 % (998142)Termination reason: Refutation not found, incomplete strategy
% 9.94/2.45 % (998142)Time elapsed: 0.025 s
% 9.94/2.45 % (998142)Peak memory usage: 91 MB
% 9.94/2.45 % (998142)Instructions burned: 51 (million)
% 9.94/2.45 % (998113)Refutation not found, incomplete strategy
% 9.94/2.45 % (998113)------------------------------
% 9.94/2.45 % (998113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.94/2.45 % (998113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.94/2.45 % (998113)CaDiCaL version: 2.1.3
% 9.94/2.45 % (998113)Termination reason: Refutation not found, incomplete strategy
% 9.94/2.45 % (998113)Time elapsed: 0.909 s
% 9.94/2.45 % (998113)Peak memory usage: 162 MB
% 9.94/2.45 % (998113)Instructions burned: 1501 (million)
% 9.94/2.45 % (998111)First to succeed.
% 9.94/2.45 % (998111)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-998064"
% 9.94/2.45 % (998144)Refutation not found, incomplete strategy
% 9.94/2.45 % (998144)------------------------------
% 9.94/2.45 % (998144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.94/2.45 % (998144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.94/2.45 % (998144)CaDiCaL version: 2.1.3
% 9.94/2.45 % (998144)Termination reason: Refutation not found, incomplete strategy
% 9.94/2.45 % (998144)Time elapsed: 0.143 s
% 9.94/2.45 % (998144)Peak memory usage: 98 MB
% 9.94/2.45 % (998144)Instructions burned: 306 (million)
% 9.94/2.45 [W927 22:47:14.891515949 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.94/2.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.94/2.45 [W927 22:47:14.891537826 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.94/2.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.94/2.45 [W927 22:47:14.891558118 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.94/2.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.94/2.45 [W927 22:47:14.891565606 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.94/2.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.94/2.45 [W927 22:47:14.891579352 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.94/2.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.94/2.45 [W927 22:47:14.891586241 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.94/2.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.94/2.45 [W927 22:47:14.891599125 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.94/2.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.94/2.45 [W927 22:47:14.891604951 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.94/2.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.94/2.45 [W927 22:47:14.891662198 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.94/2.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.94/2.45 [W927 22:47:14.891672091 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.94/2.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.94/2.45 [W927 22:47:14.891686029 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.94/2.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.94/2.45 [W927 22:47:14.891691828 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.94/2.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.94/2.45 [W927 22:47:14.934972901 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.94/2.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.94/2.45 [W927 22:47:14.935024748 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.94/2.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.94/2.45 [W927 22:47:14.935062685 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.94/2.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.94/2.45 [W927 22:47:14.935079176 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.94/2.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.94/2.45 [W927 22:47:14.935106539 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.94/2.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.94/2.45 [W927 22:47:14.935119010 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.94/2.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.94/2.45 % (998142)------------------------------
% 9.94/2.45 % (998142)------------------------------
% 9.94/2.45 % (998113)------------------------------
% 9.94/2.45 % (998113)------------------------------
% 9.94/2.45 % (998145)Refutation not found, incomplete strategy
% 9.94/2.45 % (998145)------------------------------
% 9.94/2.45 % (998145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.94/2.45 % (998145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.94/2.45 % (998145)CaDiCaL version: 2.1.3
% 9.94/2.45 % (998145)Termination reason: Refutation not found, incomplete strategy
% 9.94/2.45 % (998145)Time elapsed: 0.318 s
% 9.94/2.45 % (998145)Peak memory usage: 130 MB
% 9.94/2.45 % (998145)Instructions burned: 893 (million)
% 9.94/2.45 % SZS status Satisfiable for theBenchmark
% 9.94/2.45 % SZS output start Saturation.
% See solution above
% 10.56/2.65 % SZS output start Definitions and Model Updates.
% 10.56/2.65 % SZS output end Definitions and Model Updates.
% 10.56/2.65 % (998111)------------------------------
% 10.56/2.65 % (998111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.56/2.65 % (998111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.56/2.65 % (998111)CaDiCaL version: 2.1.3
% 10.56/2.65 % (998111)Termination reason: Satisfiable
% 10.56/2.65 % (998111)Time elapsed: 0.965 s
% 10.56/2.65 % (998111)Peak memory usage: 162 MB
% 10.56/2.65 % (998111)Instructions burned: 1583 (million)
% 10.56/2.65 % (998111)------------------------------
% 10.56/2.65 % (998111)------------------------------
% 10.56/2.65 % (998064)Success in time 1.592 s
% 10.56/2.65 % Vampire exiting
%------------------------------------------------------------------------------