%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PUZ068+2 : TPTP v9.3.1. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n017.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.70s 0.84s
% Output : Saturation 0.70s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u31303,axiom,
~ p(n7,n7,n9) ).
cnf(u31307,axiom,
~ p(n7,n8,n9) ).
cnf(u31311,axiom,
~ p(n7,n9,n9) ).
cnf(u31315,axiom,
~ p(n8,n7,n9) ).
cnf(u31320,axiom,
p(n8,n8,n9) ).
cnf(u31323,axiom,
~ p(n8,n9,n9) ).
cnf(u31327,axiom,
~ p(n9,n7,n9) ).
cnf(u31331,axiom,
~ p(n9,n8,n9) ).
cnf(u31335,axiom,
~ p(n9,n9,n9) ).
cnf(u31340,axiom,
~ p(n7,n7,n8) ).
cnf(u31344,axiom,
~ p(n7,n8,n8) ).
cnf(u31348,axiom,
~ p(n7,n9,n8) ).
cnf(u31352,axiom,
~ p(n8,n7,n8) ).
cnf(u31356,axiom,
~ p(n8,n8,n8) ).
cnf(u31360,axiom,
~ p(n8,n9,n8) ).
cnf(u31365,axiom,
p(n9,n7,n8) ).
cnf(u31368,axiom,
~ p(n9,n8,n8) ).
cnf(u31372,axiom,
~ p(n9,n9,n8) ).
cnf(u31377,axiom,
~ p(n7,n7,n7) ).
cnf(u31381,axiom,
~ p(n7,n8,n7) ).
cnf(u31385,axiom,
~ p(n7,n9,n7) ).
cnf(u31389,axiom,
~ p(n8,n7,n7) ).
cnf(u31393,axiom,
~ p(n8,n8,n7) ).
cnf(u31398,axiom,
p(n8,n9,n7) ).
cnf(u31401,axiom,
~ p(n9,n7,n7) ).
cnf(u31405,axiom,
~ p(n9,n8,n7) ).
cnf(u31409,axiom,
~ p(n9,n9,n7) ).
cnf(u31414,axiom,
~ p(n7,n7,n6) ).
cnf(u31418,axiom,
~ p(n7,n8,n6) ).
cnf(u31422,axiom,
~ p(n7,n9,n6) ).
cnf(u31427,axiom,
p(n8,n7,n6) ).
cnf(u31430,axiom,
~ p(n8,n8,n6) ).
cnf(u31434,axiom,
~ p(n8,n9,n6) ).
cnf(u31438,axiom,
~ p(n9,n7,n6) ).
cnf(u31442,axiom,
~ p(n9,n8,n6) ).
cnf(u31446,axiom,
~ p(n9,n9,n6) ).
cnf(u31451,axiom,
~ p(n7,n7,n5) ).
cnf(u31455,axiom,
~ p(n7,n8,n5) ).
cnf(u31460,axiom,
p(n7,n9,n5) ).
cnf(u31463,axiom,
~ p(n8,n7,n5) ).
cnf(u31467,axiom,
~ p(n8,n8,n5) ).
cnf(u31471,axiom,
~ p(n8,n9,n5) ).
cnf(u31475,axiom,
~ p(n9,n7,n5) ).
cnf(u31479,axiom,
~ p(n9,n8,n5) ).
cnf(u31483,axiom,
~ p(n9,n9,n5) ).
cnf(u31488,axiom,
~ p(n7,n7,n4) ).
cnf(u31492,axiom,
~ p(n7,n8,n4) ).
cnf(u31496,axiom,
~ p(n7,n9,n4) ).
cnf(u31500,axiom,
~ p(n8,n7,n4) ).
cnf(u31504,axiom,
~ p(n8,n8,n4) ).
cnf(u31508,axiom,
~ p(n8,n9,n4) ).
cnf(u31512,axiom,
~ p(n9,n7,n4) ).
cnf(u31516,axiom,
~ p(n9,n8,n4) ).
cnf(u31521,axiom,
p(n9,n9,n4) ).
cnf(u31525,axiom,
~ p(n7,n7,n3) ).
cnf(u31530,axiom,
p(n7,n8,n3) ).
cnf(u31533,axiom,
~ p(n7,n9,n3) ).
cnf(u31537,axiom,
~ p(n8,n7,n3) ).
cnf(u31541,axiom,
~ p(n8,n8,n3) ).
cnf(u31545,axiom,
~ p(n8,n9,n3) ).
cnf(u31549,axiom,
~ p(n9,n7,n3) ).
cnf(u31553,axiom,
~ p(n9,n8,n3) ).
cnf(u31557,axiom,
~ p(n9,n9,n3) ).
cnf(u31563,axiom,
p(n7,n7,n2) ).
cnf(u31566,axiom,
~ p(n7,n8,n2) ).
cnf(u31570,axiom,
~ p(n7,n9,n2) ).
cnf(u31574,axiom,
~ p(n8,n7,n2) ).
cnf(u31578,axiom,
~ p(n8,n8,n2) ).
cnf(u31582,axiom,
~ p(n8,n9,n2) ).
cnf(u31586,axiom,
~ p(n9,n7,n2) ).
cnf(u31590,axiom,
~ p(n9,n8,n2) ).
cnf(u31594,axiom,
~ p(n9,n9,n2) ).
cnf(u31599,axiom,
~ p(n7,n7,n1) ).
cnf(u31603,axiom,
~ p(n7,n8,n1) ).
cnf(u31607,axiom,
~ p(n7,n9,n1) ).
cnf(u31611,axiom,
~ p(n8,n7,n1) ).
cnf(u31615,axiom,
~ p(n8,n8,n1) ).
cnf(u31619,axiom,
~ p(n8,n9,n1) ).
cnf(u31623,axiom,
~ p(n9,n7,n1) ).
cnf(u31628,axiom,
p(n9,n8,n1) ).
cnf(u31631,axiom,
~ p(n9,n9,n1) ).
cnf(u31636,axiom,
~ p(n7,n4,n9) ).
cnf(u31640,axiom,
~ p(n7,n5,n9) ).
cnf(u31644,axiom,
~ p(n7,n6,n9) ).
cnf(u31648,axiom,
~ p(n8,n4,n9) ).
cnf(u31652,axiom,
~ p(n8,n5,n9) ).
cnf(u31656,axiom,
~ p(n8,n6,n9) ).
cnf(u31661,axiom,
p(n9,n4,n9) ).
cnf(u31664,axiom,
~ p(n9,n5,n9) ).
cnf(u31668,axiom,
~ p(n9,n6,n9) ).
cnf(u31673,axiom,
~ p(n7,n4,n8) ).
cnf(u31677,axiom,
~ p(n7,n5,n8) ).
cnf(u31681,axiom,
~ p(n7,n6,n8) ).
cnf(u31685,axiom,
~ p(n8,n4,n8) ).
cnf(u31690,axiom,
p(n8,n5,n8) ).
cnf(u31693,axiom,
~ p(n8,n6,n8) ).
cnf(u31697,axiom,
~ p(n9,n4,n8) ).
cnf(u31701,axiom,
~ p(n9,n5,n8) ).
cnf(u31705,axiom,
~ p(n9,n6,n8) ).
cnf(u31711,axiom,
p(n7,n4,n7) ).
cnf(u31714,axiom,
~ p(n7,n5,n7) ).
cnf(u31718,axiom,
~ p(n7,n6,n7) ).
cnf(u31722,axiom,
~ p(n8,n4,n7) ).
cnf(u31726,axiom,
~ p(n8,n5,n7) ).
cnf(u31730,axiom,
~ p(n8,n6,n7) ).
cnf(u31734,axiom,
~ p(n9,n4,n7) ).
cnf(u31738,axiom,
~ p(n9,n5,n7) ).
cnf(u31742,axiom,
~ p(n9,n6,n7) ).
cnf(u31747,axiom,
~ p(n7,n4,n6) ).
cnf(u31752,axiom,
p(n7,n5,n6) ).
cnf(u31755,axiom,
~ p(n7,n6,n6) ).
cnf(u31759,axiom,
~ p(n8,n4,n6) ).
cnf(u31763,axiom,
~ p(n8,n5,n6) ).
cnf(u31767,axiom,
~ p(n8,n6,n6) ).
cnf(u31771,axiom,
~ p(n9,n4,n6) ).
cnf(u31775,axiom,
~ p(n9,n5,n6) ).
cnf(u31779,axiom,
~ p(n9,n6,n6) ).
cnf(u31784,axiom,
~ p(n7,n4,n5) ).
cnf(u31788,axiom,
~ p(n7,n5,n5) ).
cnf(u31792,axiom,
~ p(n7,n6,n5) ).
cnf(u31796,axiom,
~ p(n8,n4,n5) ).
cnf(u31800,axiom,
~ p(n8,n5,n5) ).
cnf(u31804,axiom,
~ p(n8,n6,n5) ).
cnf(u31808,axiom,
~ p(n9,n4,n5) ).
cnf(u31813,axiom,
p(n9,n5,n5) ).
cnf(u31816,axiom,
~ p(n9,n6,n5) ).
cnf(u31821,axiom,
~ p(n7,n4,n4) ).
cnf(u31825,axiom,
~ p(n7,n5,n4) ).
cnf(u31829,axiom,
~ p(n7,n6,n4) ).
cnf(u31833,axiom,
~ p(n8,n4,n4) ).
cnf(u31837,axiom,
~ p(n8,n5,n4) ).
cnf(u31842,axiom,
p(n8,n6,n4) ).
cnf(u31845,axiom,
~ p(n9,n4,n4) ).
cnf(u31849,axiom,
~ p(n9,n5,n4) ).
cnf(u31853,axiom,
~ p(n9,n6,n4) ).
cnf(u31858,axiom,
~ p(n7,n4,n3) ).
cnf(u31862,axiom,
~ p(n7,n5,n3) ).
cnf(u31866,axiom,
~ p(n7,n6,n3) ).
cnf(u31871,axiom,
p(n8,n4,n3) ).
cnf(u31874,axiom,
~ p(n8,n5,n3) ).
cnf(u31878,axiom,
~ p(n8,n6,n3) ).
cnf(u31882,axiom,
~ p(n9,n4,n3) ).
cnf(u31886,axiom,
~ p(n9,n5,n3) ).
cnf(u31890,axiom,
~ p(n9,n6,n3) ).
cnf(u31895,axiom,
~ p(n7,n4,n2) ).
cnf(u31899,axiom,
~ p(n7,n5,n2) ).
cnf(u31903,axiom,
~ p(n7,n6,n2) ).
cnf(u31907,axiom,
~ p(n8,n4,n2) ).
cnf(u31911,axiom,
~ p(n8,n5,n2) ).
cnf(u31915,axiom,
~ p(n8,n6,n2) ).
cnf(u31919,axiom,
~ p(n9,n4,n2) ).
cnf(u31923,axiom,
~ p(n9,n5,n2) ).
cnf(u31928,axiom,
p(n9,n6,n2) ).
cnf(u31932,axiom,
~ p(n7,n4,n1) ).
cnf(u31936,axiom,
~ p(n7,n5,n1) ).
cnf(u31941,axiom,
p(n7,n6,n1) ).
cnf(u31944,axiom,
~ p(n8,n4,n1) ).
cnf(u31948,axiom,
~ p(n8,n5,n1) ).
cnf(u31952,axiom,
~ p(n8,n6,n1) ).
cnf(u31956,axiom,
~ p(n9,n4,n1) ).
cnf(u31960,axiom,
~ p(n9,n5,n1) ).
cnf(u31964,axiom,
~ p(n9,n6,n1) ).
cnf(u31970,axiom,
p(n7,n1,n9) ).
cnf(u31973,axiom,
~ p(n7,n2,n9) ).
cnf(u31977,axiom,
~ p(n7,n3,n9) ).
cnf(u31981,axiom,
~ p(n8,n1,n9) ).
cnf(u31985,axiom,
~ p(n8,n2,n9) ).
cnf(u31989,axiom,
~ p(n8,n3,n9) ).
cnf(u31993,axiom,
~ p(n9,n1,n9) ).
cnf(u31997,axiom,
~ p(n9,n2,n9) ).
cnf(u32001,axiom,
~ p(n9,n3,n9) ).
cnf(u32006,axiom,
~ p(n7,n1,n8) ).
cnf(u32010,axiom,
~ p(n7,n2,n8) ).
cnf(u32015,axiom,
p(n7,n3,n8) ).
cnf(u32018,axiom,
~ p(n8,n1,n8) ).
cnf(u32022,axiom,
~ p(n8,n2,n8) ).
cnf(u32026,axiom,
~ p(n8,n3,n8) ).
cnf(u32030,axiom,
~ p(n9,n1,n8) ).
cnf(u32034,axiom,
~ p(n9,n2,n8) ).
cnf(u32038,axiom,
~ p(n9,n3,n8) ).
cnf(u32043,axiom,
~ p(n7,n1,n7) ).
cnf(u32047,axiom,
~ p(n7,n2,n7) ).
cnf(u32051,axiom,
~ p(n7,n3,n7) ).
cnf(u32055,axiom,
~ p(n8,n1,n7) ).
cnf(u32059,axiom,
~ p(n8,n2,n7) ).
cnf(u32063,axiom,
~ p(n8,n3,n7) ).
cnf(u32067,axiom,
~ p(n9,n1,n7) ).
cnf(u32071,axiom,
~ p(n9,n2,n7) ).
cnf(u32076,axiom,
p(n9,n3,n7) ).
cnf(u32080,axiom,
~ p(n7,n1,n6) ).
cnf(u32084,axiom,
~ p(n7,n2,n6) ).
cnf(u32088,axiom,
~ p(n7,n3,n6) ).
cnf(u32092,axiom,
~ p(n8,n1,n6) ).
cnf(u32096,axiom,
~ p(n8,n2,n6) ).
cnf(u32100,axiom,
~ p(n8,n3,n6) ).
cnf(u32104,axiom,
~ p(n9,n1,n6) ).
cnf(u32109,axiom,
p(n9,n2,n6) ).
cnf(u32112,axiom,
~ p(n9,n3,n6) ).
cnf(u32117,axiom,
~ p(n7,n1,n5) ).
cnf(u32121,axiom,
~ p(n7,n2,n5) ).
cnf(u32125,axiom,
~ p(n7,n3,n5) ).
cnf(u32129,axiom,
~ p(n8,n1,n5) ).
cnf(u32133,axiom,
~ p(n8,n2,n5) ).
cnf(u32138,axiom,
p(n8,n3,n5) ).
cnf(u32141,axiom,
~ p(n9,n1,n5) ).
cnf(u32145,axiom,
~ p(n9,n2,n5) ).
cnf(u32149,axiom,
~ p(n9,n3,n5) ).
cnf(u32154,axiom,
~ p(n7,n1,n4) ).
cnf(u32159,axiom,
p(n7,n2,n4) ).
cnf(u32162,axiom,
~ p(n7,n3,n4) ).
cnf(u32166,axiom,
~ p(n8,n1,n4) ).
cnf(u32170,axiom,
~ p(n8,n2,n4) ).
cnf(u32174,axiom,
~ p(n8,n3,n4) ).
cnf(u32178,axiom,
~ p(n9,n1,n4) ).
cnf(u32182,axiom,
~ p(n9,n2,n4) ).
cnf(u32186,axiom,
~ p(n9,n3,n4) ).
cnf(u32191,axiom,
~ p(n7,n1,n3) ).
cnf(u32195,axiom,
~ p(n7,n2,n3) ).
cnf(u32199,axiom,
~ p(n7,n3,n3) ).
cnf(u32203,axiom,
~ p(n8,n1,n3) ).
cnf(u32207,axiom,
~ p(n8,n2,n3) ).
cnf(u32211,axiom,
~ p(n8,n3,n3) ).
cnf(u32216,axiom,
p(n9,n1,n3) ).
cnf(u32219,axiom,
~ p(n9,n2,n3) ).
cnf(u32223,axiom,
~ p(n9,n3,n3) ).
cnf(u32228,axiom,
~ p(n7,n1,n2) ).
cnf(u32232,axiom,
~ p(n7,n2,n2) ).
cnf(u32236,axiom,
~ p(n7,n3,n2) ).
cnf(u32240,axiom,
~ p(n8,n1,n2) ).
cnf(u32245,axiom,
p(n8,n2,n2) ).
cnf(u32248,axiom,
~ p(n8,n3,n2) ).
cnf(u32252,axiom,
~ p(n9,n1,n2) ).
cnf(u32256,axiom,
~ p(n9,n2,n2) ).
cnf(u32260,axiom,
~ p(n9,n3,n2) ).
cnf(u32265,axiom,
~ p(n7,n1,n1) ).
cnf(u32269,axiom,
~ p(n7,n2,n1) ).
cnf(u32273,axiom,
~ p(n7,n3,n1) ).
cnf(u32278,axiom,
p(n8,n1,n1) ).
cnf(u32281,axiom,
~ p(n8,n2,n1) ).
cnf(u32285,axiom,
~ p(n8,n3,n1) ).
cnf(u32289,axiom,
~ p(n9,n1,n1) ).
cnf(u32293,axiom,
~ p(n9,n2,n1) ).
cnf(u32297,axiom,
~ p(n9,n3,n1) ).
cnf(u32302,axiom,
~ p(n4,n7,n9) ).
cnf(u32306,axiom,
~ p(n4,n8,n9) ).
cnf(u32310,axiom,
~ p(n4,n9,n9) ).
cnf(u32315,axiom,
p(n5,n7,n9) ).
cnf(u32318,axiom,
~ p(n5,n8,n9) ).
cnf(u32322,axiom,
~ p(n5,n9,n9) ).
cnf(u32326,axiom,
~ p(n6,n7,n9) ).
cnf(u32330,axiom,
~ p(n6,n8,n9) ).
cnf(u32334,axiom,
~ p(n6,n9,n9) ).
cnf(u32339,axiom,
~ p(n4,n7,n8) ).
cnf(u32343,axiom,
~ p(n4,n8,n8) ).
cnf(u32347,axiom,
~ p(n4,n9,n8) ).
cnf(u32351,axiom,
~ p(n5,n7,n8) ).
cnf(u32356,axiom,
p(n5,n8,n8) ).
cnf(u32359,axiom,
~ p(n5,n9,n8) ).
cnf(u32363,axiom,
~ p(n6,n7,n8) ).
cnf(u32367,axiom,
~ p(n6,n8,n8) ).
cnf(u32371,axiom,
~ p(n6,n9,n8) ).
cnf(u32377,axiom,
p(n4,n7,n7) ).
cnf(u32380,axiom,
~ p(n4,n8,n7) ).
cnf(u32384,axiom,
~ p(n4,n9,n7) ).
cnf(u32388,axiom,
~ p(n5,n7,n7) ).
cnf(u32392,axiom,
~ p(n5,n8,n7) ).
cnf(u32396,axiom,
~ p(n5,n9,n7) ).
cnf(u32400,axiom,
~ p(n6,n7,n7) ).
cnf(u32404,axiom,
~ p(n6,n8,n7) ).
cnf(u32408,axiom,
~ p(n6,n9,n7) ).
cnf(u32413,axiom,
~ p(n4,n7,n6) ).
cnf(u32417,axiom,
~ p(n4,n8,n6) ).
cnf(u32421,axiom,
~ p(n4,n9,n6) ).
cnf(u32425,axiom,
~ p(n5,n7,n6) ).
cnf(u32429,axiom,
~ p(n5,n8,n6) ).
cnf(u32433,axiom,
~ p(n5,n9,n6) ).
cnf(u32437,axiom,
~ p(n6,n7,n6) ).
cnf(u32441,axiom,
~ p(n6,n8,n6) ).
cnf(u32446,axiom,
p(n6,n9,n6) ).
cnf(u32450,axiom,
~ p(n4,n7,n5) ).
cnf(u32454,axiom,
~ p(n4,n8,n5) ).
cnf(u32458,axiom,
~ p(n4,n9,n5) ).
cnf(u32462,axiom,
~ p(n5,n7,n5) ).
cnf(u32466,axiom,
~ p(n5,n8,n5) ).
cnf(u32470,axiom,
~ p(n5,n9,n5) ).
cnf(u32474,axiom,
~ p(n6,n7,n5) ).
cnf(u32479,axiom,
p(n6,n8,n5) ).
cnf(u32482,axiom,
~ p(n6,n9,n5) ).
cnf(u32487,axiom,
~ p(n4,n7,n4) ).
cnf(u32492,axiom,
p(n4,n8,n4) ).
cnf(u32495,axiom,
~ p(n4,n9,n4) ).
cnf(u32499,axiom,
~ p(n5,n7,n4) ).
cnf(u32503,axiom,
~ p(n5,n8,n4) ).
cnf(u32507,axiom,
~ p(n5,n9,n4) ).
cnf(u32511,axiom,
~ p(n6,n7,n4) ).
cnf(u32515,axiom,
~ p(n6,n8,n4) ).
cnf(u32519,axiom,
~ p(n6,n9,n4) ).
cnf(u32524,axiom,
~ p(n4,n7,n3) ).
cnf(u32528,axiom,
~ p(n4,n8,n3) ).
cnf(u32532,axiom,
~ p(n4,n9,n3) ).
cnf(u32536,axiom,
~ p(n5,n7,n3) ).
cnf(u32540,axiom,
~ p(n5,n8,n3) ).
cnf(u32544,axiom,
~ p(n5,n9,n3) ).
cnf(u32549,axiom,
p(n6,n7,n3) ).
cnf(u32552,axiom,
~ p(n6,n8,n3) ).
cnf(u32556,axiom,
~ p(n6,n9,n3) ).
cnf(u32561,axiom,
~ p(n4,n7,n2) ).
cnf(u32565,axiom,
~ p(n4,n8,n2) ).
cnf(u32570,axiom,
p(n4,n9,n2) ).
cnf(u32573,axiom,
~ p(n5,n7,n2) ).
cnf(u32577,axiom,
~ p(n5,n8,n2) ).
cnf(u32581,axiom,
~ p(n5,n9,n2) ).
cnf(u32585,axiom,
~ p(n6,n7,n2) ).
cnf(u32589,axiom,
~ p(n6,n8,n2) ).
cnf(u32593,axiom,
~ p(n6,n9,n2) ).
cnf(u32598,axiom,
~ p(n4,n7,n1) ).
cnf(u32602,axiom,
~ p(n4,n8,n1) ).
cnf(u32606,axiom,
~ p(n4,n9,n1) ).
cnf(u32610,axiom,
~ p(n5,n7,n1) ).
cnf(u32614,axiom,
~ p(n5,n8,n1) ).
cnf(u32619,axiom,
p(n5,n9,n1) ).
cnf(u32622,axiom,
~ p(n6,n7,n1) ).
cnf(u32626,axiom,
~ p(n6,n8,n1) ).
cnf(u32630,axiom,
~ p(n6,n9,n1) ).
cnf(u32635,axiom,
~ p(n4,n4,n9) ).
cnf(u32639,axiom,
~ p(n4,n5,n9) ).
cnf(u32644,axiom,
p(n4,n6,n9) ).
cnf(u32647,axiom,
~ p(n5,n4,n9) ).
cnf(u32651,axiom,
~ p(n5,n5,n9) ).
cnf(u32655,axiom,
~ p(n5,n6,n9) ).
cnf(u32659,axiom,
~ p(n6,n4,n9) ).
cnf(u32663,axiom,
~ p(n6,n5,n9) ).
cnf(u32667,axiom,
~ p(n6,n6,n9) ).
cnf(u32672,axiom,
~ p(n4,n4,n8) ).
cnf(u32676,axiom,
~ p(n4,n5,n8) ).
cnf(u32680,axiom,
~ p(n4,n6,n8) ).
cnf(u32684,axiom,
~ p(n5,n4,n8) ).
cnf(u32688,axiom,
~ p(n5,n5,n8) ).
cnf(u32692,axiom,
~ p(n5,n6,n8) ).
cnf(u32697,axiom,
p(n6,n4,n8) ).
cnf(u32700,axiom,
~ p(n6,n5,n8) ).
cnf(u32704,axiom,
~ p(n6,n6,n8) ).
cnf(u32709,axiom,
~ p(n4,n4,n7) ).
cnf(u32713,axiom,
~ p(n4,n5,n7) ).
cnf(u32717,axiom,
~ p(n4,n6,n7) ).
cnf(u32721,axiom,
~ p(n5,n4,n7) ).
cnf(u32725,axiom,
~ p(n5,n5,n7) ).
cnf(u32729,axiom,
~ p(n5,n6,n7) ).
cnf(u32733,axiom,
~ p(n6,n4,n7) ).
cnf(u32737,axiom,
~ p(n6,n5,n7) ).
cnf(u32742,axiom,
p(n6,n6,n7) ).
cnf(u32746,axiom,
~ p(n4,n4,n6) ).
cnf(u32750,axiom,
~ p(n4,n5,n6) ).
cnf(u32754,axiom,
~ p(n4,n6,n6) ).
cnf(u32759,axiom,
p(n5,n4,n6) ).
cnf(u32762,axiom,
~ p(n5,n5,n6) ).
cnf(u32766,axiom,
~ p(n5,n6,n6) ).
cnf(u32770,axiom,
~ p(n6,n4,n6) ).
cnf(u32774,axiom,
~ p(n6,n5,n6) ).
cnf(u32778,axiom,
~ p(n6,n6,n6) ).
cnf(u32784,axiom,
p(n4,n4,n5) ).
cnf(u32787,axiom,
~ p(n4,n5,n5) ).
cnf(u32791,axiom,
~ p(n4,n6,n5) ).
cnf(u32795,axiom,
~ p(n5,n4,n5) ).
cnf(u32799,axiom,
~ p(n5,n5,n5) ).
cnf(u32803,axiom,
~ p(n5,n6,n5) ).
cnf(u32807,axiom,
~ p(n6,n4,n5) ).
cnf(u32811,axiom,
~ p(n6,n5,n5) ).
cnf(u32815,axiom,
~ p(n6,n6,n5) ).
cnf(u32820,axiom,
~ p(n4,n4,n4) ).
cnf(u32824,axiom,
~ p(n4,n5,n4) ).
cnf(u32828,axiom,
~ p(n4,n6,n4) ).
cnf(u32832,axiom,
~ p(n5,n4,n4) ).
cnf(u32836,axiom,
~ p(n5,n5,n4) ).
cnf(u32840,axiom,
~ p(n5,n6,n4) ).
cnf(u32844,axiom,
~ p(n6,n4,n4) ).
cnf(u32849,axiom,
p(n6,n5,n4) ).
cnf(u32852,axiom,
~ p(n6,n6,n4) ).
cnf(u32857,axiom,
~ p(n4,n4,n3) ).
cnf(u32861,axiom,
~ p(n4,n5,n3) ).
cnf(u32865,axiom,
~ p(n4,n6,n3) ).
cnf(u32869,axiom,
~ p(n5,n4,n3) ).
cnf(u32873,axiom,
~ p(n5,n5,n3) ).
cnf(u32878,axiom,
p(n5,n6,n3) ).
cnf(u32881,axiom,
~ p(n6,n4,n3) ).
cnf(u32885,axiom,
~ p(n6,n5,n3) ).
cnf(u32889,axiom,
~ p(n6,n6,n3) ).
cnf(u32894,axiom,
~ p(n4,n4,n2) ).
cnf(u32898,axiom,
~ p(n4,n5,n2) ).
cnf(u32902,axiom,
~ p(n4,n6,n2) ).
cnf(u32906,axiom,
~ p(n5,n4,n2) ).
cnf(u32911,axiom,
p(n5,n5,n2) ).
cnf(u32914,axiom,
~ p(n5,n6,n2) ).
cnf(u32918,axiom,
~ p(n6,n4,n2) ).
cnf(u32922,axiom,
~ p(n6,n5,n2) ).
cnf(u32926,axiom,
~ p(n6,n6,n2) ).
cnf(u32931,axiom,
~ p(n4,n4,n1) ).
cnf(u32936,axiom,
p(n4,n5,n1) ).
cnf(u32939,axiom,
~ p(n4,n6,n1) ).
cnf(u32943,axiom,
~ p(n5,n4,n1) ).
cnf(u32947,axiom,
~ p(n5,n5,n1) ).
cnf(u32951,axiom,
~ p(n5,n6,n1) ).
cnf(u32955,axiom,
~ p(n6,n4,n1) ).
cnf(u32959,axiom,
~ p(n6,n5,n1) ).
cnf(u32963,axiom,
~ p(n6,n6,n1) ).
cnf(u32968,axiom,
~ p(n4,n1,n9) ).
cnf(u32972,axiom,
~ p(n4,n2,n9) ).
cnf(u32976,axiom,
~ p(n4,n3,n9) ).
cnf(u32980,axiom,
~ p(n5,n1,n9) ).
cnf(u32984,axiom,
~ p(n5,n2,n9) ).
cnf(u32988,axiom,
~ p(n5,n3,n9) ).
cnf(u32992,axiom,
~ p(n6,n1,n9) ).
cnf(u32996,axiom,
~ p(n6,n2,n9) ).
cnf(u33001,axiom,
p(n6,n3,n9) ).
cnf(u33005,axiom,
~ p(n4,n1,n8) ).
cnf(u33010,axiom,
p(n4,n2,n8) ).
cnf(u33013,axiom,
~ p(n4,n3,n8) ).
cnf(u33017,axiom,
~ p(n5,n1,n8) ).
cnf(u33021,axiom,
~ p(n5,n2,n8) ).
cnf(u33025,axiom,
~ p(n5,n3,n8) ).
cnf(u33029,axiom,
~ p(n6,n1,n8) ).
cnf(u33033,axiom,
~ p(n6,n2,n8) ).
cnf(u33037,axiom,
~ p(n6,n3,n8) ).
cnf(u33042,axiom,
~ p(n4,n1,n7) ).
cnf(u33046,axiom,
~ p(n4,n2,n7) ).
cnf(u33050,axiom,
~ p(n4,n3,n7) ).
cnf(u33054,axiom,
~ p(n5,n1,n7) ).
cnf(u33059,axiom,
p(n5,n2,n7) ).
cnf(u33062,axiom,
~ p(n5,n3,n7) ).
cnf(u33066,axiom,
~ p(n6,n1,n7) ).
cnf(u33070,axiom,
~ p(n6,n2,n7) ).
cnf(u33074,axiom,
~ p(n6,n3,n7) ).
cnf(u33080,axiom,
p(n4,n1,n6) ).
cnf(u33083,axiom,
~ p(n4,n2,n6) ).
cnf(u33087,axiom,
~ p(n4,n3,n6) ).
cnf(u33091,axiom,
~ p(n5,n1,n6) ).
cnf(u33095,axiom,
~ p(n5,n2,n6) ).
cnf(u33099,axiom,
~ p(n5,n3,n6) ).
cnf(u33103,axiom,
~ p(n6,n1,n6) ).
cnf(u33107,axiom,
~ p(n6,n2,n6) ).
cnf(u33111,axiom,
~ p(n6,n3,n6) ).
cnf(u33116,axiom,
~ p(n4,n1,n5) ).
cnf(u33120,axiom,
~ p(n4,n2,n5) ).
cnf(u33124,axiom,
~ p(n4,n3,n5) ).
cnf(u33129,axiom,
p(n5,n1,n5) ).
cnf(u33132,axiom,
~ p(n5,n2,n5) ).
cnf(u33136,axiom,
~ p(n5,n3,n5) ).
cnf(u33140,axiom,
~ p(n6,n1,n5) ).
cnf(u33144,axiom,
~ p(n6,n2,n5) ).
cnf(u33148,axiom,
~ p(n6,n3,n5) ).
cnf(u33153,axiom,
~ p(n4,n1,n4) ).
cnf(u33157,axiom,
~ p(n4,n2,n4) ).
cnf(u33161,axiom,
~ p(n4,n3,n4) ).
cnf(u33165,axiom,
~ p(n5,n1,n4) ).
cnf(u33169,axiom,
~ p(n5,n2,n4) ).
cnf(u33174,axiom,
p(n5,n3,n4) ).
cnf(u33177,axiom,
~ p(n6,n1,n4) ).
cnf(u33181,axiom,
~ p(n6,n2,n4) ).
cnf(u33185,axiom,
~ p(n6,n3,n4) ).
cnf(u33190,axiom,
~ p(n4,n1,n3) ).
cnf(u33194,axiom,
~ p(n4,n2,n3) ).
cnf(u33199,axiom,
p(n4,n3,n3) ).
cnf(u33202,axiom,
~ p(n5,n1,n3) ).
cnf(u33206,axiom,
~ p(n5,n2,n3) ).
cnf(u33210,axiom,
~ p(n5,n3,n3) ).
cnf(u33214,axiom,
~ p(n6,n1,n3) ).
cnf(u33218,axiom,
~ p(n6,n2,n3) ).
cnf(u33222,axiom,
~ p(n6,n3,n3) ).
cnf(u33227,axiom,
~ p(n4,n1,n2) ).
cnf(u33231,axiom,
~ p(n4,n2,n2) ).
cnf(u33235,axiom,
~ p(n4,n3,n2) ).
cnf(u33239,axiom,
~ p(n5,n1,n2) ).
cnf(u33243,axiom,
~ p(n5,n2,n2) ).
cnf(u33247,axiom,
~ p(n5,n3,n2) ).
cnf(u33252,axiom,
p(n6,n1,n2) ).
cnf(u33255,axiom,
~ p(n6,n2,n2) ).
cnf(u33259,axiom,
~ p(n6,n3,n2) ).
cnf(u33264,axiom,
~ p(n4,n1,n1) ).
cnf(u33268,axiom,
~ p(n4,n2,n1) ).
cnf(u33272,axiom,
~ p(n4,n3,n1) ).
cnf(u33276,axiom,
~ p(n5,n1,n1) ).
cnf(u33280,axiom,
~ p(n5,n2,n1) ).
cnf(u33284,axiom,
~ p(n5,n3,n1) ).
cnf(u33288,axiom,
~ p(n6,n1,n1) ).
cnf(u33293,axiom,
p(n6,n2,n1) ).
cnf(u33296,axiom,
~ p(n6,n3,n1) ).
cnf(u33301,axiom,
~ p(n1,n7,n9) ).
cnf(u33305,axiom,
~ p(n1,n8,n9) ).
cnf(u33309,axiom,
~ p(n1,n9,n9) ).
cnf(u33313,axiom,
~ p(n2,n7,n9) ).
cnf(u33317,axiom,
~ p(n2,n8,n9) ).
cnf(u33322,axiom,
p(n2,n9,n9) ).
cnf(u33325,axiom,
~ p(n3,n7,n9) ).
cnf(u33329,axiom,
~ p(n3,n8,n9) ).
cnf(u33333,axiom,
~ p(n3,n9,n9) ).
cnf(u33338,axiom,
~ p(n1,n7,n8) ).
cnf(u33342,axiom,
~ p(n1,n8,n8) ).
cnf(u33346,axiom,
~ p(n1,n9,n8) ).
cnf(u33350,axiom,
~ p(n2,n7,n8) ).
cnf(u33354,axiom,
~ p(n2,n8,n8) ).
cnf(u33358,axiom,
~ p(n2,n9,n8) ).
cnf(u33362,axiom,
~ p(n3,n7,n8) ).
cnf(u33366,axiom,
~ p(n3,n8,n8) ).
cnf(u33371,axiom,
p(n3,n9,n8) ).
cnf(u33375,axiom,
~ p(n1,n7,n7) ).
cnf(u33379,axiom,
~ p(n1,n8,n7) ).
cnf(u33383,axiom,
~ p(n1,n9,n7) ).
cnf(u33387,axiom,
~ p(n2,n7,n7) ).
cnf(u33391,axiom,
~ p(n2,n8,n7) ).
cnf(u33395,axiom,
~ p(n2,n9,n7) ).
cnf(u33399,axiom,
~ p(n3,n7,n7) ).
cnf(u33404,axiom,
p(n3,n8,n7) ).
cnf(u33407,axiom,
~ p(n3,n9,n7) ).
cnf(u33412,axiom,
~ p(n1,n7,n6) ).
cnf(u33416,axiom,
~ p(n1,n8,n6) ).
cnf(u33420,axiom,
~ p(n1,n9,n6) ).
cnf(u33424,axiom,
~ p(n2,n7,n6) ).
cnf(u33429,axiom,
p(n2,n8,n6) ).
cnf(u33432,axiom,
~ p(n2,n9,n6) ).
cnf(u33436,axiom,
~ p(n3,n7,n6) ).
cnf(u33440,axiom,
~ p(n3,n8,n6) ).
cnf(u33444,axiom,
~ p(n3,n9,n6) ).
cnf(u33449,axiom,
~ p(n1,n7,n5) ).
cnf(u33453,axiom,
~ p(n1,n8,n5) ).
cnf(u33457,axiom,
~ p(n1,n9,n5) ).
cnf(u33461,axiom,
~ p(n2,n7,n5) ).
cnf(u33465,axiom,
~ p(n2,n8,n5) ).
cnf(u33469,axiom,
~ p(n2,n9,n5) ).
cnf(u33474,axiom,
p(n3,n7,n5) ).
cnf(u33477,axiom,
~ p(n3,n8,n5) ).
cnf(u33481,axiom,
~ p(n3,n9,n5) ).
cnf(u33486,axiom,
~ p(n1,n7,n4) ).
cnf(u33490,axiom,
~ p(n1,n8,n4) ).
cnf(u33494,axiom,
~ p(n1,n9,n4) ).
cnf(u33499,axiom,
p(n2,n7,n4) ).
cnf(u33502,axiom,
~ p(n2,n8,n4) ).
cnf(u33506,axiom,
~ p(n2,n9,n4) ).
cnf(u33510,axiom,
~ p(n3,n7,n4) ).
cnf(u33514,axiom,
~ p(n3,n8,n4) ).
cnf(u33518,axiom,
~ p(n3,n9,n4) ).
cnf(u33523,axiom,
~ p(n1,n7,n3) ).
cnf(u33527,axiom,
~ p(n1,n8,n3) ).
cnf(u33532,axiom,
p(n1,n9,n3) ).
cnf(u33535,axiom,
~ p(n2,n7,n3) ).
cnf(u33539,axiom,
~ p(n2,n8,n3) ).
cnf(u33543,axiom,
~ p(n2,n9,n3) ).
cnf(u33547,axiom,
~ p(n3,n7,n3) ).
cnf(u33551,axiom,
~ p(n3,n8,n3) ).
cnf(u33555,axiom,
~ p(n3,n9,n3) ).
cnf(u33560,axiom,
~ p(n1,n7,n2) ).
cnf(u33565,axiom,
p(n1,n8,n2) ).
cnf(u33568,axiom,
~ p(n1,n9,n2) ).
cnf(u33572,axiom,
~ p(n2,n7,n2) ).
cnf(u33576,axiom,
~ p(n2,n8,n2) ).
cnf(u33580,axiom,
~ p(n2,n9,n2) ).
cnf(u33584,axiom,
~ p(n3,n7,n2) ).
cnf(u33588,axiom,
~ p(n3,n8,n2) ).
cnf(u33592,axiom,
~ p(n3,n9,n2) ).
cnf(u33598,axiom,
p(n1,n7,n1) ).
cnf(u33601,axiom,
~ p(n1,n8,n1) ).
cnf(u33605,axiom,
~ p(n1,n9,n1) ).
cnf(u33609,axiom,
~ p(n2,n7,n1) ).
cnf(u33613,axiom,
~ p(n2,n8,n1) ).
cnf(u33617,axiom,
~ p(n2,n9,n1) ).
cnf(u33621,axiom,
~ p(n3,n7,n1) ).
cnf(u33625,axiom,
~ p(n3,n8,n1) ).
cnf(u33629,axiom,
~ p(n3,n9,n1) ).
cnf(u33634,axiom,
~ p(n1,n4,n9) ).
cnf(u33638,axiom,
~ p(n1,n5,n9) ).
cnf(u33642,axiom,
~ p(n1,n6,n9) ).
cnf(u33646,axiom,
~ p(n2,n4,n9) ).
cnf(u33650,axiom,
~ p(n2,n5,n9) ).
cnf(u33654,axiom,
~ p(n2,n6,n9) ).
cnf(u33658,axiom,
~ p(n3,n4,n9) ).
cnf(u33663,axiom,
p(n3,n5,n9) ).
cnf(u33666,axiom,
~ p(n3,n6,n9) ).
cnf(u33671,axiom,
~ p(n1,n4,n8) ).
cnf(u33675,axiom,
~ p(n1,n5,n8) ).
cnf(u33679,axiom,
~ p(n1,n6,n8) ).
cnf(u33683,axiom,
~ p(n2,n4,n8) ).
cnf(u33687,axiom,
~ p(n2,n5,n8) ).
cnf(u33692,axiom,
p(n2,n6,n8) ).
cnf(u33695,axiom,
~ p(n3,n4,n8) ).
cnf(u33699,axiom,
~ p(n3,n5,n8) ).
cnf(u33703,axiom,
~ p(n3,n6,n8) ).
cnf(u33708,axiom,
~ p(n1,n4,n7) ).
cnf(u33713,axiom,
p(n1,n5,n7) ).
cnf(u33716,axiom,
~ p(n1,n6,n7) ).
cnf(u33720,axiom,
~ p(n2,n4,n7) ).
cnf(u33724,axiom,
~ p(n2,n5,n7) ).
cnf(u33728,axiom,
~ p(n2,n6,n7) ).
cnf(u33732,axiom,
~ p(n3,n4,n7) ).
cnf(u33736,axiom,
~ p(n3,n5,n7) ).
cnf(u33740,axiom,
~ p(n3,n6,n7) ).
cnf(u33745,axiom,
~ p(n1,n4,n6) ).
cnf(u33749,axiom,
~ p(n1,n5,n6) ).
cnf(u33753,axiom,
~ p(n1,n6,n6) ).
cnf(u33757,axiom,
~ p(n2,n4,n6) ).
cnf(u33761,axiom,
~ p(n2,n5,n6) ).
cnf(u33765,axiom,
~ p(n2,n6,n6) ).
cnf(u33769,axiom,
~ p(n3,n4,n6) ).
cnf(u33773,axiom,
~ p(n3,n5,n6) ).
cnf(u33778,axiom,
p(n3,n6,n6) ).
cnf(u33782,axiom,
~ p(n1,n4,n5) ).
cnf(u33786,axiom,
~ p(n1,n5,n5) ).
cnf(u33791,axiom,
p(n1,n6,n5) ).
cnf(u33794,axiom,
~ p(n2,n4,n5) ).
cnf(u33798,axiom,
~ p(n2,n5,n5) ).
cnf(u33802,axiom,
~ p(n2,n6,n5) ).
cnf(u33806,axiom,
~ p(n3,n4,n5) ).
cnf(u33810,axiom,
~ p(n3,n5,n5) ).
cnf(u33814,axiom,
~ p(n3,n6,n5) ).
cnf(u33820,axiom,
p(n1,n4,n4) ).
cnf(u33823,axiom,
~ p(n1,n5,n4) ).
cnf(u33827,axiom,
~ p(n1,n6,n4) ).
cnf(u33831,axiom,
~ p(n2,n4,n4) ).
cnf(u33835,axiom,
~ p(n2,n5,n4) ).
cnf(u33839,axiom,
~ p(n2,n6,n4) ).
cnf(u33843,axiom,
~ p(n3,n4,n4) ).
cnf(u33847,axiom,
~ p(n3,n5,n4) ).
cnf(u33851,axiom,
~ p(n3,n6,n4) ).
cnf(u33856,axiom,
~ p(n1,n4,n3) ).
cnf(u33860,axiom,
~ p(n1,n5,n3) ).
cnf(u33864,axiom,
~ p(n1,n6,n3) ).
cnf(u33868,axiom,
~ p(n2,n4,n3) ).
cnf(u33873,axiom,
p(n2,n5,n3) ).
cnf(u33876,axiom,
~ p(n2,n6,n3) ).
cnf(u33880,axiom,
~ p(n3,n4,n3) ).
cnf(u33884,axiom,
~ p(n3,n5,n3) ).
cnf(u33888,axiom,
~ p(n3,n6,n3) ).
cnf(u33893,axiom,
~ p(n1,n4,n2) ).
cnf(u33897,axiom,
~ p(n1,n5,n2) ).
cnf(u33901,axiom,
~ p(n1,n6,n2) ).
cnf(u33906,axiom,
p(n2,n4,n2) ).
cnf(u33909,axiom,
~ p(n2,n5,n2) ).
cnf(u33913,axiom,
~ p(n2,n6,n2) ).
cnf(u33917,axiom,
~ p(n3,n4,n2) ).
cnf(u33921,axiom,
~ p(n3,n5,n2) ).
cnf(u33925,axiom,
~ p(n3,n6,n2) ).
cnf(u33930,axiom,
~ p(n1,n4,n1) ).
cnf(u33934,axiom,
~ p(n1,n5,n1) ).
cnf(u33938,axiom,
~ p(n1,n6,n1) ).
cnf(u33942,axiom,
~ p(n2,n4,n1) ).
cnf(u33946,axiom,
~ p(n2,n5,n1) ).
cnf(u33950,axiom,
~ p(n2,n6,n1) ).
cnf(u33955,axiom,
p(n3,n4,n1) ).
cnf(u33958,axiom,
~ p(n3,n5,n1) ).
cnf(u33962,axiom,
~ p(n3,n6,n1) ).
cnf(u33967,axiom,
~ p(n1,n1,n9) ).
cnf(u33972,axiom,
p(n1,n2,n9) ).
cnf(u33975,axiom,
~ p(n1,n3,n9) ).
cnf(u33979,axiom,
~ p(n2,n1,n9) ).
cnf(u33983,axiom,
~ p(n2,n2,n9) ).
cnf(u33987,axiom,
~ p(n2,n3,n9) ).
cnf(u33991,axiom,
~ p(n3,n1,n9) ).
cnf(u33995,axiom,
~ p(n3,n2,n9) ).
cnf(u33999,axiom,
~ p(n3,n3,n9) ).
cnf(u34005,axiom,
p(n1,n1,n8) ).
cnf(u34008,axiom,
~ p(n1,n2,n8) ).
cnf(u34012,axiom,
~ p(n1,n3,n8) ).
cnf(u34016,axiom,
~ p(n2,n1,n8) ).
cnf(u34020,axiom,
~ p(n2,n2,n8) ).
cnf(u34024,axiom,
~ p(n2,n3,n8) ).
cnf(u34028,axiom,
~ p(n3,n1,n8) ).
cnf(u34032,axiom,
~ p(n3,n2,n8) ).
cnf(u34036,axiom,
~ p(n3,n3,n8) ).
cnf(u34041,axiom,
~ p(n1,n1,n7) ).
cnf(u34045,axiom,
~ p(n1,n2,n7) ).
cnf(u34049,axiom,
~ p(n1,n3,n7) ).
cnf(u34054,axiom,
p(n2,n1,n7) ).
cnf(u34057,axiom,
~ p(n2,n2,n7) ).
cnf(u34061,axiom,
~ p(n2,n3,n7) ).
cnf(u34065,axiom,
~ p(n3,n1,n7) ).
cnf(u34069,axiom,
~ p(n3,n2,n7) ).
cnf(u34073,axiom,
~ p(n3,n3,n7) ).
cnf(u34078,axiom,
~ p(n1,n1,n6) ).
cnf(u34082,axiom,
~ p(n1,n2,n6) ).
cnf(u34087,axiom,
p(n1,n3,n6) ).
cnf(u34090,axiom,
~ p(n2,n1,n6) ).
cnf(u34094,axiom,
~ p(n2,n2,n6) ).
cnf(u34098,axiom,
~ p(n2,n3,n6) ).
cnf(u34102,axiom,
~ p(n3,n1,n6) ).
cnf(u34106,axiom,
~ p(n3,n2,n6) ).
cnf(u34110,axiom,
~ p(n3,n3,n6) ).
cnf(u34115,axiom,
~ p(n1,n1,n5) ).
cnf(u34119,axiom,
~ p(n1,n2,n5) ).
cnf(u34123,axiom,
~ p(n1,n3,n5) ).
cnf(u34127,axiom,
~ p(n2,n1,n5) ).
cnf(u34132,axiom,
p(n2,n2,n5) ).
cnf(u34135,axiom,
~ p(n2,n3,n5) ).
cnf(u34139,axiom,
~ p(n3,n1,n5) ).
cnf(u34143,axiom,
~ p(n3,n2,n5) ).
cnf(u34147,axiom,
~ p(n3,n3,n5) ).
cnf(u34152,axiom,
~ p(n1,n1,n4) ).
cnf(u34156,axiom,
~ p(n1,n2,n4) ).
cnf(u34160,axiom,
~ p(n1,n3,n4) ).
cnf(u34164,axiom,
~ p(n2,n1,n4) ).
cnf(u34168,axiom,
~ p(n2,n2,n4) ).
cnf(u34172,axiom,
~ p(n2,n3,n4) ).
cnf(u34177,axiom,
p(n3,n1,n4) ).
cnf(u34180,axiom,
~ p(n3,n2,n4) ).
cnf(u34184,axiom,
~ p(n3,n3,n4) ).
cnf(u34189,axiom,
~ p(n1,n1,n3) ).
cnf(u34193,axiom,
~ p(n1,n2,n3) ).
cnf(u34197,axiom,
~ p(n1,n3,n3) ).
cnf(u34201,axiom,
~ p(n2,n1,n3) ).
cnf(u34205,axiom,
~ p(n2,n2,n3) ).
cnf(u34209,axiom,
~ p(n2,n3,n3) ).
cnf(u34213,axiom,
~ p(n3,n1,n3) ).
cnf(u34218,axiom,
p(n3,n2,n3) ).
cnf(u34221,axiom,
~ p(n3,n3,n3) ).
cnf(u34226,axiom,
~ p(n1,n1,n2) ).
cnf(u34230,axiom,
~ p(n1,n2,n2) ).
cnf(u34234,axiom,
~ p(n1,n3,n2) ).
cnf(u34238,axiom,
~ p(n2,n1,n2) ).
cnf(u34242,axiom,
~ p(n2,n2,n2) ).
cnf(u34246,axiom,
~ p(n2,n3,n2) ).
cnf(u34250,axiom,
~ p(n3,n1,n2) ).
cnf(u34254,axiom,
~ p(n3,n2,n2) ).
cnf(u34259,axiom,
p(n3,n3,n2) ).
cnf(u34263,axiom,
~ p(n1,n1,n1) ).
cnf(u34267,axiom,
~ p(n1,n2,n1) ).
cnf(u34271,axiom,
~ p(n1,n3,n1) ).
cnf(u34275,axiom,
~ p(n2,n1,n1) ).
cnf(u34279,axiom,
~ p(n2,n2,n1) ).
cnf(u34284,axiom,
p(n2,n3,n1) ).
cnf(u34287,axiom,
~ p(n3,n1,n1) ).
cnf(u34291,axiom,
~ p(n3,n2,n1) ).
cnf(u34295,axiom,
~ p(n3,n3,n1) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ068+2 : TPTP v9.3.1. Bugfixed v5.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.37 % Computer : n017.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 22:34:21 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.41 Running first-order model finding
% 0.10/0.41 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.70/0.84 % (3005926)Will run a generic schedule for satisfiability detection.
% 0.70/0.84 % (3005931)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3909735131_2997 on theBenchmark for (2997ds/0Mi)
% 0.70/0.84 % (3005932)% WARNING: option uhcvi not known.
% 0.70/0.84 % (3005932)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3218691271:i=135531:add=off:rawr=on_2997 on theBenchmark for (2997ds/135531Mi)
% 0.70/0.84 % (3005933)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3331142551:i=88024:add=on:rawr=on_2997 on theBenchmark for (2997ds/88024Mi)
% 0.70/0.84 % (3005934)dis+10_1_sil=32000:sp=arity:random_seed=1669712400:i=103:fgj=on_2997 on theBenchmark for (2997ds/103Mi)
% 0.70/0.84 % (3005935)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1520108936:i=116_2997 on theBenchmark for (2997ds/116Mi)
% 0.70/0.84 % (3005936)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4230543699:i=131_2997 on theBenchmark for (2997ds/131Mi)
% 0.70/0.84 % (3005937)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1589400790:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2997 on theBenchmark for (2997ds/159Mi)
% 0.70/0.84 % (3005934)Instruction limit reached!
% 0.70/0.84 % (3005934)------------------------------
% 0.70/0.84 % (3005934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.70/0.84 % (3005934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.70/0.84 % (3005934)CaDiCaL version: 2.1.3
% 0.70/0.84 % (3005934)Termination reason: Instruction limit
% 0.70/0.84 % (3005934)Termination phase: Property scanning
% 0.70/0.84 % (3005934)Time elapsed: 0.052 s
% 0.70/0.84 % (3005934)Peak memory usage: 22 MB
% 0.70/0.84 % (3005934)Instructions burned: 105 (million)
% 0.70/0.84 % (3005936)Instruction limit reached!
% 0.70/0.84 % (3005936)------------------------------
% 0.70/0.84 % (3005936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.70/0.84 % (3005936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.70/0.84 % (3005936)CaDiCaL version: 2.1.3
% 0.70/0.84 % (3005936)Termination reason: Instruction limit
% 0.70/0.84 % (3005936)Termination phase: Property scanning
% 0.70/0.84 % (3005936)Time elapsed: 0.063 s
% 0.70/0.84 % (3005936)Peak memory usage: 22 MB
% 0.70/0.84 % (3005936)Instructions burned: 133 (million)
% 0.70/0.84 % (3005935)Instruction limit reached!
% 0.70/0.84 % (3005935)------------------------------
% 0.70/0.84 % (3005935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.70/0.84 % (3005935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.70/0.84 % (3005935)CaDiCaL version: 2.1.3
% 0.70/0.84 % (3005935)Termination reason: Instruction limit
% 0.70/0.84 % (3005935)Termination phase: Property scanning
% 0.70/0.84 % (3005935)Time elapsed: 0.068 s
% 0.70/0.84 % (3005935)Peak memory usage: 24 MB
% 0.70/0.84 % (3005935)Instructions burned: 118 (million)
% 0.70/0.84 % (3005937)Instruction limit reached!
% 0.70/0.84 % (3005937)------------------------------
% 0.70/0.84 % (3005937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.70/0.84 % (3005937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.70/0.84 % (3005937)CaDiCaL version: 2.1.3
% 0.70/0.84 % (3005937)Termination reason: Instruction limit
% 0.70/0.84 % (3005937)Termination phase: Property scanning
% 0.70/0.84 % (3005937)Time elapsed: 0.073 s
% 0.70/0.84 % (3005937)Peak memory usage: 22 MB
% 0.70/0.84 % (3005937)Instructions burned: 161 (million)
% 0.70/0.84 % (3005945)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=545425943:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 0.70/0.84 % (3005946)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=521842371:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 0.70/0.84 % (3005947)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=1355809737:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2996 on theBenchmark for (2996ds/684Mi)
% 0.70/0.84 % (3005949)ott-21_1_sil=16000:fs=off:random_seed=3672728035:i=180:av=off:fsr=off_2996 on theBenchmark for (2996ds/180Mi)
% 0.70/0.84 % (3005946)Instruction limit reached!
% 0.70/0.84 % (3005946)------------------------------
% 0.70/0.84 % (3005946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.70/0.84 % (3005946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.70/0.84 % (3005946)CaDiCaL version: 2.1.3
% 0.70/0.84 % (3005946)Termination reason: Instruction limit
% 0.70/0.84 % (3005946)Termination phase: Property scanning
% 0.70/0.84 % (3005946)Time elapsed: 0.061 s
% 0.70/0.84 % (3005946)Peak memory usage: 22 MB
% 0.70/0.84 % (3005946)Instructions burned: 132 (million)
% 0.70/0.84 % (3005953)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1756468393:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 0.70/0.84 % (3005932) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3005926-3005932"...
% 0.70/0.84 % (3005949)Instruction limit reached!
% 0.70/0.84 % (3005949)------------------------------
% 0.70/0.84 % (3005949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.70/0.84 % (3005949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.70/0.84 % (3005949)CaDiCaL version: 2.1.3
% 0.70/0.84 % (3005949)Termination reason: Instruction limit
% 0.70/0.84 % (3005949)Termination phase: Saturation
% 0.70/0.84 % (3005949)Time elapsed: 0.080 s
% 0.70/0.84 % (3005949)Peak memory usage: 23 MB
% 0.70/0.84 % (3005949)Instructions burned: 181 (million)
% 0.70/0.84 % (3005932)...printing done.
% 0.70/0.84 % SZS status Satisfiable for theBenchmark
% 0.70/0.84 % SZS output start Saturation.
% See solution above
% 0.70/0.86 % SZS output start Definitions and Model Updates.
% 0.70/0.86 % SZS output end Definitions and Model Updates.
% 0.70/0.86 % (3005932)------------------------------
% 0.70/0.86 % (3005932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.70/0.86 % (3005932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.70/0.86 % (3005932)CaDiCaL version: 2.1.3
% 0.70/0.86 % (3005932)Termination reason: Satisfiable
% 0.70/0.86 % (3005932)Time elapsed: 0.173 s
% 0.70/0.86 % (3005932)Peak memory usage: 34 MB
% 0.70/0.86 % (3005932)Instructions burned: 324 (million)
% 0.70/0.86 % (3005926)Success in time 0.425 s
% 0.70/0.86 % Vampire exiting
%------------------------------------------------------------------------------