%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PUZ079+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:14 PM UTC 2026
% Result : Satisfiable 0.55s 0.76s
% Output : Saturation 0.55s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u31325,axiom,
~ p(n7,n7,n9) ).
cnf(u31330,axiom,
p(n7,n8,n9) ).
cnf(u31333,axiom,
~ p(n7,n9,n9) ).
cnf(u31337,axiom,
~ p(n8,n7,n9) ).
cnf(u31341,axiom,
~ p(n8,n8,n9) ).
cnf(u31345,axiom,
~ p(n8,n9,n9) ).
cnf(u31349,axiom,
~ p(n9,n7,n9) ).
cnf(u31353,axiom,
~ p(n9,n8,n9) ).
cnf(u31357,axiom,
~ p(n9,n9,n9) ).
cnf(u31362,axiom,
~ p(n7,n7,n8) ).
cnf(u31366,axiom,
~ p(n7,n8,n8) ).
cnf(u31370,axiom,
~ p(n7,n9,n8) ).
cnf(u31374,axiom,
~ p(n8,n7,n8) ).
cnf(u31378,axiom,
~ p(n8,n8,n8) ).
cnf(u31382,axiom,
~ p(n8,n9,n8) ).
cnf(u31386,axiom,
~ p(n9,n7,n8) ).
cnf(u31391,axiom,
p(n9,n8,n8) ).
cnf(u31394,axiom,
~ p(n9,n9,n8) ).
cnf(u31399,axiom,
~ p(n7,n7,n7) ).
cnf(u31403,axiom,
~ p(n7,n8,n7) ).
cnf(u31407,axiom,
~ p(n7,n9,n7) ).
cnf(u31411,axiom,
~ p(n8,n7,n7) ).
cnf(u31416,axiom,
p(n8,n8,n7) ).
cnf(u31419,axiom,
~ p(n8,n9,n7) ).
cnf(u31423,axiom,
~ p(n9,n7,n7) ).
cnf(u31427,axiom,
~ p(n9,n8,n7) ).
cnf(u31431,axiom,
~ p(n9,n9,n7) ).
cnf(u31436,axiom,
~ p(n7,n7,n6) ).
cnf(u31440,axiom,
~ p(n7,n8,n6) ).
cnf(u31444,axiom,
~ p(n7,n9,n6) ).
cnf(u31449,axiom,
p(n8,n7,n6) ).
cnf(u31452,axiom,
~ p(n8,n8,n6) ).
cnf(u31456,axiom,
~ p(n8,n9,n6) ).
cnf(u31460,axiom,
~ p(n9,n7,n6) ).
cnf(u31464,axiom,
~ p(n9,n8,n6) ).
cnf(u31468,axiom,
~ p(n9,n9,n6) ).
cnf(u31473,axiom,
~ p(n7,n7,n5) ).
cnf(u31477,axiom,
~ p(n7,n8,n5) ).
cnf(u31481,axiom,
~ p(n7,n9,n5) ).
cnf(u31485,axiom,
~ p(n8,n7,n5) ).
cnf(u31489,axiom,
~ p(n8,n8,n5) ).
cnf(u31494,axiom,
p(n8,n9,n5) ).
cnf(u31497,axiom,
~ p(n9,n7,n5) ).
cnf(u31501,axiom,
~ p(n9,n8,n5) ).
cnf(u31505,axiom,
~ p(n9,n9,n5) ).
cnf(u31510,axiom,
~ p(n7,n7,n4) ).
cnf(u31514,axiom,
~ p(n7,n8,n4) ).
cnf(u31518,axiom,
~ p(n7,n9,n4) ).
cnf(u31522,axiom,
~ p(n8,n7,n4) ).
cnf(u31526,axiom,
~ p(n8,n8,n4) ).
cnf(u31530,axiom,
~ p(n8,n9,n4) ).
cnf(u31534,axiom,
~ p(n9,n7,n4) ).
cnf(u31538,axiom,
~ p(n9,n8,n4) ).
cnf(u31543,axiom,
p(n9,n9,n4) ).
cnf(u31547,axiom,
~ p(n7,n7,n3) ).
cnf(u31551,axiom,
~ p(n7,n8,n3) ).
cnf(u31555,axiom,
~ p(n7,n9,n3) ).
cnf(u31559,axiom,
~ p(n8,n7,n3) ).
cnf(u31563,axiom,
~ p(n8,n8,n3) ).
cnf(u31567,axiom,
~ p(n8,n9,n3) ).
cnf(u31572,axiom,
p(n9,n7,n3) ).
cnf(u31575,axiom,
~ p(n9,n8,n3) ).
cnf(u31579,axiom,
~ p(n9,n9,n3) ).
cnf(u31585,axiom,
p(n7,n7,n2) ).
cnf(u31588,axiom,
~ p(n7,n8,n2) ).
cnf(u31592,axiom,
~ p(n7,n9,n2) ).
cnf(u31596,axiom,
~ p(n8,n7,n2) ).
cnf(u31600,axiom,
~ p(n8,n8,n2) ).
cnf(u31604,axiom,
~ p(n8,n9,n2) ).
cnf(u31608,axiom,
~ p(n9,n7,n2) ).
cnf(u31612,axiom,
~ p(n9,n8,n2) ).
cnf(u31616,axiom,
~ p(n9,n9,n2) ).
cnf(u31621,axiom,
~ p(n7,n7,n1) ).
cnf(u31625,axiom,
~ p(n7,n8,n1) ).
cnf(u31630,axiom,
p(n7,n9,n1) ).
cnf(u31633,axiom,
~ p(n8,n7,n1) ).
cnf(u31637,axiom,
~ p(n8,n8,n1) ).
cnf(u31641,axiom,
~ p(n8,n9,n1) ).
cnf(u31645,axiom,
~ p(n9,n7,n1) ).
cnf(u31649,axiom,
~ p(n9,n8,n1) ).
cnf(u31653,axiom,
~ p(n9,n9,n1) ).
cnf(u31658,axiom,
~ p(n7,n4,n9) ).
cnf(u31662,axiom,
~ p(n7,n5,n9) ).
cnf(u31666,axiom,
~ p(n7,n6,n9) ).
cnf(u31671,axiom,
p(n8,n4,n9) ).
cnf(u31674,axiom,
~ p(n8,n5,n9) ).
cnf(u31678,axiom,
~ p(n8,n6,n9) ).
cnf(u31682,axiom,
~ p(n9,n4,n9) ).
cnf(u31686,axiom,
~ p(n9,n5,n9) ).
cnf(u31690,axiom,
~ p(n9,n6,n9) ).
cnf(u31695,axiom,
~ p(n7,n4,n8) ).
cnf(u31699,axiom,
~ p(n7,n5,n8) ).
cnf(u31704,axiom,
p(n7,n6,n8) ).
cnf(u31707,axiom,
~ p(n8,n4,n8) ).
cnf(u31711,axiom,
~ p(n8,n5,n8) ).
cnf(u31715,axiom,
~ p(n8,n6,n8) ).
cnf(u31719,axiom,
~ p(n9,n4,n8) ).
cnf(u31723,axiom,
~ p(n9,n5,n8) ).
cnf(u31727,axiom,
~ p(n9,n6,n8) ).
cnf(u31732,axiom,
~ p(n7,n4,n7) ).
cnf(u31736,axiom,
~ p(n7,n5,n7) ).
cnf(u31740,axiom,
~ p(n7,n6,n7) ).
cnf(u31744,axiom,
~ p(n8,n4,n7) ).
cnf(u31748,axiom,
~ p(n8,n5,n7) ).
cnf(u31752,axiom,
~ p(n8,n6,n7) ).
cnf(u31756,axiom,
~ p(n9,n4,n7) ).
cnf(u31761,axiom,
p(n9,n5,n7) ).
cnf(u31764,axiom,
~ p(n9,n6,n7) ).
cnf(u31769,axiom,
~ p(n7,n4,n6) ).
cnf(u31773,axiom,
~ p(n7,n5,n6) ).
cnf(u31777,axiom,
~ p(n7,n6,n6) ).
cnf(u31781,axiom,
~ p(n8,n4,n6) ).
cnf(u31785,axiom,
~ p(n8,n5,n6) ).
cnf(u31789,axiom,
~ p(n8,n6,n6) ).
cnf(u31793,axiom,
~ p(n9,n4,n6) ).
cnf(u31797,axiom,
~ p(n9,n5,n6) ).
cnf(u31802,axiom,
p(n9,n6,n6) ).
cnf(u31806,axiom,
~ p(n7,n4,n5) ).
cnf(u31811,axiom,
p(n7,n5,n5) ).
cnf(u31814,axiom,
~ p(n7,n6,n5) ).
cnf(u31818,axiom,
~ p(n8,n4,n5) ).
cnf(u31822,axiom,
~ p(n8,n5,n5) ).
cnf(u31826,axiom,
~ p(n8,n6,n5) ).
cnf(u31830,axiom,
~ p(n9,n4,n5) ).
cnf(u31834,axiom,
~ p(n9,n5,n5) ).
cnf(u31838,axiom,
~ p(n9,n6,n5) ).
cnf(u31844,axiom,
p(n7,n4,n4) ).
cnf(u31847,axiom,
~ p(n7,n5,n4) ).
cnf(u31851,axiom,
~ p(n7,n6,n4) ).
cnf(u31855,axiom,
~ p(n8,n4,n4) ).
cnf(u31859,axiom,
~ p(n8,n5,n4) ).
cnf(u31863,axiom,
~ p(n8,n6,n4) ).
cnf(u31867,axiom,
~ p(n9,n4,n4) ).
cnf(u31871,axiom,
~ p(n9,n5,n4) ).
cnf(u31875,axiom,
~ p(n9,n6,n4) ).
cnf(u31880,axiom,
~ p(n7,n4,n3) ).
cnf(u31884,axiom,
~ p(n7,n5,n3) ).
cnf(u31888,axiom,
~ p(n7,n6,n3) ).
cnf(u31892,axiom,
~ p(n8,n4,n3) ).
cnf(u31896,axiom,
~ p(n8,n5,n3) ).
cnf(u31901,axiom,
p(n8,n6,n3) ).
cnf(u31904,axiom,
~ p(n9,n4,n3) ).
cnf(u31908,axiom,
~ p(n9,n5,n3) ).
cnf(u31912,axiom,
~ p(n9,n6,n3) ).
cnf(u31917,axiom,
~ p(n7,n4,n2) ).
cnf(u31921,axiom,
~ p(n7,n5,n2) ).
cnf(u31925,axiom,
~ p(n7,n6,n2) ).
cnf(u31929,axiom,
~ p(n8,n4,n2) ).
cnf(u31934,axiom,
p(n8,n5,n2) ).
cnf(u31937,axiom,
~ p(n8,n6,n2) ).
cnf(u31941,axiom,
~ p(n9,n4,n2) ).
cnf(u31945,axiom,
~ p(n9,n5,n2) ).
cnf(u31949,axiom,
~ p(n9,n6,n2) ).
cnf(u31954,axiom,
~ p(n7,n4,n1) ).
cnf(u31958,axiom,
~ p(n7,n5,n1) ).
cnf(u31962,axiom,
~ p(n7,n6,n1) ).
cnf(u31966,axiom,
~ p(n8,n4,n1) ).
cnf(u31970,axiom,
~ p(n8,n5,n1) ).
cnf(u31974,axiom,
~ p(n8,n6,n1) ).
cnf(u31979,axiom,
p(n9,n4,n1) ).
cnf(u31982,axiom,
~ p(n9,n5,n1) ).
cnf(u31986,axiom,
~ p(n9,n6,n1) ).
cnf(u31991,axiom,
~ p(n7,n1,n9) ).
cnf(u31995,axiom,
~ p(n7,n2,n9) ).
cnf(u31999,axiom,
~ p(n7,n3,n9) ).
cnf(u32003,axiom,
~ p(n8,n1,n9) ).
cnf(u32007,axiom,
~ p(n8,n2,n9) ).
cnf(u32011,axiom,
~ p(n8,n3,n9) ).
cnf(u32015,axiom,
~ p(n9,n1,n9) ).
cnf(u32019,axiom,
~ p(n9,n2,n9) ).
cnf(u32024,axiom,
p(n9,n3,n9) ).
cnf(u32028,axiom,
~ p(n7,n1,n8) ).
cnf(u32032,axiom,
~ p(n7,n2,n8) ).
cnf(u32036,axiom,
~ p(n7,n3,n8) ).
cnf(u32041,axiom,
p(n8,n1,n8) ).
cnf(u32044,axiom,
~ p(n8,n2,n8) ).
cnf(u32048,axiom,
~ p(n8,n3,n8) ).
cnf(u32052,axiom,
~ p(n9,n1,n8) ).
cnf(u32056,axiom,
~ p(n9,n2,n8) ).
cnf(u32060,axiom,
~ p(n9,n3,n8) ).
cnf(u32065,axiom,
~ p(n7,n1,n7) ).
cnf(u32069,axiom,
~ p(n7,n2,n7) ).
cnf(u32074,axiom,
p(n7,n3,n7) ).
cnf(u32077,axiom,
~ p(n8,n1,n7) ).
cnf(u32081,axiom,
~ p(n8,n2,n7) ).
cnf(u32085,axiom,
~ p(n8,n3,n7) ).
cnf(u32089,axiom,
~ p(n9,n1,n7) ).
cnf(u32093,axiom,
~ p(n9,n2,n7) ).
cnf(u32097,axiom,
~ p(n9,n3,n7) ).
cnf(u32103,axiom,
p(n7,n1,n6) ).
cnf(u32106,axiom,
~ p(n7,n2,n6) ).
cnf(u32110,axiom,
~ p(n7,n3,n6) ).
cnf(u32114,axiom,
~ p(n8,n1,n6) ).
cnf(u32118,axiom,
~ p(n8,n2,n6) ).
cnf(u32122,axiom,
~ p(n8,n3,n6) ).
cnf(u32126,axiom,
~ p(n9,n1,n6) ).
cnf(u32130,axiom,
~ p(n9,n2,n6) ).
cnf(u32134,axiom,
~ p(n9,n3,n6) ).
cnf(u32139,axiom,
~ p(n7,n1,n5) ).
cnf(u32143,axiom,
~ p(n7,n2,n5) ).
cnf(u32147,axiom,
~ p(n7,n3,n5) ).
cnf(u32151,axiom,
~ p(n8,n1,n5) ).
cnf(u32155,axiom,
~ p(n8,n2,n5) ).
cnf(u32159,axiom,
~ p(n8,n3,n5) ).
cnf(u32163,axiom,
~ p(n9,n1,n5) ).
cnf(u32168,axiom,
p(n9,n2,n5) ).
cnf(u32171,axiom,
~ p(n9,n3,n5) ).
cnf(u32176,axiom,
~ p(n7,n1,n4) ).
cnf(u32180,axiom,
~ p(n7,n2,n4) ).
cnf(u32184,axiom,
~ p(n7,n3,n4) ).
cnf(u32188,axiom,
~ p(n8,n1,n4) ).
cnf(u32193,axiom,
p(n8,n2,n4) ).
cnf(u32196,axiom,
~ p(n8,n3,n4) ).
cnf(u32200,axiom,
~ p(n9,n1,n4) ).
cnf(u32204,axiom,
~ p(n9,n2,n4) ).
cnf(u32208,axiom,
~ p(n9,n3,n4) ).
cnf(u32213,axiom,
~ p(n7,n1,n3) ).
cnf(u32218,axiom,
p(n7,n2,n3) ).
cnf(u32221,axiom,
~ p(n7,n3,n3) ).
cnf(u32225,axiom,
~ p(n8,n1,n3) ).
cnf(u32229,axiom,
~ p(n8,n2,n3) ).
cnf(u32233,axiom,
~ p(n8,n3,n3) ).
cnf(u32237,axiom,
~ p(n9,n1,n3) ).
cnf(u32241,axiom,
~ p(n9,n2,n3) ).
cnf(u32245,axiom,
~ p(n9,n3,n3) ).
cnf(u32250,axiom,
~ p(n7,n1,n2) ).
cnf(u32254,axiom,
~ p(n7,n2,n2) ).
cnf(u32258,axiom,
~ p(n7,n3,n2) ).
cnf(u32262,axiom,
~ p(n8,n1,n2) ).
cnf(u32266,axiom,
~ p(n8,n2,n2) ).
cnf(u32270,axiom,
~ p(n8,n3,n2) ).
cnf(u32275,axiom,
p(n9,n1,n2) ).
cnf(u32278,axiom,
~ p(n9,n2,n2) ).
cnf(u32282,axiom,
~ p(n9,n3,n2) ).
cnf(u32287,axiom,
~ p(n7,n1,n1) ).
cnf(u32291,axiom,
~ p(n7,n2,n1) ).
cnf(u32295,axiom,
~ p(n7,n3,n1) ).
cnf(u32299,axiom,
~ p(n8,n1,n1) ).
cnf(u32303,axiom,
~ p(n8,n2,n1) ).
cnf(u32308,axiom,
p(n8,n3,n1) ).
cnf(u32311,axiom,
~ p(n9,n1,n1) ).
cnf(u32315,axiom,
~ p(n9,n2,n1) ).
cnf(u32319,axiom,
~ p(n9,n3,n1) ).
cnf(u32325,axiom,
p(n4,n7,n9) ).
cnf(u32328,axiom,
~ p(n4,n8,n9) ).
cnf(u32332,axiom,
~ p(n4,n9,n9) ).
cnf(u32336,axiom,
~ p(n5,n7,n9) ).
cnf(u32340,axiom,
~ p(n5,n8,n9) ).
cnf(u32344,axiom,
~ p(n5,n9,n9) ).
cnf(u32348,axiom,
~ p(n6,n7,n9) ).
cnf(u32352,axiom,
~ p(n6,n8,n9) ).
cnf(u32356,axiom,
~ p(n6,n9,n9) ).
cnf(u32361,axiom,
~ p(n4,n7,n8) ).
cnf(u32365,axiom,
~ p(n4,n8,n8) ).
cnf(u32369,axiom,
~ p(n4,n9,n8) ).
cnf(u32373,axiom,
~ p(n5,n7,n8) ).
cnf(u32377,axiom,
~ p(n5,n8,n8) ).
cnf(u32381,axiom,
~ p(n5,n9,n8) ).
cnf(u32385,axiom,
~ p(n6,n7,n8) ).
cnf(u32389,axiom,
~ p(n6,n8,n8) ).
cnf(u32394,axiom,
p(n6,n9,n8) ).
cnf(u32398,axiom,
~ p(n4,n7,n7) ).
cnf(u32402,axiom,
~ p(n4,n8,n7) ).
cnf(u32406,axiom,
~ p(n4,n9,n7) ).
cnf(u32410,axiom,
~ p(n5,n7,n7) ).
cnf(u32414,axiom,
~ p(n5,n8,n7) ).
cnf(u32419,axiom,
p(n5,n9,n7) ).
cnf(u32422,axiom,
~ p(n6,n7,n7) ).
cnf(u32426,axiom,
~ p(n6,n8,n7) ).
cnf(u32430,axiom,
~ p(n6,n9,n7) ).
cnf(u32435,axiom,
~ p(n4,n7,n6) ).
cnf(u32439,axiom,
~ p(n4,n8,n6) ).
cnf(u32443,axiom,
~ p(n4,n9,n6) ).
cnf(u32447,axiom,
~ p(n5,n7,n6) ).
cnf(u32451,axiom,
~ p(n5,n8,n6) ).
cnf(u32455,axiom,
~ p(n5,n9,n6) ).
cnf(u32459,axiom,
~ p(n6,n7,n6) ).
cnf(u32464,axiom,
p(n6,n8,n6) ).
cnf(u32467,axiom,
~ p(n6,n9,n6) ).
cnf(u32472,axiom,
~ p(n4,n7,n5) ).
cnf(u32477,axiom,
p(n4,n8,n5) ).
cnf(u32480,axiom,
~ p(n4,n9,n5) ).
cnf(u32484,axiom,
~ p(n5,n7,n5) ).
cnf(u32488,axiom,
~ p(n5,n8,n5) ).
cnf(u32492,axiom,
~ p(n5,n9,n5) ).
cnf(u32496,axiom,
~ p(n6,n7,n5) ).
cnf(u32500,axiom,
~ p(n6,n8,n5) ).
cnf(u32504,axiom,
~ p(n6,n9,n5) ).
cnf(u32509,axiom,
~ p(n4,n7,n4) ).
cnf(u32513,axiom,
~ p(n4,n8,n4) ).
cnf(u32517,axiom,
~ p(n4,n9,n4) ).
cnf(u32521,axiom,
~ p(n5,n7,n4) ).
cnf(u32525,axiom,
~ p(n5,n8,n4) ).
cnf(u32529,axiom,
~ p(n5,n9,n4) ).
cnf(u32534,axiom,
p(n6,n7,n4) ).
cnf(u32537,axiom,
~ p(n6,n8,n4) ).
cnf(u32541,axiom,
~ p(n6,n9,n4) ).
cnf(u32546,axiom,
~ p(n4,n7,n3) ).
cnf(u32550,axiom,
~ p(n4,n8,n3) ).
cnf(u32555,axiom,
p(n4,n9,n3) ).
cnf(u32558,axiom,
~ p(n5,n7,n3) ).
cnf(u32562,axiom,
~ p(n5,n8,n3) ).
cnf(u32566,axiom,
~ p(n5,n9,n3) ).
cnf(u32570,axiom,
~ p(n6,n7,n3) ).
cnf(u32574,axiom,
~ p(n6,n8,n3) ).
cnf(u32578,axiom,
~ p(n6,n9,n3) ).
cnf(u32583,axiom,
~ p(n4,n7,n2) ).
cnf(u32587,axiom,
~ p(n4,n8,n2) ).
cnf(u32591,axiom,
~ p(n4,n9,n2) ).
cnf(u32595,axiom,
~ p(n5,n7,n2) ).
cnf(u32600,axiom,
p(n5,n8,n2) ).
cnf(u32603,axiom,
~ p(n5,n9,n2) ).
cnf(u32607,axiom,
~ p(n6,n7,n2) ).
cnf(u32611,axiom,
~ p(n6,n8,n2) ).
cnf(u32615,axiom,
~ p(n6,n9,n2) ).
cnf(u32620,axiom,
~ p(n4,n7,n1) ).
cnf(u32624,axiom,
~ p(n4,n8,n1) ).
cnf(u32628,axiom,
~ p(n4,n9,n1) ).
cnf(u32633,axiom,
p(n5,n7,n1) ).
cnf(u32636,axiom,
~ p(n5,n8,n1) ).
cnf(u32640,axiom,
~ p(n5,n9,n1) ).
cnf(u32644,axiom,
~ p(n6,n7,n1) ).
cnf(u32648,axiom,
~ p(n6,n8,n1) ).
cnf(u32652,axiom,
~ p(n6,n9,n1) ).
cnf(u32657,axiom,
~ p(n4,n4,n9) ).
cnf(u32661,axiom,
~ p(n4,n5,n9) ).
cnf(u32665,axiom,
~ p(n4,n6,n9) ).
cnf(u32669,axiom,
~ p(n5,n4,n9) ).
cnf(u32673,axiom,
~ p(n5,n5,n9) ).
cnf(u32678,axiom,
p(n5,n6,n9) ).
cnf(u32681,axiom,
~ p(n6,n4,n9) ).
cnf(u32685,axiom,
~ p(n6,n5,n9) ).
cnf(u32689,axiom,
~ p(n6,n6,n9) ).
cnf(u32694,axiom,
~ p(n4,n4,n8) ).
cnf(u32698,axiom,
~ p(n4,n5,n8) ).
cnf(u32702,axiom,
~ p(n4,n6,n8) ).
cnf(u32707,axiom,
p(n5,n4,n8) ).
cnf(u32710,axiom,
~ p(n5,n5,n8) ).
cnf(u32714,axiom,
~ p(n5,n6,n8) ).
cnf(u32718,axiom,
~ p(n6,n4,n8) ).
cnf(u32722,axiom,
~ p(n6,n5,n8) ).
cnf(u32726,axiom,
~ p(n6,n6,n8) ).
cnf(u32731,axiom,
~ p(n4,n4,n7) ).
cnf(u32735,axiom,
~ p(n4,n5,n7) ).
cnf(u32739,axiom,
~ p(n4,n6,n7) ).
cnf(u32743,axiom,
~ p(n5,n4,n7) ).
cnf(u32747,axiom,
~ p(n5,n5,n7) ).
cnf(u32751,axiom,
~ p(n5,n6,n7) ).
cnf(u32756,axiom,
p(n6,n4,n7) ).
cnf(u32759,axiom,
~ p(n6,n5,n7) ).
cnf(u32763,axiom,
~ p(n6,n6,n7) ).
cnf(u32768,axiom,
~ p(n4,n4,n6) ).
cnf(u32773,axiom,
p(n4,n5,n6) ).
cnf(u32776,axiom,
~ p(n4,n6,n6) ).
cnf(u32780,axiom,
~ p(n5,n4,n6) ).
cnf(u32784,axiom,
~ p(n5,n5,n6) ).
cnf(u32788,axiom,
~ p(n5,n6,n6) ).
cnf(u32792,axiom,
~ p(n6,n4,n6) ).
cnf(u32796,axiom,
~ p(n6,n5,n6) ).
cnf(u32800,axiom,
~ p(n6,n6,n6) ).
cnf(u32805,axiom,
~ p(n4,n4,n5) ).
cnf(u32809,axiom,
~ p(n4,n5,n5) ).
cnf(u32813,axiom,
~ p(n4,n6,n5) ).
cnf(u32817,axiom,
~ p(n5,n4,n5) ).
cnf(u32821,axiom,
~ p(n5,n5,n5) ).
cnf(u32825,axiom,
~ p(n5,n6,n5) ).
cnf(u32829,axiom,
~ p(n6,n4,n5) ).
cnf(u32833,axiom,
~ p(n6,n5,n5) ).
cnf(u32838,axiom,
p(n6,n6,n5) ).
cnf(u32842,axiom,
~ p(n4,n4,n4) ).
cnf(u32846,axiom,
~ p(n4,n5,n4) ).
cnf(u32850,axiom,
~ p(n4,n6,n4) ).
cnf(u32854,axiom,
~ p(n5,n4,n4) ).
cnf(u32859,axiom,
p(n5,n5,n4) ).
cnf(u32862,axiom,
~ p(n5,n6,n4) ).
cnf(u32866,axiom,
~ p(n6,n4,n4) ).
cnf(u32870,axiom,
~ p(n6,n5,n4) ).
cnf(u32874,axiom,
~ p(n6,n6,n4) ).
cnf(u32879,axiom,
~ p(n4,n4,n3) ).
cnf(u32883,axiom,
~ p(n4,n5,n3) ).
cnf(u32887,axiom,
~ p(n4,n6,n3) ).
cnf(u32891,axiom,
~ p(n5,n4,n3) ).
cnf(u32895,axiom,
~ p(n5,n5,n3) ).
cnf(u32899,axiom,
~ p(n5,n6,n3) ).
cnf(u32903,axiom,
~ p(n6,n4,n3) ).
cnf(u32908,axiom,
p(n6,n5,n3) ).
cnf(u32911,axiom,
~ p(n6,n6,n3) ).
cnf(u32917,axiom,
p(n4,n4,n2) ).
cnf(u32920,axiom,
~ p(n4,n5,n2) ).
cnf(u32924,axiom,
~ p(n4,n6,n2) ).
cnf(u32928,axiom,
~ p(n5,n4,n2) ).
cnf(u32932,axiom,
~ p(n5,n5,n2) ).
cnf(u32936,axiom,
~ p(n5,n6,n2) ).
cnf(u32940,axiom,
~ p(n6,n4,n2) ).
cnf(u32944,axiom,
~ p(n6,n5,n2) ).
cnf(u32948,axiom,
~ p(n6,n6,n2) ).
cnf(u32953,axiom,
~ p(n4,n4,n1) ).
cnf(u32957,axiom,
~ p(n4,n5,n1) ).
cnf(u32962,axiom,
p(n4,n6,n1) ).
cnf(u32965,axiom,
~ p(n5,n4,n1) ).
cnf(u32969,axiom,
~ p(n5,n5,n1) ).
cnf(u32973,axiom,
~ p(n5,n6,n1) ).
cnf(u32977,axiom,
~ p(n6,n4,n1) ).
cnf(u32981,axiom,
~ p(n6,n5,n1) ).
cnf(u32985,axiom,
~ p(n6,n6,n1) ).
cnf(u32990,axiom,
~ p(n4,n1,n9) ).
cnf(u32994,axiom,
~ p(n4,n2,n9) ).
cnf(u32998,axiom,
~ p(n4,n3,n9) ).
cnf(u33002,axiom,
~ p(n5,n1,n9) ).
cnf(u33006,axiom,
~ p(n5,n2,n9) ).
cnf(u33010,axiom,
~ p(n5,n3,n9) ).
cnf(u33015,axiom,
p(n6,n1,n9) ).
cnf(u33018,axiom,
~ p(n6,n2,n9) ).
cnf(u33022,axiom,
~ p(n6,n3,n9) ).
cnf(u33027,axiom,
~ p(n4,n1,n8) ).
cnf(u33031,axiom,
~ p(n4,n2,n8) ).
cnf(u33036,axiom,
p(n4,n3,n8) ).
cnf(u33039,axiom,
~ p(n5,n1,n8) ).
cnf(u33043,axiom,
~ p(n5,n2,n8) ).
cnf(u33047,axiom,
~ p(n5,n3,n8) ).
cnf(u33051,axiom,
~ p(n6,n1,n8) ).
cnf(u33055,axiom,
~ p(n6,n2,n8) ).
cnf(u33059,axiom,
~ p(n6,n3,n8) ).
cnf(u33064,axiom,
~ p(n4,n1,n7) ).
cnf(u33069,axiom,
p(n4,n2,n7) ).
cnf(u33072,axiom,
~ p(n4,n3,n7) ).
cnf(u33076,axiom,
~ p(n5,n1,n7) ).
cnf(u33080,axiom,
~ p(n5,n2,n7) ).
cnf(u33084,axiom,
~ p(n5,n3,n7) ).
cnf(u33088,axiom,
~ p(n6,n1,n7) ).
cnf(u33092,axiom,
~ p(n6,n2,n7) ).
cnf(u33096,axiom,
~ p(n6,n3,n7) ).
cnf(u33101,axiom,
~ p(n4,n1,n6) ).
cnf(u33105,axiom,
~ p(n4,n2,n6) ).
cnf(u33109,axiom,
~ p(n4,n3,n6) ).
cnf(u33113,axiom,
~ p(n5,n1,n6) ).
cnf(u33118,axiom,
p(n5,n2,n6) ).
cnf(u33121,axiom,
~ p(n5,n3,n6) ).
cnf(u33125,axiom,
~ p(n6,n1,n6) ).
cnf(u33129,axiom,
~ p(n6,n2,n6) ).
cnf(u33133,axiom,
~ p(n6,n3,n6) ).
cnf(u33138,axiom,
~ p(n4,n1,n5) ).
cnf(u33142,axiom,
~ p(n4,n2,n5) ).
cnf(u33146,axiom,
~ p(n4,n3,n5) ).
cnf(u33151,axiom,
p(n5,n1,n5) ).
cnf(u33154,axiom,
~ p(n5,n2,n5) ).
cnf(u33158,axiom,
~ p(n5,n3,n5) ).
cnf(u33162,axiom,
~ p(n6,n1,n5) ).
cnf(u33166,axiom,
~ p(n6,n2,n5) ).
cnf(u33170,axiom,
~ p(n6,n3,n5) ).
cnf(u33176,axiom,
p(n4,n1,n4) ).
cnf(u33179,axiom,
~ p(n4,n2,n4) ).
cnf(u33183,axiom,
~ p(n4,n3,n4) ).
cnf(u33187,axiom,
~ p(n5,n1,n4) ).
cnf(u33191,axiom,
~ p(n5,n2,n4) ).
cnf(u33195,axiom,
~ p(n5,n3,n4) ).
cnf(u33199,axiom,
~ p(n6,n1,n4) ).
cnf(u33203,axiom,
~ p(n6,n2,n4) ).
cnf(u33207,axiom,
~ p(n6,n3,n4) ).
cnf(u33212,axiom,
~ p(n4,n1,n3) ).
cnf(u33216,axiom,
~ p(n4,n2,n3) ).
cnf(u33220,axiom,
~ p(n4,n3,n3) ).
cnf(u33224,axiom,
~ p(n5,n1,n3) ).
cnf(u33228,axiom,
~ p(n5,n2,n3) ).
cnf(u33233,axiom,
p(n5,n3,n3) ).
cnf(u33236,axiom,
~ p(n6,n1,n3) ).
cnf(u33240,axiom,
~ p(n6,n2,n3) ).
cnf(u33244,axiom,
~ p(n6,n3,n3) ).
cnf(u33249,axiom,
~ p(n4,n1,n2) ).
cnf(u33253,axiom,
~ p(n4,n2,n2) ).
cnf(u33257,axiom,
~ p(n4,n3,n2) ).
cnf(u33261,axiom,
~ p(n5,n1,n2) ).
cnf(u33265,axiom,
~ p(n5,n2,n2) ).
cnf(u33269,axiom,
~ p(n5,n3,n2) ).
cnf(u33273,axiom,
~ p(n6,n1,n2) ).
cnf(u33277,axiom,
~ p(n6,n2,n2) ).
cnf(u33282,axiom,
p(n6,n3,n2) ).
cnf(u33286,axiom,
~ p(n4,n1,n1) ).
cnf(u33290,axiom,
~ p(n4,n2,n1) ).
cnf(u33294,axiom,
~ p(n4,n3,n1) ).
cnf(u33298,axiom,
~ p(n5,n1,n1) ).
cnf(u33302,axiom,
~ p(n5,n2,n1) ).
cnf(u33306,axiom,
~ p(n5,n3,n1) ).
cnf(u33310,axiom,
~ p(n6,n1,n1) ).
cnf(u33315,axiom,
p(n6,n2,n1) ).
cnf(u33318,axiom,
~ p(n6,n3,n1) ).
cnf(u33323,axiom,
~ p(n1,n7,n9) ).
cnf(u33327,axiom,
~ p(n1,n8,n9) ).
cnf(u33332,axiom,
p(n1,n9,n9) ).
cnf(u33335,axiom,
~ p(n2,n7,n9) ).
cnf(u33339,axiom,
~ p(n2,n8,n9) ).
cnf(u33343,axiom,
~ p(n2,n9,n9) ).
cnf(u33347,axiom,
~ p(n3,n7,n9) ).
cnf(u33351,axiom,
~ p(n3,n8,n9) ).
cnf(u33355,axiom,
~ p(n3,n9,n9) ).
cnf(u33360,axiom,
~ p(n1,n7,n8) ).
cnf(u33364,axiom,
~ p(n1,n8,n8) ).
cnf(u33368,axiom,
~ p(n1,n9,n8) ).
cnf(u33373,axiom,
p(n2,n7,n8) ).
cnf(u33376,axiom,
~ p(n2,n8,n8) ).
cnf(u33380,axiom,
~ p(n2,n9,n8) ).
cnf(u33384,axiom,
~ p(n3,n7,n8) ).
cnf(u33388,axiom,
~ p(n3,n8,n8) ).
cnf(u33392,axiom,
~ p(n3,n9,n8) ).
cnf(u33398,axiom,
p(n1,n7,n7) ).
cnf(u33401,axiom,
~ p(n1,n8,n7) ).
cnf(u33405,axiom,
~ p(n1,n9,n7) ).
cnf(u33409,axiom,
~ p(n2,n7,n7) ).
cnf(u33413,axiom,
~ p(n2,n8,n7) ).
cnf(u33417,axiom,
~ p(n2,n9,n7) ).
cnf(u33421,axiom,
~ p(n3,n7,n7) ).
cnf(u33425,axiom,
~ p(n3,n8,n7) ).
cnf(u33429,axiom,
~ p(n3,n9,n7) ).
cnf(u33434,axiom,
~ p(n1,n7,n6) ).
cnf(u33438,axiom,
~ p(n1,n8,n6) ).
cnf(u33442,axiom,
~ p(n1,n9,n6) ).
cnf(u33446,axiom,
~ p(n2,n7,n6) ).
cnf(u33450,axiom,
~ p(n2,n8,n6) ).
cnf(u33454,axiom,
~ p(n2,n9,n6) ).
cnf(u33458,axiom,
~ p(n3,n7,n6) ).
cnf(u33462,axiom,
~ p(n3,n8,n6) ).
cnf(u33467,axiom,
p(n3,n9,n6) ).
cnf(u33471,axiom,
~ p(n1,n7,n5) ).
cnf(u33475,axiom,
~ p(n1,n8,n5) ).
cnf(u33479,axiom,
~ p(n1,n9,n5) ).
cnf(u33483,axiom,
~ p(n2,n7,n5) ).
cnf(u33487,axiom,
~ p(n2,n8,n5) ).
cnf(u33491,axiom,
~ p(n2,n9,n5) ).
cnf(u33496,axiom,
p(n3,n7,n5) ).
cnf(u33499,axiom,
~ p(n3,n8,n5) ).
cnf(u33503,axiom,
~ p(n3,n9,n5) ).
cnf(u33508,axiom,
~ p(n1,n7,n4) ).
cnf(u33512,axiom,
~ p(n1,n8,n4) ).
cnf(u33516,axiom,
~ p(n1,n9,n4) ).
cnf(u33520,axiom,
~ p(n2,n7,n4) ).
cnf(u33525,axiom,
p(n2,n8,n4) ).
cnf(u33528,axiom,
~ p(n2,n9,n4) ).
cnf(u33532,axiom,
~ p(n3,n7,n4) ).
cnf(u33536,axiom,
~ p(n3,n8,n4) ).
cnf(u33540,axiom,
~ p(n3,n9,n4) ).
cnf(u33545,axiom,
~ p(n1,n7,n3) ).
cnf(u33550,axiom,
p(n1,n8,n3) ).
cnf(u33553,axiom,
~ p(n1,n9,n3) ).
cnf(u33557,axiom,
~ p(n2,n7,n3) ).
cnf(u33561,axiom,
~ p(n2,n8,n3) ).
cnf(u33565,axiom,
~ p(n2,n9,n3) ).
cnf(u33569,axiom,
~ p(n3,n7,n3) ).
cnf(u33573,axiom,
~ p(n3,n8,n3) ).
cnf(u33577,axiom,
~ p(n3,n9,n3) ).
cnf(u33582,axiom,
~ p(n1,n7,n2) ).
cnf(u33586,axiom,
~ p(n1,n8,n2) ).
cnf(u33590,axiom,
~ p(n1,n9,n2) ).
cnf(u33594,axiom,
~ p(n2,n7,n2) ).
cnf(u33598,axiom,
~ p(n2,n8,n2) ).
cnf(u33603,axiom,
p(n2,n9,n2) ).
cnf(u33606,axiom,
~ p(n3,n7,n2) ).
cnf(u33610,axiom,
~ p(n3,n8,n2) ).
cnf(u33614,axiom,
~ p(n3,n9,n2) ).
cnf(u33619,axiom,
~ p(n1,n7,n1) ).
cnf(u33623,axiom,
~ p(n1,n8,n1) ).
cnf(u33627,axiom,
~ p(n1,n9,n1) ).
cnf(u33631,axiom,
~ p(n2,n7,n1) ).
cnf(u33635,axiom,
~ p(n2,n8,n1) ).
cnf(u33639,axiom,
~ p(n2,n9,n1) ).
cnf(u33643,axiom,
~ p(n3,n7,n1) ).
cnf(u33648,axiom,
p(n3,n8,n1) ).
cnf(u33651,axiom,
~ p(n3,n9,n1) ).
cnf(u33656,axiom,
~ p(n1,n4,n9) ).
cnf(u33660,axiom,
~ p(n1,n5,n9) ).
cnf(u33664,axiom,
~ p(n1,n6,n9) ).
cnf(u33668,axiom,
~ p(n2,n4,n9) ).
cnf(u33672,axiom,
~ p(n2,n5,n9) ).
cnf(u33676,axiom,
~ p(n2,n6,n9) ).
cnf(u33680,axiom,
~ p(n3,n4,n9) ).
cnf(u33685,axiom,
p(n3,n5,n9) ).
cnf(u33688,axiom,
~ p(n3,n6,n9) ).
cnf(u33693,axiom,
~ p(n1,n4,n8) ).
cnf(u33698,axiom,
p(n1,n5,n8) ).
cnf(u33701,axiom,
~ p(n1,n6,n8) ).
cnf(u33705,axiom,
~ p(n2,n4,n8) ).
cnf(u33709,axiom,
~ p(n2,n5,n8) ).
cnf(u33713,axiom,
~ p(n2,n6,n8) ).
cnf(u33717,axiom,
~ p(n3,n4,n8) ).
cnf(u33721,axiom,
~ p(n3,n5,n8) ).
cnf(u33725,axiom,
~ p(n3,n6,n8) ).
cnf(u33730,axiom,
~ p(n1,n4,n7) ).
cnf(u33734,axiom,
~ p(n1,n5,n7) ).
cnf(u33738,axiom,
~ p(n1,n6,n7) ).
cnf(u33742,axiom,
~ p(n2,n4,n7) ).
cnf(u33746,axiom,
~ p(n2,n5,n7) ).
cnf(u33751,axiom,
p(n2,n6,n7) ).
cnf(u33754,axiom,
~ p(n3,n4,n7) ).
cnf(u33758,axiom,
~ p(n3,n5,n7) ).
cnf(u33762,axiom,
~ p(n3,n6,n7) ).
cnf(u33768,axiom,
p(n1,n4,n6) ).
cnf(u33771,axiom,
~ p(n1,n5,n6) ).
cnf(u33775,axiom,
~ p(n1,n6,n6) ).
cnf(u33779,axiom,
~ p(n2,n4,n6) ).
cnf(u33783,axiom,
~ p(n2,n5,n6) ).
cnf(u33787,axiom,
~ p(n2,n6,n6) ).
cnf(u33791,axiom,
~ p(n3,n4,n6) ).
cnf(u33795,axiom,
~ p(n3,n5,n6) ).
cnf(u33799,axiom,
~ p(n3,n6,n6) ).
cnf(u33804,axiom,
~ p(n1,n4,n5) ).
cnf(u33808,axiom,
~ p(n1,n5,n5) ).
cnf(u33812,axiom,
~ p(n1,n6,n5) ).
cnf(u33817,axiom,
p(n2,n4,n5) ).
cnf(u33820,axiom,
~ p(n2,n5,n5) ).
cnf(u33824,axiom,
~ p(n2,n6,n5) ).
cnf(u33828,axiom,
~ p(n3,n4,n5) ).
cnf(u33832,axiom,
~ p(n3,n5,n5) ).
cnf(u33836,axiom,
~ p(n3,n6,n5) ).
cnf(u33841,axiom,
~ p(n1,n4,n4) ).
cnf(u33845,axiom,
~ p(n1,n5,n4) ).
cnf(u33850,axiom,
p(n1,n6,n4) ).
cnf(u33853,axiom,
~ p(n2,n4,n4) ).
cnf(u33857,axiom,
~ p(n2,n5,n4) ).
cnf(u33861,axiom,
~ p(n2,n6,n4) ).
cnf(u33865,axiom,
~ p(n3,n4,n4) ).
cnf(u33869,axiom,
~ p(n3,n5,n4) ).
cnf(u33873,axiom,
~ p(n3,n6,n4) ).
cnf(u33878,axiom,
~ p(n1,n4,n3) ).
cnf(u33882,axiom,
~ p(n1,n5,n3) ).
cnf(u33886,axiom,
~ p(n1,n6,n3) ).
cnf(u33890,axiom,
~ p(n2,n4,n3) ).
cnf(u33894,axiom,
~ p(n2,n5,n3) ).
cnf(u33898,axiom,
~ p(n2,n6,n3) ).
cnf(u33903,axiom,
p(n3,n4,n3) ).
cnf(u33906,axiom,
~ p(n3,n5,n3) ).
cnf(u33910,axiom,
~ p(n3,n6,n3) ).
cnf(u33915,axiom,
~ p(n1,n4,n2) ).
cnf(u33919,axiom,
~ p(n1,n5,n2) ).
cnf(u33923,axiom,
~ p(n1,n6,n2) ).
cnf(u33927,axiom,
~ p(n2,n4,n2) ).
cnf(u33931,axiom,
~ p(n2,n5,n2) ).
cnf(u33935,axiom,
~ p(n2,n6,n2) ).
cnf(u33939,axiom,
~ p(n3,n4,n2) ).
cnf(u33943,axiom,
~ p(n3,n5,n2) ).
cnf(u33948,axiom,
p(n3,n6,n2) ).
cnf(u33952,axiom,
~ p(n1,n4,n1) ).
cnf(u33956,axiom,
~ p(n1,n5,n1) ).
cnf(u33960,axiom,
~ p(n1,n6,n1) ).
cnf(u33964,axiom,
~ p(n2,n4,n1) ).
cnf(u33969,axiom,
p(n2,n5,n1) ).
cnf(u33972,axiom,
~ p(n2,n6,n1) ).
cnf(u33976,axiom,
~ p(n3,n4,n1) ).
cnf(u33980,axiom,
~ p(n3,n5,n1) ).
cnf(u33984,axiom,
~ p(n3,n6,n1) ).
cnf(u33989,axiom,
~ p(n1,n1,n9) ).
cnf(u33993,axiom,
~ p(n1,n2,n9) ).
cnf(u33997,axiom,
~ p(n1,n3,n9) ).
cnf(u34001,axiom,
~ p(n2,n1,n9) ).
cnf(u34006,axiom,
p(n2,n2,n9) ).
cnf(u34009,axiom,
~ p(n2,n3,n9) ).
cnf(u34013,axiom,
~ p(n3,n1,n9) ).
cnf(u34017,axiom,
~ p(n3,n2,n9) ).
cnf(u34021,axiom,
~ p(n3,n3,n9) ).
cnf(u34026,axiom,
~ p(n1,n1,n8) ).
cnf(u34030,axiom,
~ p(n1,n2,n8) ).
cnf(u34034,axiom,
~ p(n1,n3,n8) ).
cnf(u34038,axiom,
~ p(n2,n1,n8) ).
cnf(u34042,axiom,
~ p(n2,n2,n8) ).
cnf(u34046,axiom,
~ p(n2,n3,n8) ).
cnf(u34050,axiom,
~ p(n3,n1,n8) ).
cnf(u34055,axiom,
p(n3,n2,n8) ).
cnf(u34058,axiom,
~ p(n3,n3,n8) ).
cnf(u34063,axiom,
~ p(n1,n1,n7) ).
cnf(u34067,axiom,
~ p(n1,n2,n7) ).
cnf(u34071,axiom,
~ p(n1,n3,n7) ).
cnf(u34075,axiom,
~ p(n2,n1,n7) ).
cnf(u34079,axiom,
~ p(n2,n2,n7) ).
cnf(u34083,axiom,
~ p(n2,n3,n7) ).
cnf(u34088,axiom,
p(n3,n1,n7) ).
cnf(u34091,axiom,
~ p(n3,n2,n7) ).
cnf(u34095,axiom,
~ p(n3,n3,n7) ).
cnf(u34100,axiom,
~ p(n1,n1,n6) ).
cnf(u34104,axiom,
~ p(n1,n2,n6) ).
cnf(u34108,axiom,
~ p(n1,n3,n6) ).
cnf(u34112,axiom,
~ p(n2,n1,n6) ).
cnf(u34116,axiom,
~ p(n2,n2,n6) ).
cnf(u34121,axiom,
p(n2,n3,n6) ).
cnf(u34124,axiom,
~ p(n3,n1,n6) ).
cnf(u34128,axiom,
~ p(n3,n2,n6) ).
cnf(u34132,axiom,
~ p(n3,n3,n6) ).
cnf(u34137,axiom,
~ p(n1,n1,n5) ).
cnf(u34141,axiom,
~ p(n1,n2,n5) ).
cnf(u34146,axiom,
p(n1,n3,n5) ).
cnf(u34149,axiom,
~ p(n2,n1,n5) ).
cnf(u34153,axiom,
~ p(n2,n2,n5) ).
cnf(u34157,axiom,
~ p(n2,n3,n5) ).
cnf(u34161,axiom,
~ p(n3,n1,n5) ).
cnf(u34165,axiom,
~ p(n3,n2,n5) ).
cnf(u34169,axiom,
~ p(n3,n3,n5) ).
cnf(u34174,axiom,
~ p(n1,n1,n4) ).
cnf(u34178,axiom,
~ p(n1,n2,n4) ).
cnf(u34182,axiom,
~ p(n1,n3,n4) ).
cnf(u34186,axiom,
~ p(n2,n1,n4) ).
cnf(u34190,axiom,
~ p(n2,n2,n4) ).
cnf(u34194,axiom,
~ p(n2,n3,n4) ).
cnf(u34198,axiom,
~ p(n3,n1,n4) ).
cnf(u34202,axiom,
~ p(n3,n2,n4) ).
cnf(u34207,axiom,
p(n3,n3,n4) ).
cnf(u34211,axiom,
~ p(n1,n1,n3) ).
cnf(u34215,axiom,
~ p(n1,n2,n3) ).
cnf(u34219,axiom,
~ p(n1,n3,n3) ).
cnf(u34224,axiom,
p(n2,n1,n3) ).
cnf(u34227,axiom,
~ p(n2,n2,n3) ).
cnf(u34231,axiom,
~ p(n2,n3,n3) ).
cnf(u34235,axiom,
~ p(n3,n1,n3) ).
cnf(u34239,axiom,
~ p(n3,n2,n3) ).
cnf(u34243,axiom,
~ p(n3,n3,n3) ).
cnf(u34248,axiom,
~ p(n1,n1,n2) ).
cnf(u34253,axiom,
p(n1,n2,n2) ).
cnf(u34256,axiom,
~ p(n1,n3,n2) ).
cnf(u34260,axiom,
~ p(n2,n1,n2) ).
cnf(u34264,axiom,
~ p(n2,n2,n2) ).
cnf(u34268,axiom,
~ p(n2,n3,n2) ).
cnf(u34272,axiom,
~ p(n3,n1,n2) ).
cnf(u34276,axiom,
~ p(n3,n2,n2) ).
cnf(u34280,axiom,
~ p(n3,n3,n2) ).
cnf(u34286,axiom,
p(n1,n1,n1) ).
cnf(u34289,axiom,
~ p(n1,n2,n1) ).
cnf(u34293,axiom,
~ p(n1,n3,n1) ).
cnf(u34297,axiom,
~ p(n2,n1,n1) ).
cnf(u34301,axiom,
~ p(n2,n2,n1) ).
cnf(u34305,axiom,
~ p(n2,n3,n1) ).
cnf(u34309,axiom,
~ p(n3,n1,n1) ).
cnf(u34313,axiom,
~ p(n3,n2,n1) ).
cnf(u34317,axiom,
~ p(n3,n3,n1) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ079+2 : TPTP v9.3.1. Bugfixed v5.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.39 % Computer : n017.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sun Sep 27 22:35:35 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.42 Running first-order model finding
% 0.13/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.55/0.76 % (3007675)Will run a generic schedule for satisfiability detection.
% 0.55/0.76 % (3007705)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1970460693:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 0.55/0.76 % (3007700)% WARNING: option uhcvi not known.
% 0.55/0.76 % (3007700)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=395155001:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 0.55/0.76 % (3007702)dis+10_1_sil=32000:sp=arity:random_seed=507541664:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 0.55/0.76 % (3007699)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1258995914_2998 on theBenchmark for (2998ds/0Mi)
% 0.55/0.76 % (3007701)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=89870856:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 0.55/0.76 % (3007704)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1640764201:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 0.55/0.76 % (3007703)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2371045829:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 0.55/0.76 % (3007705)Instruction limit reached!
% 0.55/0.76 % (3007705)------------------------------
% 0.55/0.76 % (3007705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.76 % (3007705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.76 % (3007705)CaDiCaL version: 2.1.3
% 0.55/0.76 % (3007705)Termination reason: Instruction limit
% 0.55/0.76 % (3007705)Termination phase: Property scanning
% 0.55/0.76 % (3007705)Time elapsed: 0.040 s
% 0.55/0.76 % (3007705)Peak memory usage: 22 MB
% 0.55/0.76 % (3007705)Instructions burned: 162 (million)
% 0.55/0.76 % (3007713)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4087174693:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 0.55/0.76 % (3007702)Instruction limit reached!
% 0.55/0.76 % (3007702)------------------------------
% 0.55/0.76 % (3007702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.76 % (3007702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.76 % (3007702)CaDiCaL version: 2.1.3
% 0.55/0.76 % (3007702)Termination reason: Instruction limit
% 0.55/0.76 % (3007702)Termination phase: Property scanning
% 0.55/0.76 % (3007702)Time elapsed: 0.049 s
% 0.55/0.76 % (3007702)Peak memory usage: 22 MB
% 0.55/0.76 % (3007702)Instructions burned: 105 (million)
% 0.55/0.76 % (3007704)Instruction limit reached!
% 0.55/0.76 % (3007704)------------------------------
% 0.55/0.76 % (3007704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.76 % (3007704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.76 % (3007704)CaDiCaL version: 2.1.3
% 0.55/0.76 % (3007704)Termination reason: Instruction limit
% 0.55/0.76 % (3007704)Termination phase: Property scanning
% 0.55/0.76 % (3007704)Time elapsed: 0.059 s
% 0.55/0.76 % (3007704)Peak memory usage: 22 MB
% 0.55/0.76 % (3007704)Instructions burned: 132 (million)
% 0.55/0.76 % (3007703)Instruction limit reached!
% 0.55/0.76 % (3007703)------------------------------
% 0.55/0.76 % (3007703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.76 % (3007703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.76 % (3007703)CaDiCaL version: 2.1.3
% 0.55/0.76 % (3007703)Termination reason: Instruction limit
% 0.55/0.76 % (3007703)Termination phase: Property scanning
% 0.55/0.76 % (3007703)Time elapsed: 0.064 s
% 0.55/0.76 % (3007703)Peak memory usage: 24 MB
% 0.55/0.76 % (3007703)Instructions burned: 117 (million)
% 0.55/0.76 % (3007715)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=526789730:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 0.55/0.76 % (3007716)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=230735126:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.55/0.76 % (3007717)ott-21_1_sil=16000:fs=off:random_seed=910982868:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 0.55/0.76 % (3007715)Instruction limit reached!
% 0.55/0.76 % (3007715)------------------------------
% 0.55/0.76 % (3007715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.76 % (3007715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.76 % (3007715)CaDiCaL version: 2.1.3
% 0.55/0.76 % (3007715)Termination reason: Instruction limit
% 0.55/0.76 % (3007715)Termination phase: Property scanning
% 0.55/0.76 % (3007715)Time elapsed: 0.060 s
% 0.55/0.76 % (3007715)Peak memory usage: 22 MB
% 0.55/0.76 % (3007715)Instructions burned: 133 (million)
% 0.55/0.76 % (3007721)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=204521710:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 0.55/0.76 % (3007717)Instruction limit reached!
% 0.55/0.76 % (3007717)------------------------------
% 0.55/0.76 % (3007717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.76 % (3007717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.76 % (3007717)CaDiCaL version: 2.1.3
% 0.55/0.76 % (3007717)Termination reason: Instruction limit
% 0.55/0.76 % (3007717)Termination phase: Saturation
% 0.55/0.76 % (3007717)Time elapsed: 0.078 s
% 0.55/0.76 % (3007717)Peak memory usage: 23 MB
% 0.55/0.76 % (3007717)Instructions burned: 180 (million)
% 0.55/0.76 % (3007700) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3007675-3007700"...
% 0.55/0.76 % (3007700)...printing done.
% 0.55/0.76 % SZS status Satisfiable for theBenchmark
% 0.55/0.76 % SZS output start Saturation.
% See solution above
% 0.55/0.77 % SZS output start Definitions and Model Updates.
% 0.55/0.77 % SZS output end Definitions and Model Updates.
% 0.55/0.77 % (3007700)------------------------------
% 0.55/0.77 % (3007700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.55/0.77 % (3007700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.55/0.77 % (3007700)CaDiCaL version: 2.1.3
% 0.55/0.77 % (3007700)Termination reason: Satisfiable
% 0.55/0.77 % (3007700)Time elapsed: 0.171 s
% 0.55/0.77 % (3007700)Peak memory usage: 34 MB
% 0.55/0.77 % (3007700)Instructions burned: 327 (million)
% 0.55/0.77 % (3007675)Success in time 0.328 s
% 0.55/0.77 % Vampire exiting
%------------------------------------------------------------------------------