%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PUZ080+2 : TPTP v9.3.1. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:32:14 PM UTC 2026
% Result : Satisfiable 0.77s 0.83s
% Output : Saturation 0.77s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u41871,axiom,
p(n7,n7,n9) ).
cnf(u41875,axiom,
p(n7,n8,n9) ).
cnf(u41879,axiom,
p(n7,n9,n9) ).
cnf(u41884,axiom,
~ p(n8,n7,n9) ).
cnf(u41887,axiom,
p(n8,n8,n9) ).
cnf(u41891,axiom,
p(n8,n9,n9) ).
cnf(u41895,axiom,
p(n9,n7,n9) ).
cnf(u41899,axiom,
p(n9,n8,n9) ).
cnf(u41903,axiom,
p(n9,n9,n9) ).
cnf(u41908,axiom,
p(n7,n7,n8) ).
cnf(u41912,axiom,
p(n7,n8,n8) ).
cnf(u41917,axiom,
~ p(n7,n9,n8) ).
cnf(u41920,axiom,
p(n8,n7,n8) ).
cnf(u41924,axiom,
p(n8,n8,n8) ).
cnf(u41928,axiom,
p(n8,n9,n8) ).
cnf(u41932,axiom,
p(n9,n7,n8) ).
cnf(u41936,axiom,
p(n9,n8,n8) ).
cnf(u41940,axiom,
p(n9,n9,n8) ).
cnf(u41945,axiom,
p(n7,n7,n7) ).
cnf(u41949,axiom,
p(n7,n8,n7) ).
cnf(u41953,axiom,
p(n7,n9,n7) ).
cnf(u41957,axiom,
p(n8,n7,n7) ).
cnf(u41961,axiom,
p(n8,n8,n7) ).
cnf(u41966,axiom,
~ p(n8,n9,n7) ).
cnf(u41969,axiom,
p(n9,n7,n7) ).
cnf(u41973,axiom,
p(n9,n8,n7) ).
cnf(u41977,axiom,
p(n9,n9,n7) ).
cnf(u41982,axiom,
p(n7,n7,n6) ).
cnf(u41986,axiom,
p(n7,n8,n6) ).
cnf(u41990,axiom,
p(n7,n9,n6) ).
cnf(u41994,axiom,
p(n8,n7,n6) ).
cnf(u41998,axiom,
p(n8,n8,n6) ).
cnf(u42002,axiom,
p(n8,n9,n6) ).
cnf(u42006,axiom,
p(n9,n7,n6) ).
cnf(u42010,axiom,
p(n9,n8,n6) ).
cnf(u42015,axiom,
~ p(n9,n9,n6) ).
cnf(u42019,axiom,
p(n7,n7,n5) ).
cnf(u42023,axiom,
p(n7,n8,n5) ).
cnf(u42027,axiom,
p(n7,n9,n5) ).
cnf(u42031,axiom,
p(n8,n7,n5) ).
cnf(u42035,axiom,
p(n8,n8,n5) ).
cnf(u42039,axiom,
p(n8,n9,n5) ).
cnf(u42043,axiom,
p(n9,n7,n5) ).
cnf(u42048,axiom,
~ p(n9,n8,n5) ).
cnf(u42051,axiom,
p(n9,n9,n5) ).
cnf(u42056,axiom,
p(n7,n7,n4) ).
cnf(u42061,axiom,
~ p(n7,n8,n4) ).
cnf(u42064,axiom,
p(n7,n9,n4) ).
cnf(u42068,axiom,
p(n8,n7,n4) ).
cnf(u42072,axiom,
p(n8,n8,n4) ).
cnf(u42076,axiom,
p(n8,n9,n4) ).
cnf(u42080,axiom,
p(n9,n7,n4) ).
cnf(u42084,axiom,
p(n9,n8,n4) ).
cnf(u42088,axiom,
p(n9,n9,n4) ).
cnf(u42093,axiom,
p(n7,n7,n3) ).
cnf(u42097,axiom,
p(n7,n8,n3) ).
cnf(u42101,axiom,
p(n7,n9,n3) ).
cnf(u42105,axiom,
p(n8,n7,n3) ).
cnf(u42109,axiom,
p(n8,n8,n3) ).
cnf(u42113,axiom,
p(n8,n9,n3) ).
cnf(u42118,axiom,
~ p(n9,n7,n3) ).
cnf(u42121,axiom,
p(n9,n8,n3) ).
cnf(u42125,axiom,
p(n9,n9,n3) ).
cnf(u42130,axiom,
p(n7,n7,n2) ).
cnf(u42134,axiom,
p(n7,n8,n2) ).
cnf(u42138,axiom,
p(n7,n9,n2) ).
cnf(u42142,axiom,
p(n8,n7,n2) ).
cnf(u42147,axiom,
~ p(n8,n8,n2) ).
cnf(u42150,axiom,
p(n8,n9,n2) ).
cnf(u42154,axiom,
p(n9,n7,n2) ).
cnf(u42158,axiom,
p(n9,n8,n2) ).
cnf(u42162,axiom,
p(n9,n9,n2) ).
cnf(u42168,axiom,
~ p(n7,n7,n1) ).
cnf(u42171,axiom,
p(n7,n8,n1) ).
cnf(u42175,axiom,
p(n7,n9,n1) ).
cnf(u42179,axiom,
p(n8,n7,n1) ).
cnf(u42183,axiom,
p(n8,n8,n1) ).
cnf(u42187,axiom,
p(n8,n9,n1) ).
cnf(u42191,axiom,
p(n9,n7,n1) ).
cnf(u42195,axiom,
p(n9,n8,n1) ).
cnf(u42199,axiom,
p(n9,n9,n1) ).
cnf(u42204,axiom,
p(n7,n4,n9) ).
cnf(u42208,axiom,
p(n7,n5,n9) ).
cnf(u42212,axiom,
p(n7,n6,n9) ).
cnf(u42216,axiom,
p(n8,n4,n9) ).
cnf(u42220,axiom,
p(n8,n5,n9) ).
cnf(u42224,axiom,
p(n8,n6,n9) ).
cnf(u42228,axiom,
p(n9,n4,n9) ).
cnf(u42232,axiom,
p(n9,n5,n9) ).
cnf(u42237,axiom,
~ p(n9,n6,n9) ).
cnf(u42241,axiom,
p(n7,n4,n8) ).
cnf(u42245,axiom,
p(n7,n5,n8) ).
cnf(u42249,axiom,
p(n7,n6,n8) ).
cnf(u42253,axiom,
p(n8,n4,n8) ).
cnf(u42257,axiom,
p(n8,n5,n8) ).
cnf(u42262,axiom,
~ p(n8,n6,n8) ).
cnf(u42265,axiom,
p(n9,n4,n8) ).
cnf(u42269,axiom,
p(n9,n5,n8) ).
cnf(u42273,axiom,
p(n9,n6,n8) ).
cnf(u42279,axiom,
~ p(n7,n4,n7) ).
cnf(u42282,axiom,
p(n7,n5,n7) ).
cnf(u42286,axiom,
p(n7,n6,n7) ).
cnf(u42290,axiom,
p(n8,n4,n7) ).
cnf(u42294,axiom,
p(n8,n5,n7) ).
cnf(u42298,axiom,
p(n8,n6,n7) ).
cnf(u42302,axiom,
p(n9,n4,n7) ).
cnf(u42306,axiom,
p(n9,n5,n7) ).
cnf(u42310,axiom,
p(n9,n6,n7) ).
cnf(u42315,axiom,
p(n7,n4,n6) ).
cnf(u42319,axiom,
p(n7,n5,n6) ).
cnf(u42323,axiom,
p(n7,n6,n6) ).
cnf(u42327,axiom,
p(n8,n4,n6) ).
cnf(u42332,axiom,
~ p(n8,n5,n6) ).
cnf(u42335,axiom,
p(n8,n6,n6) ).
cnf(u42339,axiom,
p(n9,n4,n6) ).
cnf(u42343,axiom,
p(n9,n5,n6) ).
cnf(u42347,axiom,
p(n9,n6,n6) ).
cnf(u42352,axiom,
p(n7,n4,n5) ).
cnf(u42356,axiom,
p(n7,n5,n5) ).
cnf(u42360,axiom,
p(n7,n6,n5) ).
cnf(u42365,axiom,
~ p(n8,n4,n5) ).
cnf(u42368,axiom,
p(n8,n5,n5) ).
cnf(u42372,axiom,
p(n8,n6,n5) ).
cnf(u42376,axiom,
p(n9,n4,n5) ).
cnf(u42380,axiom,
p(n9,n5,n5) ).
cnf(u42384,axiom,
p(n9,n6,n5) ).
cnf(u42389,axiom,
p(n7,n4,n4) ).
cnf(u42393,axiom,
p(n7,n5,n4) ).
cnf(u42397,axiom,
p(n7,n6,n4) ).
cnf(u42401,axiom,
p(n8,n4,n4) ).
cnf(u42405,axiom,
p(n8,n5,n4) ).
cnf(u42409,axiom,
p(n8,n6,n4) ).
cnf(u42413,axiom,
p(n9,n4,n4) ).
cnf(u42418,axiom,
~ p(n9,n5,n4) ).
cnf(u42421,axiom,
p(n9,n6,n4) ).
cnf(u42426,axiom,
p(n7,n4,n3) ).
cnf(u42431,axiom,
~ p(n7,n5,n3) ).
cnf(u42434,axiom,
p(n7,n6,n3) ).
cnf(u42438,axiom,
p(n8,n4,n3) ).
cnf(u42442,axiom,
p(n8,n5,n3) ).
cnf(u42446,axiom,
p(n8,n6,n3) ).
cnf(u42450,axiom,
p(n9,n4,n3) ).
cnf(u42454,axiom,
p(n9,n5,n3) ).
cnf(u42458,axiom,
p(n9,n6,n3) ).
cnf(u42463,axiom,
p(n7,n4,n2) ).
cnf(u42467,axiom,
p(n7,n5,n2) ).
cnf(u42472,axiom,
~ p(n7,n6,n2) ).
cnf(u42475,axiom,
p(n8,n4,n2) ).
cnf(u42479,axiom,
p(n8,n5,n2) ).
cnf(u42483,axiom,
p(n8,n6,n2) ).
cnf(u42487,axiom,
p(n9,n4,n2) ).
cnf(u42491,axiom,
p(n9,n5,n2) ).
cnf(u42495,axiom,
p(n9,n6,n2) ).
cnf(u42500,axiom,
p(n7,n4,n1) ).
cnf(u42504,axiom,
p(n7,n5,n1) ).
cnf(u42508,axiom,
p(n7,n6,n1) ).
cnf(u42512,axiom,
p(n8,n4,n1) ).
cnf(u42516,axiom,
p(n8,n5,n1) ).
cnf(u42520,axiom,
p(n8,n6,n1) ).
cnf(u42525,axiom,
~ p(n9,n4,n1) ).
cnf(u42528,axiom,
p(n9,n5,n1) ).
cnf(u42532,axiom,
p(n9,n6,n1) ).
cnf(u42537,axiom,
p(n7,n1,n9) ).
cnf(u42542,axiom,
~ p(n7,n2,n9) ).
cnf(u42545,axiom,
p(n7,n3,n9) ).
cnf(u42549,axiom,
p(n8,n1,n9) ).
cnf(u42553,axiom,
p(n8,n2,n9) ).
cnf(u42557,axiom,
p(n8,n3,n9) ).
cnf(u42561,axiom,
p(n9,n1,n9) ).
cnf(u42565,axiom,
p(n9,n2,n9) ).
cnf(u42569,axiom,
p(n9,n3,n9) ).
cnf(u42574,axiom,
p(n7,n1,n8) ).
cnf(u42578,axiom,
p(n7,n2,n8) ).
cnf(u42582,axiom,
p(n7,n3,n8) ).
cnf(u42586,axiom,
p(n8,n1,n8) ).
cnf(u42590,axiom,
p(n8,n2,n8) ).
cnf(u42594,axiom,
p(n8,n3,n8) ).
cnf(u42598,axiom,
p(n9,n1,n8) ).
cnf(u42602,axiom,
p(n9,n2,n8) ).
cnf(u42607,axiom,
~ p(n9,n3,n8) ).
cnf(u42611,axiom,
p(n7,n1,n7) ).
cnf(u42615,axiom,
p(n7,n2,n7) ).
cnf(u42619,axiom,
p(n7,n3,n7) ).
cnf(u42623,axiom,
p(n8,n1,n7) ).
cnf(u42627,axiom,
p(n8,n2,n7) ).
cnf(u42631,axiom,
p(n8,n3,n7) ).
cnf(u42636,axiom,
~ p(n9,n1,n7) ).
cnf(u42639,axiom,
p(n9,n2,n7) ).
cnf(u42643,axiom,
p(n9,n3,n7) ).
cnf(u42648,axiom,
p(n7,n1,n6) ).
cnf(u42652,axiom,
p(n7,n2,n6) ).
cnf(u42657,axiom,
~ p(n7,n3,n6) ).
cnf(u42660,axiom,
p(n8,n1,n6) ).
cnf(u42664,axiom,
p(n8,n2,n6) ).
cnf(u42668,axiom,
p(n8,n3,n6) ).
cnf(u42672,axiom,
p(n9,n1,n6) ).
cnf(u42676,axiom,
p(n9,n2,n6) ).
cnf(u42680,axiom,
p(n9,n3,n6) ).
cnf(u42686,axiom,
~ p(n7,n1,n5) ).
cnf(u42689,axiom,
p(n7,n2,n5) ).
cnf(u42693,axiom,
p(n7,n3,n5) ).
cnf(u42697,axiom,
p(n8,n1,n5) ).
cnf(u42701,axiom,
p(n8,n2,n5) ).
cnf(u42705,axiom,
p(n8,n3,n5) ).
cnf(u42709,axiom,
p(n9,n1,n5) ).
cnf(u42713,axiom,
p(n9,n2,n5) ).
cnf(u42717,axiom,
p(n9,n3,n5) ).
cnf(u42722,axiom,
p(n7,n1,n4) ).
cnf(u42726,axiom,
p(n7,n2,n4) ).
cnf(u42730,axiom,
p(n7,n3,n4) ).
cnf(u42734,axiom,
p(n8,n1,n4) ).
cnf(u42739,axiom,
~ p(n8,n2,n4) ).
cnf(u42742,axiom,
p(n8,n3,n4) ).
cnf(u42746,axiom,
p(n9,n1,n4) ).
cnf(u42750,axiom,
p(n9,n2,n4) ).
cnf(u42754,axiom,
p(n9,n3,n4) ).
cnf(u42759,axiom,
p(n7,n1,n3) ).
cnf(u42763,axiom,
p(n7,n2,n3) ).
cnf(u42767,axiom,
p(n7,n3,n3) ).
cnf(u42772,axiom,
~ p(n8,n1,n3) ).
cnf(u42775,axiom,
p(n8,n2,n3) ).
cnf(u42779,axiom,
p(n8,n3,n3) ).
cnf(u42783,axiom,
p(n9,n1,n3) ).
cnf(u42787,axiom,
p(n9,n2,n3) ).
cnf(u42791,axiom,
p(n9,n3,n3) ).
cnf(u42796,axiom,
p(n7,n1,n2) ).
cnf(u42800,axiom,
p(n7,n2,n2) ).
cnf(u42804,axiom,
p(n7,n3,n2) ).
cnf(u42808,axiom,
p(n8,n1,n2) ).
cnf(u42812,axiom,
p(n8,n2,n2) ).
cnf(u42816,axiom,
p(n8,n3,n2) ).
cnf(u42820,axiom,
p(n9,n1,n2) ).
cnf(u42825,axiom,
~ p(n9,n2,n2) ).
cnf(u42828,axiom,
p(n9,n3,n2) ).
cnf(u42833,axiom,
p(n7,n1,n1) ).
cnf(u42837,axiom,
p(n7,n2,n1) ).
cnf(u42841,axiom,
p(n7,n3,n1) ).
cnf(u42845,axiom,
p(n8,n1,n1) ).
cnf(u42849,axiom,
p(n8,n2,n1) ).
cnf(u42854,axiom,
~ p(n8,n3,n1) ).
cnf(u42857,axiom,
p(n9,n1,n1) ).
cnf(u42861,axiom,
p(n9,n2,n1) ).
cnf(u42865,axiom,
p(n9,n3,n1) ).
cnf(u42870,axiom,
p(n4,n7,n9) ).
cnf(u42874,axiom,
p(n4,n8,n9) ).
cnf(u42878,axiom,
p(n4,n9,n9) ).
cnf(u42882,axiom,
p(n5,n7,n9) ).
cnf(u42887,axiom,
~ p(n5,n8,n9) ).
cnf(u42890,axiom,
p(n5,n9,n9) ).
cnf(u42894,axiom,
p(n6,n7,n9) ).
cnf(u42898,axiom,
p(n6,n8,n9) ).
cnf(u42902,axiom,
p(n6,n9,n9) ).
cnf(u42907,axiom,
p(n4,n7,n8) ).
cnf(u42911,axiom,
p(n4,n8,n8) ).
cnf(u42915,axiom,
p(n4,n9,n8) ).
cnf(u42919,axiom,
p(n5,n7,n8) ).
cnf(u42923,axiom,
p(n5,n8,n8) ).
cnf(u42927,axiom,
p(n5,n9,n8) ).
cnf(u42931,axiom,
p(n6,n7,n8) ).
cnf(u42936,axiom,
~ p(n6,n8,n8) ).
cnf(u42939,axiom,
p(n6,n9,n8) ).
cnf(u42945,axiom,
~ p(n4,n7,n7) ).
cnf(u42948,axiom,
p(n4,n8,n7) ).
cnf(u42952,axiom,
p(n4,n9,n7) ).
cnf(u42956,axiom,
p(n5,n7,n7) ).
cnf(u42960,axiom,
p(n5,n8,n7) ).
cnf(u42964,axiom,
p(n5,n9,n7) ).
cnf(u42968,axiom,
p(n6,n7,n7) ).
cnf(u42972,axiom,
p(n6,n8,n7) ).
cnf(u42976,axiom,
p(n6,n9,n7) ).
cnf(u42981,axiom,
p(n4,n7,n6) ).
cnf(u42985,axiom,
p(n4,n8,n6) ).
cnf(u42989,axiom,
p(n4,n9,n6) ).
cnf(u42994,axiom,
~ p(n5,n7,n6) ).
cnf(u42997,axiom,
p(n5,n8,n6) ).
cnf(u43001,axiom,
p(n5,n9,n6) ).
cnf(u43005,axiom,
p(n6,n7,n6) ).
cnf(u43009,axiom,
p(n6,n8,n6) ).
cnf(u43013,axiom,
p(n6,n9,n6) ).
cnf(u43018,axiom,
p(n4,n7,n5) ).
cnf(u43022,axiom,
p(n4,n8,n5) ).
cnf(u43026,axiom,
p(n4,n9,n5) ).
cnf(u43030,axiom,
p(n5,n7,n5) ).
cnf(u43034,axiom,
p(n5,n8,n5) ).
cnf(u43038,axiom,
p(n5,n9,n5) ).
cnf(u43042,axiom,
p(n6,n7,n5) ).
cnf(u43046,axiom,
p(n6,n8,n5) ).
cnf(u43051,axiom,
~ p(n6,n9,n5) ).
cnf(u43055,axiom,
p(n4,n7,n4) ).
cnf(u43059,axiom,
p(n4,n8,n4) ).
cnf(u43063,axiom,
p(n4,n9,n4) ).
cnf(u43067,axiom,
p(n5,n7,n4) ).
cnf(u43071,axiom,
p(n5,n8,n4) ).
cnf(u43075,axiom,
p(n5,n9,n4) ).
cnf(u43080,axiom,
~ p(n6,n7,n4) ).
cnf(u43083,axiom,
p(n6,n8,n4) ).
cnf(u43087,axiom,
p(n6,n9,n4) ).
cnf(u43092,axiom,
p(n4,n7,n3) ).
cnf(u43096,axiom,
p(n4,n8,n3) ).
cnf(u43100,axiom,
p(n4,n9,n3) ).
cnf(u43104,axiom,
p(n5,n7,n3) ).
cnf(u43108,axiom,
p(n5,n8,n3) ).
cnf(u43113,axiom,
~ p(n5,n9,n3) ).
cnf(u43116,axiom,
p(n6,n7,n3) ).
cnf(u43120,axiom,
p(n6,n8,n3) ).
cnf(u43124,axiom,
p(n6,n9,n3) ).
cnf(u43129,axiom,
p(n4,n7,n2) ).
cnf(u43133,axiom,
p(n4,n8,n2) ).
cnf(u43138,axiom,
~ p(n4,n9,n2) ).
cnf(u43141,axiom,
p(n5,n7,n2) ).
cnf(u43145,axiom,
p(n5,n8,n2) ).
cnf(u43149,axiom,
p(n5,n9,n2) ).
cnf(u43153,axiom,
p(n6,n7,n2) ).
cnf(u43157,axiom,
p(n6,n8,n2) ).
cnf(u43161,axiom,
p(n6,n9,n2) ).
cnf(u43166,axiom,
p(n4,n7,n1) ).
cnf(u43171,axiom,
~ p(n4,n8,n1) ).
cnf(u43174,axiom,
p(n4,n9,n1) ).
cnf(u43178,axiom,
p(n5,n7,n1) ).
cnf(u43182,axiom,
p(n5,n8,n1) ).
cnf(u43186,axiom,
p(n5,n9,n1) ).
cnf(u43190,axiom,
p(n6,n7,n1) ).
cnf(u43194,axiom,
p(n6,n8,n1) ).
cnf(u43198,axiom,
p(n6,n9,n1) ).
cnf(u43203,axiom,
p(n4,n4,n9) ).
cnf(u43207,axiom,
p(n4,n5,n9) ).
cnf(u43211,axiom,
p(n4,n6,n9) ).
cnf(u43215,axiom,
p(n5,n4,n9) ).
cnf(u43219,axiom,
p(n5,n5,n9) ).
cnf(u43223,axiom,
p(n5,n6,n9) ).
cnf(u43228,axiom,
~ p(n6,n4,n9) ).
cnf(u43231,axiom,
p(n6,n5,n9) ).
cnf(u43235,axiom,
p(n6,n6,n9) ).
cnf(u43241,axiom,
~ p(n4,n4,n8) ).
cnf(u43244,axiom,
p(n4,n5,n8) ).
cnf(u43248,axiom,
p(n4,n6,n8) ).
cnf(u43252,axiom,
p(n5,n4,n8) ).
cnf(u43256,axiom,
p(n5,n5,n8) ).
cnf(u43260,axiom,
p(n5,n6,n8) ).
cnf(u43264,axiom,
p(n6,n4,n8) ).
cnf(u43268,axiom,
p(n6,n5,n8) ).
cnf(u43272,axiom,
p(n6,n6,n8) ).
cnf(u43277,axiom,
p(n4,n4,n7) ).
cnf(u43281,axiom,
p(n4,n5,n7) ).
cnf(u43285,axiom,
p(n4,n6,n7) ).
cnf(u43289,axiom,
p(n5,n4,n7) ).
cnf(u43293,axiom,
p(n5,n5,n7) ).
cnf(u43298,axiom,
~ p(n5,n6,n7) ).
cnf(u43301,axiom,
p(n6,n4,n7) ).
cnf(u43305,axiom,
p(n6,n5,n7) ).
cnf(u43309,axiom,
p(n6,n6,n7) ).
cnf(u43314,axiom,
p(n4,n4,n6) ).
cnf(u43318,axiom,
p(n4,n5,n6) ).
cnf(u43323,axiom,
~ p(n4,n6,n6) ).
cnf(u43326,axiom,
p(n5,n4,n6) ).
cnf(u43330,axiom,
p(n5,n5,n6) ).
cnf(u43334,axiom,
p(n5,n6,n6) ).
cnf(u43338,axiom,
p(n6,n4,n6) ).
cnf(u43342,axiom,
p(n6,n5,n6) ).
cnf(u43346,axiom,
p(n6,n6,n6) ).
cnf(u43351,axiom,
p(n4,n4,n5) ).
cnf(u43356,axiom,
~ p(n4,n5,n5) ).
cnf(u43359,axiom,
p(n4,n6,n5) ).
cnf(u43363,axiom,
p(n5,n4,n5) ).
cnf(u43367,axiom,
p(n5,n5,n5) ).
cnf(u43371,axiom,
p(n5,n6,n5) ).
cnf(u43375,axiom,
p(n6,n4,n5) ).
cnf(u43379,axiom,
p(n6,n5,n5) ).
cnf(u43383,axiom,
p(n6,n6,n5) ).
cnf(u43388,axiom,
p(n4,n4,n4) ).
cnf(u43392,axiom,
p(n4,n5,n4) ).
cnf(u43396,axiom,
p(n4,n6,n4) ).
cnf(u43401,axiom,
~ p(n5,n4,n4) ).
cnf(u43404,axiom,
p(n5,n5,n4) ).
cnf(u43408,axiom,
p(n5,n6,n4) ).
cnf(u43412,axiom,
p(n6,n4,n4) ).
cnf(u43416,axiom,
p(n6,n5,n4) ).
cnf(u43420,axiom,
p(n6,n6,n4) ).
cnf(u43425,axiom,
p(n4,n4,n3) ).
cnf(u43429,axiom,
p(n4,n5,n3) ).
cnf(u43433,axiom,
p(n4,n6,n3) ).
cnf(u43437,axiom,
p(n5,n4,n3) ).
cnf(u43441,axiom,
p(n5,n5,n3) ).
cnf(u43445,axiom,
p(n5,n6,n3) ).
cnf(u43449,axiom,
p(n6,n4,n3) ).
cnf(u43453,axiom,
p(n6,n5,n3) ).
cnf(u43458,axiom,
~ p(n6,n6,n3) ).
cnf(u43462,axiom,
p(n4,n4,n2) ).
cnf(u43466,axiom,
p(n4,n5,n2) ).
cnf(u43470,axiom,
p(n4,n6,n2) ).
cnf(u43474,axiom,
p(n5,n4,n2) ).
cnf(u43479,axiom,
~ p(n5,n5,n2) ).
cnf(u43482,axiom,
p(n5,n6,n2) ).
cnf(u43486,axiom,
p(n6,n4,n2) ).
cnf(u43490,axiom,
p(n6,n5,n2) ).
cnf(u43494,axiom,
p(n6,n6,n2) ).
cnf(u43499,axiom,
p(n4,n4,n1) ).
cnf(u43503,axiom,
p(n4,n5,n1) ).
cnf(u43507,axiom,
p(n4,n6,n1) ).
cnf(u43511,axiom,
p(n5,n4,n1) ).
cnf(u43515,axiom,
p(n5,n5,n1) ).
cnf(u43519,axiom,
p(n5,n6,n1) ).
cnf(u43523,axiom,
p(n6,n4,n1) ).
cnf(u43528,axiom,
~ p(n6,n5,n1) ).
cnf(u43531,axiom,
p(n6,n6,n1) ).
cnf(u43536,axiom,
p(n4,n1,n9) ).
cnf(u43540,axiom,
p(n4,n2,n9) ).
cnf(u43545,axiom,
~ p(n4,n3,n9) ).
cnf(u43548,axiom,
p(n5,n1,n9) ).
cnf(u43552,axiom,
p(n5,n2,n9) ).
cnf(u43556,axiom,
p(n5,n3,n9) ).
cnf(u43560,axiom,
p(n6,n1,n9) ).
cnf(u43564,axiom,
p(n6,n2,n9) ).
cnf(u43568,axiom,
p(n6,n3,n9) ).
cnf(u43573,axiom,
p(n4,n1,n8) ).
cnf(u43577,axiom,
p(n4,n2,n8) ).
cnf(u43581,axiom,
p(n4,n3,n8) ).
cnf(u43585,axiom,
p(n5,n1,n8) ).
cnf(u43590,axiom,
~ p(n5,n2,n8) ).
cnf(u43593,axiom,
p(n5,n3,n8) ).
cnf(u43597,axiom,
p(n6,n1,n8) ).
cnf(u43601,axiom,
p(n6,n2,n8) ).
cnf(u43605,axiom,
p(n6,n3,n8) ).
cnf(u43610,axiom,
p(n4,n1,n7) ).
cnf(u43614,axiom,
p(n4,n2,n7) ).
cnf(u43618,axiom,
p(n4,n3,n7) ).
cnf(u43622,axiom,
p(n5,n1,n7) ).
cnf(u43626,axiom,
p(n5,n2,n7) ).
cnf(u43630,axiom,
p(n5,n3,n7) ).
cnf(u43634,axiom,
p(n6,n1,n7) ).
cnf(u43638,axiom,
p(n6,n2,n7) ).
cnf(u43643,axiom,
~ p(n6,n3,n7) ).
cnf(u43647,axiom,
p(n4,n1,n6) ).
cnf(u43651,axiom,
p(n4,n2,n6) ).
cnf(u43655,axiom,
p(n4,n3,n6) ).
cnf(u43659,axiom,
p(n5,n1,n6) ).
cnf(u43663,axiom,
p(n5,n2,n6) ).
cnf(u43667,axiom,
p(n5,n3,n6) ).
cnf(u43671,axiom,
p(n6,n1,n6) ).
cnf(u43676,axiom,
~ p(n6,n2,n6) ).
cnf(u43679,axiom,
p(n6,n3,n6) ).
cnf(u43684,axiom,
p(n4,n1,n5) ).
cnf(u43688,axiom,
p(n4,n2,n5) ).
cnf(u43692,axiom,
p(n4,n3,n5) ).
cnf(u43696,axiom,
p(n5,n1,n5) ).
cnf(u43700,axiom,
p(n5,n2,n5) ).
cnf(u43705,axiom,
~ p(n5,n3,n5) ).
cnf(u43708,axiom,
p(n6,n1,n5) ).
cnf(u43712,axiom,
p(n6,n2,n5) ).
cnf(u43716,axiom,
p(n6,n3,n5) ).
cnf(u43722,axiom,
~ p(n4,n1,n4) ).
cnf(u43725,axiom,
p(n4,n2,n4) ).
cnf(u43729,axiom,
p(n4,n3,n4) ).
cnf(u43733,axiom,
p(n5,n1,n4) ).
cnf(u43737,axiom,
p(n5,n2,n4) ).
cnf(u43741,axiom,
p(n5,n3,n4) ).
cnf(u43745,axiom,
p(n6,n1,n4) ).
cnf(u43749,axiom,
p(n6,n2,n4) ).
cnf(u43753,axiom,
p(n6,n3,n4) ).
cnf(u43758,axiom,
p(n4,n1,n3) ).
cnf(u43763,axiom,
~ p(n4,n2,n3) ).
cnf(u43766,axiom,
p(n4,n3,n3) ).
cnf(u43770,axiom,
p(n5,n1,n3) ).
cnf(u43774,axiom,
p(n5,n2,n3) ).
cnf(u43778,axiom,
p(n5,n3,n3) ).
cnf(u43782,axiom,
p(n6,n1,n3) ).
cnf(u43786,axiom,
p(n6,n2,n3) ).
cnf(u43790,axiom,
p(n6,n3,n3) ).
cnf(u43795,axiom,
p(n4,n1,n2) ).
cnf(u43799,axiom,
p(n4,n2,n2) ).
cnf(u43803,axiom,
p(n4,n3,n2) ).
cnf(u43807,axiom,
p(n5,n1,n2) ).
cnf(u43811,axiom,
p(n5,n2,n2) ).
cnf(u43815,axiom,
p(n5,n3,n2) ).
cnf(u43820,axiom,
~ p(n6,n1,n2) ).
cnf(u43823,axiom,
p(n6,n2,n2) ).
cnf(u43827,axiom,
p(n6,n3,n2) ).
cnf(u43832,axiom,
p(n4,n1,n1) ).
cnf(u43836,axiom,
p(n4,n2,n1) ).
cnf(u43840,axiom,
p(n4,n3,n1) ).
cnf(u43845,axiom,
~ p(n5,n1,n1) ).
cnf(u43848,axiom,
p(n5,n2,n1) ).
cnf(u43852,axiom,
p(n5,n3,n1) ).
cnf(u43856,axiom,
p(n6,n1,n1) ).
cnf(u43860,axiom,
p(n6,n2,n1) ).
cnf(u43864,axiom,
p(n6,n3,n1) ).
cnf(u43869,axiom,
p(n1,n7,n9) ).
cnf(u43873,axiom,
p(n1,n8,n9) ).
cnf(u43878,axiom,
~ p(n1,n9,n9) ).
cnf(u43881,axiom,
p(n2,n7,n9) ).
cnf(u43885,axiom,
p(n2,n8,n9) ).
cnf(u43889,axiom,
p(n2,n9,n9) ).
cnf(u43893,axiom,
p(n3,n7,n9) ).
cnf(u43897,axiom,
p(n3,n8,n9) ).
cnf(u43901,axiom,
p(n3,n9,n9) ).
cnf(u43906,axiom,
p(n1,n7,n8) ).
cnf(u43910,axiom,
p(n1,n8,n8) ).
cnf(u43914,axiom,
p(n1,n9,n8) ).
cnf(u43918,axiom,
p(n2,n7,n8) ).
cnf(u43922,axiom,
p(n2,n8,n8) ).
cnf(u43926,axiom,
p(n2,n9,n8) ).
cnf(u43931,axiom,
~ p(n3,n7,n8) ).
cnf(u43934,axiom,
p(n3,n8,n8) ).
cnf(u43938,axiom,
p(n3,n9,n8) ).
cnf(u43943,axiom,
p(n1,n7,n7) ).
cnf(u43948,axiom,
~ p(n1,n8,n7) ).
cnf(u43951,axiom,
p(n1,n9,n7) ).
cnf(u43955,axiom,
p(n2,n7,n7) ).
cnf(u43959,axiom,
p(n2,n8,n7) ).
cnf(u43963,axiom,
p(n2,n9,n7) ).
cnf(u43967,axiom,
p(n3,n7,n7) ).
cnf(u43971,axiom,
p(n3,n8,n7) ).
cnf(u43975,axiom,
p(n3,n9,n7) ).
cnf(u43980,axiom,
p(n1,n7,n6) ).
cnf(u43984,axiom,
p(n1,n8,n6) ).
cnf(u43988,axiom,
p(n1,n9,n6) ).
cnf(u43992,axiom,
p(n2,n7,n6) ).
cnf(u43997,axiom,
~ p(n2,n8,n6) ).
cnf(u44000,axiom,
p(n2,n9,n6) ).
cnf(u44004,axiom,
p(n3,n7,n6) ).
cnf(u44008,axiom,
p(n3,n8,n6) ).
cnf(u44012,axiom,
p(n3,n9,n6) ).
cnf(u44017,axiom,
p(n1,n7,n5) ).
cnf(u44021,axiom,
p(n1,n8,n5) ).
cnf(u44025,axiom,
p(n1,n9,n5) ).
cnf(u44030,axiom,
~ p(n2,n7,n5) ).
cnf(u44033,axiom,
p(n2,n8,n5) ).
cnf(u44037,axiom,
p(n2,n9,n5) ).
cnf(u44041,axiom,
p(n3,n7,n5) ).
cnf(u44045,axiom,
p(n3,n8,n5) ).
cnf(u44049,axiom,
p(n3,n9,n5) ).
cnf(u44054,axiom,
p(n1,n7,n4) ).
cnf(u44058,axiom,
p(n1,n8,n4) ).
cnf(u44062,axiom,
p(n1,n9,n4) ).
cnf(u44066,axiom,
p(n2,n7,n4) ).
cnf(u44070,axiom,
p(n2,n8,n4) ).
cnf(u44074,axiom,
p(n2,n9,n4) ).
cnf(u44078,axiom,
p(n3,n7,n4) ).
cnf(u44082,axiom,
p(n3,n8,n4) ).
cnf(u44087,axiom,
~ p(n3,n9,n4) ).
cnf(u44091,axiom,
p(n1,n7,n3) ).
cnf(u44095,axiom,
p(n1,n8,n3) ).
cnf(u44099,axiom,
p(n1,n9,n3) ).
cnf(u44103,axiom,
p(n2,n7,n3) ).
cnf(u44107,axiom,
p(n2,n8,n3) ).
cnf(u44111,axiom,
p(n2,n9,n3) ).
cnf(u44115,axiom,
p(n3,n7,n3) ).
cnf(u44120,axiom,
~ p(n3,n8,n3) ).
cnf(u44123,axiom,
p(n3,n9,n3) ).
cnf(u44129,axiom,
~ p(n1,n7,n2) ).
cnf(u44132,axiom,
p(n1,n8,n2) ).
cnf(u44136,axiom,
p(n1,n9,n2) ).
cnf(u44140,axiom,
p(n2,n7,n2) ).
cnf(u44144,axiom,
p(n2,n8,n2) ).
cnf(u44148,axiom,
p(n2,n9,n2) ).
cnf(u44152,axiom,
p(n3,n7,n2) ).
cnf(u44156,axiom,
p(n3,n8,n2) ).
cnf(u44160,axiom,
p(n3,n9,n2) ).
cnf(u44165,axiom,
p(n1,n7,n1) ).
cnf(u44169,axiom,
p(n1,n8,n1) ).
cnf(u44173,axiom,
p(n1,n9,n1) ).
cnf(u44177,axiom,
p(n2,n7,n1) ).
cnf(u44181,axiom,
p(n2,n8,n1) ).
cnf(u44186,axiom,
~ p(n2,n9,n1) ).
cnf(u44189,axiom,
p(n3,n7,n1) ).
cnf(u44193,axiom,
p(n3,n8,n1) ).
cnf(u44197,axiom,
p(n3,n9,n1) ).
cnf(u44202,axiom,
p(n1,n4,n9) ).
cnf(u44206,axiom,
p(n1,n5,n9) ).
cnf(u44210,axiom,
p(n1,n6,n9) ).
cnf(u44214,axiom,
p(n2,n4,n9) ).
cnf(u44219,axiom,
~ p(n2,n5,n9) ).
cnf(u44222,axiom,
p(n2,n6,n9) ).
cnf(u44226,axiom,
p(n3,n4,n9) ).
cnf(u44230,axiom,
p(n3,n5,n9) ).
cnf(u44234,axiom,
p(n3,n6,n9) ).
cnf(u44239,axiom,
p(n1,n4,n8) ).
cnf(u44244,axiom,
~ p(n1,n5,n8) ).
cnf(u44247,axiom,
p(n1,n6,n8) ).
cnf(u44251,axiom,
p(n2,n4,n8) ).
cnf(u44255,axiom,
p(n2,n5,n8) ).
cnf(u44259,axiom,
p(n2,n6,n8) ).
cnf(u44263,axiom,
p(n3,n4,n8) ).
cnf(u44267,axiom,
p(n3,n5,n8) ).
cnf(u44271,axiom,
p(n3,n6,n8) ).
cnf(u44276,axiom,
p(n1,n4,n7) ).
cnf(u44280,axiom,
p(n1,n5,n7) ).
cnf(u44284,axiom,
p(n1,n6,n7) ).
cnf(u44288,axiom,
p(n2,n4,n7) ).
cnf(u44292,axiom,
p(n2,n5,n7) ).
cnf(u44296,axiom,
p(n2,n6,n7) ).
cnf(u44300,axiom,
p(n3,n4,n7) ).
cnf(u44305,axiom,
~ p(n3,n5,n7) ).
cnf(u44308,axiom,
p(n3,n6,n7) ).
cnf(u44313,axiom,
p(n1,n4,n6) ).
cnf(u44317,axiom,
p(n1,n5,n6) ).
cnf(u44321,axiom,
p(n1,n6,n6) ).
cnf(u44325,axiom,
p(n2,n4,n6) ).
cnf(u44329,axiom,
p(n2,n5,n6) ).
cnf(u44333,axiom,
p(n2,n6,n6) ).
cnf(u44338,axiom,
~ p(n3,n4,n6) ).
cnf(u44341,axiom,
p(n3,n5,n6) ).
cnf(u44345,axiom,
p(n3,n6,n6) ).
cnf(u44350,axiom,
p(n1,n4,n5) ).
cnf(u44354,axiom,
p(n1,n5,n5) ).
cnf(u44358,axiom,
p(n1,n6,n5) ).
cnf(u44362,axiom,
p(n2,n4,n5) ).
cnf(u44366,axiom,
p(n2,n5,n5) ).
cnf(u44370,axiom,
p(n2,n6,n5) ).
cnf(u44374,axiom,
p(n3,n4,n5) ).
cnf(u44378,axiom,
p(n3,n5,n5) ).
cnf(u44383,axiom,
~ p(n3,n6,n5) ).
cnf(u44387,axiom,
p(n1,n4,n4) ).
cnf(u44391,axiom,
p(n1,n5,n4) ).
cnf(u44395,axiom,
p(n1,n6,n4) ).
cnf(u44399,axiom,
p(n2,n4,n4) ).
cnf(u44403,axiom,
p(n2,n5,n4) ).
cnf(u44408,axiom,
~ p(n2,n6,n4) ).
cnf(u44411,axiom,
p(n3,n4,n4) ).
cnf(u44415,axiom,
p(n3,n5,n4) ).
cnf(u44419,axiom,
p(n3,n6,n4) ).
cnf(u44425,axiom,
~ p(n1,n4,n3) ).
cnf(u44428,axiom,
p(n1,n5,n3) ).
cnf(u44432,axiom,
p(n1,n6,n3) ).
cnf(u44436,axiom,
p(n2,n4,n3) ).
cnf(u44440,axiom,
p(n2,n5,n3) ).
cnf(u44444,axiom,
p(n2,n6,n3) ).
cnf(u44448,axiom,
p(n3,n4,n3) ).
cnf(u44452,axiom,
p(n3,n5,n3) ).
cnf(u44456,axiom,
p(n3,n6,n3) ).
cnf(u44461,axiom,
p(n1,n4,n2) ).
cnf(u44465,axiom,
p(n1,n5,n2) ).
cnf(u44469,axiom,
p(n1,n6,n2) ).
cnf(u44474,axiom,
~ p(n2,n4,n2) ).
cnf(u44477,axiom,
p(n2,n5,n2) ).
cnf(u44481,axiom,
p(n2,n6,n2) ).
cnf(u44485,axiom,
p(n3,n4,n2) ).
cnf(u44489,axiom,
p(n3,n5,n2) ).
cnf(u44493,axiom,
p(n3,n6,n2) ).
cnf(u44498,axiom,
p(n1,n4,n1) ).
cnf(u44502,axiom,
p(n1,n5,n1) ).
cnf(u44507,axiom,
~ p(n1,n6,n1) ).
cnf(u44510,axiom,
p(n2,n4,n1) ).
cnf(u44514,axiom,
p(n2,n5,n1) ).
cnf(u44518,axiom,
p(n2,n6,n1) ).
cnf(u44522,axiom,
p(n3,n4,n1) ).
cnf(u44526,axiom,
p(n3,n5,n1) ).
cnf(u44530,axiom,
p(n3,n6,n1) ).
cnf(u44535,axiom,
p(n1,n1,n9) ).
cnf(u44539,axiom,
p(n1,n2,n9) ).
cnf(u44543,axiom,
p(n1,n3,n9) ).
cnf(u44547,axiom,
p(n2,n1,n9) ).
cnf(u44551,axiom,
p(n2,n2,n9) ).
cnf(u44555,axiom,
p(n2,n3,n9) ).
cnf(u44560,axiom,
~ p(n3,n1,n9) ).
cnf(u44563,axiom,
p(n3,n2,n9) ).
cnf(u44567,axiom,
p(n3,n3,n9) ).
cnf(u44572,axiom,
p(n1,n1,n8) ).
cnf(u44576,axiom,
p(n1,n2,n8) ).
cnf(u44580,axiom,
p(n1,n3,n8) ).
cnf(u44585,axiom,
~ p(n2,n1,n8) ).
cnf(u44588,axiom,
p(n2,n2,n8) ).
cnf(u44592,axiom,
p(n2,n3,n8) ).
cnf(u44596,axiom,
p(n3,n1,n8) ).
cnf(u44600,axiom,
p(n3,n2,n8) ).
cnf(u44604,axiom,
p(n3,n3,n8) ).
cnf(u44609,axiom,
p(n1,n1,n7) ).
cnf(u44613,axiom,
p(n1,n2,n7) ).
cnf(u44617,axiom,
p(n1,n3,n7) ).
cnf(u44621,axiom,
p(n2,n1,n7) ).
cnf(u44626,axiom,
~ p(n2,n2,n7) ).
cnf(u44629,axiom,
p(n2,n3,n7) ).
cnf(u44633,axiom,
p(n3,n1,n7) ).
cnf(u44637,axiom,
p(n3,n2,n7) ).
cnf(u44641,axiom,
p(n3,n3,n7) ).
cnf(u44647,axiom,
~ p(n1,n1,n6) ).
cnf(u44650,axiom,
p(n1,n2,n6) ).
cnf(u44654,axiom,
p(n1,n3,n6) ).
cnf(u44658,axiom,
p(n2,n1,n6) ).
cnf(u44662,axiom,
p(n2,n2,n6) ).
cnf(u44666,axiom,
p(n2,n3,n6) ).
cnf(u44670,axiom,
p(n3,n1,n6) ).
cnf(u44674,axiom,
p(n3,n2,n6) ).
cnf(u44678,axiom,
p(n3,n3,n6) ).
cnf(u44683,axiom,
p(n1,n1,n5) ).
cnf(u44688,axiom,
~ p(n1,n2,n5) ).
cnf(u44691,axiom,
p(n1,n3,n5) ).
cnf(u44695,axiom,
p(n2,n1,n5) ).
cnf(u44699,axiom,
p(n2,n2,n5) ).
cnf(u44703,axiom,
p(n2,n3,n5) ).
cnf(u44707,axiom,
p(n3,n1,n5) ).
cnf(u44711,axiom,
p(n3,n2,n5) ).
cnf(u44715,axiom,
p(n3,n3,n5) ).
cnf(u44720,axiom,
p(n1,n1,n4) ).
cnf(u44724,axiom,
p(n1,n2,n4) ).
cnf(u44729,axiom,
~ p(n1,n3,n4) ).
cnf(u44732,axiom,
p(n2,n1,n4) ).
cnf(u44736,axiom,
p(n2,n2,n4) ).
cnf(u44740,axiom,
p(n2,n3,n4) ).
cnf(u44744,axiom,
p(n3,n1,n4) ).
cnf(u44748,axiom,
p(n3,n2,n4) ).
cnf(u44752,axiom,
p(n3,n3,n4) ).
cnf(u44757,axiom,
p(n1,n1,n3) ).
cnf(u44761,axiom,
p(n1,n2,n3) ).
cnf(u44765,axiom,
p(n1,n3,n3) ).
cnf(u44769,axiom,
p(n2,n1,n3) ).
cnf(u44773,axiom,
p(n2,n2,n3) ).
cnf(u44778,axiom,
~ p(n2,n3,n3) ).
cnf(u44781,axiom,
p(n3,n1,n3) ).
cnf(u44785,axiom,
p(n3,n2,n3) ).
cnf(u44789,axiom,
p(n3,n3,n3) ).
cnf(u44794,axiom,
p(n1,n1,n2) ).
cnf(u44798,axiom,
p(n1,n2,n2) ).
cnf(u44802,axiom,
p(n1,n3,n2) ).
cnf(u44806,axiom,
p(n2,n1,n2) ).
cnf(u44810,axiom,
p(n2,n2,n2) ).
cnf(u44814,axiom,
p(n2,n3,n2) ).
cnf(u44818,axiom,
p(n3,n1,n2) ).
cnf(u44822,axiom,
p(n3,n2,n2) ).
cnf(u44827,axiom,
~ p(n3,n3,n2) ).
cnf(u44831,axiom,
p(n1,n1,n1) ).
cnf(u44835,axiom,
p(n1,n2,n1) ).
cnf(u44839,axiom,
p(n1,n3,n1) ).
cnf(u44843,axiom,
p(n2,n1,n1) ).
cnf(u44847,axiom,
p(n2,n2,n1) ).
cnf(u44851,axiom,
p(n2,n3,n1) ).
cnf(u44855,axiom,
p(n3,n1,n1) ).
cnf(u44860,axiom,
~ p(n3,n2,n1) ).
cnf(u44863,axiom,
p(n3,n3,n1) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ080+2 : TPTP v9.3.1. Bugfixed v5.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.36 % Computer : n003.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sun Sep 27 22:41:56 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.39 Running first-order model finding
% 0.08/0.39 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.77/0.83 % (990194)Will run a generic schedule for satisfiability detection.
% 0.77/0.83 % (990201)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1210541670:i=88024:add=on:rawr=on_2997 on theBenchmark for (2997ds/88024Mi)
% 0.77/0.83 % (990200)% WARNING: option uhcvi not known.
% 0.77/0.83 % (990199)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=274021018_2997 on theBenchmark for (2997ds/0Mi)
% 0.77/0.83 % (990200)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=770900701:i=135531:add=off:rawr=on_2997 on theBenchmark for (2997ds/135531Mi)
% 0.77/0.83 % (990202)dis+10_1_sil=32000:sp=arity:random_seed=567973768:i=103:fgj=on_2997 on theBenchmark for (2997ds/103Mi)
% 0.77/0.83 % (990203)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1520412425:i=116_2997 on theBenchmark for (2997ds/116Mi)
% 0.77/0.83 % (990204)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3658114227:i=131_2997 on theBenchmark for (2997ds/131Mi)
% 0.77/0.83 % (990205)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=759944053:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2997 on theBenchmark for (2997ds/159Mi)
% 0.77/0.83 % (990202)Instruction limit reached!
% 0.77/0.83 % (990202)------------------------------
% 0.77/0.83 % (990202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.83 % (990202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.83 % (990202)CaDiCaL version: 2.1.3
% 0.77/0.83 % (990202)Termination reason: Instruction limit
% 0.77/0.83 % (990202)Termination phase: Property scanning
% 0.77/0.83 % (990202)Time elapsed: 0.053 s
% 0.77/0.83 % (990202)Peak memory usage: 22 MB
% 0.77/0.83 % (990202)Instructions burned: 105 (million)
% 0.77/0.83 % (990204)Instruction limit reached!
% 0.77/0.83 % (990204)------------------------------
% 0.77/0.83 % (990204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.83 % (990204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.83 % (990204)CaDiCaL version: 2.1.3
% 0.77/0.83 % (990204)Termination reason: Instruction limit
% 0.77/0.83 % (990204)Termination phase: Property scanning
% 0.77/0.83 % (990204)Time elapsed: 0.062 s
% 0.77/0.83 % (990204)Peak memory usage: 22 MB
% 0.77/0.83 % (990204)Instructions burned: 131 (million)
% 0.77/0.83 % (990203)Instruction limit reached!
% 0.77/0.83 % (990203)------------------------------
% 0.77/0.83 % (990203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.83 % (990203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.83 % (990203)CaDiCaL version: 2.1.3
% 0.77/0.83 % (990203)Termination reason: Instruction limit
% 0.77/0.83 % (990203)Termination phase: Property scanning
% 0.77/0.83 % (990203)Time elapsed: 0.068 s
% 0.77/0.83 % (990203)Peak memory usage: 24 MB
% 0.77/0.83 % (990203)Instructions burned: 119 (million)
% 0.77/0.83 % (990213)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1103469274:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 0.77/0.83 % (990205)Instruction limit reached!
% 0.77/0.83 % (990205)------------------------------
% 0.77/0.83 % (990205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.83 % (990205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.83 % (990205)CaDiCaL version: 2.1.3
% 0.77/0.83 % (990205)Termination reason: Instruction limit
% 0.77/0.83 % (990205)Termination phase: Property scanning
% 0.77/0.83 % (990205)Time elapsed: 0.074 s
% 0.77/0.83 % (990205)Peak memory usage: 22 MB
% 0.77/0.83 % (990205)Instructions burned: 159 (million)
% 0.77/0.83 % (990214)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2794613886:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 0.77/0.83 % (990215)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2425476482:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 0.77/0.83 % (990217)ott-21_1_sil=16000:fs=off:random_seed=713639285:i=180:av=off:fsr=off_2996 on theBenchmark for (2996ds/180Mi)
% 0.77/0.83 % (990214)Instruction limit reached!
% 0.77/0.83 % (990214)------------------------------
% 0.77/0.83 % (990214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.83 % (990214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.83 % (990214)CaDiCaL version: 2.1.3
% 0.77/0.83 % (990214)Termination reason: Instruction limit
% 0.77/0.83 % (990214)Termination phase: Property scanning
% 0.77/0.83 % (990214)Time elapsed: 0.061 s
% 0.77/0.83 % (990214)Peak memory usage: 22 MB
% 0.77/0.83 % (990214)Instructions burned: 131 (million)
% 0.77/0.83 % (990221)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=363751172:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 0.77/0.83 % (990200) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-990194-990200"...
% 0.77/0.83 % (990217)Instruction limit reached!
% 0.77/0.83 % (990217)------------------------------
% 0.77/0.83 % (990217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.83 % (990217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.83 % (990217)CaDiCaL version: 2.1.3
% 0.77/0.83 % (990217)Termination reason: Instruction limit
% 0.77/0.83 % (990217)Termination phase: Saturation
% 0.77/0.83 % (990217)Time elapsed: 0.078 s
% 0.77/0.83 % (990217)Peak memory usage: 22 MB
% 0.77/0.83 % (990217)Instructions burned: 180 (million)
% 0.77/0.83 % (990200)...printing done.
% 0.77/0.83 % SZS status Satisfiable for theBenchmark
% 0.77/0.83 % SZS output start Saturation.
% See solution above
% 0.77/0.84 % SZS output start Definitions and Model Updates.
% 0.77/0.84 globally flip the polarity of every occurrence of predicate "p"
% 0.77/0.84 % SZS output end Definitions and Model Updates.
% 0.77/0.84 % (990200)------------------------------
% 0.77/0.84 % (990200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.84 % (990200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.84 % (990200)CaDiCaL version: 2.1.3
% 0.77/0.84 % (990200)Termination reason: Satisfiable
% 0.77/0.84 % (990200)Time elapsed: 0.179 s
% 0.77/0.84 % (990200)Peak memory usage: 35 MB
% 0.77/0.84 % (990200)Instructions burned: 337 (million)
% 0.77/0.84 % (990194)Success in time 0.429 s
% 0.77/0.84 % Vampire exiting
%------------------------------------------------------------------------------