%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PUZ069+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 : n020.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:28 PM UTC 2026
% Result : Satisfiable 9.20s 2.46s
% Output : Saturation 10.53s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u31303,axiom,
~ p(n9,n9,n9) ).
cnf(u31307,axiom,
~ p(n9,n8,n9) ).
cnf(u31311,axiom,
~ p(n9,n7,n9) ).
cnf(u31315,axiom,
~ p(n8,n9,n9) ).
cnf(u31320,axiom,
p(n8,n8,n9) ).
cnf(u31323,axiom,
~ p(n8,n7,n9) ).
cnf(u31327,axiom,
~ p(n7,n9,n9) ).
cnf(u31331,axiom,
~ p(n7,n8,n9) ).
cnf(u31335,axiom,
~ p(n7,n7,n9) ).
cnf(u31340,axiom,
~ p(n9,n9,n8) ).
cnf(u31344,axiom,
~ p(n9,n8,n8) ).
cnf(u31348,axiom,
~ p(n9,n7,n8) ).
cnf(u31353,axiom,
p(n8,n9,n8) ).
cnf(u31356,axiom,
~ p(n8,n8,n8) ).
cnf(u31360,axiom,
~ p(n8,n7,n8) ).
cnf(u31364,axiom,
~ p(n7,n9,n8) ).
cnf(u31368,axiom,
~ p(n7,n8,n8) ).
cnf(u31372,axiom,
~ p(n7,n7,n8) ).
cnf(u31377,axiom,
~ p(n9,n9,n7) ).
cnf(u31381,axiom,
~ p(n9,n8,n7) ).
cnf(u31386,axiom,
p(n9,n7,n7) ).
cnf(u31389,axiom,
~ p(n8,n9,n7) ).
cnf(u31393,axiom,
~ p(n8,n8,n7) ).
cnf(u31397,axiom,
~ p(n8,n7,n7) ).
cnf(u31401,axiom,
~ p(n7,n9,n7) ).
cnf(u31405,axiom,
~ p(n7,n8,n7) ).
cnf(u31409,axiom,
~ p(n7,n7,n7) ).
cnf(u31414,axiom,
~ p(n9,n9,n6) ).
cnf(u31418,axiom,
~ p(n9,n8,n6) ).
cnf(u31422,axiom,
~ p(n9,n7,n6) ).
cnf(u31426,axiom,
~ p(n8,n9,n6) ).
cnf(u31430,axiom,
~ p(n8,n8,n6) ).
cnf(u31434,axiom,
~ p(n8,n7,n6) ).
cnf(u31438,axiom,
~ p(n7,n9,n6) ).
cnf(u31442,axiom,
~ p(n7,n8,n6) ).
cnf(u31447,axiom,
p(n7,n7,n6) ).
cnf(u31451,axiom,
~ p(n9,n9,n5) ).
cnf(u31456,axiom,
p(n9,n8,n5) ).
cnf(u31459,axiom,
~ p(n9,n7,n5) ).
cnf(u31463,axiom,
~ p(n8,n9,n5) ).
cnf(u31467,axiom,
~ p(n8,n8,n5) ).
cnf(u31471,axiom,
~ p(n8,n7,n5) ).
cnf(u31475,axiom,
~ p(n7,n9,n5) ).
cnf(u31479,axiom,
~ p(n7,n8,n5) ).
cnf(u31483,axiom,
~ p(n7,n7,n5) ).
cnf(u31489,axiom,
p(n9,n9,n4) ).
cnf(u31492,axiom,
~ p(n9,n8,n4) ).
cnf(u31496,axiom,
~ p(n9,n7,n4) ).
cnf(u31500,axiom,
~ p(n8,n9,n4) ).
cnf(u31504,axiom,
~ p(n8,n8,n4) ).
cnf(u31508,axiom,
~ p(n8,n7,n4) ).
cnf(u31512,axiom,
~ p(n7,n9,n4) ).
cnf(u31516,axiom,
~ p(n7,n8,n4) ).
cnf(u31520,axiom,
~ p(n7,n7,n4) ).
cnf(u31525,axiom,
~ p(n9,n9,n3) ).
cnf(u31529,axiom,
~ p(n9,n8,n3) ).
cnf(u31533,axiom,
~ p(n9,n7,n3) ).
cnf(u31537,axiom,
~ p(n8,n9,n3) ).
cnf(u31541,axiom,
~ p(n8,n8,n3) ).
cnf(u31545,axiom,
~ p(n8,n7,n3) ).
cnf(u31550,axiom,
p(n7,n9,n3) ).
cnf(u31553,axiom,
~ p(n7,n8,n3) ).
cnf(u31557,axiom,
~ p(n7,n7,n3) ).
cnf(u31562,axiom,
~ p(n9,n6,n9) ).
cnf(u31566,axiom,
~ p(n9,n5,n9) ).
cnf(u31570,axiom,
~ p(n9,n4,n9) ).
cnf(u31574,axiom,
~ p(n8,n6,n9) ).
cnf(u31578,axiom,
~ p(n8,n5,n9) ).
cnf(u31582,axiom,
~ p(n8,n4,n9) ).
cnf(u31586,axiom,
~ p(n7,n6,n9) ).
cnf(u31591,axiom,
p(n7,n5,n9) ).
cnf(u31594,axiom,
~ p(n7,n4,n9) ).
cnf(u31599,axiom,
~ p(n9,n6,n8) ).
cnf(u31604,axiom,
p(n9,n5,n8) ).
cnf(u31607,axiom,
~ p(n9,n4,n8) ).
cnf(u31611,axiom,
~ p(n8,n6,n8) ).
cnf(u31615,axiom,
~ p(n8,n5,n8) ).
cnf(u31619,axiom,
~ p(n8,n4,n8) ).
cnf(u31623,axiom,
~ p(n7,n6,n8) ).
cnf(u31627,axiom,
~ p(n7,n5,n8) ).
cnf(u31631,axiom,
~ p(n7,n4,n8) ).
cnf(u31636,axiom,
~ p(n9,n6,n6) ).
cnf(u31640,axiom,
~ p(n9,n5,n6) ).
cnf(u31644,axiom,
~ p(n9,n4,n6) ).
cnf(u31648,axiom,
~ p(n8,n6,n6) ).
cnf(u31653,axiom,
p(n8,n5,n6) ).
cnf(u31656,axiom,
~ p(n8,n4,n6) ).
cnf(u31660,axiom,
~ p(n7,n6,n6) ).
cnf(u31664,axiom,
~ p(n7,n5,n6) ).
cnf(u31668,axiom,
~ p(n7,n4,n6) ).
cnf(u31673,axiom,
~ p(n9,n6,n5) ).
cnf(u31677,axiom,
~ p(n9,n5,n5) ).
cnf(u31681,axiom,
~ p(n9,n4,n5) ).
cnf(u31685,axiom,
~ p(n8,n6,n5) ).
cnf(u31689,axiom,
~ p(n8,n5,n5) ).
cnf(u31694,axiom,
p(n8,n4,n5) ).
cnf(u31697,axiom,
~ p(n7,n6,n5) ).
cnf(u31701,axiom,
~ p(n7,n5,n5) ).
cnf(u31705,axiom,
~ p(n7,n4,n5) ).
cnf(u31710,axiom,
~ p(n9,n6,n4) ).
cnf(u31714,axiom,
~ p(n9,n5,n4) ).
cnf(u31718,axiom,
~ p(n9,n4,n4) ).
cnf(u31722,axiom,
~ p(n8,n6,n4) ).
cnf(u31726,axiom,
~ p(n8,n5,n4) ).
cnf(u31730,axiom,
~ p(n8,n4,n4) ).
cnf(u31735,axiom,
p(n7,n6,n4) ).
cnf(u31738,axiom,
~ p(n7,n5,n4) ).
cnf(u31742,axiom,
~ p(n7,n4,n4) ).
cnf(u31747,axiom,
~ p(n9,n6,n3) ).
cnf(u31751,axiom,
~ p(n9,n5,n3) ).
cnf(u31756,axiom,
p(n9,n4,n3) ).
cnf(u31759,axiom,
~ p(n8,n6,n3) ).
cnf(u31763,axiom,
~ p(n8,n5,n3) ).
cnf(u31767,axiom,
~ p(n8,n4,n3) ).
cnf(u31771,axiom,
~ p(n7,n6,n3) ).
cnf(u31775,axiom,
~ p(n7,n5,n3) ).
cnf(u31779,axiom,
~ p(n7,n4,n3) ).
cnf(u31785,axiom,
p(n9,n6,n2) ).
cnf(u31788,axiom,
~ p(n9,n5,n2) ).
cnf(u31792,axiom,
~ p(n9,n4,n2) ).
cnf(u31796,axiom,
~ p(n8,n6,n2) ).
cnf(u31800,axiom,
~ p(n8,n5,n2) ).
cnf(u31804,axiom,
~ p(n8,n4,n2) ).
cnf(u31808,axiom,
~ p(n7,n6,n2) ).
cnf(u31812,axiom,
~ p(n7,n5,n2) ).
cnf(u31816,axiom,
~ p(n7,n4,n2) ).
cnf(u31821,axiom,
~ p(n9,n6,n1) ).
cnf(u31825,axiom,
~ p(n9,n5,n1) ).
cnf(u31829,axiom,
~ p(n9,n4,n1) ).
cnf(u31834,axiom,
p(n8,n6,n1) ).
cnf(u31837,axiom,
~ p(n8,n5,n1) ).
cnf(u31841,axiom,
~ p(n8,n4,n1) ).
cnf(u31845,axiom,
~ p(n7,n6,n1) ).
cnf(u31849,axiom,
~ p(n7,n5,n1) ).
cnf(u31853,axiom,
~ p(n7,n4,n1) ).
cnf(u31859,axiom,
p(n9,n3,n9) ).
cnf(u31862,axiom,
~ p(n9,n2,n9) ).
cnf(u31866,axiom,
~ p(n9,n1,n9) ).
cnf(u31870,axiom,
~ p(n8,n3,n9) ).
cnf(u31874,axiom,
~ p(n8,n2,n9) ).
cnf(u31878,axiom,
~ p(n8,n1,n9) ).
cnf(u31882,axiom,
~ p(n7,n3,n9) ).
cnf(u31886,axiom,
~ p(n7,n2,n9) ).
cnf(u31890,axiom,
~ p(n7,n1,n9) ).
cnf(u31895,axiom,
~ p(n9,n3,n8) ).
cnf(u31899,axiom,
~ p(n9,n2,n8) ).
cnf(u31903,axiom,
~ p(n9,n1,n8) ).
cnf(u31907,axiom,
~ p(n8,n3,n8) ).
cnf(u31911,axiom,
~ p(n8,n2,n8) ).
cnf(u31915,axiom,
~ p(n8,n1,n8) ).
cnf(u31919,axiom,
~ p(n7,n3,n8) ).
cnf(u31924,axiom,
p(n7,n2,n8) ).
cnf(u31927,axiom,
~ p(n7,n1,n8) ).
cnf(u31932,axiom,
~ p(n9,n3,n7) ).
cnf(u31936,axiom,
~ p(n9,n2,n7) ).
cnf(u31940,axiom,
~ p(n9,n1,n7) ).
cnf(u31944,axiom,
~ p(n8,n3,n7) ).
cnf(u31948,axiom,
~ p(n8,n2,n7) ).
cnf(u31953,axiom,
p(n8,n1,n7) ).
cnf(u31956,axiom,
~ p(n7,n3,n7) ).
cnf(u31960,axiom,
~ p(n7,n2,n7) ).
cnf(u31964,axiom,
~ p(n7,n1,n7) ).
cnf(u31969,axiom,
~ p(n9,n3,n6) ).
cnf(u31973,axiom,
~ p(n9,n2,n6) ).
cnf(u31978,axiom,
p(n9,n1,n6) ).
cnf(u31981,axiom,
~ p(n8,n3,n6) ).
cnf(u31985,axiom,
~ p(n8,n2,n6) ).
cnf(u31989,axiom,
~ p(n8,n1,n6) ).
cnf(u31993,axiom,
~ p(n7,n3,n6) ).
cnf(u31997,axiom,
~ p(n7,n2,n6) ).
cnf(u32001,axiom,
~ p(n7,n1,n6) ).
cnf(u32006,axiom,
~ p(n9,n3,n5) ).
cnf(u32010,axiom,
~ p(n9,n2,n5) ).
cnf(u32014,axiom,
~ p(n9,n1,n5) ).
cnf(u32018,axiom,
~ p(n8,n3,n5) ).
cnf(u32022,axiom,
~ p(n8,n2,n5) ).
cnf(u32026,axiom,
~ p(n8,n1,n5) ).
cnf(u32031,axiom,
p(n7,n3,n5) ).
cnf(u32034,axiom,
~ p(n7,n2,n5) ).
cnf(u32038,axiom,
~ p(n7,n1,n5) ).
cnf(u32043,axiom,
~ p(n9,n3,n4) ).
cnf(u32047,axiom,
~ p(n9,n2,n4) ).
cnf(u32051,axiom,
~ p(n9,n1,n4) ).
cnf(u32056,axiom,
p(n8,n3,n4) ).
cnf(u32059,axiom,
~ p(n8,n2,n4) ).
cnf(u32063,axiom,
~ p(n8,n1,n4) ).
cnf(u32067,axiom,
~ p(n7,n3,n4) ).
cnf(u32071,axiom,
~ p(n7,n2,n4) ).
cnf(u32075,axiom,
~ p(n7,n1,n4) ).
cnf(u32080,axiom,
~ p(n9,n3,n2) ).
cnf(u32084,axiom,
~ p(n9,n2,n2) ).
cnf(u32088,axiom,
~ p(n9,n1,n2) ).
cnf(u32092,axiom,
~ p(n8,n3,n2) ).
cnf(u32096,axiom,
~ p(n8,n2,n2) ).
cnf(u32100,axiom,
~ p(n8,n1,n2) ).
cnf(u32104,axiom,
~ p(n7,n3,n2) ).
cnf(u32108,axiom,
~ p(n7,n2,n2) ).
cnf(u32113,axiom,
p(n7,n1,n2) ).
cnf(u32117,axiom,
~ p(n9,n3,n1) ).
cnf(u32122,axiom,
p(n9,n2,n1) ).
cnf(u32125,axiom,
~ p(n9,n1,n1) ).
cnf(u32129,axiom,
~ p(n8,n3,n1) ).
cnf(u32133,axiom,
~ p(n8,n2,n1) ).
cnf(u32137,axiom,
~ p(n8,n1,n1) ).
cnf(u32141,axiom,
~ p(n7,n3,n1) ).
cnf(u32145,axiom,
~ p(n7,n2,n1) ).
cnf(u32149,axiom,
~ p(n7,n1,n1) ).
cnf(u32154,axiom,
~ p(n6,n9,n9) ).
cnf(u32158,axiom,
~ p(n6,n8,n9) ).
cnf(u32162,axiom,
~ p(n6,n7,n9) ).
cnf(u32166,axiom,
~ p(n5,n9,n9) ).
cnf(u32170,axiom,
~ p(n5,n8,n9) ).
cnf(u32174,axiom,
~ p(n5,n7,n9) ).
cnf(u32178,axiom,
~ p(n4,n9,n9) ).
cnf(u32182,axiom,
~ p(n4,n8,n9) ).
cnf(u32187,axiom,
p(n4,n7,n9) ).
cnf(u32191,axiom,
~ p(n6,n9,n8) ).
cnf(u32196,axiom,
p(n6,n8,n8) ).
cnf(u32199,axiom,
~ p(n6,n7,n8) ).
cnf(u32203,axiom,
~ p(n5,n9,n8) ).
cnf(u32207,axiom,
~ p(n5,n8,n8) ).
cnf(u32211,axiom,
~ p(n5,n7,n8) ).
cnf(u32215,axiom,
~ p(n4,n9,n8) ).
cnf(u32219,axiom,
~ p(n4,n8,n8) ).
cnf(u32223,axiom,
~ p(n4,n7,n8) ).
cnf(u32229,axiom,
p(n6,n9,n7) ).
cnf(u32232,axiom,
~ p(n6,n8,n7) ).
cnf(u32236,axiom,
~ p(n6,n7,n7) ).
cnf(u32240,axiom,
~ p(n5,n9,n7) ).
cnf(u32244,axiom,
~ p(n5,n8,n7) ).
cnf(u32248,axiom,
~ p(n5,n7,n7) ).
cnf(u32252,axiom,
~ p(n4,n9,n7) ).
cnf(u32256,axiom,
~ p(n4,n8,n7) ).
cnf(u32260,axiom,
~ p(n4,n7,n7) ).
cnf(u32265,axiom,
~ p(n6,n9,n5) ).
cnf(u32269,axiom,
~ p(n6,n8,n5) ).
cnf(u32273,axiom,
~ p(n6,n7,n5) ).
cnf(u32277,axiom,
~ p(n5,n9,n5) ).
cnf(u32281,axiom,
~ p(n5,n8,n5) ).
cnf(u32285,axiom,
~ p(n5,n7,n5) ).
cnf(u32290,axiom,
p(n4,n9,n5) ).
cnf(u32293,axiom,
~ p(n4,n8,n5) ).
cnf(u32297,axiom,
~ p(n4,n7,n5) ).
cnf(u32302,axiom,
~ p(n6,n9,n4) ).
cnf(u32306,axiom,
~ p(n6,n8,n4) ).
cnf(u32310,axiom,
~ p(n6,n7,n4) ).
cnf(u32314,axiom,
~ p(n5,n9,n4) ).
cnf(u32318,axiom,
~ p(n5,n8,n4) ).
cnf(u32323,axiom,
p(n5,n7,n4) ).
cnf(u32326,axiom,
~ p(n4,n9,n4) ).
cnf(u32330,axiom,
~ p(n4,n8,n4) ).
cnf(u32334,axiom,
~ p(n4,n7,n4) ).
cnf(u32339,axiom,
~ p(n6,n9,n3) ).
cnf(u32343,axiom,
~ p(n6,n8,n3) ).
cnf(u32347,axiom,
~ p(n6,n7,n3) ).
cnf(u32351,axiom,
~ p(n5,n9,n3) ).
cnf(u32355,axiom,
~ p(n5,n8,n3) ).
cnf(u32359,axiom,
~ p(n5,n7,n3) ).
cnf(u32363,axiom,
~ p(n4,n9,n3) ).
cnf(u32368,axiom,
p(n4,n8,n3) ).
cnf(u32371,axiom,
~ p(n4,n7,n3) ).
cnf(u32376,axiom,
~ p(n6,n9,n2) ).
cnf(u32380,axiom,
~ p(n6,n8,n2) ).
cnf(u32384,axiom,
~ p(n6,n7,n2) ).
cnf(u32389,axiom,
p(n5,n9,n2) ).
cnf(u32392,axiom,
~ p(n5,n8,n2) ).
cnf(u32396,axiom,
~ p(n5,n7,n2) ).
cnf(u32400,axiom,
~ p(n4,n9,n2) ).
cnf(u32404,axiom,
~ p(n4,n8,n2) ).
cnf(u32408,axiom,
~ p(n4,n7,n2) ).
cnf(u32413,axiom,
~ p(n6,n9,n1) ).
cnf(u32417,axiom,
~ p(n6,n8,n1) ).
cnf(u32422,axiom,
p(n6,n7,n1) ).
cnf(u32425,axiom,
~ p(n5,n9,n1) ).
cnf(u32429,axiom,
~ p(n5,n8,n1) ).
cnf(u32433,axiom,
~ p(n5,n7,n1) ).
cnf(u32437,axiom,
~ p(n4,n9,n1) ).
cnf(u32441,axiom,
~ p(n4,n8,n1) ).
cnf(u32445,axiom,
~ p(n4,n7,n1) ).
cnf(u32450,axiom,
~ p(n6,n6,n9) ).
cnf(u32454,axiom,
~ p(n6,n5,n9) ).
cnf(u32459,axiom,
p(n6,n4,n9) ).
cnf(u32462,axiom,
~ p(n5,n6,n9) ).
cnf(u32466,axiom,
~ p(n5,n5,n9) ).
cnf(u32470,axiom,
~ p(n5,n4,n9) ).
cnf(u32474,axiom,
~ p(n4,n6,n9) ).
cnf(u32478,axiom,
~ p(n4,n5,n9) ).
cnf(u32482,axiom,
~ p(n4,n4,n9) ).
cnf(u32487,axiom,
~ p(n6,n6,n8) ).
cnf(u32491,axiom,
~ p(n6,n5,n8) ).
cnf(u32495,axiom,
~ p(n6,n4,n8) ).
cnf(u32499,axiom,
~ p(n5,n6,n8) ).
cnf(u32503,axiom,
~ p(n5,n5,n8) ).
cnf(u32508,axiom,
p(n5,n4,n8) ).
cnf(u32511,axiom,
~ p(n4,n6,n8) ).
cnf(u32515,axiom,
~ p(n4,n5,n8) ).
cnf(u32519,axiom,
~ p(n4,n4,n8) ).
cnf(u32524,axiom,
~ p(n6,n6,n7) ).
cnf(u32528,axiom,
~ p(n6,n5,n7) ).
cnf(u32532,axiom,
~ p(n6,n4,n7) ).
cnf(u32537,axiom,
p(n5,n6,n7) ).
cnf(u32540,axiom,
~ p(n5,n5,n7) ).
cnf(u32544,axiom,
~ p(n5,n4,n7) ).
cnf(u32548,axiom,
~ p(n4,n6,n7) ).
cnf(u32552,axiom,
~ p(n4,n5,n7) ).
cnf(u32556,axiom,
~ p(n4,n4,n7) ).
cnf(u32561,axiom,
~ p(n6,n6,n6) ).
cnf(u32565,axiom,
~ p(n6,n5,n6) ).
cnf(u32569,axiom,
~ p(n6,n4,n6) ).
cnf(u32573,axiom,
~ p(n5,n6,n6) ).
cnf(u32577,axiom,
~ p(n5,n5,n6) ).
cnf(u32581,axiom,
~ p(n5,n4,n6) ).
cnf(u32586,axiom,
p(n4,n6,n6) ).
cnf(u32589,axiom,
~ p(n4,n5,n6) ).
cnf(u32593,axiom,
~ p(n4,n4,n6) ).
cnf(u32598,axiom,
~ p(n6,n6,n1) ).
cnf(u32602,axiom,
~ p(n6,n5,n1) ).
cnf(u32606,axiom,
~ p(n6,n4,n1) ).
cnf(u32610,axiom,
~ p(n5,n6,n1) ).
cnf(u32615,axiom,
p(n5,n5,n1) ).
cnf(u32618,axiom,
~ p(n5,n4,n1) ).
cnf(u32622,axiom,
~ p(n4,n6,n1) ).
cnf(u32626,axiom,
~ p(n4,n5,n1) ).
cnf(u32630,axiom,
~ p(n4,n4,n1) ).
cnf(u32635,axiom,
~ p(n6,n3,n8) ).
cnf(u32639,axiom,
~ p(n6,n2,n8) ).
cnf(u32643,axiom,
~ p(n6,n1,n8) ).
cnf(u32647,axiom,
~ p(n5,n3,n8) ).
cnf(u32651,axiom,
~ p(n5,n2,n8) ).
cnf(u32655,axiom,
~ p(n5,n1,n8) ).
cnf(u32659,axiom,
~ p(n4,n3,n8) ).
cnf(u32663,axiom,
~ p(n4,n2,n8) ).
cnf(u32668,axiom,
p(n4,n1,n8) ).
cnf(u32672,axiom,
~ p(n6,n3,n7) ).
cnf(u32676,axiom,
~ p(n6,n2,n7) ).
cnf(u32680,axiom,
~ p(n6,n1,n7) ).
cnf(u32684,axiom,
~ p(n5,n3,n7) ).
cnf(u32688,axiom,
~ p(n5,n2,n7) ).
cnf(u32692,axiom,
~ p(n5,n1,n7) ).
cnf(u32696,axiom,
~ p(n4,n3,n7) ).
cnf(u32701,axiom,
p(n4,n2,n7) ).
cnf(u32704,axiom,
~ p(n4,n1,n7) ).
cnf(u32709,axiom,
~ p(n6,n3,n6) ).
cnf(u32714,axiom,
p(n6,n2,n6) ).
cnf(u32717,axiom,
~ p(n6,n1,n6) ).
cnf(u32721,axiom,
~ p(n5,n3,n6) ).
cnf(u32725,axiom,
~ p(n5,n2,n6) ).
cnf(u32729,axiom,
~ p(n5,n1,n6) ).
cnf(u32733,axiom,
~ p(n4,n3,n6) ).
cnf(u32737,axiom,
~ p(n4,n2,n6) ).
cnf(u32741,axiom,
~ p(n4,n1,n6) ).
cnf(u32746,axiom,
~ p(n6,n3,n5) ).
cnf(u32750,axiom,
~ p(n6,n2,n5) ).
cnf(u32754,axiom,
~ p(n6,n1,n5) ).
cnf(u32758,axiom,
~ p(n5,n3,n5) ).
cnf(u32763,axiom,
p(n5,n2,n5) ).
cnf(u32766,axiom,
~ p(n5,n1,n5) ).
cnf(u32770,axiom,
~ p(n4,n3,n5) ).
cnf(u32774,axiom,
~ p(n4,n2,n5) ).
cnf(u32778,axiom,
~ p(n4,n1,n5) ).
cnf(u32783,axiom,
~ p(n6,n3,n4) ).
cnf(u32787,axiom,
~ p(n6,n2,n4) ).
cnf(u32792,axiom,
p(n6,n1,n4) ).
cnf(u32795,axiom,
~ p(n5,n3,n4) ).
cnf(u32799,axiom,
~ p(n5,n2,n4) ).
cnf(u32803,axiom,
~ p(n5,n1,n4) ).
cnf(u32807,axiom,
~ p(n4,n3,n4) ).
cnf(u32811,axiom,
~ p(n4,n2,n4) ).
cnf(u32815,axiom,
~ p(n4,n1,n4) ).
cnf(u32820,axiom,
~ p(n6,n3,n3) ).
cnf(u32824,axiom,
~ p(n6,n2,n3) ).
cnf(u32828,axiom,
~ p(n6,n1,n3) ).
cnf(u32833,axiom,
p(n5,n3,n3) ).
cnf(u32836,axiom,
~ p(n5,n2,n3) ).
cnf(u32840,axiom,
~ p(n5,n1,n3) ).
cnf(u32844,axiom,
~ p(n4,n3,n3) ).
cnf(u32848,axiom,
~ p(n4,n2,n3) ).
cnf(u32852,axiom,
~ p(n4,n1,n3) ).
cnf(u32858,axiom,
p(n6,n3,n2) ).
cnf(u32861,axiom,
~ p(n6,n2,n2) ).
cnf(u32865,axiom,
~ p(n6,n1,n2) ).
cnf(u32869,axiom,
~ p(n5,n3,n2) ).
cnf(u32873,axiom,
~ p(n5,n2,n2) ).
cnf(u32877,axiom,
~ p(n5,n1,n2) ).
cnf(u32881,axiom,
~ p(n4,n3,n2) ).
cnf(u32885,axiom,
~ p(n4,n2,n2) ).
cnf(u32889,axiom,
~ p(n4,n1,n2) ).
cnf(u32894,axiom,
~ p(n6,n3,n1) ).
cnf(u32898,axiom,
~ p(n6,n2,n1) ).
cnf(u32902,axiom,
~ p(n6,n1,n1) ).
cnf(u32906,axiom,
~ p(n5,n3,n1) ).
cnf(u32910,axiom,
~ p(n5,n2,n1) ).
cnf(u32914,axiom,
~ p(n5,n1,n1) ).
cnf(u32919,axiom,
p(n4,n3,n1) ).
cnf(u32922,axiom,
~ p(n4,n2,n1) ).
cnf(u32926,axiom,
~ p(n4,n1,n1) ).
cnf(u32931,axiom,
~ p(n3,n9,n9) ).
cnf(u32935,axiom,
~ p(n3,n8,n9) ).
cnf(u32939,axiom,
~ p(n3,n7,n9) ).
cnf(u32943,axiom,
~ p(n2,n9,n9) ).
cnf(u32947,axiom,
~ p(n2,n8,n9) ).
cnf(u32951,axiom,
~ p(n2,n7,n9) ).
cnf(u32956,axiom,
p(n1,n9,n9) ).
cnf(u32959,axiom,
~ p(n1,n8,n9) ).
cnf(u32963,axiom,
~ p(n1,n7,n9) ).
cnf(u32968,axiom,
~ p(n3,n9,n8) ).
cnf(u32972,axiom,
~ p(n3,n8,n8) ).
cnf(u32976,axiom,
~ p(n3,n7,n8) ).
cnf(u32980,axiom,
~ p(n2,n9,n8) ).
cnf(u32984,axiom,
~ p(n2,n8,n8) ).
cnf(u32988,axiom,
~ p(n2,n7,n8) ).
cnf(u32992,axiom,
~ p(n1,n9,n8) ).
cnf(u32996,axiom,
~ p(n1,n8,n8) ).
cnf(u33001,axiom,
p(n1,n7,n8) ).
cnf(u33005,axiom,
~ p(n3,n9,n7) ).
cnf(u33009,axiom,
~ p(n3,n8,n7) ).
cnf(u33013,axiom,
~ p(n3,n7,n7) ).
cnf(u33017,axiom,
~ p(n2,n9,n7) ).
cnf(u33022,axiom,
p(n2,n8,n7) ).
cnf(u33025,axiom,
~ p(n2,n7,n7) ).
cnf(u33029,axiom,
~ p(n1,n9,n7) ).
cnf(u33033,axiom,
~ p(n1,n8,n7) ).
cnf(u33037,axiom,
~ p(n1,n7,n7) ).
cnf(u33043,axiom,
p(n3,n9,n6) ).
cnf(u33046,axiom,
~ p(n3,n8,n6) ).
cnf(u33050,axiom,
~ p(n3,n7,n6) ).
cnf(u33054,axiom,
~ p(n2,n9,n6) ).
cnf(u33058,axiom,
~ p(n2,n8,n6) ).
cnf(u33062,axiom,
~ p(n2,n7,n6) ).
cnf(u33066,axiom,
~ p(n1,n9,n6) ).
cnf(u33070,axiom,
~ p(n1,n8,n6) ).
cnf(u33074,axiom,
~ p(n1,n7,n6) ).
cnf(u33079,axiom,
~ p(n3,n9,n4) ).
cnf(u33084,axiom,
p(n3,n8,n4) ).
cnf(u33087,axiom,
~ p(n3,n7,n4) ).
cnf(u33091,axiom,
~ p(n2,n9,n4) ).
cnf(u33095,axiom,
~ p(n2,n8,n4) ).
cnf(u33099,axiom,
~ p(n2,n7,n4) ).
cnf(u33103,axiom,
~ p(n1,n9,n4) ).
cnf(u33107,axiom,
~ p(n1,n8,n4) ).
cnf(u33111,axiom,
~ p(n1,n7,n4) ).
cnf(u33116,axiom,
~ p(n3,n9,n2) ).
cnf(u33120,axiom,
~ p(n3,n8,n2) ).
cnf(u33124,axiom,
~ p(n3,n7,n2) ).
cnf(u33128,axiom,
~ p(n2,n9,n2) ).
cnf(u33132,axiom,
~ p(n2,n8,n2) ).
cnf(u33136,axiom,
~ p(n2,n7,n2) ).
cnf(u33140,axiom,
~ p(n1,n9,n2) ).
cnf(u33145,axiom,
p(n1,n8,n2) ).
cnf(u33148,axiom,
~ p(n1,n7,n2) ).
cnf(u33153,axiom,
~ p(n3,n9,n1) ).
cnf(u33157,axiom,
~ p(n3,n8,n1) ).
cnf(u33161,axiom,
~ p(n3,n7,n1) ).
cnf(u33166,axiom,
p(n2,n9,n1) ).
cnf(u33169,axiom,
~ p(n2,n8,n1) ).
cnf(u33173,axiom,
~ p(n2,n7,n1) ).
cnf(u33177,axiom,
~ p(n1,n9,n1) ).
cnf(u33181,axiom,
~ p(n1,n8,n1) ).
cnf(u33185,axiom,
~ p(n1,n7,n1) ).
cnf(u33191,axiom,
p(n3,n6,n9) ).
cnf(u33194,axiom,
~ p(n3,n5,n9) ).
cnf(u33198,axiom,
~ p(n3,n4,n9) ).
cnf(u33202,axiom,
~ p(n2,n6,n9) ).
cnf(u33206,axiom,
~ p(n2,n5,n9) ).
cnf(u33210,axiom,
~ p(n2,n4,n9) ).
cnf(u33214,axiom,
~ p(n1,n6,n9) ).
cnf(u33218,axiom,
~ p(n1,n5,n9) ).
cnf(u33222,axiom,
~ p(n1,n4,n9) ).
cnf(u33227,axiom,
~ p(n3,n6,n7) ).
cnf(u33232,axiom,
p(n3,n5,n7) ).
cnf(u33235,axiom,
~ p(n3,n4,n7) ).
cnf(u33239,axiom,
~ p(n2,n6,n7) ).
cnf(u33243,axiom,
~ p(n2,n5,n7) ).
cnf(u33247,axiom,
~ p(n2,n4,n7) ).
cnf(u33251,axiom,
~ p(n1,n6,n7) ).
cnf(u33255,axiom,
~ p(n1,n5,n7) ).
cnf(u33259,axiom,
~ p(n1,n4,n7) ).
cnf(u33264,axiom,
~ p(n3,n6,n5) ).
cnf(u33268,axiom,
~ p(n3,n5,n5) ).
cnf(u33272,axiom,
~ p(n3,n4,n5) ).
cnf(u33276,axiom,
~ p(n2,n6,n5) ).
cnf(u33280,axiom,
~ p(n2,n5,n5) ).
cnf(u33284,axiom,
~ p(n2,n4,n5) ).
cnf(u33289,axiom,
p(n1,n6,n5) ).
cnf(u33292,axiom,
~ p(n1,n5,n5) ).
cnf(u33296,axiom,
~ p(n1,n4,n5) ).
cnf(u33301,axiom,
~ p(n3,n6,n4) ).
cnf(u33305,axiom,
~ p(n3,n5,n4) ).
cnf(u33309,axiom,
~ p(n3,n4,n4) ).
cnf(u33313,axiom,
~ p(n2,n6,n4) ).
cnf(u33317,axiom,
~ p(n2,n5,n4) ).
cnf(u33322,axiom,
p(n2,n4,n4) ).
cnf(u33325,axiom,
~ p(n1,n6,n4) ).
cnf(u33329,axiom,
~ p(n1,n5,n4) ).
cnf(u33333,axiom,
~ p(n1,n4,n4) ).
cnf(u33338,axiom,
~ p(n3,n6,n3) ).
cnf(u33342,axiom,
~ p(n3,n5,n3) ).
cnf(u33346,axiom,
~ p(n3,n4,n3) ).
cnf(u33350,axiom,
~ p(n2,n6,n3) ).
cnf(u33354,axiom,
~ p(n2,n5,n3) ).
cnf(u33358,axiom,
~ p(n2,n4,n3) ).
cnf(u33362,axiom,
~ p(n1,n6,n3) ).
cnf(u33367,axiom,
p(n1,n5,n3) ).
cnf(u33370,axiom,
~ p(n1,n4,n3) ).
cnf(u33375,axiom,
~ p(n3,n6,n2) ).
cnf(u33379,axiom,
~ p(n3,n5,n2) ).
cnf(u33383,axiom,
~ p(n3,n4,n2) ).
cnf(u33387,axiom,
~ p(n2,n6,n2) ).
cnf(u33392,axiom,
p(n2,n5,n2) ).
cnf(u33395,axiom,
~ p(n2,n4,n2) ).
cnf(u33399,axiom,
~ p(n1,n6,n2) ).
cnf(u33403,axiom,
~ p(n1,n5,n2) ).
cnf(u33407,axiom,
~ p(n1,n4,n2) ).
cnf(u33412,axiom,
~ p(n3,n6,n1) ).
cnf(u33416,axiom,
~ p(n3,n5,n1) ).
cnf(u33421,axiom,
p(n3,n4,n1) ).
cnf(u33424,axiom,
~ p(n2,n6,n1) ).
cnf(u33428,axiom,
~ p(n2,n5,n1) ).
cnf(u33432,axiom,
~ p(n2,n4,n1) ).
cnf(u33436,axiom,
~ p(n1,n6,n1) ).
cnf(u33440,axiom,
~ p(n1,n5,n1) ).
cnf(u33444,axiom,
~ p(n1,n4,n1) ).
cnf(u33449,axiom,
~ p(n3,n3,n9) ).
cnf(u33453,axiom,
~ p(n3,n2,n9) ).
cnf(u33457,axiom,
~ p(n3,n1,n9) ).
cnf(u33461,axiom,
~ p(n2,n3,n9) ).
cnf(u33466,axiom,
p(n2,n2,n9) ).
cnf(u33469,axiom,
~ p(n2,n1,n9) ).
cnf(u33473,axiom,
~ p(n1,n3,n9) ).
cnf(u33477,axiom,
~ p(n1,n2,n9) ).
cnf(u33481,axiom,
~ p(n1,n1,n9) ).
cnf(u33487,axiom,
p(n3,n3,n8) ).
cnf(u33490,axiom,
~ p(n3,n2,n8) ).
cnf(u33494,axiom,
~ p(n3,n1,n8) ).
cnf(u33498,axiom,
~ p(n2,n3,n8) ).
cnf(u33502,axiom,
~ p(n2,n2,n8) ).
cnf(u33506,axiom,
~ p(n2,n1,n8) ).
cnf(u33510,axiom,
~ p(n1,n3,n8) ).
cnf(u33514,axiom,
~ p(n1,n2,n8) ).
cnf(u33518,axiom,
~ p(n1,n1,n8) ).
cnf(u33523,axiom,
~ p(n3,n3,n6) ).
cnf(u33527,axiom,
~ p(n3,n2,n6) ).
cnf(u33531,axiom,
~ p(n3,n1,n6) ).
cnf(u33536,axiom,
p(n2,n3,n6) ).
cnf(u33539,axiom,
~ p(n2,n2,n6) ).
cnf(u33543,axiom,
~ p(n2,n1,n6) ).
cnf(u33547,axiom,
~ p(n1,n3,n6) ).
cnf(u33551,axiom,
~ p(n1,n2,n6) ).
cnf(u33555,axiom,
~ p(n1,n1,n6) ).
cnf(u33560,axiom,
~ p(n3,n3,n5) ).
cnf(u33564,axiom,
~ p(n3,n2,n5) ).
cnf(u33569,axiom,
p(n3,n1,n5) ).
cnf(u33572,axiom,
~ p(n2,n3,n5) ).
cnf(u33576,axiom,
~ p(n2,n2,n5) ).
cnf(u33580,axiom,
~ p(n2,n1,n5) ).
cnf(u33584,axiom,
~ p(n1,n3,n5) ).
cnf(u33588,axiom,
~ p(n1,n2,n5) ).
cnf(u33592,axiom,
~ p(n1,n1,n5) ).
cnf(u33597,axiom,
~ p(n3,n3,n4) ).
cnf(u33601,axiom,
~ p(n3,n2,n4) ).
cnf(u33605,axiom,
~ p(n3,n1,n4) ).
cnf(u33609,axiom,
~ p(n2,n3,n4) ).
cnf(u33613,axiom,
~ p(n2,n2,n4) ).
cnf(u33617,axiom,
~ p(n2,n1,n4) ).
cnf(u33621,axiom,
~ p(n1,n3,n4) ).
cnf(u33626,axiom,
p(n1,n2,n4) ).
cnf(u33629,axiom,
~ p(n1,n1,n4) ).
cnf(u33634,axiom,
~ p(n3,n3,n3) ).
cnf(u33638,axiom,
~ p(n3,n2,n3) ).
cnf(u33642,axiom,
~ p(n3,n1,n3) ).
cnf(u33646,axiom,
~ p(n2,n3,n3) ).
cnf(u33650,axiom,
~ p(n2,n2,n3) ).
cnf(u33655,axiom,
p(n2,n1,n3) ).
cnf(u33658,axiom,
~ p(n1,n3,n3) ).
cnf(u33662,axiom,
~ p(n1,n2,n3) ).
cnf(u33666,axiom,
~ p(n1,n1,n3) ).
cnf(u33671,axiom,
~ p(n9,n9,n2) ).
cnf(u33675,axiom,
~ p(n9,n9,n1) ).
cnf(u33680,axiom,
~ p(n9,n8,n2) ).
cnf(u33684,axiom,
~ p(n9,n8,n1) ).
cnf(u33689,axiom,
~ p(n9,n7,n2) ).
cnf(u33693,axiom,
~ p(n9,n7,n1) ).
cnf(u33698,axiom,
~ p(n9,n6,n7) ).
cnf(u33703,axiom,
~ p(n9,n5,n7) ).
cnf(u33708,axiom,
~ p(n9,n4,n7) ).
cnf(u33713,axiom,
~ p(n9,n3,n3) ).
cnf(u33718,axiom,
~ p(n9,n2,n3) ).
cnf(u33723,axiom,
~ p(n9,n1,n3) ).
cnf(u33728,axiom,
~ p(n8,n9,n2) ).
cnf(u33732,axiom,
~ p(n8,n9,n1) ).
cnf(u33737,axiom,
~ p(n8,n8,n2) ).
cnf(u33741,axiom,
~ p(n8,n8,n1) ).
cnf(u33746,axiom,
~ p(n8,n6,n7) ).
cnf(u33751,axiom,
~ p(n8,n5,n7) ).
cnf(u33756,axiom,
~ p(n8,n4,n7) ).
cnf(u33761,axiom,
~ p(n8,n3,n3) ).
cnf(u33766,axiom,
~ p(n8,n1,n3) ).
cnf(u33771,axiom,
~ p(n7,n9,n2) ).
cnf(u33775,axiom,
~ p(n7,n9,n1) ).
cnf(u33780,axiom,
~ p(n7,n7,n2) ).
cnf(u33784,axiom,
~ p(n7,n7,n1) ).
cnf(u33789,axiom,
~ p(n7,n6,n7) ).
cnf(u33794,axiom,
~ p(n7,n5,n7) ).
cnf(u33799,axiom,
~ p(n7,n3,n3) ).
cnf(u33804,axiom,
~ p(n7,n2,n3) ).
cnf(u33809,axiom,
~ p(n7,n1,n3) ).
cnf(u33814,axiom,
~ p(n6,n9,n6) ).
cnf(u33819,axiom,
~ p(n6,n8,n6) ).
cnf(u33824,axiom,
~ p(n6,n7,n6) ).
cnf(u33829,axiom,
~ p(n6,n4,n5) ).
cnf(u33833,axiom,
~ p(n6,n4,n4) ).
cnf(u33837,axiom,
~ p(n6,n4,n3) ).
cnf(u33841,axiom,
~ p(n6,n4,n2) ).
cnf(u33846,axiom,
~ p(n6,n3,n9) ).
cnf(u33851,axiom,
~ p(n6,n2,n9) ).
cnf(u33856,axiom,
~ p(n6,n1,n9) ).
cnf(u33861,axiom,
~ p(n5,n9,n6) ).
cnf(u33866,axiom,
~ p(n5,n7,n6) ).
cnf(u33871,axiom,
~ p(n5,n6,n5) ).
cnf(u33875,axiom,
~ p(n5,n6,n4) ).
cnf(u33879,axiom,
~ p(n5,n6,n3) ).
cnf(u33883,axiom,
~ p(n5,n6,n2) ).
cnf(u33888,axiom,
~ p(n5,n5,n5) ).
cnf(u33892,axiom,
~ p(n5,n5,n4) ).
cnf(u33896,axiom,
~ p(n5,n5,n3) ).
cnf(u33900,axiom,
~ p(n5,n5,n2) ).
cnf(u33905,axiom,
~ p(n5,n4,n5) ).
cnf(u33909,axiom,
~ p(n5,n4,n4) ).
cnf(u33913,axiom,
~ p(n5,n4,n3) ).
cnf(u33917,axiom,
~ p(n5,n4,n2) ).
cnf(u33922,axiom,
~ p(n5,n3,n9) ).
cnf(u33927,axiom,
~ p(n5,n2,n9) ).
cnf(u33932,axiom,
~ p(n4,n9,n6) ).
cnf(u33937,axiom,
~ p(n4,n8,n6) ).
cnf(u33942,axiom,
~ p(n4,n7,n6) ).
cnf(u33947,axiom,
~ p(n4,n6,n5) ).
cnf(u33951,axiom,
~ p(n4,n6,n4) ).
cnf(u33955,axiom,
~ p(n4,n6,n3) ).
cnf(u33959,axiom,
~ p(n4,n6,n2) ).
cnf(u33964,axiom,
~ p(n4,n3,n9) ).
cnf(u33969,axiom,
~ p(n4,n2,n9) ).
cnf(u33974,axiom,
~ p(n4,n1,n9) ).
cnf(u33979,axiom,
~ p(n3,n9,n5) ).
cnf(u33983,axiom,
~ p(n3,n9,n3) ).
cnf(u33988,axiom,
~ p(n3,n8,n5) ).
cnf(u33992,axiom,
~ p(n3,n8,n3) ).
cnf(u33997,axiom,
~ p(n3,n6,n8) ).
cnf(u34001,axiom,
~ p(n3,n6,n6) ).
cnf(u34006,axiom,
~ p(n3,n5,n8) ).
cnf(u34010,axiom,
~ p(n3,n5,n6) ).
cnf(u34015,axiom,
~ p(n3,n4,n8) ).
cnf(u34019,axiom,
~ p(n3,n4,n6) ).
cnf(u34024,axiom,
~ p(n3,n3,n7) ).
cnf(u34028,axiom,
~ p(n3,n3,n2) ).
cnf(u34032,axiom,
~ p(n3,n3,n1) ).
cnf(u34037,axiom,
~ p(n3,n1,n7) ).
cnf(u34041,axiom,
~ p(n3,n1,n2) ).
cnf(u34045,axiom,
~ p(n3,n1,n1) ).
cnf(u34050,axiom,
~ p(n2,n9,n5) ).
cnf(u34054,axiom,
~ p(n2,n9,n3) ).
cnf(u34059,axiom,
~ p(n2,n8,n5) ).
cnf(u34063,axiom,
~ p(n2,n8,n3) ).
cnf(u34068,axiom,
~ p(n2,n5,n8) ).
cnf(u34072,axiom,
~ p(n2,n5,n6) ).
cnf(u34077,axiom,
~ p(n2,n4,n8) ).
cnf(u34081,axiom,
~ p(n2,n4,n6) ).
cnf(u34086,axiom,
~ p(n2,n3,n7) ).
cnf(u34090,axiom,
~ p(n2,n3,n2) ).
cnf(u34094,axiom,
~ p(n2,n3,n1) ).
cnf(u34099,axiom,
~ p(n2,n2,n7) ).
cnf(u34103,axiom,
~ p(n2,n2,n2) ).
cnf(u34107,axiom,
~ p(n2,n2,n1) ).
cnf(u34112,axiom,
~ p(n2,n1,n7) ).
cnf(u34116,axiom,
~ p(n2,n1,n2) ).
cnf(u34120,axiom,
~ p(n2,n1,n1) ).
cnf(u34125,axiom,
~ p(n1,n9,n5) ).
cnf(u34129,axiom,
~ p(n1,n9,n3) ).
cnf(u34134,axiom,
~ p(n1,n8,n5) ).
cnf(u34138,axiom,
~ p(n1,n8,n3) ).
cnf(u34143,axiom,
~ p(n1,n7,n5) ).
cnf(u34147,axiom,
~ p(n1,n7,n3) ).
cnf(u34152,axiom,
~ p(n1,n6,n8) ).
cnf(u34156,axiom,
~ p(n1,n6,n6) ).
cnf(u34161,axiom,
~ p(n1,n5,n8) ).
cnf(u34165,axiom,
~ p(n1,n5,n6) ).
cnf(u34170,axiom,
~ p(n1,n2,n7) ).
cnf(u34174,axiom,
~ p(n1,n2,n2) ).
cnf(u34178,axiom,
~ p(n1,n2,n1) ).
cnf(u34198,axiom,
~ p(n7,n8,n2) ).
cnf(u34208,axiom,
~ p(n8,n7,n1) ).
cnf(u34215,axiom,
~ p(n2,n6,n6) ).
cnf(u34220,axiom,
~ p(n6,n6,n5) ).
cnf(u34225,axiom,
~ p(n6,n6,n4) ).
cnf(u34230,axiom,
~ p(n6,n6,n2) ).
cnf(u34240,axiom,
~ p(n6,n5,n3) ).
cnf(u34244,axiom,
~ p(n4,n5,n3) ).
cnf(u34249,axiom,
~ p(n6,n5,n2) ).
cnf(u34253,axiom,
~ p(n4,n5,n2) ).
cnf(u34260,axiom,
~ p(n1,n4,n8) ).
cnf(u34265,axiom,
~ p(n4,n4,n5) ).
cnf(u34270,axiom,
~ p(n4,n4,n4) ).
cnf(u34275,axiom,
~ p(n4,n4,n3) ).
cnf(u34287,axiom,
~ p(n1,n3,n2) ).
cnf(u34292,axiom,
~ p(n1,n3,n1) ).
cnf(u34299,axiom,
~ p(n3,n2,n7) ).
cnf(u34307,axiom,
~ p(n3,n2,n1) ).
cnf(u34313,axiom,
~ p(n1,n1,n7) ).
cnf(u34322,axiom,
~ p(n1,n1,n2) ).
cnf(u34354,axiom,
~ p(n6,n5,n4) ).
cnf(u34372,axiom,
~ p(n4,n5,n5) ).
cnf(u34383,axiom,
~ p(n3,n7,n5) ).
cnf(u34394,axiom,
~ p(n2,n7,n3) ).
cnf(u31287,axiom,
p(n2,n6,n8) ).
cnf(u31294,axiom,
p(n5,n8,n6) ).
cnf(u31297,axiom,
p(n7,n4,n7) ).
cnf(u31290,axiom,
p(n3,n7,n3) ).
cnf(u31289,axiom,
p(n3,n2,n2) ).
cnf(u31291,axiom,
p(n4,n4,n2) ).
cnf(u31292,axiom,
p(n4,n5,n4) ).
cnf(u31296,axiom,
p(n6,n6,n3) ).
cnf(u31284,axiom,
p(n1,n1,n1) ).
cnf(u31286,axiom,
p(n1,n4,n6) ).
cnf(u31288,axiom,
p(n2,n7,n5) ).
cnf(u31295,axiom,
p(n6,n5,n5) ).
cnf(u31300,axiom,
p(n8,n7,n2) ).
cnf(u31293,axiom,
p(n5,n1,n9) ).
cnf(u31298,axiom,
p(n7,n8,n1) ).
cnf(u31285,axiom,
p(n1,n3,n7) ).
cnf(u31299,axiom,
p(n8,n2,n3) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ069+2 : TPTP v9.3.1. Bugfixed v5.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n020.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 22:39:50 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 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.33/1.99 % (3837998)Detected formulas, will run a generic FOF schedule.
% 3.33/1.99 % (3838008)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2674374832:s2a=on:i=139:gtg=position_2997 on theBenchmark for (2997ds/139Mi)
% 3.33/1.99 % (3838008)Instruction limit reached!
% 3.33/1.99 % (3838008)------------------------------
% 3.33/1.99 % (3838008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.33/1.99 % (3838008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.33/1.99 % (3838008)CaDiCaL version: 2.1.3
% 3.33/1.99 % (3838008)Termination reason: Instruction limit
% 3.33/1.99 % (3838008)Termination phase: Unused predicate definition removal
% 3.33/1.99 % (3838008)Time elapsed: 0.034 s
% 3.33/1.99 % (3838008)Peak memory usage: 89 MB
% 3.33/1.99 % (3838008)Instructions burned: 140 (million)
% 3.33/1.99 % (3838009)dis-21_1_sil=8000:lcm=predicate:random_seed=188975315: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.33/1.99 % (3838003)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=2655643261:i=141193_2997 on theBenchmark for (2997ds/141193Mi)
% 3.33/1.99 % (3838006)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2577293905:i=109:sd=1:ins=1:gsp=on:ss=axioms_2997 on theBenchmark for (2997ds/109Mi)
% 3.33/1.99 % (3838007)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1381648689:i=119:av=off:ss=axioms_2997 on theBenchmark for (2997ds/119Mi)
% 3.33/1.99 % (3838004)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=3130410782:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2997 on theBenchmark for (2997ds/134677Mi)
% 3.33/1.99 % (3838005)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=4188220371:i=141695:sd=1:nm=32:gsp=on:ss=included_2997 on theBenchmark for (2997ds/141695Mi)
% 3.33/1.99 % (3838007)Refutation not found, incomplete strategy
% 3.33/1.99 % (3838007)------------------------------
% 3.33/1.99 % (3838007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.33/1.99 % (3838007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.33/1.99 % (3838007)CaDiCaL version: 2.1.3
% 3.33/1.99 % (3838007)Termination reason: Refutation not found, incomplete strategy
% 3.33/1.99 % (3838007)Time elapsed: 0.018 s
% 3.33/1.99 % (3838006)Refutation not found, incomplete strategy
% 3.33/1.99 % (3838006)------------------------------
% 3.33/1.99 % (3838006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.33/1.99 % (3838007)Peak memory usage: 90 MB
% 3.33/1.99 % (3838007)Instructions burned: 33 (million)
% 3.33/1.99 % (3838006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.33/1.99 % (3838006)CaDiCaL version: 2.1.3
% 3.33/1.99 % (3838006)Termination reason: Refutation not found, incomplete strategy
% 3.33/1.99 % (3838006)Time elapsed: 0.018 s
% 3.33/1.99 % (3838006)Peak memory usage: 91 MB
% 3.33/1.99 % (3838006)Instructions burned: 33 (million)
% 3.33/1.99 % (3838009)Instruction limit reached!
% 3.33/1.99 % (3838009)------------------------------
% 3.33/1.99 % (3838009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.33/1.99 % (3838009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.33/1.99 % (3838009)CaDiCaL version: 2.1.3
% 3.33/1.99 % (3838009)Termination reason: Instruction limit
% 3.33/1.99 % (3838009)Termination phase: Preprocessing 3
% 3.33/1.99 % (3838009)Time elapsed: 0.067 s
% 3.33/1.99 % (3838009)Peak memory usage: 91 MB
% 3.33/1.99 % (3838009)Instructions burned: 131 (million)
% 3.33/1.99 % (3838011)lrs+10_1_sil=8000:sp=occurrence:random_seed=1245364451:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 3.33/1.99 % (3838011)Refutation not found, incomplete strategy
% 3.33/1.99 % (3838011)------------------------------
% 3.33/1.99 % (3838011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.33/1.99 % (3838011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.33/1.99 % (3838011)CaDiCaL version: 2.1.3
% 3.33/1.99 % (3838011)Termination reason: Refutation not found, incomplete strategy
% 3.33/1.99 % (3838011)Time elapsed: 0.010 s
% 3.33/1.99 % (3838011)Peak memory usage: 91 MB
% 3.33/1.99 % (3838011)Instructions burned: 33 (million)
% 9.20/2.41 % (3838018)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1396004863:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 9.20/2.41 % (3838006)------------------------------
% 9.20/2.41 % (3838006)------------------------------
% 9.20/2.41 % (3838007)------------------------------
% 9.20/2.41 % (3838007)------------------------------
% 9.20/2.41 % (3838011)------------------------------
% 9.20/2.41 % (3838011)------------------------------
% 9.20/2.41 % (3838018)Refutation not found, incomplete strategy
% 9.20/2.41 % (3838018)------------------------------
% 9.20/2.41 % (3838018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.20/2.41 % (3838018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/2.41 % (3838018)CaDiCaL version: 2.1.3
% 9.20/2.41 % (3838018)Termination reason: Refutation not found, incomplete strategy
% 9.20/2.41 % (3838018)Time elapsed: 0.052 s
% 9.20/2.41 % (3838018)Peak memory usage: 91 MB
% 9.20/2.41 % (3838018)Instructions burned: 123 (million)
% 9.20/2.41 % (3838023)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=448989594:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 9.20/2.41 % (3838021)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1766190902:i=325:sd=1:ss=axioms:sgt=32_2993 on theBenchmark for (2993ds/325Mi)
% 9.20/2.41 % (3838022)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=2329485050:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 9.20/2.41 % (3838023)Refutation not found, incomplete strategy
% 9.20/2.41 % (3838023)------------------------------
% 9.20/2.41 % (3838023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.20/2.41 % (3838023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/2.41 % (3838023)CaDiCaL version: 2.1.3
% 9.20/2.41 % (3838023)Termination reason: Refutation not found, incomplete strategy
% 9.20/2.41 % (3838023)Time elapsed: 0.014 s
% 9.20/2.41 % (3838023)Peak memory usage: 91 MB
% 9.20/2.41 % (3838023)Instructions burned: 51 (million)
% 9.20/2.41 % (3838021)Refutation not found, incomplete strategy
% 9.20/2.41 % (3838021)------------------------------
% 9.20/2.41 % (3838021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.20/2.41 % (3838021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/2.41 % (3838021)CaDiCaL version: 2.1.3
% 9.20/2.41 % (3838021)Termination reason: Refutation not found, incomplete strategy
% 9.20/2.41 % (3838021)Time elapsed: 0.018 s
% 9.20/2.41 % (3838021)Peak memory usage: 91 MB
% 9.20/2.41 % (3838021)Instructions burned: 33 (million)
% 9.20/2.41 [W927 22:39:51.892065505 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.20/2.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.20/2.41 [W927 22:39:51.892102142 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.20/2.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.20/2.41 [W927 22:39:51.892140449 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.20/2.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.20/2.41 [W927 22:39:51.892153662 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.20/2.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.20/2.41 [W927 22:39:51.892181406 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.20/2.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.20/2.41 [W927 22:39:51.892193059 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.20/2.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.20/2.46 [W927 22:39:51.914834107 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.20/2.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.20/2.46 [W927 22:39:51.914869208 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.20/2.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.20/2.46 [W927 22:39:51.914907835 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.20/2.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.20/2.46 [W927 22:39:51.914920275 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.20/2.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.20/2.46 [W927 22:39:51.914947148 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.20/2.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.20/2.46 [W927 22:39:51.914958728 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.20/2.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.20/2.46 % (3838022)Instruction limit reached!
% 9.20/2.46 % (3838022)------------------------------
% 9.20/2.46 % (3838022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.20/2.46 % (3838022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/2.46 % (3838022)CaDiCaL version: 2.1.3
% 9.20/2.46 % (3838022)Termination reason: Instruction limit
% 9.20/2.46 % (3838022)Termination phase: Property scanning
% 9.20/2.46 % (3838022)Time elapsed: 0.113 s
% 9.20/2.46 % (3838022)Peak memory usage: 93 MB
% 9.20/2.46 % (3838022)Instructions burned: 251 (million)
% 9.20/2.46 % (3838018)------------------------------
% 9.20/2.46 % (3838018)------------------------------
% 9.20/2.46 % (3838023)------------------------------
% 9.20/2.46 % (3838023)------------------------------
% 9.20/2.46 % (3838021)------------------------------
% 9.20/2.46 % (3838021)------------------------------
% 9.20/2.46 % (3838027)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3921761193:i=2350_2990 on theBenchmark for (2990ds/2350Mi)
% 9.20/2.46 % (3838029)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=903645267:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 9.20/2.46 % (3838028)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2317496555:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 9.20/2.46 % (3838029)Instruction limit reached!
% 9.20/2.46 % (3838029)------------------------------
% 9.20/2.46 % (3838029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.20/2.46 % (3838029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/2.46 % (3838029)CaDiCaL version: 2.1.3
% 9.20/2.46 % (3838029)Termination reason: Instruction limit
% 9.20/2.46 % (3838029)Termination phase: Property scanning
% 9.20/2.46 % (3838029)Time elapsed: 0.034 s
% 9.20/2.46 % (3838029)Peak memory usage: 92 MB
% 9.20/2.46 % (3838029)Instructions burned: 133 (million)
% 9.20/2.46 % (3838028)Instruction limit reached!
% 9.20/2.46 % (3838028)------------------------------
% 9.20/2.46 % (3838028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.20/2.46 % (3838028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/2.46 % (3838028)CaDiCaL version: 2.1.3
% 9.20/2.46 % (3838028)Termination reason: Instruction limit
% 9.20/2.46 % (3838028)Termination phase: Preprocessing 3
% 9.20/2.46 % (3838028)Time elapsed: 0.066 s
% 9.20/2.46 % (3838028)Peak memory usage: 91 MB
% 9.20/2.46 % (3838028)Instructions burned: 114 (million)
% 9.20/2.46 % (3838031)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2466429120:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2989 on theBenchmark for (2989ds/114Mi)
% 9.20/2.46 % (3838034)lrs+10_1_sil=8000:sp=occurrence:random_seed=1514765742:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2988 on theBenchmark for (2988ds/907Mi)
% 9.20/2.46 % (3838034)Refutation not found, incomplete strategy
% 9.20/2.46 % (3838034)------------------------------
% 9.20/2.46 % (3838034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.20/2.46 % (3838034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/2.46 % (3838034)CaDiCaL version: 2.1.3
% 9.20/2.46 % (3838034)Termination reason: Refutation not found, incomplete strategy
% 9.20/2.46 % (3838034)Time elapsed: 0.013 s
% 9.20/2.46 % (3838034)Peak memory usage: 91 MB
% 9.20/2.46 % (3838034)Instructions burned: 51 (million)
% 9.20/2.46 % (3838031)Instruction limit reached!
% 9.20/2.46 % (3838031)------------------------------
% 9.20/2.46 % (3838031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.20/2.46 % (3838031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/2.46 % (3838031)CaDiCaL version: 2.1.3
% 9.20/2.46 % (3838031)Termination reason: Instruction limit
% 9.20/2.46 % (3838031)Termination phase: SInE selection
% 9.20/2.46 % (3838031)Time elapsed: 0.042 s
% 9.20/2.46 % (3838031)Peak memory usage: 89 MB
% 9.20/2.46 % (3838031)Instructions burned: 116 (million)
% 9.20/2.46 % (3838005)Refutation not found, incomplete strategy
% 9.20/2.46 % (3838005)------------------------------
% 9.20/2.46 % (3838005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.20/2.46 % (3838005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/2.46 % (3838005)CaDiCaL version: 2.1.3
% 9.20/2.46 % (3838005)Termination reason: Refutation not found, incomplete strategy
% 9.20/2.46 % (3838005)Time elapsed: 0.921 s
% 9.20/2.46 % (3838005)Peak memory usage: 160 MB
% 9.20/2.46 % (3838005)Instructions burned: 1501 (million)
% 9.20/2.46 % (3838035)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3050769437:i=437:sd=1:aac=none:ss=included_2988 on theBenchmark for (2988ds/437Mi)
% 9.20/2.46 % (3838003)First to succeed.
% 9.20/2.46 % (3838003)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3837998"
% 9.20/2.46 % (3838034)------------------------------
% 9.20/2.46 % (3838034)------------------------------
% 9.20/2.46 % (3838038)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=507753630:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi)
% 9.20/2.46 % (3838035)Refutation not found, incomplete strategy
% 9.20/2.46 % (3838035)------------------------------
% 9.20/2.46 % (3838035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.20/2.46 % (3838035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/2.46 % (3838035)CaDiCaL version: 2.1.3
% 9.20/2.46 % (3838035)Termination reason: Refutation not found, incomplete strategy
% 9.20/2.46 % (3838035)Time elapsed: 0.148 s
% 9.20/2.46 % (3838035)Peak memory usage: 98 MB
% 9.20/2.46 % (3838035)Instructions burned: 306 (million)
% 9.20/2.46 % (3838040)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3451674638:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 9.20/2.46 % (3838005)------------------------------
% 9.20/2.46 % (3838005)------------------------------
% 9.20/2.46 [W927 22:39:52.581113408 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.20/2.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.20/2.46 [W927 22:39:52.581147542 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.20/2.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.20/2.46 [W927 22:39:52.581184795 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.20/2.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.20/2.46 [W927 22:39:52.581196325 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.20/2.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.20/2.46 [W927 22:39:52.581222872 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.20/2.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.20/2.46 [W927 22:39:52.581244259 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.20/2.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.20/2.46 % (3838040)Instruction limit reached!
% 9.20/2.46 % (3838040)------------------------------
% 9.20/2.46 % (3838040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.20/2.46 % (3838040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/2.46 % (3838040)CaDiCaL version: 2.1.3
% 9.20/2.46 % (3838040)Termination reason: Instruction limit
% 9.20/2.46 % (3838040)Termination phase: NewCNF
% 9.20/2.46 % (3838040)Time elapsed: 0.043 s
% 9.20/2.46 % (3838040)Peak memory usage: 94 MB
% 9.20/2.46 % (3838040)Instructions burned: 135 (million)
% 9.20/2.46 % SZS status Satisfiable for theBenchmark
% 9.20/2.46 % SZS output start Saturation.
% See solution above
% 10.53/2.56 % SZS output start Definitions and Model Updates.
% 10.53/2.56 % SZS output end Definitions and Model Updates.
% 10.53/2.56 % (3838003)------------------------------
% 10.53/2.56 % (3838003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.53/2.56 % (3838003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.53/2.56 % (3838003)CaDiCaL version: 2.1.3
% 10.53/2.56 % (3838003)Termination reason: Satisfiable
% 10.53/2.56 % (3838003)Time elapsed: 0.957 s
% 10.53/2.56 % (3838003)Peak memory usage: 155 MB
% 10.53/2.56 % (3838003)Instructions burned: 1581 (million)
% 10.53/2.56 % (3838003)------------------------------
% 10.53/2.56 % (3838003)------------------------------
% 10.53/2.56 % (3837998)Success in time 1.606 s
% 10.53/2.56 % Vampire exiting
%------------------------------------------------------------------------------