%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PUZ067+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 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:32:08 PM UTC 2026
% Result : Satisfiable 1.74s 0.83s
% Output : Saturation 1.74s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u2031,axiom,
n2 != ssA(n1,n9) ).
cnf(u2036,axiom,
n2 = ssA(n1,n8) ).
cnf(u2039,axiom,
n2 != ssA(n1,n3) ).
cnf(u2043,axiom,
n2 != ssA(n1,n2) ).
cnf(u2047,axiom,
n2 != ssA(n1,n1) ).
cnf(u2138,axiom,
n6 != ssA(n1,n8) ).
cnf(u2143,axiom,
n6 = ssA(n1,n3) ).
cnf(u2146,axiom,
n6 != ssA(n1,n2) ).
cnf(u2246,axiom,
n1 != ssA(n2,n6) ).
cnf(u2250,axiom,
n1 != ssA(n2,n5) ).
cnf(u2255,axiom,
n1 = ssA(n2,n3) ).
cnf(u2302,axiom,
n3 != ssA(n2,n9) ).
cnf(u2306,axiom,
n3 != ssA(n2,n8) ).
cnf(u2310,axiom,
n3 != ssA(n2,n7) ).
cnf(u2314,axiom,
n3 != ssA(n2,n6) ).
cnf(u2319,axiom,
n3 = ssA(n2,n5) ).
cnf(u2429,axiom,
n4 != ssA(n2,n8) ).
cnf(u2434,axiom,
n4 = ssA(n2,n7) ).
cnf(u2437,axiom,
n4 != ssA(n2,n1) ).
cnf(u2491,axiom,
n6 != ssA(n2,n9) ).
cnf(u2496,axiom,
n6 = ssA(n2,n8) ).
cnf(u2499,axiom,
n6 != ssA(n2,n7) ).
cnf(u2503,axiom,
n6 != ssA(n2,n6) ).
cnf(u2571,axiom,
n7 != ssA(n2,n9) ).
cnf(u2575,axiom,
n7 != ssA(n2,n8) ).
cnf(u2579,axiom,
n7 != ssA(n2,n7) ).
cnf(u3012,axiom,
n8 != ssA(n1,n3) ).
cnf(u3017,axiom,
n8 = ssA(n1,n1) ).
cnf(u3036,axiom,
n8 != ssA(n2,n3) ).
cnf(u3040,axiom,
n8 != ssA(n2,n1) ).
cnf(u3567,axiom,
n1 != ssA(n3,n6) ).
cnf(u3571,axiom,
n1 != ssA(n3,n5) ).
cnf(u3576,axiom,
n1 = ssA(n3,n4) ).
cnf(u3615,axiom,
n2 != ssA(n3,n8) ).
cnf(u3619,axiom,
n2 != ssA(n3,n7) ).
cnf(u3624,axiom,
n2 = ssA(n3,n3) ).
cnf(u3627,axiom,
n2 != ssA(n3,n1) ).
cnf(u3687,axiom,
n5 = ssA(n3,n7) ).
cnf(u3690,axiom,
n5 != ssA(n3,n6) ).
cnf(u3694,axiom,
n5 != ssA(n3,n5) ).
cnf(u3726,axiom,
n6 = ssA(n3,n6) ).
cnf(u3729,axiom,
n6 != ssA(n3,n5) ).
cnf(u3733,axiom,
n6 != ssA(n3,n3) ).
cnf(u3830,axiom,
n2 = ssA(n4,n9) ).
cnf(u3833,axiom,
n2 != ssA(n4,n6) ).
cnf(u3837,axiom,
n2 != ssA(n4,n3) ).
cnf(u3994,axiom,
n8 != ssA(n4,n8) ).
cnf(u3999,axiom,
n8 = ssA(n4,n2) ).
cnf(u4279,axiom,
n7 != ssA(n3,n3) ).
cnf(u4283,axiom,
n7 != ssA(n3,n1) ).
cnf(u4427,axiom,
n1 = ssA(n5,n9) ).
cnf(u4430,axiom,
n1 != ssA(n5,n8) ).
cnf(u4434,axiom,
n1 != ssA(n5,n5) ).
cnf(u4438,axiom,
n1 != ssA(n5,n2) ).
cnf(u4490,axiom,
n2 != ssA(n5,n9) ).
cnf(u4494,axiom,
n2 != ssA(n5,n8) ).
cnf(u4498,axiom,
n2 != ssA(n5,n7) ).
cnf(u4503,axiom,
n2 = ssA(n5,n5) ).
cnf(u4506,axiom,
n2 != ssA(n5,n1) ).
cnf(u4555,axiom,
n5 != ssA(n5,n5) ).
cnf(u4559,axiom,
n5 != ssA(n5,n4) ).
cnf(u5366,axiom,
n6 != ssA(n5,n9) ).
cnf(u5371,axiom,
n6 = ssA(n5,n4) ).
cnf(u5424,axiom,
n7 != ssA(n5,n7) ).
cnf(u5429,axiom,
n7 = ssA(n5,n2) ).
cnf(u5554,axiom,
n8 = ssA(n5,n8) ).
cnf(u5557,axiom,
n8 != ssA(n5,n7) ).
cnf(u5691,axiom,
n1 != ssA(n6,n9) ).
cnf(u5695,axiom,
n1 != ssA(n6,n5) ).
cnf(u5699,axiom,
n1 != ssA(n6,n3) ).
cnf(u5704,axiom,
n1 = ssA(n6,n2) ).
cnf(u5707,axiom,
n1 != ssA(n6,n1) ).
cnf(u5859,axiom,
n2 != ssA(n6,n9) ).
cnf(u5863,axiom,
n2 != ssA(n6,n7) ).
cnf(u5867,axiom,
n2 != ssA(n6,n6) ).
cnf(u5871,axiom,
n2 != ssA(n6,n5) ).
cnf(u5875,axiom,
n2 != ssA(n6,n3) ).
cnf(u5880,axiom,
n2 = ssA(n6,n1) ).
cnf(u5936,axiom,
n3 != ssA(n6,n9) ).
cnf(u5941,axiom,
n3 = ssA(n6,n7) ).
cnf(u5944,axiom,
n3 != ssA(n6,n6) ).
cnf(u5948,axiom,
n3 != ssA(n6,n5) ).
cnf(u5952,axiom,
n3 != ssA(n6,n4) ).
cnf(u5956,axiom,
n3 != ssA(n6,n3) ).
cnf(u6191,axiom,
n4 != ssA(n6,n6) ).
cnf(u6196,axiom,
n4 = ssA(n6,n5) ).
cnf(u6199,axiom,
n4 != ssA(n6,n1) ).
cnf(u6562,axiom,
n4 != ssA(n6,n3) ).
cnf(u6566,axiom,
n4 != ssA(n6,n2) ).
cnf(u7166,axiom,
n6 = ssA(n6,n9) ).
cnf(u7169,axiom,
n6 != ssA(n6,n5) ).
cnf(u7173,axiom,
n6 != ssA(n6,n4) ).
cnf(u7302,axiom,
n7 != ssA(n6,n4) ).
cnf(u7306,axiom,
n7 != ssA(n6,n3) ).
cnf(u7493,axiom,
n7 = ssA(n6,n6) ).
cnf(u7496,axiom,
n7 != ssA(n6,n1) ).
cnf(u7758,axiom,
n9 != ssA(n5,n9) ).
cnf(u7763,axiom,
n9 = ssA(n5,n7) ).
cnf(u8234,axiom,
n8 != ssA(n5,n5) ).
cnf(u8238,axiom,
n8 != ssA(n5,n4) ).
cnf(u8438,axiom,
n8 = ssA(n6,n4) ).
cnf(u8441,axiom,
n8 != ssA(n6,n1) ).
cnf(u8956,axiom,
n1 != ssA(n7,n9) ).
cnf(u8961,axiom,
n1 = ssA(n7,n6) ).
cnf(u8964,axiom,
n1 != ssA(n7,n5) ).
cnf(u9025,axiom,
n2 != ssA(n7,n9) ).
cnf(u9030,axiom,
n2 = ssA(n7,n7) ).
cnf(u9033,axiom,
n2 != ssA(n7,n3) ).
cnf(u9037,axiom,
n2 != ssA(n7,n2) ).
cnf(u9116,axiom,
n5 = ssA(n7,n9) ).
cnf(u9119,axiom,
n5 != ssA(n7,n5) ).
cnf(u9123,axiom,
n5 != ssA(n7,n3) ).
cnf(u9175,axiom,
n6 = ssA(n7,n5) ).
cnf(u9178,axiom,
n6 != ssA(n7,n1) ).
cnf(u9363,axiom,
n8 != ssA(n7,n5) ).
cnf(u9367,axiom,
n8 != ssA(n7,n1) ).
cnf(u9716,axiom,
n4 != ssA(n7,n6) ).
cnf(u9721,axiom,
n4 = ssA(n7,n2) ).
cnf(u9858,axiom,
n8 = ssA(n7,n3) ).
cnf(u9861,axiom,
n8 != ssA(n7,n2) ).
cnf(u12543,axiom,
n9 = ssA(n2,n9) ).
cnf(u12546,axiom,
n9 != ssA(n2,n1) ).
cnf(u14942,axiom,
n2 != ssA(n8,n9) ).
cnf(u14946,axiom,
n2 != ssA(n8,n8) ).
cnf(u14950,axiom,
n2 != ssA(n8,n7) ).
cnf(u14954,axiom,
n2 != ssA(n8,n6) ).
cnf(u14958,axiom,
n2 != ssA(n8,n5) ).
cnf(u14962,axiom,
n2 != ssA(n8,n3) ).
cnf(u14967,axiom,
n2 = ssA(n8,n2) ).
cnf(u15117,axiom,
n3 != ssA(n8,n9) ).
cnf(u15121,axiom,
n3 != ssA(n8,n8) ).
cnf(u15125,axiom,
n3 != ssA(n8,n5) ).
cnf(u15130,axiom,
n3 = ssA(n8,n4) ).
cnf(u15133,axiom,
n3 != ssA(n8,n3) ).
cnf(u15227,axiom,
n4 != ssA(n8,n3) ).
cnf(u15231,axiom,
n4 != ssA(n8,n2) ).
cnf(u15323,axiom,
n5 != ssA(n8,n9) ).
cnf(u15327,axiom,
n5 != ssA(n8,n7) ).
cnf(u15331,axiom,
n5 != ssA(n8,n5) ).
cnf(u15336,axiom,
n5 = ssA(n8,n3) ).
cnf(u15435,axiom,
n6 != ssA(n8,n8) ).
cnf(u15440,axiom,
n6 = ssA(n8,n7) ).
cnf(u15443,axiom,
n6 != ssA(n8,n3) ).
cnf(u15529,axiom,
n7 = ssA(n8,n9) ).
cnf(u15532,axiom,
n7 != ssA(n8,n8) ).
cnf(u15536,axiom,
n7 != ssA(n8,n3) ).
cnf(u15957,axiom,
n8 != ssA(n8,n8) ).
cnf(u15961,axiom,
n8 != ssA(n8,n3) ).
cnf(u16110,axiom,
n9 = ssA(n8,n8) ).
cnf(u16113,axiom,
n9 != ssA(n8,n5) ).
cnf(u17077,axiom,
n1 = ssA(n9,n8) ).
cnf(u17080,axiom,
n1 != ssA(n9,n6) ).
cnf(u17084,axiom,
n1 != ssA(n9,n5) ).
cnf(u17088,axiom,
n1 != ssA(n9,n4) ).
cnf(u17092,axiom,
n1 != ssA(n9,n3) ).
cnf(u17096,axiom,
n1 != ssA(n9,n2) ).
cnf(u17100,axiom,
n1 != ssA(n9,n1) ).
cnf(u17231,axiom,
n2 != ssA(n9,n7) ).
cnf(u17236,axiom,
n2 = ssA(n9,n6) ).
cnf(u17239,axiom,
n2 != ssA(n9,n5) ).
cnf(u17243,axiom,
n2 != ssA(n9,n3) ).
cnf(u17247,axiom,
n2 != ssA(n9,n2) ).
cnf(u17251,axiom,
n2 != ssA(n9,n1) ).
cnf(u17428,axiom,
n3 != ssA(n9,n7) ).
cnf(u17432,axiom,
n3 != ssA(n9,n5) ).
cnf(u17436,axiom,
n3 != ssA(n9,n4) ).
cnf(u17449,axiom,
n3 = ssA(n9,n1) ).
cnf(u17544,axiom,
n5 != ssA(n9,n7) ).
cnf(u17549,axiom,
n5 = ssA(n9,n5) ).
cnf(u17552,axiom,
n5 != ssA(n9,n4) ).
cnf(u17556,axiom,
n5 != ssA(n9,n3) ).
cnf(u17643,axiom,
n6 != ssA(n9,n7) ).
cnf(u17647,axiom,
n6 != ssA(n9,n4) ).
cnf(u17651,axiom,
n6 != ssA(n9,n3) ).
cnf(u17656,axiom,
n6 = ssA(n9,n2) ).
cnf(u17924,axiom,
n7 != ssA(n9,n7) ).
cnf(u17928,axiom,
n7 != ssA(n9,n4) ).
cnf(u17933,axiom,
n7 = ssA(n9,n3) ).
cnf(u18027,axiom,
n8 = ssA(n9,n7) ).
cnf(u18030,axiom,
n8 != ssA(n9,n4) ).
cnf(u1995,axiom,
n1 != ssA(n3,n1) ).
cnf(u918,axiom,
ssA(n5,n3) != ssA(n9,n3) ).
cnf(u749,axiom,
ssA(n8,n3) != ssA(n8,n7) ).
cnf(u1458,axiom,
ssA(n5,n8) != ssA(n6,n9) ).
cnf(u1958,axiom,
n5 != ssA(n6,n5) ).
cnf(u631,axiom,
ssA(n5,n1) != ssA(n5,n3) ).
cnf(u1161,axiom,
ssA(n2,n8) != ssA(n6,n8) ).
cnf(u877,axiom,
ssA(n4,n2) != ssA(n9,n2) ).
cnf(u391,axiom,
n3 != n5 ).
cnf(u16965,axiom,
n7 = ssA(n3,n8) ).
cnf(u1074,axiom,
ssA(n2,n6) != ssA(n3,n6) ).
cnf(u1076,axiom,
ssA(n1,n6) != ssA(n8,n6) ).
cnf(u722,axiom,
ssA(n7,n1) != ssA(n7,n2) ).
cnf(u1289,axiom,
ssA(n1,n6) != ssA(n3,n4) ).
cnf(u1917,axiom,
n1 != ssA(n3,n8) ).
cnf(u612,axiom,
ssA(n5,n3) != ssA(n5,n9) ).
cnf(u8918,axiom,
n9 != ssA(n8,n3) ).
cnf(u947,axiom,
ssA(n1,n3) != ssA(n2,n3) ).
cnf(u967,axiom,
ssA(n4,n4) != ssA(n9,n4) ).
cnf(u1859,axiom,
n1 != ssA(n4,n7) ).
cnf(u1182,axiom,
ssA(n8,n9) != ssA(n9,n9) ).
cnf(u613,axiom,
ssA(n5,n3) != ssA(n5,n8) ).
cnf(u1322,axiom,
ssA(n2,n9) != ssA(n3,n7) ).
cnf(u1822,axiom,
n4 != ssA(n6,n4) ).
cnf(u1476,axiom,
ssA(n4,n8) != ssA(n5,n9) ).
cnf(u383,axiom,
n4 != n8 ).
cnf(u387,axiom,
n3 != n9 ).
cnf(u1987,axiom,
n3 != ssA(n4,n8) ).
cnf(u1616,axiom,
ssA(n7,n7) != ssA(n9,n8) ).
cnf(u1092,axiom,
ssA(n8,n7) != ssA(n9,n7) ).
cnf(u734,axiom,
ssA(n8,n7) != ssA(n8,n8) ).
cnf(u1967,axiom,
n5 != ssA(n3,n8) ).
cnf(u1057,axiom,
ssA(n4,n6) != ssA(n9,n6) ).
cnf(u1427,axiom,
ssA(n4,n6) != ssA(n5,n4) ).
cnf(u608,axiom,
ssA(n5,n4) != ssA(n5,n8) ).
cnf(u1071,axiom,
ssA(n2,n6) != ssA(n6,n6) ).
cnf(u564,axiom,
ssA(n4,n4) != ssA(n4,n7) ).
cnf(u959,axiom,
ssA(n7,n4) != ssA(n8,n4) ).
cnf(u1205,axiom,
ssA(n2,n9) != ssA(n7,n9) ).
cnf(u1914,axiom,
n8 != ssA(n1,n8) ).
cnf(u1333,axiom,
ssA(n1,n9) != ssA(n3,n8) ).
cnf(u778,axiom,
ssA(n9,n7) != ssA(n9,n9) ).
cnf(u428,axiom,
ssA(n1,n4) != ssA(n1,n8) ).
cnf(u609,axiom,
ssA(n5,n4) != ssA(n5,n7) ).
cnf(u1864,axiom,
n1 != ssA(n6,n7) ).
cnf(u1468,axiom,
ssA(n4,n9) != ssA(n6,n8) ).
cnf(u379,axiom,
n5 != n8 ).
cnf(u1169,axiom,
ssA(n1,n8) != ssA(n5,n8) ).
cnf(u1163,axiom,
ssA(n2,n8) != ssA(n4,n8) ).
cnf(u856,axiom,
ssA(n1,n1) != ssA(n3,n1) ).
cnf(u598,axiom,
ssA(n5,n7) != ssA(n5,n9) ).
cnf(u1004,axiom,
ssA(n7,n5) != ssA(n8,n5) ).
cnf(u1831,axiom,
n3 != ssA(n3,n3) ).
cnf(u1291,axiom,
ssA(n1,n6) != ssA(n2,n5) ).
cnf(u823,axiom,
ssA(n7,n1) != ssA(n9,n1) ).
cnf(u1069,axiom,
ssA(n2,n6) != ssA(n8,n6) ).
cnf(u8756,axiom,
n6 != ssA(n4,n9) ).
cnf(u1867,axiom,
n1 != ssA(n3,n7) ).
cnf(u493,axiom,
ssA(n2,n1) != ssA(n2,n6) ).
cnf(u1048,axiom,
ssA(n7,n6) != ssA(n9,n6) ).
cnf(u790,axiom,
ssA(n9,n4) != ssA(n9,n6) ).
cnf(u424,axiom,
ssA(n1,n5) != ssA(n1,n8) ).
cnf(u1986,axiom,
n3 != ssA(n7,n1) ).
cnf(u1190,axiom,
ssA(n5,n9) != ssA(n7,n9) ).
cnf(u621,axiom,
ssA(n5,n2) != ssA(n5,n6) ).
cnf(u2008,axiom,
n4 != ssA(n9,n1) ).
cnf(u1945,axiom,
n3 != ssA(n5,n5) ).
cnf(u868,axiom,
ssA(n7,n2) != ssA(n9,n2) ).
cnf(u691,axiom,
ssA(n7,n6) != ssA(n7,n8) ).
cnf(u937,axiom,
ssA(n2,n3) != ssA(n5,n3) ).
cnf(u711,axiom,
ssA(n7,n2) != ssA(n7,n6) ).
cnf(u1154,axiom,
ssA(n3,n8) != ssA(n7,n8) ).
cnf(u1603,axiom,
ssA(n7,n9) != ssA(n9,n8) ).
cnf(u489,axiom,
ssA(n2,n2) != ssA(n2,n3) ).
cnf(u1054,axiom,
ssA(n5,n6) != ssA(n8,n6) ).
cnf(u436,axiom,
ssA(n1,n3) != ssA(n1,n5) ).
cnf(u617,axiom,
ssA(n5,n3) != ssA(n5,n4) ).
cnf(u1872,axiom,
n1 != ssA(n2,n7) ).
cnf(u1248,axiom,
ssA(n1,n2) != ssA(n3,n3) ).
cnf(u1711,axiom,
n6 = ssA(n4,n1) ).
cnf(u1171,axiom,
ssA(n1,n8) != ssA(n3,n8) ).
cnf(u606,axiom,
ssA(n5,n5) != ssA(n5,n6) ).
cnf(u1839,axiom,
n7 != ssA(n7,n5) ).
cnf(u5186,axiom,
n5 = ssA(n5,n1) ).
cnf(u703,axiom,
ssA(n7,n3) != ssA(n7,n8) ).
cnf(u707,axiom,
ssA(n7,n3) != ssA(n7,n4) ).
cnf(u1146,axiom,
ssA(n5,n8) != ssA(n6,n8) ).
cnf(u394,axiom,
n2 != n8 ).
cnf(u831,axiom,
ssA(n5,n1) != ssA(n6,n1) ).
cnf(u1077,axiom,
ssA(n1,n6) != ssA(n7,n6) ).
cnf(u1861,axiom,
n1 != ssA(n9,n7) ).
cnf(u432,axiom,
ssA(n1,n3) != ssA(n1,n9) ).
cnf(u6804,axiom,
n7 != ssA(n4,n2) ).
cnf(u1413,axiom,
ssA(n5,n5) != ssA(n6,n6) ).
cnf(u1340,axiom,
ssA(n1,n8) != ssA(n3,n7) ).
cnf(u1610,axiom,
ssA(n7,n8) != ssA(n9,n7) ).
cnf(u8628,axiom,
n6 != ssA(n3,n8) ).
cnf(u1953,axiom,
n3 != ssA(n1,n6) ).
cnf(u876,axiom,
ssA(n5,n2) != ssA(n6,n2) ).
cnf(u602,axiom,
ssA(n5,n6) != ssA(n5,n7) ).
cnf(u3883,axiom,
n3 = ssA(n4,n3) ).
cnf(u699,axiom,
ssA(n7,n4) != ssA(n7,n7) ).
cnf(u945,axiom,
ssA(n1,n3) != ssA(n4,n3) ).
cnf(u406,axiom,
n1 != n3 ).
cnf(u1164,axiom,
ssA(n2,n8) != ssA(n3,n8) ).
cnf(u827,axiom,
ssA(n6,n1) != ssA(n7,n1) ).
cnf(u1611,axiom,
ssA(n7,n8) != ssA(n8,n9) ).
cnf(u5188,axiom,
n5 != ssA(n7,n1) ).
cnf(u1143,axiom,
ssA(n5,n8) != ssA(n9,n8) ).
cnf(u1277,axiom,
ssA(n2,n6) != ssA(n3,n4) ).
cnf(u1858,axiom,
n1 != ssA(n4,n4) ).
cnf(u1062,axiom,
ssA(n3,n6) != ssA(n9,n6) ).
cnf(u1018,axiom,
ssA(n3,n5) != ssA(n8,n5) ).
cnf(u1850,axiom,
n8 != ssA(n3,n3) ).
cnf(u850,axiom,
ssA(n1,n1) != ssA(n9,n1) ).
cnf(u1817,axiom,
n2 != ssA(n4,n4) ).
cnf(u1719,axiom,
n1 = ssA(n8,n1) ).
cnf(u563,axiom,
ssA(n4,n4) != ssA(n4,n8) ).
cnf(u809,axiom,
ssA(n9,n1) != ssA(n9,n5) ).
cnf(u583,axiom,
ssA(n4,n1) != ssA(n4,n6) ).
cnf(u957,axiom,
ssA(n8,n4) != ssA(n9,n4) ).
cnf(u471,axiom,
ssA(n2,n5) != ssA(n2,n6) ).
cnf(u1026,axiom,
ssA(n2,n5) != ssA(n6,n5) ).
cnf(u1028,axiom,
ssA(n2,n5) != ssA(n4,n5) ).
cnf(u402,axiom,
n1 != n7 ).
cnf(u8170,axiom,
n8 != ssA(n7,n6) ).
cnf(u692,axiom,
ssA(n7,n6) != ssA(n7,n7) ).
cnf(u1988,axiom,
n3 != ssA(n1,n8) ).
cnf(u899,axiom,
ssA(n1,n2) != ssA(n5,n2) ).
cnf(u1604,axiom,
ssA(n7,n9) != ssA(n9,n7) ).
cnf(u1939,axiom,
n4 != ssA(n3,n3) ).
cnf(u17010,axiom,
n9 = ssA(n3,n5) ).
cnf(u1471,axiom,
ssA(n4,n9) != ssA(n5,n8) ).
cnf(u693,axiom,
ssA(n7,n5) != ssA(n7,n9) ).
cnf(u1595,axiom,
ssA(n8,n8) != ssA(n9,n7) ).
cnf(u2083,axiom,
n3 = ssA(n1,n9) ).
cnf(u467,axiom,
ssA(n2,n6) != ssA(n2,n7) ).
cnf(u1172,axiom,
ssA(n1,n8) != ssA(n2,n8) ).
cnf(u1789,axiom,
n7 != ssA(n1,n1) ).
cnf(u1507,axiom,
ssA(n8,n1) != ssA(n9,n3) ).
cnf(u688,axiom,
ssA(n7,n7) != ssA(n7,n9) ).
cnf(u1151,axiom,
ssA(n4,n8) != ssA(n5,n8) ).
cnf(u373,axiom,
n7 != n9 ).
cnf(u1157,axiom,
ssA(n3,n8) != ssA(n4,n8) ).
cnf(u508,axiom,
ssA(n3,n7) != ssA(n3,n9) ).
cnf(u1825,axiom,
n4 != ssA(n3,n4) ).
cnf(u689,axiom,
ssA(n7,n7) != ssA(n7,n8) ).
cnf(u1944,axiom,
n3 != ssA(n5,n7) ).
cnf(u571,axiom,
ssA(n4,n3) != ssA(n4,n5) ).
cnf(u479,axiom,
ssA(n2,n3) != ssA(n2,n7) ).
cnf(u1911,axiom,
n8 != ssA(n2,n8) ).
cnf(u1068,axiom,
ssA(n2,n6) != ssA(n9,n6) ).
cnf(u552,axiom,
ssA(n4,n8) != ssA(n4,n9) ).
cnf(u16945,axiom,
n7 != ssA(n7,n1) ).
cnf(u1718,axiom,
n3 = ssA(n7,n8) ).
cnf(u1996,axiom,
n1 != ssA(n2,n1) ).
cnf(u1149,axiom,
ssA(n4,n8) != ssA(n7,n8) ).
cnf(u1808,axiom,
n5 != ssA(n4,n2) ).
cnf(u870,axiom,
ssA(n6,n2) != ssA(n9,n2) ).
cnf(u1591,axiom,
ssA(n8,n9) != ssA(n9,n8) ).
cnf(u553,axiom,
ssA(n4,n7) != ssA(n4,n9) ).
cnf(u701,axiom,
ssA(n7,n4) != ssA(n7,n5) ).
cnf(u8924,axiom,
n9 != ssA(n1,n3) ).
cnf(u1113,axiom,
ssA(n2,n7) != ssA(n9,n7) ).
cnf(u1613,axiom,
ssA(n7,n8) != ssA(n8,n7) ).
cnf(u674,axiom,
ssA(n6,n1) != ssA(n6,n5) ).
cnf(u8172,axiom,
n8 != ssA(n4,n6) ).
cnf(u643,axiom,
ssA(n6,n7) != ssA(n6,n9) ).
cnf(u1017,axiom,
ssA(n3,n5) != ssA(n9,n5) ).
cnf(u8753,axiom,
n6 != ssA(n8,n9) ).
cnf(u1705,axiom,
n7 = ssA(n1,n5) ).
cnf(u388,axiom,
n3 != n8 ).
cnf(u1343,axiom,
ssA(n1,n8) != ssA(n2,n7) ).
cnf(u565,axiom,
ssA(n4,n4) != ssA(n4,n6) ).
cnf(u697,axiom,
ssA(n7,n4) != ssA(n7,n9) ).
cnf(u1952,axiom,
n3 != ssA(n3,n6) ).
cnf(u1568,axiom,
ssA(n7,n5) != ssA(n8,n4) ).
cnf(u944,axiom,
ssA(n1,n3) != ssA(n5,n3) ).
cnf(u1919,axiom,
n1 != ssA(n2,n9) ).
cnf(u655,axiom,
ssA(n6,n4) != ssA(n6,n6) ).
cnf(u1379,axiom,
ssA(n4,n3) != ssA(n6,n1) ).
cnf(u901,axiom,
ssA(n1,n2) != ssA(n3,n2) ).
cnf(u560,axiom,
ssA(n4,n5) != ssA(n4,n7) ).
cnf(u1098,axiom,
ssA(n5,n7) != ssA(n9,n7) ).
cnf(u474,axiom,
ssA(n2,n4) != ssA(n2,n7) ).
cnf(u783,axiom,
ssA(n9,n5) != ssA(n9,n9) ).
cnf(u1029,axiom,
ssA(n2,n5) != ssA(n3,n5) ).
cnf(u1941,axiom,
n4 != ssA(n4,n2) ).
cnf(u2110,axiom,
n5 = ssA(n1,n6) ).
cnf(u1520,axiom,
ssA(n7,n2) != ssA(n9,n1) ).
cnf(u1250,axiom,
ssA(n1,n2) != ssA(n3,n1) ).
cnf(u433,axiom,
ssA(n1,n3) != ssA(n1,n8) ).
cnf(u380,axiom,
n5 != n7 ).
cnf(u384,axiom,
n4 != n7 ).
cnf(u1597,axiom,
ssA(n8,n7) != ssA(n9,n9) ).
cnf(u733,axiom,
ssA(n8,n7) != ssA(n8,n9) ).
cnf(u561,axiom,
ssA(n4,n5) != ssA(n4,n6) ).
cnf(u17050,axiom,
n8 = ssA(n8,n5) ).
cnf(u1816,axiom,
n2 != ssA(n5,n4) ).
cnf(u1115,axiom,
ssA(n2,n7) != ssA(n7,n7) ).
cnf(u808,axiom,
ssA(n9,n1) != ssA(n9,n6) ).
cnf(u2118,axiom,
n5 != ssA(n4,n6) ).
cnf(u651,axiom,
ssA(n6,n5) != ssA(n6,n6) ).
cnf(u897,axiom,
ssA(n1,n2) != ssA(n7,n2) ).
cnf(u486,axiom,
ssA(n2,n2) != ssA(n2,n6) ).
cnf(u1244,axiom,
ssA(n1,n3) != ssA(n3,n1) ).
cnf(u779,axiom,
ssA(n9,n7) != ssA(n9,n8) ).
cnf(u760,axiom,
ssA(n8,n1) != ssA(n8,n9) ).
cnf(u1526,axiom,
ssA(n7,n1) != ssA(n9,n2) ).
cnf(u1095,axiom,
ssA(n6,n7) != ssA(n9,n7) ).
cnf(u1819,axiom,
n4 != ssA(n9,n4) ).
cnf(u445,axiom,
ssA(n1,n1) != ssA(n1,n9) ).
cnf(u6827,axiom,
n1 != ssA(n4,n2) ).
cnf(u376,axiom,
n6 != n8 ).
cnf(u1938,axiom,
n4 != ssA(n4,n3) ).
cnf(u1142,axiom,
ssA(n6,n8) != ssA(n7,n8) ).
cnf(u573,axiom,
ssA(n4,n2) != ssA(n4,n9) ).
cnf(u930,axiom,
ssA(n3,n3) != ssA(n6,n3) ).
cnf(u515,axiom,
ssA(n3,n5) != ssA(n3,n7) ).
cnf(u663,axiom,
ssA(n6,n2) != ssA(n6,n9) ).
cnf(u1106,axiom,
ssA(n4,n7) != ssA(n5,n7) ).
cnf(u482,axiom,
ssA(n2,n3) != ssA(n2,n4) ).
cnf(u1949,axiom,
n3 != ssA(n5,n1) ).
cnf(u1847,axiom,
n8 != ssA(n3,n6) ).
cnf(u644,axiom,
ssA(n6,n7) != ssA(n6,n8) ).
cnf(u441,axiom,
ssA(n1,n2) != ssA(n1,n6) ).
cnf(u2019,axiom,
n4 != ssA(n7,n7) ).
cnf(u7442,axiom,
n4 != ssA(n5,n5) ).
cnf(u942,axiom,
ssA(n1,n3) != ssA(n7,n3) ).
cnf(u1423,axiom,
ssA(n4,n6) != ssA(n6,n5) ).
cnf(u645,axiom,
ssA(n6,n6) != ssA(n6,n9) ).
cnf(u558,axiom,
ssA(n4,n5) != ssA(n4,n9) ).
cnf(u1982,axiom,
n3 != ssA(n7,n5) ).
cnf(u527,axiom,
ssA(n3,n3) != ssA(n3,n4) ).
cnf(u1598,axiom,
ssA(n8,n7) != ssA(n9,n8) ).
cnf(u494,axiom,
ssA(n2,n1) != ssA(n2,n5) ).
cnf(u1999,axiom,
n1 != ssA(n7,n2) ).
cnf(u17033,axiom,
n9 = ssA(n7,n1) ).
cnf(u1103,axiom,
ssA(n4,n7) != ssA(n8,n7) ).
cnf(u1237,axiom,
ssA(n2,n1) != ssA(n3,n3) ).
cnf(u1946,axiom,
n3 != ssA(n5,n4) ).
cnf(u1562,axiom,
ssA(n7,n6) != ssA(n8,n4) ).
cnf(u938,axiom,
ssA(n2,n3) != ssA(n4,n3) ).
cnf(u8626,axiom,
n6 != ssA(n5,n8) ).
cnf(u828,axiom,
ssA(n5,n1) != ssA(n9,n1) ).
cnf(u554,axiom,
ssA(n4,n7) != ssA(n4,n8) ).
cnf(u523,axiom,
ssA(n3,n3) != ssA(n3,n8) ).
cnf(u1116,axiom,
ssA(n2,n7) != ssA(n6,n7) ).
cnf(u758,axiom,
ssA(n8,n2) != ssA(n8,n4) ).
cnf(u1863,axiom,
n1 != ssA(n7,n7) ).
cnf(u1563,axiom,
ssA(n7,n5) != ssA(n9,n6) ).
cnf(u632,axiom,
ssA(n5,n1) != ssA(n5,n2) ).
cnf(u652,axiom,
ssA(n6,n4) != ssA(n6,n9) ).
cnf(u855,axiom,
ssA(n1,n1) != ssA(n4,n1) ).
cnf(u1101,axiom,
ssA(n5,n7) != ssA(n6,n7) ).
cnf(u1810,axiom,
n5 != ssA(n1,n2) ).
cnf(u6806,axiom,
n7 != ssA(n1,n2) ).
cnf(u802,axiom,
ssA(n9,n2) != ssA(n9,n5) ).
cnf(u1208,axiom,
ssA(n2,n9) != ssA(n4,n9) ).
cnf(u653,axiom,
ssA(n6,n4) != ssA(n6,n8) ).
cnf(u1862,axiom,
n1 != ssA(n8,n7) ).
cnf(u535,axiom,
ssA(n3,n1) != ssA(n3,n9) ).
cnf(u1193,axiom,
ssA(n4,n9) != ssA(n8,n9) ).
cnf(u781,axiom,
ssA(n9,n6) != ssA(n9,n8) ).
cnf(u423,axiom,
ssA(n1,n5) != ssA(n1,n9) ).
cnf(u900,axiom,
ssA(n1,n2) != ssA(n4,n2) ).
cnf(u754,axiom,
ssA(n8,n2) != ssA(n8,n8) ).
cnf(u1321,axiom,
ssA(n2,n9) != ssA(n3,n8) ).
cnf(u1821,axiom,
n4 != ssA(n7,n4) ).
cnf(u969,axiom,
ssA(n4,n4) != ssA(n7,n4) ).
cnf(u516,axiom,
ssA(n3,n5) != ssA(n3,n6) ).
cnf(u1435,axiom,
ssA(n4,n4) != ssA(n6,n6) ).
cnf(u1940,axiom,
n4 != ssA(n1,n3) ).
cnf(u851,axiom,
ssA(n1,n1) != ssA(n8,n1) ).
cnf(u1456,axiom,
ssA(n5,n9) != ssA(n6,n8) ).
cnf(u1891,axiom,
n5 != ssA(n1,n1) ).
cnf(u1072,axiom,
ssA(n2,n6) != ssA(n5,n6) ).
cnf(u1214,axiom,
ssA(n1,n9) != ssA(n5,n9) ).
cnf(u468,axiom,
ssA(n2,n5) != ssA(n2,n9) ).
cnf(u517,axiom,
ssA(n3,n4) != ssA(n3,n9) ).
cnf(u649,axiom,
ssA(n6,n5) != ssA(n6,n8) ).
cnf(u1854,axiom,
n6 != ssA(n4,n4) ).
cnf(u1508,axiom,
ssA(n8,n1) != ssA(n9,n2) ).
cnf(u419,axiom,
ssA(n1,n7) != ssA(n1,n8) ).
cnf(u896,axiom,
ssA(n1,n2) != ssA(n8,n2) ).
cnf(u766,axiom,
ssA(n8,n1) != ssA(n8,n3) ).
cnf(u735,axiom,
ssA(n8,n6) != ssA(n8,n9) ).
cnf(u512,axiom,
ssA(n3,n6) != ssA(n3,n7) ).
cnf(u1521,axiom,
ssA(n7,n2) != ssA(n8,n3) ).
cnf(u1109,axiom,
ssA(n3,n7) != ssA(n7,n7) ).
cnf(u2092,axiom,
n3 != ssA(n4,n9) ).
cnf(u1818,axiom,
n2 != ssA(n3,n4) ).
cnf(u1472,axiom,
ssA(n4,n9) != ssA(n5,n7) ).
cnf(u385,axiom,
n4 != n6 ).
cnf(u810,axiom,
ssA(n9,n1) != ssA(n9,n4) ).
cnf(u464,axiom,
ssA(n2,n7) != ssA(n2,n8) ).
cnf(u513,axiom,
ssA(n3,n5) != ssA(n3,n9) ).
cnf(u1896,axiom,
n7 != ssA(n3,n6) ).
cnf(u3973,axiom,
n5 = ssA(n4,n4) ).
cnf(u1372,axiom,
ssA(n5,n1) != ssA(n6,n3) ).
cnf(u1195,axiom,
ssA(n4,n9) != ssA(n6,n9) ).
cnf(u630,axiom,
ssA(n5,n1) != ssA(n5,n4) ).
cnf(u762,axiom,
ssA(n8,n1) != ssA(n8,n7) ).
cnf(u977,axiom,
ssA(n3,n4) != ssA(n4,n4) ).
cnf(u1948,axiom,
n3 != ssA(n5,n2) ).
cnf(u712,axiom,
ssA(n7,n2) != ssA(n7,n5) ).
cnf(u1478,axiom,
ssA(n4,n8) != ssA(n5,n7) ).
cnf(u1899,axiom,
n7 != ssA(n2,n6) ).
cnf(u397,axiom,
n2 != n5 ).
cnf(u1080,axiom,
ssA(n1,n6) != ssA(n4,n6) ).
cnf(u822,axiom,
ssA(n8,n1) != ssA(n9,n1) ).
cnf(u1094,axiom,
ssA(n7,n7) != ssA(n8,n7) ).
cnf(u525,axiom,
ssA(n3,n3) != ssA(n3,n6) ).
cnf(u1010,axiom,
ssA(n5,n5) != ssA(n7,n5) ).
cnf(u1065,axiom,
ssA(n3,n6) != ssA(n6,n6) ).
cnf(u1977,axiom,
n7 != ssA(n9,n6) ).
cnf(u1565,axiom,
ssA(n7,n5) != ssA(n9,n4) ).
cnf(u626,axiom,
ssA(n5,n1) != ssA(n5,n8) ).
cnf(u841,axiom,
ssA(n3,n1) != ssA(n5,n1) ).
cnf(u743,axiom,
ssA(n8,n4) != ssA(n8,n8) ).
cnf(u1812,axiom,
n2 != ssA(n9,n4) ).
cnf(u1186,axiom,
ssA(n6,n9) != ssA(n8,n9) ).
cnf(u1529,axiom,
ssA(n7,n1) != ssA(n8,n2) ).
cnf(u1328,axiom,
ssA(n2,n7) != ssA(n3,n8) ).
cnf(u393,axiom,
n2 != n9 ).
cnf(u7448,axiom,
n4 != ssA(n4,n6) ).
cnf(u521,axiom,
ssA(n3,n4) != ssA(n3,n5) ).
cnf(u1904,axiom,
n4 != ssA(n3,n5) ).
cnf(u1152,axiom,
ssA(n3,n8) != ssA(n9,n8) ).
cnf(u1022,axiom,
ssA(n3,n5) != ssA(n4,n5) ).
cnf(u1615,axiom,
ssA(n7,n7) != ssA(n9,n9) ).
cnf(u1503,axiom,
ssA(n8,n2) != ssA(n9,n3) ).
cnf(u1203,axiom,
ssA(n2,n9) != ssA(n9,n9) ).
cnf(u1934,axiom,
n4 != ssA(n5,n7) ).
cnf(u607,axiom,
ssA(n5,n4) != ssA(n5,n9) ).
cnf(u853,axiom,
ssA(n1,n1) != ssA(n6,n1) ).
cnf(u1957,axiom,
n5 != ssA(n6,n7) ).
cnf(u1050,axiom,
ssA(n6,n6) != ssA(n9,n6) ).
cnf(u426,axiom,
ssA(n1,n5) != ssA(n1,n6) ).
cnf(u1550,axiom,
ssA(n8,n5) != ssA(n9,n4) ).
cnf(u1893,axiom,
n2 != ssA(n3,n5) ).
cnf(u720,axiom,
ssA(n7,n1) != ssA(n7,n4) ).
cnf(u1183,axiom,
ssA(n7,n9) != ssA(n9,n9) ).
cnf(u405,axiom,
n1 != n4 ).
cnf(u1067,axiom,
ssA(n3,n6) != ssA(n4,n6) ).
cnf(u1857,axiom,
n1 != ssA(n4,n3) ).
cnf(u721,axiom,
ssA(n7,n1) != ssA(n7,n3) ).
cnf(u6824,axiom,
n1 != ssA(n8,n2) ).
cnf(u780,axiom,
ssA(n9,n6) != ssA(n9,n9) ).
cnf(u603,axiom,
ssA(n5,n5) != ssA(n5,n9) ).
cnf(u849,axiom,
ssA(n2,n1) != ssA(n3,n1) ).
cnf(u491,axiom,
ssA(n2,n1) != ssA(n2,n8) ).
cnf(u2006,axiom,
n4 != ssA(n9,n3) ).
cnf(u1720,axiom,
n4 = ssA(n9,n9) ).
cnf(u1820,axiom,
n4 != ssA(n8,n4) ).
cnf(u438,axiom,
ssA(n1,n2) != ssA(n1,n9) ).
cnf(u1196,axiom,
ssA(n4,n9) != ssA(n5,n9) ).
cnf(u710,axiom,
ssA(n7,n2) != ssA(n7,n7) ).
cnf(u1943,axiom,
n3 != ssA(n5,n8) ).
cnf(u1336,axiom,
ssA(n1,n9) != ssA(n2,n8) ).
cnf(u584,axiom,
ssA(n4,n1) != ssA(n4,n5) ).
cnf(u732,axiom,
ssA(n8,n8) != ssA(n8,n9) ).
cnf(u1047,axiom,
ssA(n8,n6) != ssA(n9,n6) ).
cnf(u935,axiom,
ssA(n2,n3) != ssA(n7,n3) ).
cnf(u1890,axiom,
n3 != ssA(n1,n1) ).
cnf(u882,axiom,
ssA(n3,n2) != ssA(n9,n2) ).
cnf(u1160,axiom,
ssA(n2,n8) != ssA(n7,n8) ).
cnf(u1849,axiom,
n8 != ssA(n3,n4) ).
cnf(u7441,axiom,
n4 != ssA(n7,n5) ).
cnf(u926,axiom,
ssA(n4,n3) != ssA(n5,n3) ).
cnf(u975,axiom,
ssA(n3,n4) != ssA(n6,n4) ).
cnf(u1807,axiom,
n5 != ssA(n5,n2) ).
cnf(u615,axiom,
ssA(n5,n3) != ssA(n5,n6) ).
cnf(u1058,axiom,
ssA(n4,n6) != ssA(n8,n6) ).
cnf(u1060,axiom,
ssA(n4,n6) != ssA(n6,n6) ).
cnf(u434,axiom,
ssA(n1,n3) != ssA(n1,n7) ).
cnf(u706,axiom,
ssA(n7,n3) != ssA(n7,n5) ).
cnf(u931,axiom,
ssA(n3,n3) != ssA(n5,n3) ).
cnf(u17395,axiom,
n2 != ssA(n9,n8) ).
cnf(u16991,axiom,
n9 = ssA(n1,n2) ).
cnf(u1971,axiom,
n5 != ssA(n5,n7) ).
cnf(u1024,axiom,
ssA(n2,n5) != ssA(n8,n5) ).
cnf(u14490,axiom,
n9 = ssA(n4,n6) ).
cnf(u1166,axiom,
ssA(n1,n8) != ssA(n8,n8) ).
cnf(u1075,axiom,
ssA(n1,n6) != ssA(n9,n6) ).
cnf(u597,axiom,
ssA(n5,n8) != ssA(n5,n9) ).
cnf(u1806,axiom,
n5 != ssA(n6,n2) ).
cnf(u1606,axiom,
ssA(n7,n9) != ssA(n8,n8) ).
cnf(u1561,axiom,
ssA(n7,n6) != ssA(n8,n5) ).
cnf(u446,axiom,
ssA(n1,n1) != ssA(n1,n8) ).
cnf(u976,axiom,
ssA(n3,n4) != ssA(n5,n4) ).
cnf(u1204,axiom,
ssA(n2,n9) != ssA(n8,n9) ).
cnf(u718,axiom,
ssA(n7,n1) != ssA(n7,n6) ).
cnf(u1951,axiom,
n3 != ssA(n4,n6) ).
cnf(u1411,axiom,
ssA(n5,n6) != ssA(n6,n5) ).
cnf(u1258,axiom,
ssA(n1,n1) != ssA(n2,n3) ).
cnf(u1055,axiom,
ssA(n5,n6) != ssA(n7,n6) ).
cnf(u943,axiom,
ssA(n1,n3) != ssA(n6,n3) ).
cnf(u1473,axiom,
ssA(n4,n8) != ssA(n6,n9) ).
cnf(u1189,axiom,
ssA(n5,n9) != ssA(n8,n9) ).
cnf(u1898,axiom,
n7 != ssA(n3,n4) ).
cnf(u465,axiom,
ssA(n2,n6) != ssA(n2,n9) ).
cnf(u1870,axiom,
n7 != ssA(n4,n4) ).
cnf(u1153,axiom,
ssA(n3,n8) != ssA(n8,n8) ).
cnf(u1592,axiom,
ssA(n8,n9) != ssA(n9,n7) ).
cnf(u840,axiom,
ssA(n3,n1) != ssA(n6,n1) ).
cnf(u1840,axiom,
n7 != ssA(n6,n5) ).
cnf(u582,axiom,
ssA(n4,n1) != ssA(n4,n7) ).
cnf(u714,axiom,
ssA(n7,n2) != ssA(n7,n3) ).
cnf(u807,axiom,
ssA(n9,n1) != ssA(n9,n7) ).
cnf(u1053,axiom,
ssA(n5,n6) != ssA(n9,n6) ).
cnf(u939,axiom,
ssA(n2,n3) != ssA(n3,n3) ).
cnf(u1593,axiom,
ssA(n8,n8) != ssA(n9,n9) ).
cnf(u1255,axiom,
ssA(n1,n1) != ssA(n3,n3) ).
cnf(u1979,axiom,
n7 != ssA(n8,n6) ).
cnf(u477,axiom,
ssA(n2,n3) != ssA(n2,n9) ).
cnf(u1383,axiom,
ssA(n4,n2) != ssA(n6,n3) ).
cnf(u605,axiom,
ssA(n5,n5) != ssA(n5,n7) ).
cnf(u1829,axiom,
n3 != ssA(n3,n5) ).
cnf(u1517,axiom,
ssA(n7,n3) != ssA(n8,n1) ).
cnf(u1714,axiom,
n4 = ssA(n5,n3) ).
cnf(u1992,axiom,
n1 != ssA(n7,n1) ).
cnf(u962,axiom,
ssA(n6,n4) != ssA(n7,n4) ).
cnf(u1145,axiom,
ssA(n5,n8) != ssA(n7,n8) ).
cnf(u375,axiom,
n6 != n9 ).
cnf(u1929,axiom,
n1 != ssA(n5,n4) ).
cnf(u852,axiom,
ssA(n1,n1) != ssA(n7,n1) ).
cnf(u578,axiom,
ssA(n4,n2) != ssA(n4,n4) ).
cnf(u675,axiom,
ssA(n6,n1) != ssA(n6,n4) ).
cnf(u921,axiom,
ssA(n5,n3) != ssA(n6,n3) ).
cnf(u1892,axiom,
n2 != ssA(n3,n6) ).
cnf(u803,axiom,
ssA(n9,n2) != ssA(n9,n4) ).
cnf(u1715,axiom,
n3 = ssA(n5,n6) ).
cnf(u1280,axiom,
ssA(n2,n5) != ssA(n3,n4) ).
cnf(u1843,axiom,
n7 != ssA(n3,n5) ).
cnf(u473,axiom,
ssA(n2,n4) != ssA(n2,n8) ).
cnf(u420,axiom,
ssA(n1,n6) != ssA(n1,n9) ).
cnf(u601,axiom,
ssA(n5,n6) != ssA(n5,n8) ).
cnf(u8778,axiom,
n8 != ssA(n8,n4) ).
cnf(u15293,axiom,
n4 = ssA(n8,n6) ).
cnf(u1232,axiom,
ssA(n2,n3) != ssA(n3,n1) ).
cnf(u1460,axiom,
ssA(n5,n8) != ssA(n6,n7) ).
cnf(u974,axiom,
ssA(n3,n4) != ssA(n7,n4) ).
cnf(u1155,axiom,
ssA(n3,n8) != ssA(n6,n8) ).
cnf(u848,axiom,
ssA(n2,n1) != ssA(n4,n1) ).
cnf(u1514,axiom,
ssA(n7,n3) != ssA(n9,n1) ).
cnf(u2014,axiom,
n4 != ssA(n2,n9) ).
cnf(u687,axiom,
ssA(n7,n8) != ssA(n7,n9) ).
cnf(u933,axiom,
ssA(n2,n3) != ssA(n9,n3) ).
cnf(u1061,axiom,
ssA(n4,n6) != ssA(n5,n6) ).
cnf(u1424,axiom,
ssA(n4,n6) != ssA(n6,n4) ).
cnf(u485,axiom,
ssA(n2,n2) != ssA(n2,n7) ).
cnf(u1848,axiom,
n8 != ssA(n3,n5) ).
cnf(u1525,axiom,
ssA(n7,n1) != ssA(n9,n3) ).
cnf(u6170,axiom,
n3 != ssA(n5,n9) ).
cnf(u970,axiom,
ssA(n4,n4) != ssA(n6,n4) ).
cnf(u1025,axiom,
ssA(n2,n5) != ssA(n7,n5) ).
cnf(u1147,axiom,
ssA(n4,n8) != ssA(n9,n8) ).
cnf(u1937,axiom,
n4 != ssA(n7,n3) ).
cnf(u586,axiom,
ssA(n4,n1) != ssA(n4,n3) ).
cnf(u929,axiom,
ssA(n3,n3) != ssA(n7,n3) ).
cnf(u390,axiom,
n3 != n6 ).
cnf(u1276,axiom,
ssA(n2,n6) != ssA(n3,n5) ).
cnf(u811,axiom,
ssA(n9,n1) != ssA(n9,n3) ).
cnf(u1288,axiom,
ssA(n1,n6) != ssA(n3,n5) ).
cnf(u664,axiom,
ssA(n6,n2) != ssA(n6,n8) ).
cnf(u6803,axiom,
n7 != ssA(n7,n2) ).
cnf(u1015,axiom,
ssA(n4,n5) != ssA(n6,n5) ).
cnf(u1970,axiom,
n5 != ssA(n5,n9) ).
cnf(u834,axiom,
ssA(n4,n1) != ssA(n7,n1) ).
cnf(u1801,axiom,
n5 != ssA(n2,n5) ).
cnf(u793,axiom,
ssA(n9,n3) != ssA(n9,n8) ).
cnf(u695,axiom,
ssA(n7,n5) != ssA(n7,n7) ).
cnf(u941,axiom,
ssA(n1,n3) != ssA(n8,n3) ).
cnf(u1138,axiom,
ssA(n7,n8) != ssA(n9,n8) ).
cnf(u1140,axiom,
ssA(n6,n8) != ssA(n9,n8) ).
cnf(u386,axiom,
n4 != n5 ).
cnf(u1981,axiom,
n3 != ssA(n7,n7) ).
cnf(u676,axiom,
ssA(n6,n1) != ssA(n6,n3) ).
cnf(u1011,axiom,
ssA(n5,n5) != ssA(n6,n5) ).
cnf(u3090,axiom,
n1 != ssA(n3,n3) ).
cnf(u1716,axiom,
n5 = ssA(n6,n8) ).
cnf(u1923,axiom,
n6 != ssA(n6,n2) ).
cnf(u1104,axiom,
ssA(n4,n7) != ssA(n7,n7) ).
cnf(u846,axiom,
ssA(n2,n1) != ssA(n6,n1) ).
cnf(u1027,axiom,
ssA(n2,n5) != ssA(n5,n5) ).
cnf(u677,axiom,
ssA(n6,n1) != ssA(n6,n2) ).
cnf(u1386,axiom,
ssA(n4,n2) != ssA(n5,n3) ).
cnf(u1865,axiom,
n1 != ssA(n5,n7) ).
cnf(u1886,axiom,
n3 != ssA(n2,n1) ).
cnf(u559,axiom,
ssA(n4,n5) != ssA(n4,n8) ).
cnf(u805,axiom,
ssA(n9,n1) != ssA(n9,n9) ).
cnf(u447,axiom,
ssA(n1,n1) != ssA(n1,n7) ).
cnf(u1717,axiom,
n7 = ssA(n7,n4) ).
cnf(u451,axiom,
ssA(n1,n1) != ssA(n1,n3) ).
cnf(u378,axiom,
n5 != n9 ).
cnf(u398,axiom,
n2 != n4 ).
cnf(u1156,axiom,
ssA(n3,n8) != ssA(n5,n8) ).
cnf(u540,axiom,
ssA(n3,n1) != ssA(n3,n4) ).
cnf(u672,axiom,
ssA(n6,n1) != ssA(n6,n7) ).
cnf(u1438,axiom,
ssA(n4,n4) != ssA(n5,n6) ).
cnf(u1023,axiom,
ssA(n2,n5) != ssA(n9,n5) ).
cnf(u842,axiom,
ssA(n3,n1) != ssA(n4,n1) ).
cnf(u492,axiom,
ssA(n2,n1) != ssA(n2,n7) ).
cnf(u1809,axiom,
n5 != ssA(n3,n2) ).
cnf(u673,axiom,
ssA(n6,n1) != ssA(n6,n6) ).
cnf(u555,axiom,
ssA(n4,n6) != ssA(n4,n9) ).
cnf(u801,axiom,
ssA(n9,n2) != ssA(n9,n6) ).
cnf(u443,axiom,
ssA(n1,n2) != ssA(n1,n4) ).
cnf(u463,axiom,
ssA(n2,n7) != ssA(n2,n9) ).
cnf(u1148,axiom,
ssA(n4,n8) != ssA(n8,n8) ).
cnf(u662,axiom,
ssA(n6,n3) != ssA(n6,n4) ).
cnf(u1895,axiom,
n2 != ssA(n1,n6) ).
cnf(u536,axiom,
ssA(n3,n1) != ssA(n3,n8) ).
cnf(u887,axiom,
ssA(n3,n2) != ssA(n4,n2) ).
cnf(u1019,axiom,
ssA(n3,n5) != ssA(n7,n5) ).
cnf(u1842,axiom,
n7 != ssA(n4,n5) ).
cnf(u12521,axiom,
n4 != ssA(n7,n1) ).
cnf(u1931,axiom,
n7 != ssA(n6,n8) ).
cnf(u1112,axiom,
ssA(n3,n7) != ssA(n4,n7) ).
cnf(u854,axiom,
ssA(n1,n1) != ssA(n5,n1) ).
cnf(u488,axiom,
ssA(n2,n2) != ssA(n2,n4) ).
cnf(u1463,axiom,
ssA(n5,n7) != ssA(n6,n8) ).
cnf(u567,axiom,
ssA(n4,n3) != ssA(n4,n9) ).
cnf(u1097,axiom,
ssA(n6,n7) != ssA(n7,n7) ).
cnf(u2009,axiom,
n4 != ssA(n8,n9) ).
cnf(u932,axiom,
ssA(n3,n3) != ssA(n4,n3) ).
cnf(u658,axiom,
ssA(n6,n3) != ssA(n6,n8) ).
cnf(u755,axiom,
ssA(n8,n2) != ssA(n8,n7) ).
cnf(u1972,axiom,
n5 != ssA(n4,n9) ).
cnf(u6164,axiom,
n3 != ssA(n8,n7) ).
cnf(u883,axiom,
ssA(n3,n2) != ssA(n8,n2) ).
cnf(u16943,axiom,
n7 = ssA(n2,n1) ).
cnf(u1795,axiom,
n1 != ssA(n1,n1) ).
cnf(u1118,axiom,
ssA(n2,n7) != ssA(n4,n7) ).
cnf(u1936,axiom,
n4 != ssA(n5,n1) ).
cnf(u1412,axiom,
ssA(n5,n6) != ssA(n6,n4) ).
cnf(u8754,axiom,
n6 != ssA(n7,n9) ).
cnf(u1552,axiom,
ssA(n8,n4) != ssA(n9,n6) ).
cnf(u928,axiom,
ssA(n3,n3) != ssA(n8,n3) ).
cnf(u670,axiom,
ssA(n6,n1) != ssA(n6,n9) ).
cnf(u1903,axiom,
n4 != ssA(n3,n6) ).
cnf(u767,axiom,
ssA(n8,n1) != ssA(n8,n2) ).
cnf(u1013,axiom,
ssA(n4,n5) != ssA(n8,n5) ).
cnf(u1210,axiom,
ssA(n1,n9) != ssA(n9,n9) ).
cnf(u1710,axiom,
n8 = ssA(n3,n9) ).
cnf(u1823,axiom,
n4 != ssA(n5,n4) ).
cnf(u13773,axiom,
n6 != ssA(n4,n6) ).
cnf(u895,axiom,
ssA(n1,n2) != ssA(n9,n2) ).
cnf(u1141,axiom,
ssA(n6,n8) != ssA(n8,n8) ).
cnf(u1925,axiom,
n6 != ssA(n5,n2) ).
cnf(u1553,axiom,
ssA(n8,n4) != ssA(n9,n5) ).
cnf(u417,axiom,
ssA(n1,n8) != ssA(n1,n9) ).
cnf(u496,axiom,
ssA(n2,n1) != ssA(n2,n3) ).
cnf(u1800,axiom,
n5 != ssA(n2,n4) ).
cnf(u1105,axiom,
ssA(n4,n7) != ssA(n6,n7) ).
cnf(u1099,axiom,
ssA(n5,n7) != ssA(n8,n7) ).
cnf(u2017,axiom,
n4 != ssA(n8,n7) ).
cnf(u792,axiom,
ssA(n9,n3) != ssA(n9,n9) ).
cnf(u1111,axiom,
ssA(n3,n7) != ssA(n5,n7) ).
cnf(u534,axiom,
ssA(n3,n2) != ssA(n3,n3) ).
cnf(u940,axiom,
ssA(n1,n3) != ssA(n9,n3) ).
cnf(u666,axiom,
ssA(n6,n2) != ssA(n6,n6) ).
cnf(u6650,axiom,
n4 != ssA(n1,n8) ).
cnf(u763,axiom,
ssA(n8,n1) != ssA(n8,n6) ).
cnf(u1009,axiom,
ssA(n5,n5) != ssA(n8,n5) ).
cnf(u12525,axiom,
n4 != ssA(n1,n2) ).
cnf(u470,axiom,
ssA(n2,n5) != ssA(n2,n7) ).
cnf(u1368,axiom,
ssA(n5,n2) != ssA(n6,n3) ).
cnf(u744,axiom,
ssA(n8,n4) != ssA(n8,n7) ).
cnf(u1207,axiom,
ssA(n2,n9) != ssA(n5,n9) ).
cnf(u1803,axiom,
n5 != ssA(n9,n2) ).
cnf(u429,axiom,
ssA(n1,n4) != ssA(n1,n7) ).
cnf(u1922,axiom,
n6 != ssA(n6,n3) ).
cnf(u557,axiom,
ssA(n4,n6) != ssA(n4,n7) ).
cnf(u1469,axiom,
ssA(n4,n9) != ssA(n6,n7) ).
cnf(u914,axiom,
ssA(n7,n3) != ssA(n8,n3) ).
cnf(u1881,axiom,
n3 != ssA(n2,n3) ).
cnf(u804,axiom,
ssA(n9,n2) != ssA(n9,n3) ).
cnf(u530,axiom,
ssA(n3,n2) != ssA(n3,n7) ).
cnf(u936,axiom,
ssA(n2,n3) != ssA(n6,n3) ).
cnf(u627,axiom,
ssA(n5,n1) != ssA(n5,n7) ).
cnf(u873,axiom,
ssA(n5,n2) != ssA(n9,n2) ).
cnf(u647,axiom,
ssA(n6,n6) != ssA(n6,n7) ).
cnf(u1021,axiom,
ssA(n3,n5) != ssA(n5,n5) ).
cnf(u1844,axiom,
n7 != ssA(n2,n5) ).
cnf(u466,axiom,
ssA(n2,n6) != ssA(n2,n8) ).
cnf(u1933,axiom,
n7 != ssA(n5,n8) ).
cnf(u756,axiom,
ssA(n8,n2) != ssA(n8,n6) ).
cnf(u425,axiom,
ssA(n1,n5) != ssA(n1,n7) ).
cnf(u963,axiom,
ssA(n5,n4) != ssA(n9,n4) ).
cnf(u372,axiom,
n8 != n9 ).
cnf(u2003,axiom,
n4 != ssA(n9,n6) ).
cnf(u1184,axiom,
ssA(n7,n9) != ssA(n8,n9) ).
cnf(u1845,axiom,
n8 != ssA(n3,n8) ).
cnf(u1107,axiom,
ssA(n3,n7) != ssA(n9,n7) ).
cnf(u757,axiom,
ssA(n8,n2) != ssA(n8,n5) ).
cnf(u800,axiom,
ssA(n9,n2) != ssA(n9,n7) ).
cnf(u542,axiom,
ssA(n3,n1) != ssA(n3,n2) ).
cnf(u1966,axiom,
n5 != ssA(n4,n8) ).
cnf(u5122,axiom,
n5 != ssA(n7,n7) ).
cnf(u885,axiom,
ssA(n3,n2) != ssA(n6,n2) ).
cnf(u399,axiom,
n2 != n3 ).
cnf(u1082,axiom,
ssA(n1,n6) != ssA(n2,n6) ).
cnf(u478,axiom,
ssA(n2,n3) != ssA(n2,n8) ).
cnf(u620,axiom,
ssA(n5,n2) != ssA(n5,n7) ).
cnf(u1830,axiom,
n3 != ssA(n3,n4) ).
cnf(u752,axiom,
ssA(n8,n3) != ssA(n8,n4) ).
cnf(u1518,axiom,
ssA(n7,n2) != ssA(n9,n3) ).
cnf(u1215,axiom,
ssA(n1,n9) != ssA(n4,n9) ).
cnf(u437,axiom,
ssA(n1,n3) != ssA(n1,n4) ).
cnf(u1930,axiom,
n7 != ssA(n6,n9) ).
cnf(u1546,axiom,
ssA(n8,n6) != ssA(n9,n5) ).
cnf(u922,axiom,
ssA(n4,n3) != ssA(n9,n3) ).
cnf(u6800,axiom,
n7 != ssA(n5,n4) ).
cnf(u753,axiom,
ssA(n8,n2) != ssA(n8,n9) ).
cnf(u812,axiom,
ssA(n9,n1) != ssA(n9,n2) ).
cnf(u538,axiom,
ssA(n3,n1) != ssA(n3,n6) ).
cnf(u881,axiom,
ssA(n4,n2) != ssA(n5,n2) ).
cnf(u395,axiom,
n2 != n7 ).
cnf(u1852,axiom,
n8 != ssA(n3,n1) ).
cnf(u1100,axiom,
ssA(n5,n7) != ssA(n7,n7) ).
cnf(u742,axiom,
ssA(n8,n4) != ssA(n8,n9) ).
cnf(u1547,axiom,
ssA(n8,n6) != ssA(n9,n4) ).
cnf(u572,axiom,
ssA(n4,n3) != ssA(n4,n4) ).
cnf(u616,axiom,
ssA(n5,n3) != ssA(n5,n5) ).
cnf(u1382,axiom,
ssA(n4,n3) != ssA(n5,n1) ).
cnf(u764,axiom,
ssA(n8,n1) != ssA(n8,n5) ).
cnf(u1079,axiom,
ssA(n1,n6) != ssA(n5,n6) ).
cnf(u839,axiom,
ssA(n3,n1) != ssA(n7,n1) ).
cnf(u1213,axiom,
ssA(n1,n9) != ssA(n6,n9) ).
cnf(u971,axiom,
ssA(n4,n4) != ssA(n5,n4) ).
cnf(u1341,axiom,
ssA(n1,n8) != ssA(n2,n9) ).
cnf(u2011,axiom,
n4 != ssA(n6,n9) ).
cnf(u786,axiom,
ssA(n9,n5) != ssA(n9,n6) ).
cnf(u1192,axiom,
ssA(n4,n9) != ssA(n9,n9) ).
cnf(u934,axiom,
ssA(n2,n3) != ssA(n8,n3) ).
cnf(u1415,axiom,
ssA(n5,n5) != ssA(n6,n4) ).
cnf(u765,axiom,
ssA(n8,n1) != ssA(n8,n4) ).
cnf(u7852,axiom,
n8 = ssA(n2,n6) ).
cnf(u519,axiom,
ssA(n3,n4) != ssA(n3,n7) ).
cnf(u407,axiom,
n1 != n2 ).
cnf(u1012,axiom,
ssA(n4,n5) != ssA(n9,n5) ).
cnf(u738,axiom,
ssA(n8,n5) != ssA(n8,n9) ).
cnf(u1991,axiom,
n1 != ssA(n8,n4) ).
cnf(u628,axiom,
ssA(n5,n1) != ssA(n5,n6) ).
cnf(u1924,axiom,
n6 != ssA(n5,n3) ).
cnf(u835,axiom,
ssA(n4,n1) != ssA(n6,n1) ).
cnf(u12518,axiom,
n4 = ssA(n3,n1) ).
cnf(u1875,axiom,
n8 != ssA(n7,n9) ).
cnf(u1056,axiom,
ssA(n5,n6) != ssA(n6,n6) ).
cnf(u798,axiom,
ssA(n9,n2) != ssA(n9,n9) ).
cnf(u452,axiom,
ssA(n1,n1) != ssA(n1,n2) ).
cnf(u629,axiom,
ssA(n5,n1) != ssA(n5,n5) ).
cnf(u761,axiom,
ssA(n8,n1) != ssA(n8,n8) ).
cnf(u1838,axiom,
n7 != ssA(n8,n5) ).
cnf(u403,axiom,
n1 != n6 ).
cnf(u1008,axiom,
ssA(n5,n5) != ssA(n9,n5) ).
cnf(u1108,axiom,
ssA(n3,n7) != ssA(n8,n7) ).
cnf(u750,axiom,
ssA(n8,n3) != ssA(n8,n6) ).
cnf(u719,axiom,
ssA(n7,n1) != ssA(n7,n5) ).
cnf(u965,axiom,
ssA(n5,n4) != ssA(n7,n4) ).
cnf(u624,axiom,
ssA(n5,n2) != ssA(n5,n3) ).
cnf(u1162,axiom,
ssA(n2,n8) != ssA(n5,n8) ).
cnf(u1790,axiom,
n7 != ssA(n1,n3) ).
cnf(u847,axiom,
ssA(n2,n1) != ssA(n5,n1) ).
cnf(u1505,axiom,
ssA(n8,n2) != ssA(n9,n1) ).
cnf(u1093,axiom,
ssA(n7,n7) != ssA(n9,n7) ).
cnf(u1802,axiom,
n5 != ssA(n2,n7) ).
cnf(u497,axiom,
ssA(n2,n1) != ssA(n2,n2) ).
cnf(u794,axiom,
ssA(n9,n3) != ssA(n9,n7) ).
cnf(u444,axiom,
ssA(n1,n2) != ssA(n1,n3) ).
cnf(u448,axiom,
ssA(n1,n1) != ssA(n1,n6) ).
cnf(u2016,axiom,
n4 != ssA(n8,n8) ).
cnf(u625,axiom,
ssA(n5,n1) != ssA(n5,n9) ).
cnf(u1880,axiom,
n8 != ssA(n1,n9) ).
cnf(u8624,axiom,
n6 != ssA(n2,n1) ).
cnf(u8919,axiom,
n9 != ssA(n7,n3) ).
cnf(u1185,axiom,
ssA(n6,n9) != ssA(n9,n9) ).
cnf(u872,axiom,
ssA(n6,n2) != ssA(n7,n2) ).
cnf(u614,axiom,
ssA(n5,n3) != ssA(n5,n7) ).
cnf(u1020,axiom,
ssA(n3,n5) != ssA(n6,n5) ).
cnf(u746,axiom,
ssA(n8,n4) != ssA(n8,n5) ).
cnf(u715,axiom,
ssA(n7,n1) != ssA(n7,n9) ).
cnf(u961,axiom,
ssA(n6,n4) != ssA(n8,n4) ).
cnf(u1932,axiom,
n7 != ssA(n5,n9) ).
cnf(u843,axiom,
ssA(n2,n1) != ssA(n9,n1) ).
cnf(u1159,axiom,
ssA(n2,n8) != ssA(n8,n8) ).
cnf(u509,axiom,
ssA(n3,n7) != ssA(n3,n8) ).
cnf(u1064,axiom,
ssA(n3,n6) != ssA(n7,n6) ).
cnf(u806,axiom,
ssA(n9,n1) != ssA(n9,n8) ).
cnf(u440,axiom,
ssA(n1,n2) != ssA(n1,n7) ).
cnf(u2002,axiom,
n4 != ssA(n9,n7) ).
cnf(u1206,axiom,
ssA(n2,n9) != ssA(n6,n9) ).
cnf(u1618,axiom,
ssA(n7,n7) != ssA(n8,n9) ).
cnf(u1846,axiom,
n8 != ssA(n3,n7) ).
cnf(u1049,axiom,
ssA(n7,n6) != ssA(n8,n6) ).
cnf(u884,axiom,
ssA(n3,n2) != ssA(n7,n2) ).
cnf(u610,axiom,
ssA(n5,n4) != ssA(n5,n6) ).
cnf(u1016,axiom,
ssA(n4,n5) != ssA(n5,n5) ).
cnf(u579,axiom,
ssA(n4,n2) != ssA(n4,n3) ).
cnf(u973,axiom,
ssA(n3,n4) != ssA(n8,n4) ).
cnf(u1170,axiom,
ssA(n1,n8) != ssA(n4,n8) ).
cnf(u1619,axiom,
ssA(n7,n7) != ssA(n8,n8) ).
cnf(u1513,axiom,
ssA(n7,n3) != ssA(n9,n2) ).
cnf(u2013,axiom,
n4 != ssA(n4,n9) ).
cnf(u708,axiom,
ssA(n7,n2) != ssA(n7,n9) ).
cnf(u1070,axiom,
ssA(n2,n6) != ssA(n7,n6) ).
cnf(u1888,axiom,
n5 != ssA(n1,n3) ).
cnf(u8189,axiom,
n4 = ssA(n4,n8) ).
cnf(u1006,axiom,
ssA(n6,n5) != ssA(n8,n5) ).
cnf(u1187,axiom,
ssA(n6,n9) != ssA(n7,n9) ).
cnf(u709,axiom,
ssA(n7,n2) != ssA(n7,n8) ).
cnf(u880,axiom,
ssA(n4,n2) != ssA(n6,n2) ).
cnf(u1418,axiom,
ssA(n5,n4) != ssA(n6,n5) ).
cnf(u622,axiom,
ssA(n5,n2) != ssA(n5,n5) ).
cnf(u837,axiom,
ssA(n3,n1) != ssA(n9,n1) ).
cnf(u1877,axiom,
n8 != ssA(n5,n9) ).
cnf(u700,axiom,
ssA(n7,n4) != ssA(n7,n6) ).
cnf(u704,axiom,
ssA(n7,n3) != ssA(n7,n7) ).
cnf(u1167,axiom,
ssA(n1,n8) != ssA(n7,n8) ).
cnf(u389,axiom,
n3 != n7 ).
cnf(u2010,axiom,
n4 != ssA(n7,n9) ).
cnf(u1002,axiom,
ssA(n8,n5) != ssA(n9,n5) ).
cnf(u1051,axiom,
ssA(n6,n6) != ssA(n8,n6) ).
cnf(u1969,axiom,
n5 != ssA(n1,n8) ).
cnf(u739,axiom,
ssA(n8,n5) != ssA(n8,n8) ).
cnf(u705,axiom,
ssA(n7,n3) != ssA(n7,n6) ).
cnf(u618,axiom,
ssA(n5,n2) != ssA(n5,n9) ).
cnf(u829,axiom,
ssA(n5,n1) != ssA(n8,n1) ).
cnf(u587,axiom,
ssA(n4,n1) != ssA(n4,n2) ).
cnf(u833,axiom,
ssA(n4,n1) != ssA(n8,n1) ).
cnf(u475,axiom,
ssA(n2,n4) != ssA(n2,n6) ).
cnf(u1704,axiom,
n4 = ssA(n1,n4) ).
cnf(u1804,axiom,
n5 != ssA(n8,n2) ).
cnf(u422,axiom,
ssA(n1,n6) != ssA(n1,n7) ).
cnf(u1927,axiom,
n1 != ssA(n6,n4) ).
cnf(u696,axiom,
ssA(n7,n5) != ssA(n7,n6) ).
cnf(u1462,axiom,
ssA(n5,n7) != ssA(n6,n9) ).
cnf(u716,axiom,
ssA(n7,n1) != ssA(n7,n8) ).
cnf(u381,axiom,
n5 != n6 ).
cnf(u919,axiom,
ssA(n5,n3) != ssA(n8,n3) ).
cnf(u1165,axiom,
ssA(n1,n8) != ssA(n9,n8) ).
cnf(u1874,axiom,
n8 != ssA(n8,n9) ).
cnf(u1078,axiom,
ssA(n1,n6) != ssA(n6,n6) ).
cnf(u16798,axiom,
n6 != ssA(n7,n3) ).
cnf(u1014,axiom,
ssA(n4,n5) != ssA(n7,n5) ).
cnf(u1833,axiom,
n3 != ssA(n7,n2) ).
cnf(u1607,axiom,
ssA(n7,n9) != ssA(n8,n7) ).
cnf(u717,axiom,
ssA(n7,n1) != ssA(n7,n7) ).
cnf(u1426,axiom,
ssA(n4,n6) != ssA(n5,n5) ).
cnf(u1926,axiom,
n1 != ssA(n6,n6) ).
cnf(u524,axiom,
ssA(n3,n3) != ssA(n3,n7) ).
cnf(u825,axiom,
ssA(n6,n1) != ssA(n9,n1) ).
cnf(u599,axiom,
ssA(n5,n7) != ssA(n5,n8) ).
cnf(u845,axiom,
ssA(n2,n1) != ssA(n7,n1) ).
cnf(u487,axiom,
ssA(n2,n2) != ssA(n2,n5) ).
cnf(u418,axiom,
ssA(n1,n7) != ssA(n1,n9) ).
cnf(u964,axiom,
ssA(n5,n4) != ssA(n8,n4) ).
cnf(u1385,axiom,
ssA(n4,n2) != ssA(n6,n1) ).
cnf(u1885,axiom,
n5 != ssA(n3,n1) ).
cnf(u580,axiom,
ssA(n4,n1) != ssA(n4,n9) ).
cnf(u2004,axiom,
n4 != ssA(n9,n5) ).
cnf(u377,axiom,
n6 != n7 ).
cnf(u915,axiom,
ssA(n6,n3) != ssA(n9,n3) ).
cnf(u878,axiom,
ssA(n4,n2) != ssA(n8,n2) ).
cnf(u1278,axiom,
ssA(n2,n5) != ssA(n3,n6) ).
cnf(u1059,axiom,
ssA(n4,n6) != ssA(n7,n6) ).
cnf(u581,axiom,
ssA(n4,n1) != ssA(n4,n8) ).
cnf(u713,axiom,
ssA(n7,n2) != ssA(n7,n4) ).
cnf(u1805,axiom,
n5 != ssA(n7,n2) ).
cnf(u8760,axiom,
n6 != ssA(n5,n7) ).
cnf(u483,axiom,
ssA(n2,n2) != ssA(n2,n9) ).
cnf(u1712,axiom,
n1 = ssA(n4,n5) ).
cnf(u430,axiom,
ssA(n1,n4) != ssA(n1,n6) ).
cnf(u960,axiom,
ssA(n6,n4) != ssA(n9,n4) ).
cnf(u1188,axiom,
ssA(n5,n9) != ssA(n9,n9) ).
cnf(u1523,axiom,
ssA(n7,n2) != ssA(n8,n1) ).
cnf(u576,axiom,
ssA(n4,n2) != ssA(n4,n6) ).
cnf(u8144,axiom,
n7 != ssA(n7,n6) ).
cnf(u927,axiom,
ssA(n3,n3) != ssA(n9,n3) ).
cnf(u6648,axiom,
n4 != ssA(n3,n8) ).
cnf(u1882,axiom,
n5 != ssA(n3,n3) ).
cnf(u1713,axiom,
n7 = ssA(n4,n7) ).
cnf(u449,axiom,
ssA(n1,n1) != ssA(n1,n5) ).
cnf(u874,axiom,
ssA(n5,n2) != ssA(n8,n2) ).
cnf(u396,axiom,
n2 != n6 ).
cnf(u1841,axiom,
n7 != ssA(n5,n5) ).
cnf(u577,axiom,
ssA(n4,n2) != ssA(n4,n5) ).
cnf(u1960,axiom,
n5 != ssA(n6,n3) ).
cnf(u1436,axiom,
ssA(n4,n4) != ssA(n6,n5) ).
cnf(u495,axiom,
ssA(n2,n1) != ssA(n2,n4) ).
cnf(u1052,axiom,
ssA(n6,n6) != ssA(n7,n6) ).
cnf(u694,axiom,
ssA(n7,n5) != ssA(n7,n8) ).
cnf(u972,axiom,
ssA(n3,n4) != ssA(n9,n4) ).
cnf(u1799,axiom,
n5 != ssA(n2,n3) ).
cnf(u568,axiom,
ssA(n4,n3) != ssA(n4,n8) ).
cnf(u1334,axiom,
ssA(n1,n9) != ssA(n3,n7) ).
cnf(u1824,axiom,
n4 != ssA(n4,n4) ).
cnf(u2012,axiom,
n4 != ssA(n5,n9) ).
cnf(u791,axiom,
ssA(n9,n4) != ssA(n9,n5) ).
cnf(u923,axiom,
ssA(n4,n3) != ssA(n8,n3) ).
cnf(u1528,axiom,
ssA(n7,n1) != ssA(n8,n3) ).
cnf(u1963,axiom,
n5 != ssA(n8,n8) ).
cnf(u1144,axiom,
ssA(n5,n8) != ssA(n8,n8) ).
cnf(u886,axiom,
ssA(n3,n2) != ssA(n5,n2) ).
cnf(u392,axiom,
n3 != n4 ).
cnf(u1158,axiom,
ssA(n2,n8) != ssA(n9,n8) ).
cnf(u569,axiom,
ssA(n4,n3) != ssA(n4,n7) ).
cnf(u1367,axiom,
ssA(n5,n3) != ssA(n6,n1) ).
cnf(u1501,axiom,
ssA(n8,n3) != ssA(n9,n2) ).
cnf(u1798,axiom,
n5 != ssA(n2,n1) ).
cnf(u1813,axiom,
n2 != ssA(n8,n4) ).
cnf(u836,axiom,
ssA(n4,n1) != ssA(n5,n1) ).
cnf(u690,axiom,
ssA(n7,n6) != ssA(n7,n9) ).
cnf(u968,axiom,
ssA(n4,n4) != ssA(n8,n4) ).
cnf(u659,axiom,
ssA(n6,n3) != ssA(n6,n7) ).
cnf(u481,axiom,
ssA(n2,n3) != ssA(n2,n5) ).
cnf(u1876,axiom,
n8 != ssA(n6,n9) ).
cnf(u787,axiom,
ssA(n9,n4) != ssA(n9,n9) ).
cnf(u8725,axiom,
n2 != ssA(n7,n1) ).
cnf(u1150,axiom,
ssA(n4,n8) != ssA(n6,n8) ).
cnf(u404,axiom,
n1 != n5 ).
cnf(u3093,axiom,
n1 != ssA(n1,n2) ).
cnf(u14368,axiom,
n2 != ssA(n7,n5) ).
cnf(u585,axiom,
ssA(n4,n1) != ssA(n4,n4) ).
cnf(u1968,axiom,
n5 != ssA(n2,n8) ).
cnf(u7440,axiom,
n4 != ssA(n8,n5) ).
cnf(u832,axiom,
ssA(n4,n1) != ssA(n9,n1) ).
cnf(u702,axiom,
ssA(n7,n3) != ssA(n7,n9) ).
cnf(u1998,axiom,
n1 != ssA(n7,n3) ).
cnf(u671,axiom,
ssA(n6,n1) != ssA(n6,n8) ).
cnf(u917,axiom,
ssA(n6,n3) != ssA(n7,n3) ).
cnf(u1114,axiom,
ssA(n2,n7) != ssA(n8,n7) ).
cnf(u490,axiom,
ssA(n2,n1) != ssA(n2,n9) ).
cnf(u799,axiom,
ssA(n9,n2) != ssA(n9,n8) ).
cnf(u1457,axiom,
ssA(n5,n9) != ssA(n6,n7) ).
cnf(u1247,axiom,
ssA(n1,n3) != ssA(n2,n1) ).
cnf(u469,axiom,
ssA(n2,n5) != ssA(n2,n8) ).
cnf(u400,axiom,
n1 != n9 ).
cnf(u1832,axiom,
n3 != ssA(n3,n1) ).
cnf(u782,axiom,
ssA(n9,n6) != ssA(n9,n7) ).
cnf(u1706,axiom,
n1 = ssA(n1,n7) ).
cnf(u1137,axiom,
ssA(n8,n8) != ssA(n9,n8) ).
cnf(u824,axiom,
ssA(n7,n1) != ssA(n8,n1) ).
cnf(u566,axiom,
ssA(n4,n4) != ssA(n4,n5) ).
cnf(u844,axiom,
ssA(n2,n1) != ssA(n8,n1) ).
cnf(u698,axiom,
ssA(n7,n4) != ssA(n7,n8) ).
cnf(u18075,axiom,
n9 = ssA(n9,n4) ).
cnf(u667,axiom,
ssA(n6,n2) != ssA(n6,n5) ).
cnf(u913,axiom,
ssA(n7,n3) != ssA(n9,n3) ).
cnf(u795,axiom,
ssA(n9,n3) != ssA(n9,n6) ).
cnf(u2007,axiom,
n4 != ssA(n9,n2) ).
cnf(u1707,axiom,
n5 = ssA(n2,n2) ).
cnf(u648,axiom,
ssA(n6,n5) != ssA(n6,n9) ).
cnf(u745,axiom,
ssA(n8,n4) != ssA(n8,n6) ).
cnf(u1835,axiom,
n3 != ssA(n1,n2) ).
cnf(u1954,axiom,
n3 != ssA(n4,n4) ).
cnf(u8922,axiom,
n9 != ssA(n3,n3) ).
cnf(u1373,axiom,
ssA(n5,n1) != ssA(n6,n2) ).
cnf(u946,axiom,
ssA(n1,n3) != ssA(n3,n3) ).
cnf(u966,axiom,
ssA(n5,n4) != ssA(n6,n4) ).
cnf(u562,axiom,
ssA(n4,n4) != ssA(n4,n9) ).
cnf(u531,axiom,
ssA(n3,n2) != ssA(n3,n6) ).
cnf(u777,axiom,
ssA(n9,n8) != ssA(n9,n9) ).
cnf(u925,axiom,
ssA(n4,n3) != ssA(n6,n3) ).
cnf(u8914,axiom,
n9 = ssA(n6,n3) ).
cnf(u1965,axiom,
n5 != ssA(n5,n8) ).
cnf(u660,axiom,
ssA(n6,n3) != ssA(n6,n6) ).
cnf(u12523,axiom,
n4 != ssA(n1,n1) ).
cnf(u522,axiom,
ssA(n3,n3) != ssA(n3,n9) ).
cnf(u958,axiom,
ssA(n7,n4) != ssA(n9,n4) ).
cnf(u1439,axiom,
ssA(n4,n4) != ssA(n5,n5) ).
cnf(u1139,axiom,
ssA(n7,n8) != ssA(n8,n8) ).
cnf(u661,axiom,
ssA(n6,n3) != ssA(n6,n5) ).
cnf(u1370,axiom,
ssA(n5,n2) != ssA(n6,n1) ).
cnf(u574,axiom,
ssA(n4,n2) != ssA(n4,n8) ).
cnf(u1548,axiom,
ssA(n8,n5) != ssA(n9,n6) ).
cnf(u789,axiom,
ssA(n9,n4) != ssA(n9,n7) ).
cnf(u431,axiom,
ssA(n1,n4) != ssA(n1,n5) ).
cnf(u510,axiom,
ssA(n3,n6) != ssA(n3,n9) ).
cnf(u2015,axiom,
n4 != ssA(n1,n9) ).
cnf(u3091,axiom,
n1 != ssA(n1,n3) ).
cnf(u1475,axiom,
ssA(n4,n8) != ssA(n6,n7) ).
cnf(u656,axiom,
ssA(n6,n4) != ssA(n6,n5) ).
cnf(u1119,axiom,
ssA(n2,n7) != ssA(n3,n7) ).
cnf(u1007,axiom,
ssA(n6,n5) != ssA(n7,n5) ).
cnf(u1253,axiom,
ssA(n1,n2) != ssA(n2,n1) ).
cnf(u1962,axiom,
n5 != ssA(n6,n1) ).
cnf(u1251,axiom,
ssA(n1,n2) != ssA(n2,n3) ).
cnf(u421,axiom,
ssA(n1,n6) != ssA(n1,n8) ).
cnf(u1381,axiom,
ssA(n4,n3) != ssA(n5,n2) ).
cnf(u476,axiom,
ssA(n2,n4) != ssA(n2,n5) ).
cnf(u657,axiom,
ssA(n6,n3) != ssA(n6,n9) ).
cnf(u570,axiom,
ssA(n4,n3) != ssA(n4,n6) ).
cnf(u1516,axiom,
ssA(n7,n3) != ssA(n8,n2) ).
cnf(u539,axiom,
ssA(n3,n1) != ssA(n3,n5) ).
cnf(u785,axiom,
ssA(n9,n5) != ssA(n9,n7) ).
cnf(u427,axiom,
ssA(n1,n4) != ssA(n1,n9) ).
cnf(u1217,axiom,
ssA(n1,n9) != ssA(n2,n9) ).
cnf(u374,axiom,
n7 != n8 ).
cnf(u646,axiom,
ssA(n6,n6) != ssA(n6,n8) ).
cnf(u1879,axiom,
n8 != ssA(n2,n9) ).
cnf(u520,axiom,
ssA(n3,n4) != ssA(n3,n6) ).
cnf(u668,axiom,
ssA(n6,n2) != ssA(n6,n4) ).
cnf(u871,axiom,
ssA(n6,n2) != ssA(n8,n2) ).
cnf(u1117,axiom,
ssA(n2,n7) != ssA(n5,n7) ).
cnf(u1003,axiom,
ssA(n7,n5) != ssA(n9,n5) ).
cnf(u1708,axiom,
n2 = ssA(n2,n4) ).
cnf(u1096,axiom,
ssA(n6,n7) != ssA(n8,n7) ).
cnf(u838,axiom,
ssA(n3,n1) != ssA(n8,n1) ).
cnf(u472,axiom,
ssA(n2,n4) != ssA(n2,n9) ).
cnf(u1559,axiom,
ssA(n7,n6) != ssA(n9,n4) ).
cnf(u5120,axiom,
n5 != ssA(n3,n4) ).
cnf(u669,axiom,
ssA(n6,n2) != ssA(n6,n3) ).
cnf(u16838,axiom,
n9 != ssA(n3,n8) ).
cnf(u1378,axiom,
ssA(n4,n3) != ssA(n6,n2) ).
cnf(u1878,axiom,
n8 != ssA(n4,n9) ).
cnf(u797,axiom,
ssA(n9,n3) != ssA(n9,n4) ).
cnf(u439,axiom,
ssA(n1,n2) != ssA(n1,n8) ).
cnf(u1993,axiom,
n1 != ssA(n5,n1) ).
cnf(u1709,axiom,
n3 = ssA(n3,n2) ).
cnf(u916,axiom,
ssA(n6,n3) != ssA(n8,n3) ).
cnf(u642,axiom,
ssA(n6,n8) != ssA(n6,n9) ).
cnf(u1337,axiom,
ssA(n1,n9) != ssA(n2,n7) ).
cnf(u1837,axiom,
n7 != ssA(n9,n5) ).
cnf(u532,axiom,
ssA(n3,n2) != ssA(n3,n5) ).
cnf(u1984,axiom,
n3 != ssA(n7,n3) ).
cnf(u867,axiom,
ssA(n8,n2) != ssA(n9,n2) ).
cnf(u1907,axiom,
n4 != ssA(n2,n5) ).
cnf(u830,axiom,
ssA(n5,n1) != ssA(n7,n1) ).
cnf(u1102,axiom,
ssA(n4,n7) != ssA(n9,n7) ).
cnf(u484,axiom,
ssA(n2,n2) != ssA(n2,n8) ).
cnf(u533,axiom,
ssA(n3,n2) != ssA(n3,n4) ).
cnf(u665,axiom,
ssA(n6,n2) != ssA(n6,n7) ).
cnf(u1920,axiom,
n1 != ssA(n2,n8) ).
cnf(u1073,axiom,
ssA(n2,n6) != ssA(n4,n6) ).
cnf(u435,axiom,
ssA(n1,n3) != ssA(n1,n6) ).
cnf(u382,axiom,
n4 != n9 ).
cnf(u912,axiom,
ssA(n8,n3) != ssA(n9,n3) ).
cnf(u654,axiom,
ssA(n6,n4) != ssA(n6,n7) ).
cnf(u1887,axiom,
n3 != ssA(n1,n3) ).
cnf(u751,axiom,
ssA(n8,n3) != ssA(n8,n5) ).
cnf(u528,axiom,
ssA(n3,n2) != ssA(n3,n9) ).
cnf(u1194,axiom,
ssA(n4,n9) != ssA(n7,n9) ).
cnf(u879,axiom,
ssA(n4,n2) != ssA(n7,n2) ).
cnf(u1834,axiom,
n3 != ssA(n4,n2) ).
cnf(u401,axiom,
n1 != n8 ).
cnf(u826,axiom,
ssA(n6,n1) != ssA(n8,n1) ).
cnf(u480,axiom,
ssA(n2,n3) != ssA(n2,n6) ).
cnf(u529,axiom,
ssA(n3,n2) != ssA(n3,n8) ).
cnf(u1912,axiom,
n8 != ssA(n2,n7) ).
cnf(u1388,axiom,
ssA(n4,n2) != ssA(n5,n1) ).
cnf(u1211,axiom,
ssA(n1,n9) != ssA(n8,n9) ).
cnf(u2001,axiom,
n4 != ssA(n9,n8) ).
cnf(u518,axiom,
ssA(n3,n4) != ssA(n3,n8) ).
cnf(u924,axiom,
ssA(n4,n3) != ssA(n7,n3) ).
cnf(u650,axiom,
ssA(n6,n5) != ssA(n6,n7) ).
cnf(u747,axiom,
ssA(n8,n3) != ssA(n8,n9) ).
cnf(u8146,axiom,
n7 != ssA(n4,n6) ).
cnf(u1558,axiom,
ssA(n7,n6) != ssA(n9,n5) ).
cnf(u1964,axiom,
n5 != ssA(n7,n8) ).
cnf(u875,axiom,
ssA(n5,n2) != ssA(n7,n2) ).
cnf(u14389,axiom,
n1 != ssA(n4,n6) ).
cnf(u8729,axiom,
n2 != ssA(n2,n1) ).
cnf(u1191,axiom,
ssA(n5,n9) != ssA(n6,n9) ).
cnf(u1110,axiom,
ssA(n3,n7) != ssA(n6,n7) ).
cnf(u541,axiom,
ssA(n3,n1) != ssA(n3,n3) ).
cnf(u1928,axiom,
n1 != ssA(n5,n6) ).
cnf(u898,axiom,
ssA(n1,n2) != ssA(n6,n2) ).
cnf(u1081,axiom,
ssA(n1,n6) != ssA(n3,n6) ).
cnf(u788,axiom,
ssA(n9,n4) != ssA(n9,n8) ).
cnf(u514,axiom,
ssA(n3,n5) != ssA(n3,n8) ).
cnf(u920,axiom,
ssA(n5,n3) != ssA(n7,n3) ).
cnf(u611,axiom,
ssA(n5,n4) != ssA(n5,n5) ).
cnf(u857,axiom,
ssA(n1,n1) != ssA(n2,n1) ).
cnf(u759,axiom,
ssA(n8,n2) != ssA(n8,n3) ).
cnf(u1005,axiom,
ssA(n6,n5) != ssA(n9,n5) ).
cnf(u1828,axiom,
n3 != ssA(n3,n7) ).
cnf(u450,axiom,
ssA(n1,n1) != ssA(n1,n4) ).
cnf(u1417,axiom,
ssA(n5,n4) != ssA(n6,n6) ).
cnf(u740,axiom,
ssA(n8,n5) != ssA(n8,n7) ).
cnf(u537,axiom,
ssA(n3,n1) != ssA(n3,n7) ).
cnf(u1792,axiom,
n7 != ssA(n1,n7) ).
cnf(u1168,axiom,
ssA(n1,n8) != ssA(n6,n8) ).
cnf(u1815,axiom,
n2 != ssA(n6,n4) ).
cnf(u741,axiom,
ssA(n8,n5) != ssA(n8,n6) ).
cnf(u784,axiom,
ssA(n9,n5) != ssA(n9,n8) ).
cnf(u526,axiom,
ssA(n3,n3) != ssA(n3,n5) ).
cnf(u1950,axiom,
n3 != ssA(n7,n6) ).
cnf(u623,axiom,
ssA(n5,n2) != ssA(n5,n4) ).
cnf(u869,axiom,
ssA(n7,n2) != ssA(n8,n2) ).
cnf(u511,axiom,
ssA(n3,n6) != ssA(n3,n8) ).
cnf(u1066,axiom,
ssA(n3,n6) != ssA(n5,n6) ).
cnf(u442,axiom,
ssA(n1,n2) != ssA(n1,n5) ).
cnf(u1566,axiom,
ssA(n7,n5) != ssA(n8,n6) ).
cnf(u462,axiom,
ssA(n2,n8) != ssA(n2,n9) ).
cnf(u604,axiom,
ssA(n5,n5) != ssA(n5,n8) ).
cnf(u736,axiom,
ssA(n8,n6) != ssA(n8,n8) ).
cnf(u1502,axiom,
ssA(n8,n3) != ssA(n9,n1) ).
cnf(u1814,axiom,
n2 != ssA(n7,n4) ).
cnf(u1873,axiom,
n8 != ssA(n9,n9) ).
cnf(u737,axiom,
ssA(n8,n6) != ssA(n8,n7) ).
cnf(u796,axiom,
ssA(n9,n3) != ssA(n9,n5) ).
cnf(u6163,axiom,
n3 != ssA(n6,n1) ).
cnf(u575,axiom,
ssA(n4,n2) != ssA(n4,n7) ).
cnf(u619,axiom,
ssA(n5,n2) != ssA(n5,n8) ).
cnf(u507,axiom,
ssA(n3,n8) != ssA(n3,n9) ).
cnf(u1608,axiom,
ssA(n7,n8) != ssA(n9,n9) ).
cnf(u1212,axiom,
ssA(n1,n9) != ssA(n7,n9) ).
cnf(u1959,axiom,
n5 != ssA(n6,n4) ).
cnf(u600,axiom,
ssA(n5,n6) != ssA(n5,n9) ).
cnf(u1366,axiom,
ssA(n5,n3) != ssA(n6,n2) ).
cnf(u748,axiom,
ssA(n8,n3) != ssA(n8,n8) ).
cnf(u1063,axiom,
ssA(n3,n6) != ssA(n8,n6) ).
cnf(u1906,axiom,
n4 != ssA(n2,n6) ).
cnf(u556,axiom,
ssA(n4,n6) != ssA(n4,n8) ).
cnf(u1325,axiom,
ssA(n2,n8) != ssA(n3,n7) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ067+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n016.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 22:43:32 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.42 Running first-order model finding
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.74/0.83 % (3061044)Will run a generic schedule for satisfiability detection.
% 1.74/0.83 % (3061053)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=485748207:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.74/0.83 % (3061050)% WARNING: option uhcvi not known.
% 1.74/0.83 % (3061049)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2834505306_2999 on theBenchmark for (2999ds/0Mi)
% 1.74/0.83 % (3061050)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1844102461:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.74/0.83 % (3061051)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1626408190:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.74/0.83 % (3061052)dis+10_1_sil=32000:sp=arity:random_seed=1899025727:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.74/0.83 % (3061054)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1436462863:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.74/0.83 % (3061055)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1646531537:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.74/0.83 % (3061053)Instruction limit reached!
% 1.74/0.83 % (3061053)------------------------------
% 1.74/0.83 % (3061053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.83 % (3061053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.83 % (3061053)CaDiCaL version: 2.1.3
% 1.74/0.83 % (3061053)Termination reason: Instruction limit
% 1.74/0.83 % (3061053)Termination phase: Saturation
% 1.74/0.83 % (3061053)Time elapsed: 0.028 s
% 1.74/0.83 % (3061053)Peak memory usage: 13 MB
% 1.74/0.83 % (3061053)Instructions burned: 117 (million)
% 1.74/0.83 % (3061063)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1541493540:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 1.74/0.83 % (3061052)Instruction limit reached!
% 1.74/0.83 % (3061052)------------------------------
% 1.74/0.83 % (3061052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.83 % (3061052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.83 % (3061052)CaDiCaL version: 2.1.3
% 1.74/0.83 % (3061052)Termination reason: Instruction limit
% 1.74/0.83 % (3061052)Termination phase: Saturation
% 1.74/0.83 % (3061052)Time elapsed: 0.046 s
% 1.74/0.83 % (3061052)Peak memory usage: 14 MB
% 1.74/0.83 % (3061052)Instructions burned: 103 (million)
% 1.74/0.83 % (3061054)Instruction limit reached!
% 1.74/0.83 % (3061054)------------------------------
% 1.74/0.83 % (3061054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.83 % (3061054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.83 % (3061054)CaDiCaL version: 2.1.3
% 1.74/0.83 % (3061054)Termination reason: Instruction limit
% 1.74/0.83 % (3061054)Termination phase: Saturation
% 1.74/0.83 % (3061054)Time elapsed: 0.052 s
% 1.74/0.83 % (3061054)Peak memory usage: 12 MB
% 1.74/0.83 % (3061054)Instructions burned: 131 (million)
% 1.74/0.83 % (3061065)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3343368257:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.74/0.83 % (3061066)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=1431800448:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.74/0.83 % (3061055)Instruction limit reached!
% 1.74/0.83 % (3061055)------------------------------
% 1.74/0.83 % (3061055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.83 % (3061055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.83 % (3061055)CaDiCaL version: 2.1.3
% 1.74/0.83 % (3061055)Termination reason: Instruction limit
% 1.74/0.83 % (3061055)Termination phase: Saturation
% 1.74/0.83 % (3061055)Time elapsed: 0.076 s
% 1.74/0.83 % (3061055)Peak memory usage: 15 MB
% 1.74/0.83 % (3061055)Instructions burned: 159 (million)
% 1.74/0.83 % (3061069)ott-21_1_sil=16000:fs=off:random_seed=3071611582:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.74/0.83 % Detected minimum model sizes of [9]
% 1.74/0.83 % Detected maximum model sizes of [max]
% 1.74/0.83 % TRYING [9]
% 1.74/0.83 % (3061065)Instruction limit reached!
% 1.74/0.83 % (3061065)------------------------------
% 1.74/0.83 % (3061065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.83 % (3061065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.83 % (3061065)CaDiCaL version: 2.1.3
% 1.74/0.83 % (3061065)Termination reason: Instruction limit
% 1.74/0.83 % (3061065)Termination phase: Saturation
% 1.74/0.83 % (3061065)Time elapsed: 0.057 s
% 1.74/0.83 % (3061065)Peak memory usage: 14 MB
% 1.74/0.83 % (3061065)Instructions burned: 133 (million)
% 1.74/0.83 % (3061071)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3368355952:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 1.74/0.83 % (3061069)Instruction limit reached!
% 1.74/0.83 % (3061069)------------------------------
% 1.74/0.83 % (3061069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.83 % (3061069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.83 % (3061069)CaDiCaL version: 2.1.3
% 1.74/0.83 % (3061069)Termination reason: Instruction limit
% 1.74/0.83 % (3061069)Termination phase: Saturation
% 1.74/0.83 % (3061069)Time elapsed: 0.075 s
% 1.74/0.83 % (3061069)Peak memory usage: 12 MB
% 1.74/0.83 % (3061069)Instructions burned: 182 (million)
% 1.74/0.83 % Detected minimum model sizes of [9]
% 1.74/0.83 % Detected maximum model sizes of [max]
% 1.74/0.83 % TRYING [9]
% 1.74/0.83 % (3061063)Instruction limit reached!
% 1.74/0.83 % (3061063)------------------------------
% 1.74/0.83 % (3061063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.83 % (3061063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.83 % (3061063)CaDiCaL version: 2.1.3
% 1.74/0.83 % (3061063)Termination reason: Instruction limit
% 1.74/0.83 % (3061063)Termination phase: Finite model building constraint generation
% 1.74/0.83 % (3061063)Time elapsed: 0.154 s
% 1.74/0.83 % (3061063)Peak memory usage: 41 MB
% 1.74/0.83 % (3061063)Instructions burned: 718 (million)
% 1.74/0.83 % (3061073)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1284739962:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 1.74/0.83 % (3061074)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=399741898:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 1.74/0.83 % (3061051) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3061044-3061051"...
% 1.74/0.83 % (3061051)...printing done.
% 1.74/0.83 % SZS status Satisfiable for theBenchmark
% 1.74/0.83 % SZS output start Saturation.
% See solution above
% 1.74/0.85 % SZS output start Definitions and Model Updates.
% 1.74/0.85 for all inputs,
% 1.74/0.85 define ssP(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56,X57,X58,X59,X60,X61,X62,X63,X64,X65,X66,X67,X68,X69,X70,X71,X72,X73,X74,X75,X76,X77,X78,X79,X80) := $true
% 1.74/0.85 % SZS output end Definitions and Model Updates.
% 1.74/0.85 % (3061051)------------------------------
% 1.74/0.85 % (3061051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.85 % (3061051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.85 % (3061051)CaDiCaL version: 2.1.3
% 1.74/0.85 % (3061051)Termination reason: Satisfiable
% 1.74/0.85 % (3061051)Time elapsed: 0.319 s
% 1.74/0.85 % (3061051)Peak memory usage: 17 MB
% 1.74/0.85 % (3061051)Instructions burned: 617 (million)
% 1.74/0.85 % (3061044)Success in time 0.407 s
% 1.74/0.85 % Vampire exiting
%------------------------------------------------------------------------------