%------------------------------------------------------------------------------
% File : Vampire-SAT---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 SAT
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:32:35 PM UTC 2026
% Result : Satisfiable 0.68s 0.85s
% Output : Saturation 0.68s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u31311,axiom,
~ p(n7,n7,n9) ).
cnf(u31316,axiom,
p(n7,n8,n9) ).
cnf(u31319,axiom,
~ p(n7,n9,n9) ).
cnf(u31323,axiom,
~ p(n8,n7,n9) ).
cnf(u31327,axiom,
~ p(n8,n8,n9) ).
cnf(u31331,axiom,
~ p(n8,n9,n9) ).
cnf(u31335,axiom,
~ p(n9,n7,n9) ).
cnf(u31339,axiom,
~ p(n9,n8,n9) ).
cnf(u31343,axiom,
~ p(n9,n9,n9) ).
cnf(u31348,axiom,
~ p(n7,n7,n8) ).
cnf(u31352,axiom,
~ p(n7,n8,n8) ).
cnf(u31356,axiom,
~ p(n7,n9,n8) ).
cnf(u31360,axiom,
~ p(n8,n7,n8) ).
cnf(u31364,axiom,
~ p(n8,n8,n8) ).
cnf(u31368,axiom,
~ p(n8,n9,n8) ).
cnf(u31372,axiom,
~ p(n9,n7,n8) ).
cnf(u31376,axiom,
~ p(n9,n8,n8) ).
cnf(u31381,axiom,
p(n9,n9,n8) ).
cnf(u31385,axiom,
~ p(n7,n7,n7) ).
cnf(u31389,axiom,
~ p(n7,n8,n7) ).
cnf(u31393,axiom,
~ p(n7,n9,n7) ).
cnf(u31397,axiom,
~ p(n8,n7,n7) ).
cnf(u31401,axiom,
~ p(n8,n8,n7) ).
cnf(u31406,axiom,
p(n8,n9,n7) ).
cnf(u31409,axiom,
~ p(n9,n7,n7) ).
cnf(u31413,axiom,
~ p(n9,n8,n7) ).
cnf(u31417,axiom,
~ p(n9,n9,n7) ).
cnf(u31422,axiom,
~ p(n7,n7,n6) ).
cnf(u31426,axiom,
~ p(n7,n8,n6) ).
cnf(u31430,axiom,
~ p(n7,n9,n6) ).
cnf(u31434,axiom,
~ p(n8,n7,n6) ).
cnf(u31439,axiom,
p(n8,n8,n6) ).
cnf(u31442,axiom,
~ p(n8,n9,n6) ).
cnf(u31446,axiom,
~ p(n9,n7,n6) ).
cnf(u31450,axiom,
~ p(n9,n8,n6) ).
cnf(u31454,axiom,
~ p(n9,n9,n6) ).
cnf(u31459,axiom,
~ p(n7,n7,n5) ).
cnf(u31463,axiom,
~ p(n7,n8,n5) ).
cnf(u31467,axiom,
~ p(n7,n9,n5) ).
cnf(u31472,axiom,
p(n8,n7,n5) ).
cnf(u31475,axiom,
~ p(n8,n8,n5) ).
cnf(u31479,axiom,
~ p(n8,n9,n5) ).
cnf(u31483,axiom,
~ p(n9,n7,n5) ).
cnf(u31487,axiom,
~ p(n9,n8,n5) ).
cnf(u31491,axiom,
~ p(n9,n9,n5) ).
cnf(u31496,axiom,
~ p(n7,n7,n4) ).
cnf(u31500,axiom,
~ p(n7,n8,n4) ).
cnf(u31505,axiom,
p(n7,n9,n4) ).
cnf(u31508,axiom,
~ p(n8,n7,n4) ).
cnf(u31512,axiom,
~ p(n8,n8,n4) ).
cnf(u31516,axiom,
~ p(n8,n9,n4) ).
cnf(u31520,axiom,
~ p(n9,n7,n4) ).
cnf(u31524,axiom,
~ p(n9,n8,n4) ).
cnf(u31528,axiom,
~ p(n9,n9,n4) ).
cnf(u31533,axiom,
~ p(n7,n7,n3) ).
cnf(u31537,axiom,
~ p(n7,n8,n3) ).
cnf(u31541,axiom,
~ p(n7,n9,n3) ).
cnf(u31545,axiom,
~ p(n8,n7,n3) ).
cnf(u31549,axiom,
~ p(n8,n8,n3) ).
cnf(u31553,axiom,
~ p(n8,n9,n3) ).
cnf(u31557,axiom,
~ p(n9,n7,n3) ).
cnf(u31562,axiom,
p(n9,n8,n3) ).
cnf(u31565,axiom,
~ p(n9,n9,n3) ).
cnf(u31570,axiom,
~ p(n7,n7,n2) ).
cnf(u31574,axiom,
~ p(n7,n8,n2) ).
cnf(u31578,axiom,
~ p(n7,n9,n2) ).
cnf(u31582,axiom,
~ p(n8,n7,n2) ).
cnf(u31586,axiom,
~ p(n8,n8,n2) ).
cnf(u31590,axiom,
~ p(n8,n9,n2) ).
cnf(u31595,axiom,
p(n9,n7,n2) ).
cnf(u31598,axiom,
~ p(n9,n8,n2) ).
cnf(u31602,axiom,
~ p(n9,n9,n2) ).
cnf(u31608,axiom,
p(n7,n7,n1) ).
cnf(u31611,axiom,
~ p(n7,n8,n1) ).
cnf(u31615,axiom,
~ p(n7,n9,n1) ).
cnf(u31619,axiom,
~ p(n8,n7,n1) ).
cnf(u31623,axiom,
~ p(n8,n8,n1) ).
cnf(u31627,axiom,
~ p(n8,n9,n1) ).
cnf(u31631,axiom,
~ p(n9,n7,n1) ).
cnf(u31635,axiom,
~ p(n9,n8,n1) ).
cnf(u31639,axiom,
~ p(n9,n9,n1) ).
cnf(u31644,axiom,
~ p(n7,n4,n9) ).
cnf(u31648,axiom,
~ p(n7,n5,n9) ).
cnf(u31652,axiom,
~ p(n7,n6,n9) ).
cnf(u31656,axiom,
~ p(n8,n4,n9) ).
cnf(u31660,axiom,
~ p(n8,n5,n9) ).
cnf(u31664,axiom,
~ p(n8,n6,n9) ).
cnf(u31669,axiom,
p(n9,n4,n9) ).
cnf(u31672,axiom,
~ p(n9,n5,n9) ).
cnf(u31676,axiom,
~ p(n9,n6,n9) ).
cnf(u31681,axiom,
~ p(n7,n4,n8) ).
cnf(u31685,axiom,
~ p(n7,n5,n8) ).
cnf(u31689,axiom,
~ p(n7,n6,n8) ).
cnf(u31693,axiom,
~ p(n8,n4,n8) ).
cnf(u31697,axiom,
~ p(n8,n5,n8) ).
cnf(u31702,axiom,
p(n8,n6,n8) ).
cnf(u31705,axiom,
~ p(n9,n4,n8) ).
cnf(u31709,axiom,
~ p(n9,n5,n8) ).
cnf(u31713,axiom,
~ p(n9,n6,n8) ).
cnf(u31718,axiom,
~ p(n7,n4,n7) ).
cnf(u31722,axiom,
~ p(n7,n5,n7) ).
cnf(u31727,axiom,
p(n7,n6,n7) ).
cnf(u31730,axiom,
~ p(n8,n4,n7) ).
cnf(u31734,axiom,
~ p(n8,n5,n7) ).
cnf(u31738,axiom,
~ p(n8,n6,n7) ).
cnf(u31742,axiom,
~ p(n9,n4,n7) ).
cnf(u31746,axiom,
~ p(n9,n5,n7) ).
cnf(u31750,axiom,
~ p(n9,n6,n7) ).
cnf(u31755,axiom,
~ p(n7,n4,n6) ).
cnf(u31759,axiom,
~ p(n7,n5,n6) ).
cnf(u31763,axiom,
~ p(n7,n6,n6) ).
cnf(u31767,axiom,
~ p(n8,n4,n6) ).
cnf(u31771,axiom,
~ p(n8,n5,n6) ).
cnf(u31775,axiom,
~ p(n8,n6,n6) ).
cnf(u31779,axiom,
~ p(n9,n4,n6) ).
cnf(u31783,axiom,
~ p(n9,n5,n6) ).
cnf(u31788,axiom,
p(n9,n6,n6) ).
cnf(u31793,axiom,
p(n7,n4,n5) ).
cnf(u31796,axiom,
~ p(n7,n5,n5) ).
cnf(u31800,axiom,
~ p(n7,n6,n5) ).
cnf(u31804,axiom,
~ p(n8,n4,n5) ).
cnf(u31808,axiom,
~ p(n8,n5,n5) ).
cnf(u31812,axiom,
~ p(n8,n6,n5) ).
cnf(u31816,axiom,
~ p(n9,n4,n5) ).
cnf(u31820,axiom,
~ p(n9,n5,n5) ).
cnf(u31824,axiom,
~ p(n9,n6,n5) ).
cnf(u31829,axiom,
~ p(n7,n4,n4) ).
cnf(u31833,axiom,
~ p(n7,n5,n4) ).
cnf(u31837,axiom,
~ p(n7,n6,n4) ).
cnf(u31841,axiom,
~ p(n8,n4,n4) ).
cnf(u31846,axiom,
p(n8,n5,n4) ).
cnf(u31849,axiom,
~ p(n8,n6,n4) ).
cnf(u31853,axiom,
~ p(n9,n4,n4) ).
cnf(u31857,axiom,
~ p(n9,n5,n4) ).
cnf(u31861,axiom,
~ p(n9,n6,n4) ).
cnf(u31866,axiom,
~ p(n7,n4,n3) ).
cnf(u31871,axiom,
p(n7,n5,n3) ).
cnf(u31874,axiom,
~ p(n7,n6,n3) ).
cnf(u31878,axiom,
~ p(n8,n4,n3) ).
cnf(u31882,axiom,
~ p(n8,n5,n3) ).
cnf(u31886,axiom,
~ p(n8,n6,n3) ).
cnf(u31890,axiom,
~ p(n9,n4,n3) ).
cnf(u31894,axiom,
~ p(n9,n5,n3) ).
cnf(u31898,axiom,
~ p(n9,n6,n3) ).
cnf(u31903,axiom,
~ p(n7,n4,n2) ).
cnf(u31907,axiom,
~ p(n7,n5,n2) ).
cnf(u31911,axiom,
~ p(n7,n6,n2) ).
cnf(u31916,axiom,
p(n8,n4,n2) ).
cnf(u31919,axiom,
~ p(n8,n5,n2) ).
cnf(u31923,axiom,
~ p(n8,n6,n2) ).
cnf(u31927,axiom,
~ p(n9,n4,n2) ).
cnf(u31931,axiom,
~ p(n9,n5,n2) ).
cnf(u31935,axiom,
~ p(n9,n6,n2) ).
cnf(u31940,axiom,
~ p(n7,n4,n1) ).
cnf(u31944,axiom,
~ p(n7,n5,n1) ).
cnf(u31948,axiom,
~ p(n7,n6,n1) ).
cnf(u31952,axiom,
~ p(n8,n4,n1) ).
cnf(u31956,axiom,
~ p(n8,n5,n1) ).
cnf(u31960,axiom,
~ p(n8,n6,n1) ).
cnf(u31964,axiom,
~ p(n9,n4,n1) ).
cnf(u31969,axiom,
p(n9,n5,n1) ).
cnf(u31972,axiom,
~ p(n9,n6,n1) ).
cnf(u31977,axiom,
~ p(n7,n1,n9) ).
cnf(u31981,axiom,
~ p(n7,n2,n9) ).
cnf(u31985,axiom,
~ p(n7,n3,n9) ).
cnf(u31990,axiom,
p(n8,n1,n9) ).
cnf(u31993,axiom,
~ p(n8,n2,n9) ).
cnf(u31997,axiom,
~ p(n8,n3,n9) ).
cnf(u32001,axiom,
~ p(n9,n1,n9) ).
cnf(u32005,axiom,
~ p(n9,n2,n9) ).
cnf(u32009,axiom,
~ p(n9,n3,n9) ).
cnf(u32014,axiom,
~ p(n7,n1,n8) ).
cnf(u32018,axiom,
~ p(n7,n2,n8) ).
cnf(u32023,axiom,
p(n7,n3,n8) ).
cnf(u32026,axiom,
~ p(n8,n1,n8) ).
cnf(u32030,axiom,
~ p(n8,n2,n8) ).
cnf(u32034,axiom,
~ p(n8,n3,n8) ).
cnf(u32038,axiom,
~ p(n9,n1,n8) ).
cnf(u32042,axiom,
~ p(n9,n2,n8) ).
cnf(u32046,axiom,
~ p(n9,n3,n8) ).
cnf(u32051,axiom,
~ p(n7,n1,n7) ).
cnf(u32055,axiom,
~ p(n7,n2,n7) ).
cnf(u32059,axiom,
~ p(n7,n3,n7) ).
cnf(u32063,axiom,
~ p(n8,n1,n7) ).
cnf(u32067,axiom,
~ p(n8,n2,n7) ).
cnf(u32071,axiom,
~ p(n8,n3,n7) ).
cnf(u32075,axiom,
~ p(n9,n1,n7) ).
cnf(u32080,axiom,
p(n9,n2,n7) ).
cnf(u32083,axiom,
~ p(n9,n3,n7) ).
cnf(u32089,axiom,
p(n7,n1,n6) ).
cnf(u32092,axiom,
~ p(n7,n2,n6) ).
cnf(u32096,axiom,
~ p(n7,n3,n6) ).
cnf(u32100,axiom,
~ p(n8,n1,n6) ).
cnf(u32104,axiom,
~ p(n8,n2,n6) ).
cnf(u32108,axiom,
~ p(n8,n3,n6) ).
cnf(u32112,axiom,
~ p(n9,n1,n6) ).
cnf(u32116,axiom,
~ p(n9,n2,n6) ).
cnf(u32120,axiom,
~ p(n9,n3,n6) ).
cnf(u32125,axiom,
~ p(n7,n1,n5) ).
cnf(u32129,axiom,
~ p(n7,n2,n5) ).
cnf(u32133,axiom,
~ p(n7,n3,n5) ).
cnf(u32137,axiom,
~ p(n8,n1,n5) ).
cnf(u32141,axiom,
~ p(n8,n2,n5) ).
cnf(u32145,axiom,
~ p(n8,n3,n5) ).
cnf(u32149,axiom,
~ p(n9,n1,n5) ).
cnf(u32153,axiom,
~ p(n9,n2,n5) ).
cnf(u32158,axiom,
p(n9,n3,n5) ).
cnf(u32162,axiom,
~ p(n7,n1,n4) ).
cnf(u32166,axiom,
~ p(n7,n2,n4) ).
cnf(u32170,axiom,
~ p(n7,n3,n4) ).
cnf(u32174,axiom,
~ p(n8,n1,n4) ).
cnf(u32178,axiom,
~ p(n8,n2,n4) ).
cnf(u32182,axiom,
~ p(n8,n3,n4) ).
cnf(u32187,axiom,
p(n9,n1,n4) ).
cnf(u32190,axiom,
~ p(n9,n2,n4) ).
cnf(u32194,axiom,
~ p(n9,n3,n4) ).
cnf(u32199,axiom,
~ p(n7,n1,n3) ).
cnf(u32203,axiom,
~ p(n7,n2,n3) ).
cnf(u32207,axiom,
~ p(n7,n3,n3) ).
cnf(u32211,axiom,
~ p(n8,n1,n3) ).
cnf(u32215,axiom,
~ p(n8,n2,n3) ).
cnf(u32220,axiom,
p(n8,n3,n3) ).
cnf(u32223,axiom,
~ p(n9,n1,n3) ).
cnf(u32227,axiom,
~ p(n9,n2,n3) ).
cnf(u32231,axiom,
~ p(n9,n3,n3) ).
cnf(u32236,axiom,
~ p(n7,n1,n2) ).
cnf(u32241,axiom,
p(n7,n2,n2) ).
cnf(u32244,axiom,
~ p(n7,n3,n2) ).
cnf(u32248,axiom,
~ p(n8,n1,n2) ).
cnf(u32252,axiom,
~ p(n8,n2,n2) ).
cnf(u32256,axiom,
~ p(n8,n3,n2) ).
cnf(u32260,axiom,
~ p(n9,n1,n2) ).
cnf(u32264,axiom,
~ p(n9,n2,n2) ).
cnf(u32268,axiom,
~ p(n9,n3,n2) ).
cnf(u32273,axiom,
~ p(n7,n1,n1) ).
cnf(u32277,axiom,
~ p(n7,n2,n1) ).
cnf(u32281,axiom,
~ p(n7,n3,n1) ).
cnf(u32285,axiom,
~ p(n8,n1,n1) ).
cnf(u32290,axiom,
p(n8,n2,n1) ).
cnf(u32293,axiom,
~ p(n8,n3,n1) ).
cnf(u32297,axiom,
~ p(n9,n1,n1) ).
cnf(u32301,axiom,
~ p(n9,n2,n1) ).
cnf(u32305,axiom,
~ p(n9,n3,n1) ).
cnf(u32310,axiom,
~ p(n4,n7,n9) ).
cnf(u32314,axiom,
~ p(n4,n8,n9) ).
cnf(u32318,axiom,
~ p(n4,n9,n9) ).
cnf(u32322,axiom,
~ p(n5,n7,n9) ).
cnf(u32326,axiom,
~ p(n5,n8,n9) ).
cnf(u32331,axiom,
p(n5,n9,n9) ).
cnf(u32334,axiom,
~ p(n6,n7,n9) ).
cnf(u32338,axiom,
~ p(n6,n8,n9) ).
cnf(u32342,axiom,
~ p(n6,n9,n9) ).
cnf(u32347,axiom,
~ p(n4,n7,n8) ).
cnf(u32351,axiom,
~ p(n4,n8,n8) ).
cnf(u32355,axiom,
~ p(n4,n9,n8) ).
cnf(u32360,axiom,
p(n5,n7,n8) ).
cnf(u32363,axiom,
~ p(n5,n8,n8) ).
cnf(u32367,axiom,
~ p(n5,n9,n8) ).
cnf(u32371,axiom,
~ p(n6,n7,n8) ).
cnf(u32375,axiom,
~ p(n6,n8,n8) ).
cnf(u32379,axiom,
~ p(n6,n9,n8) ).
cnf(u32384,axiom,
~ p(n4,n7,n7) ).
cnf(u32389,axiom,
p(n4,n8,n7) ).
cnf(u32392,axiom,
~ p(n4,n9,n7) ).
cnf(u32396,axiom,
~ p(n5,n7,n7) ).
cnf(u32400,axiom,
~ p(n5,n8,n7) ).
cnf(u32404,axiom,
~ p(n5,n9,n7) ).
cnf(u32408,axiom,
~ p(n6,n7,n7) ).
cnf(u32412,axiom,
~ p(n6,n8,n7) ).
cnf(u32416,axiom,
~ p(n6,n9,n7) ).
cnf(u32422,axiom,
p(n4,n7,n6) ).
cnf(u32425,axiom,
~ p(n4,n8,n6) ).
cnf(u32429,axiom,
~ p(n4,n9,n6) ).
cnf(u32433,axiom,
~ p(n5,n7,n6) ).
cnf(u32437,axiom,
~ p(n5,n8,n6) ).
cnf(u32441,axiom,
~ p(n5,n9,n6) ).
cnf(u32445,axiom,
~ p(n6,n7,n6) ).
cnf(u32449,axiom,
~ p(n6,n8,n6) ).
cnf(u32453,axiom,
~ p(n6,n9,n6) ).
cnf(u32458,axiom,
~ p(n4,n7,n5) ).
cnf(u32462,axiom,
~ p(n4,n8,n5) ).
cnf(u32467,axiom,
p(n4,n9,n5) ).
cnf(u32470,axiom,
~ p(n5,n7,n5) ).
cnf(u32474,axiom,
~ p(n5,n8,n5) ).
cnf(u32478,axiom,
~ p(n5,n9,n5) ).
cnf(u32482,axiom,
~ p(n6,n7,n5) ).
cnf(u32486,axiom,
~ p(n6,n8,n5) ).
cnf(u32490,axiom,
~ p(n6,n9,n5) ).
cnf(u32495,axiom,
~ p(n4,n7,n4) ).
cnf(u32499,axiom,
~ p(n4,n8,n4) ).
cnf(u32503,axiom,
~ p(n4,n9,n4) ).
cnf(u32507,axiom,
~ p(n5,n7,n4) ).
cnf(u32511,axiom,
~ p(n5,n8,n4) ).
cnf(u32515,axiom,
~ p(n5,n9,n4) ).
cnf(u32519,axiom,
~ p(n6,n7,n4) ).
cnf(u32524,axiom,
p(n6,n8,n4) ).
cnf(u32527,axiom,
~ p(n6,n9,n4) ).
cnf(u32532,axiom,
~ p(n4,n7,n3) ).
cnf(u32536,axiom,
~ p(n4,n8,n3) ).
cnf(u32540,axiom,
~ p(n4,n9,n3) ).
cnf(u32544,axiom,
~ p(n5,n7,n3) ).
cnf(u32548,axiom,
~ p(n5,n8,n3) ).
cnf(u32552,axiom,
~ p(n5,n9,n3) ).
cnf(u32557,axiom,
p(n6,n7,n3) ).
cnf(u32560,axiom,
~ p(n6,n8,n3) ).
cnf(u32564,axiom,
~ p(n6,n9,n3) ).
cnf(u32569,axiom,
~ p(n4,n7,n2) ).
cnf(u32573,axiom,
~ p(n4,n8,n2) ).
cnf(u32577,axiom,
~ p(n4,n9,n2) ).
cnf(u32581,axiom,
~ p(n5,n7,n2) ).
cnf(u32586,axiom,
p(n5,n8,n2) ).
cnf(u32589,axiom,
~ p(n5,n9,n2) ).
cnf(u32593,axiom,
~ p(n6,n7,n2) ).
cnf(u32597,axiom,
~ p(n6,n8,n2) ).
cnf(u32601,axiom,
~ p(n6,n9,n2) ).
cnf(u32606,axiom,
~ p(n4,n7,n1) ).
cnf(u32610,axiom,
~ p(n4,n8,n1) ).
cnf(u32614,axiom,
~ p(n4,n9,n1) ).
cnf(u32618,axiom,
~ p(n5,n7,n1) ).
cnf(u32622,axiom,
~ p(n5,n8,n1) ).
cnf(u32626,axiom,
~ p(n5,n9,n1) ).
cnf(u32630,axiom,
~ p(n6,n7,n1) ).
cnf(u32634,axiom,
~ p(n6,n8,n1) ).
cnf(u32639,axiom,
p(n6,n9,n1) ).
cnf(u32643,axiom,
~ p(n4,n4,n9) ).
cnf(u32647,axiom,
~ p(n4,n5,n9) ).
cnf(u32651,axiom,
~ p(n4,n6,n9) ).
cnf(u32655,axiom,
~ p(n5,n4,n9) ).
cnf(u32659,axiom,
~ p(n5,n5,n9) ).
cnf(u32663,axiom,
~ p(n5,n6,n9) ).
cnf(u32667,axiom,
~ p(n6,n4,n9) ).
cnf(u32671,axiom,
~ p(n6,n5,n9) ).
cnf(u32676,axiom,
p(n6,n6,n9) ).
cnf(u32681,axiom,
p(n4,n4,n8) ).
cnf(u32684,axiom,
~ p(n4,n5,n8) ).
cnf(u32688,axiom,
~ p(n4,n6,n8) ).
cnf(u32692,axiom,
~ p(n5,n4,n8) ).
cnf(u32696,axiom,
~ p(n5,n5,n8) ).
cnf(u32700,axiom,
~ p(n5,n6,n8) ).
cnf(u32704,axiom,
~ p(n6,n4,n8) ).
cnf(u32708,axiom,
~ p(n6,n5,n8) ).
cnf(u32712,axiom,
~ p(n6,n6,n8) ).
cnf(u32717,axiom,
~ p(n4,n4,n7) ).
cnf(u32721,axiom,
~ p(n4,n5,n7) ).
cnf(u32725,axiom,
~ p(n4,n6,n7) ).
cnf(u32729,axiom,
~ p(n5,n4,n7) ).
cnf(u32734,axiom,
p(n5,n5,n7) ).
cnf(u32737,axiom,
~ p(n5,n6,n7) ).
cnf(u32741,axiom,
~ p(n6,n4,n7) ).
cnf(u32745,axiom,
~ p(n6,n5,n7) ).
cnf(u32749,axiom,
~ p(n6,n6,n7) ).
cnf(u32754,axiom,
~ p(n4,n4,n6) ).
cnf(u32758,axiom,
~ p(n4,n5,n6) ).
cnf(u32762,axiom,
~ p(n4,n6,n6) ).
cnf(u32766,axiom,
~ p(n5,n4,n6) ).
cnf(u32770,axiom,
~ p(n5,n5,n6) ).
cnf(u32774,axiom,
~ p(n5,n6,n6) ).
cnf(u32779,axiom,
p(n6,n4,n6) ).
cnf(u32782,axiom,
~ p(n6,n5,n6) ).
cnf(u32786,axiom,
~ p(n6,n6,n6) ).
cnf(u32791,axiom,
~ p(n4,n4,n5) ).
cnf(u32795,axiom,
~ p(n4,n5,n5) ).
cnf(u32799,axiom,
~ p(n4,n6,n5) ).
cnf(u32803,axiom,
~ p(n5,n4,n5) ).
cnf(u32807,axiom,
~ p(n5,n5,n5) ).
cnf(u32811,axiom,
~ p(n5,n6,n5) ).
cnf(u32815,axiom,
~ p(n6,n4,n5) ).
cnf(u32820,axiom,
p(n6,n5,n5) ).
cnf(u32823,axiom,
~ p(n6,n6,n5) ).
cnf(u32828,axiom,
~ p(n4,n4,n4) ).
cnf(u32832,axiom,
~ p(n4,n5,n4) ).
cnf(u32837,axiom,
p(n4,n6,n4) ).
cnf(u32840,axiom,
~ p(n5,n4,n4) ).
cnf(u32844,axiom,
~ p(n5,n5,n4) ).
cnf(u32848,axiom,
~ p(n5,n6,n4) ).
cnf(u32852,axiom,
~ p(n6,n4,n4) ).
cnf(u32856,axiom,
~ p(n6,n5,n4) ).
cnf(u32860,axiom,
~ p(n6,n6,n4) ).
cnf(u32865,axiom,
~ p(n4,n4,n3) ).
cnf(u32869,axiom,
~ p(n4,n5,n3) ).
cnf(u32873,axiom,
~ p(n4,n6,n3) ).
cnf(u32877,axiom,
~ p(n5,n4,n3) ).
cnf(u32881,axiom,
~ p(n5,n5,n3) ).
cnf(u32886,axiom,
p(n5,n6,n3) ).
cnf(u32889,axiom,
~ p(n6,n4,n3) ).
cnf(u32893,axiom,
~ p(n6,n5,n3) ).
cnf(u32897,axiom,
~ p(n6,n6,n3) ).
cnf(u32902,axiom,
~ p(n4,n4,n2) ).
cnf(u32907,axiom,
p(n4,n5,n2) ).
cnf(u32910,axiom,
~ p(n4,n6,n2) ).
cnf(u32914,axiom,
~ p(n5,n4,n2) ).
cnf(u32918,axiom,
~ p(n5,n5,n2) ).
cnf(u32922,axiom,
~ p(n5,n6,n2) ).
cnf(u32926,axiom,
~ p(n6,n4,n2) ).
cnf(u32930,axiom,
~ p(n6,n5,n2) ).
cnf(u32934,axiom,
~ p(n6,n6,n2) ).
cnf(u32939,axiom,
~ p(n4,n4,n1) ).
cnf(u32943,axiom,
~ p(n4,n5,n1) ).
cnf(u32947,axiom,
~ p(n4,n6,n1) ).
cnf(u32952,axiom,
p(n5,n4,n1) ).
cnf(u32955,axiom,
~ p(n5,n5,n1) ).
cnf(u32959,axiom,
~ p(n5,n6,n1) ).
cnf(u32963,axiom,
~ p(n6,n4,n1) ).
cnf(u32967,axiom,
~ p(n6,n5,n1) ).
cnf(u32971,axiom,
~ p(n6,n6,n1) ).
cnf(u32976,axiom,
~ p(n4,n1,n9) ).
cnf(u32981,axiom,
p(n4,n2,n9) ).
cnf(u32984,axiom,
~ p(n4,n3,n9) ).
cnf(u32988,axiom,
~ p(n5,n1,n9) ).
cnf(u32992,axiom,
~ p(n5,n2,n9) ).
cnf(u32996,axiom,
~ p(n5,n3,n9) ).
cnf(u33000,axiom,
~ p(n6,n1,n9) ).
cnf(u33004,axiom,
~ p(n6,n2,n9) ).
cnf(u33008,axiom,
~ p(n6,n3,n9) ).
cnf(u33013,axiom,
~ p(n4,n1,n8) ).
cnf(u33017,axiom,
~ p(n4,n2,n8) ).
cnf(u33021,axiom,
~ p(n4,n3,n8) ).
cnf(u33025,axiom,
~ p(n5,n1,n8) ).
cnf(u33029,axiom,
~ p(n5,n2,n8) ).
cnf(u33033,axiom,
~ p(n5,n3,n8) ).
cnf(u33037,axiom,
~ p(n6,n1,n8) ).
cnf(u33042,axiom,
p(n6,n2,n8) ).
cnf(u33045,axiom,
~ p(n6,n3,n8) ).
cnf(u33050,axiom,
~ p(n4,n1,n7) ).
cnf(u33054,axiom,
~ p(n4,n2,n7) ).
cnf(u33058,axiom,
~ p(n4,n3,n7) ).
cnf(u33062,axiom,
~ p(n5,n1,n7) ).
cnf(u33066,axiom,
~ p(n5,n2,n7) ).
cnf(u33070,axiom,
~ p(n5,n3,n7) ).
cnf(u33074,axiom,
~ p(n6,n1,n7) ).
cnf(u33078,axiom,
~ p(n6,n2,n7) ).
cnf(u33083,axiom,
p(n6,n3,n7) ).
cnf(u33087,axiom,
~ p(n4,n1,n6) ).
cnf(u33091,axiom,
~ p(n4,n2,n6) ).
cnf(u33095,axiom,
~ p(n4,n3,n6) ).
cnf(u33099,axiom,
~ p(n5,n1,n6) ).
cnf(u33104,axiom,
p(n5,n2,n6) ).
cnf(u33107,axiom,
~ p(n5,n3,n6) ).
cnf(u33111,axiom,
~ p(n6,n1,n6) ).
cnf(u33115,axiom,
~ p(n6,n2,n6) ).
cnf(u33119,axiom,
~ p(n6,n3,n6) ).
cnf(u33124,axiom,
~ p(n4,n1,n5) ).
cnf(u33128,axiom,
~ p(n4,n2,n5) ).
cnf(u33132,axiom,
~ p(n4,n3,n5) ).
cnf(u33137,axiom,
p(n5,n1,n5) ).
cnf(u33140,axiom,
~ p(n5,n2,n5) ).
cnf(u33144,axiom,
~ p(n5,n3,n5) ).
cnf(u33148,axiom,
~ p(n6,n1,n5) ).
cnf(u33152,axiom,
~ p(n6,n2,n5) ).
cnf(u33156,axiom,
~ p(n6,n3,n5) ).
cnf(u33161,axiom,
~ p(n4,n1,n4) ).
cnf(u33165,axiom,
~ p(n4,n2,n4) ).
cnf(u33169,axiom,
~ p(n4,n3,n4) ).
cnf(u33173,axiom,
~ p(n5,n1,n4) ).
cnf(u33177,axiom,
~ p(n5,n2,n4) ).
cnf(u33182,axiom,
p(n5,n3,n4) ).
cnf(u33185,axiom,
~ p(n6,n1,n4) ).
cnf(u33189,axiom,
~ p(n6,n2,n4) ).
cnf(u33193,axiom,
~ p(n6,n3,n4) ).
cnf(u33199,axiom,
p(n4,n1,n3) ).
cnf(u33202,axiom,
~ p(n4,n2,n3) ).
cnf(u33206,axiom,
~ p(n4,n3,n3) ).
cnf(u33210,axiom,
~ p(n5,n1,n3) ).
cnf(u33214,axiom,
~ p(n5,n2,n3) ).
cnf(u33218,axiom,
~ p(n5,n3,n3) ).
cnf(u33222,axiom,
~ p(n6,n1,n3) ).
cnf(u33226,axiom,
~ p(n6,n2,n3) ).
cnf(u33230,axiom,
~ p(n6,n3,n3) ).
cnf(u33235,axiom,
~ p(n4,n1,n2) ).
cnf(u33239,axiom,
~ p(n4,n2,n2) ).
cnf(u33243,axiom,
~ p(n4,n3,n2) ).
cnf(u33247,axiom,
~ p(n5,n1,n2) ).
cnf(u33251,axiom,
~ p(n5,n2,n2) ).
cnf(u33255,axiom,
~ p(n5,n3,n2) ).
cnf(u33260,axiom,
p(n6,n1,n2) ).
cnf(u33263,axiom,
~ p(n6,n2,n2) ).
cnf(u33267,axiom,
~ p(n6,n3,n2) ).
cnf(u33272,axiom,
~ p(n4,n1,n1) ).
cnf(u33276,axiom,
~ p(n4,n2,n1) ).
cnf(u33281,axiom,
p(n4,n3,n1) ).
cnf(u33284,axiom,
~ p(n5,n1,n1) ).
cnf(u33288,axiom,
~ p(n5,n2,n1) ).
cnf(u33292,axiom,
~ p(n5,n3,n1) ).
cnf(u33296,axiom,
~ p(n6,n1,n1) ).
cnf(u33300,axiom,
~ p(n6,n2,n1) ).
cnf(u33304,axiom,
~ p(n6,n3,n1) ).
cnf(u33309,axiom,
~ p(n1,n7,n9) ).
cnf(u33313,axiom,
~ p(n1,n8,n9) ).
cnf(u33317,axiom,
~ p(n1,n9,n9) ).
cnf(u33322,axiom,
p(n2,n7,n9) ).
cnf(u33325,axiom,
~ p(n2,n8,n9) ).
cnf(u33329,axiom,
~ p(n2,n9,n9) ).
cnf(u33333,axiom,
~ p(n3,n7,n9) ).
cnf(u33337,axiom,
~ p(n3,n8,n9) ).
cnf(u33341,axiom,
~ p(n3,n9,n9) ).
cnf(u33346,axiom,
~ p(n1,n7,n8) ).
cnf(u33350,axiom,
~ p(n1,n8,n8) ).
cnf(u33354,axiom,
~ p(n1,n9,n8) ).
cnf(u33358,axiom,
~ p(n2,n7,n8) ).
cnf(u33362,axiom,
~ p(n2,n8,n8) ).
cnf(u33366,axiom,
~ p(n2,n9,n8) ).
cnf(u33370,axiom,
~ p(n3,n7,n8) ).
cnf(u33375,axiom,
p(n3,n8,n8) ).
cnf(u33378,axiom,
~ p(n3,n9,n8) ).
cnf(u33384,axiom,
p(n1,n7,n7) ).
cnf(u33387,axiom,
~ p(n1,n8,n7) ).
cnf(u33391,axiom,
~ p(n1,n9,n7) ).
cnf(u33395,axiom,
~ p(n2,n7,n7) ).
cnf(u33399,axiom,
~ p(n2,n8,n7) ).
cnf(u33403,axiom,
~ p(n2,n9,n7) ).
cnf(u33407,axiom,
~ p(n3,n7,n7) ).
cnf(u33411,axiom,
~ p(n3,n8,n7) ).
cnf(u33415,axiom,
~ p(n3,n9,n7) ).
cnf(u33420,axiom,
~ p(n1,n7,n6) ).
cnf(u33424,axiom,
~ p(n1,n8,n6) ).
cnf(u33428,axiom,
~ p(n1,n9,n6) ).
cnf(u33432,axiom,
~ p(n2,n7,n6) ).
cnf(u33436,axiom,
~ p(n2,n8,n6) ).
cnf(u33440,axiom,
~ p(n2,n9,n6) ).
cnf(u33444,axiom,
~ p(n3,n7,n6) ).
cnf(u33448,axiom,
~ p(n3,n8,n6) ).
cnf(u33453,axiom,
p(n3,n9,n6) ).
cnf(u33457,axiom,
~ p(n1,n7,n5) ).
cnf(u33461,axiom,
~ p(n1,n8,n5) ).
cnf(u33465,axiom,
~ p(n1,n9,n5) ).
cnf(u33469,axiom,
~ p(n2,n7,n5) ).
cnf(u33474,axiom,
p(n2,n8,n5) ).
cnf(u33477,axiom,
~ p(n2,n9,n5) ).
cnf(u33481,axiom,
~ p(n3,n7,n5) ).
cnf(u33485,axiom,
~ p(n3,n8,n5) ).
cnf(u33489,axiom,
~ p(n3,n9,n5) ).
cnf(u33494,axiom,
~ p(n1,n7,n4) ).
cnf(u33498,axiom,
~ p(n1,n8,n4) ).
cnf(u33502,axiom,
~ p(n1,n9,n4) ).
cnf(u33506,axiom,
~ p(n2,n7,n4) ).
cnf(u33510,axiom,
~ p(n2,n8,n4) ).
cnf(u33514,axiom,
~ p(n2,n9,n4) ).
cnf(u33519,axiom,
p(n3,n7,n4) ).
cnf(u33522,axiom,
~ p(n3,n8,n4) ).
cnf(u33526,axiom,
~ p(n3,n9,n4) ).
cnf(u33531,axiom,
~ p(n1,n7,n3) ).
cnf(u33535,axiom,
~ p(n1,n8,n3) ).
cnf(u33539,axiom,
~ p(n1,n9,n3) ).
cnf(u33543,axiom,
~ p(n2,n7,n3) ).
cnf(u33547,axiom,
~ p(n2,n8,n3) ).
cnf(u33552,axiom,
p(n2,n9,n3) ).
cnf(u33555,axiom,
~ p(n3,n7,n3) ).
cnf(u33559,axiom,
~ p(n3,n8,n3) ).
cnf(u33563,axiom,
~ p(n3,n9,n3) ).
cnf(u33568,axiom,
~ p(n1,n7,n2) ).
cnf(u33572,axiom,
~ p(n1,n8,n2) ).
cnf(u33577,axiom,
p(n1,n9,n2) ).
cnf(u33580,axiom,
~ p(n2,n7,n2) ).
cnf(u33584,axiom,
~ p(n2,n8,n2) ).
cnf(u33588,axiom,
~ p(n2,n9,n2) ).
cnf(u33592,axiom,
~ p(n3,n7,n2) ).
cnf(u33596,axiom,
~ p(n3,n8,n2) ).
cnf(u33600,axiom,
~ p(n3,n9,n2) ).
cnf(u33605,axiom,
~ p(n1,n7,n1) ).
cnf(u33610,axiom,
p(n1,n8,n1) ).
cnf(u33613,axiom,
~ p(n1,n9,n1) ).
cnf(u33617,axiom,
~ p(n2,n7,n1) ).
cnf(u33621,axiom,
~ p(n2,n8,n1) ).
cnf(u33625,axiom,
~ p(n2,n9,n1) ).
cnf(u33629,axiom,
~ p(n3,n7,n1) ).
cnf(u33633,axiom,
~ p(n3,n8,n1) ).
cnf(u33637,axiom,
~ p(n3,n9,n1) ).
cnf(u33642,axiom,
~ p(n1,n4,n9) ).
cnf(u33646,axiom,
~ p(n1,n5,n9) ).
cnf(u33650,axiom,
~ p(n1,n6,n9) ).
cnf(u33654,axiom,
~ p(n2,n4,n9) ).
cnf(u33658,axiom,
~ p(n2,n5,n9) ).
cnf(u33662,axiom,
~ p(n2,n6,n9) ).
cnf(u33666,axiom,
~ p(n3,n4,n9) ).
cnf(u33671,axiom,
p(n3,n5,n9) ).
cnf(u33674,axiom,
~ p(n3,n6,n9) ).
cnf(u33679,axiom,
~ p(n1,n4,n8) ).
cnf(u33683,axiom,
~ p(n1,n5,n8) ).
cnf(u33687,axiom,
~ p(n1,n6,n8) ).
cnf(u33691,axiom,
~ p(n2,n4,n8) ).
cnf(u33696,axiom,
p(n2,n5,n8) ).
cnf(u33699,axiom,
~ p(n2,n6,n8) ).
cnf(u33703,axiom,
~ p(n3,n4,n8) ).
cnf(u33707,axiom,
~ p(n3,n5,n8) ).
cnf(u33711,axiom,
~ p(n3,n6,n8) ).
cnf(u33716,axiom,
~ p(n1,n4,n7) ).
cnf(u33720,axiom,
~ p(n1,n5,n7) ).
cnf(u33724,axiom,
~ p(n1,n6,n7) ).
cnf(u33729,axiom,
p(n2,n4,n7) ).
cnf(u33732,axiom,
~ p(n2,n5,n7) ).
cnf(u33736,axiom,
~ p(n2,n6,n7) ).
cnf(u33740,axiom,
~ p(n3,n4,n7) ).
cnf(u33744,axiom,
~ p(n3,n5,n7) ).
cnf(u33748,axiom,
~ p(n3,n6,n7) ).
cnf(u33753,axiom,
~ p(n1,n4,n6) ).
cnf(u33758,axiom,
p(n1,n5,n6) ).
cnf(u33761,axiom,
~ p(n1,n6,n6) ).
cnf(u33765,axiom,
~ p(n2,n4,n6) ).
cnf(u33769,axiom,
~ p(n2,n5,n6) ).
cnf(u33773,axiom,
~ p(n2,n6,n6) ).
cnf(u33777,axiom,
~ p(n3,n4,n6) ).
cnf(u33781,axiom,
~ p(n3,n5,n6) ).
cnf(u33785,axiom,
~ p(n3,n6,n6) ).
cnf(u33790,axiom,
~ p(n1,n4,n5) ).
cnf(u33794,axiom,
~ p(n1,n5,n5) ).
cnf(u33799,axiom,
p(n1,n6,n5) ).
cnf(u33802,axiom,
~ p(n2,n4,n5) ).
cnf(u33806,axiom,
~ p(n2,n5,n5) ).
cnf(u33810,axiom,
~ p(n2,n6,n5) ).
cnf(u33814,axiom,
~ p(n3,n4,n5) ).
cnf(u33818,axiom,
~ p(n3,n5,n5) ).
cnf(u33822,axiom,
~ p(n3,n6,n5) ).
cnf(u33828,axiom,
p(n1,n4,n4) ).
cnf(u33831,axiom,
~ p(n1,n5,n4) ).
cnf(u33835,axiom,
~ p(n1,n6,n4) ).
cnf(u33839,axiom,
~ p(n2,n4,n4) ).
cnf(u33843,axiom,
~ p(n2,n5,n4) ).
cnf(u33847,axiom,
~ p(n2,n6,n4) ).
cnf(u33851,axiom,
~ p(n3,n4,n4) ).
cnf(u33855,axiom,
~ p(n3,n5,n4) ).
cnf(u33859,axiom,
~ p(n3,n6,n4) ).
cnf(u33864,axiom,
~ p(n1,n4,n3) ).
cnf(u33868,axiom,
~ p(n1,n5,n3) ).
cnf(u33872,axiom,
~ p(n1,n6,n3) ).
cnf(u33876,axiom,
~ p(n2,n4,n3) ).
cnf(u33880,axiom,
~ p(n2,n5,n3) ).
cnf(u33884,axiom,
~ p(n2,n6,n3) ).
cnf(u33889,axiom,
p(n3,n4,n3) ).
cnf(u33892,axiom,
~ p(n3,n5,n3) ).
cnf(u33896,axiom,
~ p(n3,n6,n3) ).
cnf(u33901,axiom,
~ p(n1,n4,n2) ).
cnf(u33905,axiom,
~ p(n1,n5,n2) ).
cnf(u33909,axiom,
~ p(n1,n6,n2) ).
cnf(u33913,axiom,
~ p(n2,n4,n2) ).
cnf(u33917,axiom,
~ p(n2,n5,n2) ).
cnf(u33922,axiom,
p(n2,n6,n2) ).
cnf(u33925,axiom,
~ p(n3,n4,n2) ).
cnf(u33929,axiom,
~ p(n3,n5,n2) ).
cnf(u33933,axiom,
~ p(n3,n6,n2) ).
cnf(u33938,axiom,
~ p(n1,n4,n1) ).
cnf(u33942,axiom,
~ p(n1,n5,n1) ).
cnf(u33946,axiom,
~ p(n1,n6,n1) ).
cnf(u33950,axiom,
~ p(n2,n4,n1) ).
cnf(u33954,axiom,
~ p(n2,n5,n1) ).
cnf(u33958,axiom,
~ p(n2,n6,n1) ).
cnf(u33962,axiom,
~ p(n3,n4,n1) ).
cnf(u33966,axiom,
~ p(n3,n5,n1) ).
cnf(u33971,axiom,
p(n3,n6,n1) ).
cnf(u33975,axiom,
~ p(n1,n1,n9) ).
cnf(u33979,axiom,
~ p(n1,n2,n9) ).
cnf(u33984,axiom,
p(n1,n3,n9) ).
cnf(u33987,axiom,
~ p(n2,n1,n9) ).
cnf(u33991,axiom,
~ p(n2,n2,n9) ).
cnf(u33995,axiom,
~ p(n2,n3,n9) ).
cnf(u33999,axiom,
~ p(n3,n1,n9) ).
cnf(u34003,axiom,
~ p(n3,n2,n9) ).
cnf(u34007,axiom,
~ p(n3,n3,n9) ).
cnf(u34013,axiom,
p(n1,n1,n8) ).
cnf(u34016,axiom,
~ p(n1,n2,n8) ).
cnf(u34020,axiom,
~ p(n1,n3,n8) ).
cnf(u34024,axiom,
~ p(n2,n1,n8) ).
cnf(u34028,axiom,
~ p(n2,n2,n8) ).
cnf(u34032,axiom,
~ p(n2,n3,n8) ).
cnf(u34036,axiom,
~ p(n3,n1,n8) ).
cnf(u34040,axiom,
~ p(n3,n2,n8) ).
cnf(u34044,axiom,
~ p(n3,n3,n8) ).
cnf(u34049,axiom,
~ p(n1,n1,n7) ).
cnf(u34053,axiom,
~ p(n1,n2,n7) ).
cnf(u34057,axiom,
~ p(n1,n3,n7) ).
cnf(u34061,axiom,
~ p(n2,n1,n7) ).
cnf(u34065,axiom,
~ p(n2,n2,n7) ).
cnf(u34069,axiom,
~ p(n2,n3,n7) ).
cnf(u34074,axiom,
p(n3,n1,n7) ).
cnf(u34077,axiom,
~ p(n3,n2,n7) ).
cnf(u34081,axiom,
~ p(n3,n3,n7) ).
cnf(u34086,axiom,
~ p(n1,n1,n6) ).
cnf(u34090,axiom,
~ p(n1,n2,n6) ).
cnf(u34094,axiom,
~ p(n1,n3,n6) ).
cnf(u34098,axiom,
~ p(n2,n1,n6) ).
cnf(u34102,axiom,
~ p(n2,n2,n6) ).
cnf(u34107,axiom,
p(n2,n3,n6) ).
cnf(u34110,axiom,
~ p(n3,n1,n6) ).
cnf(u34114,axiom,
~ p(n3,n2,n6) ).
cnf(u34118,axiom,
~ p(n3,n3,n6) ).
cnf(u34123,axiom,
~ p(n1,n1,n5) ).
cnf(u34127,axiom,
~ p(n1,n2,n5) ).
cnf(u34131,axiom,
~ p(n1,n3,n5) ).
cnf(u34135,axiom,
~ p(n2,n1,n5) ).
cnf(u34139,axiom,
~ p(n2,n2,n5) ).
cnf(u34143,axiom,
~ p(n2,n3,n5) ).
cnf(u34147,axiom,
~ p(n3,n1,n5) ).
cnf(u34152,axiom,
p(n3,n2,n5) ).
cnf(u34155,axiom,
~ p(n3,n3,n5) ).
cnf(u34160,axiom,
~ p(n1,n1,n4) ).
cnf(u34164,axiom,
~ p(n1,n2,n4) ).
cnf(u34168,axiom,
~ p(n1,n3,n4) ).
cnf(u34172,axiom,
~ p(n2,n1,n4) ).
cnf(u34177,axiom,
p(n2,n2,n4) ).
cnf(u34180,axiom,
~ p(n2,n3,n4) ).
cnf(u34184,axiom,
~ p(n3,n1,n4) ).
cnf(u34188,axiom,
~ p(n3,n2,n4) ).
cnf(u34192,axiom,
~ p(n3,n3,n4) ).
cnf(u34197,axiom,
~ p(n1,n1,n3) ).
cnf(u34202,axiom,
p(n1,n2,n3) ).
cnf(u34205,axiom,
~ p(n1,n3,n3) ).
cnf(u34209,axiom,
~ p(n2,n1,n3) ).
cnf(u34213,axiom,
~ p(n2,n2,n3) ).
cnf(u34217,axiom,
~ p(n2,n3,n3) ).
cnf(u34221,axiom,
~ p(n3,n1,n3) ).
cnf(u34225,axiom,
~ p(n3,n2,n3) ).
cnf(u34229,axiom,
~ p(n3,n3,n3) ).
cnf(u34234,axiom,
~ p(n1,n1,n2) ).
cnf(u34238,axiom,
~ p(n1,n2,n2) ).
cnf(u34242,axiom,
~ p(n1,n3,n2) ).
cnf(u34246,axiom,
~ p(n2,n1,n2) ).
cnf(u34250,axiom,
~ p(n2,n2,n2) ).
cnf(u34254,axiom,
~ p(n2,n3,n2) ).
cnf(u34258,axiom,
~ p(n3,n1,n2) ).
cnf(u34262,axiom,
~ p(n3,n2,n2) ).
cnf(u34267,axiom,
p(n3,n3,n2) ).
cnf(u34271,axiom,
~ p(n1,n1,n1) ).
cnf(u34275,axiom,
~ p(n1,n2,n1) ).
cnf(u34279,axiom,
~ p(n1,n3,n1) ).
cnf(u34284,axiom,
p(n2,n1,n1) ).
cnf(u34287,axiom,
~ p(n2,n2,n1) ).
cnf(u34291,axiom,
~ p(n2,n3,n1) ).
cnf(u34295,axiom,
~ p(n3,n1,n1) ).
cnf(u34299,axiom,
~ p(n3,n2,n1) ).
cnf(u34303,axiom,
~ p(n3,n3,n1) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ138+2 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.39 % Computer : n016.cluster.edu
% 0.10/0.39 % Model : x86_64 x86_64
% 0.10/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.39 % Memory : 8046.5625MB
% 0.10/0.39 % OS : Linux 6.8.0-71-generic
% 0.10/0.39 % CPULimit : 300
% 0.10/0.39 % WCLimit : 300
% 0.10/0.39 % DateTime : Sun Sep 27 22:50:18 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.42 Running first-order model finding
% 0.10/0.42 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
% 0.68/0.85 % (3067266)Will run a generic schedule for satisfiability detection.
% 0.68/0.85 % (3067274)dis+10_1_sil=32000:sp=arity:random_seed=1223562859:i=103:fgj=on_2997 on theBenchmark for (2997ds/103Mi)
% 0.68/0.85 % (3067272)% WARNING: option uhcvi not known.
% 0.68/0.85 % (3067271)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=850314582_2997 on theBenchmark for (2997ds/0Mi)
% 0.68/0.85 % (3067272)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1223094630:i=135531:add=off:rawr=on_2997 on theBenchmark for (2997ds/135531Mi)
% 0.68/0.85 % (3067273)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3757537471:i=88024:add=on:rawr=on_2997 on theBenchmark for (2997ds/88024Mi)
% 0.68/0.85 % (3067275)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=772297377:i=116_2997 on theBenchmark for (2997ds/116Mi)
% 0.68/0.85 % (3067276)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=458764722:i=131_2997 on theBenchmark for (2997ds/131Mi)
% 0.68/0.85 % (3067277)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1978489972:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2997 on theBenchmark for (2997ds/159Mi)
% 0.68/0.85 % (3067274)Instruction limit reached!
% 0.68/0.85 % (3067274)------------------------------
% 0.68/0.85 % (3067274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.68/0.85 % (3067274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.68/0.85 % (3067274)CaDiCaL version: 2.1.3
% 0.68/0.85 % (3067274)Termination reason: Instruction limit
% 0.68/0.85 % (3067274)Termination phase: Property scanning
% 0.68/0.85 % (3067274)Time elapsed: 0.029 s
% 0.68/0.85 % (3067274)Peak memory usage: 22 MB
% 0.68/0.85 % (3067274)Instructions burned: 106 (million)
% 0.68/0.85 % (3067285)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1658056605:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 0.68/0.85 % (3067276)Instruction limit reached!
% 0.68/0.85 % (3067276)------------------------------
% 0.68/0.85 % (3067276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.68/0.85 % (3067276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.68/0.85 % (3067276)CaDiCaL version: 2.1.3
% 0.68/0.85 % (3067276)Termination reason: Instruction limit
% 0.68/0.85 % (3067276)Termination phase: Property scanning
% 0.68/0.85 % (3067276)Time elapsed: 0.063 s
% 0.68/0.85 % (3067276)Peak memory usage: 22 MB
% 0.68/0.85 % (3067276)Instructions burned: 131 (million)
% 0.68/0.85 % (3067275)Instruction limit reached!
% 0.68/0.85 % (3067275)------------------------------
% 0.68/0.85 % (3067275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.68/0.85 % (3067275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.68/0.85 % (3067275)CaDiCaL version: 2.1.3
% 0.68/0.85 % (3067275)Termination reason: Instruction limit
% 0.68/0.85 % (3067275)Termination phase: Property scanning
% 0.68/0.85 % (3067275)Time elapsed: 0.067 s
% 0.68/0.85 % (3067275)Peak memory usage: 24 MB
% 0.68/0.85 % (3067275)Instructions burned: 116 (million)
% 0.68/0.85 % (3067277)Instruction limit reached!
% 0.68/0.85 % (3067277)------------------------------
% 0.68/0.85 % (3067277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.68/0.85 % (3067277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.68/0.85 % (3067277)CaDiCaL version: 2.1.3
% 0.68/0.85 % (3067277)Termination reason: Instruction limit
% 0.68/0.85 % (3067277)Termination phase: Property scanning
% 0.68/0.85 % (3067277)Time elapsed: 0.073 s
% 0.68/0.85 % (3067277)Peak memory usage: 22 MB
% 0.68/0.85 % (3067277)Instructions burned: 159 (million)
% 0.68/0.85 % (3067287)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=825746934:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 0.68/0.85 % (3067288)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=607759719:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 0.68/0.85 % (3067289)ott-21_1_sil=16000:fs=off:random_seed=1085990436:i=180:av=off:fsr=off_2996 on theBenchmark for (2996ds/180Mi)
% 0.68/0.85 % (3067287)Instruction limit reached!
% 0.68/0.85 % (3067287)------------------------------
% 0.68/0.85 % (3067287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.68/0.85 % (3067287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.68/0.85 % (3067287)CaDiCaL version: 2.1.3
% 0.68/0.85 % (3067287)Termination reason: Instruction limit
% 0.68/0.85 % (3067287)Termination phase: Property scanning
% 0.68/0.85 % (3067287)Time elapsed: 0.061 s
% 0.68/0.85 % (3067287)Peak memory usage: 22 MB
% 0.68/0.85 % (3067287)Instructions burned: 132 (million)
% 0.68/0.85 % (3067293)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2027004966:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 0.68/0.85 % (3067272) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3067266-3067272"...
% 0.68/0.85 % (3067289)Instruction limit reached!
% 0.68/0.85 % (3067289)------------------------------
% 0.68/0.85 % (3067289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.68/0.85 % (3067289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.68/0.85 % (3067289)CaDiCaL version: 2.1.3
% 0.68/0.85 % (3067289)Termination reason: Instruction limit
% 0.68/0.85 % (3067289)Termination phase: Saturation
% 0.68/0.85 % (3067289)Time elapsed: 0.079 s
% 0.68/0.85 % (3067289)Peak memory usage: 23 MB
% 0.68/0.85 % (3067289)Instructions burned: 180 (million)
% 0.68/0.85 % (3067272)...printing done.
% 0.68/0.85 % SZS status Satisfiable for theBenchmark
% 0.68/0.85 % SZS output start Saturation.
% See solution above
% 0.68/0.87 % SZS output start Definitions and Model Updates.
% 0.68/0.87 % SZS output end Definitions and Model Updates.
% 0.68/0.87 % (3067272)------------------------------
% 0.68/0.87 % (3067272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.68/0.87 % (3067272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.68/0.87 % (3067272)CaDiCaL version: 2.1.3
% 0.68/0.87 % (3067272)Termination reason: Satisfiable
% 0.68/0.87 % (3067272)Time elapsed: 0.175 s
% 0.68/0.87 % (3067272)Peak memory usage: 34 MB
% 0.68/0.87 % (3067272)Instructions burned: 328 (million)
% 0.68/0.87 % (3067266)Success in time 0.424 s
% 0.68/0.87 % Vampire exiting
%------------------------------------------------------------------------------