%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PUZ068+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 : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:32:08 PM UTC 2026
% Result : Satisfiable 1.74s 0.72s
% Output : Saturation 1.74s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u2026,axiom,
n2 != ssA(n1,n9) ).
cnf(u2031,axiom,
n2 = ssA(n1,n8) ).
cnf(u2034,axiom,
n2 != ssA(n1,n3) ).
cnf(u2038,axiom,
n2 != ssA(n1,n2) ).
cnf(u2042,axiom,
n2 != ssA(n1,n1) ).
cnf(u2132,axiom,
n6 != ssA(n1,n8) ).
cnf(u2137,axiom,
n6 = ssA(n1,n3) ).
cnf(u2140,axiom,
n6 != ssA(n1,n2) ).
cnf(u2239,axiom,
n1 != ssA(n2,n6) ).
cnf(u2243,axiom,
n1 != ssA(n2,n5) ).
cnf(u2248,axiom,
n1 = ssA(n2,n3) ).
cnf(u2295,axiom,
n3 != ssA(n2,n9) ).
cnf(u2299,axiom,
n3 != ssA(n2,n8) ).
cnf(u2303,axiom,
n3 != ssA(n2,n7) ).
cnf(u2307,axiom,
n3 != ssA(n2,n6) ).
cnf(u2312,axiom,
n3 = ssA(n2,n5) ).
cnf(u2422,axiom,
n4 != ssA(n2,n8) ).
cnf(u2427,axiom,
n4 = ssA(n2,n7) ).
cnf(u2430,axiom,
n4 != ssA(n2,n1) ).
cnf(u2482,axiom,
n6 != ssA(n2,n9) ).
cnf(u2487,axiom,
n6 = ssA(n2,n8) ).
cnf(u2490,axiom,
n6 != ssA(n2,n7) ).
cnf(u2494,axiom,
n6 != ssA(n2,n6) ).
cnf(u2562,axiom,
n7 != ssA(n2,n9) ).
cnf(u2566,axiom,
n7 != ssA(n2,n8) ).
cnf(u2570,axiom,
n7 != ssA(n2,n7) ).
cnf(u3009,axiom,
n8 != ssA(n2,n3) ).
cnf(u3013,axiom,
n8 != ssA(n2,n1) ).
cnf(u3149,axiom,
n8 != ssA(n1,n3) ).
cnf(u3154,axiom,
n8 = ssA(n1,n1) ).
cnf(u3617,axiom,
n1 != ssA(n3,n6) ).
cnf(u3621,axiom,
n1 != ssA(n3,n5) ).
cnf(u3626,axiom,
n1 = ssA(n3,n4) ).
cnf(u3665,axiom,
n2 != ssA(n3,n8) ).
cnf(u3669,axiom,
n2 != ssA(n3,n7) ).
cnf(u3674,axiom,
n2 = ssA(n3,n3) ).
cnf(u3677,axiom,
n2 != ssA(n3,n1) ).
cnf(u3778,axiom,
n5 != ssA(n3,n6) ).
cnf(u3782,axiom,
n5 != ssA(n3,n5) ).
cnf(u3873,axiom,
n6 = ssA(n3,n6) ).
cnf(u3876,axiom,
n6 != ssA(n3,n5) ).
cnf(u3880,axiom,
n6 != ssA(n3,n3) ).
cnf(u4077,axiom,
n2 = ssA(n4,n9) ).
cnf(u4080,axiom,
n2 != ssA(n4,n6) ).
cnf(u4084,axiom,
n2 != ssA(n4,n3) ).
cnf(u4272,axiom,
n1 = ssA(n5,n9) ).
cnf(u4275,axiom,
n1 != ssA(n5,n8) ).
cnf(u4279,axiom,
n1 != ssA(n5,n5) ).
cnf(u4283,axiom,
n1 != ssA(n5,n2) ).
cnf(u4368,axiom,
n2 != ssA(n5,n9) ).
cnf(u4372,axiom,
n2 != ssA(n5,n8) ).
cnf(u4376,axiom,
n2 != ssA(n5,n7) ).
cnf(u4381,axiom,
n2 = ssA(n5,n5) ).
cnf(u4384,axiom,
n2 != ssA(n5,n1) ).
cnf(u4433,axiom,
n5 != ssA(n5,n5) ).
cnf(u4437,axiom,
n5 != ssA(n5,n4) ).
cnf(u4540,axiom,
n8 != ssA(n4,n8) ).
cnf(u4545,axiom,
n8 = ssA(n4,n2) ).
cnf(u4597,axiom,
n4 = ssA(n4,n8) ).
cnf(u4600,axiom,
n4 != ssA(n4,n6) ).
cnf(u4651,axiom,
n6 != ssA(n5,n8) ).
cnf(u4655,axiom,
n6 != ssA(n5,n7) ).
cnf(u4660,axiom,
n6 = ssA(n5,n4) ).
cnf(u4850,axiom,
n7 != ssA(n5,n7) ).
cnf(u4854,axiom,
n7 != ssA(n5,n4) ).
cnf(u4966,axiom,
n8 != ssA(n5,n7) ).
cnf(u4970,axiom,
n8 != ssA(n5,n4) ).
cnf(u5028,axiom,
n1 != ssA(n6,n9) ).
cnf(u5032,axiom,
n1 != ssA(n6,n5) ).
cnf(u5036,axiom,
n1 != ssA(n6,n3) ).
cnf(u5041,axiom,
n1 = ssA(n6,n2) ).
cnf(u5044,axiom,
n1 != ssA(n6,n1) ).
cnf(u5156,axiom,
n2 != ssA(n6,n9) ).
cnf(u5160,axiom,
n2 != ssA(n6,n7) ).
cnf(u5164,axiom,
n2 != ssA(n6,n6) ).
cnf(u5168,axiom,
n2 != ssA(n6,n5) ).
cnf(u5172,axiom,
n2 != ssA(n6,n4) ).
cnf(u5176,axiom,
n2 != ssA(n6,n3) ).
cnf(u5181,axiom,
n2 = ssA(n6,n1) ).
cnf(u5437,axiom,
n3 != ssA(n6,n9) ).
cnf(u5442,axiom,
n3 = ssA(n6,n7) ).
cnf(u5445,axiom,
n3 != ssA(n6,n6) ).
cnf(u5449,axiom,
n3 != ssA(n6,n5) ).
cnf(u5453,axiom,
n3 != ssA(n6,n4) ).
cnf(u5457,axiom,
n3 != ssA(n6,n3) ).
cnf(u5519,axiom,
n4 != ssA(n6,n6) ).
cnf(u5524,axiom,
n4 = ssA(n6,n5) ).
cnf(u5527,axiom,
n4 != ssA(n6,n3) ).
cnf(u5572,axiom,
n6 = ssA(n6,n9) ).
cnf(u5575,axiom,
n6 != ssA(n6,n5) ).
cnf(u5579,axiom,
n6 != ssA(n6,n4) ).
cnf(u5704,axiom,
n9 != ssA(n5,n5) ).
cnf(u5708,axiom,
n9 != ssA(n5,n4) ).
cnf(u6358,axiom,
n4 != ssA(n6,n7) ).
cnf(u6362,axiom,
n4 != ssA(n6,n1) ).
cnf(u6594,axiom,
n6 != ssA(n6,n6) ).
cnf(u6598,axiom,
n6 != ssA(n6,n1) ).
cnf(u7200,axiom,
n5 = ssA(n3,n7) ).
cnf(u7203,axiom,
n5 != ssA(n3,n4) ).
cnf(u7224,axiom,
n7 != ssA(n3,n3) ).
cnf(u7228,axiom,
n7 != ssA(n3,n1) ).
cnf(u7418,axiom,
n7 != ssA(n6,n4) ).
cnf(u7422,axiom,
n7 != ssA(n6,n1) ).
cnf(u8139,axiom,
n7 = ssA(n6,n6) ).
cnf(u8142,axiom,
n7 != ssA(n6,n3) ).
cnf(u9885,axiom,
n6 != ssA(n1,n1) ).
cnf(u10613,axiom,
n8 = ssA(n6,n4) ).
cnf(u10616,axiom,
n8 != ssA(n6,n3) ).
cnf(u10773,axiom,
n1 = ssA(n7,n6) ).
cnf(u10776,axiom,
n1 != ssA(n7,n5) ).
cnf(u10905,axiom,
n2 != ssA(n7,n9) ).
cnf(u10910,axiom,
n2 = ssA(n7,n7) ).
cnf(u10913,axiom,
n2 != ssA(n7,n2) ).
cnf(u10991,axiom,
n5 = ssA(n7,n9) ).
cnf(u10994,axiom,
n5 != ssA(n7,n5) ).
cnf(u10998,axiom,
n5 != ssA(n7,n3) ).
cnf(u11036,axiom,
n6 = ssA(n7,n5) ).
cnf(u11039,axiom,
n6 != ssA(n7,n3) ).
cnf(u11043,axiom,
n6 != ssA(n7,n1) ).
cnf(u11077,axiom,
n8 = ssA(n7,n3) ).
cnf(u11080,axiom,
n8 != ssA(n7,n1) ).
cnf(u11763,axiom,
n2 != ssA(n8,n9) ).
cnf(u11767,axiom,
n2 != ssA(n8,n8) ).
cnf(u11771,axiom,
n2 != ssA(n8,n7) ).
cnf(u11775,axiom,
n2 != ssA(n8,n6) ).
cnf(u11779,axiom,
n2 != ssA(n8,n5) ).
cnf(u11783,axiom,
n2 != ssA(n8,n4) ).
cnf(u11787,axiom,
n2 != ssA(n8,n3) ).
cnf(u11792,axiom,
n2 = ssA(n8,n2) ).
cnf(u11976,axiom,
n3 != ssA(n8,n9) ).
cnf(u11980,axiom,
n3 != ssA(n8,n8) ).
cnf(u11984,axiom,
n3 != ssA(n8,n6) ).
cnf(u11988,axiom,
n3 != ssA(n8,n5) ).
cnf(u11993,axiom,
n3 = ssA(n8,n4) ).
cnf(u11996,axiom,
n3 != ssA(n8,n3) ).
cnf(u12114,axiom,
n4 = ssA(n8,n6) ).
cnf(u12117,axiom,
n4 != ssA(n8,n3) ).
cnf(u12154,axiom,
n5 != ssA(n8,n9) ).
cnf(u12158,axiom,
n5 != ssA(n8,n7) ).
cnf(u12162,axiom,
n5 != ssA(n8,n5) ).
cnf(u12167,axiom,
n5 = ssA(n8,n3) ).
cnf(u12228,axiom,
n6 != ssA(n8,n8) ).
cnf(u12233,axiom,
n6 = ssA(n8,n7) ).
cnf(u12236,axiom,
n6 != ssA(n8,n5) ).
cnf(u12302,axiom,
n7 = ssA(n8,n9) ).
cnf(u12305,axiom,
n7 != ssA(n8,n8) ).
cnf(u12935,axiom,
n8 != ssA(n8,n8) ).
cnf(u12939,axiom,
n8 != ssA(n8,n7) ).
cnf(u12943,axiom,
n8 != ssA(n8,n3) ).
cnf(u13206,axiom,
n9 = ssA(n8,n8) ).
cnf(u13209,axiom,
n9 != ssA(n8,n5) ).
cnf(u13382,axiom,
n1 = ssA(n9,n8) ).
cnf(u13385,axiom,
n1 != ssA(n9,n6) ).
cnf(u13389,axiom,
n1 != ssA(n9,n5) ).
cnf(u13393,axiom,
n1 != ssA(n9,n4) ).
cnf(u13397,axiom,
n1 != ssA(n9,n3) ).
cnf(u13401,axiom,
n1 != ssA(n9,n2) ).
cnf(u13405,axiom,
n1 != ssA(n9,n1) ).
cnf(u13602,axiom,
n2 != ssA(n9,n7) ).
cnf(u13607,axiom,
n2 = ssA(n9,n6) ).
cnf(u13610,axiom,
n2 != ssA(n9,n5) ).
cnf(u13614,axiom,
n2 != ssA(n9,n4) ).
cnf(u13618,axiom,
n2 != ssA(n9,n3) ).
cnf(u13622,axiom,
n2 != ssA(n9,n2) ).
cnf(u13626,axiom,
n2 != ssA(n9,n1) ).
cnf(u13821,axiom,
n3 != ssA(n9,n7) ).
cnf(u13825,axiom,
n3 != ssA(n9,n5) ).
cnf(u13829,axiom,
n3 != ssA(n9,n4) ).
cnf(u13833,axiom,
n3 != ssA(n9,n3) ).
cnf(u13837,axiom,
n3 != ssA(n9,n2) ).
cnf(u13842,axiom,
n3 = ssA(n9,n1) ).
cnf(u13939,axiom,
n5 != ssA(n9,n7) ).
cnf(u13944,axiom,
n5 = ssA(n9,n5) ).
cnf(u13947,axiom,
n5 != ssA(n9,n4) ).
cnf(u13951,axiom,
n5 != ssA(n9,n3) ).
cnf(u14087,axiom,
n6 != ssA(n9,n7) ).
cnf(u14091,axiom,
n6 != ssA(n9,n4) ).
cnf(u14095,axiom,
n6 != ssA(n9,n3) ).
cnf(u14100,axiom,
n6 = ssA(n9,n2) ).
cnf(u14251,axiom,
n7 != ssA(n9,n7) ).
cnf(u14255,axiom,
n7 != ssA(n9,n4) ).
cnf(u14260,axiom,
n7 = ssA(n9,n3) ).
cnf(u14353,axiom,
n8 = ssA(n9,n7) ).
cnf(u14356,axiom,
n8 != ssA(n9,n4) ).
cnf(u1823,axiom,
n4 != ssA(n4,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,
n5 != ssA(n6,n4) ).
cnf(u631,axiom,
ssA(n5,n1) != ssA(n5,n3) ).
cnf(u1161,axiom,
ssA(n2,n8) != ssA(n6,n8) ).
cnf(u4192,axiom,
n5 = ssA(n4,n4) ).
cnf(u391,axiom,
n3 != n5 ).
cnf(u697,axiom,
ssA(n7,n4) != ssA(n7,n9) ).
cnf(u1074,axiom,
ssA(n2,n6) != ssA(n3,n6) ).
cnf(u1076,axiom,
ssA(n1,n6) != ssA(n8,n6) ).
cnf(u722,axiom,
ssA(n7,n1) != ssA(n7,n2) ).
cnf(u1289,axiom,
ssA(n1,n6) != ssA(n3,n4) ).
cnf(u1917,axiom,
n6 != ssA(n6,n3) ).
cnf(u612,axiom,
ssA(n5,n3) != ssA(n5,n9) ).
cnf(u947,axiom,
ssA(n1,n3) != ssA(n2,n3) ).
cnf(u967,axiom,
ssA(n4,n4) != ssA(n9,n4) ).
cnf(u1859,axiom,
n1 != ssA(n3,n7) ).
cnf(u782,axiom,
ssA(n9,n6) != ssA(n9,n7) ).
cnf(u1182,axiom,
ssA(n8,n9) != ssA(n9,n9) ).
cnf(u613,axiom,
ssA(n5,n3) != ssA(n5,n8) ).
cnf(u1322,axiom,
ssA(n2,n9) != ssA(n3,n7) ).
cnf(u1822,axiom,
n4 != ssA(n5,n4) ).
cnf(u1476,axiom,
ssA(n4,n8) != ssA(n5,n9) ).
cnf(u383,axiom,
n4 != n8 ).
cnf(u387,axiom,
n3 != n9 ).
cnf(u1987,axiom,
n1 != ssA(n7,n1) ).
cnf(u1616,axiom,
ssA(n7,n7) != ssA(n9,n8) ).
cnf(u1092,axiom,
ssA(n8,n7) != ssA(n9,n7) ).
cnf(u734,axiom,
ssA(n8,n7) != ssA(n8,n8) ).
cnf(u1967,axiom,
n5 != ssA(n2,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(u12652,axiom,
n7 != ssA(n8,n4) ).
cnf(u1071,axiom,
ssA(n2,n6) != ssA(n6,n6) ).
cnf(u564,axiom,
ssA(n4,n4) != ssA(n4,n7) ).
cnf(u959,axiom,
ssA(n7,n4) != ssA(n8,n4) ).
cnf(u1205,axiom,
ssA(n2,n9) != ssA(n7,n9) ).
cnf(u1914,axiom,
n1 != ssA(n2,n9) ).
cnf(u1333,axiom,
ssA(n1,n9) != ssA(n3,n8) ).
cnf(u481,axiom,
ssA(n2,n3) != ssA(n2,n5) ).
cnf(u9693,axiom,
n6 != ssA(n7,n9) ).
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,
n8 != ssA(n7,n9) ).
cnf(u1468,axiom,
ssA(n4,n9) != ssA(n6,n8) ).
cnf(u379,axiom,
n5 != n8 ).
cnf(u1169,axiom,
ssA(n1,n8) != ssA(n5,n8) ).
cnf(u1163,axiom,
ssA(n2,n8) != ssA(n4,n8) ).
cnf(u856,axiom,
ssA(n1,n1) != ssA(n3,n1) ).
cnf(u598,axiom,
ssA(n5,n7) != ssA(n5,n9) ).
cnf(u1004,axiom,
ssA(n7,n5) != ssA(n8,n5) ).
cnf(u6476,axiom,
n3 != ssA(n5,n9) ).
cnf(u1831,axiom,
n7 != ssA(n5,n5) ).
cnf(u1291,axiom,
ssA(n1,n6) != ssA(n2,n5) ).
cnf(u8206,axiom,
n7 != ssA(n6,n2) ).
cnf(u823,axiom,
ssA(n7,n1) != ssA(n9,n1) ).
cnf(u1069,axiom,
ssA(n2,n6) != ssA(n8,n6) ).
cnf(u8209,axiom,
n7 != ssA(n7,n6) ).
cnf(u1867,axiom,
n8 != ssA(n4,n9) ).
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,
n1 != ssA(n8,n4) ).
cnf(u1190,axiom,
ssA(n5,n9) != ssA(n7,n9) ).
cnf(u621,axiom,
ssA(n5,n2) != ssA(n5,n6) ).
cnf(u2008,axiom,
n4 != ssA(n4,n9) ).
cnf(u978,axiom,
ssA(n2,n4) != ssA(n9,n4) ).
cnf(u1945,axiom,
n3 != ssA(n5,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(u9133,axiom,
n1 != ssA(n1,n2) ).
cnf(u1997,axiom,
n4 != ssA(n9,n7) ).
cnf(u489,axiom,
ssA(n2,n2) != ssA(n2,n3) ).
cnf(u14313,axiom,
n7 != ssA(n9,n1) ).
cnf(u896,axiom,
ssA(n1,n2) != ssA(n8,n2) ).
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(u1711,axiom,
n6 = ssA(n4,n1) ).
cnf(u1436,axiom,
ssA(n4,n4) != ssA(n6,n5) ).
cnf(u1171,axiom,
ssA(n1,n8) != ssA(n3,n8) ).
cnf(u606,axiom,
ssA(n5,n5) != ssA(n5,n6) ).
cnf(u703,axiom,
ssA(n7,n3) != ssA(n7,n8) ).
cnf(u707,axiom,
ssA(n7,n3) != ssA(n7,n4) ).
cnf(u1146,axiom,
ssA(n5,n8) != ssA(n6,n8) ).
cnf(u394,axiom,
n2 != n8 ).
cnf(u831,axiom,
ssA(n5,n1) != ssA(n6,n1) ).
cnf(u1077,axiom,
ssA(n1,n6) != ssA(n7,n6) ).
cnf(u1861,axiom,
n6 != ssA(n4,n4) ).
cnf(u432,axiom,
ssA(n1,n3) != ssA(n1,n9) ).
cnf(u1994,axiom,
n1 != ssA(n7,n2) ).
cnf(u1413,axiom,
ssA(n5,n5) != ssA(n6,n6) ).
cnf(u1340,axiom,
ssA(n1,n8) != ssA(n3,n7) ).
cnf(u1610,axiom,
ssA(n7,n8) != ssA(n9,n7) ).
cnf(u515,axiom,
ssA(n3,n5) != ssA(n3,n7) ).
cnf(u1953,axiom,
n3 != ssA(n4,n4) ).
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(u406,axiom,
n1 != n3 ).
cnf(u1164,axiom,
ssA(n2,n8) != ssA(n3,n8) ).
cnf(u827,axiom,
ssA(n6,n1) != ssA(n7,n1) ).
cnf(u10855,axiom,
n6 != ssA(n7,n6) ).
cnf(u1611,axiom,
ssA(n7,n8) != ssA(n8,n9) ).
cnf(u1143,axiom,
ssA(n5,n8) != ssA(n9,n8) ).
cnf(u1277,axiom,
ssA(n2,n6) != ssA(n3,n4) ).
cnf(u1858,axiom,
n1 != ssA(n4,n7) ).
cnf(u1062,axiom,
ssA(n3,n6) != ssA(n9,n6) ).
cnf(u10878,axiom,
n9 != ssA(n7,n5) ).
cnf(u850,axiom,
ssA(n1,n1) != ssA(n9,n1) ).
cnf(u1817,axiom,
n2 != ssA(n3,n4) ).
cnf(u1719,axiom,
n1 = ssA(n8,n1) ).
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(u10490,axiom,
n6 != ssA(n3,n4) ).
cnf(u692,axiom,
ssA(n7,n6) != ssA(n7,n7) ).
cnf(u1988,axiom,
n1 != ssA(n5,n1) ).
cnf(u899,axiom,
ssA(n1,n2) != ssA(n5,n2) ).
cnf(u1604,axiom,
ssA(n7,n9) != ssA(n9,n7) ).
cnf(u1939,axiom,
n4 != ssA(n1,n3) ).
cnf(u1471,axiom,
ssA(n4,n9) != ssA(n5,n8) ).
cnf(u693,axiom,
ssA(n7,n5) != ssA(n7,n9) ).
cnf(u575,axiom,
ssA(n4,n2) != ssA(n4,n7) ).
cnf(u14534,axiom,
n9 = ssA(n9,n4) ).
cnf(u467,axiom,
ssA(n2,n6) != ssA(n2,n7) ).
cnf(u1172,axiom,
ssA(n1,n8) != ssA(n2,n8) ).
cnf(u1789,axiom,
n4 != ssA(n1,n2) ).
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,
n8 != ssA(n5,n9) ).
cnf(u508,axiom,
ssA(n3,n7) != ssA(n3,n9) ).
cnf(u689,axiom,
ssA(n7,n7) != ssA(n7,n8) ).
cnf(u1944,axiom,
n3 != ssA(n5,n5) ).
cnf(u10491,axiom,
n6 != ssA(n4,n6) ).
cnf(u571,axiom,
ssA(n4,n3) != ssA(n4,n5) ).
cnf(u479,axiom,
ssA(n2,n3) != ssA(n2,n7) ).
cnf(u552,axiom,
ssA(n4,n8) != ssA(n4,n9) ).
cnf(u1718,axiom,
n3 = ssA(n7,n8) ).
cnf(u1996,axiom,
n4 != ssA(n9,n8) ).
cnf(u1149,axiom,
ssA(n4,n8) != ssA(n7,n8) ).
cnf(u1808,axiom,
n5 != ssA(n6,n2) ).
cnf(u1947,axiom,
n3 != ssA(n5,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(u1439,axiom,
ssA(n4,n4) != ssA(n5,n5) ).
cnf(u701,axiom,
ssA(n7,n4) != ssA(n7,n5) ).
cnf(u1113,axiom,
ssA(n2,n7) != ssA(n9,n7) ).
cnf(u1613,axiom,
ssA(n7,n8) != ssA(n8,n7) ).
cnf(u674,axiom,
ssA(n6,n1) != ssA(n6,n5) ).
cnf(u643,axiom,
ssA(n6,n7) != ssA(n6,n9) ).
cnf(u1017,axiom,
ssA(n3,n5) != ssA(n9,n5) ).
cnf(u4939,axiom,
n7 != ssA(n1,n2) ).
cnf(u1860,axiom,
n1 != ssA(n2,n7) ).
cnf(u11504,axiom,
n9 = ssA(n6,n3) ).
cnf(u1811,axiom,
n5 != ssA(n3,n2) ).
cnf(u1705,axiom,
n7 = ssA(n1,n5) ).
cnf(u388,axiom,
n3 != n8 ).
cnf(u1343,axiom,
ssA(n1,n8) != ssA(n2,n7) ).
cnf(u565,axiom,
ssA(n4,n4) != ssA(n4,n6) ).
cnf(u1952,axiom,
n3 != ssA(n1,n6) ).
cnf(u1839,axiom,
n3 != ssA(n3,n1) ).
cnf(u1791,axiom,
n7 != ssA(n1,n1) ).
cnf(u1568,axiom,
ssA(n7,n5) != ssA(n8,n4) ).
cnf(u944,axiom,
ssA(n1,n3) != ssA(n5,n3) ).
cnf(u1919,axiom,
n6 != ssA(n5,n3) ).
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(u8123,axiom,
n5 != ssA(n7,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,
n2 != ssA(n4,n4) ).
cnf(u1115,axiom,
ssA(n2,n7) != ssA(n7,n7) ).
cnf(u11508,axiom,
n9 != ssA(n8,n3) ).
cnf(u808,axiom,
ssA(n9,n1) != ssA(n9,n6) ).
cnf(u12654,axiom,
n7 != ssA(n8,n2) ).
cnf(u1805,axiom,
n5 != ssA(n9,n2) ).
cnf(u651,axiom,
ssA(n6,n5) != ssA(n6,n6) ).
cnf(u897,axiom,
ssA(n1,n2) != ssA(n7,n2) ).
cnf(u385,axiom,
n4 != n6 ).
cnf(u486,axiom,
ssA(n2,n2) != ssA(n2,n6) ).
cnf(u1244,axiom,
ssA(n1,n3) != ssA(n3,n1) ).
cnf(u779,axiom,
ssA(n9,n7) != ssA(n9,n8) ).
cnf(u760,axiom,
ssA(n8,n1) != ssA(n8,n9) ).
cnf(u1095,axiom,
ssA(n6,n7) != ssA(n9,n7) ).
cnf(u1819,axiom,
n4 != ssA(n8,n4) ).
cnf(u445,axiom,
ssA(n1,n1) != ssA(n1,n9) ).
cnf(u376,axiom,
n6 != n8 ).
cnf(u1938,axiom,
n4 != ssA(n3,n3) ).
cnf(u1142,axiom,
ssA(n6,n8) != ssA(n7,n8) ).
cnf(u573,axiom,
ssA(n4,n2) != ssA(n4,n9) ).
cnf(u930,axiom,
ssA(n3,n3) != ssA(n6,n3) ).
cnf(u1990,axiom,
n1 != ssA(n3,n1) ).
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(u10412,axiom,
n9 != ssA(n5,n9) ).
cnf(u1949,axiom,
n3 != ssA(n7,n6) ).
cnf(u1802,axiom,
n5 != ssA(n2,n4) ).
cnf(u1847,axiom,
n8 != ssA(n3,n5) ).
cnf(u644,axiom,
ssA(n6,n7) != ssA(n6,n8) ).
cnf(u441,axiom,
ssA(n1,n2) != ssA(n1,n6) ).
cnf(u979,axiom,
ssA(n2,n4) != ssA(n8,n4) ).
cnf(u1824,axiom,
n4 != ssA(n3,n4) ).
cnf(u9692,axiom,
n6 != ssA(n8,n9) ).
cnf(u942,axiom,
ssA(n1,n3) != ssA(n7,n3) ).
cnf(u757,axiom,
ssA(n8,n2) != ssA(n8,n5) ).
cnf(u1423,axiom,
ssA(n4,n6) != ssA(n6,n5) ).
cnf(u645,axiom,
ssA(n6,n6) != ssA(n6,n9) ).
cnf(u558,axiom,
ssA(n4,n5) != ssA(n4,n9) ).
cnf(u1982,axiom,
n3 != ssA(n4,n8) ).
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(u4130,axiom,
n3 = ssA(n4,n3) ).
cnf(u1999,axiom,
n4 != ssA(n9,n5) ).
cnf(u1103,axiom,
ssA(n4,n7) != ssA(n8,n7) ).
cnf(u10024,axiom,
n4 = ssA(n3,n1) ).
cnf(u1237,axiom,
ssA(n2,n1) != ssA(n3,n3) ).
cnf(u1548,axiom,
ssA(n8,n5) != ssA(n9,n6) ).
cnf(u1562,axiom,
ssA(n7,n6) != ssA(n8,n4) ).
cnf(u938,axiom,
ssA(n2,n3) != ssA(n4,n3) ).
cnf(u1905,axiom,
n1 != ssA(n4,n3) ).
cnf(u828,axiom,
ssA(n5,n1) != ssA(n9,n1) ).
cnf(u554,axiom,
ssA(n4,n7) != ssA(n4,n8) ).
cnf(u523,axiom,
ssA(n3,n3) != ssA(n3,n8) ).
cnf(u1116,axiom,
ssA(n2,n7) != ssA(n6,n7) ).
cnf(u758,axiom,
ssA(n8,n2) != ssA(n8,n4) ).
cnf(u11259,axiom,
n8 != ssA(n8,n4) ).
cnf(u1863,axiom,
n8 != ssA(n8,n9) ).
cnf(u1563,axiom,
ssA(n7,n5) != ssA(n9,n6) ).
cnf(u632,axiom,
ssA(n5,n1) != ssA(n5,n2) ).
cnf(u652,axiom,
ssA(n6,n4) != ssA(n6,n9) ).
cnf(u855,axiom,
ssA(n1,n1) != ssA(n4,n1) ).
cnf(u1101,axiom,
ssA(n5,n7) != ssA(n6,n7) ).
cnf(u1810,axiom,
n5 != ssA(n4,n2) ).
cnf(u802,axiom,
ssA(n9,n2) != ssA(n9,n5) ).
cnf(u1208,axiom,
ssA(n2,n9) != ssA(n4,n9) ).
cnf(u653,axiom,
ssA(n6,n4) != ssA(n6,n8) ).
cnf(u1862,axiom,
n8 != ssA(n9,n9) ).
cnf(u9130,axiom,
n1 != ssA(n3,n3) ).
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(u4579,axiom,
n5 = ssA(n5,n1) ).
cnf(u1821,axiom,
n4 != ssA(n6,n4) ).
cnf(u969,axiom,
ssA(n4,n4) != ssA(n7,n4) ).
cnf(u516,axiom,
ssA(n3,n5) != ssA(n3,n6) ).
cnf(u1940,axiom,
n4 != ssA(n4,n2) ).
cnf(u851,axiom,
ssA(n1,n1) != ssA(n8,n1) ).
cnf(u1456,axiom,
ssA(n5,n9) != ssA(n6,n8) ).
cnf(u9862,axiom,
n2 != ssA(n7,n1) ).
cnf(u1072,axiom,
ssA(n2,n6) != ssA(n5,n6) ).
cnf(u1214,axiom,
ssA(n1,n9) != ssA(n5,n9) ).
cnf(u468,axiom,
ssA(n2,n5) != ssA(n2,n9) ).
cnf(u517,axiom,
ssA(n3,n4) != ssA(n3,n9) ).
cnf(u649,axiom,
ssA(n6,n5) != ssA(n6,n8) ).
cnf(u1854,axiom,
n1 != ssA(n8,n7) ).
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,
n5 != ssA(n3,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(u1818,axiom,
n4 != ssA(n9,n4) ).
cnf(u1472,axiom,
ssA(n4,n9) != ssA(n5,n7) ).
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(n2,n5) ).
cnf(u10554,axiom,
n9 = ssA(n4,n6) ).
cnf(u1372,axiom,
ssA(n5,n1) != ssA(n6,n3) ).
cnf(u1195,axiom,
ssA(n4,n9) != ssA(n6,n9) ).
cnf(u10004,axiom,
n7 = ssA(n2,n1) ).
cnf(u630,axiom,
ssA(n5,n1) != ssA(n5,n4) ).
cnf(u11514,axiom,
n9 != ssA(n1,n3) ).
cnf(u762,axiom,
ssA(n8,n1) != ssA(n8,n7) ).
cnf(u977,axiom,
ssA(n3,n4) != ssA(n4,n4) ).
cnf(u1948,axiom,
n3 != ssA(n5,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(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(n7,n5) ).
cnf(u1565,axiom,
ssA(n7,n5) != ssA(n9,n4) ).
cnf(u626,axiom,
ssA(n5,n1) != ssA(n5,n8) ).
cnf(u841,axiom,
ssA(n3,n1) != ssA(n5,n1) ).
cnf(u743,axiom,
ssA(n8,n4) != ssA(n8,n8) ).
cnf(u1812,axiom,
n5 != ssA(n1,n2) ).
cnf(u1186,axiom,
ssA(n6,n9) != ssA(n8,n9) ).
cnf(u1529,axiom,
ssA(n7,n1) != ssA(n8,n2) ).
cnf(u1328,axiom,
ssA(n2,n7) != ssA(n3,n8) ).
cnf(u393,axiom,
n2 != n9 ).
cnf(u521,axiom,
ssA(n3,n4) != ssA(n3,n5) ).
cnf(u1152,axiom,
ssA(n3,n8) != ssA(n9,n8) ).
cnf(u1022,axiom,
ssA(n3,n5) != ssA(n4,n5) ).
cnf(u1615,axiom,
ssA(n7,n7) != ssA(n9,n9) ).
cnf(u1503,axiom,
ssA(n8,n2) != ssA(n9,n3) ).
cnf(u1203,axiom,
ssA(n2,n9) != ssA(n9,n9) ).
cnf(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(u1893,axiom,
n4 != ssA(n3,n5) ).
cnf(u720,axiom,
ssA(n7,n1) != ssA(n7,n4) ).
cnf(u1183,axiom,
ssA(n7,n9) != ssA(n9,n9) ).
cnf(u405,axiom,
n1 != n4 ).
cnf(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,
n1 != ssA(n5,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(u2006,axiom,
n4 != ssA(n6,n9) ).
cnf(u9695,axiom,
n6 != ssA(n4,n9) ).
cnf(u1720,axiom,
n4 = ssA(n9,n9) ).
cnf(u1820,axiom,
n4 != ssA(n7,n4) ).
cnf(u438,axiom,
ssA(n1,n2) != ssA(n1,n9) ).
cnf(u1196,axiom,
ssA(n4,n9) != ssA(n5,n9) ).
cnf(u710,axiom,
ssA(n7,n2) != ssA(n7,n7) ).
cnf(u1943,axiom,
n3 != ssA(n5,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(u8208,axiom,
n7 != ssA(n8,n6) ).
cnf(u882,axiom,
ssA(n3,n2) != ssA(n9,n2) ).
cnf(u1160,axiom,
ssA(n2,n8) != ssA(n7,n8) ).
cnf(u1849,axiom,
n8 != ssA(n3,n3) ).
cnf(u733,axiom,
ssA(n8,n7) != ssA(n8,n9) ).
cnf(u975,axiom,
ssA(n3,n4) != ssA(n6,n4) ).
cnf(u1807,axiom,
n5 != ssA(n7,n2) ).
cnf(u1942,axiom,
n3 != ssA(n5,n8) ).
cnf(u615,axiom,
ssA(n5,n3) != ssA(n5,n6) ).
cnf(u10873,axiom,
n9 = ssA(n3,n5) ).
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,
n8 != ssA(n2,n7) ).
cnf(u931,axiom,
ssA(n3,n3) != ssA(n5,n3) ).
cnf(u1971,axiom,
n5 != ssA(n4,n9) ).
cnf(u1024,axiom,
ssA(n2,n5) != ssA(n8,n5) ).
cnf(u1166,axiom,
ssA(n1,n8) != ssA(n8,n8) ).
cnf(u1075,axiom,
ssA(n1,n6) != ssA(n9,n6) ).
cnf(u597,axiom,
ssA(n5,n8) != ssA(n5,n9) ).
cnf(u1806,axiom,
n5 != ssA(n8,n2) ).
cnf(u1561,axiom,
ssA(n7,n6) != ssA(n8,n5) ).
cnf(u446,axiom,
ssA(n1,n1) != ssA(n1,n8) ).
cnf(u976,axiom,
ssA(n3,n4) != ssA(n5,n4) ).
cnf(u1204,axiom,
ssA(n2,n9) != ssA(n8,n9) ).
cnf(u718,axiom,
ssA(n7,n1) != ssA(n7,n6) ).
cnf(u1951,axiom,
n3 != ssA(n3,n6) ).
cnf(u1411,axiom,
ssA(n5,n6) != ssA(n6,n5) ).
cnf(u1258,axiom,
ssA(n1,n1) != ssA(n2,n3) ).
cnf(u1055,axiom,
ssA(n5,n6) != ssA(n7,n6) ).
cnf(u943,axiom,
ssA(n1,n3) != ssA(n6,n3) ).
cnf(u1473,axiom,
ssA(n4,n8) != ssA(n6,n9) ).
cnf(u1189,axiom,
ssA(n5,n9) != ssA(n8,n9) ).
cnf(u465,axiom,
ssA(n2,n6) != ssA(n2,n9) ).
cnf(u1976,axiom,
n3 != ssA(n7,n7) ).
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(u1068,axiom,
ssA(n2,n6) != ssA(n9,n6) ).
cnf(u582,axiom,
ssA(n4,n1) != ssA(n4,n7) ).
cnf(u714,axiom,
ssA(n7,n2) != ssA(n7,n3) ).
cnf(u807,axiom,
ssA(n9,n1) != ssA(n9,n7) ).
cnf(u1053,axiom,
ssA(n5,n6) != ssA(n9,n6) ).
cnf(u939,axiom,
ssA(n2,n3) != ssA(n3,n3) ).
cnf(u1593,axiom,
ssA(n8,n8) != ssA(n9,n9) ).
cnf(u1255,axiom,
ssA(n1,n1) != ssA(n3,n3) ).
cnf(u1979,axiom,
n3 != ssA(n7,n3) ).
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(u1517,axiom,
ssA(n7,n3) != ssA(n8,n1) ).
cnf(u1714,axiom,
n4 = ssA(n5,n3) ).
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,
n7 != ssA(n6,n9) ).
cnf(u852,axiom,
ssA(n1,n1) != ssA(n7,n1) ).
cnf(u578,axiom,
ssA(n4,n2) != ssA(n4,n4) ).
cnf(u675,axiom,
ssA(n6,n1) != ssA(n6,n4) ).
cnf(u921,axiom,
ssA(n5,n3) != ssA(n6,n3) ).
cnf(u1892,axiom,
n4 != ssA(n3,n6) ).
cnf(u803,axiom,
ssA(n9,n2) != ssA(n9,n4) ).
cnf(u1715,axiom,
n3 = ssA(n5,n6) ).
cnf(u1280,axiom,
ssA(n2,n5) != ssA(n3,n4) ).
cnf(u473,axiom,
ssA(n2,n4) != ssA(n2,n8) ).
cnf(u9131,axiom,
n1 != ssA(n1,n3) ).
cnf(u420,axiom,
ssA(n1,n6) != ssA(n1,n9) ).
cnf(u601,axiom,
ssA(n5,n6) != ssA(n5,n8) ).
cnf(u835,axiom,
ssA(n4,n1) != ssA(n6,n1) ).
cnf(u1232,axiom,
ssA(n2,n3) != ssA(n3,n1) ).
cnf(u1460,axiom,
ssA(n5,n8) != ssA(n6,n7) ).
cnf(u974,axiom,
ssA(n3,n4) != ssA(n7,n4) ).
cnf(u1155,axiom,
ssA(n3,n8) != ssA(n6,n8) ).
cnf(u848,axiom,
ssA(n2,n1) != ssA(n4,n1) ).
cnf(u1514,axiom,
ssA(n7,n3) != ssA(n9,n1) ).
cnf(u2014,axiom,
n4 != ssA(n7,n7) ).
cnf(u687,axiom,
ssA(n7,n8) != ssA(n7,n9) ).
cnf(u933,axiom,
ssA(n2,n3) != ssA(n9,n3) ).
cnf(u1061,axiom,
ssA(n4,n6) != ssA(n5,n6) ).
cnf(u1424,axiom,
ssA(n4,n6) != ssA(n6,n4) ).
cnf(u485,axiom,
ssA(n2,n2) != ssA(n2,n7) ).
cnf(u9848,axiom,
n2 != ssA(n7,n3) ).
cnf(u1848,axiom,
n8 != ssA(n3,n4) ).
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,
n4 != ssA(n4,n3) ).
cnf(u586,axiom,
ssA(n4,n1) != ssA(n4,n3) ).
cnf(u13351,axiom,
n8 = ssA(n8,n5) ).
cnf(u10402,axiom,
n9 = ssA(n2,n9) ).
cnf(u929,axiom,
ssA(n3,n3) != ssA(n7,n3) ).
cnf(u1900,axiom,
n8 != ssA(n2,n8) ).
cnf(u390,axiom,
n3 != n6 ).
cnf(u1276,axiom,
ssA(n2,n6) != ssA(n3,n5) ).
cnf(u811,axiom,
ssA(n9,n1) != ssA(n9,n3) ).
cnf(u1288,axiom,
ssA(n1,n6) != ssA(n3,n5) ).
cnf(u664,axiom,
ssA(n6,n2) != ssA(n6,n8) ).
cnf(u1851,axiom,
n8 != ssA(n3,n1) ).
cnf(u1015,axiom,
ssA(n4,n5) != ssA(n6,n5) ).
cnf(u1970,axiom,
n5 != ssA(n5,n7) ).
cnf(u834,axiom,
ssA(n4,n1) != ssA(n7,n1) ).
cnf(u6469,axiom,
n3 != ssA(n6,n1) ).
cnf(u1801,axiom,
n5 != ssA(n2,n3) ).
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(u10070,axiom,
n8 != ssA(n7,n6) ).
cnf(u1981,axiom,
n3 != ssA(n7,n1) ).
cnf(u676,axiom,
ssA(n6,n1) != ssA(n6,n3) ).
cnf(u1011,axiom,
ssA(n5,n5) != ssA(n6,n5) ).
cnf(u2112,axiom,
n5 != ssA(n4,n6) ).
cnf(u1716,axiom,
n5 = ssA(n6,n8) ).
cnf(u1923,axiom,
n7 != ssA(n4,n4) ).
cnf(u1104,axiom,
ssA(n4,n7) != ssA(n7,n7) ).
cnf(u846,axiom,
ssA(n2,n1) != ssA(n6,n1) ).
cnf(u1027,axiom,
ssA(n2,n5) != ssA(n5,n5) ).
cnf(u677,axiom,
ssA(n6,n1) != ssA(n6,n2) ).
cnf(u1386,axiom,
ssA(n4,n2) != ssA(n5,n3) ).
cnf(u559,axiom,
ssA(n4,n5) != ssA(n4,n8) ).
cnf(u805,axiom,
ssA(n9,n1) != ssA(n9,n9) ).
cnf(u447,axiom,
ssA(n1,n1) != ssA(n1,n7) ).
cnf(u1717,axiom,
n7 = ssA(n7,n4) ).
cnf(u451,axiom,
ssA(n1,n1) != ssA(n1,n3) ).
cnf(u378,axiom,
n5 != n9 ).
cnf(u398,axiom,
n2 != n4 ).
cnf(u1156,axiom,
ssA(n3,n8) != ssA(n5,n8) ).
cnf(u1845,axiom,
n8 != ssA(n3,n7) ).
cnf(u540,axiom,
ssA(n3,n1) != ssA(n3,n4) ).
cnf(u672,axiom,
ssA(n6,n1) != ssA(n6,n7) ).
cnf(u1438,axiom,
ssA(n4,n4) != ssA(n5,n6) ).
cnf(u1023,axiom,
ssA(n2,n5) != ssA(n9,n5) ).
cnf(u624,axiom,
ssA(n5,n2) != ssA(n5,n3) ).
cnf(u842,axiom,
ssA(n3,n1) != ssA(n4,n1) ).
cnf(u492,axiom,
ssA(n2,n1) != ssA(n2,n7) ).
cnf(u1809,axiom,
n5 != ssA(n5,n2) ).
cnf(u673,axiom,
ssA(n6,n1) != ssA(n6,n6) ).
cnf(u555,axiom,
ssA(n4,n6) != ssA(n4,n9) ).
cnf(u801,axiom,
ssA(n9,n2) != ssA(n9,n6) ).
cnf(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(n2,n6) ).
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,
n3 != ssA(n1,n2) ).
cnf(u1931,axiom,
n7 != ssA(n5,n9) ).
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(u11744,axiom,
n9 = ssA(n7,n1) ).
cnf(u1463,axiom,
ssA(n5,n7) != ssA(n6,n8) ).
cnf(u567,axiom,
ssA(n4,n3) != ssA(n4,n9) ).
cnf(u1097,axiom,
ssA(n6,n7) != ssA(n7,n7) ).
cnf(u2009,axiom,
n4 != ssA(n2,n9) ).
cnf(u932,axiom,
ssA(n3,n3) != ssA(n4,n3) ).
cnf(u658,axiom,
ssA(n6,n3) != ssA(n6,n8) ).
cnf(u1853,axiom,
n1 != ssA(n9,n7) ).
cnf(u883,axiom,
ssA(n3,n2) != ssA(n8,n2) ).
cnf(u9866,axiom,
n2 != ssA(n2,n1) ).
cnf(u1118,axiom,
ssA(n2,n7) != ssA(n4,n7) ).
cnf(u1936,axiom,
n4 != ssA(n7,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(u767,axiom,
ssA(n8,n1) != ssA(n8,n2) ).
cnf(u1013,axiom,
ssA(n4,n5) != ssA(n8,n5) ).
cnf(u1210,axiom,
ssA(n1,n9) != ssA(n9,n9) ).
cnf(u1710,axiom,
n8 = ssA(n3,n9) ).
cnf(u895,axiom,
ssA(n1,n2) != ssA(n9,n2) ).
cnf(u1141,axiom,
ssA(n6,n8) != ssA(n8,n8) ).
cnf(u1925,axiom,
n1 != ssA(n6,n6) ).
cnf(u13280,axiom,
n9 != ssA(n5,n8) ).
cnf(u11538,axiom,
n4 = ssA(n7,n2) ).
cnf(u1553,axiom,
ssA(n8,n4) != ssA(n9,n5) ).
cnf(u417,axiom,
ssA(n1,n8) != ssA(n1,n9) ).
cnf(u496,axiom,
ssA(n2,n1) != ssA(n2,n3) ).
cnf(u1800,axiom,
n5 != ssA(n2,n1) ).
cnf(u9666,axiom,
n4 != ssA(n7,n5) ).
cnf(u10006,axiom,
n7 != ssA(n7,n1) ).
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(u1111,axiom,
ssA(n3,n7) != ssA(n5,n7) ).
cnf(u534,axiom,
ssA(n3,n2) != ssA(n3,n3) ).
cnf(u940,axiom,
ssA(n1,n3) != ssA(n9,n3) ).
cnf(u666,axiom,
ssA(n6,n2) != ssA(n6,n6) ).
cnf(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(u1368,axiom,
ssA(n5,n2) != ssA(n6,n3) ).
cnf(u744,axiom,
ssA(n8,n4) != ssA(n8,n7) ).
cnf(u1207,axiom,
ssA(n2,n9) != ssA(n5,n9) ).
cnf(u1803,axiom,
n5 != ssA(n2,n5) ).
cnf(u429,axiom,
ssA(n1,n4) != ssA(n1,n7) ).
cnf(u877,axiom,
ssA(n4,n2) != ssA(n9,n2) ).
cnf(u557,axiom,
ssA(n4,n6) != ssA(n4,n7) ).
cnf(u1469,axiom,
ssA(n4,n9) != ssA(n6,n7) ).
cnf(u11429,axiom,
n1 != ssA(n7,n9) ).
cnf(u914,axiom,
ssA(n7,n3) != ssA(n8,n3) ).
cnf(u1881,axiom,
n2 != ssA(n3,n6) ).
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(u12649,axiom,
n7 != ssA(n8,n7) ).
cnf(u1021,axiom,
ssA(n3,n5) != ssA(n5,n5) ).
cnf(u1844,axiom,
n8 != ssA(n3,n8) ).
cnf(u466,axiom,
ssA(n2,n6) != ssA(n2,n8) ).
cnf(u1933,axiom,
n4 != ssA(n5,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,
n4 != ssA(n9,n1) ).
cnf(u10026,axiom,
n4 != ssA(n7,n1) ).
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(u800,axiom,
ssA(n9,n2) != ssA(n9,n7) ).
cnf(u542,axiom,
ssA(n3,n1) != ssA(n3,n2) ).
cnf(u1966,axiom,
n5 != ssA(n3,n8) ).
cnf(u885,axiom,
ssA(n3,n2) != ssA(n6,n2) ).
cnf(u399,axiom,
n2 != n3 ).
cnf(u1082,axiom,
ssA(n1,n6) != ssA(n2,n6) ).
cnf(u11509,axiom,
n9 != ssA(n7,n3) ).
cnf(u478,axiom,
ssA(n2,n3) != ssA(n2,n8) ).
cnf(u4937,axiom,
n7 != ssA(n4,n2) ).
cnf(u1797,axiom,
n1 != ssA(n1,n1) ).
cnf(u620,axiom,
ssA(n5,n2) != ssA(n5,n7) ).
cnf(u1830,axiom,
n7 != ssA(n6,n5) ).
cnf(u752,axiom,
ssA(n8,n3) != ssA(n8,n4) ).
cnf(u1518,axiom,
ssA(n7,n2) != ssA(n9,n3) ).
cnf(u1215,axiom,
ssA(n1,n9) != ssA(n4,n9) ).
cnf(u437,axiom,
ssA(n1,n3) != ssA(n1,n4) ).
cnf(u1930,axiom,
n7 != ssA(n6,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(u881,axiom,
ssA(n4,n2) != ssA(n5,n2) ).
cnf(u395,axiom,
n2 != 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(u1435,axiom,
ssA(n4,n4) != ssA(n6,n6) ).
cnf(u572,axiom,
ssA(n4,n3) != ssA(n4,n4) ).
cnf(u616,axiom,
ssA(n5,n3) != ssA(n5,n5) ).
cnf(u1382,axiom,
ssA(n4,n3) != ssA(n5,n1) ).
cnf(u764,axiom,
ssA(n8,n1) != ssA(n8,n5) ).
cnf(u1079,axiom,
ssA(n1,n6) != ssA(n5,n6) ).
cnf(u839,axiom,
ssA(n3,n1) != ssA(n7,n1) ).
cnf(u1213,axiom,
ssA(n1,n9) != ssA(n6,n9) ).
cnf(u971,axiom,
ssA(n4,n4) != ssA(n5,n4) ).
cnf(u1794,axiom,
n7 != ssA(n1,n7) ).
cnf(u1341,axiom,
ssA(n1,n8) != ssA(n2,n9) ).
cnf(u2011,axiom,
n4 != ssA(n8,n8) ).
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(u12653,axiom,
n7 != ssA(n8,n3) ).
cnf(u1415,axiom,
ssA(n5,n5) != ssA(n6,n4) ).
cnf(u765,axiom,
ssA(n8,n1) != ssA(n8,n4) ).
cnf(u519,axiom,
ssA(n3,n4) != ssA(n3,n7) ).
cnf(u407,axiom,
n1 != n2 ).
cnf(u1012,axiom,
ssA(n4,n5) != ssA(n9,n5) ).
cnf(u738,axiom,
ssA(n8,n5) != ssA(n8,n9) ).
cnf(u1991,axiom,
n1 != ssA(n2,n1) ).
cnf(u628,axiom,
ssA(n5,n1) != ssA(n5,n6) ).
cnf(u568,axiom,
ssA(n4,n3) != ssA(n4,n8) ).
cnf(u1875,axiom,
n3 != ssA(n2,n1) ).
cnf(u1056,axiom,
ssA(n5,n6) != ssA(n6,n6) ).
cnf(u798,axiom,
ssA(n9,n2) != ssA(n9,n9) ).
cnf(u452,axiom,
ssA(n1,n1) != ssA(n1,n2) ).
cnf(u629,axiom,
ssA(n5,n1) != ssA(n5,n5) ).
cnf(u761,axiom,
ssA(n8,n1) != ssA(n8,n8) ).
cnf(u1838,axiom,
n3 != ssA(n3,n3) ).
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,
n3 != ssA(n1,n8) ).
cnf(u719,axiom,
ssA(n7,n1) != ssA(n7,n5) ).
cnf(u965,axiom,
ssA(n5,n4) != ssA(n7,n4) ).
cnf(u1869,axiom,
n8 != ssA(n1,n9) ).
cnf(u1162,axiom,
ssA(n2,n8) != ssA(n5,n8) ).
cnf(u1790,axiom,
n4 != ssA(n1,n1) ).
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,
n4 != ssA(n7,n9) ).
cnf(u10411,axiom,
n9 != ssA(n7,n9) ).
cnf(u497,axiom,
ssA(n2,n1) != ssA(n2,n2) ).
cnf(u10038,axiom,
n7 = ssA(n3,n8) ).
cnf(u794,axiom,
ssA(n9,n3) != ssA(n9,n7) ).
cnf(u444,axiom,
ssA(n1,n2) != ssA(n1,n3) ).
cnf(u448,axiom,
ssA(n1,n1) != ssA(n1,n6) ).
cnf(u625,axiom,
ssA(n5,n1) != ssA(n5,n9) ).
cnf(u1880,axiom,
n5 != ssA(n1,n1) ).
cnf(u1185,axiom,
ssA(n6,n9) != ssA(n9,n9) ).
cnf(u872,axiom,
ssA(n6,n2) != ssA(n7,n2) ).
cnf(u614,axiom,
ssA(n5,n3) != ssA(n5,n7) ).
cnf(u1020,axiom,
ssA(n3,n5) != ssA(n6,n5) ).
cnf(u746,axiom,
ssA(n8,n4) != ssA(n8,n5) ).
cnf(u715,axiom,
ssA(n7,n1) != ssA(n7,n9) ).
cnf(u961,axiom,
ssA(n6,n4) != ssA(n8,n4) ).
cnf(u1932,axiom,
n7 != ssA(n5,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,
n4 != ssA(n9,n2) ).
cnf(u1206,axiom,
ssA(n2,n9) != ssA(n6,n9) ).
cnf(u1618,axiom,
ssA(n7,n7) != ssA(n8,n9) ).
cnf(u1846,axiom,
n8 != ssA(n3,n6) ).
cnf(u1049,axiom,
ssA(n7,n6) != ssA(n8,n6) ).
cnf(u1961,axiom,
n5 != ssA(n6,n1) ).
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(u708,axiom,
ssA(n7,n2) != ssA(n7,n9) ).
cnf(u1070,axiom,
ssA(n2,n6) != ssA(n7,n6) ).
cnf(u661,axiom,
ssA(n6,n3) != ssA(n6,n5) ).
cnf(u1888,axiom,
n7 != ssA(n2,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(u1418,axiom,
ssA(n5,n4) != ssA(n6,n5) ).
cnf(u622,axiom,
ssA(n5,n2) != ssA(n5,n5) ).
cnf(u1855,axiom,
n1 != ssA(n7,n7) ).
cnf(u11592,axiom,
n9 = ssA(n1,n2) ).
cnf(u837,axiom,
ssA(n3,n1) != ssA(n9,n1) ).
cnf(u1877,axiom,
n5 != ssA(n1,n3) ).
cnf(u700,axiom,
ssA(n7,n4) != ssA(n7,n6) ).
cnf(u704,axiom,
ssA(n7,n3) != ssA(n7,n7) ).
cnf(u1167,axiom,
ssA(n1,n8) != ssA(n7,n8) ).
cnf(u389,axiom,
n3 != n7 ).
cnf(u2010,axiom,
n4 != ssA(n1,n9) ).
cnf(u1002,axiom,
ssA(n8,n5) != ssA(n9,n5) ).
cnf(u1051,axiom,
ssA(n6,n6) != ssA(n8,n6) ).
cnf(u1969,axiom,
n5 != ssA(n5,n9) ).
cnf(u739,axiom,
ssA(n8,n5) != ssA(n8,n8) ).
cnf(u705,axiom,
ssA(n7,n3) != ssA(n7,n6) ).
cnf(u618,axiom,
ssA(n5,n2) != ssA(n5,n9) ).
cnf(u829,axiom,
ssA(n5,n1) != ssA(n8,n1) ).
cnf(u587,axiom,
ssA(n4,n1) != ssA(n4,n2) ).
cnf(u833,axiom,
ssA(n4,n1) != ssA(n8,n1) ).
cnf(u475,axiom,
ssA(n2,n4) != ssA(n2,n6) ).
cnf(u1704,axiom,
n4 = ssA(n1,n4) ).
cnf(u1804,axiom,
n5 != ssA(n2,n7) ).
cnf(u422,axiom,
ssA(n1,n6) != ssA(n1,n7) ).
cnf(u1927,axiom,
n1 != ssA(n5,n6) ).
cnf(u696,axiom,
ssA(n7,n5) != ssA(n7,n6) ).
cnf(u1462,axiom,
ssA(n5,n7) != ssA(n6,n9) ).
cnf(u716,axiom,
ssA(n7,n1) != ssA(n7,n8) ).
cnf(u381,axiom,
n5 != n6 ).
cnf(u919,axiom,
ssA(n5,n3) != ssA(n8,n3) ).
cnf(u1165,axiom,
ssA(n1,n8) != ssA(n9,n8) ).
cnf(u1874,axiom,
n5 != ssA(n3,n1) ).
cnf(u1078,axiom,
ssA(n1,n6) != ssA(n6,n6) ).
cnf(u1014,axiom,
ssA(n4,n5) != ssA(n7,n5) ).
cnf(u1833,axiom,
n7 != ssA(n3,n5) ).
cnf(u1607,axiom,
ssA(n7,n9) != ssA(n8,n7) ).
cnf(u717,axiom,
ssA(n7,n1) != ssA(n7,n7) ).
cnf(u1426,axiom,
ssA(n4,n6) != ssA(n5,n5) ).
cnf(u1926,axiom,
n1 != ssA(n6,n4) ).
cnf(u524,axiom,
ssA(n3,n3) != ssA(n3,n7) ).
cnf(u825,axiom,
ssA(n6,n1) != ssA(n9,n1) ).
cnf(u599,axiom,
ssA(n5,n7) != ssA(n5,n8) ).
cnf(u845,axiom,
ssA(n2,n1) != ssA(n7,n1) ).
cnf(u487,axiom,
ssA(n2,n2) != ssA(n2,n5) ).
cnf(u418,axiom,
ssA(n1,n7) != ssA(n1,n9) ).
cnf(u964,axiom,
ssA(n5,n4) != ssA(n8,n4) ).
cnf(u1868,axiom,
n8 != ssA(n2,n9) ).
cnf(u1385,axiom,
ssA(n4,n2) != ssA(n6,n1) ).
cnf(u1885,axiom,
n7 != ssA(n3,n6) ).
cnf(u580,axiom,
ssA(n4,n1) != ssA(n4,n9) ).
cnf(u2004,axiom,
n4 != ssA(n8,n9) ).
cnf(u377,axiom,
n6 != n7 ).
cnf(u915,axiom,
ssA(n6,n3) != ssA(n9,n3) ).
cnf(u539,axiom,
ssA(n3,n1) != ssA(n3,n5) ).
cnf(u878,axiom,
ssA(n4,n2) != ssA(n8,n2) ).
cnf(u1278,axiom,
ssA(n2,n5) != ssA(n3,n6) ).
cnf(u6470,axiom,
n3 != ssA(n8,n7) ).
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,
n6 != ssA(n6,n2) ).
cnf(u483,axiom,
ssA(n2,n2) != ssA(n2,n9) ).
cnf(u1712,axiom,
n1 = ssA(n4,n5) ).
cnf(u430,axiom,
ssA(n1,n4) != ssA(n1,n6) ).
cnf(u960,axiom,
ssA(n6,n4) != ssA(n9,n4) ).
cnf(u1188,axiom,
ssA(n5,n9) != ssA(n9,n9) ).
cnf(u1935,axiom,
n4 != ssA(n5,n1) ).
cnf(u1523,axiom,
ssA(n7,n2) != ssA(n8,n1) ).
cnf(u576,axiom,
ssA(n4,n2) != ssA(n4,n6) ).
cnf(u927,axiom,
ssA(n3,n3) != ssA(n9,n3) ).
cnf(u1882,axiom,
n2 != ssA(n3,n5) ).
cnf(u10072,axiom,
n8 != ssA(n4,n6) ).
cnf(u1713,axiom,
n7 = ssA(n4,n7) ).
cnf(u449,axiom,
ssA(n1,n1) != ssA(n1,n5) ).
cnf(u874,axiom,
ssA(n5,n2) != ssA(n8,n2) ).
cnf(u396,axiom,
n2 != n6 ).
cnf(u1841,axiom,
n3 != ssA(n4,n2) ).
cnf(u577,axiom,
ssA(n4,n2) != ssA(n4,n5) ).
cnf(u8211,axiom,
n7 != 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(u1334,axiom,
ssA(n1,n9) != ssA(n3,n7) ).
cnf(u1606,axiom,
ssA(n7,n9) != ssA(n8,n8) ).
cnf(u2012,axiom,
n4 != ssA(n8,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(u1963,axiom,
n5 != ssA(n7,n8) ).
cnf(u1144,axiom,
ssA(n5,n8) != ssA(n8,n8) ).
cnf(u886,axiom,
ssA(n3,n2) != ssA(n5,n2) ).
cnf(u392,axiom,
n3 != n4 ).
cnf(u1158,axiom,
ssA(n2,n8) != ssA(n9,n8) ).
cnf(u569,axiom,
ssA(n4,n3) != ssA(n4,n7) ).
cnf(u1367,axiom,
ssA(n5,n3) != ssA(n6,n1) ).
cnf(u2077,axiom,
n3 = ssA(n1,n9) ).
cnf(u1501,axiom,
ssA(n8,n3) != ssA(n9,n2) ).
cnf(u796,axiom,
ssA(n9,n3) != ssA(n9,n5) ).
cnf(u1813,axiom,
n2 != ssA(n7,n4) ).
cnf(u836,axiom,
ssA(n4,n1) != ssA(n5,n1) ).
cnf(u690,axiom,
ssA(n7,n6) != ssA(n7,n9) ).
cnf(u968,axiom,
ssA(n4,n4) != ssA(n8,n4) ).
cnf(u659,axiom,
ssA(n6,n3) != ssA(n6,n7) ).
cnf(u1876,axiom,
n3 != ssA(n1,n3) ).
cnf(u1250,axiom,
ssA(n1,n2) != ssA(n3,n1) ).
cnf(u787,axiom,
ssA(n9,n4) != ssA(n9,n9) ).
cnf(u9991,axiom,
n4 != ssA(n3,n8) ).
cnf(u1827,axiom,
n7 != ssA(n9,n5) ).
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,
n5 != ssA(n1,n8) ).
cnf(u832,axiom,
ssA(n4,n1) != ssA(n9,n1) ).
cnf(u702,axiom,
ssA(n7,n3) != ssA(n7,n9) ).
cnf(u1998,axiom,
n4 != ssA(n9,n6) ).
cnf(u9665,axiom,
n4 != ssA(n8,n5) ).
cnf(u671,axiom,
ssA(n6,n1) != ssA(n6,n8) ).
cnf(u917,axiom,
ssA(n6,n3) != ssA(n7,n3) ).
cnf(u1114,axiom,
ssA(n2,n7) != ssA(n8,n7) ).
cnf(u490,axiom,
ssA(n2,n1) != ssA(n2,n9) ).
cnf(u799,axiom,
ssA(n9,n2) != ssA(n9,n8) ).
cnf(u1457,axiom,
ssA(n5,n9) != ssA(n6,n7) ).
cnf(u1957,axiom,
n5 != ssA(n6,n5) ).
cnf(u10375,axiom,
n2 != ssA(n7,n5) ).
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(n4,n5) ).
cnf(u1706,axiom,
n1 = ssA(n1,n7) ).
cnf(u1137,axiom,
ssA(n8,n8) != ssA(n9,n8) ).
cnf(u824,axiom,
ssA(n7,n1) != ssA(n8,n1) ).
cnf(u566,axiom,
ssA(n4,n4) != ssA(n4,n5) ).
cnf(u844,axiom,
ssA(n2,n1) != ssA(n8,n1) ).
cnf(u698,axiom,
ssA(n7,n4) != ssA(n7,n8) ).
cnf(u667,axiom,
ssA(n6,n2) != ssA(n6,n5) ).
cnf(u913,axiom,
ssA(n7,n3) != ssA(n9,n3) ).
cnf(u1526,axiom,
ssA(n7,n1) != ssA(n9,n2) ).
cnf(u1884,axiom,
n2 != ssA(n1,n6) ).
cnf(u795,axiom,
ssA(n9,n3) != ssA(n9,n6) ).
cnf(u2007,axiom,
n4 != ssA(n5,n9) ).
cnf(u1707,axiom,
n5 = ssA(n2,n2) ).
cnf(u648,axiom,
ssA(n6,n5) != ssA(n6,n9) ).
cnf(u745,axiom,
ssA(n8,n4) != ssA(n8,n6) ).
cnf(u1835,axiom,
n3 != ssA(n3,n7) ).
cnf(u1373,axiom,
ssA(n5,n1) != ssA(n6,n2) ).
cnf(u1570,axiom,
ssA(n7,n4) != ssA(n9,n6) ).
cnf(u10062,axiom,
n8 = ssA(n2,n6) ).
cnf(u946,axiom,
ssA(n1,n3) != ssA(n3,n3) ).
cnf(u966,axiom,
ssA(n5,n4) != ssA(n6,n4) ).
cnf(u562,axiom,
ssA(n4,n4) != ssA(n4,n9) ).
cnf(u531,axiom,
ssA(n3,n2) != ssA(n3,n6) ).
cnf(u777,axiom,
ssA(n9,n8) != ssA(n9,n9) ).
cnf(u925,axiom,
ssA(n4,n3) != ssA(n6,n3) ).
cnf(u1571,axiom,
ssA(n7,n4) != ssA(n9,n5) ).
cnf(u1965,axiom,
n5 != ssA(n4,n8) ).
cnf(u660,axiom,
ssA(n6,n3) != ssA(n6,n6) ).
cnf(u522,axiom,
ssA(n3,n3) != ssA(n3,n9) ).
cnf(u1840,axiom,
n3 != ssA(n7,n2) ).
cnf(u958,axiom,
ssA(n7,n4) != ssA(n9,n4) ).
cnf(u1139,axiom,
ssA(n7,n8) != ssA(n8,n8) ).
cnf(u1370,axiom,
ssA(n5,n2) != ssA(n6,n1) ).
cnf(u574,axiom,
ssA(n4,n2) != ssA(n4,n8) ).
cnf(u14052,axiom,
n5 != ssA(n9,n1) ).
cnf(u1870,axiom,
n3 != ssA(n2,n3) ).
cnf(u442,axiom,
ssA(n1,n2) != ssA(n1,n5) ).
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(u1829,axiom,
n7 != ssA(n7,n5) ).
cnf(u1475,axiom,
ssA(n4,n8) != ssA(n6,n7) ).
cnf(u656,axiom,
ssA(n6,n4) != ssA(n6,n5) ).
cnf(u1119,axiom,
ssA(n2,n7) != ssA(n3,n7) ).
cnf(u1007,axiom,
ssA(n6,n5) != ssA(n7,n5) ).
cnf(u1253,axiom,
ssA(n1,n2) != ssA(n2,n1) ).
cnf(u1962,axiom,
n5 != ssA(n8,n8) ).
cnf(u1251,axiom,
ssA(n1,n2) != ssA(n2,n3) ).
cnf(u1381,axiom,
ssA(n4,n3) != ssA(n5,n2) ).
cnf(u476,axiom,
ssA(n2,n4) != ssA(n2,n5) ).
cnf(u657,axiom,
ssA(n6,n3) != ssA(n6,n9) ).
cnf(u570,axiom,
ssA(n4,n3) != ssA(n4,n6) ).
cnf(u1516,axiom,
ssA(n7,n3) != ssA(n8,n2) ).
cnf(u785,axiom,
ssA(n9,n5) != ssA(n9,n7) ).
cnf(u427,axiom,
ssA(n1,n4) != ssA(n1,n9) ).
cnf(u1217,axiom,
ssA(n1,n9) != ssA(n2,n9) ).
cnf(u374,axiom,
n7 != n8 ).
cnf(u646,axiom,
ssA(n6,n6) != ssA(n6,n8) ).
cnf(u1879,axiom,
n3 != ssA(n1,n1) ).
cnf(u520,axiom,
ssA(n3,n4) != ssA(n3,n6) ).
cnf(u668,axiom,
ssA(n6,n2) != ssA(n6,n4) ).
cnf(u871,axiom,
ssA(n6,n2) != ssA(n8,n2) ).
cnf(u1117,axiom,
ssA(n2,n7) != ssA(n5,n7) ).
cnf(u1003,axiom,
ssA(n7,n5) != ssA(n9,n5) ).
cnf(u14214,axiom,
n6 != ssA(n9,n1) ).
cnf(u9667,axiom,
n4 != ssA(n5,n5) ).
cnf(u1708,axiom,
n2 = ssA(n2,n4) ).
cnf(u1096,axiom,
ssA(n6,n7) != ssA(n8,n7) ).
cnf(u838,axiom,
ssA(n3,n1) != ssA(n8,n1) ).
cnf(u472,axiom,
ssA(n2,n4) != ssA(n2,n9) ).
cnf(u1559,axiom,
ssA(n7,n6) != ssA(n9,n4) ).
cnf(u669,axiom,
ssA(n6,n2) != ssA(n6,n3) ).
cnf(u1378,axiom,
ssA(n4,n3) != ssA(n6,n2) ).
cnf(u797,axiom,
ssA(n9,n3) != ssA(n9,n4) ).
cnf(u439,axiom,
ssA(n1,n2) != ssA(n1,n8) ).
cnf(u1993,axiom,
n1 != ssA(n7,n3) ).
cnf(u1709,axiom,
n3 = ssA(n3,n2) ).
cnf(u916,axiom,
ssA(n6,n3) != ssA(n8,n3) ).
cnf(u642,axiom,
ssA(n6,n8) != ssA(n6,n9) ).
cnf(u1337,axiom,
ssA(n1,n9) != ssA(n2,n7) ).
cnf(u1837,axiom,
n3 != ssA(n3,n4) ).
cnf(u532,axiom,
ssA(n3,n2) != ssA(n3,n5) ).
cnf(u1956,axiom,
n5 != ssA(n6,n7) ).
cnf(u867,axiom,
ssA(n8,n2) != ssA(n9,n2) ).
cnf(u13304,axiom,
n9 = ssA(n5,n7) ).
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,
n6 != ssA(n5,n2) ).
cnf(u1073,axiom,
ssA(n2,n6) != ssA(n4,n6) ).
cnf(u2104,axiom,
n5 = ssA(n1,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,
n7 != ssA(n3,n4) ).
cnf(u4936,axiom,
n7 != ssA(n7,n2) ).
cnf(u751,axiom,
ssA(n8,n3) != ssA(n8,n5) ).
cnf(u528,axiom,
ssA(n3,n2) != ssA(n3,n9) ).
cnf(u1194,axiom,
ssA(n4,n9) != ssA(n7,n9) ).
cnf(u879,axiom,
ssA(n4,n2) != ssA(n7,n2) ).
cnf(u1834,axiom,
n7 != ssA(n2,n5) ).
cnf(u13326,axiom,
n8 = ssA(n5,n8) ).
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,
n1 != ssA(n3,n8) ).
cnf(u1388,axiom,
ssA(n4,n2) != ssA(n5,n1) ).
cnf(u1211,axiom,
ssA(n1,n9) != ssA(n8,n9) ).
cnf(u2001,axiom,
n4 != ssA(n9,n3) ).
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,
n5 != ssA(n5,n8) ).
cnf(u875,axiom,
ssA(n5,n2) != ssA(n7,n2) ).
cnf(u4581,axiom,
n5 != ssA(n7,n1) ).
cnf(u1191,axiom,
ssA(n5,n9) != ssA(n6,n9) ).
cnf(u1915,axiom,
n1 != ssA(n2,n8) ).
cnf(u1110,axiom,
ssA(n3,n7) != ssA(n6,n7) ).
cnf(u541,axiom,
ssA(n3,n1) != ssA(n3,n3) ).
cnf(u1321,axiom,
ssA(n2,n9) != ssA(n3,n8) ).
cnf(u1928,axiom,
n1 != ssA(n5,n4) ).
cnf(u898,axiom,
ssA(n1,n2) != ssA(n6,n2) ).
cnf(u1081,axiom,
ssA(n1,n6) != ssA(n3,n6) ).
cnf(u1865,axiom,
n8 != ssA(n6,n9) ).
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,
n7 != ssA(n8,n5) ).
cnf(u9694,axiom,
n6 != ssA(n5,n9) ).
cnf(u1417,axiom,
ssA(n5,n4) != ssA(n6,n6) ).
cnf(u740,axiom,
ssA(n8,n5) != ssA(n8,n7) ).
cnf(u4930,axiom,
n7 = ssA(n5,n2) ).
cnf(u537,axiom,
ssA(n3,n1) != ssA(n3,n7) ).
cnf(u1792,axiom,
n7 != ssA(n1,n3) ).
cnf(u1168,axiom,
ssA(n1,n8) != ssA(n6,n8) ).
cnf(u2086,axiom,
n3 != ssA(n4,n9) ).
cnf(u1815,axiom,
n2 != ssA(n5,n4) ).
cnf(u741,axiom,
ssA(n8,n5) != ssA(n8,n6) ).
cnf(u784,axiom,
ssA(n9,n5) != ssA(n9,n8) ).
cnf(u526,axiom,
ssA(n3,n3) != ssA(n3,n5) ).
cnf(u1950,axiom,
n3 != ssA(n4,n6) ).
cnf(u623,axiom,
ssA(n5,n2) != ssA(n5,n4) ).
cnf(u869,axiom,
ssA(n7,n2) != ssA(n8,n2) ).
cnf(u511,axiom,
ssA(n3,n6) != ssA(n3,n8) ).
cnf(u1066,axiom,
ssA(n3,n6) != ssA(n5,n6) ).
cnf(u563,axiom,
ssA(n4,n4) != ssA(n4,n8) ).
cnf(u1566,axiom,
ssA(n7,n5) != ssA(n8,n6) ).
cnf(u462,axiom,
ssA(n2,n8) != ssA(n2,n9) ).
cnf(u1909,axiom,
n8 != ssA(n1,n8) ).
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(u421,axiom,
ssA(n1,n6) != ssA(n1,n8) ).
cnf(u737,axiom,
ssA(n8,n6) != ssA(n8,n7) ).
cnf(u1856,axiom,
n1 != ssA(n6,n7) ).
cnf(u9588,axiom,
n1 != ssA(n8,n2) ).
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,
n3 != ssA(n3,n5) ).
cnf(u1212,axiom,
ssA(n1,n9) != ssA(n7,n9) ).
cnf(u1959,axiom,
n5 != ssA(n6,n3) ).
cnf(u600,axiom,
ssA(n5,n6) != ssA(n5,n9) ).
cnf(u1366,axiom,
ssA(n5,n3) != ssA(n6,n2) ).
cnf(u748,axiom,
ssA(n8,n3) != ssA(n8,n8) ).
cnf(u1063,axiom,
ssA(n3,n6) != ssA(n8,n6) ).
cnf(u1906,axiom,
n1 != ssA(n4,n4) ).
cnf(u556,axiom,
ssA(n4,n6) != ssA(n4,n8) ).
cnf(u1325,axiom,
ssA(n2,n8) != ssA(n3,n7) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ068+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.36 % Computer : n015.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 22:42:01 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.39 Running first-order model finding
% 0.10/0.39 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.74/0.72 % (2086237)Will run a generic schedule for satisfiability detection.
% 1.74/0.72 % (2086248)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2337864000:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.74/0.72 % (2086243)% WARNING: option uhcvi not known.
% 1.74/0.72 % (2086242)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1114201170_2999 on theBenchmark for (2999ds/0Mi)
% 1.74/0.72 % (2086243)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2339580390:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.74/0.72 % (2086245)dis+10_1_sil=32000:sp=arity:random_seed=894124988:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.74/0.72 % (2086244)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2105385178:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.74/0.72 % (2086246)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2556138047:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.74/0.72 % (2086247)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3636162458:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.74/0.72 % (2086248)Instruction limit reached!
% 1.74/0.72 % (2086248)------------------------------
% 1.74/0.72 % (2086248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.72 % (2086248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.72 % (2086248)CaDiCaL version: 2.1.3
% 1.74/0.72 % (2086248)Termination reason: Instruction limit
% 1.74/0.72 % (2086248)Termination phase: Saturation
% 1.74/0.72 % (2086248)Time elapsed: 0.043 s
% 1.74/0.72 % (2086248)Peak memory usage: 15 MB
% 1.74/0.72 % (2086248)Instructions burned: 162 (million)
% 1.74/0.72 % (2086245)Instruction limit reached!
% 1.74/0.72 % (2086245)------------------------------
% 1.74/0.72 % (2086245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.72 % (2086245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.72 % (2086245)CaDiCaL version: 2.1.3
% 1.74/0.72 % (2086245)Termination reason: Instruction limit
% 1.74/0.72 % (2086245)Termination phase: Saturation
% 1.74/0.72 % (2086245)Time elapsed: 0.046 s
% 1.74/0.72 % (2086245)Peak memory usage: 14 MB
% 1.74/0.72 % (2086245)Instructions burned: 103 (million)
% 1.74/0.72 % (2086256)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=374174188:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.74/0.72 % (2086246)Instruction limit reached!
% 1.74/0.72 % (2086246)------------------------------
% 1.74/0.72 % (2086246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.72 % (2086246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.72 % (2086246)CaDiCaL version: 2.1.3
% 1.74/0.72 % (2086246)Termination reason: Instruction limit
% 1.74/0.72 % (2086246)Termination phase: Saturation
% 1.74/0.72 % (2086246)Time elapsed: 0.050 s
% 1.74/0.72 % (2086246)Peak memory usage: 13 MB
% 1.74/0.72 % (2086246)Instructions burned: 116 (million)
% 1.74/0.72 % (2086247)Instruction limit reached!
% 1.74/0.72 % (2086247)------------------------------
% 1.74/0.72 % (2086247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.72 % (2086247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.72 % (2086247)CaDiCaL version: 2.1.3
% 1.74/0.72 % (2086247)Termination reason: Instruction limit
% 1.74/0.72 % (2086247)Termination phase: Saturation
% 1.74/0.72 % (2086247)Time elapsed: 0.054 s
% 1.74/0.72 % (2086247)Peak memory usage: 12 MB
% 1.74/0.72 % (2086247)Instructions burned: 134 (million)
% 1.74/0.72 % (2086258)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=827377632:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.74/0.72 % (2086259)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=3230424587:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.74/0.72 % (2086260)ott-21_1_sil=16000:fs=off:random_seed=220873995:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.74/0.72 % (2086258)Instruction limit reached!
% 1.74/0.72 % (2086258)------------------------------
% 1.74/0.72 % (2086258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.72 % (2086258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.72 % (2086258)CaDiCaL version: 2.1.3
% 1.74/0.72 % (2086258)Termination reason: Instruction limit
% 1.74/0.72 % (2086258)Termination phase: Saturation
% 1.74/0.72 % (2086258)Time elapsed: 0.055 s
% 1.74/0.72 % (2086258)Peak memory usage: 14 MB
% 1.74/0.72 % (2086258)Instructions burned: 132 (million)
% 1.74/0.72 % Detected minimum model sizes of [9]
% 1.74/0.72 % Detected maximum model sizes of [max]
% 1.74/0.72 % TRYING [9]
% 1.74/0.72 % (2086264)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=88021786:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.74/0.72 % (2086260)Instruction limit reached!
% 1.74/0.72 % (2086260)------------------------------
% 1.74/0.72 % (2086260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.72 % (2086260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.72 % (2086260)CaDiCaL version: 2.1.3
% 1.74/0.72 % (2086260)Termination reason: Instruction limit
% 1.74/0.72 % (2086260)Termination phase: Saturation
% 1.74/0.72 % (2086260)Time elapsed: 0.074 s
% 1.74/0.72 % (2086260)Peak memory usage: 12 MB
% 1.74/0.72 % (2086260)Instructions burned: 181 (million)
% 1.74/0.72 % (2086266)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3036729122:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 1.74/0.72 % Detected minimum model sizes of [9]
% 1.74/0.72 % Detected maximum model sizes of [max]
% 1.74/0.72 % TRYING [9]
% 1.74/0.72 % (2086256)Instruction limit reached!
% 1.74/0.72 % (2086256)------------------------------
% 1.74/0.72 % (2086256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.72 % (2086256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.72 % (2086256)CaDiCaL version: 2.1.3
% 1.74/0.72 % (2086256)Termination reason: Instruction limit
% 1.74/0.72 % (2086256)Termination phase: Finite model building constraint generation
% 1.74/0.72 % (2086256)Time elapsed: 0.153 s
% 1.74/0.72 % (2086256)Peak memory usage: 41 MB
% 1.74/0.72 % (2086256)Instructions burned: 719 (million)
% 1.74/0.72 % (2086268)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=213405790:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 1.74/0.72 % (2086244) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2086237-2086244"...
% 1.74/0.72 % (2086244)...printing done.
% 1.74/0.72 % SZS status Satisfiable for theBenchmark
% 1.74/0.72 % SZS output start Saturation.
% See solution above
% 1.74/0.73 % SZS output start Definitions and Model Updates.
% 1.74/0.73 for all inputs,
% 1.74/0.73 define ssP(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56,X57,X58,X59,X60,X61,X62,X63,X64,X65,X66,X67,X68,X69,X70,X71,X72,X73,X74,X75,X76,X77,X78,X79,X80) := $true
% 1.74/0.73 % SZS output end Definitions and Model Updates.
% 1.74/0.73 % (2086244)------------------------------
% 1.74/0.73 % (2086244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.73 % (2086244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.73 % (2086244)CaDiCaL version: 2.1.3
% 1.74/0.73 % (2086244)Termination reason: Satisfiable
% 1.74/0.73 % (2086244)Time elapsed: 0.264 s
% 1.74/0.73 % (2086244)Peak memory usage: 17 MB
% 1.74/0.73 % (2086244)Instructions burned: 525 (million)
% 1.74/0.73 % (2086237)Success in time 0.323 s
% 1.74/0.73 % Vampire exiting
%------------------------------------------------------------------------------