%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : PUZ069+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 : n008.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:30 PM UTC 2026
% Result : Satisfiable 3.17s 1.60s
% Output : Saturation 3.17s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_942ERROR: Could not build tree for root c_0_974ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(c_0_818,plain,
p(n8,n2,n3),
inference(split_conjunct,[status(thm)],[ax368]),
[final] ).
cnf(c_0_820,plain,
p(n1,n1,n1),
inference(split_conjunct,[status(thm)],[ax353]),
[final] ).
cnf(c_0_822,plain,
p(n1,n3,n7),
inference(split_conjunct,[status(thm)],[ax354]),
[final] ).
cnf(c_0_824,plain,
p(n1,n4,n6),
inference(split_conjunct,[status(thm)],[ax355]),
[final] ).
cnf(c_0_826,plain,
p(n6,n6,n3),
inference(split_conjunct,[status(thm)],[ax365]),
[final] ).
cnf(c_0_828,plain,
p(n3,n7,n3),
inference(split_conjunct,[status(thm)],[ax359]),
[final] ).
cnf(c_0_839,plain,
~ p(n1,n2,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_817,c_0_818])]),
[final] ).
cnf(c_0_840,plain,
~ p(n1,n1,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_819,c_0_820])]),
[final] ).
cnf(c_0_841,plain,
~ p(n1,n3,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_821,c_0_822])]),
[final] ).
cnf(c_0_842,plain,
~ p(n1,n4,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_823,c_0_824])]),
[final] ).
cnf(c_0_843,plain,
~ p(n1,n6,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_825,c_0_826])]),
[final] ).
cnf(c_0_844,plain,
~ p(n1,n7,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_827,c_0_828])]),
[final] ).
cnf(c_0_845,plain,
~ p(n1,n8,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_829,c_0_828])]),
[final] ).
cnf(c_0_846,plain,
~ p(n1,n9,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_830,c_0_828])]),
[final] ).
cnf(c_0_861,plain,
p(n1,n5,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_838,c_0_839]),c_0_840]),c_0_841]),c_0_842]),c_0_843]),c_0_844]),c_0_845]),c_0_846]),
[final] ).
cnf(c_0_864,plain,
p(n4,n4,n2),
inference(split_conjunct,[status(thm)],[ax360]),
[final] ).
cnf(c_0_868,plain,
p(n7,n4,n7),
inference(split_conjunct,[status(thm)],[ax366]),
[final] ).
cnf(c_0_878,plain,
~ p(n2,n4,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_860,c_0_861])]),
[final] ).
cnf(c_0_879,plain,
~ p(n3,n4,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_862,c_0_828])]),
[final] ).
cnf(c_0_880,plain,
~ p(n4,n4,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_863,c_0_864])]),
[final] ).
cnf(c_0_881,plain,
~ p(n5,n4,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_865,c_0_826])]),
[final] ).
cnf(c_0_882,plain,
~ p(n6,n4,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_866,c_0_826])]),
[final] ).
cnf(c_0_883,plain,
~ p(n7,n4,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_867,c_0_868])]),
[final] ).
cnf(c_0_884,plain,
~ p(n8,n4,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_869,c_0_818])]),
[final] ).
cnf(c_0_895,plain,
p(n5,n8,n6),
inference(split_conjunct,[status(thm)],[ax363]),
[final] ).
cnf(c_0_898,plain,
p(n7,n8,n1),
inference(split_conjunct,[status(thm)],[ax367]),
[final] ).
cnf(c_0_901,plain,
p(n9,n4,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_877,c_0_842]),c_0_878]),c_0_879]),c_0_880]),c_0_881]),c_0_882]),c_0_883]),c_0_884]),
[final] ).
cnf(c_0_923,plain,
~ p(n2,n8,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_892,c_0_828])]),
[final] ).
cnf(c_0_924,plain,
~ p(n3,n8,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_893,c_0_828])]),
[final] ).
cnf(c_0_925,plain,
~ p(n5,n8,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_894,c_0_895])]),
[final] ).
cnf(c_0_926,plain,
~ p(n6,n8,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_896,c_0_826])]),
[final] ).
cnf(c_0_927,plain,
~ p(n7,n8,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_897,c_0_898])]),
[final] ).
cnf(c_0_928,plain,
~ p(n8,n8,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_899,c_0_818])]),
[final] ).
cnf(c_0_929,plain,
~ p(n9,n8,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_900,c_0_901])]),
[final] ).
cnf(c_0_951,plain,
p(n4,n8,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_922,c_0_845]),c_0_923]),c_0_924]),c_0_925]),c_0_926]),c_0_927]),c_0_928]),c_0_929]),
[final] ).
cnf(c_0_953,plain,
p(n5,n1,n9),
inference(split_conjunct,[status(thm)],[ax362]),
[final] ).
cnf(c_0_960,plain,
p(n2,n7,n5),
inference(split_conjunct,[status(thm)],[ax357]),
[final] ).
cnf(c_0_966,plain,
p(n6,n5,n5),
inference(split_conjunct,[status(thm)],[ax364]),
[final] ).
cnf(c_0_974,plain,
~ p(n3,n3,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_942,c_0_828])]),
[final] ).
cnf(c_0_975,plain,
~ p(n6,n3,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_943,c_0_826])]),
[final] ).
cnf(c_0_976,plain,
~ p(n7,n3,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_944,c_0_818])]),
[final] ).
cnf(c_0_977,plain,
~ p(n8,n3,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_945,c_0_818])]),
[final] ).
cnf(c_0_978,plain,
~ p(n9,n3,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_946,c_0_818])]),
[final] ).
cnf(c_0_982,plain,
~ p(n3,n1,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_949,c_0_828])]),
[final] ).
cnf(c_0_983,plain,
~ p(n4,n1,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_950,c_0_951])]),
[final] ).
cnf(c_0_984,plain,
~ p(n5,n1,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_952,c_0_953])]),
[final] ).
cnf(c_0_985,plain,
~ p(n6,n1,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_954,c_0_826])]),
[final] ).
cnf(c_0_986,plain,
~ p(n7,n1,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_955,c_0_818])]),
[final] ).
cnf(c_0_987,plain,
~ p(n8,n1,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_956,c_0_818])]),
[final] ).
cnf(c_0_988,plain,
~ p(n9,n1,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_957,c_0_818])]),
[final] ).
cnf(c_0_996,plain,
~ p(n1,n8,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_959,c_0_960])]),
[final] ).
cnf(c_0_997,plain,
~ p(n2,n8,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_961,c_0_960])]),
[final] ).
cnf(c_0_998,plain,
~ p(n3,n8,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_962,c_0_960])]),
[final] ).
cnf(c_0_999,plain,
~ p(n4,n8,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_963,c_0_951])]),
[final] ).
cnf(c_0_1000,plain,
~ p(n5,n8,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_964,c_0_895])]),
[final] ).
cnf(c_0_1001,plain,
~ p(n6,n8,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_965,c_0_966])]),
[final] ).
cnf(c_0_1002,plain,
~ p(n7,n8,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_967,c_0_898])]),
[final] ).
cnf(c_0_1010,plain,
~ p(n4,n3,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_979,c_0_951])]),
[final] ).
cnf(c_0_1012,plain,
p(n2,n1,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_981,c_0_982]),c_0_840]),c_0_983]),c_0_984]),c_0_985]),c_0_986]),c_0_987]),c_0_988]),
[final] ).
cnf(c_0_1027,plain,
~ p(n2,n3,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1011,c_0_1012])]),
[final] ).
cnf(c_0_1045,plain,
~ p(n5,n7,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1020,c_0_960])]),
[final] ).
cnf(c_0_1046,plain,
~ p(n5,n1,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1021,c_0_953])]),
[final] ).
cnf(c_0_1047,plain,
~ p(n5,n4,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1022,c_0_966])]),
[final] ).
cnf(c_0_1048,plain,
~ p(n5,n5,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1023,c_0_966])]),
[final] ).
cnf(c_0_1049,plain,
~ p(n5,n6,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1024,c_0_966])]),
[final] ).
cnf(c_0_1051,plain,
p(n5,n3,n3),
inference(sr,[status(thm)],[c_0_1026,c_0_1027]),
[final] ).
cnf(c_0_1063,plain,
~ p(n1,n9,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1037,c_0_960])]),
[final] ).
cnf(c_0_1064,plain,
~ p(n2,n9,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1038,c_0_960])]),
[final] ).
cnf(c_0_1065,plain,
~ p(n3,n9,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1039,c_0_960])]),
[final] ).
cnf(c_0_1066,plain,
~ p(n6,n9,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1040,c_0_966])]),
[final] ).
cnf(c_0_1067,plain,
~ p(n7,n9,n5),
inference(spm,[status(thm)],[c_0_1041,c_0_1042]),
[final] ).
cnf(c_0_1081,plain,
~ p(n5,n3,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1050,c_0_1051])]),
[final] ).
cnf(c_0_1083,plain,
p(n3,n2,n2),
inference(split_conjunct,[status(thm)],[ax358]),
[final] ).
cnf(c_0_1090,plain,
p(n8,n7,n2),
inference(split_conjunct,[status(thm)],[ax369]),
[final] ).
cnf(c_0_1134,plain,
~ p(n5,n2,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1082,c_0_1083])]),
[final] ).
cnf(c_0_1135,plain,
~ p(n5,n1,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1084,c_0_953])]),
[final] ).
cnf(c_0_1136,plain,
~ p(n5,n3,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1085,c_0_1051])]),
[final] ).
cnf(c_0_1137,plain,
~ p(n5,n4,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1086,c_0_864])]),
[final] ).
cnf(c_0_1138,plain,
~ p(n5,n5,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1087,c_0_864])]),
[final] ).
cnf(c_0_1139,plain,
~ p(n5,n6,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1088,c_0_864])]),
[final] ).
cnf(c_0_1140,plain,
~ p(n5,n7,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1089,c_0_1090])]),
[final] ).
cnf(c_0_1141,plain,
~ p(n5,n8,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1091,c_0_895])]),
[final] ).
cnf(c_0_1174,plain,
p(n2,n6,n8),
inference(split_conjunct,[status(thm)],[ax356]),
[final] ).
cnf(c_0_1191,plain,
p(n5,n9,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_1133,c_0_1134]),c_0_1135]),c_0_1136]),c_0_1137]),c_0_1138]),c_0_1139]),c_0_1140]),c_0_1141]),
[final] ).
cnf(c_0_1197,plain,
p(n4,n5,n4),
inference(split_conjunct,[status(thm)],[ax361]),
[final] ).
cnf(c_0_1240,plain,
~ p(n1,n4,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1172,c_0_824])]),
[final] ).
cnf(c_0_1241,plain,
~ p(n2,n4,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1173,c_0_1174])]),
[final] ).
cnf(c_0_1242,plain,
~ p(n3,n4,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1175,c_0_1174])]),
[final] ).
cnf(c_0_1243,plain,
~ p(n4,n4,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1176,c_0_864])]),
[final] ).
cnf(c_0_1244,plain,
~ p(n7,n4,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1177,c_0_868])]),
[final] ).
cnf(c_0_1245,plain,
~ p(n9,n4,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1178,c_0_901])]),
[final] ).
cnf(c_0_1253,plain,
~ p(n1,n3,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1184,c_0_822])]),
[final] ).
cnf(c_0_1254,plain,
~ p(n1,n1,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1185,c_0_820])]),
[final] ).
cnf(c_0_1255,plain,
~ p(n1,n4,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1186,c_0_824])]),
[final] ).
cnf(c_0_1256,plain,
~ p(n1,n5,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1187,c_0_966])]),
[final] ).
cnf(c_0_1257,plain,
~ p(n1,n7,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1188,c_0_960])]),
[final] ).
cnf(c_0_1259,plain,
p(n5,n2,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1190,c_0_1191])]),
[final] ).
cnf(c_0_1264,plain,
~ p(n4,n4,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1195,c_0_824])]),
[final] ).
cnf(c_0_1265,plain,
~ p(n4,n5,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1196,c_0_1197])]),
[final] ).
cnf(c_0_1266,plain,
~ p(n5,n4,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1198,c_0_824])]),
[final] ).
cnf(c_0_1267,plain,
~ p(n5,n5,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1199,c_0_895])]),
[final] ).
cnf(c_0_1268,plain,
~ p(n5,n6,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1200,c_0_895])]),
[final] ).
cnf(c_0_1269,plain,
~ p(n6,n4,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1201,c_0_824])]),
[final] ).
cnf(c_0_1270,plain,
~ p(n6,n5,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1202,c_0_966])]),
[final] ).
cnf(c_0_1271,plain,
~ p(n6,n6,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1203,c_0_826])]),
[final] ).
cnf(c_0_1290,plain,
~ p(n1,n7,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1220,c_0_824])]),
[final] ).
cnf(c_0_1291,plain,
~ p(n1,n8,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1221,c_0_824])]),
[final] ).
cnf(c_0_1292,plain,
~ p(n1,n9,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1222,c_0_824])]),
[final] ).
cnf(c_0_1293,plain,
~ p(n2,n7,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1223,c_0_960])]),
[final] ).
cnf(c_0_1294,plain,
~ p(n2,n8,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1224,c_0_895])]),
[final] ).
cnf(c_0_1295,plain,
~ p(n3,n7,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1225,c_0_828])]),
[final] ).
cnf(c_0_1296,plain,
~ p(n3,n8,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1226,c_0_895])]),
[final] ).
cnf(c_0_1298,plain,
~ p(n1,n7,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1227,c_0_820])]),
[final] ).
cnf(c_0_1299,plain,
~ p(n1,n8,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1228,c_0_820])]),
[final] ).
cnf(c_0_1300,plain,
~ p(n1,n9,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1229,c_0_820])]),
[final] ).
cnf(c_0_1315,plain,
~ p(n2,n4,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1246,c_0_960])]),
[final] ).
cnf(c_0_1316,plain,
~ p(n4,n4,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1247,c_0_864])]),
[final] ).
cnf(c_0_1317,plain,
~ p(n6,n4,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1248,c_0_966])]),
[final] ).
cnf(c_0_1318,plain,
~ p(n7,n4,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1249,c_0_868])]),
[final] ).
cnf(c_0_1319,plain,
~ p(n9,n4,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1250,c_0_901])]),
[final] ).
cnf(c_0_1322,plain,
~ p(n1,n2,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1258,c_0_1259])]),
[final] ).
cnf(c_0_1327,plain,
p(n4,n6,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_1263,c_0_1264]),c_0_1265]),c_0_1266]),c_0_1267]),c_0_1268]),c_0_1269]),c_0_1270]),c_0_1271]),
[final] ).
cnf(c_0_1349,plain,
~ p(n3,n4,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1284,c_0_824])]),
[final] ).
cnf(c_0_1350,plain,
~ p(n3,n2,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1285,c_0_1083])]),
[final] ).
cnf(c_0_1351,plain,
~ p(n3,n5,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1286,c_0_824])]),
[final] ).
cnf(c_0_1352,plain,
~ p(n3,n6,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1287,c_0_824])]),
[final] ).
cnf(c_0_1356,plain,
~ p(n2,n7,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1301,c_0_960])]),
[final] ).
cnf(c_0_1357,plain,
~ p(n2,n8,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1302,c_0_898])]),
[final] ).
cnf(c_0_1358,plain,
~ p(n3,n7,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1303,c_0_828])]),
[final] ).
cnf(c_0_1359,plain,
~ p(n3,n8,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1304,c_0_898])]),
[final] ).
cnf(c_0_1374,plain,
p(n1,n6,n5),
inference(sr,[status(thm)],[c_0_1321,c_0_1322]),
[final] ).
cnf(c_0_1377,plain,
~ p(n4,n4,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1324,c_0_864])]),
[final] ).
cnf(c_0_1378,plain,
~ p(n4,n5,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1325,c_0_1197])]),
[final] ).
cnf(c_0_1379,plain,
~ p(n4,n6,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1326,c_0_1327])]),
[final] ).
cnf(c_0_1380,plain,
~ p(n5,n4,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1328,c_0_953])]),
[final] ).
cnf(c_0_1381,plain,
~ p(n5,n5,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1329,c_0_953])]),
[final] ).
cnf(c_0_1382,plain,
~ p(n5,n6,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1330,c_0_953])]),
[final] ).
cnf(c_0_1383,plain,
~ p(n6,n5,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1331,c_0_966])]),
[final] ).
cnf(c_0_1384,plain,
~ p(n6,n6,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1332,c_0_826])]),
[final] ).
cnf(c_0_1404,plain,
~ p(n1,n3,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1341,c_0_822])]),
[final] ).
cnf(c_0_1405,plain,
~ p(n1,n1,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1342,c_0_820])]),
[final] ).
cnf(c_0_1406,plain,
~ p(n2,n1,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1343,c_0_1174])]),
[final] ).
cnf(c_0_1407,plain,
~ p(n2,n2,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1344,c_0_1174])]),
[final] ).
cnf(c_0_1408,plain,
~ p(n2,n3,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1345,c_0_1174])]),
[final] ).
cnf(c_0_1409,plain,
~ p(n3,n2,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1346,c_0_1083])]),
[final] ).
cnf(c_0_1428,plain,
~ p(n3,n4,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1373,c_0_1374])]),
[final] ).
cnf(c_0_1430,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_1376,c_0_1377]),c_0_1378]),c_0_1379]),c_0_1380]),c_0_1381]),c_0_1382]),c_0_1383]),c_0_1384]),
[final] ).
cnf(c_0_1464,plain,
~ p(n2,n1,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1415,c_0_960])]),
[final] ).
cnf(c_0_1465,plain,
~ p(n2,n2,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1416,c_0_960])]),
[final] ).
cnf(c_0_1466,plain,
~ p(n2,n3,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1417,c_0_960])]),
[final] ).
cnf(c_0_1467,plain,
~ p(n3,n2,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1418,c_0_1083])]),
[final] ).
cnf(c_0_1482,plain,
~ p(n6,n4,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1429,c_0_1430])]),
[final] ).
cnf(c_0_1489,plain,
~ p(n4,n4,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1435,c_0_864])]),
[final] ).
cnf(c_0_1490,plain,
~ p(n4,n5,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1436,c_0_1197])]),
[final] ).
cnf(c_0_1491,plain,
~ p(n4,n6,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1437,c_0_1327])]),
[final] ).
cnf(c_0_1492,plain,
~ p(n5,n4,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1438,c_0_868])]),
[final] ).
cnf(c_0_1493,plain,
~ p(n6,n4,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1439,c_0_868])]),
[final] ).
cnf(c_0_1494,plain,
~ p(n6,n5,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1440,c_0_966])]),
[final] ).
cnf(c_0_1495,plain,
~ p(n6,n6,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1441,c_0_826])]),
[final] ).
cnf(c_0_1533,plain,
~ p(n4,n4,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1474,c_0_864])]),
[final] ).
cnf(c_0_1534,plain,
~ p(n4,n5,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1475,c_0_1197])]),
[final] ).
cnf(c_0_1535,plain,
~ p(n4,n6,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1476,c_0_1327])]),
[final] ).
cnf(c_0_1536,plain,
~ p(n6,n5,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1477,c_0_966])]),
[final] ).
cnf(c_0_1537,plain,
~ p(n6,n6,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1478,c_0_826])]),
[final] ).
cnf(c_0_1540,plain,
p(n5,n4,n8),
inference(sr,[status(thm)],[c_0_1481,c_0_1482]),
[final] ).
cnf(c_0_1557,plain,
~ p(n7,n3,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1503,c_0_822])]),
[final] ).
cnf(c_0_1558,plain,
~ p(n7,n1,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1504,c_0_868])]),
[final] ).
cnf(c_0_1559,plain,
~ p(n7,n2,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1505,c_0_868])]),
[final] ).
cnf(c_0_1560,plain,
~ p(n8,n2,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1506,c_0_818])]),
[final] ).
cnf(c_0_1561,plain,
~ p(n8,n3,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1507,c_0_822])]),
[final] ).
cnf(c_0_1562,plain,
~ p(n9,n3,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1508,c_0_822])]),
[final] ).
cnf(c_0_1577,plain,
~ p(n1,n1,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1514,c_0_824])]),
[final] ).
cnf(c_0_1578,plain,
~ p(n1,n2,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1515,c_0_824])]),
[final] ).
cnf(c_0_1579,plain,
~ p(n1,n3,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1516,c_0_822])]),
[final] ).
cnf(c_0_1592,plain,
p(n4,n9,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1530,c_0_1191])]),
[final] ).
cnf(c_0_1596,plain,
~ p(n6,n4,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1538,c_0_1430])]),
[final] ).
cnf(c_0_1597,plain,
~ p(n5,n4,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1539,c_0_1540])]),
[final] ).
cnf(c_0_1600,plain,
~ p(n5,n7,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1541,c_0_828])]),
[final] ).
cnf(c_0_1601,plain,
~ p(n5,n7,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1542,c_0_895])]),
[final] ).
cnf(c_0_1602,plain,
~ p(n5,n7,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1543,c_0_953])]),
[final] ).
cnf(c_0_1615,plain,
~ p(n1,n7,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1550,c_0_822])]),
[final] ).
cnf(c_0_1616,plain,
~ p(n2,n7,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1551,c_0_960])]),
[final] ).
cnf(c_0_1617,plain,
~ p(n3,n7,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1552,c_0_828])]),
[final] ).
cnf(c_0_1618,plain,
~ p(n7,n7,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1553,c_0_868])]),
[final] ).
cnf(c_0_1619,plain,
~ p(n8,n7,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1554,c_0_1090])]),
[final] ).
cnf(c_0_1650,plain,
~ p(n4,n1,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1587,c_0_953])]),
[final] ).
cnf(c_0_1651,plain,
~ p(n4,n2,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1588,c_0_953])]),
[final] ).
cnf(c_0_1652,plain,
~ p(n4,n3,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1589,c_0_953])]),
[final] ).
cnf(c_0_1653,plain,
~ p(n4,n8,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1590,c_0_951])]),
[final] ).
cnf(c_0_1654,plain,
~ p(n4,n9,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1591,c_0_1592])]),
[final] ).
cnf(c_0_1660,plain,
~ p(n5,n7,n7),
inference(spm,[status(thm)],[c_0_1603,c_0_1604]),
[final] ).
cnf(c_0_1661,plain,
~ p(n5,n7,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1605,c_0_1540])]),
[final] ).
cnf(c_0_1697,plain,
~ p(n3,n8,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1631,c_0_1083])]),
[final] ).
cnf(c_0_1698,plain,
~ p(n4,n8,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1632,c_0_864])]),
[final] ).
cnf(c_0_1699,plain,
~ p(n7,n8,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1633,c_0_898])]),
[final] ).
cnf(c_0_1700,plain,
~ p(n8,n8,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1634,c_0_1090])]),
[final] ).
cnf(c_0_1701,plain,
~ p(n9,n8,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1635,c_0_1090])]),
[final] ).
cnf(c_0_1714,plain,
~ p(n1,n7,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1647,c_0_1090])]),
[final] ).
cnf(c_0_1716,plain,
p(n4,n7,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_1649,c_0_1650]),c_0_1651]),c_0_1652]),c_0_1377]),c_0_1378]),c_0_1379]),c_0_1653]),c_0_1654]),
[final] ).
cnf(c_0_1730,plain,
~ p(n4,n1,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1669,c_0_820])]),
[final] ).
cnf(c_0_1741,plain,
~ p(n1,n5,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1680,c_0_822])]),
[final] ).
cnf(c_0_1742,plain,
~ p(n7,n5,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1681,c_0_868])]),
[final] ).
cnf(c_0_1743,plain,
~ p(n8,n5,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1682,c_0_868])]),
[final] ).
cnf(c_0_1744,plain,
~ p(n9,n5,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1683,c_0_868])]),
[final] ).
cnf(c_0_1765,plain,
~ p(n4,n2,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1702,c_0_1083])]),
[final] ).
cnf(c_0_1766,plain,
~ p(n4,n1,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1703,c_0_864])]),
[final] ).
cnf(c_0_1767,plain,
~ p(n4,n3,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1704,c_0_864])]),
[final] ).
cnf(c_0_1768,plain,
~ p(n6,n2,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1705,c_0_1083])]),
[final] ).
cnf(c_0_1780,plain,
~ p(n1,n7,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1715,c_0_1716])]),
[final] ).
cnf(c_0_1781,plain,
~ p(n5,n7,n1),
inference(spm,[status(thm)],[c_0_1717,c_0_1718]),
[final] ).
cnf(c_0_1784,plain,
~ p(n7,n7,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1722,c_0_898])]),
[final] ).
cnf(c_0_1785,plain,
~ p(n8,n7,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1723,c_0_898])]),
[final] ).
cnf(c_0_1786,plain,
~ p(n9,n7,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1724,c_0_898])]),
[final] ).
cnf(c_0_1789,plain,
~ p(n4,n3,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1726,c_0_822])]),
[final] ).
cnf(c_0_1790,plain,
~ p(n4,n3,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1727,c_0_1197])]),
[final] ).
cnf(c_0_1793,plain,
~ p(n4,n1,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1731,c_0_1197])]),
[final] ).
cnf(c_0_1798,plain,
~ p(n4,n7,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1735,c_0_1716])]),
[final] ).
cnf(c_0_1806,plain,
~ p(n5,n6,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1745,c_0_1174])]),
[final] ).
cnf(c_0_1807,plain,
~ p(n5,n6,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1746,c_0_826])]),
[final] ).
cnf(c_0_1808,plain,
~ p(n5,n6,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1747,c_0_1197])]),
[final] ).
cnf(c_0_1841,plain,
~ p(n1,n7,n4),
inference(spm,[status(thm)],[c_0_1781,c_0_1782]),
[final] ).
cnf(c_0_1844,plain,
~ p(n4,n7,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1787,c_0_1716])]),
[final] ).
cnf(c_0_1848,plain,
~ p(n4,n3,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1791,c_0_1327])]),
[final] ).
cnf(c_0_1850,plain,
~ p(n4,n1,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1794,c_0_1327])]),
[final] ).
cnf(c_0_1857,plain,
~ p(n4,n7,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1800,c_0_895])]),
[final] ).
cnf(c_0_1858,plain,
~ p(n6,n7,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1801,c_0_895])]),
[final] ).
cnf(c_0_1859,plain,
~ p(n8,n7,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1802,c_0_1090])]),
[final] ).
cnf(c_0_1864,plain,
~ p(n1,n4,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1809,c_0_824])]),
[final] ).
cnf(c_0_1865,plain,
~ p(n1,n5,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1810,c_0_861])]),
[final] ).
cnf(c_0_1866,plain,
~ p(n2,n4,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1811,c_0_864])]),
[final] ).
cnf(c_0_1867,plain,
~ p(n2,n6,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1812,c_0_1174])]),
[final] ).
cnf(c_0_1868,plain,
~ p(n3,n4,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1813,c_0_1083])]),
[final] ).
cnf(c_0_1869,plain,
~ p(n3,n5,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1814,c_0_1083])]),
[final] ).
cnf(c_0_1870,plain,
~ p(n3,n6,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1815,c_0_1083])]),
[final] ).
cnf(c_0_1884,plain,
~ p(n1,n1,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1826,c_0_1083])]),
[final] ).
cnf(c_0_1885,plain,
~ p(n1,n2,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1827,c_0_1083])]),
[final] ).
cnf(c_0_1886,plain,
~ p(n1,n3,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1828,c_0_822])]),
[final] ).
cnf(c_0_1902,plain,
p(n1,n7,n8),
inference(sr,[status(thm)],[c_0_1840,c_0_1841]),
[final] ).
cnf(c_0_1922,plain,
~ p(n1,n6,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1871,c_0_1374])]),
[final] ).
cnf(c_0_1925,plain,
~ p(n1,n6,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1872,c_0_822])]),
[final] ).
cnf(c_0_1926,plain,
~ p(n2,n6,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1873,c_0_1174])]),
[final] ).
cnf(c_0_1927,plain,
~ p(n7,n6,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1874,c_0_868])]),
[final] ).
cnf(c_0_1928,plain,
~ p(n8,n6,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1875,c_0_868])]),
[final] ).
cnf(c_0_1929,plain,
~ p(n9,n6,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1876,c_0_868])]),
[final] ).
cnf(c_0_1944,plain,
~ p(n2,n4,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1889,c_0_824])]),
[final] ).
cnf(c_0_1945,plain,
~ p(n2,n4,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1890,c_0_868])]),
[final] ).
cnf(c_0_1960,plain,
~ p(n1,n2,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1901,c_0_1902])]),
[final] ).
cnf(c_0_1963,plain,
p(n6,n7,n1),
inference(sr,[status(thm)],[c_0_1904,c_0_1781]),
[final] ).
cnf(c_0_1972,plain,
~ p(n4,n1,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1912,c_0_1259])]),
[final] ).
cnf(c_0_1979,plain,
p(n2,n5,n2),
inference(sr,[status(thm)],[c_0_1921,c_0_1922]),
[final] ).
cnf(c_0_1999,plain,
~ p(n2,n4,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1946,c_0_1430])]),
[final] ).
cnf(c_0_2001,plain,
~ p(n2,n1,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1948,c_0_1012])]),
[final] ).
cnf(c_0_2009,plain,
~ p(n8,n4,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1954,c_0_824])]),
[final] ).
cnf(c_0_2010,plain,
~ p(n8,n2,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1955,c_0_818])]),
[final] ).
cnf(c_0_2011,plain,
~ p(n8,n6,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1956,c_0_1327])]),
[final] ).
cnf(c_0_2012,plain,
~ p(n8,n8,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1957,c_0_895])]),
[final] ).
cnf(c_0_2014,plain,
p(n2,n9,n1),
inference(sr,[status(thm)],[c_0_1959,c_0_1960]),
[final] ).
cnf(c_0_2016,plain,
~ p(n6,n7,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1962,c_0_1963])]),
[final] ).
cnf(c_0_2018,plain,
~ p(n8,n1,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1964,c_0_820])]),
[final] ).
cnf(c_0_2026,plain,
~ p(n4,n3,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1973,c_0_1259])]),
[final] ).
cnf(c_0_2032,plain,
~ p(n2,n5,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1978,c_0_1979])]),
[final] ).
cnf(c_0_2036,plain,
~ p(n1,n1,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1982,c_0_953])]),
[final] ).
cnf(c_0_2037,plain,
~ p(n1,n3,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1983,c_0_822])]),
[final] ).
cnf(c_0_2038,plain,
~ p(n1,n4,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1984,c_0_824])]),
[final] ).
cnf(c_0_2048,plain,
~ p(n2,n3,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1990,c_0_820])]),
[final] ).
cnf(c_0_2065,plain,
~ p(n1,n4,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2004,c_0_820])]),
[final] ).
cnf(c_0_2072,plain,
~ p(n2,n9,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2013,c_0_2014])]),
[final] ).
cnf(c_0_2074,plain,
p(n8,n1,n7),
inference(sr,[status(thm)],[c_0_1915,c_0_2016]),
[final] ).
cnf(c_0_2076,plain,
~ p(n8,n2,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2019,c_0_818])]),
[final] ).
cnf(c_0_2077,plain,
~ p(n8,n8,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2020,c_0_898])]),
[final] ).
cnf(c_0_2078,plain,
~ p(n8,n9,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2021,c_0_898])]),
[final] ).
cnf(c_0_2080,plain,
p(n8,n4,n5),
inference(sr,[status(thm)],[c_0_1372,c_0_1428]),
[final] ).
cnf(c_0_2083,plain,
~ p(n4,n1,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2027,c_0_1963])]),
[final] ).
cnf(c_0_2095,plain,
~ p(n1,n5,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2039,c_0_861])]),
[final] ).
cnf(c_0_2098,plain,
p(n1,n8,n2),
inference(sr,[status(thm)],[c_0_2042,c_0_1922]),
[final] ).
cnf(c_0_2106,plain,
~ p(n2,n3,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2049,c_0_822])]),
[final] ).
cnf(c_0_2107,plain,
~ p(n2,n3,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2050,c_0_1083])]),
[final] ).
cnf(c_0_2119,plain,
~ p(n7,n4,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2062,c_0_868])]),
[final] ).
cnf(c_0_2120,plain,
~ p(n9,n4,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2063,c_0_901])]),
[final] ).
cnf(c_0_2122,plain,
~ p(n7,n4,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2066,c_0_868])]),
[final] ).
cnf(c_0_2127,plain,
p(n3,n9,n6),
inference(sr,[status(thm)],[c_0_1354,c_0_2072]),
[final] ).
cnf(c_0_2128,plain,
~ p(n8,n1,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2073,c_0_2074])]),
[final] ).
cnf(c_0_2130,plain,
~ p(n8,n4,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2079,c_0_2080])]),
[final] ).
cnf(c_0_2132,plain,
p(n4,n3,n1),
inference(sr,[status(thm)],[c_0_2082,c_0_2083]),
[final] ).
cnf(c_0_2145,plain,
~ p(n1,n6,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2096,c_0_1374])]),
[final] ).
cnf(c_0_2146,plain,
~ p(n1,n8,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2097,c_0_2098])]),
[final] ).
cnf(c_0_2155,plain,
~ p(n2,n4,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2056,c_0_2014])]),
[final] ).
cnf(c_0_2158,plain,
~ p(n2,n2,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2109,c_0_820])]),
[final] ).
cnf(c_0_2168,plain,
~ p(n9,n4,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2123,c_0_901])]),
[final] ).
cnf(c_0_2176,plain,
~ p(n8,n3,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2131,c_0_2132])]),
[final] ).
cnf(c_0_2191,plain,
~ p(n1,n3,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2147,c_0_822])]),
[final] ).
cnf(c_0_2192,plain,
~ p(n1,n1,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2148,c_0_820])]),
[final] ).
cnf(c_0_2193,plain,
~ p(n1,n4,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2149,c_0_824])]),
[final] ).
cnf(c_0_2194,plain,
~ p(n1,n5,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2150,c_0_1197])]),
[final] ).
cnf(c_0_2200,plain,
~ p(n2,n3,n4),
inference(spm,[status(thm)],[c_0_2155,c_0_2156]),
[final] ).
cnf(c_0_2203,plain,
~ p(n2,n2,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2159,c_0_822])]),
[final] ).
cnf(c_0_2204,plain,
~ p(n2,n2,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2160,c_0_1083])]),
[final] ).
cnf(c_0_2205,plain,
~ p(n2,n2,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2161,c_0_818])]),
[final] ).
cnf(c_0_2221,plain,
~ p(n5,n1,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2171,c_0_953])]),
[final] ).
cnf(c_0_2231,plain,
~ p(n4,n2,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2184,c_0_1197])]),
[final] ).
cnf(c_0_2232,plain,
~ p(n5,n1,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2185,c_0_953])]),
[final] ).
cnf(c_0_2233,plain,
~ p(n5,n2,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2186,c_0_1259])]),
[final] ).
cnf(c_0_2234,plain,
~ p(n5,n3,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2187,c_0_1051])]),
[final] ).
cnf(c_0_2238,plain,
~ p(n1,n6,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2195,c_0_1374])]),
[final] ).
cnf(c_0_2239,plain,
~ p(n1,n8,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2196,c_0_2098])]),
[final] ).
cnf(c_0_2245,plain,
~ p(n2,n2,n4),
inference(spm,[status(thm)],[c_0_2206,c_0_2207]),
[final] ).
cnf(c_0_2264,plain,
p(n3,n1,n5),
inference(sr,[status(thm)],[c_0_2225,c_0_1960]),
[final] ).
cnf(c_0_2266,plain,
p(n7,n7,n6),
inference(spm,[status(thm)],[c_0_2227,c_0_2228]),
[final] ).
cnf(c_0_2295,plain,
~ p(n3,n4,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2258,c_0_868])]),
[final] ).
cnf(c_0_2300,plain,
~ p(n3,n1,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1776,c_0_2264])]),
[final] ).
cnf(c_0_2301,plain,
~ p(n7,n1,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2265,c_0_2266])]),
[final] ).
cnf(c_0_2312,plain,
~ p(n4,n6,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2279,c_0_864])]),
[final] ).
cnf(c_0_2313,plain,
~ p(n6,n6,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2280,c_0_864])]),
[final] ).
cnf(c_0_2314,plain,
~ p(n8,n6,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2281,c_0_1090])]),
[final] ).
cnf(c_0_2318,plain,
~ p(n6,n3,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2284,c_0_966])]),
[final] ).
cnf(c_0_2321,plain,
~ p(n8,n8,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2287,c_0_2080])]),
[final] ).
cnf(c_0_2324,plain,
~ p(n6,n8,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2289,c_0_895])]),
[final] ).
cnf(c_0_2325,plain,
~ p(n6,n9,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2290,c_0_895])]),
[final] ).
cnf(c_0_2350,plain,
~ p(n1,n2,n9),
inference(spm,[status(thm)],[c_0_2305,c_0_2306]),
[final] ).
cnf(c_0_2359,plain,
~ p(n3,n3,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2315,c_0_1083])]),
[final] ).
cnf(c_0_2360,plain,
~ p(n8,n3,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2316,c_0_1090])]),
[final] ).
cnf(c_0_2365,plain,
p(n9,n8,n5),
inference(sr,[status(thm)],[c_0_1019,c_0_2321]),
[final] ).
cnf(c_0_2392,plain,
~ p(n3,n4,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2342,c_0_1430])]),
[final] ).
cnf(c_0_2397,plain,
p(n1,n2,n4),
inference(sr,[status(thm)],[c_0_2349,c_0_2350]),
[final] ).
cnf(c_0_2399,plain,
~ p(n1,n2,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2351,c_0_820])]),
[final] ).
cnf(c_0_2400,plain,
~ p(n3,n2,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2352,c_0_820])]),
[final] ).
cnf(c_0_2410,plain,
~ p(n8,n3,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2363,c_0_2080])]),
[final] ).
cnf(c_0_2411,plain,
~ p(n9,n3,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2364,c_0_2365])]),
[final] ).
cnf(c_0_2447,plain,
~ p(n7,n2,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2401,c_0_898])]),
[final] ).
cnf(c_0_2461,plain,
~ p(n7,n2,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2415,c_0_1083])]),
[final] ).
cnf(c_0_2462,plain,
~ p(n7,n2,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2416,c_0_818])]),
[final] ).
cnf(c_0_2463,plain,
~ p(n7,n2,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2417,c_0_1259])]),
[final] ).
cnf(c_0_2475,plain,
~ p(n2,n9,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2426,c_0_828])]),
[final] ).
cnf(c_0_2476,plain,
~ p(n3,n9,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2427,c_0_828])]),
[final] ).
cnf(c_0_2477,plain,
~ p(n4,n9,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2428,c_0_951])]),
[final] ).
cnf(c_0_2478,plain,
~ p(n5,n9,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2429,c_0_951])]),
[final] ).
cnf(c_0_2479,plain,
~ p(n6,n9,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2430,c_0_826])]),
[final] ).
cnf(c_0_2480,plain,
~ p(n8,n9,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2431,c_0_818])]),
[final] ).
cnf(c_0_2481,plain,
~ p(n9,n9,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2432,c_0_901])]),
[final] ).
cnf(c_0_2487,plain,
~ p(n3,n6,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2436,c_0_828])]),
[final] ).
cnf(c_0_2488,plain,
~ p(n3,n6,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2437,c_0_1174])]),
[final] ).
cnf(c_0_2497,plain,
~ p(n5,n2,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2448,c_0_1259])]),
[final] ).
cnf(c_0_2500,plain,
p(n4,n1,n8),
inference(sr,[status(thm)],[c_0_2025,c_0_2083]),
[final] ).
cnf(c_0_2513,plain,
~ p(n7,n2,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2464,c_0_2266])]),
[final] ).
cnf(c_0_2514,plain,
~ p(n7,n2,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2465,c_0_2397])]),
[final] ).
cnf(c_0_2520,plain,
p(n1,n9,n9),
inference(sr,[status(thm)],[c_0_2236,c_0_2350]),
[final] ).
cnf(c_0_2526,plain,
p(n7,n9,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_2474,c_0_846]),c_0_2475]),c_0_2476]),c_0_2477]),c_0_2478]),c_0_2479]),c_0_2480]),c_0_2481]),
[final] ).
cnf(c_0_2529,plain,
~ p(n9,n6,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2483,c_0_1174])]),
[final] ).
cnf(c_0_2530,plain,
~ p(n9,n6,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2484,c_0_826])]),
[final] ).
cnf(c_0_2531,plain,
~ p(n9,n6,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2485,c_0_1327])]),
[final] ).
cnf(c_0_2533,plain,
~ p(n3,n6,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2489,c_0_1374])]),
[final] ).
cnf(c_0_2535,plain,
p(n2,n4,n4),
inference(sr,[status(thm)],[c_0_2059,c_0_2155]),
[final] ).
cnf(c_0_2537,plain,
p(n3,n4,n1),
inference(sr,[status(thm)],[c_0_2492,c_0_2155]),
[final] ).
cnf(c_0_2538,plain,
p(n3,n5,n7),
inference(spm,[status(thm)],[c_0_2493,c_0_2494]),
[final] ).
cnf(c_0_2541,plain,
~ p(n6,n2,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2498,c_0_1963])]),
[final] ).
cnf(c_0_2542,plain,
~ p(n4,n2,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2499,c_0_2500])]),
[final] ).
cnf(c_0_2552,plain,
p(n7,n3,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2509,c_0_2264])]),
[final] ).
cnf(c_0_2561,plain,
~ p(n4,n9,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2519,c_0_1197])]),
[final] ).
cnf(c_0_2562,plain,
~ p(n1,n9,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2235,c_0_2520])]),
[final] ).
cnf(c_0_2563,plain,
~ p(n2,n9,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2521,c_0_2014])]),
[final] ).
cnf(c_0_2564,plain,
~ p(n3,n9,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2522,c_0_2127])]),
[final] ).
cnf(c_0_2565,plain,
~ p(n5,n9,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2523,c_0_1191])]),
[final] ).
cnf(c_0_2566,plain,
~ p(n6,n9,n4),
inference(spm,[status(thm)],[c_0_1781,c_0_2524]),
[final] ).
cnf(c_0_2567,plain,
~ p(n7,n9,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2525,c_0_2526])]),
[final] ).
cnf(c_0_2571,plain,
~ p(n3,n6,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2534,c_0_2535])]),
[final] ).
cnf(c_0_2572,plain,
~ p(n3,n6,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2536,c_0_2537])]),
[final] ).
cnf(c_0_2573,plain,
~ p(n3,n6,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2179,c_0_2538])]),
[final] ).
cnf(c_0_2575,plain,
p(n9,n2,n1),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_2540,c_0_2541]),c_0_2542]),
[final] ).
cnf(c_0_2585,plain,
~ p(n7,n3,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2551,c_0_2552])]),
[final] ).
cnf(c_0_2589,plain,
~ p(n1,n8,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2556,c_0_822])]),
[final] ).
cnf(c_0_2590,plain,
~ p(n1,n9,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2557,c_0_822])]),
[final] ).
cnf(c_0_2595,plain,
p(n3,n6,n9),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_2570,c_0_2571]),c_0_2572]),c_0_2573]),
[final] ).
cnf(c_0_2596,plain,
~ p(n9,n6,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2574,c_0_2575])]),
[final] ).
cnf(c_0_2597,plain,
~ p(n9,n6,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2576,c_0_1374])]),
[final] ).
cnf(c_0_2600,plain,
~ p(n9,n2,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2578,c_0_1083])]),
[final] ).
cnf(c_0_2601,plain,
~ p(n9,n4,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2579,c_0_864])]),
[final] ).
cnf(c_0_2602,plain,
~ p(n9,n5,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2580,c_0_1979])]),
[final] ).
cnf(c_0_2603,plain,
~ p(n9,n7,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2581,c_0_1090])]),
[final] ).
cnf(c_0_2604,plain,
~ p(n9,n9,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2582,c_0_1090])]),
[final] ).
cnf(c_0_2612,plain,
~ p(n1,n4,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2591,c_0_822])]),
[final] ).
cnf(c_0_2634,plain,
~ p(n3,n1,n8),
inference(spm,[status(thm)],[c_0_2083,c_0_2622]),
[final] ).
cnf(c_0_2645,plain,
p(n3,n3,n8),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_1459,c_0_2634]),c_0_1960]),
[final] ).
cnf(c_0_2657,plain,
~ p(n8,n3,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2644,c_0_2645])]),
[final] ).
cnf(c_0_2690,plain,
~ p(n3,n2,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2677,c_0_1083])]),
[final] ).
cnf(c_0_2691,plain,
~ p(n5,n2,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2678,c_0_953])]),
[final] ).
cnf(c_0_2692,plain,
~ p(n6,n2,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2679,c_0_953])]),
[final] ).
cnf(c_0_2693,plain,
~ p(n8,n2,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2680,c_0_818])]),
[final] ).
cnf(c_0_2701,plain,
~ p(n5,n2,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2686,c_0_895])]),
[final] ).
cnf(c_0_2712,plain,
~ p(n4,n2,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2702,c_0_1327])]),
[final] ).
cnf(c_0_2716,plain,
p(n7,n2,n8),
inference(spm,[status(thm)],[c_0_2706,c_0_2619]),
[final] ).
cnf(c_0_2724,plain,
~ p(n7,n2,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2715,c_0_2716])]),
[final] ).
cnf(c_0_2729,plain,
p(n2,n8,n7),
inference(sr,[status(thm)],[c_0_2719,c_0_2032]),
[final] ).
cnf(c_0_2733,plain,
p(n2,n2,n9),
inference(sr,[status(thm)],[c_0_2723,c_0_2724]),
[final] ).
cnf(c_0_2737,plain,
~ p(n3,n8,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2728,c_0_2729])]),
[final] ).
cnf(c_0_2746,plain,
~ p(n2,n2,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2732,c_0_2733])]),
[final] ).
cnf(c_0_2760,plain,
p(n6,n2,n6),
inference(sr,[status(thm)],[c_0_2745,c_0_2746]),
[final] ).
cnf(c_0_2772,plain,
p(n5,n7,n4),
inference(sr,[status(thm)],[c_0_1720,c_0_1781]),
[final] ).
cnf(c_0_2776,plain,
~ p(n6,n1,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2759,c_0_2760])]),
[final] ).
cnf(c_0_2783,plain,
~ p(n5,n6,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2762,c_0_2538])]),
[final] ).
cnf(c_0_2787,plain,
~ p(n3,n8,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2764,c_0_1902])]),
[final] ).
cnf(c_0_2793,plain,
~ p(n9,n5,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2768,c_0_1197])]),
[final] ).
cnf(c_0_2794,plain,
~ p(n9,n2,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2769,c_0_2575])]),
[final] ).
cnf(c_0_2795,plain,
~ p(n9,n4,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2770,c_0_901])]),
[final] ).
cnf(c_0_2796,plain,
~ p(n9,n7,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2771,c_0_2772])]),
[final] ).
cnf(c_0_2797,plain,
~ p(n9,n8,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2773,c_0_2365])]),
[final] ).
cnf(c_0_2799,plain,
p(n9,n1,n6),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_2775,c_0_2301]),c_0_2300]),c_0_2776]),c_0_2128]),
[final] ).
cnf(c_0_2806,plain,
p(n5,n5,n1),
inference(sr,[status(thm)],[c_0_1657,c_0_2783]),
[final] ).
cnf(c_0_2820,plain,
~ p(n9,n1,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2798,c_0_2799])]),
[final] ).
cnf(c_0_2826,plain,
p(n8,n6,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2805,c_0_2806])]),
[final] ).
cnf(c_0_2829,plain,
p(n3,n8,n4),
inference(sr,[status(thm)],[c_0_2809,c_0_2350]),
[final] ).
cnf(c_0_2832,plain,
~ p(n2,n6,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2810,c_0_1174])]),
[final] ).
cnf(c_0_2833,plain,
~ p(n4,n6,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2811,c_0_1197])]),
[final] ).
cnf(c_0_2834,plain,
~ p(n6,n6,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2812,c_0_1197])]),
[final] ).
cnf(c_0_2850,plain,
~ p(n8,n5,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2821,c_0_1197])]),
[final] ).
cnf(c_0_2851,plain,
~ p(n8,n1,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2822,c_0_2074])]),
[final] ).
cnf(c_0_2852,plain,
~ p(n8,n2,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2823,c_0_818])]),
[final] ).
cnf(c_0_2853,plain,
~ p(n8,n4,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2824,c_0_2080])]),
[final] ).
cnf(c_0_2854,plain,
~ p(n8,n6,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2825,c_0_2826])]),
[final] ).
cnf(c_0_2855,plain,
~ p(n8,n7,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2827,c_0_1090])]),
[final] ).
cnf(c_0_2856,plain,
~ p(n8,n8,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2828,c_0_2829])]),
[final] ).
cnf(c_0_2902,plain,
~ p(n4,n8,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2869,c_0_951])]),
[final] ).
cnf(c_0_2906,plain,
~ p(n2,n1,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2872,c_0_1083])]),
[final] ).
cnf(c_0_2907,plain,
~ p(n2,n7,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2873,c_0_960])]),
[final] ).
cnf(c_0_2912,plain,
~ p(n5,n3,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2876,c_0_953])]),
[final] ).
cnf(c_0_2913,plain,
~ p(n6,n3,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2877,c_0_953])]),
[final] ).
cnf(c_0_2916,plain,
~ p(n9,n1,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2881,c_0_2799])]),
[final] ).
cnf(c_0_2931,plain,
~ p(n8,n1,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2894,c_0_1090])]),
[final] ).
cnf(c_0_2932,plain,
~ p(n8,n2,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2895,c_0_1083])]),
[final] ).
cnf(c_0_2948,plain,
~ p(n4,n9,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2903,c_0_1592])]),
[final] ).
cnf(c_0_2968,plain,
~ p(n2,n8,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2925,c_0_1174])]),
[final] ).
cnf(c_0_2969,plain,
~ p(n4,n8,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2926,c_0_951])]),
[final] ).
cnf(c_0_2970,plain,
~ p(n5,n8,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2927,c_0_895])]),
[final] ).
cnf(c_0_2971,plain,
~ p(n7,n8,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2928,c_0_898])]),
[final] ).
cnf(c_0_2977,plain,
~ p(n7,n6,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2933,c_0_1174])]),
[final] ).
cnf(c_0_2978,plain,
~ p(n8,n6,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2934,c_0_1174])]),
[final] ).
cnf(c_0_2982,plain,
p(n2,n3,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2937,c_0_2733])]),
[final] ).
cnf(c_0_3003,plain,
~ p(n2,n3,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2899,c_0_2733])]),
[final] ).
cnf(c_0_3004,plain,
~ p(n3,n3,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2958,c_0_2645])]),
[final] ).
cnf(c_0_3005,plain,
~ p(n7,n3,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2959,c_0_2552])]),
[final] ).
cnf(c_0_3008,plain,
~ p(n5,n8,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2961,c_0_953])]),
[final] ).
cnf(c_0_3009,plain,
~ p(n2,n8,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2962,c_0_2729])]),
[final] ).
cnf(c_0_3010,plain,
~ p(n3,n8,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2749,c_0_2520])]),
[final] ).
cnf(c_0_3011,plain,
~ p(n6,n8,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2963,c_0_1716])]),
[final] ).
cnf(c_0_3012,plain,
~ p(n7,n8,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2964,c_0_898])]),
[final] ).
cnf(c_0_3013,plain,
~ p(n9,n8,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2965,c_0_2365])]),
[final] ).
cnf(c_0_3021,plain,
~ p(n8,n4,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1312,c_0_2080])]),
[final] ).
cnf(c_0_3024,plain,
~ p(n8,n3,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2981,c_0_2982])]),
[final] ).
cnf(c_0_3032,plain,
~ p(n6,n3,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2989,c_0_822])]),
[final] ).
cnf(c_0_3052,plain,
p(n8,n8,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_3007,c_0_3008]),c_0_2146]),c_0_3009]),c_0_3010]),c_0_1653]),c_0_3011]),c_0_3012]),c_0_3013]),
[final] ).
cnf(c_0_3053,plain,
~ p(n6,n2,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2347,c_0_2397])]),
[final] ).
cnf(c_0_3067,plain,
~ p(n7,n5,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3022,c_0_2716])]),
[final] ).
cnf(c_0_3069,plain,
p(n8,n5,n6),
inference(sr,[status(thm)],[c_0_2174,c_0_3024]),
[final] ).
cnf(c_0_3075,plain,
~ p(n7,n5,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3025,c_0_1197])]),
[final] ).
cnf(c_0_3076,plain,
~ p(n7,n5,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3026,c_0_898])]),
[final] ).
cnf(c_0_3077,plain,
~ p(n7,n5,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3027,c_0_1979])]),
[final] ).
cnf(c_0_3078,plain,
~ p(n7,n5,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3028,c_0_861])]),
[final] ).
cnf(c_0_3079,plain,
~ p(n7,n5,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3029,c_0_966])]),
[final] ).
cnf(c_0_3080,plain,
~ p(n7,n5,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3030,c_0_2266])]),
[final] ).
cnf(c_0_3085,plain,
~ p(n6,n8,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3033,c_0_2729])]),
[final] ).
cnf(c_0_3089,plain,
p(n4,n2,n7),
inference(sr,[status(thm)],[c_0_3037,c_0_2083]),
[final] ).
cnf(c_0_3316,plain,
~ p(n8,n3,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3051,c_0_3052])]),
[final] ).
cnf(c_0_3319,plain,
~ p(n1,n8,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3055,c_0_2098])]),
[final] ).
cnf(c_0_3331,plain,
~ p(n8,n5,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3068,c_0_3069])]),
[final] ).
cnf(c_0_3341,plain,
~ p(n6,n1,n7),
inference(spm,[status(thm)],[c_0_3086,c_0_3087]),
[final] ).
cnf(c_0_3342,plain,
~ p(n6,n2,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3088,c_0_3089])]),
[final] ).
cnf(c_0_3565,plain,
~ p(n8,n2,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3311,c_0_818])]),
[final] ).
cnf(c_0_3566,plain,
~ p(n8,n7,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3312,c_0_1090])]),
[final] ).
cnf(c_0_3569,plain,
p(n8,n3,n4),
inference(sr,[status(thm)],[c_0_3315,c_0_3316]),
[final] ).
cnf(c_0_3575,plain,
p(n7,n6,n4),
inference(sr,[status(thm)],[c_0_3323,c_0_3316]),
[final] ).
cnf(c_0_3577,plain,
p(n7,n1,n2),
inference(sr,[status(thm)],[c_0_3325,c_0_3316]),
[final] ).
cnf(c_0_3579,plain,
~ p(n7,n6,n2),
inference(spm,[status(thm)],[c_0_3316,c_0_3327]),
[final] ).
cnf(c_0_3582,plain,
p(n9,n5,n8),
inference(sr,[status(thm)],[c_0_3330,c_0_3331]),
[final] ).
cnf(c_0_3587,plain,
p(n7,n5,n9),
inference(sr,[status(thm)],[c_0_3336,c_0_3067]),
[final] ).
cnf(c_0_3591,plain,
p(n6,n9,n7),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_3340,c_0_3341]),c_0_3342]),c_0_2016]),
[final] ).
cnf(c_0_3610,plain,
p(n9,n7,n7),
inference(sr,[status(thm)],[c_0_3361,c_0_2016]),
[final] ).
cnf(c_0_3813,plain,
~ p(n8,n1,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3567,c_0_2500])]),
[final] ).
cnf(c_0_3814,plain,
~ p(n8,n8,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3568,c_0_3052])]),
[final] ).
cnf(c_0_3815,plain,
~ p(n8,n9,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2667,c_0_3569])]),
[final] ).
cnf(c_0_3819,plain,
~ p(n6,n3,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3572,c_0_3569])]),
[final] ).
cnf(c_0_3820,plain,
~ p(n9,n3,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3573,c_0_3569])]),
[final] ).
cnf(c_0_3821,plain,
~ p(n9,n6,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3574,c_0_3575])]),
[final] ).
cnf(c_0_3822,plain,
~ p(n6,n1,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3576,c_0_3577])]),
[final] ).
cnf(c_0_3823,plain,
~ p(n9,n3,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3578,c_0_3577])]),
[final] ).
cnf(c_0_3824,plain,
~ p(n7,n1,n4),
inference(spm,[status(thm)],[c_0_3579,c_0_3580]),
[final] ).
cnf(c_0_3825,plain,
~ p(n9,n9,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3581,c_0_3582])]),
[final] ).
cnf(c_0_3826,plain,
~ p(n9,n5,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3583,c_0_3069])]),
[final] ).
cnf(c_0_3827,plain,
~ p(n6,n3,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3584,c_0_2982])]),
[final] ).
cnf(c_0_3828,plain,
~ p(n9,n3,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3585,c_0_2982])]),
[final] ).
cnf(c_0_3829,plain,
~ p(n8,n5,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3586,c_0_3587])]),
[final] ).
cnf(c_0_3830,plain,
~ p(n9,n5,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3588,c_0_3587])]),
[final] ).
cnf(c_0_3831,plain,
~ p(n7,n6,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3589,c_0_2595])]),
[final] ).
cnf(c_0_3832,plain,
~ p(n9,n6,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2568,c_0_2595])]),
[final] ).
cnf(c_0_3833,plain,
~ p(n6,n9,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3590,c_0_3591])]),
[final] ).
cnf(c_0_3834,plain,
~ p(n8,n6,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3592,c_0_2826])]),
[final] ).
cnf(c_0_3835,plain,
~ p(n8,n5,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2782,c_0_2806])]),
[final] ).
cnf(c_0_3836,plain,
~ p(n3,n5,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3593,c_0_2538])]),
[final] ).
cnf(c_0_3837,plain,
~ p(n5,n5,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2734,c_0_2538])]),
[final] ).
cnf(c_0_3838,plain,
~ p(n8,n9,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3594,c_0_2520])]),
[final] ).
cnf(c_0_3839,plain,
~ p(n9,n9,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3595,c_0_2520])]),
[final] ).
cnf(c_0_3840,plain,
~ p(n3,n5,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3596,c_0_2537])]),
[final] ).
cnf(c_0_3841,plain,
~ p(n3,n4,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3597,c_0_2535])]),
[final] ).
cnf(c_0_3842,plain,
~ p(n3,n9,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3598,c_0_2127])]),
[final] ).
cnf(c_0_3843,plain,
~ p(n3,n3,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3599,c_0_2645])]),
[final] ).
cnf(c_0_3844,plain,
~ p(n3,n3,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1458,c_0_2645])]),
[final] ).
cnf(c_0_3845,plain,
~ p(n9,n3,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3600,c_0_2645])]),
[final] ).
cnf(c_0_3846,plain,
~ p(n9,n2,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2720,c_0_2575])]),
[final] ).
cnf(c_0_3847,plain,
~ p(n9,n2,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3601,c_0_2575])]),
[final] ).
cnf(c_0_3848,plain,
~ p(n9,n2,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2703,c_0_2575])]),
[final] ).
cnf(c_0_3849,plain,
~ p(n9,n5,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3602,c_0_2575])]),
[final] ).
cnf(c_0_3850,plain,
~ p(n7,n3,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3603,c_0_2552])]),
[final] ).
cnf(c_0_3851,plain,
~ p(n7,n3,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3604,c_0_2552])]),
[final] ).
cnf(c_0_3852,plain,
~ p(n3,n1,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3605,c_0_2264])]),
[final] ).
cnf(c_0_3853,plain,
~ p(n3,n3,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2455,c_0_2264])]),
[final] ).
cnf(c_0_3854,plain,
~ p(n7,n1,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3606,c_0_2264])]),
[final] ).
cnf(c_0_3855,plain,
~ p(n2,n9,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3607,c_0_2014])]),
[final] ).
cnf(c_0_3856,plain,
~ p(n3,n9,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3608,c_0_2014])]),
[final] ).
cnf(c_0_3857,plain,
~ p(n8,n9,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3609,c_0_3610])]),
[final] ).
cnf(c_0_3858,plain,
~ p(n9,n1,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1672,c_0_3610])]),
[final] ).
cnf(c_0_3859,plain,
~ p(n9,n9,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3611,c_0_3610])]),
[final] ).
cnf(c_0_3860,plain,
~ p(n9,n2,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3612,c_0_3089])]),
[final] ).
cnf(c_0_3861,plain,
~ p(n9,n3,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3613,c_0_2132])]),
[final] ).
cnf(c_0_3862,plain,
~ p(n4,n2,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3614,c_0_2500])]),
[final] ).
cnf(c_0_3863,plain,
~ p(n4,n3,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1969,c_0_2500])]),
[final] ).
cnf(c_0_3864,plain,
~ p(n6,n1,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3615,c_0_2500])]),
[final] ).
cnf(c_0_3865,plain,
~ p(n6,n2,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3616,c_0_2500])]),
[final] ).
cnf(c_0_3866,plain,
~ p(n6,n3,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3617,c_0_2500])]),
[final] ).
cnf(c_0_3867,plain,
~ p(n9,n1,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3618,c_0_2500])]),
[final] ).
cnf(c_0_3868,plain,
~ p(n1,n9,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3619,c_0_1902])]),
[final] ).
cnf(c_0_3869,plain,
~ p(n3,n9,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3620,c_0_1902])]),
[final] ).
cnf(c_0_3870,plain,
~ p(n9,n7,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3621,c_0_1902])]),
[final] ).
cnf(c_0_3871,plain,
~ p(n7,n1,n8),
inference(spm,[status(thm)],[c_0_2083,c_0_3622]),
[final] ).
cnf(c_0_3872,plain,
~ p(n6,n3,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3623,c_0_1963])]),
[final] ).
cnf(c_0_3873,plain,
~ p(n6,n7,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3624,c_0_1963])]),
[final] ).
cnf(c_0_3874,plain,
~ p(n6,n9,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3625,c_0_1963])]),
[final] ).
cnf(c_0_3875,plain,
~ p(n6,n8,n4),
inference(spm,[status(thm)],[c_0_1781,c_0_3626]),
[final] ).
cnf(c_0_3876,plain,
~ p(n6,n7,n4),
inference(spm,[status(thm)],[c_0_1781,c_0_3627]),
[final] ).
cnf(c_0_3877,plain,
~ p(n7,n3,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3628,c_0_2266])]),
[final] ).
cnf(c_0_3878,plain,
~ p(n7,n7,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3629,c_0_2266])]),
[final] ).
cnf(c_0_3879,plain,
~ p(n7,n7,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3630,c_0_2266])]),
[final] ).
cnf(c_0_3880,plain,
~ p(n8,n9,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3631,c_0_2266])]),
[final] ).
cnf(c_0_3881,plain,
~ p(n9,n7,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3632,c_0_2266])]),
[final] ).
cnf(c_0_3882,plain,
~ p(n9,n9,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3633,c_0_2266])]),
[final] ).
cnf(c_0_3883,plain,
~ p(n5,n5,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3634,c_0_1540])]),
[final] ).
cnf(c_0_3884,plain,
~ p(n4,n7,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3635,c_0_1716])]),
[final] ).
cnf(c_0_3885,plain,
~ p(n6,n7,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3636,c_0_1716])]),
[final] ).
cnf(c_0_3886,plain,
~ p(n6,n9,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3637,c_0_1716])]),
[final] ).
cnf(c_0_3887,plain,
~ p(n7,n7,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3638,c_0_1716])]),
[final] ).
cnf(c_0_3888,plain,
~ p(n9,n7,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3639,c_0_1716])]),
[final] ).
cnf(c_0_3889,plain,
~ p(n2,n8,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3640,c_0_2729])]),
[final] ).
cnf(c_0_3890,plain,
~ p(n2,n9,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3641,c_0_2729])]),
[final] ).
cnf(c_0_3891,plain,
~ p(n3,n9,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3642,c_0_2729])]),
[final] ).
cnf(c_0_3892,plain,
~ p(n8,n8,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3643,c_0_2729])]),
[final] ).
cnf(c_0_3893,plain,
~ p(n9,n1,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3644,c_0_2365])]),
[final] ).
cnf(c_0_3894,plain,
~ p(n9,n8,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3645,c_0_2365])]),
[final] ).
cnf(c_0_3895,plain,
~ p(n9,n8,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3014,c_0_2365])]),
[final] ).
cnf(c_0_3896,plain,
~ p(n2,n5,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3646,c_0_1979])]),
[final] ).
cnf(c_0_3897,plain,
~ p(n2,n8,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3647,c_0_1979])]),
[final] ).
cnf(c_0_3898,plain,
~ p(n8,n1,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3648,c_0_2080])]),
[final] ).
cnf(c_0_3899,plain,
~ p(n8,n4,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2165,c_0_2080])]),
[final] ).
cnf(c_0_3900,plain,
~ p(n7,n6,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3649,c_0_1374])]),
[final] ).
cnf(c_0_3901,plain,
~ p(n8,n6,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3650,c_0_1374])]),
[final] ).
cnf(c_0_3902,plain,
~ p(n4,n9,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3651,c_0_1592])]),
[final] ).
cnf(c_0_3903,plain,
~ p(n4,n9,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3652,c_0_1592])]),
[final] ).
cnf(c_0_3904,plain,
~ p(n8,n9,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3653,c_0_1592])]),
[final] ).
cnf(c_0_3905,plain,
~ p(n9,n9,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3654,c_0_1592])]),
[final] ).
cnf(c_0_3906,plain,
~ p(n4,n2,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3655,c_0_1259])]),
[final] ).
cnf(c_0_3907,plain,
~ p(n5,n2,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3656,c_0_1259])]),
[final] ).
cnf(c_0_3908,plain,
~ p(n5,n2,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3657,c_0_1259])]),
[final] ).
cnf(c_0_3909,plain,
~ p(n9,n2,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3658,c_0_1259])]),
[final] ).
cnf(c_0_3910,plain,
~ p(n1,n9,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3659,c_0_1191])]),
[final] ).
cnf(c_0_3911,plain,
~ p(n2,n9,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3660,c_0_1191])]),
[final] ).
cnf(c_0_3912,plain,
~ p(n5,n9,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3661,c_0_1191])]),
[final] ).
cnf(c_0_3913,plain,
~ p(n5,n9,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1131,c_0_1191])]),
[final] ).
cnf(c_0_3914,plain,
~ p(n5,n9,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3662,c_0_1191])]),
[final] ).
cnf(c_0_3915,plain,
~ p(n5,n9,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3663,c_0_1191])]),
[final] ).
cnf(c_0_3916,plain,
~ p(n6,n8,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3664,c_0_1191])]),
[final] ).
cnf(c_0_3917,plain,
~ p(n6,n9,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3665,c_0_1191])]),
[final] ).
cnf(c_0_3918,plain,
~ p(n5,n3,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3666,c_0_1051])]),
[final] ).
cnf(c_0_3919,plain,
~ p(n5,n3,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3667,c_0_1051])]),
[final] ).
cnf(c_0_3920,plain,
~ p(n2,n1,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3668,c_0_1012])]),
[final] ).
cnf(c_0_3921,plain,
~ p(n2,n5,n1),
inference(spm,[status(thm)],[c_0_3669,c_0_3670]),
[final] ).
cnf(c_0_3922,plain,
~ p(n7,n9,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3671,c_0_2526])]),
[final] ).
cnf(c_0_3923,plain,
~ p(n7,n9,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3672,c_0_2526])]),
[final] ).
cnf(c_0_3924,plain,
~ p(n7,n6,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3673,c_0_1327])]),
[final] ).
cnf(c_0_3925,plain,
~ p(n7,n9,n6),
inference(spm,[status(thm)],[c_0_3674,c_0_3675]),
[final] ).
cnf(c_0_3926,plain,
~ p(n2,n5,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3676,c_0_861])]),
[final] ).
cnf(c_0_3927,plain,
~ p(n9,n5,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3677,c_0_861])]),
[final] ).
cnf(c_0_3928,plain,
~ p(n8,n9,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3678,c_0_1090])]),
[final] ).
cnf(c_0_3929,plain,
~ p(n8,n7,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3679,c_0_1090])]),
[final] ).
cnf(c_0_3930,plain,
~ p(n8,n5,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3680,c_0_1090])]),
[final] ).
cnf(c_0_3931,plain,
~ p(n9,n2,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3681,c_0_818])]),
[final] ).
cnf(c_0_3932,plain,
~ p(n8,n5,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3682,c_0_818])]),
[final] ).
cnf(c_0_3933,plain,
~ p(n8,n2,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3683,c_0_818])]),
[final] ).
cnf(c_0_3934,plain,
~ p(n7,n9,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3684,c_0_1090])]),
[final] ).
cnf(c_0_3935,plain,
~ p(n9,n9,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3685,c_0_898])]),
[final] ).
cnf(c_0_3936,plain,
~ p(n9,n8,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3686,c_0_898])]),
[final] ).
cnf(c_0_3937,plain,
~ p(n7,n9,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3687,c_0_898])]),
[final] ).
cnf(c_0_3938,plain,
~ p(n7,n8,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3688,c_0_898])]),
[final] ).
cnf(c_0_3939,plain,
~ p(n7,n7,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3689,c_0_1090])]),
[final] ).
cnf(c_0_3940,plain,
~ p(n7,n6,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3690,c_0_898])]),
[final] ).
cnf(c_0_3941,plain,
~ p(n9,n4,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3691,c_0_868])]),
[final] ).
cnf(c_0_3942,plain,
~ p(n8,n4,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3692,c_0_868])]),
[final] ).
cnf(c_0_3943,plain,
~ p(n7,n9,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3693,c_0_868])]),
[final] ).
cnf(c_0_3944,plain,
~ p(n7,n8,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3694,c_0_868])]),
[final] ).
cnf(c_0_3945,plain,
~ p(n7,n4,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3695,c_0_868])]),
[final] ).
cnf(c_0_3946,plain,
~ p(n7,n3,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3696,c_0_898])]),
[final] ).
cnf(c_0_3947,plain,
~ p(n6,n8,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3697,c_0_898])]),
[final] ).
cnf(c_0_3948,plain,
~ p(n6,n7,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3698,c_0_1090])]),
[final] ).
cnf(c_0_3949,plain,
~ p(n8,n6,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3699,c_0_826])]),
[final] ).
cnf(c_0_3950,plain,
~ p(n7,n6,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3700,c_0_826])]),
[final] ).
cnf(c_0_3951,plain,
~ p(n9,n5,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3701,c_0_966])]),
[final] ).
cnf(c_0_3952,plain,
~ p(n8,n5,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3702,c_0_966])]),
[final] ).
cnf(c_0_3953,plain,
~ p(n6,n6,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3703,c_0_966])]),
[final] ).
cnf(c_0_3954,plain,
~ p(n6,n5,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3704,c_0_966])]),
[final] ).
cnf(c_0_3955,plain,
~ p(n6,n5,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3705,c_0_966])]),
[final] ).
cnf(c_0_3956,plain,
~ p(n6,n2,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3706,c_0_966])]),
[final] ).
cnf(c_0_3957,plain,
~ p(n6,n2,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3707,c_0_826])]),
[final] ).
cnf(c_0_3958,plain,
~ p(n6,n1,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3708,c_0_966])]),
[final] ).
cnf(c_0_3959,plain,
~ p(n9,n8,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3709,c_0_895])]),
[final] ).
cnf(c_0_3960,plain,
~ p(n7,n8,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3710,c_0_895])]),
[final] ).
cnf(c_0_3961,plain,
~ p(n5,n9,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3711,c_0_895])]),
[final] ).
cnf(c_0_3962,plain,
~ p(n5,n8,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3712,c_0_895])]),
[final] ).
cnf(c_0_3963,plain,
~ p(n5,n8,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3713,c_0_895])]),
[final] ).
cnf(c_0_3964,plain,
~ p(n5,n8,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3714,c_0_895])]),
[final] ).
cnf(c_0_3965,plain,
~ p(n5,n5,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3715,c_0_826])]),
[final] ).
cnf(c_0_3966,plain,
~ p(n5,n3,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3716,c_0_895])]),
[final] ).
cnf(c_0_3967,plain,
~ p(n5,n2,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3717,c_0_818])]),
[final] ).
cnf(c_0_3968,plain,
~ p(n9,n1,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3718,c_0_953])]),
[final] ).
cnf(c_0_3969,plain,
~ p(n8,n1,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3719,c_0_953])]),
[final] ).
cnf(c_0_3970,plain,
~ p(n7,n1,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3720,c_0_953])]),
[final] ).
cnf(c_0_3971,plain,
~ p(n6,n1,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3721,c_0_953])]),
[final] ).
cnf(c_0_3972,plain,
~ p(n5,n9,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3722,c_0_953])]),
[final] ).
cnf(c_0_3973,plain,
~ p(n5,n1,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3723,c_0_953])]),
[final] ).
cnf(c_0_3974,plain,
~ p(n5,n1,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3724,c_0_953])]),
[final] ).
cnf(c_0_3975,plain,
~ p(n4,n9,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3725,c_0_895])]),
[final] ).
cnf(c_0_3976,plain,
~ p(n4,n8,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3726,c_0_895])]),
[final] ).
cnf(c_0_3977,plain,
~ p(n4,n8,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3727,c_0_898])]),
[final] ).
cnf(c_0_3978,plain,
~ p(n4,n6,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3728,c_0_966])]),
[final] ).
cnf(c_0_3979,plain,
~ p(n4,n6,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3729,c_0_826])]),
[final] ).
cnf(c_0_3980,plain,
~ p(n6,n5,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3730,c_0_1197])]),
[final] ).
cnf(c_0_3981,plain,
~ p(n6,n4,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3731,c_0_1197])]),
[final] ).
cnf(c_0_3982,plain,
~ p(n5,n5,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3732,c_0_1197])]),
[final] ).
cnf(c_0_3983,plain,
~ p(n5,n4,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3733,c_0_1197])]),
[final] ).
cnf(c_0_3984,plain,
~ p(n4,n8,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3734,c_0_1197])]),
[final] ).
cnf(c_0_3985,plain,
~ p(n4,n7,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3735,c_0_1197])]),
[final] ).
cnf(c_0_3986,plain,
~ p(n4,n5,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3736,c_0_1197])]),
[final] ).
cnf(c_0_3987,plain,
~ p(n4,n5,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3737,c_0_1197])]),
[final] ).
cnf(c_0_3988,plain,
~ p(n4,n5,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3738,c_0_1197])]),
[final] ).
cnf(c_0_3989,plain,
~ p(n8,n4,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3739,c_0_864])]),
[final] ).
cnf(c_0_3990,plain,
~ p(n7,n4,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3740,c_0_864])]),
[final] ).
cnf(c_0_3991,plain,
~ p(n6,n5,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3741,c_0_864])]),
[final] ).
cnf(c_0_3992,plain,
~ p(n6,n4,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3742,c_0_864])]),
[final] ).
cnf(c_0_3993,plain,
~ p(n4,n9,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3743,c_0_864])]),
[final] ).
cnf(c_0_3994,plain,
~ p(n4,n7,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3744,c_0_864])]),
[final] ).
cnf(c_0_3995,plain,
~ p(n4,n5,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3745,c_0_864])]),
[final] ).
cnf(c_0_3996,plain,
~ p(n4,n4,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3746,c_0_864])]),
[final] ).
cnf(c_0_3997,plain,
~ p(n4,n2,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3747,c_0_818])]),
[final] ).
cnf(c_0_3998,plain,
~ p(n9,n7,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3748,c_0_828])]),
[final] ).
cnf(c_0_3999,plain,
~ p(n8,n7,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3749,c_0_828])]),
[final] ).
cnf(c_0_4000,plain,
~ p(n7,n7,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3750,c_0_828])]),
[final] ).
cnf(c_0_4001,plain,
~ p(n6,n7,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3751,c_0_828])]),
[final] ).
cnf(c_0_4002,plain,
~ p(n4,n7,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3752,c_0_828])]),
[final] ).
cnf(c_0_4003,plain,
~ p(n3,n7,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3753,c_0_828])]),
[final] ).
cnf(c_0_4004,plain,
~ p(n3,n7,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3754,c_0_828])]),
[final] ).
cnf(c_0_4005,plain,
~ p(n3,n7,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3755,c_0_828])]),
[final] ).
cnf(c_0_4006,plain,
~ p(n3,n5,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3756,c_0_966])]),
[final] ).
cnf(c_0_4007,plain,
~ p(n3,n5,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3757,c_0_1197])]),
[final] ).
cnf(c_0_4008,plain,
~ p(n3,n5,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3758,c_0_828])]),
[final] ).
cnf(c_0_4009,plain,
~ p(n3,n9,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3759,c_0_1083])]),
[final] ).
cnf(c_0_4010,plain,
~ p(n3,n7,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3760,c_0_1083])]),
[final] ).
cnf(c_0_4011,plain,
~ p(n3,n2,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3761,c_0_1083])]),
[final] ).
cnf(c_0_4012,plain,
~ p(n3,n2,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3762,c_0_1083])]),
[final] ).
cnf(c_0_4013,plain,
~ p(n3,n1,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3763,c_0_953])]),
[final] ).
cnf(c_0_4014,plain,
~ p(n3,n1,n2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3764,c_0_1083])]),
[final] ).
cnf(c_0_4015,plain,
~ p(n9,n7,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3765,c_0_960])]),
[final] ).
cnf(c_0_4016,plain,
~ p(n8,n7,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3766,c_0_960])]),
[final] ).
cnf(c_0_4017,plain,
~ p(n7,n7,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3767,c_0_960])]),
[final] ).
cnf(c_0_4018,plain,
~ p(n6,n7,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3768,c_0_960])]),
[final] ).
cnf(c_0_4019,plain,
~ p(n4,n7,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3769,c_0_960])]),
[final] ).
cnf(c_0_4020,plain,
~ p(n3,n7,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3770,c_0_960])]),
[final] ).
cnf(c_0_4021,plain,
~ p(n2,n7,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3771,c_0_960])]),
[final] ).
cnf(c_0_4022,plain,
~ p(n2,n7,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3772,c_0_960])]),
[final] ).
cnf(c_0_4023,plain,
~ p(n2,n7,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3773,c_0_960])]),
[final] ).
cnf(c_0_4024,plain,
~ p(n6,n6,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3774,c_0_1174])]),
[final] ).
cnf(c_0_4025,plain,
~ p(n4,n6,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3775,c_0_1174])]),
[final] ).
cnf(c_0_4026,plain,
~ p(n3,n5,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3776,c_0_1174])]),
[final] ).
cnf(c_0_4027,plain,
~ p(n2,n9,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3777,c_0_1174])]),
[final] ).
cnf(c_0_4028,plain,
~ p(n2,n7,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3778,c_0_1174])]),
[final] ).
cnf(c_0_4029,plain,
~ p(n2,n6,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3779,c_0_1174])]),
[final] ).
cnf(c_0_4030,plain,
~ p(n2,n6,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3780,c_0_1174])]),
[final] ).
cnf(c_0_4031,plain,
~ p(n2,n6,n3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3781,c_0_1174])]),
[final] ).
cnf(c_0_4032,plain,
~ p(n2,n6,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3782,c_0_1174])]),
[final] ).
cnf(c_0_4033,plain,
~ p(n2,n5,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3783,c_0_1174])]),
[final] ).
cnf(c_0_4034,plain,
~ p(n2,n5,n5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3784,c_0_960])]),
[final] ).
cnf(c_0_4035,plain,
~ p(n2,n5,n4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3785,c_0_1197])]),
[final] ).
cnf(c_0_4036,plain,
~ p(n2,n1,n9),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3786,c_0_953])]),
[final] ).
cnf(c_0_4037,plain,
~ p(n1,n6,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3787,c_0_1174])]),
[final] ).
cnf(c_0_4038,plain,
~ p(n1,n5,n8),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3788,c_0_1174])]),
[final] ).
cnf(c_0_4039,plain,
~ p(n9,n4,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3789,c_0_824])]),
[final] ).
cnf(c_0_4040,plain,
~ p(n7,n4,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3790,c_0_824])]),
[final] ).
cnf(c_0_4041,plain,
~ p(n2,n6,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3791,c_0_824])]),
[final] ).
cnf(c_0_4042,plain,
~ p(n2,n5,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3792,c_0_824])]),
[final] ).
cnf(c_0_4043,plain,
~ p(n1,n6,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3793,c_0_824])]),
[final] ).
cnf(c_0_4044,plain,
~ p(n1,n5,n6),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3794,c_0_824])]),
[final] ).
cnf(c_0_4045,plain,
~ p(n5,n3,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3795,c_0_822])]),
[final] ).
cnf(c_0_4046,plain,
~ p(n3,n3,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3796,c_0_822])]),
[final] ).
cnf(c_0_4047,plain,
~ p(n3,n2,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3797,c_0_822])]),
[final] ).
cnf(c_0_4048,plain,
~ p(n3,n1,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3798,c_0_822])]),
[final] ).
cnf(c_0_4049,plain,
~ p(n2,n1,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3799,c_0_822])]),
[final] ).
cnf(c_0_4050,plain,
~ p(n1,n2,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3800,c_0_822])]),
[final] ).
cnf(c_0_4051,plain,
~ p(n1,n1,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3801,c_0_822])]),
[final] ).
cnf(c_0_4052,plain,
~ p(n9,n1,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3802,c_0_820])]),
[final] ).
cnf(c_0_4053,plain,
~ p(n7,n1,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3803,c_0_820])]),
[final] ).
cnf(c_0_4054,plain,
~ p(n6,n1,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3804,c_0_820])]),
[final] ).
cnf(c_0_4055,plain,
~ p(n5,n1,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3805,c_0_820])]),
[final] ).
cnf(c_0_4056,plain,
~ p(n3,n3,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3806,c_0_820])]),
[final] ).
cnf(c_0_4057,plain,
~ p(n3,n1,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3807,c_0_820])]),
[final] ).
cnf(c_0_4058,plain,
~ p(n2,n1,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3808,c_0_820])]),
[final] ).
cnf(c_0_4059,plain,
~ p(n1,n6,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3809,c_0_820])]),
[final] ).
cnf(c_0_4060,plain,
~ p(n1,n5,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3810,c_0_820])]),
[final] ).
cnf(c_0_4061,plain,
~ p(n1,n3,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3811,c_0_820])]),
[final] ).
cnf(c_0_4062,plain,
p(n8,n9,n8),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_3812,c_0_3021]),c_0_3813]),c_0_2657]),c_0_3331]),c_0_3814]),
[final] ).
cnf(c_0_4063,plain,
p(n9,n3,n9),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_2955,c_0_3005]),c_0_3003]),c_0_3004]),c_0_3316]),
[final] ).
cnf(c_0_4064,plain,
p(n9,n9,n4),
inference(sr,[status(thm)],[c_0_2593,c_0_3815]),
[final] ).
cnf(c_0_4065,plain,
p(n6,n1,n4),
inference(sr,[status(thm)],[c_0_3816,c_0_3579]),
[final] ).
cnf(c_0_4066,plain,
p(n6,n3,n2),
inference(sr,[status(thm)],[c_0_2606,c_0_3579]),
[final] ).
cnf(c_0_4067,plain,
p(n9,n6,n2),
inference(sr,[status(thm)],[c_0_3817,c_0_3579]),
[final] ).
cnf(c_0_4068,plain,
p(n6,n8,n8),
inference(sr,[status(thm)],[c_0_3818,c_0_3814]),
[final] ).
cnf(c_0_4069,plain,
p(n5,n6,n7),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2748,c_0_2538])]),
[final] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ069+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.08/0.37 % Computer : n008.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Mon Sep 21 03:50:00 UTC 2026
% 0.08/0.38 % CPUTime :
% 0.08/0.38 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.42 Running first-order theorem proving
% 0.08/0.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
% 3.17/1.60 % Version: 3.5.1
% 3.17/1.60 % Preprocessing class: FMLSSMSMSSSNFFN.
% 3.17/1.60 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 3.17/1.60 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S4d with 900s (3) cores
% 3.17/1.60 % Starting new_bool_3 with 600s (2) cores
% 3.17/1.60 % Starting new_bool_1 with 600s (2) cores
% 3.17/1.60 % Starting sh5l with 300s (1) cores
% 3.17/1.60 % new_bool_3 with pid 82945 completed with status 9
% 3.17/1.60 % new_bool_1 with pid 82946 completed with status 9
% 3.17/1.60 % sh5l with pid 82947 completed with status 9
% 3.17/1.60 % G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S4d with pid 82944 completed with status 1
% 3.17/1.60 % Result found by G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S4d
% 3.17/1.60 % Preprocessing class: FMLSSMSMSSSNFFN.
% 3.17/1.60 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 3.17/1.60 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S4d with 900s (3) cores
% 3.17/1.60 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 3.17/1.60 % No SInE strategy applied
% 3.17/1.60 % Search class: FGHNF-SMLM00-SFFFFFNN
% 3.17/1.60 % Scheduled 7 strats onto 3 cores with 900 seconds (900 total)
% 3.17/1.60 % Starting SubtermCWHack with 82s (1) cores
% 3.17/1.60 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S4d with 91s (1) cores
% 3.17/1.60 % Starting H----_011_C07_F1_PI_AE_SP_S0V with 82s (1) cores
% 3.17/1.60 % H----_011_C07_F1_PI_AE_SP_S0V with pid 82989 completed with status 1
% 3.17/1.60 % Result found by H----_011_C07_F1_PI_AE_SP_S0V
% 3.17/1.60 % Preprocessing class: FMLSSMSMSSSNFFN.
% 3.17/1.60 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 3.17/1.60 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S4d with 900s (3) cores
% 3.17/1.60 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 3.17/1.60 % No SInE strategy applied
% 3.17/1.60 % Search class: FGHNF-SMLM00-SFFFFFNN
% 3.17/1.60 % Scheduled 7 strats onto 3 cores with 900 seconds (900 total)
% 3.17/1.60 % Starting SubtermCWHack with 82s (1) cores
% 3.17/1.60 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S4d with 91s (1) cores
% 3.17/1.60 % Starting H----_011_C07_F1_PI_AE_SP_S0V with 82s (1) cores
% 3.17/1.60 % Preprocessing time : 0.039 s
% 3.17/1.60
% 3.17/1.60 % No proof found!
% 3.17/1.60 % SZS status Satisfiable
% 3.17/1.60 % SZS output start Saturation
% See solution above
% 3.17/1.60 % Parsed axioms : 10547
% 3.17/1.60 % Removed by relevancy pruning/SinE : 0
% 3.17/1.60 % Initial clauses : 10547
% 3.17/1.60 % Removed in clause preprocessing : 0
% 3.17/1.60 % Initial clauses in saturation : 10547
% 3.17/1.60 % Processed clauses : 15045
% 3.17/1.60 % ...of these trivial : 392
% 3.17/1.60 % ...subsumed : 6314
% 3.17/1.60 % ...remaining for further processing : 8339
% 3.17/1.60 % Other redundant clauses eliminated : 0
% 3.17/1.60 % Clauses deleted for lack of memory : 0
% 3.17/1.60 % Backward-subsumed : 5890
% 3.17/1.60 % Backward-rewritten : 922
% 3.17/1.60 % Generated clauses : 11755
% 3.17/1.60 % ...of the previous two non-redundant : 9892
% 3.17/1.60 % ...aggressively subsumed : 0
% 3.17/1.60 % Contextual simplify-reflections : 0
% 3.17/1.60 % Paramodulations : 10957
% 3.17/1.60 % Factorizations : 0
% 3.17/1.60 % NegExts : 0
% 3.17/1.60 % Equation resolutions : 0
% 3.17/1.60 % Disequality decompositions : 0
% 3.17/1.60 % Total rewrite steps : 1881
% 3.17/1.60 % ...of those cached : 1800
% 3.17/1.60 % Propositional unsat checks : 0
% 3.17/1.60 % Propositional check models : 0
% 3.17/1.60 % Propositional check unsatisfiable : 0
% 3.17/1.60 % Propositional clauses : 0
% 3.17/1.60 % Propositional clauses after purity: 0
% 3.17/1.60 % Propositional unsat core size : 0
% 3.17/1.60 % Propositional preprocessing time : 0.000
% 3.17/1.60 % Propositional encoding time : 0.000
% 3.17/1.60 % Propositional solver time : 0.000
% 3.17/1.60 % Success case prop preproc time : 0.000
% 3.17/1.60 % Success case prop encoding time : 0.000
% 3.17/1.60 % Success case prop solver time : 0.000
% 3.17/1.60 % Current number of processed clauses : 729
% 3.17/1.60 % Positive orientable unit clauses : 81
% 3.17/1.60 % Positive unorientable unit clauses: 0
% 3.17/1.60 % Negative unit clauses : 648
% 3.17/1.60 % Non-unit-clauses : 0
% 3.17/1.60 % Current number of unprocessed clauses: 0
% 3.17/1.60 % ...number of literals in the above : 0
% 3.17/1.60 % Current number of archived formulas : 0
% 3.17/1.60 % Current number of archived clauses : 7610
% 3.17/1.60 % Clause-clause subsumption calls (NU) : 2045228
% 3.17/1.60 % Rec. Clause-clause subsumption calls : 1417466
% 3.17/1.60 % Non-unit clause-clause subsumptions : 1687
% 3.17/1.60 % Unit Clause-clause subsumption calls : 305818
% 3.17/1.60 % Rewrite failures with RHS unbound : 0
% 3.17/1.60 % BW rewrite match attempts : 581
% 3.17/1.60 % BW rewrite match successes : 61
% 3.17/1.60 % Condensation attempts : 0
% 3.17/1.60 % Condensation successes : 0
% 3.17/1.60 % Termbank termtop insertions : 864569
% 3.17/1.60 % Search garbage collected termcells : 20415
% 3.17/1.60
% 3.17/1.60 % -------------------------------------------------
% 3.17/1.60 % User time : 0.972 s
% 3.17/1.60 % System time : 0.053 s
% 3.17/1.60 % Total time : 1.025 s
% 3.17/1.60 % Maximum resident set size: 21892 pages
% 3.17/1.60
% 3.17/1.60 % -------------------------------------------------
% 3.17/1.60 % User time : 2.774 s
% 3.17/1.60 % System time : 0.212 s
% 3.17/1.60 % Total time : 2.985 s
% 3.17/1.60 % Maximum resident set size: 9216 pages
% 3.17/1.60 % E exiting
%------------------------------------------------------------------------------