%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PUZ070+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n018.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.31s 0.79s
% Output : Saturation 1.31s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u2032,axiom,
n1 != ssA(n1,n3) ).
cnf(u2037,axiom,
n1 = ssA(n1,n1) ).
cnf(u2072,axiom,
n2 != ssA(n1,n9) ).
cnf(u2076,axiom,
n2 != ssA(n1,n8) ).
cnf(u2081,axiom,
n2 = ssA(n1,n7) ).
cnf(u2084,axiom,
n2 != ssA(n1,n3) ).
cnf(u2130,axiom,
n3 != ssA(n1,n9) ).
cnf(u2134,axiom,
n3 != ssA(n1,n8) ).
cnf(u2138,axiom,
n3 != ssA(n1,n7) ).
cnf(u2143,axiom,
n3 = ssA(n1,n4) ).
cnf(u2185,axiom,
n4 = ssA(n1,n9) ).
cnf(u2188,axiom,
n4 != ssA(n1,n7) ).
cnf(u2372,axiom,
n2 != ssA(n2,n8) ).
cnf(u2376,axiom,
n2 != ssA(n2,n6) ).
cnf(u2381,axiom,
n2 = ssA(n2,n5) ).
cnf(u2384,axiom,
n2 != ssA(n2,n3) ).
cnf(u2388,axiom,
n2 != ssA(n2,n2) ).
cnf(u2392,axiom,
n2 != ssA(n2,n1) ).
cnf(u2452,axiom,
n3 != ssA(n2,n8) ).
cnf(u2456,axiom,
n3 != ssA(n2,n6) ).
cnf(u2460,axiom,
n3 != ssA(n2,n5) ).
cnf(u2464,axiom,
n3 != ssA(n2,n4) ).
cnf(u2468,axiom,
n3 != ssA(n2,n3) ).
cnf(u2473,axiom,
n3 = ssA(n2,n2) ).
cnf(u2585,axiom,
n8 = ssA(n1,n8) ).
cnf(u2588,axiom,
n8 != ssA(n1,n4) ).
cnf(u2711,axiom,
n4 != ssA(n2,n6) ).
cnf(u2715,axiom,
n4 != ssA(n2,n5) ).
cnf(u2932,axiom,
n4 = ssA(n2,n4) ).
cnf(u2957,axiom,
n5 != ssA(n2,n8) ).
cnf(u2961,axiom,
n5 != ssA(n2,n3) ).
cnf(u2997,axiom,
n7 != ssA(n2,n6) ).
cnf(u3001,axiom,
n7 != ssA(n2,n5) ).
cnf(u3121,axiom,
n1 = ssA(n3,n6) ).
cnf(u3124,axiom,
n1 != ssA(n3,n4) ).
cnf(u3128,axiom,
n1 != ssA(n3,n3) ).
cnf(u3132,axiom,
n1 != ssA(n3,n2) ).
cnf(u3167,axiom,
n2 != ssA(n3,n9) ).
cnf(u3171,axiom,
n2 != ssA(n3,n8) ).
cnf(u3175,axiom,
n2 != ssA(n3,n7) ).
cnf(u3179,axiom,
n2 != ssA(n3,n4) ).
cnf(u3184,axiom,
n2 = ssA(n3,n3) ).
cnf(u3187,axiom,
n2 != ssA(n3,n2) ).
cnf(u3617,axiom,
n9 = ssA(n2,n3) ).
cnf(u3620,axiom,
n9 != ssA(n2,n2) ).
cnf(u3736,axiom,
n9 != ssA(n2,n8) ).
cnf(u3740,axiom,
n9 != ssA(n2,n1) ).
cnf(u3818,axiom,
n3 != ssA(n3,n9) ).
cnf(u3822,axiom,
n3 != ssA(n3,n8) ).
cnf(u3827,axiom,
n3 = ssA(n3,n7) ).
cnf(u3830,axiom,
n3 != ssA(n3,n4) ).
cnf(u3834,axiom,
n3 != ssA(n3,n2) ).
cnf(u3952,axiom,
n5 != ssA(n3,n9) ).
cnf(u3957,axiom,
n5 = ssA(n3,n8) ).
cnf(u3960,axiom,
n5 != ssA(n3,n2) ).
cnf(u4003,axiom,
n7 != ssA(n3,n8) ).
cnf(u4008,axiom,
n7 = ssA(n3,n4) ).
cnf(u4389,axiom,
n8 != ssA(n3,n9) ).
cnf(u4394,axiom,
n8 = ssA(n3,n2) ).
cnf(u4522,axiom,
n1 != ssA(n4,n7) ).
cnf(u4526,axiom,
n1 != ssA(n4,n2) ).
cnf(u4530,axiom,
n1 != ssA(n4,n1) ).
cnf(u4565,axiom,
n4 != ssA(n4,n9) ).
cnf(u4570,axiom,
n4 = ssA(n4,n6) ).
cnf(u4573,axiom,
n4 != ssA(n4,n3) ).
cnf(u4577,axiom,
n4 != ssA(n4,n2) ).
cnf(u4616,axiom,
n5 = ssA(n4,n9) ).
cnf(u4619,axiom,
n5 != ssA(n4,n6) ).
cnf(u4648,axiom,
n6 != ssA(n4,n6) ).
cnf(u4652,axiom,
n6 != ssA(n4,n3) ).
cnf(u4686,axiom,
n7 != ssA(n4,n7) ).
cnf(u4690,axiom,
n7 != ssA(n4,n3) ).
cnf(u4761,axiom,
n1 != ssA(n5,n8) ).
cnf(u4765,axiom,
n1 != ssA(n5,n7) ).
cnf(u4770,axiom,
n1 = ssA(n5,n5) ).
cnf(u4822,axiom,
n3 != ssA(n5,n9) ).
cnf(u4826,axiom,
n3 != ssA(n5,n3) ).
cnf(u4859,axiom,
n4 != ssA(n5,n6) ).
cnf(u4864,axiom,
n4 = ssA(n5,n3) ).
cnf(u4900,axiom,
n6 = ssA(n5,n4) ).
cnf(u4903,axiom,
n6 != ssA(n5,n3) ).
cnf(u5010,axiom,
n7 != ssA(n5,n7) ).
cnf(u5014,axiom,
n7 != ssA(n5,n3) ).
cnf(u5094,axiom,
n1 = ssA(n6,n8) ).
cnf(u5097,axiom,
n1 != ssA(n6,n7) ).
cnf(u5101,axiom,
n1 != ssA(n6,n6) ).
cnf(u5105,axiom,
n1 != ssA(n6,n5) ).
cnf(u5109,axiom,
n1 != ssA(n6,n4) ).
cnf(u5113,axiom,
n1 != ssA(n6,n3) ).
cnf(u5117,axiom,
n1 != ssA(n6,n2) ).
cnf(u5121,axiom,
n1 != ssA(n6,n1) ).
cnf(u5553,axiom,
n2 != ssA(n5,n8) ).
cnf(u5558,axiom,
n2 = ssA(n5,n6) ).
cnf(u5700,axiom,
n8 != ssA(n5,n9) ).
cnf(u5705,axiom,
n8 = ssA(n5,n7) ).
cnf(u5766,axiom,
n2 != ssA(n6,n8) ).
cnf(u5770,axiom,
n2 != ssA(n6,n6) ).
cnf(u5774,axiom,
n2 != ssA(n6,n4) ).
cnf(u5778,axiom,
n2 != ssA(n6,n3) ).
cnf(u5783,axiom,
n2 = ssA(n6,n2) ).
cnf(u5786,axiom,
n2 != ssA(n6,n1) ).
cnf(u5929,axiom,
n3 != ssA(n6,n9) ).
cnf(u5933,axiom,
n3 != ssA(n6,n8) ).
cnf(u5937,axiom,
n3 != ssA(n6,n7) ).
cnf(u5942,axiom,
n3 = ssA(n6,n3) ).
cnf(u5945,axiom,
n3 != ssA(n6,n1) ).
cnf(u6053,axiom,
n4 != ssA(n6,n9) ).
cnf(u6058,axiom,
n4 = ssA(n6,n7) ).
cnf(u6061,axiom,
n4 != ssA(n6,n6) ).
cnf(u6065,axiom,
n4 != ssA(n6,n4) ).
cnf(u6069,axiom,
n4 != ssA(n6,n3) ).
cnf(u6212,axiom,
n5 != ssA(n6,n7) ).
cnf(u6216,axiom,
n5 != ssA(n6,n6) ).
cnf(u6221,axiom,
n5 = ssA(n6,n4) ).
cnf(u6224,axiom,
n5 != ssA(n6,n3) ).
cnf(u6228,axiom,
n5 != ssA(n6,n1) ).
cnf(u6918,axiom,
n6 != ssA(n4,n9) ).
cnf(u6923,axiom,
n6 = ssA(n4,n2) ).
cnf(u6943,axiom,
n8 != ssA(n3,n7) ).
cnf(u7117,axiom,
n4 != ssA(n6,n8) ).
cnf(u7121,axiom,
n4 != ssA(n6,n5) ).
cnf(u7171,axiom,
n5 != ssA(n6,n9) ).
cnf(u7175,axiom,
n5 != ssA(n6,n8) ).
cnf(u7570,axiom,
n9 != ssA(n4,n9) ).
cnf(u7575,axiom,
n9 = ssA(n4,n7) ).
cnf(u8266,axiom,
n3 != ssA(n6,n2) ).
cnf(u9207,axiom,
n6 != ssA(n6,n6) ).
cnf(u9211,axiom,
n6 != ssA(n6,n4) ).
cnf(u9215,axiom,
n6 != ssA(n6,n3) ).
cnf(u10059,axiom,
n4 != ssA(n5,n9) ).
cnf(u10063,axiom,
n4 != ssA(n5,n5) ).
cnf(u13159,axiom,
n7 != ssA(n6,n7) ).
cnf(u13163,axiom,
n7 != ssA(n6,n4) ).
cnf(u13167,axiom,
n7 != ssA(n6,n3) ).
cnf(u13211,axiom,
n8 != ssA(n6,n4) ).
cnf(u13215,axiom,
n8 != ssA(n6,n3) ).
cnf(u13428,axiom,
n6 != ssA(n6,n8) ).
cnf(u13432,axiom,
n6 != ssA(n6,n2) ).
cnf(u13721,axiom,
n1 = ssA(n7,n7) ).
cnf(u13724,axiom,
n1 != ssA(n7,n2) ).
cnf(u13728,axiom,
n1 != ssA(n7,n1) ).
cnf(u13768,axiom,
n3 = ssA(n7,n9) ).
cnf(u13771,axiom,
n3 != ssA(n7,n6) ).
cnf(u13775,axiom,
n3 != ssA(n7,n5) ).
cnf(u13779,axiom,
n3 != ssA(n7,n2) ).
cnf(u13961,axiom,
n5 != ssA(n7,n2) ).
cnf(u13965,axiom,
n5 != ssA(n7,n1) ).
cnf(u14011,axiom,
n6 != ssA(n7,n9) ).
cnf(u14015,axiom,
n6 != ssA(n7,n2) ).
cnf(u14085,axiom,
n7 != ssA(n7,n9) ).
cnf(u14090,axiom,
n7 = ssA(n7,n5) ).
cnf(u14183,axiom,
n2 = ssA(n8,n9) ).
cnf(u14186,axiom,
n2 != ssA(n8,n8) ).
cnf(u14190,axiom,
n2 != ssA(n8,n7) ).
cnf(u14194,axiom,
n2 != ssA(n8,n6) ).
cnf(u14198,axiom,
n2 != ssA(n8,n5) ).
cnf(u14202,axiom,
n2 != ssA(n8,n1) ).
cnf(u14250,axiom,
n3 != ssA(n8,n9) ).
cnf(u14254,axiom,
n3 != ssA(n8,n8) ).
cnf(u14258,axiom,
n3 != ssA(n8,n6) ).
cnf(u14262,axiom,
n3 != ssA(n8,n5) ).
cnf(u14266,axiom,
n3 != ssA(n8,n2) ).
cnf(u14335,axiom,
n4 != ssA(n8,n9) ).
cnf(u14339,axiom,
n4 != ssA(n8,n7) ).
cnf(u14343,axiom,
n4 != ssA(n8,n5) ).
cnf(u14347,axiom,
n4 != ssA(n8,n3) ).
cnf(u14352,axiom,
n4 = ssA(n8,n2) ).
cnf(u14424,axiom,
n5 != ssA(n8,n6) ).
cnf(u14429,axiom,
n5 = ssA(n8,n3) ).
cnf(u14432,axiom,
n5 != ssA(n8,n2) ).
cnf(u15187,axiom,
n3 != ssA(n8,n3) ).
cnf(u15461,axiom,
n6 = ssA(n6,n9) ).
cnf(u15464,axiom,
n6 != ssA(n6,n1) ).
cnf(u16006,axiom,
n8 != ssA(n6,n7) ).
cnf(u16011,axiom,
n8 = ssA(n6,n1) ).
cnf(u17100,axiom,
n9 != ssA(n7,n5) ).
cnf(u17105,axiom,
n9 = ssA(n7,n2) ).
cnf(u18536,axiom,
n8 != ssA(n6,n9) ).
cnf(u18540,axiom,
n8 != ssA(n6,n2) ).
cnf(u20013,axiom,
n7 != ssA(n7,n7) ).
cnf(u20017,axiom,
n7 != ssA(n7,n1) ).
cnf(u21153,axiom,
n7 != ssA(n5,n6) ).
cnf(u21157,axiom,
n7 != ssA(n5,n5) ).
cnf(u21222,axiom,
n9 != ssA(n6,n9) ).
cnf(u21226,axiom,
n9 != ssA(n6,n7) ).
cnf(u22861,axiom,
n9 != ssA(n6,n8) ).
cnf(u22865,axiom,
n9 != ssA(n6,n1) ).
cnf(u28003,axiom,
n3 = ssA(n8,n1) ).
cnf(u29620,axiom,
n6 != ssA(n8,n8) ).
cnf(u29624,axiom,
n6 != ssA(n8,n2) ).
cnf(u29628,axiom,
n6 != ssA(n8,n1) ).
cnf(u29707,axiom,
n7 = ssA(n8,n7) ).
cnf(u29710,axiom,
n7 != ssA(n8,n1) ).
cnf(u29793,axiom,
n8 != ssA(n8,n9) ).
cnf(u29797,axiom,
n8 != ssA(n8,n7) ).
cnf(u30286,axiom,
n7 != ssA(n8,n9) ).
cnf(u30290,axiom,
n7 != ssA(n8,n5) ).
cnf(u30455,axiom,
n8 != ssA(n8,n6) ).
cnf(u30460,axiom,
n8 = ssA(n8,n5) ).
cnf(u30677,axiom,
n9 = ssA(n8,n8) ).
cnf(u30680,axiom,
n9 != ssA(n8,n2) ).
cnf(u30775,axiom,
n1 != ssA(n9,n6) ).
cnf(u30779,axiom,
n1 != ssA(n9,n5) ).
cnf(u30783,axiom,
n1 != ssA(n9,n4) ).
cnf(u30787,axiom,
n1 != ssA(n9,n3) ).
cnf(u30792,axiom,
n1 = ssA(n9,n2) ).
cnf(u30795,axiom,
n1 != ssA(n9,n1) ).
cnf(u30933,axiom,
n2 != ssA(n9,n9) ).
cnf(u30937,axiom,
n2 != ssA(n9,n8) ).
cnf(u30941,axiom,
n2 != ssA(n9,n6) ).
cnf(u30945,axiom,
n2 != ssA(n9,n5) ).
cnf(u30949,axiom,
n2 != ssA(n9,n4) ).
cnf(u30953,axiom,
n2 != ssA(n9,n3) ).
cnf(u30958,axiom,
n2 = ssA(n9,n1) ).
cnf(u31151,axiom,
n3 != ssA(n9,n9) ).
cnf(u31155,axiom,
n3 != ssA(n9,n8) ).
cnf(u31160,axiom,
n3 = ssA(n9,n6) ).
cnf(u31163,axiom,
n3 != ssA(n9,n5) ).
cnf(u31167,axiom,
n3 != ssA(n9,n4) ).
cnf(u31304,axiom,
n4 != ssA(n9,n9) ).
cnf(u31308,axiom,
n4 != ssA(n9,n8) ).
cnf(u31313,axiom,
n4 = ssA(n9,n5) ).
cnf(u31316,axiom,
n4 != ssA(n9,n4) ).
cnf(u31320,axiom,
n4 != ssA(n9,n3) ).
cnf(u31487,axiom,
n6 = ssA(n9,n8) ).
cnf(u31490,axiom,
n6 != ssA(n9,n4) ).
cnf(u31535,axiom,
n7 != ssA(n9,n9) ).
cnf(u31539,axiom,
n7 != ssA(n9,n4) ).
cnf(u31544,axiom,
n7 = ssA(n9,n3) ).
cnf(u31675,axiom,
n8 = ssA(n9,n9) ).
cnf(u31678,axiom,
n8 != ssA(n9,n4) ).
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,
n8 != ssA(n5,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(u1074,axiom,
ssA(n2,n6) != ssA(n3,n6) ).
cnf(u722,axiom,
ssA(n7,n1) != ssA(n7,n2) ).
cnf(u643,axiom,
ssA(n6,n7) != ssA(n6,n9) ).
cnf(u612,axiom,
ssA(n5,n3) != ssA(n5,n9) ).
cnf(u28961,axiom,
n3 != ssA(n1,n3) ).
cnf(u29465,axiom,
n7 = ssA(n4,n1) ).
cnf(u947,axiom,
ssA(n1,n3) != ssA(n2,n3) ).
cnf(u967,axiom,
ssA(n4,n4) != ssA(n9,n4) ).
cnf(u1859,axiom,
n9 != ssA(n6,n6) ).
cnf(u782,axiom,
ssA(n9,n6) != ssA(n9,n7) ).
cnf(u28799,axiom,
n8 != ssA(n4,n1) ).
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(u29211,axiom,
n5 != ssA(n8,n1) ).
cnf(u745,axiom,
ssA(n8,n4) != ssA(n8,n6) ).
cnf(u1822,axiom,
n4 != ssA(n9,n1) ).
cnf(u27155,axiom,
n2 != ssA(n8,n3) ).
cnf(u383,axiom,
n4 != n8 ).
cnf(u387,axiom,
n3 != n9 ).
cnf(u1616,axiom,
ssA(n7,n7) != ssA(n9,n8) ).
cnf(u992,axiom,
ssA(n1,n4) != ssA(n2,n4) ).
cnf(u1092,axiom,
ssA(n8,n7) != ssA(n9,n7) ).
cnf(u734,axiom,
ssA(n8,n7) != ssA(n8,n8) ).
cnf(u1967,axiom,
n8 != ssA(n2,n3) ).
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(u959,axiom,
ssA(n7,n4) != ssA(n8,n4) ).
cnf(u1914,axiom,
n9 != ssA(n2,n4) ).
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(u1864,axiom,
n6 != ssA(n9,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(u1831,axiom,
n4 != ssA(n1,n1) ).
cnf(u823,axiom,
ssA(n7,n1) != ssA(n9,n1) ).
cnf(u1069,axiom,
ssA(n2,n6) != ssA(n8,n6) ).
cnf(u1867,axiom,
n6 != ssA(n6,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,
n4 != ssA(n7,n2) ).
cnf(u1190,axiom,
ssA(n5,n9) != ssA(n7,n9) ).
cnf(u621,axiom,
ssA(n5,n2) != ssA(n5,n6) ).
cnf(u2008,axiom,
n5 != ssA(n8,n7) ).
cnf(u978,axiom,
ssA(n2,n4) != ssA(n9,n4) ).
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(u990,axiom,
ssA(n1,n4) != ssA(n4,n4) ).
cnf(u1711,axiom,
n8 = ssA(n4,n4) ).
cnf(u606,axiom,
ssA(n5,n5) != ssA(n5,n6) ).
cnf(u1839,axiom,
n7 != 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(u831,axiom,
ssA(n5,n1) != ssA(n6,n1) ).
cnf(u1861,axiom,
n9 != ssA(n4,n6) ).
cnf(u432,axiom,
ssA(n1,n3) != ssA(n1,n9) ).
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(u986,axiom,
ssA(n1,n4) != ssA(n8,n4) ).
cnf(u515,axiom,
ssA(n3,n5) != ssA(n3,n7) ).
cnf(u1953,axiom,
n3 != ssA(n5,n6) ).
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(u945,axiom,
ssA(n1,n3) != ssA(n4,n3) ).
cnf(u23332,axiom,
n2 != ssA(n5,n3) ).
cnf(u406,axiom,
n1 != n3 ).
cnf(u29545,axiom,
n9 = ssA(n3,n9) ).
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(u29167,axiom,
n3 != ssA(n9,n3) ).
cnf(u1304,axiom,
ssA(n1,n4) != ssA(n2,n5) ).
cnf(u1143,axiom,
ssA(n5,n8) != ssA(n9,n8) ).
cnf(u1277,axiom,
ssA(n2,n6) != ssA(n3,n4) ).
cnf(u1858,axiom,
n9 != ssA(n7,n6) ).
cnf(u1062,axiom,
ssA(n3,n6) != ssA(n9,n6) ).
cnf(u1850,axiom,
n5 != ssA(n6,n5) ).
cnf(u28958,axiom,
n3 != ssA(n2,n1) ).
cnf(u850,axiom,
ssA(n1,n1) != ssA(n9,n1) ).
cnf(u1256,axiom,
ssA(n1,n1) != ssA(n3,n2) ).
cnf(u1817,axiom,
n1 != ssA(n2,n2) ).
cnf(u1719,axiom,
n1 = ssA(n8,n4) ).
cnf(u23261,axiom,
n3 != ssA(n5,n7) ).
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(u1869,axiom,
n6 != ssA(n4,n7) ).
cnf(u692,axiom,
ssA(n7,n6) != ssA(n7,n7) ).
cnf(u1988,axiom,
n4 != ssA(n5,n8) ).
cnf(u1604,axiom,
ssA(n7,n9) != ssA(n9,n7) ).
cnf(u1939,axiom,
n9 != ssA(n6,n3) ).
cnf(u1120,axiom,
ssA(n1,n7) != ssA(n9,n7) ).
cnf(u1471,axiom,
ssA(n4,n9) != ssA(n5,n8) ).
cnf(u693,axiom,
ssA(n7,n5) != ssA(n7,n9) ).
cnf(u1902,axiom,
n2 != ssA(n4,n2) ).
cnf(u575,axiom,
ssA(n4,n2) != ssA(n4,n7) ).
cnf(u467,axiom,
ssA(n2,n6) != ssA(n2,n7) ).
cnf(u1172,axiom,
ssA(n1,n8) != ssA(n2,n8) ).
cnf(u1789,axiom,
n7 != ssA(n1,n9) ).
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,
n6 != ssA(n7,n7) ).
cnf(u508,axiom,
ssA(n3,n7) != ssA(n3,n9) ).
cnf(u1825,axiom,
n4 != ssA(n8,n1) ).
cnf(u689,axiom,
ssA(n7,n7) != ssA(n7,n8) ).
cnf(u1944,axiom,
n5 != ssA(n5,n4) ).
cnf(u571,axiom,
ssA(n4,n3) != ssA(n4,n5) ).
cnf(u479,axiom,
ssA(n2,n3) != ssA(n2,n7) ).
cnf(u1911,axiom,
n9 != ssA(n3,n4) ).
cnf(u552,axiom,
ssA(n4,n8) != ssA(n4,n9) ).
cnf(u1718,axiom,
n4 = ssA(n7,n8) ).
cnf(u1996,axiom,
n1 != ssA(n5,n4) ).
cnf(u29553,axiom,
n9 != ssA(n8,n9) ).
cnf(u1149,axiom,
ssA(n4,n8) != ssA(n7,n8) ).
cnf(u1561,axiom,
ssA(n7,n6) != ssA(n8,n5) ).
cnf(u1947,axiom,
n5 != ssA(n4,n3) ).
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,
n5 != ssA(n7,n9) ).
cnf(u1282,axiom,
ssA(n2,n4) != ssA(n3,n6) ).
cnf(u1613,axiom,
ssA(n7,n8) != ssA(n8,n7) ).
cnf(u674,axiom,
ssA(n6,n1) != ssA(n6,n5) ).
cnf(u564,axiom,
ssA(n4,n4) != ssA(n4,n7) ).
cnf(u1860,axiom,
n9 != ssA(n5,n6) ).
cnf(u29511,axiom,
n7 != ssA(n9,n6) ).
cnf(u29502,axiom,
n7 = ssA(n6,n6) ).
cnf(u27181,axiom,
n8 != ssA(n2,n1) ).
cnf(u1811,axiom,
n6 != ssA(n2,n5) ).
cnf(u1705,axiom,
n5 = ssA(n1,n5) ).
cnf(u388,axiom,
n3 != n8 ).
cnf(u565,axiom,
ssA(n4,n4) != ssA(n4,n6) ).
cnf(u697,axiom,
ssA(n7,n4) != ssA(n7,n9) ).
cnf(u1952,axiom,
n3 != ssA(n6,n4) ).
cnf(u1791,axiom,
n7 != ssA(n1,n7) ).
cnf(u1568,axiom,
ssA(n7,n5) != ssA(n8,n4) ).
cnf(u944,axiom,
ssA(n1,n3) != ssA(n5,n3) ).
cnf(u1919,axiom,
n9 != ssA(n4,n1) ).
cnf(u655,axiom,
ssA(n6,n4) != ssA(n6,n6) ).
cnf(u1379,axiom,
ssA(n4,n3) != ssA(n6,n1) ).
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(u1941,axiom,
n9 != ssA(n4,n3) ).
cnf(u1520,axiom,
ssA(n7,n2) != ssA(n9,n1) ).
cnf(u433,axiom,
ssA(n1,n3) != ssA(n1,n8) ).
cnf(u1231,axiom,
ssA(n2,n3) != ssA(n3,n2) ).
cnf(u380,axiom,
n5 != n7 ).
cnf(u384,axiom,
n4 != n7 ).
cnf(u561,axiom,
ssA(n4,n5) != ssA(n4,n6) ).
cnf(u1816,axiom,
n1 != ssA(n2,n3) ).
cnf(u1121,axiom,
ssA(n1,n7) != ssA(n8,n7) ).
cnf(u808,axiom,
ssA(n9,n1) != ssA(n9,n6) ).
cnf(u1805,axiom,
n9 != ssA(n1,n1) ).
cnf(u651,axiom,
ssA(n6,n5) != ssA(n6,n6) ).
cnf(u1868,axiom,
n6 != ssA(n5,n7) ).
cnf(u486,axiom,
ssA(n2,n2) != ssA(n2,n6) ).
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(u445,axiom,
ssA(n1,n1) != ssA(n1,n9) ).
cnf(u376,axiom,
n6 != n8 ).
cnf(u4255,axiom,
n7 != ssA(n5,n4) ).
cnf(u1142,axiom,
ssA(n6,n8) != ssA(n7,n8) ).
cnf(u573,axiom,
ssA(n4,n2) != ssA(n4,n9) ).
cnf(u7627,axiom,
n7 = ssA(n2,n8) ).
cnf(u930,axiom,
ssA(n3,n3) != ssA(n6,n3) ).
cnf(u1259,axiom,
ssA(n1,n1) != ssA(n2,n2) ).
cnf(u1171,axiom,
ssA(n1,n8) != ssA(n3,n8) ).
cnf(u1990,axiom,
n4 != ssA(n2,n8) ).
cnf(u889,axiom,
ssA(n2,n2) != ssA(n8,n2) ).
cnf(u663,axiom,
ssA(n6,n2) != ssA(n6,n9) ).
cnf(u27163,axiom,
n2 != ssA(n1,n1) ).
cnf(u1106,axiom,
ssA(n4,n7) != ssA(n5,n7) ).
cnf(u482,axiom,
ssA(n2,n3) != ssA(n2,n4) ).
cnf(u1847,axiom,
n5 != ssA(n9,n5) ).
cnf(u644,axiom,
ssA(n6,n7) != ssA(n6,n8) ).
cnf(u979,axiom,
ssA(n2,n4) != ssA(n8,n4) ).
cnf(u29232,axiom,
n6 != ssA(n9,n9) ).
cnf(u1824,axiom,
n6 != ssA(n3,n4) ).
cnf(u1200,axiom,
ssA(n3,n9) != ssA(n6,n9) ).
cnf(u1300,axiom,
ssA(n1,n4) != ssA(n3,n6) ).
cnf(u942,axiom,
ssA(n1,n3) != ssA(n7,n3) ).
cnf(u1423,axiom,
ssA(n4,n6) != ssA(n6,n5) ).
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(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(n1,n4) ).
cnf(u1103,axiom,
ssA(n4,n7) != ssA(n8,n7) ).
cnf(u991,axiom,
ssA(n1,n4) != ssA(n3,n4) ).
cnf(u1237,axiom,
ssA(n2,n1) != ssA(n3,n3) ).
cnf(u1548,axiom,
ssA(n8,n5) != ssA(n9,n6) ).
cnf(u1946,axiom,
n5 != ssA(n4,n2) ).
cnf(u1562,axiom,
ssA(n7,n6) != ssA(n8,n4) ).
cnf(u938,axiom,
ssA(n2,n3) != ssA(n4,n3) ).
cnf(u1905,axiom,
n2 != ssA(n4,n7) ).
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,
n9 != ssA(n2,n6) ).
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(u23143,axiom,
n9 != ssA(n9,n5) ).
cnf(u855,axiom,
ssA(n1,n1) != ssA(n4,n1) ).
cnf(u1101,axiom,
ssA(n5,n7) != ssA(n6,n7) ).
cnf(u987,axiom,
ssA(n1,n4) != ssA(n7,n4) ).
cnf(u1810,axiom,
n6 != ssA(n2,n4) ).
cnf(u802,axiom,
ssA(n9,n2) != ssA(n9,n5) ).
cnf(u653,axiom,
ssA(n6,n4) != ssA(n6,n8) ).
cnf(u1862,axiom,
n9 != ssA(n3,n6) ).
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(u754,axiom,
ssA(n8,n2) != ssA(n8,n8) ).
cnf(u1821,axiom,
n4 != ssA(n3,n5) ).
cnf(u969,axiom,
ssA(n4,n4) != ssA(n7,n4) ).
cnf(u516,axiom,
ssA(n3,n5) != ssA(n3,n6) ).
cnf(u1940,axiom,
n9 != ssA(n6,n2) ).
cnf(u851,axiom,
ssA(n1,n1) != ssA(n8,n1) ).
cnf(u1456,axiom,
ssA(n5,n9) != ssA(n6,n8) ).
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(u1508,axiom,
ssA(n8,n1) != ssA(n9,n2) ).
cnf(u419,axiom,
ssA(n1,n7) != ssA(n1,n8) ).
cnf(u766,axiom,
ssA(n8,n1) != ssA(n8,n3) ).
cnf(u1871,axiom,
n6 != ssA(n1,n7) ).
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(u1818,axiom,
n1 != ssA(n2,n1) ).
cnf(u1472,axiom,
ssA(n4,n9) != ssA(n5,n7) ).
cnf(u23141,axiom,
n9 = ssA(n6,n5) ).
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(u29344,axiom,
n5 = ssA(n2,n1) ).
cnf(u1201,axiom,
ssA(n3,n9) != ssA(n5,n9) ).
cnf(u1195,axiom,
ssA(n4,n9) != ssA(n6,n9) ).
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(n4,n1) ).
cnf(u712,axiom,
ssA(n7,n2) != ssA(n7,n5) ).
cnf(u397,axiom,
n2 != n5 ).
cnf(u822,axiom,
ssA(n8,n1) != ssA(n9,n1) ).
cnf(u1094,axiom,
ssA(n7,n7) != ssA(n8,n7) ).
cnf(u1303,axiom,
ssA(n1,n4) != ssA(n2,n6) ).
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(u1565,axiom,
ssA(n7,n5) != ssA(n9,n4) ).
cnf(u626,axiom,
ssA(n5,n1) != ssA(n5,n8) ).
cnf(u743,axiom,
ssA(n8,n4) != ssA(n8,n8) ).
cnf(u989,axiom,
ssA(n1,n4) != ssA(n5,n4) ).
cnf(u1812,axiom,
n1 != ssA(n2,n8) ).
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(u1152,axiom,
ssA(n3,n8) != ssA(n9,n8) ).
cnf(u1615,axiom,
ssA(n7,n7) != ssA(n9,n9) ).
cnf(u1503,axiom,
ssA(n8,n2) != ssA(n9,n3) ).
cnf(u1934,axiom,
n6 != ssA(n1,n9) ).
cnf(u607,axiom,
ssA(n5,n4) != ssA(n5,n9) ).
cnf(u853,axiom,
ssA(n1,n1) != ssA(n6,n1) ).
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(u720,axiom,
ssA(n7,n1) != ssA(n7,n4) ).
cnf(u1183,axiom,
ssA(n7,n9) != ssA(n9,n9) ).
cnf(u23259,axiom,
n3 != ssA(n8,n7) ).
cnf(u405,axiom,
n1 != n4 ).
cnf(u1067,axiom,
ssA(n3,n6) != ssA(n4,n6) ).
cnf(u1857,axiom,
n9 != ssA(n8,n6) ).
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(u491,axiom,
ssA(n2,n1) != ssA(n2,n8) ).
cnf(u963,axiom,
ssA(n5,n4) != ssA(n9,n4) ).
cnf(u1720,axiom,
n5 = ssA(n9,n7) ).
cnf(u1820,axiom,
n4 != ssA(n3,n4) ).
cnf(u1196,axiom,
ssA(n4,n9) != ssA(n5,n9) ).
cnf(u710,axiom,
ssA(n7,n2) != ssA(n7,n7) ).
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(u18224,axiom,
n5 != ssA(n5,n6) ).
cnf(u882,axiom,
ssA(n3,n2) != ssA(n9,n2) ).
cnf(u1160,axiom,
ssA(n2,n8) != ssA(n7,n8) ).
cnf(u1849,axiom,
n5 != ssA(n7,n5) ).
cnf(u733,axiom,
ssA(n8,n7) != ssA(n8,n9) ).
cnf(u29324,axiom,
n6 = ssA(n1,n3) ).
cnf(u1942,axiom,
n9 != ssA(n4,n2) ).
cnf(u29478,axiom,
n1 = ssA(n4,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,
n2 != ssA(n4,n1) ).
cnf(u931,axiom,
ssA(n3,n3) != ssA(n5,n3) ).
cnf(u1971,axiom,
n2 != ssA(n5,n9) ).
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(u804,axiom,
ssA(n9,n2) != ssA(n9,n3) ).
cnf(u536,axiom,
ssA(n3,n1) != ssA(n3,n8) ).
cnf(u597,axiom,
ssA(n5,n8) != ssA(n5,n9) ).
cnf(u1984,axiom,
n4 != ssA(n7,n5) ).
cnf(u1523,axiom,
ssA(n7,n2) != ssA(n8,n1) ).
cnf(u446,axiom,
ssA(n1,n1) != ssA(n1,n8) ).
cnf(u976,axiom,
ssA(n3,n4) != ssA(n5,n4) ).
cnf(u718,axiom,
ssA(n7,n1) != ssA(n7,n6) ).
cnf(u1951,axiom,
n3 != ssA(n6,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(u1189,axiom,
ssA(n5,n9) != ssA(n8,n9) ).
cnf(u1898,axiom,
n6 != ssA(n2,n6) ).
cnf(u465,axiom,
ssA(n2,n6) != ssA(n2,n9) ).
cnf(u890,axiom,
ssA(n2,n2) != ssA(n7,n2) ).
cnf(u1976,axiom,
n8 != ssA(n8,n1) ).
cnf(u1153,axiom,
ssA(n3,n8) != ssA(n8,n8) ).
cnf(u1592,axiom,
ssA(n8,n9) != ssA(n9,n7) ).
cnf(u1068,axiom,
ssA(n2,n6) != ssA(n9,n6) ).
cnf(u582,axiom,
ssA(n4,n1) != ssA(n4,n7) ).
cnf(u988,axiom,
ssA(n1,n4) != ssA(n6,n4) ).
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,
n2 != ssA(n2,n4) ).
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,
n4 != ssA(n4,n1) ).
cnf(u1714,axiom,
n9 = ssA(n5,n1) ).
cnf(u1814,axiom,
n1 != ssA(n2,n5) ).
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(n3,n7) ).
cnf(u852,axiom,
ssA(n1,n1) != ssA(n7,n1) ).
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,
n7 != ssA(n2,n3) ).
cnf(u803,axiom,
ssA(n9,n2) != ssA(n9,n4) ).
cnf(u1715,axiom,
n5 = ssA(n5,n2) ).
cnf(u1481,axiom,
ssA(n4,n7) != ssA(n6,n8) ).
cnf(u1280,axiom,
ssA(n2,n5) != ssA(n3,n4) ).
cnf(u1843,axiom,
n6 != ssA(n6,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(u27265,axiom,
n2 != ssA(n9,n2) ).
cnf(u1856,axiom,
n9 != ssA(n9,n6) ).
cnf(u742,axiom,
ssA(n8,n4) != ssA(n8,n9) ).
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(u2014,axiom,
n5 != ssA(n8,n9) ).
cnf(u687,axiom,
ssA(n7,n8) != ssA(n7,n9) ).
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,
n8 != ssA(n9,n2) ).
cnf(u29177,axiom,
n3 != ssA(n4,n1) ).
cnf(u1424,axiom,
ssA(n4,n6) != ssA(n6,n4) ).
cnf(u485,axiom,
ssA(n2,n2) != ssA(n2,n7) ).
cnf(u29409,axiom,
n3 != ssA(n7,n1) ).
cnf(u1848,axiom,
n5 != ssA(n8,n5) ).
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,
n1 != ssA(n1,n7) ).
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(u1483,axiom,
ssA(n4,n7) != ssA(n5,n9) ).
cnf(u664,axiom,
ssA(n6,n2) != ssA(n6,n8) ).
cnf(u1851,axiom,
n5 != ssA(n5,n5) ).
cnf(u1015,axiom,
ssA(n4,n5) != ssA(n6,n5) ).
cnf(u1970,axiom,
n2 != ssA(n6,n7) ).
cnf(u834,axiom,
ssA(n4,n1) != ssA(n7,n1) ).
cnf(u982,axiom,
ssA(n2,n4) != ssA(n5,n4) ).
cnf(u1801,axiom,
n9 != ssA(n1,n7) ).
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(u27178,axiom,
n8 != ssA(n4,n2) ).
cnf(u1981,axiom,
n2 != ssA(n5,n4) ).
cnf(u676,axiom,
ssA(n6,n1) != ssA(n6,n3) ).
cnf(u3474,axiom,
n1 != ssA(n4,n6) ).
cnf(u3471,axiom,
n1 != ssA(n8,n6) ).
cnf(u1011,axiom,
ssA(n5,n5) != ssA(n6,n5) ).
cnf(u1716,axiom,
n8 = ssA(n7,n3) ).
cnf(u1923,axiom,
n5 != ssA(n2,n6) ).
cnf(u1104,axiom,
ssA(n4,n7) != ssA(n7,n7) ).
cnf(u846,axiom,
ssA(n2,n1) != ssA(n6,n1) ).
cnf(u4257,axiom,
n7 != ssA(n2,n4) ).
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(u29364,axiom,
n3 = ssA(n5,n8) ).
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,
n2 = 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(u1845,axiom,
n6 != ssA(n4,n5) ).
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,
n2 != ssA(n1,n4) ).
cnf(u22218,axiom,
n2 != ssA(n5,n5) ).
cnf(u492,axiom,
ssA(n2,n1) != ssA(n2,n7) ).
cnf(u1809,axiom,
n6 != ssA(n2,n2) ).
cnf(u673,axiom,
ssA(n6,n1) != ssA(n6,n6) ).
cnf(u23289,axiom,
n5 != ssA(n1,n9) ).
cnf(u555,axiom,
ssA(n4,n6) != ssA(n4,n9) ).
cnf(u801,axiom,
ssA(n9,n2) != ssA(n9,n6) ).
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(u1595,axiom,
ssA(n8,n8) != ssA(n9,n7) ).
cnf(u887,axiom,
ssA(n3,n2) != ssA(n4,n2) ).
cnf(u1842,axiom,
n6 != ssA(n7,n5) ).
cnf(u29239,axiom,
n6 != ssA(n5,n8) ).
cnf(u1931,axiom,
n6 != ssA(n3,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(u1394,axiom,
ssA(n4,n1) != ssA(n5,n2) ).
cnf(u1894,axiom,
n7 != ssA(n2,n1) ).
cnf(u567,axiom,
ssA(n4,n3) != ssA(n4,n9) ).
cnf(u1097,axiom,
ssA(n6,n7) != ssA(n7,n7) ).
cnf(u2009,axiom,
n5 != ssA(n7,n7) ).
cnf(u2000,axiom,
n1 != ssA(n7,n6) ).
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(u28637,axiom,
n8 != ssA(n5,n4) ).
cnf(u1972,axiom,
n2 != ssA(n5,n7) ).
cnf(u845,axiom,
ssA(n2,n1) != ssA(n7,n1) ).
cnf(u883,axiom,
ssA(n3,n2) != ssA(n8,n2) ).
cnf(u1795,axiom,
n7 != ssA(n1,n3) ).
cnf(u1936,axiom,
n6 != ssA(n1,n8) ).
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(u767,axiom,
ssA(n8,n1) != ssA(n8,n2) ).
cnf(u29216,axiom,
n5 != ssA(n1,n3) ).
cnf(u1013,axiom,
ssA(n4,n5) != ssA(n8,n5) ).
cnf(u1210,axiom,
ssA(n1,n9) != ssA(n9,n9) ).
cnf(u1710,axiom,
n6 = ssA(n3,n5) ).
cnf(u1141,axiom,
ssA(n6,n8) != ssA(n8,n8) ).
cnf(u1925,axiom,
n5 != ssA(n2,n4) ).
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,
n9 != ssA(n1,n8) ).
cnf(u29171,axiom,
n3 != ssA(n4,n3) ).
cnf(u1105,axiom,
ssA(n4,n7) != ssA(n6,n7) ).
cnf(u1099,axiom,
ssA(n5,n7) != ssA(n8,n7) ).
cnf(u792,axiom,
ssA(n9,n3) != ssA(n9,n9) ).
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(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(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(u1803,axiom,
n9 != ssA(n1,n4) ).
cnf(u429,axiom,
ssA(n1,n4) != ssA(n1,n7) ).
cnf(u1922,axiom,
n5 != ssA(n3,n4) ).
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(u1881,axiom,
n1 != ssA(n4,n9) ).
cnf(u1597,axiom,
ssA(n8,n7) != ssA(n9,n9) ).
cnf(u1243,axiom,
ssA(n1,n3) != ssA(n3,n2) ).
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(u1844,axiom,
n6 != ssA(n5,n5) ).
cnf(u466,axiom,
ssA(n2,n6) != ssA(n2,n8) ).
cnf(u917,axiom,
ssA(n6,n3) != ssA(n7,n3) ).
cnf(u756,axiom,
ssA(n8,n2) != ssA(n8,n6) ).
cnf(u425,axiom,
ssA(n1,n5) != ssA(n1,n7) ).
cnf(u1238,axiom,
ssA(n2,n1) != ssA(n3,n2) ).
cnf(u372,axiom,
n8 != n9 ).
cnf(u1808,axiom,
n6 != ssA(n2,n1) ).
cnf(u29139,axiom,
n1 != ssA(n9,n8) ).
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(u1966,axiom,
n8 != ssA(n4,n3) ).
cnf(u885,axiom,
ssA(n3,n2) != ssA(n6,n2) ).
cnf(u399,axiom,
n2 != n3 ).
cnf(u29254,axiom,
n9 != ssA(n7,n1) ).
cnf(u478,axiom,
ssA(n2,n3) != ssA(n2,n8) ).
cnf(u620,axiom,
ssA(n5,n2) != ssA(n5,n7) ).
cnf(u1830,axiom,
n4 != ssA(n2,n1) ).
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(u27134,axiom,
n8 != ssA(n1,n1) ).
cnf(u437,axiom,
ssA(n1,n3) != ssA(n1,n4) ).
cnf(u975,axiom,
ssA(n3,n4) != ssA(n6,n4) ).
cnf(u22263,axiom,
n4 != ssA(n5,n4) ).
cnf(u1930,axiom,
n6 != ssA(n3,n9) ).
cnf(u1349,axiom,
ssA(n1,n7) != ssA(n2,n8) ).
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(u27135,axiom,
n8 != ssA(n5,n8) ).
cnf(u1484,axiom,
ssA(n4,n7) != ssA(n5,n8) ).
cnf(u881,axiom,
ssA(n4,n2) != ssA(n5,n2) ).
cnf(u395,axiom,
n2 != n7 ).
cnf(u1852,axiom,
n5 != ssA(n4,n5) ).
cnf(u1100,axiom,
ssA(n5,n7) != ssA(n7,n7) ).
cnf(u1975,axiom,
n8 != ssA(n8,n2) ).
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(u1213,axiom,
ssA(n1,n9) != ssA(n6,n9) ).
cnf(u971,axiom,
ssA(n4,n4) != ssA(n5,n4) ).
cnf(u824,axiom,
ssA(n7,n1) != ssA(n8,n1) ).
cnf(u1794,axiom,
n7 != ssA(n1,n4) ).
cnf(u2011,axiom,
n5 != ssA(n4,n7) ).
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,
n8 != ssA(n9,n1) ).
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,
n4 != ssA(n1,n8) ).
cnf(u628,axiom,
ssA(n5,n1) != ssA(n5,n6) ).
cnf(u28960,axiom,
n3 != ssA(n4,n2) ).
cnf(u835,axiom,
ssA(n4,n1) != ssA(n6,n1) ).
cnf(u983,axiom,
ssA(n2,n4) != ssA(n4,n4) ).
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,
n7 != ssA(n3,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(u1983,axiom,
n4 != ssA(n7,n7) ).
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(u1790,axiom,
n7 != 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,
n5 != ssA(n9,n4) ).
cnf(u497,axiom,
ssA(n2,n1) != ssA(n2,n2) ).
cnf(u794,axiom,
ssA(n9,n3) != ssA(n9,n7) ).
cnf(u448,axiom,
ssA(n1,n1) != ssA(n1,n6) ).
cnf(u625,axiom,
ssA(n5,n1) != ssA(n5,n9) ).
cnf(u27266,axiom,
n2 != ssA(n8,n2) ).
cnf(u1880,axiom,
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(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(u843,axiom,
ssA(n2,n1) != ssA(n9,n1) ).
cnf(u1159,axiom,
ssA(n2,n8) != ssA(n8,n8) ).
cnf(u1883,axiom,
n1 != ssA(n1,n9) ).
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(u1618,axiom,
ssA(n7,n7) != ssA(n8,n9) ).
cnf(u1049,axiom,
ssA(n7,n6) != ssA(n8,n6) ).
cnf(u1961,axiom,
n8 != ssA(n7,n5) ).
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(u1796,axiom,
n7 != ssA(n1,n1) ).
cnf(u1170,axiom,
ssA(n1,n8) != ssA(n4,n8) ).
cnf(u27267,axiom,
n2 != ssA(n7,n2) ).
cnf(u1619,axiom,
ssA(n7,n7) != ssA(n8,n8) ).
cnf(u2013,axiom,
n5 != ssA(n1,n7) ).
cnf(u708,axiom,
ssA(n7,n2) != ssA(n7,n9) ).
cnf(u1070,axiom,
ssA(n2,n6) != ssA(n7,n6) ).
cnf(u28505,axiom,
n4 != ssA(n5,n7) ).
cnf(u1888,axiom,
n7 != ssA(n3,n3) ).
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(u1855,axiom,
n5 != ssA(n2,n5) ).
cnf(u30647,axiom,
n6 = ssA(n8,n6) ).
cnf(u1877,axiom,
n1 != ssA(n8,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,
n5 != ssA(n5,n7) ).
cnf(u1002,axiom,
ssA(n8,n5) != ssA(n9,n5) ).
cnf(u1051,axiom,
ssA(n6,n6) != ssA(n8,n6) ).
cnf(u1969,axiom,
n2 != ssA(n6,n9) ).
cnf(u739,axiom,
ssA(n8,n5) != ssA(n8,n8) ).
cnf(u705,axiom,
ssA(n7,n3) != ssA(n7,n6) ).
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,
n7 = ssA(n1,n2) ).
cnf(u1804,axiom,
n9 != ssA(n1,n3) ).
cnf(u422,axiom,
ssA(n1,n6) != ssA(n1,n7) ).
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(u27131,axiom,
n8 != ssA(n1,n7) ).
cnf(u381,axiom,
n5 != n6 ).
cnf(u919,axiom,
ssA(n5,n3) != ssA(n8,n3) ).
cnf(u1165,axiom,
ssA(n1,n8) != ssA(n9,n8) ).
cnf(u23260,axiom,
n3 != ssA(n7,n7) ).
cnf(u1014,axiom,
ssA(n4,n5) != ssA(n7,n5) ).
cnf(u1833,axiom,
n7 != ssA(n8,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,
n6 != ssA(n1,n4) ).
cnf(u825,axiom,
ssA(n6,n1) != ssA(n9,n1) ).
cnf(u599,axiom,
ssA(n5,n7) != ssA(n5,n8) ).
cnf(u510,axiom,
ssA(n3,n6) != ssA(n3,n9) ).
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,
n4 != ssA(n2,n2) ).
cnf(u27179,axiom,
n8 != ssA(n2,n2) ).
cnf(u580,axiom,
ssA(n4,n1) != ssA(n4,n9) ).
cnf(u377,axiom,
n6 != n7 ).
cnf(u915,axiom,
ssA(n6,n3) != ssA(n9,n3) ).
cnf(u1955,axiom,
n8 != ssA(n6,n6) ).
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(u483,axiom,
ssA(n2,n2) != ssA(n2,n9) ).
cnf(u1712,axiom,
n3 = 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(u1935,axiom,
n1 != ssA(n1,n8) ).
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(u1882,axiom,
n1 != ssA(n3,n9) ).
cnf(u1713,axiom,
n2 = ssA(n4,n8) ).
cnf(u449,axiom,
ssA(n1,n1) != ssA(n1,n5) ).
cnf(u3475,axiom,
n1 != ssA(n2,n6) ).
cnf(u874,axiom,
ssA(n5,n2) != ssA(n8,n2) ).
cnf(u396,axiom,
n2 != n6 ).
cnf(u1841,axiom,
n6 != ssA(n8,n5) ).
cnf(u577,axiom,
ssA(n4,n2) != ssA(n4,n5) ).
cnf(u1960,axiom,
n8 != ssA(n7,n7) ).
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,
n9 != ssA(n1,n9) ).
cnf(u568,axiom,
ssA(n4,n3) != ssA(n4,n8) ).
cnf(u1334,axiom,
ssA(n1,n9) != ssA(n3,n7) ).
cnf(u1606,axiom,
ssA(n7,n9) != ssA(n8,n8) ).
cnf(u2012,axiom,
n5 != ssA(n3,n7) ).
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(u29233,axiom,
n6 != ssA(n8,n9) ).
cnf(u1963,axiom,
n8 != ssA(n7,n2) ).
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(n1,n4) ).
cnf(u836,axiom,
ssA(n4,n1) != ssA(n5,n1) ).
cnf(u7633,axiom,
n7 != ssA(n5,n8) ).
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,
n1 != ssA(n9,n9) ).
cnf(u787,axiom,
ssA(n9,n4) != ssA(n9,n9) ).
cnf(u27158,axiom,
n2 != ssA(n4,n3) ).
cnf(u1827,axiom,
n4 != ssA(n6,n1) ).
cnf(u1150,axiom,
ssA(n4,n8) != ssA(n6,n8) ).
cnf(u404,axiom,
n1 != n5 ).
cnf(u585,axiom,
ssA(n4,n1) != ssA(n4,n4) ).
cnf(u1968,axiom,
n8 != ssA(n1,n3) ).
cnf(u1216,axiom,
ssA(n1,n9) != ssA(n3,n9) ).
cnf(u3473,axiom,
n1 != ssA(n5,n6) ).
cnf(u832,axiom,
ssA(n4,n1) != ssA(n9,n1) ).
cnf(u702,axiom,
ssA(n7,n3) != ssA(n7,n9) ).
cnf(u671,axiom,
ssA(n6,n1) != ssA(n6,n8) ).
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,
n8 != ssA(n5,n6) ).
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,
n7 != ssA(n9,n2) ).
cnf(u1706,axiom,
n9 = ssA(n1,n6) ).
cnf(u1137,axiom,
ssA(n8,n8) != ssA(n9,n8) ).
cnf(u1921,axiom,
n9 != ssA(n5,n5) ).
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(u1884,axiom,
n4 != ssA(n2,n3) ).
cnf(u23288,axiom,
n5 != ssA(n1,n8) ).
cnf(u795,axiom,
ssA(n9,n3) != ssA(n9,n6) ).
cnf(u2007,axiom,
n5 != ssA(n9,n1) ).
cnf(u1707,axiom,
n6 = ssA(n2,n7) ).
cnf(u29140,axiom,
n1 != ssA(n8,n8) ).
cnf(u648,axiom,
ssA(n6,n5) != ssA(n6,n9) ).
cnf(u1111,axiom,
ssA(n3,n7) != ssA(n5,n7) ).
cnf(u1835,axiom,
n7 != ssA(n6,n2) ).
cnf(u29396,axiom,
n6 = ssA(n7,n1) ).
cnf(u1954,axiom,
n3 != ssA(n5,n4) ).
cnf(u1570,axiom,
ssA(n7,n4) != ssA(n9,n6) ).
cnf(u946,axiom,
ssA(n1,n3) != ssA(n3,n3) ).
cnf(u966,axiom,
ssA(n5,n4) != ssA(n6,n4) ).
cnf(u1913,axiom,
n9 != ssA(n2,n5) ).
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(u1122,axiom,
ssA(n1,n7) != ssA(n7,n7) ).
cnf(u1124,axiom,
ssA(n1,n7) != ssA(n5,n7) ).
cnf(u29582,axiom,
n8 = ssA(n2,n6) ).
cnf(u1571,axiom,
ssA(n7,n4) != ssA(n9,n5) ).
cnf(u1965,axiom,
n8 != ssA(n5,n3) ).
cnf(u660,axiom,
ssA(n6,n3) != ssA(n6,n6) ).
cnf(u1840,axiom,
n6 != ssA(n9,n5) ).
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(u574,axiom,
ssA(n4,n2) != ssA(n4,n8) ).
cnf(u1870,axiom,
n6 != ssA(n3,n7) ).
cnf(u789,axiom,
ssA(n9,n4) != ssA(n9,n7) ).
cnf(u431,axiom,
ssA(n1,n4) != ssA(n1,n5) ).
cnf(u27679,axiom,
n5 = ssA(n7,n6) ).
cnf(u2015,axiom,
n5 != ssA(n8,n8) ).
cnf(u524,axiom,
ssA(n3,n3) != ssA(n3,n7) ).
cnf(u656,axiom,
ssA(n6,n4) != ssA(n6,n5) ).
cnf(u23285,axiom,
n5 != ssA(n5,n8) ).
cnf(u1007,axiom,
ssA(n6,n5) != ssA(n7,n5) ).
cnf(u1962,axiom,
n8 != ssA(n7,n4) ).
cnf(u1381,axiom,
ssA(n4,n3) != ssA(n5,n2) ).
cnf(u476,axiom,
ssA(n2,n4) != ssA(n2,n5) ).
cnf(u1793,axiom,
n7 != ssA(n1,n5) ).
cnf(u657,axiom,
ssA(n6,n3) != ssA(n6,n9) ).
cnf(u570,axiom,
ssA(n4,n3) != ssA(n4,n6) ).
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(u1246,axiom,
ssA(n1,n3) != ssA(n2,n2) ).
cnf(u374,axiom,
n7 != n8 ).
cnf(u646,axiom,
ssA(n6,n6) != ssA(n6,n8) ).
cnf(u1879,axiom,
n1 != ssA(n6,n9) ).
cnf(u23335,axiom,
n2 != ssA(n4,n6) ).
cnf(u520,axiom,
ssA(n3,n4) != ssA(n3,n6) ).
cnf(u2006,axiom,
n5 != ssA(n9,n2) ).
cnf(u668,axiom,
ssA(n6,n2) != ssA(n6,n4) ).
cnf(u871,axiom,
ssA(n6,n2) != ssA(n8,n2) ).
cnf(u1003,axiom,
ssA(n7,n5) != ssA(n9,n5) ).
cnf(u1826,axiom,
n4 != ssA(n7,n1) ).
cnf(u1480,axiom,
ssA(n4,n7) != ssA(n6,n9) ).
cnf(u1708,axiom,
n1 = ssA(n2,n9) ).
cnf(u1096,axiom,
ssA(n6,n7) != ssA(n8,n7) ).
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,
n1 != ssA(n7,n9) ).
cnf(u797,axiom,
ssA(n9,n3) != ssA(n9,n4) ).
cnf(u1709,axiom,
n4 = ssA(n3,n1) ).
cnf(u916,axiom,
ssA(n6,n3) != ssA(n8,n3) ).
cnf(u642,axiom,
ssA(n6,n8) != ssA(n6,n9) ).
cnf(u1837,axiom,
n7 != ssA(n4,n2) ).
cnf(u985,axiom,
ssA(n1,n4) != ssA(n9,n4) ).
cnf(u532,axiom,
ssA(n3,n2) != ssA(n3,n5) ).
cnf(u1956,axiom,
n8 != ssA(n6,n5) ).
cnf(u867,axiom,
ssA(n8,n2) != ssA(n9,n2) ).
cnf(u28867,axiom,
n7 = ssA(n5,n9) ).
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,
n9 != ssA(n5,n4) ).
cnf(u1073,axiom,
ssA(n2,n6) != ssA(n4,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(u1887,axiom,
n4 != 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(u23144,axiom,
n9 != ssA(n8,n5) ).
cnf(u879,axiom,
ssA(n4,n2) != ssA(n7,n2) ).
cnf(u1125,axiom,
ssA(n1,n7) != ssA(n4,n7) ).
cnf(u1834,axiom,
n7 != ssA(n7,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(u1211,axiom,
ssA(n1,n9) != ssA(n8,n9) ).
cnf(u2001,axiom,
n1 != ssA(n7,n5) ).
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(u31726,axiom,
n9 = ssA(n9,n4) ).
cnf(u1558,axiom,
ssA(n7,n6) != ssA(n9,n5) ).
cnf(u1964,axiom,
n8 != ssA(n7,n1) ).
cnf(u875,axiom,
ssA(n5,n2) != ssA(n7,n2) ).
cnf(u1191,axiom,
ssA(n5,n9) != ssA(n6,n9) ).
cnf(u1915,axiom,
n5 != ssA(n3,n6) ).
cnf(u1110,axiom,
ssA(n3,n7) != ssA(n6,n7) ).
cnf(u541,axiom,
ssA(n3,n1) != ssA(n3,n3) ).
cnf(u1928,axiom,
n1 != ssA(n3,n8) ).
cnf(u1865,axiom,
n6 != ssA(n8,n7) ).
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,
n4 != ssA(n5,n1) ).
cnf(u1202,axiom,
ssA(n3,n9) != ssA(n4,n9) ).
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(u29426,axiom,
n6 != ssA(n4,n1) ).
cnf(u1792,axiom,
n7 != ssA(n1,n6) ).
cnf(u1168,axiom,
ssA(n1,n8) != ssA(n6,n8) ).
cnf(u1815,axiom,
n1 != ssA(n2,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(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(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(u29512,axiom,
n7 != ssA(n8,n6) ).
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,
n7 != ssA(n5,n2) ).
cnf(u1212,axiom,
ssA(n1,n9) != ssA(n7,n9) ).
cnf(u1959,axiom,
n8 != ssA(n7,n8) ).
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) ).
cnf(u1325,axiom,
ssA(n2,n8) != ssA(n3,n7) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ070+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.39 % Computer : n018.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sun Sep 27 22:41:39 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.42 Running first-order model finding
% 0.13/0.42 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.31/0.79 % (2801063)Will run a generic schedule for satisfiability detection.
% 1.31/0.79 % (2801070)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1064991801:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.31/0.79 % (2801069)% WARNING: option uhcvi not known.
% 1.31/0.79 % (2801068)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=946184281_2999 on theBenchmark for (2999ds/0Mi)
% 1.31/0.79 % (2801069)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3804887702:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.31/0.79 % (2801071)dis+10_1_sil=32000:sp=arity:random_seed=1688022406:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.31/0.79 % (2801072)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=821485372:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.31/0.79 % (2801073)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3073284160:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.31/0.79 % (2801074)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3145462603:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.31/0.79 % (2801071)Instruction limit reached!
% 1.31/0.79 % (2801071)------------------------------
% 1.31/0.79 % (2801071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.79 % (2801071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.79 % (2801071)CaDiCaL version: 2.1.3
% 1.31/0.79 % (2801071)Termination reason: Instruction limit
% 1.31/0.79 % (2801071)Termination phase: Saturation
% 1.31/0.79 % (2801071)Time elapsed: 0.048 s
% 1.31/0.79 % (2801071)Peak memory usage: 14 MB
% 1.31/0.79 % (2801071)Instructions burned: 103 (million)
% 1.31/0.79 % (2801072)Instruction limit reached!
% 1.31/0.79 % (2801072)------------------------------
% 1.31/0.79 % (2801072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.79 % (2801072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.79 % (2801072)CaDiCaL version: 2.1.3
% 1.31/0.79 % (2801072)Termination reason: Instruction limit
% 1.31/0.79 % (2801072)Termination phase: Saturation
% 1.31/0.79 % (2801072)Time elapsed: 0.050 s
% 1.31/0.79 % (2801072)Peak memory usage: 13 MB
% 1.31/0.79 % (2801072)Instructions burned: 117 (million)
% 1.31/0.79 % (2801073)Instruction limit reached!
% 1.31/0.79 % (2801073)------------------------------
% 1.31/0.79 % (2801073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.79 % (2801073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.79 % (2801073)CaDiCaL version: 2.1.3
% 1.31/0.79 % (2801073)Termination reason: Instruction limit
% 1.31/0.79 % (2801073)Termination phase: Saturation
% 1.31/0.79 % (2801073)Time elapsed: 0.052 s
% 1.31/0.79 % (2801073)Peak memory usage: 12 MB
% 1.31/0.79 % (2801073)Instructions burned: 132 (million)
% 1.31/0.79 % (2801082)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4127316801:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 1.31/0.79 % (2801083)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=941204028:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.31/0.79 % (2801084)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=3126010556:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.31/0.79 % (2801074)Instruction limit reached!
% 1.31/0.79 % (2801074)------------------------------
% 1.31/0.79 % (2801074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.79 % (2801074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.79 % (2801074)CaDiCaL version: 2.1.3
% 1.31/0.79 % (2801074)Termination reason: Instruction limit
% 1.31/0.79 % (2801074)Termination phase: Saturation
% 1.31/0.79 % (2801074)Time elapsed: 0.075 s
% 1.31/0.79 % (2801074)Peak memory usage: 15 MB
% 1.31/0.79 % (2801074)Instructions burned: 159 (million)
% 1.31/0.79 % (2801088)ott-21_1_sil=16000:fs=off:random_seed=2216977779:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.31/0.79 % (2801083)Instruction limit reached!
% 1.31/0.79 % (2801083)------------------------------
% 1.31/0.79 % (2801083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.79 % (2801083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.79 % (2801083)CaDiCaL version: 2.1.3
% 1.31/0.79 % (2801083)Termination reason: Instruction limit
% 1.31/0.79 % (2801083)Termination phase: Saturation
% 1.31/0.79 % (2801083)Time elapsed: 0.057 s
% 1.31/0.79 % (2801083)Peak memory usage: 14 MB
% 1.31/0.79 % (2801083)Instructions burned: 133 (million)
% 1.31/0.79 % (2801090)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3510418959:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 1.31/0.79 % (2801088)Instruction limit reached!
% 1.31/0.79 % (2801088)------------------------------
% 1.31/0.79 % (2801088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.79 % (2801088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.79 % (2801088)CaDiCaL version: 2.1.3
% 1.31/0.79 % (2801088)Termination reason: Instruction limit
% 1.31/0.79 % (2801088)Termination phase: Saturation
% 1.31/0.79 % (2801088)Time elapsed: 0.075 s
% 1.31/0.79 % (2801088)Peak memory usage: 12 MB
% 1.31/0.79 % (2801088)Instructions burned: 182 (million)
% 1.31/0.79 % Detected minimum model sizes of [9]
% 1.31/0.79 % Detected maximum model sizes of [max]
% 1.31/0.79 % TRYING [9]
% 1.31/0.79 % (2801092)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2154620466:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 1.31/0.79 % Detected minimum model sizes of [9]
% 1.31/0.79 % Detected maximum model sizes of [max]
% 1.31/0.79 % TRYING [9]
% 1.31/0.79 % (2801070) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2801063-2801070"...
% 1.31/0.79 % (2801070)...printing done.
% 1.31/0.79 % SZS status Satisfiable for theBenchmark
% 1.31/0.79 % SZS output start Saturation.
% See solution above
% 1.31/0.81 % SZS output start Definitions and Model Updates.
% 1.31/0.81 for all inputs,
% 1.31/0.81 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.31/0.81 % SZS output end Definitions and Model Updates.
% 1.31/0.81 % (2801070)------------------------------
% 1.31/0.81 % (2801070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.81 % (2801070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.81 % (2801070)CaDiCaL version: 2.1.3
% 1.31/0.81 % (2801070)Termination reason: Satisfiable
% 1.31/0.81 % (2801070)Time elapsed: 0.288 s
% 1.31/0.81 % (2801070)Peak memory usage: 19 MB
% 1.31/0.81 % (2801070)Instructions burned: 1025 (million)
% 1.31/0.81 % (2801063)Success in time 0.363 s
% 1.31/0.81 % Vampire exiting
%------------------------------------------------------------------------------