%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PUZ068+2 : TPTP v9.3.1. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.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.38s 2.49s
% Output : Saturation 10.67s
% 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(u31349,axiom,
p(n9,n7,n8) ).
cnf(u31352,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(u31385,axiom,
~ p(n9,n7,n7) ).
cnf(u31390,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(u31435,axiom,
p(n8,n7,n6) ).
cnf(u31438,axiom,
~ p(n7,n9,n6) ).
cnf(u31442,axiom,
~ p(n7,n8,n6) ).
cnf(u31446,axiom,
~ p(n7,n7,n6) ).
cnf(u31451,axiom,
~ p(n9,n9,n5) ).
cnf(u31455,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(u31476,axiom,
p(n7,n9,n5) ).
cnf(u31479,axiom,
~ p(n7,n8,n5) ).
cnf(u31483,axiom,
~ p(n7,n7,n5) ).
cnf(u31488,axiom,
~ p(n9,n9,n2) ).
cnf(u31492,axiom,
~ p(n9,n8,n2) ).
cnf(u31496,axiom,
~ p(n9,n7,n2) ).
cnf(u31500,axiom,
~ p(n8,n9,n2) ).
cnf(u31504,axiom,
~ p(n8,n8,n2) ).
cnf(u31508,axiom,
~ p(n8,n7,n2) ).
cnf(u31512,axiom,
~ p(n7,n9,n2) ).
cnf(u31516,axiom,
~ p(n7,n8,n2) ).
cnf(u31521,axiom,
p(n7,n7,n2) ).
cnf(u31525,axiom,
~ p(n9,n9,n1) ).
cnf(u31530,axiom,
p(n9,n8,n1) ).
cnf(u31533,axiom,
~ p(n9,n7,n1) ).
cnf(u31537,axiom,
~ p(n8,n9,n1) ).
cnf(u31541,axiom,
~ p(n8,n8,n1) ).
cnf(u31545,axiom,
~ p(n8,n7,n1) ).
cnf(u31549,axiom,
~ p(n7,n9,n1) ).
cnf(u31553,axiom,
~ p(n7,n8,n1) ).
cnf(u31557,axiom,
~ p(n7,n7,n1) ).
cnf(u31562,axiom,
~ p(n9,n6,n9) ).
cnf(u31566,axiom,
~ p(n9,n5,n9) ).
cnf(u31571,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(u31590,axiom,
~ p(n7,n5,n9) ).
cnf(u31594,axiom,
~ p(n7,n4,n9) ).
cnf(u31599,axiom,
~ p(n9,n6,n8) ).
cnf(u31603,axiom,
~ p(n9,n5,n8) ).
cnf(u31607,axiom,
~ p(n9,n4,n8) ).
cnf(u31611,axiom,
~ p(n8,n6,n8) ).
cnf(u31616,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(u31652,axiom,
~ p(n8,n5,n6) ).
cnf(u31656,axiom,
~ p(n8,n4,n6) ).
cnf(u31660,axiom,
~ p(n7,n6,n6) ).
cnf(u31665,axiom,
p(n7,n5,n6) ).
cnf(u31668,axiom,
~ p(n7,n4,n6) ).
cnf(u31673,axiom,
~ p(n9,n6,n5) ).
cnf(u31678,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(u31693,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(u31723,axiom,
p(n8,n6,n4) ).
cnf(u31726,axiom,
~ p(n8,n5,n4) ).
cnf(u31730,axiom,
~ p(n8,n4,n4) ).
cnf(u31734,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(u31755,axiom,
~ p(n9,n4,n3) ).
cnf(u31759,axiom,
~ p(n8,n6,n3) ).
cnf(u31763,axiom,
~ p(n8,n5,n3) ).
cnf(u31768,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(u31833,axiom,
~ p(n8,n6,n1) ).
cnf(u31837,axiom,
~ p(n8,n5,n1) ).
cnf(u31841,axiom,
~ p(n8,n4,n1) ).
cnf(u31846,axiom,
p(n7,n6,n1) ).
cnf(u31849,axiom,
~ p(n7,n5,n1) ).
cnf(u31853,axiom,
~ p(n7,n4,n1) ).
cnf(u31858,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(u31891,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(u31920,axiom,
p(n7,n3,n8) ).
cnf(u31923,axiom,
~ p(n7,n2,n8) ).
cnf(u31927,axiom,
~ p(n7,n1,n8) ).
cnf(u31933,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(u31952,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(u31974,axiom,
p(n9,n2,n6) ).
cnf(u31977,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(u32019,axiom,
p(n8,n3,n5) ).
cnf(u32022,axiom,
~ p(n8,n2,n5) ).
cnf(u32026,axiom,
~ p(n8,n1,n5) ).
cnf(u32030,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(u32055,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(u32072,axiom,
p(n7,n2,n4) ).
cnf(u32075,axiom,
~ p(n7,n1,n4) ).
cnf(u32080,axiom,
~ p(n9,n3,n3) ).
cnf(u32084,axiom,
~ p(n9,n2,n3) ).
cnf(u32089,axiom,
p(n9,n1,n3) ).
cnf(u32092,axiom,
~ p(n8,n3,n3) ).
cnf(u32096,axiom,
~ p(n8,n2,n3) ).
cnf(u32100,axiom,
~ p(n8,n1,n3) ).
cnf(u32104,axiom,
~ p(n7,n3,n3) ).
cnf(u32108,axiom,
~ p(n7,n2,n3) ).
cnf(u32112,axiom,
~ p(n7,n1,n3) ).
cnf(u32117,axiom,
~ p(n9,n3,n2) ).
cnf(u32121,axiom,
~ p(n9,n2,n2) ).
cnf(u32125,axiom,
~ p(n9,n1,n2) ).
cnf(u32129,axiom,
~ p(n8,n3,n2) ).
cnf(u32134,axiom,
p(n8,n2,n2) ).
cnf(u32137,axiom,
~ p(n8,n1,n2) ).
cnf(u32141,axiom,
~ p(n7,n3,n2) ).
cnf(u32145,axiom,
~ p(n7,n2,n2) ).
cnf(u32149,axiom,
~ p(n7,n1,n2) ).
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(u32175,axiom,
p(n5,n7,n9) ).
cnf(u32178,axiom,
~ p(n4,n9,n9) ).
cnf(u32182,axiom,
~ p(n4,n8,n9) ).
cnf(u32186,axiom,
~ p(n4,n7,n9) ).
cnf(u32191,axiom,
~ p(n6,n9,n8) ).
cnf(u32195,axiom,
~ p(n6,n8,n8) ).
cnf(u32199,axiom,
~ p(n6,n7,n8) ).
cnf(u32203,axiom,
~ p(n5,n9,n8) ).
cnf(u32208,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,n6) ).
cnf(u32232,axiom,
~ p(n6,n8,n6) ).
cnf(u32236,axiom,
~ p(n6,n7,n6) ).
cnf(u32240,axiom,
~ p(n5,n9,n6) ).
cnf(u32244,axiom,
~ p(n5,n8,n6) ).
cnf(u32248,axiom,
~ p(n5,n7,n6) ).
cnf(u32252,axiom,
~ p(n4,n9,n6) ).
cnf(u32256,axiom,
~ p(n4,n8,n6) ).
cnf(u32260,axiom,
~ p(n4,n7,n6) ).
cnf(u32265,axiom,
~ p(n6,n9,n4) ).
cnf(u32269,axiom,
~ p(n6,n8,n4) ).
cnf(u32273,axiom,
~ p(n6,n7,n4) ).
cnf(u32277,axiom,
~ p(n5,n9,n4) ).
cnf(u32281,axiom,
~ p(n5,n8,n4) ).
cnf(u32285,axiom,
~ p(n5,n7,n4) ).
cnf(u32289,axiom,
~ p(n4,n9,n4) ).
cnf(u32294,axiom,
p(n4,n8,n4) ).
cnf(u32297,axiom,
~ p(n4,n7,n4) ).
cnf(u32302,axiom,
~ p(n6,n9,n3) ).
cnf(u32306,axiom,
~ p(n6,n8,n3) ).
cnf(u32311,axiom,
p(n6,n7,n3) ).
cnf(u32314,axiom,
~ p(n5,n9,n3) ).
cnf(u32318,axiom,
~ p(n5,n8,n3) ).
cnf(u32322,axiom,
~ p(n5,n7,n3) ).
cnf(u32326,axiom,
~ p(n4,n9,n3) ).
cnf(u32330,axiom,
~ p(n4,n8,n3) ).
cnf(u32334,axiom,
~ p(n4,n7,n3) ).
cnf(u32339,axiom,
~ p(n6,n9,n2) ).
cnf(u32343,axiom,
~ p(n6,n8,n2) ).
cnf(u32347,axiom,
~ p(n6,n7,n2) ).
cnf(u32351,axiom,
~ p(n5,n9,n2) ).
cnf(u32355,axiom,
~ p(n5,n8,n2) ).
cnf(u32359,axiom,
~ p(n5,n7,n2) ).
cnf(u32364,axiom,
p(n4,n9,n2) ).
cnf(u32367,axiom,
~ p(n4,n8,n2) ).
cnf(u32371,axiom,
~ p(n4,n7,n2) ).
cnf(u32376,axiom,
~ p(n6,n9,n1) ).
cnf(u32380,axiom,
~ p(n6,n8,n1) ).
cnf(u32384,axiom,
~ p(n6,n7,n1) ).
cnf(u32389,axiom,
p(n5,n9,n1) ).
cnf(u32392,axiom,
~ p(n5,n8,n1) ).
cnf(u32396,axiom,
~ p(n5,n7,n1) ).
cnf(u32400,axiom,
~ p(n4,n9,n1) ).
cnf(u32404,axiom,
~ p(n4,n8,n1) ).
cnf(u32408,axiom,
~ p(n4,n7,n1) ).
cnf(u32413,axiom,
~ p(n6,n6,n9) ).
cnf(u32417,axiom,
~ p(n6,n5,n9) ).
cnf(u32421,axiom,
~ p(n6,n4,n9) ).
cnf(u32425,axiom,
~ p(n5,n6,n9) ).
cnf(u32429,axiom,
~ p(n5,n5,n9) ).
cnf(u32433,axiom,
~ p(n5,n4,n9) ).
cnf(u32438,axiom,
p(n4,n6,n9) ).
cnf(u32441,axiom,
~ p(n4,n5,n9) ).
cnf(u32445,axiom,
~ p(n4,n4,n9) ).
cnf(u32450,axiom,
~ p(n6,n6,n8) ).
cnf(u32454,axiom,
~ p(n6,n5,n8) ).
cnf(u32459,axiom,
p(n6,n4,n8) ).
cnf(u32462,axiom,
~ p(n5,n6,n8) ).
cnf(u32466,axiom,
~ p(n5,n5,n8) ).
cnf(u32470,axiom,
~ p(n5,n4,n8) ).
cnf(u32474,axiom,
~ p(n4,n6,n8) ).
cnf(u32478,axiom,
~ p(n4,n5,n8) ).
cnf(u32482,axiom,
~ p(n4,n4,n8) ).
cnf(u32488,axiom,
p(n6,n6,n7) ).
cnf(u32491,axiom,
~ p(n6,n5,n7) ).
cnf(u32495,axiom,
~ p(n6,n4,n7) ).
cnf(u32499,axiom,
~ p(n5,n6,n7) ).
cnf(u32503,axiom,
~ p(n5,n5,n7) ).
cnf(u32507,axiom,
~ p(n5,n4,n7) ).
cnf(u32511,axiom,
~ p(n4,n6,n7) ).
cnf(u32515,axiom,
~ p(n4,n5,n7) ).
cnf(u32519,axiom,
~ p(n4,n4,n7) ).
cnf(u32524,axiom,
~ p(n6,n6,n6) ).
cnf(u32528,axiom,
~ p(n6,n5,n6) ).
cnf(u32532,axiom,
~ p(n6,n4,n6) ).
cnf(u32536,axiom,
~ p(n5,n6,n6) ).
cnf(u32540,axiom,
~ p(n5,n5,n6) ).
cnf(u32545,axiom,
p(n5,n4,n6) ).
cnf(u32548,axiom,
~ p(n4,n6,n6) ).
cnf(u32552,axiom,
~ p(n4,n5,n6) ).
cnf(u32556,axiom,
~ p(n4,n4,n6) ).
cnf(u32561,axiom,
~ p(n6,n6,n5) ).
cnf(u32565,axiom,
~ p(n6,n5,n5) ).
cnf(u32569,axiom,
~ p(n6,n4,n5) ).
cnf(u32573,axiom,
~ p(n5,n6,n5) ).
cnf(u32577,axiom,
~ p(n5,n5,n5) ).
cnf(u32581,axiom,
~ p(n5,n4,n5) ).
cnf(u32585,axiom,
~ p(n4,n6,n5) ).
cnf(u32589,axiom,
~ p(n4,n5,n5) ).
cnf(u32594,axiom,
p(n4,n4,n5) ).
cnf(u32598,axiom,
~ p(n6,n6,n4) ).
cnf(u32603,axiom,
p(n6,n5,n4) ).
cnf(u32606,axiom,
~ p(n6,n4,n4) ).
cnf(u32610,axiom,
~ p(n5,n6,n4) ).
cnf(u32614,axiom,
~ p(n5,n5,n4) ).
cnf(u32618,axiom,
~ p(n5,n4,n4) ).
cnf(u32622,axiom,
~ p(n4,n6,n4) ).
cnf(u32626,axiom,
~ p(n4,n5,n4) ).
cnf(u32630,axiom,
~ p(n4,n4,n4) ).
cnf(u32635,axiom,
~ p(n6,n6,n2) ).
cnf(u32639,axiom,
~ p(n6,n5,n2) ).
cnf(u32643,axiom,
~ p(n6,n4,n2) ).
cnf(u32647,axiom,
~ p(n5,n6,n2) ).
cnf(u32652,axiom,
p(n5,n5,n2) ).
cnf(u32655,axiom,
~ p(n5,n4,n2) ).
cnf(u32659,axiom,
~ p(n4,n6,n2) ).
cnf(u32663,axiom,
~ p(n4,n5,n2) ).
cnf(u32667,axiom,
~ p(n4,n4,n2) ).
cnf(u32673,axiom,
p(n6,n3,n9) ).
cnf(u32676,axiom,
~ p(n6,n2,n9) ).
cnf(u32680,axiom,
~ p(n6,n1,n9) ).
cnf(u32684,axiom,
~ p(n5,n3,n9) ).
cnf(u32688,axiom,
~ p(n5,n2,n9) ).
cnf(u32692,axiom,
~ p(n5,n1,n9) ).
cnf(u32696,axiom,
~ p(n4,n3,n9) ).
cnf(u32700,axiom,
~ p(n4,n2,n9) ).
cnf(u32704,axiom,
~ p(n4,n1,n9) ).
cnf(u32709,axiom,
~ p(n6,n3,n8) ).
cnf(u32713,axiom,
~ p(n6,n2,n8) ).
cnf(u32717,axiom,
~ p(n6,n1,n8) ).
cnf(u32721,axiom,
~ p(n5,n3,n8) ).
cnf(u32725,axiom,
~ p(n5,n2,n8) ).
cnf(u32729,axiom,
~ p(n5,n1,n8) ).
cnf(u32733,axiom,
~ p(n4,n3,n8) ).
cnf(u32738,axiom,
p(n4,n2,n8) ).
cnf(u32741,axiom,
~ p(n4,n1,n8) ).
cnf(u32746,axiom,
~ p(n6,n3,n7) ).
cnf(u32750,axiom,
~ p(n6,n2,n7) ).
cnf(u32754,axiom,
~ p(n6,n1,n7) ).
cnf(u32758,axiom,
~ p(n5,n3,n7) ).
cnf(u32763,axiom,
p(n5,n2,n7) ).
cnf(u32766,axiom,
~ p(n5,n1,n7) ).
cnf(u32770,axiom,
~ p(n4,n3,n7) ).
cnf(u32774,axiom,
~ p(n4,n2,n7) ).
cnf(u32778,axiom,
~ p(n4,n1,n7) ).
cnf(u32783,axiom,
~ p(n6,n3,n5) ).
cnf(u32787,axiom,
~ p(n6,n2,n5) ).
cnf(u32791,axiom,
~ p(n6,n1,n5) ).
cnf(u32795,axiom,
~ p(n5,n3,n5) ).
cnf(u32799,axiom,
~ p(n5,n2,n5) ).
cnf(u32804,axiom,
p(n5,n1,n5) ).
cnf(u32807,axiom,
~ p(n4,n3,n5) ).
cnf(u32811,axiom,
~ p(n4,n2,n5) ).
cnf(u32815,axiom,
~ p(n4,n1,n5) ).
cnf(u32820,axiom,
~ p(n6,n3,n3) ).
cnf(u32824,axiom,
~ p(n6,n2,n3) ).
cnf(u32828,axiom,
~ p(n6,n1,n3) ).
cnf(u32832,axiom,
~ p(n5,n3,n3) ).
cnf(u32836,axiom,
~ p(n5,n2,n3) ).
cnf(u32840,axiom,
~ p(n5,n1,n3) ).
cnf(u32845,axiom,
p(n4,n3,n3) ).
cnf(u32848,axiom,
~ p(n4,n2,n3) ).
cnf(u32852,axiom,
~ p(n4,n1,n3) ).
cnf(u32857,axiom,
~ p(n6,n3,n2) ).
cnf(u32861,axiom,
~ p(n6,n2,n2) ).
cnf(u32866,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(u32899,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(u32918,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(u32944,axiom,
p(n2,n9,n9) ).
cnf(u32947,axiom,
~ p(n2,n8,n9) ).
cnf(u32951,axiom,
~ p(n2,n7,n9) ).
cnf(u32955,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,n7) ).
cnf(u32973,axiom,
p(n3,n8,n7) ).
cnf(u32976,axiom,
~ p(n3,n7,n7) ).
cnf(u32980,axiom,
~ p(n2,n9,n7) ).
cnf(u32984,axiom,
~ p(n2,n8,n7) ).
cnf(u32988,axiom,
~ p(n2,n7,n7) ).
cnf(u32992,axiom,
~ p(n1,n9,n7) ).
cnf(u32996,axiom,
~ p(n1,n8,n7) ).
cnf(u33000,axiom,
~ p(n1,n7,n7) ).
cnf(u33005,axiom,
~ p(n3,n9,n6) ).
cnf(u33009,axiom,
~ p(n3,n8,n6) ).
cnf(u33013,axiom,
~ p(n3,n7,n6) ).
cnf(u33017,axiom,
~ p(n2,n9,n6) ).
cnf(u33022,axiom,
p(n2,n8,n6) ).
cnf(u33025,axiom,
~ p(n2,n7,n6) ).
cnf(u33029,axiom,
~ p(n1,n9,n6) ).
cnf(u33033,axiom,
~ p(n1,n8,n6) ).
cnf(u33037,axiom,
~ p(n1,n7,n6) ).
cnf(u33042,axiom,
~ p(n3,n9,n5) ).
cnf(u33046,axiom,
~ p(n3,n8,n5) ).
cnf(u33051,axiom,
p(n3,n7,n5) ).
cnf(u33054,axiom,
~ p(n2,n9,n5) ).
cnf(u33058,axiom,
~ p(n2,n8,n5) ).
cnf(u33062,axiom,
~ p(n2,n7,n5) ).
cnf(u33066,axiom,
~ p(n1,n9,n5) ).
cnf(u33070,axiom,
~ p(n1,n8,n5) ).
cnf(u33074,axiom,
~ p(n1,n7,n5) ).
cnf(u33079,axiom,
~ p(n3,n9,n4) ).
cnf(u33083,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(u33100,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,n3) ).
cnf(u33120,axiom,
~ p(n3,n8,n3) ).
cnf(u33124,axiom,
~ p(n3,n7,n3) ).
cnf(u33128,axiom,
~ p(n2,n9,n3) ).
cnf(u33132,axiom,
~ p(n2,n8,n3) ).
cnf(u33136,axiom,
~ p(n2,n7,n3) ).
cnf(u33141,axiom,
p(n1,n9,n3) ).
cnf(u33144,axiom,
~ p(n1,n8,n3) ).
cnf(u33148,axiom,
~ p(n1,n7,n3) ).
cnf(u33153,axiom,
~ p(n3,n9,n2) ).
cnf(u33157,axiom,
~ p(n3,n8,n2) ).
cnf(u33161,axiom,
~ p(n3,n7,n2) ).
cnf(u33165,axiom,
~ p(n2,n9,n2) ).
cnf(u33169,axiom,
~ p(n2,n8,n2) ).
cnf(u33173,axiom,
~ p(n2,n7,n2) ).
cnf(u33177,axiom,
~ p(n1,n9,n2) ).
cnf(u33182,axiom,
p(n1,n8,n2) ).
cnf(u33185,axiom,
~ p(n1,n7,n2) ).
cnf(u33190,axiom,
~ p(n3,n6,n9) ).
cnf(u33195,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,n8) ).
cnf(u33231,axiom,
~ p(n3,n5,n8) ).
cnf(u33235,axiom,
~ p(n3,n4,n8) ).
cnf(u33240,axiom,
p(n2,n6,n8) ).
cnf(u33243,axiom,
~ p(n2,n5,n8) ).
cnf(u33247,axiom,
~ p(n2,n4,n8) ).
cnf(u33251,axiom,
~ p(n1,n6,n8) ).
cnf(u33255,axiom,
~ p(n1,n5,n8) ).
cnf(u33259,axiom,
~ p(n1,n4,n8) ).
cnf(u33265,axiom,
p(n3,n6,n6) ).
cnf(u33268,axiom,
~ p(n3,n5,n6) ).
cnf(u33272,axiom,
~ p(n3,n4,n6) ).
cnf(u33276,axiom,
~ p(n2,n6,n6) ).
cnf(u33280,axiom,
~ p(n2,n5,n6) ).
cnf(u33284,axiom,
~ p(n2,n4,n6) ).
cnf(u33288,axiom,
~ p(n1,n6,n6) ).
cnf(u33292,axiom,
~ p(n1,n5,n6) ).
cnf(u33296,axiom,
~ p(n1,n4,n6) ).
cnf(u33301,axiom,
~ p(n3,n6,n5) ).
cnf(u33305,axiom,
~ p(n3,n5,n5) ).
cnf(u33309,axiom,
~ p(n3,n4,n5) ).
cnf(u33313,axiom,
~ p(n2,n6,n5) ).
cnf(u33317,axiom,
~ p(n2,n5,n5) ).
cnf(u33321,axiom,
~ p(n2,n4,n5) ).
cnf(u33326,axiom,
p(n1,n6,n5) ).
cnf(u33329,axiom,
~ p(n1,n5,n5) ).
cnf(u33333,axiom,
~ p(n1,n4,n5) ).
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(u33355,axiom,
p(n2,n5,n3) ).
cnf(u33358,axiom,
~ p(n2,n4,n3) ).
cnf(u33362,axiom,
~ p(n1,n6,n3) ).
cnf(u33366,axiom,
~ p(n1,n5,n3) ).
cnf(u33370,axiom,
~ p(n1,n4,n3) ).
cnf(u33375,axiom,
~ p(n3,n6,n1) ).
cnf(u33379,axiom,
~ p(n3,n5,n1) ).
cnf(u33384,axiom,
p(n3,n4,n1) ).
cnf(u33387,axiom,
~ p(n2,n6,n1) ).
cnf(u33391,axiom,
~ p(n2,n5,n1) ).
cnf(u33395,axiom,
~ p(n2,n4,n1) ).
cnf(u33399,axiom,
~ p(n1,n6,n1) ).
cnf(u33403,axiom,
~ p(n1,n5,n1) ).
cnf(u33407,axiom,
~ p(n1,n4,n1) ).
cnf(u33412,axiom,
~ p(n3,n3,n9) ).
cnf(u33416,axiom,
~ p(n3,n2,n9) ).
cnf(u33420,axiom,
~ p(n3,n1,n9) ).
cnf(u33424,axiom,
~ p(n2,n3,n9) ).
cnf(u33428,axiom,
~ p(n2,n2,n9) ).
cnf(u33432,axiom,
~ p(n2,n1,n9) ).
cnf(u33436,axiom,
~ p(n1,n3,n9) ).
cnf(u33441,axiom,
p(n1,n2,n9) ).
cnf(u33444,axiom,
~ p(n1,n1,n9) ).
cnf(u33449,axiom,
~ p(n3,n3,n8) ).
cnf(u33453,axiom,
~ p(n3,n2,n8) ).
cnf(u33457,axiom,
~ p(n3,n1,n8) ).
cnf(u33461,axiom,
~ p(n2,n3,n8) ).
cnf(u33465,axiom,
~ p(n2,n2,n8) ).
cnf(u33469,axiom,
~ p(n2,n1,n8) ).
cnf(u33473,axiom,
~ p(n1,n3,n8) ).
cnf(u33477,axiom,
~ p(n1,n2,n8) ).
cnf(u33482,axiom,
p(n1,n1,n8) ).
cnf(u33486,axiom,
~ p(n3,n3,n7) ).
cnf(u33490,axiom,
~ p(n3,n2,n7) ).
cnf(u33494,axiom,
~ p(n3,n1,n7) ).
cnf(u33498,axiom,
~ p(n2,n3,n7) ).
cnf(u33502,axiom,
~ p(n2,n2,n7) ).
cnf(u33507,axiom,
p(n2,n1,n7) ).
cnf(u33510,axiom,
~ p(n1,n3,n7) ).
cnf(u33514,axiom,
~ p(n1,n2,n7) ).
cnf(u33518,axiom,
~ p(n1,n1,n7) ).
cnf(u33523,axiom,
~ p(n3,n3,n6) ).
cnf(u33527,axiom,
~ p(n3,n2,n6) ).
cnf(u33531,axiom,
~ p(n3,n1,n6) ).
cnf(u33535,axiom,
~ p(n2,n3,n6) ).
cnf(u33539,axiom,
~ p(n2,n2,n6) ).
cnf(u33543,axiom,
~ p(n2,n1,n6) ).
cnf(u33548,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,n4) ).
cnf(u33564,axiom,
~ p(n3,n2,n4) ).
cnf(u33569,axiom,
p(n3,n1,n4) ).
cnf(u33572,axiom,
~ p(n2,n3,n4) ).
cnf(u33576,axiom,
~ p(n2,n2,n4) ).
cnf(u33580,axiom,
~ p(n2,n1,n4) ).
cnf(u33584,axiom,
~ p(n1,n3,n4) ).
cnf(u33588,axiom,
~ p(n1,n2,n4) ).
cnf(u33592,axiom,
~ p(n1,n1,n4) ).
cnf(u33598,axiom,
p(n3,n3,n2) ).
cnf(u33601,axiom,
~ p(n3,n2,n2) ).
cnf(u33605,axiom,
~ p(n3,n1,n2) ).
cnf(u33609,axiom,
~ p(n2,n3,n2) ).
cnf(u33613,axiom,
~ p(n2,n2,n2) ).
cnf(u33617,axiom,
~ p(n2,n1,n2) ).
cnf(u33621,axiom,
~ p(n1,n3,n2) ).
cnf(u33625,axiom,
~ p(n1,n2,n2) ).
cnf(u33629,axiom,
~ p(n1,n1,n2) ).
cnf(u33634,axiom,
~ p(n3,n3,n1) ).
cnf(u33638,axiom,
~ p(n3,n2,n1) ).
cnf(u33642,axiom,
~ p(n3,n1,n1) ).
cnf(u33647,axiom,
p(n2,n3,n1) ).
cnf(u33650,axiom,
~ p(n2,n2,n1) ).
cnf(u33654,axiom,
~ p(n2,n1,n1) ).
cnf(u33658,axiom,
~ p(n1,n3,n1) ).
cnf(u33662,axiom,
~ p(n1,n2,n1) ).
cnf(u33666,axiom,
~ p(n1,n1,n1) ).
cnf(u33671,axiom,
~ p(n9,n8,n4) ).
cnf(u33675,axiom,
~ p(n9,n8,n3) ).
cnf(u33680,axiom,
~ p(n9,n7,n4) ).
cnf(u33684,axiom,
~ p(n9,n7,n3) ).
cnf(u33689,axiom,
~ p(n9,n6,n7) ).
cnf(u33694,axiom,
~ p(n9,n5,n7) ).
cnf(u33699,axiom,
~ p(n9,n4,n7) ).
cnf(u33704,axiom,
~ p(n9,n3,n1) ).
cnf(u33709,axiom,
~ p(n9,n2,n1) ).
cnf(u33714,axiom,
~ p(n9,n1,n1) ).
cnf(u33719,axiom,
~ p(n8,n9,n4) ).
cnf(u33723,axiom,
~ p(n8,n9,n3) ).
cnf(u33728,axiom,
~ p(n8,n8,n4) ).
cnf(u33732,axiom,
~ p(n8,n8,n3) ).
cnf(u33737,axiom,
~ p(n8,n7,n4) ).
cnf(u33741,axiom,
~ p(n8,n7,n3) ).
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,n1) ).
cnf(u33766,axiom,
~ p(n8,n2,n1) ).
cnf(u33771,axiom,
~ p(n7,n9,n4) ).
cnf(u33775,axiom,
~ p(n7,n9,n3) ).
cnf(u33780,axiom,
~ p(n7,n7,n4) ).
cnf(u33784,axiom,
~ p(n7,n7,n3) ).
cnf(u33789,axiom,
~ p(n7,n6,n7) ).
cnf(u33794,axiom,
~ p(n7,n5,n7) ).
cnf(u33799,axiom,
~ p(n7,n3,n1) ).
cnf(u33804,axiom,
~ p(n7,n2,n1) ).
cnf(u33809,axiom,
~ p(n7,n1,n1) ).
cnf(u33814,axiom,
~ p(n6,n9,n7) ).
cnf(u33818,axiom,
~ p(n6,n9,n5) ).
cnf(u33823,axiom,
~ p(n6,n7,n7) ).
cnf(u33827,axiom,
~ p(n6,n7,n5) ).
cnf(u33832,axiom,
~ p(n6,n6,n3) ).
cnf(u33836,axiom,
~ p(n6,n6,n1) ).
cnf(u33841,axiom,
~ p(n6,n5,n3) ).
cnf(u33845,axiom,
~ p(n6,n5,n1) ).
cnf(u33850,axiom,
~ p(n6,n4,n3) ).
cnf(u33854,axiom,
~ p(n6,n4,n1) ).
cnf(u33859,axiom,
~ p(n6,n3,n6) ).
cnf(u33863,axiom,
~ p(n6,n3,n4) ).
cnf(u33868,axiom,
~ p(n6,n2,n6) ).
cnf(u33872,axiom,
~ p(n6,n2,n4) ).
cnf(u33877,axiom,
~ p(n6,n1,n6) ).
cnf(u33881,axiom,
~ p(n6,n1,n4) ).
cnf(u33886,axiom,
~ p(n5,n9,n7) ).
cnf(u33890,axiom,
~ p(n5,n9,n5) ).
cnf(u33895,axiom,
~ p(n5,n8,n7) ).
cnf(u33899,axiom,
~ p(n5,n8,n5) ).
cnf(u33904,axiom,
~ p(n5,n7,n7) ).
cnf(u33908,axiom,
~ p(n5,n7,n5) ).
cnf(u33913,axiom,
~ p(n5,n5,n3) ).
cnf(u33917,axiom,
~ p(n5,n5,n1) ).
cnf(u33922,axiom,
~ p(n5,n4,n3) ).
cnf(u33926,axiom,
~ p(n5,n4,n1) ).
cnf(u33931,axiom,
~ p(n5,n2,n6) ).
cnf(u33935,axiom,
~ p(n5,n2,n4) ).
cnf(u33940,axiom,
~ p(n5,n1,n6) ).
cnf(u33944,axiom,
~ p(n5,n1,n4) ).
cnf(u33949,axiom,
~ p(n4,n9,n7) ).
cnf(u33953,axiom,
~ p(n4,n9,n5) ).
cnf(u33958,axiom,
~ p(n4,n8,n7) ).
cnf(u33962,axiom,
~ p(n4,n8,n5) ).
cnf(u33967,axiom,
~ p(n4,n6,n3) ).
cnf(u33971,axiom,
~ p(n4,n6,n1) ).
cnf(u33976,axiom,
~ p(n4,n4,n3) ).
cnf(u33980,axiom,
~ p(n4,n4,n1) ).
cnf(u33985,axiom,
~ p(n4,n3,n6) ).
cnf(u33989,axiom,
~ p(n4,n3,n4) ).
cnf(u33994,axiom,
~ p(n4,n2,n6) ).
cnf(u33998,axiom,
~ p(n4,n2,n4) ).
cnf(u34003,axiom,
~ p(n3,n8,n8) ).
cnf(u34007,axiom,
~ p(n3,n8,n1) ).
cnf(u34012,axiom,
~ p(n3,n7,n8) ).
cnf(u34016,axiom,
~ p(n3,n7,n1) ).
cnf(u34021,axiom,
~ p(n3,n6,n7) ).
cnf(u34025,axiom,
~ p(n3,n6,n4) ).
cnf(u34029,axiom,
~ p(n3,n6,n2) ).
cnf(u34034,axiom,
~ p(n3,n5,n7) ).
cnf(u34038,axiom,
~ p(n3,n5,n4) ).
cnf(u34042,axiom,
~ p(n3,n5,n2) ).
cnf(u34047,axiom,
~ p(n3,n4,n7) ).
cnf(u34051,axiom,
~ p(n3,n4,n4) ).
cnf(u34055,axiom,
~ p(n3,n4,n2) ).
cnf(u34060,axiom,
~ p(n3,n3,n5) ).
cnf(u34064,axiom,
~ p(n3,n3,n3) ).
cnf(u34069,axiom,
~ p(n3,n1,n5) ).
cnf(u34073,axiom,
~ p(n3,n1,n3) ).
cnf(u34078,axiom,
~ p(n2,n9,n8) ).
cnf(u34082,axiom,
~ p(n2,n9,n1) ).
cnf(u34087,axiom,
~ p(n2,n8,n8) ).
cnf(u34091,axiom,
~ p(n2,n8,n1) ).
cnf(u34096,axiom,
~ p(n2,n7,n8) ).
cnf(u34100,axiom,
~ p(n2,n7,n1) ).
cnf(u34105,axiom,
~ p(n2,n6,n7) ).
cnf(u34109,axiom,
~ p(n2,n6,n4) ).
cnf(u34113,axiom,
~ p(n2,n6,n2) ).
cnf(u34118,axiom,
~ p(n2,n5,n7) ).
cnf(u34122,axiom,
~ p(n2,n5,n4) ).
cnf(u34126,axiom,
~ p(n2,n5,n2) ).
cnf(u34131,axiom,
~ p(n2,n3,n5) ).
cnf(u34135,axiom,
~ p(n2,n3,n3) ).
cnf(u34140,axiom,
~ p(n2,n1,n5) ).
cnf(u34144,axiom,
~ p(n2,n1,n3) ).
cnf(u34149,axiom,
~ p(n1,n9,n8) ).
cnf(u34153,axiom,
~ p(n1,n9,n1) ).
cnf(u34158,axiom,
~ p(n1,n8,n8) ).
cnf(u34162,axiom,
~ p(n1,n8,n1) ).
cnf(u34167,axiom,
~ p(n1,n6,n7) ).
cnf(u34171,axiom,
~ p(n1,n6,n4) ).
cnf(u34175,axiom,
~ p(n1,n6,n2) ).
cnf(u34180,axiom,
~ p(n1,n3,n5) ).
cnf(u34184,axiom,
~ p(n1,n3,n3) ).
cnf(u34189,axiom,
~ p(n1,n2,n5) ).
cnf(u34193,axiom,
~ p(n1,n2,n3) ).
cnf(u34198,axiom,
~ p(n1,n1,n5) ).
cnf(u34202,axiom,
~ p(n1,n1,n3) ).
cnf(u34211,axiom,
~ p(n9,n9,n3) ).
cnf(u34217,axiom,
~ p(n3,n9,n1) ).
cnf(u34224,axiom,
~ p(n6,n8,n7) ).
cnf(u34230,axiom,
~ p(n7,n8,n4) ).
cnf(u34238,axiom,
~ p(n1,n7,n8) ).
cnf(u34244,axiom,
~ p(n4,n7,n5) ).
cnf(u34259,axiom,
~ p(n5,n6,n1) ).
cnf(u34268,axiom,
~ p(n1,n5,n4) ).
cnf(u34273,axiom,
~ p(n4,n5,n3) ).
cnf(u34278,axiom,
~ p(n1,n5,n2) ).
cnf(u34292,axiom,
~ p(n5,n3,n6) ).
cnf(u34312,axiom,
~ p(n4,n1,n4) ).
cnf(u34366,axiom,
~ p(n3,n2,n5) ).
cnf(u34376,axiom,
~ p(n2,n4,n7) ).
cnf(u34382,axiom,
~ p(n2,n4,n4) ).
cnf(u34387,axiom,
~ p(n2,n2,n3) ).
cnf(u34398,axiom,
~ p(n1,n4,n2) ).
cnf(u35666,axiom,
~ p(n1,n4,n7) ).
cnf(u31287,axiom,
p(n2,n2,n5) ).
cnf(u31297,axiom,
p(n7,n4,n7) ).
cnf(u31290,axiom,
p(n3,n9,n8) ).
cnf(u31299,axiom,
p(n8,n1,n1) ).
cnf(u31291,axiom,
p(n4,n1,n6) ).
cnf(u31292,axiom,
p(n4,n5,n1) ).
cnf(u31294,axiom,
p(n5,n3,n4) ).
cnf(u31296,axiom,
p(n6,n8,n5) ).
cnf(u31284,axiom,
p(n1,n4,n4) ).
cnf(u31286,axiom,
p(n1,n7,n1) ).
cnf(u31288,axiom,
p(n2,n4,n2) ).
cnf(u31295,axiom,
p(n5,n6,n3) ).
cnf(u31300,axiom,
p(n9,n9,n4) ).
cnf(u31293,axiom,
p(n4,n7,n7) ).
cnf(u31298,axiom,
p(n7,n8,n3) ).
cnf(u31285,axiom,
p(n1,n5,n7) ).
cnf(u31289,axiom,
p(n3,n2,n3) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ068+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.11/0.39 % Computer : n016.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 22:43:48 UTC 2026
% 0.11/0.40 % CPUTime :
% 0.11/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.43 Running first-order theorem proving
% 0.11/0.43 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
% 7.91/2.18 % (3061479)Detected formulas, will run a generic FOF schedule.
% 7.91/2.18 % (3061485)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=3479093629:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2997 on theBenchmark for (2997ds/134677Mi)
% 7.91/2.18 % (3061484)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=471007021:i=141193_2997 on theBenchmark for (2997ds/141193Mi)
% 7.91/2.18 % (3061489)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=395610943:s2a=on:i=139:gtg=position_2997 on theBenchmark for (2997ds/139Mi)
% 7.91/2.18 % (3061488)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3228183027:i=119:av=off:ss=axioms_2997 on theBenchmark for (2997ds/119Mi)
% 7.91/2.18 % (3061486)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=3035796900:i=141695:sd=1:nm=32:gsp=on:ss=included_2997 on theBenchmark for (2997ds/141695Mi)
% 7.91/2.18 % (3061487)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=531519402:i=109:sd=1:ins=1:gsp=on:ss=axioms_2997 on theBenchmark for (2997ds/109Mi)
% 7.91/2.18 % (3061490)dis-21_1_sil=8000:lcm=predicate:random_seed=698823227: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)
% 7.91/2.18 % (3061488)Refutation not found, incomplete strategy
% 7.91/2.18 % (3061488)------------------------------
% 7.91/2.18 % (3061488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.91/2.18 % (3061488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.91/2.18 % (3061488)CaDiCaL version: 2.1.3
% 7.91/2.18 % (3061487)Refutation not found, incomplete strategy
% 7.91/2.18 % (3061487)------------------------------
% 7.91/2.18 % (3061487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.91/2.18 % (3061488)Termination reason: Refutation not found, incomplete strategy
% 7.91/2.18 % (3061488)Time elapsed: 0.018 s
% 7.91/2.18 % (3061488)Peak memory usage: 90 MB
% 7.91/2.18 % (3061487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.91/2.18 % (3061488)Instructions burned: 33 (million)
% 7.91/2.18 % (3061487)CaDiCaL version: 2.1.3
% 7.91/2.18 % (3061487)Termination reason: Refutation not found, incomplete strategy
% 7.91/2.18 % (3061487)Time elapsed: 0.018 s
% 7.91/2.18 % (3061487)Peak memory usage: 90 MB
% 7.91/2.18 % (3061487)Instructions burned: 33 (million)
% 7.91/2.18 % (3061489)Instruction limit reached!
% 7.91/2.18 % (3061489)------------------------------
% 7.91/2.18 % (3061489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.91/2.18 % (3061489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.91/2.18 % (3061489)CaDiCaL version: 2.1.3
% 7.91/2.18 % (3061489)Termination reason: Instruction limit
% 7.91/2.18 % (3061489)Termination phase: Unused predicate definition removal
% 7.91/2.18 % (3061489)Time elapsed: 0.061 s
% 7.91/2.18 % (3061489)Peak memory usage: 89 MB
% 7.91/2.18 % (3061489)Instructions burned: 139 (million)
% 7.91/2.18 % (3061490)Instruction limit reached!
% 7.91/2.18 % (3061490)------------------------------
% 7.91/2.18 % (3061490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.91/2.18 % (3061490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.91/2.18 % (3061490)CaDiCaL version: 2.1.3
% 7.91/2.18 % (3061490)Termination reason: Instruction limit
% 7.91/2.18 % (3061490)Termination phase: Preprocessing 3
% 7.91/2.18 % (3061490)Time elapsed: 0.066 s
% 7.91/2.18 % (3061490)Peak memory usage: 91 MB
% 7.91/2.18 % (3061490)Instructions burned: 130 (million)
% 7.91/2.18 % (3061498)lrs+10_1_sil=8000:sp=occurrence:random_seed=4196904757:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 7.91/2.18 % (3061498)Refutation not found, incomplete strategy
% 7.91/2.18 % (3061498)------------------------------
% 7.91/2.18 % (3061498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.91/2.18 % (3061498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.91/2.18 % (3061498)CaDiCaL version: 2.1.3
% 7.91/2.18 % (3061498)Termination reason: Refutation not found, incomplete strategy
% 7.91/2.18 % (3061498)Time elapsed: 0.018 s
% 7.91/2.18 % (3061498)Peak memory usage: 91 MB
% 7.91/2.18 % (3061498)Instructions burned: 33 (million)
% 9.38/2.48 % (3061499)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3128292752:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 9.38/2.48 % (3061488)------------------------------
% 9.38/2.48 % (3061488)------------------------------
% 9.38/2.48 % (3061487)------------------------------
% 9.38/2.48 % (3061487)------------------------------
% 9.38/2.48 % (3061499)Refutation not found, incomplete strategy
% 9.38/2.48 % (3061499)------------------------------
% 9.38/2.48 % (3061499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.38/2.48 % (3061499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.38/2.48 % (3061499)CaDiCaL version: 2.1.3
% 9.38/2.48 % (3061499)Termination reason: Refutation not found, incomplete strategy
% 9.38/2.48 % (3061499)Time elapsed: 0.052 s
% 9.38/2.48 % (3061499)Peak memory usage: 91 MB
% 9.38/2.48 % (3061499)Instructions burned: 123 (million)
% 9.38/2.48 % (3061502)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2709823314:i=325:sd=1:ss=axioms:sgt=32_2993 on theBenchmark for (2993ds/325Mi)
% 9.38/2.48 % (3061503)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=604522394:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 9.38/2.48 % (3061502)Refutation not found, incomplete strategy
% 9.38/2.48 % (3061502)------------------------------
% 9.38/2.48 % (3061502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.38/2.48 % (3061502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.38/2.48 % (3061502)CaDiCaL version: 2.1.3
% 9.38/2.48 % (3061502)Termination reason: Refutation not found, incomplete strategy
% 9.38/2.48 % (3061502)Time elapsed: 0.018 s
% 9.38/2.48 % (3061502)Peak memory usage: 90 MB
% 9.38/2.48 % (3061502)Instructions burned: 33 (million)
% 9.38/2.48 % (3061498)------------------------------
% 9.38/2.48 % (3061498)------------------------------
% 9.38/2.48 [W927 22:43:49.186009795 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.38/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.38/2.48 [W927 22:43:49.186052355 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.38/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.38/2.48 [W927 22:43:49.186091075 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.38/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.38/2.48 [W927 22:43:49.186102435 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.38/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.38/2.48 [W927 22:43:49.186127981 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.38/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.38/2.48 [W927 22:43:49.186149095 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.38/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.38/2.48 [W927 22:43:49.210346500 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.38/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.38/2.48 [W927 22:43:49.210447760 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.38/2.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.38/2.49 [W927 22:43:49.210493443 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.38/2.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.38/2.49 [W927 22:43:49.210504503 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.38/2.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.38/2.49 [W927 22:43:49.210538440 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.38/2.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.38/2.49 [W927 22:43:49.210549483 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.38/2.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.38/2.49 % (3061499)------------------------------
% 9.38/2.49 % (3061499)------------------------------
% 9.38/2.49 % (3061503)Instruction limit reached!
% 9.38/2.49 % (3061503)------------------------------
% 9.38/2.49 % (3061503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.38/2.49 % (3061503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.38/2.49 % (3061503)CaDiCaL version: 2.1.3
% 9.38/2.49 % (3061503)Termination reason: Instruction limit
% 9.38/2.49 % (3061503)Termination phase: Property scanning
% 9.38/2.49 % (3061503)Time elapsed: 0.112 s
% 9.38/2.49 % (3061503)Peak memory usage: 92 MB
% 9.38/2.49 % (3061503)Instructions burned: 249 (million)
% 9.38/2.49 % (3061506)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1732655690:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2991 on theBenchmark for (2991ds/294Mi)
% 9.38/2.49 % (3061506)Refutation not found, incomplete strategy
% 9.38/2.49 % (3061506)------------------------------
% 9.38/2.49 % (3061506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.38/2.49 % (3061506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.38/2.49 % (3061506)CaDiCaL version: 2.1.3
% 9.38/2.49 % (3061506)Termination reason: Refutation not found, incomplete strategy
% 9.38/2.49 % (3061506)Time elapsed: 0.027 s
% 9.38/2.49 % (3061506)Peak memory usage: 91 MB
% 9.38/2.49 % (3061506)Instructions burned: 51 (million)
% 9.38/2.49 % (3061502)------------------------------
% 9.38/2.49 % (3061502)------------------------------
% 9.38/2.49 % (3061507)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3367565039:i=2350_2990 on theBenchmark for (2990ds/2350Mi)
% 9.38/2.49 % (3061508)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3129457787:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 9.38/2.49 % (3061508)Instruction limit reached!
% 9.38/2.49 % (3061508)------------------------------
% 9.38/2.49 % (3061508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.38/2.49 % (3061508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.38/2.49 % (3061508)CaDiCaL version: 2.1.3
% 9.38/2.49 % (3061508)Termination reason: Instruction limit
% 9.38/2.49 % (3061508)Termination phase: Preprocessing 3
% 9.38/2.49 % (3061508)Time elapsed: 0.061 s
% 9.38/2.49 % (3061508)Peak memory usage: 90 MB
% 9.38/2.49 % (3061508)Instructions burned: 114 (million)
% 9.38/2.49 % (3061512)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3152414537:i=127:av=off:fsr=off:sup=off_2988 on theBenchmark for (2988ds/127Mi)
% 9.38/2.49 % (3061486)Refutation not found, incomplete strategy
% 9.38/2.49 % (3061486)------------------------------
% 9.38/2.49 % (3061486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.38/2.49 % (3061486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.38/2.49 % (3061486)CaDiCaL version: 2.1.3
% 9.38/2.49 % (3061486)Termination reason: Refutation not found, incomplete strategy
% 9.38/2.49 % (3061486)Time elapsed: 0.917 s
% 9.38/2.49 % (3061486)Peak memory usage: 160 MB
% 9.38/2.49 % (3061486)Instructions burned: 1500 (million)
% 9.38/2.49 % (3061506)------------------------------
% 9.38/2.49 % (3061506)------------------------------
% 9.38/2.49 % (3061512)Instruction limit reached!
% 9.38/2.49 % (3061512)------------------------------
% 9.38/2.49 % (3061512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.38/2.49 % (3061512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.38/2.49 % (3061512)CaDiCaL version: 2.1.3
% 9.38/2.49 % (3061512)Termination reason: Instruction limit
% 9.38/2.49 % (3061512)Termination phase: Property scanning
% 9.38/2.49 % (3061512)Time elapsed: 0.058 s
% 9.38/2.49 % (3061512)Peak memory usage: 92 MB
% 9.38/2.49 % (3061512)Instructions burned: 129 (million)
% 9.38/2.49 % (3061513)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=37926944:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2988 on theBenchmark for (2988ds/114Mi)
% 9.38/2.49 % (3061484)First to succeed.
% 9.38/2.49 % (3061484)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3061479"
% 9.38/2.49 % (3061513)Instruction limit reached!
% 9.38/2.49 % (3061513)------------------------------
% 9.38/2.49 % (3061513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.38/2.49 % (3061513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.38/2.49 % (3061513)CaDiCaL version: 2.1.3
% 9.38/2.49 % (3061513)Termination reason: Instruction limit
% 9.38/2.49 % (3061513)Termination phase: SInE selection
% 9.38/2.49 % (3061513)Time elapsed: 0.043 s
% 9.38/2.49 % (3061513)Peak memory usage: 89 MB
% 9.38/2.49 % (3061513)Instructions burned: 116 (million)
% 9.38/2.49 % (3061516)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4130440576:i=437:sd=1:aac=none:ss=included_2986 on theBenchmark for (2986ds/437Mi)
% 9.38/2.49 % (3061515)lrs+10_1_sil=8000:sp=occurrence:random_seed=3826589688:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2986 on theBenchmark for (2986ds/907Mi)
% 9.38/2.49 % (3061515)Refutation not found, incomplete strategy
% 9.38/2.49 % (3061515)------------------------------
% 9.38/2.49 % (3061515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.38/2.49 % (3061515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.38/2.49 % (3061515)CaDiCaL version: 2.1.3
% 9.38/2.49 % (3061515)Termination reason: Refutation not found, incomplete strategy
% 9.38/2.49 % (3061515)Time elapsed: 0.025 s
% 9.38/2.49 % (3061515)Peak memory usage: 91 MB
% 9.38/2.49 % (3061515)Instructions burned: 51 (million)
% 9.38/2.49 % (3061518)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2013993491:i=5202:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/5202Mi)
% 9.38/2.49 % (3061486)------------------------------
% 9.38/2.49 % (3061486)------------------------------
% 9.38/2.49 [W927 22:43:50.912805723 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.38/2.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.38/2.49 [W927 22:43:50.912839573 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.38/2.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.38/2.49 [W927 22:43:50.912876546 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.38/2.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.38/2.49 [W927 22:43:50.912887633 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.38/2.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.38/2.49 [W927 22:43:50.912912936 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.38/2.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.38/2.49 [W927 22:43:50.912924693 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.38/2.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.38/2.49 % SZS status Satisfiable for theBenchmark
% 9.38/2.49 % SZS output start Saturation.
% See solution above
% 10.67/2.69 % SZS output start Definitions and Model Updates.
% 10.67/2.69 % SZS output end Definitions and Model Updates.
% 10.67/2.69 % (3061484)------------------------------
% 10.67/2.69 % (3061484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.67/2.69 % (3061484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.69 % (3061484)CaDiCaL version: 2.1.3
% 10.67/2.69 % (3061484)Termination reason: Satisfiable
% 10.67/2.69 % (3061484)Time elapsed: 0.955 s
% 10.67/2.69 % (3061484)Peak memory usage: 162 MB
% 10.67/2.69 % (3061484)Instructions burned: 1583 (million)
% 10.67/2.69 % (3061484)------------------------------
% 10.67/2.69 % (3061484)------------------------------
% 10.67/2.69 % (3061479)Success in time 1.611 s
% 10.67/2.69 % Vampire exiting
%------------------------------------------------------------------------------