%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PUZ069+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 : n012.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:09 PM UTC 2026
% Result : Satisfiable 1.18s 0.57s
% Output : Saturation 1.18s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u2044,axiom,
n2 != ssA(n1,n9) ).
cnf(u2049,axiom,
n2 = ssA(n1,n8) ).
cnf(u2052,axiom,
n2 != ssA(n1,n6) ).
cnf(u2056,axiom,
n2 != ssA(n1,n5) ).
cnf(u2131,axiom,
n4 != ssA(n1,n9) ).
cnf(u2135,axiom,
n4 != ssA(n1,n7) ).
cnf(u2139,axiom,
n4 != ssA(n1,n6) ).
cnf(u2144,axiom,
n4 = ssA(n1,n2) ).
cnf(u2204,axiom,
n8 != ssA(n1,n9) ).
cnf(u2209,axiom,
n8 = ssA(n1,n7) ).
cnf(u2283,axiom,
n1 = ssA(n2,n9) ).
cnf(u2286,axiom,
n1 != ssA(n2,n5) ).
cnf(u2290,axiom,
n1 != ssA(n2,n4) ).
cnf(u2329,axiom,
n2 != ssA(n2,n9) ).
cnf(u2333,axiom,
n2 != ssA(n2,n8) ).
cnf(u2338,axiom,
n2 = ssA(n2,n5) ).
cnf(u2382,axiom,
n3 != ssA(n2,n3) ).
cnf(u2387,axiom,
n3 = ssA(n2,n1) ).
cnf(u2417,axiom,
n4 != ssA(n2,n9) ).
cnf(u2421,axiom,
n4 != ssA(n2,n8) ).
cnf(u2425,axiom,
n4 != ssA(n2,n3) ).
cnf(u2429,axiom,
n4 != ssA(n2,n2) ).
cnf(u2562,axiom,
n6 != ssA(n2,n9) ).
cnf(u2567,axiom,
n6 = ssA(n2,n3) ).
cnf(u2614,axiom,
n7 != ssA(n2,n9) ).
cnf(u2619,axiom,
n7 = ssA(n2,n8) ).
cnf(u2733,axiom,
n5 = ssA(n1,n6) ).
cnf(u2736,axiom,
n5 != ssA(n1,n2) ).
cnf(u2784,axiom,
n1 != ssA(n3,n9) ).
cnf(u2788,axiom,
n1 != ssA(n3,n8) ).
cnf(u2792,axiom,
n1 != ssA(n3,n6) ).
cnf(u2796,axiom,
n1 != ssA(n3,n5) ).
cnf(u2801,axiom,
n1 = ssA(n3,n4) ).
cnf(u2982,axiom,
n4 != ssA(n3,n9) ).
cnf(u2987,axiom,
n4 = ssA(n3,n8) ).
cnf(u2990,axiom,
n4 != ssA(n3,n6) ).
cnf(u2994,axiom,
n4 != ssA(n3,n3) ).
cnf(u2998,axiom,
n4 != ssA(n3,n1) ).
cnf(u3272,axiom,
n5 != ssA(n3,n6) ).
cnf(u3276,axiom,
n5 != ssA(n3,n3) ).
cnf(u3444,axiom,
n6 = ssA(n3,n9) ).
cnf(u3447,axiom,
n6 != ssA(n3,n3) ).
cnf(u3745,axiom,
n7 != ssA(n3,n8) ).
cnf(u3749,axiom,
n7 != ssA(n3,n6) ).
cnf(u3779,axiom,
n6 != ssA(n2,n2) ).
cnf(u3783,axiom,
n6 != ssA(n2,n1) ).
cnf(u3885,axiom,
n5 != ssA(n3,n4) ).
cnf(u3890,axiom,
n5 = ssA(n3,n1) ).
cnf(u4278,axiom,
n8 = ssA(n3,n3) ).
cnf(u4281,axiom,
n8 != ssA(n3,n1) ).
cnf(u4371,axiom,
n1 != ssA(n4,n9) ).
cnf(u4375,axiom,
n1 != ssA(n4,n8) ).
cnf(u4379,axiom,
n1 != ssA(n4,n7) ).
cnf(u4383,axiom,
n1 != ssA(n4,n6) ).
cnf(u4388,axiom,
n1 = ssA(n4,n3) ).
cnf(u4391,axiom,
n1 != ssA(n4,n2) ).
cnf(u4429,axiom,
n3 != ssA(n4,n9) ).
cnf(u4434,axiom,
n3 = ssA(n4,n8) ).
cnf(u4437,axiom,
n3 != ssA(n4,n7) ).
cnf(u4441,axiom,
n3 != ssA(n4,n3) ).
cnf(u4445,axiom,
n3 != ssA(n4,n1) ).
cnf(u4486,axiom,
n5 = ssA(n4,n9) ).
cnf(u4489,axiom,
n5 != ssA(n4,n8) ).
cnf(u4493,axiom,
n5 != ssA(n4,n3) ).
cnf(u4531,axiom,
n6 = ssA(n4,n6) ).
cnf(u4534,axiom,
n6 != ssA(n4,n3) ).
cnf(u4569,axiom,
n7 != ssA(n4,n8) ).
cnf(u4573,axiom,
n7 != ssA(n4,n7) ).
cnf(u4684,axiom,
n8 != ssA(n4,n8) ).
cnf(u4688,axiom,
n8 != ssA(n4,n3) ).
cnf(u4776,axiom,
n1 != ssA(n5,n9) ).
cnf(u4780,axiom,
n1 != ssA(n5,n7) ).
cnf(u4784,axiom,
n1 != ssA(n5,n6) ).
cnf(u4789,axiom,
n1 = ssA(n5,n5) ).
cnf(u4792,axiom,
n1 != ssA(n5,n4) ).
cnf(u4796,axiom,
n1 != ssA(n5,n3) ).
cnf(u4800,axiom,
n1 != ssA(n5,n2) ).
cnf(u4861,axiom,
n2 = ssA(n5,n9) ).
cnf(u4864,axiom,
n2 != ssA(n5,n4) ).
cnf(u4868,axiom,
n2 != ssA(n5,n3) ).
cnf(u4872,axiom,
n2 != ssA(n5,n2) ).
cnf(u4991,axiom,
n4 != ssA(n5,n5) ).
cnf(u4995,axiom,
n4 != ssA(n5,n2) ).
cnf(u5104,axiom,
n3 != ssA(n5,n9) ).
cnf(u5108,axiom,
n3 != ssA(n5,n7) ).
cnf(u5808,axiom,
n7 != ssA(n5,n5) ).
cnf(u5812,axiom,
n7 != ssA(n5,n4) ).
cnf(u5885,axiom,
n1 != ssA(n6,n9) ).
cnf(u5889,axiom,
n1 != ssA(n6,n8) ).
cnf(u5894,axiom,
n1 = ssA(n6,n7) ).
cnf(u5897,axiom,
n1 != ssA(n6,n4) ).
cnf(u5901,axiom,
n1 != ssA(n6,n3) ).
cnf(u5905,axiom,
n1 != ssA(n6,n2) ).
cnf(u6193,axiom,
n9 != ssA(n4,n9) ).
cnf(u6197,axiom,
n9 != ssA(n4,n6) ).
cnf(u6321,axiom,
n2 != ssA(n6,n9) ).
cnf(u6325,axiom,
n2 != ssA(n6,n8) ).
cnf(u6329,axiom,
n2 != ssA(n6,n4) ).
cnf(u6334,axiom,
n2 = ssA(n6,n3) ).
cnf(u6337,axiom,
n2 != ssA(n6,n2) ).
cnf(u6341,axiom,
n2 != ssA(n6,n1) ).
cnf(u6501,axiom,
n4 != ssA(n6,n8) ).
cnf(u6505,axiom,
n4 != ssA(n6,n3) ).
cnf(u6509,axiom,
n4 != ssA(n6,n2) ).
cnf(u6514,axiom,
n4 = ssA(n6,n1) ).
cnf(u6569,axiom,
n6 != ssA(n6,n8) ).
cnf(u6573,axiom,
n6 != ssA(n6,n3) ).
cnf(u6578,axiom,
n6 = ssA(n6,n2) ).
cnf(u6660,axiom,
n7 != ssA(n6,n8) ).
cnf(u6664,axiom,
n7 != ssA(n6,n4) ).
cnf(u7066,axiom,
n8 = ssA(n6,n8) ).
cnf(u7069,axiom,
n8 != ssA(n6,n4) ).
cnf(u7205,axiom,
n6 != ssA(n6,n1) ).
cnf(u7336,axiom,
n9 != ssA(n2,n4) ).
cnf(u7341,axiom,
n9 = ssA(n2,n2) ).
cnf(u7857,axiom,
n4 != ssA(n6,n9) ).
cnf(u7861,axiom,
n4 != ssA(n6,n7) ).
cnf(u7945,axiom,
n7 != ssA(n6,n7) ).
cnf(u7949,axiom,
n7 != ssA(n6,n1) ).
cnf(u8632,axiom,
n5 != ssA(n4,n2) ).
cnf(u8636,axiom,
n5 != ssA(n4,n1) ).
cnf(u10040,axiom,
n7 = ssA(n6,n9) ).
cnf(u10043,axiom,
n7 != ssA(n6,n2) ).
cnf(u10247,axiom,
n8 != ssA(n4,n2) ).
cnf(u10252,axiom,
n8 = ssA(n4,n1) ).
cnf(u10555,axiom,
n9 != ssA(n6,n9) ).
cnf(u10560,axiom,
n9 = ssA(n6,n4) ).
cnf(u10709,axiom,
n2 != ssA(n7,n6) ).
cnf(u10713,axiom,
n2 != ssA(n7,n5) ).
cnf(u10718,axiom,
n2 = ssA(n7,n1) ).
cnf(u11109,axiom,
n3 = ssA(n7,n9) ).
cnf(u11112,axiom,
n3 != ssA(n7,n5) ).
cnf(u12897,axiom,
n2 != ssA(n7,n3) ).
cnf(u12956,axiom,
n8 != ssA(n3,n8) ).
cnf(u13889,axiom,
n7 = ssA(n3,n5) ).
cnf(u13892,axiom,
n7 != ssA(n3,n4) ).
cnf(u14293,axiom,
n4 != ssA(n7,n3) ).
cnf(u14297,axiom,
n4 != ssA(n7,n2) ).
cnf(u14343,axiom,
n6 = ssA(n7,n7) ).
cnf(u14346,axiom,
n6 != ssA(n7,n5) ).
cnf(u14474,axiom,
n8 != ssA(n7,n5) ).
cnf(u14478,axiom,
n8 != ssA(n7,n3) ).
cnf(u14730,axiom,
n8 != ssA(n7,n7) ).
cnf(u14735,axiom,
n8 = ssA(n7,n2) ).
cnf(u14814,axiom,
n1 != ssA(n8,n9) ).
cnf(u14818,axiom,
n1 != ssA(n8,n8) ).
cnf(u14823,axiom,
n1 = ssA(n8,n6) ).
cnf(u14826,axiom,
n1 != ssA(n8,n5) ).
cnf(u14830,axiom,
n1 != ssA(n8,n4) ).
cnf(u14834,axiom,
n1 != ssA(n8,n3) ).
cnf(u14926,axiom,
n4 != ssA(n8,n9) ).
cnf(u14930,axiom,
n4 != ssA(n8,n8) ).
cnf(u14934,axiom,
n4 != ssA(n8,n6) ).
cnf(u14938,axiom,
n4 != ssA(n8,n5) ).
cnf(u14942,axiom,
n4 != ssA(n8,n4) ).
cnf(u14946,axiom,
n4 != ssA(n8,n1) ).
cnf(u15050,axiom,
n5 != ssA(n8,n8) ).
cnf(u15054,axiom,
n5 != ssA(n8,n6) ).
cnf(u15058,axiom,
n5 != ssA(n8,n5) ).
cnf(u15063,axiom,
n5 = ssA(n8,n4) ).
cnf(u15066,axiom,
n5 != ssA(n8,n1) ).
cnf(u15111,axiom,
n6 != ssA(n8,n6) ).
cnf(u15116,axiom,
n6 = ssA(n8,n5) ).
cnf(u15119,axiom,
n6 != ssA(n8,n1) ).
cnf(u15183,axiom,
n7 != ssA(n8,n6) ).
cnf(u15187,axiom,
n7 != ssA(n8,n4) ).
cnf(u15192,axiom,
n7 = ssA(n8,n1) ).
cnf(u15330,axiom,
n6 != ssA(n8,n9) ).
cnf(u15383,axiom,
n7 != ssA(n8,n9) ).
cnf(u15387,axiom,
n7 != ssA(n8,n5) ).
cnf(u16465,axiom,
n5 != ssA(n8,n9) ).
cnf(u16469,axiom,
n5 != ssA(n8,n3) ).
cnf(u17429,axiom,
n9 != ssA(n7,n3) ).
cnf(u17433,axiom,
n9 != ssA(n7,n2) ).
cnf(u17999,axiom,
n9 != ssA(n7,n6) ).
cnf(u18004,axiom,
n9 = ssA(n7,n5) ).
cnf(u18100,axiom,
n8 != ssA(n8,n8) ).
cnf(u18104,axiom,
n8 != ssA(n8,n3) ).
cnf(u18274,axiom,
n1 != ssA(n9,n9) ).
cnf(u18278,axiom,
n1 != ssA(n9,n8) ).
cnf(u18282,axiom,
n1 != ssA(n9,n7) ).
cnf(u18286,axiom,
n1 != ssA(n9,n6) ).
cnf(u18290,axiom,
n1 != ssA(n9,n5) ).
cnf(u18294,axiom,
n1 != ssA(n9,n4) ).
cnf(u18298,axiom,
n1 != ssA(n9,n3) ).
cnf(u18303,axiom,
n1 = ssA(n9,n2) ).
cnf(u18419,axiom,
n2 != ssA(n9,n9) ).
cnf(u18423,axiom,
n2 != ssA(n9,n8) ).
cnf(u18427,axiom,
n2 != ssA(n9,n7) ).
cnf(u18432,axiom,
n2 = ssA(n9,n6) ).
cnf(u18435,axiom,
n2 != ssA(n9,n5) ).
cnf(u18439,axiom,
n2 != ssA(n9,n4) ).
cnf(u18443,axiom,
n2 != ssA(n9,n3) ).
cnf(u18447,axiom,
n2 != ssA(n9,n1) ).
cnf(u18650,axiom,
n3 != ssA(n9,n9) ).
cnf(u18654,axiom,
n3 != ssA(n9,n8) ).
cnf(u18658,axiom,
n3 != ssA(n9,n7) ).
cnf(u18662,axiom,
n3 != ssA(n9,n5) ).
cnf(u18667,axiom,
n3 = ssA(n9,n4) ).
cnf(u18670,axiom,
n3 != ssA(n9,n3) ).
cnf(u18674,axiom,
n3 != ssA(n9,n1) ).
cnf(u18960,axiom,
n4 = ssA(n9,n9) ).
cnf(u18963,axiom,
n4 != ssA(n9,n8) ).
cnf(u18967,axiom,
n4 != ssA(n9,n7) ).
cnf(u18971,axiom,
n4 != ssA(n9,n5) ).
cnf(u18975,axiom,
n4 != ssA(n9,n3) ).
cnf(u18979,axiom,
n4 != ssA(n9,n1) ).
cnf(u19297,axiom,
n5 = ssA(n9,n8) ).
cnf(u19300,axiom,
n5 != ssA(n9,n5) ).
cnf(u19304,axiom,
n5 != ssA(n9,n3) ).
cnf(u19308,axiom,
n5 != ssA(n9,n1) ).
cnf(u19462,axiom,
n6 != ssA(n9,n7) ).
cnf(u19475,axiom,
n6 = ssA(n9,n1) ).
cnf(u19538,axiom,
n7 = ssA(n9,n7) ).
cnf(u19541,axiom,
n7 != ssA(n9,n5) ).
cnf(u19587,axiom,
n8 = ssA(n9,n5) ).
cnf(u19590,axiom,
n8 != ssA(n9,n3) ).
cnf(u1995,axiom,
n7 != ssA(n2,n4) ).
cnf(u918,axiom,
ssA(n5,n3) != ssA(n9,n3) ).
cnf(u749,axiom,
ssA(n8,n3) != ssA(n8,n7) ).
cnf(u1958,axiom,
n5 != ssA(n5,n6) ).
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(u1789,axiom,
n1 != ssA(n1,n9) ).
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(u612,axiom,
ssA(n5,n3) != ssA(n5,n9) ).
cnf(u17125,axiom,
n4 = ssA(n2,n4) ).
cnf(u967,axiom,
ssA(n4,n4) != ssA(n9,n4) ).
cnf(u1859,axiom,
n2 != ssA(n2,n1) ).
cnf(u782,axiom,
ssA(n9,n6) != ssA(n9,n7) ).
cnf(u1182,axiom,
ssA(n8,n9) != ssA(n9,n9) ).
cnf(u1391,axiom,
ssA(n4,n1) != ssA(n6,n2) ).
cnf(u613,axiom,
ssA(n5,n3) != ssA(n5,n8) ).
cnf(u760,axiom,
ssA(n8,n1) != ssA(n8,n9) ).
cnf(u745,axiom,
ssA(n8,n4) != ssA(n8,n6) ).
cnf(u1822,axiom,
n7 != ssA(n9,n3) ).
cnf(u1476,axiom,
ssA(n4,n8) != ssA(n5,n9) ).
cnf(u383,axiom,
n4 != n8 ).
cnf(u387,axiom,
n3 != n9 ).
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(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(u959,axiom,
ssA(n7,n4) != ssA(n8,n4) ).
cnf(u1205,axiom,
ssA(n2,n9) != ssA(n7,n9) ).
cnf(u1333,axiom,
ssA(n1,n9) != ssA(n3,n8) ).
cnf(u481,axiom,
ssA(n2,n3) != ssA(n2,n5) ).
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(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(u598,axiom,
ssA(n5,n7) != ssA(n5,n9) ).
cnf(u1004,axiom,
ssA(n7,n5) != ssA(n8,n5) ).
cnf(u16880,axiom,
n9 != ssA(n5,n4) ).
cnf(u1831,axiom,
n6 != ssA(n8,n4) ).
cnf(u1291,axiom,
ssA(n1,n6) != ssA(n2,n5) ).
cnf(u823,axiom,
ssA(n7,n1) != ssA(n9,n1) ).
cnf(u12550,axiom,
n6 != ssA(n1,n9) ).
cnf(u17985,axiom,
n5 = ssA(n7,n3) ).
cnf(u1867,axiom,
n3 != ssA(n1,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(n5,n4) ).
cnf(u1190,axiom,
ssA(n5,n9) != ssA(n7,n9) ).
cnf(u621,axiom,
ssA(n5,n2) != ssA(n5,n6) ).
cnf(u1830,axiom,
n6 != ssA(n9,n4) ).
cnf(u978,axiom,
ssA(n2,n4) != ssA(n9,n4) ).
cnf(u1033,axiom,
ssA(n1,n5) != ssA(n6,n5) ).
cnf(u1945,axiom,
n5 != ssA(n6,n4) ).
cnf(u12592,axiom,
n6 != ssA(n4,n2) ).
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(u1908,axiom,
n8 != ssA(n3,n4) ).
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(u1248,axiom,
ssA(n1,n2) != ssA(n3,n3) ).
cnf(u1348,axiom,
ssA(n1,n7) != ssA(n2,n9) ).
cnf(u1711,axiom,
n2 = ssA(n4,n4) ).
cnf(u1171,axiom,
ssA(n1,n8) != ssA(n3,n8) ).
cnf(u18235,axiom,
n9 = ssA(n8,n8) ).
cnf(u606,axiom,
ssA(n5,n5) != ssA(n5,n6) ).
cnf(u1839,axiom,
n2 != ssA(n2,n2) ).
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(u1077,axiom,
ssA(n1,n6) != ssA(n7,n6) ).
cnf(u19777,axiom,
n9 = ssA(n9,n3) ).
cnf(u432,axiom,
ssA(n1,n3) != ssA(n1,n9) ).
cnf(u1994,axiom,
n7 != ssA(n7,n1) ).
cnf(u1413,axiom,
ssA(n5,n5) != ssA(n6,n6) ).
cnf(u1610,axiom,
ssA(n7,n8) != ssA(n9,n7) ).
cnf(u1035,axiom,
ssA(n1,n5) != ssA(n4,n5) ).
cnf(u1096,axiom,
ssA(n6,n7) != ssA(n8,n7) ).
cnf(u876,axiom,
ssA(n5,n2) != ssA(n6,n2) ).
cnf(u602,axiom,
ssA(n5,n6) != ssA(n5,n7) ).
cnf(u699,axiom,
ssA(n7,n4) != ssA(n7,n7) ).
cnf(u1916,axiom,
n6 != ssA(n2,n5) ).
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(u1143,axiom,
ssA(n5,n8) != ssA(n9,n8) ).
cnf(u1858,axiom,
n2 != ssA(n2,n3) ).
cnf(u1062,axiom,
ssA(n3,n6) != ssA(n9,n6) ).
cnf(u1817,axiom,
n1 != ssA(n3,n1) ).
cnf(u1719,axiom,
n3 = ssA(n8,n2) ).
cnf(u563,axiom,
ssA(n4,n4) != ssA(n4,n8) ).
cnf(u14665,axiom,
n8 != ssA(n1,n2) ).
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(u1869,axiom,
n3 != ssA(n7,n7) ).
cnf(u692,axiom,
ssA(n7,n6) != ssA(n7,n7) ).
cnf(u899,axiom,
ssA(n1,n2) != ssA(n5,n2) ).
cnf(u18041,axiom,
n4 = ssA(n7,n6) ).
cnf(u1604,axiom,
ssA(n7,n9) != ssA(n9,n7) ).
cnf(u1939,axiom,
n3 != ssA(n1,n8) ).
cnf(u801,axiom,
ssA(n9,n2) != ssA(n9,n6) ).
cnf(u1120,axiom,
ssA(n1,n7) != ssA(n9,n7) ).
cnf(u1075,axiom,
ssA(n1,n6) != ssA(n9,n6) ).
cnf(u693,axiom,
ssA(n7,n5) != ssA(n7,n9) ).
cnf(u16884,axiom,
n9 != ssA(n5,n6) ).
cnf(u1902,axiom,
n9 != ssA(n3,n1) ).
cnf(u575,axiom,
ssA(n4,n2) != ssA(n4,n7) ).
cnf(u17177,axiom,
n4 != ssA(n3,n4) ).
cnf(u467,axiom,
ssA(n2,n6) != ssA(n2,n7) ).
cnf(u1172,axiom,
ssA(n1,n8) != ssA(n2,n8) ).
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(u1866,axiom,
n7 != ssA(n2,n1) ).
cnf(u18905,axiom,
n2 != ssA(n9,n2) ).
cnf(u508,axiom,
ssA(n3,n7) != ssA(n3,n9) ).
cnf(u1825,axiom,
n7 != ssA(n6,n3) ).
cnf(u689,axiom,
ssA(n7,n7) != ssA(n7,n8) ).
cnf(u571,axiom,
ssA(n4,n3) != ssA(n4,n5) ).
cnf(u479,axiom,
ssA(n2,n3) != ssA(n2,n7) ).
cnf(u1036,axiom,
ssA(n1,n5) != ssA(n3,n5) ).
cnf(u1911,axiom,
n6 != ssA(n3,n6) ).
cnf(u552,axiom,
ssA(n4,n8) != ssA(n4,n9) ).
cnf(u1718,axiom,
n1 = ssA(n7,n8) ).
cnf(u1149,axiom,
ssA(n4,n8) != ssA(n7,n8) ).
cnf(u1288,axiom,
ssA(n1,n6) != ssA(n3,n5) ).
cnf(u17936,axiom,
n7 = ssA(n5,n6) ).
cnf(u1808,axiom,
n8 != ssA(n2,n3) ).
cnf(u1947,axiom,
n5 != ssA(n6,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(u2016,axiom,
n3 != ssA(n1,n2) ).
cnf(u1282,axiom,
ssA(n2,n4) != ssA(n3,n6) ).
cnf(u1155,axiom,
ssA(n3,n8) != ssA(n6,n8) ).
cnf(u1910,axiom,
n8 != ssA(n1,n5) ).
cnf(u1613,axiom,
ssA(n7,n8) != ssA(n8,n7) ).
cnf(u674,axiom,
ssA(n6,n1) != ssA(n6,n5) ).
cnf(u643,axiom,
ssA(n6,n7) != ssA(n6,n9) ).
cnf(u1017,axiom,
ssA(n3,n5) != ssA(n9,n5) ).
cnf(u564,axiom,
ssA(n4,n4) != ssA(n4,n7) ).
cnf(u12547,axiom,
n6 != ssA(n3,n1) ).
cnf(u1811,axiom,
n1 != ssA(n9,n1) ).
cnf(u1705,axiom,
n7 = ssA(n1,n3) ).
cnf(u388,axiom,
n3 != n8 ).
cnf(u11080,axiom,
n3 = ssA(n5,n3) ).
cnf(u565,axiom,
ssA(n4,n4) != ssA(n4,n6) ).
cnf(u697,axiom,
ssA(n7,n4) != ssA(n7,n9) ).
cnf(u1952,axiom,
n5 != ssA(n3,n5) ).
cnf(u1791,axiom,
n1 != ssA(n1,n7) ).
cnf(u1568,axiom,
ssA(n7,n5) != ssA(n8,n4) ).
cnf(u17961,axiom,
n8 = ssA(n5,n4) ).
cnf(u1919,axiom,
n3 != ssA(n2,n8) ).
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(u1520,axiom,
ssA(n7,n2) != ssA(n9,n1) ).
cnf(u433,axiom,
ssA(n1,n3) != ssA(n1,n8) ).
cnf(u380,axiom,
n5 != n7 ).
cnf(u384,axiom,
n4 != n7 ).
cnf(u561,axiom,
ssA(n4,n5) != ssA(n4,n6) ).
cnf(u1816,axiom,
n1 != ssA(n4,n1) ).
cnf(u1121,axiom,
ssA(n1,n7) != ssA(n8,n7) ).
cnf(u808,axiom,
ssA(n9,n1) != ssA(n9,n6) ).
cnf(u1805,axiom,
n8 != ssA(n2,n7) ).
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(u18059,axiom,
n9 = ssA(n3,n6) ).
cnf(u779,axiom,
ssA(n9,n7) != ssA(n9,n8) ).
cnf(u1526,axiom,
ssA(n7,n1) != ssA(n9,n2) ).
cnf(u1095,axiom,
ssA(n6,n7) != ssA(n9,n7) ).
cnf(u376,axiom,
n6 != n8 ).
cnf(u1938,axiom,
n5 != ssA(n1,n9) ).
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(u1897,axiom,
n4 != ssA(n2,n5) ).
cnf(u11086,axiom,
n3 != ssA(n3,n3) ).
cnf(u515,axiom,
ssA(n3,n5) != ssA(n3,n7) ).
cnf(u889,axiom,
ssA(n2,n2) != ssA(n8,n2) ).
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,
n5 != ssA(n7,n5) ).
cnf(u1847,axiom,
n8 != ssA(n4,n6) ).
cnf(u644,axiom,
ssA(n6,n7) != ssA(n6,n8) ).
cnf(u979,axiom,
ssA(n2,n4) != ssA(n8,n4) ).
cnf(u16258,axiom,
n5 != ssA(n2,n3) ).
cnf(u1824,axiom,
n7 != ssA(n7,n3) ).
cnf(u1200,axiom,
ssA(n3,n9) != ssA(n6,n9) ).
cnf(u1123,axiom,
ssA(n1,n7) != ssA(n6,n7) ).
cnf(u645,axiom,
ssA(n6,n6) != ssA(n6,n9) ).
cnf(u558,axiom,
ssA(n4,n5) != ssA(n4,n9) ).
cnf(u1982,axiom,
n3 != ssA(n4,n6) ).
cnf(u527,axiom,
ssA(n3,n3) != ssA(n3,n4) ).
cnf(u1846,axiom,
n8 != ssA(n5,n6) ).
cnf(u1598,axiom,
ssA(n8,n7) != ssA(n9,n8) ).
cnf(u494,axiom,
ssA(n2,n1) != ssA(n2,n5) ).
cnf(u1999,axiom,
n1 != ssA(n7,n6) ).
cnf(u1103,axiom,
ssA(n4,n7) != ssA(n8,n7) ).
cnf(u1237,axiom,
ssA(n2,n1) != ssA(n3,n3) ).
cnf(u1548,axiom,
ssA(n8,n5) != ssA(n9,n6) ).
cnf(u1946,axiom,
n5 != ssA(n6,n3) ).
cnf(u1562,axiom,
ssA(n7,n6) != ssA(n8,n4) ).
cnf(u938,axiom,
ssA(n2,n3) != ssA(n4,n3) ).
cnf(u1235,axiom,
ssA(n2,n2) != ssA(n3,n1) ).
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(u758,axiom,
ssA(n8,n2) != ssA(n8,n4) ).
cnf(u1863,axiom,
n7 != ssA(n3,n1) ).
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(u1101,axiom,
ssA(n5,n7) != ssA(n6,n7) ).
cnf(u1810,axiom,
n8 != ssA(n2,n1) ).
cnf(u2027,axiom,
n2 != ssA(n1,n7) ).
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(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,
n5 != ssA(n2,n2) ).
cnf(u969,axiom,
ssA(n4,n4) != ssA(n7,n4) ).
cnf(u516,axiom,
ssA(n3,n5) != ssA(n3,n6) ).
cnf(u1940,axiom,
n5 != ssA(n1,n8) ).
cnf(u1456,axiom,
ssA(n5,n9) != ssA(n6,n8) ).
cnf(u1214,axiom,
ssA(n1,n9) != ssA(n5,n9) ).
cnf(u468,axiom,
ssA(n2,n5) != ssA(n2,n9) ).
cnf(u1295,axiom,
ssA(n1,n5) != ssA(n3,n4) ).
cnf(u517,axiom,
ssA(n3,n4) != ssA(n3,n9) ).
cnf(u649,axiom,
ssA(n6,n5) != ssA(n6,n8) ).
cnf(u1854,axiom,
n5 != ssA(n5,n7) ).
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(u981,axiom,
ssA(n2,n4) != ssA(n6,n4) ).
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(n1,n5) ).
cnf(u2021,axiom,
n2 != ssA(n8,n1) ).
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,
n4 != ssA(n3,n5) ).
cnf(u1201,axiom,
ssA(n3,n9) != ssA(n5,n9) ).
cnf(u1195,axiom,
ssA(n4,n9) != ssA(n6,n9) ).
cnf(u1985,axiom,
n3 != ssA(n5,n5) ).
cnf(u888,axiom,
ssA(n2,n2) != ssA(n9,n2) ).
cnf(u630,axiom,
ssA(n5,n1) != ssA(n5,n4) ).
cnf(u762,axiom,
ssA(n8,n1) != ssA(n8,n7) ).
cnf(u1323,axiom,
ssA(n2,n8) != ssA(n3,n9) ).
cnf(u977,axiom,
ssA(n3,n4) != ssA(n4,n4) ).
cnf(u1948,axiom,
n5 != ssA(n6,n1) ).
cnf(u712,axiom,
ssA(n7,n2) != ssA(n7,n5) ).
cnf(u1478,axiom,
ssA(n4,n8) != ssA(n5,n7) ).
cnf(u397,axiom,
n2 != n5 ).
cnf(u1080,axiom,
ssA(n1,n6) != ssA(n4,n6) ).
cnf(u822,axiom,
ssA(n8,n1) != ssA(n9,n1) ).
cnf(u2018,axiom,
n3 != ssA(n7,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,
n3 != ssA(n6,n3) ).
cnf(u1565,axiom,
ssA(n7,n5) != ssA(n9,n4) ).
cnf(u473,axiom,
ssA(n2,n4) != ssA(n2,n8) ).
cnf(u626,axiom,
ssA(n5,n1) != ssA(n5,n8) ).
cnf(u11166,axiom,
n5 = ssA(n5,n2) ).
cnf(u841,axiom,
ssA(n3,n1) != ssA(n5,n1) ).
cnf(u743,axiom,
ssA(n8,n4) != ssA(n8,n8) ).
cnf(u1812,axiom,
n1 != ssA(n8,n1) ).
cnf(u1186,axiom,
ssA(n6,n9) != ssA(n8,n9) ).
cnf(u1529,axiom,
ssA(n7,n1) != ssA(n8,n2) ).
cnf(u393,axiom,
n2 != n9 ).
cnf(u521,axiom,
ssA(n3,n4) != ssA(n3,n5) ).
cnf(u1904,axiom,
n9 != ssA(n7,n1) ).
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(u607,axiom,
ssA(n5,n4) != ssA(n5,n9) ).
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(u1393,axiom,
ssA(n4,n1) != ssA(n5,n3) ).
cnf(u1893,axiom,
n4 != ssA(n4,n2) ).
cnf(u720,axiom,
ssA(n7,n1) != ssA(n7,n4) ).
cnf(u1183,axiom,
ssA(n7,n9) != ssA(n9,n9) ).
cnf(u405,axiom,
n1 != n4 ).
cnf(u755,axiom,
ssA(n8,n2) != ssA(n8,n7) ).
cnf(u1018,axiom,
ssA(n3,n5) != ssA(n8,n5) ).
cnf(u1067,axiom,
ssA(n3,n6) != ssA(n4,n6) ).
cnf(u1857,axiom,
n5 != ssA(n1,n7) ).
cnf(u721,axiom,
ssA(n7,n1) != ssA(n7,n3) ).
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(u1720,axiom,
n2 = ssA(n8,n7) ).
cnf(u1820,axiom,
n5 != ssA(n2,n1) ).
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,
n9 != ssA(n6,n2) ).
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,
n4 != ssA(n4,n7) ).
cnf(u18165,axiom,
n4 = ssA(n8,n3) ).
cnf(u12839,axiom,
n9 = ssA(n4,n7) ).
cnf(u882,axiom,
ssA(n3,n2) != ssA(n9,n2) ).
cnf(u1160,axiom,
ssA(n2,n8) != ssA(n7,n8) ).
cnf(u11168,axiom,
n5 != ssA(n7,n2) ).
cnf(u902,axiom,
ssA(n1,n2) != ssA(n2,n2) ).
cnf(u1849,axiom,
n8 != ssA(n1,n6) ).
cnf(u733,axiom,
ssA(n8,n7) != ssA(n8,n9) ).
cnf(u1807,axiom,
n8 != ssA(n2,n4) ).
cnf(u12156,axiom,
n4 != ssA(n7,n7) ).
cnf(u1942,axiom,
n9 != ssA(n6,n3) ).
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(u980,axiom,
ssA(n2,n4) != ssA(n7,n4) ).
cnf(u706,axiom,
ssA(n7,n3) != ssA(n7,n5) ).
cnf(u1901,axiom,
n9 != ssA(n2,n1) ).
cnf(u931,axiom,
ssA(n3,n3) != ssA(n5,n3) ).
cnf(u1971,axiom,
n6 != ssA(n6,n7) ).
cnf(u1024,axiom,
ssA(n2,n5) != ssA(n8,n5) ).
cnf(u894,axiom,
ssA(n2,n2) != ssA(n3,n2) ).
cnf(u1166,axiom,
ssA(n1,n8) != ssA(n8,n8) ).
cnf(u597,axiom,
ssA(n5,n8) != ssA(n5,n9) ).
cnf(u9973,axiom,
n7 != ssA(n1,n9) ).
cnf(u1806,axiom,
n8 != ssA(n2,n5) ).
cnf(u1523,axiom,
ssA(n7,n2) != ssA(n8,n1) ).
cnf(u1561,axiom,
ssA(n7,n6) != ssA(n8,n5) ).
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(u1055,axiom,
ssA(n5,n6) != ssA(n7,n6) ).
cnf(u12083,axiom,
n5 != ssA(n2,n9) ).
cnf(u1473,axiom,
ssA(n4,n8) != ssA(n6,n9) ).
cnf(u1189,axiom,
ssA(n5,n9) != ssA(n8,n9) ).
cnf(u1898,axiom,
n4 != ssA(n1,n5) ).
cnf(u465,axiom,
ssA(n2,n6) != ssA(n2,n9) ).
cnf(u890,axiom,
ssA(n2,n2) != ssA(n7,n2) ).
cnf(u1818,axiom,
n1 != ssA(n2,n1) ).
cnf(u1976,axiom,
n3 != ssA(n6,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(u582,axiom,
ssA(n4,n1) != ssA(n4,n7) ).
cnf(u714,axiom,
ssA(n7,n2) != ssA(n7,n3) ).
cnf(u1993,axiom,
n7 != ssA(n7,n2) ).
cnf(u2028,axiom,
n2 != ssA(n7,n9) ).
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(u1979,axiom,
n3 != ssA(n6,n1) ).
cnf(u477,axiom,
ssA(n2,n3) != ssA(n2,n9) ).
cnf(u1032,axiom,
ssA(n1,n5) != ssA(n7,n5) ).
cnf(u18928,axiom,
n3 != ssA(n9,n2) ).
cnf(u1383,axiom,
ssA(n4,n2) != ssA(n6,n3) ).
cnf(u605,axiom,
ssA(n5,n5) != ssA(n5,n7) ).
cnf(u1829,axiom,
n7 != ssA(n2,n3) ).
cnf(u1517,axiom,
ssA(n7,n3) != ssA(n8,n1) ).
cnf(u1714,axiom,
n6 = ssA(n5,n8) ).
cnf(u1814,axiom,
n1 != ssA(n6,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,
n6 != ssA(n7,n8) ).
cnf(u1879,axiom,
n2 != ssA(n2,n4) ).
cnf(u578,axiom,
ssA(n4,n2) != ssA(n4,n4) ).
cnf(u984,axiom,
ssA(n2,n4) != ssA(n3,n4) ).
cnf(u675,axiom,
ssA(n6,n1) != ssA(n6,n4) ).
cnf(u921,axiom,
ssA(n5,n3) != ssA(n6,n3) ).
cnf(u1892,axiom,
n4 != ssA(n4,n3) ).
cnf(u803,axiom,
ssA(n9,n2) != ssA(n9,n4) ).
cnf(u1715,axiom,
n5 = ssA(n6,n5) ).
cnf(u1481,axiom,
ssA(n4,n7) != ssA(n6,n8) ).
cnf(u1280,axiom,
ssA(n2,n5) != ssA(n3,n4) ).
cnf(u1843,axiom,
n8 != ssA(n8,n6) ).
cnf(u420,axiom,
ssA(n1,n6) != ssA(n1,n9) ).
cnf(u601,axiom,
ssA(n5,n6) != ssA(n5,n8) ).
cnf(u1856,axiom,
n5 != ssA(n3,n7) ).
cnf(u1232,axiom,
ssA(n2,n3) != ssA(n3,n1) ).
cnf(u974,axiom,
ssA(n3,n4) != ssA(n7,n4) ).
cnf(u848,axiom,
ssA(n2,n1) != ssA(n4,n1) ).
cnf(u1514,axiom,
ssA(n7,n3) != ssA(n9,n1) ).
cnf(u1823,axiom,
n7 != ssA(n8,n3) ).
cnf(u687,axiom,
ssA(n7,n8) != ssA(n7,n9) ).
cnf(u1283,axiom,
ssA(n2,n4) != ssA(n3,n5) ).
cnf(u933,axiom,
ssA(n2,n3) != ssA(n9,n3) ).
cnf(u1345,axiom,
ssA(n1,n7) != ssA(n3,n9) ).
cnf(u1061,axiom,
ssA(n4,n6) != ssA(n5,n6) ).
cnf(u1973,axiom,
n6 != ssA(n4,n7) ).
cnf(u1424,axiom,
ssA(n4,n6) != ssA(n6,n4) ).
cnf(u485,axiom,
ssA(n2,n2) != ssA(n2,n7) ).
cnf(u1848,axiom,
n8 != ssA(n3,n6) ).
cnf(u1525,axiom,
ssA(n7,n1) != ssA(n9,n3) ).
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,
n3 != ssA(n1,n9) ).
cnf(u586,axiom,
ssA(n4,n1) != ssA(n4,n3) ).
cnf(u929,axiom,
ssA(n3,n3) != ssA(n7,n3) ).
cnf(u390,axiom,
n3 != n6 ).
cnf(u811,axiom,
ssA(n9,n1) != ssA(n9,n3) ).
cnf(u2023,axiom,
n2 != ssA(n6,n7) ).
cnf(u1483,axiom,
ssA(n4,n7) != ssA(n5,n9) ).
cnf(u664,axiom,
ssA(n6,n2) != ssA(n6,n8) ).
cnf(u17943,axiom,
n7 != ssA(n7,n6) ).
cnf(u1851,axiom,
n5 != ssA(n8,n7) ).
cnf(u1015,axiom,
ssA(n4,n5) != ssA(n6,n5) ).
cnf(u1078,axiom,
ssA(n1,n6) != ssA(n6,n6) ).
cnf(u1970,axiom,
n6 != ssA(n6,n9) ).
cnf(u1298,axiom,
ssA(n1,n5) != ssA(n2,n4) ).
cnf(u834,axiom,
ssA(n4,n1) != ssA(n7,n1) ).
cnf(u982,axiom,
ssA(n2,n4) != ssA(n5,n4) ).
cnf(u1801,axiom,
n6 != ssA(n1,n2) ).
cnf(u2022,axiom,
n2 != ssA(n7,n7) ).
cnf(u793,axiom,
ssA(n9,n3) != ssA(n9,n8) ).
cnf(u695,axiom,
ssA(n7,n5) != ssA(n7,n7) ).
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(n5,n6) ).
cnf(u676,axiom,
ssA(n6,n1) != ssA(n6,n3) ).
cnf(u1011,axiom,
ssA(n5,n5) != ssA(n6,n5) ).
cnf(u1716,axiom,
n3 = ssA(n6,n6) ).
cnf(u1923,axiom,
n6 != ssA(n5,n6) ).
cnf(u1104,axiom,
ssA(n4,n7) != ssA(n7,n7) ).
cnf(u846,axiom,
ssA(n2,n1) != ssA(n6,n1) ).
cnf(u16791,axiom,
n4 != ssA(n7,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(u1886,axiom,
n1 != ssA(n2,n2) ).
cnf(u559,axiom,
ssA(n4,n5) != ssA(n4,n8) ).
cnf(u805,axiom,
ssA(n9,n1) != ssA(n9,n9) ).
cnf(u1717,axiom,
n7 = ssA(n7,n4) ).
cnf(u378,axiom,
n5 != n9 ).
cnf(u398,axiom,
n2 != n4 ).
cnf(u1156,axiom,
ssA(n3,n8) != ssA(n5,n8) ).
cnf(u1845,axiom,
n8 != ssA(n6,n6) ).
cnf(u540,axiom,
ssA(n3,n1) != ssA(n3,n4) ).
cnf(u672,axiom,
ssA(n6,n1) != ssA(n6,n7) ).
cnf(u1023,axiom,
ssA(n2,n5) != ssA(n9,n5) ).
cnf(u1978,axiom,
n3 != ssA(n6,n2) ).
cnf(u12061,axiom,
n3 != ssA(n3,n8) ).
cnf(u842,axiom,
ssA(n3,n1) != ssA(n4,n1) ).
cnf(u492,axiom,
ssA(n2,n1) != ssA(n2,n7) ).
cnf(u1809,axiom,
n8 != ssA(n2,n2) ).
cnf(u673,axiom,
ssA(n6,n1) != ssA(n6,n6) ).
cnf(u555,axiom,
ssA(n4,n6) != ssA(n4,n9) ).
cnf(u443,axiom,
ssA(n1,n2) != ssA(n1,n4) ).
cnf(u1233,axiom,
ssA(n2,n2) != ssA(n3,n3) ).
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,
n4 != ssA(n7,n5) ).
cnf(u1595,axiom,
ssA(n8,n8) != ssA(n9,n7) ).
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,
n8 != ssA(n9,n6) ).
cnf(u708,axiom,
ssA(n7,n2) != ssA(n7,n9) ).
cnf(u1931,axiom,
n6 != ssA(n3,n8) ).
cnf(u1112,axiom,
ssA(n3,n7) != ssA(n4,n7) ).
cnf(u488,axiom,
ssA(n2,n2) != ssA(n2,n4) ).
cnf(u1463,axiom,
ssA(n5,n7) != ssA(n6,n8) ).
cnf(u1394,axiom,
ssA(n4,n1) != ssA(n5,n2) ).
cnf(u1894,axiom,
n4 != ssA(n4,n1) ).
cnf(u567,axiom,
ssA(n4,n3) != ssA(n4,n9) ).
cnf(u1097,axiom,
ssA(n6,n7) != ssA(n7,n7) ).
cnf(u2009,axiom,
n3 != ssA(n8,n1) ).
cnf(u2000,axiom,
n1 != ssA(n7,n5) ).
cnf(u932,axiom,
ssA(n3,n3) != ssA(n4,n3) ).
cnf(u658,axiom,
ssA(n6,n3) != ssA(n6,n8) ).
cnf(u1853,axiom,
n5 != ssA(n6,n7) ).
cnf(u1972,axiom,
n6 != ssA(n4,n9) ).
cnf(u883,axiom,
ssA(n3,n2) != ssA(n8,n2) ).
cnf(u825,axiom,
ssA(n6,n1) != ssA(n9,n1) ).
cnf(u1795,axiom,
n1 != ssA(n1,n3) ).
cnf(u1412,axiom,
ssA(n5,n6) != ssA(n6,n4) ).
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,
n9 != ssA(n4,n1) ).
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,
n3 = ssA(n3,n7) ).
cnf(u895,axiom,
ssA(n1,n2) != ssA(n9,n2) ).
cnf(u1141,axiom,
ssA(n6,n8) != ssA(n8,n8) ).
cnf(u1850,axiom,
n5 != ssA(n9,n7) ).
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(u1105,axiom,
ssA(n4,n7) != ssA(n6,n7) ).
cnf(u1099,axiom,
ssA(n5,n7) != ssA(n8,n7) ).
cnf(u2017,axiom,
n3 != ssA(n7,n3) ).
cnf(u792,axiom,
ssA(n9,n3) != ssA(n9,n9) ).
cnf(u534,axiom,
ssA(n3,n2) != ssA(n3,n3) ).
cnf(u666,axiom,
ssA(n6,n2) != ssA(n6,n6) ).
cnf(u763,axiom,
ssA(n8,n1) != ssA(n8,n6) ).
cnf(u1009,axiom,
ssA(n5,n5) != ssA(n8,n5) ).
cnf(u1574,axiom,
ssA(n7,n4) != ssA(n8,n5) ).
cnf(u1980,axiom,
n3 != ssA(n7,n6) ).
cnf(u470,axiom,
ssA(n2,n5) != ssA(n2,n7) ).
cnf(u891,axiom,
ssA(n2,n2) != ssA(n6,n2) ).
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,
n6 != ssA(n1,n7) ).
cnf(u429,axiom,
ssA(n1,n4) != ssA(n1,n7) ).
cnf(u1922,axiom,
n6 != ssA(n5,n7) ).
cnf(u1126,axiom,
ssA(n1,n7) != ssA(n3,n7) ).
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(u17088,axiom,
n9 = ssA(n1,n9) ).
cnf(u1881,axiom,
n1 != ssA(n3,n3) ).
cnf(u1597,axiom,
ssA(n8,n7) != ssA(n9,n9) ).
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,
n8 != ssA(n7,n6) ).
cnf(u466,axiom,
ssA(n2,n6) != ssA(n2,n8) ).
cnf(u1933,axiom,
n6 != ssA(n1,n8) ).
cnf(u12882,axiom,
n9 != ssA(n7,n7) ).
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,
n1 != ssA(n7,n2) ).
cnf(u1184,axiom,
ssA(n7,n9) != ssA(n8,n9) ).
cnf(u926,axiom,
ssA(n4,n3) != ssA(n5,n3) ).
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(u885,axiom,
ssA(n3,n2) != ssA(n6,n2) ).
cnf(u399,axiom,
n2 != n3 ).
cnf(u478,axiom,
ssA(n2,n3) != ssA(n2,n8) ).
cnf(u1797,axiom,
n7 != ssA(n1,n2) ).
cnf(u620,axiom,
ssA(n5,n2) != ssA(n5,n7) ).
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(u975,axiom,
ssA(n3,n4) != ssA(n6,n4) ).
cnf(u1930,axiom,
n6 != ssA(n4,n8) ).
cnf(u1349,axiom,
ssA(n1,n7) != ssA(n2,n8) ).
cnf(u1953,axiom,
n5 != ssA(n2,n5) ).
cnf(u1546,axiom,
ssA(n8,n6) != ssA(n9,n5) ).
cnf(u922,axiom,
ssA(n4,n3) != ssA(n9,n3) ).
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,
n5 != ssA(n7,n7) ).
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(u616,axiom,
ssA(n5,n3) != ssA(n5,n5) ).
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(u1794,axiom,
n1 != ssA(n1,n4) ).
cnf(u1341,axiom,
ssA(n1,n8) != ssA(n2,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(u1346,axiom,
ssA(n1,n7) != ssA(n3,n8) ).
cnf(u1974,axiom,
n3 != ssA(n6,n7) ).
cnf(u519,axiom,
ssA(n3,n4) != ssA(n3,n7) ).
cnf(u893,axiom,
ssA(n2,n2) != ssA(n4,n2) ).
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,
n7 != ssA(n7,n7) ).
cnf(u628,axiom,
ssA(n5,n1) != ssA(n5,n6) ).
cnf(u1924,axiom,
n6 != ssA(n5,n5) ).
cnf(u835,axiom,
ssA(n4,n1) != ssA(n6,n1) ).
cnf(u983,axiom,
ssA(n2,n4) != ssA(n4,n4) ).
cnf(u1003,axiom,
ssA(n7,n5) != ssA(n9,n5) ).
cnf(u16812,axiom,
n6 != ssA(n7,n2) ).
cnf(u1875,axiom,
n2 != ssA(n4,n2) ).
cnf(u1056,axiom,
ssA(n5,n6) != ssA(n6,n6) ).
cnf(u798,axiom,
ssA(n9,n2) != ssA(n9,n9) ).
cnf(u1198,axiom,
ssA(n3,n9) != ssA(n8,n9) ).
cnf(u629,axiom,
ssA(n5,n1) != ssA(n5,n5) ).
cnf(u761,axiom,
ssA(n8,n1) != ssA(n8,n8) ).
cnf(u1838,axiom,
n2 != ssA(n1,n2) ).
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(u430,axiom,
ssA(n1,n4) != ssA(n1,n6) ).
cnf(u1983,axiom,
n3 != ssA(n3,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(u1390,axiom,
ssA(n4,n1) != ssA(n6,n3) ).
cnf(u16256,axiom,
n5 != ssA(n7,n1) ).
cnf(u1790,axiom,
n1 != ssA(n1,n8) ).
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(u2005,axiom,
n1 != ssA(n2,n8) ).
cnf(u1202,axiom,
ssA(n3,n9) != ssA(n4,n9) ).
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(u16885,axiom,
n9 != ssA(n5,n5) ).
cnf(u17819,axiom,
n7 != ssA(n7,n5) ).
cnf(u625,axiom,
ssA(n5,n1) != ssA(n5,n9) ).
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,
n6 != ssA(n2,n8) ).
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,
n1 != ssA(n7,n3) ).
cnf(u1206,axiom,
ssA(n2,n9) != ssA(n6,n9) ).
cnf(u1618,axiom,
ssA(n7,n7) != ssA(n8,n9) ).
cnf(u2024,axiom,
n2 != ssA(n5,n7) ).
cnf(u1049,axiom,
ssA(n7,n6) != ssA(n8,n6) ).
cnf(u1961,axiom,
n4 != ssA(n6,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,
n3 != ssA(n4,n2) ).
cnf(u17925,axiom,
n5 != ssA(n7,n6) ).
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(u622,axiom,
ssA(n5,n2) != ssA(n5,n5) ).
cnf(u1855,axiom,
n5 != ssA(n4,n7) ).
cnf(u837,axiom,
ssA(n3,n1) != ssA(n9,n1) ).
cnf(u1034,axiom,
ssA(n1,n5) != ssA(n5,n5) ).
cnf(u1877,axiom,
n2 != ssA(n7,n4) ).
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,
n3 != ssA(n7,n2) ).
cnf(u1002,axiom,
ssA(n8,n5) != ssA(n9,n5) ).
cnf(u1051,axiom,
ssA(n6,n6) != ssA(n8,n6) ).
cnf(u1969,axiom,
n2 != ssA(n5,n5) ).
cnf(u739,axiom,
ssA(n8,n5) != ssA(n8,n8) ).
cnf(u705,axiom,
ssA(n7,n3) != ssA(n7,n6) ).
cnf(u574,axiom,
ssA(n4,n2) != ssA(n4,n8) ).
cnf(u892,axiom,
ssA(n2,n2) != ssA(n5,n2) ).
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,
n1 = ssA(n1,n1) ).
cnf(u422,axiom,
ssA(n1,n6) != ssA(n1,n7) ).
cnf(u1927,axiom,
n6 != ssA(n5,n2) ).
cnf(u12593,axiom,
n6 != ssA(n4,n1) ).
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(u1031,axiom,
ssA(n1,n5) != ssA(n8,n5) ).
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,
n2 != ssA(n4,n3) ).
cnf(u1293,axiom,
ssA(n1,n5) != ssA(n3,n6) ).
cnf(u1014,axiom,
ssA(n4,n5) != ssA(n7,n5) ).
cnf(u1833,axiom,
n6 != ssA(n6,n4) ).
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,
n6 != ssA(n5,n3) ).
cnf(u524,axiom,
ssA(n3,n3) != ssA(n3,n7) ).
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,
n1 != ssA(n2,n3) ).
cnf(u580,axiom,
ssA(n4,n1) != ssA(n4,n9) ).
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(u1918,axiom,
n3 != ssA(n2,n9) ).
cnf(u483,axiom,
ssA(n2,n2) != ssA(n2,n9) ).
cnf(u1712,axiom,
n4 = ssA(n4,n5) ).
cnf(u960,axiom,
ssA(n6,n4) != ssA(n9,n4) ).
cnf(u1188,axiom,
ssA(n5,n9) != ssA(n9,n9) ).
cnf(u572,axiom,
ssA(n4,n3) != ssA(n4,n4) ).
cnf(u576,axiom,
ssA(n4,n2) != ssA(n4,n6) ).
cnf(u927,axiom,
ssA(n3,n3) != ssA(n9,n3) ).
cnf(u1713,axiom,
n9 = ssA(n5,n1) ).
cnf(u874,axiom,
ssA(n5,n2) != ssA(n8,n2) ).
cnf(u396,axiom,
n2 != n6 ).
cnf(u1841,axiom,
n2 != ssA(n3,n1) ).
cnf(u577,axiom,
ssA(n4,n2) != ssA(n4,n5) ).
cnf(u1960,axiom,
n5 != ssA(n4,n6) ).
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,
n1 != ssA(n1,n2) ).
cnf(u568,axiom,
ssA(n4,n3) != ssA(n4,n8) ).
cnf(u1606,axiom,
ssA(n7,n9) != ssA(n8,n8) ).
cnf(u2012,axiom,
n3 != ssA(n5,n2) ).
cnf(u791,axiom,
ssA(n9,n4) != ssA(n9,n5) ).
cnf(u1037,axiom,
ssA(n1,n5) != ssA(n2,n5) ).
cnf(u923,axiom,
ssA(n4,n3) != ssA(n8,n3) ).
cnf(u1528,axiom,
ssA(n7,n1) != ssA(n8,n3) ).
cnf(u1963,axiom,
n4 != ssA(n5,n6) ).
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,
n7 != ssA(n1,n7) ).
cnf(u10902,axiom,
n2 != ssA(n4,n9) ).
cnf(u1813,axiom,
n1 != ssA(n7,n1) ).
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(u1876,axiom,
n2 != ssA(n4,n1) ).
cnf(u1250,axiom,
ssA(n1,n2) != ssA(n3,n1) ).
cnf(u787,axiom,
ssA(n9,n4) != ssA(n9,n9) ).
cnf(u10906,axiom,
n2 != ssA(n4,n8) ).
cnf(u1827,axiom,
n7 != ssA(n4,n3) ).
cnf(u1150,axiom,
ssA(n4,n8) != ssA(n6,n8) ).
cnf(u404,axiom,
n1 != n5 ).
cnf(u585,axiom,
ssA(n4,n1) != ssA(n4,n4) ).
cnf(u16882,axiom,
n9 != ssA(n3,n4) ).
cnf(u1968,axiom,
n2 != ssA(n5,n6) ).
cnf(u1216,axiom,
ssA(n1,n9) != ssA(n3,n9) ).
cnf(u832,axiom,
ssA(n4,n1) != ssA(n9,n1) ).
cnf(u702,axiom,
ssA(n7,n3) != ssA(n7,n9) ).
cnf(u1998,axiom,
n1 != ssA(n7,n7) ).
cnf(u671,axiom,
ssA(n6,n1) != ssA(n6,n8) ).
cnf(u917,axiom,
ssA(n6,n3) != ssA(n7,n3) ).
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(u1957,axiom,
n9 != ssA(n4,n2) ).
cnf(u469,axiom,
ssA(n2,n5) != ssA(n2,n8) ).
cnf(u400,axiom,
n1 != n9 ).
cnf(u1832,axiom,
n6 != ssA(n7,n4) ).
cnf(u1706,axiom,
n6 = ssA(n1,n4) ).
cnf(u1137,axiom,
ssA(n8,n8) != ssA(n9,n8) ).
cnf(u1921,axiom,
n5 != ssA(n3,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(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(u1707,axiom,
n8 = ssA(n2,n6) ).
cnf(u648,axiom,
ssA(n6,n5) != ssA(n6,n9) ).
cnf(u1111,axiom,
ssA(n3,n7) != ssA(n5,n7) ).
cnf(u1835,axiom,
n6 != ssA(n4,n4) ).
cnf(u1954,axiom,
n5 != ssA(n1,n5) ).
cnf(u1030,axiom,
ssA(n1,n5) != ssA(n9,n5) ).
cnf(u1570,axiom,
ssA(n7,n4) != ssA(n9,n6) ).
cnf(u966,axiom,
ssA(n5,n4) != ssA(n6,n4) ).
cnf(u562,axiom,
ssA(n4,n4) != ssA(n4,n9) ).
cnf(u12884,axiom,
n9 != ssA(n1,n7) ).
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(u1122,axiom,
ssA(n1,n7) != ssA(n7,n7) ).
cnf(u1124,axiom,
ssA(n1,n7) != ssA(n5,n7) ).
cnf(u1571,axiom,
ssA(n7,n4) != ssA(n9,n5) ).
cnf(u1965,axiom,
n2 != ssA(n6,n6) ).
cnf(u660,axiom,
ssA(n6,n3) != ssA(n6,n6) ).
cnf(u1840,axiom,
n2 != ssA(n7,n2) ).
cnf(u958,axiom,
ssA(n7,n4) != ssA(n9,n4) ).
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(u1870,axiom,
n3 != ssA(n3,n1) ).
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,
n3 != ssA(n2,n2) ).
cnf(u1475,axiom,
ssA(n4,n8) != ssA(n6,n7) ).
cnf(u18185,axiom,
n8 = ssA(n8,n9) ).
cnf(u656,axiom,
ssA(n6,n4) != ssA(n6,n5) ).
cnf(u1007,axiom,
ssA(n6,n5) != ssA(n7,n5) ).
cnf(u1253,axiom,
ssA(n1,n2) != ssA(n2,n1) ).
cnf(u1962,axiom,
n4 != ssA(n6,n4) ).
cnf(u1251,axiom,
ssA(n1,n2) != ssA(n2,n3) ).
cnf(u1381,axiom,
ssA(n4,n3) != ssA(n5,n2) ).
cnf(u831,axiom,
ssA(n5,n1) != ssA(n6,n1) ).
cnf(u476,axiom,
ssA(n2,n4) != ssA(n2,n5) ).
cnf(u1793,axiom,
n1 != ssA(n1,n5) ).
cnf(u1292,axiom,
ssA(n1,n6) != ssA(n2,n4) ).
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(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(u1826,axiom,
n7 != ssA(n5,n3) ).
cnf(u1480,axiom,
ssA(n4,n7) != ssA(n6,n9) ).
cnf(u1708,axiom,
n5 = ssA(n2,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(u669,axiom,
ssA(n6,n2) != ssA(n6,n3) ).
cnf(u1378,axiom,
ssA(n4,n3) != ssA(n6,n2) ).
cnf(u1878,axiom,
n2 != ssA(n3,n4) ).
cnf(u1209,axiom,
ssA(n2,n9) != ssA(n3,n9) ).
cnf(u797,axiom,
ssA(n9,n3) != ssA(n9,n4) ).
cnf(u439,axiom,
ssA(n1,n2) != ssA(n1,n8) ).
cnf(u1709,axiom,
n2 = ssA(n3,n2) ).
cnf(u441,axiom,
ssA(n1,n2) != ssA(n1,n6) ).
cnf(u916,axiom,
ssA(n6,n3) != ssA(n8,n3) ).
cnf(u642,axiom,
ssA(n6,n8) != ssA(n6,n9) ).
cnf(u16127,axiom,
n2 != ssA(n3,n3) ).
cnf(u1837,axiom,
n6 != ssA(n2,n4) ).
cnf(u532,axiom,
ssA(n3,n2) != ssA(n3,n5) ).
cnf(u1984,axiom,
n3 != ssA(n1,n6) ).
cnf(u1956,axiom,
n9 != ssA(n4,n3) ).
cnf(u867,axiom,
ssA(n8,n2) != ssA(n9,n2) ).
cnf(u1907,axiom,
n8 != ssA(n3,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(u17859,axiom,
n6 != ssA(n8,n3) ).
cnf(u533,axiom,
ssA(n3,n2) != ssA(n3,n4) ).
cnf(u665,axiom,
ssA(n6,n2) != ssA(n6,n7) ).
cnf(u1920,axiom,
n5 != ssA(n3,n9) ).
cnf(u12594,axiom,
n6 != ssA(n7,n6) ).
cnf(u1573,axiom,
ssA(n7,n4) != ssA(n8,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(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(u1125,axiom,
ssA(n1,n7) != ssA(n4,n7) ).
cnf(u1834,axiom,
n6 != ssA(n5,n4) ).
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,
n6 != ssA(n3,n5) ).
cnf(u1211,axiom,
ssA(n1,n9) != ssA(n8,n9) ).
cnf(u16447,axiom,
n7 = ssA(n4,n2) ).
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(u1558,axiom,
ssA(n7,n6) != ssA(n9,n5) ).
cnf(u1964,axiom,
n4 != ssA(n5,n4) ).
cnf(u875,axiom,
ssA(n5,n2) != ssA(n7,n2) ).
cnf(u10903,axiom,
n2 != ssA(n3,n9) ).
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(u898,axiom,
ssA(n1,n2) != ssA(n6,n2) ).
cnf(u1081,axiom,
ssA(n1,n6) != ssA(n3,n6) ).
cnf(u1865,axiom,
n7 != ssA(n2,n2) ).
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(u759,axiom,
ssA(n8,n2) != ssA(n8,n3) ).
cnf(u1005,axiom,
ssA(n6,n5) != ssA(n9,n5) ).
cnf(u1828,axiom,
n7 != ssA(n3,n3) ).
cnf(u11529,axiom,
n4 = ssA(n5,n7) ).
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,
n1 != ssA(n1,n6) ).
cnf(u1168,axiom,
ssA(n1,n8) != ssA(n6,n8) ).
cnf(u1815,axiom,
n1 != ssA(n5,n1) ).
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,
n5 != ssA(n5,n5) ).
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(u1199,axiom,
ssA(n3,n9) != ssA(n7,n9) ).
cnf(u421,axiom,
ssA(n1,n6) != ssA(n1,n8) ).
cnf(u9972,axiom,
n7 != ssA(n1,n8) ).
cnf(u1873,axiom,
n2 != ssA(n4,n7) ).
cnf(u737,axiom,
ssA(n8,n6) != ssA(n8,n7) ).
cnf(u796,axiom,
ssA(n9,n3) != ssA(n9,n5) ).
cnf(u522,axiom,
ssA(n3,n3) != ssA(n3,n9) ).
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(u1836,axiom,
n6 != ssA(n3,n4) ).
cnf(u1212,axiom,
ssA(n1,n9) != ssA(n7,n9) ).
cnf(u1959,axiom,
n5 != ssA(n5,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(u1197,axiom,
ssA(n3,n9) != ssA(n9,n9) ).
cnf(u556,axiom,
ssA(n4,n6) != ssA(n4,n8) ).
cnf(u1338,axiom,
ssA(n1,n8) != ssA(n3,n9) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : PUZ069+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.04/0.31 % Computer : n012.cluster.edu
% 0.04/0.31 % Model : x86_64 x86_64
% 0.04/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.31 % Memory : 8046.5625MB
% 0.04/0.31 % OS : Linux 6.8.0-71-generic
% 0.04/0.31 % CPULimit : 300
% 0.04/0.31 % WCLimit : 300
% 0.04/0.31 % DateTime : Sun Sep 27 22:38:35 UTC 2026
% 0.04/0.32 % CPUTime :
% 0.04/0.32 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.33 Running first-order model finding
% 0.07/0.33 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.18/0.57 % (2823703)Will run a generic schedule for satisfiability detection.
% 1.18/0.57 % (2823709)% WARNING: option uhcvi not known.
% 1.18/0.57 % (2823710)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=566462772:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.18/0.57 % (2823711)dis+10_1_sil=32000:sp=arity:random_seed=1507251414:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.18/0.57 % (2823709)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4289599320:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.18/0.57 % (2823708)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=146679333_2999 on theBenchmark for (2999ds/0Mi)
% 1.18/0.57 % (2823712)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1524043274:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.18/0.57 % (2823713)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1995181992:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.18/0.57 % (2823714)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3393019703:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.18/0.57 % (2823711)Instruction limit reached!
% 1.18/0.57 % (2823711)------------------------------
% 1.18/0.57 % (2823711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.18/0.57 % (2823711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.18/0.57 % (2823711)CaDiCaL version: 2.1.3
% 1.18/0.57 % (2823711)Termination reason: Instruction limit
% 1.18/0.57 % (2823711)Termination phase: Saturation
% 1.18/0.57 % (2823711)Time elapsed: 0.026 s
% 1.18/0.57 % (2823711)Peak memory usage: 14 MB
% 1.18/0.57 % (2823711)Instructions burned: 104 (million)
% 1.18/0.57 % (2823712)Instruction limit reached!
% 1.18/0.57 % (2823712)------------------------------
% 1.18/0.57 % (2823712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.18/0.57 % (2823712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.18/0.57 % (2823712)CaDiCaL version: 2.1.3
% 1.18/0.57 % (2823712)Termination reason: Instruction limit
% 1.18/0.57 % (2823712)Termination phase: Saturation
% 1.18/0.57 % (2823712)Time elapsed: 0.028 s
% 1.18/0.57 % (2823712)Peak memory usage: 13 MB
% 1.18/0.57 % (2823712)Instructions burned: 119 (million)
% 1.18/0.57 % (2823713)Instruction limit reached!
% 1.18/0.57 % (2823713)------------------------------
% 1.18/0.57 % (2823713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.18/0.57 % (2823713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.18/0.57 % (2823713)CaDiCaL version: 2.1.3
% 1.18/0.57 % (2823713)Termination reason: Instruction limit
% 1.18/0.57 % (2823713)Termination phase: Saturation
% 1.18/0.57 % (2823713)Time elapsed: 0.029 s
% 1.18/0.57 % (2823713)Peak memory usage: 12 MB
% 1.18/0.57 % (2823713)Instructions burned: 134 (million)
% 1.18/0.57 % (2823722)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2183113863:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.18/0.57 % (2823723)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2258415070:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.18/0.57 % (2823724)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=719078304:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 1.18/0.57 % (2823714)Instruction limit reached!
% 1.18/0.57 % (2823714)------------------------------
% 1.18/0.57 % (2823714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.18/0.57 % (2823714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.18/0.57 % (2823714)CaDiCaL version: 2.1.3
% 1.18/0.57 % (2823714)Termination reason: Instruction limit
% 1.18/0.57 % (2823714)Termination phase: Saturation
% 1.18/0.57 % (2823714)Time elapsed: 0.042 s
% 1.18/0.57 % (2823714)Peak memory usage: 15 MB
% 1.18/0.57 % (2823714)Instructions burned: 161 (million)
% 1.18/0.57 % (2823728)ott-21_1_sil=16000:fs=off:random_seed=160116052:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 1.18/0.57 % (2823723)Instruction limit reached!
% 1.18/0.57 % (2823723)------------------------------
% 1.18/0.57 % (2823723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.18/0.57 % (2823723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.18/0.57 % (2823723)CaDiCaL version: 2.1.3
% 1.18/0.57 % (2823723)Termination reason: Instruction limit
% 1.18/0.57 % (2823723)Termination phase: Saturation
% 1.18/0.57 % (2823723)Time elapsed: 0.031 s
% 1.18/0.57 % (2823723)Peak memory usage: 14 MB
% 1.18/0.57 % (2823723)Instructions burned: 134 (million)
% 1.18/0.57 % (2823730)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=173795643:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.18/0.57 % Detected minimum model sizes of [9]
% 1.18/0.57 % Detected maximum model sizes of [max]
% 1.18/0.57 % TRYING [9]
% 1.18/0.57 % (2823728)Instruction limit reached!
% 1.18/0.57 % (2823728)------------------------------
% 1.18/0.57 % (2823728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.18/0.57 % (2823728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.18/0.57 % (2823728)CaDiCaL version: 2.1.3
% 1.18/0.57 % (2823728)Termination reason: Instruction limit
% 1.18/0.57 % (2823728)Termination phase: Saturation
% 1.18/0.57 % (2823728)Time elapsed: 0.049 s
% 1.18/0.57 % (2823728)Peak memory usage: 12 MB
% 1.18/0.57 % (2823728)Instructions burned: 184 (million)
% 1.18/0.57 % (2823732)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2182695102:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 1.18/0.57 % Detected minimum model sizes of [9]
% 1.18/0.57 % Detected maximum model sizes of [max]
% 1.18/0.57 % TRYING [9]
% 1.18/0.57 % (2823710) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2823703-2823710"...
% 1.18/0.57 % (2823710)...printing done.
% 1.18/0.57 % SZS status Satisfiable for theBenchmark
% 1.18/0.57 % SZS output start Saturation.
% See solution above
% 1.18/0.58 % SZS output start Definitions and Model Updates.
% 1.18/0.58 for all inputs,
% 1.18/0.58 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.18/0.58 % SZS output end Definitions and Model Updates.
% 1.18/0.58 % (2823710)------------------------------
% 1.18/0.58 % (2823710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.18/0.58 % (2823710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.18/0.58 % (2823710)CaDiCaL version: 2.1.3
% 1.18/0.58 % (2823710)Termination reason: Satisfiable
% 1.18/0.58 % (2823710)Time elapsed: 0.191 s
% 1.18/0.58 % (2823710)Peak memory usage: 17 MB
% 1.18/0.58 % (2823710)Instructions burned: 674 (million)
% 1.18/0.58 % (2823703)Success in time 0.235 s
% 1.18/0.58 % Vampire exiting
%------------------------------------------------------------------------------