%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PUZ080+2 : TPTP v9.3.1. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n006.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.41s 2.47s
% Output : Saturation 10.76s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u31317,axiom,
~ p(n9,n9,n8) ).
cnf(u31321,axiom,
~ p(n9,n8,n8) ).
cnf(u31325,axiom,
~ p(n9,n7,n8) ).
cnf(u31329,axiom,
~ p(n8,n9,n8) ).
cnf(u31333,axiom,
~ p(n8,n8,n8) ).
cnf(u31337,axiom,
~ p(n8,n7,n8) ).
cnf(u31342,axiom,
p(n7,n9,n8) ).
cnf(u31345,axiom,
~ p(n7,n8,n8) ).
cnf(u31349,axiom,
~ p(n7,n7,n8) ).
cnf(u31355,axiom,
p(n9,n9,n6) ).
cnf(u31358,axiom,
~ p(n9,n8,n6) ).
cnf(u31362,axiom,
~ p(n9,n7,n6) ).
cnf(u31366,axiom,
~ p(n8,n9,n6) ).
cnf(u31370,axiom,
~ p(n8,n8,n6) ).
cnf(u31374,axiom,
~ p(n8,n7,n6) ).
cnf(u31378,axiom,
~ p(n7,n9,n6) ).
cnf(u31382,axiom,
~ p(n7,n8,n6) ).
cnf(u31386,axiom,
~ p(n7,n7,n6) ).
cnf(u31391,axiom,
~ p(n9,n9,n5) ).
cnf(u31396,axiom,
p(n9,n8,n5) ).
cnf(u31399,axiom,
~ p(n9,n7,n5) ).
cnf(u31403,axiom,
~ p(n8,n9,n5) ).
cnf(u31407,axiom,
~ p(n8,n8,n5) ).
cnf(u31411,axiom,
~ p(n8,n7,n5) ).
cnf(u31415,axiom,
~ p(n7,n9,n5) ).
cnf(u31419,axiom,
~ p(n7,n8,n5) ).
cnf(u31423,axiom,
~ p(n7,n7,n5) ).
cnf(u31428,axiom,
~ p(n9,n9,n4) ).
cnf(u31432,axiom,
~ p(n9,n8,n4) ).
cnf(u31436,axiom,
~ p(n9,n7,n4) ).
cnf(u31440,axiom,
~ p(n8,n9,n4) ).
cnf(u31444,axiom,
~ p(n8,n8,n4) ).
cnf(u31448,axiom,
~ p(n8,n7,n4) ).
cnf(u31452,axiom,
~ p(n7,n9,n4) ).
cnf(u31457,axiom,
p(n7,n8,n4) ).
cnf(u31460,axiom,
~ p(n7,n7,n4) ).
cnf(u31465,axiom,
~ p(n9,n9,n2) ).
cnf(u31469,axiom,
~ p(n9,n8,n2) ).
cnf(u31473,axiom,
~ p(n9,n7,n2) ).
cnf(u31477,axiom,
~ p(n8,n9,n2) ).
cnf(u31482,axiom,
p(n8,n8,n2) ).
cnf(u31485,axiom,
~ p(n8,n7,n2) ).
cnf(u31489,axiom,
~ p(n7,n9,n2) ).
cnf(u31493,axiom,
~ p(n7,n8,n2) ).
cnf(u31497,axiom,
~ p(n7,n7,n2) ).
cnf(u31503,axiom,
p(n9,n6,n9) ).
cnf(u31506,axiom,
~ p(n9,n5,n9) ).
cnf(u31510,axiom,
~ p(n9,n4,n9) ).
cnf(u31514,axiom,
~ p(n8,n6,n9) ).
cnf(u31518,axiom,
~ p(n8,n5,n9) ).
cnf(u31522,axiom,
~ p(n8,n4,n9) ).
cnf(u31526,axiom,
~ p(n7,n6,n9) ).
cnf(u31530,axiom,
~ p(n7,n5,n9) ).
cnf(u31534,axiom,
~ p(n7,n4,n9) ).
cnf(u31539,axiom,
~ p(n9,n6,n8) ).
cnf(u31543,axiom,
~ p(n9,n5,n8) ).
cnf(u31547,axiom,
~ p(n9,n4,n8) ).
cnf(u31552,axiom,
p(n8,n6,n8) ).
cnf(u31555,axiom,
~ p(n8,n5,n8) ).
cnf(u31559,axiom,
~ p(n8,n4,n8) ).
cnf(u31563,axiom,
~ p(n7,n6,n8) ).
cnf(u31567,axiom,
~ p(n7,n5,n8) ).
cnf(u31571,axiom,
~ p(n7,n4,n8) ).
cnf(u31576,axiom,
~ p(n9,n6,n6) ).
cnf(u31580,axiom,
~ p(n9,n5,n6) ).
cnf(u31584,axiom,
~ p(n9,n4,n6) ).
cnf(u31588,axiom,
~ p(n8,n6,n6) ).
cnf(u31593,axiom,
p(n8,n5,n6) ).
cnf(u31596,axiom,
~ p(n8,n4,n6) ).
cnf(u31600,axiom,
~ p(n7,n6,n6) ).
cnf(u31604,axiom,
~ p(n7,n5,n6) ).
cnf(u31608,axiom,
~ p(n7,n4,n6) ).
cnf(u31613,axiom,
~ p(n9,n6,n5) ).
cnf(u31617,axiom,
~ p(n9,n5,n5) ).
cnf(u31621,axiom,
~ p(n9,n4,n5) ).
cnf(u31625,axiom,
~ p(n8,n6,n5) ).
cnf(u31629,axiom,
~ p(n8,n5,n5) ).
cnf(u31634,axiom,
p(n8,n4,n5) ).
cnf(u31637,axiom,
~ p(n7,n6,n5) ).
cnf(u31641,axiom,
~ p(n7,n5,n5) ).
cnf(u31645,axiom,
~ p(n7,n4,n5) ).
cnf(u31650,axiom,
~ p(n9,n6,n4) ).
cnf(u31655,axiom,
p(n9,n5,n4) ).
cnf(u31658,axiom,
~ p(n9,n4,n4) ).
cnf(u31662,axiom,
~ p(n8,n6,n4) ).
cnf(u31666,axiom,
~ p(n8,n5,n4) ).
cnf(u31670,axiom,
~ p(n8,n4,n4) ).
cnf(u31674,axiom,
~ p(n7,n6,n4) ).
cnf(u31678,axiom,
~ p(n7,n5,n4) ).
cnf(u31682,axiom,
~ p(n7,n4,n4) ).
cnf(u31687,axiom,
~ p(n9,n6,n3) ).
cnf(u31691,axiom,
~ p(n9,n5,n3) ).
cnf(u31695,axiom,
~ p(n9,n4,n3) ).
cnf(u31699,axiom,
~ p(n8,n6,n3) ).
cnf(u31703,axiom,
~ p(n8,n5,n3) ).
cnf(u31707,axiom,
~ p(n8,n4,n3) ).
cnf(u31711,axiom,
~ p(n7,n6,n3) ).
cnf(u31716,axiom,
p(n7,n5,n3) ).
cnf(u31719,axiom,
~ p(n7,n4,n3) ).
cnf(u31724,axiom,
~ p(n9,n6,n1) ).
cnf(u31728,axiom,
~ p(n9,n5,n1) ).
cnf(u31733,axiom,
p(n9,n4,n1) ).
cnf(u31736,axiom,
~ p(n8,n6,n1) ).
cnf(u31740,axiom,
~ p(n8,n5,n1) ).
cnf(u31744,axiom,
~ p(n8,n4,n1) ).
cnf(u31748,axiom,
~ p(n7,n6,n1) ).
cnf(u31752,axiom,
~ p(n7,n5,n1) ).
cnf(u31756,axiom,
~ p(n7,n4,n1) ).
cnf(u31761,axiom,
~ p(n9,n3,n9) ).
cnf(u31765,axiom,
~ p(n9,n2,n9) ).
cnf(u31769,axiom,
~ p(n9,n1,n9) ).
cnf(u31773,axiom,
~ p(n8,n3,n9) ).
cnf(u31777,axiom,
~ p(n8,n2,n9) ).
cnf(u31781,axiom,
~ p(n8,n1,n9) ).
cnf(u31785,axiom,
~ p(n7,n3,n9) ).
cnf(u31790,axiom,
p(n7,n2,n9) ).
cnf(u31793,axiom,
~ p(n7,n1,n9) ).
cnf(u31798,axiom,
~ p(n9,n3,n7) ).
cnf(u31802,axiom,
~ p(n9,n2,n7) ).
cnf(u31807,axiom,
p(n9,n1,n7) ).
cnf(u31810,axiom,
~ p(n8,n3,n7) ).
cnf(u31814,axiom,
~ p(n8,n2,n7) ).
cnf(u31818,axiom,
~ p(n8,n1,n7) ).
cnf(u31822,axiom,
~ p(n7,n3,n7) ).
cnf(u31826,axiom,
~ p(n7,n2,n7) ).
cnf(u31830,axiom,
~ p(n7,n1,n7) ).
cnf(u31835,axiom,
~ p(n9,n3,n5) ).
cnf(u31839,axiom,
~ p(n9,n2,n5) ).
cnf(u31843,axiom,
~ p(n9,n1,n5) ).
cnf(u31847,axiom,
~ p(n8,n3,n5) ).
cnf(u31851,axiom,
~ p(n8,n2,n5) ).
cnf(u31855,axiom,
~ p(n8,n1,n5) ).
cnf(u31859,axiom,
~ p(n7,n3,n5) ).
cnf(u31863,axiom,
~ p(n7,n2,n5) ).
cnf(u31868,axiom,
p(n7,n1,n5) ).
cnf(u31872,axiom,
~ p(n9,n3,n4) ).
cnf(u31876,axiom,
~ p(n9,n2,n4) ).
cnf(u31880,axiom,
~ p(n9,n1,n4) ).
cnf(u31884,axiom,
~ p(n8,n3,n4) ).
cnf(u31889,axiom,
p(n8,n2,n4) ).
cnf(u31892,axiom,
~ p(n8,n1,n4) ).
cnf(u31896,axiom,
~ p(n7,n3,n4) ).
cnf(u31900,axiom,
~ p(n7,n2,n4) ).
cnf(u31904,axiom,
~ p(n7,n1,n4) ).
cnf(u31909,axiom,
~ p(n9,n3,n2) ).
cnf(u31914,axiom,
p(n9,n2,n2) ).
cnf(u31917,axiom,
~ p(n9,n1,n2) ).
cnf(u31921,axiom,
~ p(n8,n3,n2) ).
cnf(u31925,axiom,
~ p(n8,n2,n2) ).
cnf(u31929,axiom,
~ p(n8,n1,n2) ).
cnf(u31933,axiom,
~ p(n7,n3,n2) ).
cnf(u31937,axiom,
~ p(n7,n2,n2) ).
cnf(u31941,axiom,
~ p(n7,n1,n2) ).
cnf(u31946,axiom,
~ p(n6,n9,n9) ).
cnf(u31950,axiom,
~ p(n6,n8,n9) ).
cnf(u31954,axiom,
~ p(n6,n7,n9) ).
cnf(u31958,axiom,
~ p(n5,n9,n9) ).
cnf(u31963,axiom,
p(n5,n8,n9) ).
cnf(u31966,axiom,
~ p(n5,n7,n9) ).
cnf(u31970,axiom,
~ p(n4,n9,n9) ).
cnf(u31974,axiom,
~ p(n4,n8,n9) ).
cnf(u31978,axiom,
~ p(n4,n7,n9) ).
cnf(u31983,axiom,
~ p(n6,n9,n8) ).
cnf(u31988,axiom,
p(n6,n8,n8) ).
cnf(u31991,axiom,
~ p(n6,n7,n8) ).
cnf(u31995,axiom,
~ p(n5,n9,n8) ).
cnf(u31999,axiom,
~ p(n5,n8,n8) ).
cnf(u32003,axiom,
~ p(n5,n7,n8) ).
cnf(u32007,axiom,
~ p(n4,n9,n8) ).
cnf(u32011,axiom,
~ p(n4,n8,n8) ).
cnf(u32015,axiom,
~ p(n4,n7,n8) ).
cnf(u32020,axiom,
~ p(n6,n9,n7) ).
cnf(u32024,axiom,
~ p(n6,n8,n7) ).
cnf(u32028,axiom,
~ p(n6,n7,n7) ).
cnf(u32032,axiom,
~ p(n5,n9,n7) ).
cnf(u32036,axiom,
~ p(n5,n8,n7) ).
cnf(u32040,axiom,
~ p(n5,n7,n7) ).
cnf(u32044,axiom,
~ p(n4,n9,n7) ).
cnf(u32048,axiom,
~ p(n4,n8,n7) ).
cnf(u32053,axiom,
p(n4,n7,n7) ).
cnf(u32057,axiom,
~ p(n6,n9,n6) ).
cnf(u32061,axiom,
~ p(n6,n8,n6) ).
cnf(u32065,axiom,
~ p(n6,n7,n6) ).
cnf(u32069,axiom,
~ p(n5,n9,n6) ).
cnf(u32073,axiom,
~ p(n5,n8,n6) ).
cnf(u32078,axiom,
p(n5,n7,n6) ).
cnf(u32081,axiom,
~ p(n4,n9,n6) ).
cnf(u32085,axiom,
~ p(n4,n8,n6) ).
cnf(u32089,axiom,
~ p(n4,n7,n6) ).
cnf(u32095,axiom,
p(n6,n9,n5) ).
cnf(u32098,axiom,
~ p(n6,n8,n5) ).
cnf(u32102,axiom,
~ p(n6,n7,n5) ).
cnf(u32106,axiom,
~ p(n5,n9,n5) ).
cnf(u32110,axiom,
~ p(n5,n8,n5) ).
cnf(u32114,axiom,
~ p(n5,n7,n5) ).
cnf(u32118,axiom,
~ p(n4,n9,n5) ).
cnf(u32122,axiom,
~ p(n4,n8,n5) ).
cnf(u32126,axiom,
~ p(n4,n7,n5) ).
cnf(u32131,axiom,
~ p(n6,n9,n4) ).
cnf(u32135,axiom,
~ p(n6,n8,n4) ).
cnf(u32140,axiom,
p(n6,n7,n4) ).
cnf(u32143,axiom,
~ p(n5,n9,n4) ).
cnf(u32147,axiom,
~ p(n5,n8,n4) ).
cnf(u32151,axiom,
~ p(n5,n7,n4) ).
cnf(u32155,axiom,
~ p(n4,n9,n4) ).
cnf(u32159,axiom,
~ p(n4,n8,n4) ).
cnf(u32163,axiom,
~ p(n4,n7,n4) ).
cnf(u32168,axiom,
~ p(n6,n9,n3) ).
cnf(u32172,axiom,
~ p(n6,n8,n3) ).
cnf(u32176,axiom,
~ p(n6,n7,n3) ).
cnf(u32181,axiom,
p(n5,n9,n3) ).
cnf(u32184,axiom,
~ p(n5,n8,n3) ).
cnf(u32188,axiom,
~ p(n5,n7,n3) ).
cnf(u32192,axiom,
~ p(n4,n9,n3) ).
cnf(u32196,axiom,
~ p(n4,n8,n3) ).
cnf(u32200,axiom,
~ p(n4,n7,n3) ).
cnf(u32205,axiom,
~ p(n6,n9,n1) ).
cnf(u32209,axiom,
~ p(n6,n8,n1) ).
cnf(u32213,axiom,
~ p(n6,n7,n1) ).
cnf(u32217,axiom,
~ p(n5,n9,n1) ).
cnf(u32221,axiom,
~ p(n5,n8,n1) ).
cnf(u32225,axiom,
~ p(n5,n7,n1) ).
cnf(u32229,axiom,
~ p(n4,n9,n1) ).
cnf(u32234,axiom,
p(n4,n8,n1) ).
cnf(u32237,axiom,
~ p(n4,n7,n1) ).
cnf(u32242,axiom,
~ p(n6,n6,n9) ).
cnf(u32246,axiom,
~ p(n6,n5,n9) ).
cnf(u32251,axiom,
p(n6,n4,n9) ).
cnf(u32254,axiom,
~ p(n5,n6,n9) ).
cnf(u32258,axiom,
~ p(n5,n5,n9) ).
cnf(u32262,axiom,
~ p(n5,n4,n9) ).
cnf(u32266,axiom,
~ p(n4,n6,n9) ).
cnf(u32270,axiom,
~ p(n4,n5,n9) ).
cnf(u32274,axiom,
~ p(n4,n4,n9) ).
cnf(u32279,axiom,
~ p(n6,n6,n5) ).
cnf(u32283,axiom,
~ p(n6,n5,n5) ).
cnf(u32287,axiom,
~ p(n6,n4,n5) ).
cnf(u32291,axiom,
~ p(n5,n6,n5) ).
cnf(u32295,axiom,
~ p(n5,n5,n5) ).
cnf(u32299,axiom,
~ p(n5,n4,n5) ).
cnf(u32303,axiom,
~ p(n4,n6,n5) ).
cnf(u32308,axiom,
p(n4,n5,n5) ).
cnf(u32311,axiom,
~ p(n4,n4,n5) ).
cnf(u32317,axiom,
p(n6,n6,n3) ).
cnf(u32320,axiom,
~ p(n6,n5,n3) ).
cnf(u32324,axiom,
~ p(n6,n4,n3) ).
cnf(u32328,axiom,
~ p(n5,n6,n3) ).
cnf(u32332,axiom,
~ p(n5,n5,n3) ).
cnf(u32336,axiom,
~ p(n5,n4,n3) ).
cnf(u32340,axiom,
~ p(n4,n6,n3) ).
cnf(u32344,axiom,
~ p(n4,n5,n3) ).
cnf(u32348,axiom,
~ p(n4,n4,n3) ).
cnf(u32353,axiom,
~ p(n6,n6,n2) ).
cnf(u32357,axiom,
~ p(n6,n5,n2) ).
cnf(u32361,axiom,
~ p(n6,n4,n2) ).
cnf(u32365,axiom,
~ p(n5,n6,n2) ).
cnf(u32370,axiom,
p(n5,n5,n2) ).
cnf(u32373,axiom,
~ p(n5,n4,n2) ).
cnf(u32377,axiom,
~ p(n4,n6,n2) ).
cnf(u32381,axiom,
~ p(n4,n5,n2) ).
cnf(u32385,axiom,
~ p(n4,n4,n2) ).
cnf(u32390,axiom,
~ p(n6,n3,n9) ).
cnf(u32394,axiom,
~ p(n6,n2,n9) ).
cnf(u32398,axiom,
~ p(n6,n1,n9) ).
cnf(u32402,axiom,
~ p(n5,n3,n9) ).
cnf(u32406,axiom,
~ p(n5,n2,n9) ).
cnf(u32410,axiom,
~ p(n5,n1,n9) ).
cnf(u32415,axiom,
p(n4,n3,n9) ).
cnf(u32418,axiom,
~ p(n4,n2,n9) ).
cnf(u32422,axiom,
~ p(n4,n1,n9) ).
cnf(u32427,axiom,
~ p(n6,n3,n8) ).
cnf(u32431,axiom,
~ p(n6,n2,n8) ).
cnf(u32435,axiom,
~ p(n6,n1,n8) ).
cnf(u32439,axiom,
~ p(n5,n3,n8) ).
cnf(u32444,axiom,
p(n5,n2,n8) ).
cnf(u32447,axiom,
~ p(n5,n1,n8) ).
cnf(u32451,axiom,
~ p(n4,n3,n8) ).
cnf(u32455,axiom,
~ p(n4,n2,n8) ).
cnf(u32459,axiom,
~ p(n4,n1,n8) ).
cnf(u32465,axiom,
p(n6,n3,n7) ).
cnf(u32468,axiom,
~ p(n6,n2,n7) ).
cnf(u32472,axiom,
~ p(n6,n1,n7) ).
cnf(u32476,axiom,
~ p(n5,n3,n7) ).
cnf(u32480,axiom,
~ p(n5,n2,n7) ).
cnf(u32484,axiom,
~ p(n5,n1,n7) ).
cnf(u32488,axiom,
~ p(n4,n3,n7) ).
cnf(u32492,axiom,
~ p(n4,n2,n7) ).
cnf(u32496,axiom,
~ p(n4,n1,n7) ).
cnf(u32501,axiom,
~ p(n6,n3,n6) ).
cnf(u32506,axiom,
p(n6,n2,n6) ).
cnf(u32509,axiom,
~ p(n6,n1,n6) ).
cnf(u32513,axiom,
~ p(n5,n3,n6) ).
cnf(u32517,axiom,
~ p(n5,n2,n6) ).
cnf(u32521,axiom,
~ p(n5,n1,n6) ).
cnf(u32525,axiom,
~ p(n4,n3,n6) ).
cnf(u32529,axiom,
~ p(n4,n2,n6) ).
cnf(u32533,axiom,
~ p(n4,n1,n6) ).
cnf(u32538,axiom,
~ p(n6,n3,n5) ).
cnf(u32542,axiom,
~ p(n6,n2,n5) ).
cnf(u32546,axiom,
~ p(n6,n1,n5) ).
cnf(u32551,axiom,
p(n5,n3,n5) ).
cnf(u32554,axiom,
~ p(n5,n2,n5) ).
cnf(u32558,axiom,
~ p(n5,n1,n5) ).
cnf(u32562,axiom,
~ p(n4,n3,n5) ).
cnf(u32566,axiom,
~ p(n4,n2,n5) ).
cnf(u32570,axiom,
~ p(n4,n1,n5) ).
cnf(u32575,axiom,
~ p(n6,n3,n3) ).
cnf(u32579,axiom,
~ p(n6,n2,n3) ).
cnf(u32583,axiom,
~ p(n6,n1,n3) ).
cnf(u32587,axiom,
~ p(n5,n3,n3) ).
cnf(u32591,axiom,
~ p(n5,n2,n3) ).
cnf(u32595,axiom,
~ p(n5,n1,n3) ).
cnf(u32599,axiom,
~ p(n4,n3,n3) ).
cnf(u32604,axiom,
p(n4,n2,n3) ).
cnf(u32607,axiom,
~ p(n4,n1,n3) ).
cnf(u32612,axiom,
~ p(n6,n3,n2) ).
cnf(u32616,axiom,
~ p(n6,n2,n2) ).
cnf(u32621,axiom,
p(n6,n1,n2) ).
cnf(u32624,axiom,
~ p(n5,n3,n2) ).
cnf(u32628,axiom,
~ p(n5,n2,n2) ).
cnf(u32632,axiom,
~ p(n5,n1,n2) ).
cnf(u32636,axiom,
~ p(n4,n3,n2) ).
cnf(u32640,axiom,
~ p(n4,n2,n2) ).
cnf(u32644,axiom,
~ p(n4,n1,n2) ).
cnf(u32649,axiom,
~ p(n6,n3,n1) ).
cnf(u32653,axiom,
~ p(n6,n2,n1) ).
cnf(u32657,axiom,
~ p(n6,n1,n1) ).
cnf(u32661,axiom,
~ p(n5,n3,n1) ).
cnf(u32665,axiom,
~ p(n5,n2,n1) ).
cnf(u32670,axiom,
p(n5,n1,n1) ).
cnf(u32673,axiom,
~ p(n4,n3,n1) ).
cnf(u32677,axiom,
~ p(n4,n2,n1) ).
cnf(u32681,axiom,
~ p(n4,n1,n1) ).
cnf(u32686,axiom,
~ p(n3,n9,n9) ).
cnf(u32690,axiom,
~ p(n3,n8,n9) ).
cnf(u32694,axiom,
~ p(n3,n7,n9) ).
cnf(u32698,axiom,
~ p(n2,n9,n9) ).
cnf(u32702,axiom,
~ p(n2,n8,n9) ).
cnf(u32706,axiom,
~ p(n2,n7,n9) ).
cnf(u32711,axiom,
p(n1,n9,n9) ).
cnf(u32714,axiom,
~ p(n1,n8,n9) ).
cnf(u32718,axiom,
~ p(n1,n7,n9) ).
cnf(u32723,axiom,
~ p(n3,n9,n8) ).
cnf(u32727,axiom,
~ p(n3,n8,n8) ).
cnf(u32732,axiom,
p(n3,n7,n8) ).
cnf(u32735,axiom,
~ p(n2,n9,n8) ).
cnf(u32739,axiom,
~ p(n2,n8,n8) ).
cnf(u32743,axiom,
~ p(n2,n7,n8) ).
cnf(u32747,axiom,
~ p(n1,n9,n8) ).
cnf(u32751,axiom,
~ p(n1,n8,n8) ).
cnf(u32755,axiom,
~ p(n1,n7,n8) ).
cnf(u32760,axiom,
~ p(n3,n9,n7) ).
cnf(u32764,axiom,
~ p(n3,n8,n7) ).
cnf(u32768,axiom,
~ p(n3,n7,n7) ).
cnf(u32772,axiom,
~ p(n2,n9,n7) ).
cnf(u32776,axiom,
~ p(n2,n8,n7) ).
cnf(u32780,axiom,
~ p(n2,n7,n7) ).
cnf(u32784,axiom,
~ p(n1,n9,n7) ).
cnf(u32789,axiom,
p(n1,n8,n7) ).
cnf(u32792,axiom,
~ p(n1,n7,n7) ).
cnf(u32797,axiom,
~ p(n3,n9,n5) ).
cnf(u32801,axiom,
~ p(n3,n8,n5) ).
cnf(u32805,axiom,
~ p(n3,n7,n5) ).
cnf(u32809,axiom,
~ p(n2,n9,n5) ).
cnf(u32813,axiom,
~ p(n2,n8,n5) ).
cnf(u32818,axiom,
p(n2,n7,n5) ).
cnf(u32821,axiom,
~ p(n1,n9,n5) ).
cnf(u32825,axiom,
~ p(n1,n8,n5) ).
cnf(u32829,axiom,
~ p(n1,n7,n5) ).
cnf(u32834,axiom,
~ p(n3,n9,n3) ).
cnf(u32839,axiom,
p(n3,n8,n3) ).
cnf(u32842,axiom,
~ p(n3,n7,n3) ).
cnf(u32846,axiom,
~ p(n2,n9,n3) ).
cnf(u32850,axiom,
~ p(n2,n8,n3) ).
cnf(u32854,axiom,
~ p(n2,n7,n3) ).
cnf(u32858,axiom,
~ p(n1,n9,n3) ).
cnf(u32862,axiom,
~ p(n1,n8,n3) ).
cnf(u32866,axiom,
~ p(n1,n7,n3) ).
cnf(u32871,axiom,
~ p(n3,n9,n2) ).
cnf(u32875,axiom,
~ p(n3,n8,n2) ).
cnf(u32879,axiom,
~ p(n3,n7,n2) ).
cnf(u32883,axiom,
~ p(n2,n9,n2) ).
cnf(u32887,axiom,
~ p(n2,n8,n2) ).
cnf(u32891,axiom,
~ p(n2,n7,n2) ).
cnf(u32895,axiom,
~ p(n1,n9,n2) ).
cnf(u32899,axiom,
~ p(n1,n8,n2) ).
cnf(u32904,axiom,
p(n1,n7,n2) ).
cnf(u32908,axiom,
~ p(n3,n9,n1) ).
cnf(u32912,axiom,
~ p(n3,n8,n1) ).
cnf(u32916,axiom,
~ p(n3,n7,n1) ).
cnf(u32921,axiom,
p(n2,n9,n1) ).
cnf(u32924,axiom,
~ p(n2,n8,n1) ).
cnf(u32928,axiom,
~ p(n2,n7,n1) ).
cnf(u32932,axiom,
~ p(n1,n9,n1) ).
cnf(u32936,axiom,
~ p(n1,n8,n1) ).
cnf(u32940,axiom,
~ p(n1,n7,n1) ).
cnf(u32945,axiom,
~ p(n3,n6,n8) ).
cnf(u32949,axiom,
~ p(n3,n5,n8) ).
cnf(u32953,axiom,
~ p(n3,n4,n8) ).
cnf(u32957,axiom,
~ p(n2,n6,n8) ).
cnf(u32961,axiom,
~ p(n2,n5,n8) ).
cnf(u32965,axiom,
~ p(n2,n4,n8) ).
cnf(u32969,axiom,
~ p(n1,n6,n8) ).
cnf(u32974,axiom,
p(n1,n5,n8) ).
cnf(u32977,axiom,
~ p(n1,n4,n8) ).
cnf(u32982,axiom,
~ p(n3,n6,n7) ).
cnf(u32987,axiom,
p(n3,n5,n7) ).
cnf(u32990,axiom,
~ p(n3,n4,n7) ).
cnf(u32994,axiom,
~ p(n2,n6,n7) ).
cnf(u32998,axiom,
~ p(n2,n5,n7) ).
cnf(u33002,axiom,
~ p(n2,n4,n7) ).
cnf(u33006,axiom,
~ p(n1,n6,n7) ).
cnf(u33010,axiom,
~ p(n1,n5,n7) ).
cnf(u33014,axiom,
~ p(n1,n4,n7) ).
cnf(u33019,axiom,
~ p(n3,n6,n6) ).
cnf(u33023,axiom,
~ p(n3,n5,n6) ).
cnf(u33028,axiom,
p(n3,n4,n6) ).
cnf(u33031,axiom,
~ p(n2,n6,n6) ).
cnf(u33035,axiom,
~ p(n2,n5,n6) ).
cnf(u33039,axiom,
~ p(n2,n4,n6) ).
cnf(u33043,axiom,
~ p(n1,n6,n6) ).
cnf(u33047,axiom,
~ p(n1,n5,n6) ).
cnf(u33051,axiom,
~ p(n1,n4,n6) ).
cnf(u33057,axiom,
p(n3,n6,n5) ).
cnf(u33060,axiom,
~ p(n3,n5,n5) ).
cnf(u33064,axiom,
~ p(n3,n4,n5) ).
cnf(u33068,axiom,
~ p(n2,n6,n5) ).
cnf(u33072,axiom,
~ p(n2,n5,n5) ).
cnf(u33076,axiom,
~ p(n2,n4,n5) ).
cnf(u33080,axiom,
~ p(n1,n6,n5) ).
cnf(u33084,axiom,
~ p(n1,n5,n5) ).
cnf(u33088,axiom,
~ p(n1,n4,n5) ).
cnf(u33093,axiom,
~ p(n3,n6,n4) ).
cnf(u33097,axiom,
~ p(n3,n5,n4) ).
cnf(u33101,axiom,
~ p(n3,n4,n4) ).
cnf(u33106,axiom,
p(n2,n6,n4) ).
cnf(u33109,axiom,
~ p(n2,n5,n4) ).
cnf(u33113,axiom,
~ p(n2,n4,n4) ).
cnf(u33117,axiom,
~ p(n1,n6,n4) ).
cnf(u33121,axiom,
~ p(n1,n5,n4) ).
cnf(u33125,axiom,
~ p(n1,n4,n4) ).
cnf(u33130,axiom,
~ p(n3,n6,n2) ).
cnf(u33134,axiom,
~ p(n3,n5,n2) ).
cnf(u33138,axiom,
~ p(n3,n4,n2) ).
cnf(u33142,axiom,
~ p(n2,n6,n2) ).
cnf(u33146,axiom,
~ p(n2,n5,n2) ).
cnf(u33151,axiom,
p(n2,n4,n2) ).
cnf(u33154,axiom,
~ p(n1,n6,n2) ).
cnf(u33158,axiom,
~ p(n1,n5,n2) ).
cnf(u33162,axiom,
~ p(n1,n4,n2) ).
cnf(u33167,axiom,
~ p(n3,n3,n8) ).
cnf(u33171,axiom,
~ p(n3,n2,n8) ).
cnf(u33175,axiom,
~ p(n3,n1,n8) ).
cnf(u33179,axiom,
~ p(n2,n3,n8) ).
cnf(u33183,axiom,
~ p(n2,n2,n8) ).
cnf(u33188,axiom,
p(n2,n1,n8) ).
cnf(u33191,axiom,
~ p(n1,n3,n8) ).
cnf(u33195,axiom,
~ p(n1,n2,n8) ).
cnf(u33199,axiom,
~ p(n1,n1,n8) ).
cnf(u33204,axiom,
~ p(n3,n3,n6) ).
cnf(u33208,axiom,
~ p(n3,n2,n6) ).
cnf(u33212,axiom,
~ p(n3,n1,n6) ).
cnf(u33216,axiom,
~ p(n2,n3,n6) ).
cnf(u33220,axiom,
~ p(n2,n2,n6) ).
cnf(u33224,axiom,
~ p(n2,n1,n6) ).
cnf(u33228,axiom,
~ p(n1,n3,n6) ).
cnf(u33232,axiom,
~ p(n1,n2,n6) ).
cnf(u33237,axiom,
p(n1,n1,n6) ).
cnf(u33241,axiom,
~ p(n3,n3,n5) ).
cnf(u33245,axiom,
~ p(n3,n2,n5) ).
cnf(u33249,axiom,
~ p(n3,n1,n5) ).
cnf(u33253,axiom,
~ p(n2,n3,n5) ).
cnf(u33257,axiom,
~ p(n2,n2,n5) ).
cnf(u33261,axiom,
~ p(n2,n1,n5) ).
cnf(u33265,axiom,
~ p(n1,n3,n5) ).
cnf(u33270,axiom,
p(n1,n2,n5) ).
cnf(u33273,axiom,
~ p(n1,n1,n5) ).
cnf(u33278,axiom,
~ p(n3,n3,n4) ).
cnf(u33282,axiom,
~ p(n3,n2,n4) ).
cnf(u33286,axiom,
~ p(n3,n1,n4) ).
cnf(u33290,axiom,
~ p(n2,n3,n4) ).
cnf(u33294,axiom,
~ p(n2,n2,n4) ).
cnf(u33298,axiom,
~ p(n2,n1,n4) ).
cnf(u33303,axiom,
p(n1,n3,n4) ).
cnf(u33306,axiom,
~ p(n1,n2,n4) ).
cnf(u33310,axiom,
~ p(n1,n1,n4) ).
cnf(u33315,axiom,
~ p(n3,n3,n3) ).
cnf(u33319,axiom,
~ p(n3,n2,n3) ).
cnf(u33323,axiom,
~ p(n3,n1,n3) ).
cnf(u33328,axiom,
p(n2,n3,n3) ).
cnf(u33331,axiom,
~ p(n2,n2,n3) ).
cnf(u33335,axiom,
~ p(n2,n1,n3) ).
cnf(u33339,axiom,
~ p(n1,n3,n3) ).
cnf(u33343,axiom,
~ p(n1,n2,n3) ).
cnf(u33347,axiom,
~ p(n1,n1,n3) ).
cnf(u33353,axiom,
p(n3,n3,n2) ).
cnf(u33356,axiom,
~ p(n3,n2,n2) ).
cnf(u33360,axiom,
~ p(n3,n1,n2) ).
cnf(u33364,axiom,
~ p(n2,n3,n2) ).
cnf(u33368,axiom,
~ p(n2,n2,n2) ).
cnf(u33372,axiom,
~ p(n2,n1,n2) ).
cnf(u33376,axiom,
~ p(n1,n3,n2) ).
cnf(u33380,axiom,
~ p(n1,n2,n2) ).
cnf(u33384,axiom,
~ p(n1,n1,n2) ).
cnf(u33389,axiom,
~ p(n3,n3,n1) ).
cnf(u33394,axiom,
p(n3,n2,n1) ).
cnf(u33397,axiom,
~ p(n3,n1,n1) ).
cnf(u33401,axiom,
~ p(n2,n3,n1) ).
cnf(u33405,axiom,
~ p(n2,n2,n1) ).
cnf(u33409,axiom,
~ p(n2,n1,n1) ).
cnf(u33413,axiom,
~ p(n1,n3,n1) ).
cnf(u33417,axiom,
~ p(n1,n2,n1) ).
cnf(u33421,axiom,
~ p(n1,n1,n1) ).
cnf(u33426,axiom,
~ p(n9,n9,n9) ).
cnf(u33430,axiom,
~ p(n9,n9,n7) ).
cnf(u33434,axiom,
~ p(n9,n9,n3) ).
cnf(u33438,axiom,
~ p(n9,n9,n1) ).
cnf(u33443,axiom,
~ p(n9,n8,n9) ).
cnf(u33447,axiom,
~ p(n9,n8,n7) ).
cnf(u33451,axiom,
~ p(n9,n8,n3) ).
cnf(u33455,axiom,
~ p(n9,n8,n1) ).
cnf(u33460,axiom,
~ p(n9,n6,n7) ).
cnf(u33464,axiom,
~ p(n9,n6,n2) ).
cnf(u33469,axiom,
~ p(n9,n5,n7) ).
cnf(u33473,axiom,
~ p(n9,n5,n2) ).
cnf(u33478,axiom,
~ p(n9,n4,n7) ).
cnf(u33482,axiom,
~ p(n9,n4,n2) ).
cnf(u33487,axiom,
~ p(n9,n2,n8) ).
cnf(u33491,axiom,
~ p(n9,n2,n6) ).
cnf(u33495,axiom,
~ p(n9,n2,n3) ).
cnf(u33499,axiom,
~ p(n9,n2,n1) ).
cnf(u33504,axiom,
~ p(n9,n1,n8) ).
cnf(u33508,axiom,
~ p(n9,n1,n6) ).
cnf(u33512,axiom,
~ p(n9,n1,n3) ).
cnf(u33516,axiom,
~ p(n9,n1,n1) ).
cnf(u33521,axiom,
~ p(n8,n8,n9) ).
cnf(u33525,axiom,
~ p(n8,n8,n7) ).
cnf(u33529,axiom,
~ p(n8,n8,n3) ).
cnf(u33533,axiom,
~ p(n8,n8,n1) ).
cnf(u33538,axiom,
~ p(n8,n6,n7) ).
cnf(u33542,axiom,
~ p(n8,n6,n2) ).
cnf(u33547,axiom,
~ p(n8,n5,n7) ).
cnf(u33551,axiom,
~ p(n8,n5,n2) ).
cnf(u33556,axiom,
~ p(n8,n4,n7) ).
cnf(u33560,axiom,
~ p(n8,n4,n2) ).
cnf(u33565,axiom,
~ p(n8,n2,n8) ).
cnf(u33569,axiom,
~ p(n8,n2,n6) ).
cnf(u33573,axiom,
~ p(n8,n2,n3) ).
cnf(u33577,axiom,
~ p(n8,n2,n1) ).
cnf(u33582,axiom,
~ p(n7,n9,n9) ).
cnf(u33586,axiom,
~ p(n7,n9,n7) ).
cnf(u33590,axiom,
~ p(n7,n9,n3) ).
cnf(u33594,axiom,
~ p(n7,n9,n1) ).
cnf(u33599,axiom,
~ p(n7,n8,n9) ).
cnf(u33603,axiom,
~ p(n7,n8,n7) ).
cnf(u33607,axiom,
~ p(n7,n8,n3) ).
cnf(u33611,axiom,
~ p(n7,n8,n1) ).
cnf(u33616,axiom,
~ p(n7,n5,n7) ).
cnf(u33620,axiom,
~ p(n7,n5,n2) ).
cnf(u33625,axiom,
~ p(n7,n2,n8) ).
cnf(u33629,axiom,
~ p(n7,n2,n6) ).
cnf(u33633,axiom,
~ p(n7,n2,n3) ).
cnf(u33637,axiom,
~ p(n7,n2,n1) ).
cnf(u33642,axiom,
~ p(n7,n1,n8) ).
cnf(u33646,axiom,
~ p(n7,n1,n6) ).
cnf(u33650,axiom,
~ p(n7,n1,n3) ).
cnf(u33654,axiom,
~ p(n7,n1,n1) ).
cnf(u33659,axiom,
~ p(n6,n9,n2) ).
cnf(u33664,axiom,
~ p(n6,n8,n2) ).
cnf(u33669,axiom,
~ p(n6,n7,n2) ).
cnf(u33674,axiom,
~ p(n6,n6,n8) ).
cnf(u33678,axiom,
~ p(n6,n6,n7) ).
cnf(u33682,axiom,
~ p(n6,n6,n6) ).
cnf(u33686,axiom,
~ p(n6,n6,n4) ).
cnf(u33690,axiom,
~ p(n6,n6,n1) ).
cnf(u33695,axiom,
~ p(n6,n4,n8) ).
cnf(u33699,axiom,
~ p(n6,n4,n7) ).
cnf(u33703,axiom,
~ p(n6,n4,n6) ).
cnf(u33707,axiom,
~ p(n6,n4,n4) ).
cnf(u33711,axiom,
~ p(n6,n4,n1) ).
cnf(u33716,axiom,
~ p(n6,n3,n4) ).
cnf(u33721,axiom,
~ p(n6,n2,n4) ).
cnf(u33726,axiom,
~ p(n6,n1,n4) ).
cnf(u33731,axiom,
~ p(n5,n9,n2) ).
cnf(u33736,axiom,
~ p(n5,n8,n2) ).
cnf(u33741,axiom,
~ p(n5,n7,n2) ).
cnf(u33746,axiom,
~ p(n5,n5,n8) ).
cnf(u33750,axiom,
~ p(n5,n5,n7) ).
cnf(u33754,axiom,
~ p(n5,n5,n6) ).
cnf(u33758,axiom,
~ p(n5,n5,n4) ).
cnf(u33762,axiom,
~ p(n5,n5,n1) ).
cnf(u33767,axiom,
~ p(n5,n3,n4) ).
cnf(u33772,axiom,
~ p(n5,n2,n4) ).
cnf(u33777,axiom,
~ p(n5,n1,n4) ).
cnf(u33782,axiom,
~ p(n4,n8,n2) ).
cnf(u33787,axiom,
~ p(n4,n7,n2) ).
cnf(u33792,axiom,
~ p(n4,n5,n8) ).
cnf(u33796,axiom,
~ p(n4,n5,n7) ).
cnf(u33800,axiom,
~ p(n4,n5,n6) ).
cnf(u33804,axiom,
~ p(n4,n5,n4) ).
cnf(u33808,axiom,
~ p(n4,n5,n1) ).
cnf(u33813,axiom,
~ p(n4,n3,n4) ).
cnf(u33818,axiom,
~ p(n4,n2,n4) ).
cnf(u33823,axiom,
~ p(n3,n8,n6) ).
cnf(u33827,axiom,
~ p(n3,n8,n4) ).
cnf(u33832,axiom,
~ p(n3,n7,n6) ).
cnf(u33836,axiom,
~ p(n3,n7,n4) ).
cnf(u33841,axiom,
~ p(n3,n6,n9) ).
cnf(u33845,axiom,
~ p(n3,n6,n3) ).
cnf(u33849,axiom,
~ p(n3,n6,n1) ).
cnf(u33854,axiom,
~ p(n3,n5,n9) ).
cnf(u33858,axiom,
~ p(n3,n5,n3) ).
cnf(u33862,axiom,
~ p(n3,n5,n1) ).
cnf(u33867,axiom,
~ p(n3,n4,n9) ).
cnf(u33871,axiom,
~ p(n3,n4,n3) ).
cnf(u33875,axiom,
~ p(n3,n4,n1) ).
cnf(u33880,axiom,
~ p(n3,n3,n9) ).
cnf(u33884,axiom,
~ p(n3,n3,n7) ).
cnf(u33889,axiom,
~ p(n3,n2,n9) ).
cnf(u33893,axiom,
~ p(n3,n2,n7) ).
cnf(u33898,axiom,
~ p(n2,n9,n6) ).
cnf(u33902,axiom,
~ p(n2,n9,n4) ).
cnf(u33907,axiom,
~ p(n2,n7,n6) ).
cnf(u33911,axiom,
~ p(n2,n7,n4) ).
cnf(u33916,axiom,
~ p(n2,n6,n9) ).
cnf(u33920,axiom,
~ p(n2,n6,n3) ).
cnf(u33924,axiom,
~ p(n2,n6,n1) ).
cnf(u33929,axiom,
~ p(n2,n4,n9) ).
cnf(u33933,axiom,
~ p(n2,n4,n3) ).
cnf(u33937,axiom,
~ p(n2,n4,n1) ).
cnf(u33942,axiom,
~ p(n2,n3,n9) ).
cnf(u33946,axiom,
~ p(n2,n3,n7) ).
cnf(u33951,axiom,
~ p(n2,n1,n9) ).
cnf(u33955,axiom,
~ p(n2,n1,n7) ).
cnf(u33960,axiom,
~ p(n1,n9,n6) ).
cnf(u33964,axiom,
~ p(n1,n9,n4) ).
cnf(u33969,axiom,
~ p(n1,n8,n6) ).
cnf(u33973,axiom,
~ p(n1,n8,n4) ).
cnf(u33978,axiom,
~ p(n1,n7,n6) ).
cnf(u33982,axiom,
~ p(n1,n7,n4) ).
cnf(u33987,axiom,
~ p(n1,n5,n9) ).
cnf(u33991,axiom,
~ p(n1,n5,n3) ).
cnf(u33995,axiom,
~ p(n1,n5,n1) ).
cnf(u34000,axiom,
~ p(n1,n3,n9) ).
cnf(u34004,axiom,
~ p(n1,n3,n7) ).
cnf(u34009,axiom,
~ p(n1,n2,n9) ).
cnf(u34013,axiom,
~ p(n1,n2,n7) ).
cnf(u34018,axiom,
~ p(n1,n1,n9) ).
cnf(u34022,axiom,
~ p(n1,n1,n7) ).
cnf(u34027,axiom,
~ p(n8,n9,n9) ).
cnf(u34033,axiom,
~ p(n3,n9,n6) ).
cnf(u34039,axiom,
~ p(n8,n9,n3) ).
cnf(u34044,axiom,
~ p(n8,n9,n1) ).
cnf(u34053,axiom,
~ p(n2,n8,n4) ).
cnf(u34062,axiom,
~ p(n9,n7,n7) ).
cnf(u34066,axiom,
~ p(n8,n7,n7) ).
cnf(u34070,axiom,
~ p(n7,n7,n7) ).
cnf(u34079,axiom,
~ p(n1,n6,n9) ).
cnf(u34084,axiom,
~ p(n5,n6,n8) ).
cnf(u34088,axiom,
~ p(n4,n6,n8) ).
cnf(u34094,axiom,
~ p(n5,n6,n4) ).
cnf(u34098,axiom,
~ p(n4,n6,n4) ).
cnf(u34103,axiom,
~ p(n1,n6,n3) ).
cnf(u34108,axiom,
~ p(n6,n5,n8) ).
cnf(u34113,axiom,
~ p(n6,n5,n7) ).
cnf(u34118,axiom,
~ p(n6,n5,n6) ).
cnf(u34124,axiom,
~ p(n6,n5,n4) ).
cnf(u34129,axiom,
~ p(n2,n5,n3) ).
cnf(u34135,axiom,
~ p(n1,n4,n9) ).
cnf(u34140,axiom,
~ p(n5,n4,n6) ).
cnf(u34144,axiom,
~ p(n4,n4,n6) ).
cnf(u34150,axiom,
~ p(n7,n4,n2) ).
cnf(u34155,axiom,
~ p(n5,n4,n1) ).
cnf(u34159,axiom,
~ p(n4,n4,n1) ).
cnf(u34163,axiom,
~ p(n1,n4,n1) ).
cnf(u34172,axiom,
~ p(n9,n3,n3) ).
cnf(u34176,axiom,
~ p(n8,n3,n3) ).
cnf(u34180,axiom,
~ p(n7,n3,n3) ).
cnf(u34186,axiom,
~ p(n2,n2,n9) ).
cnf(u34198,axiom,
~ p(n8,n1,n8) ).
cnf(u34203,axiom,
~ p(n3,n1,n7) ).
cnf(u34208,axiom,
~ p(n8,n1,n6) ).
cnf(u34215,axiom,
~ p(n8,n1,n1) ).
cnf(u34220,axiom,
~ p(n9,n7,n9) ).
cnf(u34226,axiom,
~ p(n9,n3,n6) ).
cnf(u34234,axiom,
~ p(n9,n7,n1) ).
cnf(u34238,axiom,
~ p(n9,n3,n1) ).
cnf(u34243,axiom,
~ p(n8,n3,n8) ).
cnf(u34248,axiom,
~ p(n8,n3,n6) ).
cnf(u34256,axiom,
~ p(n7,n7,n9) ).
cnf(u34261,axiom,
~ p(n7,n3,n8) ).
cnf(u34268,axiom,
~ p(n7,n7,n3) ).
cnf(u34282,axiom,
~ p(n5,n4,n8) ).
cnf(u34287,axiom,
~ p(n5,n6,n6) ).
cnf(u34295,axiom,
~ p(n5,n6,n1) ).
cnf(u34301,axiom,
~ p(n4,n6,n7) ).
cnf(u34305,axiom,
~ p(n4,n4,n7) ).
cnf(u34312,axiom,
~ p(n4,n6,n1) ).
cnf(u34329,axiom,
~ p(n2,n5,n1) ).
cnf(u34384,axiom,
~ p(n8,n7,n3) ).
cnf(u34390,axiom,
~ p(n8,n7,n1) ).
cnf(u34568,axiom,
~ p(n7,n6,n7) ).
cnf(u34740,axiom,
~ p(n7,n3,n1) ).
cnf(u35044,axiom,
~ p(n5,n4,n7) ).
cnf(u35141,axiom,
~ p(n4,n4,n4) ).
cnf(u31312,axiom,
p(n8,n9,n7) ).
cnf(u31292,axiom,
p(n1,n6,n1) ).
cnf(u31305,axiom,
p(n7,n3,n6) ).
cnf(u31311,axiom,
p(n8,n7,n9) ).
cnf(u31296,axiom,
p(n3,n1,n9) ).
cnf(u31297,axiom,
p(n3,n9,n4) ).
cnf(u31299,axiom,
p(n4,n4,n8) ).
cnf(u31302,axiom,
p(n5,n4,n4) ).
cnf(u31291,axiom,
p(n1,n4,n3) ).
cnf(u31301,axiom,
p(n4,n9,n2) ).
cnf(u31310,axiom,
p(n8,n3,n1) ).
cnf(u31307,axiom,
p(n7,n6,n2) ).
cnf(u31303,axiom,
p(n5,n6,n7) ).
cnf(u31314,axiom,
p(n9,n7,n3) ).
cnf(u31304,axiom,
p(n6,n5,n1) ).
cnf(u31295,axiom,
p(n2,n8,n6) ).
cnf(u31300,axiom,
p(n4,n6,n6) ).
cnf(u31294,axiom,
p(n2,n5,n9) ).
cnf(u31306,axiom,
p(n7,n4,n7) ).
cnf(u31293,axiom,
p(n2,n2,n7) ).
cnf(u31298,axiom,
p(n4,n1,n4) ).
cnf(u31308,axiom,
p(n7,n7,n1) ).
cnf(u31313,axiom,
p(n9,n3,n8) ).
cnf(u31309,axiom,
p(n8,n1,n3) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ080+2 : TPTP v9.3.1. Bugfixed v5.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n006.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.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 22:39:55 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.43/2.01 % (3394137)Detected formulas, will run a generic FOF schedule.
% 3.43/2.01 % (3394146)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=950752083:i=119:av=off:ss=axioms_2997 on theBenchmark for (2997ds/119Mi)
% 3.43/2.01 % (3394146)Refutation not found, incomplete strategy
% 3.43/2.01 % (3394146)------------------------------
% 3.43/2.01 % (3394146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/2.01 % (3394146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/2.01 % (3394146)CaDiCaL version: 2.1.3
% 3.43/2.01 % (3394146)Termination reason: Refutation not found, incomplete strategy
% 3.43/2.01 % (3394146)Time elapsed: 0.010 s
% 3.43/2.01 % (3394146)Peak memory usage: 91 MB
% 3.43/2.01 % (3394146)Instructions burned: 33 (million)
% 3.43/2.01 % (3394142)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=2161028286:i=141193_2997 on theBenchmark for (2997ds/141193Mi)
% 3.43/2.01 % (3394143)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=1968199552:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2997 on theBenchmark for (2997ds/134677Mi)
% 3.43/2.01 % (3394148)dis-21_1_sil=8000:lcm=predicate:random_seed=3906705453:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2997 on theBenchmark for (2997ds/129Mi)
% 3.43/2.01 % (3394147)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1085652442:s2a=on:i=139:gtg=position_2997 on theBenchmark for (2997ds/139Mi)
% 3.43/2.01 % (3394145)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=107964794:i=109:sd=1:ins=1:gsp=on:ss=axioms_2997 on theBenchmark for (2997ds/109Mi)
% 3.43/2.01 % (3394144)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=2727312603:i=141695:sd=1:nm=32:gsp=on:ss=included_2997 on theBenchmark for (2997ds/141695Mi)
% 3.43/2.01 % (3394145)Refutation not found, incomplete strategy
% 3.43/2.01 % (3394145)------------------------------
% 3.43/2.01 % (3394145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/2.01 % (3394145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/2.01 % (3394145)CaDiCaL version: 2.1.3
% 3.43/2.01 % (3394145)Termination reason: Refutation not found, incomplete strategy
% 3.43/2.01 % (3394145)Time elapsed: 0.018 s
% 3.43/2.01 % (3394145)Peak memory usage: 91 MB
% 3.43/2.01 % (3394145)Instructions burned: 33 (million)
% 3.43/2.01 % (3394147)Instruction limit reached!
% 3.43/2.01 % (3394147)------------------------------
% 3.43/2.01 % (3394147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/2.01 % (3394147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/2.01 % (3394147)CaDiCaL version: 2.1.3
% 3.43/2.01 % (3394147)Termination reason: Instruction limit
% 3.43/2.01 % (3394147)Termination phase: Unused predicate definition removal
% 3.43/2.01 % (3394147)Time elapsed: 0.062 s
% 3.43/2.01 % (3394147)Peak memory usage: 89 MB
% 3.43/2.01 % (3394147)Instructions burned: 140 (million)
% 3.43/2.01 % (3394148)Instruction limit reached!
% 3.43/2.01 % (3394148)------------------------------
% 3.43/2.01 % (3394148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/2.01 % (3394148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/2.01 % (3394148)CaDiCaL version: 2.1.3
% 3.43/2.01 % (3394148)Termination reason: Instruction limit
% 3.43/2.01 % (3394148)Termination phase: Preprocessing 3
% 3.43/2.01 % (3394148)Time elapsed: 0.067 s
% 3.43/2.01 % (3394148)Peak memory usage: 91 MB
% 3.43/2.01 % (3394148)Instructions burned: 131 (million)
% 3.43/2.01 % (3394146)------------------------------
% 3.43/2.01 % (3394146)------------------------------
% 3.43/2.01 % (3394156)lrs+10_1_sil=8000:sp=occurrence:random_seed=926847664:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 3.43/2.01 % (3394157)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2053551309:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 3.43/2.01 % (3394158)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3960566204:i=325:sd=1:ss=axioms:sgt=32_2994 on theBenchmark for (2994ds/325Mi)
% 3.43/2.01 % (3394158)Refutation not found, incomplete strategy
% 3.43/2.01 % (3394158)------------------------------
% 3.43/2.01 % (3394158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.91/2.37 % (3394158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.91/2.37 % (3394158)CaDiCaL version: 2.1.3
% 8.91/2.37 % (3394158)Termination reason: Refutation not found, incomplete strategy
% 8.91/2.37 % (3394158)Time elapsed: 0.009 s
% 8.91/2.37 % (3394158)Peak memory usage: 91 MB
% 8.91/2.37 % (3394158)Instructions burned: 33 (million)
% 8.91/2.37 % (3394156)Refutation not found, incomplete strategy
% 8.91/2.37 % (3394156)------------------------------
% 8.91/2.37 % (3394156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.91/2.37 % (3394156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.91/2.37 % (3394156)CaDiCaL version: 2.1.3
% 8.91/2.37 % (3394156)Termination reason: Refutation not found, incomplete strategy
% 8.91/2.37 % (3394156)Time elapsed: 0.018 s
% 8.91/2.37 % (3394156)Peak memory usage: 91 MB
% 8.91/2.37 % (3394156)Instructions burned: 33 (million)
% 8.91/2.37 % (3394145)------------------------------
% 8.91/2.37 % (3394145)------------------------------
% 8.91/2.37 % (3394157)Refutation not found, incomplete strategy
% 8.91/2.37 % (3394157)------------------------------
% 8.91/2.37 % (3394157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.91/2.37 % (3394157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.91/2.37 % (3394157)CaDiCaL version: 2.1.3
% 8.91/2.37 % (3394157)Termination reason: Refutation not found, incomplete strategy
% 8.91/2.37 % (3394157)Time elapsed: 0.052 s
% 8.91/2.37 % (3394157)Peak memory usage: 91 MB
% 8.91/2.37 % (3394157)Instructions burned: 123 (million)
% 8.91/2.37 % (3394158)------------------------------
% 8.91/2.37 % (3394158)------------------------------
% 8.91/2.37 % (3394162)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=1644874413:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 8.91/2.37 % (3394156)------------------------------
% 8.91/2.37 % (3394156)------------------------------
% 8.91/2.37 [W927 22:39:57.487525057 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.
% 8.91/2.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.91/2.37 [W927 22:39:57.487558777 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.
% 8.91/2.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.91/2.37 [W927 22:39:57.487598560 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.
% 8.91/2.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.91/2.37 [W927 22:39:57.487611684 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.
% 8.91/2.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.91/2.37 [W927 22:39:57.487641194 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.
% 8.91/2.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.91/2.37 [W927 22:39:57.487652954 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.
% 8.91/2.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.91/2.37 % (3394163)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1565031348:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2992 on theBenchmark for (2992ds/294Mi)
% 8.91/2.37 [W927 22:39:57.515533743 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.41/2.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.41/2.40 [W927 22:39:57.515576080 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.41/2.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.41/2.40 [W927 22:39:57.515614293 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.41/2.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.41/2.40 [W927 22:39:57.515625473 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.41/2.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.41/2.40 [W927 22:39:57.515652110 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.41/2.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.41/2.40 [W927 22:39:57.515714273 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.41/2.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.41/2.40 % (3394157)------------------------------
% 9.41/2.40 % (3394157)------------------------------
% 9.41/2.40 % (3394163)Refutation not found, incomplete strategy
% 9.41/2.40 % (3394163)------------------------------
% 9.41/2.40 % (3394163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.41/2.40 % (3394163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.41/2.40 % (3394163)CaDiCaL version: 2.1.3
% 9.41/2.40 % (3394163)Termination reason: Refutation not found, incomplete strategy
% 9.41/2.40 % (3394163)Time elapsed: 0.014 s
% 9.41/2.40 % (3394163)Peak memory usage: 91 MB
% 9.41/2.40 % (3394163)Instructions burned: 51 (million)
% 9.41/2.40 % (3394162)Instruction limit reached!
% 9.41/2.40 % (3394162)------------------------------
% 9.41/2.40 % (3394162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.41/2.40 % (3394162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.41/2.40 % (3394162)CaDiCaL version: 2.1.3
% 9.41/2.40 % (3394162)Termination reason: Instruction limit
% 9.41/2.40 % (3394162)Termination phase: Property scanning
% 9.41/2.40 % (3394162)Time elapsed: 0.110 s
% 9.41/2.40 % (3394162)Peak memory usage: 93 MB
% 9.41/2.40 % (3394162)Instructions burned: 249 (million)
% 9.41/2.40 % (3394165)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1083644422:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 9.41/2.40 % (3394163)------------------------------
% 9.41/2.40 % (3394163)------------------------------
% 9.41/2.40 % (3394167)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=891499534:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 9.41/2.40 % (3394168)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1027172593:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 9.41/2.40 % (3394167)Instruction limit reached!
% 9.41/2.40 % (3394167)------------------------------
% 9.41/2.40 % (3394167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.41/2.40 % (3394167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.41/2.40 % (3394167)CaDiCaL version: 2.1.3
% 9.41/2.40 % (3394167)Termination reason: Instruction limit
% 9.41/2.40 % (3394167)Termination phase: Preprocessing 3
% 9.41/2.40 % (3394167)Time elapsed: 0.067 s
% 9.41/2.40 % (3394167)Peak memory usage: 91 MB
% 9.41/2.40 % (3394167)Instructions burned: 115 (million)
% 9.41/2.40 % (3394168)Instruction limit reached!
% 9.41/2.40 % (3394168)------------------------------
% 9.41/2.40 % (3394168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.41/2.40 % (3394168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.41/2.47 % (3394168)CaDiCaL version: 2.1.3
% 9.41/2.47 % (3394168)Termination reason: Instruction limit
% 9.41/2.47 % (3394168)Termination phase: Property scanning
% 9.41/2.47 % (3394168)Time elapsed: 0.062 s
% 9.41/2.47 % (3394168)Peak memory usage: 92 MB
% 9.41/2.47 % (3394168)Instructions burned: 129 (million)
% 9.41/2.47 % (3394170)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=760053758:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2989 on theBenchmark for (2989ds/114Mi)
% 9.41/2.47 % (3394170)Instruction limit reached!
% 9.41/2.47 % (3394170)------------------------------
% 9.41/2.47 % (3394170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.41/2.47 % (3394170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.41/2.47 % (3394170)CaDiCaL version: 2.1.3
% 9.41/2.47 % (3394170)Termination reason: Instruction limit
% 9.41/2.47 % (3394170)Termination phase: SInE selection
% 9.41/2.47 % (3394170)Time elapsed: 0.022 s
% 9.41/2.47 % (3394170)Peak memory usage: 89 MB
% 9.41/2.47 % (3394170)Instructions burned: 115 (million)
% 9.41/2.47 % (3394144)Refutation not found, incomplete strategy
% 9.41/2.47 % (3394144)------------------------------
% 9.41/2.47 % (3394144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.41/2.47 % (3394144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.41/2.47 % (3394144)CaDiCaL version: 2.1.3
% 9.41/2.47 % (3394144)Termination reason: Refutation not found, incomplete strategy
% 9.41/2.47 % (3394144)Time elapsed: 0.907 s
% 9.41/2.47 % (3394144)Peak memory usage: 148 MB
% 9.41/2.47 % (3394144)Instructions burned: 1502 (million)
% 9.41/2.47 % (3394173)lrs+10_1_sil=8000:sp=occurrence:random_seed=2470172188:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2988 on theBenchmark for (2988ds/907Mi)
% 9.41/2.47 % (3394174)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2941238924:i=437:sd=1:aac=none:ss=included_2988 on theBenchmark for (2988ds/437Mi)
% 9.41/2.47 % (3394173)Refutation not found, incomplete strategy
% 9.41/2.47 % (3394173)------------------------------
% 9.41/2.47 % (3394173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.41/2.47 % (3394173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.41/2.47 % (3394173)CaDiCaL version: 2.1.3
% 9.41/2.47 % (3394173)Termination reason: Refutation not found, incomplete strategy
% 9.41/2.47 % (3394173)Time elapsed: 0.026 s
% 9.41/2.47 % (3394173)Peak memory usage: 91 MB
% 9.41/2.47 % (3394173)Instructions burned: 51 (million)
% 9.41/2.47 % (3394176)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3537429066:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi)
% 9.41/2.47 % (3394142)First to succeed.
% 9.41/2.47 % (3394142)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3394137"
% 9.41/2.47 % (3394174)Refutation not found, incomplete strategy
% 9.41/2.47 % (3394174)------------------------------
% 9.41/2.47 % (3394174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.41/2.47 % (3394174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.41/2.47 % (3394174)CaDiCaL version: 2.1.3
% 9.41/2.47 % (3394174)Termination reason: Refutation not found, incomplete strategy
% 9.41/2.47 % (3394174)Time elapsed: 0.141 s
% 9.41/2.47 % (3394174)Peak memory usage: 98 MB
% 9.41/2.47 % (3394174)Instructions burned: 307 (million)
% 9.41/2.47 [W927 22:39:57.139483944 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.41/2.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.41/2.47 [W927 22:39:57.139542001 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.41/2.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.41/2.47 [W927 22:39:57.139578998 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.41/2.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.41/2.47 [W927 22:39:57.139591111 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.41/2.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.41/2.47 [W927 22:39:57.139621321 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.41/2.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.41/2.47 [W927 22:39:57.139631638 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.41/2.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.41/2.47 % (3394144)------------------------------
% 9.41/2.47 % (3394144)------------------------------
% 9.41/2.47 [W927 22:39:57.172462076 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.41/2.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.41/2.47 [W927 22:39:57.172485564 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.41/2.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.41/2.47 [W927 22:39:57.172507257 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.41/2.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.41/2.47 [W927 22:39:57.172514447 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.41/2.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.41/2.47 [W927 22:39:57.172528099 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.41/2.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.41/2.47 [W927 22:39:57.172534669 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.41/2.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.41/2.47 [W927 22:39:57.172548449 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.41/2.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.41/2.47 [W927 22:39:57.172555030 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.41/2.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.41/2.47 [W927 22:39:57.172567963 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.41/2.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.41/2.47 [W927 22:39:57.172574523 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.41/2.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.41/2.47 [W927 22:39:57.172587469 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.41/2.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.41/2.47 [W927 22:39:57.172593924 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.41/2.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.41/2.47 % (3394173)------------------------------
% 9.41/2.47 % (3394173)------------------------------
% 9.41/2.47 % SZS status Satisfiable for theBenchmark
% 9.41/2.47 % SZS output start Saturation.
% See solution above
% 10.76/2.67 % SZS output start Definitions and Model Updates.
% 10.76/2.67 % SZS output end Definitions and Model Updates.
% 10.76/2.67 % (3394142)------------------------------
% 10.76/2.67 % (3394142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.76/2.67 % (3394142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.76/2.67 % (3394142)CaDiCaL version: 2.1.3
% 10.76/2.67 % (3394142)Termination reason: Satisfiable
% 10.76/2.67 % (3394142)Time elapsed: 0.967 s
% 10.76/2.67 % (3394142)Peak memory usage: 162 MB
% 10.76/2.67 % (3394142)Instructions burned: 1581 (million)
% 10.76/2.67 % (3394142)------------------------------
% 10.76/2.67 % (3394142)------------------------------
% 10.76/2.67 % (3394137)Success in time 1.628 s
% 10.76/2.67 % Vampire exiting
%------------------------------------------------------------------------------