%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : PUZ080+2 : TPTP v9.3.1. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n004.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 : Thu Sep 24 02:02:34 PM UTC 2026
% Result : Satisfiable 2.22s 6.35s
% Output : Saturation 2.22s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_909ERROR: Could not build tree for root c_0_973ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(c_0_887,plain,
p(n1,n4,n3),
inference(split_conjunct,[status(thm)],[ax143]),
[final] ).
cnf(c_0_889,plain,
p(n1,n6,n1),
inference(split_conjunct,[status(thm)],[ax161]),
[final] ).
cnf(c_0_892,plain,
p(n4,n4,n8),
inference(split_conjunct,[status(thm)],[ax448]),
[final] ).
cnf(c_0_894,plain,
p(n5,n4,n4),
inference(split_conjunct,[status(thm)],[ax544]),
[final] ).
cnf(c_0_896,plain,
p(n6,n5,n1),
inference(split_conjunct,[status(thm)],[ax651]),
[final] ).
cnf(c_0_898,plain,
p(n7,n4,n7),
inference(split_conjunct,[status(thm)],[ax747]),
[final] ).
cnf(c_0_900,plain,
p(n8,n3,n1),
inference(split_conjunct,[status(thm)],[ax831]),
[final] ).
cnf(c_0_914,plain,
p(n7,n6,n2),
inference(split_conjunct,[status(thm)],[ax762]),
[final] ).
cnf(c_0_925,plain,
p(n3,n1,n9),
inference(split_conjunct,[status(thm)],[ax319]),
[final] ).
cnf(c_0_927,plain,
p(n2,n5,n9),
inference(split_conjunct,[status(thm)],[ax259]),
[final] ).
cnf(c_0_930,plain,
p(n7,n3,n6),
inference(split_conjunct,[status(thm)],[ax736]),
[final] ).
cnf(c_0_933,plain,
p(n9,n3,n8),
inference(split_conjunct,[status(thm)],[ax938]),
[final] ).
cnf(c_0_948,plain,
~ p(n1,n4,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_886,c_0_887])]),
[final] ).
cnf(c_0_949,plain,
~ p(n2,n4,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_888,c_0_889])]),
[final] ).
cnf(c_0_950,plain,
~ p(n3,n4,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_890,c_0_889])]),
[final] ).
cnf(c_0_951,plain,
~ p(n4,n4,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_891,c_0_892])]),
[final] ).
cnf(c_0_952,plain,
~ p(n5,n4,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_893,c_0_894])]),
[final] ).
cnf(c_0_953,plain,
~ p(n6,n4,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_895,c_0_896])]),
[final] ).
cnf(c_0_954,plain,
~ p(n7,n4,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_897,c_0_898])]),
[final] ).
cnf(c_0_955,plain,
~ p(n8,n4,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_899,c_0_900])]),
[final] ).
cnf(c_0_973,plain,
~ p(n1,n4,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_909,c_0_887])]),
[final] ).
cnf(c_0_974,plain,
~ p(n4,n4,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_910,c_0_892])]),
[final] ).
cnf(c_0_975,plain,
~ p(n5,n4,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_911,c_0_894])]),
[final] ).
cnf(c_0_976,plain,
~ p(n7,n4,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_912,c_0_898])]),
[final] ).
cnf(c_0_977,plain,
~ p(n8,n4,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_913,c_0_914])]),
[final] ).
cnf(c_0_978,plain,
~ p(n9,n4,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_915,c_0_914])]),
[final] ).
cnf(c_0_984,plain,
p(n2,n2,n7),
inference(split_conjunct,[status(thm)],[ax227]),
[final] ).
cnf(c_0_987,plain,
p(n8,n7,n9),
inference(split_conjunct,[status(thm)],[ax879]),
[final] ).
cnf(c_0_990,plain,
~ p(n1,n3,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_924,c_0_925])]),
[final] ).
cnf(c_0_991,plain,
~ p(n2,n3,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_926,c_0_927])]),
[final] ).
cnf(c_0_992,plain,
~ p(n3,n3,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_928,c_0_925])]),
[final] ).
cnf(c_0_993,plain,
~ p(n7,n3,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_929,c_0_930])]),
[final] ).
cnf(c_0_994,plain,
~ p(n8,n3,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_931,c_0_900])]),
[final] ).
cnf(c_0_995,plain,
~ p(n9,n3,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_932,c_0_933])]),
[final] ).
cnf(c_0_1010,plain,
p(n9,n4,n1),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_947,c_0_948]),c_0_949]),c_0_950]),c_0_951]),c_0_952]),c_0_953]),c_0_954]),c_0_955]),
[final] ).
cnf(c_0_1016,plain,
p(n9,n7,n3),
inference(split_conjunct,[status(thm)],[ax973]),
[final] ).
cnf(c_0_1018,plain,
p(n2,n8,n6),
inference(split_conjunct,[status(thm)],[ax286]),
[final] ).
cnf(c_0_1021,plain,
p(n3,n9,n4),
inference(split_conjunct,[status(thm)],[ax394]),
[final] ).
cnf(c_0_1051,plain,
~ p(n1,n2,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_982,c_0_925])]),
[final] ).
cnf(c_0_1052,plain,
~ p(n2,n2,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_983,c_0_984])]),
[final] ).
cnf(c_0_1053,plain,
~ p(n3,n2,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_985,c_0_925])]),
[final] ).
cnf(c_0_1054,plain,
~ p(n8,n2,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_986,c_0_987])]),
[final] ).
cnf(c_0_1064,plain,
~ p(n1,n4,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1002,c_0_887])]),
[final] ).
cnf(c_0_1065,plain,
~ p(n2,n4,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1003,c_0_927])]),
[final] ).
cnf(c_0_1066,plain,
~ p(n3,n4,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1004,c_0_927])]),
[final] ).
cnf(c_0_1067,plain,
~ p(n4,n4,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1005,c_0_892])]),
[final] ).
cnf(c_0_1068,plain,
~ p(n5,n4,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1006,c_0_894])]),
[final] ).
cnf(c_0_1069,plain,
~ p(n7,n4,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1007,c_0_898])]),
[final] ).
cnf(c_0_1070,plain,
~ p(n8,n4,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1008,c_0_987])]),
[final] ).
cnf(c_0_1071,plain,
~ p(n9,n4,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1009,c_0_1010])]),
[final] ).
cnf(c_0_1075,plain,
~ p(n1,n7,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1012,c_0_887])]),
[final] ).
cnf(c_0_1076,plain,
~ p(n1,n8,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1013,c_0_887])]),
[final] ).
cnf(c_0_1077,plain,
~ p(n1,n9,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1014,c_0_887])]),
[final] ).
cnf(c_0_1078,plain,
~ p(n2,n7,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1015,c_0_1016])]),
[final] ).
cnf(c_0_1079,plain,
~ p(n2,n8,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1017,c_0_1018])]),
[final] ).
cnf(c_0_1080,plain,
~ p(n3,n7,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1019,c_0_1016])]),
[final] ).
cnf(c_0_1081,plain,
~ p(n3,n9,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1020,c_0_1021])]),
[final] ).
cnf(c_0_1086,plain,
p(n7,n7,n1),
inference(split_conjunct,[status(thm)],[ax771]),
[final] ).
cnf(c_0_1123,plain,
~ p(n4,n2,n9),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1055,c_0_1056]),c_0_1057]),c_0_1058]),
[final] ).
cnf(c_0_1124,plain,
~ p(n6,n2,n9),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1059,c_0_1056]),c_0_1060]),c_0_1061]),
[final] ).
cnf(c_0_1126,plain,
p(n6,n4,n9),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_1063,c_0_1064]),c_0_1065]),c_0_1066]),c_0_1067]),c_0_1068]),c_0_1069]),c_0_1070]),c_0_1071]),
[final] ).
cnf(c_0_1144,plain,
~ p(n1,n7,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1082,c_0_889])]),
[final] ).
cnf(c_0_1145,plain,
~ p(n1,n8,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1083,c_0_889])]),
[final] ).
cnf(c_0_1146,plain,
~ p(n1,n9,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1084,c_0_889])]),
[final] ).
cnf(c_0_1147,plain,
~ p(n2,n7,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1085,c_0_1086])]),
[final] ).
cnf(c_0_1148,plain,
~ p(n2,n8,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1087,c_0_1018])]),
[final] ).
cnf(c_0_1149,plain,
~ p(n3,n7,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1088,c_0_1086])]),
[final] ).
cnf(c_0_1150,plain,
~ p(n3,n9,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1089,c_0_1021])]),
[final] ).
cnf(c_0_1161,plain,
p(n4,n9,n2),
inference(split_conjunct,[status(thm)],[ax492]),
[final] ).
cnf(c_0_1174,plain,
p(n4,n6,n6),
inference(split_conjunct,[status(thm)],[ax466]),
[final] ).
cnf(c_0_1176,plain,
p(n5,n6,n7),
inference(split_conjunct,[status(thm)],[ax567]),
[final] ).
cnf(c_0_1179,plain,
p(n8,n1,n3),
inference(split_conjunct,[status(thm)],[ax813]),
[final] ).
cnf(c_0_1224,plain,
~ p(n6,n3,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1125,c_0_1126])]),
[final] ).
cnf(c_0_1248,plain,
~ p(n1,n5,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1157,c_0_1126])]),
[final] ).
cnf(c_0_1249,plain,
~ p(n2,n5,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1158,c_0_927])]),
[final] ).
cnf(c_0_1250,plain,
~ p(n3,n5,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1159,c_0_1126])]),
[final] ).
cnf(c_0_1251,plain,
~ p(n4,n5,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1160,c_0_1161])]),
[final] ).
cnf(c_0_1252,plain,
~ p(n6,n5,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1162,c_0_896])]),
[final] ).
cnf(c_0_1253,plain,
~ p(n7,n5,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1163,c_0_914])]),
[final] ).
cnf(c_0_1254,plain,
~ p(n8,n5,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1164,c_0_914])]),
[final] ).
cnf(c_0_1255,plain,
~ p(n9,n5,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1165,c_0_914])]),
[final] ).
cnf(c_0_1261,plain,
~ p(n1,n6,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1170,c_0_887])]),
[final] ).
cnf(c_0_1262,plain,
~ p(n2,n6,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1171,c_0_887])]),
[final] ).
cnf(c_0_1263,plain,
~ p(n3,n6,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1172,c_0_887])]),
[final] ).
cnf(c_0_1264,plain,
~ p(n4,n6,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1173,c_0_1174])]),
[final] ).
cnf(c_0_1265,plain,
~ p(n5,n6,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1175,c_0_1176])]),
[final] ).
cnf(c_0_1266,plain,
~ p(n7,n6,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1177,c_0_914])]),
[final] ).
cnf(c_0_1267,plain,
~ p(n8,n6,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1178,c_0_1179])]),
[final] ).
cnf(c_0_1268,plain,
~ p(n9,n6,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1180,c_0_1016])]),
[final] ).
cnf(c_0_1308,plain,
p(n4,n1,n4),
inference(split_conjunct,[status(thm)],[ax414]),
[final] ).
cnf(c_0_1350,plain,
p(n5,n5,n2),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_1247,c_0_1248]),c_0_1249]),c_0_1250]),c_0_1251]),c_0_1252]),c_0_1253]),c_0_1254]),c_0_1255]),
[final] ).
cnf(c_0_1355,plain,
p(n6,n6,n3),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_1260,c_0_1261]),c_0_1262]),c_0_1263]),c_0_1264]),c_0_1265]),c_0_1266]),c_0_1267]),c_0_1268]),
[final] ).
cnf(c_0_1386,plain,
~ p(n1,n3,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1284,c_0_984])]),
[final] ).
cnf(c_0_1387,plain,
~ p(n2,n3,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1285,c_0_984])]),
[final] ).
cnf(c_0_1388,plain,
~ p(n3,n3,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1286,c_0_984])]),
[final] ).
cnf(c_0_1389,plain,
~ p(n5,n3,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1287,c_0_1176])]),
[final] ).
cnf(c_0_1390,plain,
~ p(n7,n3,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1288,c_0_930])]),
[final] ).
cnf(c_0_1391,plain,
~ p(n8,n3,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1289,c_0_900])]),
[final] ).
cnf(c_0_1392,plain,
~ p(n9,n3,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1290,c_0_933])]),
[final] ).
cnf(c_0_1414,plain,
~ p(n3,n3,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1306,c_0_1021])]),
[final] ).
cnf(c_0_1415,plain,
~ p(n4,n3,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1307,c_0_1308])]),
[final] ).
cnf(c_0_1416,plain,
~ p(n5,n3,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1309,c_0_1308])]),
[final] ).
cnf(c_0_1417,plain,
~ p(n6,n3,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1310,c_0_1308])]),
[final] ).
cnf(c_0_1418,plain,
~ p(n7,n3,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1311,c_0_930])]),
[final] ).
cnf(c_0_1419,plain,
~ p(n8,n3,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1312,c_0_900])]),
[final] ).
cnf(c_0_1420,plain,
~ p(n9,n3,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1313,c_0_933])]),
[final] ).
cnf(c_0_1426,plain,
~ p(n1,n6,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1319,c_0_889])]),
[final] ).
cnf(c_0_1427,plain,
~ p(n2,n6,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1320,c_0_927])]),
[final] ).
cnf(c_0_1428,plain,
~ p(n3,n6,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1321,c_0_927])]),
[final] ).
cnf(c_0_1429,plain,
~ p(n4,n6,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1322,c_0_1174])]),
[final] ).
cnf(c_0_1430,plain,
~ p(n5,n6,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1323,c_0_1176])]),
[final] ).
cnf(c_0_1431,plain,
~ p(n6,n6,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1324,c_0_1126])]),
[final] ).
cnf(c_0_1432,plain,
~ p(n7,n6,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1325,c_0_914])]),
[final] ).
cnf(c_0_1433,plain,
~ p(n8,n6,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1326,c_0_987])]),
[final] ).
cnf(c_0_1449,plain,
~ p(n3,n1,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1334,c_0_984])]),
[final] ).
cnf(c_0_1450,plain,
~ p(n3,n2,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1335,c_0_984])]),
[final] ).
cnf(c_0_1451,plain,
~ p(n3,n4,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1336,c_0_898])]),
[final] ).
cnf(c_0_1452,plain,
~ p(n3,n6,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1337,c_0_1176])]),
[final] ).
cnf(c_0_1453,plain,
~ p(n3,n8,n7),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1338,c_0_1339]),c_0_1340]),
[final] ).
cnf(c_0_1454,plain,
~ p(n3,n9,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1341,c_0_1021])]),
[final] ).
cnf(c_0_1460,plain,
~ p(n4,n4,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1346,c_0_892])]),
[final] ).
cnf(c_0_1461,plain,
~ p(n4,n6,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1347,c_0_1174])]),
[final] ).
cnf(c_0_1462,plain,
~ p(n5,n4,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1348,c_0_894])]),
[final] ).
cnf(c_0_1463,plain,
~ p(n5,n5,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1349,c_0_1350])]),
[final] ).
cnf(c_0_1464,plain,
~ p(n5,n6,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1351,c_0_1176])]),
[final] ).
cnf(c_0_1465,plain,
~ p(n6,n4,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1352,c_0_1126])]),
[final] ).
cnf(c_0_1466,plain,
~ p(n6,n5,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1353,c_0_896])]),
[final] ).
cnf(c_0_1467,plain,
~ p(n6,n6,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1354,c_0_1355])]),
[final] ).
cnf(c_0_1476,plain,
~ p(n1,n7,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1363,c_0_1021])]),
[final] ).
cnf(c_0_1477,plain,
~ p(n2,n7,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1364,c_0_1021])]),
[final] ).
cnf(c_0_1478,plain,
~ p(n3,n7,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1365,c_0_1021])]),
[final] ).
cnf(c_0_1479,plain,
~ p(n4,n7,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1366,c_0_1308])]),
[final] ).
cnf(c_0_1480,plain,
~ p(n5,n7,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1367,c_0_894])]),
[final] ).
cnf(c_0_1481,plain,
~ p(n7,n7,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1368,c_0_1086])]),
[final] ).
cnf(c_0_1482,plain,
~ p(n8,n7,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1369,c_0_987])]),
[final] ).
cnf(c_0_1483,plain,
~ p(n9,n7,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1370,c_0_1016])]),
[final] ).
cnf(c_0_1493,plain,
~ p(n1,n1,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1378,c_0_984])]),
[final] ).
cnf(c_0_1494,plain,
~ p(n2,n1,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1379,c_0_984])]),
[final] ).
cnf(c_0_1495,plain,
~ p(n4,n1,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1380,c_0_1308])]),
[final] ).
cnf(c_0_1496,plain,
~ p(n5,n1,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1381,c_0_1176])]),
[final] ).
cnf(c_0_1497,plain,
~ p(n7,n1,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1382,c_0_898])]),
[final] ).
cnf(c_0_1498,plain,
~ p(n8,n1,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1383,c_0_1179])]),
[final] ).
cnf(c_0_1509,plain,
~ p(n1,n5,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1399,c_0_887])]),
[final] ).
cnf(c_0_1510,plain,
~ p(n2,n5,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1400,c_0_887])]),
[final] ).
cnf(c_0_1511,plain,
~ p(n3,n5,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1401,c_0_887])]),
[final] ).
cnf(c_0_1512,plain,
~ p(n5,n5,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1402,c_0_1350])]),
[final] ).
cnf(c_0_1513,plain,
~ p(n6,n5,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1403,c_0_896])]),
[final] ).
cnf(c_0_1514,plain,
~ p(n8,n5,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1404,c_0_1179])]),
[final] ).
cnf(c_0_1515,plain,
~ p(n9,n5,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1405,c_0_1016])]),
[final] ).
cnf(c_0_1518,plain,
~ p(n2,n2,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1407,c_0_984])]),
[final] ).
cnf(c_0_1519,plain,
~ p(n3,n2,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1408,c_0_1021])]),
[final] ).
cnf(c_0_1520,plain,
~ p(n4,n2,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1409,c_0_1308])]),
[final] ).
cnf(c_0_1521,plain,
~ p(n5,n2,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1410,c_0_1308])]),
[final] ).
cnf(c_0_1522,plain,
~ p(n6,n2,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1411,c_0_1308])]),
[final] ).
cnf(c_0_1528,plain,
p(n9,n6,n9),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_1425,c_0_1426]),c_0_1427]),c_0_1428]),c_0_1429]),c_0_1430]),c_0_1431]),c_0_1432]),c_0_1433]),
[final] ).
cnf(c_0_1553,plain,
p(n4,n5,n5),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_1459,c_0_1460]),c_0_1461]),c_0_1462]),c_0_1463]),c_0_1464]),c_0_1465]),c_0_1466]),c_0_1467]),
[final] ).
cnf(c_0_1566,plain,
p(n6,n7,n4),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_1475,c_0_1476]),c_0_1477]),c_0_1478]),c_0_1479]),c_0_1480]),c_0_1481]),c_0_1482]),c_0_1483]),
[final] ).
cnf(c_0_1579,plain,
~ p(n6,n1,n7),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1499,c_0_1500]),c_0_1501]),
[final] ).
cnf(c_0_1595,plain,
~ p(n4,n5,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1516,c_0_1355])]),
[final] ).
cnf(c_0_1598,plain,
~ p(n1,n2,n4),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1523,c_0_1524]),c_0_1525]),
[final] ).
cnf(c_0_1600,plain,
p(n7,n2,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1527,c_0_1528])]),
[final] ).
cnf(c_0_1603,plain,
~ p(n1,n6,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1529,c_0_889])]),
[final] ).
cnf(c_0_1604,plain,
~ p(n3,n6,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1530,c_0_1021])]),
[final] ).
cnf(c_0_1605,plain,
~ p(n4,n6,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1531,c_0_1308])]),
[final] ).
cnf(c_0_1606,plain,
~ p(n5,n6,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1532,c_0_894])]),
[final] ).
cnf(c_0_1607,plain,
~ p(n6,n6,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1533,c_0_894])]),
[final] ).
cnf(c_0_1608,plain,
~ p(n7,n6,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1534,c_0_914])]),
[final] ).
cnf(c_0_1624,plain,
~ p(n4,n7,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1549,c_0_1086])]),
[final] ).
cnf(c_0_1625,plain,
~ p(n4,n7,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1550,c_0_1161])]),
[final] ).
cnf(c_0_1626,plain,
~ p(n4,n7,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1551,c_0_1016])]),
[final] ).
cnf(c_0_1627,plain,
~ p(n4,n7,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1552,c_0_1553])]),
[final] ).
cnf(c_0_1628,plain,
~ p(n4,n7,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1554,c_0_1174])]),
[final] ).
cnf(c_0_1629,plain,
~ p(n4,n7,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1555,c_0_892])]),
[final] ).
cnf(c_0_1630,plain,
~ p(n4,n7,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1556,c_0_987])]),
[final] ).
cnf(c_0_1642,plain,
~ p(n1,n7,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1562,c_0_1018])]),
[final] ).
cnf(c_0_1643,plain,
~ p(n2,n7,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1563,c_0_1018])]),
[final] ).
cnf(c_0_1644,plain,
~ p(n3,n7,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1564,c_0_1018])]),
[final] ).
cnf(c_0_1645,plain,
~ p(n6,n7,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1565,c_0_1566])]),
[final] ).
cnf(c_0_1646,plain,
~ p(n7,n7,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1567,c_0_930])]),
[final] ).
cnf(c_0_1647,plain,
~ p(n8,n7,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1568,c_0_987])]),
[final] ).
cnf(c_0_1648,plain,
~ p(n9,n7,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1569,c_0_1016])]),
[final] ).
cnf(c_0_1659,plain,
~ p(n3,n1,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1573,c_0_925])]),
[final] ).
cnf(c_0_1660,plain,
~ p(n4,n1,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1574,c_0_1308])]),
[final] ).
cnf(c_0_1661,plain,
~ p(n7,n1,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1575,c_0_914])]),
[final] ).
cnf(c_0_1662,plain,
~ p(n8,n1,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1576,c_0_1179])]),
[final] ).
cnf(c_0_1664,plain,
p(n9,n1,n7),
inference(sr,[status(thm)],[c_0_1578,c_0_1579]),
[final] ).
cnf(c_0_1681,plain,
~ p(n2,n5,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1588,c_0_927])]),
[final] ).
cnf(c_0_1682,plain,
~ p(n3,n5,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1589,c_0_1021])]),
[final] ).
cnf(c_0_1683,plain,
~ p(n4,n5,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1590,c_0_1308])]),
[final] ).
cnf(c_0_1684,plain,
~ p(n5,n5,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1591,c_0_894])]),
[final] ).
cnf(c_0_1685,plain,
~ p(n6,n5,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1592,c_0_894])]),
[final] ).
cnf(c_0_1687,plain,
p(n7,n5,n3),
inference(sr,[status(thm)],[c_0_1594,c_0_1595]),
[final] ).
cnf(c_0_1690,plain,
~ p(n7,n2,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1599,c_0_1600])]),
[final] ).
cnf(c_0_1693,plain,
~ p(n9,n6,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1609,c_0_1528])]),
[final] ).
cnf(c_0_1712,plain,
~ p(n1,n4,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1616,c_0_887])]),
[final] ).
cnf(c_0_1713,plain,
~ p(n1,n6,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1617,c_0_889])]),
[final] ).
cnf(c_0_1714,plain,
~ p(n2,n4,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1618,c_0_984])]),
[final] ).
cnf(c_0_1715,plain,
~ p(n2,n5,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1619,c_0_984])]),
[final] ).
cnf(c_0_1716,plain,
~ p(n2,n6,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1620,c_0_984])]),
[final] ).
cnf(c_0_1718,plain,
p(n4,n7,n7),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_1623,c_0_1624]),c_0_1625]),c_0_1626]),c_0_1479]),c_0_1627]),c_0_1628]),c_0_1629]),c_0_1630]),
[final] ).
cnf(c_0_1730,plain,
p(n5,n7,n6),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_1641,c_0_1642]),c_0_1643]),c_0_1644]),c_0_1628]),c_0_1645]),c_0_1646]),c_0_1647]),c_0_1648]),
[final] ).
cnf(c_0_1734,plain,
p(n8,n9,n7),
inference(split_conjunct,[status(thm)],[ax897]),
[final] ).
cnf(c_0_1753,plain,
~ p(n9,n1,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1663,c_0_1664])]),
[final] ).
cnf(c_0_1771,plain,
~ p(n7,n5,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1686,c_0_1687])]),
[final] ).
cnf(c_0_1798,plain,
~ p(n2,n5,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1704,c_0_927])]),
[final] ).
cnf(c_0_1799,plain,
~ p(n4,n5,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1705,c_0_892])]),
[final] ).
cnf(c_0_1800,plain,
~ p(n5,n5,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1706,c_0_892])]),
[final] ).
cnf(c_0_1801,plain,
~ p(n6,n5,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1707,c_0_892])]),
[final] ).
cnf(c_0_1802,plain,
~ p(n9,n5,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1708,c_0_933])]),
[final] ).
cnf(c_0_1806,plain,
~ p(n1,n5,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1717,c_0_1718])]),
[final] ).
cnf(c_0_1814,plain,
~ p(n1,n9,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1725,c_0_1018])]),
[final] ).
cnf(c_0_1815,plain,
~ p(n2,n9,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1726,c_0_1018])]),
[final] ).
cnf(c_0_1816,plain,
~ p(n3,n9,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1727,c_0_1018])]),
[final] ).
cnf(c_0_1817,plain,
~ p(n4,n9,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1728,c_0_1174])]),
[final] ).
cnf(c_0_1818,plain,
~ p(n5,n9,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1729,c_0_1730])]),
[final] ).
cnf(c_0_1819,plain,
~ p(n6,n9,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1731,c_0_1730])]),
[final] ).
cnf(c_0_1820,plain,
~ p(n7,n9,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1732,c_0_930])]),
[final] ).
cnf(c_0_1821,plain,
~ p(n8,n9,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1733,c_0_1734])]),
[final] ).
cnf(c_0_1845,plain,
~ p(n5,n1,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1754,c_0_1350])]),
[final] ).
cnf(c_0_1848,plain,
~ p(n1,n1,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1756,c_0_889])]),
[final] ).
cnf(c_0_1849,plain,
~ p(n3,n1,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1757,c_0_925])]),
[final] ).
cnf(c_0_1850,plain,
~ p(n4,n1,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1758,c_0_1308])]),
[final] ).
cnf(c_0_1851,plain,
~ p(n6,n1,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1759,c_0_896])]),
[final] ).
cnf(c_0_1852,plain,
~ p(n7,n1,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1760,c_0_1086])]),
[final] ).
cnf(c_0_1853,plain,
~ p(n8,n1,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1761,c_0_1179])]),
[final] ).
cnf(c_0_1854,plain,
~ p(n9,n1,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1762,c_0_900])]),
[final] ).
cnf(c_0_1901,plain,
~ p(n7,n5,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1803,c_0_1687])]),
[final] ).
cnf(c_0_1903,plain,
p(n3,n5,n7),
inference(sr,[status(thm)],[c_0_1805,c_0_1806]),
[final] ).
cnf(c_0_1905,plain,
~ p(n2,n5,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1807,c_0_927])]),
[final] ).
cnf(c_0_1906,plain,
~ p(n4,n5,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1808,c_0_1174])]),
[final] ).
cnf(c_0_1907,plain,
~ p(n5,n5,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1809,c_0_1174])]),
[final] ).
cnf(c_0_1908,plain,
~ p(n6,n5,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1810,c_0_1174])]),
[final] ).
cnf(c_0_1909,plain,
~ p(n7,n5,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1811,c_0_930])]),
[final] ).
cnf(c_0_1911,plain,
p(n9,n9,n6),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_1813,c_0_1814]),c_0_1815]),c_0_1816]),c_0_1817]),c_0_1818]),c_0_1819]),c_0_1820]),c_0_1821]),
[final] ).
cnf(c_0_1924,plain,
~ p(n1,n2,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1832,c_0_889])]),
[final] ).
cnf(c_0_1925,plain,
~ p(n2,n2,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1833,c_0_984])]),
[final] ).
cnf(c_0_1926,plain,
~ p(n6,n2,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1834,c_0_896])]),
[final] ).
cnf(c_0_1927,plain,
~ p(n7,n2,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1835,c_0_1086])]),
[final] ).
cnf(c_0_1928,plain,
~ p(n8,n2,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1836,c_0_900])]),
[final] ).
cnf(c_0_1929,plain,
~ p(n9,n2,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1837,c_0_900])]),
[final] ).
cnf(c_0_1942,plain,
~ p(n2,n1,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1856,c_0_1018])]),
[final] ).
cnf(c_0_1943,plain,
~ p(n3,n1,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1857,c_0_925])]),
[final] ).
cnf(c_0_1944,plain,
~ p(n4,n1,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1858,c_0_1308])]),
[final] ).
cnf(c_0_1945,plain,
~ p(n7,n1,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1859,c_0_930])]),
[final] ).
cnf(c_0_1946,plain,
~ p(n8,n1,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1860,c_0_930])]),
[final] ).
cnf(c_0_1947,plain,
~ p(n9,n1,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1861,c_0_930])]),
[final] ).
cnf(c_0_1960,plain,
~ p(n2,n9,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1875,c_0_927])]),
[final] ).
cnf(c_0_1961,plain,
~ p(n3,n9,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1876,c_0_925])]),
[final] ).
cnf(c_0_1962,plain,
~ p(n4,n9,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1877,c_0_1161])]),
[final] ).
cnf(c_0_1963,plain,
~ p(n6,n9,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1878,c_0_1126])]),
[final] ).
cnf(c_0_1964,plain,
~ p(n7,n9,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1879,c_0_987])]),
[final] ).
cnf(c_0_1965,plain,
~ p(n8,n9,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1880,c_0_987])]),
[final] ).
cnf(c_0_1966,plain,
~ p(n9,n9,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1881,c_0_987])]),
[final] ).
cnf(c_0_1976,plain,
~ p(n3,n3,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1889,c_0_930])]),
[final] ).
cnf(c_0_1977,plain,
~ p(n3,n6,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1890,c_0_1174])]),
[final] ).
cnf(c_0_1978,plain,
~ p(n3,n8,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1891,c_0_1018])]),
[final] ).
cnf(c_0_1990,plain,
~ p(n3,n5,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1902,c_0_1903])]),
[final] ).
cnf(c_0_1992,plain,
~ p(n9,n5,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1910,c_0_1911])]),
[final] ).
cnf(c_0_1996,plain,
~ p(n1,n3,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1914,c_0_933])]),
[final] ).
cnf(c_0_1997,plain,
~ p(n2,n2,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1915,c_0_984])]),
[final] ).
cnf(c_0_1998,plain,
~ p(n2,n3,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1916,c_0_933])]),
[final] ).
cnf(c_0_1999,plain,
~ p(n3,n1,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1917,c_0_925])]),
[final] ).
cnf(c_0_2000,plain,
~ p(n3,n3,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1918,c_0_933])]),
[final] ).
cnf(c_0_2009,plain,
~ p(n4,n9,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1930,c_0_1161])]),
[final] ).
cnf(c_0_2010,plain,
~ p(n6,n9,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1931,c_0_896])]),
[final] ).
cnf(c_0_2011,plain,
~ p(n7,n9,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1932,c_0_1086])]),
[final] ).
cnf(c_0_2012,plain,
~ p(n8,n9,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1933,c_0_1086])]),
[final] ).
cnf(c_0_2013,plain,
~ p(n9,n9,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1934,c_0_1086])]),
[final] ).
cnf(c_0_2038,plain,
~ p(n4,n9,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1967,c_0_1161])]),
[final] ).
cnf(c_0_2039,plain,
~ p(n6,n9,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1968,c_0_1355])]),
[final] ).
cnf(c_0_2040,plain,
~ p(n7,n9,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1969,c_0_1016])]),
[final] ).
cnf(c_0_2041,plain,
~ p(n8,n9,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1970,c_0_1179])]),
[final] ).
cnf(c_0_2042,plain,
~ p(n9,n9,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1971,c_0_1016])]),
[final] ).
cnf(c_0_2050,plain,
~ p(n1,n1,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1981,c_0_887])]),
[final] ).
cnf(c_0_2051,plain,
~ p(n1,n2,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1982,c_0_887])]),
[final] ).
cnf(c_0_2052,plain,
~ p(n1,n3,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1983,c_0_887])]),
[final] ).
cnf(c_0_2053,plain,
~ p(n2,n1,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1984,c_0_1179])]),
[final] ).
cnf(c_0_2054,plain,
~ p(n2,n2,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1985,c_0_984])]),
[final] ).
cnf(c_0_2055,plain,
~ p(n3,n1,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1986,c_0_925])]),
[final] ).
cnf(c_0_2061,plain,
~ p(n3,n5,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1993,c_0_1903])]),
[final] ).
cnf(c_0_2066,plain,
~ p(n1,n3,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2001,c_0_889])]),
[final] ).
cnf(c_0_2067,plain,
~ p(n2,n3,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2002,c_0_900])]),
[final] ).
cnf(c_0_2068,plain,
~ p(n3,n3,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2003,c_0_900])]),
[final] ).
cnf(c_0_2092,plain,
~ p(n1,n8,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2020,c_0_1021])]),
[final] ).
cnf(c_0_2093,plain,
~ p(n2,n8,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2021,c_0_1018])]),
[final] ).
cnf(c_0_2094,plain,
~ p(n3,n8,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2022,c_0_1021])]),
[final] ).
cnf(c_0_2095,plain,
~ p(n4,n8,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2023,c_0_1308])]),
[final] ).
cnf(c_0_2096,plain,
~ p(n5,n8,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2024,c_0_894])]),
[final] ).
cnf(c_0_2097,plain,
~ p(n6,n8,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2025,c_0_1566])]),
[final] ).
cnf(c_0_2098,plain,
~ p(n9,n8,n4),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2026,c_0_2027]),c_0_2028]),
[final] ).
cnf(c_0_2194,plain,
~ p(n2,n8,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2145,c_0_927])]),
[final] ).
cnf(c_0_2195,plain,
~ p(n3,n8,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2146,c_0_925])]),
[final] ).
cnf(c_0_2196,plain,
~ p(n6,n8,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2147,c_0_1126])]),
[final] ).
cnf(c_0_2197,plain,
~ p(n7,n8,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2148,c_0_987])]),
[final] ).
cnf(c_0_2198,plain,
~ p(n8,n8,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2149,c_0_987])]),
[final] ).
cnf(c_0_2199,plain,
~ p(n9,n8,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2150,c_0_987])]),
[final] ).
cnf(c_0_2201,plain,
p(n1,n9,n9),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1141,c_0_2152]),c_0_2153]),
[final] ).
cnf(c_0_2213,plain,
~ p(n6,n8,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2170,c_0_896])]),
[final] ).
cnf(c_0_2214,plain,
~ p(n7,n8,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2171,c_0_1086])]),
[final] ).
cnf(c_0_2215,plain,
~ p(n8,n8,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2172,c_0_1086])]),
[final] ).
cnf(c_0_2216,plain,
~ p(n9,n8,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2173,c_0_1086])]),
[final] ).
cnf(c_0_2219,plain,
~ p(n5,n7,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2175,c_0_1730])]),
[final] ).
cnf(c_0_2220,plain,
~ p(n6,n7,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2176,c_0_1566])]),
[final] ).
cnf(c_0_2221,plain,
~ p(n7,n7,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2177,c_0_1086])]),
[final] ).
cnf(c_0_2222,plain,
~ p(n8,n7,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2178,c_0_987])]),
[final] ).
cnf(c_0_2223,plain,
~ p(n9,n7,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2179,c_0_933])]),
[final] ).
cnf(c_0_2239,plain,
~ p(n1,n8,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2200,c_0_2201])]),
[final] ).
cnf(c_0_2242,plain,
~ p(n4,n1,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2202,c_0_1308])]),
[final] ).
cnf(c_0_2243,plain,
~ p(n4,n4,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2203,c_0_887])]),
[final] ).
cnf(c_0_2246,plain,
~ p(n1,n1,n8),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2207,c_0_2208]),c_0_2209]),
[final] ).
cnf(c_0_2269,plain,
~ p(n4,n3,n3),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2244,c_0_2245]),c_0_2246]),
[final] ).
cnf(c_0_2276,plain,
~ p(n1,n8,n8),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2250,c_0_2251]),c_0_2252]),c_0_2253]),
[final] ).
cnf(c_0_2277,plain,
~ p(n2,n8,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2254,c_0_1018])]),
[final] ).
cnf(c_0_2278,plain,
~ p(n3,n8,n8),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2255,c_0_2251]),c_0_2256]),c_0_2257]),
[final] ).
cnf(c_0_2279,plain,
~ p(n4,n8,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2258,c_0_892])]),
[final] ).
cnf(c_0_2280,plain,
~ p(n9,n8,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2259,c_0_933])]),
[final] ).
cnf(c_0_2282,plain,
p(n7,n8,n4),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2261,c_0_2262]),c_0_2263]),
[final] ).
cnf(c_0_2298,plain,
~ p(n7,n8,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2281,c_0_2282])]),
[final] ).
cnf(c_0_2335,plain,
p(n4,n3,n9),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2316,c_0_2317]),c_0_2318]),
[final] ).
cnf(c_0_2342,plain,
~ p(n1,n6,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2324,c_0_889])]),
[final] ).
cnf(c_0_2343,plain,
~ p(n4,n6,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2325,c_0_892])]),
[final] ).
cnf(c_0_2344,plain,
~ p(n5,n6,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2326,c_0_892])]),
[final] ).
cnf(c_0_2345,plain,
~ p(n6,n6,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2327,c_0_892])]),
[final] ).
cnf(c_0_2346,plain,
~ p(n7,n6,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2328,c_0_914])]),
[final] ).
cnf(c_0_2347,plain,
~ p(n9,n6,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2329,c_0_933])]),
[final] ).
cnf(c_0_2352,plain,
~ p(n4,n8,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2334,c_0_2335])]),
[final] ).
cnf(c_0_2400,plain,
p(n6,n8,n8),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2379,c_0_2373]),c_0_2380]),
[final] ).
cnf(c_0_2403,plain,
~ p(n6,n9,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2382,c_0_1161])]),
[final] ).
cnf(c_0_2404,plain,
~ p(n6,n9,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2383,c_0_1021])]),
[final] ).
cnf(c_0_2405,plain,
~ p(n6,n9,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2384,c_0_1734])]),
[final] ).
cnf(c_0_2406,plain,
~ p(n6,n9,n8),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2385,c_0_2358]),c_0_2386]),c_0_2387]),
[final] ).
cnf(c_0_2419,plain,
~ p(n6,n2,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2397,c_0_1355])]),
[final] ).
cnf(c_0_2420,plain,
~ p(n6,n2,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2398,c_0_984])]),
[final] ).
cnf(c_0_2421,plain,
~ p(n6,n2,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2399,c_0_2400])]),
[final] ).
cnf(c_0_2423,plain,
p(n6,n9,n5),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_2402,c_0_2010]),c_0_2403]),c_0_2039]),c_0_2404]),c_0_1819]),c_0_2405]),c_0_2406]),c_0_1963]),
[final] ).
cnf(c_0_2429,plain,
~ p(n4,n3,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2412,c_0_1718])]),
[final] ).
cnf(c_0_2439,plain,
~ p(n6,n2,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2422,c_0_2423])]),
[final] ).
cnf(c_0_2441,plain,
~ p(n4,n2,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2424,c_0_1161])]),
[final] ).
cnf(c_0_2442,plain,
~ p(n4,n3,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2425,c_0_1161])]),
[final] ).
cnf(c_0_2443,plain,
~ p(n5,n2,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2426,c_0_1350])]),
[final] ).
cnf(c_0_2444,plain,
~ p(n5,n3,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2427,c_0_1350])]),
[final] ).
cnf(c_0_2446,plain,
p(n6,n3,n7),
inference(sr,[status(thm)],[c_0_1500,c_0_2429]),
[final] ).
cnf(c_0_2449,plain,
~ p(n7,n2,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2431,c_0_914])]),
[final] ).
cnf(c_0_2450,plain,
~ p(n7,n3,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2432,c_0_930])]),
[final] ).
cnf(c_0_2451,plain,
~ p(n8,n3,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2433,c_0_900])]),
[final] ).
cnf(c_0_2452,plain,
~ p(n9,n3,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2434,c_0_933])]),
[final] ).
cnf(c_0_2461,plain,
~ p(n6,n3,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2445,c_0_2446])]),
[final] ).
cnf(c_0_2472,plain,
~ p(n6,n2,n2),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2462,c_0_2463]),c_0_2464]),
[final] ).
cnf(c_0_2482,plain,
p(n6,n1,n2),
inference(sr,[status(thm)],[c_0_2471,c_0_2472]),
[final] ).
cnf(c_0_2484,plain,
~ p(n1,n1,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2473,c_0_1308])]),
[final] ).
cnf(c_0_2485,plain,
~ p(n1,n4,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2474,c_0_887])]),
[final] ).
cnf(c_0_2486,plain,
~ p(n1,n9,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2475,c_0_1021])]),
[final] ).
cnf(c_0_2496,plain,
~ p(n3,n2,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2481,c_0_2482])]),
[final] ).
cnf(c_0_2533,plain,
~ p(n2,n2,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2492,c_0_984])]),
[final] ).
cnf(c_0_2535,plain,
~ p(n6,n4,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1090,c_0_1126])]),
[final] ).
cnf(c_0_2537,plain,
p(n3,n4,n6),
inference(sr,[status(thm)],[c_0_2495,c_0_2496]),
[final] ).
cnf(c_0_2543,plain,
~ p(n1,n5,n4),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2502,c_0_2159]),c_0_2503]),
[final] ).
cnf(c_0_2579,plain,
~ p(n3,n4,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2536,c_0_2537])]),
[final] ).
cnf(c_0_2584,plain,
p(n1,n3,n4),
inference(sr,[status(thm)],[c_0_2542,c_0_2543]),
[final] ).
cnf(c_0_2595,plain,
~ p(n1,n6,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2551,c_0_889])]),
[final] ).
cnf(c_0_2596,plain,
~ p(n7,n6,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2552,c_0_914])]),
[final] ).
cnf(c_0_2631,plain,
p(n2,n4,n2),
inference(sr,[status(thm)],[c_0_2578,c_0_2579]),
[final] ).
cnf(c_0_2632,plain,
~ p(n1,n1,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2580,c_0_2482])]),
[final] ).
cnf(c_0_2633,plain,
~ p(n1,n2,n2),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2581,c_0_2463]),c_0_2582]),
[final] ).
cnf(c_0_2634,plain,
~ p(n1,n3,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2583,c_0_2584])]),
[final] ).
cnf(c_0_2635,plain,
~ p(n3,n2,n2),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2585,c_0_2463]),c_0_2586]),
[final] ).
cnf(c_0_2640,plain,
~ p(n7,n2,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2590,c_0_1179])]),
[final] ).
cnf(c_0_2641,plain,
~ p(n8,n2,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2591,c_0_1179])]),
[final] ).
cnf(c_0_2642,plain,
~ p(n9,n2,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2592,c_0_1179])]),
[final] ).
cnf(c_0_2649,plain,
~ p(n9,n6,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2597,c_0_1528])]),
[final] ).
cnf(c_0_2652,plain,
~ p(n1,n4,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2599,c_0_887])]),
[final] ).
cnf(c_0_2653,plain,
~ p(n7,n4,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2600,c_0_898])]),
[final] ).
cnf(c_0_2654,plain,
~ p(n9,n4,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2601,c_0_1010])]),
[final] ).
cnf(c_0_2668,plain,
~ p(n4,n1,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2607,c_0_1308])]),
[final] ).
cnf(c_0_2669,plain,
~ p(n7,n1,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2608,c_0_933])]),
[final] ).
cnf(c_0_2670,plain,
~ p(n8,n1,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2609,c_0_1179])]),
[final] ).
cnf(c_0_2671,plain,
~ p(n9,n1,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2610,c_0_933])]),
[final] ).
cnf(c_0_2677,plain,
~ p(n1,n3,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2613,c_0_930])]),
[final] ).
cnf(c_0_2678,plain,
~ p(n2,n2,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2614,c_0_984])]),
[final] ).
cnf(c_0_2679,plain,
~ p(n2,n3,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2615,c_0_1018])]),
[final] ).
cnf(c_0_2691,plain,
~ p(n5,n9,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2622,c_0_1161])]),
[final] ).
cnf(c_0_2692,plain,
~ p(n5,n9,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2623,c_0_1021])]),
[final] ).
cnf(c_0_2693,plain,
~ p(n5,n9,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2624,c_0_1176])]),
[final] ).
cnf(c_0_2694,plain,
~ p(n5,n9,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2625,c_0_2400])]),
[final] ).
cnf(c_0_2695,plain,
~ p(n5,n9,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2626,c_0_2201])]),
[final] ).
cnf(c_0_2699,plain,
p(n3,n3,n2),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2630,c_0_2631])]),c_0_2632]),c_0_2633]),c_0_2634]),c_0_2635]),
[final] ).
cnf(c_0_2752,plain,
~ p(n1,n5,n6),
inference(spm,[status(thm)],[c_0_2496,c_0_2113]),
[final] ).
cnf(c_0_2756,plain,
~ p(n5,n9,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2696,c_0_2423])]),
[final] ).
cnf(c_0_2758,plain,
~ p(n3,n3,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2698,c_0_2699])]),
[final] ).
cnf(c_0_2760,plain,
p(n1,n1,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2701,c_0_2482])]),
[final] ).
cnf(c_0_2815,plain,
~ p(n4,n2,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2746,c_0_1174])]),
[final] ).
cnf(c_0_2816,plain,
~ p(n4,n3,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2747,c_0_1174])]),
[final] ).
cnf(c_0_2817,plain,
~ p(n5,n1,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2017,c_0_1730])]),
[final] ).
cnf(c_0_2818,plain,
~ p(n5,n2,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2748,c_0_1730])]),
[final] ).
cnf(c_0_2819,plain,
~ p(n5,n3,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2749,c_0_930])]),
[final] ).
cnf(c_0_2820,plain,
~ p(n6,n3,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2750,c_0_930])]),
[final] ).
cnf(c_0_2823,plain,
p(n9,n5,n4),
inference(sr,[status(thm)],[c_0_2751,c_0_2752]),
[final] ).
cnf(c_0_2828,plain,
~ p(n1,n2,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2759,c_0_2760])]),
[final] ).
cnf(c_0_2832,plain,
~ p(n2,n4,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2764,c_0_887])]),
[final] ).
cnf(c_0_2835,plain,
~ p(n5,n3,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2766,c_0_900])]),
[final] ).
cnf(c_0_2836,plain,
~ p(n5,n3,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2767,c_0_933])]),
[final] ).
cnf(c_0_2837,plain,
~ p(n5,n3,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2768,c_0_2335])]),
[final] ).
cnf(c_0_2868,plain,
~ p(n1,n9,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2788,c_0_1734])]),
[final] ).
cnf(c_0_2869,plain,
~ p(n2,n7,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2789,c_0_984])]),
[final] ).
cnf(c_0_2870,plain,
~ p(n2,n8,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2790,c_0_984])]),
[final] ).
cnf(c_0_2871,plain,
~ p(n2,n9,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2791,c_0_984])]),
[final] ).
cnf(c_0_2884,plain,
~ p(n5,n7,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2801,c_0_1086])]),
[final] ).
cnf(c_0_2885,plain,
~ p(n6,n7,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2802,c_0_896])]),
[final] ).
cnf(c_0_2887,plain,
p(n5,n8,n9),
inference(sr,[status(thm)],[c_0_2266,c_0_2352]),
[final] ).
cnf(c_0_2907,plain,
~ p(n9,n2,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2261,c_0_2823])]),
[final] ).
cnf(c_0_2910,plain,
p(n3,n8,n3),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2206,c_0_2827]),c_0_2246]),c_0_2828]),
[final] ).
cnf(c_0_2923,plain,
~ p(n1,n6,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2844,c_0_889])]),
[final] ).
cnf(c_0_2924,plain,
~ p(n1,n9,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2845,c_0_1161])]),
[final] ).
cnf(c_0_2927,plain,
~ p(n5,n7,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2847,c_0_1161])]),
[final] ).
cnf(c_0_2928,plain,
~ p(n6,n7,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2848,c_0_1161])]),
[final] ).
cnf(c_0_2929,plain,
~ p(n7,n7,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2849,c_0_914])]),
[final] ).
cnf(c_0_2930,plain,
~ p(n8,n7,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2850,c_0_987])]),
[final] ).
cnf(c_0_2931,plain,
~ p(n9,n7,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2851,c_0_1016])]),
[final] ).
cnf(c_0_2943,plain,
~ p(n2,n1,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2859,c_0_1308])]),
[final] ).
cnf(c_0_2944,plain,
~ p(n2,n4,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2860,c_0_894])]),
[final] ).
cnf(c_0_2945,plain,
~ p(n2,n9,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2861,c_0_1021])]),
[final] ).
cnf(c_0_2978,plain,
~ p(n5,n8,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2886,c_0_2887])]),
[final] ).
cnf(c_0_2981,plain,
~ p(n1,n7,n8),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2891,c_0_2892]),c_0_2893]),
[final] ).
cnf(c_0_2995,plain,
p(n8,n2,n4),
inference(sr,[status(thm)],[c_0_1773,c_0_2907]),
[final] ).
cnf(c_0_2998,plain,
p(n2,n9,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2876,c_0_2910])]),
[final] ).
cnf(c_0_3040,plain,
~ p(n3,n4,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2939,c_0_1021])]),
[final] ).
cnf(c_0_3255,plain,
p(n1,n5,n8),
inference(sr,[status(thm)],[c_0_2159,c_0_2752]),
[final] ).
cnf(c_0_3264,plain,
~ p(n1,n2,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2966,c_0_984])]),
[final] ).
cnf(c_0_3267,plain,
~ p(n5,n4,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2968,c_0_892])]),
[final] ).
cnf(c_0_3268,plain,
~ p(n5,n8,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2313,c_0_2887])]),
[final] ).
cnf(c_0_3269,plain,
~ p(n2,n1,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2969,c_0_2910])]),
[final] ).
cnf(c_0_3271,plain,
~ p(n2,n7,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2970,c_0_927])]),
[final] ).
cnf(c_0_3274,plain,
~ p(n5,n7,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2972,c_0_1016])]),
[final] ).
cnf(c_0_3275,plain,
~ p(n6,n7,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2973,c_0_1016])]),
[final] ).
cnf(c_0_3276,plain,
~ p(n6,n8,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2974,c_0_1355])]),
[final] ).
cnf(c_0_3282,plain,
~ p(n6,n1,n8),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2982,c_0_2983]),c_0_2984]),
[final] ).
cnf(c_0_3292,plain,
~ p(n8,n2,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2994,c_0_2995])]),
[final] ).
cnf(c_0_3294,plain,
~ p(n5,n3,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2997,c_0_2998])]),
[final] ).
cnf(c_0_3305,plain,
~ p(n7,n2,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3009,c_0_933])]),
[final] ).
cnf(c_0_3306,plain,
~ p(n7,n3,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3010,c_0_930])]),
[final] ).
cnf(c_0_3307,plain,
~ p(n7,n4,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3011,c_0_892])]),
[final] ).
cnf(c_0_3311,plain,
~ p(n1,n8,n2),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3016,c_0_3017]),c_0_3018]),c_0_3019]),
[final] ).
cnf(c_0_3321,plain,
~ p(n7,n1,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3028,c_0_1179])]),
[final] ).
cnf(c_0_3322,plain,
~ p(n7,n1,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3029,c_0_1308])]),
[final] ).
cnf(c_0_3323,plain,
~ p(n7,n1,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3030,c_0_925])]),
[final] ).
cnf(c_0_3543,plain,
~ p(n2,n8,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3251,c_0_1018])]),
[final] ).
cnf(c_0_3546,plain,
p(n8,n4,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3254,c_0_3255])]),
[final] ).
cnf(c_0_3551,plain,
p(n3,n6,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3260,c_0_3255])]),
[final] ).
cnf(c_0_3553,plain,
p(n1,n8,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3262,c_0_1718])]),
[final] ).
cnf(c_0_3557,plain,
p(n5,n1,n1),
inference(sr,[status(thm)],[c_0_1939,c_0_3269]),
[final] ).
cnf(c_0_3559,plain,
~ p(n2,n7,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3272,c_0_2631])]),
[final] ).
cnf(c_0_3561,plain,
~ p(n5,n8,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3277,c_0_2887])]),
[final] ).
cnf(c_0_3566,plain,
~ p(n2,n8,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3283,c_0_1018])]),
[final] ).
cnf(c_0_3567,plain,
~ p(n3,n8,n2),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3284,c_0_3017]),c_0_3285]),c_0_3286]),
[final] ).
cnf(c_0_3568,plain,
~ p(n4,n8,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3287,c_0_1161])]),
[final] ).
cnf(c_0_3569,plain,
~ p(n5,n8,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3288,c_0_1161])]),
[final] ).
cnf(c_0_3570,plain,
~ p(n6,n8,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3289,c_0_1161])]),
[final] ).
cnf(c_0_3571,plain,
~ p(n7,n8,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3290,c_0_914])]),
[final] ).
cnf(c_0_3573,plain,
p(n9,n2,n2),
inference(sr,[status(thm)],[c_0_2463,c_0_3292]),
[final] ).
cnf(c_0_3575,plain,
p(n5,n3,n5),
inference(sr,[status(thm)],[c_0_2915,c_0_3294]),
[final] ).
cnf(c_0_3577,plain,
p(n4,n2,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3296,c_0_2910])]),
[final] ).
cnf(c_0_3579,plain,
p(n3,n2,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3298,c_0_2910])]),
[final] ).
cnf(c_0_3586,plain,
p(n7,n9,n8),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_3304,c_0_2669]),c_0_3305]),c_0_3306]),c_0_3307]),c_0_1901]),c_0_2346]),c_0_2221]),c_0_2298]),
[final] ).
cnf(c_0_3588,plain,
p(n8,n6,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2373,c_0_3255])]),
[final] ).
cnf(c_0_3590,plain,
p(n1,n7,n2),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3310,c_0_3255])]),c_0_2632]),c_0_2633]),c_0_2634]),c_0_3311]),
[final] ).
cnf(c_0_3595,plain,
p(n8,n5,n6),
inference(sr,[status(thm)],[c_0_2119,c_0_2752]),
[final] ).
cnf(c_0_3600,plain,
p(n7,n1,n5),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_3320,c_0_1852]),c_0_1661]),c_0_3321]),c_0_3322]),c_0_1945]),c_0_1497]),c_0_2669]),c_0_3323]),
[final] ).
cnf(c_0_3609,plain,
p(n2,n6,n4),
inference(sr,[status(thm)],[c_0_3332,c_0_2543]),
[final] ).
cnf(c_0_3815,plain,
~ p(n7,n8,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3544,c_0_2282])]),
[final] ).
cnf(c_0_3816,plain,
~ p(n8,n8,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3545,c_0_3546])]),
[final] ).
cnf(c_0_3817,plain,
~ p(n6,n8,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3547,c_0_2400])]),
[final] ).
cnf(c_0_3818,plain,
~ p(n5,n8,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3548,c_0_2887])]),
[final] ).
cnf(c_0_3819,plain,
~ p(n4,n8,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3549,c_0_1553])]),
[final] ).
cnf(c_0_3820,plain,
~ p(n3,n8,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3550,c_0_3551])]),
[final] ).
cnf(c_0_3821,plain,
~ p(n1,n8,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3552,c_0_3553])]),
[final] ).
cnf(c_0_3823,plain,
~ p(n1,n2,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3555,c_0_2482])]),
[final] ).
cnf(c_0_3825,plain,
~ p(n5,n1,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2737,c_0_3557])]),
[final] ).
cnf(c_0_3827,plain,
~ p(n2,n7,n8),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_3269,c_0_2980]),c_0_2246]),c_0_3282]),
[final] ).
cnf(c_0_3829,plain,
~ p(n4,n8,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3562,c_0_2910])]),
[final] ).
cnf(c_0_3833,plain,
~ p(n9,n8,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3572,c_0_3573])]),
[final] ).
cnf(c_0_3834,plain,
~ p(n5,n2,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3574,c_0_3575])]),
[final] ).
cnf(c_0_3835,plain,
~ p(n5,n2,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3576,c_0_3577])]),
[final] ).
cnf(c_0_3836,plain,
~ p(n5,n2,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3578,c_0_3579])]),
[final] ).
cnf(c_0_3837,plain,
~ p(n5,n9,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2908,c_0_2998])]),
[final] ).
cnf(c_0_3838,plain,
~ p(n2,n9,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2795,c_0_2910])]),
[final] ).
cnf(c_0_3839,plain,
~ p(n3,n2,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3580,c_0_2910])]),
[final] ).
cnf(c_0_3840,plain,
~ p(n3,n8,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3581,c_0_2910])]),
[final] ).
cnf(c_0_3841,plain,
~ p(n2,n3,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3582,c_0_2910])]),
[final] ).
cnf(c_0_3842,plain,
~ p(n3,n2,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3583,c_0_2910])]),
[final] ).
cnf(c_0_3843,plain,
~ p(n4,n2,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3584,c_0_2910])]),
[final] ).
cnf(c_0_3844,plain,
~ p(n2,n9,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3585,c_0_3586])]),
[final] ).
cnf(c_0_3845,plain,
~ p(n3,n2,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3587,c_0_3551])]),
[final] ).
cnf(c_0_3846,plain,
~ p(n8,n6,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2863,c_0_3588])]),
[final] ).
cnf(c_0_3847,plain,
~ p(n1,n7,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3589,c_0_3590])]),
[final] ).
cnf(c_0_3848,plain,
~ p(n3,n7,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3591,c_0_3590])]),
[final] ).
cnf(c_0_3849,plain,
~ p(n2,n3,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2575,c_0_2631])]),
[final] ).
cnf(c_0_3850,plain,
~ p(n2,n4,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3592,c_0_2631])]),
[final] ).
cnf(c_0_3851,plain,
~ p(n3,n6,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2361,c_0_3255])]),
[final] ).
cnf(c_0_3852,plain,
~ p(n3,n7,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3593,c_0_3255])]),
[final] ).
cnf(c_0_3853,plain,
~ p(n3,n3,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3594,c_0_3255])]),
[final] ).
cnf(c_0_3854,plain,
~ p(n8,n5,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2621,c_0_3595])]),
[final] ).
cnf(c_0_3855,plain,
~ p(n8,n5,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2058,c_0_3595])]),
[final] ).
cnf(c_0_3856,plain,
~ p(n3,n4,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3596,c_0_2537])]),
[final] ).
cnf(c_0_3857,plain,
~ p(n8,n4,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3597,c_0_2537])]),
[final] ).
cnf(c_0_3858,plain,
~ p(n2,n1,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3598,c_0_2482])]),
[final] ).
cnf(c_0_3859,plain,
~ p(n6,n1,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2076,c_0_2482])]),
[final] ).
cnf(c_0_3860,plain,
~ p(n1,n1,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3599,c_0_3600])]),
[final] ).
cnf(c_0_3861,plain,
~ p(n2,n1,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3601,c_0_3600])]),
[final] ).
cnf(c_0_3862,plain,
~ p(n5,n1,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3602,c_0_3600])]),
[final] ).
cnf(c_0_3863,plain,
~ p(n8,n2,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3603,c_0_3600])]),
[final] ).
cnf(c_0_3864,plain,
~ p(n9,n2,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3604,c_0_3600])]),
[final] ).
cnf(c_0_3865,plain,
~ p(n2,n9,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3605,c_0_2423])]),
[final] ).
cnf(c_0_3866,plain,
~ p(n6,n1,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3606,c_0_2423])]),
[final] ).
cnf(c_0_3867,plain,
~ p(n7,n9,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3607,c_0_2423])]),
[final] ).
cnf(c_0_3868,plain,
~ p(n8,n8,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3608,c_0_2400])]),
[final] ).
cnf(c_0_3869,plain,
~ p(n2,n6,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2725,c_0_3609])]),
[final] ).
cnf(c_0_3870,plain,
~ p(n2,n6,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3610,c_0_3609])]),
[final] ).
cnf(c_0_3871,plain,
~ p(n1,n3,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3611,c_0_2584])]),
[final] ).
cnf(c_0_3872,plain,
~ p(n2,n3,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3335,c_0_2584])]),
[final] ).
cnf(c_0_3873,plain,
~ p(n8,n6,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3612,c_0_2584])]),
[final] ).
cnf(c_0_3874,plain,
~ p(n6,n3,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3613,c_0_2446])]),
[final] ).
cnf(c_0_3875,plain,
~ p(n1,n7,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2965,c_0_1718])]),
[final] ).
cnf(c_0_3876,plain,
~ p(n3,n7,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1621,c_0_1718])]),
[final] ).
cnf(c_0_3877,plain,
~ p(n4,n8,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3614,c_0_1718])]),
[final] ).
cnf(c_0_3878,plain,
~ p(n6,n8,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3615,c_0_1718])]),
[final] ).
cnf(c_0_3879,plain,
~ p(n4,n2,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3616,c_0_1553])]),
[final] ).
cnf(c_0_3880,plain,
~ p(n4,n3,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3617,c_0_1553])]),
[final] ).
cnf(c_0_3881,plain,
~ p(n8,n5,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3618,c_0_1553])]),
[final] ).
cnf(c_0_3882,plain,
~ p(n1,n9,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3619,c_0_2201])]),
[final] ).
cnf(c_0_3883,plain,
~ p(n9,n9,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3620,c_0_1911])]),
[final] ).
cnf(c_0_3884,plain,
~ p(n8,n8,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3621,c_0_2282])]),
[final] ).
cnf(c_0_3885,plain,
~ p(n1,n9,n8),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3622,c_0_2251]),c_0_3623]),c_0_3624]),
[final] ).
cnf(c_0_3886,plain,
~ p(n5,n7,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3625,c_0_1730])]),
[final] ).
cnf(c_0_3887,plain,
~ p(n9,n5,n5),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3626,c_0_2864]),c_0_3627]),
[final] ).
cnf(c_0_3888,plain,
~ p(n6,n7,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3628,c_0_1566])]),
[final] ).
cnf(c_0_3889,plain,
~ p(n6,n7,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3629,c_0_1566])]),
[final] ).
cnf(c_0_3890,plain,
~ p(n3,n5,n5),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3630,c_0_3631]),c_0_3632]),
[final] ).
cnf(c_0_3891,plain,
~ p(n1,n5,n5),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3630,c_0_3633]),c_0_3634]),
[final] ).
cnf(c_0_3892,plain,
~ p(n5,n2,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3635,c_0_1600])]),
[final] ).
cnf(c_0_3893,plain,
~ p(n7,n2,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3636,c_0_1600])]),
[final] ).
cnf(c_0_3894,plain,
~ p(n9,n2,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1423,c_0_1528])]),
[final] ).
cnf(c_0_3895,plain,
~ p(n7,n5,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3637,c_0_1687])]),
[final] ).
cnf(c_0_3896,plain,
~ p(n6,n3,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3638,c_0_1355])]),
[final] ).
cnf(c_0_3897,plain,
~ p(n9,n4,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3639,c_0_1010])]),
[final] ).
cnf(c_0_3898,plain,
~ p(n9,n1,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3640,c_0_1664])]),
[final] ).
cnf(c_0_3899,plain,
~ p(n9,n8,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3641,c_0_1016])]),
[final] ).
cnf(c_0_3900,plain,
~ p(n9,n7,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3642,c_0_1016])]),
[final] ).
cnf(c_0_3901,plain,
~ p(n9,n9,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3643,c_0_933])]),
[final] ).
cnf(c_0_3902,plain,
~ p(n9,n3,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3644,c_0_933])]),
[final] ).
cnf(c_0_3903,plain,
~ p(n9,n2,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3645,c_0_933])]),
[final] ).
cnf(c_0_3904,plain,
~ p(n9,n9,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3646,c_0_1734])]),
[final] ).
cnf(c_0_3905,plain,
~ p(n9,n8,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3647,c_0_1734])]),
[final] ).
cnf(c_0_3906,plain,
~ p(n9,n7,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3648,c_0_1734])]),
[final] ).
cnf(c_0_3907,plain,
~ p(n8,n9,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3649,c_0_1734])]),
[final] ).
cnf(c_0_3908,plain,
~ p(n8,n9,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3650,c_0_1734])]),
[final] ).
cnf(c_0_3909,plain,
~ p(n8,n8,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3651,c_0_1734])]),
[final] ).
cnf(c_0_3910,plain,
~ p(n9,n7,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3652,c_0_987])]),
[final] ).
cnf(c_0_3911,plain,
~ p(n8,n7,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3653,c_0_987])]),
[final] ).
cnf(c_0_3912,plain,
~ p(n8,n7,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3654,c_0_987])]),
[final] ).
cnf(c_0_3913,plain,
~ p(n9,n3,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3655,c_0_900])]),
[final] ).
cnf(c_0_3914,plain,
~ p(n8,n3,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3656,c_0_900])]),
[final] ).
cnf(c_0_3915,plain,
~ p(n8,n3,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3657,c_0_900])]),
[final] ).
cnf(c_0_3916,plain,
~ p(n8,n2,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3658,c_0_933])]),
[final] ).
cnf(c_0_3917,plain,
~ p(n9,n3,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3659,c_0_1179])]),
[final] ).
cnf(c_0_3918,plain,
~ p(n9,n1,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3660,c_0_1179])]),
[final] ).
cnf(c_0_3919,plain,
~ p(n8,n8,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3661,c_0_1179])]),
[final] ).
cnf(c_0_3920,plain,
~ p(n8,n7,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3662,c_0_1179])]),
[final] ).
cnf(c_0_3921,plain,
~ p(n8,n3,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3663,c_0_1179])]),
[final] ).
cnf(c_0_3922,plain,
~ p(n8,n1,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3664,c_0_1179])]),
[final] ).
cnf(c_0_3923,plain,
~ p(n7,n8,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3665,c_0_1016])]),
[final] ).
cnf(c_0_3924,plain,
~ p(n9,n7,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3666,c_0_1086])]),
[final] ).
cnf(c_0_3925,plain,
~ p(n8,n7,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3667,c_0_1086])]),
[final] ).
cnf(c_0_3926,plain,
~ p(n7,n7,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3668,c_0_1086])]),
[final] ).
cnf(c_0_3927,plain,
~ p(n7,n7,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3669,c_0_1086])]),
[final] ).
cnf(c_0_3928,plain,
~ p(n7,n7,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3670,c_0_1086])]),
[final] ).
cnf(c_0_3929,plain,
~ p(n9,n6,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3671,c_0_914])]),
[final] ).
cnf(c_0_3930,plain,
~ p(n8,n6,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3672,c_0_914])]),
[final] ).
cnf(c_0_3931,plain,
~ p(n9,n5,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3673,c_0_898])]),
[final] ).
cnf(c_0_3932,plain,
~ p(n9,n4,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3674,c_0_898])]),
[final] ).
cnf(c_0_3933,plain,
~ p(n8,n5,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3675,c_0_898])]),
[final] ).
cnf(c_0_3934,plain,
~ p(n8,n4,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3676,c_0_898])]),
[final] ).
cnf(c_0_3935,plain,
~ p(n7,n9,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3677,c_0_898])]),
[final] ).
cnf(c_0_3936,plain,
~ p(n7,n8,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3678,c_0_898])]),
[final] ).
cnf(c_0_3937,plain,
~ p(n7,n7,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3679,c_0_898])]),
[final] ).
cnf(c_0_3938,plain,
~ p(n7,n5,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3680,c_0_898])]),
[final] ).
cnf(c_0_3939,plain,
~ p(n9,n3,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3681,c_0_930])]),
[final] ).
cnf(c_0_3940,plain,
~ p(n9,n2,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3682,c_0_930])]),
[final] ).
cnf(c_0_3941,plain,
~ p(n8,n3,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3683,c_0_930])]),
[final] ).
cnf(c_0_3942,plain,
~ p(n8,n2,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3684,c_0_930])]),
[final] ).
cnf(c_0_3943,plain,
~ p(n7,n4,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3685,c_0_930])]),
[final] ).
cnf(c_0_3944,plain,
~ p(n7,n3,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3686,c_0_930])]),
[final] ).
cnf(c_0_3945,plain,
~ p(n7,n3,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3687,c_0_930])]),
[final] ).
cnf(c_0_3946,plain,
~ p(n7,n3,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3688,c_0_930])]),
[final] ).
cnf(c_0_3947,plain,
~ p(n7,n2,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3689,c_0_930])]),
[final] ).
cnf(c_0_3948,plain,
~ p(n6,n7,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3690,c_0_987])]),
[final] ).
cnf(c_0_3949,plain,
~ p(n6,n6,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3691,c_0_914])]),
[final] ).
cnf(c_0_3950,plain,
~ p(n9,n5,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3692,c_0_896])]),
[final] ).
cnf(c_0_3951,plain,
~ p(n8,n5,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3693,c_0_896])]),
[final] ).
cnf(c_0_3952,plain,
~ p(n7,n5,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3694,c_0_896])]),
[final] ).
cnf(c_0_3953,plain,
~ p(n6,n3,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3695,c_0_933])]),
[final] ).
cnf(c_0_3954,plain,
~ p(n6,n3,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3696,c_0_896])]),
[final] ).
cnf(c_0_3955,plain,
~ p(n6,n1,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3697,c_0_1179])]),
[final] ).
cnf(c_0_3956,plain,
~ p(n5,n7,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3698,c_0_987])]),
[final] ).
cnf(c_0_3957,plain,
~ p(n9,n6,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3699,c_0_1176])]),
[final] ).
cnf(c_0_3958,plain,
~ p(n8,n6,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3700,c_0_1176])]),
[final] ).
cnf(c_0_3959,plain,
~ p(n7,n6,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3701,c_0_1176])]),
[final] ).
cnf(c_0_3960,plain,
~ p(n6,n6,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3702,c_0_1176])]),
[final] ).
cnf(c_0_3961,plain,
~ p(n6,n5,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3703,c_0_1176])]),
[final] ).
cnf(c_0_3962,plain,
~ p(n6,n4,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3704,c_0_1176])]),
[final] ).
cnf(c_0_3963,plain,
~ p(n5,n8,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3705,c_0_1176])]),
[final] ).
cnf(c_0_3964,plain,
~ p(n5,n7,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3706,c_0_1176])]),
[final] ).
cnf(c_0_3965,plain,
~ p(n5,n6,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3707,c_0_1176])]),
[final] ).
cnf(c_0_3966,plain,
~ p(n5,n5,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3708,c_0_1176])]),
[final] ).
cnf(c_0_3967,plain,
~ p(n5,n5,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3709,c_0_896])]),
[final] ).
cnf(c_0_3968,plain,
~ p(n9,n4,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3710,c_0_894])]),
[final] ).
cnf(c_0_3969,plain,
~ p(n8,n4,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3711,c_0_894])]),
[final] ).
cnf(c_0_3970,plain,
~ p(n7,n4,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3712,c_0_894])]),
[final] ).
cnf(c_0_3971,plain,
~ p(n6,n4,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3713,c_0_894])]),
[final] ).
cnf(c_0_3972,plain,
~ p(n5,n4,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3714,c_0_894])]),
[final] ).
cnf(c_0_3973,plain,
~ p(n5,n1,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3715,c_0_1179])]),
[final] ).
cnf(c_0_3974,plain,
~ p(n9,n9,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3716,c_0_1161])]),
[final] ).
cnf(c_0_3975,plain,
~ p(n8,n9,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3717,c_0_1161])]),
[final] ).
cnf(c_0_3976,plain,
~ p(n7,n9,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3718,c_0_1161])]),
[final] ).
cnf(c_0_3977,plain,
~ p(n4,n9,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3719,c_0_1161])]),
[final] ).
cnf(c_0_3978,plain,
~ p(n4,n9,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3720,c_0_1161])]),
[final] ).
cnf(c_0_3979,plain,
~ p(n9,n6,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3721,c_0_1174])]),
[final] ).
cnf(c_0_3980,plain,
~ p(n8,n6,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3722,c_0_1174])]),
[final] ).
cnf(c_0_3981,plain,
~ p(n7,n6,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3723,c_0_1174])]),
[final] ).
cnf(c_0_3982,plain,
~ p(n6,n6,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3724,c_0_1174])]),
[final] ).
cnf(c_0_3983,plain,
~ p(n6,n4,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3725,c_0_1174])]),
[final] ).
cnf(c_0_3984,plain,
~ p(n5,n6,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3726,c_0_1174])]),
[final] ).
cnf(c_0_3985,plain,
~ p(n5,n4,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3727,c_0_1174])]),
[final] ).
cnf(c_0_3986,plain,
~ p(n4,n6,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3728,c_0_1174])]),
[final] ).
cnf(c_0_3987,plain,
~ p(n4,n6,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3729,c_0_1174])]),
[final] ).
cnf(c_0_3988,plain,
~ p(n4,n5,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3730,c_0_1176])]),
[final] ).
cnf(c_0_3989,plain,
~ p(n4,n5,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3731,c_0_896])]),
[final] ).
cnf(c_0_3990,plain,
~ p(n9,n4,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3732,c_0_892])]),
[final] ).
cnf(c_0_3991,plain,
~ p(n8,n4,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3733,c_0_892])]),
[final] ).
cnf(c_0_3992,plain,
~ p(n6,n4,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3734,c_0_892])]),
[final] ).
cnf(c_0_3993,plain,
~ p(n4,n9,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3735,c_0_892])]),
[final] ).
cnf(c_0_3994,plain,
~ p(n4,n4,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3736,c_0_892])]),
[final] ).
cnf(c_0_3995,plain,
~ p(n4,n4,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3737,c_0_892])]),
[final] ).
cnf(c_0_3996,plain,
~ p(n4,n3,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3738,c_0_892])]),
[final] ).
cnf(c_0_3997,plain,
~ p(n4,n3,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3739,c_0_900])]),
[final] ).
cnf(c_0_3998,plain,
~ p(n4,n2,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3740,c_0_892])]),
[final] ).
cnf(c_0_3999,plain,
~ p(n9,n1,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3741,c_0_1308])]),
[final] ).
cnf(c_0_4000,plain,
~ p(n8,n1,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3742,c_0_1308])]),
[final] ).
cnf(c_0_4001,plain,
~ p(n6,n1,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3743,c_0_1308])]),
[final] ).
cnf(c_0_4002,plain,
~ p(n5,n1,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3744,c_0_1308])]),
[final] ).
cnf(c_0_4003,plain,
~ p(n4,n4,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3745,c_0_1308])]),
[final] ).
cnf(c_0_4004,plain,
~ p(n4,n1,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3746,c_0_1308])]),
[final] ).
cnf(c_0_4005,plain,
~ p(n9,n9,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3747,c_0_1021])]),
[final] ).
cnf(c_0_4006,plain,
~ p(n8,n9,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3748,c_0_1021])]),
[final] ).
cnf(c_0_4007,plain,
~ p(n7,n9,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3749,c_0_1021])]),
[final] ).
cnf(c_0_4008,plain,
~ p(n4,n9,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3750,c_0_1021])]),
[final] ).
cnf(c_0_4009,plain,
~ p(n3,n9,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3751,c_0_1021])]),
[final] ).
cnf(c_0_4010,plain,
~ p(n3,n9,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3752,c_0_1021])]),
[final] ).
cnf(c_0_4011,plain,
~ p(n3,n9,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3753,c_0_1021])]),
[final] ).
cnf(c_0_4012,plain,
~ p(n3,n6,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3754,c_0_914])]),
[final] ).
cnf(c_0_4013,plain,
~ p(n3,n4,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3755,c_0_892])]),
[final] ).
cnf(c_0_4014,plain,
~ p(n9,n1,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3756,c_0_925])]),
[final] ).
cnf(c_0_4015,plain,
~ p(n8,n1,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3757,c_0_925])]),
[final] ).
cnf(c_0_4016,plain,
~ p(n6,n1,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3758,c_0_925])]),
[final] ).
cnf(c_0_4017,plain,
~ p(n5,n1,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3759,c_0_925])]),
[final] ).
cnf(c_0_4018,plain,
~ p(n4,n1,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3760,c_0_925])]),
[final] ).
cnf(c_0_4019,plain,
~ p(n3,n7,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3761,c_0_925])]),
[final] ).
cnf(c_0_4020,plain,
~ p(n3,n1,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3762,c_0_925])]),
[final] ).
cnf(c_0_4021,plain,
~ p(n3,n1,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3763,c_0_925])]),
[final] ).
cnf(c_0_4022,plain,
~ p(n2,n9,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3764,c_0_1161])]),
[final] ).
cnf(c_0_4023,plain,
~ p(n9,n8,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3765,c_0_1018])]),
[final] ).
cnf(c_0_4024,plain,
~ p(n8,n8,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3766,c_0_1018])]),
[final] ).
cnf(c_0_4025,plain,
~ p(n7,n8,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3767,c_0_1018])]),
[final] ).
cnf(c_0_4026,plain,
~ p(n6,n8,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3768,c_0_1018])]),
[final] ).
cnf(c_0_4027,plain,
~ p(n5,n8,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3769,c_0_1018])]),
[final] ).
cnf(c_0_4028,plain,
~ p(n4,n8,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3770,c_0_1018])]),
[final] ).
cnf(c_0_4029,plain,
~ p(n2,n6,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3771,c_0_1018])]),
[final] ).
cnf(c_0_4030,plain,
~ p(n2,n6,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3772,c_0_914])]),
[final] ).
cnf(c_0_4031,plain,
~ p(n9,n5,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3773,c_0_927])]),
[final] ).
cnf(c_0_4032,plain,
~ p(n8,n5,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3774,c_0_927])]),
[final] ).
cnf(c_0_4033,plain,
~ p(n7,n5,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3775,c_0_927])]),
[final] ).
cnf(c_0_4034,plain,
~ p(n6,n5,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3776,c_0_927])]),
[final] ).
cnf(c_0_4035,plain,
~ p(n5,n5,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3777,c_0_927])]),
[final] ).
cnf(c_0_4036,plain,
~ p(n4,n5,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3778,c_0_927])]),
[final] ).
cnf(c_0_4037,plain,
~ p(n3,n5,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3779,c_0_927])]),
[final] ).
cnf(c_0_4038,plain,
~ p(n2,n5,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3780,c_0_927])]),
[final] ).
cnf(c_0_4039,plain,
~ p(n2,n4,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3781,c_0_892])]),
[final] ).
cnf(c_0_4040,plain,
~ p(n2,n4,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3782,c_0_1018])]),
[final] ).
cnf(c_0_4041,plain,
~ p(n9,n2,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3783,c_0_984])]),
[final] ).
cnf(c_0_4042,plain,
~ p(n8,n2,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3784,c_0_984])]),
[final] ).
cnf(c_0_4043,plain,
~ p(n7,n2,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3785,c_0_984])]),
[final] ).
cnf(c_0_4044,plain,
~ p(n5,n2,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3786,c_0_984])]),
[final] ).
cnf(c_0_4045,plain,
~ p(n4,n2,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3787,c_0_984])]),
[final] ).
cnf(c_0_4046,plain,
~ p(n2,n2,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3788,c_0_984])]),
[final] ).
cnf(c_0_4047,plain,
~ p(n2,n1,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3789,c_0_927])]),
[final] ).
cnf(c_0_4048,plain,
~ p(n1,n8,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3790,c_0_1018])]),
[final] ).
cnf(c_0_4049,plain,
~ p(n1,n7,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3791,c_0_987])]),
[final] ).
cnf(c_0_4050,plain,
~ p(n9,n6,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3792,c_0_889])]),
[final] ).
cnf(c_0_4051,plain,
~ p(n8,n6,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3793,c_0_889])]),
[final] ).
cnf(c_0_4052,plain,
~ p(n7,n6,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3794,c_0_889])]),
[final] ).
cnf(c_0_4053,plain,
~ p(n6,n6,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3795,c_0_889])]),
[final] ).
cnf(c_0_4054,plain,
~ p(n5,n6,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3796,c_0_889])]),
[final] ).
cnf(c_0_4055,plain,
~ p(n4,n6,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3797,c_0_889])]),
[final] ).
cnf(c_0_4056,plain,
~ p(n3,n6,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3798,c_0_889])]),
[final] ).
cnf(c_0_4057,plain,
~ p(n3,n5,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3799,c_0_889])]),
[final] ).
cnf(c_0_4058,plain,
~ p(n2,n6,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3800,c_0_889])]),
[final] ).
cnf(c_0_4059,plain,
~ p(n2,n5,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3801,c_0_889])]),
[final] ).
cnf(c_0_4060,plain,
~ p(n1,n6,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3802,c_0_889])]),
[final] ).
cnf(c_0_4061,plain,
~ p(n1,n5,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3803,c_0_927])]),
[final] ).
cnf(c_0_4062,plain,
~ p(n1,n5,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3804,c_0_889])]),
[final] ).
cnf(c_0_4063,plain,
~ p(n9,n4,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3805,c_0_887])]),
[final] ).
cnf(c_0_4064,plain,
~ p(n8,n4,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3806,c_0_887])]),
[final] ).
cnf(c_0_4065,plain,
~ p(n7,n4,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3807,c_0_887])]),
[final] ).
cnf(c_0_4066,plain,
~ p(n6,n4,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3808,c_0_887])]),
[final] ).
cnf(c_0_4067,plain,
~ p(n5,n4,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3809,c_0_887])]),
[final] ).
cnf(c_0_4068,plain,
~ p(n3,n4,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3810,c_0_887])]),
[final] ).
cnf(c_0_4069,plain,
~ p(n1,n4,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3811,c_0_887])]),
[final] ).
cnf(c_0_4070,plain,
~ p(n1,n4,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3812,c_0_887])]),
[final] ).
cnf(c_0_4071,plain,
~ p(n1,n1,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3813,c_0_925])]),
[final] ).
cnf(c_0_4072,plain,
p(n9,n8,n5),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_3814,c_0_3815]),c_0_3816]),c_0_3817]),c_0_3818]),c_0_3819]),c_0_3820]),c_0_3821]),
[final] ).
cnf(c_0_4073,plain,
p(n1,n2,n5),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_3822,c_0_2633]),c_0_3823]),c_0_2828]),
[final] ).
cnf(c_0_4074,plain,
p(n5,n2,n8),
inference(sr,[status(thm)],[c_0_3824,c_0_3825]),
[final] ).
cnf(c_0_4075,plain,
p(n2,n7,n5),
inference(sr,[status(thm)],[c_0_3826,c_0_3827]),
[final] ).
cnf(c_0_4076,plain,
p(n2,n1,n8),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2806,c_0_3557])]),c_0_2246]),c_0_3282]),
[final] ).
cnf(c_0_4077,plain,
p(n5,n9,n3),
inference(sr,[status(thm)],[c_0_3828,c_0_3829]),
[final] ).
cnf(c_0_4078,plain,
p(n4,n8,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3830,c_0_2910])]),
[final] ).
cnf(c_0_4079,plain,
p(n3,n7,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3831,c_0_2910])]),
[final] ).
cnf(c_0_4080,plain,
p(n2,n3,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3001,c_0_2910])]),
[final] ).
cnf(c_0_4081,plain,
p(n8,n8,n2),
inference(sr,[status(thm)],[c_0_3832,c_0_3833]),
[final] ).
cnf(c_0_4082,plain,
p(n6,n2,n6),
inference(sr,[status(thm)],[c_0_2459,c_0_2472]),
[final] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ080+2 : TPTP v9.3.1. Bugfixed v5.4.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/5.38 % Computer : n004.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.09/5.38 % CPULimit : 300
% 0.09/5.38 % WCLimit : 300
% 0.09/5.38 % DateTime : Mon Sep 21 03:49:55 UTC 2026
% 0.09/5.38 % CPUTime :
% 0.09/5.38 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/5.42 Running first-order theorem proving
% 0.14/5.42 Running: /export/starexec/sandbox/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.22/6.35 % Version: 3.5.1
% 2.22/6.35 % Preprocessing class: FMLSSMSMSSSNFFN.
% 2.22/6.35 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 2.22/6.35 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S4d with 900s (3) cores
% 2.22/6.35 % Starting new_bool_3 with 600s (2) cores
% 2.22/6.35 % Starting new_bool_1 with 600s (2) cores
% 2.22/6.35 % Starting sh5l with 300s (1) cores
% 2.22/6.35 % new_bool_3 with pid 2181435 completed with status 9
% 2.22/6.35 % new_bool_1 with pid 2181436 completed with status 9
% 2.22/6.35 % sh5l with pid 2181437 completed with status 9
% 2.22/6.35 % G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S4d with pid 2181434 completed with status 1
% 2.22/6.35 % Result found by G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S4d
% 2.22/6.35 % Preprocessing class: FMLSSMSMSSSNFFN.
% 2.22/6.35 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 2.22/6.35 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S4d with 900s (3) cores
% 2.22/6.35 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 2.22/6.35 % No SInE strategy applied
% 2.22/6.35 % Search class: FGHNF-SMLM00-SFFFFFNN
% 2.22/6.35 % Scheduled 7 strats onto 3 cores with 900 seconds (900 total)
% 2.22/6.35 % Starting SubtermCWHack with 82s (1) cores
% 2.22/6.35 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S4d with 91s (1) cores
% 2.22/6.35 % Starting H----_011_C07_F1_PI_AE_SP_S0V with 82s (1) cores
% 2.22/6.35 % SubtermCWHack with pid 2181477 completed with status 1
% 2.22/6.35 % Result found by SubtermCWHack
% 2.22/6.35 % Preprocessing class: FMLSSMSMSSSNFFN.
% 2.22/6.35 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 2.22/6.35 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S4d with 900s (3) cores
% 2.22/6.35 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 2.22/6.35 % No SInE strategy applied
% 2.22/6.35 % Search class: FGHNF-SMLM00-SFFFFFNN
% 2.22/6.35 % Scheduled 7 strats onto 3 cores with 900 seconds (900 total)
% 2.22/6.35 % Starting SubtermCWHack with 82s (1) cores
% 2.22/6.35 % Preprocessing time : 0.039 s
% 2.22/6.35
% 2.22/6.35 % No proof found!
% 2.22/6.35 % SZS status Satisfiable
% 2.22/6.35 % SZS output start Saturation
% See solution above
% 2.22/6.36 % Parsed axioms : 10554
% 2.22/6.36 % Removed by relevancy pruning/SinE : 0
% 2.22/6.36 % Initial clauses : 10554
% 2.22/6.36 % Removed in clause preprocessing : 0
% 2.22/6.36 % Initial clauses in saturation : 10554
% 2.22/6.36 % Processed clauses : 13270
% 2.22/6.36 % ...of these trivial : 257
% 2.22/6.36 % ...subsumed : 7137
% 2.22/6.36 % ...remaining for further processing : 5876
% 2.22/6.36 % Other redundant clauses eliminated : 0
% 2.22/6.36 % Clauses deleted for lack of memory : 0
% 2.22/6.36 % Backward-subsumed : 4556
% 2.22/6.36 % Backward-rewritten : 435
% 2.22/6.36 % Generated clauses : 5696
% 2.22/6.36 % ...of the previous two non-redundant : 5115
% 2.22/6.36 % ...aggressively subsumed : 0
% 2.22/6.36 % Contextual simplify-reflections : 134
% 2.22/6.36 % Paramodulations : 5540
% 2.22/6.36 % Factorizations : 0
% 2.22/6.36 % NegExts : 0
% 2.22/6.36 % Equation resolutions : 0
% 2.22/6.36 % Disequality decompositions : 0
% 2.22/6.36 % Total rewrite steps : 1364
% 2.22/6.36 % ...of those cached : 1283
% 2.22/6.36 % Propositional unsat checks : 0
% 2.22/6.36 % Propositional check models : 0
% 2.22/6.36 % Propositional check unsatisfiable : 0
% 2.22/6.36 % Propositional clauses : 0
% 2.22/6.36 % Propositional clauses after purity: 0
% 2.22/6.36 % Propositional unsat core size : 0
% 2.22/6.36 % Propositional preprocessing time : 0.000
% 2.22/6.36 % Propositional encoding time : 0.000
% 2.22/6.36 % Propositional solver time : 0.000
% 2.22/6.36 % Success case prop preproc time : 0.000
% 2.22/6.36 % Success case prop encoding time : 0.000
% 2.22/6.36 % Success case prop solver time : 0.000
% 2.22/6.36 % Current number of processed clauses : 729
% 2.22/6.36 % Positive orientable unit clauses : 81
% 2.22/6.36 % Positive unorientable unit clauses: 0
% 2.22/6.36 % Negative unit clauses : 648
% 2.22/6.36 % Non-unit-clauses : 0
% 2.22/6.36 % Current number of unprocessed clauses: 0
% 2.22/6.36 % ...number of literals in the above : 0
% 2.22/6.36 % Current number of archived formulas : 0
% 2.22/6.36 % Current number of archived clauses : 5147
% 2.22/6.36 % Clause-clause subsumption calls (NU) : 1498321
% 2.22/6.36 % Rec. Clause-clause subsumption calls : 942360
% 2.22/6.36 % Non-unit clause-clause subsumptions : 1447
% 2.22/6.36 % Unit Clause-clause subsumption calls : 276849
% 2.22/6.36 % Rewrite failures with RHS unbound : 0
% 2.22/6.36 % BW rewrite match attempts : 508
% 2.22/6.36 % BW rewrite match successes : 52
% 2.22/6.36 % Condensation attempts : 0
% 2.22/6.36 % Condensation successes : 0
% 2.22/6.36 % Termbank termtop insertions : 778134
% 2.22/6.36 % Search garbage collected termcells : 20415
% 2.22/6.36
% 2.22/6.36 % -------------------------------------------------
% 2.22/6.36 % User time : 0.737 s
% 2.22/6.36 % System time : 0.045 s
% 2.22/6.36 % Total time : 0.782 s
% 2.22/6.36 % Maximum resident set size: 21892 pages
% 2.22/6.36
% 2.22/6.36 % -------------------------------------------------
% 2.22/6.36 % User time : 2.056 s
% 2.22/6.36 % System time : 0.212 s
% 2.22/6.36 % Total time : 2.268 s
% 2.22/6.36 % Maximum resident set size: 9472 pages
% 2.22/6.36 % E exiting
%------------------------------------------------------------------------------