%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PUZ079+2 : TPTP v9.3.1. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 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:31:31 PM UTC 2026
% Result : Satisfiable 9.59s 2.09s
% Output : Saturation 10.17s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u31325,axiom,
~ p(n9,n9,n9) ).
cnf(u31329,axiom,
~ p(n9,n8,n9) ).
cnf(u31333,axiom,
~ p(n9,n7,n9) ).
cnf(u31337,axiom,
~ p(n8,n9,n9) ).
cnf(u31341,axiom,
~ p(n8,n8,n9) ).
cnf(u31345,axiom,
~ p(n8,n7,n9) ).
cnf(u31349,axiom,
~ p(n7,n9,n9) ).
cnf(u31354,axiom,
p(n7,n8,n9) ).
cnf(u31357,axiom,
~ p(n7,n7,n9) ).
cnf(u31362,axiom,
~ p(n9,n9,n8) ).
cnf(u31367,axiom,
p(n9,n8,n8) ).
cnf(u31370,axiom,
~ p(n9,n7,n8) ).
cnf(u31374,axiom,
~ p(n8,n9,n8) ).
cnf(u31378,axiom,
~ p(n8,n8,n8) ).
cnf(u31382,axiom,
~ p(n8,n7,n8) ).
cnf(u31386,axiom,
~ p(n7,n9,n8) ).
cnf(u31390,axiom,
~ p(n7,n8,n8) ).
cnf(u31394,axiom,
~ p(n7,n7,n8) ).
cnf(u31399,axiom,
~ p(n9,n9,n7) ).
cnf(u31403,axiom,
~ p(n9,n8,n7) ).
cnf(u31407,axiom,
~ p(n9,n7,n7) ).
cnf(u31411,axiom,
~ p(n8,n9,n7) ).
cnf(u31416,axiom,
p(n8,n8,n7) ).
cnf(u31419,axiom,
~ p(n8,n7,n7) ).
cnf(u31423,axiom,
~ p(n7,n9,n7) ).
cnf(u31427,axiom,
~ p(n7,n8,n7) ).
cnf(u31431,axiom,
~ p(n7,n7,n7) ).
cnf(u31436,axiom,
~ p(n9,n9,n6) ).
cnf(u31440,axiom,
~ p(n9,n8,n6) ).
cnf(u31444,axiom,
~ p(n9,n7,n6) ).
cnf(u31448,axiom,
~ p(n8,n9,n6) ).
cnf(u31452,axiom,
~ p(n8,n8,n6) ).
cnf(u31457,axiom,
p(n8,n7,n6) ).
cnf(u31460,axiom,
~ p(n7,n9,n6) ).
cnf(u31464,axiom,
~ p(n7,n8,n6) ).
cnf(u31468,axiom,
~ p(n7,n7,n6) ).
cnf(u31473,axiom,
~ p(n9,n9,n5) ).
cnf(u31477,axiom,
~ p(n9,n8,n5) ).
cnf(u31481,axiom,
~ p(n9,n7,n5) ).
cnf(u31486,axiom,
p(n8,n9,n5) ).
cnf(u31489,axiom,
~ p(n8,n8,n5) ).
cnf(u31493,axiom,
~ p(n8,n7,n5) ).
cnf(u31497,axiom,
~ p(n7,n9,n5) ).
cnf(u31501,axiom,
~ p(n7,n8,n5) ).
cnf(u31505,axiom,
~ p(n7,n7,n5) ).
cnf(u31510,axiom,
~ p(n9,n9,n3) ).
cnf(u31514,axiom,
~ p(n9,n8,n3) ).
cnf(u31519,axiom,
p(n9,n7,n3) ).
cnf(u31522,axiom,
~ p(n8,n9,n3) ).
cnf(u31526,axiom,
~ p(n8,n8,n3) ).
cnf(u31530,axiom,
~ p(n8,n7,n3) ).
cnf(u31534,axiom,
~ p(n7,n9,n3) ).
cnf(u31538,axiom,
~ p(n7,n8,n3) ).
cnf(u31542,axiom,
~ p(n7,n7,n3) ).
cnf(u31547,axiom,
~ p(n9,n9,n1) ).
cnf(u31551,axiom,
~ p(n9,n8,n1) ).
cnf(u31555,axiom,
~ p(n9,n7,n1) ).
cnf(u31559,axiom,
~ p(n8,n9,n1) ).
cnf(u31563,axiom,
~ p(n8,n8,n1) ).
cnf(u31567,axiom,
~ p(n8,n7,n1) ).
cnf(u31572,axiom,
p(n7,n9,n1) ).
cnf(u31575,axiom,
~ p(n7,n8,n1) ).
cnf(u31579,axiom,
~ p(n7,n7,n1) ).
cnf(u31584,axiom,
~ p(n9,n6,n8) ).
cnf(u31588,axiom,
~ p(n9,n5,n8) ).
cnf(u31592,axiom,
~ p(n9,n4,n8) ).
cnf(u31596,axiom,
~ p(n8,n6,n8) ).
cnf(u31600,axiom,
~ p(n8,n5,n8) ).
cnf(u31604,axiom,
~ p(n8,n4,n8) ).
cnf(u31609,axiom,
p(n7,n6,n8) ).
cnf(u31612,axiom,
~ p(n7,n5,n8) ).
cnf(u31616,axiom,
~ p(n7,n4,n8) ).
cnf(u31621,axiom,
~ p(n9,n6,n7) ).
cnf(u31626,axiom,
p(n9,n5,n7) ).
cnf(u31629,axiom,
~ p(n9,n4,n7) ).
cnf(u31633,axiom,
~ p(n8,n6,n7) ).
cnf(u31637,axiom,
~ p(n8,n5,n7) ).
cnf(u31641,axiom,
~ p(n8,n4,n7) ).
cnf(u31645,axiom,
~ p(n7,n6,n7) ).
cnf(u31649,axiom,
~ p(n7,n5,n7) ).
cnf(u31653,axiom,
~ p(n7,n4,n7) ).
cnf(u31658,axiom,
~ p(n9,n6,n4) ).
cnf(u31662,axiom,
~ p(n9,n5,n4) ).
cnf(u31666,axiom,
~ p(n9,n4,n4) ).
cnf(u31670,axiom,
~ p(n8,n6,n4) ).
cnf(u31674,axiom,
~ p(n8,n5,n4) ).
cnf(u31678,axiom,
~ p(n8,n4,n4) ).
cnf(u31682,axiom,
~ p(n7,n6,n4) ).
cnf(u31686,axiom,
~ p(n7,n5,n4) ).
cnf(u31691,axiom,
p(n7,n4,n4) ).
cnf(u31695,axiom,
~ p(n9,n6,n2) ).
cnf(u31699,axiom,
~ p(n9,n5,n2) ).
cnf(u31703,axiom,
~ p(n9,n4,n2) ).
cnf(u31707,axiom,
~ p(n8,n6,n2) ).
cnf(u31712,axiom,
p(n8,n5,n2) ).
cnf(u31715,axiom,
~ p(n8,n4,n2) ).
cnf(u31719,axiom,
~ p(n7,n6,n2) ).
cnf(u31723,axiom,
~ p(n7,n5,n2) ).
cnf(u31727,axiom,
~ p(n7,n4,n2) ).
cnf(u31733,axiom,
p(n9,n3,n9) ).
cnf(u31736,axiom,
~ p(n9,n2,n9) ).
cnf(u31740,axiom,
~ p(n9,n1,n9) ).
cnf(u31744,axiom,
~ p(n8,n3,n9) ).
cnf(u31748,axiom,
~ p(n8,n2,n9) ).
cnf(u31752,axiom,
~ p(n8,n1,n9) ).
cnf(u31756,axiom,
~ p(n7,n3,n9) ).
cnf(u31760,axiom,
~ p(n7,n2,n9) ).
cnf(u31764,axiom,
~ p(n7,n1,n9) ).
cnf(u31769,axiom,
~ p(n9,n3,n8) ).
cnf(u31773,axiom,
~ p(n9,n2,n8) ).
cnf(u31777,axiom,
~ p(n9,n1,n8) ).
cnf(u31781,axiom,
~ p(n8,n3,n8) ).
cnf(u31785,axiom,
~ p(n8,n2,n8) ).
cnf(u31790,axiom,
p(n8,n1,n8) ).
cnf(u31793,axiom,
~ p(n7,n3,n8) ).
cnf(u31797,axiom,
~ p(n7,n2,n8) ).
cnf(u31801,axiom,
~ p(n7,n1,n8) ).
cnf(u31806,axiom,
~ p(n9,n3,n6) ).
cnf(u31810,axiom,
~ p(n9,n2,n6) ).
cnf(u31814,axiom,
~ p(n9,n1,n6) ).
cnf(u31818,axiom,
~ p(n8,n3,n6) ).
cnf(u31822,axiom,
~ p(n8,n2,n6) ).
cnf(u31826,axiom,
~ p(n8,n1,n6) ).
cnf(u31830,axiom,
~ p(n7,n3,n6) ).
cnf(u31834,axiom,
~ p(n7,n2,n6) ).
cnf(u31839,axiom,
p(n7,n1,n6) ).
cnf(u31843,axiom,
~ p(n9,n3,n5) ).
cnf(u31848,axiom,
p(n9,n2,n5) ).
cnf(u31851,axiom,
~ p(n9,n1,n5) ).
cnf(u31855,axiom,
~ p(n8,n3,n5) ).
cnf(u31859,axiom,
~ p(n8,n2,n5) ).
cnf(u31863,axiom,
~ p(n8,n1,n5) ).
cnf(u31867,axiom,
~ p(n7,n3,n5) ).
cnf(u31871,axiom,
~ p(n7,n2,n5) ).
cnf(u31875,axiom,
~ p(n7,n1,n5) ).
cnf(u31880,axiom,
~ p(n9,n3,n4) ).
cnf(u31884,axiom,
~ p(n9,n2,n4) ).
cnf(u31888,axiom,
~ p(n9,n1,n4) ).
cnf(u31892,axiom,
~ p(n8,n3,n4) ).
cnf(u31897,axiom,
p(n8,n2,n4) ).
cnf(u31900,axiom,
~ p(n8,n1,n4) ).
cnf(u31904,axiom,
~ p(n7,n3,n4) ).
cnf(u31908,axiom,
~ p(n7,n2,n4) ).
cnf(u31912,axiom,
~ p(n7,n1,n4) ).
cnf(u31917,axiom,
~ p(n9,n3,n3) ).
cnf(u31921,axiom,
~ p(n9,n2,n3) ).
cnf(u31925,axiom,
~ p(n9,n1,n3) ).
cnf(u31929,axiom,
~ p(n8,n3,n3) ).
cnf(u31933,axiom,
~ p(n8,n2,n3) ).
cnf(u31937,axiom,
~ p(n8,n1,n3) ).
cnf(u31941,axiom,
~ p(n7,n3,n3) ).
cnf(u31946,axiom,
p(n7,n2,n3) ).
cnf(u31949,axiom,
~ p(n7,n1,n3) ).
cnf(u31954,axiom,
~ p(n9,n3,n1) ).
cnf(u31958,axiom,
~ p(n9,n2,n1) ).
cnf(u31962,axiom,
~ p(n9,n1,n1) ).
cnf(u31967,axiom,
p(n8,n3,n1) ).
cnf(u31970,axiom,
~ p(n8,n2,n1) ).
cnf(u31974,axiom,
~ p(n8,n1,n1) ).
cnf(u31978,axiom,
~ p(n7,n3,n1) ).
cnf(u31982,axiom,
~ p(n7,n2,n1) ).
cnf(u31986,axiom,
~ p(n7,n1,n1) ).
cnf(u31991,axiom,
~ p(n6,n9,n9) ).
cnf(u31995,axiom,
~ p(n6,n8,n9) ).
cnf(u31999,axiom,
~ p(n6,n7,n9) ).
cnf(u32003,axiom,
~ p(n5,n9,n9) ).
cnf(u32007,axiom,
~ p(n5,n8,n9) ).
cnf(u32011,axiom,
~ p(n5,n7,n9) ).
cnf(u32015,axiom,
~ p(n4,n9,n9) ).
cnf(u32019,axiom,
~ p(n4,n8,n9) ).
cnf(u32024,axiom,
p(n4,n7,n9) ).
cnf(u32028,axiom,
~ p(n6,n9,n7) ).
cnf(u32032,axiom,
~ p(n6,n8,n7) ).
cnf(u32036,axiom,
~ p(n6,n7,n7) ).
cnf(u32041,axiom,
p(n5,n9,n7) ).
cnf(u32044,axiom,
~ p(n5,n8,n7) ).
cnf(u32048,axiom,
~ p(n5,n7,n7) ).
cnf(u32052,axiom,
~ p(n4,n9,n7) ).
cnf(u32056,axiom,
~ p(n4,n8,n7) ).
cnf(u32060,axiom,
~ p(n4,n7,n7) ).
cnf(u32065,axiom,
~ p(n6,n9,n4) ).
cnf(u32069,axiom,
~ p(n6,n8,n4) ).
cnf(u32074,axiom,
p(n6,n7,n4) ).
cnf(u32077,axiom,
~ p(n5,n9,n4) ).
cnf(u32081,axiom,
~ p(n5,n8,n4) ).
cnf(u32085,axiom,
~ p(n5,n7,n4) ).
cnf(u32089,axiom,
~ p(n4,n9,n4) ).
cnf(u32093,axiom,
~ p(n4,n8,n4) ).
cnf(u32097,axiom,
~ p(n4,n7,n4) ).
cnf(u32102,axiom,
~ p(n6,n9,n2) ).
cnf(u32106,axiom,
~ p(n6,n8,n2) ).
cnf(u32110,axiom,
~ p(n6,n7,n2) ).
cnf(u32114,axiom,
~ p(n5,n9,n2) ).
cnf(u32119,axiom,
p(n5,n8,n2) ).
cnf(u32122,axiom,
~ p(n5,n7,n2) ).
cnf(u32126,axiom,
~ p(n4,n9,n2) ).
cnf(u32130,axiom,
~ p(n4,n8,n2) ).
cnf(u32134,axiom,
~ p(n4,n7,n2) ).
cnf(u32139,axiom,
~ p(n6,n6,n9) ).
cnf(u32143,axiom,
~ p(n6,n5,n9) ).
cnf(u32147,axiom,
~ p(n6,n4,n9) ).
cnf(u32152,axiom,
p(n5,n6,n9) ).
cnf(u32155,axiom,
~ p(n5,n5,n9) ).
cnf(u32159,axiom,
~ p(n5,n4,n9) ).
cnf(u32163,axiom,
~ p(n4,n6,n9) ).
cnf(u32167,axiom,
~ p(n4,n5,n9) ).
cnf(u32171,axiom,
~ p(n4,n4,n9) ).
cnf(u32176,axiom,
~ p(n6,n6,n8) ).
cnf(u32180,axiom,
~ p(n6,n5,n8) ).
cnf(u32184,axiom,
~ p(n6,n4,n8) ).
cnf(u32188,axiom,
~ p(n5,n6,n8) ).
cnf(u32192,axiom,
~ p(n5,n5,n8) ).
cnf(u32197,axiom,
p(n5,n4,n8) ).
cnf(u32200,axiom,
~ p(n4,n6,n8) ).
cnf(u32204,axiom,
~ p(n4,n5,n8) ).
cnf(u32208,axiom,
~ p(n4,n4,n8) ).
cnf(u32213,axiom,
~ p(n6,n6,n7) ).
cnf(u32217,axiom,
~ p(n6,n5,n7) ).
cnf(u32222,axiom,
p(n6,n4,n7) ).
cnf(u32225,axiom,
~ p(n5,n6,n7) ).
cnf(u32229,axiom,
~ p(n5,n5,n7) ).
cnf(u32233,axiom,
~ p(n5,n4,n7) ).
cnf(u32237,axiom,
~ p(n4,n6,n7) ).
cnf(u32241,axiom,
~ p(n4,n5,n7) ).
cnf(u32245,axiom,
~ p(n4,n4,n7) ).
cnf(u32250,axiom,
~ p(n6,n6,n6) ).
cnf(u32254,axiom,
~ p(n6,n5,n6) ).
cnf(u32258,axiom,
~ p(n6,n4,n6) ).
cnf(u32262,axiom,
~ p(n5,n6,n6) ).
cnf(u32266,axiom,
~ p(n5,n5,n6) ).
cnf(u32270,axiom,
~ p(n5,n4,n6) ).
cnf(u32274,axiom,
~ p(n4,n6,n6) ).
cnf(u32279,axiom,
p(n4,n5,n6) ).
cnf(u32282,axiom,
~ p(n4,n4,n6) ).
cnf(u32288,axiom,
p(n6,n6,n5) ).
cnf(u32291,axiom,
~ p(n6,n5,n5) ).
cnf(u32295,axiom,
~ p(n6,n4,n5) ).
cnf(u32299,axiom,
~ p(n5,n6,n5) ).
cnf(u32303,axiom,
~ p(n5,n5,n5) ).
cnf(u32307,axiom,
~ p(n5,n4,n5) ).
cnf(u32311,axiom,
~ p(n4,n6,n5) ).
cnf(u32315,axiom,
~ p(n4,n5,n5) ).
cnf(u32319,axiom,
~ p(n4,n4,n5) ).
cnf(u32324,axiom,
~ p(n6,n6,n4) ).
cnf(u32328,axiom,
~ p(n6,n5,n4) ).
cnf(u32332,axiom,
~ p(n6,n4,n4) ).
cnf(u32336,axiom,
~ p(n5,n6,n4) ).
cnf(u32341,axiom,
p(n5,n5,n4) ).
cnf(u32344,axiom,
~ p(n5,n4,n4) ).
cnf(u32348,axiom,
~ p(n4,n6,n4) ).
cnf(u32352,axiom,
~ p(n4,n5,n4) ).
cnf(u32356,axiom,
~ p(n4,n4,n4) ).
cnf(u32361,axiom,
~ p(n6,n6,n3) ).
cnf(u32366,axiom,
p(n6,n5,n3) ).
cnf(u32369,axiom,
~ p(n6,n4,n3) ).
cnf(u32373,axiom,
~ p(n5,n6,n3) ).
cnf(u32377,axiom,
~ p(n5,n5,n3) ).
cnf(u32381,axiom,
~ p(n5,n4,n3) ).
cnf(u32385,axiom,
~ p(n4,n6,n3) ).
cnf(u32389,axiom,
~ p(n4,n5,n3) ).
cnf(u32393,axiom,
~ p(n4,n4,n3) ).
cnf(u32398,axiom,
~ p(n6,n6,n2) ).
cnf(u32402,axiom,
~ p(n6,n5,n2) ).
cnf(u32406,axiom,
~ p(n6,n4,n2) ).
cnf(u32410,axiom,
~ p(n5,n6,n2) ).
cnf(u32414,axiom,
~ p(n5,n5,n2) ).
cnf(u32418,axiom,
~ p(n5,n4,n2) ).
cnf(u32422,axiom,
~ p(n4,n6,n2) ).
cnf(u32426,axiom,
~ p(n4,n5,n2) ).
cnf(u32431,axiom,
p(n4,n4,n2) ).
cnf(u32435,axiom,
~ p(n6,n6,n1) ).
cnf(u32439,axiom,
~ p(n6,n5,n1) ).
cnf(u32443,axiom,
~ p(n6,n4,n1) ).
cnf(u32447,axiom,
~ p(n5,n6,n1) ).
cnf(u32451,axiom,
~ p(n5,n5,n1) ).
cnf(u32455,axiom,
~ p(n5,n4,n1) ).
cnf(u32460,axiom,
p(n4,n6,n1) ).
cnf(u32463,axiom,
~ p(n4,n5,n1) ).
cnf(u32467,axiom,
~ p(n4,n4,n1) ).
cnf(u32472,axiom,
~ p(n6,n3,n8) ).
cnf(u32476,axiom,
~ p(n6,n2,n8) ).
cnf(u32480,axiom,
~ p(n6,n1,n8) ).
cnf(u32484,axiom,
~ p(n5,n3,n8) ).
cnf(u32488,axiom,
~ p(n5,n2,n8) ).
cnf(u32492,axiom,
~ p(n5,n1,n8) ).
cnf(u32497,axiom,
p(n4,n3,n8) ).
cnf(u32500,axiom,
~ p(n4,n2,n8) ).
cnf(u32504,axiom,
~ p(n4,n1,n8) ).
cnf(u32509,axiom,
~ p(n6,n3,n6) ).
cnf(u32513,axiom,
~ p(n6,n2,n6) ).
cnf(u32517,axiom,
~ p(n6,n1,n6) ).
cnf(u32521,axiom,
~ p(n5,n3,n6) ).
cnf(u32526,axiom,
p(n5,n2,n6) ).
cnf(u32529,axiom,
~ p(n5,n1,n6) ).
cnf(u32533,axiom,
~ p(n4,n3,n6) ).
cnf(u32537,axiom,
~ p(n4,n2,n6) ).
cnf(u32541,axiom,
~ p(n4,n1,n6) ).
cnf(u32546,axiom,
~ p(n6,n3,n5) ).
cnf(u32550,axiom,
~ p(n6,n2,n5) ).
cnf(u32554,axiom,
~ p(n6,n1,n5) ).
cnf(u32558,axiom,
~ p(n5,n3,n5) ).
cnf(u32562,axiom,
~ p(n5,n2,n5) ).
cnf(u32567,axiom,
p(n5,n1,n5) ).
cnf(u32570,axiom,
~ p(n4,n3,n5) ).
cnf(u32574,axiom,
~ p(n4,n2,n5) ).
cnf(u32578,axiom,
~ p(n4,n1,n5) ).
cnf(u32584,axiom,
p(n6,n3,n2) ).
cnf(u32587,axiom,
~ p(n6,n2,n2) ).
cnf(u32591,axiom,
~ p(n6,n1,n2) ).
cnf(u32595,axiom,
~ p(n5,n3,n2) ).
cnf(u32599,axiom,
~ p(n5,n2,n2) ).
cnf(u32603,axiom,
~ p(n5,n1,n2) ).
cnf(u32607,axiom,
~ p(n4,n3,n2) ).
cnf(u32611,axiom,
~ p(n4,n2,n2) ).
cnf(u32615,axiom,
~ p(n4,n1,n2) ).
cnf(u32620,axiom,
~ p(n3,n9,n8) ).
cnf(u32624,axiom,
~ p(n3,n8,n8) ).
cnf(u32628,axiom,
~ p(n3,n7,n8) ).
cnf(u32632,axiom,
~ p(n2,n9,n8) ).
cnf(u32636,axiom,
~ p(n2,n8,n8) ).
cnf(u32641,axiom,
p(n2,n7,n8) ).
cnf(u32644,axiom,
~ p(n1,n9,n8) ).
cnf(u32648,axiom,
~ p(n1,n8,n8) ).
cnf(u32652,axiom,
~ p(n1,n7,n8) ).
cnf(u32657,axiom,
~ p(n3,n9,n7) ).
cnf(u32661,axiom,
~ p(n3,n8,n7) ).
cnf(u32665,axiom,
~ p(n3,n7,n7) ).
cnf(u32669,axiom,
~ p(n2,n9,n7) ).
cnf(u32673,axiom,
~ p(n2,n8,n7) ).
cnf(u32677,axiom,
~ p(n2,n7,n7) ).
cnf(u32681,axiom,
~ p(n1,n9,n7) ).
cnf(u32685,axiom,
~ p(n1,n8,n7) ).
cnf(u32690,axiom,
p(n1,n7,n7) ).
cnf(u32695,axiom,
p(n3,n9,n6) ).
cnf(u32698,axiom,
~ p(n3,n8,n6) ).
cnf(u32702,axiom,
~ p(n3,n7,n6) ).
cnf(u32706,axiom,
~ p(n2,n9,n6) ).
cnf(u32710,axiom,
~ p(n2,n8,n6) ).
cnf(u32714,axiom,
~ p(n2,n7,n6) ).
cnf(u32718,axiom,
~ p(n1,n9,n6) ).
cnf(u32722,axiom,
~ p(n1,n8,n6) ).
cnf(u32726,axiom,
~ p(n1,n7,n6) ).
cnf(u32731,axiom,
~ p(n3,n9,n4) ).
cnf(u32735,axiom,
~ p(n3,n8,n4) ).
cnf(u32739,axiom,
~ p(n3,n7,n4) ).
cnf(u32743,axiom,
~ p(n2,n9,n4) ).
cnf(u32748,axiom,
p(n2,n8,n4) ).
cnf(u32751,axiom,
~ p(n2,n7,n4) ).
cnf(u32755,axiom,
~ p(n1,n9,n4) ).
cnf(u32759,axiom,
~ p(n1,n8,n4) ).
cnf(u32763,axiom,
~ p(n1,n7,n4) ).
cnf(u32768,axiom,
~ p(n3,n9,n3) ).
cnf(u32772,axiom,
~ p(n3,n8,n3) ).
cnf(u32776,axiom,
~ p(n3,n7,n3) ).
cnf(u32780,axiom,
~ p(n2,n9,n3) ).
cnf(u32784,axiom,
~ p(n2,n8,n3) ).
cnf(u32788,axiom,
~ p(n2,n7,n3) ).
cnf(u32792,axiom,
~ p(n1,n9,n3) ).
cnf(u32797,axiom,
p(n1,n8,n3) ).
cnf(u32800,axiom,
~ p(n1,n7,n3) ).
cnf(u32805,axiom,
~ p(n3,n9,n2) ).
cnf(u32809,axiom,
~ p(n3,n8,n2) ).
cnf(u32813,axiom,
~ p(n3,n7,n2) ).
cnf(u32818,axiom,
p(n2,n9,n2) ).
cnf(u32821,axiom,
~ p(n2,n8,n2) ).
cnf(u32825,axiom,
~ p(n2,n7,n2) ).
cnf(u32829,axiom,
~ p(n1,n9,n2) ).
cnf(u32833,axiom,
~ p(n1,n8,n2) ).
cnf(u32837,axiom,
~ p(n1,n7,n2) ).
cnf(u32842,axiom,
~ p(n3,n9,n1) ).
cnf(u32847,axiom,
p(n3,n8,n1) ).
cnf(u32850,axiom,
~ p(n3,n7,n1) ).
cnf(u32854,axiom,
~ p(n2,n9,n1) ).
cnf(u32858,axiom,
~ p(n2,n8,n1) ).
cnf(u32862,axiom,
~ p(n2,n7,n1) ).
cnf(u32866,axiom,
~ p(n1,n9,n1) ).
cnf(u32870,axiom,
~ p(n1,n8,n1) ).
cnf(u32874,axiom,
~ p(n1,n7,n1) ).
cnf(u32879,axiom,
~ p(n3,n6,n8) ).
cnf(u32883,axiom,
~ p(n3,n5,n8) ).
cnf(u32887,axiom,
~ p(n3,n4,n8) ).
cnf(u32891,axiom,
~ p(n2,n6,n8) ).
cnf(u32895,axiom,
~ p(n2,n5,n8) ).
cnf(u32899,axiom,
~ p(n2,n4,n8) ).
cnf(u32903,axiom,
~ p(n1,n6,n8) ).
cnf(u32908,axiom,
p(n1,n5,n8) ).
cnf(u32911,axiom,
~ p(n1,n4,n8) ).
cnf(u32916,axiom,
~ p(n3,n6,n3) ).
cnf(u32920,axiom,
~ p(n3,n5,n3) ).
cnf(u32925,axiom,
p(n3,n4,n3) ).
cnf(u32928,axiom,
~ p(n2,n6,n3) ).
cnf(u32932,axiom,
~ p(n2,n5,n3) ).
cnf(u32936,axiom,
~ p(n2,n4,n3) ).
cnf(u32940,axiom,
~ p(n1,n6,n3) ).
cnf(u32944,axiom,
~ p(n1,n5,n3) ).
cnf(u32948,axiom,
~ p(n1,n4,n3) ).
cnf(u32954,axiom,
p(n3,n6,n2) ).
cnf(u32957,axiom,
~ p(n3,n5,n2) ).
cnf(u32961,axiom,
~ p(n3,n4,n2) ).
cnf(u32965,axiom,
~ p(n2,n6,n2) ).
cnf(u32969,axiom,
~ p(n2,n5,n2) ).
cnf(u32973,axiom,
~ p(n2,n4,n2) ).
cnf(u32977,axiom,
~ p(n1,n6,n2) ).
cnf(u32981,axiom,
~ p(n1,n5,n2) ).
cnf(u32985,axiom,
~ p(n1,n4,n2) ).
cnf(u32990,axiom,
~ p(n3,n6,n1) ).
cnf(u32994,axiom,
~ p(n3,n5,n1) ).
cnf(u32998,axiom,
~ p(n3,n4,n1) ).
cnf(u33002,axiom,
~ p(n2,n6,n1) ).
cnf(u33007,axiom,
p(n2,n5,n1) ).
cnf(u33010,axiom,
~ p(n2,n4,n1) ).
cnf(u33014,axiom,
~ p(n1,n6,n1) ).
cnf(u33018,axiom,
~ p(n1,n5,n1) ).
cnf(u33022,axiom,
~ p(n1,n4,n1) ).
cnf(u33027,axiom,
~ p(n3,n3,n9) ).
cnf(u33031,axiom,
~ p(n3,n2,n9) ).
cnf(u33035,axiom,
~ p(n3,n1,n9) ).
cnf(u33039,axiom,
~ p(n2,n3,n9) ).
cnf(u33044,axiom,
p(n2,n2,n9) ).
cnf(u33047,axiom,
~ p(n2,n1,n9) ).
cnf(u33051,axiom,
~ p(n1,n3,n9) ).
cnf(u33055,axiom,
~ p(n1,n2,n9) ).
cnf(u33059,axiom,
~ p(n1,n1,n9) ).
cnf(u33064,axiom,
~ p(n3,n3,n8) ).
cnf(u33069,axiom,
p(n3,n2,n8) ).
cnf(u33072,axiom,
~ p(n3,n1,n8) ).
cnf(u33076,axiom,
~ p(n2,n3,n8) ).
cnf(u33080,axiom,
~ p(n2,n2,n8) ).
cnf(u33084,axiom,
~ p(n2,n1,n8) ).
cnf(u33088,axiom,
~ p(n1,n3,n8) ).
cnf(u33092,axiom,
~ p(n1,n2,n8) ).
cnf(u33096,axiom,
~ p(n1,n1,n8) ).
cnf(u33101,axiom,
~ p(n3,n3,n7) ).
cnf(u33105,axiom,
~ p(n3,n2,n7) ).
cnf(u33110,axiom,
p(n3,n1,n7) ).
cnf(u33113,axiom,
~ p(n2,n3,n7) ).
cnf(u33117,axiom,
~ p(n2,n2,n7) ).
cnf(u33121,axiom,
~ p(n2,n1,n7) ).
cnf(u33125,axiom,
~ p(n1,n3,n7) ).
cnf(u33129,axiom,
~ p(n1,n2,n7) ).
cnf(u33133,axiom,
~ p(n1,n1,n7) ).
cnf(u33138,axiom,
~ p(n3,n3,n6) ).
cnf(u33142,axiom,
~ p(n3,n2,n6) ).
cnf(u33146,axiom,
~ p(n3,n1,n6) ).
cnf(u33151,axiom,
p(n2,n3,n6) ).
cnf(u33154,axiom,
~ p(n2,n2,n6) ).
cnf(u33158,axiom,
~ p(n2,n1,n6) ).
cnf(u33162,axiom,
~ p(n1,n3,n6) ).
cnf(u33166,axiom,
~ p(n1,n2,n6) ).
cnf(u33170,axiom,
~ p(n1,n1,n6) ).
cnf(u33175,axiom,
~ p(n3,n3,n5) ).
cnf(u33179,axiom,
~ p(n3,n2,n5) ).
cnf(u33183,axiom,
~ p(n3,n1,n5) ).
cnf(u33187,axiom,
~ p(n2,n3,n5) ).
cnf(u33191,axiom,
~ p(n2,n2,n5) ).
cnf(u33195,axiom,
~ p(n2,n1,n5) ).
cnf(u33200,axiom,
p(n1,n3,n5) ).
cnf(u33203,axiom,
~ p(n1,n2,n5) ).
cnf(u33207,axiom,
~ p(n1,n1,n5) ).
cnf(u33212,axiom,
~ p(n3,n3,n3) ).
cnf(u33216,axiom,
~ p(n3,n2,n3) ).
cnf(u33220,axiom,
~ p(n3,n1,n3) ).
cnf(u33224,axiom,
~ p(n2,n3,n3) ).
cnf(u33228,axiom,
~ p(n2,n2,n3) ).
cnf(u33233,axiom,
p(n2,n1,n3) ).
cnf(u33236,axiom,
~ p(n1,n3,n3) ).
cnf(u33240,axiom,
~ p(n1,n2,n3) ).
cnf(u33244,axiom,
~ p(n1,n1,n3) ).
cnf(u33249,axiom,
~ p(n3,n3,n2) ).
cnf(u33253,axiom,
~ p(n3,n2,n2) ).
cnf(u33257,axiom,
~ p(n3,n1,n2) ).
cnf(u33261,axiom,
~ p(n2,n3,n2) ).
cnf(u33265,axiom,
~ p(n2,n2,n2) ).
cnf(u33269,axiom,
~ p(n2,n1,n2) ).
cnf(u33273,axiom,
~ p(n1,n3,n2) ).
cnf(u33278,axiom,
p(n1,n2,n2) ).
cnf(u33281,axiom,
~ p(n1,n1,n2) ).
cnf(u33286,axiom,
~ p(n9,n8,n4) ).
cnf(u33290,axiom,
~ p(n9,n8,n2) ).
cnf(u33295,axiom,
~ p(n9,n7,n4) ).
cnf(u33299,axiom,
~ p(n9,n7,n2) ).
cnf(u33304,axiom,
~ p(n9,n5,n9) ).
cnf(u33308,axiom,
~ p(n9,n5,n6) ).
cnf(u33312,axiom,
~ p(n9,n5,n5) ).
cnf(u33316,axiom,
~ p(n9,n5,n3) ).
cnf(u33320,axiom,
~ p(n9,n5,n1) ).
cnf(u33325,axiom,
~ p(n9,n3,n7) ).
cnf(u33329,axiom,
~ p(n9,n3,n2) ).
cnf(u33334,axiom,
~ p(n9,n2,n7) ).
cnf(u33338,axiom,
~ p(n9,n2,n2) ).
cnf(u33343,axiom,
~ p(n8,n9,n4) ).
cnf(u33347,axiom,
~ p(n8,n9,n2) ).
cnf(u33352,axiom,
~ p(n8,n8,n4) ).
cnf(u33356,axiom,
~ p(n8,n8,n2) ).
cnf(u33361,axiom,
~ p(n8,n7,n4) ).
cnf(u33365,axiom,
~ p(n8,n7,n2) ).
cnf(u33370,axiom,
~ p(n8,n5,n9) ).
cnf(u33374,axiom,
~ p(n8,n5,n6) ).
cnf(u33378,axiom,
~ p(n8,n5,n5) ).
cnf(u33382,axiom,
~ p(n8,n5,n3) ).
cnf(u33386,axiom,
~ p(n8,n5,n1) ).
cnf(u33391,axiom,
~ p(n8,n3,n7) ).
cnf(u33395,axiom,
~ p(n8,n3,n2) ).
cnf(u33400,axiom,
~ p(n8,n2,n7) ).
cnf(u33404,axiom,
~ p(n8,n2,n2) ).
cnf(u33409,axiom,
~ p(n8,n1,n7) ).
cnf(u33413,axiom,
~ p(n8,n1,n2) ).
cnf(u33418,axiom,
~ p(n7,n9,n4) ).
cnf(u33422,axiom,
~ p(n7,n9,n2) ).
cnf(u33427,axiom,
~ p(n7,n8,n4) ).
cnf(u33431,axiom,
~ p(n7,n8,n2) ).
cnf(u33436,axiom,
~ p(n7,n6,n9) ).
cnf(u33440,axiom,
~ p(n7,n6,n6) ).
cnf(u33444,axiom,
~ p(n7,n6,n5) ).
cnf(u33448,axiom,
~ p(n7,n6,n3) ).
cnf(u33452,axiom,
~ p(n7,n6,n1) ).
cnf(u33457,axiom,
~ p(n7,n4,n9) ).
cnf(u33461,axiom,
~ p(n7,n4,n6) ).
cnf(u33465,axiom,
~ p(n7,n4,n5) ).
cnf(u33469,axiom,
~ p(n7,n4,n3) ).
cnf(u33473,axiom,
~ p(n7,n4,n1) ).
cnf(u33478,axiom,
~ p(n7,n2,n7) ).
cnf(u33482,axiom,
~ p(n7,n2,n2) ).
cnf(u33487,axiom,
~ p(n7,n1,n7) ).
cnf(u33491,axiom,
~ p(n7,n1,n2) ).
cnf(u33496,axiom,
~ p(n6,n7,n8) ).
cnf(u33500,axiom,
~ p(n6,n7,n6) ).
cnf(u33504,axiom,
~ p(n6,n7,n5) ).
cnf(u33508,axiom,
~ p(n6,n7,n3) ).
cnf(u33512,axiom,
~ p(n6,n7,n1) ).
cnf(u33520,axiom,
~ p(n6,n3,n9) ).
cnf(u33524,axiom,
~ p(n6,n3,n7) ).
cnf(u33528,axiom,
~ p(n6,n3,n4) ).
cnf(u33532,axiom,
~ p(n6,n3,n3) ).
cnf(u33536,axiom,
~ p(n6,n3,n1) ).
cnf(u33541,axiom,
~ p(n5,n9,n8) ).
cnf(u33545,axiom,
~ p(n5,n9,n6) ).
cnf(u33549,axiom,
~ p(n5,n9,n5) ).
cnf(u33553,axiom,
~ p(n5,n9,n3) ).
cnf(u33557,axiom,
~ p(n5,n9,n1) ).
cnf(u33562,axiom,
~ p(n5,n8,n8) ).
cnf(u33566,axiom,
~ p(n5,n8,n6) ).
cnf(u33570,axiom,
~ p(n5,n8,n5) ).
cnf(u33574,axiom,
~ p(n5,n8,n3) ).
cnf(u33578,axiom,
~ p(n5,n8,n1) ).
cnf(u33586,axiom,
~ p(n5,n2,n9) ).
cnf(u33590,axiom,
~ p(n5,n2,n7) ).
cnf(u33594,axiom,
~ p(n5,n2,n4) ).
cnf(u33598,axiom,
~ p(n5,n2,n3) ).
cnf(u33602,axiom,
~ p(n5,n2,n1) ).
cnf(u33607,axiom,
~ p(n5,n1,n9) ).
cnf(u33611,axiom,
~ p(n5,n1,n7) ).
cnf(u33615,axiom,
~ p(n5,n1,n4) ).
cnf(u33619,axiom,
~ p(n5,n1,n3) ).
cnf(u33623,axiom,
~ p(n5,n1,n1) ).
cnf(u33628,axiom,
~ p(n4,n7,n8) ).
cnf(u33632,axiom,
~ p(n4,n7,n6) ).
cnf(u33636,axiom,
~ p(n4,n7,n5) ).
cnf(u33640,axiom,
~ p(n4,n7,n3) ).
cnf(u33644,axiom,
~ p(n4,n7,n1) ).
cnf(u33652,axiom,
~ p(n4,n3,n9) ).
cnf(u33656,axiom,
~ p(n4,n3,n7) ).
cnf(u33660,axiom,
~ p(n4,n3,n4) ).
cnf(u33664,axiom,
~ p(n4,n3,n3) ).
cnf(u33668,axiom,
~ p(n4,n3,n1) ).
cnf(u33673,axiom,
~ p(n3,n9,n9) ).
cnf(u33677,axiom,
~ p(n3,n9,n5) ).
cnf(u33682,axiom,
~ p(n3,n8,n9) ).
cnf(u33686,axiom,
~ p(n3,n8,n5) ).
cnf(u33691,axiom,
~ p(n3,n6,n9) ).
cnf(u33695,axiom,
~ p(n3,n6,n7) ).
cnf(u33699,axiom,
~ p(n3,n6,n6) ).
cnf(u33703,axiom,
~ p(n3,n6,n5) ).
cnf(u33707,axiom,
~ p(n3,n6,n4) ).
cnf(u33712,axiom,
~ p(n3,n4,n9) ).
cnf(u33716,axiom,
~ p(n3,n4,n7) ).
cnf(u33720,axiom,
~ p(n3,n4,n6) ).
cnf(u33724,axiom,
~ p(n3,n4,n5) ).
cnf(u33728,axiom,
~ p(n3,n4,n4) ).
cnf(u33733,axiom,
~ p(n3,n2,n4) ).
cnf(u33737,axiom,
~ p(n3,n2,n1) ).
cnf(u33742,axiom,
~ p(n3,n1,n4) ).
cnf(u33746,axiom,
~ p(n3,n1,n1) ).
cnf(u33751,axiom,
~ p(n2,n9,n9) ).
cnf(u33755,axiom,
~ p(n2,n9,n5) ).
cnf(u33760,axiom,
~ p(n2,n8,n9) ).
cnf(u33764,axiom,
~ p(n2,n8,n5) ).
cnf(u33769,axiom,
~ p(n2,n7,n9) ).
cnf(u33773,axiom,
~ p(n2,n7,n5) ).
cnf(u33778,axiom,
~ p(n2,n5,n9) ).
cnf(u33782,axiom,
~ p(n2,n5,n7) ).
cnf(u33786,axiom,
~ p(n2,n5,n6) ).
cnf(u33790,axiom,
~ p(n2,n5,n5) ).
cnf(u33794,axiom,
~ p(n2,n5,n4) ).
cnf(u33799,axiom,
~ p(n2,n3,n4) ).
cnf(u33803,axiom,
~ p(n2,n3,n1) ).
cnf(u33808,axiom,
~ p(n2,n2,n4) ).
cnf(u33812,axiom,
~ p(n2,n2,n1) ).
cnf(u33817,axiom,
~ p(n2,n1,n4) ).
cnf(u33821,axiom,
~ p(n2,n1,n1) ).
cnf(u33826,axiom,
~ p(n1,n8,n9) ).
cnf(u33830,axiom,
~ p(n1,n8,n5) ).
cnf(u33835,axiom,
~ p(n1,n7,n9) ).
cnf(u33839,axiom,
~ p(n1,n7,n5) ).
cnf(u33844,axiom,
~ p(n1,n5,n9) ).
cnf(u33848,axiom,
~ p(n1,n5,n7) ).
cnf(u33852,axiom,
~ p(n1,n5,n6) ).
cnf(u33856,axiom,
~ p(n1,n5,n5) ).
cnf(u33860,axiom,
~ p(n1,n5,n4) ).
cnf(u33865,axiom,
~ p(n1,n3,n4) ).
cnf(u33869,axiom,
~ p(n1,n3,n1) ).
cnf(u33874,axiom,
~ p(n1,n2,n4) ).
cnf(u33878,axiom,
~ p(n1,n2,n1) ).
cnf(u33884,axiom,
~ p(n6,n9,n6) ).
cnf(u33888,axiom,
~ p(n4,n9,n6) ).
cnf(u33893,axiom,
~ p(n6,n9,n5) ).
cnf(u33897,axiom,
~ p(n4,n9,n5) ).
cnf(u33901,axiom,
~ p(n1,n9,n5) ).
cnf(u33906,axiom,
~ p(n9,n9,n2) ).
cnf(u33911,axiom,
~ p(n6,n9,n1) ).
cnf(u33915,axiom,
~ p(n4,n9,n1) ).
cnf(u33921,axiom,
~ p(n6,n8,n8) ).
cnf(u33925,axiom,
~ p(n4,n8,n8) ).
cnf(u33932,axiom,
~ p(n6,n8,n3) ).
cnf(u33936,axiom,
~ p(n4,n8,n3) ).
cnf(u33942,axiom,
~ p(n6,n8,n1) ).
cnf(u33946,axiom,
~ p(n4,n8,n1) ).
cnf(u33951,axiom,
~ p(n3,n7,n9) ).
cnf(u33956,axiom,
~ p(n5,n7,n8) ).
cnf(u33962,axiom,
~ p(n5,n7,n6) ).
cnf(u33967,axiom,
~ p(n7,n7,n4) ).
cnf(u33972,axiom,
~ p(n5,n7,n3) ).
cnf(u33977,axiom,
~ p(n9,n6,n9) ).
cnf(u33981,axiom,
~ p(n8,n6,n9) ).
cnf(u33985,axiom,
~ p(n2,n6,n9) ).
cnf(u33989,axiom,
~ p(n1,n6,n9) ).
cnf(u33995,axiom,
~ p(n9,n6,n5) ).
cnf(u33999,axiom,
~ p(n8,n6,n5) ).
cnf(u34003,axiom,
~ p(n2,n6,n5) ).
cnf(u34007,axiom,
~ p(n1,n6,n5) ).
cnf(u34013,axiom,
~ p(n9,n6,n1) ).
cnf(u34017,axiom,
~ p(n8,n6,n1) ).
cnf(u34023,axiom,
~ p(n3,n5,n7) ).
cnf(u34028,axiom,
~ p(n7,n5,n6) ).
cnf(u34032,axiom,
~ p(n3,n5,n6) ).
cnf(u34037,axiom,
~ p(n3,n5,n4) ).
cnf(u34042,axiom,
~ p(n7,n5,n3) ).
cnf(u34048,axiom,
~ p(n7,n5,n1) ).
cnf(u34054,axiom,
~ p(n2,n4,n7) ).
cnf(u34058,axiom,
~ p(n1,n4,n7) ).
cnf(u34063,axiom,
~ p(n2,n4,n4) ).
cnf(u34067,axiom,
~ p(n1,n4,n4) ).
cnf(u34072,axiom,
~ p(n9,n4,n3) ).
cnf(u34076,axiom,
~ p(n8,n4,n3) ).
cnf(u34082,axiom,
~ p(n5,n3,n9) ).
cnf(u34090,axiom,
~ p(n7,n3,n2) ).
cnf(u34095,axiom,
~ p(n5,n3,n1) ).
cnf(u34099,axiom,
~ p(n3,n3,n1) ).
cnf(u34104,axiom,
~ p(n6,n2,n9) ).
cnf(u34108,axiom,
~ p(n4,n2,n9) ).
cnf(u34116,axiom,
~ p(n6,n2,n4) ).
cnf(u34120,axiom,
~ p(n4,n2,n4) ).
cnf(u34125,axiom,
~ p(n6,n2,n3) ).
cnf(u34129,axiom,
~ p(n4,n2,n3) ).
cnf(u34136,axiom,
~ p(n9,n1,n7) ).
cnf(u34140,axiom,
~ p(n6,n1,n7) ).
cnf(u34144,axiom,
~ p(n4,n1,n7) ).
cnf(u34151,axiom,
~ p(n6,n1,n3) ).
cnf(u34155,axiom,
~ p(n4,n1,n3) ).
cnf(u34160,axiom,
~ p(n9,n4,n9) ).
cnf(u34167,axiom,
~ p(n9,n4,n5) ).
cnf(u34172,axiom,
~ p(n9,n6,n3) ).
cnf(u34179,axiom,
~ p(n8,n6,n6) ).
cnf(u34183,axiom,
~ p(n8,n4,n6) ).
cnf(u34188,axiom,
~ p(n8,n4,n5) ).
cnf(u34195,axiom,
~ p(n8,n4,n1) ).
cnf(u34200,axiom,
~ p(n7,n5,n9) ).
cnf(u34210,axiom,
~ p(n6,n2,n7) ).
cnf(u34215,axiom,
~ p(n6,n8,n5) ).
cnf(u34220,axiom,
~ p(n6,n1,n4) ).
cnf(u34225,axiom,
~ p(n6,n9,n3) ).
cnf(u34233,axiom,
~ p(n5,n3,n7) ).
cnf(u34239,axiom,
~ p(n5,n7,n5) ).
cnf(u34244,axiom,
~ p(n5,n3,n4) ).
cnf(u34250,axiom,
~ p(n4,n1,n9) ).
cnf(u34255,axiom,
~ p(n4,n9,n8) ).
cnf(u34260,axiom,
~ p(n4,n8,n6) ).
cnf(u34266,axiom,
~ p(n4,n2,n1) ).
cnf(u34270,axiom,
~ p(n4,n1,n1) ).
cnf(u34281,axiom,
~ p(n2,n4,n9) ).
cnf(u34287,axiom,
~ p(n2,n6,n6) ).
cnf(u34291,axiom,
~ p(n2,n4,n6) ).
cnf(u34296,axiom,
~ p(n2,n6,n4) ).
cnf(u34305,axiom,
~ p(n1,n6,n7) ).
cnf(u34310,axiom,
~ p(n1,n4,n5) ).
cnf(u34492,axiom,
~ p(n9,n4,n6) ).
cnf(u35149,axiom,
~ p(n6,n1,n1) ).
cnf(u35464,axiom,
~ p(n3,n5,n5) ).
cnf(u35521,axiom,
~ p(n1,n6,n6) ).
cnf(u35594,axiom,
~ p(n1,n4,n9) ).
cnf(u35774,axiom,
~ p(n1,n1,n4) ).
cnf(u31319,axiom,
p(n9,n1,n2) ).
cnf(u31312,axiom,
p(n6,n8,n6) ).
cnf(u31305,axiom,
p(n4,n2,n7) ).
cnf(u31311,axiom,
p(n6,n2,n1) ).
cnf(u31296,axiom,
p(n1,n4,n6) ).
cnf(u31317,axiom,
p(n8,n4,n9) ).
cnf(u31297,axiom,
p(n1,n6,n4) ).
cnf(u31309,axiom,
p(n5,n7,n1) ).
cnf(u31302,axiom,
p(n3,n5,n9) ).
cnf(u31318,axiom,
p(n8,n6,n3) ).
cnf(u31301,axiom,
p(n3,n3,n4) ).
cnf(u31316,axiom,
p(n7,n7,n2) ).
cnf(u31310,axiom,
p(n6,n1,n9) ).
cnf(u31320,axiom,
p(n9,n4,n1) ).
cnf(u31303,axiom,
p(n3,n7,n5) ).
cnf(u31321,axiom,
p(n9,n6,n6) ).
cnf(u31314,axiom,
p(n7,n3,n7) ).
cnf(u31304,axiom,
p(n4,n1,n4) ).
cnf(u31295,axiom,
p(n1,n1,n1) ).
cnf(u31300,axiom,
p(n2,n6,n7) ).
cnf(u31306,axiom,
p(n4,n8,n5) ).
cnf(u31315,axiom,
p(n7,n5,n5) ).
cnf(u31322,axiom,
p(n9,n9,n4) ).
cnf(u31307,axiom,
p(n4,n9,n3) ).
cnf(u31298,axiom,
p(n1,n9,n9) ).
cnf(u31299,axiom,
p(n2,n4,n5) ).
cnf(u31308,axiom,
p(n5,n3,n3) ).
cnf(u31313,axiom,
p(n6,n9,n8) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ079+2 : TPTP v9.3.1. Bugfixed v5.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n017.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 22:35:35 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.16/0.42 Running first-order theorem proving
% 0.16/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.16/1.56 % (3007734)Detected formulas, will run a generic FOF schedule.
% 5.16/1.56 % (3007822)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=4126320469:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.16/1.56 % (3007827)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3930347274:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.16/1.56 % (3007830)dis-21_1_sil=8000:lcm=predicate:random_seed=609348603:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 5.16/1.56 % (3007826)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3158514055:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.16/1.56 % (3007829)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1718008255:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.16/1.56 % (3007825)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2222290037:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.16/1.56 % (3007823)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2606301473:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.16/1.56 % (3007827)Refutation not found, incomplete strategy
% 5.16/1.56 % (3007827)------------------------------
% 5.16/1.56 % (3007827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.16/1.56 % (3007827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.16/1.56 % (3007827)CaDiCaL version: 2.1.3
% 5.16/1.56 % (3007827)Termination reason: Refutation not found, incomplete strategy
% 5.16/1.56 % (3007827)Time elapsed: 0.017 s
% 5.16/1.56 % (3007827)Peak memory usage: 90 MB
% 5.16/1.56 % (3007827)Instructions burned: 33 (million)
% 5.16/1.56 % (3007826)Refutation not found, incomplete strategy
% 5.16/1.56 % (3007826)------------------------------
% 5.16/1.56 % (3007826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.16/1.56 % (3007826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.16/1.56 % (3007826)CaDiCaL version: 2.1.3
% 5.16/1.56 % (3007826)Termination reason: Refutation not found, incomplete strategy
% 5.16/1.56 % (3007826)Time elapsed: 0.018 s
% 5.16/1.56 % (3007826)Peak memory usage: 90 MB
% 5.16/1.56 % (3007826)Instructions burned: 33 (million)
% 5.16/1.56 % (3007829)Instruction limit reached!
% 5.16/1.56 % (3007829)------------------------------
% 5.16/1.56 % (3007829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.16/1.56 % (3007829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.16/1.56 % (3007829)CaDiCaL version: 2.1.3
% 5.16/1.56 % (3007829)Termination reason: Instruction limit
% 5.16/1.56 % (3007829)Termination phase: Unused predicate definition removal
% 5.16/1.56 % (3007829)Time elapsed: 0.056 s
% 5.16/1.56 % (3007829)Peak memory usage: 89 MB
% 5.16/1.56 % (3007829)Instructions burned: 140 (million)
% 5.16/1.56 % (3007830)Instruction limit reached!
% 5.16/1.56 % (3007830)------------------------------
% 5.16/1.56 % (3007830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.16/1.56 % (3007830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.16/1.56 % (3007830)CaDiCaL version: 2.1.3
% 5.16/1.56 % (3007830)Termination reason: Instruction limit
% 5.16/1.56 % (3007830)Termination phase: Preprocessing 3
% 5.16/1.56 % (3007830)Time elapsed: 0.065 s
% 5.16/1.56 % (3007830)Peak memory usage: 91 MB
% 5.16/1.56 % (3007830)Instructions burned: 130 (million)
% 5.16/1.56 % (3007863)lrs+10_1_sil=8000:sp=occurrence:random_seed=1488018283:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 5.16/1.56 % (3007863)Refutation not found, incomplete strategy
% 5.16/1.56 % (3007863)------------------------------
% 5.16/1.56 % (3007863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.16/1.56 % (3007863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.16/1.56 % (3007863)CaDiCaL version: 2.1.3
% 5.16/1.56 % (3007863)Termination reason: Refutation not found, incomplete strategy
% 5.16/1.56 % (3007863)Time elapsed: 0.010 s
% 5.16/1.56 % (3007863)Peak memory usage: 91 MB
% 5.16/1.56 % (3007863)Instructions burned: 33 (million)
% 7.52/1.97 % (3007864)lrs+10_1_sil=32000:urr=on:br=off:random_seed=415192915:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 7.52/1.97 % (3007826)------------------------------
% 7.52/1.97 % (3007826)------------------------------
% 7.52/1.97 % (3007827)------------------------------
% 7.52/1.97 % (3007827)------------------------------
% 7.52/1.97 % (3007864)Refutation not found, incomplete strategy
% 7.52/1.97 % (3007864)------------------------------
% 7.52/1.97 % (3007864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.52/1.97 % (3007864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.52/1.97 % (3007864)CaDiCaL version: 2.1.3
% 7.52/1.97 % (3007864)Termination reason: Refutation not found, incomplete strategy
% 7.52/1.97 % (3007864)Time elapsed: 0.052 s
% 7.52/1.97 % (3007864)Peak memory usage: 91 MB
% 7.52/1.97 % (3007864)Instructions burned: 123 (million)
% 7.52/1.97 % (3007863)------------------------------
% 7.52/1.97 % (3007863)------------------------------
% 7.52/1.97 % (3007909)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1624074917:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 7.52/1.97 % (3007910)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1954256462:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 7.52/1.97 % (3007911)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3550901113:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 7.52/1.97 % (3007909)Refutation not found, incomplete strategy
% 7.52/1.97 % (3007909)------------------------------
% 7.52/1.97 % (3007909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.52/1.97 % (3007909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.52/1.97 % (3007909)CaDiCaL version: 2.1.3
% 7.52/1.97 % (3007909)Termination reason: Refutation not found, incomplete strategy
% 7.52/1.97 % (3007909)Time elapsed: 0.018 s
% 7.52/1.97 % (3007909)Peak memory usage: 91 MB
% 7.52/1.97 % (3007909)Instructions burned: 33 (million)
% 7.52/1.97 % (3007911)Refutation not found, incomplete strategy
% 7.52/1.97 % (3007911)------------------------------
% 7.52/1.97 % (3007911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.52/1.97 % (3007911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.52/1.97 % (3007911)CaDiCaL version: 2.1.3
% 7.52/1.97 % (3007911)Termination reason: Refutation not found, incomplete strategy
% 7.52/1.97 % (3007911)Time elapsed: 0.013 s
% 7.52/1.97 % (3007911)Peak memory usage: 91 MB
% 7.52/1.97 % (3007911)Instructions burned: 51 (million)
% 7.52/1.97 [W927 22:35:36.053907484 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.52/1.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.52/1.97 [W927 22:35:36.053952255 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.52/1.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.52/1.97 [W927 22:35:36.053989401 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.52/1.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.52/1.97 [W927 22:35:36.054010212 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.52/1.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.52/1.97 [W927 22:35:36.054040008 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.52/1.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.52/1.97 [W927 22:35:36.054051599 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.59/2.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.59/2.09 % (3007864)------------------------------
% 9.59/2.09 % (3007864)------------------------------
% 9.59/2.09 % (3007910)Instruction limit reached!
% 9.59/2.09 % (3007910)------------------------------
% 9.59/2.09 % (3007910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.59/2.09 % (3007910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.59/2.09 % (3007910)CaDiCaL version: 2.1.3
% 9.59/2.09 % (3007910)Termination reason: Instruction limit
% 9.59/2.09 % (3007910)Termination phase: Property scanning
% 9.59/2.09 % (3007910)Time elapsed: 0.112 s
% 9.59/2.09 % (3007910)Peak memory usage: 92 MB
% 9.59/2.09 % (3007910)Instructions burned: 249 (million)
% 9.59/2.09 [W927 22:35:36.085700084 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.59/2.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.59/2.09 [W927 22:35:36.085742871 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.59/2.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.59/2.09 [W927 22:35:36.085779648 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.59/2.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.59/2.09 [W927 22:35:36.085790621 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.59/2.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.59/2.09 [W927 22:35:36.085818745 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.59/2.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.59/2.09 [W927 22:35:36.085830411 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.59/2.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.59/2.09 % (3007911)------------------------------
% 9.59/2.09 % (3007911)------------------------------
% 9.59/2.09 % (3007915)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4109834768:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 9.59/2.09 % (3007916)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4009122612:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 9.59/2.09 % (3007909)------------------------------
% 9.59/2.09 % (3007909)------------------------------
% 9.59/2.09 % (3007917)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1996000227:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 9.59/2.09 % (3007916)Instruction limit reached!
% 9.59/2.09 % (3007916)------------------------------
% 9.59/2.09 % (3007916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.59/2.09 % (3007916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.59/2.09 % (3007916)CaDiCaL version: 2.1.3
% 9.59/2.09 % (3007916)Termination reason: Instruction limit
% 9.59/2.09 % (3007916)Termination phase: Preprocessing 3
% 9.59/2.09 % (3007916)Time elapsed: 0.062 s
% 9.59/2.09 % (3007916)Peak memory usage: 91 MB
% 9.59/2.09 % (3007916)Instructions burned: 114 (million)
% 9.59/2.09 % (3007917)Instruction limit reached!
% 9.59/2.09 % (3007917)------------------------------
% 9.59/2.09 % (3007917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.59/2.09 % (3007917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.59/2.09 % (3007917)CaDiCaL version: 2.1.3
% 9.59/2.09 % (3007917)Termination reason: Instruction limit
% 9.59/2.09 % (3007917)Termination phase: Property scanning
% 9.59/2.09 % (3007917)Time elapsed: 0.035 s
% 9.59/2.09 % (3007917)Peak memory usage: 92 MB
% 9.59/2.09 % (3007917)Instructions burned: 130 (million)
% 9.59/2.09 % (3007920)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2536192687:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 9.59/2.09 % (3007922)lrs+10_1_sil=8000:sp=occurrence:random_seed=4186616434:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 9.59/2.09 % (3007922)Refutation not found, incomplete strategy
% 9.59/2.09 % (3007922)------------------------------
% 9.59/2.09 % (3007922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.59/2.09 % (3007922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.59/2.09 % (3007922)CaDiCaL version: 2.1.3
% 9.59/2.09 % (3007922)Termination reason: Refutation not found, incomplete strategy
% 9.59/2.09 % (3007922)Time elapsed: 0.013 s
% 9.59/2.09 % (3007922)Peak memory usage: 91 MB
% 9.59/2.09 % (3007922)Instructions burned: 51 (million)
% 9.59/2.09 % (3007923)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3507489547:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 9.59/2.09 % (3007920)Instruction limit reached!
% 9.59/2.09 % (3007920)------------------------------
% 9.59/2.09 % (3007920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.59/2.09 % (3007920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.59/2.09 % (3007920)CaDiCaL version: 2.1.3
% 9.59/2.09 % (3007920)Termination reason: Instruction limit
% 9.59/2.09 % (3007920)Termination phase: SInE selection
% 9.59/2.09 % (3007920)Time elapsed: 0.043 s
% 9.59/2.09 % (3007920)Peak memory usage: 89 MB
% 9.59/2.09 % (3007920)Instructions burned: 116 (million)
% 9.59/2.09 % (3007825)Refutation not found, incomplete strategy
% 9.59/2.09 % (3007825)------------------------------
% 9.59/2.09 % (3007825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.59/2.09 % (3007825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.59/2.09 % (3007825)CaDiCaL version: 2.1.3
% 9.59/2.09 % (3007825)Termination reason: Refutation not found, incomplete strategy
% 9.59/2.09 % (3007825)Time elapsed: 0.920 s
% 9.59/2.09 % (3007825)Peak memory usage: 161 MB
% 9.59/2.09 % (3007825)Instructions burned: 1501 (million)
% 9.59/2.09 % (3007922)------------------------------
% 9.59/2.09 % (3007922)------------------------------
% 9.59/2.09 % (3007822)First to succeed.
% 9.59/2.09 % (3007822)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3007734"
% 9.59/2.09 % (3007923)Refutation not found, incomplete strategy
% 9.59/2.09 % (3007923)------------------------------
% 9.59/2.09 % (3007923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.59/2.09 % (3007923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.59/2.09 % (3007923)CaDiCaL version: 2.1.3
% 9.59/2.09 % (3007923)Termination reason: Refutation not found, incomplete strategy
% 9.59/2.09 % (3007923)Time elapsed: 0.145 s
% 9.59/2.09 % (3007923)Peak memory usage: 98 MB
% 9.59/2.09 % (3007923)Instructions burned: 307 (million)
% 9.59/2.09 % (3007927)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=903773593:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 9.59/2.09 % (3007928)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=337289962:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 9.59/2.09 % (3007928)Instruction limit reached!
% 9.59/2.09 % (3007928)------------------------------
% 9.59/2.09 % (3007928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.59/2.09 % (3007928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.59/2.09 % (3007928)CaDiCaL version: 2.1.3
% 9.59/2.09 % (3007928)Termination reason: Instruction limit
% 9.59/2.09 % (3007928)Termination phase: NewCNF
% 9.59/2.09 % (3007928)Time elapsed: 0.044 s
% 9.59/2.09 % (3007928)Peak memory usage: 94 MB
% 9.59/2.09 % (3007928)Instructions burned: 136 (million)
% 9.59/2.09 [W927 22:35:37.693753871 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.59/2.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.59/2.09 [W927 22:35:37.693785061 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.59/2.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.59/2.09 [W927 22:35:37.693824441 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.59/2.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.59/2.09 [W927 22:35:37.693835281 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.59/2.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.59/2.09 [W927 22:35:37.693862248 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.59/2.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.59/2.09 [W927 22:35:37.693872985 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.59/2.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.59/2.09 % (3007825)------------------------------
% 9.59/2.09 % (3007825)------------------------------
% 9.59/2.09 % (3007931)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1050182015:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 9.59/2.09 % (3007931)Refutation not found, incomplete strategy
% 9.59/2.09 % (3007931)------------------------------
% 9.59/2.09 % (3007931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.59/2.09 % (3007931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.59/2.09 % (3007931)CaDiCaL version: 2.1.3
% 9.59/2.09 % (3007931)Termination reason: Refutation not found, incomplete strategy
% 9.59/2.09 % (3007931)Time elapsed: 0.014 s
% 9.59/2.09 % (3007931)Peak memory usage: 91 MB
% 9.59/2.09 % (3007931)Instructions burned: 51 (million)
% 9.59/2.09 % (3007923)------------------------------
% 9.59/2.09 % (3007923)------------------------------
% 9.59/2.09 % SZS status Satisfiable for theBenchmark
% 9.59/2.09 % SZS output start Saturation.
% See solution above
% 10.17/2.29 % SZS output start Definitions and Model Updates.
% 10.17/2.29 % SZS output end Definitions and Model Updates.
% 10.17/2.29 % (3007822)------------------------------
% 10.17/2.29 % (3007822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.17/2.29 % (3007822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.17/2.29 % (3007822)CaDiCaL version: 2.1.3
% 10.17/2.29 % (3007822)Termination reason: Satisfiable
% 10.17/2.29 % (3007822)Time elapsed: 0.969 s
% 10.17/2.29 % (3007822)Peak memory usage: 162 MB
% 10.17/2.29 % (3007822)Instructions burned: 1581 (million)
% 10.17/2.29 % (3007822)------------------------------
% 10.17/2.29 % (3007822)------------------------------
% 10.17/2.29 % (3007734)Success in time 1.467 s
% 10.17/2.29 % Vampire exiting
%------------------------------------------------------------------------------