%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PUZ069+2 : TPTP v9.3.1. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n008.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:32:09 PM UTC 2026
% Result : Satisfiable 0.74s 0.86s
% Output : Saturation 0.74s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u41850,axiom,
p(n7,n7,n9) ).
cnf(u41854,axiom,
p(n7,n8,n9) ).
cnf(u41858,axiom,
p(n7,n9,n9) ).
cnf(u41862,axiom,
p(n8,n7,n9) ).
cnf(u41867,axiom,
~ p(n8,n8,n9) ).
cnf(u41870,axiom,
p(n8,n9,n9) ).
cnf(u41874,axiom,
p(n9,n7,n9) ).
cnf(u41878,axiom,
p(n9,n8,n9) ).
cnf(u41882,axiom,
p(n9,n9,n9) ).
cnf(u41887,axiom,
p(n7,n7,n8) ).
cnf(u41891,axiom,
p(n7,n8,n8) ).
cnf(u41895,axiom,
p(n7,n9,n8) ).
cnf(u41899,axiom,
p(n8,n7,n8) ).
cnf(u41903,axiom,
p(n8,n8,n8) ).
cnf(u41908,axiom,
~ p(n8,n9,n8) ).
cnf(u41911,axiom,
p(n9,n7,n8) ).
cnf(u41915,axiom,
p(n9,n8,n8) ).
cnf(u41919,axiom,
p(n9,n9,n8) ).
cnf(u41924,axiom,
p(n7,n7,n7) ).
cnf(u41928,axiom,
p(n7,n8,n7) ).
cnf(u41932,axiom,
p(n7,n9,n7) ).
cnf(u41936,axiom,
p(n8,n7,n7) ).
cnf(u41940,axiom,
p(n8,n8,n7) ).
cnf(u41944,axiom,
p(n8,n9,n7) ).
cnf(u41949,axiom,
~ p(n9,n7,n7) ).
cnf(u41952,axiom,
p(n9,n8,n7) ).
cnf(u41956,axiom,
p(n9,n9,n7) ).
cnf(u41962,axiom,
~ p(n7,n7,n6) ).
cnf(u41965,axiom,
p(n7,n8,n6) ).
cnf(u41969,axiom,
p(n7,n9,n6) ).
cnf(u41973,axiom,
p(n8,n7,n6) ).
cnf(u41977,axiom,
p(n8,n8,n6) ).
cnf(u41981,axiom,
p(n8,n9,n6) ).
cnf(u41985,axiom,
p(n9,n7,n6) ).
cnf(u41989,axiom,
p(n9,n8,n6) ).
cnf(u41993,axiom,
p(n9,n9,n6) ).
cnf(u41998,axiom,
p(n7,n7,n5) ).
cnf(u42002,axiom,
p(n7,n8,n5) ).
cnf(u42006,axiom,
p(n7,n9,n5) ).
cnf(u42010,axiom,
p(n8,n7,n5) ).
cnf(u42014,axiom,
p(n8,n8,n5) ).
cnf(u42018,axiom,
p(n8,n9,n5) ).
cnf(u42022,axiom,
p(n9,n7,n5) ).
cnf(u42027,axiom,
~ p(n9,n8,n5) ).
cnf(u42030,axiom,
p(n9,n9,n5) ).
cnf(u42035,axiom,
p(n7,n7,n4) ).
cnf(u42039,axiom,
p(n7,n8,n4) ).
cnf(u42043,axiom,
p(n7,n9,n4) ).
cnf(u42047,axiom,
p(n8,n7,n4) ).
cnf(u42051,axiom,
p(n8,n8,n4) ).
cnf(u42055,axiom,
p(n8,n9,n4) ).
cnf(u42059,axiom,
p(n9,n7,n4) ).
cnf(u42063,axiom,
p(n9,n8,n4) ).
cnf(u42068,axiom,
~ p(n9,n9,n4) ).
cnf(u42072,axiom,
p(n7,n7,n3) ).
cnf(u42076,axiom,
p(n7,n8,n3) ).
cnf(u42081,axiom,
~ p(n7,n9,n3) ).
cnf(u42084,axiom,
p(n8,n7,n3) ).
cnf(u42088,axiom,
p(n8,n8,n3) ).
cnf(u42092,axiom,
p(n8,n9,n3) ).
cnf(u42096,axiom,
p(n9,n7,n3) ).
cnf(u42100,axiom,
p(n9,n8,n3) ).
cnf(u42104,axiom,
p(n9,n9,n3) ).
cnf(u42109,axiom,
p(n7,n7,n2) ).
cnf(u42113,axiom,
p(n7,n8,n2) ).
cnf(u42117,axiom,
p(n7,n9,n2) ).
cnf(u42122,axiom,
~ p(n8,n7,n2) ).
cnf(u42125,axiom,
p(n8,n8,n2) ).
cnf(u42129,axiom,
p(n8,n9,n2) ).
cnf(u42133,axiom,
p(n9,n7,n2) ).
cnf(u42137,axiom,
p(n9,n8,n2) ).
cnf(u42141,axiom,
p(n9,n9,n2) ).
cnf(u42146,axiom,
p(n7,n7,n1) ).
cnf(u42151,axiom,
~ p(n7,n8,n1) ).
cnf(u42154,axiom,
p(n7,n9,n1) ).
cnf(u42158,axiom,
p(n8,n7,n1) ).
cnf(u42162,axiom,
p(n8,n8,n1) ).
cnf(u42166,axiom,
p(n8,n9,n1) ).
cnf(u42170,axiom,
p(n9,n7,n1) ).
cnf(u42174,axiom,
p(n9,n8,n1) ).
cnf(u42178,axiom,
p(n9,n9,n1) ).
cnf(u42183,axiom,
p(n7,n4,n9) ).
cnf(u42188,axiom,
~ p(n7,n5,n9) ).
cnf(u42191,axiom,
p(n7,n6,n9) ).
cnf(u42195,axiom,
p(n8,n4,n9) ).
cnf(u42199,axiom,
p(n8,n5,n9) ).
cnf(u42203,axiom,
p(n8,n6,n9) ).
cnf(u42207,axiom,
p(n9,n4,n9) ).
cnf(u42211,axiom,
p(n9,n5,n9) ).
cnf(u42215,axiom,
p(n9,n6,n9) ).
cnf(u42220,axiom,
p(n7,n4,n8) ).
cnf(u42224,axiom,
p(n7,n5,n8) ).
cnf(u42228,axiom,
p(n7,n6,n8) ).
cnf(u42232,axiom,
p(n8,n4,n8) ).
cnf(u42236,axiom,
p(n8,n5,n8) ).
cnf(u42240,axiom,
p(n8,n6,n8) ).
cnf(u42244,axiom,
p(n9,n4,n8) ).
cnf(u42249,axiom,
~ p(n9,n5,n8) ).
cnf(u42252,axiom,
p(n9,n6,n8) ).
cnf(u42258,axiom,
~ p(n7,n4,n7) ).
cnf(u42261,axiom,
p(n7,n5,n7) ).
cnf(u42265,axiom,
p(n7,n6,n7) ).
cnf(u42269,axiom,
p(n8,n4,n7) ).
cnf(u42273,axiom,
p(n8,n5,n7) ).
cnf(u42277,axiom,
p(n8,n6,n7) ).
cnf(u42281,axiom,
p(n9,n4,n7) ).
cnf(u42285,axiom,
p(n9,n5,n7) ).
cnf(u42289,axiom,
p(n9,n6,n7) ).
cnf(u42294,axiom,
p(n7,n4,n6) ).
cnf(u42298,axiom,
p(n7,n5,n6) ).
cnf(u42302,axiom,
p(n7,n6,n6) ).
cnf(u42306,axiom,
p(n8,n4,n6) ).
cnf(u42311,axiom,
~ p(n8,n5,n6) ).
cnf(u42314,axiom,
p(n8,n6,n6) ).
cnf(u42318,axiom,
p(n9,n4,n6) ).
cnf(u42322,axiom,
p(n9,n5,n6) ).
cnf(u42326,axiom,
p(n9,n6,n6) ).
cnf(u42331,axiom,
p(n7,n4,n5) ).
cnf(u42335,axiom,
p(n7,n5,n5) ).
cnf(u42339,axiom,
p(n7,n6,n5) ).
cnf(u42344,axiom,
~ p(n8,n4,n5) ).
cnf(u42347,axiom,
p(n8,n5,n5) ).
cnf(u42351,axiom,
p(n8,n6,n5) ).
cnf(u42355,axiom,
p(n9,n4,n5) ).
cnf(u42359,axiom,
p(n9,n5,n5) ).
cnf(u42363,axiom,
p(n9,n6,n5) ).
cnf(u42368,axiom,
p(n7,n4,n4) ).
cnf(u42372,axiom,
p(n7,n5,n4) ).
cnf(u42377,axiom,
~ p(n7,n6,n4) ).
cnf(u42380,axiom,
p(n8,n4,n4) ).
cnf(u42384,axiom,
p(n8,n5,n4) ).
cnf(u42388,axiom,
p(n8,n6,n4) ).
cnf(u42392,axiom,
p(n9,n4,n4) ).
cnf(u42396,axiom,
p(n9,n5,n4) ).
cnf(u42400,axiom,
p(n9,n6,n4) ).
cnf(u42405,axiom,
p(n7,n4,n3) ).
cnf(u42409,axiom,
p(n7,n5,n3) ).
cnf(u42413,axiom,
p(n7,n6,n3) ).
cnf(u42417,axiom,
p(n8,n4,n3) ).
cnf(u42421,axiom,
p(n8,n5,n3) ).
cnf(u42425,axiom,
p(n8,n6,n3) ).
cnf(u42430,axiom,
~ p(n9,n4,n3) ).
cnf(u42433,axiom,
p(n9,n5,n3) ).
cnf(u42437,axiom,
p(n9,n6,n3) ).
cnf(u42442,axiom,
p(n7,n4,n2) ).
cnf(u42446,axiom,
p(n7,n5,n2) ).
cnf(u42450,axiom,
p(n7,n6,n2) ).
cnf(u42454,axiom,
p(n8,n4,n2) ).
cnf(u42458,axiom,
p(n8,n5,n2) ).
cnf(u42462,axiom,
p(n8,n6,n2) ).
cnf(u42466,axiom,
p(n9,n4,n2) ).
cnf(u42470,axiom,
p(n9,n5,n2) ).
cnf(u42475,axiom,
~ p(n9,n6,n2) ).
cnf(u42479,axiom,
p(n7,n4,n1) ).
cnf(u42483,axiom,
p(n7,n5,n1) ).
cnf(u42487,axiom,
p(n7,n6,n1) ).
cnf(u42491,axiom,
p(n8,n4,n1) ).
cnf(u42495,axiom,
p(n8,n5,n1) ).
cnf(u42500,axiom,
~ p(n8,n6,n1) ).
cnf(u42503,axiom,
p(n9,n4,n1) ).
cnf(u42507,axiom,
p(n9,n5,n1) ).
cnf(u42511,axiom,
p(n9,n6,n1) ).
cnf(u42516,axiom,
p(n7,n1,n9) ).
cnf(u42520,axiom,
p(n7,n2,n9) ).
cnf(u42524,axiom,
p(n7,n3,n9) ).
cnf(u42528,axiom,
p(n8,n1,n9) ).
cnf(u42532,axiom,
p(n8,n2,n9) ).
cnf(u42536,axiom,
p(n8,n3,n9) ).
cnf(u42540,axiom,
p(n9,n1,n9) ).
cnf(u42544,axiom,
p(n9,n2,n9) ).
cnf(u42549,axiom,
~ p(n9,n3,n9) ).
cnf(u42553,axiom,
p(n7,n1,n8) ).
cnf(u42558,axiom,
~ p(n7,n2,n8) ).
cnf(u42561,axiom,
p(n7,n3,n8) ).
cnf(u42565,axiom,
p(n8,n1,n8) ).
cnf(u42569,axiom,
p(n8,n2,n8) ).
cnf(u42573,axiom,
p(n8,n3,n8) ).
cnf(u42577,axiom,
p(n9,n1,n8) ).
cnf(u42581,axiom,
p(n9,n2,n8) ).
cnf(u42585,axiom,
p(n9,n3,n8) ).
cnf(u42590,axiom,
p(n7,n1,n7) ).
cnf(u42594,axiom,
p(n7,n2,n7) ).
cnf(u42598,axiom,
p(n7,n3,n7) ).
cnf(u42603,axiom,
~ p(n8,n1,n7) ).
cnf(u42606,axiom,
p(n8,n2,n7) ).
cnf(u42610,axiom,
p(n8,n3,n7) ).
cnf(u42614,axiom,
p(n9,n1,n7) ).
cnf(u42618,axiom,
p(n9,n2,n7) ).
cnf(u42622,axiom,
p(n9,n3,n7) ).
cnf(u42627,axiom,
p(n7,n1,n6) ).
cnf(u42631,axiom,
p(n7,n2,n6) ).
cnf(u42635,axiom,
p(n7,n3,n6) ).
cnf(u42639,axiom,
p(n8,n1,n6) ).
cnf(u42643,axiom,
p(n8,n2,n6) ).
cnf(u42647,axiom,
p(n8,n3,n6) ).
cnf(u42652,axiom,
~ p(n9,n1,n6) ).
cnf(u42655,axiom,
p(n9,n2,n6) ).
cnf(u42659,axiom,
p(n9,n3,n6) ).
cnf(u42664,axiom,
p(n7,n1,n5) ).
cnf(u42668,axiom,
p(n7,n2,n5) ).
cnf(u42673,axiom,
~ p(n7,n3,n5) ).
cnf(u42676,axiom,
p(n8,n1,n5) ).
cnf(u42680,axiom,
p(n8,n2,n5) ).
cnf(u42684,axiom,
p(n8,n3,n5) ).
cnf(u42688,axiom,
p(n9,n1,n5) ).
cnf(u42692,axiom,
p(n9,n2,n5) ).
cnf(u42696,axiom,
p(n9,n3,n5) ).
cnf(u42701,axiom,
p(n7,n1,n4) ).
cnf(u42705,axiom,
p(n7,n2,n4) ).
cnf(u42709,axiom,
p(n7,n3,n4) ).
cnf(u42713,axiom,
p(n8,n1,n4) ).
cnf(u42717,axiom,
p(n8,n2,n4) ).
cnf(u42722,axiom,
~ p(n8,n3,n4) ).
cnf(u42725,axiom,
p(n9,n1,n4) ).
cnf(u42729,axiom,
p(n9,n2,n4) ).
cnf(u42733,axiom,
p(n9,n3,n4) ).
cnf(u42738,axiom,
p(n7,n1,n3) ).
cnf(u42742,axiom,
p(n7,n2,n3) ).
cnf(u42746,axiom,
p(n7,n3,n3) ).
cnf(u42750,axiom,
p(n8,n1,n3) ).
cnf(u42755,axiom,
~ p(n8,n2,n3) ).
cnf(u42758,axiom,
p(n8,n3,n3) ).
cnf(u42762,axiom,
p(n9,n1,n3) ).
cnf(u42766,axiom,
p(n9,n2,n3) ).
cnf(u42770,axiom,
p(n9,n3,n3) ).
cnf(u42776,axiom,
~ p(n7,n1,n2) ).
cnf(u42779,axiom,
p(n7,n2,n2) ).
cnf(u42783,axiom,
p(n7,n3,n2) ).
cnf(u42787,axiom,
p(n8,n1,n2) ).
cnf(u42791,axiom,
p(n8,n2,n2) ).
cnf(u42795,axiom,
p(n8,n3,n2) ).
cnf(u42799,axiom,
p(n9,n1,n2) ).
cnf(u42803,axiom,
p(n9,n2,n2) ).
cnf(u42807,axiom,
p(n9,n3,n2) ).
cnf(u42812,axiom,
p(n7,n1,n1) ).
cnf(u42816,axiom,
p(n7,n2,n1) ).
cnf(u42820,axiom,
p(n7,n3,n1) ).
cnf(u42824,axiom,
p(n8,n1,n1) ).
cnf(u42828,axiom,
p(n8,n2,n1) ).
cnf(u42832,axiom,
p(n8,n3,n1) ).
cnf(u42836,axiom,
p(n9,n1,n1) ).
cnf(u42841,axiom,
~ p(n9,n2,n1) ).
cnf(u42844,axiom,
p(n9,n3,n1) ).
cnf(u42850,axiom,
~ p(n4,n7,n9) ).
cnf(u42853,axiom,
p(n4,n8,n9) ).
cnf(u42857,axiom,
p(n4,n9,n9) ).
cnf(u42861,axiom,
p(n5,n7,n9) ).
cnf(u42865,axiom,
p(n5,n8,n9) ).
cnf(u42869,axiom,
p(n5,n9,n9) ).
cnf(u42873,axiom,
p(n6,n7,n9) ).
cnf(u42877,axiom,
p(n6,n8,n9) ).
cnf(u42881,axiom,
p(n6,n9,n9) ).
cnf(u42886,axiom,
p(n4,n7,n8) ).
cnf(u42890,axiom,
p(n4,n8,n8) ).
cnf(u42894,axiom,
p(n4,n9,n8) ).
cnf(u42898,axiom,
p(n5,n7,n8) ).
cnf(u42902,axiom,
p(n5,n8,n8) ).
cnf(u42906,axiom,
p(n5,n9,n8) ).
cnf(u42910,axiom,
p(n6,n7,n8) ).
cnf(u42915,axiom,
~ p(n6,n8,n8) ).
cnf(u42918,axiom,
p(n6,n9,n8) ).
cnf(u42923,axiom,
p(n4,n7,n7) ).
cnf(u42927,axiom,
p(n4,n8,n7) ).
cnf(u42931,axiom,
p(n4,n9,n7) ).
cnf(u42935,axiom,
p(n5,n7,n7) ).
cnf(u42939,axiom,
p(n5,n8,n7) ).
cnf(u42943,axiom,
p(n5,n9,n7) ).
cnf(u42947,axiom,
p(n6,n7,n7) ).
cnf(u42951,axiom,
p(n6,n8,n7) ).
cnf(u42956,axiom,
~ p(n6,n9,n7) ).
cnf(u42960,axiom,
p(n4,n7,n6) ).
cnf(u42964,axiom,
p(n4,n8,n6) ).
cnf(u42968,axiom,
p(n4,n9,n6) ).
cnf(u42972,axiom,
p(n5,n7,n6) ).
cnf(u42977,axiom,
~ p(n5,n8,n6) ).
cnf(u42980,axiom,
p(n5,n9,n6) ).
cnf(u42984,axiom,
p(n6,n7,n6) ).
cnf(u42988,axiom,
p(n6,n8,n6) ).
cnf(u42992,axiom,
p(n6,n9,n6) ).
cnf(u42997,axiom,
p(n4,n7,n5) ).
cnf(u43001,axiom,
p(n4,n8,n5) ).
cnf(u43006,axiom,
~ p(n4,n9,n5) ).
cnf(u43009,axiom,
p(n5,n7,n5) ).
cnf(u43013,axiom,
p(n5,n8,n5) ).
cnf(u43017,axiom,
p(n5,n9,n5) ).
cnf(u43021,axiom,
p(n6,n7,n5) ).
cnf(u43025,axiom,
p(n6,n8,n5) ).
cnf(u43029,axiom,
p(n6,n9,n5) ).
cnf(u43034,axiom,
p(n4,n7,n4) ).
cnf(u43038,axiom,
p(n4,n8,n4) ).
cnf(u43042,axiom,
p(n4,n9,n4) ).
cnf(u43047,axiom,
~ p(n5,n7,n4) ).
cnf(u43050,axiom,
p(n5,n8,n4) ).
cnf(u43054,axiom,
p(n5,n9,n4) ).
cnf(u43058,axiom,
p(n6,n7,n4) ).
cnf(u43062,axiom,
p(n6,n8,n4) ).
cnf(u43066,axiom,
p(n6,n9,n4) ).
cnf(u43071,axiom,
p(n4,n7,n3) ).
cnf(u43076,axiom,
~ p(n4,n8,n3) ).
cnf(u43079,axiom,
p(n4,n9,n3) ).
cnf(u43083,axiom,
p(n5,n7,n3) ).
cnf(u43087,axiom,
p(n5,n8,n3) ).
cnf(u43091,axiom,
p(n5,n9,n3) ).
cnf(u43095,axiom,
p(n6,n7,n3) ).
cnf(u43099,axiom,
p(n6,n8,n3) ).
cnf(u43103,axiom,
p(n6,n9,n3) ).
cnf(u43108,axiom,
p(n4,n7,n2) ).
cnf(u43112,axiom,
p(n4,n8,n2) ).
cnf(u43116,axiom,
p(n4,n9,n2) ).
cnf(u43120,axiom,
p(n5,n7,n2) ).
cnf(u43124,axiom,
p(n5,n8,n2) ).
cnf(u43129,axiom,
~ p(n5,n9,n2) ).
cnf(u43132,axiom,
p(n6,n7,n2) ).
cnf(u43136,axiom,
p(n6,n8,n2) ).
cnf(u43140,axiom,
p(n6,n9,n2) ).
cnf(u43145,axiom,
p(n4,n7,n1) ).
cnf(u43149,axiom,
p(n4,n8,n1) ).
cnf(u43153,axiom,
p(n4,n9,n1) ).
cnf(u43157,axiom,
p(n5,n7,n1) ).
cnf(u43161,axiom,
p(n5,n8,n1) ).
cnf(u43165,axiom,
p(n5,n9,n1) ).
cnf(u43170,axiom,
~ p(n6,n7,n1) ).
cnf(u43173,axiom,
p(n6,n8,n1) ).
cnf(u43177,axiom,
p(n6,n9,n1) ).
cnf(u43182,axiom,
p(n4,n4,n9) ).
cnf(u43186,axiom,
p(n4,n5,n9) ).
cnf(u43190,axiom,
p(n4,n6,n9) ).
cnf(u43194,axiom,
p(n5,n4,n9) ).
cnf(u43198,axiom,
p(n5,n5,n9) ).
cnf(u43202,axiom,
p(n5,n6,n9) ).
cnf(u43207,axiom,
~ p(n6,n4,n9) ).
cnf(u43210,axiom,
p(n6,n5,n9) ).
cnf(u43214,axiom,
p(n6,n6,n9) ).
cnf(u43219,axiom,
p(n4,n4,n8) ).
cnf(u43223,axiom,
p(n4,n5,n8) ).
cnf(u43227,axiom,
p(n4,n6,n8) ).
cnf(u43232,axiom,
~ p(n5,n4,n8) ).
cnf(u43235,axiom,
p(n5,n5,n8) ).
cnf(u43239,axiom,
p(n5,n6,n8) ).
cnf(u43243,axiom,
p(n6,n4,n8) ).
cnf(u43247,axiom,
p(n6,n5,n8) ).
cnf(u43251,axiom,
p(n6,n6,n8) ).
cnf(u43256,axiom,
p(n4,n4,n7) ).
cnf(u43260,axiom,
p(n4,n5,n7) ).
cnf(u43264,axiom,
p(n4,n6,n7) ).
cnf(u43268,axiom,
p(n5,n4,n7) ).
cnf(u43272,axiom,
p(n5,n5,n7) ).
cnf(u43277,axiom,
~ p(n5,n6,n7) ).
cnf(u43280,axiom,
p(n6,n4,n7) ).
cnf(u43284,axiom,
p(n6,n5,n7) ).
cnf(u43288,axiom,
p(n6,n6,n7) ).
cnf(u43293,axiom,
p(n4,n4,n6) ).
cnf(u43297,axiom,
p(n4,n5,n6) ).
cnf(u43302,axiom,
~ p(n4,n6,n6) ).
cnf(u43305,axiom,
p(n5,n4,n6) ).
cnf(u43309,axiom,
p(n5,n5,n6) ).
cnf(u43313,axiom,
p(n5,n6,n6) ).
cnf(u43317,axiom,
p(n6,n4,n6) ).
cnf(u43321,axiom,
p(n6,n5,n6) ).
cnf(u43325,axiom,
p(n6,n6,n6) ).
cnf(u43330,axiom,
p(n4,n4,n5) ).
cnf(u43334,axiom,
p(n4,n5,n5) ).
cnf(u43338,axiom,
p(n4,n6,n5) ).
cnf(u43342,axiom,
p(n5,n4,n5) ).
cnf(u43346,axiom,
p(n5,n5,n5) ).
cnf(u43350,axiom,
p(n5,n6,n5) ).
cnf(u43354,axiom,
p(n6,n4,n5) ).
cnf(u43359,axiom,
~ p(n6,n5,n5) ).
cnf(u43362,axiom,
p(n6,n6,n5) ).
cnf(u43367,axiom,
p(n4,n4,n4) ).
cnf(u43372,axiom,
~ p(n4,n5,n4) ).
cnf(u43375,axiom,
p(n4,n6,n4) ).
cnf(u43379,axiom,
p(n5,n4,n4) ).
cnf(u43383,axiom,
p(n5,n5,n4) ).
cnf(u43387,axiom,
p(n5,n6,n4) ).
cnf(u43391,axiom,
p(n6,n4,n4) ).
cnf(u43395,axiom,
p(n6,n5,n4) ).
cnf(u43399,axiom,
p(n6,n6,n4) ).
cnf(u43404,axiom,
p(n4,n4,n3) ).
cnf(u43408,axiom,
p(n4,n5,n3) ).
cnf(u43412,axiom,
p(n4,n6,n3) ).
cnf(u43416,axiom,
p(n5,n4,n3) ).
cnf(u43420,axiom,
p(n5,n5,n3) ).
cnf(u43424,axiom,
p(n5,n6,n3) ).
cnf(u43428,axiom,
p(n6,n4,n3) ).
cnf(u43432,axiom,
p(n6,n5,n3) ).
cnf(u43437,axiom,
~ p(n6,n6,n3) ).
cnf(u43442,axiom,
~ p(n4,n4,n2) ).
cnf(u43445,axiom,
p(n4,n5,n2) ).
cnf(u43449,axiom,
p(n4,n6,n2) ).
cnf(u43453,axiom,
p(n5,n4,n2) ).
cnf(u43457,axiom,
p(n5,n5,n2) ).
cnf(u43461,axiom,
p(n5,n6,n2) ).
cnf(u43465,axiom,
p(n6,n4,n2) ).
cnf(u43469,axiom,
p(n6,n5,n2) ).
cnf(u43473,axiom,
p(n6,n6,n2) ).
cnf(u43478,axiom,
p(n4,n4,n1) ).
cnf(u43482,axiom,
p(n4,n5,n1) ).
cnf(u43486,axiom,
p(n4,n6,n1) ).
cnf(u43490,axiom,
p(n5,n4,n1) ).
cnf(u43495,axiom,
~ p(n5,n5,n1) ).
cnf(u43498,axiom,
p(n5,n6,n1) ).
cnf(u43502,axiom,
p(n6,n4,n1) ).
cnf(u43506,axiom,
p(n6,n5,n1) ).
cnf(u43510,axiom,
p(n6,n6,n1) ).
cnf(u43515,axiom,
p(n4,n1,n9) ).
cnf(u43519,axiom,
p(n4,n2,n9) ).
cnf(u43523,axiom,
p(n4,n3,n9) ).
cnf(u43528,axiom,
~ p(n5,n1,n9) ).
cnf(u43531,axiom,
p(n5,n2,n9) ).
cnf(u43535,axiom,
p(n5,n3,n9) ).
cnf(u43539,axiom,
p(n6,n1,n9) ).
cnf(u43543,axiom,
p(n6,n2,n9) ).
cnf(u43547,axiom,
p(n6,n3,n9) ).
cnf(u43553,axiom,
~ p(n4,n1,n8) ).
cnf(u43556,axiom,
p(n4,n2,n8) ).
cnf(u43560,axiom,
p(n4,n3,n8) ).
cnf(u43564,axiom,
p(n5,n1,n8) ).
cnf(u43568,axiom,
p(n5,n2,n8) ).
cnf(u43572,axiom,
p(n5,n3,n8) ).
cnf(u43576,axiom,
p(n6,n1,n8) ).
cnf(u43580,axiom,
p(n6,n2,n8) ).
cnf(u43584,axiom,
p(n6,n3,n8) ).
cnf(u43589,axiom,
p(n4,n1,n7) ).
cnf(u43594,axiom,
~ p(n4,n2,n7) ).
cnf(u43597,axiom,
p(n4,n3,n7) ).
cnf(u43601,axiom,
p(n5,n1,n7) ).
cnf(u43605,axiom,
p(n5,n2,n7) ).
cnf(u43609,axiom,
p(n5,n3,n7) ).
cnf(u43613,axiom,
p(n6,n1,n7) ).
cnf(u43617,axiom,
p(n6,n2,n7) ).
cnf(u43621,axiom,
p(n6,n3,n7) ).
cnf(u43626,axiom,
p(n4,n1,n6) ).
cnf(u43630,axiom,
p(n4,n2,n6) ).
cnf(u43634,axiom,
p(n4,n3,n6) ).
cnf(u43638,axiom,
p(n5,n1,n6) ).
cnf(u43642,axiom,
p(n5,n2,n6) ).
cnf(u43646,axiom,
p(n5,n3,n6) ).
cnf(u43650,axiom,
p(n6,n1,n6) ).
cnf(u43655,axiom,
~ p(n6,n2,n6) ).
cnf(u43658,axiom,
p(n6,n3,n6) ).
cnf(u43663,axiom,
p(n4,n1,n5) ).
cnf(u43667,axiom,
p(n4,n2,n5) ).
cnf(u43671,axiom,
p(n4,n3,n5) ).
cnf(u43675,axiom,
p(n5,n1,n5) ).
cnf(u43680,axiom,
~ p(n5,n2,n5) ).
cnf(u43683,axiom,
p(n5,n3,n5) ).
cnf(u43687,axiom,
p(n6,n1,n5) ).
cnf(u43691,axiom,
p(n6,n2,n5) ).
cnf(u43695,axiom,
p(n6,n3,n5) ).
cnf(u43700,axiom,
p(n4,n1,n4) ).
cnf(u43704,axiom,
p(n4,n2,n4) ).
cnf(u43708,axiom,
p(n4,n3,n4) ).
cnf(u43712,axiom,
p(n5,n1,n4) ).
cnf(u43716,axiom,
p(n5,n2,n4) ).
cnf(u43720,axiom,
p(n5,n3,n4) ).
cnf(u43725,axiom,
~ p(n6,n1,n4) ).
cnf(u43728,axiom,
p(n6,n2,n4) ).
cnf(u43732,axiom,
p(n6,n3,n4) ).
cnf(u43737,axiom,
p(n4,n1,n3) ).
cnf(u43741,axiom,
p(n4,n2,n3) ).
cnf(u43745,axiom,
p(n4,n3,n3) ).
cnf(u43749,axiom,
p(n5,n1,n3) ).
cnf(u43753,axiom,
p(n5,n2,n3) ).
cnf(u43758,axiom,
~ p(n5,n3,n3) ).
cnf(u43761,axiom,
p(n6,n1,n3) ).
cnf(u43765,axiom,
p(n6,n2,n3) ).
cnf(u43769,axiom,
p(n6,n3,n3) ).
cnf(u43774,axiom,
p(n4,n1,n2) ).
cnf(u43778,axiom,
p(n4,n2,n2) ).
cnf(u43782,axiom,
p(n4,n3,n2) ).
cnf(u43786,axiom,
p(n5,n1,n2) ).
cnf(u43790,axiom,
p(n5,n2,n2) ).
cnf(u43794,axiom,
p(n5,n3,n2) ).
cnf(u43798,axiom,
p(n6,n1,n2) ).
cnf(u43802,axiom,
p(n6,n2,n2) ).
cnf(u43807,axiom,
~ p(n6,n3,n2) ).
cnf(u43811,axiom,
p(n4,n1,n1) ).
cnf(u43815,axiom,
p(n4,n2,n1) ).
cnf(u43820,axiom,
~ p(n4,n3,n1) ).
cnf(u43823,axiom,
p(n5,n1,n1) ).
cnf(u43827,axiom,
p(n5,n2,n1) ).
cnf(u43831,axiom,
p(n5,n3,n1) ).
cnf(u43835,axiom,
p(n6,n1,n1) ).
cnf(u43839,axiom,
p(n6,n2,n1) ).
cnf(u43843,axiom,
p(n6,n3,n1) ).
cnf(u43848,axiom,
p(n1,n7,n9) ).
cnf(u43852,axiom,
p(n1,n8,n9) ).
cnf(u43857,axiom,
~ p(n1,n9,n9) ).
cnf(u43860,axiom,
p(n2,n7,n9) ).
cnf(u43864,axiom,
p(n2,n8,n9) ).
cnf(u43868,axiom,
p(n2,n9,n9) ).
cnf(u43872,axiom,
p(n3,n7,n9) ).
cnf(u43876,axiom,
p(n3,n8,n9) ).
cnf(u43880,axiom,
p(n3,n9,n9) ).
cnf(u43886,axiom,
~ p(n1,n7,n8) ).
cnf(u43889,axiom,
p(n1,n8,n8) ).
cnf(u43893,axiom,
p(n1,n9,n8) ).
cnf(u43897,axiom,
p(n2,n7,n8) ).
cnf(u43901,axiom,
p(n2,n8,n8) ).
cnf(u43905,axiom,
p(n2,n9,n8) ).
cnf(u43909,axiom,
p(n3,n7,n8) ).
cnf(u43913,axiom,
p(n3,n8,n8) ).
cnf(u43917,axiom,
p(n3,n9,n8) ).
cnf(u43922,axiom,
p(n1,n7,n7) ).
cnf(u43926,axiom,
p(n1,n8,n7) ).
cnf(u43930,axiom,
p(n1,n9,n7) ).
cnf(u43934,axiom,
p(n2,n7,n7) ).
cnf(u43939,axiom,
~ p(n2,n8,n7) ).
cnf(u43942,axiom,
p(n2,n9,n7) ).
cnf(u43946,axiom,
p(n3,n7,n7) ).
cnf(u43950,axiom,
p(n3,n8,n7) ).
cnf(u43954,axiom,
p(n3,n9,n7) ).
cnf(u43959,axiom,
p(n1,n7,n6) ).
cnf(u43963,axiom,
p(n1,n8,n6) ).
cnf(u43967,axiom,
p(n1,n9,n6) ).
cnf(u43971,axiom,
p(n2,n7,n6) ).
cnf(u43975,axiom,
p(n2,n8,n6) ).
cnf(u43979,axiom,
p(n2,n9,n6) ).
cnf(u43983,axiom,
p(n3,n7,n6) ).
cnf(u43987,axiom,
p(n3,n8,n6) ).
cnf(u43992,axiom,
~ p(n3,n9,n6) ).
cnf(u43996,axiom,
p(n1,n7,n5) ).
cnf(u44000,axiom,
p(n1,n8,n5) ).
cnf(u44004,axiom,
p(n1,n9,n5) ).
cnf(u44009,axiom,
~ p(n2,n7,n5) ).
cnf(u44012,axiom,
p(n2,n8,n5) ).
cnf(u44016,axiom,
p(n2,n9,n5) ).
cnf(u44020,axiom,
p(n3,n7,n5) ).
cnf(u44024,axiom,
p(n3,n8,n5) ).
cnf(u44028,axiom,
p(n3,n9,n5) ).
cnf(u44033,axiom,
p(n1,n7,n4) ).
cnf(u44037,axiom,
p(n1,n8,n4) ).
cnf(u44041,axiom,
p(n1,n9,n4) ).
cnf(u44045,axiom,
p(n2,n7,n4) ).
cnf(u44049,axiom,
p(n2,n8,n4) ).
cnf(u44053,axiom,
p(n2,n9,n4) ).
cnf(u44057,axiom,
p(n3,n7,n4) ).
cnf(u44062,axiom,
~ p(n3,n8,n4) ).
cnf(u44065,axiom,
p(n3,n9,n4) ).
cnf(u44070,axiom,
p(n1,n7,n3) ).
cnf(u44074,axiom,
p(n1,n8,n3) ).
cnf(u44078,axiom,
p(n1,n9,n3) ).
cnf(u44082,axiom,
p(n2,n7,n3) ).
cnf(u44086,axiom,
p(n2,n8,n3) ).
cnf(u44090,axiom,
p(n2,n9,n3) ).
cnf(u44095,axiom,
~ p(n3,n7,n3) ).
cnf(u44098,axiom,
p(n3,n8,n3) ).
cnf(u44102,axiom,
p(n3,n9,n3) ).
cnf(u44107,axiom,
p(n1,n7,n2) ).
cnf(u44112,axiom,
~ p(n1,n8,n2) ).
cnf(u44115,axiom,
p(n1,n9,n2) ).
cnf(u44119,axiom,
p(n2,n7,n2) ).
cnf(u44123,axiom,
p(n2,n8,n2) ).
cnf(u44127,axiom,
p(n2,n9,n2) ).
cnf(u44131,axiom,
p(n3,n7,n2) ).
cnf(u44135,axiom,
p(n3,n8,n2) ).
cnf(u44139,axiom,
p(n3,n9,n2) ).
cnf(u44144,axiom,
p(n1,n7,n1) ).
cnf(u44148,axiom,
p(n1,n8,n1) ).
cnf(u44152,axiom,
p(n1,n9,n1) ).
cnf(u44156,axiom,
p(n2,n7,n1) ).
cnf(u44160,axiom,
p(n2,n8,n1) ).
cnf(u44165,axiom,
~ p(n2,n9,n1) ).
cnf(u44168,axiom,
p(n3,n7,n1) ).
cnf(u44172,axiom,
p(n3,n8,n1) ).
cnf(u44176,axiom,
p(n3,n9,n1) ).
cnf(u44181,axiom,
p(n1,n4,n9) ).
cnf(u44185,axiom,
p(n1,n5,n9) ).
cnf(u44189,axiom,
p(n1,n6,n9) ).
cnf(u44193,axiom,
p(n2,n4,n9) ).
cnf(u44197,axiom,
p(n2,n5,n9) ).
cnf(u44201,axiom,
p(n2,n6,n9) ).
cnf(u44205,axiom,
p(n3,n4,n9) ).
cnf(u44209,axiom,
p(n3,n5,n9) ).
cnf(u44214,axiom,
~ p(n3,n6,n9) ).
cnf(u44218,axiom,
p(n1,n4,n8) ).
cnf(u44222,axiom,
p(n1,n5,n8) ).
cnf(u44226,axiom,
p(n1,n6,n8) ).
cnf(u44230,axiom,
p(n2,n4,n8) ).
cnf(u44234,axiom,
p(n2,n5,n8) ).
cnf(u44239,axiom,
~ p(n2,n6,n8) ).
cnf(u44242,axiom,
p(n3,n4,n8) ).
cnf(u44246,axiom,
p(n3,n5,n8) ).
cnf(u44250,axiom,
p(n3,n6,n8) ).
cnf(u44255,axiom,
p(n1,n4,n7) ).
cnf(u44259,axiom,
p(n1,n5,n7) ).
cnf(u44263,axiom,
p(n1,n6,n7) ).
cnf(u44267,axiom,
p(n2,n4,n7) ).
cnf(u44271,axiom,
p(n2,n5,n7) ).
cnf(u44275,axiom,
p(n2,n6,n7) ).
cnf(u44279,axiom,
p(n3,n4,n7) ).
cnf(u44284,axiom,
~ p(n3,n5,n7) ).
cnf(u44287,axiom,
p(n3,n6,n7) ).
cnf(u44293,axiom,
~ p(n1,n4,n6) ).
cnf(u44296,axiom,
p(n1,n5,n6) ).
cnf(u44300,axiom,
p(n1,n6,n6) ).
cnf(u44304,axiom,
p(n2,n4,n6) ).
cnf(u44308,axiom,
p(n2,n5,n6) ).
cnf(u44312,axiom,
p(n2,n6,n6) ).
cnf(u44316,axiom,
p(n3,n4,n6) ).
cnf(u44320,axiom,
p(n3,n5,n6) ).
cnf(u44324,axiom,
p(n3,n6,n6) ).
cnf(u44329,axiom,
p(n1,n4,n5) ).
cnf(u44333,axiom,
p(n1,n5,n5) ).
cnf(u44338,axiom,
~ p(n1,n6,n5) ).
cnf(u44341,axiom,
p(n2,n4,n5) ).
cnf(u44345,axiom,
p(n2,n5,n5) ).
cnf(u44349,axiom,
p(n2,n6,n5) ).
cnf(u44353,axiom,
p(n3,n4,n5) ).
cnf(u44357,axiom,
p(n3,n5,n5) ).
cnf(u44361,axiom,
p(n3,n6,n5) ).
cnf(u44366,axiom,
p(n1,n4,n4) ).
cnf(u44370,axiom,
p(n1,n5,n4) ).
cnf(u44374,axiom,
p(n1,n6,n4) ).
cnf(u44379,axiom,
~ p(n2,n4,n4) ).
cnf(u44382,axiom,
p(n2,n5,n4) ).
cnf(u44386,axiom,
p(n2,n6,n4) ).
cnf(u44390,axiom,
p(n3,n4,n4) ).
cnf(u44394,axiom,
p(n3,n5,n4) ).
cnf(u44398,axiom,
p(n3,n6,n4) ).
cnf(u44403,axiom,
p(n1,n4,n3) ).
cnf(u44408,axiom,
~ p(n1,n5,n3) ).
cnf(u44411,axiom,
p(n1,n6,n3) ).
cnf(u44415,axiom,
p(n2,n4,n3) ).
cnf(u44419,axiom,
p(n2,n5,n3) ).
cnf(u44423,axiom,
p(n2,n6,n3) ).
cnf(u44427,axiom,
p(n3,n4,n3) ).
cnf(u44431,axiom,
p(n3,n5,n3) ).
cnf(u44435,axiom,
p(n3,n6,n3) ).
cnf(u44440,axiom,
p(n1,n4,n2) ).
cnf(u44444,axiom,
p(n1,n5,n2) ).
cnf(u44448,axiom,
p(n1,n6,n2) ).
cnf(u44452,axiom,
p(n2,n4,n2) ).
cnf(u44457,axiom,
~ p(n2,n5,n2) ).
cnf(u44460,axiom,
p(n2,n6,n2) ).
cnf(u44464,axiom,
p(n3,n4,n2) ).
cnf(u44468,axiom,
p(n3,n5,n2) ).
cnf(u44472,axiom,
p(n3,n6,n2) ).
cnf(u44477,axiom,
p(n1,n4,n1) ).
cnf(u44481,axiom,
p(n1,n5,n1) ).
cnf(u44485,axiom,
p(n1,n6,n1) ).
cnf(u44489,axiom,
p(n2,n4,n1) ).
cnf(u44493,axiom,
p(n2,n5,n1) ).
cnf(u44497,axiom,
p(n2,n6,n1) ).
cnf(u44502,axiom,
~ p(n3,n4,n1) ).
cnf(u44505,axiom,
p(n3,n5,n1) ).
cnf(u44509,axiom,
p(n3,n6,n1) ).
cnf(u44514,axiom,
p(n1,n1,n9) ).
cnf(u44518,axiom,
p(n1,n2,n9) ).
cnf(u44522,axiom,
p(n1,n3,n9) ).
cnf(u44526,axiom,
p(n2,n1,n9) ).
cnf(u44531,axiom,
~ p(n2,n2,n9) ).
cnf(u44534,axiom,
p(n2,n3,n9) ).
cnf(u44538,axiom,
p(n3,n1,n9) ).
cnf(u44542,axiom,
p(n3,n2,n9) ).
cnf(u44546,axiom,
p(n3,n3,n9) ).
cnf(u44551,axiom,
p(n1,n1,n8) ).
cnf(u44555,axiom,
p(n1,n2,n8) ).
cnf(u44559,axiom,
p(n1,n3,n8) ).
cnf(u44563,axiom,
p(n2,n1,n8) ).
cnf(u44567,axiom,
p(n2,n2,n8) ).
cnf(u44571,axiom,
p(n2,n3,n8) ).
cnf(u44575,axiom,
p(n3,n1,n8) ).
cnf(u44579,axiom,
p(n3,n2,n8) ).
cnf(u44584,axiom,
~ p(n3,n3,n8) ).
cnf(u44588,axiom,
p(n1,n1,n7) ).
cnf(u44592,axiom,
p(n1,n2,n7) ).
cnf(u44597,axiom,
~ p(n1,n3,n7) ).
cnf(u44600,axiom,
p(n2,n1,n7) ).
cnf(u44604,axiom,
p(n2,n2,n7) ).
cnf(u44608,axiom,
p(n2,n3,n7) ).
cnf(u44612,axiom,
p(n3,n1,n7) ).
cnf(u44616,axiom,
p(n3,n2,n7) ).
cnf(u44620,axiom,
p(n3,n3,n7) ).
cnf(u44625,axiom,
p(n1,n1,n6) ).
cnf(u44629,axiom,
p(n1,n2,n6) ).
cnf(u44633,axiom,
p(n1,n3,n6) ).
cnf(u44637,axiom,
p(n2,n1,n6) ).
cnf(u44641,axiom,
p(n2,n2,n6) ).
cnf(u44646,axiom,
~ p(n2,n3,n6) ).
cnf(u44649,axiom,
p(n3,n1,n6) ).
cnf(u44653,axiom,
p(n3,n2,n6) ).
cnf(u44657,axiom,
p(n3,n3,n6) ).
cnf(u44662,axiom,
p(n1,n1,n5) ).
cnf(u44666,axiom,
p(n1,n2,n5) ).
cnf(u44670,axiom,
p(n1,n3,n5) ).
cnf(u44674,axiom,
p(n2,n1,n5) ).
cnf(u44678,axiom,
p(n2,n2,n5) ).
cnf(u44682,axiom,
p(n2,n3,n5) ).
cnf(u44687,axiom,
~ p(n3,n1,n5) ).
cnf(u44690,axiom,
p(n3,n2,n5) ).
cnf(u44694,axiom,
p(n3,n3,n5) ).
cnf(u44699,axiom,
p(n1,n1,n4) ).
cnf(u44704,axiom,
~ p(n1,n2,n4) ).
cnf(u44707,axiom,
p(n1,n3,n4) ).
cnf(u44711,axiom,
p(n2,n1,n4) ).
cnf(u44715,axiom,
p(n2,n2,n4) ).
cnf(u44719,axiom,
p(n2,n3,n4) ).
cnf(u44723,axiom,
p(n3,n1,n4) ).
cnf(u44727,axiom,
p(n3,n2,n4) ).
cnf(u44731,axiom,
p(n3,n3,n4) ).
cnf(u44736,axiom,
p(n1,n1,n3) ).
cnf(u44740,axiom,
p(n1,n2,n3) ).
cnf(u44744,axiom,
p(n1,n3,n3) ).
cnf(u44749,axiom,
~ p(n2,n1,n3) ).
cnf(u44752,axiom,
p(n2,n2,n3) ).
cnf(u44756,axiom,
p(n2,n3,n3) ).
cnf(u44760,axiom,
p(n3,n1,n3) ).
cnf(u44764,axiom,
p(n3,n2,n3) ).
cnf(u44768,axiom,
p(n3,n3,n3) ).
cnf(u44773,axiom,
p(n1,n1,n2) ).
cnf(u44777,axiom,
p(n1,n2,n2) ).
cnf(u44781,axiom,
p(n1,n3,n2) ).
cnf(u44785,axiom,
p(n2,n1,n2) ).
cnf(u44789,axiom,
p(n2,n2,n2) ).
cnf(u44793,axiom,
p(n2,n3,n2) ).
cnf(u44797,axiom,
p(n3,n1,n2) ).
cnf(u44802,axiom,
~ p(n3,n2,n2) ).
cnf(u44805,axiom,
p(n3,n3,n2) ).
cnf(u44811,axiom,
~ p(n1,n1,n1) ).
cnf(u44814,axiom,
p(n1,n2,n1) ).
cnf(u44818,axiom,
p(n1,n3,n1) ).
cnf(u44822,axiom,
p(n2,n1,n1) ).
cnf(u44826,axiom,
p(n2,n2,n1) ).
cnf(u44830,axiom,
p(n2,n3,n1) ).
cnf(u44834,axiom,
p(n3,n1,n1) ).
cnf(u44838,axiom,
p(n3,n2,n1) ).
cnf(u44842,axiom,
p(n3,n3,n1) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ069+2 : TPTP v9.3.1. Bugfixed v5.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.39 % Computer : n008.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 22:40:10 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.42 Running first-order model finding
% 0.11/0.42 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.74/0.86 % (1672058)Will run a generic schedule for satisfiability detection.
% 0.74/0.86 % (1672067)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3147122048:i=116_2997 on theBenchmark for (2997ds/116Mi)
% 0.74/0.86 % (1672064)% WARNING: option uhcvi not known.
% 0.74/0.86 % (1672063)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3643088388_2997 on theBenchmark for (2997ds/0Mi)
% 0.74/0.86 % (1672064)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2340776033:i=135531:add=off:rawr=on_2997 on theBenchmark for (2997ds/135531Mi)
% 0.74/0.86 % (1672065)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=290616236:i=88024:add=on:rawr=on_2997 on theBenchmark for (2997ds/88024Mi)
% 0.74/0.86 % (1672066)dis+10_1_sil=32000:sp=arity:random_seed=1046241012:i=103:fgj=on_2997 on theBenchmark for (2997ds/103Mi)
% 0.74/0.86 % (1672068)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1758374077:i=131_2997 on theBenchmark for (2997ds/131Mi)
% 0.74/0.86 % (1672069)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=419524300:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2997 on theBenchmark for (2997ds/159Mi)
% 0.74/0.86 % (1672067)Instruction limit reached!
% 0.74/0.86 % (1672067)------------------------------
% 0.74/0.86 % (1672067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.86 % (1672067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.86 % (1672067)CaDiCaL version: 2.1.3
% 0.74/0.86 % (1672067)Termination reason: Instruction limit
% 0.74/0.86 % (1672067)Termination phase: Property scanning
% 0.74/0.86 % (1672067)Time elapsed: 0.040 s
% 0.74/0.86 % (1672067)Peak memory usage: 24 MB
% 0.74/0.86 % (1672067)Instructions burned: 119 (million)
% 0.74/0.86 % (1672066)Instruction limit reached!
% 0.74/0.86 % (1672066)------------------------------
% 0.74/0.86 % (1672066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.86 % (1672066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.86 % (1672066)CaDiCaL version: 2.1.3
% 0.74/0.86 % (1672066)Termination reason: Instruction limit
% 0.74/0.86 % (1672066)Termination phase: Property scanning
% 0.74/0.86 % (1672066)Time elapsed: 0.052 s
% 0.74/0.86 % (1672066)Peak memory usage: 22 MB
% 0.74/0.86 % (1672066)Instructions burned: 105 (million)
% 0.74/0.86 % (1672077)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=806946188:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 0.74/0.86 % (1672069)Instruction limit reached!
% 0.74/0.86 % (1672069)------------------------------
% 0.74/0.86 % (1672069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.86 % (1672069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.86 % (1672069)CaDiCaL version: 2.1.3
% 0.74/0.86 % (1672069)Termination reason: Instruction limit
% 0.74/0.86 % (1672069)Termination phase: Property scanning
% 0.74/0.86 % (1672069)Time elapsed: 0.056 s
% 0.74/0.86 % (1672069)Peak memory usage: 21 MB
% 0.74/0.86 % (1672069)Instructions burned: 163 (million)
% 0.74/0.86 % (1672068)Instruction limit reached!
% 0.74/0.86 % (1672068)------------------------------
% 0.74/0.86 % (1672068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.86 % (1672068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.86 % (1672068)CaDiCaL version: 2.1.3
% 0.74/0.86 % (1672068)Termination reason: Instruction limit
% 0.74/0.86 % (1672068)Termination phase: Property scanning
% 0.74/0.86 % (1672068)Time elapsed: 0.063 s
% 0.74/0.86 % (1672068)Peak memory usage: 22 MB
% 0.74/0.86 % (1672068)Instructions burned: 133 (million)
% 0.74/0.86 % (1672080)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=2762237788:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 0.74/0.86 % (1672078)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2630278482:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 0.74/0.86 % (1672081)ott-21_1_sil=16000:fs=off:random_seed=2694040934:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 0.74/0.86 % (1672078)Instruction limit reached!
% 0.74/0.86 % (1672078)------------------------------
% 0.74/0.86 % (1672078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.86 % (1672078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.86 % (1672078)CaDiCaL version: 2.1.3
% 0.74/0.86 % (1672078)Termination reason: Instruction limit
% 0.74/0.86 % (1672078)Termination phase: Property scanning
% 0.74/0.86 % (1672078)Time elapsed: 0.061 s
% 0.74/0.86 % (1672078)Peak memory usage: 22 MB
% 0.74/0.86 % (1672078)Instructions burned: 133 (million)
% 0.74/0.86 % (1672085)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3774376717:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 0.74/0.86 % (1672081)Instruction limit reached!
% 0.74/0.86 % (1672081)------------------------------
% 0.74/0.86 % (1672081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.86 % (1672081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.86 % (1672081)CaDiCaL version: 2.1.3
% 0.74/0.86 % (1672081)Termination reason: Instruction limit
% 0.74/0.86 % (1672081)Termination phase: Saturation
% 0.74/0.86 % (1672081)Time elapsed: 0.078 s
% 0.74/0.86 % (1672081)Peak memory usage: 23 MB
% 0.74/0.86 % (1672081)Instructions burned: 180 (million)
% 0.74/0.86 % (1672064) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1672058-1672064"...
% 0.74/0.86 % (1672080) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1672058-1672080"...
% 0.74/0.86 % (1672087)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1323348765:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 0.74/0.86 % (1672064)...printing done.
% 0.74/0.86 % (1672080)...printing done.
% 0.74/0.86 % SZS status Satisfiable for theBenchmark
% 0.74/0.86 % SZS output start Saturation.
% See solution above
% 0.74/0.87 % SZS output start Definitions and Model Updates.
% 0.74/0.87 globally flip the polarity of every occurrence of predicate "p"
% 0.74/0.87 % SZS output end Definitions and Model Updates.
% 0.74/0.87 % (1672064)------------------------------
% 0.74/0.87 % (1672064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.87 % (1672064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.87 % (1672064)CaDiCaL version: 2.1.3
% 0.74/0.87 % (1672064)Termination reason: Satisfiable
% 0.74/0.87 % (1672064)Time elapsed: 0.176 s
% 0.74/0.87 % (1672064)Peak memory usage: 35 MB
% 0.74/0.87 % (1672064)Instructions burned: 335 (million)
% 0.74/0.87 % (1672058)Success in time 0.43 s
% 0.74/0.87 % Vampire exiting
%------------------------------------------------------------------------------